\chapter{Tacticals}

 \index{tacticals|(}

 Tacticals are operations on tactics.  Their implementation makes use of

 functional programming techniques, especially for sequences.  Most of the

 time, you may forget about this and regard tacticals as high-level control

 structures.

 \section{The basic tacticals}

 \subsection{Joining two tactics}

 \index{tacticals!joining two tactics}

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

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

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

 alternation.

 \begin{ttbox} 

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

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

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

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

 \end{ttbox}

 \begin{ttdescription}

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

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

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

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

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

 concatenates the results.

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

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

 tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it

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

 $tac@2$ is excluded.

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

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

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

 search.\index{search}

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

 interleaves the results of $tac@1$ and~$tac@2$.  Thus, it includes all

 possible next states, even if one of the tactics returns an infinite

 sequence.

 \end{ttdescription}

 \subsection{Joining a list of tactics}

 \index{tacticals!joining a list of tactics}

 \begin{ttbox} 

 EVERY : tactic list -> tactic

 FIRST : tactic list -> tactic

 \end{ttbox}

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

 {\tt ORELSE}\@.

 \begin{ttdescription}

 \item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}] 

 abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}.  It is useful for

 writing a series of tactics to be executed in sequence.

 \item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}] 

 abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}.  It is useful for

 writing a series of tactics to be attempted one after another.

 \end{ttdescription}

 \subsection{Repetition tacticals}

 \index{tacticals!repetition}

 \begin{ttbox} 

 TRY             : tactic -> tactic

 REPEAT_DETERM   : tactic -> tactic

 REPEAT_DETERM_N : int -> tactic -> tactic

 REPEAT          : tactic -> tactic

 REPEAT1         : tactic -> tactic

 DETERM_UNTIL    : (thm -> bool) -> tactic -> tactic

 trace_REPEAT    : bool ref \hfill{\bf initially false}

 \end{ttbox}

 \begin{ttdescription}

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

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

 if non-empty; otherwise it returns the original state.  Thus, it applies

 {\it tac\/} at most once.

 \item[\ttindexbold{REPEAT_DETERM} {\it tac}] 

 applies {\it tac\/} to the proof state and, recursively, to the head of the

 resulting sequence.  It returns the first state to make {\it tac\/} fail.

 It is deterministic, discarding alternative outcomes.

 \item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] 

 is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions

 is bound by {\it n} (unless negative).

 \item[\ttindexbold{REPEAT} {\it tac}] 

 applies {\it tac\/} to the proof state and, recursively, to each element of

 the resulting sequence.  The resulting sequence consists of those states

 that make {\it tac\/} fail.  Thus, it applies {\it tac\/} as many times as

 possible (including zero times), and allows backtracking over each

 invocation of {\it tac}.  It is more general than {\tt REPEAT_DETERM}, but

 requires more space.

 \item[\ttindexbold{REPEAT1} {\it tac}] 

 is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at

 least once, failing if this is impossible.

 \item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] 

 applies {\it tac\/} to the proof state and, recursively, to the head of the

 resulting sequence, until the predicate {\it p} (applied on the proof state)

 yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate 

 states. It is deterministic, discarding alternative outcomes.

 \item[set \ttindexbold{trace_REPEAT};] 

 enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}

 and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.

 \end{ttdescription}

 \subsection{Identities for tacticals}

 \index{tacticals!identities for}

 \begin{ttbox} 

 all_tac : tactic

 no_tac  : tactic

 \end{ttbox}

 \begin{ttdescription}

 \item[\ttindexbold{all_tac}] 

 maps any proof state to the one-element sequence containing that state.

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

 tactical \ttindex{THEN}\@.

 \item[\ttindexbold{no_tac}] 

 maps any proof state to the empty sequence.  Thus it succeeds for no state.

 It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and 

 \ttindex{INTLEAVE}\@.  Also, it is a zero element for \ttindex{THEN}, which means that

 \hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}.

 \end{ttdescription}

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

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

 as follows: 

 \begin{ttbox} 

 fun TRY tac = tac ORELSE all_tac;

 fun REPEAT tac =

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

 \end{ttbox}

 If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.

 Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt

 INTLEAVE}, it applies $tac$ as many times as possible in each

 outcome.

 \begin{warn}

 Note {\tt REPEAT}'s explicit abstraction over the proof state.  Recursive

 tacticals must be coded in this awkward fashion to avoid infinite

 recursion.  With the following definition, \hbox{\tt REPEAT $tac$} would

 loop due to \ML's eager evaluation strategy:

 \begin{ttbox} 

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

 \end{ttbox}

 \par\noindent

 The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly

 and using tail recursion.  This sacrifices clarity, but saves much space by

 discarding intermediate proof states.

 \end{warn}

 \section{Control and search tacticals}

 \index{search!tacticals|(}

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

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

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

 to express.  The main search procedures, depth-first, breadth-first and

 best-first, are provided as tacticals.  They generate the search tree by

 repeatedly applying a given tactic.

 \subsection{Filtering a tactic's results}

 \index{tacticals!for filtering}

 \index{tactics!filtering results of}

 \begin{ttbox} 

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

 CHANGED : tactic -> tactic

 \end{ttbox}

 \begin{ttdescription}

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

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

 result states that satisfy~$p$.

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

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

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

 always has some effect on the state.

 \end{ttdescription}

 \subsection{Depth-first search}

 \index{tacticals!searching}

 \index{tracing!of searching tacticals}

 \begin{ttbox} 

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

 DEPTH_SOLVE   :                tactic -> tactic

 DEPTH_SOLVE_1 :                tactic -> tactic

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

 \end{ttbox}

 \begin{ttdescription}

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

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

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

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

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

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

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

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

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

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

 \item[set \ttindexbold{trace_DEPTH_FIRST};] 

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

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

 \end{ttdescription}

 \subsection{Other search strategies}

 \index{tacticals!searching}

 \index{tracing!of searching tacticals}

 \begin{ttbox} 

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

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

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

                   -> tactic                    \hfill{\bf infix 1}

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

 \end{ttbox}

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

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

 result from {\it tac}.

 \begin{ttdescription}

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

 uses breadth-first search to find states for which {\it satp\/} is true.

 For most applications, it is too slow.

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

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

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

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

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

 adds the new states to the list, and continues.  

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

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

 subgoals it has.

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

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

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

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

 \item[set \ttindexbold{trace_BEST_FIRST};] 

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

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

 \end{ttdescription}

 \subsection{Auxiliary tacticals for searching}

 \index{tacticals!conditional}

 \index{tacticals!deterministic}

 \begin{ttbox} 

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

 IF_UNSOLVED         : tactic -> tactic

 SOLVE               : tactic -> tactic

 DETERM              : tactic -> tactic

 DETERM_UNTIL_SOLVED : tactic -> tactic

 \end{ttbox}

 \begin{ttdescription}

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

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

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

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

 evaluated because \ML{} uses eager evaluation.

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

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

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

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

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

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

 left.

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

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

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

 argument deterministic.

 \item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] 

 forces repeated deterministic application of {\it tac\/} to the proof state 

 until the goal is solved completely.

 \end{ttdescription}

 \subsection{Predicates and functions useful for searching}

 \index{theorems!size of}

 \index{theorems!equality of}

 \begin{ttbox} 

 has_fewer_prems : int -> thm -> bool

 eq_thm          : thm * thm -> bool

 eq_thm_prop     : thm * thm -> bool

 size_of_thm     : thm -> int

 \end{ttbox}

 \begin{ttdescription}

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

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

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

 be given to the searching tacticals.

 \item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and

   $thm@2$ are equal.  Both theorems must have compatible signatures.  Both

   theorems must have the same conclusions, the same hypotheses (in the same

   order), and the same set of sort hypotheses.  Names of bound variables are

   ignored.

 \item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the

   propositions of $thm@1$ and $thm@2$ are equal.  Names of bound variables are

   ignored.

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

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

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

 \ttindex{BEST_FIRST}. 

 \end{ttdescription}

 \index{search!tacticals|)}

 \section{Tacticals for subgoal numbering}

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

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

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

 Subgoals are designated by a positive integer, so Isabelle provides

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

 \subsection{Restricting a tactic to one subgoal}

 \index{tactics!restricting to a subgoal}

 \index{tacticals!for restriction to a subgoal}

 \begin{ttbox} 

 SELECT_GOAL : tactic -> int -> tactic

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

 \end{ttbox}

 \begin{ttdescription}

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

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

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

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

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

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

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

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

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

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

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

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

   SELECT_GOAL} inserts a quantifier to create the state

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

 \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}

 takes subgoal~$i$, of the form 

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

 and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level

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

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

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

 $\theta\Imp\theta$.

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

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

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

 Meta-level assumptions may not contain unknowns.  Unknowns in the

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

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

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

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

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

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

 of an inference rule (these are called {\bf higher-level assumptions}).  

 \begin{ttbox} 

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

 \end{ttbox} 

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

   METAHYPS}. 

 \end{ttdescription}

 \begin{warn}

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

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

 \end{warn}

 \subsection{Scanning for a subgoal by number}

 \index{tacticals!scanning for subgoals}

 \begin{ttbox} 

 ALLGOALS         : (int -> tactic) -> tactic

 TRYALL           : (int -> tactic) -> tactic

 SOMEGOAL         : (int -> tactic) -> tactic

 FIRSTGOAL        : (int -> tactic) -> tactic

 REPEAT_SOME      : (int -> tactic) -> tactic

 REPEAT_FIRST     : (int -> tactic) -> tactic

 trace_goalno_tac : (int -> tactic) -> int -> tactic

 \end{ttbox}

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

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

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

 subgoals, or to one subgoal.  

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

 \begin{ttdescription}

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

 is equivalent to

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

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

 avoid problems when subgoals are added or deleted).

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

 is equivalent to

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

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

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

 assumption.

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

 is equivalent to

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

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

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

 failing if this is impossible.

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

 is equivalent to

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

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

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

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

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

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

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

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

 is non-empty, then it is returned, with the side-effect of printing {\tt

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

 sequence and prints nothing.

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

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

 \end{ttdescription}

 \subsection{Joining tactic functions}

 \index{tacticals!joining tactic functions}

 \begin{ttbox} 

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

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

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

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

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

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

 \end{ttbox}

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

 \begin{ttbox} 

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

 \end{ttbox}

 can be simplified to

 \begin{ttbox} 

 SOMEGOAL (resolve_tac rls  ORELSE'  eresolve_tac erls)

 \end{ttbox}

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

 provided, because function composition accomplishes the same purpose.

 The tactic

 \begin{ttbox} 

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

 \end{ttbox}

 can be simplified to

 \begin{ttbox} 

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

 \end{ttbox}

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

 \begin{center} \tt

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

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

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

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

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

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

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

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

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

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

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

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

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

 \end{tabular}

 \end{center}

 \subsection{Applying a list of tactics to 1}

 \index{tacticals!joining tactic functions}

 \begin{ttbox} 

 EVERY1: (int -> tactic) list -> tactic

 FIRST1: (int -> tactic) list -> tactic

 \end{ttbox}

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

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

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

 and {\tt FIRST1}:

 \begin{center} \tt

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

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

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

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

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

 \end{tabular}

 \end{center}

 \index{tacticals|)}

 %%% Local Variables: 

 %%% mode: latex

 %%% TeX-master: "ref"

 %%% End: