doc-src/IsarImplementation/Thy/document/Tactic.tex
 author wenzelm Sun, 29 Jan 2012 22:12:25 +0100 changeset 46278 408e3acfdbb9 parent 46277 aea65ff733b4 permissions -rw-r--r--

%
\begin{isabellebody}%
\def\isabellecontext{Tactic}%
%
%
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Tactic\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
%
%
\isamarkupchapter{Tactical reasoning%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Tactical reasoning works by refining an initial claim in a
backwards fashion, until a solved form is reached.  A \isa{goal}
consists of several subgoals that need to be solved in order to
achieve the main statement; zero subgoals means that the proof may
be finished.  A \isa{tactic} is a refinement operation that maps
a goal to a lazy sequence of potential successors.  A \isa{tactical} is a combinator for composing tactics.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Goals \label{sec:tactical-goals}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle/Pure represents a goal as a theorem stating that the
subgoals imply the main goal: \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}.  The outermost goal structure is that of a Horn Clause: i.e.\
an iterated implication without any quantifiers\footnote{Recall that
outermost \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} is always represented via schematic
variables in the body: \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}.  These variables may get
instantiated during the course of reasoning.}.  For \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}
a goal is called solved''.

The structure of each subgoal \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} is that of a
general Hereditary Harrop Formula \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{2E}{\isachardot}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}.  Here \isa{x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub k} are goal parameters, i.e.\
arbitrary-but-fixed entities of certain types, and \isa{H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m} are goal hypotheses, i.e.\ facts that may
be assumed locally.  Together, this forms the goal context of the
conclusion \isa{B} to be established.  The goal hypotheses may be
again arbitrary Hereditary Harrop Formulas, although the level of
nesting rarely exceeds 1--2 in practice.

The main conclusion \isa{C} is internally marked as a protected
proposition, which is represented explicitly by the notation \isa{{\isaliteral{23}{\isacharhash}}C} here.  This ensures that the decomposition into subgoals and
main conclusion is well-defined for arbitrarily structured claims.

\medskip Basic goal management is performed via the following
Isabelle/Pure rules:

$\infer[\isa{{\isaliteral{28}{\isacharparenleft}}init{\isaliteral{29}{\isacharparenright}}}]{\isa{C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}}{} \qquad \infer[\isa{{\isaliteral{28}{\isacharparenleft}}finish{\isaliteral{29}{\isacharparenright}}}]{\isa{C}}{\isa{{\isaliteral{23}{\isacharhash}}C}}$

\medskip The following low-level variants admit general reasoning
with protected propositions:

$\infer[\isa{{\isaliteral{28}{\isacharparenleft}}protect{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{23}{\isacharhash}}C}}{\isa{C}} \qquad \infer[\isa{{\isaliteral{28}{\isacharparenleft}}conclude{\isaliteral{29}{\isacharparenright}}}]{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}}$%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\
\indexdef{}{ML}{Goal.finish}\verb|Goal.finish: Proof.context -> thm -> thm| \\
\indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\
\indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
\end{mldecls}

\begin{description}

\item \verb|Goal.init|~\isa{C} initializes a tactical goal from
the well-formed proposition \isa{C}.

\item \verb|Goal.finish|~\isa{ctxt\ thm} checks whether theorem
\isa{thm} is a solved goal (no subgoals), and concludes the
result by removing the goal protection.  The context is only
required for printing error messages.

\item \verb|Goal.protect|~\isa{thm} protects the full statement
of theorem \isa{thm}.

