author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 55547  384bfd19ee61 
permissions  rwrr 
29755  1 
theory Tactic 
2 
imports Base 

3 
begin 

18537  4 

20452  5 
chapter {* Tactical reasoning *} 
18537  6 

34930  7 
text {* Tactical reasoning works by refining an initial claim in a 
20474  8 
backwards fashion, until a solved form is reached. A @{text "goal"} 
9 
consists of several subgoals that need to be solved in order to 

10 
achieve the main statement; zero subgoals means that the proof may 

11 
be finished. A @{text "tactic"} is a refinement operation that maps 

12 
a goal to a lazy sequence of potential successors. A @{text 

34930  13 
"tactical"} is a combinator for composing tactics. *} 
18537  14 

15 

16 
section {* Goals \label{sec:tacticalgoals} *} 

17 

20451  18 
text {* 
29758  19 
Isabelle/Pure represents a goal as a theorem stating that the 
20 
subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> 

21 
C"}. The outermost goal structure is that of a Horn Clause: i.e.\ 

22 
an iterated implication without any quantifiers\footnote{Recall that 

23 
outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic 

24 
variables in the body: @{text "\<phi>[?x]"}. These variables may get 

25 
instantiated during the course of reasoning.}. For @{text "n = 0"} 

26 
a goal is called ``solved''. 

18537  27 

29761  28 
The structure of each subgoal @{text "A\<^sub>i"} is that of a 
29 
general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> 

30 
\<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}. Here @{text 

31 
"x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\ 

32 
arbitrarybutfixed entities of certain types, and @{text 

33 
"H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may 

34 
be assumed locally. Together, this forms the goal context of the 

35 
conclusion @{text B} to be established. The goal hypotheses may be 

36 
again arbitrary Hereditary Harrop Formulas, although the level of 

37 
nesting rarely exceeds 12 in practice. 

18537  38 

20451  39 
The main conclusion @{text C} is internally marked as a protected 
29758  40 
proposition, which is represented explicitly by the notation @{text 
34930  41 
"#C"} here. This ensures that the decomposition into subgoals and 
42 
main conclusion is welldefined for arbitrarily structured claims. 

18537  43 

20451  44 
\medskip Basic goal management is performed via the following 
45 
Isabelle/Pure rules: 

18537  46 

47 
\[ 

48 
\infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad 

20547  49 
\infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}} 
18537  50 
\] 
51 

52 
\medskip The following lowlevel variants admit general reasoning 

53 
with protected propositions: 

54 

55 
\[ 

52456  56 
\infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}} 
57 
\] 

58 
\[ 

59 
\infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}} 

18537  60 
\] 
61 
*} 

62 

63 
text %mlref {* 

64 
\begin{mldecls} 

65 
@{index_ML Goal.init: "cterm > thm"} \\ 

32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset

66 
@{index_ML Goal.finish: "Proof.context > thm > thm"} \\ 
52456  67 
@{index_ML Goal.protect: "int > thm > thm"} \\ 
18537  68 
@{index_ML Goal.conclude: "thm > thm"} \\ 
69 
\end{mldecls} 

70 

71 
\begin{description} 

72 

20474  73 
\item @{ML "Goal.init"}~@{text C} initializes a tactical goal from 
74 
the wellformed proposition @{text C}. 

18537  75 

32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset

76 
\item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem 
20474  77 
@{text "thm"} is a solved goal (no subgoals), and concludes the 
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset

78 
result by removing the goal protection. The context is only 
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset

79 
required for printing error messages. 
18537  80 

52456  81 
\item @{ML "Goal.protect"}~@{text "n thm"} protects the statement 
82 
of theorem @{text "thm"}. The parameter @{text n} indicates the 

83 
number of premises to be retained. 

18537  84 

20474  85 
\item @{ML "Goal.conclude"}~@{text "thm"} removes the goal 
86 
protection, even if there are pending subgoals. 

18537  87 

88 
\end{description} 

89 
*} 

90 

91 

39847  92 
section {* Tactics\label{sec:tactics} *} 
18537  93 

28781  94 
text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that 
95 
maps a given goal state (represented as a theorem, cf.\ 

96 
\secref{sec:tacticalgoals}) to a lazy sequence of potential 

97 
successor states. The underlying sequence implementation is lazy 

98 
both in head and tail, and is purely functional in \emph{not} 

99 
supporting memoing.\footnote{The lack of memoing and the strict 

100 
nature of SML requires some care when working with lowlevel 

101 
sequence operations, to avoid duplicate or premature evaluation of 

34930  102 
results. It also means that modified runtime behavior, such as 
103 
timeout, is very hard to achieve for general tactics.} 

18537  104 

28781  105 
An \emph{empty result sequence} means that the tactic has failed: in 
34930  106 
a compound tactic expression other tactics might be tried instead, 
28781  107 
or the whole refinement step might fail outright, producing a 
34930  108 
toplevel error message in the end. When implementing tactics from 
109 
scratch, one should take care to observe the basic protocol of 

110 
mapping regular error conditions to an empty result; only serious 

111 
faults should emerge as exceptions. 

28781  112 

113 
By enumerating \emph{multiple results}, a tactic can easily express 

114 
the potential outcome of an internal search process. There are also 

115 
combinators for building proof tools that involve search 

116 
systematically, see also \secref{sec:tacticals}. 

117 

34930  118 
\medskip As explained before, a goal state essentially consists of a 
119 
list of subgoals that imply the main goal (conclusion). Tactics may 

120 
operate on all subgoals or on a particularly specified subgoal, but 

121 
must not change the main conclusion (apart from instantiating 

122 
schematic goal variables). 

18537  123 

28781  124 
Tactics with explicit \emph{subgoal addressing} are of the form 
125 
@{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal 

126 
(counting from 1). If the subgoal number is out of range, the 

127 
tactic should fail with an empty result sequence, but must not raise 

128 
an exception! 

129 

130 
Operating on a particular subgoal means to replace it by an interval 

131 
of zero or more subgoals in the same place; other subgoals must not 

132 
be affected, apart from instantiating schematic variables ranging 

133 
over the whole goal state. 

134 

135 
A common pattern of composing tactics with subgoal addressing is to 

136 
try the first one, and then the second one only if the subgoal has 

137 
not been solved yet. Special care is required here to avoid bumping 

28782  138 
into unrelated subgoals that happen to come after the original 
139 
subgoal. Assuming that there is only a single initial subgoal is a 

140 
very common error when implementing tactics! 

141 

142 
Tactics with internal subgoal addressing should expose the subgoal 

143 
index as @{text "int"} argument in full generality; a hardwired 

34930  144 
subgoal 1 is not acceptable. 
28781  145 

146 
\medskip The main wellformedness conditions for proper tactics are 

147 
summarized as follows. 

148 

149 
\begin{itemize} 

150 

151 
\item General tactic failure is indicated by an empty result, only 

152 
serious faults may produce an exception. 

153 

154 
\item The main conclusion must not be changed, apart from 

155 
instantiating schematic variables. 

156 

157 
\item A tactic operates either uniformly on all subgoals, or 

158 
specifically on a selected subgoal (without bumping into unrelated 

159 
subgoals). 

160 

161 
\item Range errors in subgoal addressing produce an empty result. 

162 

163 
\end{itemize} 

28782  164 

165 
Some of these conditions are checked by higherlevel goal 

34930  166 
infrastructure (\secref{sec:structgoals}); others are not checked 
28782  167 
explicitly, and violating them merely results in illbehaved tactics 
168 
experienced by the user (e.g.\ tactics that insist in being 

34930  169 
applicable only to singleton goals, or prevent composition via 
46260  170 
standard tacticals such as @{ML REPEAT}). 
28782  171 
*} 
172 

173 
text %mlref {* 

174 
\begin{mldecls} 

175 
@{index_ML_type tactic: "thm > thm Seq.seq"} \\ 

28783  176 
@{index_ML no_tac: tactic} \\ 
177 
@{index_ML all_tac: tactic} \\ 

178 
@{index_ML print_tac: "string > tactic"} \\[1ex] 

179 
@{index_ML PRIMITIVE: "(thm > thm) > tactic"} \\[1ex] 

28782  180 
@{index_ML SUBGOAL: "(term * int > tactic) > int > tactic"} \\ 
181 
@{index_ML CSUBGOAL: "(cterm * int > tactic) > int > tactic"} \\ 

52463  182 
@{index_ML SELECT_GOAL: "tactic > int > tactic"} \\ 
183 
@{index_ML PREFER_GOAL: "tactic > int > tactic"} \\ 

28782  184 
\end{mldecls} 
185 

186 
\begin{description} 

187 

39864  188 
\item Type @{ML_type tactic} represents tactics. The 
189 
wellformedness conditions described above need to be observed. See 

40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
39864
diff
changeset

190 
also @{file "~~/src/Pure/General/seq.ML"} for the underlying 
39864  191 
implementation of lazy sequences. 
28782  192 

39864  193 
\item Type @{ML_type "int > tactic"} represents tactics with 
194 
explicit subgoal addressing, with wellformedness conditions as 

195 
described above. 

28782  196 

28783  197 
\item @{ML no_tac} is a tactic that always fails, returning the 
198 
empty sequence. 

199 

200 
\item @{ML all_tac} is a tactic that always succeeds, returning a 

201 
singleton sequence with unchanged goal state. 

202 

203 
\item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but 

204 
prints a message together with the goal state on the tracing 

205 
channel. 

206 

28782  207 
\item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule 
208 
into a tactic with unique result. Exception @{ML THM} is considered 

209 
a regular tactic failure and produces an empty result; other 

210 
exceptions are passed through. 

211 

212 
\item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the 

28783  213 
most basic form to produce a tactic with subgoal addressing. The 
28782  214 
given abstraction over the subgoal term and subgoal number allows to 
215 
peek at the relevant information of the full goal state. The 

216 
subgoal range is checked as required above. 

217 

218 
\item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the 

28783  219 
subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This 
28782  220 
avoids expensive recertification in situations where the subgoal is 
221 
used directly for primitive inferences. 

222 

52463  223 
\item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the 
224 
specified subgoal @{text "i"}. This rearranges subgoals and the 

225 
main goal protection (\secref{sec:tacticalgoals}), while retaining 

226 
the syntactic context of the overall goal state (concerning 

227 
schematic variables etc.). 

228 

229 
\item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put 

230 
@{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but 

231 
without changing the main goal protection. 

232 

28782  233 
\end{description} 
28781  234 
*} 
18537  235 

236 

28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

237 
subsection {* Resolution and assumption tactics \label{sec:resolveassumetac} *} 
28783  238 

239 
text {* \emph{Resolution} is the most basic mechanism for refining a 

240 
subgoal using a theorem as objectlevel rule. 

241 
\emph{Elimresolution} is particularly suited for elimination rules: 

242 
it resolves with a rule, proves its first premise by assumption, and 

243 
finally deletes that assumption from any new subgoals. 

244 
\emph{Destructresolution} is like elimresolution, but the given 

245 
destruction rules are first turned into canonical elimination 

246 
format. \emph{Forwardresolution} is like destructresolution, but 

28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

247 
without deleting the selected assumption. The @{text "r/e/d/f"} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

248 
naming convention is maintained for several different kinds of 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

249 
resolution rules and tactics. 
28783  250 

251 
Assumption tactics close a subgoal by unifying some of its premises 

252 
against its conclusion. 

253 

254 
\medskip All the tactics in this section operate on a subgoal 

255 
designated by a positive integer. Other subgoals might be affected 

256 
indirectly, due to instantiation of schematic variables. 

257 

258 
There are various sources of nondeterminism, the tactic result 

259 
sequence enumerates all possibilities of the following choices (if 

260 
applicable): 

261 

262 
\begin{enumerate} 

263 

264 
\item selecting one of the rules given as argument to the tactic; 

265 

266 
\item selecting a subgoal premise to eliminate, unifying it against 

267 
the first premise of the rule; 

268 

269 
\item unifying the conclusion of the subgoal to the conclusion of 

270 
the rule. 

271 

272 
\end{enumerate} 

273 

274 
Recall that higherorder unification may produce multiple results 

275 
that are enumerated here. 

276 
*} 

277 

278 
text %mlref {* 

279 
\begin{mldecls} 

280 
@{index_ML resolve_tac: "thm list > int > tactic"} \\ 

281 
@{index_ML eresolve_tac: "thm list > int > tactic"} \\ 

282 
@{index_ML dresolve_tac: "thm list > int > tactic"} \\ 

50072  283 
@{index_ML forward_tac: "thm list > int > tactic"} \\ 
284 
@{index_ML biresolve_tac: "(bool * thm) list > int > tactic"} \\[1ex] 

28783  285 
@{index_ML assume_tac: "int > tactic"} \\ 
286 
@{index_ML eq_assume_tac: "int > tactic"} \\[1ex] 

287 
@{index_ML match_tac: "thm list > int > tactic"} \\ 

288 
@{index_ML ematch_tac: "thm list > int > tactic"} \\ 

289 
@{index_ML dmatch_tac: "thm list > int > tactic"} \\ 

50072  290 
@{index_ML bimatch_tac: "(bool * thm) list > int > tactic"} \\ 
28783  291 
\end{mldecls} 
292 

293 
\begin{description} 

294 

295 
\item @{ML resolve_tac}~@{text "thms i"} refines the goal state 

296 
using the given theorems, which should normally be introduction 

297 
rules. The tactic resolves a rule's conclusion with subgoal @{text 

298 
i}, replacing it by the corresponding versions of the rule's 

299 
premises. 

300 

301 
\item @{ML eresolve_tac}~@{text "thms i"} performs elimresolution 

46278  302 
with the given theorems, which are normally be elimination rules. 
303 

304 
Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML 

305 
assume_tac}, which facilitates mixing of assumption steps with 

306 
genuine eliminations. 

28783  307 

308 
\item @{ML dresolve_tac}~@{text "thms i"} performs 

309 
destructresolution with the given theorems, which should normally 

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

311 
applying one of the rules. 

312 

313 
\item @{ML forward_tac} is like @{ML dresolve_tac} except that the 

314 
selected assumption is not deleted. It applies a rule to an 

315 
assumption, adding the result as a new assumption. 

316 

50072  317 
\item @{ML biresolve_tac}~@{text "brls i"} refines the proof state 
318 
by resolution or elimresolution on each rule, as indicated by its 

319 
flag. It affects subgoal @{text "i"} of the proof state. 

320 

321 
For each pair @{text "(flag, rule)"}, it applies resolution if the 

322 
flag is @{text "false"} and elimresolution if the flag is @{text 

323 
"true"}. A single tactic call handles a mixture of introduction and 

324 
elimination rules, which is useful to organize the search process 

325 
systematically in proof tools. 

326 

28783  327 
\item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i} 
328 
by assumption (modulo higherorder unification). 

329 

330 
\item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks 

331 
only for immediate @{text "\<alpha>"}convertibility instead of using 

332 
unification. It succeeds (with a unique next state) if one of the 

333 
assumptions is equal to the subgoal's conclusion. Since it does not 

334 
instantiate variables, it cannot make other subgoals unprovable. 

335 

50072  336 
\item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML 
337 
bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac}, 

338 
@{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do 

53096  339 
not instantiate schematic variables in the goal state.% 
340 
\footnote{Strictly speaking, matching means to treat the unknowns in the goal 

341 
state as constants, but these tactics merely discard unifiers that would 

342 
update the goal state. In rare situations (where the conclusion and 

343 
goal state have flexible terms at the same position), the tactic 

344 
will fail even though an acceptable unifier exists.} 

345 
These tactics were written for a specific application within the classical reasoner. 

28783  346 

347 
Flexible subgoals are not updated at will, but are left alone. 

348 
\end{description} 

349 
*} 

350 

351 

28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

352 
subsection {* Explicit instantiation within a subgoal context *} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

353 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

354 
text {* The main resolution tactics (\secref{sec:resolveassumetac}) 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

355 
use higherorder unification, which works well in many practical 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

356 
situations despite its daunting theoretical properties. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

357 
Nonetheless, there are important problem classes where unguided 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

358 
higherorder unification is not so useful. This typically involves 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

359 
rules like universal elimination, existential introduction, or 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

360 
equational substitution. Here the unification problem involves 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

361 
fully flexible @{text "?P ?x"} schemes, which are hard to manage 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

362 
without further hints. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

363 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

364 
By providing a (small) rigid term for @{text "?x"} explicitly, the 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

365 
remaining unification problem is to assign a (large) term to @{text 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

366 
"?P"}, according to the shape of the given subgoal. This is 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

367 
sufficiently wellbehaved in most practical situations. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

368 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

369 
\medskip Isabelle provides separate versions of the standard @{text 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

370 
"r/e/d/f"} resolution tactics that allow to provide explicit 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

371 
instantiations of unknowns of the given rule, wrt.\ terms that refer 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

372 
to the implicit context of the selected subgoal. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

373 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

374 
An instantiation consists of a list of pairs of the form @{text 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

375 
"(?x, t)"}, where @{text ?x} is a schematic variable occurring in 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

376 
the given rule, and @{text t} is a term from the current proof 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

377 
context, augmented by the local goal parameters of the selected 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

378 
subgoal; cf.\ the @{text "focus"} operation described in 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

379 
\secref{sec:variables}. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

380 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

381 
Entering the syntactic context of a subgoal is a brittle operation, 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

382 
because its exact form is somewhat accidental, and the choice of 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

383 
bound variable names depends on the presence of other local and 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

384 
global names. Explicit renaming of subgoal parameters prior to 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

385 
explicit instantiation might help to achieve a bit more robustness. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

386 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

387 
Type instantiations may be given as well, via pairs like @{text 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

388 
"(?'a, \<tau>)"}. Type instantiations are distinguished from term 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

389 
instantiations by the syntactic form of the schematic variable. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

390 
Types are instantiated before terms are. Since term instantiation 
34930  391 
already performs simple typeinference, so explicit type 
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

392 
instantiations are seldom necessary. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

393 
*} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

394 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

