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