author paulson Wed, 30 Apr 1997 16:36:59 +0200 changeset 3089 32dad29d4666 parent 3088 857c1c05f0c7 child 3090 eeb4d0c7f748
Documented blast_tac
 doc-src/Ref/classical.tex file | annotate | diff | comparison | revisions
--- 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
+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},
+\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
+\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}