104

1 
%% $Id$


2 
\chapter{Tacticals}


3 
\index{tacticals(}


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 highlevel control


7 
structures.


8 


9 
\section{The basic tacticals}


10 
\subsection{Joining two tactics}

323

11 
\index{tacticals!joining two tactics}

104

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


15 
alternation.


16 
\begin{ttbox}


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}


21 
\end{ttbox}

323

22 
\begin{ttdescription}


23 
\item[$tac@1$ \ttindexbold{THEN} $tac@2$]

104

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.


29 

323

30 
\item[$tac@1$ \ttindexbold{ORELSE} $tac@2$]

104

31 
makes a choice between the two tactics. Applied to a state, it


32 
tries~$tac@1$ and returns the result if nonempty; if $tac@1$ fails then it


33 
uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then


34 
$tac@2$ is excluded.


35 

323

36 
\item[$tac@1$ \ttindexbold{APPEND} $tac@2$]

104

37 
concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment

323

38 
to either tactic, {\tt APPEND} helps avoid incompleteness during


39 
search.\index{search}

104

40 

323

41 
\item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$]

104

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


44 
sequence.

323

45 
\end{ttdescription}

104

46 


47 


48 
\subsection{Joining a list of tactics}

323

49 
\index{tacticals!joining a list of tactics}

104

50 
\begin{ttbox}


51 
EVERY : tactic list > tactic


52 
FIRST : tactic list > tactic


53 
\end{ttbox}


54 
{\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and


55 
{\tt ORELSE}\@.

323

56 
\begin{ttdescription}

104

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.


60 


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.

323

64 
\end{ttdescription}

104

65 


66 


67 
\subsection{Repetition tacticals}

323

68 
\index{tacticals!repetition}

104

69 
\begin{ttbox}


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}


75 
\end{ttbox}

323

76 
\begin{ttdescription}

104

77 
\item[\ttindexbold{TRY} {\it tac}]


78 
applies {\it tac\/} to the proof state and returns the resulting sequence,


79 
if nonempty; otherwise it returns the original state. Thus, it applies


80 
{\it tac\/} at most once.


81 


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.


86 


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


93 
requires more space.


94 


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.


98 

323

99 
\item[\ttindexbold{trace_REPEAT} := true;]

286

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.

323

102 
\end{ttdescription}

104

103 


104 


105 
\subsection{Identities for tacticals}

323

106 
\index{tacticals!identities for}

104

107 
\begin{ttbox}


108 
all_tac : tactic


109 
no_tac : tactic


110 
\end{ttbox}

323

111 
\begin{ttdescription}

104

112 
\item[\ttindexbold{all_tac}]


113 
maps any proof state to the oneelement sequence containing that state.


114 
Thus, it succeeds for all states. It is the identity element of the


115 
tactical \ttindex{THEN}\@.


116 


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}.

323

122 
\end{ttdescription}

104

123 
These primitive tactics are useful when writing tacticals. For example,


124 
\ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded


125 
as follows:


126 
\begin{ttbox}


127 
fun TRY tac = tac ORELSE all_tac;


128 


129 
fun REPEAT tac = Tactic


130 
(fn state => tapply((tac THEN REPEAT tac) ORELSE all_tac,


131 
state));


132 
\end{ttbox}


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


136 
outcome.


137 


138 
\begin{warn}


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

332

142 
loop due to \ML's eager evaluation strategy:

104

143 
\begin{ttbox}


144 
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;


145 
\end{ttbox}


146 
\par\noindent


