104

1 
%% $Id$


2 
\chapter{Tactics} \label{tactics}


3 
\index{tactics(}


4 
Tactics have type \ttindexbold{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; the basic tactics suffice for most proofs.


8 


9 
\section{Resolution and assumption tactics}


10 
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using


11 
a rule. {\bf Elimresolution} is particularly suited for elimination


12 
rules, while {\bf destructresolution} 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.


16 


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


19 
range.


20 


21 
\subsection{Resolution tactics}


22 
\index{tactics!resolutionbold}


23 
\begin{ttbox}


24 
resolve_tac : thm list > int > tactic


25 
eresolve_tac : thm list > int > tactic


26 
dresolve_tac : thm list > int > tactic


27 
forward_tac : thm list > int > tactic


28 
\end{ttbox}


29 
These perform resolution on a list of theorems, $thms$, representing a list


30 
of objectrules. When generating next states, they take each of the rules


31 
in the order given. Each rule may yield several next states, or none:


32 
higherorder resolution may yield multiple resolvents.


33 
\begin{description}


34 
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]


35 
refines the proof state using the objectrules, which should normally be


36 
introduction rules. It resolves an objectrule's conclusion with


37 
subgoal~$i$ of the proof state.


38 


39 
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]


40 
refines the proof state by elimresolution with the objectrules, which


41 
should normally be elimination rules. It resolves with a rule, solves


42 
its first premise by assumption, and finally {\bf deletes} that assumption


43 
from any new subgoals.


44 


45 
\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]


46 
performs destructresolution with the objectrules, which normally should


47 
be destruction rules. This replaces an assumption by the result of


48 
applying one of the rules.


49 


50 
\item[\ttindexbold{forward_tac}]


51 
is like \ttindex{dresolve_tac} except that the selected assumption is not


52 
deleted. It applies a rule to an assumption, adding the result as a new


53 
assumption.


54 
\end{description}


55 


56 
\subsection{Assumption tactics}


57 
\index{tactics!assumptionbold}


58 
\begin{ttbox}


59 
assume_tac : int > tactic


60 
eq_assume_tac : int > tactic


61 
\end{ttbox}


62 
\begin{description}


63 
\item[\ttindexbold{assume_tac} {\it i}]


64 
attempts to solve subgoal~$i$ by assumption.


65 


66 
\item[\ttindexbold{eq_assume_tac}]


67 
is like {\tt assume_tac} but does not use unification. It succeeds (with a


68 
{\bf unique} next state) if one of the assumptions is identical to the


69 
subgoal's conclusion. Since it does not instantiate variables, it cannot


70 
make other subgoals unprovable. It is intended to be called from proof


71 
strategies, not interactively.


72 
\end{description}


73 


74 
\subsection{Matching tactics} \label{match_tac}


75 
\index{tactics!matchingbold}


76 
\begin{ttbox}


77 
match_tac : thm list > int > tactic


78 
ematch_tac : thm list > int > tactic


79 
dmatch_tac : thm list > int > tactic


80 
\end{ttbox}


81 
These are just like the resolution tactics except that they never


82 
instantiate unknowns in the proof state. Flexible subgoals are not updated


83 
willynilly, but are left alone. Matching  strictly speaking  means


84 
treating the unknowns in the proof state as constants; these tactics merely


85 
discard unifiers that would update the proof state.


86 
\begin{description}


87 
\item[\ttindexbold{match_tac} {\it thms} {\it i}]


88 
refines the proof state using the objectrules, matching an objectrule's


89 
conclusion with subgoal~$i$ of the proof state.


90 


91 
\item[\ttindexbold{ematch_tac}]


92 
is like {\tt match_tac}, but performs elimresolution.


93 


94 
\item[\ttindexbold{dmatch_tac}]


95 
is like {\tt match_tac}, but performs destructresolution.


96 
\end{description}


97 


98 


99 
\subsection{Resolution with instantiation} \label{res_inst_tac}


100 
\index{tactics!instantiationbold}


101 
\begin{ttbox}


102 
res_inst_tac : (string*string)list > thm > int > tactic


103 
eres_inst_tac : (string*string)list > thm > int > tactic


104 
dres_inst_tac : (string*string)list > thm > int > tactic


105 
forw_inst_tac : (string*string)list > thm > int > tactic


106 
\end{ttbox}


107 
These tactics are designed for applying rules such as substitution and


108 
induction, which cause difficulties for higherorder unification. The


109 
tactics accept explicit instantiations for schematic variables in the rule


110 
 typically, in the rule's conclusion. Each instantiation is a pair


111 
{\tt($v$,$e$)}, where $v$ can be a type variable or ordinary variable:


112 
\begin{itemize}


113 
\item If $v$ is the {\bf type variable} {\tt'a}, then


114 
the rule must contain a schematic type variable \verb$?'a$ of some


115 
sort~$s$, and $e$ should be a type of sort $s$.


116 


117 
\item If $v$ is the {\bf variable} {\tt P}, then


118 
the rule must contain a schematic variable \verb$?P$ of some type~$\tau$,


119 
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and


120 
$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$


121 
instantiates any schematic type variables in $\tau$, these instantiations


122 
are recorded for application to the rule.


123 
\end{itemize}


124 
Types are instantiated before terms. Because type instantiations are


125 
inferred from term instantiations, explicit type instantiations are seldom


126 
necessary  if \verb$?t$ has type \verb$?'a$, then the instantiation list


127 
\verb$[("'a","bool"),("t","True")]$ may be simplified to


128 
\verb$[("t","True")]$. Type unknowns in the proof state may cause


129 
failure because the tactics cannot instantiate them.


130 


131 
The instantiation tactics act on a given subgoal. Terms in the


132 
instantiations are typechecked in the context of that subgoal  in


133 
particular, they may refer to that subgoal's parameters. Any unknowns in


134 
the terms receive subscripts and are lifted over the parameters; thus, you


135 
may not refer to unknowns in the subgoal.


136 


137 
\begin{description}


138 
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]


139 
instantiates the rule {\it thm} with the instantiations {\it insts}, as


140 
described above, and then performs resolution on subgoal~$i$. Resolution


141 
typically causes further instantiations; you need not give explicit


142 
instantiations for every variable in the rule.


143 


144 
\item[\ttindexbold{eres_inst_tac}]


145 
is like {\tt res_inst_tac}, but performs elimresolution.


146 


147 
\item[\ttindexbold{dres_inst_tac}]


148 
is like {\tt res_inst_tac}, but performs destructresolution.


149 


150 
\item[\ttindexbold{forw_inst_tac}]


151 
is like {\tt dres_inst_tac} except that the selected assumption is not


152 
deleted. It applies the instantiated rule to an assumption, adding the


153 
result as a new assumption.


154 
\end{description}


155 


156 


157 
\section{Other basic tactics}


158 
\subsection{Definitions and metalevel rewriting}


159 
\index{tactics!metarewritingbold}\index{rewriting!metalevel}


160 
Definitions in Isabelle have the form $t\equiv u$, where typically $t$ is a


161 
constant or a constant applied to a list of variables, for example $\it


162 
sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$,


163 
are not supported.) {\bf Unfolding} the definition $t\equiv u$ means using


164 
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf


165 
Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until


166 
no rewrites are applicable to any subterm.


167 


168 
There are rules for unfolding and folding definitions; Isabelle does not do


169 
this automatically. The corresponding tactics rewrite the proof state,


170 
yielding a unique result. See also the {\tt goalw} command, which is the


171 
easiest way of handling definitions.


172 
\begin{ttbox}


173 
rewrite_goals_tac : thm list > tactic


174 
rewrite_tac : thm list > tactic


175 
fold_goals_tac : thm list > tactic


176 
fold_tac : thm list > tactic


177 
\end{ttbox}


178 
\begin{description}


179 
\item[\ttindexbold{rewrite_goals_tac} {\it defs}]


180 
unfolds the {\it defs} throughout the subgoals of the proof state, while


181 
leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a


182 
particular subgoal.


183 


184 
\item[\ttindexbold{rewrite_tac} {\it defs}]


185 
unfolds the {\it defs} throughout the proof state, including the main goal


186 
 not normally desirable!


187 


188 
\item[\ttindexbold{fold_goals_tac} {\it defs}]


189 
folds the {\it defs} throughout the subgoals of the proof state, while


190 
leaving the main goal unchanged.


191 


192 
\item[\ttindexbold{fold_tac} {\it defs}]


193 
folds the {\it defs} throughout the proof state.


194 
\end{description}


195 


196 


197 
\subsection{Tactic shortcuts}


198 
\index{shortcuts!for tacticsbold}


199 
\index{tactics!resolution}\index{tactics!assumption}


200 
\index{tactics!metarewriting}


201 
\begin{ttbox}


202 
rtac : thm > int >tactic


203 
etac : thm > int >tactic


204 
dtac : thm > int >tactic


205 
atac : int >tactic


206 
ares_tac : thm list > int > tactic


207 
rewtac : thm > tactic


208 
\end{ttbox}


209 
These abbreviate common uses of tactics.


210 
\begin{description}


211 
\item[\ttindexbold{rtac} {\it thm} {\it i}]


212 
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.


213 


214 
\item[\ttindexbold{etac} {\it thm} {\it i}]


215 
abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elimresolution.


216 


217 
\item[\ttindexbold{dtac} {\it thm} {\it i}]


218 
abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing


219 
destructresolution.


220 


221 
\item[\ttindexbold{atac} {\it i}]


222 
is a synonym for \hbox{\tt assume_tac {\it i}}, doing proof by assumption.


223 


224 
\item[\ttindexbold{ares_tac} {\it thms} {\it i}]


225 
tries proof by assumption and resolution; it abbreviates


226 
\begin{ttbox}


227 
assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}


228 
\end{ttbox}


229 


230 
\item[\ttindexbold{rewtac} {\it def}]


231 
abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.


232 
\end{description}


233 


234 


235 
\subsection{Inserting premises and facts}\label{cut_facts_tac}


236 
\index{tactics!for inserting factsbold}


237 
\begin{ttbox}


238 
cut_facts_tac : thm list > int > tactic

286

239 
cut_inst_tac : (string*string)list > thm > int > tactic


240 
subgoal_tac : string > int > tactic

104

241 
\end{ttbox}


242 
These tactics add assumptions  which must be proved, sooner or later 


243 
to a given subgoal.


244 
\begin{description}


245 
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]


246 
adds the {\it thms} as new assumptions to subgoal~$i$. Once they have

286

247 
been inserted as assumptions, they become subject to tactics such as {\tt


248 
eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises


249 
are inserted: Isabelle cannot use assumptions that contain $\Imp$


250 
or~$\Forall$. Sometimes the theorems are premises of a rule being


251 
derived, returned by~{\tt goal}; instead of calling this tactic, you


252 
could state the goal with an outermost metaquantifier.


253 


254 
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]


255 
instantiates the {\it thm} with the instantiations {\it insts}, as


256 
described in \S\ref{res_inst_tac}. It adds the resulting theorem as a


257 
new assumption to subgoal~$i$.

104

258 


259 
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]


260 
adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same


261 
{\it formula} as a new subgoal, $i+1$.


262 
\end{description}


263 


264 


265 
\subsection{Theorems useful with tactics}


266 
\index{theorems!of pure theorybold}


267 
\begin{ttbox}


268 
asm_rl: thm


269 
cut_rl: thm


270 
\end{ttbox}


271 
\begin{description}


272 
\item[\ttindexbold{asm_rl}]


273 
is $\psi\Imp\psi$. Under elimresolution it does proof by assumption, and


274 
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to


275 
\begin{ttbox}


276 
assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}


277 
\end{ttbox}


278 


279 
\item[\ttindexbold{cut_rl}]


280 
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting


281 
assumptions; it underlies \ttindex{forward_tac}, \ttindex{cut_facts_tac}


282 
and \ttindex{subgoal_tac}.


283 
\end{description}


284 


285 


286 
\section{Obscure tactics}


287 
\subsection{Tidying the proof state}


288 
\index{parameters!removing unusedbold}


289 
\index{flexflex constraints}


290 
\begin{ttbox}


291 
prune_params_tac : tactic


292 
flexflex_tac : tactic


293 
\end{ttbox}


294 
\begin{description}


295 
\item[\ttindexbold{prune_params_tac}]


296 
removes unused parameters from all subgoals of the proof state. It works


297 
by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can


298 
make the proof state more readable. It is used with


299 
\ttindex{rule_by_tactic} to simplify the resulting theorem.


300 


301 
\item[\ttindexbold{flexflex_tac}]


302 
removes all flexflex pairs from the proof state by applying the trivial


303 
unifier. This drastic step loses information, and should only be done as


304 
the last step of a proof.


305 


306 
Flexflex constraints arise from difficult cases of higherorder


307 
unification. To prevent this, use \ttindex{res_inst_tac} to instantiate


308 
some variables in a rule~(\S\ref{res_inst_tac}). Normally flexflex


309 
constraints can be ignored; they often disappear as unknowns get


310 
instantiated.


311 
\end{description}


312 


313 


314 
\subsection{Renaming parameters in a goal} \index{parameters!renamingbold}


315 
\begin{ttbox}


316 
rename_tac : string > int > tactic


317 
rename_last_tac : string > string list > int > tactic


318 
Logic.set_rename_prefix : string > unit


319 
Logic.auto_rename : bool ref \hfill{\bf initially false}


320 
\end{ttbox}


321 
When creating a parameter, Isabelle chooses its name by matching variable


322 
names via the objectrule. Given the rule $(\forall I)$ formalized as


323 
$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that


324 
the $\Forall$bound variable in the premise has the same name as the


325 
$\forall$bound variable in the conclusion.


326 


327 
Sometimes there is insufficient information and Isabelle chooses an


328 
arbitrary name. The renaming tactics let you override Isabelle's choice.


329 
Because renaming parameters has no logical effect on the proof state, the


330 
{\tt by} command prints the needless message {\tt Warning:\ same as previous


331 
level}.


332 


333 
Alternatively, you can suppress the naming mechanism described above and


334 
have Isabelle generate uniform names for parameters. These names have the


335 
form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired


336 
prefix. They are ugly but predictable.


337 


338 
\begin{description}


339 
\item[\ttindexbold{rename_tac} {\it str} {\it i}]


340 
interprets the string {\it str} as a series of blankseparated variable


341 
names, and uses them to rename the parameters of subgoal~$i$. The names


342 
must be distinct. If there are fewer names than parameters, then the


343 
tactic renames the innermost parameters and may modify the remaining ones


344 
to ensure that all the parameters are distinct.


345 


346 
\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]


347 
generates a list of names by attaching each of the {\it suffixes\/} to the


348 
{\it prefix}. It is intended for coding structural induction tactics,


349 
where several of the new parameters should have related names.


350 


351 
\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]


352 
sets the prefix for uniform renaming to~{\it prefix}. The default prefix


353 
is {\tt"k"}.


354 


355 
\item[\ttindexbold{Logic.auto_rename} \tt:= true;]


356 
makes Isabelle generate uniform names for parameters.


357 
\end{description}


358 


359 


360 
\subsection{Composition: resolution without lifting}


361 
\index{tactics!for compositionbold}


362 
\begin{ttbox}


363 
compose_tac: (bool * thm * int) > int > tactic


364 
\end{ttbox}


365 
{\bf Composing} two rules means to resolve them without prior lifting or


366 
renaming of unknowns. This lowlevel operation, which underlies the


367 
resolution tactics, may occasionally be useful for special effects.


368 
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a


369 
rule, then passes the result to {\tt compose_tac}.


370 
\begin{description}


371 
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]


372 
refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to


373 
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need


374 
{\bf not} be atomic; thus $m$ determines the number of new subgoals. If


375 
$flag$ is {\tt true} then it performs elimresolution  it solves the


376 
first premise of~$rule$ by assumption and deletes that assumption.


377 
\end{description}


378 


379 


380 
\section{Managing lots of rules}


381 
These operations are not intended for interactive use. They are concerned


382 
with the processing of large numbers of rules in automatic proof


383 
strategies. Higherorder resolution involving a long list of rules is


384 
slow. Filtering techniques can shorten the list of rules given to


385 
resolution, and can also detect whether a given subgoal is too flexible,


