author  paulson 
Wed, 07 Oct 1998 10:31:30 +0200  
changeset 5619  76a8c72e3fd4 
parent 5371  e27558a68b8d 
child 6618  13293a7d4a57 
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 

4317  9 
This chapter only presents the primitive tactics. Substantial proofs 
10 
require the power of automatic tools like simplification 

11 
(Chapter~\ref{chap:simplification}) and classical tableau reasoning 

12 
(Chapter~\ref{chap:classical}). 

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

13 

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

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

17 
rules, while {\bf destructresolution} is particularly suited for 

18 
destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is 

19 
maintained for several different kinds of resolution tactics, as well as 

20 
the shortcuts in the subgoal module. 

21 

22 
All the tactics in this section act on a subgoal designated by a positive 

23 
integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of 

24 
range. 

25 

26 
\subsection{Resolution tactics} 

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

30 
resolve_tac : thm list > int > tactic 

31 
eresolve_tac : thm list > int > tactic 

32 
dresolve_tac : thm list > int > tactic 

33 
forward_tac : thm list > int > tactic 

34 
\end{ttbox} 

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

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

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

38 
higherorder resolution may yield multiple resolvents. 

323  39 
\begin{ttdescription} 
104  40 
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}] 
323  41 
refines the proof state using the rules, which should normally be 
42 
introduction rules. It resolves a rule's conclusion with 

43 
subgoal~$i$ of the proof state. 

104  44 

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

323  46 
\index{elimresolution} 
47 
performs elimresolution with the rules, which should normally be 

4607  48 
elimination rules. It resolves with a rule, proves its first premise by 
49 
assumption, and finally \emph{deletes} that assumption from any new 

50 
subgoals. (To rotate a rule's premises, 

51 
see \texttt{rotate_prems} in~\S\ref{MiscellaneousForwardRules}.) 

104  52 

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

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

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

57 
applying one of the rules. 

104  58 

323  59 
\item[\ttindexbold{forward_tac}]\index{forward proof} 
60 
is like {\tt dresolve_tac} except that the selected assumption is not 

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

62 
assumption. 

63 
\end{ttdescription} 

104  64 

65 
\subsection{Assumption tactics} 

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

69 
eq_assume_tac : int > tactic 

70 
\end{ttbox} 

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

74 

75 
\item[\ttindexbold{eq_assume_tac}] 

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

4607  77 
\emph{unique} next state) if one of the assumptions is identical to the 
104  78 
subgoal's conclusion. Since it does not instantiate variables, it cannot 
79 
make other subgoals unprovable. It is intended to be called from proof 

80 
strategies, not interactively. 

323  81 
\end{ttdescription} 
104  82 

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

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

87 
ematch_tac : thm list > int > tactic 

88 
dmatch_tac : thm list > int > tactic 

89 
\end{ttbox} 

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

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

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

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

94 
discard unifiers that would update the proof state. 

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

100 
\item[\ttindexbold{ematch_tac}] 

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

102 

103 
\item[\ttindexbold{dmatch_tac}] 

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

323  105 
\end{ttdescription} 
104  106 

107 

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

323  109 
\index{tactics!instantiation}\index{instantiation} 
104  110 
\begin{ttbox} 
111 
res_inst_tac : (string*string)list > thm > int > tactic 

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

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

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

115 
\end{ttbox} 

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

117 
induction, which cause difficulties for higherorder unification. The 

332  118 
tactics accept explicit instantiations for unknowns in the rule  
119 
typically, in the rule's conclusion. Each instantiation is a pair 

4607  120 
{\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading 
332  121 
question mark! 
104  122 
\begin{itemize} 
332  123 
\item If $v$ is the type unknown {\tt'a}, then 
124 
the rule must contain a type unknown \verb$?'a$ of some 

104  125 
sort~$s$, and $e$ should be a type of sort $s$. 
126 

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

104  129 
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and 
130 
$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$ 

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

134 
Types are instantiated before terms. Because type instantiations are 

135 
inferred from term instantiations, explicit type instantiations are seldom 

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

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

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

139 
failure because the tactics cannot instantiate them. 

140 

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

142 
instantiations are typechecked in the context of that subgoal  in 

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

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

145 
may not refer to unknowns in the subgoal. 

146 

323  147 
\begin{ttdescription} 
104  148 
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}] 
149 
instantiates the rule {\it thm} with the instantiations {\it insts}, as 

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

151 
typically causes further instantiations; you need not give explicit 

332  152 
instantiations for every unknown in the rule. 
104  153 

154 
\item[\ttindexbold{eres_inst_tac}] 

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

156 

157 
\item[\ttindexbold{dres_inst_tac}] 

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

159 

160 
\item[\ttindexbold{forw_inst_tac}] 

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

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

163 
result as a new assumption. 

323  164 
\end{ttdescription} 
104  165 

166 

167 
\section{Other basic tactics} 

168 
\subsection{Tactic shortcuts} 

323  169 
\index{shortcuts!for tactics} 
104  170 
\index{tactics!resolution}\index{tactics!assumption} 
171 
\index{tactics!metarewriting} 

172 
\begin{ttbox} 

332  173 
rtac : thm > int > tactic 
174 
etac : thm > int > tactic 

175 
dtac : thm > int > tactic 

176 
atac : int > tactic 

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

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

184 

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

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

187 

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

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

190 
destructresolution. 

191 

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

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

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

196 
tries proof by assumption and resolution; it abbreviates 

197 
\begin{ttbox} 

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

199 
\end{ttbox} 

200 

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

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

323  203 
\end{ttdescription} 
104  204 

205 

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

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

286  210 
cut_inst_tac : (string*string)list > thm > int > tactic 
211 
subgoal_tac : string > int > tactic 

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

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

286  218 
been inserted as assumptions, they become subject to tactics such as {\tt 
219 
eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises 

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

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

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

223 
could state the goal with an outermost metaquantifier. 

224 

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

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

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

228 
new assumption to subgoal~$i$. 

104  229 

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

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

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

457  233 

234 
\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] 

235 
uses {\tt subgoal_tac} to add the members of the list of {\it 

236 
formulae} as assumptions to subgoal~$i$. 

323  237 
\end{ttdescription} 
104  238 

239 

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

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

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

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

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

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

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

246 
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

247 
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

248 
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

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

250 

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

251 
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

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

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

254 

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

255 

4317  256 
\subsection{Definitions and metalevel rewriting} \label{sec:rewrite_goals} 
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

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

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

259 

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

260 
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

261 
constant or a constant applied to a list of variables, for example $\it 
4317  262 
sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$, 
263 
are also supported. {\bf Unfolding} the definition ${t\equiv u}$ means using 

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

264 
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

265 
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

266 
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

267 

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

268 
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

269 
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

270 
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

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

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

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

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

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

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

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

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

279 
\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

280 
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

281 
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

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

283 

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

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

285 
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

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

287 

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

288 
\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

289 
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

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

291 

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

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

293 
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

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

295 

4317  296 
\begin{warn} 
297 
These tactics only cope with definitions expressed as metalevel 

298 
equalities ($\equiv$). More general equivalences are handled by the 

299 
simplifier, provided that it is set up appropriately for your logic 

300 
(see Chapter~\ref{chap:simplification}). 

301 
\end{warn} 

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

302 

104  303 
\subsection{Theorems useful with tactics} 
323  304 
\index{theorems!of pure theory} 
104  305 
\begin{ttbox} 
306 
asm_rl: thm 

307 
cut_rl: thm 

308 
\end{ttbox} 

323  309 
\begin{ttdescription} 
310 
\item[\tdx{asm_rl}] 

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

313 
\begin{ttbox} 

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

315 
\end{ttbox} 

316 

323  317 
\item[\tdx{cut_rl}] 
104  318 
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting 
323  319 
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac} 
320 
and {\tt subgoal_tac}. 

321 
\end{ttdescription} 

104  322 

323 

324 
\section{Obscure tactics} 

1212  325 

323  326 
\subsection{Renaming parameters in a goal} \index{parameters!renaming} 
104  327 
\begin{ttbox} 
328 
rename_tac : string > int > tactic 

329 
rename_last_tac : string > string list > int > tactic 

330 
Logic.set_rename_prefix : string > unit 

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

332 
\end{ttbox} 

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

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

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

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

337 
$\forall$bound variable in the conclusion. 

338 

339 
Sometimes there is insufficient information and Isabelle chooses an 

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

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

323  342 
{\tt by} command prints the message {\tt Warning:\ same as previous 
104  343 
level}. 
344 

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

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

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

348 
prefix. They are ugly but predictable. 

349 

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

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

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

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

356 
to ensure that all the parameters are distinct. 

357 

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

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

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

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

362 

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

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

365 
is {\tt"k"}. 

366 

4317  367 
\item[set \ttindexbold{Logic.auto_rename};] 
104  368 
makes Isabelle generate uniform names for parameters. 
323  369 
\end{ttdescription} 
104  370 

371 

2612  372 
\subsection{Manipulating assumptions} 
373 
\index{assumptions!rotating} 

374 
\begin{ttbox} 

375 
thin_tac : string > int > tactic 

376 
rotate_tac : int > int > tactic 

377 
\end{ttbox} 

378 
\begin{ttdescription} 

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

380 
\index{assumptions!deleting} 

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

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

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

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

385 

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

387 
\index{assumptions!rotating} 

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

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

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

391 
processes assumptions from left to right. 

392 
\end{ttdescription} 

393 

394 

395 
\subsection{Tidying the proof state} 

3400  396 
\index{duplicate subgoals!removing} 
2612  397 
\index{parameters!removing unused} 
398 
\index{flexflex constraints} 

399 
\begin{ttbox} 

3400  400 
distinct_subgoals_tac : tactic 
401 
prune_params_tac : tactic 

402 
flexflex_tac : tactic 

2612  403 
\end{ttbox} 
404 
\begin{ttdescription} 

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

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

408 

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

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

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

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

414 

415 
\item[\ttindexbold{flexflex_tac}] 

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

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

418 
the last step of a proof. 

419 

420 
Flexflex constraints arise from difficult cases of higherorder 

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

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

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

424 
instantiated. 

425 
\end{ttdescription} 

426 

427 

104  428 
\subsection{Composition: resolution without lifting} 
323  429 
\index{tactics!for composition} 
104  430 
\begin{ttbox} 
431 
compose_tac: (bool * thm * int) > int > tactic 

432 
\end{ttbox} 

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

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

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

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

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

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

323  445 
\end{ttdescription} 
104  446 

447 

4276  448 
\section{*Managing lots of rules} 
104  449 
These operations are not intended for interactive use. They are concerned 
450 
with the processing of large numbers of rules in automatic proof 

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

452 
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

453 
resolution, and can also detect whether a subgoal is too flexible, 
104  454 
with too many rules applicable. 
455 

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

457 
\index{tactics!resolution} 

458 
\begin{ttbox} 

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

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

461 
subgoals_of_brl : bool*thm > int 

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

463 
\end{ttbox} 

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

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

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

467 
mixture of introduction and elimination rules. 

468 

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

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

473 

474 
\item[\ttindexbold{bimatch_tac}] 

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

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

477 

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

4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4317
diff
changeset

479 
returns the number of new subgoals that bires\o\lu\tion would yield for the 
104  480 
pair (if applied to a suitable subgoal). This is $n$ if the flag is 
481 
{\tt false} and $n1$ if the flag is {\tt true}, where $n$ is the number 

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

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

484 

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

486 
returns the result of 

487 
\begin{ttbox} 

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

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

494 

495 

323  496 
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} 
104  497 
\index{discrimination netsbold} 
498 
\index{tactics!resolution} 

499 
\begin{ttbox} 

500 
net_resolve_tac : thm list > int > tactic 

501 
net_match_tac : thm list > int > tactic 

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

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

504 
filt_resolve_tac : thm list > int > int > tactic 

505 
could_unify : term*term>bool 

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

507 
\end{ttbox} 

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

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

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

323  513 
\index{lambda abs@$\lambda$abstractions} 
104  514 
$\lambda$abstractions as unknowns, since they could $\eta$contract to 
515 
anything. 

516 

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

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

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

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

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

522 
useful filters. 

523 

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

525 
elimination rules indexed by their major premise. Isabelle provides 

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

332  529 
goal. To avoid repeatedly constructing the nets, use currying: bind the 
104  530 
resulting tactics to \ML{} identifiers. 
531 

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

535 
resolve_tac}. 

536 

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

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

539 
match_tac}. 

540 

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

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

543 
biresolve_tac}. 

544 

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

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

547 
bimatch_tac}. 

548 

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

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

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

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

553 

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

555 
type inference. 

556 

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

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

561 

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

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

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

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

566 
is no longer than {\it limit}. 

323  567 
\end{ttdescription} 
104  568 

569 

4317  570 
\section{Programming tools for proof strategies} 
104  571 
Do not consider using the primitives discussed in this section unless you 
323  572 
really need to code tactics from scratch. 
104  573 

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

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

4276  577 
\mltydx{Seq.seq}. To simplify the types of tactics and tacticals, 
3561  578 
Isabelle defines a type abbreviation: 
104  579 
\begin{ttbox} 
4276  580 
type tactic = thm > thm Seq.seq 
104  581 
\end{ttbox} 
3108  582 
The following operations provide means for coding tactics in a clean style. 
104  583 
\begin{ttbox} 
584 
PRIMITIVE : (thm > thm) > tactic 

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

586 
\end{ttbox} 

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

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

591 
sequence. 

104  592 

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

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

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

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

104  598 
\begin{ttbox} 
323  599 
SUBGOAL (fn (t,i) => {\it tacticvalued expression}) 
104  600 
\end{ttbox} 
323  601 
\end{ttdescription} 
104  602 

603 

604 
\subsection{Tracing} 

323  605 
\index{tactics!tracing} 
104  606 
\index{tracing!of tactics} 
607 
\begin{ttbox} 

608 
pause_tac: tactic 

609 
print_tac: tactic 

610 
\end{ttbox} 

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

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

614 
options. 

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

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

104  620 

621 
\item[\ttindexbold{print_tac}] 

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

623 
the terminal. 

323  624 
\end{ttdescription} 
104  625 

626 

4276  627 
\section{*Sequences} 
104  628 
\index{sequences (lazy lists)bold} 
4276  629 
The module {\tt Seq} declares a type of lazy lists. It uses 
323  630 
Isabelle's type \mltydx{option} to represent the possible presence 
104  631 
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of 
632 
a value: 

633 
\begin{ttbox} 

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

635 
\end{ttbox} 

4276  636 
The {\tt Seq} structure is supposed to be accessed via fully qualified 
4317  637 
names and should not be \texttt{open}. 
104  638 

323  639 
\subsection{Basic operations on sequences} 
104  640 
\begin{ttbox} 
4276  641 
Seq.empty : 'a seq 
642 
Seq.make : (unit > ('a * 'a seq) option) > 'a seq 

643 
Seq.single : 'a > 'a seq 

644 
Seq.pull : 'a seq > ('a * 'a seq) option 

104  645 
\end{ttbox} 
323  646 
\begin{ttdescription} 
4276  647 
\item[Seq.empty] is the empty sequence. 
104  648 

4276  649 
\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the 
650 
sequence with head~$x$ and tail~$xq$, neither of which is evaluated. 

104  651 

4276  652 
\item[Seq.single $x$] 
104  653 
constructs the sequence containing the single element~$x$. 
654 

4276  655 
\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and 
656 
{\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$. 

657 
Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/} 

658 
the value of~$x$; it is not stored! 

323  659 
\end{ttdescription} 
104  660 

661 

323  662 
\subsection{Converting between sequences and lists} 
104  663 
\begin{ttbox} 
4276  664 
Seq.chop : int * 'a seq > 'a list * 'a seq 
665 
Seq.list_of : 'a seq > 'a list 

666 
Seq.of_list : 'a list > 'a seq 

104  667 
\end{ttbox} 
323  668 
\begin{ttdescription} 
4276  669 
\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a 
670 
list, paired with the remaining elements of~$xq$. If $xq$ has fewer 

671 
than~$n$ elements, then so will the list. 

672 

673 
\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be 

674 
finite, as a list. 

675 

676 
\item[Seq.of_list $xs$] creates a sequence containing the elements 

677 
of~$xs$. 

323  678 
\end{ttdescription} 
104  679 

680 

323  681 
\subsection{Combining sequences} 
104  682 
\begin{ttbox} 
4276  683 
Seq.append : 'a seq * 'a seq > 'a seq 
684 
Seq.interleave : 'a seq * 'a seq > 'a seq 

685 
Seq.flat : 'a seq seq > 'a seq 

686 
Seq.map : ('a > 'b) > 'a seq > 'b seq 

687 
Seq.filter : ('a > bool) > 'a seq > 'a seq 

104  688 
\end{ttbox} 
323  689 
\begin{ttdescription} 
4276  690 
\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$. 
691 

692 
\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by 

693 
interleaving their elements. The result contains all the elements 

694 
of the sequences, even if both are infinite. 

695 

696 
\item[Seq.flat $xqq$] concatenates a sequence of sequences. 

697 

698 
\item[Seq.map $f$ $xq$] applies $f$ to every element 

699 
of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$. 

700 

701 
\item[Seq.filter $p$ $xq$] returns the sequence consisting of all 

702 
elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}. 

323  703 
\end{ttdescription} 
104  704 

705 
\index{tactics)} 

5371  706 

707 

708 
%%% Local Variables: 

709 
%%% mode: latex 

710 
%%% TeXmaster: "ref" 

711 
%%% End: 