doc-src/Ref/tctical.tex
changeset 104 d8205bb279a7
child 286 e7efbf03562b
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/tctical.tex	Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,505 @@
+%% $Id$
+\chapter{Tacticals}
+\index{tacticals|(}
+\index{tactics!combining|see{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|bold}
+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{description}
+\item[\tt $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[\tt $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[\tt $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.
+
+\item[\tt $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{description}
+
+
+\subsection{Joining a list of tactics}
+\index{tacticals!joining a list of tactics|bold}
+\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{description}
+\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{description}
+
+
+\subsection{Repetition tacticals}
+\index{tacticals!repetition|bold}
+\begin{ttbox} 
+TRY           : tactic -> tactic
+REPEAT_DETERM : tactic -> tactic
+REPEAT        : tactic -> tactic
+REPEAT1       : tactic -> tactic
+trace_REPEAT  : bool ref \hfill{\bf initially false}
+\end{ttbox}
+\begin{description}
+\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} {\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{trace_REPEAT} \tt:= true;] 
+enables an interactive tracing mode for {\tt REPEAT_DETERM} and {\tt
+REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
+\end{description}
+
+
+\subsection{Identities for tacticals}
+\index{tacticals!identities for|bold}
+\begin{ttbox} 
+all_tac : tactic
+no_tac  : tactic
+\end{ttbox}
+\begin{description}
+\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{description}
+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 = Tactic
+     (fn state => tapply((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:
+\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}
+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|bold}
+\index{tactics!filtering results of|bold}
+\begin{ttbox} 
+FILTER  : (thm -> bool) -> tactic -> tactic
+CHANGED : tactic -> tactic
+\end{ttbox}
+\begin{description}
+\item[\tt \tt 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{description}
+
+
+\subsection{Depth-first search}
+\index{tacticals!searching|bold}
+\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{description}
+\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[\ttindexbold{trace_DEPTH_FIRST} \tt:= true;] 
+enables interactive tracing for {\tt DEPTH_FIRST}.  To view the
+tracing options, type {\tt h} at the prompt.
+\end{description}
+
+
+\subsection{Other search strategies}
+\index{tacticals!searching|bold}
+\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{description}
+\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[\ttindexbold{trace_BEST_FIRST} \tt:= true;] 
+enables an interactive tracing mode for {\tt BEST_FIRST}.  To view the
+tracing options, type {\tt h} at the prompt.
+\end{description}
+
+
+\subsection{Auxiliary tacticals for searching}
+\index{tacticals!conditional}
+\index{tacticals!deterministic}
+\begin{ttbox} 
+COND        : (thm->bool) -> tactic -> tactic -> tactic
+IF_UNSOLVED : tactic -> tactic
+DETERM      : tactic -> tactic
+\end{ttbox}
+\begin{description}
+\item[\tt \tt 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{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.
+\end{description}
+
+
+\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
+size_of_thm     : thm -> int
+\end{ttbox}
+\begin{description}
+\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}($thm1$,$thm2$)] 
+reports whether $thm1$ and $thm2$ are equal.  Both theorems must have
+identical signatures.  Both theorems must have the same conclusions, and
+the same hypotheses, in the same order.  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{description}
+
+
+\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{description}
+\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$}.
+
+Its workings are devious.  {\tt SELECT_GOAL} creates a state of the
+form $\phi\Imp\phi$, with one subgoal.  If subgoal~$i$ has the form say
+$\psi\Imp\theta$, then {\tt SELECT_GOAL} creates the state 
+\[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta) \]
+rather than $\List{\psi\Imp\theta;\; \psi}\Imp\theta$, which has two
+subgoals.
+
+\item[\ttindexbold{METAHYPS} {\it tacf} $i$] 
+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
+$\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} 
+\end{description}
+
+\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|bold}
+\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{description}
+\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 {\bf 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,
+\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 {\bf downwards}.  
+\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 {\bf upwards}.
+
+\item[\ttindexbold{REPEAT_SOME} {\it tacf}] 
+applies {\it tacf} once or more to a subgoal, counting {\bf downwards}.
+
+\item[\ttindexbold{REPEAT_FIRST} {\it tacf}] 
+applies {\it tacf} once or more to a subgoal, counting {\bf 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{description}
+
+
+\subsection{Joining tactic functions}
+\index{tacticals!joining tactic functions|bold}
+\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|bold}
+\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|)}