--- a/doc-src/IsarRef/Thy/Generic.thy Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sun Jun 05 22:02:54 2011 +0200
@@ -582,7 +582,7 @@
section {* The Classical Reasoner \label{sec:classical} *}
-subsection {* Introduction *}
+subsection {* Basic concepts *}
text {* Although Isabelle is generic, many users will be working in
some extension of classical first-order logic. Isabelle/ZF is built
@@ -884,64 +884,31 @@
text {*
\begin{matharray}{rcl}
@{method_def blast} & : & @{text method} \\
+ @{method_def auto} & : & @{text method} \\
+ @{method_def force} & : & @{text method} \\
@{method_def fast} & : & @{text method} \\
@{method_def slow} & : & @{text method} \\
@{method_def best} & : & @{text method} \\
- @{method_def safe} & : & @{text method} \\
- @{method_def clarify} & : & @{text method} \\
- \end{matharray}
-
- @{rail "
- @@{method blast} @{syntax nat}? (@{syntax clamod} * )
- ;
- (@@{method fast} | @@{method slow} | @@{method best} | @@{method safe} | @@{method clarify})
- (@{syntax clamod} * )
- ;
-
- @{syntax_def clamod}:
- (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
- "}
-
- \begin{description}
-
- \item @{method blast} refers to the classical tableau prover (see
- @{ML blast_tac} in \cite{isabelle-ref}). The optional argument
- specifies a user-supplied search bound (default 20).
-
- \item @{method fast}, @{method slow}, @{method best}, @{method
- safe}, and @{method clarify} refer to the generic classical
- reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
- safe_tac}, and @{ML 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.
-*}
-
-
-subsection {* Combined automated methods \label{sec:clasimp} *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def auto} & : & @{text method} \\
- @{method_def force} & : & @{text method} \\
- @{method_def clarsimp} & : & @{text method} \\
@{method_def fastsimp} & : & @{text method} \\
@{method_def slowsimp} & : & @{text method} \\
@{method_def bestsimp} & : & @{text method} \\
\end{matharray}
@{rail "
+ @@{method blast} @{syntax nat}? (@{syntax clamod} * )
+ ;
@@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
;
- (@@{method force} | @@{method clarsimp} | @@{method fastsimp} | @@{method slowsimp} |
- @@{method bestsimp}) (@{syntax clasimpmod} * )
+ @@{method force} (@{syntax clasimpmod} * )
+ ;
+ (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )
;
-
+ (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
+ (@{syntax clasimpmod} * )
+ ;
+ @{syntax_def clamod}:
+ (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
+ ;
@{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
('cong' | 'split') (() | 'add' | 'del') |
'iff' (((() | 'add') '?'?) | 'del') |
@@ -950,19 +917,121 @@
\begin{description}
- \item @{method auto}, @{method force}, @{method clarsimp}, @{method
- fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access
- to Isabelle's combined simplification and classical reasoning
- tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
- 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 @{text simp}
- here.
+ \item @{method 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 @{method fastsimp}.
+
+ \item It does not perform higher-order unification, as needed by the
+ rule @{thm [source=false] rangeI} in HOL. There are often
+ alternatives to such rules, for example @{thm [source=false]
+ range_eqI}.
+
+ \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 @{method fast} but can
+ be slower. If @{method blast} fails or seems to be running forever,
+ try @{method 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, @{method blast} starts
+ with a bound of 0 and increases it successively to 20. In contrast,
+ @{text "(blast lim)"} tries to prove the goal using a search bound
+ of @{text "lim"}. Sometimes a slow proof using @{method blast} can
+ be made much faster by supplying the successful search bound to this
+ proof method instead.
+
+ \item @{method 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 @{method 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 @{method fast}, @{method best}, @{method slow} attempt to
+ prove the first subgoal using sequent-style reasoning as explained
+ before. Unlike @{method blast}, they construct proofs directly in
+ Isabelle.
- Facts provided by forward chaining are inserted into the goal before
- doing the search.
+ There is a difference in search strategy and back-tracking: @{method
+ fast} uses depth-first search and @{method best} uses best-first
+ search (guided by a heuristic function: normally the total size of
+ the proof state).
+
+ Method @{method slow} is like @{method 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.
+
+ \item @{method fastsimp}, @{method slowsimp}, @{method bestsimp} are
+ like @{method fast}, @{method slow}, @{method 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 @{text 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.
+*}
+
+
+subsection {* Semi-automated methods *}
+
+text {* 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}
+ @{method_def safe} & : & @{text method} \\
+ @{method_def clarify} & : & @{text method} \\
+ @{method_def clarsimp} & : & @{text method} \\
+ \end{matharray}
+
+ @{rail "
+ (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
+ ;
+ @@{method clarsimp} (@{syntax clasimpmod} * )
+ "}
+
+ \begin{description}
+
+ \item @{method safe} repeatedly performs safe steps on all subgoals.
+ It is deterministic, with at most one outcome.
+
+ \item @{method clarify} performs a series of safe steps as follows.
+
+ No splitting step is applied; for example, the subgoal @{text "A \<and>
+ B"} is left as a conjunction. Proof by assumption, Modus Ponens,
+ etc., may be performed provided they do not instantiate unknowns.
+ Assumptions of the form @{text "x = t"} may be eliminated. The safe
+ wrapper tactical is applied.
+
+ \item @{method clarsimp} acts like @{method 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}
*}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sun Jun 05 22:02:54 2011 +0200
@@ -520,9 +520,8 @@
automated termination proof by searching for a lexicographic
combination of size measures on the arguments of the function. The
method accepts the same arguments as the @{method auto} method,
- which it uses internally to prove local descents. The same context
- modifiers as for @{method auto} are accepted, see
- \secref{sec:clasimp}.
+ which it uses internally to prove local descents. The @{syntax
+ clasimpmod} modifiers are accepted (as for @{method auto}).
In case of failure, extensive information is printed, which can help
to analyse the situation (cf.\ \cite{isabelle-function}).
@@ -536,8 +535,8 @@
tried in order. The search for a termination proof uses SAT solving
internally.
- For local descent proofs, the same context modifiers as for @{method
- auto} are accepted, see \secref{sec:clasimp}.
+ For local descent proofs, the @{syntax clasimpmod} modifiers are
+ accepted (as for @{method auto}).
\end{description}
*}
@@ -647,9 +646,9 @@
results. The @{text recdef_simp}, @{text recdef_cong}, and @{text
recdef_wf} hints refer to auxiliary rules to be used in the internal
automated proof process of TFL. Additional @{syntax clasimpmod}
- declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
- context of the Simplifier (cf.\ \secref{sec:simplifier}) and
- Classical reasoner (cf.\ \secref{sec:classical}).
+ declarations may be given to tune the context of the Simplifier
+ (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
+ \secref{sec:classical}).
\item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
proof for leftover termination condition number @{text i} (default
--- 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}%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sun Jun 05 22:02:54 2011 +0200
@@ -759,9 +759,7 @@
automated termination proof by searching for a lexicographic
combination of size measures on the arguments of the function. The
method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
- which it uses internally to prove local descents. The same context
- modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
- \secref{sec:clasimp}.
+ which it uses internally to prove local descents. The \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}).
In case of failure, extensive information is printed, which can help
to analyse the situation (cf.\ \cite{isabelle-function}).
@@ -775,7 +773,8 @@
tried in order. The search for a termination proof uses SAT solving
internally.
- For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
+ For local descent proofs, the \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are
+ accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}).
\end{description}%
\end{isamarkuptext}%
@@ -955,9 +954,9 @@
TFL to recover from failed proof attempts, returning unfinished
results. The \isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}, \isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}, and \isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf} hints refer to auxiliary rules to be used in the internal
automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
- declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
- context of the Simplifier (cf.\ \secref{sec:simplifier}) and
- Classical reasoner (cf.\ \secref{sec:classical}).
+ declarations may be given to tune the context of the Simplifier
+ (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
+ \secref{sec:classical}).
\item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the
proof for leftover termination condition number \isa{i} (default
--- a/doc-src/Ref/classical.tex Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/Ref/classical.tex Sun Jun 05 22:02:54 2011 +0200
@@ -124,129 +124,28 @@
\section{The classical tactics}
-\index{classical reasoner!tactics} If installed, the classical module provides
-powerful theorem-proving tactics.
-
-
-\subsection{The tableau prover}
-The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
-coded directly in \ML. It then reconstructs the proof using Isabelle
-tactics. It is faster and more powerful than the other classical
-reasoning tactics, but has major limitations too.
-\begin{itemize}
-\item It does not use the wrapper tacticals described above, such as
- \ttindex{addss}.
-\item It does not perform higher-order unification, as needed by the rule {\tt
- rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives
- to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
-\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 {\small\tt Function Var's argument not a bound variable}.
-\item Its proof strategy is more general than \texttt{fast_tac}'s but can be
- slower. If \texttt{blast_tac} fails or seems to be running forever, try {\tt
- fast_tac} and the other tactics described below.
-\end{itemize}
-%
-\begin{ttbox}
-blast_tac : claset -> int -> tactic
-Blast.depth_tac : claset -> int -> int -> tactic
-Blast.trace : bool ref \hfill{\bf initially false}
-\end{ttbox}
-The two tactics differ on how they bound the number of unsafe steps used in a
-proof. While \texttt{blast_tac} starts with a bound of zero and increases it
-successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
-\begin{ttdescription}
-\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
- subgoal~$i$, increasing the search bound using iterative
- deepening~\cite{korf85}.
-
-\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
- to prove subgoal~$i$ using a search bound of $lim$. Sometimes a slow
- proof using \texttt{blast_tac} can be made much faster by supplying the
- successful search bound to this tactic instead.
-
-\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
- causes the tableau prover to print a trace of its search. At each step it
- displays the formula currently being examined and reports whether the branch
- has been closed, extended or split.
-\end{ttdescription}
-
-
-\subsection{Automatic tactics}\label{sec:automatic-tactics}
-\begin{ttbox}
-type clasimpset = claset * simpset;
-auto_tac : clasimpset -> tactic
-force_tac : clasimpset -> int -> tactic
-auto : unit -> unit
-force : int -> unit
-\end{ttbox}
-The automatic tactics attempt to prove goals using a combination of
-simplification and classical reasoning.
-\begin{ttdescription}
-\item[\ttindexbold{auto_tac $(cs,ss)$}] 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.
-(Unfortunately, attempting to prove the hard ones may take a long time.)
-\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$
-completely. It tries to apply all fancy tactics it knows about,
-performing a rather exhaustive search.
-\end{ttdescription}
-
\subsection{Semi-automatic tactics}
\begin{ttbox}
-clarify_tac : claset -> int -> tactic
clarify_step_tac : claset -> int -> tactic
-clarsimp_tac : clasimpset -> int -> tactic
\end{ttbox}
-Use these when the automatic tactics fail. They perform all the obvious
-logical inferences that do not split the subgoal. The result is a
-simpler subgoal that can be tackled by other means, such as by
-instantiating quantifiers yourself.
+
\begin{ttdescription}
-\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
-subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
performed provided they do not instantiate unknowns. Assumptions of the
form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
applied.
-\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
-also does simplification with the given simpset. Note that if the simpset
-includes a splitter for the premises, the subgoal may still be split.
\end{ttdescription}
\subsection{Other classical tactics}
\begin{ttbox}
-fast_tac : claset -> int -> tactic
-best_tac : claset -> int -> tactic
-slow_tac : claset -> int -> tactic
slow_best_tac : claset -> int -> tactic
\end{ttbox}
-These tactics attempt to prove a subgoal using sequent-style reasoning.
-Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their
-effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
-this subgoal or fail. The \texttt{slow_} versions conduct a broader
-search.%
-\footnote{They may, when backtracking from a failed proof attempt, undo even
- the step of proving a subgoal by assumption.}
-The best-first tactics are guided by a heuristic function: typically, the
-total size of the proof state. This function is supplied in the functor call
-that sets up the classical reasoner.
\begin{ttdescription}
-\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
-depth-first search to prove subgoal~$i$.
-
-\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
-best-first search to prove subgoal~$i$.
-
-\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
-depth-first search to prove subgoal~$i$.
-
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
best-first search to prove subgoal~$i$.
\end{ttdescription}
@@ -277,7 +176,6 @@
\subsection{Single-step tactics}
\begin{ttbox}
safe_step_tac : claset -> int -> tactic
-safe_tac : claset -> tactic
inst_step_tac : claset -> int -> tactic
step_tac : claset -> int -> tactic
slow_step_tac : claset -> int -> tactic
@@ -290,9 +188,6 @@
include proof by assumption or Modus Ponens (taking care not to instantiate
unknowns), or substitution.
-\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
-subgoals. It is deterministic, with at most one outcome.
-
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
but allows unknowns to be instantiated.