# HG changeset patch # User wenzelm # Date 1272449929 -7200 # Node ID 2f383885d8f8aea5f771029b5095a647895b3afe # Parent d37c6eed81171e83a30c57f7ed6c18cc7943afda removed material that is out of scope of this manual; diff -r d37c6eed8117 -r 2f383885d8f8 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 28 12:07:52 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 28 12:18:49 2010 +0200 @@ -897,98 +897,6 @@ *} -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>*"} & : & @{text "proof \"} \\ - @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \"} \\ - @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \"} \\ - @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \"} \\ - @{method_def (HOL) metis} & : & @{text method} \\ - \end{matharray} - - \begin{rail} - 'sledgehammer' ( nameref * ) - ; - 'atp\_messages' ('(' nat ')')? - ; - - 'metis' thmrefs - ; - \end{rail} - - \begin{description} - - \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 @{command (HOL) atp_messages} displays recent messages issued - by automated theorem provers. This allows to examine results that - might have got lost due to the asynchronous nature of default - @{command (HOL) sledgehammer} output. An optional message limit may - be specified (default 5). - - \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{description} -*} - - section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *} text {* diff -r d37c6eed8117 -r 2f383885d8f8 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 28 12:07:52 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 28 12:18:49 2010 +0200 @@ -915,98 +915,6 @@ \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}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\ - \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}} \\ - \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}} \\ - \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}} \\ - \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}} \\ - \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\ - \end{matharray} - - \begin{rail} - 'sledgehammer' ( nameref * ) - ; - 'atp\_messages' ('(' nat ')')? - ; - - 'metis' thmrefs - ; - \end{rail} - - \begin{description} - - \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{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued - by automated theorem provers. This allows to examine results that - might have got lost due to the asynchronous nature of default - \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may - be specified (default 5). - - \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{description}% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}% } \isamarkuptrue%