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 of
7 classical first-order logic. Isabelle's set theory~ZF is built upon
8 theory~FOL, while HOL conceptually contains first-order logic as a fragment.
9 Theorem-proving in predicate logic is undecidable, but many researchers have
10 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 We shall first discuss the underlying principles, then present the classical
32 reasoner. Finally, we shall see how to instantiate it for new logics. The
33 logics FOL, ZF, HOL and HOLCF have it already installed.
36 \section{The sequent calculus}
37 \index{sequent calculus}
38 Isabelle supports natural deduction, which is easy to use for interactive
39 proof. But natural deduction does not easily lend itself to automation,
40 and has a bias towards intuitionism. For certain proofs in classical
41 logic, it can not be called natural. The {\bf sequent calculus}, a
42 generalization of natural deduction, is easier to automate.
44 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
45 and~$\Delta$ are sets of formulae.%
46 \footnote{For first-order logic, sequents can equivalently be made from
47 lists or multisets of formulae.} The sequent
48 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
49 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
50 Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
51 while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf
52 basic} if its left and right sides have a common formula, as in $P,Q\turn
53 Q,R$; basic sequents are trivially valid.
55 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
56 side of the $\turn$~symbol they operate on. Rules that operate on the
57 right side are analogous to natural deduction's introduction rules, and
58 left rules are analogous to elimination rules.
59 Recall the natural deduction rules for
61 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
62 {Fig.\ts\ref{fol-fig}}.
63 The sequent calculus analogue of~$({\imp}I)$ is the rule
65 \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
68 This breaks down some implication on the right side of a sequent; $\Gamma$
69 and $\Delta$ stand for the sets of formulae that are unaffected by the
70 inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
73 \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
76 This breaks down some disjunction on the right side, replacing it by both
77 disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
79 To illustrate the use of multiple formulae on the right, let us prove
80 the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we
81 reduce this formula to a basic sequent:
82 \[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
83 {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
84 {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
85 {P, Q \turn Q, P\qquad\qquad}}}
87 This example is typical of the sequent calculus: start with the desired
88 theorem and apply rules backwards in a fairly arbitrary manner. This yields a
89 surprisingly effective proof procedure. Quantifiers add few complications,
90 since Isabelle handles parameters and schematic variables. See Chapter~10
91 of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further
95 \section{Simulating sequents by natural deduction}
96 Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@.
97 But natural deduction is easier to work with, and most object-logics employ
98 it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
99 Q@1,\ldots,Q@n$ by the Isabelle formula
100 \[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
101 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
102 Elim-resolution plays a key role in simulating sequent proofs.
104 We can easily handle reasoning on the left.
106 \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{{\S}\ref{destruct}},
107 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
108 achieves a similar effect as the corresponding sequent rules. For the
109 other connectives, we use sequent-style elimination rules instead of
110 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
111 the rule $(\neg L)$ has no effect under our representation of sequents!
113 \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)
115 What about reasoning on the right? Introduction rules can only affect the
116 formula in the conclusion, namely~$Q@1$. The other right-side formulae are
117 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.
118 \index{assumptions!negated}
119 In order to operate on one of these, it must first be exchanged with~$Q@1$.
120 Elim-resolution with the {\bf swap} rule has this effect:
121 $$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$
122 To ensure that swaps occur only when necessary, each introduction rule is
123 converted into a swapped form: it is resolved with the second premise
124 of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
125 called~$({\neg\conj}E)$, is
126 \[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
127 Similarly, the swapped form of~$({\imp}I)$ is
128 \[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \]
129 Swapped introduction rules are applied using elim-resolution, which deletes
130 the negated formula. Our representation of sequents also requires the use
131 of ordinary introduction rules. If we had no regard for readability, we
132 could treat the right side more uniformly by representing sequents as
133 \[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
136 \section{Extra rules for the sequent calculus}
137 As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
138 must be replaced by sequent-style elimination rules. In addition, we need
139 rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
140 Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
141 simulates $({\disj}R)$:
142 \[ (\neg Q\Imp P) \Imp P\disj Q \]
143 The destruction rule $({\imp}E)$ is replaced by
144 \[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
145 Quantifier replication also requires special rules. In classical logic,
146 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
147 $(\exists R)$ and $(\forall L)$ are dual:
148 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
149 {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
151 \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
152 {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
154 Thus both kinds of quantifier may be replicated. Theorems requiring
155 multiple uses of a universal formula are easy to invent; consider
156 \[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
157 for any~$n>1$. Natural examples of the multiple use of an existential
158 formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
160 Forgoing quantifier replication loses completeness, but gains decidability,
161 since the search space becomes finite. Many useful theorems can be proved
162 without replication, and the search generally delivers its verdict in a
163 reasonable time. To adopt this approach, represent the sequent rules
164 $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
165 E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
167 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
168 Elim-resolution with this rule will delete the universal formula after a
169 single use. To replicate universal quantifiers, replace the rule by
171 \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
174 To replicate existential quantifiers, replace $(\exists I)$ by
175 \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
176 All introduction rules mentioned above are also useful in swapped form.
178 Replication makes the search space infinite; we must apply the rules with
179 care. The classical reasoner distinguishes between safe and unsafe
180 rules, applying the latter only when there is no alternative. Depth-first
181 search may well go down a blind alley; best-first search is better behaved
182 in an infinite search space. However, quantifier replication is too
183 expensive to prove any but the simplest theorems.
186 \section{Classical rule sets}
187 \index{classical sets}
188 Each automatic tactic takes a {\bf classical set} --- a collection of
189 rules, classified as introduction or elimination and as {\bf safe} or {\bf
190 unsafe}. In general, safe rules can be attempted blindly, while unsafe
191 rules must be used with care. A safe rule must never reduce a provable
192 goal to an unprovable set of subgoals.
194 The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
195 rule is unsafe whose premises contain new unknowns. The elimination
196 rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
197 which discards the assumption $\forall x{.}P(x)$ and replaces it by the
198 weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
199 similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
200 since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
201 In classical first-order logic, all rules are safe except those mentioned
204 The safe/unsafe distinction is vague, and may be regarded merely as a way
205 of giving some rules priority over others. One could argue that
206 $({\disj}E)$ is unsafe, because repeated application of it could generate
207 exponentially many subgoals. Induction rules are unsafe because inductive
208 proofs are difficult to set up automatically. Any inference is unsafe that
209 instantiates an unknown in the proof state --- thus \ttindex{match_tac}
210 must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
211 is unsafe if it instantiates unknowns shared with other subgoals --- thus
212 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
214 \subsection{Adding rules to classical sets}
215 Classical rule sets belong to the abstract type \mltydx{claset}, which
216 supports the following operations (provided the classical reasoner is
220 print_cs : claset -> unit
221 rep_cs : claset -> \{safeEs: thm list, safeIs: thm list,
222 hazEs: thm list, hazIs: thm list,
223 swrappers: (string * wrapper) list,
224 uwrappers: (string * wrapper) list,
225 safe0_netpair: netpair, safep_netpair: netpair,
226 haz_netpair: netpair, dup_netpair: netpair\}
227 addSIs : claset * thm list -> claset \hfill{\bf infix 4}
228 addSEs : claset * thm list -> claset \hfill{\bf infix 4}
229 addSDs : claset * thm list -> claset \hfill{\bf infix 4}
230 addIs : claset * thm list -> claset \hfill{\bf infix 4}
231 addEs : claset * thm list -> claset \hfill{\bf infix 4}
232 addDs : claset * thm list -> claset \hfill{\bf infix 4}
233 delrules : claset * thm list -> claset \hfill{\bf infix 4}
235 The add operations ignore any rule already present in the claset with the same
236 classification (such as safe introduction). They print a warning if the rule
237 has already been added with some other classification, but add the rule
238 anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the
239 claset, but see the warning below concerning destruction rules.
240 \begin{ttdescription}
241 \item[\ttindexbold{empty_cs}] is the empty classical set.
243 \item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,
244 which is the rules. All other parts are non-printable.
246 \item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal
247 components, namely the safe introduction and elimination rules, the unsafe
248 introduction and elimination rules, the lists of safe and unsafe wrappers
249 (see \ref{sec:modifying-search}), and the internalized forms of the rules.
251 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
252 adds safe introduction~$rules$ to~$cs$.
254 \item[$cs$ addSEs $rules$] \indexbold{*addSEs}
255 adds safe elimination~$rules$ to~$cs$.
257 \item[$cs$ addSDs $rules$] \indexbold{*addSDs}
258 adds safe destruction~$rules$ to~$cs$.
260 \item[$cs$ addIs $rules$] \indexbold{*addIs}
261 adds unsafe introduction~$rules$ to~$cs$.
263 \item[$cs$ addEs $rules$] \indexbold{*addEs}
264 adds unsafe elimination~$rules$ to~$cs$.
266 \item[$cs$ addDs $rules$] \indexbold{*addDs}
267 adds unsafe destruction~$rules$ to~$cs$.
269 \item[$cs$ delrules $rules$] \indexbold{*delrules}
270 deletes~$rules$ from~$cs$. It prints a warning for those rules that are not
275 If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete
278 \(cs\) delrules [make_elim \(rule\)]
281 This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert
282 the destruction rules to elimination rules by applying \ttindex{make_elim},
283 and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.
286 Introduction rules are those that can be applied using ordinary resolution.
287 The classical set automatically generates their swapped forms, which will
288 be applied using elim-resolution. Elimination rules are applied using
289 elim-resolution. In a classical set, rules are sorted by the number of new
290 subgoals they will yield; rules that generate the fewest subgoals will be
291 tried first (see {\S}\ref{biresolve_tac}).
293 For elimination and destruction rules there are variants of the add operations
294 adding a rule in a way such that it is applied only if also its second premise
295 can be unified with an assumption of the current proof state:
296 \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}
298 addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
299 addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
300 addE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
301 addD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
304 A rule to be added in this special way must be given a name, which is used
305 to delete it again -- when desired -- using \texttt{delSWrappers} or
306 \texttt{delWrappers}, respectively. This is because these add operations
307 are implemented as wrappers (see \ref{sec:modifying-search} below).
311 \subsection{Modifying the search step}
312 \label{sec:modifying-search}
313 For a given classical set, the proof strategy is simple. Perform as many safe
314 inferences as possible; or else, apply certain safe rules, allowing
315 instantiation of unknowns; or else, apply an unsafe rule. The tactics also
316 eliminate assumptions of the form $x=t$ by substitution if they have been set
317 up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below).
318 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
319 and~$P$, then replace $P\imp Q$ by~$Q$.
321 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
322 you to modify this basic proof strategy by applying two lists of arbitrary
323 {\bf wrapper tacticals} to it.
324 The first wrapper list, which is considered to contain safe wrappers only,
325 affects \ttindex{safe_step_tac} and all the tactics that call it.
326 The second one, which may contain unsafe wrappers, affects the unsafe parts
327 of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
328 A wrapper transforms each step of the search, for example
329 by attempting other tactics before or after the original step tactic.
330 All members of a wrapper list are applied in turn to the respective step tactic.
332 Initially the two wrapper lists are empty, which means no modification of the
333 step tactics. Safe and unsafe wrappers are added to a claset
334 with the functions given below, supplying them with wrapper names.
335 These names may be used to selectively delete wrappers.
338 type wrapper = (int -> tactic) -> (int -> tactic);
340 addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
341 addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
342 addSafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
343 delSWrapper : claset * string -> claset \hfill{\bf infix 4}
345 addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
346 addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
347 addafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
348 delWrapper : claset * string -> claset \hfill{\bf infix 4}
350 addSss : claset * simpset -> claset \hfill{\bf infix 4}
351 addss : claset * simpset -> claset \hfill{\bf infix 4}
355 \begin{ttdescription}
356 \item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
357 adds a new wrapper, which should yield a safe tactic,
358 to modify the existing safe step tactic.
360 \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
361 adds the given tactic as a safe wrapper, such that it is tried
362 {\em before} each safe step of the search.
364 \item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
365 adds the given tactic as a safe wrapper, such that it is tried
366 when a safe step of the search would fail.
368 \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
369 deletes the safe wrapper with the given name.
371 \item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
372 adds a new wrapper to modify the existing (unsafe) step tactic.
374 \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
375 adds the given tactic as an unsafe wrapper, such that it its result is
376 concatenated {\em before} the result of each unsafe step.
378 \item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
379 adds the given tactic as an unsafe wrapper, such that it its result is
380 concatenated {\em after} the result of each unsafe step.
382 \item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
383 deletes the unsafe wrapper with the given name.
385 \item[$cs$ addSss $ss$] \indexbold{*addss}
386 adds the simpset~$ss$ to the classical set. The assumptions and goal will be
387 simplified, in a rather safe way, after each safe step of the search.
389 \item[$cs$ addss $ss$] \indexbold{*addss}
390 adds the simpset~$ss$ to the classical set. The assumptions and goal will be
391 simplified, before the each unsafe step of the search.
395 \index{simplification!from classical reasoner}
396 Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
397 are not part of the classical reasoner.
398 , which are used as primitives
399 for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
400 implemented as wrapper tacticals.
403 Being defined as wrappers, these operators are inappropriate for adding more
404 than one simpset at a time: the simpset added last overwrites any earlier ones.
405 When a simpset combined with a claset is to be augmented, this should done
406 {\em before} combining it with the claset.
410 \section{The classical tactics}
411 \index{classical reasoner!tactics} If installed, the classical module provides
412 powerful theorem-proving tactics. Most of them have capitalized analogues
413 that use the default claset; see {\S}\ref{sec:current-claset}.
416 \subsection{The tableau prover}
417 The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
418 coded directly in \ML. It then reconstructs the proof using Isabelle
419 tactics. It is faster and more powerful than the other classical
420 reasoning tactics, but has major limitations too.
422 \item It does not use the wrapper tacticals described above, such as
424 \item It ignores types, which can cause problems in HOL. If it applies a rule
425 whose types are inappropriate, then proof reconstruction will fail.
426 \item It does not perform higher-order unification, as needed by the rule {\tt
427 rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives
428 to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
429 \item Function variables may only be applied to parameters of the subgoal.
430 (This restriction arises because the prover does not use higher-order
431 unification.) If other function variables are present then the prover will
432 fail with the message {\small\tt Function Var's argument not a bound variable}.
433 \item Its proof strategy is more general than \texttt{fast_tac}'s but can be
434 slower. If \texttt{blast_tac} fails or seems to be running forever, try {\tt
435 fast_tac} and the other tactics described below.
439 blast_tac : claset -> int -> tactic
440 Blast.depth_tac : claset -> int -> int -> tactic
441 Blast.trace : bool ref \hfill{\bf initially false}
443 The two tactics differ on how they bound the number of unsafe steps used in a
444 proof. While \texttt{blast_tac} starts with a bound of zero and increases it
445 successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
446 \begin{ttdescription}
447 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
448 subgoal~$i$, increasing the search bound using iterative
449 deepening~\cite{korf85}.
451 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
452 to prove subgoal~$i$ using a search bound of $lim$. Sometimes 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{Automatic tactics}\label{sec:automatic-tactics}
465 type clasimpset = claset * simpset;
466 auto_tac : clasimpset -> tactic
467 force_tac : clasimpset -> int -> tactic
471 The automatic tactics attempt to prove goals using a combination of
472 simplification and classical reasoning.
473 \begin{ttdescription}
474 \item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where
475 there are a lot of mostly trivial subgoals; it proves all the easy ones,
476 leaving the ones it cannot prove.
477 (Unfortunately, attempting to prove the hard ones may take a long time.)
478 \item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$
479 completely. It tries to apply all fancy tactics it knows about,
480 performing a rather exhaustive search.
482 They must be supplied both a simpset and a claset; therefore
483 they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which
484 use the default claset and simpset (see {\S}\ref{sec:current-claset} below).
486 the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;}
487 while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
490 \subsection{Semi-automatic tactics}
492 clarify_tac : claset -> int -> tactic
493 clarify_step_tac : claset -> int -> tactic
494 clarsimp_tac : clasimpset -> int -> tactic
496 Use these when the automatic tactics fail. They perform all the obvious
497 logical inferences that do not split the subgoal. The result is a
498 simpler subgoal that can be tackled by other means, such as by
499 instantiating quantifiers yourself.
500 \begin{ttdescription}
501 \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
502 subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
503 \item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
504 subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
505 B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
506 performed provided they do not instantiate unknowns. Assumptions of the
507 form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
509 \item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
510 also does simplification with the given simpset. Note that if the simpset
511 includes a splitter for the premises, the subgoal may still be split.
515 \subsection{Other classical tactics}
517 fast_tac : claset -> int -> tactic
518 best_tac : claset -> int -> tactic
519 slow_tac : claset -> int -> tactic
520 slow_best_tac : claset -> int -> tactic
522 These tactics attempt to prove a subgoal using sequent-style reasoning.
523 Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their
524 effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
525 this subgoal or fail. The \texttt{slow_} versions conduct a broader
527 \footnote{They may, when backtracking from a failed proof attempt, undo even
528 the step of proving a subgoal by assumption.}
530 The best-first tactics are guided by a heuristic function: typically, the
531 total size of the proof state. This function is supplied in the functor call
532 that sets up the classical reasoner.
533 \begin{ttdescription}
534 \item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
535 depth-first search to prove subgoal~$i$.
537 \item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
538 best-first search to prove subgoal~$i$.
540 \item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
541 depth-first search to prove subgoal~$i$.
543 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
544 best-first search to prove subgoal~$i$.
548 \subsection{Depth-limited automatic tactics}
550 depth_tac : claset -> int -> int -> tactic
551 deepen_tac : claset -> int -> int -> tactic
553 These work by exhaustive search up to a specified depth. Unsafe rules are
554 modified to preserve the formula they act on, so that it be used repeatedly.
555 They can prove more goals than \texttt{fast_tac} can but are much
556 slower, for example if the assumptions have many universal quantifiers.
558 The depth limits the number of unsafe steps. If you can estimate the minimum
559 number of unsafe steps needed, supply this value as~$m$ to save time.
560 \begin{ttdescription}
561 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
562 tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
564 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
565 tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac}
566 repeatedly with increasing depths, starting with~$m$.
570 \subsection{Single-step tactics}
572 safe_step_tac : claset -> int -> tactic
573 safe_tac : claset -> tactic
574 inst_step_tac : claset -> int -> tactic
575 step_tac : claset -> int -> tactic
576 slow_step_tac : claset -> int -> tactic
578 The automatic proof procedures call these tactics. By calling them
579 yourself, you can execute these procedures one step at a time.
580 \begin{ttdescription}
581 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
582 subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may
583 include proof by assumption or Modus Ponens (taking care not to instantiate
584 unknowns), or substitution.
586 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
587 subgoals. It is deterministic, with at most one outcome.
589 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
590 but allows unknowns to be instantiated.
592 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
593 procedure. The unsafe wrapper tacticals are applied to a tactic that tries
594 \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
597 \item[\ttindexbold{slow_step_tac}]
598 resembles \texttt{step_tac}, but allows backtracking between using safe
599 rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
600 The resulting search space is larger.
604 \subsection{The current claset}\label{sec:current-claset}
606 Each theory is equipped with an implicit \emph{current claset}
607 \index{claset!current}. This is a default set of classical
608 rules. The underlying idea is quite similar to that of a current
609 simpset described in {\S}\ref{sec:simp-for-dummies}; please read that
610 section, including its warnings.
614 Blast_tac : int -> tactic
616 Force_tac : int -> tactic
617 Fast_tac : int -> tactic
618 Best_tac : int -> tactic
619 Deepen_tac : int -> int -> tactic
620 Clarify_tac : int -> tactic
621 Clarify_step_tac : int -> tactic
622 Clarsimp_tac : int -> tactic
624 Safe_step_tac : int -> tactic
625 Step_tac : int -> tactic
627 \indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac}
628 \indexbold{*Best_tac}\indexbold{*Fast_tac}%
629 \indexbold{*Deepen_tac}
630 \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac}
631 \indexbold{*Safe_tac}\indexbold{*Safe_step_tac}
632 \indexbold{*Step_tac}
633 make use of the current claset. For example, \texttt{Blast_tac} is defined as
635 fun Blast_tac i st = blast_tac (claset()) i st;
637 and gets the current claset, only after it is applied to a proof state.
640 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
642 \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
643 \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
644 are used to add rules to the current claset. They work exactly like their
645 lower case counterparts, such as \texttt{addSIs}. Calling
647 Delrules : thm list -> unit
649 deletes rules from the current claset.
652 \subsection{Accessing the current claset}
653 \label{sec:access-current-claset}
655 the functions to access the current claset are analogous to the functions
656 for the current simpset, so please see \ref{sec:access-current-simpset}
659 claset : unit -> claset
660 claset_ref : unit -> claset ref
661 claset_of : theory -> claset
662 claset_ref_of : theory -> claset ref
663 print_claset : theory -> unit
664 CLASET :(claset -> tactic) -> tactic
665 CLASET' :(claset -> 'a -> tactic) -> 'a -> tactic
666 CLASIMPSET :(clasimpset -> tactic) -> tactic
667 CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
671 \subsection{Other useful tactics}
672 \index{tactics!for contradiction}
673 \index{tactics!for Modus Ponens}
675 contr_tac : int -> tactic
676 mp_tac : int -> tactic
677 eq_mp_tac : int -> tactic
678 swap_res_tac : thm list -> int -> tactic
680 These can be used in the body of a specialized search.
681 \begin{ttdescription}
682 \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
683 solves subgoal~$i$ by detecting a contradiction among two assumptions of
684 the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The
685 tactic can produce multiple outcomes, enumerating all possible
688 \item[\ttindexbold{mp_tac} {\it i}]
689 is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
690 subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
691 $P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
694 \item[\ttindexbold{eq_mp_tac} {\it i}]
695 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
698 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
699 the proof state using {\it thms}, which should be a list of introduction
700 rules. First, it attempts to prove the goal using \texttt{assume_tac} or
701 \texttt{contr_tac}. It then attempts to apply each rule in turn, attempting
702 resolution and also elim-resolution with the swapped form.
705 \subsection{Creating swapped rules}
707 swapify : thm list -> thm list
708 joinrules : thm list * thm list -> (bool * thm) list
710 \begin{ttdescription}
711 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
712 swapped versions of~{\it thms}, regarded as introduction rules.
714 \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
715 joins introduction rules, their swapped versions, and elimination rules for
716 use with \ttindex{biresolve_tac}. Each rule is paired with~\texttt{false}
717 (indicating ordinary resolution) or~\texttt{true} (indicating
722 \section{Setting up the classical reasoner}\label{sec:classical-setup}
723 \index{classical reasoner!setting up}
724 Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL},
725 have the classical reasoner already set up.
726 When defining a new classical logic, you should set up the reasoner yourself.
727 It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the
728 argument signature \texttt{CLASSICAL_DATA}:
730 signature CLASSICAL_DATA =
735 val sizef : thm -> int
736 val hyp_subst_tacs : (int -> tactic) list
739 Thus, the functor requires the following items:
740 \begin{ttdescription}
741 \item[\tdxbold{mp}] should be the Modus Ponens rule
742 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
744 \item[\tdxbold{not_elim}] should be the contradiction rule
745 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
747 \item[\tdxbold{swap}] should be the swap rule
748 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
750 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
751 search. It should estimate the size of the remaining subgoals. A good
752 heuristic function is \ttindex{size_of_thm}, which measures the size of the
753 proof state. Another size function might ignore certain subgoals (say,
754 those concerned with type-checking). A heuristic function might simply
757 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
758 the hypotheses, typically created by \ttindex{HypsubstFun} (see
759 Chapter~\ref{substitution}). This list can, of course, be empty. The
760 tactics are assumed to be safe!
762 The functor is not at all sensitive to the formalization of the
763 object-logic. It does not even examine the rules, but merely applies
764 them according to its fixed strategy. The functor resides in {\tt
765 Provers/classical.ML} in the Isabelle sources.
767 \index{classical reasoner|)}
769 \section{Setting up the combination with the simplifier}
770 \label{sec:clasimp-setup}
772 To combine the classical reasoner and the simplifier, we simply call the
773 \ML{} functor \ttindex{ClasimpFun} that assembles the parts as required.
774 It takes a structure (of signature \texttt{CLASIMP_DATA}) as
775 argment, which can be contructed on the fly:
777 structure Clasimp = ClasimpFun
778 (structure Simplifier = Simplifier
779 and Classical = Classical
785 %%% TeX-master: "ref"