--- a/doc-src/Ref/classical.tex Sun Jun 05 20:23:05 2011 +0200
+++ b/doc-src/Ref/classical.tex Sun Jun 05 22:02:54 2011 +0200
@@ -124,129 +124,28 @@
\section{The classical tactics}
-\index{classical reasoner!tactics} If installed, the classical module provides
-powerful theorem-proving tactics.
-
-
-\subsection{The tableau prover}
-The tactic \texttt{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}.
-\item It does not perform higher-order unification, as needed by the rule {\tt
- rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives
- to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
-\item Function variables may only be applied to parameters of the subgoal.
-(This restriction arises because the prover does not use higher-order
-unification.) If other function variables are present then the prover will
-fail with the message {\small\tt Function Var's argument not a bound variable}.
-\item Its proof strategy is more general than \texttt{fast_tac}'s but can be
- slower. If \texttt{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 \texttt{blast_tac} starts with a bound of zero and increases it
-successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
-\begin{ttdescription}
-\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
- subgoal~$i$, increasing the search bound using iterative
- deepening~\cite{korf85}.
-
-\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
- to prove subgoal~$i$ using a search bound of $lim$. Sometimes a slow
- proof using \texttt{blast_tac} can be made much faster by supplying the
- successful search bound to this tactic instead.
-
-\item[set \ttindexbold{Blast.trace};] \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{Automatic tactics}\label{sec:automatic-tactics}
-\begin{ttbox}
-type clasimpset = claset * simpset;
-auto_tac : clasimpset -> tactic
-force_tac : clasimpset -> int -> tactic
-auto : unit -> unit
-force : int -> unit
-\end{ttbox}
-The automatic tactics attempt to prove goals using a combination of
-simplification and classical reasoning.
-\begin{ttdescription}
-\item[\ttindexbold{auto_tac $(cs,ss)$}] 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.)
-\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$
-completely. It tries to apply all fancy tactics it knows about,
-performing a rather exhaustive search.
-\end{ttdescription}
-
\subsection{Semi-automatic tactics}
\begin{ttbox}
-clarify_tac : claset -> int -> tactic
clarify_step_tac : claset -> int -> tactic
-clarsimp_tac : clasimpset -> int -> tactic
\end{ttbox}
-Use these when the automatic tactics fail. They perform all the obvious
-logical inferences that do not split the subgoal. The result is a
-simpler subgoal that can be tackled by other means, such as by
-instantiating quantifiers yourself.
+
\begin{ttdescription}
-\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
-subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
performed provided they do not instantiate unknowns. Assumptions of the
form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
applied.
-\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
-also does simplification with the given simpset. Note that if the simpset
-includes a splitter for the premises, the subgoal may still be split.
\end{ttdescription}
\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 attempt to prove a subgoal using sequent-style reasoning.
-Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their
-effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
-this subgoal or fail. The \texttt{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
-that sets up the classical reasoner.
\begin{ttdescription}
-\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
-depth-first search to prove subgoal~$i$.
-
-\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
-best-first search to prove subgoal~$i$.
-
-\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
-depth-first search to prove subgoal~$i$.
-
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
best-first search to prove subgoal~$i$.
\end{ttdescription}
@@ -277,7 +176,6 @@
\subsection{Single-step tactics}
\begin{ttbox}
safe_step_tac : claset -> int -> tactic
-safe_tac : claset -> tactic
inst_step_tac : claset -> int -> tactic
step_tac : claset -> int -> tactic
slow_step_tac : claset -> int -> tactic
@@ -290,9 +188,6 @@
include proof by assumption or Modus Ponens (taking care not to instantiate
unknowns), or substitution.
-\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
-subgoals. It is deterministic, with at most one outcome.
-
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
but allows unknowns to be instantiated.