%% $Id$\chapter{Tactics} \label{tactics}\index{tactics|(} Tactics have type \mltydx{tactic}. This is just anabbreviation for functions from theorems to theorem sequences, wherethe theorems represent states of a backward proof. Tactics seldomneed to be coded from scratch, as functions; instead they areexpressed using basic tactics and tacticals.This chapter only presents the primitive tactics. Substantial proofs requirethe power of simplification (Chapter~\ref{chap:simplification}) and classicalreasoning (Chapter~\ref{chap:classical}).\section{Resolution and assumption tactics}{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal usinga rule. {\bf Elim-resolution} is particularly suited for eliminationrules, while {\bf destruct-resolution} is particularly suited fordestruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention ismaintained for several different kinds of resolution tactics, as well asthe shortcuts in the subgoal module.All the tactics in this section act on a subgoal designated by a positiveinteger~$i$. They fail (by returning the empty sequence) if~$i$ is out ofrange.\subsection{Resolution tactics}\index{resolution!tactics}\index{tactics!resolution|bold}\begin{ttbox} resolve_tac : thm list -> int -> tacticeresolve_tac : thm list -> int -> tacticdresolve_tac : thm list -> int -> tacticforward_tac : thm list -> int -> tactic \end{ttbox}These perform resolution on a list of theorems, $thms$, representing a listof object-rules. When generating next states, they take each of the rulesin the order given. Each rule may yield several next states, or none:higher-order resolution may yield multiple resolvents.\begin{ttdescription}\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] refines the proof state using the rules, which should normally be introduction rules. It resolves a rule's conclusion with subgoal~$i$ of the proof state.\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution} performs elim-resolution with the rules, which should normally be elimination rules. It resolves with a rule, solves its first premise by assumption, and finally {\em deletes\/} that assumption from any new subgoals.\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] \index{forward proof}\index{destruct-resolution} performs destruct-resolution with the rules, which normally should be destruction rules. This replaces an assumption by the result of applying one of the rules.\item[\ttindexbold{forward_tac}]\index{forward proof} is like {\tt dresolve_tac} except that the selected assumption is not deleted. It applies a rule to an assumption, adding the result as a new assumption.\end{ttdescription}\subsection{Assumption tactics}\index{tactics!assumption|bold}\index{assumptions!tactics for}\begin{ttbox} assume_tac : int -> tacticeq_assume_tac : int -> tactic\end{ttbox} \begin{ttdescription}\item[\ttindexbold{assume_tac} {\it i}] attempts to solve subgoal~$i$ by assumption.\item[\ttindexbold{eq_assume_tac}] is like {\tt assume_tac} but does not use unification. It succeeds (with a{\em unique\/} next state) if one of the assumptions is identical to thesubgoal's conclusion. Since it does not instantiate variables, it cannotmake other subgoals unprovable. It is intended to be called from proofstrategies, not interactively.\end{ttdescription}\subsection{Matching tactics} \label{match_tac}\index{tactics!matching}\begin{ttbox} match_tac : thm list -> int -> tacticematch_tac : thm list -> int -> tacticdmatch_tac : thm list -> int -> tactic\end{ttbox}These are just like the resolution tactics except that they neverinstantiate unknowns in the proof state. Flexible subgoals are not updatedwilly-nilly, but are left alone. Matching --- strictly speaking --- meanstreating the unknowns in the proof state as constants; these tactics merelydiscard unifiers that would update the proof state.\begin{ttdescription}\item[\ttindexbold{match_tac} {\it thms} {\it i}] refines the proof state using the rules, matching a rule'sconclusion with subgoal~$i$ of the proof state.\item[\ttindexbold{ematch_tac}] is like {\tt match_tac}, but performs elim-resolution.\item[\ttindexbold{dmatch_tac}] is like {\tt match_tac}, but performs destruct-resolution.\end{ttdescription}\subsection{Resolution with instantiation} \label{res_inst_tac}\index{tactics!instantiation}\index{instantiation}\begin{ttbox} res_inst_tac : (string*string)list -> thm -> int -> tacticeres_inst_tac : (string*string)list -> thm -> int -> tacticdres_inst_tac : (string*string)list -> thm -> int -> tacticforw_inst_tac : (string*string)list -> thm -> int -> tactic\end{ttbox}These tactics are designed for applying rules such as substitution andinduction, which cause difficulties for higher-order unification. Thetactics accept explicit instantiations for unknowns in the rule ---typically, in the rule's conclusion. Each instantiation is a pair{\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leadingquestion mark!\begin{itemize}\item If $v$ is the type unknown {\tt'a}, thenthe rule must contain a type unknown \verb$?'a$ of somesort~$s$, and $e$ should be a type of sort $s$.\item If $v$ is the unknown {\tt P}, thenthe rule must contain an unknown \verb$?P$ of some type~$\tau$,and $e$ should be a term of some type~$\sigma$ such that $\tau$ and$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$instantiates any type unknowns in $\tau$, these instantiationsare recorded for application to the rule.\end{itemize}Types are instantiated before terms. Because type instantiations areinferred from term instantiations, explicit type instantiations are seldomnecessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list\verb$[("'a","bool"),("t","True")]$ may be simplified to\verb$[("t","True")]$. Type unknowns in the proof state may causefailure because the tactics cannot instantiate them.The instantiation tactics act on a given subgoal. Terms in theinstantiations are type-checked in the context of that subgoal --- inparticular, they may refer to that subgoal's parameters. Any unknowns inthe terms receive subscripts and are lifted over the parameters; thus, youmay not refer to unknowns in the subgoal.\begin{ttdescription}\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]instantiates the rule {\it thm} with the instantiations {\it insts}, asdescribed above, and then performs resolution on subgoal~$i$. Resolutiontypically causes further instantiations; you need not give explicitinstantiations for every unknown in the rule.\item[\ttindexbold{eres_inst_tac}] is like {\tt res_inst_tac}, but performs elim-resolution.\item[\ttindexbold{dres_inst_tac}] is like {\tt res_inst_tac}, but performs destruct-resolution.\item[\ttindexbold{forw_inst_tac}] is like {\tt dres_inst_tac} except that the selected assumption is notdeleted. It applies the instantiated rule to an assumption, adding theresult as a new assumption.\end{ttdescription}\section{Other basic tactics}\subsection{Tactic shortcuts}\index{shortcuts!for tactics}\index{tactics!resolution}\index{tactics!assumption}\index{tactics!meta-rewriting}\begin{ttbox} rtac : thm -> int -> tacticetac : thm -> int -> tacticdtac : thm -> int -> tacticatac : int -> tacticares_tac : thm list -> int -> tacticrewtac : thm -> tactic\end{ttbox}These abbreviate common uses of tactics.\begin{ttdescription}\item[\ttindexbold{rtac} {\it thm} {\it i}] abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.\item[\ttindexbold{etac} {\it thm} {\it i}] abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.\item[\ttindexbold{dtac} {\it thm} {\it i}] abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doingdestruct-resolution.\item[\ttindexbold{atac} {\it i}] abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.\item[\ttindexbold{ares_tac} {\it thms} {\it i}] tries proof by assumption and resolution; it abbreviates\begin{ttbox}assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}\end{ttbox}\item[\ttindexbold{rewtac} {\it def}] abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.\end{ttdescription}\subsection{Inserting premises and facts}\label{cut_facts_tac}\index{tactics!for inserting facts}\index{assumptions!inserting}\begin{ttbox} cut_facts_tac : thm list -> int -> tacticcut_inst_tac : (string*string)list -> thm -> int -> tacticsubgoal_tac : string -> int -> tacticsubgoal_tacs : string list -> int -> tactic\end{ttbox}These tactics add assumptions to a subgoal.\begin{ttdescription}\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] adds the {\it thms} as new assumptions to subgoal~$i$. Once they have been inserted as assumptions, they become subject to tactics such as {\tt eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises are inserted: Isabelle cannot use assumptions that contain $\Imp$ or~$\Forall$. Sometimes the theorems are premises of a rule being derived, returned by~{\tt goal}; instead of calling this tactic, you could state the goal with an outermost meta-quantifier.\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}] instantiates the {\it thm} with the instantiations {\it insts}, as described in \S\ref{res_inst_tac}. It adds the resulting theorem as a new assumption to subgoal~$i$. \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same{\it formula} as a new subgoal, $i+1$.\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] uses {\tt subgoal_tac} to add the members of the list of {\it formulae} as assumptions to subgoal~$i$. \end{ttdescription}\subsection{``Putting off'' a subgoal}\begin{ttbox} defer_tac : int -> tactic\end{ttbox}\begin{ttdescription}\item[\ttindexbold{defer_tac} {\it i}] moves subgoal~$i$ to the last position in the proof state. It can be useful when correcting a proof script: if the tactic given for subgoal~$i$ fails, calling {\tt defer_tac} instead will let you continue with the rest of the script. The tactic fails if subgoal~$i$ does not exist or if the proof state contains type unknowns. \end{ttdescription}\subsection{Definitions and meta-level rewriting}\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}\index{definitions}Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically aconstant or a constant applied to a list of variables, for example $\itsqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$,are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means usingit as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bfFolding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues untilno rewrites are applicable to any subterm.There are rules for unfolding and folding definitions; Isabelle does not dothis automatically. The corresponding tactics rewrite the proof state,yielding a single next state. See also the {\tt goalw} command, which is theeasiest way of handling definitions.\begin{ttbox} rewrite_goals_tac : thm list -> tacticrewrite_tac : thm list -> tacticfold_goals_tac : thm list -> tacticfold_tac : thm list -> tactic\end{ttbox}\begin{ttdescription}\item[\ttindexbold{rewrite_goals_tac} {\it defs}] unfolds the {\it defs} throughout the subgoals of the proof state, whileleaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to aparticular subgoal.\item[\ttindexbold{rewrite_tac} {\it defs}] unfolds the {\it defs} throughout the proof state, including the main goal--- not normally desirable!\item[\ttindexbold{fold_goals_tac} {\it defs}] folds the {\it defs} throughout the subgoals of the proof state, whileleaving the main goal unchanged.\item[\ttindexbold{fold_tac} {\it defs}] folds the {\it defs} throughout the proof state.\end{ttdescription}\subsection{Theorems useful with tactics}\index{theorems!of pure theory}\begin{ttbox} asm_rl: thm cut_rl: thm \end{ttbox}\begin{ttdescription}\item[\tdx{asm_rl}] is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to\begin{ttbox} assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}\end{ttbox}\item[\tdx{cut_rl}] is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for insertingassumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}and {\tt subgoal_tac}.\end{ttdescription}\section{Obscure tactics}\subsection{Renaming parameters in a goal} \index{parameters!renaming}\begin{ttbox} rename_tac : string -> int -> tacticrename_last_tac : string -> string list -> int -> tacticLogic.set_rename_prefix : string -> unitLogic.auto_rename : bool ref \hfill{\bf initially false}\end{ttbox}When creating a parameter, Isabelle chooses its name by matching variablenames via the object-rule. Given the rule $(\forall I)$ formalized as$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note thatthe $\Forall$-bound variable in the premise has the same name as the$\forall$-bound variable in the conclusion. Sometimes there is insufficient information and Isabelle chooses anarbitrary name. The renaming tactics let you override Isabelle's choice.Because renaming parameters has no logical effect on the proof state, the{\tt by} command prints the message {\tt Warning:\ same as previouslevel}.Alternatively, you can suppress the naming mechanism described above andhave Isabelle generate uniform names for parameters. These names have theform $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desiredprefix. They are ugly but predictable.\begin{ttdescription}\item[\ttindexbold{rename_tac} {\it str} {\it i}] interprets the string {\it str} as a series of blank-separated variablenames, and uses them to rename the parameters of subgoal~$i$. The namesmust be distinct. If there are fewer names than parameters, then thetactic renames the innermost parameters and may modify the remaining onesto ensure that all the parameters are distinct.\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}] generates a list of names by attaching each of the {\it suffixes\/} to the {\it prefix}. It is intended for coding structural induction tactics,where several of the new parameters should have related names.\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};] sets the prefix for uniform renaming to~{\it prefix}. The default prefixis {\tt"k"}.\item[\ttindexbold{Logic.auto_rename} := true;] makes Isabelle generate uniform names for parameters. \end{ttdescription}\subsection{Manipulating assumptions}\index{assumptions!rotating}\begin{ttbox} thin_tac : string -> int -> tacticrotate_tac : int -> int -> tactic\end{ttbox}\begin{ttdescription}\item[\ttindexbold{thin_tac} {\it formula} $i$] \index{assumptions!deleting}deletes the specified assumption from subgoal $i$. Often the assumptioncan be abbreviated, replacing subformul{\ae} by unknowns; the first matchingassumption will be deleted. Removing useless assumptions from a subgoalincreases its readability and can make search tactics run faster.\item[\ttindexbold{rotate_tac} $n$ $i$] \index{assumptions!rotating}rotates the assumptions of subgoal $i$ by $n$ positions: from right to leftif $n$ is positive, and from left to right if $n$ is negative. This is sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which processes assumptions from left to right.\end{ttdescription}\subsection{Tidying the proof state}\index{duplicate subgoals!removing}\index{parameters!removing unused}\index{flex-flex constraints}\begin{ttbox} distinct_subgoals_tac : tacticprune_params_tac : tacticflexflex_tac : tactic\end{ttbox}\begin{ttdescription}\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a proof state. (These arise especially in \ZF{}, where the subgoals are essentially type constraints.)\item[\ttindexbold{prune_params_tac}] removes unused parameters from all subgoals of the proof state. It works by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can make the proof state more readable. It is used with \ttindex{rule_by_tactic} to simplify the resulting theorem.\item[\ttindexbold{flexflex_tac}] removes all flex-flex pairs from the proof state by applying the trivial unifier. This drastic step loses information, and should only be done as the last step of a proof. Flex-flex constraints arise from difficult cases of higher-order unification. To prevent this, use \ttindex{res_inst_tac} to instantiate some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex constraints can be ignored; they often disappear as unknowns get instantiated.\end{ttdescription}\subsection{Composition: resolution without lifting}\index{tactics!for composition}\begin{ttbox}compose_tac: (bool * thm * int) -> int -> tactic\end{ttbox}{\bf Composing} two rules means resolving them without prior lifting orrenaming of unknowns. This low-level operation, which underlies theresolution tactics, may occasionally be useful for special effects.A typical application is \ttindex{res_inst_tac}, which lifts and instantiates arule, then passes the result to {\tt compose_tac}.\begin{ttdescription}\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken tohave the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ neednot be atomic; thus $m$ determines the number of new subgoals. If$flag$ is {\tt true} then it performs elim-resolution --- it solves thefirst premise of~$rule$ by assumption and deletes that assumption.\end{ttdescription}\section{*Managing lots of rules}These operations are not intended for interactive use. They are concernedwith the processing of large numbers of rules in automatic proofstrategies. Higher-order resolution involving a long list of rules isslow. Filtering techniques can shorten the list of rules given toresolution, and can also detect whether a subgoal is too flexible,with too many rules applicable.\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}\index{tactics!resolution}\begin{ttbox} biresolve_tac : (bool*thm)list -> int -> tacticbimatch_tac : (bool*thm)list -> int -> tacticsubgoals_of_brl : bool*thm -> intlessb : (bool*thm) * (bool*thm) -> bool\end{ttbox}{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For eachpair, it applies resolution if the flag is~{\tt false} andelim-resolution if the flag is~{\tt true}. A single tactic call handles amixture of introduction and elimination rules.\begin{ttdescription}\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] refines the proof state by resolution or elim-resolution on each rule, asindicated by its flag. It affects subgoal~$i$ of the proof state.\item[\ttindexbold{bimatch_tac}] is like {\tt biresolve_tac}, but performs matching: unknowns in theproof state are never updated (see~\S\ref{match_tac}).\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] returns the number of new subgoals that bi-resolution would yield for thepair (if applied to a suitable subgoal). This is $n$ if the flag is{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the numberof premises of the rule. Elim-resolution yields one fewer subgoal thanordinary resolution because it solves the major premise by assumption.\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] returns the result of \begin{ttbox}subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}\end{ttbox}\end{ttdescription}Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it(flag,rule)$ pairs by the number of new subgoals they will yield. Thus,those that yield the fewest subgoals should be tried first.\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}\index{discrimination nets|bold}\index{tactics!resolution}\begin{ttbox} net_resolve_tac : thm list -> int -> tacticnet_match_tac : thm list -> int -> tacticnet_biresolve_tac: (bool*thm) list -> int -> tacticnet_bimatch_tac : (bool*thm) list -> int -> tacticfilt_resolve_tac : thm list -> int -> int -> tacticcould_unify : term*term->boolfilter_thms : (term*term->bool) -> int*term*thm list -> thm list\end{ttbox}The module {\tt Net} implements a discrimination net data structure forfast selection of rules \cite[Chapter 14]{charniak80}. A term isclassified by the symbol list obtained by flattening it in preorder.The flattening takes account of function applications, constants, and freeand bound variables; it identifies all unknowns and also regards\index{lambda abs@$\lambda$-abstractions}$\lambda$-abstractions as unknowns, since they could $\eta$-contract toanything. A discrimination net serves as a polymorphic dictionary indexed by terms.The module provides various functions for inserting and removing items fromnets. It provides functions for returning all items whose term could matchor unify with a target term. The matching and unification tests areoverly lax (due to the identifications mentioned above) but they serve asuseful filters.A net can store introduction rules indexed by their conclusion, andelimination rules indexed by their major premise. Isabelle providesseveral functions for `compiling' long lists of rules into fastresolution tactics. When supplied with a list of theorems, these functionsbuild a discrimination net; the net is used when the tactic is applied to agoal. To avoid repeatedly constructing the nets, use currying: bind theresulting tactics to \ML{} identifiers.\begin{ttdescription}\item[\ttindexbold{net_resolve_tac} {\it thms}] builds a discrimination net to obtain the effect of a similar call to {\ttresolve_tac}.\item[\ttindexbold{net_match_tac} {\it thms}] builds a discrimination net to obtain the effect of a similar call to {\ttmatch_tac}.\item[\ttindexbold{net_biresolve_tac} {\it brls}] builds a discrimination net to obtain the effect of a similar call to {\ttbiresolve_tac}.\item[\ttindexbold{net_bimatch_tac} {\it brls}] builds a discrimination net to obtain the effect of a similar call to {\ttbimatch_tac}.\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] uses discrimination nets to extract the {\it thms} that are applicable tosubgoal~$i$. If more than {\it maxr\/} theorems are applicable then thetactic fails. Otherwise it calls {\tt resolve_tac}. This tactic helps avoid runaway instantiation of unknowns, for example intype inference.\item[\ttindexbold{could_unify} ({\it t},{\it u})] returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, andotherwise returns~{\tt true}. It assumes all variables are distinct,reporting that {\tt ?a=?a} may unify with {\tt 0=1}.\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] returns the list of potentially resolvable rules (in {\it thms\/}) for thesubgoal {\it prem}, using the predicate {\it could\/} to compare theconclusion of the subgoal with the conclusion of each rule. The resulting listis no longer than {\it limit}.\end{ttdescription}\section{*Programming tools for proof strategies}Do not consider using the primitives discussed in this section unless youreally need to code tactics from scratch.\subsection{Operations on type {\tt tactic}}\index{tactics!primitives for coding} A tactic maps theorems to sequences oftheorems. The type constructor for sequences (lazy lists) is called\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,Isabelle defines a type abbreviation:\begin{ttbox} type tactic = thm -> thm Seq.seq\end{ttbox} The following operations provide means for coding tactics in a clean style.\begin{ttbox} PRIMITIVE : (thm -> thm) -> tactic SUBGOAL : ((term*int) -> tactic) -> int -> tactic\end{ttbox} \begin{ttdescription}\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that applies $f$ to the proof state and returns the result as a one-element sequence. If $f$ raises an exception, then the tactic's result is the empty sequence.\item[\ttindexbold{SUBGOAL} $f$ $i$] extracts subgoal~$i$ from the proof state as a term~$t$, and computes atactic by calling~$f(t,i)$. It applies the resulting tactic to the samestate. The tactic body is expressed using tactics and tacticals, but maypeek at a particular subgoal:\begin{ttbox} SUBGOAL (fn (t,i) => {\it tactic-valued expression})\end{ttbox} \end{ttdescription}\subsection{Tracing}\index{tactics!tracing}\index{tracing!of tactics}\begin{ttbox} pause_tac: tacticprint_tac: tactic\end{ttbox}These tactics print tracing information when they are applied to a proofstate. Their output may be difficult to interpret. Note that certain ofthe searching tacticals, such as {\tt REPEAT}, have built-in tracingoptions.\begin{ttdescription}\item[\ttindexbold{pause_tac}] prints {\footnotesize\tt** Press RETURN to continue:} and then reads a linefrom the terminal. If this line is blank then it returns the proof stateunchanged; otherwise it fails (which may terminate a repetition).\item[\ttindexbold{print_tac}] returns the proof state unchanged, with the side effect of printing it atthe terminal.\end{ttdescription}\section{*Sequences}\index{sequences (lazy lists)|bold}The module {\tt Seq} declares a type of lazy lists. It usesIsabelle's type \mltydx{option} to represent the possible presence(\ttindexbold{Some}) or absence (\ttindexbold{None}) ofa value:\begin{ttbox}datatype 'a option = None | Some of 'a;\end{ttbox}The {\tt Seq} structure is supposed to be accessed via fully qualifiednames and should not be \texttt{open}ed.\subsection{Basic operations on sequences}\begin{ttbox} Seq.empty : 'a seqSeq.make : (unit -> ('a * 'a seq) option) -> 'a seqSeq.single : 'a -> 'a seqSeq.pull : 'a seq -> ('a * 'a seq) option\end{ttbox}\begin{ttdescription}\item[Seq.empty] is the empty sequence.\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the sequence with head~$x$ and tail~$xq$, neither of which is evaluated.\item[Seq.single $x$] constructs the sequence containing the single element~$x$.\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$. Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/} the value of~$x$; it is not stored!\end{ttdescription}\subsection{Converting between sequences and lists}\begin{ttbox} Seq.chop : int * 'a seq -> 'a list * 'a seqSeq.list_of : 'a seq -> 'a listSeq.of_list : 'a list -> 'a seq\end{ttbox}\begin{ttdescription}\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a list, paired with the remaining elements of~$xq$. If $xq$ has fewer than~$n$ elements, then so will the list.\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be finite, as a list.\item[Seq.of_list $xs$] creates a sequence containing the elements of~$xs$.\end{ttdescription}\subsection{Combining sequences}\begin{ttbox} Seq.append : 'a seq * 'a seq -> 'a seqSeq.interleave : 'a seq * 'a seq -> 'a seqSeq.flat : 'a seq seq -> 'a seqSeq.map : ('a -> 'b) -> 'a seq -> 'b seqSeq.filter : ('a -> bool) -> 'a seq -> 'a seq\end{ttbox} \begin{ttdescription}\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by interleaving their elements. The result contains all the elements of the sequences, even if both are infinite.\item[Seq.flat $xqq$] concatenates a sequence of sequences.\item[Seq.map $f$ $xq$] applies $f$ to every element of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.\item[Seq.filter $p$ $xq$] returns the sequence consisting of all elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.\end{ttdescription}\index{tactics|)}