\item \verb|Goal.conclude|~\isa{thm} removes the goal
protection, even if there are pending subgoals.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsection{Tactics\label{sec:tactics}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \isa{tactic} is a function \isa{goal\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ goal\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} that
maps a given goal state (represented as a theorem, cf.\
\secref{sec:tactical-goals}) to a lazy sequence of potential
successor states.  The underlying sequence implementation is lazy
both in head and tail, and is purely functional in \emph{not}
supporting memoing.\footnote{The lack of memoing and the strict
nature of SML requires some care when working with low-level
sequence operations, to avoid duplicate or premature evaluation of
results.  It also means that modified runtime behavior, such as
timeout, is very hard to achieve for general tactics.}

An \emph{empty result sequence} means that the tactic has failed: in
a compound tactic expression other tactics might be tried instead,
or the whole refinement step might fail outright, producing a
toplevel error message in the end.  When implementing tactics from
scratch, one should take care to observe the basic protocol of
mapping regular error conditions to an empty result; only serious
faults should emerge as exceptions.

By enumerating \emph{multiple results}, a tactic can easily express
the potential outcome of an internal search process.  There are also
combinators for building proof tools that involve search

\medskip As explained before, a goal state essentially consists of a
list of subgoals that imply the main goal (conclusion).  Tactics may
operate on all subgoals or on a particularly specified subgoal, but
must not change the main conclusion (apart from instantiating
schematic goal variables).

Tactics with explicit \emph{subgoal addressing} are of the form
\isa{int\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ tactic} and may be applied to a particular subgoal
(counting from 1).  If the subgoal number is out of range, the
tactic should fail with an empty result sequence, but must not raise
an exception!

Operating on a particular subgoal means to replace it by an interval
of zero or more subgoals in the same place; other subgoals must not
be affected, apart from instantiating schematic variables ranging
over the whole goal state.

A common pattern of composing tactics with subgoal addressing is to
try the first one, and then the second one only if the subgoal has
not been solved yet.  Special care is required here to avoid bumping
into unrelated subgoals that happen to come after the original
subgoal.  Assuming that there is only a single initial subgoal is a
very common error when implementing tactics!

Tactics with internal subgoal addressing should expose the subgoal
index as \isa{int} argument in full generality; a hardwired
subgoal 1 is not acceptable.

\medskip The main well-formedness conditions for proper tactics are
summarized as follows.

\begin{itemize}

\item General tactic failure is indicated by an empty result, only
serious faults may produce an exception.

\item The main conclusion must not be changed, apart from
instantiating schematic variables.

\item A tactic operates either uniformly on all subgoals, or
specifically on a selected subgoal (without bumping into unrelated
subgoals).

\item Range errors in subgoal addressing produce an empty result.

\end{itemize}

Some of these conditions are checked by higher-level goal
infrastructure (\secref{sec:struct-goals}); others are not checked
explicitly, and violating them merely results in ill-behaved tactics
experienced by the user (e.g.\ tactics that insist in being
applicable only to singleton goals, or prevent composition via
standard tacticals such as \verb|REPEAT|).%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{tactic}\verb|type tactic = thm -> thm Seq.seq| \\
\indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\
\indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\
\indexdef{}{ML}{print\_tac}\verb|print_tac: string -> tactic| \\[1ex]
\indexdef{}{ML}{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex]
\indexdef{}{ML}{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\
\indexdef{}{ML}{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\
\end{mldecls}

\begin{description}

\item Type \verb|tactic| represents tactics.  The
well-formedness conditions described above need to be observed.  See
also \verb|~~/src/Pure/General/seq.ML| for the underlying
implementation of lazy sequences.

\item Type \verb|int -> tactic| represents tactics with
explicit subgoal addressing, with well-formedness conditions as
described above.

\item \verb|no_tac| is a tactic that always fails, returning the
empty sequence.

\item \verb|all_tac| is a tactic that always succeeds, returning a
singleton sequence with unchanged goal state.

\item \verb|print_tac|~\isa{message} is like \verb|all_tac|, but
prints a message together with the goal state on the tracing
channel.

\item \verb|PRIMITIVE|~\isa{rule} turns a primitive inference rule
into a tactic with unique result.  Exception \verb|THM| is considered
a regular tactic failure and produces an empty result; other
exceptions are passed through.

\item \verb|SUBGOAL|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ tactic{\isaliteral{29}{\isacharparenright}}} is the
most basic form to produce a tactic with subgoal addressing.  The
given abstraction over the subgoal term and subgoal number allows to
peek at the relevant information of the full goal state.  The
subgoal range is checked as required above.

\item \verb|CSUBGOAL| is similar to \verb|SUBGOAL|, but passes the
subgoal as \verb|cterm| instead of raw \verb|term|.  This
avoids expensive re-certification in situations where the subgoal is
used directly for primitive inferences.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsubsection{Resolution and assumption tactics \label{sec:resolve-assume-tac}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\emph{Resolution} is the most basic mechanism for refining a
subgoal using a theorem as object-level rule.
\emph{Elim-resolution} is particularly suited for elimination rules:
it resolves with a rule, proves its first premise by assumption, and
finally deletes that assumption from any new subgoals.
\emph{Destruct-resolution} is like elim-resolution, but the given
destruction rules are first turned into canonical elimination
format.  \emph{Forward-resolution} is like destruct-resolution, but
without deleting the selected assumption.  The \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f}
naming convention is maintained for several different kinds of
resolution rules and tactics.

Assumption tactics close a subgoal by unifying some of its premises
against its conclusion.

\medskip All the tactics in this section operate on a subgoal
designated by a positive integer.  Other subgoals might be affected
indirectly, due to instantiation of schematic variables.

There are various sources of non-determinism, the tactic result
sequence enumerates all possibilities of the following choices (if
applicable):

\begin{enumerate}

\item selecting one of the rules given as argument to the tactic;

\item selecting a subgoal premise to eliminate, unifying it against
the first premise of the rule;

\item unifying the conclusion of the subgoal to the conclusion of
the rule.

\end{enumerate}

Recall that higher-order unification may produce multiple results
that are enumerated here.%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex]
\indexdef{}{ML}{assume\_tac}\verb|assume_tac: int -> tactic| \\
\indexdef{}{ML}{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex]
\indexdef{}{ML}{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\
\end{mldecls}

\begin{description}

\item \verb|resolve_tac|~\isa{thms\ i} refines the goal state
using the given theorems, which should normally be introduction
rules.  The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's
premises.

\item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution
with the given theorems, which are normally be elimination rules.

Note that \verb|eresolve_tac [asm_rl]| is equivalent to \verb|assume_tac|, which facilitates mixing of assumption steps with
genuine eliminations.

\item \verb|dresolve_tac|~\isa{thms\ i} performs
destruct-resolution with the given theorems, which should normally
be destruction rules.  This replaces an assumption by the result of
applying one of the rules.

\item \verb|forward_tac| is like \verb|dresolve_tac| except that the
selected assumption is not deleted.  It applies a rule to an
assumption, adding the result as a new assumption.

\item \verb|assume_tac|~\isa{i} attempts to solve subgoal \isa{i}
by assumption (modulo higher-order unification).

\item \verb|eq_assume_tac| is similar to \verb|assume_tac|, but checks
only for immediate \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-convertibility instead of using
unification.  It succeeds (with a unique next state) if one of the
assumptions is equal to the subgoal's conclusion.  Since it does not
instantiate variables, it cannot make other subgoals unprovable.

\item \verb|match_tac|, \verb|ematch_tac|, and \verb|dmatch_tac| are
similar to \verb|resolve_tac|, \verb|eresolve_tac|, and \verb|dresolve_tac|, respectively, but do not instantiate schematic
variables in the goal state.

Flexible subgoals are not updated at will, but are left alone.
Strictly speaking, matching means to treat the unknowns in the goal
state as constants; these tactics merely discard unifiers that would
update the goal state.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsubsection{Explicit instantiation within a subgoal context%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The main resolution tactics (\secref{sec:resolve-assume-tac})
use higher-order unification, which works well in many practical
situations despite its daunting theoretical properties.
Nonetheless, there are important problem classes where unguided
higher-order unification is not so useful.  This typically involves
rules like universal elimination, existential introduction, or
equational substitution.  Here the unification problem involves
fully flexible \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x} schemes, which are hard to manage
without further hints.

By providing a (small) rigid term for \isa{{\isaliteral{3F}{\isacharquery}}x} explicitly, the
remaining unification problem is to assign a (large) term to \isa{{\isaliteral{3F}{\isacharquery}}P}, according to the shape of the given subgoal.  This is
sufficiently well-behaved in most practical situations.

\medskip Isabelle provides separate versions of the standard \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f} resolution tactics that allow to provide explicit
instantiations of unknowns of the given rule, wrt.\ terms that refer
to the implicit context of the selected subgoal.

An instantiation consists of a list of pairs of the form \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}, where \isa{{\isaliteral{3F}{\isacharquery}}x} is a schematic variable occurring in
the given rule, and \isa{t} is a term from the current proof
context, augmented by the local goal parameters of the selected
subgoal; cf.\ the \isa{focus} operation described in
\secref{sec:variables}.

