--- a/doc-src/Ref/tctical.tex Thu Jan 26 21:25:18 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-
-\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: