1.1 --- a/doc-src/Ref/classical.tex Wed Apr 30 16:36:38 1997 +0200
1.2 +++ b/doc-src/Ref/classical.tex Wed Apr 30 16:36:59 1997 +0200
1.3 @@ -31,11 +31,12 @@
1.4 The simplest way to apply the classical reasoner (to subgoal~$i$) is as
1.5 follows:
1.6 \begin{ttbox}
1.7 -by (Fast_tac \(i\));
1.8 +by (Blast_tac \(i\));
1.9 \end{ttbox}
1.10 If the subgoal is a simple formula of the predicate calculus or set theory,
1.11 then it should be proved quickly. However, to use the classical reasoner
1.12 -effectively, you need to know how it works.
1.13 +effectively, you need to know how it works and how to choose among the many
1.14 +tactics available, including {\tt Fast_tac} and {\tt Best_tac}.
1.15
1.16 We shall first discuss the underlying principles, then present the classical
1.17 reasoner. Finally, we shall see how to instantiate it for new logics. The
1.18 @@ -228,7 +229,11 @@
1.19 addDs : claset * thm list -> claset \hfill{\bf infix 4}
1.20 delrules : claset * thm list -> claset \hfill{\bf infix 4}
1.21 \end{ttbox}
1.22 -The add operations do not check for repetitions.
1.23 +The add operations ignore any rule already present in the claset with the same
1.24 +classification (such as Safe Introduction). They print a warning if the rule
1.25 +has already been added with some other classification, but add the rule
1.26 +anyway. Calling {\tt delrules} deletes all occurrences of a rule from the
1.27 +claset, but see the warning below concerning destruction rules.
1.28 \begin{ttdescription}
1.29 \item[\ttindexbold{empty_cs}] is the empty classical set.
1.30
1.31 @@ -253,9 +258,22 @@
1.32 adds unsafe destruction~$rules$ to~$cs$.
1.33
1.34 \item[$cs$ delrules $rules$] \indexbold{*delrules}
1.35 -deletes~$rules$ from~$cs$.
1.36 +deletes~$rules$ from~$cs$. It prints a warning for those rules that are not
1.37 +in~$cs$.
1.38 \end{ttdescription}
1.39
1.40 +\begin{warn}
1.41 + If you added $rule$ using {\tt addSDs} or {\tt addDs}, then you must delete
1.42 + it as follows:
1.43 +\begin{ttbox}
1.44 +\(cs\) delrules [make_elim \(rule\)]
1.45 +\end{ttbox}
1.46 +\par\noindent
1.47 +This is necessary because the operators {\tt addSDs} and {\tt addDs} convert
1.48 +the destruction rules to elimination rules by applying \ttindex{make_elim},
1.49 +and then insert them using {\tt addSEs} and {\tt addEs}, respectively.
1.50 +\end{warn}
1.51 +
1.52 Introduction rules are those that can be applied using ordinary resolution.
1.53 The classical set automatically generates their swapped forms, which will
1.54 be applied using elim-resolution. Elimination rules are applied using
1.55 @@ -272,7 +290,8 @@
1.56 below). They may perform a form of Modus Ponens: if there are assumptions
1.57 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
1.58
1.59 -The classical reasoner allows you to modify this basic proof strategy by
1.60 +The classical reasoning tactics---except {\tt blast_tac}!---allow you to
1.61 +modify this basic proof strategy by
1.62 applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
1.63 the search. Usually they are the identity tacticals, but they could apply
1.64 another tactic before or after the step tactic. The first one, which is
1.65 @@ -343,6 +362,51 @@
1.66 If installed, the classical module provides several tactics (and other
1.67 operations) for simulating the classical sequent calculus.
1.68
1.69 +\subsection{The automatic tableau prover}
1.70 +The tactic {\tt blast_tac} finds a proof rapidly using a separate tableau
1.71 +prover and then reconstructs the proof using Isabelle tactics. It is much
1.72 +faster and more powerful than the other classical reasoning tactics, but has
1.73 +major limitations too.
1.74 +\begin{itemize}
1.75 +\item It does not use the wrapper tacticals described above, such as
1.76 + \ttindex{addss}.
1.77 +\item It ignores types, which can cause problems in \HOL. If it applies a rule
1.78 + whose types are inappropriate, then proof reconstruction will fail.
1.79 +\item It does not perform higher-order unification, as needed by the rule {\tt
1.80 + rangeI} in {\HOL} and {\tt RepFunI} in {\ZF}. There are often
1.81 + alternatives to such rules, for example {\tt
1.82 + range_eqI} and {\tt RepFun_eqI}.
1.83 +\item The message {\small\tt Function Var's argument not a bound variable\ }
1.84 +relates to the lack of higher-order unification. Function variables
1.85 +may only be applied to parameters of the subgoal.
1.86 +\item Its proof strategy is more general than {\tt fast_tac}'s but can be
1.87 + slower. If {\tt blast_tac} fails or seems to be running forever, try {\tt
1.88 + fast_tac} and the other tactics described below.
1.89 +\end{itemize}
1.90 +%
1.91 +\begin{ttbox}
1.92 +blast_tac : claset -> int -> tactic
1.93 +Blast.depth_tac : claset -> int -> int -> tactic
1.94 +Blast.trace : bool ref \hfill{\bf initially false}
1.95 +\end{ttbox}
1.96 +The two tactics differ on how they bound the number of unsafe steps used in a
1.97 +proof. While {\tt blast_tac} starts with a bound of zero and increases it
1.98 +successively to~20, {\tt Blast.depth_tac} applies a user-supplied search bound.
1.99 +\begin{ttdescription}
1.100 +\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
1.101 + subgoal~$i$ using iterative deepening to increase the search bound.
1.102 +
1.103 +\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
1.104 + to prove subgoal~$i$ using a search bound of $lim$. Often a slow
1.105 + proof using {\tt blast_tac} can be made much faster by supplying the
1.106 + successful search bound to this tactic instead.
1.107 +
1.108 +\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}
1.109 + causes the tableau prover to print a trace of its search. At each step it
1.110 + displays the formula currently being examined and reports whether the branch
1.111 + has been closed, extended or split.
1.112 +\end{ttdescription}
1.113 +
1.114 \subsection{The automatic tactics}
1.115 \begin{ttbox}
1.116 fast_tac : claset -> int -> tactic
1.117 @@ -352,7 +416,7 @@
1.118 \end{ttbox}
1.119 These tactics work by applying {\tt step_tac} or {\tt slow_step_tac}
1.120 repeatedly. Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal;
1.121 -they either solve this subgoal or fail. The {\tt slow_} versions are more
1.122 +they either prove this subgoal or fail. The {\tt slow_} versions are more
1.123 powerful but can be much slower.
1.124
1.125 The best-first tactics are guided by a heuristic function: typically, the
1.126 @@ -360,16 +424,16 @@
1.127 that sets up the classical reasoner.
1.128 \begin{ttdescription}
1.129 \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
1.130 -depth-first search, to solve subgoal~$i$.
1.131 +depth-first search, to prove subgoal~$i$.
1.132
1.133 \item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
1.134 -best-first search, to solve subgoal~$i$.
1.135 +best-first search, to prove subgoal~$i$.
1.136
1.137 \item[\ttindexbold{slow_tac} $cs$ $i$] applies {\tt slow_step_tac} using
1.138 -depth-first search, to solve subgoal~$i$.
1.139 +depth-first search, to prove subgoal~$i$.
1.140
1.141 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies {\tt slow_step_tac} using
1.142 -best-first search, to solve subgoal~$i$.
1.143 +best-first search, to prove subgoal~$i$.
1.144 \end{ttdescription}
1.145
1.146
1.147 @@ -387,10 +451,10 @@
1.148 number of unsafe steps needed, supply this value as~$m$ to save time.
1.149 \begin{ttdescription}
1.150 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
1.151 -tries to solve subgoal~$i$ by exhaustive search up to depth~$m$.
1.152 +tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
1.153
1.154 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
1.155 -tries to solve subgoal~$i$ by iterative deepening. It calls {\tt depth_tac}
1.156 +tries to prove subgoal~$i$ by iterative deepening. It calls {\tt depth_tac}
1.157 repeatedly with increasing depths, starting with~$m$.
1.158 \end{ttdescription}
1.159
1.160 @@ -437,16 +501,17 @@
1.161 warnings. Just like simpsets, clasets can be associated with theories. The
1.162 tactics
1.163 \begin{ttbox}
1.164 -Step_tac : int -> tactic
1.165 +Blast_tac : int -> tactic
1.166 Fast_tac : int -> tactic
1.167 Best_tac : int -> tactic
1.168 Deepen_tac : int -> int -> tactic
1.169 +Step_tac : int -> tactic
1.170 \end{ttbox}
1.171 -\indexbold{*Step_tac} \indexbold{*Best_tac} \indexbold{*Fast_tac}
1.172 -\indexbold{*Deepen_tac}
1.173 -make use of the current claset. E.g.~{\tt Fast_tac} is defined as follows:
1.174 +\indexbold{*Blast_tac}\indexbold{*Best_tac}\indexbold{*Fast_tac}%
1.175 +\indexbold{*Deepen_tac}\indexbold{*Step_tac}
1.176 +make use of the current claset. E.g. {\tt Blast_tac} is defined as follows:
1.177 \begin{ttbox}
1.178 -fun Fast_tac i = fast_tac (!claset) i;
1.179 +fun Blast_tac i = fast_tac (!claset) i;
1.180 \end{ttbox}
1.181 where \ttindex{!claset} is the current claset.
1.182 The functions
1.183 @@ -492,7 +557,7 @@
1.184
1.185 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
1.186 the proof state using {\it thms}, which should be a list of introduction
1.187 -rules. First, it attempts to solve the goal using {\tt assume_tac} or
1.188 +rules. First, it attempts to prove the goal using {\tt assume_tac} or
1.189 {\tt contr_tac}. It then attempts to apply each rule in turn, attempting
1.190 resolution and also elim-resolution with the swapped form.
1.191 \end{ttdescription}