%% $Id$

 \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        : tactic -> tactic

 REPEAT1       : 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} {\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} := true;] 

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

 \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[\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{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[\ttindexbold{trace_DEPTH_FIRST} := true;] 

 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[\ttindexbold{trace_BEST_FIRST} := true;] 

 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

 DETERM      : tactic -> tactic

 \end{ttbox}

 \begin{ttdescription}

 \item[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{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

 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}($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{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 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} 

 \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|)}