doc-src/Ref/tactic.tex

+%% $Id$
+\chapter{Tactics} \label{tactics}
+\index{tactics|(}
+Tactics have type \ttindexbold{tactic}.  They are essentially
+functions from theorems to theorem sequences, where the theorems represent
+states of a backward proof.  Tactics seldom need to be coded from scratch,
+as functions; the basic tactics suffice for most proofs.
+
+\section{Resolution and assumption tactics}
+{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
+a rule.  {\bf Elim-resolution} is particularly suited for elimination
+rules, while {\bf destruct-resolution} is particularly suited for
+destruction rules.  The {\tt r}, {\tt e}, {\tt d} naming convention is
+maintained for several different kinds of resolution tactics, as well as
+the shortcuts in the subgoal module.
+
+All the tactics in this section act on a subgoal designated by a positive
+integer~$i$.  They fail (by returning the empty sequence) if~$i$ is out of
+range.
+
+\subsection{Resolution tactics}
+\index{tactics!resolution|bold}
+\begin{ttbox} 
+resolve_tac  : thm list -> int -> tactic
+eresolve_tac : thm list -> int -> tactic
+dresolve_tac : thm list -> int -> tactic
+forward_tac  : thm list -> int -> tactic 
+\end{ttbox}
+These perform resolution on a list of theorems, $thms$, representing a list
+of object-rules.  When generating next states, they take each of the rules
+in the order given.  Each rule may yield several next states, or none:
+higher-order resolution may yield multiple resolvents.
+\begin{description}
+\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
+refines the proof state using the object-rules, which should normally be
+introduction rules.  It resolves an object-rule's conclusion with
+subgoal~$i$ of the proof state.
+
+\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
+refines the proof state by elim-resolution with the object-rules, which
+should normally be elimination rules.  It resolves with a rule, solves
+its first premise by assumption, and finally {\bf deletes} that assumption
+from any new subgoals.
+
+\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
+performs destruct-resolution with the object-rules, which normally should
+be destruction rules.  This replaces an assumption by the result of
+applying one of the rules.
+
+\item[\ttindexbold{forward_tac}] 
+is like \ttindex{dresolve_tac} except that the selected assumption is not
+deleted.  It applies a rule to an assumption, adding the result as a new
+assumption.
+\end{description}
+
+\subsection{Assumption tactics}
+\index{tactics!assumption|bold}
+\begin{ttbox} 
+assume_tac    : int -> tactic
+eq_assume_tac : int -> tactic
+\end{ttbox} 
+\begin{description}
+\item[\ttindexbold{assume_tac} {\it i}] 
+attempts to solve subgoal~$i$ by assumption.
+
+\item[\ttindexbold{eq_assume_tac}] 
+is like {\tt assume_tac} but does not use unification.  It succeeds (with a
+{\bf unique} next state) if one of the assumptions is identical to the
+subgoal's conclusion.  Since it does not instantiate variables, it cannot
+make other subgoals unprovable.  It is intended to be called from proof
+strategies, not interactively.
+\end{description}
+
+\subsection{Matching tactics} \label{match_tac}
+\index{tactics!matching|bold}
+\begin{ttbox} 
+match_tac  : thm list -> int -> tactic
+ematch_tac : thm list -> int -> tactic
+dmatch_tac : thm list -> int -> tactic
+\end{ttbox}
+These are just like the resolution tactics except that they never
+instantiate unknowns in the proof state.  Flexible subgoals are not updated
+willy-nilly, but are left alone.  Matching --- strictly speaking --- means
+treating the unknowns in the proof state as constants; these tactics merely
+discard unifiers that would update the proof state.
+\begin{description}
+\item[\ttindexbold{match_tac} {\it thms} {\it i}] 
+refines the proof state using the object-rules, matching an object-rule's
+conclusion with subgoal~$i$ of the proof state.
+
+\item[\ttindexbold{ematch_tac}] 
+is like {\tt match_tac}, but performs elim-resolution.
+
+\item[\ttindexbold{dmatch_tac}] 
+is like {\tt match_tac}, but performs destruct-resolution.
+\end{description}
+
+
+\subsection{Resolution with instantiation} \label{res_inst_tac}
+\index{tactics!instantiation|bold}
+\begin{ttbox} 
+res_inst_tac  : (string*string)list -> thm -> int -> tactic
+eres_inst_tac : (string*string)list -> thm -> int -> tactic
+dres_inst_tac : (string*string)list -> thm -> int -> tactic
+forw_inst_tac : (string*string)list -> thm -> int -> tactic
+\end{ttbox}
+These tactics are designed for applying rules such as substitution and
+induction, which cause difficulties for higher-order unification.  The
+tactics accept explicit instantiations for schematic variables in the rule
+--- typically, in the rule's conclusion.  Each instantiation is a pair
+{\tt($v$,$e$)}, where $v$ can be a type variable or ordinary variable:
+\begin{itemize}
+\item If $v$ is the {\bf type variable} {\tt'a}, then
+the rule must contain a schematic type variable \verb$?'a$ of some
+sort~$s$, and $e$ should be a type of sort $s$.
+
+\item If $v$ is the {\bf variable} {\tt P}, then
+the rule must contain a schematic variable \verb$?P$ of some type~$\tau$,
+and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
+$\sigma$ are unifiable.  If the unification of $\tau$ and $\sigma$
+instantiates any schematic type variables in $\tau$, these instantiations
+are recorded for application to the rule.
+\end{itemize}
+Types are instantiated before terms.  Because type instantiations are
+inferred from term instantiations, explicit type instantiations are seldom
+necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
+\verb$[("'a","bool"),("t","True")]$ may be simplified to
+\verb$[("t","True")]$.  Type unknowns in the proof state may cause
+failure because the tactics cannot instantiate them.
+
+The instantiation tactics act on a given subgoal.  Terms in the
+instantiations are type-checked in the context of that subgoal --- in
+particular, they may refer to that subgoal's parameters.  Any unknowns in
+the terms receive subscripts and are lifted over the parameters; thus, you
+may not refer to unknowns in the subgoal.
+
+\begin{description}
+\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
+instantiates the rule {\it thm} with the instantiations {\it insts}, as
+described above, and then performs resolution on subgoal~$i$.  Resolution
+typically causes further instantiations; you need not give explicit
+instantiations for every variable in the rule.
+
+\item[\ttindexbold{eres_inst_tac}] 
+is like {\tt res_inst_tac}, but performs elim-resolution.
+
+\item[\ttindexbold{dres_inst_tac}] 
+is like {\tt res_inst_tac}, but performs destruct-resolution.
+
+\item[\ttindexbold{forw_inst_tac}] 
+is like {\tt dres_inst_tac} except that the selected assumption is not
+deleted.  It applies the instantiated rule to an assumption, adding the
+result as a new assumption.
+\end{description}
+
+
+\section{Other basic tactics}
+\subsection{Definitions and meta-level rewriting}
+\index{tactics!meta-rewriting|bold}\index{rewriting!meta-level}
+Definitions in Isabelle have the form $t\equiv u$, where typically $t$ is a
+constant or a constant applied to a list of variables, for example $\it
+sqr(n)\equiv n\times n$.  (Conditional definitions, $\phi\Imp t\equiv u$,
+are not supported.)  {\bf Unfolding} the definition $t\equiv u$ means using
+it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
+Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
+no rewrites are applicable to any subterm.
+
+There are rules for unfolding and folding definitions; Isabelle does not do
+this automatically.  The corresponding tactics rewrite the proof state,
+yielding a unique result.  See also the {\tt goalw} command, which is the
+easiest way of handling definitions.
+\begin{ttbox} 
+rewrite_goals_tac : thm list -> tactic
+rewrite_tac       : thm list -> tactic
+fold_goals_tac    : thm list -> tactic
+fold_tac          : thm list -> tactic
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
+unfolds the {\it defs} throughout the subgoals of the proof state, while
+leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
+particular subgoal.
+
+\item[\ttindexbold{rewrite_tac} {\it defs}]  
+unfolds the {\it defs} throughout the proof state, including the main goal
+--- not normally desirable!
+
+\item[\ttindexbold{fold_goals_tac} {\it defs}]  
+folds the {\it defs} throughout the subgoals of the proof state, while
+leaving the main goal unchanged.
+
+\item[\ttindexbold{fold_tac} {\it defs}]  
+folds the {\it defs} throughout the proof state.
+\end{description}
+
+
+\subsection{Tactic shortcuts}
+\index{shortcuts!for tactics|bold}
+\index{tactics!resolution}\index{tactics!assumption}
+\index{tactics!meta-rewriting}
+\begin{ttbox} 
+rtac     : thm -> int ->tactic
+etac     : thm -> int ->tactic
+dtac     : thm -> int ->tactic
+atac     : int ->tactic
+ares_tac : thm list -> int -> tactic
+rewtac   : thm -> tactic
+\end{ttbox}
+These abbreviate common uses of tactics.
+\begin{description}
+\item[\ttindexbold{rtac} {\it thm} {\it i}] 
+abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
+
+\item[\ttindexbold{etac} {\it thm} {\it i}] 
+abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
+
+\item[\ttindexbold{dtac} {\it thm} {\it i}] 
+abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
+destruct-resolution.
+
+\item[\ttindexbold{atac} {\it i}] 
+is a synonym for \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
+
+\item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
+tries proof by assumption and resolution; it abbreviates
+\begin{ttbox}
+assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
+\end{ttbox}
+
+\item[\ttindexbold{rewtac} {\it def}] 
+abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
+\end{description}
+
+
+\subsection{Inserting premises and facts}\label{cut_facts_tac}
+\index{tactics!for inserting facts|bold}
+\begin{ttbox} 
+cut_facts_tac : thm list -> int -> tactic
+subgoal_tac   :   string -> int -> tactic
+\end{ttbox}
+These tactics add assumptions --- which must be proved, sooner or later ---
+to a given subgoal.
+\begin{description}
+\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
+  adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
+  been inserted as assumptions, they become subject to {\tt eresolve_tac}
+  and {\tt rewrite_goals_tac}.  Only rules with no premises are inserted:
+  Isabelle cannot use assumptions that contain $\Imp$ or~$\Forall$.  Sometimes
+  the theorems are premises of a rule being derived, returned by~{\tt
+    goal}; instead of calling this tactic, you could state the goal with an
+  outermost meta-quantifier.
+
+\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
+adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
+{\it formula} as a new subgoal, $i+1$.
+\end{description}
+
+
+\subsection{Theorems useful with tactics}
+\index{theorems!of pure theory|bold}
+\begin{ttbox} 
+asm_rl: thm 
+cut_rl: thm 
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{asm_rl}] 
+is $\psi\Imp\psi$.  Under elim-resolution it does proof by assumption, and
+\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
+\begin{ttbox} 
+assume_tac {\it i}  ORELSE  eresolve_tac {\it thms} {\it i}
+\end{ttbox}
+
+\item[\ttindexbold{cut_rl}] 
+is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting
+assumptions; it underlies \ttindex{forward_tac}, \ttindex{cut_facts_tac}
+and \ttindex{subgoal_tac}.
+\end{description}
+
+
+\section{Obscure tactics}
+\subsection{Tidying the proof state}
+\index{parameters!removing unused|bold}
+\index{flex-flex constraints}
+\begin{ttbox} 
+prune_params_tac : tactic
+flexflex_tac     : tactic
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{prune_params_tac}]  
+  removes unused parameters from all subgoals of the proof state.  It works
+  by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
+  make the proof state more readable.  It is used with
+  \ttindex{rule_by_tactic} to simplify the resulting theorem.
+
+\item[\ttindexbold{flexflex_tac}]  
+  removes all flex-flex pairs from the proof state by applying the trivial
+  unifier.  This drastic step loses information, and should only be done as
+  the last step of a proof.
+
+  Flex-flex constraints arise from difficult cases of higher-order
+  unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
+  some variables in a rule~(\S\ref{res_inst_tac}).  Normally flex-flex
+  constraints can be ignored; they often disappear as unknowns get
+  instantiated.
+\end{description}
+
+
+\subsection{Renaming parameters in a goal} \index{parameters!renaming|bold}
+\begin{ttbox} 
+rename_tac        : string -> int -> tactic
+rename_last_tac   : string -> string list -> int -> tactic
+Logic.set_rename_prefix : string -> unit
+Logic.auto_rename       : bool ref      \hfill{\bf initially false}
+\end{ttbox}
+When creating a parameter, Isabelle chooses its name by matching variable
+names via the object-rule.  Given the rule $(\forall I)$ formalized as
+$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
+the $\Forall$-bound variable in the premise has the same name as the
+$\forall$-bound variable in the conclusion.  
+
+Sometimes there is insufficient information and Isabelle chooses an
+arbitrary name.  The renaming tactics let you override Isabelle's choice.
+Because renaming parameters has no logical effect on the proof state, the
+{\tt by} command prints the needless message {\tt Warning:\ same as previous
+level}.
+
+Alternatively, you can suppress the naming mechanism described above and
+have Isabelle generate uniform names for parameters.  These names have the
+form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
+prefix.  They are ugly but predictable.
+
+\begin{description}
+\item[\ttindexbold{rename_tac} {\it str} {\it i}] 
+interprets the string {\it str} as a series of blank-separated variable
+names, and uses them to rename the parameters of subgoal~$i$.  The names
+must be distinct.  If there are fewer names than parameters, then the
+tactic renames the innermost parameters and may modify the remaining ones
+to ensure that all the parameters are distinct.
+
+\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}] 
+generates a list of names by attaching each of the {\it suffixes\/} to the 
+{\it prefix}.  It is intended for coding structural induction tactics,
+where several of the new parameters should have related names.
+
+\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};] 
+sets the prefix for uniform renaming to~{\it prefix}.  The default prefix
+is {\tt"k"}.
+
+\item[\ttindexbold{Logic.auto_rename} \tt:= true;] 
+makes Isabelle generate uniform names for parameters. 
+\end{description}
+
+
+\subsection{Composition: resolution without lifting}
+\index{tactics!for composition|bold}
+\begin{ttbox}
+compose_tac: (bool * thm * int) -> int -> tactic
+\end{ttbox}
+{\bf Composing} two rules means to resolve them without prior lifting or
+renaming of unknowns.  This low-level operation, which underlies the
+resolution tactics, may occasionally be useful for special effects.
+A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
+rule, then passes the result to {\tt compose_tac}.
+\begin{description}
+\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
+refines subgoal~$i$ using $rule$, without lifting.  The $rule$ is taken to
+have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
+{\bf not} be atomic; thus $m$ determines the number of new subgoals.  If
+$flag$ is {\tt true} then it performs elim-resolution --- it solves the
+first premise of~$rule$ by assumption and deletes that assumption.
+\end{description}
+
+
+\section{Managing lots of rules}
+These operations are not intended for interactive use.  They are concerned
+with the processing of large numbers of rules in automatic proof
+strategies.  Higher-order resolution involving a long list of rules is
+slow.  Filtering techniques can shorten the list of rules given to
+resolution, and can also detect whether a given subgoal is too flexible,
+with too many rules applicable.
+
+\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
+\index{tactics!resolution}
+\begin{ttbox} 
+biresolve_tac   : (bool*thm)list -> int -> tactic
+bimatch_tac     : (bool*thm)list -> int -> tactic
+subgoals_of_brl : bool*thm -> int
+lessb           : (bool*thm) * (bool*thm) -> bool
+\end{ttbox}
+{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
+pair, it applies resolution if the flag is~{\tt false} and
+elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
+mixture of introduction and elimination rules.
+
+\begin{description}
+\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
+refines the proof state by resolution or elim-resolution on each rule, as
+indicated by its flag.  It affects subgoal~$i$ of the proof state.
+
+\item[\ttindexbold{bimatch_tac}] 
+is like {\tt biresolve_tac}, but performs matching: unknowns in the
+proof state are never updated (see~\S\ref{match_tac}).
+
+\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
+returns the number of new subgoals that bi-resolution would yield for the
+pair (if applied to a suitable subgoal).  This is $n$ if the flag is
+{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
+of premises of the rule.  Elim-resolution yields one fewer subgoal than
+ordinary resolution because it solves the major premise by assumption.
+
+\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
+returns the result of 
+\begin{ttbox}
+subgoals_of_brl {\it brl1} < subgoals_of_brl {\it brl2}
+\end{ttbox}
+Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
+(flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
+those that yield the fewest subgoals should be tried first.
+\end{description}
+
+
+\subsection{Discrimination nets for fast resolution}
+\index{discrimination nets|bold}
+\index{tactics!resolution}
+\begin{ttbox} 
+net_resolve_tac  : thm list -> int -> tactic
+net_match_tac    : thm list -> int -> tactic
+net_biresolve_tac: (bool*thm) list -> int -> tactic
+net_bimatch_tac  : (bool*thm) list -> int -> tactic
+filt_resolve_tac : thm list -> int -> int -> tactic
+could_unify      : term*term->bool
+filter_thms      : (term*term->bool) -> int*term*thm list -> thm list
+\end{ttbox}
+The module \ttindex{Net} implements a discrimination net data structure for
+fast selection of rules \cite[Chapter 14]{charniak80}.  A term is
+classified by the symbol list obtained by flattening it in preorder.
+The flattening takes account of function applications, constants, and free
+and bound variables; it identifies all unknowns and also regards
+$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
+anything.  
+
+A discrimination net serves as a polymorphic dictionary indexed by terms.
+The module provides various functions for inserting and removing items from
+nets.  It provides functions for returning all items whose term could match
+or unify with a target term.  The matching and unification tests are
+overly lax (due to the identifications mentioned above) but they serve as
+useful filters.
+
+A net can store introduction rules indexed by their conclusion, and
+elimination rules indexed by their major premise.  Isabelle provides
+several functions for ``compiling'' long lists of rules into fast
+resolution tactics.  When supplied with a list of theorems, these functions
+build a discrimination net; the net is used when the tactic is applied to a
+goal.  To avoid repreatedly constructing the nets, use currying: bind the
+resulting tactics to \ML{} identifiers.
+
+\begin{description}
+\item[\ttindexbold{net_resolve_tac} {\it thms}] 
+builds a discrimination net to obtain the effect of a similar call to {\tt
+resolve_tac}.
+
+\item[\ttindexbold{net_match_tac} {\it thms}] 
+builds a discrimination net to obtain the effect of a similar call to {\tt
+match_tac}.
+
+\item[\ttindexbold{net_biresolve_tac} {\it brls}] 
+builds a discrimination net to obtain the effect of a similar call to {\tt
+biresolve_tac}.
+
+\item[\ttindexbold{net_bimatch_tac} {\it brls}] 
+builds a discrimination net to obtain the effect of a similar call to {\tt
+bimatch_tac}.
+
+\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 
+uses discrimination nets to extract the {\it thms} that are applicable to
+subgoal~$i$.  If more than {\it maxr\/} theorems are applicable then the
+tactic fails.  Otherwise it calls {\tt resolve_tac}.  
+
+This tactic helps avoid runaway instantiation of unknowns, for example in
+type inference.
+
+\item[\ttindexbold{could_unify} ({\it t},{\it u})] 
+returns {\tt false} if~$t$ and~$u$ are ``obviously'' non-unifiable, and
+otherwise returns~{\tt true}.  It assumes all variables are distinct,
+reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
+
+\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 
+returns the list of potentially resolvable rules (in {\it thms\/}) for the
+subgoal {\it prem}, using the predicate {\it could\/} to compare the
+conclusion of the subgoal with the conclusion of each rule.  The resulting list
+is no longer than {\it limit}.
+\end{description}
+
+
+\section{Programming tools for proof strategies}
+Do not consider using the primitives discussed in this section unless you
+really need to code tactics from scratch,
+
+\subsection{Operations on type {\tt tactic}}
+\index{tactics!primitives for coding|bold}
+A tactic maps theorems to theorem sequences (lazy lists).  The type
+constructor for sequences is called \ttindex{Sequence.seq}.  To simplify the
+types of tactics and tacticals, Isabelle defines a type of tactics:
+\begin{ttbox} 
+datatype tactic = Tactic of thm -> thm Sequence.seq
+\end{ttbox} 
+{\tt Tactic} and {\tt tapply} convert between tactics and functions.  The
+other operations provide means for coding tactics in a clean style.
+\begin{ttbox} 
+tapply    : tactic * thm -> thm Sequence.seq
+Tactic    :     (thm -> thm Sequence.seq) -> tactic
+PRIMITIVE :                  (thm -> thm) -> tactic  
+STATE     :               (thm -> tactic) -> tactic
+SUBGOAL   : ((term*int) -> tactic) -> int -> tactic
+\end{ttbox} 
+\begin{description}
+\item[\ttindexbold{tapply} {\it tac} {\it thm}]  
+returns the result of applying the tactic, as a function, to {\it thm}.
+
+\item[\ttindexbold{Tactic} {\it f}]  
+packages {\it f} as a tactic.
+
+\item[\ttindexbold{PRIMITIVE} $f$] 
+applies $f$ to the proof state and returns the result as a
+one-element sequence.  This packages the meta-rule~$f$ as a tactic.
+
+\item[\ttindexbold{STATE} $f$] 
+applies $f$ to the proof state and then applies the resulting tactic to the
+same state.  It supports the following style, where the tactic body is
+expressed at a high level, but may peek at the proof state:
+\begin{ttbox} 
+STATE (fn state => {\it some tactic})
+\end{ttbox} 
+
+\item[\ttindexbold{SUBGOAL} $f$ $i$] 
+extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
+tactic by calling~$f(t,i)$.  It applies the resulting tactic to the same
+state.  The tactic body is expressed at a high level, but may peek at a
+particular subgoal:
+\begin{ttbox} 
+SUBGOAL (fn (t,i) => {\it some tactic})
+\end{ttbox} 
+\end{description}
+
+
+\subsection{Tracing}
+\index{tactics!tracing|bold}
+\index{tracing!of tactics}
+\begin{ttbox} 
+pause_tac: tactic
+print_tac: tactic
+\end{ttbox}
+These violate the functional behaviour of tactics by printing information
+when they are applied to a proof state.  Their output may be difficult to
+interpret.  Note that certain of the searching tacticals, such as {\tt
+REPEAT}, have built-in tracing options.
+\begin{description}
+\item[\ttindexbold{pause_tac}] 
+prints {\tt** Press RETURN to continue:} and then reads a line from the
+terminal.  If this line is blank then it returns the proof state unchanged;
+otherwise it fails (which may terminate a repetition).
+
+\item[\ttindexbold{print_tac}] 
+returns the proof state unchanged, with the side effect of printing it at
+the terminal.
+\end{description}
+
+
+\subsection{Sequences}
+\index{sequences (lazy lists)|bold}
+The module \ttindex{Sequence} declares a type of lazy lists.  It uses
+Isabelle's type \ttindexbold{option} to represent the possible presence
+(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
+a value:
+\begin{ttbox}
+datatype 'a option = None  |  Some of 'a;
+\end{ttbox}
+
+\subsubsection{Basic operations on sequences}
+\begin{ttbox} 
+Sequence.null   : 'a Sequence.seq
+Sequence.seqof  : (unit -> ('a * 'a Sequence.seq) option)
+                     -> 'a Sequence.seq
+Sequence.single : 'a -> 'a Sequence.seq
+Sequence.pull   : 'a Sequence.seq -> ('a * 'a Sequence.seq) option
+\end{ttbox}
+\begin{description}
+\item[{\tt Sequence.null}] 
+is the empty sequence.
+
+\item[\tt Sequence.seqof (fn()=> Some($x$,$s$))] 
+constructs the sequence with head~$x$ and tail~$s$, neither of which is
+evaluated.
+
+\item[{\tt Sequence.single} $x$] 
+constructs the sequence containing the single element~$x$.
+
+\item[{\tt Sequence.pull} $s$] 
+returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
+sequence has head~$x$ and tail~$s'$.  Warning: calling \hbox{Sequence.pull
+$s$} again will {\bf recompute} the value of~$x$; it is not stored!
+\end{description}
+
+
+\subsubsection{Converting between sequences and lists}
+\begin{ttbox} 
+Sequence.chop: int * 'a Sequence.seq -> 'a list * 'a Sequence.seq
+Sequence.list_of_s : 'a Sequence.seq -> 'a list
+Sequence.s_of_list : 'a list -> 'a Sequence.seq
+\end{ttbox}
+\begin{description}
+\item[{\tt Sequence.chop} ($n$, $s$)] 
+returns the first~$n$ elements of~$s$ as a list, paired with the remaining
+elements of~$s$.  If $s$ has fewer than~$n$ elements, then so will the
+list.
+
+\item[{\tt Sequence.list_of_s} $s$] 
+returns the elements of~$s$, which must be finite, as a list.
+
+\item[{\tt Sequence.s_of_list} $l$] 
+creates a sequence containing the elements of~$l$.
+\end{description}
+
+
+\subsubsection{Combining sequences}
+\begin{ttbox} 
+Sequence.append: 'a Sequence.seq * 'a Sequence.seq -> 'a Sequence.seq
+Sequence.interleave : 'a Sequence.seq * 'a Sequence.seq
+                                                   -> 'a Sequence.seq
+Sequence.flats   : 'a Sequence.seq Sequence.seq -> 'a Sequence.seq
+Sequence.maps    : ('a -> 'b) -> 'a Sequence.seq -> 'b Sequence.seq
+Sequence.filters : ('a -> bool) -> 'a Sequence.seq -> 'a Sequence.seq
+\end{ttbox} 
+\begin{description}
+\item[{\tt Sequence.append} ($s@1$, $s@2$)] 
+concatenates $s@1$ to $s@2$.
+
+\item[{\tt Sequence.interleave} ($s@1$, $s@2$)] 
+joins $s@1$ with $s@2$ by interleaving their elements.  The result contains
+all the elements of the sequences, even if both are infinite.
+
+\item[{\tt Sequence.flats} $ss$] 
+concatenates a sequence of sequences.
+
+\item[{\tt Sequence.maps} $f$ $s$] 
+applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
+$f(x@1),f(x@2),\ldots$.
+
+\item[{\tt Sequence.filters} $p$ $s$] 
+returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$
+is {\tt true}.
+\end{description}
+
+\index{tactics|)}