summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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 -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: