author paulson Mon, 19 May 1997 15:22:41 +0200 changeset 3224 4ea2aa9f93a5 parent 3223 49f1a09576c2 child 3225 cee363fc07d7
Documented auto_tac
 doc-src/Ref/classical.tex file | annotate | diff | comparison | revisions
--- 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
@@ -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 @@
\index{tactics!for contradiction}