147 
The builtin {\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.


150 
\end{warn}


151 


152 


153 
\section{Control and search tacticals}

323

154 
\index{search!tacticals(}


155 

104

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, depthfirst, breadthfirst and


160 
bestfirst, are provided as tacticals. They generate the search tree by


161 
repeatedly applying a given tactic.


162 


163 


164 
\subsection{Filtering a tactic's results}

323

165 
\index{tacticals!for filtering}


166 
\index{tactics!filtering results of}

104

167 
\begin{ttbox}


168 
FILTER : (thm > bool) > tactic > tactic


169 
CHANGED : tactic > tactic


170 
\end{ttbox}

323

171 
\begin{ttdescription}

1118

172 
\item[\ttindexbold{FILTER} {\it p} $tac$]

104

173 
applies $tac$ to the proof state and returns a sequence consisting of those


174 
result states that satisfy~$p$.


175 


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.

323

180 
\end{ttdescription}

104

181 


182 


183 
\subsection{Depthfirst search}

323

184 
\index{tacticals!searching}

104

185 
\index{tracing!of searching tacticals}


186 
\begin{ttbox}


187 
DEPTH_FIRST : (thm>bool) > tactic > tactic

332

188 
DEPTH_SOLVE : tactic > tactic


189 
DEPTH_SOLVE_1 : tactic > tactic

104

190 
trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}


191 
\end{ttbox}

323

192 
\begin{ttdescription}

104

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.


198 


199 
\item[\ttindexbold{DEPTH_SOLVE} {\it tac}]


200 
uses {\tt DEPTH_FIRST} to search for states having no subgoals.


201 


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.


205 

323

206 
\item[\ttindexbold{trace_DEPTH_FIRST} := true;]

104

207 
enables interactive tracing for {\tt DEPTH_FIRST}. To view the


208 
tracing options, type {\tt h} at the prompt.

323

209 
\end{ttdescription}

104

210 


211 


212 
\subsection{Other search strategies}

323

213 
\index{tacticals!searching}

104

214 
\index{tracing!of searching tacticals}


215 
\begin{ttbox}

332

216 
BREADTH_FIRST : (thm>bool) > tactic > tactic

104

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}


221 
\end{ttbox}


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}.

323

225 
\begin{ttdescription}

104

226 
\item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}]


227 
uses breadthfirst search to find states for which {\it satp\/} is true.


228 
For most applications, it is too slow.


229 


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.


236 


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


239 
subgoals it has.


240 


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.


245 

323

246 
\item[\ttindexbold{trace_BEST_FIRST} := true;]

286

247 
enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To


248 
view the tracing options, type {\tt h} at the prompt.

323

249 
\end{ttdescription}

104

250 


251 


252 
\subsection{Auxiliary tacticals for searching}


253 
\index{tacticals!conditional}


254 
\index{tacticals!deterministic}


255 
\begin{ttbox}


256 
COND : (thm>bool) > tactic > tactic > tactic


257 
IF_UNSOLVED : tactic > tactic


258 
DETERM : tactic > tactic


259 
\end{ttbox}

323

260 
\begin{ttdescription}

1118

261 
\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$]

104

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.


266 


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.


271 


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.

323

276 
\end{ttdescription}

104

277 


278 


279 
\subsection{Predicates and functions useful for searching}


280 
\index{theorems!size of}


281 
\index{theorems!equality of}


282 
\begin{ttbox}


283 
has_fewer_prems : int > thm > bool


284 
eq_thm : thm * thm > bool


285 
size_of_thm : thm > int


286 
\end{ttbox}

323

287 
\begin{ttdescription}

104

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.


292 


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


297 
ignored.


298 


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}.

323

303 
\end{ttdescription}


304 


305 
\index{search!tacticals)}

104

306 


307 


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}.


314 


315 


316 
\subsection{Restricting a tactic to one subgoal}


317 
\index{tactics!restricting to a subgoal}


318 
\index{tacticals!for restriction to a subgoal}


319 
\begin{ttbox}


320 
SELECT_GOAL : tactic > int > tactic


321 
METAHYPS : (thm list > tactic) > int > tactic


322 
\end{ttbox}

323

323 
\begin{ttdescription}

104

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$}.


331 

323

332 
{\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,

332

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

323

338 
\[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]

104

339 

323

340 
\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{metaassumptions}

104

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 metalevel


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


347 
$\theta\Imp\theta$.


348 


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.


352 

286

353 
Metalevel 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

323

357 
unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.

104

358 


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 higherlevel assumptions}).


362 
\begin{ttbox}


363 
val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);


364 
\end{ttbox}

332

365 
The function \ttindex{gethyps} is useful for debugging applications of {\tt


366 
METAHYPS}.

323

367 
\end{ttdescription}

104

368 


369 
\begin{warn}


370 
{\tt METAHYPS} fails if the context or new subgoals contain type unknowns.


371 
In principle, the tactical could treat these like ordinary unknowns.


372 
\end{warn}


373 


374 


375 
\subsection{Scanning for a subgoal by number}

323

376 
\index{tacticals!scanning for subgoals}

104

377 
\begin{ttbox}


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


385 
\end{ttbox}


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.


390 


391 
Suppose that the original proof state has $n$ subgoals.


392 

323

393 
\begin{ttdescription}

104

394 
\item[\ttindexbold{ALLGOALS} {\it tacf}]


395 
is equivalent to


396 
\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.


397 

323

398 
It applies {\it tacf} to all the subgoals, counting downwards (to

104

399 
avoid problems when subgoals are added or deleted).


400 


401 
\item[\ttindexbold{TRYALL} {\it tacf}]


402 
is equivalent to

323

403 
\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.

104

404 


405 
It attempts to apply {\it tacf} to all the subgoals. For instance,

286

406 
the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by

104

407 
assumption.


408 


409 
\item[\ttindexbold{SOMEGOAL} {\it tacf}]


410 
is equivalent to


411 
\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.


412 

323

413 
It applies {\it tacf} to one subgoal, counting downwards. For instance,

286

414 
the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,


415 
failing if this is impossible.

104

416 


417 
\item[\ttindexbold{FIRSTGOAL} {\it tacf}]


418 
is equivalent to


419 
\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.


420 

323

421 
It applies {\it tacf} to one subgoal, counting upwards.

104

422 


423 
\item[\ttindexbold{REPEAT_SOME} {\it tacf}]

323

424 
applies {\it tacf} once or more to a subgoal, counting downwards.

104

425 


426 
\item[\ttindexbold{REPEAT_FIRST} {\it tacf}]

323

427 
applies {\it tacf} once or more to a subgoal, counting upwards.

104

428 


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 nonempty, then it is returned, with the sideeffect of printing {\tt


432 
Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty


433 
sequence and prints nothing.


434 

323

435 
It indicates that `the tactic worked for subgoal~$i$' and is mainly used

104

436 
with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.

323

437 
\end{ttdescription}

104

438 


439 


440 
\subsection{Joining tactic functions}

323

441 
\index{tacticals!joining tactic functions}

104

442 
\begin{ttbox}


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


449 
\end{ttbox}


450 
These help to express tactics that specify subgoal numbers. The tactic


451 
\begin{ttbox}


452 
SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i)


453 
\end{ttbox}


454 
can be simplified to


455 
\begin{ttbox}


456 
SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)


457 
\end{ttbox}


458 
Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not


459 
provided, because function composition accomplishes the same purpose.


460 
The tactic


461 
\begin{ttbox}


462 
ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i))


463 
\end{ttbox}


464 
can be simplified to


465 
\begin{ttbox}


466 
ALLGOALS (REPEAT o (etac exE ORELSE' atac))


467 
\end{ttbox}


468 
These tacticals are polymorphic; $x$ need not be an integer.


469 
\begin{center} \tt


470 
\begin{tabular}{r@{\rm\ \ yields\ \ }l}

323

471 
$(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &

104

472 
$tacf@1(x)$~~THEN~~$tacf@2(x)$ \\


473 

323

474 
$(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &

104

475 
$tacf@1(x)$ ORELSE $tacf@2(x)$ \\


476 

323

477 
$(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &

104

478 
$tacf@1(x)$ APPEND $tacf@2(x)$ \\


479 

323

480 
$(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &

104

481 
$tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\


482 


483 
EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &


484 
EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\


485 


486 
FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &


487 
FIRST $[tacf@1(x),\ldots,tacf@n(x)]$


488 
\end{tabular}


489 
\end{center}


490 


491 


492 
\subsection{Applying a list of tactics to 1}

323

493 
\index{tacticals!joining tactic functions}

104

494 
\begin{ttbox}


495 
EVERY1: (int > tactic) list > tactic


496 
FIRST1: (int > tactic) list > tactic


497 
\end{ttbox}


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}


501 
and {\tt FIRST1}:


502 
\begin{center} \tt


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)]$ \\


506 


507 
FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &


508 
FIRST $[tacf@1(1),\ldots,tacf@n(1)]$


509 
\end{tabular}


510 
\end{center}


511 


512 
\index{tacticals)}