386 
with too many rules applicable.


387 


388 
\subsection{Combined resolution and elimresolution} \label{biresolve_tac}


389 
\index{tactics!resolution}


390 
\begin{ttbox}


391 
biresolve_tac : (bool*thm)list > int > tactic


392 
bimatch_tac : (bool*thm)list > int > tactic


393 
subgoals_of_brl : bool*thm > int


394 
lessb : (bool*thm) * (bool*thm) > bool


395 
\end{ttbox}


396 
{\bf Biresolution} takes a list of $\it (flag,rule)$ pairs. For each


397 
pair, it applies resolution if the flag is~{\tt false} and


398 
elimresolution if the flag is~{\tt true}. A single tactic call handles a


399 
mixture of introduction and elimination rules.


400 


401 
\begin{description}


402 
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]


403 
refines the proof state by resolution or elimresolution on each rule, as


404 
indicated by its flag. It affects subgoal~$i$ of the proof state.


405 


406 
\item[\ttindexbold{bimatch_tac}]


407 
is like {\tt biresolve_tac}, but performs matching: unknowns in the


408 
proof state are never updated (see~\S\ref{match_tac}).


409 


410 
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]


411 
returns the number of new subgoals that biresolution would yield for the


412 
pair (if applied to a suitable subgoal). This is $n$ if the flag is


413 
{\tt false} and $n1$ if the flag is {\tt true}, where $n$ is the number


414 
of premises of the rule. Elimresolution yields one fewer subgoal than


415 
ordinary resolution because it solves the major premise by assumption.


416 


417 
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]


418 
returns the result of


419 
\begin{ttbox}


420 
subgoals_of_brl {\it brl1} < subgoals_of_brl {\it brl2}


421 
\end{ttbox}


422 
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it


423 
(flag,rule)$ pairs by the number of new subgoals they will yield. Thus,


424 
those that yield the fewest subgoals should be tried first.


425 
\end{description}


426 


427 


428 
\subsection{Discrimination nets for fast resolution}


429 
\index{discrimination netsbold}


430 
\index{tactics!resolution}


431 
\begin{ttbox}


432 
net_resolve_tac : thm list > int > tactic


433 
net_match_tac : thm list > int > tactic


434 
net_biresolve_tac: (bool*thm) list > int > tactic


435 
net_bimatch_tac : (bool*thm) list > int > tactic


436 
filt_resolve_tac : thm list > int > int > tactic


437 
could_unify : term*term>bool


438 
filter_thms : (term*term>bool) > int*term*thm list > thm list


439 
\end{ttbox}


440 
The module \ttindex{Net} implements a discrimination net data structure for


441 
fast selection of rules \cite[Chapter 14]{charniak80}. A term is


442 
classified by the symbol list obtained by flattening it in preorder.


443 
The flattening takes account of function applications, constants, and free


444 
and bound variables; it identifies all unknowns and also regards


445 
$\lambda$abstractions as unknowns, since they could $\eta$contract to


446 
anything.


447 


448 
A discrimination net serves as a polymorphic dictionary indexed by terms.


449 
The module provides various functions for inserting and removing items from


450 
nets. It provides functions for returning all items whose term could match


451 
or unify with a target term. The matching and unification tests are


452 
overly lax (due to the identifications mentioned above) but they serve as


453 
useful filters.


454 


455 
A net can store introduction rules indexed by their conclusion, and


456 
elimination rules indexed by their major premise. Isabelle provides


457 
several functions for ``compiling'' long lists of rules into fast


458 
resolution tactics. When supplied with a list of theorems, these functions


459 
build a discrimination net; the net is used when the tactic is applied to a


460 
goal. To avoid repreatedly constructing the nets, use currying: bind the


461 
resulting tactics to \ML{} identifiers.


462 


463 
\begin{description}


464 
\item[\ttindexbold{net_resolve_tac} {\it thms}]


465 
builds a discrimination net to obtain the effect of a similar call to {\tt


466 
resolve_tac}.


467 


468 
\item[\ttindexbold{net_match_tac} {\it thms}]


469 
builds a discrimination net to obtain the effect of a similar call to {\tt


470 
match_tac}.


471 


