author  wenzelm 
Sun, 29 Jan 2012 22:12:25 +0100  
changeset 46278  408e3acfdbb9 
parent 46277  aea65ff733b4 
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 
\[ 

56 
\infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad 

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

58 
\] 

59 
*} 

60 

61 
text %mlref {* 

62 
\begin{mldecls} 

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

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

64 
@{index_ML Goal.finish: "Proof.context > thm > thm"} \\ 
18537  65 
@{index_ML Goal.protect: "thm > thm"} \\ 
66 
@{index_ML Goal.conclude: "thm > thm"} \\ 

67 
\end{mldecls} 

68 

69 
\begin{description} 

70 

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

18537  73 

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

74 
\item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem 
20474  75 
@{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

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

77 
required for printing error messages. 
18537  78 

20474  79 
\item @{ML "Goal.protect"}~@{text "thm"} protects the full statement 
80 
of theorem @{text "thm"}. 

18537  81 

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

18537  84 

85 
\end{description} 

86 
*} 

87 

88 

39847  89 
section {* Tactics\label{sec:tactics} *} 
18537  90 

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

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

94 
successor states. The underlying sequence implementation is lazy 

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

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

97 
nature of SML requires some care when working with lowlevel 

98 
sequence operations, to avoid duplicate or premature evaluation of 

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

18537  101 

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

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

108 
faults should emerge as exceptions. 

28781  109 

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

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

112 
combinators for building proof tools that involve search 

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

114 

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

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

118 
must not change the main conclusion (apart from instantiating 

119 
schematic goal variables). 

18537  120 

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

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

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

125 
an exception! 

126 

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

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

129 
be affected, apart from instantiating schematic variables ranging 

130 
over the whole goal state. 

131 

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

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

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

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

137 
very common error when implementing tactics! 

138 

139 
Tactics with internal subgoal addressing should expose the subgoal 

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

34930  141 
subgoal 1 is not acceptable. 
28781  142 

143 
\medskip The main wellformedness conditions for proper tactics are 

144 
summarized as follows. 

145 

146 
\begin{itemize} 

147 

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

149 
serious faults may produce an exception. 

150 

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

152 
instantiating schematic variables. 

153 

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

155 
specifically on a selected subgoal (without bumping into unrelated 

156 
subgoals). 

157 

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

159 

160 
\end{itemize} 

28782  161 

162 
Some of these conditions are checked by higherlevel goal 

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

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

170 
text %mlref {* 

171 
\begin{mldecls} 

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

28783  173 
@{index_ML no_tac: tactic} \\ 
174 
@{index_ML all_tac: tactic} \\ 

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

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

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

179 
\end{mldecls} 

180 

181 
\begin{description} 

182 

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

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

185 
also @{file "~~/src/Pure/General/seq.ML"} for the underlying 
39864  186 
implementation of lazy sequences. 
28782  187 

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

190 
described above. 

28782  191 

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

194 

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

196 
singleton sequence with unchanged goal state. 

197 

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

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

200 
channel. 

201 

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

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

205 
exceptions are passed through. 

206 

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

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

211 
subgoal range is checked as required above. 

212 

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

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

217 

218 
\end{description} 

28781  219 
*} 
18537  220 

221 

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

222 
subsection {* Resolution and assumption tactics \label{sec:resolveassumetac} *} 
28783  223 

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

225 
subgoal using a theorem as objectlevel rule. 

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

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

228 
finally deletes that assumption from any new subgoals. 

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

230 
destruction rules are first turned into canonical elimination 

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

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

232 
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

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

234 
resolution rules and tactics. 
28783  235 

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

237 
against its conclusion. 

238 

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

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

241 
indirectly, due to instantiation of schematic variables. 

242 

243 
There are various sources of nondeterminism, the tactic result 

244 
sequence enumerates all possibilities of the following choices (if 

245 
applicable): 

246 

247 
\begin{enumerate} 

248 

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

250 

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

252 
the first premise of the rule; 

253 

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

255 
the rule. 

256 

257 
\end{enumerate} 

258 

259 
Recall that higherorder unification may produce multiple results 

260 
that are enumerated here. 

261 
*} 

262 

