author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 10347  c0cfc4ac12e2 
child 17818  38c889d77282 
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 

10347  108 
\subsection{Explicit instantiation} \label{res_inst_tac} 
323  109 
\index{tactics!instantiation}\index{instantiation} 
104  110 
\begin{ttbox} 
10347  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 
instantiate_tac : (string*string)list > tactic 

104  116 
\end{ttbox} 
10347  117 
The first four of these tactics are designed for applying rules by resolution 
118 
such as substitution and induction, which cause difficulties for higherorder 

119 
unification. The tactics accept explicit instantiations for unknowns 

120 
in the rule typically, in the rule's conclusion. The last one, 

121 
{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state, 

122 
independently of rule application. 

123 

124 
Each instantiation is a pair {\tt($v$,$e$)}, 

125 
where $v$ is an unknown \emph{without} its leading question mark! 

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

104  129 
sort~$s$, and $e$ should be a type of sort $s$. 
130 

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

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

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

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

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

104  143 
failure because the tactics cannot instantiate them. 
144 

10347  145 
The first four instantiation tactics act on a given subgoal. Terms in the 
104  146 
instantiations are typechecked in the context of that subgoal  in 
147 
particular, they may refer to that subgoal's parameters. Any unknowns in 

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

149 
may not refer to unknowns in the subgoal. 

150 

323  151 
\begin{ttdescription} 
104  152 
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}] 
153 
instantiates the rule {\it thm} with the instantiations {\it insts}, as 

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

155 
typically causes further instantiations; you need not give explicit 

332  156 
instantiations for every unknown in the rule. 
104  157 

158 
\item[\ttindexbold{eres_inst_tac}] 

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

160 

161 
\item[\ttindexbold{dres_inst_tac}] 

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

163 

164 
\item[\ttindexbold{forw_inst_tac}] 

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

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

167 
result as a new assumption. 

10347  168 

169 
\item[\ttindexbold{instantiate_tac} {\it insts}] 

170 
instantiates unknowns in the proof state. This affects the main goal as 

171 
well as all subgoals. 

323  172 
\end{ttdescription} 
104  173 

174 

175 
\section{Other basic tactics} 

176 
\subsection{Tactic shortcuts} 

323  177 
\index{shortcuts!for tactics} 
104  178 
\index{tactics!resolution}\index{tactics!assumption} 
179 
\index{tactics!metarewriting} 

180 
\begin{ttbox} 

7491  181 
rtac : thm > int > tactic 
182 
etac : thm > int > tactic 

183 
dtac : thm > int > tactic 

184 
ftac : thm > int > tactic 

185 
atac : int > tactic 

186 
eatac : thm > int > int > tactic 

187 
datac : thm > int > int > tactic 

188 
fatac : thm > int > int > tactic 

189 
ares_tac : thm list > int > tactic 

190 
rewtac : thm > tactic 

104  191 
\end{ttbox} 
192 
These abbreviate common uses of tactics. 

323  193 
\begin{ttdescription} 
104  194 
\item[\ttindexbold{rtac} {\it thm} {\it i}] 
195 
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution. 

196 

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

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

199 

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

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

202 
destructresolution. 

203 

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

206 
destructresolution without deleting the assumption. 

207 

104  208 
\item[\ttindexbold{atac} {\it i}] 
332  209 
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption. 
104  210 

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

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

214 

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

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

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

218 

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

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

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

222 

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

225 
\begin{ttbox} 

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

227 
\end{ttbox} 

228 

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

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

323  231 
\end{ttdescription} 
104  232 

233 

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

323  235 
\index{tactics!for inserting facts}\index{assumptions!inserting} 
104  236 
\begin{ttbox} 
237 
cut_facts_tac : thm list > int > tactic 

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

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

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

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

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

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

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

251 
could state the goal with an outermost metaquantifier. 

252 

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

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

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

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

9568  259 
adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same 
104  260 
{\it formula} as a new subgoal, $i+1$. 
457  261 

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

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

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

323  265 
\end{ttdescription} 
104  266 

267 

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

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

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

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

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

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

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

274 
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

275 
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

276 
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

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

278 

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

279 
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

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

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

282 

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

283 

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

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

286 
\index{definitions} 
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 
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

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

292 
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

293 
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

294 
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

295 

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

296 
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

297 
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

298 
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

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

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

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

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

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

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

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

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

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

308 
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

309 
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

310 
particular subgoal. 
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{rewrite_tac} {\it defs}] 
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset

313 
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

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

315 

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

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

317 
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

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

319 

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

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

321 
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

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

323 

4317  324 
\begin{warn} 
325 
These tactics only cope with definitions expressed as metalevel 

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

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

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

329 
\end{warn} 

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

330 

104  331 
\subsection{Theorems useful with tactics} 
323  332 
\index{theorems!of pure theory} 
104  333 
\begin{ttbox} 
334 
asm_rl: thm 

335 
cut_rl: thm 

336 
\end{ttbox} 

323  337 
\begin{ttdescription} 
338 
\item[\tdx{asm_rl}] 

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

341 
\begin{ttbox} 

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

343 
\end{ttbox} 

344 

323  345 
\item[\tdx{cut_rl}] 
104  346 
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting 
323  347 
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac} 
348 
and {\tt subgoal_tac}. 

349 
\end{ttdescription} 

104  350 

351 

352 
\section{Obscure tactics} 

1212  353 

323  354 
\subsection{Renaming parameters in a goal} \index{parameters!renaming} 
104  355 
\begin{ttbox} 
356 
rename_tac : string > int > tactic 

357 
rename_last_tac : string > string list > int > tactic 

358 
Logic.set_rename_prefix : string > unit 

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

360 
\end{ttbox} 

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

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

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

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

365 
$\forall$bound variable in the conclusion. 

366 

367 
Sometimes there is insufficient information and Isabelle chooses an 

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

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

323  370 
{\tt by} command prints the message {\tt Warning:\ same as previous 
104  371 
level}. 
372 

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

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

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

376 
prefix. They are ugly but predictable. 

377 

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

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

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

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

384 
to ensure that all the parameters are distinct. 

385 

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

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

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

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

390 

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

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

393 
is {\tt"k"}. 

394 

4317  395 
\item[set \ttindexbold{Logic.auto_rename};] 
104  396 
makes Isabelle generate uniform names for parameters. 
323  397 
\end{ttdescription} 
104  398 

399 

2612  400 
\subsection{Manipulating assumptions} 
401 
\index{assumptions!rotating} 

402 
\begin{ttbox} 

403 
thin_tac : string > int > tactic 

404 
rotate_tac : int > int > tactic 

405 
\end{ttbox} 

406 
\begin{ttdescription} 

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

408 
\index{assumptions!deleting} 

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

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

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

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

413 

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

415 
\index{assumptions!rotating} 

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

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

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

419 
processes assumptions from left to right. 

420 
\end{ttdescription} 

421 

422 

423 
\subsection{Tidying the proof state} 

3400  424 
\index{duplicate subgoals!removing} 
2612  425 
\index{parameters!removing unused} 
426 
\index{flexflex constraints} 

427 
\begin{ttbox} 

3400  428 
distinct_subgoals_tac : tactic 
429 
prune_params_tac : tactic 

430 
flexflex_tac : tactic 

2612  431 
\end{ttbox} 
432 
\begin{ttdescription} 

9695  433 
\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a 
434 
proof state. (These arise especially in ZF, where the subgoals are 

435 
essentially type constraints.) 

3400  436 

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

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

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

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

442 

443 
\item[\ttindexbold{flexflex_tac}] 

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

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

446 
the last step of a proof. 

447 

448 
Flexflex constraints arise from difficult cases of higherorder 

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

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

453 
\end{ttdescription} 

454 

455 

104  456 
\subsection{Composition: resolution without lifting} 
323  457 
\index{tactics!for composition} 
104  458 
\begin{ttbox} 
459 
compose_tac: (bool * thm * int) > int > tactic 

460 
\end{ttbox} 

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

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

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

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

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

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

323  473 
\end{ttdescription} 
104  474 

475 

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

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

480 
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

481 
resolution, and can also detect whether a subgoal is too flexible, 
104  482 
with too many rules applicable. 
483 

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

485 
\index{tactics!resolution} 

486 
\begin{ttbox} 

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

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

489 
subgoals_of_brl : bool*thm > int 

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

491 
\end{ttbox} 

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

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

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

495 
mixture of introduction and elimination rules. 

496 

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

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

501 

502 
\item[\ttindexbold{bimatch_tac}] 

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

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

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

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

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

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

512 

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

514 
returns the result of 

515 
\begin{ttbox} 

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

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

522 

523 

323  524 
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} 
104  525 
\index{discrimination netsbold} 
526 
\index{tactics!resolution} 

527 
\begin{ttbox} 

528 
net_resolve_tac : thm list > int > tactic 

529 
net_match_tac : thm list > int > tactic 

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

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

532 
filt_resolve_tac : thm list > int > int > tactic 

533 
could_unify : term*term>bool 

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

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

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

323  541 
\index{lambda abs@$\lambda$abstractions} 
104  542 
$\lambda$abstractions as unknowns, since they could $\eta$contract to 
543 
anything. 

544 

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

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

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

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

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

550 
useful filters. 

551 

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

553 
elimination rules indexed by their major premise. Isabelle provides 

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

332  557 
goal. To avoid repeatedly constructing the nets, use currying: bind the 
104  558 
resulting tactics to \ML{} identifiers. 
559 

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

563 
resolve_tac}. 

564 

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

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

567 
match_tac}. 

568 

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

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

571 
biresolve_tac}. 

572 

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

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

575 
bimatch_tac}. 

576 

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

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

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

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

581 

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

583 
type inference. 

584 

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

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

589 

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

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

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

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

594 
is no longer than {\it limit}. 

323  595 
\end{ttdescription} 
104  596 

597 

4317  598 
\section{Programming tools for proof strategies} 
104  599 
Do not consider using the primitives discussed in this section unless you 
323  600 
really need to code tactics from scratch. 
104  601 

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

4276  605 
\mltydx{Seq.seq}. To simplify the types of tactics and tacticals, 
3561  606 
Isabelle defines a type abbreviation: 
104  607 
\begin{ttbox} 
4276  608 
type tactic = thm > thm Seq.seq 
104  609 
\end{ttbox} 
3108  610 
The following operations provide means for coding tactics in a clean style. 
104  611 
\begin{ttbox} 
612 
PRIMITIVE : (thm > thm) > tactic 

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

614 
\end{ttbox} 

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

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

619 
sequence. 

104  620 

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

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

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

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

104  626 
\begin{ttbox} 
323  627 
SUBGOAL (fn (t,i) => {\it tacticvalued expression}) 
104  628 
\end{ttbox} 
323  629 
\end{ttdescription} 
104  630 

631 

632 
\subsection{Tracing} 

323  633 
\index{tactics!tracing} 
104  634 
\index{tracing!of tactics} 
635 
\begin{ttbox} 

636 
pause_tac: tactic 

637 
print_tac: tactic 

638 
\end{ttbox} 

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

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

642 
options. 

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

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

104  648 

649 
\item[\ttindexbold{print_tac}] 

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

651 
the terminal. 

323  652 
\end{ttdescription} 
104  653 

654 

4276  655 
\section{*Sequences} 
104  656 
\index{sequences (lazy lists)bold} 
4276  657 
The module {\tt Seq} declares a type of lazy lists. It uses 
323  658 
Isabelle's type \mltydx{option} to represent the possible presence 
104  659 
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of 
660 
a value: 

661 
\begin{ttbox} 

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

663 
\end{ttbox} 

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

323  667 
\subsection{Basic operations on sequences} 
104  668 
\begin{ttbox} 
4276  669 
Seq.empty : 'a seq 
670 
Seq.make : (unit > ('a * 'a seq) option) > 'a seq 

671 
Seq.single : 'a > 'a seq 

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

104  673 
\end{ttbox} 
323  674 
\begin{ttdescription} 
4276  675 
\item[Seq.empty] is the empty sequence. 
104  676 

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

104  679 

4276  680 
\item[Seq.single $x$] 
104  681 
constructs the sequence containing the single element~$x$. 
682 

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

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

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

323  687 
\end{ttdescription} 
104  688 

689 

323  690 
\subsection{Converting between sequences and lists} 
104  691 
\begin{ttbox} 
4276  692 
Seq.chop : int * 'a seq > 'a list * 'a seq 
693 
Seq.list_of : 'a seq > 'a list 

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

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

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

700 

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

702 
finite, as a list. 

703 

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

705 
of~$xs$. 

323  706 
\end{ttdescription} 
104  707 

708 

323  709 
\subsection{Combining sequences} 
104  710 
\begin{ttbox} 
4276  711 
Seq.append : 'a seq * 'a seq > 'a seq 
712 
Seq.interleave : 'a seq * 'a seq > 'a seq 

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

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

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

104  716 
\end{ttbox} 
323  717 
\begin{ttdescription} 
4276  718 
\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$. 
719 

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

721 
interleaving their elements. The result contains all the elements 

722 
of the sequences, even if both are infinite. 

723 

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

725 

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

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

728 

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

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

323  731 
\end{ttdescription} 
104  732 

733 
\index{tactics)} 

5371  734 

735 

736 
%%% Local Variables: 

737 
%%% mode: latex 

738 
%%% TeXmaster: "ref" 

739 
%%% End: 