Entering the syntactic context of a subgoal is a brittle operation,
because its exact form is somewhat accidental, and the choice of
bound variable names depends on the presence of other local and
global names.  Explicit renaming of subgoal parameters prior to
explicit instantiation might help to achieve a bit more robustness.

Type instantiations may be given as well, via pairs like \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}.  Type instantiations are distinguished from term
instantiations by the syntactic form of the schematic variable.
Types are instantiated before terms are.  Since term instantiation
already performs simple type-inference, so explicit type
instantiations are seldom necessary.%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
\indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
\indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
\indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
\indexdef{}{ML}{subgoal\_tac}\verb|subgoal_tac: Proof.context -> string -> int -> tactic| \\
\indexdef{}{ML}{thin\_tac}\verb|thin_tac: Proof.context -> string -> int -> tactic| \\
\indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
\end{mldecls}

\begin{description}

\item \verb|res_inst_tac|~\isa{ctxt\ insts\ thm\ i} instantiates the
rule \isa{thm} with the instantiations \isa{insts}, as described
above, and then performs resolution on subgoal \isa{i}.

\item \verb|eres_inst_tac| is like \verb|res_inst_tac|, but performs
elim-resolution.

\item \verb|dres_inst_tac| is like \verb|res_inst_tac|, but performs
destruct-resolution.

