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[set \ttindexbold{trace_REPEAT};]
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;
130 (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state);
132 If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
133 Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt
134 INTLEAVE}, it applies $tac$ as many times as possible in each
138 Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive
139 tacticals must be coded in this awkward fashion to avoid infinite
140 recursion. With the following definition, \hbox{\tt REPEAT $tac$} would
141 loop due to \ML's eager evaluation strategy:
143 fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
146 The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly
147 and using tail recursion. This sacrifices clarity, but saves much space by
148 discarding intermediate proof states.
152 \section{Control and search tacticals}
153 \index{search!tacticals|(}
155 A predicate on theorems, namely a function of type \hbox{\tt thm->bool},
156 can test whether a proof state enjoys some desirable property --- such as
157 having no subgoals. Tactics that search for satisfactory states are easy
158 to express. The main search procedures, depth-first, breadth-first and
159 best-first, are provided as tacticals. They generate the search tree by
160 repeatedly applying a given tactic.
163 \subsection{Filtering a tactic's results}
164 \index{tacticals!for filtering}
165 \index{tactics!filtering results of}
167 FILTER : (thm -> bool) -> tactic -> tactic
168 CHANGED : tactic -> tactic
170 \begin{ttdescription}
171 \item[\ttindexbold{FILTER} {\it p} $tac$]
172 applies $tac$ to the proof state and returns a sequence consisting of those
173 result states that satisfy~$p$.
175 \item[\ttindexbold{CHANGED} {\it tac}]
176 applies {\it tac\/} to the proof state and returns precisely those states
177 that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}}
178 always has some effect on the state.
182 \subsection{Depth-first search}
183 \index{tacticals!searching}
184 \index{tracing!of searching tacticals}
186 DEPTH_FIRST : (thm->bool) -> tactic -> tactic
187 DEPTH_SOLVE : tactic -> tactic
188 DEPTH_SOLVE_1 : tactic -> tactic
189 trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}
191 \begin{ttdescription}
192 \item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}]
193 returns the proof state if {\it satp} returns true. Otherwise it applies
194 {\it tac}, then recursively searches from each element of the resulting
195 sequence. The code uses a stack for efficiency, in effect applying
196 \hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state.
198 \item[\ttindexbold{DEPTH_SOLVE} {\it tac}]
199 uses {\tt DEPTH_FIRST} to search for states having no subgoals.
201 \item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}]
202 uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
203 given state. Thus, it insists upon solving at least one subgoal.
205 \item[set \ttindexbold{trace_DEPTH_FIRST};]
206 enables interactive tracing for {\tt DEPTH_FIRST}. To view the
207 tracing options, type {\tt h} at the prompt.
211 \subsection{Other search strategies}
212 \index{tacticals!searching}
213 \index{tracing!of searching tacticals}
215 BREADTH_FIRST : (thm->bool) -> tactic -> tactic
216 BEST_FIRST : (thm->bool)*(thm->int) -> tactic -> tactic
217 THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
218 -> tactic \hfill{\bf infix 1}
219 trace_BEST_FIRST: bool ref \hfill{\bf initially false}
221 These search strategies will find a solution if one exists. However, they
222 do not enumerate all solutions; they terminate after the first satisfactory
223 result from {\it tac}.
224 \begin{ttdescription}
225 \item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}]
226 uses breadth-first search to find states for which {\it satp\/} is true.
227 For most applications, it is too slow.
229 \item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}]
230 does a heuristic search, using {\it distf\/} to estimate the distance from
231 a satisfactory state. It maintains a list of states ordered by distance.
232 It applies $tac$ to the head of this list; if the result contains any
233 satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST}
234 adds the new states to the list, and continues.
236 The distance function is typically \ttindex{size_of_thm}, which computes
237 the size of the state. The smaller the state, the fewer and simpler
240 \item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$]
241 is like {\tt BEST_FIRST}, except that the priority queue initially
242 contains the result of applying $tac@0$ to the proof state. This tactical
243 permits separate tactics for starting the search and continuing the search.
245 \item[set \ttindexbold{trace_BEST_FIRST};]
246 enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To
247 view the tracing options, type {\tt h} at the prompt.
251 \subsection{Auxiliary tacticals for searching}
252 \index{tacticals!conditional}
253 \index{tacticals!deterministic}
255 COND : (thm->bool) -> tactic -> tactic -> tactic
256 IF_UNSOLVED : tactic -> tactic
257 DETERM : tactic -> tactic
259 \begin{ttdescription}
260 \item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$]
261 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
262 otherwise. It is a conditional tactical in that only one of $tac@1$ and
263 $tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are
264 evaluated because \ML{} uses eager evaluation.
266 \item[\ttindexbold{IF_UNSOLVED} {\it tac}]
267 applies {\it tac\/} to the proof state if it has any subgoals, and simply
268 returns the proof state otherwise. Many common tactics, such as {\tt
269 resolve_tac}, fail if applied to a proof state that has no subgoals.
271 \item[\ttindexbold{DETERM} {\it tac}]
272 applies {\it tac\/} to the proof state and returns the head of the
273 resulting sequence. {\tt DETERM} limits the search space by making its
274 argument deterministic.
278 \subsection{Predicates and functions useful for searching}
279 \index{theorems!size of}
280 \index{theorems!equality of}
282 has_fewer_prems : int -> thm -> bool
283 eq_thm : thm * thm -> bool
284 size_of_thm : thm -> int
286 \begin{ttdescription}
287 \item[\ttindexbold{has_fewer_prems} $n$ $thm$]
288 reports whether $thm$ has fewer than~$n$ premises. By currying,
289 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may
290 be given to the searching tacticals.
292 \item[\ttindexbold{eq_thm} ($thm_1$, $thm_2$)] reports whether $thm_1$
293 and $thm_2$ are equal. Both theorems must have identical
294 signatures. Both theorems must have the same conclusions, and the
295 same hypotheses, in the same order. Names of bound variables are
298 \item[\ttindexbold{size_of_thm} $thm$]
299 computes the size of $thm$, namely the number of variables, constants and
300 abstractions in its conclusion. It may serve as a distance function for
301 \ttindex{BEST_FIRST}.
304 \index{search!tacticals|)}
307 \section{Tacticals for subgoal numbering}
308 When conducting a backward proof, we normally consider one goal at a time.
309 A tactic can affect the entire proof state, but many tactics --- such as
310 {\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal.
311 Subgoals are designated by a positive integer, so Isabelle provides
312 tacticals for combining values of type {\tt int->tactic}.
315 \subsection{Restricting a tactic to one subgoal}
316 \index{tactics!restricting to a subgoal}
317 \index{tacticals!for restriction to a subgoal}
319 SELECT_GOAL : tactic -> int -> tactic
320 METAHYPS : (thm list -> tactic) -> int -> tactic
322 \begin{ttdescription}
323 \item[\ttindexbold{SELECT_GOAL} {\it tac} $i$]
324 restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It
325 fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal
326 (do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof
327 state and uses the result to refine the original proof state at
328 subgoal~$i$. If {\it tac\/} returns multiple results then so does
329 \hbox{\tt SELECT_GOAL {\it tac} $i$}.
331 {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
332 with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$
333 then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
334 $\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
335 Such a proof state might cause tactics to go astray. Therefore {\tt
336 SELECT_GOAL} inserts a quantifier to create the state
337 \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
339 \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
340 takes subgoal~$i$, of the form
341 \[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
342 and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
343 assumptions. In these theorems, the subgoal's parameters ($x@1$,
344 \ldots,~$x@l$) become free variables. It supplies the assumptions to
345 $tacf$ and applies the resulting tactic to the proof state
348 If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
349 possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
350 lifted back into the original context, yielding $n$ subgoals.
352 Meta-level assumptions may not contain unknowns. Unknowns in the
353 hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
354 \ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
355 cannot instantiate them. Unknowns in $\theta$ may be instantiated. New
356 unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
358 Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves
359 subgoal~$i$ with one of its own assumptions, which may itself have the form
360 of an inference rule (these are called {\bf higher-level assumptions}).
362 val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
364 The function \ttindex{gethyps} is useful for debugging applications of {\tt
369 {\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
370 In principle, the tactical could treat these like ordinary unknowns.
374 \subsection{Scanning for a subgoal by number}
375 \index{tacticals!scanning for subgoals}
377 ALLGOALS : (int -> tactic) -> tactic
378 TRYALL : (int -> tactic) -> tactic
379 SOMEGOAL : (int -> tactic) -> tactic
380 FIRSTGOAL : (int -> tactic) -> tactic
381 REPEAT_SOME : (int -> tactic) -> tactic
382 REPEAT_FIRST : (int -> tactic) -> tactic
383 trace_goalno_tac : (int -> tactic) -> int -> tactic
385 These apply a tactic function of type {\tt int -> tactic} to all the
386 subgoal numbers of a proof state, and join the resulting tactics using
387 \ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the
388 subgoals, or to one subgoal.
390 Suppose that the original proof state has $n$ subgoals.
392 \begin{ttdescription}
393 \item[\ttindexbold{ALLGOALS} {\it tacf}]
395 \hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.
397 It applies {\it tacf} to all the subgoals, counting downwards (to
398 avoid problems when subgoals are added or deleted).
400 \item[\ttindexbold{TRYALL} {\it tacf}]
402 \hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.
404 It attempts to apply {\it tacf} to all the subgoals. For instance,
405 the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
408 \item[\ttindexbold{SOMEGOAL} {\it tacf}]
410 \hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.
412 It applies {\it tacf} to one subgoal, counting downwards. For instance,
413 the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
414 failing if this is impossible.
416 \item[\ttindexbold{FIRSTGOAL} {\it tacf}]
418 \hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.
420 It applies {\it tacf} to one subgoal, counting upwards.
422 \item[\ttindexbold{REPEAT_SOME} {\it tacf}]
423 applies {\it tacf} once or more to a subgoal, counting downwards.
425 \item[\ttindexbold{REPEAT_FIRST} {\it tacf}]
426 applies {\it tacf} once or more to a subgoal, counting upwards.
428 \item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]
429 applies \hbox{\it tac i\/} to the proof state. If the resulting sequence
430 is non-empty, then it is returned, with the side-effect of printing {\tt
431 Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty
432 sequence and prints nothing.
434 It indicates that `the tactic worked for subgoal~$i$' and is mainly used
435 with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
439 \subsection{Joining tactic functions}
440 \index{tacticals!joining tactic functions}
442 THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1}
443 ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
444 APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
445 INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
446 EVERY' : ('a -> tactic) list -> 'a -> tactic
447 FIRST' : ('a -> tactic) list -> 'a -> tactic
449 These help to express tactics that specify subgoal numbers. The tactic
451 SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i)
455 SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)
457 Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not
458 provided, because function composition accomplishes the same purpose.
461 ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i))
465 ALLGOALS (REPEAT o (etac exE ORELSE' atac))
467 These tacticals are polymorphic; $x$ need not be an integer.
469 \begin{tabular}{r@{\rm\ \ yields\ \ }l}
470 $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &
471 $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\
473 $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &
474 $tacf@1(x)$ ORELSE $tacf@2(x)$ \\
476 $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &
477 $tacf@1(x)$ APPEND $tacf@2(x)$ \\
479 $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &
480 $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\
482 EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &
483 EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\
485 FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &
486 FIRST $[tacf@1(x),\ldots,tacf@n(x)]$
491 \subsection{Applying a list of tactics to 1}
492 \index{tacticals!joining tactic functions}
494 EVERY1: (int -> tactic) list -> tactic
495 FIRST1: (int -> tactic) list -> tactic
497 A common proof style is to treat the subgoals as a stack, always
498 restricting attention to the first subgoal. Such proofs contain long lists
499 of tactics, each applied to~1. These can be simplified using {\tt EVERY1}
502 \begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}
503 EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &
504 EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\
506 FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &
507 FIRST $[tacf@1(1),\ldots,tacf@n(1)]$