263 
text %mlref {* 

264 
\begin{mldecls} 

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

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

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

268 
@{index_ML forward_tac: "thm list > int > tactic"} \\[1ex] 

269 
@{index_ML assume_tac: "int > tactic"} \\ 

270 
@{index_ML eq_assume_tac: "int > tactic"} \\[1ex] 

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

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

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

274 
\end{mldecls} 

275 

276 
\begin{description} 

277 

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

279 
using the given theorems, which should normally be introduction 

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

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

282 
premises. 

283 

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

46278  285 
with the given theorems, which are normally be elimination rules. 
286 

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

288 
assume_tac}, which facilitates mixing of assumption steps with 

289 
genuine eliminations. 

28783  290 

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

292 
destructresolution with the given theorems, which should normally 

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

294 
applying one of the rules. 

295 

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

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

298 
assumption, adding the result as a new assumption. 

299 

300 
\item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i} 

301 
by assumption (modulo higherorder unification). 

302 

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

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

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

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

307 
instantiate variables, it cannot make other subgoals unprovable. 

308 

309 
\item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are 

310 
similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML 

311 
dresolve_tac}, respectively, but do not instantiate schematic 

312 
variables in the goal state. 

313 

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

315 
Strictly speaking, matching means to treat the unknowns in the goal 

316 
state as constants; these tactics merely discard unifiers that would 

317 
update the goal state. 

318 

319 
\end{description} 

320 
*} 

321 

322 

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

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

324 

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

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

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

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

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

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

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

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

332 
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

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

334 

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

335 
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

336 
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

337 
"?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

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

339 

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

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

341 
"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

342 
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

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

344 

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

345 
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

346 
"(?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

347 
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

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

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

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

351 

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

352 
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

353 
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

354 
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

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

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

357 

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

358 
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

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

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

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

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

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

365 

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

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

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

368 
@{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

369 
@{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

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

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

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

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

376 

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

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

378 

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

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

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

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

382 

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

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

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

385 

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

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

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

388 

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

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

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

391 

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

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

395 

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

398 
schematic variables, to abbreviate the intended proposition; the 

399 
first matching subgoal premise will be deleted. Removing useless 

400 
premises from a subgoal increases its readability and can make 

401 
search tactics run faster. 

402 

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

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

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

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

406 

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

407 
\end{description} 
34930  408 

409 
For historical reasons, the above instantiation tactics take 

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

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

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

413 
structure with explicit context management. 

28785
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 

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

416 

46274  417 
subsection {* Rearranging goal states *} 
418 

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

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

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

422 
concrete presentation these conceptual sets of formulae. *} 

423 

424 
text %mlref {* 

425 
\begin{mldecls} 

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

46276  427 
@{index_ML distinct_subgoals_tac: tactic} \\ 
428 
@{index_ML flexflex_tac: tactic} \\ 

46274  429 
\end{mldecls} 
430 

431 
\begin{description} 

432 

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

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

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

436 

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

439 

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

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

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

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

444 

445 
Flexflex constraints arise from difficult cases of higherorder 

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

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

448 
ignored; they often disappear as unknowns get instantiated. 

449 

46274  450 
\end{description} 
451 
*} 

452 

28781  453 
section {* Tacticals \label{sec:tacticals} *} 
18537  454 

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

457 
sequential composition, disjunctive choice, iteration, or goal 

458 
addressing. Various search strategies may be expressed via 

459 
tacticals. 

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

460 
*} 
46258  461 

462 

463 
subsection {* Combining tactics *} 

464 

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

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

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

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

46258  470 
"APPEND"}. Further details become visible in ML due to explicit 
46262  471 
subgoal addressing. 
472 
*} 

46258  473 

474 
text %mlref {* 

475 
\begin{mldecls} 

46262  476 
@{index_ML_op "THEN": "tactic * tactic > tactic"} \\ 
477 
@{index_ML_op "ORELSE": "tactic * tactic > tactic"} \\ 

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

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

481 

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

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

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

487 
\end{mldecls} 

488 

489 
\begin{description} 

18537  490 

46262  491 
\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

492 
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

493 
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

494 
@{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

495 
"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

496 
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

497 
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

498 
states. 
46258  499 

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

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

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

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

505 
from the result. 

46258  506 

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

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

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

511 
the cost of potential inefficiencies. 

39852  512 

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

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

516 
succeeds. 

46258  517 

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

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

521 
always fails. 

46258  522 

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

46258  527 

46264  528 
The other primed tacticals work analogously. 
46258  529 

530 
\end{description} 

531 
*} 

30272  532 

46259  533 

534 
subsection {* Repetition tacticals *} 

535 

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

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

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

539 

540 
text %mlref {* 

541 
\begin{mldecls} 

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

46266  543 
@{index_ML "REPEAT": "tactic > tactic"} \\ 
544 
@{index_ML "REPEAT1": "tactic > tactic"} \\ 

46259  545 
@{index_ML "REPEAT_DETERM": "tactic > tactic"} \\ 
546 
@{index_ML "REPEAT_DETERM_N": "int > tactic > tactic"} \\ 

547 
\end{mldecls} 

548 

549 
\begin{description} 

550 

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

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

554 
once. 

555 

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

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

46259  559 

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

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

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

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

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

566 
REPEAT_DETERM}, but requires more space. 

567 

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

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

570 
is impossible. 

571 

46266  572 
\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

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

576 

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

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

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

46259  580 

581 
\end{description} 

582 
*} 