\item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that
the selected assumption is not deleted.

\item \verb|subgoal_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} adds the proposition
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as local premise to subgoal \isa{i}, and poses the
same as a new subgoal \isa{i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} (in the original context).

\item \verb|thin_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} deletes the specified
premise from subgoal \isa{i}.  Note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain
schematic variables, to abbreviate the intended proposition; the
first matching subgoal premise will be deleted.  Removing useless
premises from a subgoal increases its readability and can make
search tactics run faster.

\item \verb|rename_tac|~\isa{names\ i} renames the innermost
parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers).

\end{description}

For historical reasons, the above instantiation tactics take
unparsed string arguments, which makes them hard to use in general
ML code.  The slightly more advanced \verb|Subgoal.FOCUS| combinator
of \secref{sec:struct-goals} allows to refer to internal goal
structure with explicit context management.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsubsection{Rearranging goal states%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
In rare situations there is a need to rearrange goal states:
either the overall collection of subgoals, or the local structure of
a subgoal.  Various administrative tactics allow to operate on the
concrete presentation these conceptual sets of formulae.%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{rotate\_tac}\verb|rotate_tac: int -> int -> tactic| \\
\indexdef{}{ML}{distinct\_subgoals\_tac}\verb|distinct_subgoals_tac: tactic| \\
\indexdef{}{ML}{flexflex\_tac}\verb|flexflex_tac: tactic| \\
\end{mldecls}

\begin{description}

\item \verb|rotate_tac|~\isa{n\ i} rotates the premises of subgoal
\isa{i} by \isa{n} positions: from right to left if \isa{n} is
positive, and from left to right if \isa{n} is negative.

\item \verb|distinct_subgoals_tac| removes duplicate subgoals from a
proof state.  This is potentially inefficient.

\item \verb|flexflex_tac| removes all flex-flex pairs from the proof
state by applying the trivial unifier.  This drastic step loses
information.  It is already part of the Isar infrastructure for
facts resulting from goals, and rarely needs to be invoked manually.

Flex-flex constraints arise from difficult cases of higher-order
unification.  To prevent this, use \verb|res_inst_tac| to instantiate
some variables in a rule.  Normally flex-flex constraints can be
ignored; they often disappear as unknowns get instantiated.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsection{Tacticals \label{sec:tacticals}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \emph{tactical} is a functional combinator for building up
complex tactics from simpler ones.  Common tacticals perform
sequential composition, disjunctive choice, iteration, or goal
addressing.  Various search strategies may be expressed via
tacticals.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Combining tactics%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Sequential composition and alternative choices are the most
basic ways to combine tactics, similarly to \verb|,|'' and
\verb||\verb,|,\verb||'' in Isar method notation.  This corresponds to
\verb|THEN| and \verb|ORELSE| in ML, but there are further
possibilities for fine-tuning alternation of tactics such as \verb|APPEND|.  Further details become visible in ML due to explicit
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML infix}{THEN}\verb|infix THEN: tactic * tactic -> tactic| \\
\indexdef{}{ML infix}{ORELSE}\verb|infix ORELSE: tactic * tactic -> tactic| \\
\indexdef{}{ML infix}{APPEND}\verb|infix APPEND: tactic * tactic -> tactic| \\
\indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\
\indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex]

