--- a/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 22:02:54 2011 +0200
@@ -924,7 +924,7 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{Introduction%
+\isamarkupsubsection{Basic concepts%
}
\isamarkuptrue%
%
@@ -1318,11 +1318,14 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{method}{blast}\hypertarget{method.blast}{\hyperlink{method.blast}{\mbox{\isa{blast}}}} & : & \isa{method} \\
+ \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isa{method} \\
+ \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isa{method} \\
\indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isa{method} \\
\indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isa{method} \\
\indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isa{method} \\
- \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isa{method} \\
- \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isa{method} \\
+ \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
+ \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
+ \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
\end{matharray}
\begin{railoutput}
@@ -1337,23 +1340,51 @@
\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
\rail@endplus
\rail@end
-\rail@begin{5}{}
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{method.fast}{\mbox{\isa{fast}}}}[]
\rail@nextbar{1}
\rail@term{\hyperlink{method.slow}{\mbox{\isa{slow}}}}[]
\rail@nextbar{2}
\rail@term{\hyperlink{method.best}{\mbox{\isa{best}}}}[]
-\rail@nextbar{3}
-\rail@term{\hyperlink{method.safe}{\mbox{\isa{safe}}}}[]
-\rail@nextbar{4}
-\rail@term{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}}[]
\rail@endbar
\rail@plus
\rail@nextplus{1}
\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
\rail@endplus
\rail@end
+\rail@begin{3}{}
+\rail@bar
+\rail@term{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
+\rail@endplus
+\rail@end
\rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
\rail@bar
\rail@bar
@@ -1375,72 +1406,6 @@
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
-\end{railoutput}
-
-
- \begin{description}
-
- \item \hyperlink{method.blast}{\mbox{\isa{blast}}} refers to the classical tableau prover (see
- \verb|blast_tac| in \cite{isabelle-ref}). The optional argument
- specifies a user-supplied search bound (default 20).
-
- \item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.safe}{\mbox{\isa{safe}}}, and \hyperlink{method.clarify}{\mbox{\isa{clarify}}} refer to the generic classical
- reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite{isabelle-ref} for more
- information.
-
- \end{description}
-
- Any of the above methods support additional modifiers of the context
- of classical rules. Their semantics is analogous to the attributes
- given before. Facts provided by forward chaining are inserted into
- the goal before commencing proof search.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Combined automated methods \label{sec:clasimp}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{method}{auto}\hypertarget{method.auto}{\hyperlink{method.auto}{\mbox{\isa{auto}}}} & : & \isa{method} \\
- \indexdef{}{method}{force}\hypertarget{method.force}{\hyperlink{method.force}{\mbox{\isa{force}}}} & : & \isa{method} \\
- \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isa{method} \\
- \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
- \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
- \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{2}{}
-\rail@term{\hyperlink{method.auto}{\mbox{\isa{auto}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@endbar
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
-\rail@endplus
-\rail@end
-\rail@begin{5}{}
-\rail@bar
-\rail@term{\hyperlink{method.force}{\mbox{\isa{force}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}}[]
-\rail@nextbar{2}
-\rail@term{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}}[]
-\rail@nextbar{3}
-\rail@term{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}}[]
-\rail@nextbar{4}
-\rail@term{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}}[]
-\rail@endbar
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
-\rail@endplus
-\rail@end
\rail@begin{14}{\indexdef{}{syntax}{clasimpmod}\hypertarget{syntax.clasimpmod}{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}}
\rail@bar
\rail@term{\isa{simp}}[]
@@ -1505,17 +1470,137 @@
\begin{description}
- \item \hyperlink{method.auto}{\mbox{\isa{auto}}}, \hyperlink{method.force}{\mbox{\isa{force}}}, \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}, \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, and \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} provide access
- to Isabelle's combined simplification and classical reasoning
- tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
- added as wrapper, see \cite{isabelle-ref} for more information. The
- modifier arguments correspond to those given in
- \secref{sec:simplifier} and \secref{sec:classical}. Just note that
- the ones related to the Simplifier are prefixed by \isa{simp}
- here.
+ \item \hyperlink{method.blast}{\mbox{\isa{blast}}} is a separate classical tableau prover that
+ uses the same classical rule declarations as explained before.
+
+ Proof search is coded directly in ML using special data structures.
+ A successful proof is then reconstructed using regular Isabelle
+ inferences. It is faster and more powerful than the other classical
+ reasoning tools, but has major limitations too.
+
+ \begin{itemize}
+
+ \item It does not use the classical wrapper tacticals, such as the
+ integration with the Simplifier of \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}.
+
+ \item It does not perform higher-order unification, as needed by the
+ rule \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f} in HOL. There are often
+ alternatives to such rules, for example \isa{{\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f}.
+
+ \item Function variables may only be applied to parameters of the
+ subgoal. (This restriction arises because the prover does not use
+ higher-order unification.) If other function variables are present
+ then the prover will fail with the message \texttt{Function Var's
+ argument not a bound variable}.
+
+ \item Its proof strategy is more general than \hyperlink{method.fast}{\mbox{\isa{fast}}} but can
+ be slower. If \hyperlink{method.blast}{\mbox{\isa{blast}}} fails or seems to be running forever,
+ try \hyperlink{method.fast}{\mbox{\isa{fast}}} and the other proof tools described below.
+
+ \end{itemize}
+
+ The optional integer argument specifies a bound for the number of
+ unsafe steps used in a proof. By default, \hyperlink{method.blast}{\mbox{\isa{blast}}} starts
+ with a bound of 0 and increases it successively to 20. In contrast,
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}blast\ lim{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} tries to prove the goal using a search bound
+ of \isa{{\isaliteral{22}{\isachardoublequote}}lim{\isaliteral{22}{\isachardoublequote}}}. Sometimes a slow proof using \hyperlink{method.blast}{\mbox{\isa{blast}}} can
+ be made much faster by supplying the successful search bound to this
+ proof method instead.
+
+ \item \hyperlink{method.auto}{\mbox{\isa{auto}}} combines classical reasoning with
+ simplification. It is intended for situations where there are a lot
+ of mostly trivial subgoals; it proves all the easy ones, leaving the
+ ones it cannot prove. Occasionally, attempting to prove the hard
+ ones may take a long time.
+
+ %FIXME auto nat arguments
+
+ \item \hyperlink{method.force}{\mbox{\isa{force}}} is intended to prove the first subgoal
+ completely, using many fancy proof tools and performing a rather
+ exhaustive search. As a result, proof attempts may take rather long
+ or diverge easily.
+
+ \item \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}} attempt to
+ prove the first subgoal using sequent-style reasoning as explained
+ before. Unlike \hyperlink{method.blast}{\mbox{\isa{blast}}}, they construct proofs directly in
+ Isabelle.
+
+ There is a difference in search strategy and back-tracking: \hyperlink{method.fast}{\mbox{\isa{fast}}} uses depth-first search and \hyperlink{method.best}{\mbox{\isa{best}}} uses best-first
+ search (guided by a heuristic function: normally the total size of
+ the proof state).
+
+ Method \hyperlink{method.slow}{\mbox{\isa{slow}}} is like \hyperlink{method.fast}{\mbox{\isa{fast}}}, but conducts a broader
+ search: it may, when backtracking from a failed proof attempt, undo
+ even the step of proving a subgoal by assumption.
- Facts provided by forward chaining are inserted into the goal before
- doing the search.
+ \item \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are
+ like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
+ but use the Simplifier as additional wrapper.
+
+ \end{description}
+
+ Any of the above methods support additional modifiers of the context
+ of classical (and simplifier) rules, but the ones related to the
+ Simplifier are explicitly prefixed by \isa{simp} here. The
+ semantics of these ad-hoc rule declarations is analogous to the
+ attributes given before. Facts provided by forward chaining are
+ inserted into the goal before commencing proof search.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Semi-automated methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+These proof methods may help in situations when the
+ fully-automated tools fail. The result is a simpler subgoal that
+ can be tackled by other means, such as by manual instantiation of
+ quantifiers.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{method}{safe}\hypertarget{method.safe}{\hyperlink{method.safe}{\mbox{\isa{safe}}}} & : & \isa{method} \\
+ \indexdef{}{method}{clarify}\hypertarget{method.clarify}{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}} & : & \isa{method} \\
+ \indexdef{}{method}{clarsimp}\hypertarget{method.clarsimp}{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}} & : & \isa{method} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{2}{}
+\rail@bar
+\rail@term{\hyperlink{method.safe}{\mbox{\isa{safe}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.clarify}{\mbox{\isa{clarify}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}}}[]
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
+\rail@endplus
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
+ It is deterministic, with at most one outcome.
+
+ \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
+
+ No splitting step is applied; for example, the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction. Proof by assumption, Modus Ponens,
+ etc., may be performed provided they do not instantiate unknowns.
+ Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated. The safe
+ wrapper tactical is applied.
+
+ \item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
+ simplification. Note that if the Simplifier context includes a
+ splitter for the premises, the subgoal may still be split.
\end{description}%
\end{isamarkuptext}%