2 \chapter{The Classical Reasoner}\label{chap:classical}
3 \index{classical reasoner|(}
4 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
6 Although Isabelle is generic, many users will be working in some
7 extension of classical first-order logic. Isabelle's set theory~{\tt
8 ZF} is built upon theory~\texttt{FOL}, while {\HOL}
9 conceptually contains first-order logic as a fragment.
10 Theorem-proving in predicate logic is undecidable, but many
11 researchers have developed strategies to assist in this task.
13 Isabelle's classical reasoner is an \ML{} functor that accepts certain
14 information about a logic and delivers a suite of automatic tactics. Each
15 tactic takes a collection of rules and executes a simple, non-clausal proof
16 procedure. They are slow and simplistic compared with resolution theorem
17 provers, but they can save considerable time and effort. They can prove
18 theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
20 \[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))
21 \imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
22 \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
23 \imp \neg (\exists z. \forall x. F(x,z))
26 The tactics are generic. They are not restricted to first-order logic, and
27 have been heavily used in the development of Isabelle's set theory. Few
28 interactive proof assistants provide this much automation. The tactics can
29 be traced, and their components can be called directly; in this manner,
30 any proof can be viewed interactively.
32 The simplest way to apply the classical reasoner (to subgoal~$i$) is to type
36 This command quickly proves most simple formulas of the predicate calculus or
37 set theory. To attempt to prove \emph{all} subgoals using a combination of
38 rewriting and classical reasoning, try
42 To do all obvious logical steps, even if they do not prove the
43 subgoal, type one of the following:
45 by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}}
46 by Safe_tac; \emph{\textrm{applies to all subgoals}}
48 You need to know how the classical reasoner works in order to use it
49 effectively. There are many tactics to choose from, including {\tt
50 Fast_tac} and \texttt{Best_tac}.
52 We shall first discuss the underlying principles, then present the
53 classical reasoner. Finally, we shall see how to instantiate it for
54 new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already
58 \section{The sequent calculus}
59 \index{sequent calculus}
60 Isabelle supports natural deduction, which is easy to use for interactive
61 proof. But natural deduction does not easily lend itself to automation,
62 and has a bias towards intuitionism. For certain proofs in classical
63 logic, it can not be called natural. The {\bf sequent calculus}, a
64 generalization of natural deduction, is easier to automate.
66 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
67 and~$\Delta$ are sets of formulae.%
68 \footnote{For first-order logic, sequents can equivalently be made from
69 lists or multisets of formulae.} The sequent
70 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
71 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
72 Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
73 while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf
74 basic} if its left and right sides have a common formula, as in $P,Q\turn
75 Q,R$; basic sequents are trivially valid.
77 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
78 side of the $\turn$~symbol they operate on. Rules that operate on the
79 right side are analogous to natural deduction's introduction rules, and
80 left rules are analogous to elimination rules.
81 Recall the natural deduction rules for
83 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
84 {Fig.\ts\ref{fol-fig}}.
85 The sequent calculus analogue of~$({\imp}I)$ is the rule
87 \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
90 This breaks down some implication on the right side of a sequent; $\Gamma$
91 and $\Delta$ stand for the sets of formulae that are unaffected by the
92 inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
95 \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
98 This breaks down some disjunction on the right side, replacing it by both
99 disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
101 To illustrate the use of multiple formulae on the right, let us prove
102 the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we
103 reduce this formula to a basic sequent:
104 \[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
105 {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
106 {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
107 {P, Q \turn Q, P\qquad\qquad}}}
109 This example is typical of the sequent calculus: start with the desired
110 theorem and apply rules backwards in a fairly arbitrary manner. This yields a
111 surprisingly effective proof procedure. Quantifiers add few complications,
112 since Isabelle handles parameters and schematic variables. See Chapter~10
113 of {\em ML for the Working Programmer}~\cite{paulson91} for further
117 \section{Simulating sequents by natural deduction}
118 Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@.
119 But natural deduction is easier to work with, and most object-logics employ
120 it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
121 Q@1,\ldots,Q@n$ by the Isabelle formula
122 \[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
123 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
124 Elim-resolution plays a key role in simulating sequent proofs.
126 We can easily handle reasoning on the left.
128 \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
129 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
130 achieves a similar effect as the corresponding sequent rules. For the
131 other connectives, we use sequent-style elimination rules instead of
132 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
133 the rule $(\neg L)$ has no effect under our representation of sequents!
135 \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)
137 What about reasoning on the right? Introduction rules can only affect the
138 formula in the conclusion, namely~$Q@1$. The other right-side formulae are
139 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.
140 \index{assumptions!negated}
141 In order to operate on one of these, it must first be exchanged with~$Q@1$.
142 Elim-resolution with the {\bf swap} rule has this effect:
143 $$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$
144 To ensure that swaps occur only when necessary, each introduction rule is
145 converted into a swapped form: it is resolved with the second premise
146 of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
147 called~$({\neg\conj}E)$, is
148 \[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
149 Similarly, the swapped form of~$({\imp}I)$ is
150 \[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \]
151 Swapped introduction rules are applied using elim-resolution, which deletes
152 the negated formula. Our representation of sequents also requires the use
153 of ordinary introduction rules. If we had no regard for readability, we
154 could treat the right side more uniformly by representing sequents as
155 \[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
158 \section{Extra rules for the sequent calculus}
159 As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
160 must be replaced by sequent-style elimination rules. In addition, we need
161 rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
162 Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
163 simulates $({\disj}R)$:
164 \[ (\neg Q\Imp P) \Imp P\disj Q \]
165 The destruction rule $({\imp}E)$ is replaced by
166 \[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
167 Quantifier replication also requires special rules. In classical logic,
168 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
169 $(\exists R)$ and $(\forall L)$ are dual:
170 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
171 {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
173 \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
174 {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
176 Thus both kinds of quantifier may be replicated. Theorems requiring
177 multiple uses of a universal formula are easy to invent; consider
178 \[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
179 for any~$n>1$. Natural examples of the multiple use of an existential
180 formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
182 Forgoing quantifier replication loses completeness, but gains decidability,
183 since the search space becomes finite. Many useful theorems can be proved
184 without replication, and the search generally delivers its verdict in a
185 reasonable time. To adopt this approach, represent the sequent rules
186 $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
187 E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
189 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
190 Elim-resolution with this rule will delete the universal formula after a
191 single use. To replicate universal quantifiers, replace the rule by
193 \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
196 To replicate existential quantifiers, replace $(\exists I)$ by
197 \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
198 All introduction rules mentioned above are also useful in swapped form.
200 Replication makes the search space infinite; we must apply the rules with
201 care. The classical reasoner distinguishes between safe and unsafe
202 rules, applying the latter only when there is no alternative. Depth-first
203 search may well go down a blind alley; best-first search is better behaved
204 in an infinite search space. However, quantifier replication is too
205 expensive to prove any but the simplest theorems.
208 \section{Classical rule sets}
209 \index{classical sets}
210 Each automatic tactic takes a {\bf classical set} --- a collection of
211 rules, classified as introduction or elimination and as {\bf safe} or {\bf
212 unsafe}. In general, safe rules can be attempted blindly, while unsafe
213 rules must be used with care. A safe rule must never reduce a provable
214 goal to an unprovable set of subgoals.
216 The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
217 rule is unsafe whose premises contain new unknowns. The elimination
218 rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
219 which discards the assumption $\forall x{.}P(x)$ and replaces it by the
220 weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
221 similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
222 since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
223 In classical first-order logic, all rules are safe except those mentioned
226 The safe/unsafe distinction is vague, and may be regarded merely as a way
227 of giving some rules priority over others. One could argue that
228 $({\disj}E)$ is unsafe, because repeated application of it could generate
229 exponentially many subgoals. Induction rules are unsafe because inductive
230 proofs are difficult to set up automatically. Any inference is unsafe that
231 instantiates an unknown in the proof state --- thus \ttindex{match_tac}
232 must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
233 is unsafe if it instantiates unknowns shared with other subgoals --- thus
234 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
236 \subsection{Adding rules to classical sets}
237 Classical rule sets belong to the abstract type \mltydx{claset}, which
238 supports the following operations (provided the classical reasoner is
242 print_cs : claset -> unit
243 addSIs : claset * thm list -> claset \hfill{\bf infix 4}
244 addSEs : claset * thm list -> claset \hfill{\bf infix 4}
245 addSDs : claset * thm list -> claset \hfill{\bf infix 4}
246 addIs : claset * thm list -> claset \hfill{\bf infix 4}
247 addEs : claset * thm list -> claset \hfill{\bf infix 4}
248 addDs : claset * thm list -> claset \hfill{\bf infix 4}
249 delrules : claset * thm list -> claset \hfill{\bf infix 4}
251 The add operations ignore any rule already present in the claset with the same
252 classification (such as Safe Introduction). They print a warning if the rule
253 has already been added with some other classification, but add the rule
254 anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the
255 claset, but see the warning below concerning destruction rules.
256 \begin{ttdescription}
257 \item[\ttindexbold{empty_cs}] is the empty classical set.
259 \item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
261 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
262 adds safe introduction~$rules$ to~$cs$.
264 \item[$cs$ addSEs $rules$] \indexbold{*addSEs}
265 adds safe elimination~$rules$ to~$cs$.
267 \item[$cs$ addSDs $rules$] \indexbold{*addSDs}
268 adds safe destruction~$rules$ to~$cs$.
270 \item[$cs$ addIs $rules$] \indexbold{*addIs}
271 adds unsafe introduction~$rules$ to~$cs$.
273 \item[$cs$ addEs $rules$] \indexbold{*addEs}
274 adds unsafe elimination~$rules$ to~$cs$.
276 \item[$cs$ addDs $rules$] \indexbold{*addDs}
277 adds unsafe destruction~$rules$ to~$cs$.
279 \item[$cs$ delrules $rules$] \indexbold{*delrules}
280 deletes~$rules$ from~$cs$. It prints a warning for those rules that are not
285 If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete
288 \(cs\) delrules [make_elim \(rule\)]
291 This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert
292 the destruction rules to elimination rules by applying \ttindex{make_elim},
293 and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.
296 Introduction rules are those that can be applied using ordinary resolution.
297 The classical set automatically generates their swapped forms, which will
298 be applied using elim-resolution. Elimination rules are applied using
299 elim-resolution. In a classical set, rules are sorted by the number of new
300 subgoals they will yield; rules that generate the fewest subgoals will be
301 tried first (see \S\ref{biresolve_tac}).
304 \subsection{Modifying the search step}
305 For a given classical set, the proof strategy is simple. Perform as many safe
306 inferences as possible; or else, apply certain safe rules, allowing
307 instantiation of unknowns; or else, apply an unsafe rule. The tactics also
308 eliminate assumptions of the form $x=t$ by substitution if they have been set
309 up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
310 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
311 and~$P$, then replace $P\imp Q$ by~$Q$.
313 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
314 you to modify this basic proof strategy by applying two lists of arbitrary
315 {\bf wrapper tacticals} to it.
316 The first wrapper list, which is considered to contain safe wrappers only,
317 affects \ttindex{safe_step_tac} and all the tactics that call it.
318 The second one, which may contain unsafe wrappers, affects \ttindex{step_tac},
319 \ttindex{slow_step_tac} and the tactics that call them.
320 A wrapper transforms each step of the search, for example
321 by invoking other tactics before or alternatively to the original step tactic.
322 All members of a wrapper list are applied in turn to the respective step tactic.
324 Initially the two wrapper lists are empty, which means no modification of the
325 step tactics. Safe and unsafe wrappers are added to a claset
326 with the functions given below, supplying them with wrapper names.
327 These names may be used to selectively delete wrappers.
330 type wrapper = (int -> tactic) -> (int -> tactic);
331 addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
332 addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
333 addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
334 delSWrapper : claset * string -> claset \hfill{\bf infix 4}
335 addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
336 addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
337 addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
338 delWrapper : claset * string -> claset \hfill{\bf infix 4}
340 addss : claset * simpset -> claset \hfill{\bf infix 4}
343 \index{simplification!from classical reasoner} The wrapper tacticals
344 underly the operator addss, which combines each search step by
345 simplification. Strictly speaking, \texttt{addss} is not part of the
346 classical reasoner. It should be defined when the simplifier is
350 fun cs addss ss = cs addbefore asm_full_simp_tac ss;
353 \begin{ttdescription}
354 \item[$cs$ addss $ss$] \indexbold{*addss}
355 adds the simpset~$ss$ to the classical set. The assumptions and goal will be
356 simplified, in a safe way, after the safe steps of the search.
358 \item[$cs$ addSbefore $tac$] \indexbold{*addSbefore}
359 changes the safe wrapper tactical to apply the given tactic {\em before}
360 each safe step of the search.
362 \item[$cs$ addSaltern $tac$] \indexbold{*addSaltern}
363 changes the safe wrapper tactical to apply the given tactic when a safe step
364 of the search would fail.
366 \item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper}
367 specifies a new safe wrapper tactical.
369 \item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper}
370 composes the $tactical$ with the existing safe wrapper tactical,
371 to combine their effects.
373 \item[$cs$ addbefore $tac$] \indexbold{*addbefore}
374 changes the (unsafe) wrapper tactical to apply the given tactic, which should
375 be safe, {\em before} each step of the search.
377 \item[$cs$ addaltern $tac$] \indexbold{*addaltern}
378 changes the (unsafe) wrapper tactical to apply the given tactic
379 {\em alternatively} after each step of the search.
381 \item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper}
382 specifies a new (unsafe) wrapper tactical.
384 \item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper}
385 composes the $tactical$ with the existing (unsafe) wrapper tactical,
386 to combine their effects.
390 \section{The classical tactics}
391 \index{classical reasoner!tactics} If installed, the classical module provides
392 powerful theorem-proving tactics. Most of them have capitalized analogues
393 that use the default claset; see \S\ref{sec:current-claset}.
395 \subsection{Semi-automatic tactics}
397 clarify_tac : claset -> int -> tactic
398 clarify_step_tac : claset -> int -> tactic
400 Use these when the automatic tactics fail. They perform all the obvious
401 logical inferences that do not split the subgoal. The result is a
402 simpler subgoal that can be tackled by other means, such as by
403 instantiating quantifiers yourself.
404 \begin{ttdescription}
405 \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
406 subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
408 \item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
409 subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
410 B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
411 performed provided they do not instantiate unknowns. Assumptions of the
412 form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
417 \subsection{The tableau prover}
418 The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
419 coded directly in \ML. It then reconstructs the proof using Isabelle
420 tactics. It is faster and more powerful than the other classical
421 reasoning tactics, but has major limitations too.
423 \item It does not use the wrapper tacticals described above, such as
425 \item It ignores types, which can cause problems in \HOL. If it applies a rule
426 whose types are inappropriate, then proof reconstruction will fail.
427 \item It does not perform higher-order unification, as needed by the rule {\tt
428 rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}. There are often
429 alternatives to such rules, for example {\tt
430 range_eqI} and \texttt{RepFun_eqI}.
431 \item The message {\small\tt Function Var's argument not a bound variable\ }
432 relates to the lack of higher-order unification. Function variables
433 may only be applied to parameters of the subgoal.
434 \item Its proof strategy is more general than \texttt{fast_tac}'s but can be
435 slower. If \texttt{blast_tac} fails or seems to be running forever, try {\tt
436 fast_tac} and the other tactics described below.
440 blast_tac : claset -> int -> tactic
441 Blast.depth_tac : claset -> int -> int -> tactic
442 Blast.trace : bool ref \hfill{\bf initially false}
444 The two tactics differ on how they bound the number of unsafe steps used in a
445 proof. While \texttt{blast_tac} starts with a bound of zero and increases it
446 successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
447 \begin{ttdescription}
448 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
449 subgoal~$i$ using iterative deepening to increase the search bound.
451 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
452 to prove subgoal~$i$ using a search bound of $lim$. Often a slow
453 proof using \texttt{blast_tac} can be made much faster by supplying the
454 successful search bound to this tactic instead.
456 \item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
457 causes the tableau prover to print a trace of its search. At each step it
458 displays the formula currently being examined and reports whether the branch
459 has been closed, extended or split.
463 \subsection{An automatic tactic}
465 auto_tac : claset * simpset -> tactic
468 The auto-tactic attempts to prove all subgoals using a combination of
469 simplification and classical reasoning. It is intended for situations where
470 there are a lot of mostly trivial subgoals; it proves all the easy ones,
471 leaving the ones it cannot prove. (Unfortunately, attempting to prove the
472 hard ones may take a long time.) It must be supplied both a simpset and a
473 claset; therefore it is most easily called as \texttt{Auto_tac}, which uses
474 the default claset and simpset (see \S\ref{sec:current-claset} below). For
475 interactive use, the shorthand \texttt{auto();} abbreviates
480 \subsection{Other classical tactics}
482 fast_tac : claset -> int -> tactic
483 best_tac : claset -> int -> tactic
484 slow_tac : claset -> int -> tactic
485 slow_best_tac : claset -> int -> tactic
487 These tactics attempt to prove a subgoal using sequent-style reasoning.
488 Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their
489 effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
490 this subgoal or fail. The \texttt{slow_} versions conduct a broader
492 \footnote{They may, when backtracking from a failed proof attempt, undo even
493 the step of proving a subgoal by assumption.}
495 The best-first tactics are guided by a heuristic function: typically, the
496 total size of the proof state. This function is supplied in the functor call
497 that sets up the classical reasoner.
498 \begin{ttdescription}
499 \item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
500 depth-first search, to prove subgoal~$i$.
502 \item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
503 best-first search, to prove subgoal~$i$.
505 \item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
506 depth-first search, to prove subgoal~$i$.
508 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
509 best-first search, to prove subgoal~$i$.
513 \subsection{Depth-limited automatic tactics}
515 depth_tac : claset -> int -> int -> tactic
516 deepen_tac : claset -> int -> int -> tactic
518 These work by exhaustive search up to a specified depth. Unsafe rules are
519 modified to preserve the formula they act on, so that it be used repeatedly.
520 They can prove more goals than \texttt{fast_tac} can but are much
521 slower, for example if the assumptions have many universal quantifiers.
523 The depth limits the number of unsafe steps. If you can estimate the minimum
524 number of unsafe steps needed, supply this value as~$m$ to save time.
525 \begin{ttdescription}
526 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
527 tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
529 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
530 tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac}
531 repeatedly with increasing depths, starting with~$m$.
535 \subsection{Single-step tactics}
537 safe_step_tac : claset -> int -> tactic
538 safe_tac : claset -> tactic
539 inst_step_tac : claset -> int -> tactic
540 step_tac : claset -> int -> tactic
541 slow_step_tac : claset -> int -> tactic
543 The automatic proof procedures call these tactics. By calling them
544 yourself, you can execute these procedures one step at a time.
545 \begin{ttdescription}
546 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
547 subgoal~$i$. The safe wrapper tactical is applied to a tactic that may
548 include proof by assumption or Modus Ponens (taking care not to instantiate
549 unknowns), or substitution.
551 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
552 subgoals. It is deterministic, with at most one outcome.
554 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
555 but allows unknowns to be instantiated.
557 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
558 procedure. The (unsafe) wrapper tactical is applied to a tactic that tries
559 \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$.
561 \item[\ttindexbold{slow_step_tac}]
562 resembles \texttt{step_tac}, but allows backtracking between using safe
563 rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
564 The resulting search space is larger.
567 \subsection{The current claset}\label{sec:current-claset}
569 Each theory is equipped with an implicit \emph{current
570 claset}\index{claset!current}. This is a default set of classical
571 rules. The underlying idea is quite similar to that of a current
572 simpset described in \S\ref{sec:simp-for-dummies}; please read that
573 section, including its warnings. The implicit claset can be accessed
576 claset : unit -> claset
577 claset_ref : unit -> claset ref
578 claset_of : theory -> claset
579 claset_ref_of : theory -> claset ref
580 print_claset : theory -> unit
585 Blast_tac : int -> tactic
587 Fast_tac : int -> tactic
588 Best_tac : int -> tactic
589 Deepen_tac : int -> int -> tactic
590 Clarify_tac : int -> tactic
591 Clarify_step_tac : int -> tactic
593 Safe_step_tac : int -> tactic
594 Step_tac : int -> tactic
596 \indexbold{*Blast_tac}\indexbold{*Auto_tac}
597 \indexbold{*Best_tac}\indexbold{*Fast_tac}%
598 \indexbold{*Deepen_tac}
599 \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}
600 \indexbold{*Safe_tac}\indexbold{*Safe_step_tac}
601 \indexbold{*Step_tac}
602 make use of the current claset. For example, \texttt{Blast_tac} is defined as
604 fun Blast_tac i st = blast_tac (claset()) i st;
606 and gets the current claset, only after it is applied to a proof
609 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
611 \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
612 \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
613 are used to add rules to the current claset. They work exactly like their
614 lower case counterparts, such as \texttt{addSIs}. Calling
616 Delrules : thm list -> unit
618 deletes rules from the current claset.
620 \subsection{Other useful tactics}
621 \index{tactics!for contradiction}
622 \index{tactics!for Modus Ponens}
624 contr_tac : int -> tactic
625 mp_tac : int -> tactic
626 eq_mp_tac : int -> tactic
627 swap_res_tac : thm list -> int -> tactic
629 These can be used in the body of a specialized search.
630 \begin{ttdescription}
631 \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
632 solves subgoal~$i$ by detecting a contradiction among two assumptions of
633 the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The
634 tactic can produce multiple outcomes, enumerating all possible
637 \item[\ttindexbold{mp_tac} {\it i}]
638 is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
639 subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
640 $P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
643 \item[\ttindexbold{eq_mp_tac} {\it i}]
644 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
647 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
648 the proof state using {\it thms}, which should be a list of introduction
649 rules. First, it attempts to prove the goal using \texttt{assume_tac} or
650 \texttt{contr_tac}. It then attempts to apply each rule in turn, attempting
651 resolution and also elim-resolution with the swapped form.
654 \subsection{Creating swapped rules}
656 swapify : thm list -> thm list
657 joinrules : thm list * thm list -> (bool * thm) list
659 \begin{ttdescription}
660 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
661 swapped versions of~{\it thms}, regarded as introduction rules.
663 \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
664 joins introduction rules, their swapped versions, and elimination rules for
665 use with \ttindex{biresolve_tac}. Each rule is paired with~\texttt{false}
666 (indicating ordinary resolution) or~\texttt{true} (indicating
671 \section{Setting up the classical reasoner}\label{sec:classical-setup}
672 \index{classical reasoner!setting up}
673 Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, have
674 the classical reasoner already set up. When defining a new classical logic,
675 you should set up the reasoner yourself. It consists of the \ML{} functor
676 \ttindex{ClassicalFun}, which takes the argument
680 signature CLASSICAL_DATA =
685 val sizef : thm -> int
686 val hyp_subst_tacs : (int -> tactic) list
689 Thus, the functor requires the following items:
690 \begin{ttdescription}
691 \item[\tdxbold{mp}] should be the Modus Ponens rule
692 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
694 \item[\tdxbold{not_elim}] should be the contradiction rule
695 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
697 \item[\tdxbold{swap}] should be the swap rule
698 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
700 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
701 search. It should estimate the size of the remaining subgoals. A good
702 heuristic function is \ttindex{size_of_thm}, which measures the size of the
703 proof state. Another size function might ignore certain subgoals (say,
704 those concerned with type checking). A heuristic function might simply
707 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
708 the hypotheses, typically created by \ttindex{HypsubstFun} (see
709 Chapter~\ref{substitution}). This list can, of course, be empty. The
710 tactics are assumed to be safe!
712 The functor is not at all sensitive to the formalization of the
713 object-logic. It does not even examine the rules, but merely applies
714 them according to its fixed strategy. The functor resides in {\tt
715 Provers/classical.ML} in the Isabelle sources.
717 \index{classical reasoner|)}