author  wenzelm 
Fri, 04 Aug 2000 22:53:44 +0200  
changeset 9523  232b09dba0fe 
parent 8136  8c65f3ca13f2 
child 9568  20c410fb5104 
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, 

7491  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} 

8136  134 
Types are instantiated before terms are. Because type instantiations are 
104  135 
inferred from term instantiations, explicit type instantiations are seldom 
136 
necessary  if \verb$?t$ has type \verb$?'a$, then the instantiation list 

8136  137 
\texttt{[("'a","bool"), ("t","True")]} may be simplified to 
138 
\texttt{[("t","True")]}. Type unknowns in the proof state may cause 

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

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

175 
dtac : thm > int > tactic 

176 
ftac : thm > int > tactic 

177 
atac : int > tactic 

178 
eatac : thm > int > int > tactic 

179 
datac : thm > int > int > tactic 

180 
fatac : thm > int > int > tactic 

181 
ares_tac : thm list > int > tactic 

182 
rewtac : thm > tactic 

104  183 
\end{ttbox} 
184 
These abbreviate common uses of tactics. 

323  185 
\begin{ttdescription} 
104  186 
\item[\ttindexbold{rtac} {\it thm} {\it i}] 
187 
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution. 

188 

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

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

191 

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

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

194 
destructresolution. 

195 

7491  196 
\item[\ttindexbold{ftac} {\it thm} {\it i}] 
197 
abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing 

198 
destructresolution without deleting the assumption. 

199 

104  200 
\item[\ttindexbold{atac} {\it i}] 
332  201 
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption. 
104  202 

7491  203 
\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}] 
204 
performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac}, 

205 
solving additionally {\it j}~premises of the rule {\it thm} by assumption. 

206 

207 
\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}] 

208 
performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac}, 

209 
solving additionally {\it j}~premises of the rule {\it thm} by assumption. 

210 

211 
\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}] 

212 
performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac}, 

213 
solving additionally {\it j}~premises of the rule {\it thm} by assumption. 

214 

104  215 
\item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
216 
tries proof by assumption and resolution; it abbreviates 

217 
\begin{ttbox} 

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

219 
\end{ttbox} 

220 

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

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

323  223 
\end{ttdescription} 
104  224 

225 

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

323  227 
\index{tactics!for inserting facts}\index{assumptions!inserting} 
104  228 
\begin{ttbox} 
229 
cut_facts_tac : thm list > int > tactic 

286  230 
cut_inst_tac : (string*string)list > thm > int > tactic 
231 
subgoal_tac : string > int > tactic 

9523  232 
subgoals_tac : string list > int > tactic 
104  233 
\end{ttbox} 
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

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

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

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

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

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

243 
could state the goal with an outermost metaquantifier. 

244 

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

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

7491  247 
described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a 
286  248 
new assumption to subgoal~$i$. 
104  249 

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

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

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

457  253 

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

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

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

323  257 
\end{ttdescription} 
104  258 

259 

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

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

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

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

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

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

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

266 
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

267 
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

268 
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

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

270 

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

271 
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

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

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

274 

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

275 

4317  276 
\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

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

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

279 

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

280 
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

281 
constant or a constant applied to a list of variables, for example $\it 
4317  282 
sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$, 
283 
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

284 
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

285 
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

286 
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

287 

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

288 
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

289 
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

290 
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

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

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

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

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

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

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

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

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

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

300 
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

301 
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

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

303 

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

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

305 
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

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

307 

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

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

309 
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

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

311 

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

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

313 
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

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

315 

4317  316 
\begin{warn} 
317 
These tactics only cope with definitions expressed as metalevel 

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

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

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

321 
\end{warn} 

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

322 

104  323 
\subsection{Theorems useful with tactics} 
323  324 
\index{theorems!of pure theory} 
104  325 
\begin{ttbox} 
326 
asm_rl: thm 

327 
cut_rl: thm 

328 
\end{ttbox} 

323  329 
\begin{ttdescription} 
330 
\item[\tdx{asm_rl}] 

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

333 
\begin{ttbox} 

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

335 
\end{ttbox} 

336 

323  337 
\item[\tdx{cut_rl}] 
104  338 
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting 
323  339 
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac} 
340 
and {\tt subgoal_tac}. 

341 
\end{ttdescription} 

104  342 

343 

344 
\section{Obscure tactics} 

1212  345 

323  346 
\subsection{Renaming parameters in a goal} \index{parameters!renaming} 
104  347 
\begin{ttbox} 
348 
rename_tac : string > int > tactic 

349 
rename_last_tac : string > string list > int > tactic 

350 
Logic.set_rename_prefix : string > unit 

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

352 
\end{ttbox} 

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

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

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

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

357 
$\forall$bound variable in the conclusion. 

358 

359 
Sometimes there is insufficient information and Isabelle chooses an 

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

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

323  362 
{\tt by} command prints the message {\tt Warning:\ same as previous 
104  363 
level}. 
364 

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

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

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

368 
prefix. They are ugly but predictable. 

369 

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

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

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

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

376 
to ensure that all the parameters are distinct. 

377 

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

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

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

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

382 

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

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

385 
is {\tt"k"}. 

386 

4317  387 
\item[set \ttindexbold{Logic.auto_rename};] 
104  388 
makes Isabelle generate uniform names for parameters. 
323  389 
\end{ttdescription} 
104  390 

391 

2612  392 
\subsection{Manipulating assumptions} 
393 
\index{assumptions!rotating} 

394 
\begin{ttbox} 

395 
thin_tac : string > int > tactic 

396 
rotate_tac : int > int > tactic 

397 
\end{ttbox} 

398 
\begin{ttdescription} 

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

400 
\index{assumptions!deleting} 

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

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

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

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

405 

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

407 
\index{assumptions!rotating} 

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

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

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

411 
processes assumptions from left to right. 

412 
\end{ttdescription} 

413 

414 

415 
\subsection{Tidying the proof state} 

3400  416 
\index{duplicate subgoals!removing} 
2612  417 
\index{parameters!removing unused} 
418 
\index{flexflex constraints} 

419 
\begin{ttbox} 

3400  420 
distinct_subgoals_tac : tactic 
421 
prune_params_tac : tactic 

422 
flexflex_tac : tactic 

2612  423 
\end{ttbox} 
424 
\begin{ttdescription} 

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

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

428 

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

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

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

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

434 

435 
\item[\ttindexbold{flexflex_tac}] 

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

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

438 
the last step of a proof. 

439 

440 
Flexflex constraints arise from difficult cases of higherorder 

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

7491  442 
some variables in a rule~({\S}\ref{res_inst_tac}). Normally flexflex 
2612  443 
constraints can be ignored; they often disappear as unknowns get 
444 
instantiated. 

445 
\end{ttdescription} 

446 

447 

104  448 
\subsection{Composition: resolution without lifting} 
323  449 
\index{tactics!for composition} 
104  450 
\begin{ttbox} 
451 
compose_tac: (bool * thm * int) > int > tactic 

452 
\end{ttbox} 

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

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

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

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

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

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

323  465 
\end{ttdescription} 
104  466 

467 

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

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

472 
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

473 
resolution, and can also detect whether a subgoal is too flexible, 
104  474 
with too many rules applicable. 
475 

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

477 
\index{tactics!resolution} 

478 
\begin{ttbox} 

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

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

481 
subgoals_of_brl : bool*thm > int 

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

483 
\end{ttbox} 

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

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

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

487 
mixture of introduction and elimination rules. 

488 

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

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

493 

494 
\item[\ttindexbold{bimatch_tac}] 

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

7491  496 
proof state are never updated (see~{\S}\ref{match_tac}). 
104  497 

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

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

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

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

504 

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

506 
returns the result of 

507 
\begin{ttbox} 

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

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

514 

515 

323  516 
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} 
104  517 
\index{discrimination netsbold} 
518 
\index{tactics!resolution} 

519 
\begin{ttbox} 

520 
net_resolve_tac : thm list > int > tactic 

521 
net_match_tac : thm list > int > tactic 

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

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

524 
filt_resolve_tac : thm list > int > int > tactic 

525 
could_unify : term*term>bool 

8136  526 
filter_thms : (term*term>bool) > int*term*thm list > thm{\ts}list 
104  527 
\end{ttbox} 
323  528 
The module {\tt Net} implements a discrimination net data structure for 
104  529 
fast selection of rules \cite[Chapter 14]{charniak80}. A term is 
530 
classified by the symbol list obtained by flattening it in preorder. 

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

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

323  533 
\index{lambda abs@$\lambda$abstractions} 
104  534 
$\lambda$abstractions as unknowns, since they could $\eta$contract to 
535 
anything. 

536 

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

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

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

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

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

542 
useful filters. 

543 

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

545 
elimination rules indexed by their major premise. Isabelle provides 

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

332  549 
goal. To avoid repeatedly constructing the nets, use currying: bind the 
104  550 
resulting tactics to \ML{} identifiers. 
551 

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

555 
resolve_tac}. 

556 

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

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

559 
match_tac}. 

560 

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

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

563 
biresolve_tac}. 

564 

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

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

567 
bimatch_tac}. 

568 

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

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

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

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

573 

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

575 
type inference. 

576 

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

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

581 

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

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

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

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

586 
is no longer than {\it limit}. 

323  587 
\end{ttdescription} 
104  588 

589 

4317  590 
\section{Programming tools for proof strategies} 
104  591 
Do not consider using the primitives discussed in this section unless you 
323  592 
really need to code tactics from scratch. 
104  593 

6618  594 
\subsection{Operations on tactics} 
3561  595 
\index{tactics!primitives for coding} A tactic maps theorems to sequences of 
596 
theorems. The type constructor for sequences (lazy lists) is called 

4276  597 
\mltydx{Seq.seq}. To simplify the types of tactics and tacticals, 
3561  598 
Isabelle defines a type abbreviation: 
104  599 
\begin{ttbox} 
4276  600 
type tactic = thm > thm Seq.seq 
104  601 
\end{ttbox} 
3108  602 
The following operations provide means for coding tactics in a clean style. 
104  603 
\begin{ttbox} 
604 
PRIMITIVE : (thm > thm) > tactic 

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

606 
\end{ttbox} 

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

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

611 
sequence. 

104  612 

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

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

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

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

104  618 
\begin{ttbox} 
323  619 
SUBGOAL (fn (t,i) => {\it tacticvalued expression}) 
104  620 
\end{ttbox} 
323  621 
\end{ttdescription} 
104  622 

623 

624 
\subsection{Tracing} 

323  625 
\index{tactics!tracing} 
104  626 
\index{tracing!of tactics} 
627 
\begin{ttbox} 

628 
pause_tac: tactic 

629 
print_tac: tactic 

630 
\end{ttbox} 

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

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

634 
options. 

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

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

104  640 

641 
\item[\ttindexbold{print_tac}] 

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

643 
the terminal. 

323  644 
\end{ttdescription} 
104  645 

646 

4276  647 
\section{*Sequences} 
104  648 
\index{sequences (lazy lists)bold} 
4276  649 
The module {\tt Seq} declares a type of lazy lists. It uses 
323  650 
Isabelle's type \mltydx{option} to represent the possible presence 
104  651 
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of 
652 
a value: 

653 
\begin{ttbox} 

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

655 
\end{ttbox} 

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

323  659 
\subsection{Basic operations on sequences} 
104  660 
\begin{ttbox} 
4276  661 
Seq.empty : 'a seq 
662 
Seq.make : (unit > ('a * 'a seq) option) > 'a seq 

663 
Seq.single : 'a > 'a seq 

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

104  665 
\end{ttbox} 
323  666 
\begin{ttdescription} 
4276  667 
\item[Seq.empty] is the empty sequence. 
104  668 

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

104  671 

4276  672 
\item[Seq.single $x$] 
104  673 
constructs the sequence containing the single element~$x$. 
674 

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

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

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

323  679 
\end{ttdescription} 
104  680 

681 

323  682 
\subsection{Converting between sequences and lists} 
104  683 
\begin{ttbox} 
4276  684 
Seq.chop : int * 'a seq > 'a list * 'a seq 
685 
Seq.list_of : 'a seq > 'a list 

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

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

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

692 

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

694 
finite, as a list. 

695 

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

697 
of~$xs$. 

323  698 
\end{ttdescription} 
104  699 

700 

323  701 
\subsection{Combining sequences} 
104  702 
\begin{ttbox} 
4276  703 
Seq.append : 'a seq * 'a seq > 'a seq 
704 
Seq.interleave : 'a seq * 'a seq > 'a seq 

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

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

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

104  708 
\end{ttbox} 
323  709 
\begin{ttdescription} 
4276  710 
\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$. 
711 

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

713 
interleaving their elements. The result contains all the elements 

714 
of the sequences, even if both are infinite. 

715 

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

717 

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

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

720 

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

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

323  723 
\end{ttdescription} 
104  724 

725 
\index{tactics)} 

5371  726 

727 

728 
%%% Local Variables: 

729 
%%% mode: latex 

730 
%%% TeXmaster: "ref" 

731 
%%% End: 