472 
\item[\ttindexbold{net_biresolve_tac} {\it brls}]


473 
builds a discrimination net to obtain the effect of a similar call to {\tt


474 
biresolve_tac}.


475 


476 
\item[\ttindexbold{net_bimatch_tac} {\it brls}]


477 
builds a discrimination net to obtain the effect of a similar call to {\tt


478 
bimatch_tac}.


479 


480 
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]


481 
uses discrimination nets to extract the {\it thms} that are applicable to


482 
subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the


483 
tactic fails. Otherwise it calls {\tt resolve_tac}.


484 


485 
This tactic helps avoid runaway instantiation of unknowns, for example in


486 
type inference.


487 


488 
\item[\ttindexbold{could_unify} ({\it t},{\it u})]


489 
returns {\tt false} if~$t$ and~$u$ are ``obviously'' nonunifiable, and


490 
otherwise returns~{\tt true}. It assumes all variables are distinct,


491 
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.


492 


493 
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]


494 
returns the list of potentially resolvable rules (in {\it thms\/}) for the


495 
subgoal {\it prem}, using the predicate {\it could\/} to compare the


496 
conclusion of the subgoal with the conclusion of each rule. The resulting list


497 
is no longer than {\it limit}.


498 
\end{description}


499 


500 


501 
\section{Programming tools for proof strategies}


502 
Do not consider using the primitives discussed in this section unless you


503 
really need to code tactics from scratch,


504 


505 
\subsection{Operations on type {\tt tactic}}


506 
\index{tactics!primitives for codingbold}


507 
A tactic maps theorems to theorem sequences (lazy lists). The type


508 
constructor for sequences is called \ttindex{Sequence.seq}. To simplify the


509 
types of tactics and tacticals, Isabelle defines a type of tactics:


510 
\begin{ttbox}


511 
datatype tactic = Tactic of thm > thm Sequence.seq


512 
\end{ttbox}


513 
{\tt Tactic} and {\tt tapply} convert between tactics and functions. The


514 
other operations provide means for coding tactics in a clean style.


515 
\begin{ttbox}


516 
tapply : tactic * thm > thm Sequence.seq


517 
Tactic : (thm > thm Sequence.seq) > tactic


518 
PRIMITIVE : (thm > thm) > tactic


519 
STATE : (thm > tactic) > tactic


520 
SUBGOAL : ((term*int) > tactic) > int > tactic


521 
\end{ttbox}


522 
\begin{description}


523 
\item[\ttindexbold{tapply} {\it tac} {\it thm}]


524 
returns the result of applying the tactic, as a function, to {\it thm}.


525 


526 
\item[\ttindexbold{Tactic} {\it f}]


527 
packages {\it f} as a tactic.


528 


529 
\item[\ttindexbold{PRIMITIVE} $f$]


530 
applies $f$ to the proof state and returns the result as a


531 
oneelement sequence. This packages the metarule~$f$ as a tactic.


532 


533 
\item[\ttindexbold{STATE} $f$]


534 
applies $f$ to the proof state and then applies the resulting tactic to the


535 
same state. It supports the following style, where the tactic body is


536 
expressed at a high level, but may peek at the proof state:


537 
\begin{ttbox}


538 
STATE (fn state => {\it some tactic})


539 
\end{ttbox}


540 


541 
\item[\ttindexbold{SUBGOAL} $f$ $i$]


542 
extracts subgoal~$i$ from the proof state as a term~$t$, and computes a


543 
tactic by calling~$f(t,i)$. It applies the resulting tactic to the same


544 
state. The tactic body is expressed at a high level, but may peek at a


545 
particular subgoal:


546 
\begin{ttbox}


547 
SUBGOAL (fn (t,i) => {\it some tactic})


548 
\end{ttbox}


549 
\end{description}


550 


551 


552 
\subsection{Tracing}


553 
\index{tactics!tracingbold}


554 
\index{tracing!of tactics}


555 
\begin{ttbox}


556 
pause_tac: tactic


557 
print_tac: tactic


558 
\end{ttbox}


559 
These violate the functional behaviour of tactics by printing information


560 
when they are applied to a proof state. Their output may be difficult to


