author  oheimb 
Wed, 12 Nov 1997 18:58:50 +0100  
changeset 4223  f60e3d2c81d3 
parent 3950  e9d5bcae8351 
child 4276  a770eae2cdb0 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Tactics} \label{tactics} 

3108  3 
\index{tactics(} Tactics have type \mltydx{tactic}. This is just an 
4 
abbreviation for functions from theorems to theorem sequences, where 

5 
the theorems represent states of a backward proof. Tactics seldom 

6 
need to be coded from scratch, as functions; instead they are 

7 
expressed using basic tactics and tacticals. 

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 
3950  10 
the power of simplification (Chapter~\ref{chap:simplification}) and classical 
11 
reasoning (Chapter~\ref{chap:classical}). 

2039
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 

323  318 
\subsection{Renaming parameters in a goal} \index{parameters!renaming} 
104  319 
\begin{ttbox} 
320 
rename_tac : string > int > tactic 

321 
rename_last_tac : string > string list > int > tactic 

322 
Logic.set_rename_prefix : string > unit 

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

324 
\end{ttbox} 

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

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

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

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

329 
$\forall$bound variable in the conclusion. 

330 

331 
Sometimes there is insufficient information and Isabelle chooses an 

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

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

323  334 
{\tt by} command prints the message {\tt Warning:\ same as previous 
104  335 
level}. 
336 

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

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

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

340 
prefix. They are ugly but predictable. 

341 

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

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

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

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

348 
to ensure that all the parameters are distinct. 

349 

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

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

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

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

354 

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

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

357 
is {\tt"k"}. 

358 

323  359 
\item[\ttindexbold{Logic.auto_rename} := true;] 
104  360 
makes Isabelle generate uniform names for parameters. 
323  361 
\end{ttdescription} 
104  362 

363 

2612  364 
\subsection{Manipulating assumptions} 
365 
\index{assumptions!rotating} 

366 
\begin{ttbox} 

367 
thin_tac : string > int > tactic 

368 
rotate_tac : int > int > tactic 

369 
\end{ttbox} 

370 
\begin{ttdescription} 

371 
\item[\ttindexbold{thin_tac} {\it formula} $i$] 

372 
\index{assumptions!deleting} 

373 
deletes the specified assumption from subgoal $i$. Often the assumption 

374 
can be abbreviated, replacing subformul{\ae} by unknowns; the first matching 

375 
assumption will be deleted. Removing useless assumptions from a subgoal 

376 
increases its readability and can make search tactics run faster. 

377 

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

379 
\index{assumptions!rotating} 

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

381 
if $n$ is positive, and from left to right if $n$ is negative. This is 

382 
sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which 

383 
processes assumptions from left to right. 

384 
\end{ttdescription} 

385 

386 

387 
\subsection{Tidying the proof state} 

3400  388 
\index{duplicate subgoals!removing} 
2612  389 
\index{parameters!removing unused} 
390 
\index{flexflex constraints} 

391 
\begin{ttbox} 

3400  392 
distinct_subgoals_tac : tactic 
393 
prune_params_tac : tactic 

394 
flexflex_tac : tactic 

2612  395 
\end{ttbox} 
396 
\begin{ttdescription} 

3400  397 
\item[\ttindexbold{distinct_subgoals_tac}] 
398 
removes duplicate subgoals from a proof state. (These arise especially 

399 
in \ZF{}, where the subgoals are essentially type constraints.) 

400 

2612  401 
\item[\ttindexbold{prune_params_tac}] 
402 
removes unused parameters from all subgoals of the proof state. It works 

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

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

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

406 

407 
\item[\ttindexbold{flexflex_tac}] 

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

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

410 
the last step of a proof. 

411 

412 
Flexflex constraints arise from difficult cases of higherorder 

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

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

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

416 
instantiated. 

417 
\end{ttdescription} 

418 

419 

104  420 
\subsection{Composition: resolution without lifting} 
323  421 
\index{tactics!for composition} 
104  422 
\begin{ttbox} 
423 
compose_tac: (bool * thm * int) > int > tactic 

424 
\end{ttbox} 

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

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

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

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

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

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

323  437 
\end{ttdescription} 
104  438 

439 

440 
\section{Managing lots of rules} 

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

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

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

444 
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

445 
resolution, and can also detect whether a subgoal is too flexible, 
104  446 
with too many rules applicable. 
447 

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

449 
\index{tactics!resolution} 

450 
\begin{ttbox} 

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

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

453 
subgoals_of_brl : bool*thm > int 

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

455 
\end{ttbox} 

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

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

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

459 
mixture of introduction and elimination rules. 

460 

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

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

465 

466 
\item[\ttindexbold{bimatch_tac}] 

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

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

469 

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

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

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

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

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

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

476 

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

478 
returns the result of 

479 
\begin{ttbox} 

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

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

486 

487 

323  488 
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} 
104  489 
\index{discrimination netsbold} 
490 
\index{tactics!resolution} 

491 
\begin{ttbox} 

492 
net_resolve_tac : thm list > int > tactic 

493 
net_match_tac : thm list > int > tactic 

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

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

496 
filt_resolve_tac : thm list > int > int > tactic 

497 
could_unify : term*term>bool 

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

499 
\end{ttbox} 

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

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

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

323  505 
\index{lambda abs@$\lambda$abstractions} 
104  506 
$\lambda$abstractions as unknowns, since they could $\eta$contract to 
507 
anything. 

508 

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

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

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

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

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

514 
useful filters. 

515 

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

517 
elimination rules indexed by their major premise. Isabelle provides 

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

332  521 
goal. To avoid repeatedly constructing the nets, use currying: bind the 
104  522 
resulting tactics to \ML{} identifiers. 
523 

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

527 
resolve_tac}. 

528 

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

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

531 
match_tac}. 

532 

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

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

535 
biresolve_tac}. 

536 

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

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

539 
bimatch_tac}. 

540 

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

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

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

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

545 

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

547 
type inference. 

548 

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

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

553 

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

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

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

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

558 
is no longer than {\it limit}. 

323  559 
\end{ttdescription} 
104  560 

561 

562 
\section{Programming tools for proof strategies} 

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

323  564 
really need to code tactics from scratch. 
104  565 

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

3561  567 
\index{tactics!primitives for coding} A tactic maps theorems to sequences of 
568 
theorems. The type constructor for sequences (lazy lists) is called 

569 
\mltydx{Sequence.seq}. To simplify the types of tactics and tacticals, 

570 
Isabelle defines a type abbreviation: 

104  571 
\begin{ttbox} 
3108  572 
type tactic = thm > thm Sequence.seq 
104  573 
\end{ttbox} 
3108  574 
The following operations provide means for coding tactics in a clean style. 
104  575 
\begin{ttbox} 
576 
PRIMITIVE : (thm > thm) > tactic 

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

578 
\end{ttbox} 

323  579 
\begin{ttdescription} 
3561  580 
\item[\ttindexbold{PRIMITIVE} $f$] packages the metarule~$f$ as a tactic that 
581 
applies $f$ to the proof state and returns the result as a oneelement 

582 
sequence. If $f$ raises an exception, then the tactic's result is the empty 

583 
sequence. 

104  584 

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

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

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

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

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

595 

596 
\subsection{Tracing} 

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

600 
pause_tac: tactic 

601 
print_tac: tactic 

602 
\end{ttbox} 

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

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

606 
options. 

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

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

104  612 

613 
\item[\ttindexbold{print_tac}] 

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

615 
the terminal. 

323  616 
\end{ttdescription} 
104  617 

618 

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

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

625 
\begin{ttbox} 

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

627 
\end{ttbox} 

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

630 
Sequence.null}. 

104  631 

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

636 
single : 'a > 'a seq 

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

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

104  641 
is the empty sequence. 
642 

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

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

645 
evaluated. 

646 

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

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

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

656 

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

661 
s_of_list : 'a list > 'a seq 

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

667 
list. 

668 

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

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

676 

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

681 
flats : 'a seq seq > 'a seq 

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

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

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

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

692 

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

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

699 

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

323  703 
\end{ttdescription} 
104  704 

705 
\index{tactics)} 