104

1 
%% $Id$


2 
\chapter{Tacticals}


3 
\index{tacticals(}


4 
\index{tactics!combiningsee{tacticals}}


5 
Tacticals are operations on tactics. Their implementation makes use of


6 
functional programming techniques, especially for sequences. Most of the


7 
time, you may forget about this and regard tacticals as highlevel control


8 
structures.


9 


10 
\section{The basic tacticals}


11 
\subsection{Joining two tactics}


12 
\index{tacticals!joining two tacticsbold}


13 
The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and


14 
alternation, underlie most of the other control structures in Isabelle.


15 
{\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of


16 
alternation.


17 
\begin{ttbox}


18 
THEN : tactic * tactic > tactic \hfill{\bf infix 1}


19 
ORELSE : tactic * tactic > tactic \hfill{\bf infix}


20 
APPEND : tactic * tactic > tactic \hfill{\bf infix}


21 
INTLEAVE : tactic * tactic > tactic \hfill{\bf infix}


22 
\end{ttbox}


23 
\begin{description}


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


25 
is the sequential composition of the two tactics. Applied to a proof


26 
state, it returns all states reachable in two steps by applying $tac@1$


27 
followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a


28 
sequence of next states; then, it applies $tac@2$ to each of these and


29 
concatenates the results.


30 


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


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


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


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


35 
$tac@2$ is excluded.


36 


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


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


39 
to either tactic, {\tt APPEND} helps avoid incompleteness during search.


40 


41 
\item[\tt $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


44 
sequence.


45 
\end{description}


46 


47 


48 
\subsection{Joining a list of tactics}


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


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


56 
\begin{description}


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.


64 
\end{description}


65 


66 


67 
\subsection{Repetition tacticals}


68 
\index{tacticals!repetitionbold}


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}


76 
\begin{description}


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 


99 
\item[\ttindexbold{trace_REPEAT} \tt:= 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.

104

102 
\end{description}


103 


104 


105 
\subsection{Identities for tacticals}


106 
\index{tacticals!identities forbold}


107 
\begin{ttbox}


108 
all_tac : tactic


109 
no_tac : tactic


110 
\end{ttbox}


111 
\begin{description}


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


122 
\end{description}


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


142 
loop:


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}


154 
A predicate on theorems, namely a function of type \hbox{\tt thm>bool},


155 
can test whether a proof state enjoys some desirable property  such as


156 
having no subgoals. Tactics that search for satisfactory states are easy


157 
to express. The main search procedures, depthfirst, breadthfirst and


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


159 
repeatedly applying a given tactic.


160 


161 


162 
\subsection{Filtering a tactic's results}


163 
\index{tacticals!for filteringbold}


164 
\index{tactics!filtering results ofbold}


165 
\begin{ttbox}


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


167 
CHANGED : tactic > tactic


168 
\end{ttbox}


169 
\begin{description}


170 
\item[\tt \tt FILTER {\it p} $tac$]


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


172 
result states that satisfy~$p$.


173 


174 
\item[\ttindexbold{CHANGED} {\it tac}]


175 
applies {\it tac\/} to the proof state and returns precisely those states


176 
that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}}


177 
always has some effect on the state.


178 
\end{description}


179 


180 


181 
\subsection{Depthfirst search}


182 
\index{tacticals!searchingbold}


183 
\index{tracing!of searching tacticals}


184 
\begin{ttbox}


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


186 
DEPTH_SOLVE : tactic > tactic


187 
DEPTH_SOLVE_1 : tactic > tactic


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


189 
\end{ttbox}


190 
\begin{description}


191 
\item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}]


192 
returns the proof state if {\it satp} returns true. Otherwise it applies


193 
{\it tac}, then recursively searches from each element of the resulting


194 
sequence. The code uses a stack for efficiency, in effect applying


195 
\hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state.


196 


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


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


199 


200 
\item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}]


201 
uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the


202 
given state. Thus, it insists upon solving at least one subgoal.


203 


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


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


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


207 
\end{description}


208 


209 


210 
\subsection{Other search strategies}


211 
\index{tacticals!searchingbold}


212 
\index{tracing!of searching tacticals}


213 
\begin{ttbox}


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


215 
BEST_FIRST : (thm>bool)*(thm>int) > tactic > tactic


216 
THEN_BEST_FIRST : tactic * ((thm>bool) * (thm>int) * tactic)


217 
> tactic \hfill{\bf infix 1}


218 
trace_BEST_FIRST: bool ref \hfill{\bf initially false}


219 
\end{ttbox}


220 
These search strategies will find a solution if one exists. However, they


221 
do not enumerate all solutions; they terminate after the first satisfactory


222 
result from {\it tac}.


223 
\begin{description}


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


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


226 
For most applications, it is too slow.


227 


228 
\item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}]


229 
does a heuristic search, using {\it distf\/} to estimate the distance from


230 
a satisfactory state. It maintains a list of states ordered by distance.


231 
It applies $tac$ to the head of this list; if the result contains any


232 
satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST}


233 
adds the new states to the list, and continues.


234 


235 
The distance function is typically \ttindex{size_of_thm}, which computes


236 
the size of the state. The smaller the state, the fewer and simpler


237 
subgoals it has.


238 


239 
\item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$]


240 
is like {\tt BEST_FIRST}, except that the priority queue initially


241 
contains the result of applying $tac@0$ to the proof state. This tactical


242 
permits separate tactics for starting the search and continuing the search.


243 


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

286

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


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

104

247 
\end{description}


248 


249 


250 
\subsection{Auxiliary tacticals for searching}


251 
\index{tacticals!conditional}


252 
\index{tacticals!deterministic}


253 
\begin{ttbox}


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


255 
IF_UNSOLVED : tactic > tactic


256 
DETERM : tactic > tactic


257 
\end{ttbox}


258 
\begin{description}


259 
\item[\tt \tt COND {\it p} $tac@1$ $tac@2$]


260 
applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$


261 
otherwise. It is a conditional tactical in that only one of $tac@1$ and


262 
$tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are


263 
evaluated because \ML{} uses eager evaluation.


264 


265 
\item[\ttindexbold{IF_UNSOLVED} {\it tac}]


266 
applies {\it tac\/} to the proof state if it has any subgoals, and simply


267 
returns the proof state otherwise. Many common tactics, such as {\tt


268 
resolve_tac}, fail if applied to a proof state that has no subgoals.


269 


270 
\item[\ttindexbold{DETERM} {\it tac}]


271 
applies {\it tac\/} to the proof state and returns the head of the


272 
resulting sequence. {\tt DETERM} limits the search space by making its


273 
argument deterministic.


274 
\end{description}


275 


276 


277 
\subsection{Predicates and functions useful for searching}


278 
\index{theorems!size of}


279 
\index{theorems!equality of}


280 
\begin{ttbox}


281 
has_fewer_prems : int > thm > bool


282 
eq_thm : thm * thm > bool


283 
size_of_thm : thm > int


284 
\end{ttbox}


285 
\begin{description}


286 
\item[\ttindexbold{has_fewer_prems} $n$ $thm$]


287 
reports whether $thm$ has fewer than~$n$ premises. By currying,


288 
\hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may


289 
be given to the searching tacticals.


290 


291 
\item[\ttindexbold{eq_thm}($thm1$,$thm2$)]


292 
reports whether $thm1$ and $thm2$ are equal. Both theorems must have


293 
identical signatures. Both theorems must have the same conclusions, and


294 
the same hypotheses, in the same order. Names of bound variables are


295 
ignored.


296 


297 
\item[\ttindexbold{size_of_thm} $thm$]


298 
computes the size of $thm$, namely the number of variables, constants and


299 
abstractions in its conclusion. It may serve as a distance function for


300 
\ttindex{BEST_FIRST}.


301 
\end{description}


302 


303 


304 
\section{Tacticals for subgoal numbering}


305 
When conducting a backward proof, we normally consider one goal at a time.


306 
A tactic can affect the entire proof state, but many tactics  such as


307 
{\tt resolve_tac} and {\tt assume_tac}  work on a single subgoal.


308 
Subgoals are designated by a positive integer, so Isabelle provides


309 
tacticals for combining values of type {\tt int>tactic}.


310 


311 


312 
\subsection{Restricting a tactic to one subgoal}


313 
\index{tactics!restricting to a subgoal}


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


315 
\begin{ttbox}


316 
SELECT_GOAL : tactic > int > tactic


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


318 
\end{ttbox}


319 
\begin{description}


320 
\item[\ttindexbold{SELECT_GOAL} {\it tac} $i$]


321 
restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It


322 
fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal


323 
(do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof


324 
state and uses the result to refine the original proof state at


325 
subgoal~$i$. If {\it tac\/} returns multiple results then so does


326 
\hbox{\tt SELECT_GOAL {\it tac} $i$}.


327 


328 
Its workings are devious. {\tt SELECT_GOAL} creates a state of the


329 
form $\phi\Imp\phi$, with one subgoal. If subgoal~$i$ has the form say


330 
$\psi\Imp\theta$, then {\tt SELECT_GOAL} creates the state


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


332 
rather than $\List{\psi\Imp\theta;\; \psi}\Imp\theta$, which has two


333 
subgoals.


334 


335 
\item[\ttindexbold{METAHYPS} {\it tacf} $i$]


336 
takes subgoal~$i$, of the form


337 
\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]


338 
and creates the list $\theta'@1$, \ldots, $\theta'@k$ of metalevel


339 
assumptions. In these theorems, the subgoal's parameters ($x@1$,


340 
\ldots,~$x@l$) become free variables. It supplies the assumptions to


341 
$tacf$ and applies the resulting tactic to the proof state


342 
$\theta\Imp\theta$.


343 


344 
If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,


345 
possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is


346 
lifted back into the original context, yielding $n$ subgoals.


347 

286

348 
Metalevel assumptions may not contain unknowns. Unknowns in the


349 
hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,


350 
\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call


351 
cannot instantiate them. Unknowns in $\theta$ may be instantiated. New


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

104

353 


354 
Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves


355 
subgoal~$i$ with one of its own assumptions, which may itself have the form


356 
of an inference rule (these are called {\bf higherlevel assumptions}).


357 
\begin{ttbox}


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


359 
\end{ttbox}


360 
\end{description}


361 


362 
\begin{warn}


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


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


365 
\end{warn}


366 


367 


368 
\subsection{Scanning for a subgoal by number}


369 
\index{tacticals!scanning for subgoalsbold}


370 
\begin{ttbox}


371 
ALLGOALS : (int > tactic) > tactic


372 
TRYALL : (int > tactic) > tactic


373 
SOMEGOAL : (int > tactic) > tactic


374 
FIRSTGOAL : (int > tactic) > tactic


375 
REPEAT_SOME : (int > tactic) > tactic


376 
REPEAT_FIRST : (int > tactic) > tactic


377 
trace_goalno_tac : (int > tactic) > int > tactic


378 
\end{ttbox}


379 
These apply a tactic function of type {\tt int > tactic} to all the


380 
subgoal numbers of a proof state, and join the resulting tactics using


381 
\ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the


382 
subgoals, or to one subgoal.


383 


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


385 


386 
\begin{description}


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


388 
is equivalent to


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


390 


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


392 
avoid problems when subgoals are added or deleted).


393 


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


395 
is equivalent to


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


397 


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

286

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

104

400 
assumption.


401 


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


403 
is equivalent to


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


405 

286

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


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


408 
failing if this is impossible.

104

409 


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


411 
is equivalent to


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


413 


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


415 


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


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


418 


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


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


421 


422 
\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]


423 
applies \hbox{\it tac i\/} to the proof state. If the resulting sequence


424 
is nonempty, then it is returned, with the sideeffect of printing {\tt


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


426 
sequence and prints nothing.


427 


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


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


430 
\end{description}


431 


432 


433 
\subsection{Joining tactic functions}


434 
\index{tacticals!joining tactic functionsbold}


435 
\begin{ttbox}


436 
THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix 1}


437 
ORELSE' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix}


438 
APPEND' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix}


439 
INTLEAVE' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix}


440 
EVERY' : ('a > tactic) list > 'a > tactic


441 
FIRST' : ('a > tactic) list > 'a > tactic


442 
\end{ttbox}


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


444 
\begin{ttbox}


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


446 
\end{ttbox}


447 
can be simplified to


448 
\begin{ttbox}


449 
SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)


450 
\end{ttbox}


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


452 
provided, because function composition accomplishes the same purpose.


453 
The tactic


454 
\begin{ttbox}


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


456 
\end{ttbox}


457 
can be simplified to


458 
\begin{ttbox}


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


460 
\end{ttbox}


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


462 
\begin{center} \tt


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


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


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


466 


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


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


469 


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


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


472 


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


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


475 


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


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


478 


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


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


481 
\end{tabular}


482 
\end{center}


483 


484 


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


486 
\index{tacticals!joining tactic functionsbold}


487 
\begin{ttbox}


488 
EVERY1: (int > tactic) list > tactic


489 
FIRST1: (int > tactic) list > tactic


490 
\end{ttbox}


491 
A common proof style is to treat the subgoals as a stack, always


492 
restricting attention to the first subgoal. Such proofs contain long lists


493 
of tactics, each applied to~1. These can be simplified using {\tt EVERY1}


494 
and {\tt FIRST1}:


495 
\begin{center} \tt


496 
\begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}


497 
EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &


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


499 


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


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


502 
\end{tabular}


503 
\end{center}


504 


505 
\index{tacticals)}
