%% $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_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
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 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 $\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: