author  paulson 
Thu, 26 Sep 1996 17:14:02 +0200  
changeset 2039  79c86b966257 
parent 1212  7059356e18e0 
child 2612  28232396b60e 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Tactics} \label{tactics} 

3 
\index{tactics(} 

323  4 
Tactics have type \mltydx{tactic}. They are essentially 
104  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, 

323  7 
as functions; instead they are expressed using basic tactics and tacticals. 
104  8 

2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

9 
This chapter only presents the primitive tactics. Substantial proofs require 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

10 
the power of simplification (Chapter~\ref{simpchap}) and classical reasoning 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

11 
(Chapter~\ref{chap:classical}). 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

12 

104  13 
\section{Resolution and assumption tactics} 
14 
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using 

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

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

20 

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 

23 
range. 

24 

25 
\subsection{Resolution tactics} 

323  26 
\index{resolution!tactics} 
104  27 
\index{tactics!resolutionbold} 
28 
\begin{ttbox} 

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 

33 
\end{ttbox} 

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

35 
of objectrules. 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 
higherorder resolution may yield multiple resolvents. 

323  38 
\begin{ttdescription} 
104  39 
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
323  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. 

104  43 

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

323  45 
\index{elimresolution} 
46 
performs elimresolution 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 

49 
subgoals. 

104  50 

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

323  52 
\index{forward proof}\index{destructresolution} 
53 
performs destructresolution with the rules, which normally should 

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

55 
applying one of the rules. 

104  56 

323  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 

60 
assumption. 

61 
\end{ttdescription} 

104  62 

63 
\subsection{Assumption tactics} 

323  64 
\index{tactics!assumptionbold}\index{assumptions!tactics for} 
104  65 
\begin{ttbox} 
66 
assume_tac : int > tactic 

67 
eq_assume_tac : int > tactic 

68 
\end{ttbox} 

323  69 
\begin{ttdescription} 
104  70 
\item[\ttindexbold{assume_tac} {\it i}] 
71 
attempts to solve subgoal~$i$ by assumption. 

72 

73 
\item[\ttindexbold{eq_assume_tac}] 

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

323  75 
{\em unique\/} next state) if one of the assumptions is identical to the 
104  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. 

323  79 
\end{ttdescription} 
104  80 

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

323  82 
\index{tactics!matching} 
104  83 
\begin{ttbox} 
84 
match_tac : thm list > int > tactic 

85 
ematch_tac : thm list > int > tactic 

86 
dmatch_tac : thm list > int > tactic 

87 
\end{ttbox} 

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 
willynilly, 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. 

323  93 
\begin{ttdescription} 
104  94 
\item[\ttindexbold{match_tac} {\it thms} {\it i}] 
323  95 
refines the proof state using the rules, matching a rule's 
104  96 
conclusion with subgoal~$i$ of the proof state. 
97 

98 
\item[\ttindexbold{ematch_tac}] 

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

100 

101 
\item[\ttindexbold{dmatch_tac}] 

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

323  103 
\end{ttdescription} 
104  104 

105 

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

323  107 
\index{tactics!instantiation}\index{instantiation} 
104  108 
\begin{ttbox} 
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 

113 
\end{ttbox} 

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

115 
induction, which cause difficulties for higherorder unification. The 

332  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 

119 
question mark! 

104  120 
\begin{itemize} 
332  121 
\item If $v$ is the type unknown {\tt'a}, then 
122 
the rule must contain a type unknown \verb$?'a$ of some 

104  123 
sort~$s$, and $e$ should be a type of sort $s$. 
124 

332  125 
\item If $v$ is the unknown {\tt P}, then 
126 
the rule must contain an unknown \verb$?P$ of some type~$\tau$, 

104  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$ 

332  129 
instantiates any type unknowns in $\tau$, these instantiations 
104  130 
are recorded for application to the rule. 
131 
\end{itemize} 

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. 

138 

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

140 
instantiations are typechecked 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. 

144 

323  145 
\begin{ttdescription} 
104  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 

332  150 
instantiations for every unknown in the rule. 
104  151 

152 
\item[\ttindexbold{eres_inst_tac}] 

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

154 

155 
\item[\ttindexbold{dres_inst_tac}] 

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

157 

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. 

323  162 
\end{ttdescription} 
104  163 

164 

165 
\section{Other basic tactics} 

166 
\subsection{Tactic shortcuts} 

323  167 
\index{shortcuts!for tactics} 
104  168 
\index{tactics!resolution}\index{tactics!assumption} 
169 
\index{tactics!metarewriting} 

170 
\begin{ttbox} 

332  171 
rtac : thm > int > tactic 
172 
etac : thm > int > tactic 

173 
dtac : thm > int > tactic 

174 
atac : int > tactic 

104  175 
ares_tac : thm list > int > tactic 
332  176 
rewtac : thm > tactic 
104  177 
\end{ttbox} 
178 
These abbreviate common uses of tactics. 

323  179 
\begin{ttdescription} 
104  180 
\item[\ttindexbold{rtac} {\it thm} {\it i}] 
181 
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution. 

182 

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

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

185 

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

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

188 
destructresolution. 

189 

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

332  191 
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption. 
104  192 

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

194 
tries proof by assumption and resolution; it abbreviates 

195 
\begin{ttbox} 

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

197 
\end{ttbox} 

198 

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

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

323  201 
\end{ttdescription} 
104  202 

203 

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

323  205 
\index{tactics!for inserting facts}\index{assumptions!inserting} 
104  206 
\begin{ttbox} 
207 
cut_facts_tac : thm list > int > tactic 

286  208 
cut_inst_tac : (string*string)list > thm > int > tactic 
209 
subgoal_tac : string > int > tactic 

457  210 
subgoal_tacs : string list > int > tactic 
104  211 
\end{ttbox} 
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

212 
These tactics add assumptions to a subgoal. 
323  213 
\begin{ttdescription} 
104  214 
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
215 
adds the {\it thms} as new assumptions to subgoal~$i$. Once they have 

286  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 metaquantifier. 

222 

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$. 

104  227 

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$. 

457  231 

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$. 

323  235 
\end{ttdescription} 
104  236 

237 

2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

238 
\subsection{``Putting off'' a subgoal} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

239 
\begin{ttbox} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

240 
defer_tac : int > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

241 
\end{ttbox} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

242 
\begin{ttdescription} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

243 
\item[\ttindexbold{defer_tac} {\it i}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

244 
moves subgoal~$i$ to the last position in the proof state. It can be 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

245 
useful when correcting a proof script: if the tactic given for subgoal~$i$ 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

246 
fails, calling {\tt defer_tac} instead will let you continue with the rest 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

247 
of the script. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

248 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

249 
The tactic fails if subgoal~$i$ does not exist or if the proof state 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

250 
contains type unknowns. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

251 
\end{ttdescription} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

252 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

253 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

254 
\subsection{Definitions and metalevel rewriting} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

255 
\index{tactics!metarewritingbold}\index{metarewritingbold} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

256 
\index{definitions} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

257 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

258 
Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

259 
constant or a constant applied to a list of variables, for example $\it 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

260 
sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$, 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

261 
are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means using 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

262 
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

263 
Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

264 
no rewrites are applicable to any subterm. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

265 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

266 
There are rules for unfolding and folding definitions; Isabelle does not do 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

267 
this automatically. The corresponding tactics rewrite the proof state, 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

268 
yielding a single next state. See also the {\tt goalw} command, which is the 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

269 
easiest way of handling definitions. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

270 
\begin{ttbox} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

271 
rewrite_goals_tac : thm list > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

272 
rewrite_tac : thm list > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

273 
fold_goals_tac : thm list > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

274 
fold_tac : thm list > tactic 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

275 
\end{ttbox} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

276 
\begin{ttdescription} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

277 
\item[\ttindexbold{rewrite_goals_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

278 
unfolds the {\it defs} throughout the subgoals of the proof state, while 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

279 
leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

280 
particular subgoal. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

281 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

282 
\item[\ttindexbold{rewrite_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

283 
unfolds the {\it defs} throughout the proof state, including the main goal 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

284 
 not normally desirable! 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

285 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

286 
\item[\ttindexbold{fold_goals_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

287 
folds the {\it defs} throughout the subgoals of the proof state, while 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

288 
leaving the main goal unchanged. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

289 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

290 
\item[\ttindexbold{fold_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

291 
folds the {\it defs} throughout the proof state. 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

292 
\end{ttdescription} 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

293 

79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

294 

104  295 
\subsection{Theorems useful with tactics} 
323  296 
\index{theorems!of pure theory} 
104  297 
\begin{ttbox} 
298 
asm_rl: thm 

299 
cut_rl: thm 

300 
\end{ttbox} 

323  301 
\begin{ttdescription} 
302 
\item[\tdx{asm_rl}] 

104  303 
is $\psi\Imp\psi$. Under elimresolution it does proof by assumption, and 
304 
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to 

305 
\begin{ttbox} 

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

307 
\end{ttbox} 

308 

323  309 
\item[\tdx{cut_rl}] 
104  310 
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting 
323  311 
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac} 
312 
and {\tt subgoal_tac}. 

313 
\end{ttdescription} 

104  314 

315 

316 
\section{Obscure tactics} 

1212  317 

318 
\subsection{Rotating assumptions} 

319 
\index{assumptions!rotating} 

320 
\begin{ttbox} 

321 
rotate_tac : int > int > tactic 

322 
\end{ttbox} 

323 
\begin{ttdescription} 

324 
\item[\ttindexbold{rotate_tac} $n$ $i$] 

325 
rotates the assumptions of subgoal $i$ by $n$ positions: from right to left, 

326 
if $n$ is positive, and from left to right, if $n$ is negative. Sometimes 

327 
necessary in connection with \ttindex{asm_full_simp_tac}. 

328 

329 
\end{ttdescription} 

330 

104  331 
\subsection{Tidying the proof state} 
323  332 
\index{parameters!removing unused} 
104  333 
\index{flexflex constraints} 
334 
\begin{ttbox} 

335 
prune_params_tac : tactic 

336 
flexflex_tac : tactic 

337 
\end{ttbox} 

323  338 
\begin{ttdescription} 
104  339 
\item[\ttindexbold{prune_params_tac}] 
340 
removes unused parameters from all subgoals of the proof state. It works 

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

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

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

344 

345 
\item[\ttindexbold{flexflex_tac}] 

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

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

348 
the last step of a proof. 

349 

350 
Flexflex constraints arise from difficult cases of higherorder 

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

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

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

354 
instantiated. 

323  355 
\end{ttdescription} 
104  356 

357 

323  358 
\subsection{Renaming parameters in a goal} \index{parameters!renaming} 
104  359 
\begin{ttbox} 
360 
rename_tac : string > int > tactic 

361 
rename_last_tac : string > string list > int > tactic 

362 
Logic.set_rename_prefix : string > unit 

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

364 
\end{ttbox} 

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

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

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

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

369 
$\forall$bound variable in the conclusion. 

370 

371 
Sometimes there is insufficient information and Isabelle chooses an 

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

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

323  374 
{\tt by} command prints the message {\tt Warning:\ same as previous 
104  375 
level}. 
376 

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

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

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

380 
prefix. They are ugly but predictable. 

381 

323  382 
\begin{ttdescription} 
104  383 
\item[\ttindexbold{rename_tac} {\it str} {\it i}] 
384 
interprets the string {\it str} as a series of blankseparated variable 

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

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

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

388 
to ensure that all the parameters are distinct. 

389 

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

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

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

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

394 

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

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

397 
is {\tt"k"}. 

398 

323  399 
\item[\ttindexbold{Logic.auto_rename} := true;] 
104  400 
makes Isabelle generate uniform names for parameters. 
323  401 
\end{ttdescription} 
104  402 

403 

404 
\subsection{Composition: resolution without lifting} 

323  405 
\index{tactics!for composition} 
104  406 
\begin{ttbox} 
407 
compose_tac: (bool * thm * int) > int > tactic 

408 
\end{ttbox} 

332  409 
{\bf Composing} two rules means resolving them without prior lifting or 
104  410 
renaming of unknowns. This lowlevel operation, which underlies the 
411 
resolution tactics, may occasionally be useful for special effects. 

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

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

323  414 
\begin{ttdescription} 
104  415 
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] 
416 
refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to 

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

323  418 
not be atomic; thus $m$ determines the number of new subgoals. If 
104  419 
$flag$ is {\tt true} then it performs elimresolution  it solves the 
420 
first premise of~$rule$ by assumption and deletes that assumption. 

323  421 
\end{ttdescription} 
104  422 

423 

424 
\section{Managing lots of rules} 

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

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

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

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

2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

429 
resolution, and can also detect whether a subgoal is too flexible, 
104  430 
with too many rules applicable. 
431 

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

433 
\index{tactics!resolution} 

434 
\begin{ttbox} 

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

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

437 
subgoals_of_brl : bool*thm > int 

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

439 
\end{ttbox} 

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

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

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

443 
mixture of introduction and elimination rules. 

444 

323  445 
\begin{ttdescription} 
104  446 
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
447 
refines the proof state by resolution or elimresolution on each rule, as 

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

449 

450 
\item[\ttindexbold{bimatch_tac}] 

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

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

453 

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

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

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

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

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

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

460 

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

462 
returns the result of 

463 
\begin{ttbox} 

332  464 
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2} 
104  465 
\end{ttbox} 
323  466 
\end{ttdescription} 
104  467 
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it 
468 
(flag,rule)$ pairs by the number of new subgoals they will yield. Thus, 

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

470 

471 

323  472 
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} 
104  473 
\index{discrimination netsbold} 
474 
\index{tactics!resolution} 

475 
\begin{ttbox} 

476 
net_resolve_tac : thm list > int > tactic 

477 
net_match_tac : thm list > int > tactic 

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

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

480 
filt_resolve_tac : thm list > int > int > tactic 

481 
could_unify : term*term>bool 

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

483 
\end{ttbox} 

323  484 
The module {\tt Net} implements a discrimination net data structure for 
104  485 
fast selection of rules \cite[Chapter 14]{charniak80}. A term is 
486 
classified by the symbol list obtained by flattening it in preorder. 

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

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

323  489 
\index{lambda abs@$\lambda$abstractions} 
104  490 
$\lambda$abstractions as unknowns, since they could $\eta$contract to 
491 
anything. 

492 

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

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

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

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

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

498 
useful filters. 

499 

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

501 
elimination rules indexed by their major premise. Isabelle provides 

323  502 
several functions for `compiling' long lists of rules into fast 
104  503 
resolution tactics. When supplied with a list of theorems, these functions 
504 
build a discrimination net; the net is used when the tactic is applied to a 

332  505 
goal. To avoid repeatedly constructing the nets, use currying: bind the 
104  506 
resulting tactics to \ML{} identifiers. 
507 

323  508 
\begin{ttdescription} 
104  509 
\item[\ttindexbold{net_resolve_tac} {\it thms}] 
510 
builds a discrimination net to obtain the effect of a similar call to {\tt 

511 
resolve_tac}. 

512 

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

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

515 
match_tac}. 

516 

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

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

519 
biresolve_tac}. 

520 

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

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

523 
bimatch_tac}. 

524 

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

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

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

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

529 

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

531 
type inference. 

532 

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

323  534 
returns {\tt false} if~$t$ and~$u$ are `obviously' nonunifiable, and 
104  535 
otherwise returns~{\tt true}. It assumes all variables are distinct, 
536 
reporting that {\tt ?a=?a} may unify with {\tt 0=1}. 

537 

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

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

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

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

542 
is no longer than {\it limit}. 

323  543 
\end{ttdescription} 
104  544 

545 

546 
\section{Programming tools for proof strategies} 

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

323  548 
really need to code tactics from scratch. 
104  549 

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

323  551 
\index{tactics!primitives for coding} 
104  552 
A tactic maps theorems to theorem sequences (lazy lists). The type 
323  553 
constructor for sequences is called \mltydx{Sequence.seq}. To simplify the 
104  554 
types of tactics and tacticals, Isabelle defines a type of tactics: 
555 
\begin{ttbox} 

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

557 
\end{ttbox} 

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

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

560 
\begin{ttbox} 

561 
tapply : tactic * thm > thm Sequence.seq 

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

563 
PRIMITIVE : (thm > thm) > tactic 

564 
STATE : (thm > tactic) > tactic 

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

566 
\end{ttbox} 

323  567 
\begin{ttdescription} 
568 
\item[\ttindexbold{tapply}({\it tac}, {\it thm})] 

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

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

572 
packages {\it f} as a tactic. 

573 

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

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

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

577 

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

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

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

323  581 
expressed using tactics and tacticals, but may peek at the proof state: 
104  582 
\begin{ttbox} 
323  583 
STATE (fn state => {\it tacticvalued expression}) 
104  584 
\end{ttbox} 
585 

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

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

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

323  589 
state. The tactic body is expressed using tactics and tacticals, but may 
590 
peek at a particular subgoal: 

104  591 
\begin{ttbox} 
323  592 
SUBGOAL (fn (t,i) => {\it tacticvalued expression}) 
104  593 
\end{ttbox} 
323  594 
\end{ttdescription} 
104  595 

596 

597 
\subsection{Tracing} 

323  598 
\index{tactics!tracing} 
104  599 
\index{tracing!of tactics} 
600 
\begin{ttbox} 

601 
pause_tac: tactic 

602 
print_tac: tactic 

603 
\end{ttbox} 

332  604 
These tactics print tracing information when they are applied to a proof 
605 
state. Their output may be difficult to interpret. Note that certain of 

606 
the searching tacticals, such as {\tt REPEAT}, have builtin tracing 

607 
options. 

323  608 
\begin{ttdescription} 
104  609 
\item[\ttindexbold{pause_tac}] 
332  610 
prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line 
611 
from the terminal. If this line is blank then it returns the proof state 

612 
unchanged; otherwise it fails (which may terminate a repetition). 

104  613 

614 
\item[\ttindexbold{print_tac}] 

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

616 
the terminal. 

323  617 
\end{ttdescription} 
104  618 

619 

323  620 
\section{Sequences} 
104  621 
\index{sequences (lazy lists)bold} 
323  622 
The module {\tt Sequence} declares a type of lazy lists. It uses 
623 
Isabelle's type \mltydx{option} to represent the possible presence 

104  624 
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of 
625 
a value: 

626 
\begin{ttbox} 

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

628 
\end{ttbox} 

286  629 
For clarity, the module name {\tt Sequence} is omitted from the signature 
630 
specifications below; for instance, {\tt null} appears instead of {\tt 

631 
Sequence.null}. 

104  632 

323  633 
\subsection{Basic operations on sequences} 
104  634 
\begin{ttbox} 
286  635 
null : 'a seq 
636 
seqof : (unit > ('a * 'a seq) option) > 'a seq 

637 
single : 'a > 'a seq 

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

104  639 
\end{ttbox} 
323  640 
\begin{ttdescription} 
641 
\item[Sequence.null] 

104  642 
is the empty sequence. 
643 

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

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

646 
evaluated. 

647 

323  648 
\item[Sequence.single $x$] 
104  649 
constructs the sequence containing the single element~$x$. 
650 

323  651 
\item[Sequence.pull $s$] 
104  652 
returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the 
653 
sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull 

332  654 
$s$} again will {\it recompute\/} the value of~$x$; it is not stored! 
323  655 
\end{ttdescription} 
104  656 

657 

323  658 
\subsection{Converting between sequences and lists} 
104  659 
\begin{ttbox} 
286  660 
chop : int * 'a seq > 'a list * 'a seq 
661 
list_of_s : 'a seq > 'a list 

662 
s_of_list : 'a list > 'a seq 

104  663 
\end{ttbox} 
323  664 
\begin{ttdescription} 
332  665 
\item[Sequence.chop($n$,$s$)] 
104  666 
returns the first~$n$ elements of~$s$ as a list, paired with the remaining 
667 
elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the 

668 
list. 

669 

323  670 
\item[Sequence.list_of_s $s$] 
104  671 
returns the elements of~$s$, which must be finite, as a list. 
672 

323  673 
\item[Sequence.s_of_list $l$] 
104  674 
creates a sequence containing the elements of~$l$. 
323  675 
\end{ttdescription} 
104  676 

677 

323  678 
\subsection{Combining sequences} 
104  679 
\begin{ttbox} 
286  680 
append : 'a seq * 'a seq > 'a seq 
681 
interleave : 'a seq * 'a seq > 'a seq 

682 
flats : 'a seq seq > 'a seq 

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

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

104  685 
\end{ttbox} 
323  686 
\begin{ttdescription} 
332  687 
\item[Sequence.append($s@1$,$s@2$)] 
104  688 
concatenates $s@1$ to $s@2$. 
689 

332  690 
\item[Sequence.interleave($s@1$,$s@2$)] 
104  691 
joins $s@1$ with $s@2$ by interleaving their elements. The result contains 
692 
all the elements of the sequences, even if both are infinite. 

693 

323  694 
\item[Sequence.flats $ss$] 
104  695 
concatenates a sequence of sequences. 
696 

323  697 
\item[Sequence.maps $f$ $s$] 
104  698 
applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence 
699 
$f(x@1),f(x@2),\ldots$. 

700 

323  701 
\item[Sequence.filters $p$ $s$] 
104  702 
returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$ 
703 
is {\tt true}. 

323  704 
\end{ttdescription} 
104  705 

706 
\index{tactics)} 