583 

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

46259  586 

46260  587 
\begin{itemize} 
46259  588 

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

46259  591 

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

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

595 
equivalent to @{ML no_tac}. 

46259  596 

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

599 
implementation tricks): 

46259  600 

46260  601 
\end{itemize} 
46259  602 
*} 
603 

604 
ML {* 

605 
fun TRY tac = tac ORELSE all_tac; 

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

607 
*} 

608 

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

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

46259  612 
possible in each outcome. 
613 

614 
\begin{warn} 

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

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

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

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

46259  620 
\end{warn} 
621 
*} 

622 

623 
ML {* 

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

46259  626 
*} 
627 

46263  628 

46267  629 
subsection {* Applying tactics to subgoal ranges *} 
46263  630 

631 
text {* Tactics with explicit subgoal addressing 

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

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

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

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

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

638 
these tacticals address subgoal ranges counting downwards from 

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

640 
newly emerging subgoals are concatenated in the result, without 

641 
interfering each other. Nonetheless, there might be situations 

46266  642 
where a different order is desired. *} 
46263  643 

644 
text %mlref {* 

645 
\begin{mldecls} 

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

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

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

46267  649 
@{index_ML HEADGOAL: "(int > tactic) > tactic"} \\ 
46263  650 
@{index_ML REPEAT_SOME: "(int > tactic) > tactic"} \\ 
651 
@{index_ML REPEAT_FIRST: "(int > tactic) > tactic"} \\ 

46267  652 
@{index_ML RANGE: "(int > tactic) list > int > tactic"} \\ 
46263  653 
\end{mldecls} 
654 

655 
\begin{description} 

656 

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

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

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

660 

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

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

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

664 

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

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

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

668 

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

671 

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

674 

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

676 
more to a subgoal, counting upwards. 

677 

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

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

681 
corresponding range of subgoals, counting downwards. 

682 

46263  683 
\end{description} 
684 
*} 

685 

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

686 

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

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

688 

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

689 
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

690 
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

691 
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

692 
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

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

694 
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

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

696 

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

697 

46270  698 
text %mlref "" 
699 

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

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

701 

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

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

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

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

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

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

707 

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

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

709 

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

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

711 
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

712 
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

713 

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

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

715 
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

716 
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

717 
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

718 

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

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

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

721 

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

722 

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

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

724 

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

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

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

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

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

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

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

731 

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

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

733 

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

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

735 
@{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

736 
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

737 
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

738 
@{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

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

740 

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

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

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

743 

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

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

745 
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

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

747 

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

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

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

750 

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

751 

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

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

753 

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

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

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

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

757 
@{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

758 
@{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

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

760 

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

761 
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

762 
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

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

764 

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

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

766 

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

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

768 
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

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

770 

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

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

772 
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

773 
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

774 
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

775 
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

776 
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

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

778 

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

779 
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

780 
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

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

782 

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

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

784 
@{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

785 
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

786 
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

787 
continuing the search. 
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 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

791 

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 
subsubsection {* Auxiliary tacticals for searching *} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

794 

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

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

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

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

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

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

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

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

802 

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

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

804 

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

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

806 
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

807 
@{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

808 
@{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

809 
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

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

811 

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

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

813 
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

814 
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

815 
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

816 

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

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

818 
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

819 

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

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

821 
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

822 
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

823 

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

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

825 
*} 
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 

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

828 
subsubsection {* Predicates and functions useful for searching *} 
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 
text {* 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

834 
@{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

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

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

837 

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

838 
\begin{description} 
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 
\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

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

842 

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

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

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

845 
compatible background theories. Both theorems must have the same 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

847 
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

848 

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

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

850 
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

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

852 

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

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

854 
"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

855 
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

856 
@{ML BEST_FIRST}. 
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 
\end{description} 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

860 

18537  861 
end 