2 \chapter{Tactics} \label{tactics}
4 Tactics have type \mltydx{tactic}. They are essentially
5 functions from theorems to theorem sequences, where the theorems represent
6 states of a backward proof. Tactics seldom need to be coded from scratch,
7 as functions; instead they are expressed using basic tactics and tacticals.
9 \section{Resolution and assumption tactics}
10 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
11 a rule. {\bf Elim-resolution} is particularly suited for elimination
12 rules, while {\bf destruct-resolution} is particularly suited for
13 destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
14 maintained for several different kinds of resolution tactics, as well as
15 the shortcuts in the subgoal module.
17 All the tactics in this section act on a subgoal designated by a positive
18 integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
21 \subsection{Resolution tactics}
22 \index{resolution!tactics}
23 \index{tactics!resolution|bold}
25 resolve_tac : thm list -> int -> tactic
26 eresolve_tac : thm list -> int -> tactic
27 dresolve_tac : thm list -> int -> tactic
28 forward_tac : thm list -> int -> tactic
30 These perform resolution on a list of theorems, $thms$, representing a list
31 of object-rules. When generating next states, they take each of the rules
32 in the order given. Each rule may yield several next states, or none:
33 higher-order resolution may yield multiple resolvents.
35 \item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
36 refines the proof state using the rules, which should normally be
37 introduction rules. It resolves a rule's conclusion with
38 subgoal~$i$ of the proof state.
40 \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
41 \index{elim-resolution}
42 performs elim-resolution with the rules, which should normally be
43 elimination rules. It resolves with a rule, solves its first premise by
44 assumption, and finally {\em deletes\/} that assumption from any new
47 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
48 \index{forward proof}\index{destruct-resolution}
49 performs destruct-resolution with the rules, which normally should
50 be destruction rules. This replaces an assumption by the result of
51 applying one of the rules.
53 \item[\ttindexbold{forward_tac}]\index{forward proof}
54 is like {\tt dresolve_tac} except that the selected assumption is not
55 deleted. It applies a rule to an assumption, adding the result as a new
59 \subsection{Assumption tactics}
60 \index{tactics!assumption|bold}\index{assumptions!tactics for}
62 assume_tac : int -> tactic
63 eq_assume_tac : int -> tactic
66 \item[\ttindexbold{assume_tac} {\it i}]
67 attempts to solve subgoal~$i$ by assumption.
69 \item[\ttindexbold{eq_assume_tac}]
70 is like {\tt assume_tac} but does not use unification. It succeeds (with a
71 {\em unique\/} next state) if one of the assumptions is identical to the
72 subgoal's conclusion. Since it does not instantiate variables, it cannot
73 make other subgoals unprovable. It is intended to be called from proof
74 strategies, not interactively.
77 \subsection{Matching tactics} \label{match_tac}
78 \index{tactics!matching}
80 match_tac : thm list -> int -> tactic
81 ematch_tac : thm list -> int -> tactic
82 dmatch_tac : thm list -> int -> tactic
84 These are just like the resolution tactics except that they never
85 instantiate unknowns in the proof state. Flexible subgoals are not updated
86 willy-nilly, but are left alone. Matching --- strictly speaking --- means
87 treating the unknowns in the proof state as constants; these tactics merely
88 discard unifiers that would update the proof state.
90 \item[\ttindexbold{match_tac} {\it thms} {\it i}]
91 refines the proof state using the rules, matching a rule's
92 conclusion with subgoal~$i$ of the proof state.
94 \item[\ttindexbold{ematch_tac}]
95 is like {\tt match_tac}, but performs elim-resolution.
97 \item[\ttindexbold{dmatch_tac}]
98 is like {\tt match_tac}, but performs destruct-resolution.
102 \subsection{Resolution with instantiation} \label{res_inst_tac}
103 \index{tactics!instantiation}\index{instantiation}
105 res_inst_tac : (string*string)list -> thm -> int -> tactic
106 eres_inst_tac : (string*string)list -> thm -> int -> tactic
107 dres_inst_tac : (string*string)list -> thm -> int -> tactic
108 forw_inst_tac : (string*string)list -> thm -> int -> tactic
110 These tactics are designed for applying rules such as substitution and
111 induction, which cause difficulties for higher-order unification. The
112 tactics accept explicit instantiations for unknowns in the rule ---
113 typically, in the rule's conclusion. Each instantiation is a pair
114 {\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading
117 \item If $v$ is the type unknown {\tt'a}, then
118 the rule must contain a type unknown \verb$?'a$ of some
119 sort~$s$, and $e$ should be a type of sort $s$.
121 \item If $v$ is the unknown {\tt P}, then
122 the rule must contain an unknown \verb$?P$ of some type~$\tau$,
123 and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
124 $\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
125 instantiates any type unknowns in $\tau$, these instantiations
126 are recorded for application to the rule.
128 Types are instantiated before terms. Because type instantiations are
129 inferred from term instantiations, explicit type instantiations are seldom
130 necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
131 \verb$[("'a","bool"),("t","True")]$ may be simplified to
132 \verb$[("t","True")]$. Type unknowns in the proof state may cause
133 failure because the tactics cannot instantiate them.
135 The instantiation tactics act on a given subgoal. Terms in the
136 instantiations are type-checked in the context of that subgoal --- in
137 particular, they may refer to that subgoal's parameters. Any unknowns in
138 the terms receive subscripts and are lifted over the parameters; thus, you
139 may not refer to unknowns in the subgoal.
141 \begin{ttdescription}
142 \item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
143 instantiates the rule {\it thm} with the instantiations {\it insts}, as
144 described above, and then performs resolution on subgoal~$i$. Resolution
145 typically causes further instantiations; you need not give explicit
146 instantiations for every unknown in the rule.
148 \item[\ttindexbold{eres_inst_tac}]
149 is like {\tt res_inst_tac}, but performs elim-resolution.
151 \item[\ttindexbold{dres_inst_tac}]
152 is like {\tt res_inst_tac}, but performs destruct-resolution.
154 \item[\ttindexbold{forw_inst_tac}]
155 is like {\tt dres_inst_tac} except that the selected assumption is not
156 deleted. It applies the instantiated rule to an assumption, adding the
157 result as a new assumption.
161 \section{Other basic tactics}
162 \subsection{Definitions and meta-level rewriting}
163 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
166 Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
167 constant or a constant applied to a list of variables, for example $\it
168 sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$,
169 are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means using
170 it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf
171 Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until
172 no rewrites are applicable to any subterm.
174 There are rules for unfolding and folding definitions; Isabelle does not do
175 this automatically. The corresponding tactics rewrite the proof state,
176 yielding a single next state. See also the {\tt goalw} command, which is the
177 easiest way of handling definitions.
179 rewrite_goals_tac : thm list -> tactic
180 rewrite_tac : thm list -> tactic
181 fold_goals_tac : thm list -> tactic
182 fold_tac : thm list -> tactic
184 \begin{ttdescription}
185 \item[\ttindexbold{rewrite_goals_tac} {\it defs}]
186 unfolds the {\it defs} throughout the subgoals of the proof state, while
187 leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a
190 \item[\ttindexbold{rewrite_tac} {\it defs}]
191 unfolds the {\it defs} throughout the proof state, including the main goal
192 --- not normally desirable!
194 \item[\ttindexbold{fold_goals_tac} {\it defs}]
195 folds the {\it defs} throughout the subgoals of the proof state, while
196 leaving the main goal unchanged.
198 \item[\ttindexbold{fold_tac} {\it defs}]
199 folds the {\it defs} throughout the proof state.
203 \subsection{Tactic shortcuts}
204 \index{shortcuts!for tactics}
205 \index{tactics!resolution}\index{tactics!assumption}
206 \index{tactics!meta-rewriting}
208 rtac : thm -> int -> tactic
209 etac : thm -> int -> tactic
210 dtac : thm -> int -> tactic
212 ares_tac : thm list -> int -> tactic
213 rewtac : thm -> tactic
215 These abbreviate common uses of tactics.
216 \begin{ttdescription}
217 \item[\ttindexbold{rtac} {\it thm} {\it i}]
218 abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
220 \item[\ttindexbold{etac} {\it thm} {\it i}]
221 abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
223 \item[\ttindexbold{dtac} {\it thm} {\it i}]
224 abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
227 \item[\ttindexbold{atac} {\it i}]
228 abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
230 \item[\ttindexbold{ares_tac} {\it thms} {\it i}]
231 tries proof by assumption and resolution; it abbreviates
233 assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
236 \item[\ttindexbold{rewtac} {\it def}]
237 abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
241 \subsection{Inserting premises and facts}\label{cut_facts_tac}
242 \index{tactics!for inserting facts}\index{assumptions!inserting}
244 cut_facts_tac : thm list -> int -> tactic
245 cut_inst_tac : (string*string)list -> thm -> int -> tactic
246 subgoal_tac : string -> int -> tactic
247 subgoal_tacs : string list -> int -> tactic
249 These tactics add assumptions to a given subgoal.
250 \begin{ttdescription}
251 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
252 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
253 been inserted as assumptions, they become subject to tactics such as {\tt
254 eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
255 are inserted: Isabelle cannot use assumptions that contain $\Imp$
256 or~$\Forall$. Sometimes the theorems are premises of a rule being
257 derived, returned by~{\tt goal}; instead of calling this tactic, you
258 could state the goal with an outermost meta-quantifier.
260 \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
261 instantiates the {\it thm} with the instantiations {\it insts}, as
262 described in \S\ref{res_inst_tac}. It adds the resulting theorem as a
263 new assumption to subgoal~$i$.
265 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
266 adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
267 {\it formula} as a new subgoal, $i+1$.
269 \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
270 uses {\tt subgoal_tac} to add the members of the list of {\it
271 formulae} as assumptions to subgoal~$i$.
275 \subsection{Theorems useful with tactics}
276 \index{theorems!of pure theory}
281 \begin{ttdescription}
283 is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and
284 \hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
286 assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}
290 is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
291 assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
292 and {\tt subgoal_tac}.
296 \section{Obscure tactics}
298 \subsection{Rotating assumptions}
299 \index{assumptions!rotating}
301 rotate_tac : int -> int -> tactic
303 \begin{ttdescription}
304 \item[\ttindexbold{rotate_tac} $n$ $i$]
305 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left,
306 if $n$ is positive, and from left to right, if $n$ is negative. Sometimes
307 necessary in connection with \ttindex{asm_full_simp_tac}.
311 \subsection{Tidying the proof state}
312 \index{parameters!removing unused}
313 \index{flex-flex constraints}
315 prune_params_tac : tactic
316 flexflex_tac : tactic
318 \begin{ttdescription}
319 \item[\ttindexbold{prune_params_tac}]
320 removes unused parameters from all subgoals of the proof state. It works
321 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
322 make the proof state more readable. It is used with
323 \ttindex{rule_by_tactic} to simplify the resulting theorem.
325 \item[\ttindexbold{flexflex_tac}]
326 removes all flex-flex pairs from the proof state by applying the trivial
327 unifier. This drastic step loses information, and should only be done as
328 the last step of a proof.
330 Flex-flex constraints arise from difficult cases of higher-order
331 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
332 some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex
333 constraints can be ignored; they often disappear as unknowns get
338 \subsection{Renaming parameters in a goal} \index{parameters!renaming}
340 rename_tac : string -> int -> tactic
341 rename_last_tac : string -> string list -> int -> tactic
342 Logic.set_rename_prefix : string -> unit
343 Logic.auto_rename : bool ref \hfill{\bf initially false}
345 When creating a parameter, Isabelle chooses its name by matching variable
346 names via the object-rule. Given the rule $(\forall I)$ formalized as
347 $\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
348 the $\Forall$-bound variable in the premise has the same name as the
349 $\forall$-bound variable in the conclusion.
351 Sometimes there is insufficient information and Isabelle chooses an
352 arbitrary name. The renaming tactics let you override Isabelle's choice.
353 Because renaming parameters has no logical effect on the proof state, the
354 {\tt by} command prints the message {\tt Warning:\ same as previous
357 Alternatively, you can suppress the naming mechanism described above and
358 have Isabelle generate uniform names for parameters. These names have the
359 form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
360 prefix. They are ugly but predictable.
362 \begin{ttdescription}
363 \item[\ttindexbold{rename_tac} {\it str} {\it i}]
364 interprets the string {\it str} as a series of blank-separated variable
365 names, and uses them to rename the parameters of subgoal~$i$. The names
366 must be distinct. If there are fewer names than parameters, then the
367 tactic renames the innermost parameters and may modify the remaining ones
368 to ensure that all the parameters are distinct.
370 \item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
371 generates a list of names by attaching each of the {\it suffixes\/} to the
372 {\it prefix}. It is intended for coding structural induction tactics,
373 where several of the new parameters should have related names.
375 \item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
376 sets the prefix for uniform renaming to~{\it prefix}. The default prefix
379 \item[\ttindexbold{Logic.auto_rename} := true;]
380 makes Isabelle generate uniform names for parameters.
384 \subsection{Composition: resolution without lifting}
385 \index{tactics!for composition}
387 compose_tac: (bool * thm * int) -> int -> tactic
389 {\bf Composing} two rules means resolving them without prior lifting or
390 renaming of unknowns. This low-level operation, which underlies the
391 resolution tactics, may occasionally be useful for special effects.
392 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
393 rule, then passes the result to {\tt compose_tac}.
394 \begin{ttdescription}
395 \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
396 refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
397 have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
398 not be atomic; thus $m$ determines the number of new subgoals. If
399 $flag$ is {\tt true} then it performs elim-resolution --- it solves the
400 first premise of~$rule$ by assumption and deletes that assumption.
404 \section{Managing lots of rules}
405 These operations are not intended for interactive use. They are concerned
406 with the processing of large numbers of rules in automatic proof
407 strategies. Higher-order resolution involving a long list of rules is
408 slow. Filtering techniques can shorten the list of rules given to
409 resolution, and can also detect whether a given subgoal is too flexible,
410 with too many rules applicable.
412 \subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
413 \index{tactics!resolution}
415 biresolve_tac : (bool*thm)list -> int -> tactic
416 bimatch_tac : (bool*thm)list -> int -> tactic
417 subgoals_of_brl : bool*thm -> int
418 lessb : (bool*thm) * (bool*thm) -> bool
420 {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
421 pair, it applies resolution if the flag is~{\tt false} and
422 elim-resolution if the flag is~{\tt true}. A single tactic call handles a
423 mixture of introduction and elimination rules.
425 \begin{ttdescription}
426 \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
427 refines the proof state by resolution or elim-resolution on each rule, as
428 indicated by its flag. It affects subgoal~$i$ of the proof state.
430 \item[\ttindexbold{bimatch_tac}]
431 is like {\tt biresolve_tac}, but performs matching: unknowns in the
432 proof state are never updated (see~\S\ref{match_tac}).
434 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
435 returns the number of new subgoals that bi-resolution would yield for the
436 pair (if applied to a suitable subgoal). This is $n$ if the flag is
437 {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
438 of premises of the rule. Elim-resolution yields one fewer subgoal than
439 ordinary resolution because it solves the major premise by assumption.
441 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
442 returns the result of
444 subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
447 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
448 (flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
449 those that yield the fewest subgoals should be tried first.
452 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
453 \index{discrimination nets|bold}
454 \index{tactics!resolution}
456 net_resolve_tac : thm list -> int -> tactic
457 net_match_tac : thm list -> int -> tactic
458 net_biresolve_tac: (bool*thm) list -> int -> tactic
459 net_bimatch_tac : (bool*thm) list -> int -> tactic
460 filt_resolve_tac : thm list -> int -> int -> tactic
461 could_unify : term*term->bool
462 filter_thms : (term*term->bool) -> int*term*thm list -> thm list
464 The module {\tt Net} implements a discrimination net data structure for
465 fast selection of rules \cite[Chapter 14]{charniak80}. A term is
466 classified by the symbol list obtained by flattening it in preorder.
467 The flattening takes account of function applications, constants, and free
468 and bound variables; it identifies all unknowns and also regards
469 \index{lambda abs@$\lambda$-abstractions}
470 $\lambda$-abstractions as unknowns, since they could $\eta$-contract to
473 A discrimination net serves as a polymorphic dictionary indexed by terms.
474 The module provides various functions for inserting and removing items from
475 nets. It provides functions for returning all items whose term could match
476 or unify with a target term. The matching and unification tests are
477 overly lax (due to the identifications mentioned above) but they serve as
480 A net can store introduction rules indexed by their conclusion, and
481 elimination rules indexed by their major premise. Isabelle provides
482 several functions for `compiling' long lists of rules into fast
483 resolution tactics. When supplied with a list of theorems, these functions
484 build a discrimination net; the net is used when the tactic is applied to a
485 goal. To avoid repeatedly constructing the nets, use currying: bind the
486 resulting tactics to \ML{} identifiers.
488 \begin{ttdescription}
489 \item[\ttindexbold{net_resolve_tac} {\it thms}]
490 builds a discrimination net to obtain the effect of a similar call to {\tt
493 \item[\ttindexbold{net_match_tac} {\it thms}]
494 builds a discrimination net to obtain the effect of a similar call to {\tt
497 \item[\ttindexbold{net_biresolve_tac} {\it brls}]
498 builds a discrimination net to obtain the effect of a similar call to {\tt
501 \item[\ttindexbold{net_bimatch_tac} {\it brls}]
502 builds a discrimination net to obtain the effect of a similar call to {\tt
505 \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
506 uses discrimination nets to extract the {\it thms} that are applicable to
507 subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
508 tactic fails. Otherwise it calls {\tt resolve_tac}.
510 This tactic helps avoid runaway instantiation of unknowns, for example in
513 \item[\ttindexbold{could_unify} ({\it t},{\it u})]
514 returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
515 otherwise returns~{\tt true}. It assumes all variables are distinct,
516 reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
518 \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
519 returns the list of potentially resolvable rules (in {\it thms\/}) for the
520 subgoal {\it prem}, using the predicate {\it could\/} to compare the
521 conclusion of the subgoal with the conclusion of each rule. The resulting list
522 is no longer than {\it limit}.
526 \section{Programming tools for proof strategies}
527 Do not consider using the primitives discussed in this section unless you
528 really need to code tactics from scratch.
530 \subsection{Operations on type {\tt tactic}}
531 \index{tactics!primitives for coding}
532 A tactic maps theorems to theorem sequences (lazy lists). The type
533 constructor for sequences is called \mltydx{Sequence.seq}. To simplify the
534 types of tactics and tacticals, Isabelle defines a type of tactics:
536 datatype tactic = Tactic of thm -> thm Sequence.seq
538 {\tt Tactic} and {\tt tapply} convert between tactics and functions. The
539 other operations provide means for coding tactics in a clean style.
541 tapply : tactic * thm -> thm Sequence.seq
542 Tactic : (thm -> thm Sequence.seq) -> tactic
543 PRIMITIVE : (thm -> thm) -> tactic
544 STATE : (thm -> tactic) -> tactic
545 SUBGOAL : ((term*int) -> tactic) -> int -> tactic
547 \begin{ttdescription}
548 \item[\ttindexbold{tapply}({\it tac}, {\it thm})]
549 returns the result of applying the tactic, as a function, to {\it thm}.
551 \item[\ttindexbold{Tactic} {\it f}]
552 packages {\it f} as a tactic.
554 \item[\ttindexbold{PRIMITIVE} $f$]
555 applies $f$ to the proof state and returns the result as a
556 one-element sequence. This packages the meta-rule~$f$ as a tactic.
558 \item[\ttindexbold{STATE} $f$]
559 applies $f$ to the proof state and then applies the resulting tactic to the
560 same state. It supports the following style, where the tactic body is
561 expressed using tactics and tacticals, but may peek at the proof state:
563 STATE (fn state => {\it tactic-valued expression})
566 \item[\ttindexbold{SUBGOAL} $f$ $i$]
567 extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
568 tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
569 state. The tactic body is expressed using tactics and tacticals, but may
570 peek at a particular subgoal:
572 SUBGOAL (fn (t,i) => {\it tactic-valued expression})
578 \index{tactics!tracing}
579 \index{tracing!of tactics}
584 These tactics print tracing information when they are applied to a proof
585 state. Their output may be difficult to interpret. Note that certain of
586 the searching tacticals, such as {\tt REPEAT}, have built-in tracing
588 \begin{ttdescription}
589 \item[\ttindexbold{pause_tac}]
590 prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
591 from the terminal. If this line is blank then it returns the proof state
592 unchanged; otherwise it fails (which may terminate a repetition).
594 \item[\ttindexbold{print_tac}]
595 returns the proof state unchanged, with the side effect of printing it at
601 \index{sequences (lazy lists)|bold}
602 The module {\tt Sequence} declares a type of lazy lists. It uses
603 Isabelle's type \mltydx{option} to represent the possible presence
604 (\ttindexbold{Some}) or absence (\ttindexbold{None}) of
607 datatype 'a option = None | Some of 'a;
609 For clarity, the module name {\tt Sequence} is omitted from the signature
610 specifications below; for instance, {\tt null} appears instead of {\tt
613 \subsection{Basic operations on sequences}
616 seqof : (unit -> ('a * 'a seq) option) -> 'a seq
617 single : 'a -> 'a seq
618 pull : 'a seq -> ('a * 'a seq) option
620 \begin{ttdescription}
622 is the empty sequence.
624 \item[\tt Sequence.seqof (fn()=> Some($x$,$s$))]
625 constructs the sequence with head~$x$ and tail~$s$, neither of which is
628 \item[Sequence.single $x$]
629 constructs the sequence containing the single element~$x$.
631 \item[Sequence.pull $s$]
632 returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
633 sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull
634 $s$} again will {\it recompute\/} the value of~$x$; it is not stored!
638 \subsection{Converting between sequences and lists}
640 chop : int * 'a seq -> 'a list * 'a seq
641 list_of_s : 'a seq -> 'a list
642 s_of_list : 'a list -> 'a seq
644 \begin{ttdescription}
645 \item[Sequence.chop($n$,$s$)]
646 returns the first~$n$ elements of~$s$ as a list, paired with the remaining
647 elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the
650 \item[Sequence.list_of_s $s$]
651 returns the elements of~$s$, which must be finite, as a list.
653 \item[Sequence.s_of_list $l$]
654 creates a sequence containing the elements of~$l$.
658 \subsection{Combining sequences}
660 append : 'a seq * 'a seq -> 'a seq
661 interleave : 'a seq * 'a seq -> 'a seq
662 flats : 'a seq seq -> 'a seq
663 maps : ('a -> 'b) -> 'a seq -> 'b seq
664 filters : ('a -> bool) -> 'a seq -> 'a seq
666 \begin{ttdescription}
667 \item[Sequence.append($s@1$,$s@2$)]
668 concatenates $s@1$ to $s@2$.
670 \item[Sequence.interleave($s@1$,$s@2$)]
671 joins $s@1$ with $s@2$ by interleaving their elements. The result contains
672 all the elements of the sequences, even if both are infinite.
674 \item[Sequence.flats $ss$]
675 concatenates a sequence of sequences.
677 \item[Sequence.maps $f$ $s$]
678 applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
679 $f(x@1),f(x@2),\ldots$.
681 \item[Sequence.filters $p$ $s$]
682 returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$