# HG changeset patch
# User paulson
# Date 862411019 -7200
# Node ID 32dad29d4666de8aac69b9ea9c53ab69db5485fa
# Parent  857c1c05f0c74e13df50dadbe135cca390c4a250
Documented blast_tac

diff -r 857c1c05f0c7 -r 32dad29d4666 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Wed Apr 30 16:36:38 1997 +0200
+++ b/doc-src/Ref/classical.tex	Wed Apr 30 16:36:59 1997 +0200
@@ -31,11 +31,12 @@
 The simplest way to apply the classical reasoner (to subgoal~$i$) is as
 follows:
 \begin{ttbox}
-by (Fast_tac \(i\));
+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.
+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}.
 
 We shall first discuss the underlying principles, then present the classical
 reasoner.  Finally, we shall see how to instantiate it for new logics.  The
@@ -228,7 +229,11 @@
 addDs       : claset * thm list -> claset                 \hfill{\bf infix 4}
 delrules    : claset * thm list -> claset                 \hfill{\bf infix 4}
 \end{ttbox}
-The add operations do not check for repetitions.
+The add operations ignore any rule already present in the claset with the same
+classification (such as Safe Introduction).  They print a warning if the rule
+has already been added with some other classification, but add the rule
+anyway.  Calling {\tt delrules} deletes all occurrences of a rule from the
+claset, but see the warning below concerning destruction rules.
 \begin{ttdescription}
 \item[\ttindexbold{empty_cs}] is the empty classical set.
 
@@ -253,9 +258,22 @@
 adds unsafe destruction~$rules$ to~$cs$.
 
 \item[$cs$ delrules $rules$] \indexbold{*delrules}
-deletes~$rules$ from~$cs$.
+deletes~$rules$ from~$cs$.  It prints a warning for those rules that are not
+in~$cs$.
 \end{ttdescription}
 
+\begin{warn}
+  If you added $rule$ using {\tt addSDs} or {\tt addDs}, then you must delete
+  it as follows:
+\begin{ttbox}
+\(cs\) delrules [make_elim \(rule\)]
+\end{ttbox}
+\par\noindent
+This is necessary because the operators {\tt addSDs} and {\tt addDs} convert
+the destruction rules to elimination rules by applying \ttindex{make_elim},
+and then insert them using {\tt addSEs} and {\tt addEs}, respectively.
+\end{warn}
+
 Introduction rules are those that can be applied using ordinary resolution.
 The classical set automatically generates their swapped forms, which will
 be applied using elim-resolution.  Elimination rules are applied using
@@ -272,7 +290,8 @@
 below).  They may perform a form of Modus Ponens: if there are assumptions
 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
 
-The classical reasoner allows you to modify this basic proof strategy by
+The classical reasoning tactics---except {\tt blast_tac}!---allow you to
+modify this basic proof strategy by 
 applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
 the search.  Usually they are the identity tacticals, but they could apply 
 another tactic before or after the step tactic. The first one, which is
@@ -343,6 +362,51 @@
 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.  
+\begin{itemize}
+\item It does not use the wrapper tacticals described above, such as
+  \ttindex{addss}.
+\item It ignores types, which can cause problems in \HOL.  If it applies a rule
+  whose types are inappropriate, then proof reconstruction will fail.
+\item It does not perform higher-order unification, as needed by the rule {\tt
+    rangeI} in {\HOL} and {\tt RepFunI} in {\ZF}.  There are often
+    alternatives to such rules, for example {\tt
+    range_eqI} and {\tt RepFun_eqI}.
+\item The message {\small\tt Function Var's argument not a bound variable\ }
+relates to the lack of higher-order unification.  Function variables
+may only be applied to parameters of the subgoal.
+\item Its proof strategy is more general than {\tt fast_tac}'s but can be
+  slower.  If {\tt 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 {\tt blast_tac} starts with a bound of zero and increases it
+successively to~20, {\tt Blast.depth_tac} applies a user-supplied search bound.
+\begin{ttdescription}
+\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
+  subgoal~$i$ using iterative deepening to increase the search bound.
+  
+\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
+  to prove subgoal~$i$ using a search bound of $lim$.  Often a slow
+  proof using {\tt blast_tac} can be made much faster by supplying the
+  successful search bound to this tactic instead.
+  
+\item[\ttindexbold{Blast.trace} := true;] \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{The automatic tactics}
 \begin{ttbox} 
 fast_tac      : claset -> int -> tactic
@@ -352,7 +416,7 @@
 \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 solve this subgoal or fail.  The {\tt slow_} versions are more
+they either prove this subgoal or fail.  The {\tt slow_} versions are more
 powerful but can be much slower.  
 
 The best-first tactics are guided by a heuristic function: typically, the
@@ -360,16 +424,16 @@
 that sets up the classical reasoner.
 \begin{ttdescription}
 \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
-depth-first search, to solve subgoal~$i$.
+depth-first search, to prove subgoal~$i$.
 
 \item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
-best-first search, to solve subgoal~$i$.
+best-first search, to prove subgoal~$i$.
 
 \item[\ttindexbold{slow_tac} $cs$ $i$] applies {\tt slow_step_tac} using
-depth-first search, to solve subgoal~$i$.
+depth-first search, to prove subgoal~$i$.
 
 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies {\tt slow_step_tac} using
-best-first search, to solve subgoal~$i$.
+best-first search, to prove subgoal~$i$.
 \end{ttdescription}
 
 
@@ -387,10 +451,10 @@
 number of unsafe steps needed, supply this value as~$m$ to save time.
 \begin{ttdescription}
 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
-tries to solve subgoal~$i$ by exhaustive search up to depth~$m$.
+tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
 
 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
-tries to solve subgoal~$i$ by iterative deepening.  It calls {\tt depth_tac}
+tries to prove subgoal~$i$ by iterative deepening.  It calls {\tt depth_tac}
 repeatedly with increasing depths, starting with~$m$.
 \end{ttdescription}
 
@@ -437,16 +501,17 @@
 warnings.  Just like simpsets, clasets can be associated with theories.  The
 tactics
 \begin{ttbox}
-Step_tac     : int -> tactic
+Blast_tac     : int -> tactic
 Fast_tac     : int -> tactic
 Best_tac     : int -> tactic
 Deepen_tac   : int -> int -> tactic
+Step_tac     : int -> tactic
 \end{ttbox}
-\indexbold{*Step_tac} \indexbold{*Best_tac} \indexbold{*Fast_tac}
-\indexbold{*Deepen_tac} 
-make use of the current claset. E.g.~{\tt Fast_tac} is defined as follows:
+\indexbold{*Blast_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}
-fun Fast_tac i = fast_tac (!claset) i;
+fun Blast_tac i = fast_tac (!claset) i;
 \end{ttbox}
 where \ttindex{!claset} is the current claset.
 The functions
@@ -492,7 +557,7 @@
 
 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
 the proof state using {\it thms}, which should be a list of introduction
-rules.  First, it attempts to solve the goal using {\tt assume_tac} or
+rules.  First, it attempts to prove the goal using {\tt assume_tac} or
 {\tt contr_tac}.  It then attempts to apply each rule in turn, attempting
 resolution and also elim-resolution with the swapped form.
 \end{ttdescription}