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 paulson@2039: subgoal_tacs : 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: