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