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 

4317

99 
\item[set \ttindexbold{trace_REPEAT};]

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 

3108

129 
fun REPEAT tac =


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

104

131 
\end{ttbox}


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


135 
outcome.


136 


137 
\begin{warn}


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

332

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

104

142 
\begin{ttbox}


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


144 
\end{ttbox}


145 
\par\noindent


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


149 
\end{warn}


150 


151 


152 
\section{Control and search tacticals}

323

153 
\index{search!tacticals(}


154 

104

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


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


160 
repeatedly applying a given tactic.


161 


162 


163 
\subsection{Filtering a tactic's results}

323

164 
\index{tacticals!for filtering}


165 
\index{tactics!filtering results of}

104

166 
\begin{ttbox}


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


168 
CHANGED : tactic > tactic


169 
\end{ttbox}

323

170 
\begin{ttdescription}

1118

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

104

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


173 
result states that satisfy~$p$.


174 


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.

323

179 
\end{ttdescription}

104

180 


181 


182 
\subsection{Depthfirst search}

323

183 
\index{tacticals!searching}

104

184 
\index{tracing!of searching tacticals}


185 
\begin{ttbox}


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

332

187 
DEPTH_SOLVE : tactic > tactic


188 
DEPTH_SOLVE_1 : tactic > tactic

104

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


190 
\end{ttbox}

323

191 
\begin{ttdescription}

104

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.


197 


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


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


200 


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.


204 

4317

205 
\item[set \ttindexbold{trace_DEPTH_FIRST};]

104

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


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

323

208 
\end{ttdescription}

104

209 


210 


211 
\subsection{Other search strategies}

323

212 
\index{tacticals!searching}

104

213 
\index{tracing!of searching tacticals}


214 
\begin{ttbox}

332

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

104

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}


220 
\end{ttbox}


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

323

224 
\begin{ttdescription}

104

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


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


227 
For most applications, it is too slow.


228 


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.


235 


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


238 
subgoals it has.


239 


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.


244 

4317

245 
\item[set \ttindexbold{trace_BEST_FIRST};]

286

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


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

323

248 
\end{ttdescription}

104

249 


250 


251 
\subsection{Auxiliary tacticals for searching}


252 
\index{tacticals!conditional}


253 
\index{tacticals!deterministic}


254 
\begin{ttbox}


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


256 
IF_UNSOLVED : tactic > tactic

5754

257 
SOLVE : tactic > tactic

104

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 

5754

272 
\item[\ttindexbold{SOLVE} {\it tac}]


273 
applies {\it tac\/} to the proof state and then fails iff there are subgoals


274 
left.


275 

104

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.

323

280 
\end{ttdescription}

104

281 


282 


283 
\subsection{Predicates and functions useful for searching}


284 
\index{theorems!size of}


285 
\index{theorems!equality of}


286 
\begin{ttbox}


287 
has_fewer_prems : int > thm > bool


288 
eq_thm : thm * thm > bool


289 
size_of_thm : thm > int


290 
\end{ttbox}

323

291 
\begin{ttdescription}

104

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.


296 

4317

297 
\item[\ttindexbold{eq_thm} ($thm_1$, $thm_2$)] reports whether $thm_1$


298 
and $thm_2$ are equal. Both theorems must have identical


299 
signatures. Both theorems must have the same conclusions, and the


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


301 
ignored.

104

302 


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


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


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


306 
\ttindex{BEST_FIRST}.

323

307 
\end{ttdescription}


308 


309 
\index{search!tacticals)}

104

310 


311 


312 
\section{Tacticals for subgoal numbering}


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


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


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


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


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


318 


319 


320 
\subsection{Restricting a tactic to one subgoal}


321 
\index{tactics!restricting to a subgoal}


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


323 
\begin{ttbox}


324 
SELECT_GOAL : tactic > int > tactic


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


326 
\end{ttbox}

323

327 
\begin{ttdescription}

104

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


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


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


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


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


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


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


335 

323

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

332

337 
with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$


338 
then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact


339 
$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.


340 
Such a proof state might cause tactics to go astray. Therefore {\tt


341 
SELECT_GOAL} inserts a quantifier to create the state

323

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

104

343 

323

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

104

345 
takes subgoal~$i$, of the form


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


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


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


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


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


351 
$\theta\Imp\theta$.


352 


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


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


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


356 

286

357 
Metalevel assumptions may not contain unknowns. Unknowns in the


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


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


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

323

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

104

362 


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


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


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


366 
\begin{ttbox}


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


368 
\end{ttbox}

332

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


370 
METAHYPS}.

323

371 
\end{ttdescription}

104

372 


373 
\begin{warn}


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


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


376 
\end{warn}


377 


378 


379 
\subsection{Scanning for a subgoal by number}

323

380 
\index{tacticals!scanning for subgoals}

104

381 
\begin{ttbox}


382 
ALLGOALS : (int > tactic) > tactic


383 
TRYALL : (int > tactic) > tactic


384 
SOMEGOAL : (int > tactic) > tactic


385 
FIRSTGOAL : (int > tactic) > tactic


386 
REPEAT_SOME : (int > tactic) > tactic


387 
REPEAT_FIRST : (int > tactic) > tactic


388 
trace_goalno_tac : (int > tactic) > int > tactic


389 
\end{ttbox}


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


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


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


393 
subgoals, or to one subgoal.


394 


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


396 

323

397 
\begin{ttdescription}

104

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


399 
is equivalent to


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


401 

323

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

104

403 
avoid problems when subgoals are added or deleted).


404 


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


406 
is equivalent to

323

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

104

408 


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

286

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

104

411 
assumption.


412 


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


414 
is equivalent to


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


416 

323

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

286

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


419 
failing if this is impossible.

104

420 


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


422 
is equivalent to


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


424 

323

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

104

426 


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

323

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

104

429 


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

323

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

104

432 


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


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


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


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


437 
sequence and prints nothing.


438 

323

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

104

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

323

441 
\end{ttdescription}

104

442 


443 


444 
\subsection{Joining tactic functions}

323

445 
\index{tacticals!joining tactic functions}

104

446 
\begin{ttbox}


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


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


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


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


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


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


453 
\end{ttbox}


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


455 
\begin{ttbox}


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


457 
\end{ttbox}


458 
can be simplified to


459 
\begin{ttbox}


460 
SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)


461 
\end{ttbox}


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


463 
provided, because function composition accomplishes the same purpose.


464 
The tactic


465 
\begin{ttbox}


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


467 
\end{ttbox}


468 
can be simplified to


469 
\begin{ttbox}


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


471 
\end{ttbox}


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


473 
\begin{center} \tt


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

323

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

104

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


477 

323

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

104

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


480 

323

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

104

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


483 

323

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

104

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


486 


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


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


489 


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


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


492 
\end{tabular}


493 
\end{center}


494 


495 


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

323

497 
\index{tacticals!joining tactic functions}

104

498 
\begin{ttbox}


499 
EVERY1: (int > tactic) list > tactic


500 
FIRST1: (int > tactic) list > tactic


501 
\end{ttbox}


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


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


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


505 
and {\tt FIRST1}:


506 
\begin{center} \tt


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


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


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


510 


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


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


513 
\end{tabular}


514 
\end{center}


515 


516 
\index{tacticals)}

5371

517 


518 


519 
%%% Local Variables:


520 
%%% mode: latex


521 
%%% TeXmaster: "ref"


522 
%%% End:
