added sledgehammer etc.;
authorwenzelm
Wed Oct 15 21:06:15 2008 +0200 (2008-10-15)
changeset 28603b40800eef8a7
parent 28602 a79582c29bd5
child 28604 f36496b73227
added sledgehammer etc.;
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Oct 15 19:43:11 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Oct 15 21:06:15 2008 +0200
     1.3 @@ -775,6 +775,90 @@
     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>*"} & : & \isarkeep{proof} \\
    1.35 +    @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
    1.36 +    @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
    1.37 +    @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
    1.38 +    @{method_def (HOL) metis} & : & \isarmeth \\
    1.39 +  \end{matharray}
    1.40 +
    1.41 +  \begin{rail}
    1.42 +  'sledgehammer' (nameref *)
    1.43 +  ;
    1.44 +
    1.45 +  'metis' thmrefs
    1.46 +  ;
    1.47 +  \end{rail}
    1.48 +
    1.49 +  \begin{descr}
    1.50 +
    1.51 +  \item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots>
    1.52 +  prover\<^sub>n"}] invokes the specified automated theorem provers on
    1.53 +  the first subgoal.  Provers are run in parallel, the first
    1.54 +  successful result is displayed, and the other attempts are
    1.55 +  terminated.
    1.56 +
    1.57 +  Provers are defined in the theory context, see also @{command (HOL)
    1.58 +  print_atps}.  If no provers are given as arguments to @{command
    1.59 +  (HOL) sledgehammer}, the system refers to the default defined as
    1.60 +  ``ATP provers'' preference by the user interface.
    1.61 +
    1.62 +  There are additional preferences for timeout (default: 60 seconds),
    1.63 +  and the maximum number of independent prover processes (default: 5);
    1.64 +  excessive provers are automatically terminated.
    1.65 +
    1.66 +  \item [@{command (HOL) print_atps}] prints the list of automated
    1.67 +  theorem provers available to the @{command (HOL) sledgehammer}
    1.68 +  command.
    1.69 +
    1.70 +  \item [@{command (HOL) atp_info}] prints information about presently
    1.71 +  running provers, including elapsed runtime, and the remaining time
    1.72 +  until timeout.
    1.73 +
    1.74 +  \item [@{command (HOL) atp_kill}] terminates all presently running
    1.75 +  provers.
    1.76 +
    1.77 +  \item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis
    1.78 +  prover with the given facts.  Metis is an automated proof tool of
    1.79 +  medium strength, but is fully integrated into Isabelle/HOL, with
    1.80 +  explicit inferences going through the kernel.  Thus its results are
    1.81 +  guaranteed to be ``correct by construction''.
    1.82 +
    1.83 +  Note that all facts used with Metis need to be specified as explicit
    1.84 +  arguments.  There are no rule declarations as for other Isabelle
    1.85 +  provers, like @{method blast} or @{method fast}.
    1.86 +
    1.87 +  \end{descr}
    1.88 +*}
    1.89 +
    1.90 +
    1.91  section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *}
    1.92  
    1.93  text {*
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Oct 15 19:43:11 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Oct 15 21:06:15 2008 +0200
     2.3 @@ -782,6 +782,89 @@
     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}} & : & \isarkeep{proof} \\
    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}} & : & \isarkeep{theory~|~proof} \\
    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}} & : & \isarkeep{\cdot} \\
    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}} & : & \isarkeep{\cdot} \\
    2.40 +    \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\
    2.41 +  \end{matharray}
    2.42 +
    2.43 +  \begin{rail}
    2.44 +  'sledgehammer' (nameref *)
    2.45 +  ;
    2.46 +
    2.47 +  'metis' thmrefs
    2.48 +  ;
    2.49 +  \end{rail}
    2.50 +
    2.51 +  \begin{descr}
    2.52 +
    2.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
    2.54 +  the first subgoal.  Provers are run in parallel, the first
    2.55 +  successful result is displayed, and the other attempts are
    2.56 +  terminated.
    2.57 +
    2.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
    2.59 +  ``ATP provers'' preference by the user interface.
    2.60 +
    2.61 +  There are additional preferences for timeout (default: 60 seconds),
    2.62 +  and the maximum number of independent prover processes (default: 5);
    2.63 +  excessive provers are automatically terminated.
    2.64 +
    2.65 +  \item [\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated
    2.66 +  theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}
    2.67 +  command.
    2.68 +
    2.69 +  \item [\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently
    2.70 +  running provers, including elapsed runtime, and the remaining time
    2.71 +  until timeout.
    2.72 +
    2.73 +  \item [\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running
    2.74 +  provers.
    2.75 +
    2.76 +  \item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis
    2.77 +  prover with the given facts.  Metis is an automated proof tool of
    2.78 +  medium strength, but is fully integrated into Isabelle/HOL, with
    2.79 +  explicit inferences going through the kernel.  Thus its results are
    2.80 +  guaranteed to be ``correct by construction''.
    2.81 +
    2.82 +  Note that all facts used with Metis need to be specified as explicit
    2.83 +  arguments.  There are no rule declarations as for other Isabelle
    2.84 +  provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.
    2.85 +
    2.86 +  \end{descr}%
    2.87 +\end{isamarkuptext}%
    2.88 +\isamarkuptrue%
    2.89 +%
    2.90  \isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}%
    2.91  }
    2.92  \isamarkuptrue%