removed material that is out of scope of this manual;
authorwenzelm
Wed Apr 28 12:18:49 2010 +0200 (2010-04-28)
changeset 364532f383885d8f8
parent 36452 d37c6eed8117
child 36454 f2b5bcc61a8c
removed material that is out of scope of this manual;
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 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 {*
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Apr 28 12:07:52 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Apr 28 12:18:49 2010 +0200
     2.3 @@ -915,98 +915,6 @@
     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}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\
    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}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    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}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
    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}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
    2.40 -    \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
    2.41 -    \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
    2.42 -  \end{matharray}
    2.43 -
    2.44 -  \begin{rail}
    2.45 -  'sledgehammer' ( nameref * )
    2.46 -  ;
    2.47 -  'atp\_messages' ('(' nat ')')?
    2.48 -  ;
    2.49 -
    2.50 -  'metis' thmrefs
    2.51 -  ;
    2.52 -  \end{rail}
    2.53 -
    2.54 -  \begin{description}
    2.55 -
    2.56 -  \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}
    2.57 -  invokes the specified automated theorem provers on the first
    2.58 -  subgoal.  Provers are run in parallel, the first successful result
    2.59 -  is displayed, and the other attempts are terminated.
    2.60 -
    2.61 -  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.62 -  ``ATP provers'' preference by the user interface.
    2.63 -
    2.64 -  There are additional preferences for timeout (default: 60 seconds),
    2.65 -  and the maximum number of independent prover processes (default: 5);
    2.66 -  excessive provers are automatically terminated.
    2.67 -
    2.68 -  \item \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}} prints the list of automated
    2.69 -  theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}
    2.70 -  command.
    2.71 -
    2.72 -  \item \hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}} prints information about presently
    2.73 -  running provers, including elapsed runtime, and the remaining time
    2.74 -  until timeout.
    2.75 -
    2.76 -  \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
    2.77 -  provers.
    2.78 -
    2.79 -  \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
    2.80 -  by automated theorem provers.  This allows to examine results that
    2.81 -  might have got lost due to the asynchronous nature of default
    2.82 -  \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.  An optional message limit may
    2.83 -  be specified (default 5).
    2.84 -
    2.85 -  \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
    2.86 -  with the given facts.  Metis is an automated proof tool of medium
    2.87 -  strength, but is fully integrated into Isabelle/HOL, with explicit
    2.88 -  inferences going through the kernel.  Thus its results are
    2.89 -  guaranteed to be ``correct by construction''.
    2.90 -
    2.91 -  Note that all facts used with Metis need to be specified as explicit
    2.92 -  arguments.  There are no rule declarations as for other Isabelle
    2.93 -  provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.
    2.94 -
    2.95 -  \end{description}%
    2.96 -\end{isamarkuptext}%
    2.97 -\isamarkuptrue%
    2.98 -%
    2.99  \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
   2.100  }
   2.101  \isamarkuptrue%