1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 28 12:07:52 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 28 12:18:49 2010 +0200
1.3 @@ -897,98 +897,6 @@
1.4 *}
1.5
1.6
1.7 -section {* Invoking automated reasoning tools --- The Sledgehammer *}
1.8 -
1.9 -text {*
1.10 - Isabelle/HOL includes a generic \emph{ATP manager} that allows
1.11 - external automated reasoning tools to crunch a pending goal.
1.12 - Supported provers include E\footnote{\url{http://www.eprover.org}},
1.13 - SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.
1.14 - There is also a wrapper to invoke provers remotely via the
1.15 - SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}
1.16 - web service.
1.17 -
1.18 - The problem passed to external provers consists of the goal together
1.19 - with a smart selection of lemmas from the current theory context.
1.20 - The result of a successful proof search is some source text that
1.21 - usually reconstructs the proof within Isabelle, without requiring
1.22 - external provers again. The Metis
1.23 - prover\footnote{\url{http://www.gilith.com/software/metis/}} that is
1.24 - integrated into Isabelle/HOL is being used here.
1.25 -
1.26 - In this mode of operation, heavy means of automated reasoning are
1.27 - used as a strong relevance filter, while the main proof checking
1.28 - works via explicit inferences going through the Isabelle kernel.
1.29 - Moreover, rechecking Isabelle proof texts with already specified
1.30 - auxiliary facts is much faster than performing fully automated
1.31 - search over and over again.
1.32 -
1.33 - \begin{matharray}{rcl}
1.34 - @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1.35 - @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1.36 - @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
1.37 - @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
1.38 - @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
1.39 - @{method_def (HOL) metis} & : & @{text method} \\
1.40 - \end{matharray}
1.41 -
1.42 - \begin{rail}
1.43 - 'sledgehammer' ( nameref * )
1.44 - ;
1.45 - 'atp\_messages' ('(' nat ')')?
1.46 - ;
1.47 -
1.48 - 'metis' thmrefs
1.49 - ;
1.50 - \end{rail}
1.51 -
1.52 - \begin{description}
1.53 -
1.54 - \item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> prover\<^sub>n"}
1.55 - invokes the specified automated theorem provers on the first
1.56 - subgoal. Provers are run in parallel, the first successful result
1.57 - is displayed, and the other attempts are terminated.
1.58 -
1.59 - Provers are defined in the theory context, see also @{command (HOL)
1.60 - print_atps}. If no provers are given as arguments to @{command
1.61 - (HOL) sledgehammer}, the system refers to the default defined as
1.62 - ``ATP provers'' preference by the user interface.
1.63 -
1.64 - There are additional preferences for timeout (default: 60 seconds),
1.65 - and the maximum number of independent prover processes (default: 5);
1.66 - excessive provers are automatically terminated.
1.67 -
1.68 - \item @{command (HOL) print_atps} prints the list of automated
1.69 - theorem provers available to the @{command (HOL) sledgehammer}
1.70 - command.
1.71 -
1.72 - \item @{command (HOL) atp_info} prints information about presently
1.73 - running provers, including elapsed runtime, and the remaining time
1.74 - until timeout.
1.75 -
1.76 - \item @{command (HOL) atp_kill} terminates all presently running
1.77 - provers.
1.78 -
1.79 - \item @{command (HOL) atp_messages} displays recent messages issued
1.80 - by automated theorem provers. This allows to examine results that
1.81 - might have got lost due to the asynchronous nature of default
1.82 - @{command (HOL) sledgehammer} output. An optional message limit may
1.83 - be specified (default 5).
1.84 -
1.85 - \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
1.86 - with the given facts. Metis is an automated proof tool of medium
1.87 - strength, but is fully integrated into Isabelle/HOL, with explicit
1.88 - inferences going through the kernel. Thus its results are
1.89 - guaranteed to be ``correct by construction''.
1.90 -
1.91 - Note that all facts used with Metis need to be specified as explicit
1.92 - arguments. There are no rule declarations as for other Isabelle
1.93 - provers, like @{method blast} or @{method fast}.
1.94 -
1.95 - \end{description}
1.96 -*}
1.97 -
1.98 -
1.99 section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
1.100
1.101 text {*
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 28 12:07:52 2010 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 28 12:18:49 2010 +0200
2.3 @@ -915,98 +915,6 @@
2.4 \end{isamarkuptext}%
2.5 \isamarkuptrue%
2.6 %
2.7 -\isamarkupsection{Invoking automated reasoning tools --- The Sledgehammer%
2.8 -}
2.9 -\isamarkuptrue%
2.10 -%
2.11 -\begin{isamarkuptext}%
2.12 -Isabelle/HOL includes a generic \emph{ATP manager} that allows
2.13 - external automated reasoning tools to crunch a pending goal.
2.14 - Supported provers include E\footnote{\url{http://www.eprover.org}},
2.15 - SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.
2.16 - There is also a wrapper to invoke provers remotely via the
2.17 - SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}
2.18 - web service.
2.19 -
2.20 - The problem passed to external provers consists of the goal together
2.21 - with a smart selection of lemmas from the current theory context.
2.22 - The result of a successful proof search is some source text that
2.23 - usually reconstructs the proof within Isabelle, without requiring
2.24 - external provers again. The Metis
2.25 - prover\footnote{\url{http://www.gilith.com/software/metis/}} that is
2.26 - integrated into Isabelle/HOL is being used here.
2.27 -
2.28 - In this mode of operation, heavy means of automated reasoning are
2.29 - used as a strong relevance filter, while the main proof checking
2.30 - works via explicit inferences going through the Isabelle kernel.
2.31 - Moreover, rechecking Isabelle proof texts with already specified
2.32 - auxiliary facts is much faster than performing fully automated
2.33 - search over and over again.
2.34 -
2.35 - \begin{matharray}{rcl}
2.36 - \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\
2.37 - \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
2.38 - \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
2.39 - \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
2.40 - \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
2.41 - \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
2.42 - \end{matharray}
2.43 -
2.44 - \begin{rail}
2.45 - 'sledgehammer' ( nameref * )
2.46 - ;
2.47 - 'atp\_messages' ('(' nat ')')?
2.48 - ;
2.49 -
2.50 - 'metis' thmrefs
2.51 - ;
2.52 - \end{rail}
2.53 -
2.54 - \begin{description}
2.55 -
2.56 - \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}
2.57 - invokes the specified automated theorem provers on the first
2.58 - subgoal. Provers are run in parallel, the first successful result
2.59 - is displayed, and the other attempts are terminated.
2.60 -
2.61 - Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}. If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as
2.62 - ``ATP provers'' preference by the user interface.
2.63 -
2.64 - There are additional preferences for timeout (default: 60 seconds),
2.65 - and the maximum number of independent prover processes (default: 5);
2.66 - excessive provers are automatically terminated.
2.67 -
2.68 - \item \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}} prints the list of automated
2.69 - theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}
2.70 - command.
2.71 -
2.72 - \item \hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}} prints information about presently
2.73 - running provers, including elapsed runtime, and the remaining time
2.74 - until timeout.
2.75 -
2.76 - \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
2.77 - provers.
2.78 -
2.79 - \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
2.80 - by automated theorem provers. This allows to examine results that
2.81 - might have got lost due to the asynchronous nature of default
2.82 - \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may
2.83 - be specified (default 5).
2.84 -
2.85 - \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
2.86 - with the given facts. Metis is an automated proof tool of medium
2.87 - strength, but is fully integrated into Isabelle/HOL, with explicit
2.88 - inferences going through the kernel. Thus its results are
2.89 - guaranteed to be ``correct by construction''.
2.90 -
2.91 - Note that all facts used with Metis need to be specified as explicit
2.92 - arguments. There are no rule declarations as for other Isabelle
2.93 - provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.
2.94 -
2.95 - \end{description}%
2.96 -\end{isamarkuptext}%
2.97 -\isamarkuptrue%
2.98 -%
2.99 \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
2.100 }
2.101 \isamarkuptrue%