# HG changeset patch # User wenzelm # Date 1307304174 -7200 # Node ID 41394a61cca9ebb4cdd2df56c3895eafe72a8058 # Parent 7f9d7b55ea9059f18dc428d9a4d8524d70a3f41b updated and re-unified classical proof methods; tuned; diff -r 7f9d7b55ea90 -r 41394a61cca9 doc-src/IsarRef/Thy/Generic.thy --- 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 \ + 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} *} diff -r 7f9d7b55ea90 -r 41394a61cca9 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 diff -r 7f9d7b55ea90 -r 41394a61cca9 doc-src/IsarRef/Thy/document/Generic.tex --- 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}% diff -r 7f9d7b55ea90 -r 41394a61cca9 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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 diff -r 7f9d7b55ea90 -r 41394a61cca9 doc-src/Ref/classical.tex --- 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.