
lcp@104: %% $Id$
lcp@104: \chapter{Tactics} \label{tactics}
wenzelm@3108: \index{tactics|(} Tactics have type \mltydx{tactic}.  This is just an
wenzelm@3108: abbreviation for functions from theorems to theorem sequences, where
wenzelm@3108: the theorems represent states of a backward proof.  Tactics seldom
wenzelm@3108: need to be coded from scratch, as functions; instead they are
wenzelm@3108: expressed using basic tactics and tacticals.
lcp@104: 
wenzelm@4317: This chapter only presents the primitive tactics.  Substantial proofs
wenzelm@4317: require the power of automatic tools like simplification
wenzelm@4317: (Chapter~\ref{chap:simplification}) and classical tableau reasoning
wenzelm@4317: (Chapter~\ref{chap:classical}).
paulson@2039: 
lcp@104: \section{Resolution and assumption tactics}
lcp@104: {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
lcp@104: a rule.  {\bf Elim-resolution} is particularly suited for elimination
lcp@104: rules, while {\bf destruct-resolution} is particularly suited for
lcp@104: destruction rules.  The {\tt r}, {\tt e}, {\tt d} naming convention is
lcp@104: maintained for several different kinds of resolution tactics, as well as
lcp@104: the shortcuts in the subgoal module.
lcp@104: 
lcp@104: All the tactics in this section act on a subgoal designated by a positive
lcp@104: integer~$i$.  They fail (by returning the empty sequence) if~$i$ is out of
lcp@104: range.
lcp@104: 
lcp@104: \subsection{Resolution tactics}
lcp@323: \index{resolution!tactics}
lcp@104: \index{tactics!resolution|bold}
lcp@104: \begin{ttbox} 
lcp@104: resolve_tac  : thm list -> int -> tactic
lcp@104: eresolve_tac : thm list -> int -> tactic
lcp@104: dresolve_tac : thm list -> int -> tactic
lcp@104: forward_tac  : thm list -> int -> tactic 
lcp@104: \end{ttbox}
lcp@104: These perform resolution on a list of theorems, $thms$, representing a list
lcp@104: of object-rules.  When generating next states, they take each of the rules
lcp@104: in the order given.  Each rule may yield several next states, or none:
lcp@104: higher-order resolution may yield multiple resolvents.
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
lcp@323:   refines the proof state using the rules, which should normally be
lcp@323:   introduction rules.  It resolves a rule's conclusion with
lcp@323:   subgoal~$i$ of the proof state.
lcp@104: 
lcp@104: \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
lcp@323:   \index{elim-resolution}
lcp@323:   performs elim-resolution with the rules, which should normally be
paulson@4607:   elimination rules.  It resolves with a rule, proves its first premise by
paulson@4607:   assumption, and finally \emph{deletes} that assumption from any new
paulson@4607:   subgoals.  (To rotate a rule's premises,
oheimb@7491:   see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
lcp@104: 
lcp@104: \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
lcp@323:   \index{forward proof}\index{destruct-resolution}
lcp@323:   performs destruct-resolution with the rules, which normally should
lcp@323:   be destruction rules.  This replaces an assumption by the result of
lcp@323:   applying one of the rules.
lcp@104: 
lcp@323: \item[\ttindexbold{forward_tac}]\index{forward proof}
lcp@323:   is like {\tt dresolve_tac} except that the selected assumption is not
lcp@323:   deleted.  It applies a rule to an assumption, adding the result as a new
lcp@323:   assumption.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: \subsection{Assumption tactics}
lcp@323: \index{tactics!assumption|bold}\index{assumptions!tactics for}
lcp@104: \begin{ttbox} 
lcp@104: assume_tac    : int -> tactic
lcp@104: eq_assume_tac : int -> tactic
lcp@104: \end{ttbox} 
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{assume_tac} {\it i}] 
lcp@104: attempts to solve subgoal~$i$ by assumption.
lcp@104: 
lcp@104: \item[\ttindexbold{eq_assume_tac}] 
lcp@104: is like {\tt assume_tac} but does not use unification.  It succeeds (with a
paulson@4607: \emph{unique} next state) if one of the assumptions is identical to the
lcp@104: subgoal's conclusion.  Since it does not instantiate variables, it cannot
lcp@104: make other subgoals unprovable.  It is intended to be called from proof
lcp@104: strategies, not interactively.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: \subsection{Matching tactics} \label{match_tac}
lcp@323: \index{tactics!matching}
lcp@104: \begin{ttbox} 
lcp@104: match_tac  : thm list -> int -> tactic
lcp@104: ematch_tac : thm list -> int -> tactic
lcp@104: dmatch_tac : thm list -> int -> tactic
lcp@104: \end{ttbox}
lcp@104: These are just like the resolution tactics except that they never
lcp@104: instantiate unknowns in the proof state.  Flexible subgoals are not updated
lcp@104: willy-nilly, but are left alone.  Matching --- strictly speaking --- means
lcp@104: treating the unknowns in the proof state as constants; these tactics merely
lcp@104: discard unifiers that would update the proof state.
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{match_tac} {\it thms} {\it i}] 
lcp@323: refines the proof state using the rules, matching a rule's
lcp@104: conclusion with subgoal~$i$ of the proof state.
lcp@104: 
lcp@104: \item[\ttindexbold{ematch_tac}] 
lcp@104: is like {\tt match_tac}, but performs elim-resolution.
lcp@104: 
lcp@104: \item[\ttindexbold{dmatch_tac}] 
lcp@104: is like {\tt match_tac}, but performs destruct-resolution.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@104: \subsection{Resolution with instantiation} \label{res_inst_tac}
lcp@323: \index{tactics!instantiation}\index{instantiation}
lcp@104: \begin{ttbox} 
lcp@104: res_inst_tac  : (string*string)list -> thm -> int -> tactic
lcp@104: eres_inst_tac : (string*string)list -> thm -> int -> tactic
lcp@104: dres_inst_tac : (string*string)list -> thm -> int -> tactic
lcp@104: forw_inst_tac : (string*string)list -> thm -> int -> tactic
lcp@104: \end{ttbox}
lcp@104: These tactics are designed for applying rules such as substitution and
lcp@104: induction, which cause difficulties for higher-order unification.  The
lcp@332: tactics accept explicit instantiations for unknowns in the rule ---
lcp@332: typically, in the rule's conclusion.  Each instantiation is a pair
paulson@4607: {\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading
lcp@332: question mark!
lcp@104: \begin{itemize}
lcp@332: \item If $v$ is the type unknown {\tt'a}, then
lcp@332: the rule must contain a type unknown \verb$?'a$ of some
lcp@104: sort~$s$, and $e$ should be a type of sort $s$.
lcp@104: 
lcp@332: \item If $v$ is the unknown {\tt P}, then
lcp@332: the rule must contain an unknown \verb$?P$ of some type~$\tau$,
lcp@104: and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
lcp@104: $\sigma$ are unifiable.  If the unification of $\tau$ and $\sigma$
lcp@332: instantiates any type unknowns in $\tau$, these instantiations
lcp@104: are recorded for application to the rule.
lcp@104: \end{itemize}
paulson@8136: Types are instantiated before terms are.  Because type instantiations are
lcp@104: inferred from term instantiations, explicit type instantiations are seldom
lcp@104: necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
paulson@8136: \texttt{[("'a","bool"), ("t","True")]} may be simplified to
paulson@8136: \texttt{[("t","True")]}.  Type unknowns in the proof state may cause
lcp@104: failure because the tactics cannot instantiate them.
lcp@104: 
lcp@104: The instantiation tactics act on a given subgoal.  Terms in the
lcp@104: instantiations are type-checked in the context of that subgoal --- in
lcp@104: particular, they may refer to that subgoal's parameters.  Any unknowns in
lcp@104: the terms receive subscripts and are lifted over the parameters; thus, you
lcp@104: may not refer to unknowns in the subgoal.
lcp@104: 
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
lcp@104: instantiates the rule {\it thm} with the instantiations {\it insts}, as
lcp@104: described above, and then performs resolution on subgoal~$i$.  Resolution
lcp@104: typically causes further instantiations; you need not give explicit
lcp@332: instantiations for every unknown in the rule.
lcp@104: 
lcp@104: \item[\ttindexbold{eres_inst_tac}] 
lcp@104: is like {\tt res_inst_tac}, but performs elim-resolution.
lcp@104: 
lcp@104: \item[\ttindexbold{dres_inst_tac}] 
lcp@104: is like {\tt res_inst_tac}, but performs destruct-resolution.
lcp@104: 
lcp@104: \item[\ttindexbold{forw_inst_tac}] 
lcp@104: is like {\tt dres_inst_tac} except that the selected assumption is not
lcp@104: deleted.  It applies the instantiated rule to an assumption, adding the
lcp@104: result as a new assumption.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@104: \section{Other basic tactics}
paulson@2039: \subsection{Tactic shortcuts}
paulson@2039: \index{shortcuts!for tactics}
paulson@2039: \index{tactics!resolution}\index{tactics!assumption}
paulson@2039: \index{tactics!meta-rewriting}
paulson@2039: \begin{ttbox} 
oheimb@7491: rtac     :      thm ->        int -> tactic
oheimb@7491: etac     :      thm ->        int -> tactic
oheimb@7491: dtac     :      thm ->        int -> tactic
oheimb@7491: ftac     :      thm ->        int -> tactic
oheimb@7491: atac     :                    int -> tactic
oheimb@7491: eatac    :      thm -> int -> int -> tactic
oheimb@7491: datac    :      thm -> int -> int -> tactic
oheimb@7491: fatac    :      thm -> int -> int -> tactic
oheimb@7491: ares_tac :      thm list   -> int -> tactic
oheimb@7491: rewtac   :      thm ->               tactic
paulson@2039: \end{ttbox}
paulson@2039: These abbreviate common uses of tactics.
paulson@2039: \begin{ttdescription}
paulson@2039: \item[\ttindexbold{rtac} {\it thm} {\it i}] 
paulson@2039: abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
paulson@2039: 
paulson@2039: \item[\ttindexbold{etac} {\it thm} {\it i}] 
paulson@2039: abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
paulson@2039: 
paulson@2039: \item[\ttindexbold{dtac} {\it thm} {\it i}] 
paulson@2039: abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
paulson@2039: destruct-resolution.
paulson@2039: 
oheimb@7491: \item[\ttindexbold{ftac} {\it thm} {\it i}] 
oheimb@7491: abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
oheimb@7491: destruct-resolution without deleting the assumption.
oheimb@7491: 
paulson@2039: \item[\ttindexbold{atac} {\it i}] 
paulson@2039: abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
paulson@2039: 
oheimb@7491: \item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}] 
oheimb@7491: performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac}, 
oheimb@7491: solving additionally {\it j}~premises of the rule {\it thm} by assumption.
oheimb@7491: 
oheimb@7491: \item[\ttindexbold{datac} {\it thm} {\it j} {\it i}] 
oheimb@7491: performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac}, 
oheimb@7491: solving additionally {\it j}~premises of the rule {\it thm} by assumption.
oheimb@7491: 
oheimb@7491: \item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}] 
oheimb@7491: performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac}, 
oheimb@7491: solving additionally {\it j}~premises of the rule {\it thm} by assumption.
oheimb@7491: 
paulson@2039: \item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
paulson@2039: tries proof by assumption and resolution; it abbreviates
paulson@2039: \begin{ttbox}
paulson@2039: assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
paulson@2039: \end{ttbox}
paulson@2039: 
paulson@2039: \item[\ttindexbold{rewtac} {\it def}] 
paulson@2039: abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
paulson@2039: \end{ttdescription}
paulson@2039: 
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}] 
paulson@2039: adds the {\it formula} as a 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: 
lcp@323: \subsection{Renaming parameters in a goal} \index{parameters!renaming}
lcp@104: \begin{ttbox} 
lcp@104: rename_tac        : string -> int -> tactic
lcp@104: rename_last_tac   : string -> string list -> int -> tactic
lcp@104: Logic.set_rename_prefix : string -> unit
lcp@104: Logic.auto_rename       : bool ref      \hfill{\bf initially false}
lcp@104: \end{ttbox}
lcp@104: When creating a parameter, Isabelle chooses its name by matching variable
lcp@104: names via the object-rule.  Given the rule $(\forall I)$ formalized as
lcp@104: $\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
lcp@104: the $\Forall$-bound variable in the premise has the same name as the
lcp@104: $\forall$-bound variable in the conclusion.  
lcp@104: 
lcp@104: Sometimes there is insufficient information and Isabelle chooses an
lcp@104: arbitrary name.  The renaming tactics let you override Isabelle's choice.
lcp@104: Because renaming parameters has no logical effect on the proof state, the
lcp@323: {\tt by} command prints the message {\tt Warning:\ same as previous
lcp@104: level}.
lcp@104: 
lcp@104: Alternatively, you can suppress the naming mechanism described above and
lcp@104: have Isabelle generate uniform names for parameters.  These names have the
lcp@104: form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
lcp@104: prefix.  They are ugly but predictable.
lcp@104: 
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{rename_tac} {\it str} {\it i}] 
lcp@104: interprets the string {\it str} as a series of blank-separated variable
lcp@104: names, and uses them to rename the parameters of subgoal~$i$.  The names
lcp@104: must be distinct.  If there are fewer names than parameters, then the
lcp@104: tactic renames the innermost parameters and may modify the remaining ones
lcp@104: to ensure that all the parameters are distinct.
lcp@104: 
lcp@104: \item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}] 
lcp@104: generates a list of names by attaching each of the {\it suffixes\/} to the 
lcp@104: {\it prefix}.  It is intended for coding structural induction tactics,
lcp@104: where several of the new parameters should have related names.
lcp@104: 
lcp@104: \item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};] 
lcp@104: sets the prefix for uniform renaming to~{\it prefix}.  The default prefix
lcp@104: is {\tt"k"}.
lcp@104: 
wenzelm@4317: \item[set \ttindexbold{Logic.auto_rename};] 
lcp@104: makes Isabelle generate uniform names for parameters. 
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
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}
paulson@3400: \item[\ttindexbold{distinct_subgoals_tac}]  
paulson@3400:   removes duplicate subgoals from a proof state.  (These arise especially
paulson@3400:   in \ZF{}, where the subgoals are 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: 
wenzelm@4317: \section{Programming tools for proof strategies}
lcp@104: Do not consider using the primitives discussed in this section unless you
lcp@323: really need to code tactics from scratch.
lcp@104: 
wenzelm@6618: \subsection{Operations on tactics}
paulson@3561: \index{tactics!primitives for coding} A tactic maps theorems to sequences of
paulson@3561: theorems.  The type constructor for sequences (lazy lists) is called
wenzelm@4276: \mltydx{Seq.seq}.  To simplify the types of tactics and tacticals,
paulson@3561: Isabelle defines a type abbreviation:
lcp@104: \begin{ttbox} 
wenzelm@4276: type tactic = thm -> thm Seq.seq
lcp@104: \end{ttbox} 
wenzelm@3108: The following operations provide means for coding tactics in a clean style.
lcp@104: \begin{ttbox} 
lcp@104: PRIMITIVE :                  (thm -> thm) -> tactic  
lcp@104: SUBGOAL   : ((term*int) -> tactic) -> int -> tactic
lcp@104: \end{ttbox} 
lcp@323: \begin{ttdescription}
paulson@3561: \item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
paulson@3561:   applies $f$ to the proof state and returns the result as a one-element
paulson@3561:   sequence.  If $f$ raises an exception, then the tactic's result is the empty
paulson@3561:   sequence.
lcp@104: 
lcp@104: \item[\ttindexbold{SUBGOAL} $f$ $i$] 
lcp@104: extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
lcp@104: tactic by calling~$f(t,i)$.  It applies the resulting tactic to the same
lcp@323: state.  The tactic body is expressed using tactics and tacticals, but may
lcp@323: peek at a particular subgoal:
lcp@104: \begin{ttbox} 
lcp@323: SUBGOAL (fn (t,i) => {\it tactic-valued expression})
lcp@104: \end{ttbox} 
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@104: \subsection{Tracing}
lcp@323: \index{tactics!tracing}
lcp@104: \index{tracing!of tactics}
lcp@104: \begin{ttbox} 
lcp@104: pause_tac: tactic
lcp@104: print_tac: tactic
lcp@104: \end{ttbox}
lcp@332: These tactics print tracing information when they are applied to a proof
lcp@332: state.  Their output may be difficult to interpret.  Note that certain of
lcp@332: the searching tacticals, such as {\tt REPEAT}, have built-in tracing
lcp@332: options.
lcp@323: \begin{ttdescription}
lcp@104: \item[\ttindexbold{pause_tac}] 
lcp@332: prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
lcp@332: from the terminal.  If this line is blank then it returns the proof state
lcp@332: unchanged; otherwise it fails (which may terminate a repetition).
lcp@104: 
lcp@104: \item[\ttindexbold{print_tac}] 
lcp@104: returns the proof state unchanged, with the side effect of printing it at
lcp@104: the terminal.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
wenzelm@4276: \section{*Sequences}
lcp@104: \index{sequences (lazy lists)|bold}
wenzelm@4276: The module {\tt Seq} declares a type of lazy lists.  It uses
lcp@323: Isabelle's type \mltydx{option} to represent the possible presence
lcp@104: (\ttindexbold{Some}) or absence (\ttindexbold{None}) of
lcp@104: a value:
lcp@104: \begin{ttbox}
lcp@104: datatype 'a option = None  |  Some of 'a;
lcp@104: \end{ttbox}
wenzelm@4276: The {\tt Seq} structure is supposed to be accessed via fully qualified
wenzelm@4317: names and should not be \texttt{open}.
lcp@104: 
lcp@323: \subsection{Basic operations on sequences}
lcp@104: \begin{ttbox} 
wenzelm@4276: Seq.empty   : 'a seq
wenzelm@4276: Seq.make    : (unit -> ('a * 'a seq) option) -> 'a seq
wenzelm@4276: Seq.single  : 'a -> 'a seq
wenzelm@4276: Seq.pull    : 'a seq -> ('a * 'a seq) option
lcp@104: \end{ttbox}
lcp@323: \begin{ttdescription}
wenzelm@4276: \item[Seq.empty] is the empty sequence.
lcp@104: 
wenzelm@4276: \item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
wenzelm@4276:   sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
lcp@104: 
wenzelm@4276: \item[Seq.single $x$] 
lcp@104: constructs the sequence containing the single element~$x$.
lcp@104: 
wenzelm@4276: \item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
wenzelm@4276:   {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
wenzelm@4276:   Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
wenzelm@4276:   the value of~$x$; it is not stored!
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@323: \subsection{Converting between sequences and lists}
lcp@104: \begin{ttbox} 
wenzelm@4276: Seq.chop    : int * 'a seq -> 'a list * 'a seq
wenzelm@4276: Seq.list_of : 'a seq -> 'a list
wenzelm@4276: Seq.of_list : 'a list -> 'a seq
lcp@104: \end{ttbox}
lcp@323: \begin{ttdescription}
wenzelm@4276: \item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
wenzelm@4276:   list, paired with the remaining elements of~$xq$.  If $xq$ has fewer
wenzelm@4276:   than~$n$ elements, then so will the list.
wenzelm@4276:   
wenzelm@4276: \item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
wenzelm@4276:   finite, as a list.
wenzelm@4276:   
wenzelm@4276: \item[Seq.of_list $xs$] creates a sequence containing the elements
wenzelm@4276:   of~$xs$.
lcp@323: \end{ttdescription}
lcp@104: 
lcp@104: 
lcp@323: \subsection{Combining sequences}
lcp@104: \begin{ttbox} 
wenzelm@4276: Seq.append      : 'a seq * 'a seq -> 'a seq
wenzelm@4276: Seq.interleave  : 'a seq * 'a seq -> 'a seq
wenzelm@4276: Seq.flat        : 'a seq seq -> 'a seq
wenzelm@4276: Seq.map         : ('a -> 'b) -> 'a seq -> 'b seq
wenzelm@4276: Seq.filter      : ('a -> bool) -> 'a seq -> 'a seq
lcp@104: \end{ttbox} 
lcp@323: \begin{ttdescription}
wenzelm@4276: \item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
wenzelm@4276:   
wenzelm@4276: \item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
wenzelm@4276:   interleaving their elements.  The result contains all the elements
wenzelm@4276:   of the sequences, even if both are infinite.
wenzelm@4276:   
wenzelm@4276: \item[Seq.flat $xqq$] concatenates a sequence of sequences.
wenzelm@4276:   
wenzelm@4276: \item[Seq.map $f$ $xq$] applies $f$ to every element
wenzelm@4276:   of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
wenzelm@4276:   
wenzelm@4276: \item[Seq.filter $p$ $xq$] returns the sequence consisting of all
wenzelm@4276:   elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
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: 




