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 SOLVE : tactic -> tactic
258 DETERM : tactic -> tactic
260 \begin{ttdescription}
261 \item[\ttindexbold{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{SOLVE} {\it tac}]
273 applies {\it tac\/} to the proof state and then fails iff there are subgoals
276 \item[\ttindexbold{DETERM} {\it tac}]
277 applies {\it tac\/} to the proof state and returns the head of the
278 resulting sequence. {\tt DETERM} limits the search space by making its
279 argument deterministic.
283 \subsection{Predicates and functions useful for searching}
284 \index{theorems!size of}
285 \index{theorems!equality of}
287 has_fewer_prems : int -> thm -> bool
288 eq_thm : thm * thm -> bool
289 size_of_thm : thm -> int
291 \begin{ttdescription}
292 \item[\ttindexbold{has_fewer_prems} $n$ $thm$]
293 reports whether $thm$ has fewer than~$n$ premises. By currying,
294 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may
295 be given to the searching tacticals.
297 \item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
298 $thm@2$ are equal. Both theorems must have identical signatures. Both
299 theorems must have the same conclusions, and the same hypotheses, in the
300 same order. Names of bound variables are ignored.
302 \item[\ttindexbold{size_of_thm} $thm$]
303 computes the size of $thm$, namely the number of variables, constants and
304 abstractions in its conclusion. It may serve as a distance function for
305 \ttindex{BEST_FIRST}.
308 \index{search!tacticals|)}
311 \section{Tacticals for subgoal numbering}
312 When conducting a backward proof, we normally consider one goal at a time.
313 A tactic can affect the entire proof state, but many tactics --- such as
314 {\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal.
315 Subgoals are designated by a positive integer, so Isabelle provides
316 tacticals for combining values of type {\tt int->tactic}.
319 \subsection{Restricting a tactic to one subgoal}
320 \index{tactics!restricting to a subgoal}
321 \index{tacticals!for restriction to a subgoal}
323 SELECT_GOAL : tactic -> int -> tactic
324 METAHYPS : (thm list -> tactic) -> int -> tactic
326 \begin{ttdescription}
327 \item[\ttindexbold{SELECT_GOAL} {\it tac} $i$]
328 restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It
329 fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal
330 (do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof
331 state and uses the result to refine the original proof state at
332 subgoal~$i$. If {\it tac\/} returns multiple results then so does
333 \hbox{\tt SELECT_GOAL {\it tac} $i$}.
335 {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
336 with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$
337 then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
338 $\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
339 Such a proof state might cause tactics to go astray. Therefore {\tt
340 SELECT_GOAL} inserts a quantifier to create the state
341 \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
343 \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
344 takes subgoal~$i$, of the form
345 \[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
346 and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
347 assumptions. In these theorems, the subgoal's parameters ($x@1$,
348 \ldots,~$x@l$) become free variables. It supplies the assumptions to
349 $tacf$ and applies the resulting tactic to the proof state
352 If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
353 possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
354 lifted back into the original context, yielding $n$ subgoals.
356 Meta-level assumptions may not contain unknowns. Unknowns in the
357 hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
358 \ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
359 cannot instantiate them. Unknowns in $\theta$ may be instantiated. New
360 unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
362 Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves
363 subgoal~$i$ with one of its own assumptions, which may itself have the form
364 of an inference rule (these are called {\bf higher-level assumptions}).
366 val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
368 The function \ttindex{gethyps} is useful for debugging applications of {\tt
373 {\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
374 In principle, the tactical could treat these like ordinary unknowns.
378 \subsection{Scanning for a subgoal by number}
379 \index{tacticals!scanning for subgoals}
381 ALLGOALS : (int -> tactic) -> tactic
382 TRYALL : (int -> tactic) -> tactic
383 SOMEGOAL : (int -> tactic) -> tactic
384 FIRSTGOAL : (int -> tactic) -> tactic
385 REPEAT_SOME : (int -> tactic) -> tactic
386 REPEAT_FIRST : (int -> tactic) -> tactic
387 trace_goalno_tac : (int -> tactic) -> int -> tactic
389 These apply a tactic function of type {\tt int -> tactic} to all the
390 subgoal numbers of a proof state, and join the resulting tactics using
391 \ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the
392 subgoals, or to one subgoal.
394 Suppose that the original proof state has $n$ subgoals.
396 \begin{ttdescription}
397 \item[\ttindexbold{ALLGOALS} {\it tacf}]
399 \hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.
401 It applies {\it tacf} to all the subgoals, counting downwards (to
402 avoid problems when subgoals are added or deleted).
404 \item[\ttindexbold{TRYALL} {\it tacf}]
406 \hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.
408 It attempts to apply {\it tacf} to all the subgoals. For instance,
409 the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
412 \item[\ttindexbold{SOMEGOAL} {\it tacf}]
414 \hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.
416 It applies {\it tacf} to one subgoal, counting downwards. For instance,
417 the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
418 failing if this is impossible.
420 \item[\ttindexbold{FIRSTGOAL} {\it tacf}]
422 \hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.
424 It applies {\it tacf} to one subgoal, counting upwards.
426 \item[\ttindexbold{REPEAT_SOME} {\it tacf}]
427 applies {\it tacf} once or more to a subgoal, counting downwards.
429 \item[\ttindexbold{REPEAT_FIRST} {\it tacf}]
430 applies {\it tacf} once or more to a subgoal, counting upwards.
432 \item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]
433 applies \hbox{\it tac i\/} to the proof state. If the resulting sequence
434 is non-empty, then it is returned, with the side-effect of printing {\tt
435 Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty
436 sequence and prints nothing.
438 It indicates that `the tactic worked for subgoal~$i$' and is mainly used
439 with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
443 \subsection{Joining tactic functions}
444 \index{tacticals!joining tactic functions}
446 THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1}
447 ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
448 APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
449 INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
450 EVERY' : ('a -> tactic) list -> 'a -> tactic
451 FIRST' : ('a -> tactic) list -> 'a -> tactic
453 These help to express tactics that specify subgoal numbers. The tactic
455 SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i)
459 SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)
461 Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not
462 provided, because function composition accomplishes the same purpose.
465 ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i))
469 ALLGOALS (REPEAT o (etac exE ORELSE' atac))
471 These tacticals are polymorphic; $x$ need not be an integer.
473 \begin{tabular}{r@{\rm\ \ yields\ \ }l}
474 $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &
475 $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\
477 $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &
478 $tacf@1(x)$ ORELSE $tacf@2(x)$ \\
480 $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &
481 $tacf@1(x)$ APPEND $tacf@2(x)$ \\
483 $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &
484 $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\
486 EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &
487 EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\
489 FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &
490 FIRST $[tacf@1(x),\ldots,tacf@n(x)]$
495 \subsection{Applying a list of tactics to 1}
496 \index{tacticals!joining tactic functions}
498 EVERY1: (int -> tactic) list -> tactic
499 FIRST1: (int -> tactic) list -> tactic
501 A common proof style is to treat the subgoals as a stack, always
502 restricting attention to the first subgoal. Such proofs contain long lists
503 of tactics, each applied to~1. These can be simplified using {\tt EVERY1}
506 \begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}
507 EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &
508 EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\
510 FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &
511 FIRST $[tacf@1(1),\ldots,tacf@n(1)]$
520 %%% TeX-master: "ref"