# 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}