\indexdef{}{ML infix}{THEN'}\verb|infix THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
\indexdef{}{ML infix}{ORELSE'}\verb|infix ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
\indexdef{}{ML infix}{APPEND'}\verb|infix APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
\indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\
\indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\
\end{mldecls}

\begin{description}

state, it returns all states reachable in two steps by applying
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the goal state, getting a sequence of possible next
states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and
concatenates the results to produce again one flat sequence of
states.

tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  This is a deterministic
from the result.

\verb|ORELSE| there is \emph{no commitment} to either tactic, so
\verb|APPEND| helps to avoid incompleteness during search, at
the cost of potential inefficiencies.

Note that \verb|EVERY []| is the same as \verb|all_tac|: it always
succeeds.

\item \verb|FIRST|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}.  Note that \verb|FIRST []| is the same as \verb|no_tac|: it
always fails.

\item \verb|THEN'| is the lifted version of \verb|THEN|, for

The other primed tacticals work analogously.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsubsection{Repetition tacticals%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
These tacticals provide further control over repetition of
tactics, beyond the stylized forms of \verb|?|''  and
\verb|+|'' in Isar method expressions.%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\
\indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
\indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\
\indexdef{}{ML}{REPEAT\_DETERM}\verb|REPEAT_DETERM: tactic -> tactic| \\
\indexdef{}{ML}{REPEAT\_DETERM\_N}\verb|REPEAT_DETERM_N: int -> tactic -> tactic| \\
\end{mldecls}

\begin{description}

\item \verb|TRY|~\isa{tac} applies \isa{tac} to the goal
state and returns the resulting sequence, if non-empty; otherwise it
returns the original state.  Thus, it applies \isa{tac} at most
once.

Note that for tactics with subgoal addressing, the combinator can be
applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}.  There is no need for \verb|TRY'|.

\item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the goal
state and, recursively, to each element of the resulting sequence.
The resulting sequence consists of those states that make \isa{tac} fail.  Thus, it applies \isa{tac} as many times as
possible (including zero times), and allows backtracking over each
invocation of \isa{tac}.  \verb|REPEAT| is more general than \verb|REPEAT_DETERM|, but requires more space.

\item \verb|REPEAT1|~\isa{tac} is like \verb|REPEAT|~\isa{tac}
but it always applies \isa{tac} at least once, failing if this
is impossible.

\item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
goal state and, recursively, to the head of the resulting sequence.
It returns the first state to make \isa{tac} fail.  It is

\item \verb|REPEAT_DETERM_N|~\isa{n\ tac} is like \verb|REPEAT_DETERM|~\isa{tac} but the number of repetitions is bound
by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}).

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
%
%
\isatagmlex
%
\begin{isamarkuptext}%
The basic tactics and tacticals considered above follow
some algebraic laws:

\begin{itemize}

\item \verb|all_tac| is the identity element of the tactical \verb|THEN|.

\item \verb|no_tac| is the identity element of \verb|ORELSE| and
\verb|APPEND|.  Also, it is a zero element for \verb|THEN|,
which means that \isa{tac}~\verb|THEN|~\verb|no_tac| is
equivalent to \verb|no_tac|.

