2 \chapter{Tactics} \label{tactics}
3 \index{tactics|(} Tactics have type \mltydx{tactic}. This is just an
4 abbreviation for functions from theorems to theorem sequences, where
5 the theorems represent states of a backward proof. Tactics seldom
6 need to be coded from scratch, as functions; instead they are
7 expressed using basic tactics and tacticals.
9 This chapter only presents the primitive tactics. Substantial proofs
10 require the power of automatic tools like simplification
11 (Chapter~\ref{chap:simplification}) and classical tableau reasoning
12 (Chapter~\ref{chap:classical}).
14 \section{Resolution and assumption tactics}
15 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
16 a rule. {\bf Elim-resolution} is particularly suited for elimination
17 rules, while {\bf destruct-resolution} is particularly suited for
18 destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
19 maintained for several different kinds of resolution tactics, as well as
20 the shortcuts in the subgoal module.
22 All the tactics in this section act on a subgoal designated by a positive
23 integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
26 \subsection{Resolution tactics}
27 \index{resolution!tactics}
28 \index{tactics!resolution|bold}
30 resolve_tac : thm list -> int -> tactic
31 eresolve_tac : thm list -> int -> tactic
32 dresolve_tac : thm list -> int -> tactic
33 forward_tac : thm list -> int -> tactic
35 These perform resolution on a list of theorems, $thms$, representing a list
36 of object-rules. When generating next states, they take each of the rules
37 in the order given. Each rule may yield several next states, or none:
38 higher-order resolution may yield multiple resolvents.
40 \item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
41 refines the proof state using the rules, which should normally be
42 introduction rules. It resolves a rule's conclusion with
43 subgoal~$i$ of the proof state.
45 \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
46 \index{elim-resolution}
47 performs elim-resolution with the rules, which should normally be
48 elimination rules. It resolves with a rule, proves its first premise by
49 assumption, and finally \emph{deletes} that assumption from any new
50 subgoals. (To rotate a rule's premises,
51 see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
53 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
54 \index{forward proof}\index{destruct-resolution}
55 performs destruct-resolution with the rules, which normally should
56 be destruction rules. This replaces an assumption by the result of
57 applying one of the rules.
59 \item[\ttindexbold{forward_tac}]\index{forward proof}
60 is like {\tt dresolve_tac} except that the selected assumption is not
61 deleted. It applies a rule to an assumption, adding the result as a new
65 \subsection{Assumption tactics}
66 \index{tactics!assumption|bold}\index{assumptions!tactics for}
68 assume_tac : int -> tactic
69 eq_assume_tac : int -> tactic
72 \item[\ttindexbold{assume_tac} {\it i}]
73 attempts to solve subgoal~$i$ by assumption.
75 \item[\ttindexbold{eq_assume_tac}]
76 is like {\tt assume_tac} but does not use unification. It succeeds (with a
77 \emph{unique} next state) if one of the assumptions is identical to the
78 subgoal's conclusion. Since it does not instantiate variables, it cannot
79 make other subgoals unprovable. It is intended to be called from proof
80 strategies, not interactively.
83 \subsection{Matching tactics} \label{match_tac}
84 \index{tactics!matching}
86 match_tac : thm list -> int -> tactic
87 ematch_tac : thm list -> int -> tactic
88 dmatch_tac : thm list -> int -> tactic
90 These are just like the resolution tactics except that they never
91 instantiate unknowns in the proof state. Flexible subgoals are not updated
92 willy-nilly, but are left alone. Matching --- strictly speaking --- means
93 treating the unknowns in the proof state as constants; these tactics merely
94 discard unifiers that would update the proof state.
96 \item[\ttindexbold{match_tac} {\it thms} {\it i}]
97 refines the proof state using the rules, matching a rule's
98 conclusion with subgoal~$i$ of the proof state.
100 \item[\ttindexbold{ematch_tac}]
101 is like {\tt match_tac}, but performs elim-resolution.
103 \item[\ttindexbold{dmatch_tac}]
104 is like {\tt match_tac}, but performs destruct-resolution.
108 \subsection{Resolution with instantiation} \label{res_inst_tac}
109 \index{tactics!instantiation}\index{instantiation}
111 res_inst_tac : (string*string)list -> thm -> int -> tactic
112 eres_inst_tac : (string*string)list -> thm -> int -> tactic
113 dres_inst_tac : (string*string)list -> thm -> int -> tactic
114 forw_inst_tac : (string*string)list -> thm -> int -> tactic
116 These tactics are designed for applying rules such as substitution and
117 induction, which cause difficulties for higher-order unification. The
118 tactics accept explicit instantiations for unknowns in the rule ---
119 typically, in the rule's conclusion. Each instantiation is a pair
120 {\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading
123 \item If $v$ is the type unknown {\tt'a}, then
124 the rule must contain a type unknown \verb$?'a$ of some
125 sort~$s$, and $e$ should be a type of sort $s$.
127 \item If $v$ is the unknown {\tt P}, then
128 the rule must contain an unknown \verb$?P$ of some type~$\tau$,
129 and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
130 $\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
131 instantiates any type unknowns in $\tau$, these instantiations
132 are recorded for application to the rule.
134 Types are instantiated before terms are. Because type instantiations are
135 inferred from term instantiations, explicit type instantiations are seldom
136 necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
137 \texttt{[("'a","bool"), ("t","True")]} may be simplified to
138 \texttt{[("t","True")]}. Type unknowns in the proof state may cause
139 failure because the tactics cannot instantiate them.
141 The instantiation tactics act on a given subgoal. Terms in the
142 instantiations are type-checked in the context of that subgoal --- in
143 particular, they may refer to that subgoal's parameters. Any unknowns in
144 the terms receive subscripts and are lifted over the parameters; thus, you
145 may not refer to unknowns in the subgoal.
147 \begin{ttdescription}
148 \item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
149 instantiates the rule {\it thm} with the instantiations {\it insts}, as
150 described above, and then performs resolution on subgoal~$i$. Resolution
151 typically causes further instantiations; you need not give explicit
152 instantiations for every unknown in the rule.
154 \item[\ttindexbold{eres_inst_tac}]
155 is like {\tt res_inst_tac}, but performs elim-resolution.
157 \item[\ttindexbold{dres_inst_tac}]
158 is like {\tt res_inst_tac}, but performs destruct-resolution.
160 \item[\ttindexbold{forw_inst_tac}]
161 is like {\tt dres_inst_tac} except that the selected assumption is not
162 deleted. It applies the instantiated rule to an assumption, adding the
163 result as a new assumption.
167 \section{Other basic tactics}
168 \subsection{Tactic shortcuts}
169 \index{shortcuts!for tactics}
170 \index{tactics!resolution}\index{tactics!assumption}
171 \index{tactics!meta-rewriting}
173 rtac : thm -> int -> tactic
174 etac : thm -> int -> tactic
175 dtac : thm -> int -> tactic
176 ftac : thm -> int -> tactic
178 eatac : thm -> int -> int -> tactic
179 datac : thm -> int -> int -> tactic
180 fatac : thm -> int -> int -> tactic
181 ares_tac : thm list -> int -> tactic
182 rewtac : thm -> tactic
184 These abbreviate common uses of tactics.
185 \begin{ttdescription}
186 \item[\ttindexbold{rtac} {\it thm} {\it i}]
187 abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
189 \item[\ttindexbold{etac} {\it thm} {\it i}]
190 abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
192 \item[\ttindexbold{dtac} {\it thm} {\it i}]
193 abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
196 \item[\ttindexbold{ftac} {\it thm} {\it i}]
197 abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
198 destruct-resolution without deleting the assumption.
200 \item[\ttindexbold{atac} {\it i}]
201 abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
203 \item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}]
204 performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac},
205 solving additionally {\it j}~premises of the rule {\it thm} by assumption.
207 \item[\ttindexbold{datac} {\it thm} {\it j} {\it i}]
208 performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac},
209 solving additionally {\it j}~premises of the rule {\it thm} by assumption.
211 \item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}]
212 performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac},
213 solving additionally {\it j}~premises of the rule {\it thm} by assumption.
215 \item[\ttindexbold{ares_tac} {\it thms} {\it i}]
216 tries proof by assumption and resolution; it abbreviates
218 assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
221 \item[\ttindexbold{rewtac} {\it def}]
222 abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
226 \subsection{Inserting premises and facts}\label{cut_facts_tac}
227 \index{tactics!for inserting facts}\index{assumptions!inserting}
229 cut_facts_tac : thm list -> int -> tactic
230 cut_inst_tac : (string*string)list -> thm -> int -> tactic
231 subgoal_tac : string -> int -> tactic
232 subgoals_tac : string list -> int -> tactic
234 These tactics add assumptions to a subgoal.
235 \begin{ttdescription}
236 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
237 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
238 been inserted as assumptions, they become subject to tactics such as {\tt
239 eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
240 are inserted: Isabelle cannot use assumptions that contain $\Imp$
241 or~$\Forall$. Sometimes the theorems are premises of a rule being
242 derived, returned by~{\tt goal}; instead of calling this tactic, you
243 could state the goal with an outermost meta-quantifier.
245 \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
246 instantiates the {\it thm} with the instantiations {\it insts}, as
247 described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a
248 new assumption to subgoal~$i$.
250 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
251 adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
252 {\it formula} as a new subgoal, $i+1$.
254 \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
255 uses {\tt subgoal_tac} to add the members of the list of {\it
256 formulae} as assumptions to subgoal~$i$.
260 \subsection{``Putting off'' a subgoal}
262 defer_tac : int -> tactic
264 \begin{ttdescription}
265 \item[\ttindexbold{defer_tac} {\it i}]
266 moves subgoal~$i$ to the last position in the proof state. It can be
267 useful when correcting a proof script: if the tactic given for subgoal~$i$
268 fails, calling {\tt defer_tac} instead will let you continue with the rest
271 The tactic fails if subgoal~$i$ does not exist or if the proof state
272 contains type unknowns.
276 \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
277 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
280 Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
281 constant or a constant applied to a list of variables, for example $\it
282 sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$,
283 are also supported. {\bf Unfolding} the definition ${t\equiv u}$ means using
284 it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf
285 Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until
286 no rewrites are applicable to any subterm.
288 There are rules for unfolding and folding definitions; Isabelle does not do
289 this automatically. The corresponding tactics rewrite the proof state,
290 yielding a single next state. See also the {\tt goalw} command, which is the
291 easiest way of handling definitions.
293 rewrite_goals_tac : thm list -> tactic
294 rewrite_tac : thm list -> tactic
295 fold_goals_tac : thm list -> tactic
296 fold_tac : thm list -> tactic
298 \begin{ttdescription}
299 \item[\ttindexbold{rewrite_goals_tac} {\it defs}]
300 unfolds the {\it defs} throughout the subgoals of the proof state, while
301 leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a
304 \item[\ttindexbold{rewrite_tac} {\it defs}]
305 unfolds the {\it defs} throughout the proof state, including the main goal
306 --- not normally desirable!
308 \item[\ttindexbold{fold_goals_tac} {\it defs}]
309 folds the {\it defs} throughout the subgoals of the proof state, while
310 leaving the main goal unchanged.
312 \item[\ttindexbold{fold_tac} {\it defs}]
313 folds the {\it defs} throughout the proof state.
317 These tactics only cope with definitions expressed as meta-level
318 equalities ($\equiv$). More general equivalences are handled by the
319 simplifier, provided that it is set up appropriately for your logic
320 (see Chapter~\ref{chap:simplification}).
323 \subsection{Theorems useful with tactics}
324 \index{theorems!of pure theory}
329 \begin{ttdescription}
331 is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and
332 \hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
334 assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}
338 is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
339 assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
340 and {\tt subgoal_tac}.
344 \section{Obscure tactics}
346 \subsection{Renaming parameters in a goal} \index{parameters!renaming}
348 rename_tac : string -> int -> tactic
349 rename_last_tac : string -> string list -> int -> tactic
350 Logic.set_rename_prefix : string -> unit
351 Logic.auto_rename : bool ref \hfill{\bf initially false}
353 When creating a parameter, Isabelle chooses its name by matching variable
354 names via the object-rule. Given the rule $(\forall I)$ formalized as
355 $\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
356 the $\Forall$-bound variable in the premise has the same name as the
357 $\forall$-bound variable in the conclusion.
359 Sometimes there is insufficient information and Isabelle chooses an
360 arbitrary name. The renaming tactics let you override Isabelle's choice.
361 Because renaming parameters has no logical effect on the proof state, the
362 {\tt by} command prints the message {\tt Warning:\ same as previous
365 Alternatively, you can suppress the naming mechanism described above and
366 have Isabelle generate uniform names for parameters. These names have the
367 form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
368 prefix. They are ugly but predictable.
370 \begin{ttdescription}
371 \item[\ttindexbold{rename_tac} {\it str} {\it i}]
372 interprets the string {\it str} as a series of blank-separated variable
373 names, and uses them to rename the parameters of subgoal~$i$. The names
374 must be distinct. If there are fewer names than parameters, then the
375 tactic renames the innermost parameters and may modify the remaining ones
376 to ensure that all the parameters are distinct.
378 \item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
379 generates a list of names by attaching each of the {\it suffixes\/} to the
380 {\it prefix}. It is intended for coding structural induction tactics,
381 where several of the new parameters should have related names.
383 \item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
384 sets the prefix for uniform renaming to~{\it prefix}. The default prefix
387 \item[set \ttindexbold{Logic.auto_rename};]
388 makes Isabelle generate uniform names for parameters.
392 \subsection{Manipulating assumptions}
393 \index{assumptions!rotating}
395 thin_tac : string -> int -> tactic
396 rotate_tac : int -> int -> tactic
398 \begin{ttdescription}
399 \item[\ttindexbold{thin_tac} {\it formula} $i$]
400 \index{assumptions!deleting}
401 deletes the specified assumption from subgoal $i$. Often the assumption
402 can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
403 assumption will be deleted. Removing useless assumptions from a subgoal
404 increases its readability and can make search tactics run faster.
406 \item[\ttindexbold{rotate_tac} $n$ $i$]
407 \index{assumptions!rotating}
408 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
409 if $n$ is positive, and from left to right if $n$ is negative. This is
410 sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which
411 processes assumptions from left to right.
415 \subsection{Tidying the proof state}
416 \index{duplicate subgoals!removing}
417 \index{parameters!removing unused}
418 \index{flex-flex constraints}
420 distinct_subgoals_tac : tactic
421 prune_params_tac : tactic
422 flexflex_tac : tactic
424 \begin{ttdescription}
425 \item[\ttindexbold{distinct_subgoals_tac}]
426 removes duplicate subgoals from a proof state. (These arise especially
427 in \ZF{}, where the subgoals are essentially type constraints.)
429 \item[\ttindexbold{prune_params_tac}]
430 removes unused parameters from all subgoals of the proof state. It works
431 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
432 make the proof state more readable. It is used with
433 \ttindex{rule_by_tactic} to simplify the resulting theorem.
435 \item[\ttindexbold{flexflex_tac}]
436 removes all flex-flex pairs from the proof state by applying the trivial
437 unifier. This drastic step loses information, and should only be done as
438 the last step of a proof.
440 Flex-flex constraints arise from difficult cases of higher-order
441 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
442 some variables in a rule~({\S}\ref{res_inst_tac}). Normally flex-flex
443 constraints can be ignored; they often disappear as unknowns get
448 \subsection{Composition: resolution without lifting}
449 \index{tactics!for composition}
451 compose_tac: (bool * thm * int) -> int -> tactic
453 {\bf Composing} two rules means resolving them without prior lifting or
454 renaming of unknowns. This low-level operation, which underlies the
455 resolution tactics, may occasionally be useful for special effects.
456 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
457 rule, then passes the result to {\tt compose_tac}.
458 \begin{ttdescription}
459 \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
460 refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
461 have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
462 not be atomic; thus $m$ determines the number of new subgoals. If
463 $flag$ is {\tt true} then it performs elim-resolution --- it solves the
464 first premise of~$rule$ by assumption and deletes that assumption.
468 \section{*Managing lots of rules}
469 These operations are not intended for interactive use. They are concerned
470 with the processing of large numbers of rules in automatic proof
471 strategies. Higher-order resolution involving a long list of rules is
472 slow. Filtering techniques can shorten the list of rules given to
473 resolution, and can also detect whether a subgoal is too flexible,
474 with too many rules applicable.
476 \subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
477 \index{tactics!resolution}
479 biresolve_tac : (bool*thm)list -> int -> tactic
480 bimatch_tac : (bool*thm)list -> int -> tactic
481 subgoals_of_brl : bool*thm -> int
482 lessb : (bool*thm) * (bool*thm) -> bool
484 {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
485 pair, it applies resolution if the flag is~{\tt false} and
486 elim-resolution if the flag is~{\tt true}. A single tactic call handles a
487 mixture of introduction and elimination rules.
489 \begin{ttdescription}
490 \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
491 refines the proof state by resolution or elim-resolution on each rule, as
492 indicated by its flag. It affects subgoal~$i$ of the proof state.
494 \item[\ttindexbold{bimatch_tac}]
495 is like {\tt biresolve_tac}, but performs matching: unknowns in the
496 proof state are never updated (see~{\S}\ref{match_tac}).
498 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
499 returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
500 pair (if applied to a suitable subgoal). This is $n$ if the flag is
501 {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
502 of premises of the rule. Elim-resolution yields one fewer subgoal than
503 ordinary resolution because it solves the major premise by assumption.
505 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
506 returns the result of
508 subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
511 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
512 (flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
513 those that yield the fewest subgoals should be tried first.
516 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
517 \index{discrimination nets|bold}
518 \index{tactics!resolution}
520 net_resolve_tac : thm list -> int -> tactic
521 net_match_tac : thm list -> int -> tactic
522 net_biresolve_tac: (bool*thm) list -> int -> tactic
523 net_bimatch_tac : (bool*thm) list -> int -> tactic
524 filt_resolve_tac : thm list -> int -> int -> tactic
525 could_unify : term*term->bool
526 filter_thms : (term*term->bool) -> int*term*thm list -> thm{\ts}list
528 The module {\tt Net} implements a discrimination net data structure for
529 fast selection of rules \cite[Chapter 14]{charniak80}. A term is
530 classified by the symbol list obtained by flattening it in preorder.
531 The flattening takes account of function applications, constants, and free
532 and bound variables; it identifies all unknowns and also regards
533 \index{lambda abs@$\lambda$-abstractions}
534 $\lambda$-abstractions as unknowns, since they could $\eta$-contract to
537 A discrimination net serves as a polymorphic dictionary indexed by terms.
538 The module provides various functions for inserting and removing items from
539 nets. It provides functions for returning all items whose term could match
540 or unify with a target term. The matching and unification tests are
541 overly lax (due to the identifications mentioned above) but they serve as
544 A net can store introduction rules indexed by their conclusion, and
545 elimination rules indexed by their major premise. Isabelle provides
546 several functions for `compiling' long lists of rules into fast
547 resolution tactics. When supplied with a list of theorems, these functions
548 build a discrimination net; the net is used when the tactic is applied to a
549 goal. To avoid repeatedly constructing the nets, use currying: bind the
550 resulting tactics to \ML{} identifiers.
552 \begin{ttdescription}
553 \item[\ttindexbold{net_resolve_tac} {\it thms}]
554 builds a discrimination net to obtain the effect of a similar call to {\tt
557 \item[\ttindexbold{net_match_tac} {\it thms}]
558 builds a discrimination net to obtain the effect of a similar call to {\tt
561 \item[\ttindexbold{net_biresolve_tac} {\it brls}]
562 builds a discrimination net to obtain the effect of a similar call to {\tt
565 \item[\ttindexbold{net_bimatch_tac} {\it brls}]
566 builds a discrimination net to obtain the effect of a similar call to {\tt
569 \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
570 uses discrimination nets to extract the {\it thms} that are applicable to
571 subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
572 tactic fails. Otherwise it calls {\tt resolve_tac}.
574 This tactic helps avoid runaway instantiation of unknowns, for example in
577 \item[\ttindexbold{could_unify} ({\it t},{\it u})]
578 returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
579 otherwise returns~{\tt true}. It assumes all variables are distinct,
580 reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
582 \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
583 returns the list of potentially resolvable rules (in {\it thms\/}) for the
584 subgoal {\it prem}, using the predicate {\it could\/} to compare the
585 conclusion of the subgoal with the conclusion of each rule. The resulting list
586 is no longer than {\it limit}.
590 \section{Programming tools for proof strategies}
591 Do not consider using the primitives discussed in this section unless you
592 really need to code tactics from scratch.
594 \subsection{Operations on tactics}
595 \index{tactics!primitives for coding} A tactic maps theorems to sequences of
596 theorems. The type constructor for sequences (lazy lists) is called
597 \mltydx{Seq.seq}. To simplify the types of tactics and tacticals,
598 Isabelle defines a type abbreviation:
600 type tactic = thm -> thm Seq.seq
602 The following operations provide means for coding tactics in a clean style.
604 PRIMITIVE : (thm -> thm) -> tactic
605 SUBGOAL : ((term*int) -> tactic) -> int -> tactic
607 \begin{ttdescription}
608 \item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
609 applies $f$ to the proof state and returns the result as a one-element
610 sequence. If $f$ raises an exception, then the tactic's result is the empty
613 \item[\ttindexbold{SUBGOAL} $f$ $i$]
614 extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
615 tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
616 state. The tactic body is expressed using tactics and tacticals, but may
617 peek at a particular subgoal:
619 SUBGOAL (fn (t,i) => {\it tactic-valued expression})
625 \index{tactics!tracing}
626 \index{tracing!of tactics}
631 These tactics print tracing information when they are applied to a proof
632 state. Their output may be difficult to interpret. Note that certain of
633 the searching tacticals, such as {\tt REPEAT}, have built-in tracing
635 \begin{ttdescription}
636 \item[\ttindexbold{pause_tac}]
637 prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
638 from the terminal. If this line is blank then it returns the proof state
639 unchanged; otherwise it fails (which may terminate a repetition).
641 \item[\ttindexbold{print_tac}]
642 returns the proof state unchanged, with the side effect of printing it at
648 \index{sequences (lazy lists)|bold}
649 The module {\tt Seq} declares a type of lazy lists. It uses
650 Isabelle's type \mltydx{option} to represent the possible presence
651 (\ttindexbold{Some}) or absence (\ttindexbold{None}) of
654 datatype 'a option = None | Some of 'a;
656 The {\tt Seq} structure is supposed to be accessed via fully qualified
657 names and should not be \texttt{open}.
659 \subsection{Basic operations on sequences}
662 Seq.make : (unit -> ('a * 'a seq) option) -> 'a seq
663 Seq.single : 'a -> 'a seq
664 Seq.pull : 'a seq -> ('a * 'a seq) option
666 \begin{ttdescription}
667 \item[Seq.empty] is the empty sequence.
669 \item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
670 sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
672 \item[Seq.single $x$]
673 constructs the sequence containing the single element~$x$.
675 \item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
676 {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
677 Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
678 the value of~$x$; it is not stored!
682 \subsection{Converting between sequences and lists}
684 Seq.chop : int * 'a seq -> 'a list * 'a seq
685 Seq.list_of : 'a seq -> 'a list
686 Seq.of_list : 'a list -> 'a seq
688 \begin{ttdescription}
689 \item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
690 list, paired with the remaining elements of~$xq$. If $xq$ has fewer
691 than~$n$ elements, then so will the list.
693 \item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
696 \item[Seq.of_list $xs$] creates a sequence containing the elements
701 \subsection{Combining sequences}
703 Seq.append : 'a seq * 'a seq -> 'a seq
704 Seq.interleave : 'a seq * 'a seq -> 'a seq
705 Seq.flat : 'a seq seq -> 'a seq
706 Seq.map : ('a -> 'b) -> 'a seq -> 'b seq
707 Seq.filter : ('a -> bool) -> 'a seq -> 'a seq
709 \begin{ttdescription}
710 \item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
712 \item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
713 interleaving their elements. The result contains all the elements
714 of the sequences, even if both are infinite.
716 \item[Seq.flat $xqq$] concatenates a sequence of sequences.
718 \item[Seq.map $f$ $xq$] applies $f$ to every element
719 of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
721 \item[Seq.filter $p$ $xq$] returns the sequence consisting of all
722 elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
730 %%% TeX-master: "ref"