2 \chapter{Tactics} \label{tactics}
5 \section{Other basic tactics}
7 \subsection{Inserting premises and facts}\label{cut_facts_tac}
8 \index{tactics!for inserting facts}\index{assumptions!inserting}
10 cut_facts_tac : thm list -> int -> tactic
11 cut_inst_tac : (string*string)list -> thm -> int -> tactic
12 subgoal_tac : string -> int -> tactic
13 subgoals_tac : string list -> int -> tactic
15 These tactics add assumptions to a subgoal.
17 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
18 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
19 been inserted as assumptions, they become subject to tactics such as {\tt
20 eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
21 are inserted: Isabelle cannot use assumptions that contain $\Imp$
22 or~$\Forall$. Sometimes the theorems are premises of a rule being
23 derived, returned by~{\tt goal}; instead of calling this tactic, you
24 could state the goal with an outermost meta-quantifier.
26 \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
27 instantiates the {\it thm} with the instantiations {\it insts}, as
28 described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a
29 new assumption to subgoal~$i$.
31 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
32 adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
33 {\it formula} as a new subgoal, $i+1$.
35 \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
36 uses {\tt subgoal_tac} to add the members of the list of {\it
37 formulae} as assumptions to subgoal~$i$.
41 \subsection{``Putting off'' a subgoal}
43 defer_tac : int -> tactic
46 \item[\ttindexbold{defer_tac} {\it i}]
47 moves subgoal~$i$ to the last position in the proof state. It can be
48 useful when correcting a proof script: if the tactic given for subgoal~$i$
49 fails, calling {\tt defer_tac} instead will let you continue with the rest
52 The tactic fails if subgoal~$i$ does not exist or if the proof state
53 contains type unknowns.
57 \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
58 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
61 Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
62 constant or a constant applied to a list of variables, for example $\it
63 sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$,
64 are also supported. {\bf Unfolding} the definition ${t\equiv u}$ means using
65 it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf
66 Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until
67 no rewrites are applicable to any subterm.
69 There are rules for unfolding and folding definitions; Isabelle does not do
70 this automatically. The corresponding tactics rewrite the proof state,
71 yielding a single next state. See also the {\tt goalw} command, which is the
72 easiest way of handling definitions.
74 rewrite_goals_tac : thm list -> tactic
75 rewrite_tac : thm list -> tactic
76 fold_goals_tac : thm list -> tactic
77 fold_tac : thm list -> tactic
80 \item[\ttindexbold{rewrite_goals_tac} {\it defs}]
81 unfolds the {\it defs} throughout the subgoals of the proof state, while
82 leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a
85 \item[\ttindexbold{rewrite_tac} {\it defs}]
86 unfolds the {\it defs} throughout the proof state, including the main goal
87 --- not normally desirable!
89 \item[\ttindexbold{fold_goals_tac} {\it defs}]
90 folds the {\it defs} throughout the subgoals of the proof state, while
91 leaving the main goal unchanged.
93 \item[\ttindexbold{fold_tac} {\it defs}]
94 folds the {\it defs} throughout the proof state.
98 These tactics only cope with definitions expressed as meta-level
99 equalities ($\equiv$). More general equivalences are handled by the
100 simplifier, provided that it is set up appropriately for your logic
101 (see Chapter~\ref{chap:simplification}).
104 \subsection{Theorems useful with tactics}
105 \index{theorems!of pure theory}
110 \begin{ttdescription}
112 is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and
113 \hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
115 assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}
119 is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
120 assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
121 and {\tt subgoal_tac}.
125 \section{Obscure tactics}
127 \subsection{Manipulating assumptions}
128 \index{assumptions!rotating}
130 thin_tac : string -> int -> tactic
131 rotate_tac : int -> int -> tactic
133 \begin{ttdescription}
134 \item[\ttindexbold{thin_tac} {\it formula} $i$]
135 \index{assumptions!deleting}
136 deletes the specified assumption from subgoal $i$. Often the assumption
137 can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
138 assumption will be deleted. Removing useless assumptions from a subgoal
139 increases its readability and can make search tactics run faster.
141 \item[\ttindexbold{rotate_tac} $n$ $i$]
142 \index{assumptions!rotating}
143 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
144 if $n$ is positive, and from left to right if $n$ is negative. This is
145 sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which
146 processes assumptions from left to right.
150 \subsection{Tidying the proof state}
151 \index{duplicate subgoals!removing}
152 \index{parameters!removing unused}
153 \index{flex-flex constraints}
155 distinct_subgoals_tac : tactic
156 prune_params_tac : tactic
157 flexflex_tac : tactic
159 \begin{ttdescription}
160 \item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
161 proof state. (These arise especially in ZF, where the subgoals are
162 essentially type constraints.)
164 \item[\ttindexbold{prune_params_tac}]
165 removes unused parameters from all subgoals of the proof state. It works
166 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
167 make the proof state more readable. It is used with
168 \ttindex{rule_by_tactic} to simplify the resulting theorem.
170 \item[\ttindexbold{flexflex_tac}]
171 removes all flex-flex pairs from the proof state by applying the trivial
172 unifier. This drastic step loses information, and should only be done as
173 the last step of a proof.
175 Flex-flex constraints arise from difficult cases of higher-order
176 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
177 some variables in a rule~({\S}\ref{res_inst_tac}). Normally flex-flex
178 constraints can be ignored; they often disappear as unknowns get
183 \subsection{Composition: resolution without lifting}
184 \index{tactics!for composition}
186 compose_tac: (bool * thm * int) -> int -> tactic
188 {\bf Composing} two rules means resolving them without prior lifting or
189 renaming of unknowns. This low-level operation, which underlies the
190 resolution tactics, may occasionally be useful for special effects.
191 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
192 rule, then passes the result to {\tt compose_tac}.
193 \begin{ttdescription}
194 \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
195 refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
196 have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
197 not be atomic; thus $m$ determines the number of new subgoals. If
198 $flag$ is {\tt true} then it performs elim-resolution --- it solves the
199 first premise of~$rule$ by assumption and deletes that assumption.
203 \section{*Managing lots of rules}
204 These operations are not intended for interactive use. They are concerned
205 with the processing of large numbers of rules in automatic proof
206 strategies. Higher-order resolution involving a long list of rules is
207 slow. Filtering techniques can shorten the list of rules given to
208 resolution, and can also detect whether a subgoal is too flexible,
209 with too many rules applicable.
211 \subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
212 \index{tactics!resolution}
214 biresolve_tac : (bool*thm)list -> int -> tactic
215 bimatch_tac : (bool*thm)list -> int -> tactic
216 subgoals_of_brl : bool*thm -> int
217 lessb : (bool*thm) * (bool*thm) -> bool
219 {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
220 pair, it applies resolution if the flag is~{\tt false} and
221 elim-resolution if the flag is~{\tt true}. A single tactic call handles a
222 mixture of introduction and elimination rules.
224 \begin{ttdescription}
225 \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
226 refines the proof state by resolution or elim-resolution on each rule, as
227 indicated by its flag. It affects subgoal~$i$ of the proof state.
229 \item[\ttindexbold{bimatch_tac}]
230 is like {\tt biresolve_tac}, but performs matching: unknowns in the
231 proof state are never updated (see~{\S}\ref{match_tac}).
233 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
234 returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
235 pair (if applied to a suitable subgoal). This is $n$ if the flag is
236 {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
237 of premises of the rule. Elim-resolution yields one fewer subgoal than
238 ordinary resolution because it solves the major premise by assumption.
240 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
241 returns the result of
243 subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
246 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
247 (flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
248 those that yield the fewest subgoals should be tried first.
251 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
252 \index{discrimination nets|bold}
253 \index{tactics!resolution}
255 net_resolve_tac : thm list -> int -> tactic
256 net_match_tac : thm list -> int -> tactic
257 net_biresolve_tac: (bool*thm) list -> int -> tactic
258 net_bimatch_tac : (bool*thm) list -> int -> tactic
259 filt_resolve_tac : thm list -> int -> int -> tactic
260 could_unify : term*term->bool
261 filter_thms : (term*term->bool) -> int*term*thm list -> thm{\ts}list
263 The module {\tt Net} implements a discrimination net data structure for
264 fast selection of rules \cite[Chapter 14]{charniak80}. A term is
265 classified by the symbol list obtained by flattening it in preorder.
266 The flattening takes account of function applications, constants, and free
267 and bound variables; it identifies all unknowns and also regards
268 \index{lambda abs@$\lambda$-abstractions}
269 $\lambda$-abstractions as unknowns, since they could $\eta$-contract to
272 A discrimination net serves as a polymorphic dictionary indexed by terms.
273 The module provides various functions for inserting and removing items from
274 nets. It provides functions for returning all items whose term could match
275 or unify with a target term. The matching and unification tests are
276 overly lax (due to the identifications mentioned above) but they serve as
279 A net can store introduction rules indexed by their conclusion, and
280 elimination rules indexed by their major premise. Isabelle provides
281 several functions for `compiling' long lists of rules into fast
282 resolution tactics. When supplied with a list of theorems, these functions
283 build a discrimination net; the net is used when the tactic is applied to a
284 goal. To avoid repeatedly constructing the nets, use currying: bind the
285 resulting tactics to \ML{} identifiers.
287 \begin{ttdescription}
288 \item[\ttindexbold{net_resolve_tac} {\it thms}]
289 builds a discrimination net to obtain the effect of a similar call to {\tt
292 \item[\ttindexbold{net_match_tac} {\it thms}]
293 builds a discrimination net to obtain the effect of a similar call to {\tt
296 \item[\ttindexbold{net_biresolve_tac} {\it brls}]
297 builds a discrimination net to obtain the effect of a similar call to {\tt
300 \item[\ttindexbold{net_bimatch_tac} {\it brls}]
301 builds a discrimination net to obtain the effect of a similar call to {\tt
304 \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
305 uses discrimination nets to extract the {\it thms} that are applicable to
306 subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
307 tactic fails. Otherwise it calls {\tt resolve_tac}.
309 This tactic helps avoid runaway instantiation of unknowns, for example in
312 \item[\ttindexbold{could_unify} ({\it t},{\it u})]
313 returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
314 otherwise returns~{\tt true}. It assumes all variables are distinct,
315 reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
317 \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
318 returns the list of potentially resolvable rules (in {\it thms\/}) for the
319 subgoal {\it prem}, using the predicate {\it could\/} to compare the
320 conclusion of the subgoal with the conclusion of each rule. The resulting list
321 is no longer than {\it limit}.
329 %%% TeX-master: "ref"