author wenzelm Wed, 15 Feb 2012 20:47:32 +0100 changeset 46491 c505ea79e2db parent 46490 e4863ab5e09b child 46492 bf96ed9e55c1
removed obsolete files;
 doc-src/Ref/defining.tex file | annotate | diff | comparison | revisions doc-src/Ref/tctical.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/defining.tex	Wed Feb 15 20:41:13 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,314 +0,0 @@
-
-\chapter{Defining Logics} \label{Defining-Logics}
-
-\section{Mixfix declarations} \label{sec:mixfix}
-\index{mixfix declarations|(}
-
-When defining a theory, you declare new constants by giving their names,
-their type, and an optional {\bf mixfix annotation}.  Mixfix annotations
-allow you to extend Isabelle's basic $\lambda$-calculus syntax with
-readable notation.  They can express any context-free priority grammar.
-Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
-general than the priority declarations of \ML\ and Prolog.
-
-A mixfix annotation defines a production of the priority grammar.  It
-describes the concrete syntax, the translation to abstract syntax, and the
-pretty printing.  Special case annotations provide a simple means of
-specifying infix operators and binders.
-
-\subsection{The general mixfix form}
-Here is a detailed account of mixfix declarations.  Suppose the following
-line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy}
-file:
-\begin{center}
-  {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
-\end{center}
-This constant declaration and mixfix annotation are interpreted as follows:
-\begin{itemize}\index{productions}
-\item The string {\tt $c$} is the name of the constant associated with the
-  production; unless it is a valid identifier, it must be enclosed in
-  quotes.  If $c$ is empty (given as~{\tt ""}) then this is a copy
-  production.\index{productions!copy} Otherwise, parsing an instance of the
-  phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
-    $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
-  argument.
-
-  \item The constant $c$, if non-empty, is declared to have type $\sigma$
-    ({\tt consts} section only).
-
-  \item The string $template$ specifies the right-hand side of
-    the production.  It has the form
-    $w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n,$
-    where each occurrence of {\tt_} denotes an argument position and
-    the~$w@i$ do not contain~{\tt _}.  (If you want a literal~{\tt _} in
-    the concrete syntax, you must escape it as described below.)  The $w@i$
-    may consist of \rmindex{delimiters}, spaces or
-    \rmindex{pretty printing} annotations (see below).
-
-  \item The type $\sigma$ specifies the production's nonterminal symbols
-    (or name tokens).  If $template$ is of the form above then $\sigma$
-    must be a function type with at least~$n$ argument positions, say
-    $\sigma = [\tau@1, \dots, \tau@n] \To \tau$.  Nonterminal symbols are
-    derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described
-    below.  Any of these may be function types.
-
-  \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
-      [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
-    priority\indexbold{priorities} required of any phrase that may appear
-    as the $i$-th argument.  Missing priorities default to~0.
-
-  \item The integer $p$ is the priority of this production.  If
-    omitted, it defaults to the maximal priority.  Priorities range
-    between 0 and \ttindexbold{max_pri} (= 1000).
-
-\end{itemize}
-%
-The resulting production is $A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, -A@2^{(p@2)}\, \dots\, A@n^{(p@n)}\, w@n$ where $A$ and the $A@i$ are the
-nonterminals corresponding to the types $\tau$ and $\tau@i$ respectively.
-The nonterminal symbol associated with a type $(\ldots)ty$ is {\tt logic}, if
-this is a logical type (namely one of class {\tt logic} excluding {\tt
-prop}).  Otherwise it is $ty$ (note that only the outermost type constructor
-is taken into account).  Finally, the nonterminal of a type variable is {\tt
-any}.
-
-\begin{warn}
-  Theories must sometimes declare types for purely syntactic purposes ---
-  merely playing the role of nonterminals.  One example is \tydx{type}, the
-  built-in type of types.  This is a type of all types' in the syntactic
-  sense only.  Do not declare such types under {\tt arities} as belonging to
-  class {\tt logic}\index{*logic class}, for that would make them useless as
-  separate nonterminal symbols.
-\end{warn}
-
-Associating nonterminals with types allows a constant's type to specify
-syntax as well.  We can declare the function~$f$ to have type $[\tau@1, -\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the layout
-of the function's $n$ arguments.  The constant's name, in this case~$f$, will
-also serve as the label in the abstract syntax tree.
-
-You may also declare mixfix syntax without adding constants to the theory's
-signature, by using a {\tt syntax} section instead of {\tt consts}.  Thus a
-production need not map directly to a logical function (this typically
-Chapter~\ref{chap:syntax}).
-
-
-\medskip
-As a special case of the general mixfix declaration, the form
-\begin{center}
-  {\tt $c$ ::\ "$\sigma$" ("$template$")}
-\end{center}
-specifies no priorities.  The resulting production puts no priority
-constraints on any of its arguments and has maximal priority itself.
-Omitting priorities in this manner is prone to syntactic ambiguities unless
-the production's right-hand side is fully bracketed, as in
-\verb|"if _ then _ else _ fi"|.
-
-Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
-is sensible only if~$c$ is an identifier.  Otherwise you will be unable to
-write terms involving~$c$.
-
-
-\subsection{Example: arithmetic expressions}
-\index{examples!of mixfix declarations}
-This theory specification contains a {\tt syntax} section with mixfix
-declarations encoding the priority grammar from
-\S\ref{sec:priority_grammars}:
-\begin{ttbox}
-ExpSyntax = Pure +
-types
-  exp
-syntax
-  "0" :: exp                 ("0"      9)
-  "+" :: [exp, exp] => exp   ("_ + _"  [0, 1] 0)
-  "*" :: [exp, exp] => exp   ("_ * _"  [3, 2] 2)
-  "-" :: exp => exp          ("- _"    [3] 3)
-end
-\end{ttbox}
-Executing {\tt Syntax.print_gram} reveals the productions derived from the
-above mixfix declarations (lots of additional information deleted):
-\begin{ttbox}
-Syntax.print_gram (syn_of ExpSyntax.thy);
-{\out exp = "0"  => "0" (9)}
-{\out exp = exp[0] "+" exp[1]  => "+" (0)}
-{\out exp = exp[3] "*" exp[2]  => "*" (2)}
-{\out exp = "-" exp[3]  => "-" (3)}
-\end{ttbox}
-
-Note that because {\tt exp} is not of class {\tt logic}, it has been
-retained as a separate nonterminal.  This also entails that the syntax
-does not provide for identifiers or paranthesized expressions.
-Normally you would also want to add the declaration {\tt arities
-  exp::logic} after {\tt types} and use {\tt consts} instead of {\tt
-  syntax}.  Try this as an exercise and study the changes in the
-grammar.
-
-
-\subsection{Infixes}
-\indexbold{infixes}
-
-Infix operators associating to the left or right can be declared using
-{\tt infixl} or {\tt infixr}.  Basically, the form {\tt $c$ ::\
-  $\sigma$ (infixl $p$)} abbreviates the mixfix declarations
-\begin{ttbox}
-"op $$c$$" :: $$\sigma$$   ("(_ $$c$$/ _)" [$$p$$, $$p+1$$] $$p$$)
-"op $$c$$" :: $$\sigma$$   ("op $$c$$")
-\end{ttbox}
-and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations
-\begin{ttbox}
-"op $$c$$" :: $$\sigma$$   ("(_ $$c$$/ _)" [$$p+1$$, $$p$$] $$p$$)
-"op $$c$$" :: $$\sigma$$   ("op $$c$$")
-\end{ttbox}
-The infix operator is declared as a constant with the prefix {\tt op}.
-Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
-function symbols, as in \ML.  Special characters occurring in~$c$ must be
-escaped, as in delimiters, using a single quote.
-
-A slightly more general form of infix declarations allows constant
-names to be independent from their concrete syntax, namely \texttt{$c$
-  ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}.  As
-an example consider:
-\begin{ttbox}
-and :: [bool, bool] => bool  (infixr "&" 35)
-\end{ttbox}
-The internal constant name will then be just \texttt{and}, without any
-\texttt{op} prefixed.
-
-
-\subsection{Binders}
-\indexbold{binders}
-\begingroup
-\def\Q{{\cal Q}}
-A {\bf binder} is a variable-binding construct such as a quantifier.  The
-constant declaration
-\begin{ttbox}
-$$c$$ :: $$\sigma$$   (binder "$$\Q$$" [$$pb$$] $$p$$)
-\end{ttbox}
-introduces a constant~$c$ of type~$\sigma$, which must have the form
-$(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
-$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
-and the whole term has type~$\tau@3$.  The optional integer $pb$
-specifies the body's priority, by default~$p$.  Special characters
-in $\Q$ must be escaped using a single quote.
-
-The declaration is expanded internally to something like
-\begin{ttbox}
-$$c$$\hskip3pt    :: ($$\tau@1$$ => $$\tau@2$$) => $$\tau@3$$
-"$$\Q$$"  :: [idts, $$\tau@2$$] => $$\tau@3$$   ("(3$$\Q$$_./ _)" [0, $$pb$$] $$p$$)
-\end{ttbox}
-Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
-\index{type constraints}
-optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The
-declaration also installs a parse translation\index{translations!parse}
-for~$\Q$ and a print translation\index{translations!print} for~$c$ to
-translate between the internal and external forms.
-
-A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a
-list of variables.  The external form $\Q~x@1~x@2 \ldots x@n. P$
-corresponds to the internal form
-$c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)).$
-
-\medskip
-For example, let us declare the quantifier~$\forall$:\index{quantifiers}
-\begin{ttbox}
-All :: ('a => o) => o   (binder "ALL " 10)
-\end{ttbox}
-This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
-  $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall
-back on ${\tt All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL
-  $x$.$P$} have type~$o$, the type of formulae, while the bound variable
-can be polymorphic.
-\endgroup
-
-\index{mixfix declarations|)}
-
-
-\section{*Alternative print modes} \label{sec:prmodes}
-\index{print modes|(}
-%
-Isabelle's pretty printer supports alternative output syntaxes.  These
-may be used independently or in cooperation.  The currently active
-print modes (with precedence from left to right) are determined by a
-reference variable.
-\begin{ttbox}\index{*print_mode}
-print_mode: string list ref
-\end{ttbox}
-Initially this may already contain some print mode identifiers,
-depending on how Isabelle has been invoked (e.g.\ by some user
-interface).  So changes should be incremental --- adding or deleting
-modes relative to the current value.
-
-Any \ML{} string is a legal print mode identifier, without any predeclaration
-required.  The following names should be considered reserved, though:
-\texttt{""} (the empty string), \texttt{symbols}, \texttt{xsymbols}, and
-\texttt{latex}.
-
-There is a separate table of mixfix productions for pretty printing
-associated with each print mode.  The currently active ones are
-conceptually just concatenated from left to right, with the standard
-syntax output table always coming last as default.  Thus mixfix
-productions of preceding modes in the list may override those of later
-ones.
-
-\medskip The canonical application of print modes is optional printing
-of mathematical symbols from a special screen font instead of {\sc
-  ascii}.  Another example is to re-use Isabelle's advanced
-$\lambda$-term printing mechanisms to generate completely different
-output, say for interfacing external tools like \rmindex{model
-
-\index{print modes|)}
-
-
-\section{Ambiguity of parsed expressions} \label{sec:ambiguity}
-\index{ambiguity!of parsed expressions}
-
-To keep the grammar small and allow common productions to be shared
-all logical types (except {\tt prop}) are internally represented
-by one nonterminal, namely {\tt logic}.  This and omitted or too freely
-chosen priorities may lead to ways of parsing an expression that were
-not intended by the theory's maker.  In most cases Isabelle is able to
-select one of multiple parse trees that an expression has lead
-to by checking which of them can be typed correctly.  But this may not
-work in every case and always slows down parsing.
-The warning and error messages that can be produced during this process are
-as follows:
-
-If an ambiguity can be resolved by type inference the following
-warning is shown to remind the user that parsing is (unnecessarily)
-slowed down.  In cases where it's not easily possible to eliminate the
-ambiguity the frequency of the warning can be controlled by changing
-the value of {\tt Syntax.ambiguity_level} which has type {\tt int
-ref}.  Its default value is 1 and by increasing it one can control how
-many parse trees are necessary to generate the warning.
-
-\begin{ttbox}
-{\out Ambiguous input "\dots"}
-{\out produces the following parse trees:}
-{\out \dots}
-{\out Fortunately, only one parse tree is type correct.}
-{\out You may still want to disambiguate your grammar or your input.}
-\end{ttbox}
-
-The following message is normally caused by using the same
-syntax in two different productions:
-
-\begin{ttbox}
-{\out Ambiguous input "..."}
-{\out produces the following parse trees:}
-{\out \dots}
-{\out More than one term is type correct:}
-{\out \dots}
-\end{ttbox}
-
-Ambiguities occuring in syntax translation rules cannot be resolved by
-type inference because it is not necessary for these rules to be type
-correct.  Therefore Isabelle always generates an error message and the
-ambiguity should be eliminated by changing the grammar or the rule.
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: 
--- a/doc-src/Ref/tctical.tex	Wed Feb 15 20:41:13 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,544 +0,0 @@
-
-\chapter{Tacticals}
-\index{tacticals|(}
-Tacticals are operations on tactics.  Their implementation makes use of
-functional programming techniques, especially for sequences.  Most of the
-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
-\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}
-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|)}
-
-
-\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: