4 Tacticals are operations on tactics. Their implementation makes use of
5 functional programming techniques, especially for sequences. Most of the
6 time, you may forget about this and regard tacticals as high-level control
9 \section{The basic tacticals}
10 \subsection{Joining two tactics}
11 \index{tacticals!joining two tactics}
12 The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and
13 alternation, underlie most of the other control structures in Isabelle.
14 {\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of
17 THEN : tactic * tactic -> tactic \hfill{\bf infix 1}
18 ORELSE : tactic * tactic -> tactic \hfill{\bf infix}
19 APPEND : tactic * tactic -> tactic \hfill{\bf infix}
20 INTLEAVE : tactic * tactic -> tactic \hfill{\bf infix}
23 \item[$tac@1$ \ttindexbold{THEN} $tac@2$]
24 is the sequential composition of the two tactics. Applied to a proof
25 state, it returns all states reachable in two steps by applying $tac@1$
26 followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a
27 sequence of next states; then, it applies $tac@2$ to each of these and
28 concatenates the results.
30 \item[$tac@1$ \ttindexbold{ORELSE} $tac@2$]
31 makes a choice between the two tactics. Applied to a state, it
32 tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it
33 uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then
36 \item[$tac@1$ \ttindexbold{APPEND} $tac@2$]
37 concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment
38 to either tactic, {\tt APPEND} helps avoid incompleteness during
41 \item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$]
42 interleaves the results of $tac@1$ and~$tac@2$. Thus, it includes all
43 possible next states, even if one of the tactics returns an infinite
48 \subsection{Joining a list of tactics}
49 \index{tacticals!joining a list of tactics}
51 EVERY : tactic list -> tactic
52 FIRST : tactic list -> tactic
54 {\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and
57 \item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}]
58 abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}. It is useful for
59 writing a series of tactics to be executed in sequence.
61 \item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}]
62 abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}. It is useful for
63 writing a series of tactics to be attempted one after another.
67 \subsection{Repetition tacticals}
68 \index{tacticals!repetition}
70 TRY : tactic -> tactic
71 REPEAT_DETERM : tactic -> tactic
72 REPEAT : tactic -> tactic
73 REPEAT1 : tactic -> tactic
74 trace_REPEAT : bool ref \hfill{\bf initially false}
77 \item[\ttindexbold{TRY} {\it tac}]
78 applies {\it tac\/} to the proof state and returns the resulting sequence,
79 if non-empty; otherwise it returns the original state. Thus, it applies
80 {\it tac\/} at most once.
82 \item[\ttindexbold{REPEAT_DETERM} {\it tac}]
83 applies {\it tac\/} to the proof state and, recursively, to the head of the
84 resulting sequence. It returns the first state to make {\it tac\/} fail.
85 It is deterministic, discarding alternative outcomes.
87 \item[\ttindexbold{REPEAT} {\it tac}]
88 applies {\it tac\/} to the proof state and, recursively, to each element of
89 the resulting sequence. The resulting sequence consists of those states
90 that make {\it tac\/} fail. Thus, it applies {\it tac\/} as many times as
91 possible (including zero times), and allows backtracking over each
92 invocation of {\it tac}. It is more general than {\tt REPEAT_DETERM}, but
95 \item[\ttindexbold{REPEAT1} {\it tac}]
96 is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
97 least once, failing if this is impossible.
99 \item[\ttindexbold{trace_REPEAT} := true;]
100 enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
101 and {\tt REPEAT}. To view the tracing options, type {\tt h} at the prompt.
105 \subsection{Identities for tacticals}
106 \index{tacticals!identities for}
111 \begin{ttdescription}
112 \item[\ttindexbold{all_tac}]
113 maps any proof state to the one-element sequence containing that state.
114 Thus, it succeeds for all states. It is the identity element of the
115 tactical \ttindex{THEN}\@.
117 \item[\ttindexbold{no_tac}]
118 maps any proof state to the empty sequence. Thus it succeeds for no state.
119 It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and
120 \ttindex{INTLEAVE}\@. Also, it is a zero element for \ttindex{THEN}, which means that
121 \hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}.
123 These primitive tactics are useful when writing tacticals. For example,
124 \ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded
127 fun TRY tac = tac ORELSE all_tac;
129 fun REPEAT tac = Tactic
130 (fn state => tapply((tac THEN REPEAT tac) ORELSE all_tac,
133 If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
134 Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt
135 INTLEAVE}, it applies $tac$ as many times as possible in each
139 Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive
140 tacticals must be coded in this awkward fashion to avoid infinite
141 recursion. With the following definition, \hbox{\tt REPEAT $tac$} would
142 loop due to \ML's eager evaluation strategy:
144 fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
147 The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly
148 and using tail recursion. This sacrifices clarity, but saves much space by
149 discarding intermediate proof states.
153 \section{Control and search tacticals}
154 \index{search!tacticals|(}
156 A predicate on theorems, namely a function of type \hbox{\tt thm->bool},
157 can test whether a proof state enjoys some desirable property --- such as
158 having no subgoals. Tactics that search for satisfactory states are easy
159 to express. The main search procedures, depth-first, breadth-first and
160 best-first, are provided as tacticals. They generate the search tree by
161 repeatedly applying a given tactic.
164 \subsection{Filtering a tactic's results}
165 \index{tacticals!for filtering}
166 \index{tactics!filtering results of}
168 FILTER : (thm -> bool) -> tactic -> tactic
169 CHANGED : tactic -> tactic
171 \begin{ttdescription}
172 \item[\tt FILTER {\it p} $tac$]
173 applies $tac$ to the proof state and returns a sequence consisting of those
174 result states that satisfy~$p$.
176 \item[\ttindexbold{CHANGED} {\it tac}]
177 applies {\it tac\/} to the proof state and returns precisely those states
178 that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}}
179 always has some effect on the state.
183 \subsection{Depth-first search}
184 \index{tacticals!searching}
185 \index{tracing!of searching tacticals}
187 DEPTH_FIRST : (thm->bool) -> tactic -> tactic
188 DEPTH_SOLVE : tactic -> tactic
189 DEPTH_SOLVE_1 : tactic -> tactic
190 trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}
192 \begin{ttdescription}
193 \item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}]
194 returns the proof state if {\it satp} returns true. Otherwise it applies
195 {\it tac}, then recursively searches from each element of the resulting
196 sequence. The code uses a stack for efficiency, in effect applying
197 \hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state.
199 \item[\ttindexbold{DEPTH_SOLVE} {\it tac}]
200 uses {\tt DEPTH_FIRST} to search for states having no subgoals.
202 \item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}]
203 uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
204 given state. Thus, it insists upon solving at least one subgoal.
206 \item[\ttindexbold{trace_DEPTH_FIRST} := true;]
207 enables interactive tracing for {\tt DEPTH_FIRST}. To view the
208 tracing options, type {\tt h} at the prompt.
212 \subsection{Other search strategies}
213 \index{tacticals!searching}
214 \index{tracing!of searching tacticals}
216 BREADTH_FIRST : (thm->bool) -> tactic -> tactic
217 BEST_FIRST : (thm->bool)*(thm->int) -> tactic -> tactic
218 THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
219 -> tactic \hfill{\bf infix 1}
220 trace_BEST_FIRST: bool ref \hfill{\bf initially false}
222 These search strategies will find a solution if one exists. However, they
223 do not enumerate all solutions; they terminate after the first satisfactory
224 result from {\it tac}.
225 \begin{ttdescription}
226 \item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}]
227 uses breadth-first search to find states for which {\it satp\/} is true.
228 For most applications, it is too slow.
230 \item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}]
231 does a heuristic search, using {\it distf\/} to estimate the distance from
232 a satisfactory state. It maintains a list of states ordered by distance.
233 It applies $tac$ to the head of this list; if the result contains any
234 satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST}
235 adds the new states to the list, and continues.
237 The distance function is typically \ttindex{size_of_thm}, which computes
238 the size of the state. The smaller the state, the fewer and simpler
241 \item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$]
242 is like {\tt BEST_FIRST}, except that the priority queue initially
243 contains the result of applying $tac@0$ to the proof state. This tactical
244 permits separate tactics for starting the search and continuing the search.
246 \item[\ttindexbold{trace_BEST_FIRST} := true;]
247 enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To
248 view the tracing options, type {\tt h} at the prompt.
252 \subsection{Auxiliary tacticals for searching}
253 \index{tacticals!conditional}
254 \index{tacticals!deterministic}
256 COND : (thm->bool) -> tactic -> tactic -> tactic
257 IF_UNSOLVED : tactic -> tactic
258 DETERM : tactic -> tactic
260 \begin{ttdescription}
261 \item[COND {\it p} $tac@1$ $tac@2$]
262 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
263 otherwise. It is a conditional tactical in that only one of $tac@1$ and
264 $tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are
265 evaluated because \ML{} uses eager evaluation.
267 \item[\ttindexbold{IF_UNSOLVED} {\it tac}]
268 applies {\it tac\/} to the proof state if it has any subgoals, and simply
269 returns the proof state otherwise. Many common tactics, such as {\tt
270 resolve_tac}, fail if applied to a proof state that has no subgoals.
272 \item[\ttindexbold{DETERM} {\it tac}]
273 applies {\it tac\/} to the proof state and returns the head of the
274 resulting sequence. {\tt DETERM} limits the search space by making its
275 argument deterministic.
279 \subsection{Predicates and functions useful for searching}
280 \index{theorems!size of}
281 \index{theorems!equality of}
283 has_fewer_prems : int -> thm -> bool
284 eq_thm : thm * thm -> bool
285 size_of_thm : thm -> int
287 \begin{ttdescription}
288 \item[\ttindexbold{has_fewer_prems} $n$ $thm$]
289 reports whether $thm$ has fewer than~$n$ premises. By currying,
290 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may
291 be given to the searching tacticals.
293 \item[\ttindexbold{eq_thm}($thm1$,$thm2$)]
294 reports whether $thm1$ and $thm2$ are equal. Both theorems must have
295 identical signatures. Both theorems must have the same conclusions, and
296 the same hypotheses, in the same order. Names of bound variables are
299 \item[\ttindexbold{size_of_thm} $thm$]
300 computes the size of $thm$, namely the number of variables, constants and
301 abstractions in its conclusion. It may serve as a distance function for
302 \ttindex{BEST_FIRST}.
305 \index{search!tacticals|)}
308 \section{Tacticals for subgoal numbering}
309 When conducting a backward proof, we normally consider one goal at a time.
310 A tactic can affect the entire proof state, but many tactics --- such as
311 {\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal.
312 Subgoals are designated by a positive integer, so Isabelle provides
313 tacticals for combining values of type {\tt int->tactic}.
316 \subsection{Restricting a tactic to one subgoal}
317 \index{tactics!restricting to a subgoal}
318 \index{tacticals!for restriction to a subgoal}
320 SELECT_GOAL : tactic -> int -> tactic
321 METAHYPS : (thm list -> tactic) -> int -> tactic
323 \begin{ttdescription}
324 \item[\ttindexbold{SELECT_GOAL} {\it tac} $i$]
325 restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It
326 fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal
327 (do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof
328 state and uses the result to refine the original proof state at
329 subgoal~$i$. If {\it tac\/} returns multiple results then so does
330 \hbox{\tt SELECT_GOAL {\it tac} $i$}.
332 {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
333 with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$
334 then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
335 $\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
336 Such a proof state might cause tactics to go astray. Therefore {\tt
337 SELECT_GOAL} inserts a quantifier to create the state
338 \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
340 \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
341 takes subgoal~$i$, of the form
342 \[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
343 and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
344 assumptions. In these theorems, the subgoal's parameters ($x@1$,
345 \ldots,~$x@l$) become free variables. It supplies the assumptions to
346 $tacf$ and applies the resulting tactic to the proof state
349 If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
350 possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
351 lifted back into the original context, yielding $n$ subgoals.
353 Meta-level assumptions may not contain unknowns. Unknowns in the
354 hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
355 \ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
356 cannot instantiate them. Unknowns in $\theta$ may be instantiated. New
357 unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
359 Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves
360 subgoal~$i$ with one of its own assumptions, which may itself have the form
361 of an inference rule (these are called {\bf higher-level assumptions}).
363 val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
365 The function \ttindex{gethyps} is useful for debugging applications of {\tt
370 {\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
371 In principle, the tactical could treat these like ordinary unknowns.
375 \subsection{Scanning for a subgoal by number}
376 \index{tacticals!scanning for subgoals}
378 ALLGOALS : (int -> tactic) -> tactic
379 TRYALL : (int -> tactic) -> tactic
380 SOMEGOAL : (int -> tactic) -> tactic
381 FIRSTGOAL : (int -> tactic) -> tactic
382 REPEAT_SOME : (int -> tactic) -> tactic
383 REPEAT_FIRST : (int -> tactic) -> tactic
384 trace_goalno_tac : (int -> tactic) -> int -> tactic
386 These apply a tactic function of type {\tt int -> tactic} to all the
387 subgoal numbers of a proof state, and join the resulting tactics using
388 \ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the
389 subgoals, or to one subgoal.
391 Suppose that the original proof state has $n$ subgoals.
393 \begin{ttdescription}
394 \item[\ttindexbold{ALLGOALS} {\it tacf}]
396 \hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.
398 It applies {\it tacf} to all the subgoals, counting downwards (to
399 avoid problems when subgoals are added or deleted).
401 \item[\ttindexbold{TRYALL} {\it tacf}]
403 \hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.
405 It attempts to apply {\it tacf} to all the subgoals. For instance,
406 the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
409 \item[\ttindexbold{SOMEGOAL} {\it tacf}]
411 \hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.
413 It applies {\it tacf} to one subgoal, counting downwards. For instance,
414 the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
415 failing if this is impossible.
417 \item[\ttindexbold{FIRSTGOAL} {\it tacf}]
419 \hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.
421 It applies {\it tacf} to one subgoal, counting upwards.
423 \item[\ttindexbold{REPEAT_SOME} {\it tacf}]
424 applies {\it tacf} once or more to a subgoal, counting downwards.
426 \item[\ttindexbold{REPEAT_FIRST} {\it tacf}]
427 applies {\it tacf} once or more to a subgoal, counting upwards.
429 \item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]
430 applies \hbox{\it tac i\/} to the proof state. If the resulting sequence
431 is non-empty, then it is returned, with the side-effect of printing {\tt
432 Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty
433 sequence and prints nothing.
435 It indicates that `the tactic worked for subgoal~$i$' and is mainly used
436 with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
440 \subsection{Joining tactic functions}
441 \index{tacticals!joining tactic functions}
443 THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1}
444 ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
445 APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
446 INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
447 EVERY' : ('a -> tactic) list -> 'a -> tactic
448 FIRST' : ('a -> tactic) list -> 'a -> tactic
450 These help to express tactics that specify subgoal numbers. The tactic
452 SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i)
456 SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)
458 Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not
459 provided, because function composition accomplishes the same purpose.
462 ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i))
466 ALLGOALS (REPEAT o (etac exE ORELSE' atac))
468 These tacticals are polymorphic; $x$ need not be an integer.
470 \begin{tabular}{r@{\rm\ \ yields\ \ }l}
471 $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &
472 $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\
474 $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &
475 $tacf@1(x)$ ORELSE $tacf@2(x)$ \\
477 $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &
478 $tacf@1(x)$ APPEND $tacf@2(x)$ \\
480 $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &
481 $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\
483 EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &
484 EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\
486 FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &
487 FIRST $[tacf@1(x),\ldots,tacf@n(x)]$
492 \subsection{Applying a list of tactics to 1}
493 \index{tacticals!joining tactic functions}
495 EVERY1: (int -> tactic) list -> tactic
496 FIRST1: (int -> tactic) list -> tactic
498 A common proof style is to treat the subgoals as a stack, always
499 restricting attention to the first subgoal. Such proofs contain long lists
500 of tactics, each applied to~1. These can be simplified using {\tt EVERY1}
503 \begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}
504 EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &
505 EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\
507 FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &
508 FIRST $[tacf@1(1),\ldots,tacf@n(1)]$