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{simp-chap}) and classical reasoning
11 (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{parameters!removing unused}
389 \index{flex-flex constraints}
391 prune_params_tac : tactic
392 flexflex_tac : tactic
394 \begin{ttdescription}
395 \item[\ttindexbold{prune_params_tac}]
396 removes unused parameters from all subgoals of the proof state. It works
397 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
398 make the proof state more readable. It is used with
399 \ttindex{rule_by_tactic} to simplify the resulting theorem.
401 \item[\ttindexbold{flexflex_tac}]
402 removes all flex-flex pairs from the proof state by applying the trivial
403 unifier. This drastic step loses information, and should only be done as
404 the last step of a proof.
406 Flex-flex constraints arise from difficult cases of higher-order
407 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
408 some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex
409 constraints can be ignored; they often disappear as unknowns get
414 \subsection{Composition: resolution without lifting}
415 \index{tactics!for composition}
417 compose_tac: (bool * thm * int) -> int -> tactic
419 {\bf Composing} two rules means resolving them without prior lifting or
420 renaming of unknowns. This low-level operation, which underlies the
421 resolution tactics, may occasionally be useful for special effects.
422 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
423 rule, then passes the result to {\tt compose_tac}.
424 \begin{ttdescription}
425 \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
426 refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
427 have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
428 not be atomic; thus $m$ determines the number of new subgoals. If
429 $flag$ is {\tt true} then it performs elim-resolution --- it solves the
430 first premise of~$rule$ by assumption and deletes that assumption.
434 \section{Managing lots of rules}
435 These operations are not intended for interactive use. They are concerned
436 with the processing of large numbers of rules in automatic proof
437 strategies. Higher-order resolution involving a long list of rules is
438 slow. Filtering techniques can shorten the list of rules given to
439 resolution, and can also detect whether a subgoal is too flexible,
440 with too many rules applicable.
442 \subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
443 \index{tactics!resolution}
445 biresolve_tac : (bool*thm)list -> int -> tactic
446 bimatch_tac : (bool*thm)list -> int -> tactic
447 subgoals_of_brl : bool*thm -> int
448 lessb : (bool*thm) * (bool*thm) -> bool
450 {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
451 pair, it applies resolution if the flag is~{\tt false} and
452 elim-resolution if the flag is~{\tt true}. A single tactic call handles a
453 mixture of introduction and elimination rules.
455 \begin{ttdescription}
456 \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
457 refines the proof state by resolution or elim-resolution on each rule, as
458 indicated by its flag. It affects subgoal~$i$ of the proof state.
460 \item[\ttindexbold{bimatch_tac}]
461 is like {\tt biresolve_tac}, but performs matching: unknowns in the
462 proof state are never updated (see~\S\ref{match_tac}).
464 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
465 returns the number of new subgoals that bi-resolution would yield for the
466 pair (if applied to a suitable subgoal). This is $n$ if the flag is
467 {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
468 of premises of the rule. Elim-resolution yields one fewer subgoal than
469 ordinary resolution because it solves the major premise by assumption.
471 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
472 returns the result of
474 subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
477 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
478 (flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
479 those that yield the fewest subgoals should be tried first.
482 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
483 \index{discrimination nets|bold}
484 \index{tactics!resolution}
486 net_resolve_tac : thm list -> int -> tactic
487 net_match_tac : thm list -> int -> tactic
488 net_biresolve_tac: (bool*thm) list -> int -> tactic
489 net_bimatch_tac : (bool*thm) list -> int -> tactic
490 filt_resolve_tac : thm list -> int -> int -> tactic
491 could_unify : term*term->bool
492 filter_thms : (term*term->bool) -> int*term*thm list -> thm list
494 The module {\tt Net} implements a discrimination net data structure for
495 fast selection of rules \cite[Chapter 14]{charniak80}. A term is
496 classified by the symbol list obtained by flattening it in preorder.
497 The flattening takes account of function applications, constants, and free
498 and bound variables; it identifies all unknowns and also regards
499 \index{lambda abs@$\lambda$-abstractions}
500 $\lambda$-abstractions as unknowns, since they could $\eta$-contract to
503 A discrimination net serves as a polymorphic dictionary indexed by terms.
504 The module provides various functions for inserting and removing items from
505 nets. It provides functions for returning all items whose term could match
506 or unify with a target term. The matching and unification tests are
507 overly lax (due to the identifications mentioned above) but they serve as
510 A net can store introduction rules indexed by their conclusion, and
511 elimination rules indexed by their major premise. Isabelle provides
512 several functions for `compiling' long lists of rules into fast
513 resolution tactics. When supplied with a list of theorems, these functions
514 build a discrimination net; the net is used when the tactic is applied to a
515 goal. To avoid repeatedly constructing the nets, use currying: bind the
516 resulting tactics to \ML{} identifiers.
518 \begin{ttdescription}
519 \item[\ttindexbold{net_resolve_tac} {\it thms}]
520 builds a discrimination net to obtain the effect of a similar call to {\tt
523 \item[\ttindexbold{net_match_tac} {\it thms}]
524 builds a discrimination net to obtain the effect of a similar call to {\tt
527 \item[\ttindexbold{net_biresolve_tac} {\it brls}]
528 builds a discrimination net to obtain the effect of a similar call to {\tt
531 \item[\ttindexbold{net_bimatch_tac} {\it brls}]
532 builds a discrimination net to obtain the effect of a similar call to {\tt
535 \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
536 uses discrimination nets to extract the {\it thms} that are applicable to
537 subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
538 tactic fails. Otherwise it calls {\tt resolve_tac}.
540 This tactic helps avoid runaway instantiation of unknowns, for example in
543 \item[\ttindexbold{could_unify} ({\it t},{\it u})]
544 returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
545 otherwise returns~{\tt true}. It assumes all variables are distinct,
546 reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
548 \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
549 returns the list of potentially resolvable rules (in {\it thms\/}) for the
550 subgoal {\it prem}, using the predicate {\it could\/} to compare the
551 conclusion of the subgoal with the conclusion of each rule. The resulting list
552 is no longer than {\it limit}.
556 \section{Programming tools for proof strategies}
557 Do not consider using the primitives discussed in this section unless you
558 really need to code tactics from scratch.
560 \subsection{Operations on type {\tt tactic}}
561 \index{tactics!primitives for coding}
562 A tactic maps theorems to theorem sequences (lazy lists). The type
563 constructor for sequences is called \mltydx{Sequence.seq}. To simplify the
564 types of tactics and tacticals, Isabelle defines a type abbreviations:
566 type tactic = thm -> thm Sequence.seq
568 The following operations provide means for coding tactics in a clean style.
570 PRIMITIVE : (thm -> thm) -> tactic
571 STATE : (thm -> tactic) -> tactic
572 SUBGOAL : ((term*int) -> tactic) -> int -> tactic
574 \begin{ttdescription}
575 \item[\ttindexbold{PRIMITIVE} $f$]
576 applies $f$ to the proof state and returns the result as a
577 one-element sequence. This packages the meta-rule~$f$ as a tactic.
579 \item[\ttindexbold{STATE} $f$]
580 applies $f$ to the proof state and then applies the resulting tactic to the
581 same state. It supports the following style, where the tactic body is
582 expressed using tactics and tacticals, but may peek at the proof state:
584 STATE (fn state => {\it tactic-valued expression})
587 \item[\ttindexbold{SUBGOAL} $f$ $i$]
588 extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
589 tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
590 state. The tactic body is expressed using tactics and tacticals, but may
591 peek at a particular subgoal:
593 SUBGOAL (fn (t,i) => {\it tactic-valued expression})
599 \index{tactics!tracing}
600 \index{tracing!of tactics}
605 These tactics print tracing information when they are applied to a proof
606 state. Their output may be difficult to interpret. Note that certain of
607 the searching tacticals, such as {\tt REPEAT}, have built-in tracing
609 \begin{ttdescription}
610 \item[\ttindexbold{pause_tac}]
611 prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
612 from the terminal. If this line is blank then it returns the proof state
613 unchanged; otherwise it fails (which may terminate a repetition).
615 \item[\ttindexbold{print_tac}]
616 returns the proof state unchanged, with the side effect of printing it at
622 \index{sequences (lazy lists)|bold}
623 The module {\tt Sequence} declares a type of lazy lists. It uses
624 Isabelle's type \mltydx{option} to represent the possible presence
625 (\ttindexbold{Some}) or absence (\ttindexbold{None}) of
628 datatype 'a option = None | Some of 'a;
630 For clarity, the module name {\tt Sequence} is omitted from the signature
631 specifications below; for instance, {\tt null} appears instead of {\tt
634 \subsection{Basic operations on sequences}
637 seqof : (unit -> ('a * 'a seq) option) -> 'a seq
638 single : 'a -> 'a seq
639 pull : 'a seq -> ('a * 'a seq) option
641 \begin{ttdescription}
643 is the empty sequence.
645 \item[\tt Sequence.seqof (fn()=> Some($x$,$s$))]
646 constructs the sequence with head~$x$ and tail~$s$, neither of which is
649 \item[Sequence.single $x$]
650 constructs the sequence containing the single element~$x$.
652 \item[Sequence.pull $s$]
653 returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
654 sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull
655 $s$} again will {\it recompute\/} the value of~$x$; it is not stored!
659 \subsection{Converting between sequences and lists}
661 chop : int * 'a seq -> 'a list * 'a seq
662 list_of_s : 'a seq -> 'a list
663 s_of_list : 'a list -> 'a seq
665 \begin{ttdescription}
666 \item[Sequence.chop($n$,$s$)]
667 returns the first~$n$ elements of~$s$ as a list, paired with the remaining
668 elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the
671 \item[Sequence.list_of_s $s$]
672 returns the elements of~$s$, which must be finite, as a list.
674 \item[Sequence.s_of_list $l$]
675 creates a sequence containing the elements of~$l$.
679 \subsection{Combining sequences}
681 append : 'a seq * 'a seq -> 'a seq
682 interleave : 'a seq * 'a seq -> 'a seq
683 flats : 'a seq seq -> 'a seq
684 maps : ('a -> 'b) -> 'a seq -> 'b seq
685 filters : ('a -> bool) -> 'a seq -> 'a seq
687 \begin{ttdescription}
688 \item[Sequence.append($s@1$,$s@2$)]
689 concatenates $s@1$ to $s@2$.
691 \item[Sequence.interleave($s@1$,$s@2$)]
692 joins $s@1$ with $s@2$ by interleaving their elements. The result contains
693 all the elements of the sequences, even if both are infinite.
695 \item[Sequence.flats $ss$]
696 concatenates a sequence of sequences.
698 \item[Sequence.maps $f$ $s$]
699 applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
700 $f(x@1),f(x@2),\ldots$.
702 \item[Sequence.filters $p$ $s$]
703 returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$