%% $Id$

 \chapter{Tactics} \label{tactics}

 \index{tactics|(} Tactics have type \mltydx{tactic}.  This is just an

 abbreviation for 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; instead they are

 expressed using basic tactics and tacticals.

 This chapter only presents the primitive tactics.  Substantial proofs

 require the power of automatic tools like simplification

 (Chapter~\ref{chap:simplification}) and classical tableau reasoning

 (Chapter~\ref{chap:classical}).

 \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{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{ttdescription}

 \item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 

   refines the proof state using the rules, which should normally be

   introduction rules.  It resolves a rule's conclusion with

   subgoal~$i$ of the proof state.

 \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 

   \index{elim-resolution}

   performs elim-resolution with the rules, which should normally be

   elimination rules.  It resolves with a rule, solves its first premise by

   assumption, and finally {\em deletes\/} that assumption from any new

   subgoals.

 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 

   \index{forward proof}\index{destruct-resolution}

   performs destruct-resolution with the rules, which normally should

   be destruction rules.  This replaces an assumption by the result of

   applying one of the rules.

 \item[\ttindexbold{forward_tac}]\index{forward proof}

   is like {\tt 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{ttdescription}

 \subsection{Assumption tactics}

 \index{tactics!assumption|bold}\index{assumptions!tactics for}

 \begin{ttbox} 

 assume_tac    : int -> tactic

 eq_assume_tac : int -> tactic

 \end{ttbox} 

 \begin{ttdescription}

 \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

 {\em 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{ttdescription}

 \subsection{Matching tactics} \label{match_tac}

 \index{tactics!matching}

 \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{ttdescription}

 \item[\ttindexbold{match_tac} {\it thms} {\it i}] 

 refines the proof state using the rules, matching a 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{ttdescription}

 \subsection{Resolution with instantiation} \label{res_inst_tac}

 \index{tactics!instantiation}\index{instantiation}

 \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 unknowns in the rule ---

 typically, in the rule's conclusion.  Each instantiation is a pair

 {\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading

 question mark!

 \begin{itemize}

 \item If $v$ is the type unknown {\tt'a}, then

 the rule must contain a type unknown \verb$?'a$ of some

 sort~$s$, and $e$ should be a type of sort $s$.

 \item If $v$ is the unknown {\tt P}, then

 the rule must contain an unknown \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 type unknowns 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{ttdescription}

 \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 unknown 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{ttdescription}

 \section{Other basic tactics}

 \subsection{Tactic shortcuts}

 \index{shortcuts!for tactics}

 \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{ttdescription}

 \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}] 

 abbreviates \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{ttdescription}

 \subsection{Inserting premises and facts}\label{cut_facts_tac}

 \index{tactics!for inserting facts}\index{assumptions!inserting}

 \begin{ttbox} 

 cut_facts_tac : thm list -> int -> tactic

 cut_inst_tac  : (string*string)list -> thm -> int -> tactic

 subgoal_tac   : string -> int -> tactic

 subgoal_tacs  : string list -> int -> tactic

 \end{ttbox}

 These tactics add assumptions to a subgoal.

 \begin{ttdescription}

 \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 tactics such as {\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{cut_inst_tac} {\it insts} {\it thm} {\it i}]

   instantiates the {\it thm} with the instantiations {\it insts}, as

   described in \S\ref{res_inst_tac}.  It adds the resulting theorem as a

   new assumption to subgoal~$i$. 

 \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$.

 \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] 

   uses {\tt subgoal_tac} to add the members of the list of {\it

     formulae} as assumptions to subgoal~$i$. 

 \end{ttdescription}

 \subsection{``Putting off'' a subgoal}

 \begin{ttbox} 

 defer_tac : int -> tactic

 \end{ttbox}

 \begin{ttdescription}

 \item[\ttindexbold{defer_tac} {\it i}] 

   moves subgoal~$i$ to the last position in the proof state.  It can be

   useful when correcting a proof script: if the tactic given for subgoal~$i$

   fails, calling {\tt defer_tac} instead will let you continue with the rest

   of the script.

   The tactic fails if subgoal~$i$ does not exist or if the proof state

   contains type unknowns. 

 \end{ttdescription}

 \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}

 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}

 \index{definitions}

 Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically 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 also 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 single next state.  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{ttdescription}

 \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{ttdescription}

 \begin{warn}

   These tactics only cope with definitions expressed as meta-level

   equalities ($\equiv$).  More general equivalences are handled by the

   simplifier, provided that it is set up appropriately for your logic

   (see Chapter~\ref{chap:simplification}).

 \end{warn}

 \subsection{Theorems useful with tactics}

 \index{theorems!of pure theory}

 \begin{ttbox} 

 asm_rl: thm 

 cut_rl: thm 

 \end{ttbox}

 \begin{ttdescription}

 \item[\tdx{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[\tdx{cut_rl}] 

 is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting

 assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}

 and {\tt subgoal_tac}.

 \end{ttdescription}

 \section{Obscure tactics}

 \subsection{Renaming parameters in a goal} \index{parameters!renaming}

 \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 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{ttdescription}

 \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[set \ttindexbold{Logic.auto_rename};] 

 makes Isabelle generate uniform names for parameters. 

 \end{ttdescription}

 \subsection{Manipulating assumptions}

 \index{assumptions!rotating}

 \begin{ttbox} 

 thin_tac   : string -> int -> tactic

 rotate_tac : int -> int -> tactic

 \end{ttbox}

 \begin{ttdescription}

 \item[\ttindexbold{thin_tac} {\it formula} $i$]  

 \index{assumptions!deleting}

 deletes the specified assumption from subgoal $i$.  Often the assumption

 can be abbreviated, replacing subformul{\ae} by unknowns; the first matching

 assumption will be deleted.  Removing useless assumptions from a subgoal

 increases its readability and can make search tactics run faster.

 \item[\ttindexbold{rotate_tac} $n$ $i$]  

 \index{assumptions!rotating}

 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left

 if $n$ is positive, and from left to right if $n$ is negative.  This is 

 sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 

 processes assumptions from left to right.

 \end{ttdescription}

 \subsection{Tidying the proof state}

 \index{duplicate subgoals!removing}

 \index{parameters!removing unused}

 \index{flex-flex constraints}

 \begin{ttbox} 

 distinct_subgoals_tac : tactic

 prune_params_tac      : tactic

 flexflex_tac          : tactic

 \end{ttbox}

 \begin{ttdescription}

 \item[\ttindexbold{distinct_subgoals_tac}]  

   removes duplicate subgoals from a proof state.  (These arise especially

   in \ZF{}, where the subgoals are essentially type constraints.)

 \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{ttdescription}

 \subsection{Composition: resolution without lifting}

 \index{tactics!for composition}

 \begin{ttbox}

 compose_tac: (bool * thm * int) -> int -> tactic

 \end{ttbox}

 {\bf Composing} two rules means resolving 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{ttdescription}

 \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

 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{ttdescription}

 \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 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{ttdescription}

 \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}

 \end{ttdescription}

 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.

 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}

 \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 {\tt 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

 \index{lambda abs@$\lambda$-abstractions}

 $\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 repeatedly constructing the nets, use currying: bind the

 resulting tactics to \ML{} identifiers.

 \begin{ttdescription}

 \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{ttdescription}

 \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} A tactic maps theorems to sequences of

 theorems.  The type constructor for sequences (lazy lists) is called

 \mltydx{Seq.seq}.  To simplify the types of tactics and tacticals,

 Isabelle defines a type abbreviation:

 \begin{ttbox} 

 type tactic = thm -> thm Seq.seq

 \end{ttbox} 

 The following operations provide means for coding tactics in a clean style.

 \begin{ttbox} 

 PRIMITIVE :                  (thm -> thm) -> tactic  

 SUBGOAL   : ((term*int) -> tactic) -> int -> tactic

 \end{ttbox} 

 \begin{ttdescription}

 \item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that

   applies $f$ to the proof state and returns the result as a one-element

   sequence.  If $f$ raises an exception, then the tactic's result is the empty

   sequence.

 \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 using tactics and tacticals, but may

 peek at a particular subgoal:

 \begin{ttbox} 

 SUBGOAL (fn (t,i) => {\it tactic-valued expression})

 \end{ttbox} 

 \end{ttdescription}

 \subsection{Tracing}

 \index{tactics!tracing}

 \index{tracing!of tactics}

 \begin{ttbox} 

 pause_tac: tactic

 print_tac: tactic

 \end{ttbox}

 These tactics print tracing 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{ttdescription}

 \item[\ttindexbold{pause_tac}] 

 prints {\footnotesize\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{ttdescription}

 \section{*Sequences}

 \index{sequences (lazy lists)|bold}

 The module {\tt Seq} declares a type of lazy lists.  It uses

 Isabelle's type \mltydx{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}

 The {\tt Seq} structure is supposed to be accessed via fully qualified

 names and should not be \texttt{open}.

 \subsection{Basic operations on sequences}

 \begin{ttbox} 

 Seq.empty   : 'a seq

 Seq.make    : (unit -> ('a * 'a seq) option) -> 'a seq

 Seq.single  : 'a -> 'a seq

 Seq.pull    : 'a seq -> ('a * 'a seq) option

 \end{ttbox}

 \begin{ttdescription}

 \item[Seq.empty] is the empty sequence.

 \item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the

   sequence with head~$x$ and tail~$xq$, neither of which is evaluated.

 \item[Seq.single $x$] 

 constructs the sequence containing the single element~$x$.

 \item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and

   {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.

   Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}

   the value of~$x$; it is not stored!

 \end{ttdescription}

 \subsection{Converting between sequences and lists}

 \begin{ttbox} 

 Seq.chop    : int * 'a seq -> 'a list * 'a seq

 Seq.list_of : 'a seq -> 'a list

 Seq.of_list : 'a list -> 'a seq

 \end{ttbox}

 \begin{ttdescription}

 \item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a

   list, paired with the remaining elements of~$xq$.  If $xq$ has fewer

   than~$n$ elements, then so will the list.

 \item[Seq.list_of $xq$] returns the elements of~$xq$, which must be

   finite, as a list.

 \item[Seq.of_list $xs$] creates a sequence containing the elements

   of~$xs$.

 \end{ttdescription}

 \subsection{Combining sequences}

 \begin{ttbox} 

 Seq.append      : 'a seq * 'a seq -> 'a seq

 Seq.interleave  : 'a seq * 'a seq -> 'a seq

 Seq.flat        : 'a seq seq -> 'a seq

 Seq.map         : ('a -> 'b) -> 'a seq -> 'b seq

 Seq.filter      : ('a -> bool) -> 'a seq -> 'a seq

 \end{ttbox} 

 \begin{ttdescription}

 \item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.

 \item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by

   interleaving their elements.  The result contains all the elements

   of the sequences, even if both are infinite.

 \item[Seq.flat $xqq$] concatenates a sequence of sequences.

 \item[Seq.map $f$ $xq$] applies $f$ to every element

   of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.

 \item[Seq.filter $p$ $xq$] returns the sequence consisting of all

   elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.

 \end{ttdescription}

 \index{tactics|)}