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 {*