# HG changeset patch # User paulson # Date 864048161 -7200 # Node ID 4ea2aa9f93a51dba89332ff3ab0e9c70a0f771d1 # Parent 49f1a09576c23f1840e448c8ceab37695883c759 Documented auto_tac diff -r 49f1a09576c2 -r 4ea2aa9f93a5 doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Mon May 19 15:22:21 1997 +0200 +++ b/doc-src/Ref/classical.tex Mon May 19 15:22:41 1997 +0200 @@ -35,9 +35,14 @@ by (Blast_tac \(i\)); \end{ttbox} If the subgoal is a simple formula of the predicate calculus or set theory, -then it should be proved quickly. However, to use the classical reasoner -effectively, you need to know how it works and how to choose among the many -tactics available, including {\tt Fast_tac} and {\tt Best_tac}. +then it should be proved quickly. To attempt to prove \emph{all} subgoals +using a combination of rewriting and classical reasoning, try +\begin{ttbox} +by (Auto_tac()); +\end{ttbox} +To use the classical reasoner effectively, you need to know how it works. It +provides many tactics to choose from, including {\tt Fast_tac} and {\tt + Best_tac}. We shall first discuss the underlying principles, then present the classical reasoner. Finally, we shall see how to instantiate it for @@ -374,11 +379,11 @@ If installed, the classical module provides several tactics (and other operations) for simulating the classical sequent calculus. -\subsection{The automatic tableau prover} -The tactic {\tt blast_tac} finds a proof rapidly using a separate tableau -prover and then reconstructs the proof using Isabelle tactics. It is much -faster and more powerful than the other classical reasoning tactics, but has -major limitations too. +\subsection{The tableau prover} +The tactic {\tt 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}. @@ -419,17 +424,38 @@ has been closed, extended or split. \end{ttdescription} -\subsection{The automatic tactics} + +\subsection{An automatic tactic} +\begin{ttbox} +auto_tac : claset * simpset -> tactic +auto : unit -> unit +\end{ttbox} +The auto-tactic attempts to prove all subgoals using a combination of +simplification and classical reasoning. 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. (Unfortunately, attempting to prove the +hard ones may take a long time.) It must be supplied both a simpset and a +claset; therefore it is most easily called as \texttt{Auto_tac}, which uses +the default claset and simpset (see \S\ref{sec:current-claset} below). For +interactive use, the shorthand \texttt{auto();} abbreviates +\begin{ttbox} +by (Auto_tac()); +\end{ttbox} + +\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 work by applying {\tt step_tac} or {\tt slow_step_tac} -repeatedly. Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; -they either prove this subgoal or fail. The {\tt slow_} versions are more -powerful but can be much slower. +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 {\tt SELECT_GOAL}) to one subgoal; they either prove +this subgoal or fail. The {\tt 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 @@ -505,7 +531,7 @@ The resulting search space is larger. \end{ttdescription} -\subsection{The current claset} +\subsection{The current claset}\label{sec:current-claset} Some logics (\FOL, {\HOL} and \ZF) support the concept of a current claset\index{claset!current}. This is a default set of classical rules. The underlying idea is quite similar to that of a current simpset described in @@ -514,12 +540,14 @@ tactics \begin{ttbox} Blast_tac : int -> tactic +Auto_tac : unit -> tactic Fast_tac : int -> tactic Best_tac : int -> tactic Deepen_tac : int -> int -> tactic Step_tac : int -> tactic \end{ttbox} -\indexbold{*Blast_tac}\indexbold{*Best_tac}\indexbold{*Fast_tac}% +\indexbold{*Blast_tac}\indexbold{*Auto_tac} +\indexbold{*Best_tac}\indexbold{*Fast_tac}% \indexbold{*Deepen_tac}\indexbold{*Step_tac} make use of the current claset. E.g. {\tt Blast_tac} is defined as follows: \begin{ttbox} @@ -533,12 +561,11 @@ \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs} \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs} are used to add rules to the current claset. They work exactly like their -lower case counterparts {\tt addSIs} etc. +lower case counterparts, such as {\tt addSIs}. Calling \begin{ttbox} Delrules : thm list -> unit \end{ttbox} -deletes rules from the current claset. You do not need to worry via which of -the above {\tt Add} functions the rule was initially added. +deletes rules from the current claset. \subsection{Other useful tactics} \index{tactics!for contradiction}