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 require
10 the power of simplification (Chapter~\ref{chap:simplification}) and classical
11 reasoning (Chapter~\ref{chap:classical}).
13 \section{Resolution and assumption tactics}
14 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
15 a rule. {\bf Elim-resolution} is particularly suited for elimination
16 rules, while {\bf destruct-resolution} is particularly suited for
17 destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
18 maintained for several different kinds of resolution tactics, as well as
19 the shortcuts in the subgoal module.
21 All the tactics in this section act on a subgoal designated by a positive
22 integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
25 \subsection{Resolution tactics}
26 \index{resolution!tactics}
27 \index{tactics!resolution|bold}
29 resolve_tac : thm list -> int -> tactic
30 eresolve_tac : thm list -> int -> tactic
31 dresolve_tac : thm list -> int -> tactic
32 forward_tac : thm list -> int -> tactic
34 These perform resolution on a list of theorems, $thms$, representing a list
35 of object-rules. When generating next states, they take each of the rules
36 in the order given. Each rule may yield several next states, or none:
37 higher-order resolution may yield multiple resolvents.
39 \item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
40 refines the proof state using the rules, which should normally be
41 introduction rules. It resolves a rule's conclusion with
42 subgoal~$i$ of the proof state.
44 \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
45 \index{elim-resolution}
46 performs elim-resolution with the rules, which should normally be
47 elimination rules. It resolves with a rule, solves its first premise by
48 assumption, and finally {\em deletes\/} that assumption from any new
51 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
52 \index{forward proof}\index{destruct-resolution}
53 performs destruct-resolution with the rules, which normally should
54 be destruction rules. This replaces an assumption by the result of
55 applying one of the rules.
57 \item[\ttindexbold{forward_tac}]\index{forward proof}
58 is like {\tt dresolve_tac} except that the selected assumption is not
59 deleted. It applies a rule to an assumption, adding the result as a new
63 \subsection{Assumption tactics}
64 \index{tactics!assumption|bold}\index{assumptions!tactics for}
66 assume_tac : int -> tactic
67 eq_assume_tac : int -> tactic
70 \item[\ttindexbold{assume_tac} {\it i}]
71 attempts to solve subgoal~$i$ by assumption.
73 \item[\ttindexbold{eq_assume_tac}]
74 is like {\tt assume_tac} but does not use unification. It succeeds (with a
75 {\em unique\/} next state) if one of the assumptions is identical to the
76 subgoal's conclusion. Since it does not instantiate variables, it cannot
77 make other subgoals unprovable. It is intended to be called from proof
78 strategies, not interactively.
81 \subsection{Matching tactics} \label{match_tac}
82 \index{tactics!matching}
84 match_tac : thm list -> int -> tactic
85 ematch_tac : thm list -> int -> tactic
86 dmatch_tac : thm list -> int -> tactic
88 These are just like the resolution tactics except that they never
89 instantiate unknowns in the proof state. Flexible subgoals are not updated
90 willy-nilly, but are left alone. Matching --- strictly speaking --- means
91 treating the unknowns in the proof state as constants; these tactics merely
92 discard unifiers that would update the proof state.
94 \item[\ttindexbold{match_tac} {\it thms} {\it i}]
95 refines the proof state using the rules, matching a rule's
96 conclusion with subgoal~$i$ of the proof state.
98 \item[\ttindexbold{ematch_tac}]
99 is like {\tt match_tac}, but performs elim-resolution.
101 \item[\ttindexbold{dmatch_tac}]
102 is like {\tt match_tac}, but performs destruct-resolution.
106 \subsection{Resolution with instantiation} \label{res_inst_tac}
107 \index{tactics!instantiation}\index{instantiation}
109 res_inst_tac : (string*string)list -> thm -> int -> tactic
110 eres_inst_tac : (string*string)list -> thm -> int -> tactic
111 dres_inst_tac : (string*string)list -> thm -> int -> tactic
112 forw_inst_tac : (string*string)list -> thm -> int -> tactic
114 These tactics are designed for applying rules such as substitution and
115 induction, which cause difficulties for higher-order unification. The
116 tactics accept explicit instantiations for unknowns in the rule ---
117 typically, in the rule's conclusion. Each instantiation is a pair
118 {\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading
121 \item If $v$ is the type unknown {\tt'a}, then
122 the rule must contain a type unknown \verb$?'a$ of some
123 sort~$s$, and $e$ should be a type of sort $s$.
125 \item If $v$ is the unknown {\tt P}, then
126 the rule must contain an unknown \verb$?P$ of some type~$\tau$,
127 and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
128 $\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
129 instantiates any type unknowns in $\tau$, these instantiations
130 are recorded for application to the rule.
132 Types are instantiated before terms. Because type instantiations are
133 inferred from term instantiations, explicit type instantiations are seldom
134 necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
135 \verb$[("'a","bool"),("t","True")]$ may be simplified to
136 \verb$[("t","True")]$. Type unknowns in the proof state may cause
137 failure because the tactics cannot instantiate them.
139 The instantiation tactics act on a given subgoal. Terms in the
140 instantiations are type-checked in the context of that subgoal --- in
141 particular, they may refer to that subgoal's parameters. Any unknowns in
142 the terms receive subscripts and are lifted over the parameters; thus, you
143 may not refer to unknowns in the subgoal.
145 \begin{ttdescription}
146 \item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
147 instantiates the rule {\it thm} with the instantiations {\it insts}, as
148 described above, and then performs resolution on subgoal~$i$. Resolution
149 typically causes further instantiations; you need not give explicit
150 instantiations for every unknown in the rule.
152 \item[\ttindexbold{eres_inst_tac}]
153 is like {\tt res_inst_tac}, but performs elim-resolution.
155 \item[\ttindexbold{dres_inst_tac}]
156 is like {\tt res_inst_tac}, but performs destruct-resolution.
158 \item[\ttindexbold{forw_inst_tac}]
159 is like {\tt dres_inst_tac} except that the selected assumption is not
160 deleted. It applies the instantiated rule to an assumption, adding the
161 result as a new assumption.
165 \section{Other basic tactics}
166 \subsection{Tactic shortcuts}
167 \index{shortcuts!for tactics}
168 \index{tactics!resolution}\index{tactics!assumption}
169 \index{tactics!meta-rewriting}
171 rtac : thm -> int -> tactic
172 etac : thm -> int -> tactic
173 dtac : thm -> int -> tactic
175 ares_tac : thm list -> int -> tactic
176 rewtac : thm -> tactic
178 These abbreviate common uses of tactics.
179 \begin{ttdescription}
180 \item[\ttindexbold{rtac} {\it thm} {\it i}]
181 abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
183 \item[\ttindexbold{etac} {\it thm} {\it i}]
184 abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
186 \item[\ttindexbold{dtac} {\it thm} {\it i}]
187 abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
190 \item[\ttindexbold{atac} {\it i}]
191 abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
193 \item[\ttindexbold{ares_tac} {\it thms} {\it i}]
194 tries proof by assumption and resolution; it abbreviates
196 assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
199 \item[\ttindexbold{rewtac} {\it def}]
200 abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
204 \subsection{Inserting premises and facts}\label{cut_facts_tac}
205 \index{tactics!for inserting facts}\index{assumptions!inserting}
207 cut_facts_tac : thm list -> int -> tactic
208 cut_inst_tac : (string*string)list -> thm -> int -> tactic
209 subgoal_tac : string -> int -> tactic
210 subgoal_tacs : string list -> int -> tactic
212 These tactics add assumptions to a subgoal.
213 \begin{ttdescription}
214 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
215 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
216 been inserted as assumptions, they become subject to tactics such as {\tt
217 eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
218 are inserted: Isabelle cannot use assumptions that contain $\Imp$
219 or~$\Forall$. Sometimes the theorems are premises of a rule being
220 derived, returned by~{\tt goal}; instead of calling this tactic, you
221 could state the goal with an outermost meta-quantifier.
223 \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
224 instantiates the {\it thm} with the instantiations {\it insts}, as
225 described in \S\ref{res_inst_tac}. It adds the resulting theorem as a
226 new assumption to subgoal~$i$.
228 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
229 adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
230 {\it formula} as a new subgoal, $i+1$.
232 \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
233 uses {\tt subgoal_tac} to add the members of the list of {\it
234 formulae} as assumptions to subgoal~$i$.
238 \subsection{``Putting off'' a subgoal}
240 defer_tac : int -> tactic
242 \begin{ttdescription}
243 \item[\ttindexbold{defer_tac} {\it i}]
244 moves subgoal~$i$ to the last position in the proof state. It can be
245 useful when correcting a proof script: if the tactic given for subgoal~$i$
246 fails, calling {\tt defer_tac} instead will let you continue with the rest
249 The tactic fails if subgoal~$i$ does not exist or if the proof state
250 contains type unknowns.
254 \subsection{Definitions and meta-level rewriting}
255 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
258 Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
259 constant or a constant applied to a list of variables, for example $\it
260 sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$,
261 are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means using
262 it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf
263 Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until
264 no rewrites are applicable to any subterm.
266 There are rules for unfolding and folding definitions; Isabelle does not do
267 this automatically. The corresponding tactics rewrite the proof state,
268 yielding a single next state. See also the {\tt goalw} command, which is the
269 easiest way of handling definitions.
271 rewrite_goals_tac : thm list -> tactic
272 rewrite_tac : thm list -> tactic
273 fold_goals_tac : thm list -> tactic
274 fold_tac : thm list -> tactic
276 \begin{ttdescription}
277 \item[\ttindexbold{rewrite_goals_tac} {\it defs}]
278 unfolds the {\it defs} throughout the subgoals of the proof state, while
279 leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a
282 \item[\ttindexbold{rewrite_tac} {\it defs}]
283 unfolds the {\it defs} throughout the proof state, including the main goal
284 --- not normally desirable!
286 \item[\ttindexbold{fold_goals_tac} {\it defs}]
287 folds the {\it defs} throughout the subgoals of the proof state, while
288 leaving the main goal unchanged.
290 \item[\ttindexbold{fold_tac} {\it defs}]
291 folds the {\it defs} throughout the proof state.
295 \subsection{Theorems useful with tactics}
296 \index{theorems!of pure theory}
301 \begin{ttdescription}
303 is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and
304 \hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
306 assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}
310 is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
311 assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
312 and {\tt subgoal_tac}.
316 \section{Obscure tactics}
318 \subsection{Renaming parameters in a goal} \index{parameters!renaming}
320 rename_tac : string -> int -> tactic
321 rename_last_tac : string -> string list -> int -> tactic
322 Logic.set_rename_prefix : string -> unit
323 Logic.auto_rename : bool ref \hfill{\bf initially false}
325 When creating a parameter, Isabelle chooses its name by matching variable
326 names via the object-rule. Given the rule $(\forall I)$ formalized as
327 $\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
328 the $\Forall$-bound variable in the premise has the same name as the
329 $\forall$-bound variable in the conclusion.
331 Sometimes there is insufficient information and Isabelle chooses an
332 arbitrary name. The renaming tactics let you override Isabelle's choice.
333 Because renaming parameters has no logical effect on the proof state, the
334 {\tt by} command prints the message {\tt Warning:\ same as previous
337 Alternatively, you can suppress the naming mechanism described above and
338 have Isabelle generate uniform names for parameters. These names have the
339 form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
340 prefix. They are ugly but predictable.
342 \begin{ttdescription}
343 \item[\ttindexbold{rename_tac} {\it str} {\it i}]
344 interprets the string {\it str} as a series of blank-separated variable
345 names, and uses them to rename the parameters of subgoal~$i$. The names
346 must be distinct. If there are fewer names than parameters, then the
347 tactic renames the innermost parameters and may modify the remaining ones
348 to ensure that all the parameters are distinct.
350 \item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
351 generates a list of names by attaching each of the {\it suffixes\/} to the
352 {\it prefix}. It is intended for coding structural induction tactics,
353 where several of the new parameters should have related names.
355 \item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
356 sets the prefix for uniform renaming to~{\it prefix}. The default prefix
359 \item[\ttindexbold{Logic.auto_rename} := true;]
360 makes Isabelle generate uniform names for parameters.
364 \subsection{Manipulating assumptions}
365 \index{assumptions!rotating}
367 thin_tac : string -> int -> tactic
368 rotate_tac : int -> int -> tactic
370 \begin{ttdescription}
371 \item[\ttindexbold{thin_tac} {\it formula} $i$]
372 \index{assumptions!deleting}
373 deletes the specified assumption from subgoal $i$. Often the assumption
374 can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
375 assumption will be deleted. Removing useless assumptions from a subgoal
376 increases its readability and can make search tactics run faster.
378 \item[\ttindexbold{rotate_tac} $n$ $i$]
379 \index{assumptions!rotating}
380 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
381 if $n$ is positive, and from left to right if $n$ is negative. This is
382 sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which
383 processes assumptions from left to right.
387 \subsection{Tidying the proof state}
388 \index{duplicate subgoals!removing}
389 \index{parameters!removing unused}
390 \index{flex-flex constraints}
392 distinct_subgoals_tac : tactic
393 prune_params_tac : tactic
394 flexflex_tac : tactic
396 \begin{ttdescription}
397 \item[\ttindexbold{distinct_subgoals_tac}]
398 removes duplicate subgoals from a proof state. (These arise especially
399 in \ZF{}, where the subgoals are essentially type constraints.)
401 \item[\ttindexbold{prune_params_tac}]
402 removes unused parameters from all subgoals of the proof state. It works
403 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
404 make the proof state more readable. It is used with
405 \ttindex{rule_by_tactic} to simplify the resulting theorem.
407 \item[\ttindexbold{flexflex_tac}]
408 removes all flex-flex pairs from the proof state by applying the trivial
409 unifier. This drastic step loses information, and should only be done as
410 the last step of a proof.
412 Flex-flex constraints arise from difficult cases of higher-order
413 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
414 some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex
415 constraints can be ignored; they often disappear as unknowns get
420 \subsection{Composition: resolution without lifting}
421 \index{tactics!for composition}
423 compose_tac: (bool * thm * int) -> int -> tactic
425 {\bf Composing} two rules means resolving them without prior lifting or
426 renaming of unknowns. This low-level operation, which underlies the
427 resolution tactics, may occasionally be useful for special effects.
428 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
429 rule, then passes the result to {\tt compose_tac}.
430 \begin{ttdescription}
431 \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
432 refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
433 have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
434 not be atomic; thus $m$ determines the number of new subgoals. If
435 $flag$ is {\tt true} then it performs elim-resolution --- it solves the
436 first premise of~$rule$ by assumption and deletes that assumption.
440 \section{Managing lots of rules}
441 These operations are not intended for interactive use. They are concerned
442 with the processing of large numbers of rules in automatic proof
443 strategies. Higher-order resolution involving a long list of rules is
444 slow. Filtering techniques can shorten the list of rules given to
445 resolution, and can also detect whether a subgoal is too flexible,
446 with too many rules applicable.
448 \subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
449 \index{tactics!resolution}
451 biresolve_tac : (bool*thm)list -> int -> tactic
452 bimatch_tac : (bool*thm)list -> int -> tactic
453 subgoals_of_brl : bool*thm -> int
454 lessb : (bool*thm) * (bool*thm) -> bool
456 {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
457 pair, it applies resolution if the flag is~{\tt false} and
458 elim-resolution if the flag is~{\tt true}. A single tactic call handles a
459 mixture of introduction and elimination rules.
461 \begin{ttdescription}
462 \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
463 refines the proof state by resolution or elim-resolution on each rule, as
464 indicated by its flag. It affects subgoal~$i$ of the proof state.
466 \item[\ttindexbold{bimatch_tac}]
467 is like {\tt biresolve_tac}, but performs matching: unknowns in the
468 proof state are never updated (see~\S\ref{match_tac}).
470 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
471 returns the number of new subgoals that bi-resolution would yield for the
472 pair (if applied to a suitable subgoal). This is $n$ if the flag is
473 {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
474 of premises of the rule. Elim-resolution yields one fewer subgoal than
475 ordinary resolution because it solves the major premise by assumption.
477 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
478 returns the result of
480 subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
483 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
484 (flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
485 those that yield the fewest subgoals should be tried first.
488 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
489 \index{discrimination nets|bold}
490 \index{tactics!resolution}
492 net_resolve_tac : thm list -> int -> tactic
493 net_match_tac : thm list -> int -> tactic
494 net_biresolve_tac: (bool*thm) list -> int -> tactic
495 net_bimatch_tac : (bool*thm) list -> int -> tactic
496 filt_resolve_tac : thm list -> int -> int -> tactic
497 could_unify : term*term->bool
498 filter_thms : (term*term->bool) -> int*term*thm list -> thm list
500 The module {\tt Net} implements a discrimination net data structure for
501 fast selection of rules \cite[Chapter 14]{charniak80}. A term is
502 classified by the symbol list obtained by flattening it in preorder.
503 The flattening takes account of function applications, constants, and free
504 and bound variables; it identifies all unknowns and also regards
505 \index{lambda abs@$\lambda$-abstractions}
506 $\lambda$-abstractions as unknowns, since they could $\eta$-contract to
509 A discrimination net serves as a polymorphic dictionary indexed by terms.
510 The module provides various functions for inserting and removing items from
511 nets. It provides functions for returning all items whose term could match
512 or unify with a target term. The matching and unification tests are
513 overly lax (due to the identifications mentioned above) but they serve as
516 A net can store introduction rules indexed by their conclusion, and
517 elimination rules indexed by their major premise. Isabelle provides
518 several functions for `compiling' long lists of rules into fast
519 resolution tactics. When supplied with a list of theorems, these functions
520 build a discrimination net; the net is used when the tactic is applied to a
521 goal. To avoid repeatedly constructing the nets, use currying: bind the
522 resulting tactics to \ML{} identifiers.
524 \begin{ttdescription}
525 \item[\ttindexbold{net_resolve_tac} {\it thms}]
526 builds a discrimination net to obtain the effect of a similar call to {\tt
529 \item[\ttindexbold{net_match_tac} {\it thms}]
530 builds a discrimination net to obtain the effect of a similar call to {\tt
533 \item[\ttindexbold{net_biresolve_tac} {\it brls}]
534 builds a discrimination net to obtain the effect of a similar call to {\tt
537 \item[\ttindexbold{net_bimatch_tac} {\it brls}]
538 builds a discrimination net to obtain the effect of a similar call to {\tt
541 \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
542 uses discrimination nets to extract the {\it thms} that are applicable to
543 subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
544 tactic fails. Otherwise it calls {\tt resolve_tac}.
546 This tactic helps avoid runaway instantiation of unknowns, for example in
549 \item[\ttindexbold{could_unify} ({\it t},{\it u})]
550 returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
551 otherwise returns~{\tt true}. It assumes all variables are distinct,
552 reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
554 \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
555 returns the list of potentially resolvable rules (in {\it thms\/}) for the
556 subgoal {\it prem}, using the predicate {\it could\/} to compare the
557 conclusion of the subgoal with the conclusion of each rule. The resulting list
558 is no longer than {\it limit}.
562 \section{Programming tools for proof strategies}
563 Do not consider using the primitives discussed in this section unless you
564 really need to code tactics from scratch.
566 \subsection{Operations on type {\tt tactic}}
567 \index{tactics!primitives for coding} A tactic maps theorems to sequences of
568 theorems. The type constructor for sequences (lazy lists) is called
569 \mltydx{Sequence.seq}. To simplify the types of tactics and tacticals,
570 Isabelle defines a type abbreviation:
572 type tactic = thm -> thm Sequence.seq
574 The following operations provide means for coding tactics in a clean style.
576 PRIMITIVE : (thm -> thm) -> tactic
577 SUBGOAL : ((term*int) -> tactic) -> int -> tactic
579 \begin{ttdescription}
580 \item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
581 applies $f$ to the proof state and returns the result as a one-element
582 sequence. If $f$ raises an exception, then the tactic's result is the empty
585 \item[\ttindexbold{SUBGOAL} $f$ $i$]
586 extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
587 tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
588 state. The tactic body is expressed using tactics and tacticals, but may
589 peek at a particular subgoal:
591 SUBGOAL (fn (t,i) => {\it tactic-valued expression})
597 \index{tactics!tracing}
598 \index{tracing!of tactics}
603 These tactics print tracing information when they are applied to a proof
604 state. Their output may be difficult to interpret. Note that certain of
605 the searching tacticals, such as {\tt REPEAT}, have built-in tracing
607 \begin{ttdescription}
608 \item[\ttindexbold{pause_tac}]
609 prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
610 from the terminal. If this line is blank then it returns the proof state
611 unchanged; otherwise it fails (which may terminate a repetition).
613 \item[\ttindexbold{print_tac}]
614 returns the proof state unchanged, with the side effect of printing it at
620 \index{sequences (lazy lists)|bold}
621 The module {\tt Sequence} declares a type of lazy lists. It uses
622 Isabelle's type \mltydx{option} to represent the possible presence
623 (\ttindexbold{Some}) or absence (\ttindexbold{None}) of
626 datatype 'a option = None | Some of 'a;
628 For clarity, the module name {\tt Sequence} is omitted from the signature
629 specifications below; for instance, {\tt null} appears instead of {\tt
632 \subsection{Basic operations on sequences}
635 seqof : (unit -> ('a * 'a seq) option) -> 'a seq
636 single : 'a -> 'a seq
637 pull : 'a seq -> ('a * 'a seq) option
639 \begin{ttdescription}
641 is the empty sequence.
643 \item[\tt Sequence.seqof (fn()=> Some($x$,$s$))]
644 constructs the sequence with head~$x$ and tail~$s$, neither of which is
647 \item[Sequence.single $x$]
648 constructs the sequence containing the single element~$x$.
650 \item[Sequence.pull $s$]
651 returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
652 sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull
653 $s$} again will {\it recompute\/} the value of~$x$; it is not stored!
657 \subsection{Converting between sequences and lists}
659 chop : int * 'a seq -> 'a list * 'a seq
660 list_of_s : 'a seq -> 'a list
661 s_of_list : 'a list -> 'a seq
663 \begin{ttdescription}
664 \item[Sequence.chop($n$,$s$)]
665 returns the first~$n$ elements of~$s$ as a list, paired with the remaining
666 elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the
669 \item[Sequence.list_of_s $s$]
670 returns the elements of~$s$, which must be finite, as a list.
672 \item[Sequence.s_of_list $l$]
673 creates a sequence containing the elements of~$l$.
677 \subsection{Combining sequences}
679 append : 'a seq * 'a seq -> 'a seq
680 interleave : 'a seq * 'a seq -> 'a seq
681 flats : 'a seq seq -> 'a seq
682 maps : ('a -> 'b) -> 'a seq -> 'b seq
683 filters : ('a -> bool) -> 'a seq -> 'a seq
685 \begin{ttdescription}
686 \item[Sequence.append($s@1$,$s@2$)]
687 concatenates $s@1$ to $s@2$.
689 \item[Sequence.interleave($s@1$,$s@2$)]
690 joins $s@1$ with $s@2$ by interleaving their elements. The result contains
691 all the elements of the sequences, even if both are infinite.
693 \item[Sequence.flats $ss$]
694 concatenates a sequence of sequences.
696 \item[Sequence.maps $f$ $s$]
697 applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
698 $f(x@1),f(x@2),\ldots$.
700 \item[Sequence.filters $p$ $s$]
701 returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$