wenzelm@30184: 
lcp@104: \chapter{Tactics} \label{tactics}
wenzelm@30184: \index{tactics|(}
lcp@104: 
lcp@104: \section{Other basic tactics}
paulson@2039: 
paulson@2039: \subsection{Inserting premises and facts}\label{cut_facts_tac}
paulson@2039: \index{tactics!for inserting facts}\index{assumptions!inserting}
paulson@2039: \begin{ttbox} 
paulson@2039: cut_facts_tac : thm list -> int -> tactic
paulson@2039: cut_inst_tac  : (string*string)list -> thm -> int -> tactic
paulson@2039: subgoal_tac   : string -> int -> tactic
wenzelm@9523: subgoals_tac  : string list -> int -> tactic
paulson@2039: \end{ttbox}
paulson@2039: These tactics add assumptions to a subgoal.
paulson@2039: \begin{ttdescription}
paulson@2039: \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
paulson@2039:   adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
paulson@2039:   been inserted as assumptions, they become subject to tactics such as {\tt
paulson@2039:     eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
paulson@2039:   are inserted: Isabelle cannot use assumptions that contain $\Imp$
paulson@2039:   or~$\Forall$.  Sometimes the theorems are premises of a rule being
paulson@2039:   derived, returned by~{\tt goal}; instead of calling this tactic, you
paulson@2039:   could state the goal with an outermost meta-quantifier.
paulson@2039: 
paulson@2039: \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
paulson@2039:   instantiates the {\it thm} with the instantiations {\it insts}, as
oheimb@7491:   described in {\S}\ref{res_inst_tac}.  It adds the resulting theorem as a
paulson@2039:   new assumption to subgoal~$i$. 
paulson@2039: 
paulson@2039: \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
wenzelm@9568: adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
paulson@2039: {\it formula} as a new subgoal, $i+1$.
paulson@2039: 
paulson@2039: \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] 
paulson@2039:   uses {\tt subgoal_tac} to add the members of the list of {\it
paulson@2039:     formulae} as assumptions to subgoal~$i$. 
paulson@2039: \end{ttdescription}
paulson@2039: 
paulson@2039: 
paulson@2039: \subsection{``Putting off'' a subgoal}
paulson@2039: \begin{ttbox} 
paulson@2039: defer_tac : int -> tactic
paulson@2039: \end{ttbox}
paulson@2039: \begin{ttdescription}
paulson@2039: \item[\ttindexbold{defer_tac} {\it i}] 
paulson@2039:   moves subgoal~$i$ to the last position in the proof state.  It can be
paulson@2039:   useful when correcting a proof script: if the tactic given for subgoal~$i$
paulson@2039:   fails, calling {\tt defer_tac} instead will let you continue with the rest
paulson@2039:   of the script.
paulson@2039: 
paulson@2039:   The tactic fails if subgoal~$i$ does not exist or if the proof state
paulson@2039:   contains type unknowns. 
paulson@2039: \end{ttdescription}
paulson@2039: 
paulson@2039: 
wenzelm@4317: \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
lcp@323: \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
lcp@323: \index{definitions}
lcp@323: 
lcp@332: Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
lcp@104: constant or a constant applied to a list of variables, for example $\it
wenzelm@4317: sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
wenzelm@4317: are also supported.  {\bf Unfolding} the definition ${t\equiv u}$ means using
lcp@104: it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
lcp@104: Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
lcp@104: no rewrites are applicable to any subterm.
lcp@104: 
lcp@104: There are rules for unfolding and folding definitions; Isabelle does not do
lcp@104: this automatically.  The corresponding tactics rewrite the proof state,
lcp@332: yielding a single next state.  See also the {\tt goalw} command, which is the
lcp@104: easiest way of handling definitions.
lcp@104: \begin{ttbox} 
lcp@104: rewrite_goals_tac : thm list -> tactic
lcp@104: rewrite_tac       : thm list -> tactic
lcp@104: fold_goals_tac    : thm list -> tactic
lcp@104: fold_tac          : thm list -> tactic
lcp@104: \end{ttbox}
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
lcp@104: unfolds the {\it defs} throughout the subgoals of the proof state, while
lcp@104: leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
lcp@104: particular subgoal.
lcp@104: 
lcp@104: \item[\ttindexbold{rewrite_tac} {\it defs}]  
lcp@104: unfolds the {\it defs} throughout the proof state, including the main goal
lcp@104: --- not normally desirable!
lcp@104: 
lcp@104: \item[\ttindexbold{fold_goals_tac} {\it defs}]  
lcp@104: folds the {\it defs} throughout the subgoals of the proof state, while
lcp@104: leaving the main goal unchanged.
lcp@104: 
lcp@104: \item[\ttindexbold{fold_tac} {\it defs}]  
lcp@104: folds the {\it defs} throughout the proof state.
lcp@323: \end{ttdescription}
lcp@104: 
wenzelm@4317: \begin{warn}
wenzelm@4317:   These tactics only cope with definitions expressed as meta-level
wenzelm@4317:   equalities ($\equiv$).  More general equivalences are handled by the
wenzelm@4317:   simplifier, provided that it is set up appropriately for your logic
wenzelm@4317:   (see Chapter~\ref{chap:simplification}).
wenzelm@4317: \end{warn}
lcp@104: 
lcp@104: \subsection{Theorems useful with tactics}
lcp@323: \index{theorems!of pure theory}
lcp@104: \begin{ttbox} 
lcp@104: asm_rl: thm 
lcp@104: cut_rl: thm 
lcp@104: \end{ttbox}
lcp@323: \begin{ttdescription}
lcp@323: \item[\tdx{asm_rl}] 
lcp@104: is $\psi\Imp\psi$.  Under elim-resolution it does proof by assumption, and
lcp@104: \hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
lcp@104: \begin{ttbox} 
lcp@104: assume_tac {\it i}  ORELSE  eresolve_tac {\it thms} {\it i}
lcp@104: \end{ttbox}
lcp@104: 
lcp@323: \item[\tdx{cut_rl}] 
lcp@104: is $\List{\psi\Imp\theta,\psi}\Imp\theta$.  It is useful for inserting
lcp@323: assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
lcp@323: and {\tt subgoal_tac}.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@104: \section{Obscure tactics}
nipkow@1212: 
paulson@2612: \subsection{Manipulating assumptions}
paulson@2612: \index{assumptions!rotating}
paulson@2612: \begin{ttbox} 
paulson@2612: thin_tac   : string -> int -> tactic
paulson@2612: rotate_tac : int -> int -> tactic
paulson@2612: \end{ttbox}
paulson@2612: \begin{ttdescription}
paulson@2612: \item[\ttindexbold{thin_tac} {\it formula} $i$]  
paulson@2612: \index{assumptions!deleting}
paulson@2612: deletes the specified assumption from subgoal $i$.  Often the assumption
paulson@2612: can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
paulson@2612: assumption will be deleted.  Removing useless assumptions from a subgoal
paulson@2612: increases its readability and can make search tactics run faster.
paulson@2612: 
paulson@2612: \item[\ttindexbold{rotate_tac} $n$ $i$]  
paulson@2612: \index{assumptions!rotating}
paulson@2612: rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
paulson@2612: if $n$ is positive, and from left to right if $n$ is negative.  This is 
paulson@2612: sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 
paulson@2612: processes assumptions from left to right.
paulson@2612: \end{ttdescription}
paulson@2612: 
paulson@2612: 
paulson@2612: \subsection{Tidying the proof state}
paulson@3400: \index{duplicate subgoals!removing}
paulson@2612: \index{parameters!removing unused}
paulson@2612: \index{flex-flex constraints}
paulson@2612: \begin{ttbox} 
paulson@3400: distinct_subgoals_tac : tactic
paulson@3400: prune_params_tac      : tactic
paulson@3400: flexflex_tac          : tactic
paulson@2612: \end{ttbox}
paulson@2612: \begin{ttdescription}
wenzelm@9695: \item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
wenzelm@9695:   proof state.  (These arise especially in ZF, where the subgoals are
wenzelm@9695:   essentially type constraints.)
paulson@3400: 
paulson@2612: \item[\ttindexbold{prune_params_tac}]  
paulson@2612:   removes unused parameters from all subgoals of the proof state.  It works
paulson@2612:   by rewriting with the theorem $(\Forall x. V)\equiv V$.  This tactic can
paulson@2612:   make the proof state more readable.  It is used with
paulson@2612:   \ttindex{rule_by_tactic} to simplify the resulting theorem.
paulson@2612: 
paulson@2612: \item[\ttindexbold{flexflex_tac}]  
paulson@2612:   removes all flex-flex pairs from the proof state by applying the trivial
paulson@2612:   unifier.  This drastic step loses information, and should only be done as
paulson@2612:   the last step of a proof.
paulson@2612: 
paulson@2612:   Flex-flex constraints arise from difficult cases of higher-order
paulson@2612:   unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
oheimb@7491:   some variables in a rule~({\S}\ref{res_inst_tac}).  Normally flex-flex
paulson@2612:   constraints can be ignored; they often disappear as unknowns get
paulson@2612:   instantiated.
paulson@2612: \end{ttdescription}
paulson@2612: 
paulson@2612: 
lcp@104: \subsection{Composition: resolution without lifting}
lcp@323: \index{tactics!for composition}
lcp@104: \begin{ttbox}
lcp@104: compose_tac: (bool * thm * int) -> int -> tactic
lcp@104: \end{ttbox}
lcp@332: {\bf Composing} two rules means resolving them without prior lifting or
lcp@104: renaming of unknowns.  This low-level operation, which underlies the
lcp@104: resolution tactics, may occasionally be useful for special effects.
lcp@104: A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
lcp@104: rule, then passes the result to {\tt compose_tac}.
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
lcp@104: refines subgoal~$i$ using $rule$, without lifting.  The $rule$ is taken to
lcp@104: have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
lcp@323: not be atomic; thus $m$ determines the number of new subgoals.  If
lcp@104: $flag$ is {\tt true} then it performs elim-resolution --- it solves the
lcp@104: first premise of~$rule$ by assumption and deletes that assumption.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
wenzelm@4276: \section{*Managing lots of rules}
lcp@104: These operations are not intended for interactive use.  They are concerned
lcp@104: with the processing of large numbers of rules in automatic proof
lcp@104: strategies.  Higher-order resolution involving a long list of rules is
lcp@104: slow.  Filtering techniques can shorten the list of rules given to
paulson@2039: resolution, and can also detect whether a subgoal is too flexible,
lcp@104: with too many rules applicable.
lcp@104: 
lcp@104: \subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
lcp@104: \index{tactics!resolution}
lcp@104: \begin{ttbox} 
lcp@104: biresolve_tac   : (bool*thm)list -> int -> tactic
lcp@104: bimatch_tac     : (bool*thm)list -> int -> tactic
lcp@104: subgoals_of_brl : bool*thm -> int
lcp@104: lessb           : (bool*thm) * (bool*thm) -> bool
lcp@104: \end{ttbox}
lcp@104: {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
lcp@104: pair, it applies resolution if the flag is~{\tt false} and
lcp@104: elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
lcp@104: mixture of introduction and elimination rules.
lcp@104: 
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
lcp@104: refines the proof state by resolution or elim-resolution on each rule, as
lcp@104: indicated by its flag.  It affects subgoal~$i$ of the proof state.
lcp@104: 
lcp@104: \item[\ttindexbold{bimatch_tac}] 
lcp@104: is like {\tt biresolve_tac}, but performs matching: unknowns in the
oheimb@7491: proof state are never updated (see~{\S}\ref{match_tac}).
lcp@104: 
lcp@104: \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
paulson@4597: returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
lcp@104: pair (if applied to a suitable subgoal).  This is $n$ if the flag is
lcp@104: {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
lcp@104: of premises of the rule.  Elim-resolution yields one fewer subgoal than
lcp@104: ordinary resolution because it solves the major premise by assumption.
lcp@104: 
lcp@104: \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
lcp@104: returns the result of 
lcp@104: \begin{ttbox}
lcp@332: subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
lcp@104: \end{ttbox}
lcp@323: \end{ttdescription}
lcp@104: Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
lcp@104: (flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
lcp@104: those that yield the fewest subgoals should be tried first.
lcp@104: 
lcp@104: 
lcp@323: \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
lcp@104: \index{discrimination nets|bold}
lcp@104: \index{tactics!resolution}
lcp@104: \begin{ttbox} 
lcp@104: net_resolve_tac  : thm list -> int -> tactic
lcp@104: net_match_tac    : thm list -> int -> tactic
lcp@104: net_biresolve_tac: (bool*thm) list -> int -> tactic
lcp@104: net_bimatch_tac  : (bool*thm) list -> int -> tactic
lcp@104: filt_resolve_tac : thm list -> int -> int -> tactic
lcp@104: could_unify      : term*term->bool
paulson@8136: filter_thms      : (term*term->bool) -> int*term*thm list -> thm{\ts}list
lcp@104: \end{ttbox}
lcp@323: The module {\tt Net} implements a discrimination net data structure for
lcp@104: fast selection of rules \cite[Chapter 14]{charniak80}.  A term is
lcp@104: classified by the symbol list obtained by flattening it in preorder.
lcp@104: The flattening takes account of function applications, constants, and free
lcp@104: and bound variables; it identifies all unknowns and also regards
lcp@323: \index{lambda abs@$\lambda$-abstractions}
lcp@104: $\lambda$-abstractions as unknowns, since they could $\eta$-contract to
lcp@104: anything.  
lcp@104: 
lcp@104: A discrimination net serves as a polymorphic dictionary indexed by terms.
lcp@104: The module provides various functions for inserting and removing items from
lcp@104: nets.  It provides functions for returning all items whose term could match
lcp@104: or unify with a target term.  The matching and unification tests are
lcp@104: overly lax (due to the identifications mentioned above) but they serve as
lcp@104: useful filters.
lcp@104: 
lcp@104: A net can store introduction rules indexed by their conclusion, and
lcp@104: elimination rules indexed by their major premise.  Isabelle provides
lcp@323: several functions for `compiling' long lists of rules into fast
lcp@104: resolution tactics.  When supplied with a list of theorems, these functions
lcp@104: build a discrimination net; the net is used when the tactic is applied to a
lcp@332: goal.  To avoid repeatedly constructing the nets, use currying: bind the
lcp@104: resulting tactics to \ML{} identifiers.
lcp@104: 
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{net_resolve_tac} {\it thms}] 
lcp@104: builds a discrimination net to obtain the effect of a similar call to {\tt
lcp@104: resolve_tac}.
lcp@104: 
lcp@104: \item[\ttindexbold{net_match_tac} {\it thms}] 
lcp@104: builds a discrimination net to obtain the effect of a similar call to {\tt
lcp@104: match_tac}.
lcp@104: 
lcp@104: \item[\ttindexbold{net_biresolve_tac} {\it brls}] 
lcp@104: builds a discrimination net to obtain the effect of a similar call to {\tt
lcp@104: biresolve_tac}.
lcp@104: 
lcp@104: \item[\ttindexbold{net_bimatch_tac} {\it brls}] 
lcp@104: builds a discrimination net to obtain the effect of a similar call to {\tt
lcp@104: bimatch_tac}.
lcp@104: 
lcp@104: \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] 
lcp@104: uses discrimination nets to extract the {\it thms} that are applicable to
lcp@104: subgoal~$i$.  If more than {\it maxr\/} theorems are applicable then the
lcp@104: tactic fails.  Otherwise it calls {\tt resolve_tac}.  
lcp@104: 
lcp@104: This tactic helps avoid runaway instantiation of unknowns, for example in
lcp@104: type inference.
lcp@104: 
lcp@104: \item[\ttindexbold{could_unify} ({\it t},{\it u})] 
lcp@323: returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
lcp@104: otherwise returns~{\tt true}.  It assumes all variables are distinct,
lcp@104: reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
lcp@104: 
lcp@104: \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] 
lcp@104: returns the list of potentially resolvable rules (in {\it thms\/}) for the
lcp@104: subgoal {\it prem}, using the predicate {\it could\/} to compare the
lcp@104: conclusion of the subgoal with the conclusion of each rule.  The resulting list
lcp@104: is no longer than {\it limit}.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: \index{tactics|)}
wenzelm@5371: 
wenzelm@5371: 
wenzelm@5371: %%% Local Variables: 
wenzelm@5371: %%% mode: latex
wenzelm@5371: %%% TeX-master: "ref"
wenzelm@5371: %%% End: