1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 15 19:43:11 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 15 21:06:15 2008 +0200
1.3 @@ -782,6 +782,89 @@
1.4 \end{isamarkuptext}%
1.5 \isamarkuptrue%
1.6 %
1.7 +\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
1.8 +}
1.9 +\isamarkuptrue%
1.10 +%
1.11 +\begin{isamarkuptext}%
1.12 +Isabelle/HOL includes a generic \emph{ATP manager} that allows
1.13 + external automated reasoning tools to crunch a pending goal.
1.14 + Supported provers include E\footnote{\url{http://www.eprover.org}},
1.15 + SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.
1.16 + There is also a wrapper to invoke provers remotely via the
1.17 + SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}
1.18 + web service.
1.19 +
1.20 + The problem passed to external provers consists of the goal together
1.21 + with a smart selection of lemmas from the current theory context.
1.22 + The result of a successful proof search is some source text that
1.23 + usually reconstructs the proof within Isabelle, without requiring
1.24 + external provers again. The Metis
1.25 + prover\footnote{\url{http://www.gilith.com/software/metis/}} that is
1.26 + integrated into Isabelle/HOL is being used here.
1.27 +
1.28 + In this mode of operation, heavy means of automated reasoning are
1.29 + used as a strong relevance filter, while the main proof checking
1.30 + works via explicit inferences going through the Isabelle kernel.
1.31 + Moreover, rechecking Isabelle proof texts with already specified
1.32 + auxiliary facts is much faster than performing fully automated
1.33 + search over and over again.
1.34 +
1.35 + \begin{matharray}{rcl}
1.36 + \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
1.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}} & : & \isarkeep{theory~|~proof} \\
1.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}} & : & \isarkeep{\cdot} \\
1.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}} & : & \isarkeep{\cdot} \\
1.40 + \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\
1.41 + \end{matharray}
1.42 +
1.43 + \begin{rail}
1.44 + 'sledgehammer' (nameref *)
1.45 + ;
1.46 +
1.47 + 'metis' thmrefs
1.48 + ;
1.49 + \end{rail}
1.50 +
1.51 + \begin{descr}
1.52 +
1.53 + \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
1.54 + the first subgoal. Provers are run in parallel, the first
1.55 + successful result is displayed, and the other attempts are
1.56 + terminated.
1.57 +
1.58 + 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
1.59 + ``ATP provers'' preference by the user interface.
1.60 +
1.61 + There are additional preferences for timeout (default: 60 seconds),
1.62 + and the maximum number of independent prover processes (default: 5);
1.63 + excessive provers are automatically terminated.
1.64 +
1.65 + \item [\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated
1.66 + theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}
1.67 + command.
1.68 +
1.69 + \item [\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently
1.70 + running provers, including elapsed runtime, and the remaining time
1.71 + until timeout.
1.72 +
1.73 + \item [\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running
1.74 + provers.
1.75 +
1.76 + \item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis
1.77 + prover with the given facts. Metis is an automated proof tool of
1.78 + medium strength, but is fully integrated into Isabelle/HOL, with
1.79 + explicit inferences going through the kernel. Thus its results are
1.80 + guaranteed to be ``correct by construction''.
1.81 +
1.82 + Note that all facts used with Metis need to be specified as explicit
1.83 + arguments. There are no rule declarations as for other Isabelle
1.84 + provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.
1.85 +
1.86 + \end{descr}%
1.87 +\end{isamarkuptext}%
1.88 +\isamarkuptrue%
1.89 +%
1.90 \isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}%
1.91 }
1.92 \isamarkuptrue%