\item \verb|TRY| and \verb|REPEAT| can be expressed as (recursive)
functions over more basic combinators (ignoring some internal
implementation tricks):

\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlex
{\isafoldmlex}%
%
%
%
%
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ fun\ TRY\ tac\ {\isaliteral{3D}{\isacharequal}}\ tac\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ fun\ REPEAT\ tac\ st\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}\ st{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
%
%
\begin{isamarkuptext}%
If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}.  \verb|REPEAT| uses \verb|ORELSE| and not
\verb|APPEND|, it applies \isa{tac} as many times as
possible in each outcome.

\begin{warn}
Note the explicit abstraction over the goal state in the ML
definition of \verb|REPEAT|.  Recursive tacticals must be coded in
this awkward fashion to avoid infinite recursion of eager functional
evaluation in Standard ML.  The following attempt would make \verb|REPEAT|~\isa{tac} loop:
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}BAD\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ does\ not\ terminate{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ fun\ REPEAT\ tac\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline
{\isaliteral{2A7D}{\isacharverbatimclose}}%
\endisatagML
{\isafoldML}%
%
%
%
\isamarkupsubsection{Applying tactics to subgoal ranges%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\verb|int -> tactic| can be used together with tacticals that
act like subgoal quantifiers'': guided by success of the body
tactic a certain range of subgoals is covered.  Thus the body tactic
is applied to \emph{all} subgoals, \emph{some} subgoal etc.

Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals.  Many of
these tacticals address subgoal ranges counting downwards from
\isa{n} towards \isa{{\isadigit{1}}}.  This has the fortunate effect that
newly emerging subgoals are concatenated in the result, without
interfering each other.  Nonetheless, there might be situations
where a different order is desired.%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\
\end{mldecls}

\begin{description}

\item \verb|ALLGOALS|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\ {\isadigit{1}}}.  It
applies the \isa{tac} to all the subgoals, counting downwards.

\item \verb|SOMEGOAL|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ {\isadigit{1}}}.  It
applies \isa{tac} to one subgoal, counting downwards.

\item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}.  It
applies \isa{tac} to one subgoal, counting upwards.

It applies \isa{tac} unconditionally to the first subgoal.

\item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or
more to a subgoal, counting downwards.

\item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or
more to a subgoal, counting upwards.

