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 extension
7 of classical first-order logic. Isabelle's set theory~{\tt ZF} is built
8 upon theory~{\tt FOL}, while higher-order logic contains first-order logic
9 as a fragment. Theorem-proving in predicate logic is undecidable, but many
10 researchers have developed strategies to assist in this task.
12 Isabelle's classical reasoner is an \ML{} functor that accepts certain
13 information about a logic and delivers a suite of automatic tactics. Each
14 tactic takes a collection of rules and executes a simple, non-clausal proof
15 procedure. They are slow and simplistic compared with resolution theorem
16 provers, but they can save considerable time and effort. They can prove
17 theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
19 \[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))
20 \imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
21 \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
22 \imp \neg (\exists z. \forall x. F(x,z))
25 The tactics are generic. They are not restricted to first-order logic, and
26 have been heavily used in the development of Isabelle's set theory. Few
27 interactive proof assistants provide this much automation. The tactics can
28 be traced, and their components can be called directly; in this manner,
29 any proof can be viewed interactively.
31 The simplest way to apply the classical reasoner (to subgoal~$i$) is as
36 If the subgoal is a simple formula of the predicate calculus or set theory,
37 then it should be proved quickly. However, to use the classical reasoner
38 effectively, you need to know how it works and how to choose among the many
39 tactics available, including {\tt Fast_tac} and {\tt Best_tac}.
41 We shall first discuss the underlying principles, then present the classical
42 reasoner. Finally, we shall see how to instantiate it for new logics. The
43 logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already installed.
46 \section{The sequent calculus}
47 \index{sequent calculus}
48 Isabelle supports natural deduction, which is easy to use for interactive
49 proof. But natural deduction does not easily lend itself to automation,
50 and has a bias towards intuitionism. For certain proofs in classical
51 logic, it can not be called natural. The {\bf sequent calculus}, a
52 generalization of natural deduction, is easier to automate.
54 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
55 and~$\Delta$ are sets of formulae.%
56 \footnote{For first-order logic, sequents can equivalently be made from
57 lists or multisets of formulae.} The sequent
58 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
59 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
60 Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
61 while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf
62 basic} if its left and right sides have a common formula, as in $P,Q\turn
63 Q,R$; basic sequents are trivially valid.
65 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
66 side of the $\turn$~symbol they operate on. Rules that operate on the
67 right side are analogous to natural deduction's introduction rules, and
68 left rules are analogous to elimination rules.
69 Recall the natural deduction rules for
71 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
72 {Fig.\ts\ref{fol-fig}}.
73 The sequent calculus analogue of~$({\imp}I)$ is the rule
74 $$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
76 This breaks down some implication on the right side of a sequent; $\Gamma$
77 and $\Delta$ stand for the sets of formulae that are unaffected by the
78 inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
80 $$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
82 This breaks down some disjunction on the right side, replacing it by both
83 disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
85 To illustrate the use of multiple formulae on the right, let us prove
86 the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we
87 reduce this formula to a basic sequent:
88 \[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
89 {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
90 {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
91 {P, Q \turn Q, P\qquad\qquad}}}
93 This example is typical of the sequent calculus: start with the desired
94 theorem and apply rules backwards in a fairly arbitrary manner. This yields a
95 surprisingly effective proof procedure. Quantifiers add few complications,
96 since Isabelle handles parameters and schematic variables. See Chapter~10
97 of {\em ML for the Working Programmer}~\cite{paulson91} for further
101 \section{Simulating sequents by natural deduction}
102 Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.
103 But natural deduction is easier to work with, and most object-logics employ
104 it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
105 Q@1,\ldots,Q@n$ by the Isabelle formula
106 \[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
107 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
108 Elim-resolution plays a key role in simulating sequent proofs.
110 We can easily handle reasoning on the left.
112 \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
113 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
114 achieves a similar effect as the corresponding sequent rules. For the
115 other connectives, we use sequent-style elimination rules instead of
116 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
117 the rule $(\neg L)$ has no effect under our representation of sequents!
118 $$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
120 What about reasoning on the right? Introduction rules can only affect the
121 formula in the conclusion, namely~$Q@1$. The other right-side formulae are
122 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.
123 \index{assumptions!negated}
124 In order to operate on one of these, it must first be exchanged with~$Q@1$.
125 Elim-resolution with the {\bf swap} rule has this effect:
126 $$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$
127 To ensure that swaps occur only when necessary, each introduction rule is
128 converted into a swapped form: it is resolved with the second premise
129 of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
130 called~$({\neg\conj}E)$, is
131 \[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
132 Similarly, the swapped form of~$({\imp}I)$ is
133 \[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \]
134 Swapped introduction rules are applied using elim-resolution, which deletes
135 the negated formula. Our representation of sequents also requires the use
136 of ordinary introduction rules. If we had no regard for readability, we
137 could treat the right side more uniformly by representing sequents as
138 \[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
141 \section{Extra rules for the sequent calculus}
142 As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
143 must be replaced by sequent-style elimination rules. In addition, we need
144 rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
145 Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
146 simulates $({\disj}R)$:
147 \[ (\neg Q\Imp P) \Imp P\disj Q \]
148 The destruction rule $({\imp}E)$ is replaced by
149 \[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
150 Quantifier replication also requires special rules. In classical logic,
151 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
152 $(\exists R)$ and $(\forall L)$ are dual:
153 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
154 {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
156 \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
157 {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
159 Thus both kinds of quantifier may be replicated. Theorems requiring
160 multiple uses of a universal formula are easy to invent; consider
161 \[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
162 for any~$n>1$. Natural examples of the multiple use of an existential
163 formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
165 Forgoing quantifier replication loses completeness, but gains decidability,
166 since the search space becomes finite. Many useful theorems can be proved
167 without replication, and the search generally delivers its verdict in a
168 reasonable time. To adopt this approach, represent the sequent rules
169 $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
170 E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
172 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
173 Elim-resolution with this rule will delete the universal formula after a
174 single use. To replicate universal quantifiers, replace the rule by
175 $$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
176 \eqno(\forall E@3) $$
177 To replicate existential quantifiers, replace $(\exists I)$ by
178 \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
179 All introduction rules mentioned above are also useful in swapped form.
181 Replication makes the search space infinite; we must apply the rules with
182 care. The classical reasoner distinguishes between safe and unsafe
183 rules, applying the latter only when there is no alternative. Depth-first
184 search may well go down a blind alley; best-first search is better behaved
185 in an infinite search space. However, quantifier replication is too
186 expensive to prove any but the simplest theorems.
189 \section{Classical rule sets}
190 \index{classical sets}
191 Each automatic tactic takes a {\bf classical set} --- a collection of
192 rules, classified as introduction or elimination and as {\bf safe} or {\bf
193 unsafe}. In general, safe rules can be attempted blindly, while unsafe
194 rules must be used with care. A safe rule must never reduce a provable
195 goal to an unprovable set of subgoals.
197 The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
198 rule is unsafe whose premises contain new unknowns. The elimination
199 rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
200 which discards the assumption $\forall x{.}P(x)$ and replaces it by the
201 weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
202 similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
203 since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
204 In classical first-order logic, all rules are safe except those mentioned
207 The safe/unsafe distinction is vague, and may be regarded merely as a way
208 of giving some rules priority over others. One could argue that
209 $({\disj}E)$ is unsafe, because repeated application of it could generate
210 exponentially many subgoals. Induction rules are unsafe because inductive
211 proofs are difficult to set up automatically. Any inference is unsafe that
212 instantiates an unknown in the proof state --- thus \ttindex{match_tac}
213 must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
214 is unsafe if it instantiates unknowns shared with other subgoals --- thus
215 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
217 \subsection{Adding rules to classical sets}
218 Classical rule sets belong to the abstract type \mltydx{claset}, which
219 supports the following operations (provided the classical reasoner is
223 print_cs : claset -> unit
224 addSIs : claset * thm list -> claset \hfill{\bf infix 4}
225 addSEs : claset * thm list -> claset \hfill{\bf infix 4}
226 addSDs : claset * thm list -> claset \hfill{\bf infix 4}
227 addIs : claset * thm list -> claset \hfill{\bf infix 4}
228 addEs : claset * thm list -> claset \hfill{\bf infix 4}
229 addDs : claset * thm list -> claset \hfill{\bf infix 4}
230 delrules : claset * thm list -> claset \hfill{\bf infix 4}
232 The add operations ignore any rule already present in the claset with the same
233 classification (such as Safe Introduction). They print a warning if the rule
234 has already been added with some other classification, but add the rule
235 anyway. Calling {\tt delrules} deletes all occurrences of a rule from the
236 claset, but see the warning below concerning destruction rules.
237 \begin{ttdescription}
238 \item[\ttindexbold{empty_cs}] is the empty classical set.
240 \item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
242 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
243 adds safe introduction~$rules$ to~$cs$.
245 \item[$cs$ addSEs $rules$] \indexbold{*addSEs}
246 adds safe elimination~$rules$ to~$cs$.
248 \item[$cs$ addSDs $rules$] \indexbold{*addSDs}
249 adds safe destruction~$rules$ to~$cs$.
251 \item[$cs$ addIs $rules$] \indexbold{*addIs}
252 adds unsafe introduction~$rules$ to~$cs$.
254 \item[$cs$ addEs $rules$] \indexbold{*addEs}
255 adds unsafe elimination~$rules$ to~$cs$.
257 \item[$cs$ addDs $rules$] \indexbold{*addDs}
258 adds unsafe destruction~$rules$ to~$cs$.
260 \item[$cs$ delrules $rules$] \indexbold{*delrules}
261 deletes~$rules$ from~$cs$. It prints a warning for those rules that are not
266 If you added $rule$ using {\tt addSDs} or {\tt addDs}, then you must delete
269 \(cs\) delrules [make_elim \(rule\)]
272 This is necessary because the operators {\tt addSDs} and {\tt addDs} convert
273 the destruction rules to elimination rules by applying \ttindex{make_elim},
274 and then insert them using {\tt addSEs} and {\tt addEs}, respectively.
277 Introduction rules are those that can be applied using ordinary resolution.
278 The classical set automatically generates their swapped forms, which will
279 be applied using elim-resolution. Elimination rules are applied using
280 elim-resolution. In a classical set, rules are sorted by the number of new
281 subgoals they will yield; rules that generate the fewest subgoals will be
282 tried first (see \S\ref{biresolve_tac}).
285 \subsection{Modifying the search step}
286 For a given classical set, the proof strategy is simple. Perform as many
287 safe inferences as possible; or else, apply certain safe rules, allowing
288 instantiation of unknowns; or else, apply an unsafe rule. The tactics may
289 also apply {\tt hyp_subst_tac}, if they have been set up to do so (see
290 below). They may perform a form of Modus Ponens: if there are assumptions
291 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
293 The classical reasoning tactics---except {\tt blast_tac}!---allow you to
294 modify this basic proof strategy by
295 applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
296 the search. Usually they are the identity tacticals, but they could apply
297 another tactic before or after the step tactic. The first one, which is
298 considered to be safe, affects \ttindex{safe_step_tac} and all the tactics that
299 call it. The the second one, which may be unsafe, affects
300 \ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call them.
303 addss : claset * simpset -> claset \hfill{\bf infix 4}
304 addSbefore : claset * (int -> tactic) -> claset \hfill{\bf infix 4}
305 addSaltern : claset * (int -> tactic) -> claset \hfill{\bf infix 4}
306 setSWrapper : claset * ((int -> tactic) ->
307 (int -> tactic)) -> claset \hfill{\bf infix 4}
308 compSWrapper : claset * ((int -> tactic) ->
309 (int -> tactic)) -> claset \hfill{\bf infix 4}
310 addbefore : claset * (int -> tactic) -> claset \hfill{\bf infix 4}
311 addaltern : claset * (int -> tactic) -> claset \hfill{\bf infix 4}
312 setWrapper : claset * ((int -> tactic) ->
313 (int -> tactic)) -> claset \hfill{\bf infix 4}
314 compWrapper : claset * ((int -> tactic) ->
315 (int -> tactic)) -> claset \hfill{\bf infix 4}
318 \index{simplification!from classical reasoner}
319 The wrapper tacticals underly the operator \ttindex{addss}, which combines
320 each search step by simplification. Strictly speaking, {\tt addss} is not
321 part of the classical reasoner. It should be defined (using {\tt addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is installed.
323 \begin{ttdescription}
324 \item[$cs$ addss $ss$] \indexbold{*addss}
325 adds the simpset~$ss$ to the classical set. The assumptions and goal will be
326 simplified, in a safe way, after the safe steps of the search.
328 \item[$cs$ addSbefore $tac$] \indexbold{*addSbefore}
329 changes the safe wrapper tactical to apply the given tactic {\em before}
330 each safe step of the search.
332 \item[$cs$ addSaltern $tac$] \indexbold{*addSaltern}
333 changes the safe wrapper tactical to apply the given tactic when a safe step
334 of the search would fail.
336 \item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper}
337 specifies a new safe wrapper tactical.
339 \item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper}
340 composes the $tactical$ with the existing safe wrapper tactical,
341 to combine their effects.
343 \item[$cs$ addbefore $tac$] \indexbold{*addbefore}
344 changes the (unsafe) wrapper tactical to apply the given tactic, which should
345 be safe, {\em before} each step of the search.
347 \item[$cs$ addaltern $tac$] \indexbold{*addaltern}
348 changes the (unsafe) wrapper tactical to apply the given tactic
349 {\em alternatively} after each step of the search.
351 \item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper}
352 specifies a new (unsafe) wrapper tactical.
354 \item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper}
355 composes the $tactical$ with the existing (unsafe) wrapper tactical,
356 to combine their effects.
360 \section{The classical tactics}
361 \index{classical reasoner!tactics}
362 If installed, the classical module provides several tactics (and other
363 operations) for simulating the classical sequent calculus.
365 \subsection{The automatic tableau prover}
366 The tactic {\tt blast_tac} finds a proof rapidly using a separate tableau
367 prover and then reconstructs the proof using Isabelle tactics. It is much
368 faster and more powerful than the other classical reasoning tactics, but has
369 major limitations too.
371 \item It does not use the wrapper tacticals described above, such as
373 \item It ignores types, which can cause problems in \HOL. If it applies a rule
374 whose types are inappropriate, then proof reconstruction will fail.
375 \item It does not perform higher-order unification, as needed by the rule {\tt
376 rangeI} in {\HOL} and {\tt RepFunI} in {\ZF}. There are often
377 alternatives to such rules, for example {\tt
378 range_eqI} and {\tt RepFun_eqI}.
379 \item The message {\small\tt Function Var's argument not a bound variable\ }
380 relates to the lack of higher-order unification. Function variables
381 may only be applied to parameters of the subgoal.
382 \item Its proof strategy is more general than {\tt fast_tac}'s but can be
383 slower. If {\tt blast_tac} fails or seems to be running forever, try {\tt
384 fast_tac} and the other tactics described below.
388 blast_tac : claset -> int -> tactic
389 Blast.depth_tac : claset -> int -> int -> tactic
390 Blast.trace : bool ref \hfill{\bf initially false}
392 The two tactics differ on how they bound the number of unsafe steps used in a
393 proof. While {\tt blast_tac} starts with a bound of zero and increases it
394 successively to~20, {\tt Blast.depth_tac} applies a user-supplied search bound.
395 \begin{ttdescription}
396 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
397 subgoal~$i$ using iterative deepening to increase the search bound.
399 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
400 to prove subgoal~$i$ using a search bound of $lim$. Often a slow
401 proof using {\tt blast_tac} can be made much faster by supplying the
402 successful search bound to this tactic instead.
404 \item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}
405 causes the tableau prover to print a trace of its search. At each step it
406 displays the formula currently being examined and reports whether the branch
407 has been closed, extended or split.
410 \subsection{The automatic tactics}
412 fast_tac : claset -> int -> tactic
413 best_tac : claset -> int -> tactic
414 slow_tac : claset -> int -> tactic
415 slow_best_tac : claset -> int -> tactic
417 These tactics work by applying {\tt step_tac} or {\tt slow_step_tac}
418 repeatedly. Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal;
419 they either prove this subgoal or fail. The {\tt slow_} versions are more
420 powerful but can be much slower.
422 The best-first tactics are guided by a heuristic function: typically, the
423 total size of the proof state. This function is supplied in the functor call
424 that sets up the classical reasoner.
425 \begin{ttdescription}
426 \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
427 depth-first search, to prove subgoal~$i$.
429 \item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
430 best-first search, to prove subgoal~$i$.
432 \item[\ttindexbold{slow_tac} $cs$ $i$] applies {\tt slow_step_tac} using
433 depth-first search, to prove subgoal~$i$.
435 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies {\tt slow_step_tac} using
436 best-first search, to prove subgoal~$i$.
440 \subsection{Depth-limited tactics}
442 depth_tac : claset -> int -> int -> tactic
443 deepen_tac : claset -> int -> int -> tactic
445 These work by exhaustive search up to a specified depth. Unsafe rules are
446 modified to preserve the formula they act on, so that it be used repeatedly.
447 They can prove more goals than {\tt fast_tac} can but are much
448 slower, for example if the assumptions have many universal quantifiers.
450 The depth limits the number of unsafe steps. If you can estimate the minimum
451 number of unsafe steps needed, supply this value as~$m$ to save time.
452 \begin{ttdescription}
453 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
454 tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
456 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
457 tries to prove subgoal~$i$ by iterative deepening. It calls {\tt depth_tac}
458 repeatedly with increasing depths, starting with~$m$.
462 \subsection{Single-step tactics}
464 safe_step_tac : claset -> int -> tactic
465 safe_tac : claset -> tactic
466 inst_step_tac : claset -> int -> tactic
467 step_tac : claset -> int -> tactic
468 slow_step_tac : claset -> int -> tactic
470 The automatic proof procedures call these tactics. By calling them
471 yourself, you can execute these procedures one step at a time.
472 \begin{ttdescription}
473 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
474 subgoal~$i$. The safe wrapper tactical is applied to a tactic that may include
475 proof by assumption or Modus Ponens (taking care not to instantiate unknowns),
476 or {\tt hyp_subst_tac}.
478 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
479 subgoals. It is deterministic, with at most one outcome. If the automatic
480 tactics fail, try using {\tt safe_tac} to open up your formula; then you
481 can replicate certain quantifiers explicitly by applying appropriate rules.
483 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
484 but allows unknowns to be instantiated.
486 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
487 procedure. The (unsafe) wrapper tactical is applied to a tactic that tries
488 {\tt safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
490 \item[\ttindexbold{slow_step_tac}]
491 resembles {\tt step_tac}, but allows backtracking between using safe
492 rules with instantiation ({\tt inst_step_tac}) and using unsafe rules.
493 The resulting search space is larger.
496 \subsection{The current claset}
497 Some logics (\FOL, {\HOL} and \ZF) support the concept of a current
498 claset\index{claset!current}. This is a default set of classical rules. The
499 underlying idea is quite similar to that of a current simpset described in
500 \S\ref{sec:simp-for-dummies}; please read that section, including its
501 warnings. Just like simpsets, clasets can be associated with theories. The
504 Blast_tac : int -> tactic
505 Fast_tac : int -> tactic
506 Best_tac : int -> tactic
507 Deepen_tac : int -> int -> tactic
508 Step_tac : int -> tactic
510 \indexbold{*Blast_tac}\indexbold{*Best_tac}\indexbold{*Fast_tac}%
511 \indexbold{*Deepen_tac}\indexbold{*Step_tac}
512 make use of the current claset. E.g. {\tt Blast_tac} is defined as follows:
514 fun Blast_tac i = fast_tac (!claset) i;
516 where \ttindex{!claset} is the current claset.
519 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
521 \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
522 \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
523 are used to add rules to the current claset. They work exactly like their
524 lower case counterparts {\tt addSIs} etc.
526 Delrules : thm list -> unit
528 deletes rules from the current claset. You do not need to worry via which of
529 the above {\tt Add} functions the rule was initially added.
531 \subsection{Other useful tactics}
532 \index{tactics!for contradiction}
533 \index{tactics!for Modus Ponens}
535 contr_tac : int -> tactic
536 mp_tac : int -> tactic
537 eq_mp_tac : int -> tactic
538 swap_res_tac : thm list -> int -> tactic
540 These can be used in the body of a specialized search.
541 \begin{ttdescription}
542 \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
543 solves subgoal~$i$ by detecting a contradiction among two assumptions of
544 the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The
545 tactic can produce multiple outcomes, enumerating all possible
548 \item[\ttindexbold{mp_tac} {\it i}]
549 is like {\tt contr_tac}, but also attempts to perform Modus Ponens in
550 subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
551 $P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
554 \item[\ttindexbold{eq_mp_tac} {\it i}]
555 is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
558 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
559 the proof state using {\it thms}, which should be a list of introduction
560 rules. First, it attempts to prove the goal using {\tt assume_tac} or
561 {\tt contr_tac}. It then attempts to apply each rule in turn, attempting
562 resolution and also elim-resolution with the swapped form.
565 \subsection{Creating swapped rules}
567 swapify : thm list -> thm list
568 joinrules : thm list * thm list -> (bool * thm) list
570 \begin{ttdescription}
571 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
572 swapped versions of~{\it thms}, regarded as introduction rules.
574 \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
575 joins introduction rules, their swapped versions, and elimination rules for
576 use with \ttindex{biresolve_tac}. Each rule is paired with~{\tt false}
577 (indicating ordinary resolution) or~{\tt true} (indicating
582 \section{Setting up the classical reasoner}
583 \index{classical reasoner!setting up}
584 Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
585 the classical reasoner already set up. When defining a new classical logic,
586 you should set up the reasoner yourself. It consists of the \ML{} functor
587 \ttindex{ClassicalFun}, which takes the argument
588 signature {\tt CLASSICAL_DATA}:
590 signature CLASSICAL_DATA =
595 val sizef : thm -> int
596 val hyp_subst_tacs : (int -> tactic) list
599 Thus, the functor requires the following items:
600 \begin{ttdescription}
601 \item[\tdxbold{mp}] should be the Modus Ponens rule
602 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
604 \item[\tdxbold{not_elim}] should be the contradiction rule
605 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
607 \item[\tdxbold{swap}] should be the swap rule
608 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
610 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
611 search. It should estimate the size of the remaining subgoals. A good
612 heuristic function is \ttindex{size_of_thm}, which measures the size of the
613 proof state. Another size function might ignore certain subgoals (say,
614 those concerned with type checking). A heuristic function might simply
617 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
618 the hypotheses, typically created by \ttindex{HypsubstFun} (see
619 Chapter~\ref{substitution}). This list can, of course, be empty. The
620 tactics are assumed to be safe!
622 The functor is not at all sensitive to the formalization of the
623 object-logic. It does not even examine the rules, but merely applies them
624 according to its fixed strategy. The functor resides in {\tt
625 Provers/classical.ML} in the Isabelle distribution directory.
627 \index{classical reasoner|)}