--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/thm.tex Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,640 @@
+%% $Id$
+\chapter{Theorems and Forward Proof}
+\index{theorems|(}
+Theorems, which represent the axioms, theorems and rules of object-logics,
+have type {\tt thm}\indexbold{*thm}. This chapter begins by describing
+operations that print theorems and that join them in forward proof. Most
+theorem operations are intended for advanced applications, such as
+programming new proof procedures. Many of these operations refer to
+signatures, certified terms and certified types, which have the \ML{} types
+{\tt Sign.sg}, {\tt Sign.cterm} and {\tt Sign.ctyp} and are discussed in
+Chapter~\ref{theories}. Beginning users should ignore such complexities
+--- and skip all but the first section of this chapter.
+
+The theorem operations do not print error messages. Instead, they raise
+exception~\ttindex{THM}\@. Use \ttindex{print_exn} to display
+exceptions nicely:
+\begin{ttbox}
+allI RS mp handle e => print_exn e;
+{\out Exception THM raised:}
+{\out RSN: no unifiers -- premise 1}
+{\out (!!x. ?P(x)) ==> ALL x. ?P(x)}
+{\out [| ?P --> ?Q; ?P |] ==> ?Q}
+{\out}
+{\out uncaught exception THM}
+\end{ttbox}
+
+
+\section{Basic operations on theorems}
+\subsection{Pretty-printing a theorem}
+\index{theorems!printing|bold}\index{printing!theorems|bold}
+\subsubsection{Top-level commands}
+\begin{ttbox}
+prth: thm -> thm
+prths: thm list -> thm list
+prthq: thm Sequence.seq -> thm Sequence.seq
+\end{ttbox}
+These are for interactive use. They are identity functions that display,
+then return, their argument. The \ML{} identifier {\tt it} will refer to
+the value just displayed.
+\begin{description}
+\item[\ttindexbold{prth} {\it thm}]
+prints {\it thm\/} at the terminal.
+
+\item[\ttindexbold{prths} {\it thms}]
+prints {\it thms}, a list of theorems.
+
+\item[\ttindexbold{prthq} {\it thmq}]
+prints {\it thmq}, a sequence of theorems. It is useful for inspecting
+the output of a tactic.
+\end{description}
+
+\subsubsection{Operations for programming}
+\begin{ttbox}
+print_thm : thm -> unit
+print_goals : int -> thm -> unit
+string_of_thm : thm -> string
+\end{ttbox}
+Functions with result type {\tt unit} are convenient for imperative
+programming.
+\begin{description}
+\item[\ttindexbold{print_thm} {\it thm}]
+prints {\it thm\/} at the terminal.
+
+\item[\ttindexbold{print_goals} {\it limit\/} {\it thm}]
+prints {\it thm\/} in goal style, with the premises as subgoals. It prints
+at most {\it limit\/} subgoals. The subgoal module calls {\tt print_goals}
+to display proof states.
+
+\item[\ttindexbold{string_of_thm} {\it thm}]
+converts {\it thm\/} to a string.
+\end{description}
+
+
+\subsection{Forwards proof: joining rules by resolution}
+\index{theorems!joining by resolution|bold}
+\index{meta-rules!resolution|bold}
+\begin{ttbox}
+RSN : thm * (int * thm) -> thm \hfill{\bf infix}
+RS : thm * thm -> thm \hfill{\bf infix}
+MRS : thm list * thm -> thm \hfill{\bf infix}
+RLN : thm list * (int * thm list) -> thm list \hfill{\bf infix}
+RL : thm list * thm list -> thm list \hfill{\bf infix}
+MRL: thm list list * thm list -> thm list \hfill{\bf infix}
+\end{ttbox}
+Putting rules together is a simple way of deriving new rules. These
+functions are especially useful with destruction rules.
+\begin{description}
+\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN}
+resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$. It
+raises exception \ttindex{THM} unless there is precisely one resolvent.
+
+\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS}
+abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}. Thus, it resolves the
+conclusion of $thm@1$ with the first premise of~$thm@2$.
+
+\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS}
+ uses {\tt RLN} to resolve $thm@i$ against premise~$i$ of $thm$, for
+ $i=n$, \ldots,~1. This applies $thm@n$, \ldots, $thm@1$ to the first $n$
+ premises of $thm$. Because the theorems are used from right to left, it
+ does not matter if the $thm@i$ create new premises. {\tt MRS} is useful
+ for expressing proof trees.
+
+\item[\tt$thms1$ RLN $(i,thms2)$] \indexbold{*RLN}
+for every $thm@1$ in $thms1$ and $thm@2$ in $thms2$, it resolves the
+conclusion of $thm@1$ with the $i$th premise of~$thm@2$, accumulating the
+results. It is useful for combining lists of theorems.
+
+\item[\tt$thms1$ RL $thms2$] \indexbold{*RL}
+abbreviates \hbox{\tt$thms1$ RLN $(1,thms2)$}.
+
+\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL}
+is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
+It too is useful for expressing proof trees.
+\end{description}
+
+
+\subsection{Expanding definitions in theorems}
+\index{theorems!meta-level rewriting in|bold}\index{rewriting!meta-level}
+\begin{ttbox}
+rewrite_rule : thm list -> thm -> thm
+rewrite_goals_rule : thm list -> thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{rewrite_rule} {\it defs} {\it thm}]
+unfolds the {\it defs} throughout the theorem~{\it thm}.
+
+\item[\ttindexbold{rewrite_goals_rule} {\it defs} {\it thm}]
+unfolds the {\it defs} in the premises of~{\it thm}, but leaves the
+conclusion unchanged. This rule underlies \ttindex{rewrite_goals_tac}, but
+serves little purpose in forward proof.
+\end{description}
+
+
+\subsection{Instantiating a theorem} \index{theorems!instantiating|bold}
+\begin{ttbox}
+read_instantiate : (string*string)list -> thm -> thm
+read_instantiate_sg : Sign.sg -> (string*string)list -> thm -> thm
+cterm_instantiate : (Sign.cterm*Sign.cterm)list -> thm -> thm
+\end{ttbox}
+These meta-rules instantiate type and term unknowns in a theorem. They are
+occasionally useful. They can prevent difficulties with higher-order
+unification, and define specialized versions of rules.
+\begin{description}
+\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}]
+processes the instantiations {\it insts} and instantiates the rule~{\it
+thm}. The processing of instantiations is described
+in~\S\ref{res_inst_tac}, under {\tt res_inst_tac}.
+
+Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule
+and refine a particular subgoal. The tactic allows instantiation by the
+subgoal's parameters, and reads the instantiations using the signature
+associated with the proof state. The remaining two instantiation functions
+are highly specialized; most users should ignore them.
+
+\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}]
+resembles \hbox{\tt read_instantiate {\it insts} {\it thm}}, but reads the
+instantiates under signature~{\it sg}. This is necessary when you want to
+instantiate a rule from a general theory, such as first-order logic, using
+the notation of some specialized theory. Use the function {\tt
+sign_of} to get the signature of a theory.
+
+\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}]
+is similar to {\tt read_instantiate}, but the instantiations are provided
+as pairs of certified terms, not as strings to be read.
+\end{description}
+
+
+\subsection{Miscellaneous forward rules}
+\index{theorems!standardizing|bold}
+\begin{ttbox}
+standard : thm -> thm
+zero_var_indexes : thm -> thm
+make_elim : thm -> thm
+rule_by_tactic : tactic -> thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{standard} $thm$]
+puts $thm$ into the standard form of object-rules. It discharges all
+meta-hypotheses, replaces free variables by schematic variables, and
+renames schematic variables to have subscript zero.
+
+\item[\ttindexbold{zero_var_indexes} $thm$]
+makes all schematic variables have subscript zero, renaming them to avoid
+clashes.
+
+\item[\ttindexbold{make_elim} $thm$]
+\index{rules!converting destruction to elimination}
+converts $thm$, a destruction rule of the form $\List{P@1;\ldots;P@m}\Imp
+Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$. This
+is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
+
+\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}]
+ applies {\it tac\/} to the {\it thm}, freezing its variables first, then
+ yields the proof state returned by the tactic. In typical usage, the
+ {\it thm\/} represents an instance of a rule with several premises, some
+ with contradictory assumptions (because of the instantiation). The
+ tactic proves those subgoals and does whatever else it can, and returns
+ whatever is left.
+\end{description}
+
+
+\subsection{Taking a theorem apart}
+\index{theorems!taking apart|bold}
+\index{flex-flex constraints}
+\begin{ttbox}
+concl_of : thm -> term
+prems_of : thm -> term list
+nprems_of : thm -> int
+tpairs_of : thm -> (term*term)list
+stamps_of_thy : thm -> string ref list
+dest_state : thm*int -> (term*term)list * term list * term * term
+rep_thm : thm -> \{prop:term, hyps:term list,
+ maxidx:int, sign:Sign.sg\}
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{concl_of} $thm$]
+returns the conclusion of $thm$ as a term.
+
+\item[\ttindexbold{prems_of} $thm$]
+returns the premises of $thm$ as a list of terms.
+
+\item[\ttindexbold{nprems_of} $thm$]
+returns the number of premises in $thm$: {\tt length(prems_of~$thm$)}.
+
+\item[\ttindexbold{tpairs_of} $thm$]
+returns the flex-flex constraints of $thm$.
+
+\item[\ttindexbold{stamps_of_thm} $thm$]
+returns the stamps of the signature associated with~$thm$.
+
+\item[\ttindexbold{dest_state} $(thm,i)$]
+decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
+list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem
+(this will be an implication if there are more than $i$ subgoals).
+
+\item[\ttindexbold{rep_thm} $thm$]
+decomposes $thm$ as a record containing the statement of~$thm$, its list of
+meta-hypotheses, the maximum subscript of its unknowns, and its signature.
+\end{description}
+
+
+\subsection{Tracing flags for unification}
+\index{tracing!of unification}
+\begin{ttbox}
+Unify.trace_simp : bool ref \hfill{\bf initially false}
+Unify.trace_types : bool ref \hfill{\bf initially false}
+Unify.trace_bound : int ref \hfill{\bf initially 10}
+Unify.search_bound : int ref \hfill{\bf initially 20}
+\end{ttbox}
+Tracing the search may be useful when higher-order unification behaves
+unexpectedly. Letting {\tt res_inst_tac} circumvent the problem is easier,
+though.
+\begin{description}
+\item[\ttindexbold{Unify.trace_simp} \tt:= true;]
+causes tracing of the simplification phase.
+
+\item[\ttindexbold{Unify.trace_types} \tt:= true;]
+generates warnings of incompleteness, when unification is not considering
+all possible instantiations of type unknowns.
+
+\item[\ttindexbold{Unify.trace_bound} \tt:= $n$]
+causes unification to print tracing information once it reaches depth~$n$.
+Use $n=0$ for full tracing. At the default value of~10, tracing
+information is almost never printed.
+
+\item[\ttindexbold{Unify.search_bound} \tt:= $n$]
+causes unification to limit its search to depth~$n$. Because of this
+bound, higher-order unification cannot return an infinite sequence, though
+it can return a very long one. The search rarely approaches the default
+value of~20. If the search is cut off, unification prints {\tt
+***Unification bound exceeded}.
+\end{description}
+
+
+\section{Primitive meta-level inference rules}
+\index{meta-rules|(}
+These implement the meta-logic in {\sc lcf} style, as functions from theorems
+to theorems. They are, rarely, useful for deriving results in the pure
+theory. Mainly, they are included for completeness, and most users should
+not bother with them. The meta-rules raise exception \ttindex{THM} to signal
+malformed premises, incompatible signatures and similar errors.
+
+The meta-logic uses natural deduction. Each theorem may depend on
+meta-hypotheses, or assumptions. Certain rules, such as $({\Imp}I)$,
+discharge assumptions; in most other rules, the conclusion depends on all
+of the assumptions of the premises. Formally, the system works with
+assertions of the form
+\[ \phi \quad [\phi@1,\ldots,\phi@n], \]
+where $\phi@1$,~\ldots,~$\phi@n$ are the hypotheses. Do not confuse
+meta-level assumptions with the object-level assumptions in a subgoal,
+which are represented in the meta-logic using~$\Imp$.
+
+Each theorem has a signature. Certified terms have a signature. When a
+rule takes several premises and certified terms, it merges the signatures
+to make a signature for the conclusion. This fails if the signatures are
+incompatible.
+
+The {\em implication\/} rules are $({\Imp}I)$
+and $({\Imp}E)$:
+\[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}} \qquad
+ \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi} \]
+
+Equality of truth values means logical equivalence:
+\[ \infer[({\equiv}I)]{\phi\equiv\psi}{\infer*{\psi}{[\phi]} &
+ \infer*{\phi}{[\psi]}}
+ \qquad
+ \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi} \]
+
+The {\em equality\/} rules are reflexivity, symmetry, and transitivity:
+\[ {a\equiv a}\,(refl) \qquad
+ \infer[(sym)]{b\equiv a}{a\equiv b} \qquad
+ \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c} \]
+
+The $\lambda$-conversions are $\alpha$-conversion, $\beta$-conversion, and
+extensionality:\footnote{$\alpha$-conversion holds if $y$ is not free
+in~$a$; $(ext)$ holds if $x$ is not free in the assumptions, $f$, or~$g$.}
+\[ {(\lambda x.a) \equiv (\lambda y.a[y/x])} \qquad
+ {((\lambda x.a)(b)) \equiv a[b/x]} \qquad
+ \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)} \]
+
+The {\it abstraction\/} and {\it combination\/} rules permit the conversion
+of subterms:\footnote{Abstraction holds if $x$ is not free in the
+assumptions.}
+\[ \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b} \qquad
+ \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b} \]
+
+The {\em universal quantification\/} rules are $(\Forall I)$ and $(\Forall
+E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
+\[ \infer[(\Forall I)]{\Forall x.\phi}{\phi} \qquad
+ \infer[(\Forall I)]{\phi[b/x]}{\Forall x.\phi} \]
+
+
+\subsection{Propositional rules}
+\index{meta-rules!assumption|bold}
+\subsubsection{Assumption}
+\begin{ttbox}
+assume: Sign.cterm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{assume} $ct$]
+makes the theorem \(\phi \quad[\phi]\), where $\phi$ is the value of~$ct$.
+The rule checks that $ct$ has type $prop$ and contains no unknowns, which
+are not allowed in hypotheses.
+\end{description}
+
+\subsubsection{Implication}
+\index{meta-rules!implication|bold}
+\begin{ttbox}
+implies_intr : Sign.cterm -> thm -> thm
+implies_intr_list : Sign.cterm list -> thm -> thm
+implies_intr_hyps : thm -> thm
+implies_elim : thm -> thm -> thm
+implies_elim_list : thm -> thm list -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{implies_intr} $ct$ $thm$]
+is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$. It
+maps the premise $\psi\quad[\phi]$ to the conclusion $\phi\Imp\psi$. The
+rule checks that $ct$ has type $prop$.
+
+\item[\ttindexbold{implies_intr_list} $cts$ $thm$]
+applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
+
+\item[\ttindexbold{implies_intr_hyps} $thm$]
+applies $({\Imp}I)$ to discharge all the hypotheses of~$thm$. It maps the
+premise $\phi \quad [\phi@1,\ldots,\phi@n]$ to the conclusion
+$\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
+
+\item[\ttindexbold{implies_elim} $thm@1$ $thm@2$]
+applies $({\Imp}E)$ to $thm@1$ and~$thm@2$. It maps the premises $\phi\Imp
+\psi$ and $\phi$ to the conclusion~$\psi$.
+
+\item[\ttindexbold{implies_elim_list} $thm$ $thms$]
+applies $({\Imp}E)$ repeatedly to $thm$, using each element of~$thms$ in
+turn. It maps the premises $[\phi@1,\ldots,\phi@n]\Imp\psi$ and
+$\phi@1$,\ldots,$\phi@n$ to the conclusion~$\psi$.
+\end{description}
+
+\subsubsection{Logical equivalence (equality)}
+\index{meta-rules!logical equivalence|bold}
+\begin{ttbox}
+equal_intr : thm -> thm -> thm equal_elim : thm -> thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$]
+applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises
+$\psi\quad[\phi]$ and $\phi\quad[\psi]$ to the conclusion~$\phi\equiv\psi$.
+
+\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$]
+applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises
+$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
+\end{description}
+
+
+\subsection{Equality rules}
+\index{meta-rules!equality|bold}
+\begin{ttbox}
+reflexive : Sign.cterm -> thm
+symmetric : thm -> thm
+transitive : thm -> thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{reflexive} $ct$]
+makes the theorem \(ct=ct\).
+
+\item[\ttindexbold{symmetric} $thm$]
+maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
+
+\item[\ttindexbold{transitive} $thm@1$ $thm@2$]
+maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
+\end{description}
+
+
+\subsection{The $\lambda$-conversion rules}
+\index{meta-rules!$\lambda$-conversion|bold}
+\begin{ttbox}
+beta_conversion : Sign.cterm -> thm
+extensional : thm -> thm
+abstract_rule : string -> Sign.cterm -> thm -> thm
+combination : thm -> thm -> thm
+\end{ttbox}
+There is no rule for $\alpha$-conversion because Isabelle's internal
+representation ignores bound variable names, except when communicating with
+the user.
+\begin{description}
+\item[\ttindexbold{beta_conversion} $ct$]
+makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
+term $(\lambda x.a)(b)$.
+
+\item[\ttindexbold{extensional} $thm$]
+maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
+Parameter~$x$ is taken from the premise. It may be an unknown or a free
+variable (provided it does not occur in the hypotheses); it must not occur
+in $f$ or~$g$.
+
+\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$]
+maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
+(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
+Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
+variable (provided it does not occur in the hypotheses). In the
+conclusion, the bound variable is named~$v$.
+
+\item[\ttindexbold{combination} $thm@1$ $thm@2$]
+maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
+g(b)$.
+\end{description}
+
+
+\subsection{Universal quantifier rules}
+\index{meta-rules!quantifier|bold}
+\subsubsection{Forall introduction}
+\begin{ttbox}
+forall_intr : Sign.cterm -> thm -> thm
+forall_intr_list : Sign.cterm list -> thm -> thm
+forall_intr_frees : thm -> thm
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{forall_intr} $x$ $thm$]
+applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
+The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
+Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
+variable (provided it does not occur in the hypotheses).
+
+\item[\ttindexbold{forall_intr_list} $xs$ $thm$]
+applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
+
+\item[\ttindexbold{forall_intr_frees} $thm$]
+applies $({\Forall}I)$ repeatedly, generalizing over all the free variables
+of the premise.
+\end{description}
+
+
+\subsubsection{Forall elimination}
+\begin{ttbox}
+forall_elim : Sign.cterm -> thm -> thm
+forall_elim_list : Sign.cterm list -> thm -> thm
+forall_elim_var : int -> thm -> thm
+forall_elim_vars : int -> thm -> thm
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{forall_elim} $ct$ $thm$]
+applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
+$\phi[ct/x]$. The rule checks that $ct$ and $x$ have the same type.
+
+\item[\ttindexbold{forall_elim_list} $cts$ $thm$]
+applies $({\Forall}E)$ repeatedly, on every element of the list~$cts$.
+
+\item[\ttindexbold{forall_elim_var} $k$ $thm$]
+applies $({\Forall}E)$, mapping the premise $\Forall x.\phi$ to the conclusion
+$\phi[\Var{x@k}/x]$. Thus, it replaces the outermost $\Forall$-bound
+variable by an unknown having subscript~$k$.
+
+\item[\ttindexbold{forall_elim_vars} $ks$ $thm$]
+applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$.
+\end{description}
+
+\subsubsection{Instantiation of unknowns}
+\index{meta-rules!instantiation|bold}
+\begin{ttbox}
+instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list
+ -> thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{instantiate} $tyinsts$ $insts$ $thm$]
+performs simultaneous substitution of types for type unknowns (the
+$tyinsts$) and terms for term unknowns (the $insts$). Instantiations are
+given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
+same type as $v$) or a type (of the same sort as~$v$). All the unknowns
+must be distinct. The rule normalizes its conclusion.
+\end{description}
+
+
+\subsection{Freezing/thawing type variables}
+\index{meta-rules!for type variables|bold}
+\begin{ttbox}
+freezeT: thm -> thm
+varifyT: thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{freezeT} $thm$]
+converts all the type unknowns in $thm$ to free type variables.
+
+\item[\ttindexbold{varifyT} $thm$]
+converts all the free type variables in $thm$ to type unknowns.
+\end{description}
+
+
+\section{Derived rules for goal-directed proof}
+Most of these rules have the sole purpose of implementing particular
+tactics. There are few occasions for applying them directly to a theorem.
+
+\subsection{Proof by assumption}
+\index{meta-rules!assumption|bold}
+\begin{ttbox}
+assumption : int -> thm -> thm Sequence.seq
+eq_assumption : int -> thm -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{assumption} {\it i} $thm$]
+attempts to solve premise~$i$ of~$thm$ by assumption.
+
+\item[\ttindexbold{eq_assumption}]
+is like {\tt assumption} but does not use unification.
+\end{description}
+
+
+\subsection{Resolution}
+\index{meta-rules!resolution|bold}
+\begin{ttbox}
+biresolution : bool -> (bool*thm)list -> int -> thm
+ -> thm Sequence.seq
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$]
+performs bi-resolution on subgoal~$i$ of~$state$, using the 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}. If $match$
+is~{\tt true}, the $state$ is not instantiated.
+\end{description}
+
+
+\subsection{Composition: resolution without lifting}
+\index{meta-rules!for composition|bold}
+\begin{ttbox}
+compose : thm * int * thm -> thm list
+COMP : thm * thm -> thm
+bicompose : bool -> bool * thm * int -> int -> thm
+ -> thm Sequence.seq
+\end{ttbox}
+In forward proof, a typical use of composition is to regard an assertion of
+the form $\phi\Imp\psi$ as atomic. Schematic variables are not renamed, so
+beware of clashes!
+\begin{description}
+\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)]
+uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
+of~$thm@2$. Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
+\phi@n} \Imp \phi$. For each $s$ that unifies~$\psi$ and $\phi@i$, the
+result list contains the theorem
+\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
+\]
+
+\item[\tt $thm@1$ COMP $thm@2$]
+calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
+unique; otherwise, it raises exception~\ttindex{THM}\@. It is
+analogous to {\tt RS}\@.
+
+For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
+that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg A)$, which is the
+principle of contrapositives. Then the result would be the
+derived rule $\neg(b=a)\Imp\neg(a=b)$.
+
+\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
+refines subgoal~$i$ of $state$ 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. If $match$ is~{\tt true}, the $state$ is not instantiated.
+\end{description}
+
+
+\subsection{Other meta-rules}
+\begin{ttbox}
+trivial : Sign.cterm -> thm
+lift_rule : (thm * int) -> thm -> thm
+rename_params_rule : string list * int -> thm -> thm
+rewrite_cterm : thm list -> Sign.cterm -> thm
+flexflex_rule : thm -> thm Sequence.seq
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{trivial} $ct$]
+makes the theorem \(\phi\Imp\phi\), where $\phi$ is the value of~$ct$.
+This is the initial state for a goal-directed proof of~$\phi$. The rule
+checks that $ct$ has type~$prop$.
+
+\item[\ttindexbold{lift_rule} ($state$, $i$) $rule$] \index{lifting}
+prepares $rule$ for resolution by lifting it over the parameters and
+assumptions of subgoal~$i$ of~$state$.
+
+\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$]
+uses the $names$ to rename the parameters of premise~$i$ of $thm$. The
+names must be distinct. If there are fewer names than parameters, then the
+rule renames the innermost parameters and may modify the remaining ones to
+ensure that all the parameters are distinct.
+\index{parameters!renaming}
+
+\item[\ttindexbold{rewrite_cterm} $defs$ $ct$]
+transforms $ct$ to $ct'$ by repeatedly applying $defs$ as rewrite rules; it
+returns the conclusion~$ct\equiv ct'$. This underlies the meta-rewriting
+tactics and rules.
+\index{terms!meta-level rewriting in|bold}\index{rewriting!meta-level}
+
+\item[\ttindexbold{flexflex_rule} $thm$] \index{flex-flex constraints}
+\index{meta-rules!for flex-flex constraints|bold}
+removes all flex-flex pairs from $thm$ using the trivial unifier.
+\end{description}
+\index{theorems|)}
+\index{meta-rules|)}