561 
interpret. Note that certain of the searching tacticals, such as {\tt


562 
REPEAT}, have builtin tracing options.


563 
\begin{description}


564 
\item[\ttindexbold{pause_tac}]


565 
prints {\tt** Press RETURN to continue:} and then reads a line from the


566 
terminal. If this line is blank then it returns the proof state unchanged;


567 
otherwise it fails (which may terminate a repetition).


568 


569 
\item[\ttindexbold{print_tac}]


570 
returns the proof state unchanged, with the side effect of printing it at


571 
the terminal.


572 
\end{description}


573 


574 


575 
\subsection{Sequences}


576 
\index{sequences (lazy lists)bold}


577 
The module \ttindex{Sequence} declares a type of lazy lists. It uses


578 
Isabelle's type \ttindexbold{option} to represent the possible presence


579 
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of


580 
a value:


581 
\begin{ttbox}


582 
datatype 'a option = None  Some of 'a;


583 
\end{ttbox}

286

584 
For clarity, the module name {\tt Sequence} is omitted from the signature


585 
specifications below; for instance, {\tt null} appears instead of {\tt


586 
Sequence.null}.

104

587 


588 
\subsubsection{Basic operations on sequences}


589 
\begin{ttbox}

286

590 
null : 'a seq


591 
seqof : (unit > ('a * 'a seq) option) > 'a seq


592 
single : 'a > 'a seq


593 
pull : 'a seq > ('a * 'a seq) option

104

594 
\end{ttbox}


595 
\begin{description}


596 
\item[{\tt Sequence.null}]


597 
is the empty sequence.


598 


599 
\item[\tt Sequence.seqof (fn()=> Some($x$,$s$))]


600 
constructs the sequence with head~$x$ and tail~$s$, neither of which is


601 
evaluated.


602 


603 
\item[{\tt Sequence.single} $x$]


604 
constructs the sequence containing the single element~$x$.


605 


606 
\item[{\tt Sequence.pull} $s$]


607 
returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the


608 
sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull


609 
$s$} again will {\bf recompute} the value of~$x$; it is not stored!


610 
\end{description}


611 


612 


613 
\subsubsection{Converting between sequences and lists}


614 
\begin{ttbox}

286

615 
chop : int * 'a seq > 'a list * 'a seq


616 
list_of_s : 'a seq > 'a list


617 
s_of_list : 'a list > 'a seq

104

618 
\end{ttbox}


619 
\begin{description}


620 
\item[{\tt Sequence.chop} ($n$, $s$)]


621 
returns the first~$n$ elements of~$s$ as a list, paired with the remaining


622 
elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the


623 
list.


624 


625 
\item[{\tt Sequence.list_of_s} $s$]


626 
returns the elements of~$s$, which must be finite, as a list.


627 


628 
\item[{\tt Sequence.s_of_list} $l$]


629 
creates a sequence containing the elements of~$l$.


630 
\end{description}


631 


632 


633 
\subsubsection{Combining sequences}


634 
\begin{ttbox}

286

635 
append : 'a seq * 'a seq > 'a seq


636 
interleave : 'a seq * 'a seq > 'a seq


637 
flats : 'a seq seq > 'a seq


638 
maps : ('a > 'b) > 'a seq > 'b seq


639 
filters : ('a > bool) > 'a seq > 'a seq

104

640 
\end{ttbox}


641 
\begin{description}


642 
\item[{\tt Sequence.append} ($s@1$, $s@2$)]


643 
concatenates $s@1$ to $s@2$.


644 


645 
\item[{\tt Sequence.interleave} ($s@1$, $s@2$)]


646 
joins $s@1$ with $s@2$ by interleaving their elements. The result contains


647 
all the elements of the sequences, even if both are infinite.


648 


649 
\item[{\tt Sequence.flats} $ss$]


650 
concatenates a sequence of sequences.


651 


652 
\item[{\tt Sequence.maps} $f$ $s$]


653 
applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence


654 
$f(x@1),f(x@2),\ldots$.


655 


656 
\item[{\tt Sequence.filters} $p$ $s$]


657 
returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$


658 
is {\tt true}.


659 
\end{description}


660 


661 
\index{tactics)}
