# HG changeset patch # User wenzelm # Date 1224097575 -7200 # Node ID b40800eef8a7b65660a449c0a11d6563d160c1c1 # Parent a79582c29bd5abd9b7d52fb172065ef106c54fc5 added sledgehammer etc.; diff -r a79582c29bd5 -r b40800eef8a7 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 15 19:43:11 2008 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 15 21:06:15 2008 +0200 @@ -775,6 +775,90 @@ *} +section {* Invoking automated reasoning tools -- The Sledgehammer *} + +text {* + Isabelle/HOL includes a generic \emph{ATP manager} that allows + external automated reasoning tools to crunch a pending goal. + Supported provers include E\footnote{\url{http://www.eprover.org}}, + SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire. + There is also a wrapper to invoke provers remotely via the + SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}} + web service. + + The problem passed to external provers consists of the goal together + with a smart selection of lemmas from the current theory context. + The result of a successful proof search is some source text that + usually reconstructs the proof within Isabelle, without requiring + external provers again. The Metis + prover\footnote{\url{http://www.gilith.com/software/metis/}} that is + integrated into Isabelle/HOL is being used here. + + In this mode of operation, heavy means of automated reasoning are + used as a strong relevance filter, while the main proof checking + works via explicit inferences going through the Isabelle kernel. + Moreover, rechecking Isabelle proof texts with already specified + auxiliary facts is much faster than performing fully automated + search over and over again. + + \begin{matharray}{rcl} + @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ + @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + @{method_def (HOL) metis} & : & \isarmeth \\ + \end{matharray} + + \begin{rail} + 'sledgehammer' (nameref *) + ; + + 'metis' thmrefs + ; + \end{rail} + + \begin{descr} + + \item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \ + prover\<^sub>n"}] invokes the specified automated theorem provers on + the first subgoal. Provers are run in parallel, the first + successful result is displayed, and the other attempts are + terminated. + + Provers are defined in the theory context, see also @{command (HOL) + print_atps}. If no provers are given as arguments to @{command + (HOL) sledgehammer}, the system refers to the default defined as + ``ATP provers'' preference by the user interface. + + There are additional preferences for timeout (default: 60 seconds), + and the maximum number of independent prover processes (default: 5); + excessive provers are automatically terminated. + + \item [@{command (HOL) print_atps}] prints the list of automated + theorem provers available to the @{command (HOL) sledgehammer} + command. + + \item [@{command (HOL) atp_info}] prints information about presently + running provers, including elapsed runtime, and the remaining time + until timeout. + + \item [@{command (HOL) atp_kill}] terminates all presently running + provers. + + \item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis + prover with the given facts. Metis is an automated proof tool of + medium strength, but is fully integrated into Isabelle/HOL, with + explicit inferences going through the kernel. Thus its results are + guaranteed to be ``correct by construction''. + + Note that all facts used with Metis need to be specified as explicit + arguments. There are no rule declarations as for other Isabelle + provers, like @{method blast} or @{method fast}. + + \end{descr} +*} + + section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *} text {* diff -r a79582c29bd5 -r b40800eef8a7 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 15 19:43:11 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 15 21:06:15 2008 +0200 @@ -782,6 +782,89 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle/HOL includes a generic \emph{ATP manager} that allows + external automated reasoning tools to crunch a pending goal. + Supported provers include E\footnote{\url{http://www.eprover.org}}, + SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire. + There is also a wrapper to invoke provers remotely via the + SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}} + web service. + + The problem passed to external provers consists of the goal together + with a smart selection of lemmas from the current theory context. + The result of a successful proof search is some source text that + usually reconstructs the proof within Isabelle, without requiring + external provers again. The Metis + prover\footnote{\url{http://www.gilith.com/software/metis/}} that is + integrated into Isabelle/HOL is being used here. + + In this mode of operation, heavy means of automated reasoning are + used as a strong relevance filter, while the main proof checking + works via explicit inferences going through the Isabelle kernel. + Moreover, rechecking Isabelle proof texts with already specified + auxiliary facts is much faster than performing fully automated + search over and over again. + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ + \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}} & : & \isarkeep{theory~|~proof} \\ + \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}} & : & \isarkeep{\cdot} \\ + \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}} & : & \isarkeep{\cdot} \\ + \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\ + \end{matharray} + + \begin{rail} + 'sledgehammer' (nameref *) + ; + + 'metis' thmrefs + ; + \end{rail} + + \begin{descr} + + \item [\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}] invokes the specified automated theorem provers on + the first subgoal. Provers are run in parallel, the first + successful result is displayed, and the other attempts are + terminated. + + 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 + ``ATP provers'' preference by the user interface. + + There are additional preferences for timeout (default: 60 seconds), + and the maximum number of independent prover processes (default: 5); + excessive provers are automatically terminated. + + \item [\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated + theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} + command. + + \item [\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently + running provers, including elapsed runtime, and the remaining time + until timeout. + + \item [\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running + provers. + + \item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis + prover with the given facts. Metis is an automated proof tool of + medium strength, but is fully integrated into Isabelle/HOL, with + explicit inferences going through the kernel. Thus its results are + guaranteed to be ``correct by construction''. + + Note that all facts used with Metis need to be specified as explicit + arguments. There are no rule declarations as for other Isabelle + provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}% } \isamarkuptrue%