\item \verb|RANGE|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}.  It applies the given list of tactics to the
corresponding range of subgoals, counting downwards.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsubsection{Control and search tacticals%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A predicate on theorems \verb|thm -> bool| can test
whether a goal state enjoys some desirable property --- such as
having no subgoals.  Tactics that search for satisfactory goal
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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagmlref
%
\begin{isamarkuptext}%
%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
%
%
\isamarkupsubsubsection{Filtering a tactic's results%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{FILTER}\verb|FILTER: (thm -> bool) -> tactic -> tactic| \\
\indexdef{}{ML}{CHANGED}\verb|CHANGED: tactic -> tactic| \\
\end{mldecls}

\begin{description}

\item \verb|FILTER|~\isa{sat\ tac} applies \isa{tac} to the
goal state and returns a sequence consisting of those result goal
states that are satisfactory in the sense of \isa{sat}.

\item \verb|CHANGED|~\isa{tac} applies \isa{tac} to the goal
state and returns precisely those states that differ from the
original state (according to \verb|Thm.eq_thm|).  Thus \verb|CHANGED|~\isa{tac} always has some effect on the state.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Depth-first search%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{DEPTH\_FIRST}\verb|DEPTH_FIRST: (thm -> bool) -> tactic -> tactic| \\
\indexdef{}{ML}{DEPTH\_SOLVE}\verb|DEPTH_SOLVE: tactic -> tactic| \\
\indexdef{}{ML}{DEPTH\_SOLVE\_1}\verb|DEPTH_SOLVE_1: tactic -> tactic| \\
\end{mldecls}

\begin{description}

\item \verb|DEPTH_FIRST|~\isa{sat\ tac} returns the goal state if
\isa{sat} returns true.  Otherwise it applies \isa{tac},
then recursively searches from each element of the resulting
sequence.  The code uses a stack for efficiency, in effect applying
\isa{tac}~\verb|THEN|~\verb|DEPTH_FIRST|~\isa{sat\ tac} to
the state.

\item \verb|DEPTH_SOLVE|\isa{tac} uses \verb|DEPTH_FIRST| to
search for states having no subgoals.

\item \verb|DEPTH_SOLVE_1|~\isa{tac} uses \verb|DEPTH_FIRST| to
search for states having fewer subgoals than the given state.  Thus,
it insists upon solving at least one subgoal.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Other search strategies%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{BEST\_FIRST}\verb|BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic| \\
\indexdef{}{ML}{THEN\_BEST\_FIRST}\verb|THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic| \\
\end{mldecls}

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 \isa{tac}.

\begin{description}

search to find states for which \isa{sat} is true.  For most
applications, it is too slow.

\item \verb|BEST_FIRST|~\isa{{\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} does a heuristic
search, using \isa{dist} to estimate the distance from a
satisfactory state (in the sense of \isa{sat}).  It maintains a
list of states ordered by distance.  It applies \isa{tac} to the
head of this list; if the result contains any satisfactory states,
then it returns them.  Otherwise, \verb|BEST_FIRST| adds the new
states to the list, and continues.

The distance function is typically \verb|size_of_thm|, which computes
the size of the state.  The smaller the state, the fewer and simpler
subgoals it has.

\item \verb|THEN_BEST_FIRST|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} is like
\verb|BEST_FIRST|, except that the priority queue initially contains
the result of applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}} to the goal state.  This
tactical permits separate tactics for starting the search and
continuing the search.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Auxiliary tacticals for searching%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{COND}\verb|COND: (thm -> bool) -> tactic -> tactic -> tactic| \\
\indexdef{}{ML}{IF\_UNSOLVED}\verb|IF_UNSOLVED: tactic -> tactic| \\
\indexdef{}{ML}{SOLVE}\verb|SOLVE: tactic -> tactic| \\
\indexdef{}{ML}{DETERM}\verb|DETERM: tactic -> tactic| \\
\end{mldecls}

\begin{description}

the goal state if it satisfies predicate \isa{sat}, and applies
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}.  It is a conditional tactical in that only one of
because ML uses eager evaluation.

\item \verb|IF_UNSOLVED|~\isa{tac} applies \isa{tac} to the
goal state if it has any subgoals, and simply returns the goal state
otherwise.  Many common tactics, such as \verb|resolve_tac|, fail if
applied to a goal state that has no subgoals.

\item \verb|SOLVE|~\isa{tac} applies \isa{tac} to the goal
state and then fails iff there are subgoals left.

\item \verb|DETERM|~\isa{tac} applies \isa{tac} to the goal
state and returns the head of the resulting sequence.  \verb|DETERM|
limits the search space by making its argument deterministic.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{Predicates and functions useful for searching%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{has\_fewer\_prems}\verb|has_fewer_prems: int -> thm -> bool| \\
\indexdef{}{ML}{Thm.eq\_thm}\verb|Thm.eq_thm: thm * thm -> bool| \\
\indexdef{}{ML}{Thm.eq\_thm\_prop}\verb|Thm.eq_thm_prop: thm * thm -> bool| \\
\indexdef{}{ML}{size\_of\_thm}\verb|size_of_thm: thm -> int| \\
\end{mldecls}

\begin{description}

\item \verb|has_fewer_prems|~\isa{n\ thm} reports whether \isa{thm} has fewer than \isa{n} premises.

compatible background theories.  Both theorems must have the same
conclusions, the same set of hypotheses, and the same set of sort
hypotheses.  Names of bound variables are ignored as usual.

Names of bound variables are ignored.

\item \verb|size_of_thm|~\isa{thm} computes the size of \isa{thm}, namely the number of variables, constants and abstractions
in its conclusion.  It may serve as a distance function for
\verb|BEST_FIRST|.

\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
%
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%