395 
text %mlref {* 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

396 
\begin{mldecls} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

397 
@{index_ML res_inst_tac: "Proof.context > (indexname * string) list > thm > int > tactic"} \\ 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

398 
@{index_ML eres_inst_tac: "Proof.context > (indexname * string) list > thm > int > tactic"} \\ 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

399 
@{index_ML dres_inst_tac: "Proof.context > (indexname * string) list > thm > int > tactic"} \\ 
46271  400 
@{index_ML forw_inst_tac: "Proof.context > (indexname * string) list > thm > int > tactic"} \\ 
401 
@{index_ML subgoal_tac: "Proof.context > string > int > tactic"} \\ 

46277  402 
@{index_ML thin_tac: "Proof.context > string > int > tactic"} \\ 
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

403 
@{index_ML rename_tac: "string list > int > tactic"} \\ 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

404 
\end{mldecls} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

405 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

406 
\begin{description} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

407 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

408 
\item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

409 
rule @{text thm} with the instantiations @{text insts}, as described 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

410 
above, and then performs resolution on subgoal @{text i}. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

411 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

412 
\item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

413 
elimresolution. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

414 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

415 
\item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

416 
destructresolution. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

417 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

418 
\item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

419 
the selected assumption is not deleted. 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

420 

46271  421 
\item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition 
422 
@{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the 

423 
same as a new subgoal @{text "i + 1"} (in the original context). 

424 

46277  425 
\item @{ML thin_tac}~@{text "ctxt \<phi> i"} deletes the specified 
426 
premise from subgoal @{text i}. Note that @{text \<phi>} may contain 

427 
schematic variables, to abbreviate the intended proposition; the 

428 
first matching subgoal premise will be deleted. Removing useless 

429 
premises from a subgoal increases its readability and can make 

430 
search tactics run faster. 

431 

28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

432 
\item @{ML rename_tac}~@{text "names i"} renames the innermost 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

433 
parameters of subgoal @{text i} according to the provided @{text 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

434 
names} (which need to be distinct indentifiers). 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

435 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

436 
\end{description} 
34930  437 

438 
For historical reasons, the above instantiation tactics take 

439 
unparsed string arguments, which makes them hard to use in general 

440 
ML code. The slightly more advanced @{ML Subgoal.FOCUS} combinator 

441 
of \secref{sec:structgoals} allows to refer to internal goal 

442 
structure with explicit context management. 

28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

443 
*} 
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

444 

64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset

445 

46274  446 
subsection {* Rearranging goal states *} 
447 

448 
text {* In rare situations there is a need to rearrange goal states: 

449 
either the overall collection of subgoals, or the local structure of 

450 
a subgoal. Various administrative tactics allow to operate on the 

451 
concrete presentation these conceptual sets of formulae. *} 

452 

453 
text %mlref {* 

454 
\begin{mldecls} 

455 
@{index_ML rotate_tac: "int > int > tactic"} \\ 

46276  456 
@{index_ML distinct_subgoals_tac: tactic} \\ 
457 
@{index_ML flexflex_tac: tactic} \\ 

46274  458 
\end{mldecls} 
459 

460 
\begin{description} 

461 

462 
\item @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal 

463 
@{text i} by @{text n} positions: from right to left if @{text n} is 

464 
positive, and from left to right if @{text n} is negative. 

465 

46276  466 
\item @{ML distinct_subgoals_tac} removes duplicate subgoals from a 
467 
proof state. This is potentially inefficient. 

468 

469 
\item @{ML flexflex_tac} removes all flexflex pairs from the proof 

470 
state by applying the trivial unifier. This drastic step loses 

471 
information. It is already part of the Isar infrastructure for 

472 
facts resulting from goals, and rarely needs to be invoked manually. 

473 

474 
Flexflex constraints arise from difficult cases of higherorder 

475 
unification. To prevent this, use @{ML res_inst_tac} to instantiate 

476 
some variables in a rule. Normally flexflex constraints can be 

477 
ignored; they often disappear as unknowns get instantiated. 

478 

46274  479 
\end{description} 
480 
*} 

481 

50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

482 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

483 
subsection {* Raw composition: resolution without lifting *} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

484 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

485 
text {* 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

486 
Raw composition of two rules means resolving them without prior 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

487 
lifting or renaming of unknowns. This lowlevel operation, which 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

488 
underlies the resolution tactics, may occasionally be useful for 
52467  489 
special effects. Schematic variables are not renamed by default, so 
490 
beware of clashes! 

50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

491 
*} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

492 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

493 
text %mlref {* 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

494 
\begin{mldecls} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

495 
@{index_ML compose_tac: "(bool * thm * int) > int > tactic"} \\ 
52467  496 
@{index_ML Drule.compose: "thm * int * thm > thm"} \\ 
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

497 
@{index_ML_op COMP: "thm * thm > thm"} \\ 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

498 
\end{mldecls} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

499 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

500 
\begin{description} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

501 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

502 
\item @{ML compose_tac}~@{text "(flag, rule, m) i"} refines subgoal 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

503 
@{text "i"} using @{text "rule"}, without lifting. The @{text 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

504 
"rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

505 
@{text "\<psi>"} need not be atomic; thus @{text "m"} determines the 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

506 
number of new subgoals. If @{text "flag"} is @{text "true"} then it 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

507 
performs elimresolution  it solves the first premise of @{text 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

508 
"rule"} by assumption and deletes that assumption. 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

509 

52465  510 
\item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"}, 
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

511 
regarded as an atomic formula, to solve premise @{text "i"} of 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

512 
@{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text 
52467  513 
"\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. The unique @{text "s"} that 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52820
diff
changeset

514 
unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow> 
52467  515 
\<dots> \<phi>\<^sub>i\<^sub>\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}. Multiple results are considered as 
516 
error (exception @{ML THM}). 

50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

517 

52467  518 
\item @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose 
519 
(thm\<^sub>1, 1, thm\<^sub>2)"}. 

50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

520 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

521 
\end{description} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

522 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

523 
\begin{warn} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

524 
These lowlevel operations are stepping outside the structure 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

525 
imposed by regular rule resolution. Used without understanding of 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

526 
the consequences, they may produce results that cause problems with 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

527 
standard rules and tactics later on. 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

528 
\end{warn} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

529 
*} 
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

530 

0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset

531 

28781  532 
section {* Tacticals \label{sec:tacticals} *} 
18537  533 

46258  534 
text {* A \emph{tactical} is a functional combinator for building up 
535 
complex tactics from simpler ones. Common tacticals perform 

536 
sequential composition, disjunctive choice, iteration, or goal 

537 
addressing. Various search strategies may be expressed via 

538 
tacticals. 

46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

539 
*} 
46258  540 

541 

542 
subsection {* Combining tactics *} 

543 

544 
text {* Sequential composition and alternative choices are the most 

545 
basic ways to combine tactics, similarly to ``@{verbatim ","}'' and 

546 
``@{verbatim ""}'' in Isar method notation. This corresponds to 

46262  547 
@{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further 
548 
possibilities for finetuning alternation of tactics such as @{ML_op 

46258  549 
"APPEND"}. Further details become visible in ML due to explicit 
46262  550 
subgoal addressing. 
551 
*} 

46258  552 

553 
text %mlref {* 

554 
\begin{mldecls} 

46262  555 
@{index_ML_op "THEN": "tactic * tactic > tactic"} \\ 
556 
@{index_ML_op "ORELSE": "tactic * tactic > tactic"} \\ 

557 
@{index_ML_op "APPEND": "tactic * tactic > tactic"} \\ 

46258  558 
@{index_ML "EVERY": "tactic list > tactic"} \\ 
559 
@{index_ML "FIRST": "tactic list > tactic"} \\[0.5ex] 

560 

46262  561 
@{index_ML_op "THEN'": "('a > tactic) * ('a > tactic) > 'a > tactic"} \\ 
562 
@{index_ML_op "ORELSE'": "('a > tactic) * ('a > tactic) > 'a > tactic"} \\ 

563 
@{index_ML_op "APPEND'": "('a > tactic) * ('a > tactic) > 'a > tactic"} \\ 

46258  564 
@{index_ML "EVERY'": "('a > tactic) list > 'a > tactic"} \\ 
565 
@{index_ML "FIRST'": "('a > tactic) list > 'a > tactic"} \\ 

566 
\end{mldecls} 

567 

568 
\begin{description} 

18537  569 

46262  570 
\item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential 
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

571 
composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

572 
state, it returns all states reachable in two steps by applying 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

573 
@{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it applies @{text 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

574 
"tac\<^sub>1"} to the goal state, getting a sequence of possible next 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

575 
states; then, it applies @{text "tac\<^sub>2"} to each of these and 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

576 
concatenates the results to produce again one flat sequence of 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

577 
states. 
46258  578 

46262  579 
\item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice 
580 
between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it 

581 
tries @{text "tac\<^sub>1"} and returns the result if nonempty; if @{text 

582 
"tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}. This is a deterministic 

583 
choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded 

584 
from the result. 

46258  585 

46262  586 
\item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the 
587 
possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike 

588 
@{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so 

589 
@{ML_op "APPEND"} helps to avoid incompleteness during search, at 

590 
the cost of potential inefficiencies. 

39852  591 

46262  592 
\item @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text 
593 
"tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}. 

594 
Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always 

595 
succeeds. 

46258  596 

46262  597 
\item @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text 
598 
"tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text 

599 
"tac\<^sub>n"}. Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it 

600 
always fails. 

46258  601 

46264  602 
\item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for 
46266  603 
tactics with explicit subgoal addressing. So @{text 
46264  604 
"(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text 
605 
"(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}. 

46258  606 

46264  607 
The other primed tacticals work analogously. 
46258  608 

609 
\end{description} 

610 
*} 

30272  611 

46259  612 

613 
subsection {* Repetition tacticals *} 

614 

615 
text {* These tacticals provide further control over repetition of 

616 
tactics, beyond the stylized forms of ``@{verbatim "?"}'' and 

617 
``@{verbatim "+"}'' in Isar method expressions. *} 

618 

619 
text %mlref {* 

620 
\begin{mldecls} 

621 
@{index_ML "TRY": "tactic > tactic"} \\ 

46266  622 
@{index_ML "REPEAT": "tactic > tactic"} \\ 
623 
@{index_ML "REPEAT1": "tactic > tactic"} \\ 

46259  624 
@{index_ML "REPEAT_DETERM": "tactic > tactic"} \\ 
625 
@{index_ML "REPEAT_DETERM_N": "int > tactic > tactic"} \\ 

626 
\end{mldecls} 

627 

628 
\begin{description} 

629 

46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

630 
\item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal 
46259  631 
state and returns the resulting sequence, if nonempty; otherwise it 
632 
returns the original state. Thus, it applies @{text "tac"} at most 

633 
once. 

634 

46266  635 
Note that for tactics with subgoal addressing, the combinator can be 
636 
applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text 

637 
"tac"}. There is no need for @{verbatim TRY'}. 

46259  638 

46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

639 
\item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal 
46259  640 
state and, recursively, to each element of the resulting sequence. 
641 
The resulting sequence consists of those states that make @{text 

642 
"tac"} fail. Thus, it applies @{text "tac"} as many times as 

643 
possible (including zero times), and allows backtracking over each 

644 
invocation of @{text "tac"}. @{ML REPEAT} is more general than @{ML 

645 
REPEAT_DETERM}, but requires more space. 

646 

647 
\item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"} 

648 
but it always applies @{text "tac"} at least once, failing if this 

649 
is impossible. 

650 

46266  651 
\item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the 
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

652 
goal state and, recursively, to the head of the resulting sequence. 
46266  653 
It returns the first state to make @{text "tac"} fail. It is 
654 
deterministic, discarding alternative outcomes. 

655 

656 
\item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML 

657 
REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound 

658 
by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}). 

46259  659 

660 
\end{description} 

661 
*} 

662 

46260  663 
text %mlex {* The basic tactics and tacticals considered above follow 
664 
some algebraic laws: 

46259  665 

46260  666 
\begin{itemize} 
46259  667 

46262  668 
\item @{ML all_tac} is the identity element of the tactical @{ML_op 
669 
"THEN"}. 

46259  670 

46262  671 
\item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and 
672 
@{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"}, 

673 
which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is 

674 
equivalent to @{ML no_tac}. 

46259  675 

46260  676 
\item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) 
677 
functions over more basic combinators (ignoring some internal 

678 
implementation tricks): 

46259  679 

46260  680 
\end{itemize} 
46259  681 
*} 
682 

683 
ML {* 

684 
fun TRY tac = tac ORELSE all_tac; 

685 
fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st; 

686 
*} 

687 

688 
text {* If @{text "tac"} can return multiple outcomes then so can @{ML 

46262  689 
REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML_op "ORELSE"} and not 
690 
@{ML_op "APPEND"}, it applies @{text "tac"} as many times as 

46259  691 
possible in each outcome. 
692 

693 
\begin{warn} 

46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

694 
Note the explicit abstraction over the goal state in the ML 
46260  695 
definition of @{ML REPEAT}. Recursive tacticals must be coded in 
696 
this awkward fashion to avoid infinite recursion of eager functional 

697 
evaluation in Standard ML. The following attempt would make @{ML 

698 
REPEAT}~@{text "tac"} loop: 

46259  699 
\end{warn} 
700 
*} 

701 

702 
ML {* 

46260  703 
(*BAD  does not terminate!*) 
704 
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; 

46259  705 
*} 
706 

46263  707 

46267  708 
subsection {* Applying tactics to subgoal ranges *} 
46263  709 

710 
text {* Tactics with explicit subgoal addressing 

711 
@{ML_type "int > tactic"} can be used together with tacticals that 

712 
act like ``subgoal quantifiers'': guided by success of the body 

713 
tactic a certain range of subgoals is covered. Thus the body tactic 

46267  714 
is applied to \emph{all} subgoals, \emph{some} subgoal etc. 
46263  715 

716 
Suppose that the goal state has @{text "n \<ge> 0"} subgoals. Many of 

717 
these tacticals address subgoal ranges counting downwards from 

718 
@{text "n"} towards @{text "1"}. This has the fortunate effect that 

719 
newly emerging subgoals are concatenated in the result, without 

720 
interfering each other. Nonetheless, there might be situations 

46266  721 
where a different order is desired. *} 
46263  722 

723 
text %mlref {* 

724 
\begin{mldecls} 

725 
@{index_ML ALLGOALS: "(int > tactic) > tactic"} \\ 

726 
@{index_ML SOMEGOAL: "(int > tactic) > tactic"} \\ 

727 
@{index_ML FIRSTGOAL: "(int > tactic) > tactic"} \\ 

46267  728 
@{index_ML HEADGOAL: "(int > tactic) > tactic"} \\ 
46263  729 
@{index_ML REPEAT_SOME: "(int > tactic) > tactic"} \\ 
730 
@{index_ML REPEAT_FIRST: "(int > tactic) > tactic"} \\ 

46267  731 
@{index_ML RANGE: "(int > tactic) list > int > tactic"} \\ 
46263  732 
\end{mldecls} 
733 

734 
\begin{description} 

735 

736 
\item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac 

737 
n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}. It 

738 
applies the @{text tac} to all the subgoals, counting downwards. 

739 

740 
\item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac 

741 
n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}. It 

742 
applies @{text "tac"} to one subgoal, counting downwards. 

743 

744 
\item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac 

745 
1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}. It 

746 
applies @{text "tac"} to one subgoal, counting upwards. 

747 

46267  748 
\item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}. 
749 
It applies @{text "tac"} unconditionally to the first subgoal. 

750 

46263  751 
\item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or 
752 
more to a subgoal, counting downwards. 

753 

754 
\item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or 

755 
more to a subgoal, counting upwards. 

756 

46267  757 
\item @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to 
758 
@{text "tac\<^sub>k (i + k  1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op 

759 
THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the 

760 
corresponding range of subgoals, counting downwards. 

761 

46263  762 
\end{description} 
763 
*} 

764 

46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

765 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

766 
subsection {* Control and search tacticals *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

767 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

768 
text {* A predicate on theorems @{ML_type "thm > bool"} can test 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

769 
whether a goal state enjoys some desirable property  such as 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

770 
having no subgoals. Tactics that search for satisfactory goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

771 
states are easy to express. The main search procedures, 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

772 
depthfirst, breadthfirst and bestfirst, are provided as 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

773 
tacticals. They generate the search tree by repeatedly applying a 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

774 
given tactic. *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

775 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

776 

46270  777 
text %mlref "" 
778 

46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

779 
subsubsection {* Filtering a tactic's results *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

780 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

781 
text {* 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

782 
\begin{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

783 
@{index_ML FILTER: "(thm > bool) > tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

784 
@{index_ML CHANGED: "tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

785 
\end{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

786 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

787 
\begin{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

788 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

789 
\item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

790 
goal state and returns a sequence consisting of those result goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

791 
states that are satisfactory in the sense of @{text "sat"}. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

792 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

793 
\item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

794 
state and returns precisely those states that differ from the 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

795 
original state (according to @{ML Thm.eq_thm}). Thus @{ML 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

796 
CHANGED}~@{text "tac"} always has some effect on the state. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

797 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

798 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

799 
*} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

800 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

801 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

802 
subsubsection {* Depthfirst search *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

803 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

804 
text {* 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

805 
\begin{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

806 
@{index_ML DEPTH_FIRST: "(thm > bool) > tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

807 
@{index_ML DEPTH_SOLVE: "tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

808 
@{index_ML DEPTH_SOLVE_1: "tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

809 
\end{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

810 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

811 
\begin{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

812 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

813 
\item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

814 
@{text "sat"} returns true. Otherwise it applies @{text "tac"}, 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

815 
then recursively searches from each element of the resulting 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

816 
sequence. The code uses a stack for efficiency, in effect applying 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

817 
@{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

818 
the state. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

819 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

820 
\item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

821 
search for states having no subgoals. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

822 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

823 
\item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

824 
search for states having fewer subgoals than the given state. Thus, 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

825 
it insists upon solving at least one subgoal. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

826 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

827 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

828 
*} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

829 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

830 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

831 
subsubsection {* Other search strategies *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

832 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

833 
text {* 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

834 
\begin{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

835 
@{index_ML BREADTH_FIRST: "(thm > bool) > tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

836 
@{index_ML BEST_FIRST: "(thm > bool) * (thm > int) > tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

837 
@{index_ML THEN_BEST_FIRST: "tactic > (thm > bool) * (thm > int) > tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

838 
\end{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

839 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

840 
These search strategies will find a solution if one exists. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

841 
However, they do not enumerate all solutions; they terminate after 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

842 
the first satisfactory result from @{text "tac"}. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

843 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

844 
\begin{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

845 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

846 
\item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadthfirst 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

847 
search to find states for which @{text "sat"} is true. For most 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

848 
applications, it is too slow. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

849 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

850 
\item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

851 
search, using @{text "dist"} to estimate the distance from a 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

852 
satisfactory state (in the sense of @{text "sat"}). It maintains a 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

853 
list of states ordered by distance. It applies @{text "tac"} to the 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

854 
head of this list; if the result contains any satisfactory states, 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

855 
then it returns them. Otherwise, @{ML BEST_FIRST} adds the new 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

856 
states to the list, and continues. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

857 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

858 
The distance function is typically @{ML size_of_thm}, which computes 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

859 
the size of the state. The smaller the state, the fewer and simpler 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

860 
subgoals it has. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

861 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

862 
\item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

863 
@{ML BEST_FIRST}, except that the priority queue initially contains 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

864 
the result of applying @{text "tac\<^sub>0"} to the goal state. This 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

865 
tactical permits separate tactics for starting the search and 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

866 
continuing the search. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

867 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

868 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

869 
*} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

870 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

871 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

872 
subsubsection {* Auxiliary tacticals for searching *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

873 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

874 
text {* 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

875 
\begin{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

876 
@{index_ML COND: "(thm > bool) > tactic > tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

877 
@{index_ML IF_UNSOLVED: "tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

878 
@{index_ML SOLVE: "tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

879 
@{index_ML DETERM: "tactic > tactic"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

880 
\end{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

881 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

882 
\begin{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

883 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

884 
\item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

885 
the goal state if it satisfies predicate @{text "sat"}, and applies 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

886 
@{text "tac\<^sub>2"}. It is a conditional tactical in that only one of 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

887 
@{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

888 
However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

889 
because ML uses eager evaluation. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

890 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

891 
\item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

892 
goal state if it has any subgoals, and simply returns the goal state 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

893 
otherwise. Many common tactics, such as @{ML resolve_tac}, fail if 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

894 
applied to a goal state that has no subgoals. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

895 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

896 
\item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

897 
state and then fails iff there are subgoals left. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

898 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

899 
\item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

900 
state and returns the head of the resulting sequence. @{ML DETERM} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

901 
limits the search space by making its argument deterministic. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

902 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

903 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

904 
*} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

905 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

906 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

907 
subsubsection {* Predicates and functions useful for searching *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

908 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

909 
text {* 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

910 
\begin{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

911 
@{index_ML has_fewer_prems: "int > thm > bool"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

912 
@{index_ML Thm.eq_thm: "thm * thm > bool"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

913 
@{index_ML Thm.eq_thm_prop: "thm * thm > bool"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

914 
@{index_ML size_of_thm: "thm > int"} \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

915 
\end{mldecls} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

916 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

917 
\begin{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

918 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

919 
\item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

920 
"thm"} has fewer than @{text "n"} premises. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

921 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

922 
\item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text 
55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOLIMP);
wenzelm
parents:
53096
diff
changeset

923 
"thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the 
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOLIMP);
wenzelm
parents:
53096
diff
changeset

924 
same conclusions, the same set of hypotheses, and the same set of sort 
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

925 
hypotheses. Names of bound variables are ignored as usual. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

926 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

927 
\item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

928 
the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

929 
Names of bound variables are ignored. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

930 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

931 
\item @{ML size_of_thm}~@{text "thm"} computes the size of @{text 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

932 
"thm"}, namely the number of variables, constants and abstractions 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

933 
in its conclusion. It may serve as a distance function for 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

934 
@{ML BEST_FIRST}. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

935 

e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

936 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

937 
*} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

938 

18537  939 
end 