--- 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
-requires additional syntactic translations, see also
-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
- checkers} (see also \texttt{HOL/Modelcheck}).
-
-\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
-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
-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: