\chapter{Tacticals}
\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|)}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: