author  wenzelm 
Sun, 29 Jan 2012 22:12:25 +0100  
changeset 46278  408e3acfdbb9 
parent 46277  aea65ff733b4 
permissions  rwrr 
30296  1 
% 
2 
\begin{isabellebody}% 

3 
\def\isabellecontext{Tactic}% 

4 
% 

5 
\isadelimtheory 

6 
% 

7 
\endisadelimtheory 

8 
% 

9 
\isatagtheory 

10 
\isacommand{theory}\isamarkupfalse% 

11 
\ Tactic\isanewline 

12 
\isakeyword{imports}\ Base\isanewline 

13 
\isakeyword{begin}% 

14 
\endisatagtheory 

15 
{\isafoldtheory}% 

16 
% 

17 
\isadelimtheory 

18 
% 

19 
\endisadelimtheory 

20 
% 

21 
\isamarkupchapter{Tactical reasoning% 

22 
} 

23 
\isamarkuptrue% 

24 
% 

25 
\begin{isamarkuptext}% 

35001  26 
Tactical reasoning works by refining an initial claim in a 
30296  27 
backwards fashion, until a solved form is reached. A \isa{goal} 
28 
consists of several subgoals that need to be solved in order to 

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

30 
be finished. A \isa{tactic} is a refinement operation that maps 

31 
a goal to a lazy sequence of potential successors. A \isa{tactical} is a combinator for composing tactics.% 

32 
\end{isamarkuptext}% 

33 
\isamarkuptrue% 

34 
% 

35 
\isamarkupsection{Goals \label{sec:tacticalgoals}% 

36 
} 

37 
\isamarkuptrue% 

38 
% 

39 
\begin{isamarkuptext}% 

40 
Isabelle/Pure represents a goal as a theorem stating that the 

40406  41 
subgoals imply the main goal: \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}. The outermost goal structure is that of a Horn Clause: i.e.\ 
30296  42 
an iterated implication without any quantifiers\footnote{Recall that 
40406  43 
outermost \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} is always represented via schematic 
44 
variables in the body: \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}. These variables may get 

45 
instantiated during the course of reasoning.}. For \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} 

30296  46 
a goal is called ``solved''. 
47 

40406  48 
The structure of each subgoal \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} is that of a 
49 
general Hereditary Harrop Formula \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{2E}{\isachardot}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}. Here \isa{x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub k} are goal parameters, i.e.\ 

50 
arbitrarybutfixed entities of certain types, and \isa{H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m} are goal hypotheses, i.e.\ facts that may 

30296  51 
be assumed locally. Together, this forms the goal context of the 
52 
conclusion \isa{B} to be established. The goal hypotheses may be 

53 
again arbitrary Hereditary Harrop Formulas, although the level of 

54 
nesting rarely exceeds 12 in practice. 

55 

56 
The main conclusion \isa{C} is internally marked as a protected 

40406  57 
proposition, which is represented explicitly by the notation \isa{{\isaliteral{23}{\isacharhash}}C} here. This ensures that the decomposition into subgoals and 
35001  58 
main conclusion is welldefined for arbitrarily structured claims. 
30296  59 

60 
\medskip Basic goal management is performed via the following 

61 
Isabelle/Pure rules: 

62 

63 
\[ 

40406  64 
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}init{\isaliteral{29}{\isacharparenright}}}]{\isa{C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}}{} \qquad 
65 
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}finish{\isaliteral{29}{\isacharparenright}}}]{\isa{C}}{\isa{{\isaliteral{23}{\isacharhash}}C}} 

30296  66 
\] 
67 

68 
\medskip The following lowlevel variants admit general reasoning 

69 
with protected propositions: 

70 

71 
\[ 

40406  72 
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}protect{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{23}{\isacharhash}}C}}{\isa{C}} \qquad 
73 
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}conclude{\isaliteral{29}{\isacharparenright}}}]{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}} 

30296  74 
\]% 
75 
\end{isamarkuptext}% 

76 
\isamarkuptrue% 

77 
% 

78 
\isadelimmlref 

79 
% 

80 
\endisadelimmlref 

81 
% 

82 
\isatagmlref 

83 
% 

84 
\begin{isamarkuptext}% 

85 
\begin{mldecls} 

86 
\indexdef{}{ML}{Goal.init}\verbGoal.init: cterm > thm \\ 

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

87 
\indexdef{}{ML}{Goal.finish}\verbGoal.finish: Proof.context > thm > thm \\ 
30296  88 
\indexdef{}{ML}{Goal.protect}\verbGoal.protect: thm > thm \\ 
89 
\indexdef{}{ML}{Goal.conclude}\verbGoal.conclude: thm > thm \\ 

90 
\end{mldecls} 

91 

92 
\begin{description} 

93 

94 
\item \verbGoal.init~\isa{C} initializes a tactical goal from 

95 
the wellformed proposition \isa{C}. 

96 

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

97 
\item \verbGoal.finish~\isa{ctxt\ thm} checks whether theorem 
30296  98 
\isa{thm} is a solved goal (no subgoals), and concludes the 
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30296
diff
changeset

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

100 
required for printing error messages. 
30296  101 

102 
\item \verbGoal.protect~\isa{thm} protects the full statement 

103 
of theorem \isa{thm}. 

104 

105 
\item \verbGoal.conclude~\isa{thm} removes the goal 

106 
protection, even if there are pending subgoals. 

107 

108 
\end{description}% 

109 
\end{isamarkuptext}% 

110 
\isamarkuptrue% 

111 
% 

112 
\endisatagmlref 

113 
{\isafoldmlref}% 

114 
% 

115 
\isadelimmlref 

116 
% 

117 
\endisadelimmlref 

118 
% 

39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

119 
\isamarkupsection{Tactics\label{sec:tactics}% 
30296  120 
} 
121 
\isamarkuptrue% 

122 
% 

123 
\begin{isamarkuptext}% 

40406  124 
A \isa{tactic} is a function \isa{goal\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ goal\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} that 
30296  125 
maps a given goal state (represented as a theorem, cf.\ 
126 
\secref{sec:tacticalgoals}) to a lazy sequence of potential 

127 
successor states. The underlying sequence implementation is lazy 

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

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

130 
nature of SML requires some care when working with lowlevel 

131 
sequence operations, to avoid duplicate or premature evaluation of 

35001  132 
results. It also means that modified runtime behavior, such as 
133 
timeout, is very hard to achieve for general tactics.} 

30296  134 

135 
An \emph{empty result sequence} means that the tactic has failed: in 

35001  136 
a compound tactic expression other tactics might be tried instead, 
30296  137 
or the whole refinement step might fail outright, producing a 
35001  138 
toplevel error message in the end. When implementing tactics from 
139 
scratch, one should take care to observe the basic protocol of 

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

141 
faults should emerge as exceptions. 

30296  142 

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

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

145 
combinators for building proof tools that involve search 

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

147 

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

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

151 
must not change the main conclusion (apart from instantiating 

152 
schematic goal variables). 

30296  153 

154 
Tactics with explicit \emph{subgoal addressing} are of the form 

40406  155 
\isa{int\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ tactic} and may be applied to a particular subgoal 
30296  156 
(counting from 1). If the subgoal number is out of range, the 
157 
tactic should fail with an empty result sequence, but must not raise 

158 
an exception! 

159 

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

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

162 
be affected, apart from instantiating schematic variables ranging 

163 
over the whole goal state. 

164 

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

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

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

168 
into unrelated subgoals that happen to come after the original 

169 
subgoal. Assuming that there is only a single initial subgoal is a 

170 
very common error when implementing tactics! 

171 

172 
Tactics with internal subgoal addressing should expose the subgoal 

173 
index as \isa{int} argument in full generality; a hardwired 

35001  174 
subgoal 1 is not acceptable. 
30296  175 

176 
\medskip The main wellformedness conditions for proper tactics are 

177 
summarized as follows. 

178 

179 
\begin{itemize} 

180 

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

182 
serious faults may produce an exception. 

183 

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

185 
instantiating schematic variables. 

186 

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

188 
specifically on a selected subgoal (without bumping into unrelated 

189 
subgoals). 

190 

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

192 

193 
\end{itemize} 

194 

195 
Some of these conditions are checked by higherlevel goal 

35001  196 
infrastructure (\secref{sec:structgoals}); others are not checked 
30296  197 
explicitly, and violating them merely results in illbehaved tactics 
198 
experienced by the user (e.g.\ tactics that insist in being 

35001  199 
applicable only to singleton goals, or prevent composition via 
46260  200 
standard tacticals such as \verbREPEAT).% 
30296  201 
\end{isamarkuptext}% 
202 
\isamarkuptrue% 

203 
% 

204 
\isadelimmlref 

205 
% 

206 
\endisadelimmlref 

207 
% 

208 
\isatagmlref 

209 
% 

210 
\begin{isamarkuptext}% 

211 
\begin{mldecls} 

212 
\indexdef{}{ML type}{tactic}\verbtype tactic = thm > thm Seq.seq \\ 

213 
\indexdef{}{ML}{no\_tac}\verbno_tac: tactic \\ 

214 
\indexdef{}{ML}{all\_tac}\verball_tac: tactic \\ 

215 
\indexdef{}{ML}{print\_tac}\verbprint_tac: string > tactic \\[1ex] 

216 
\indexdef{}{ML}{PRIMITIVE}\verbPRIMITIVE: (thm > thm) > tactic \\[1ex] 

217 
\indexdef{}{ML}{SUBGOAL}\verbSUBGOAL: (term * int > tactic) > int > tactic \\ 

218 
\indexdef{}{ML}{CSUBGOAL}\verbCSUBGOAL: (cterm * int > tactic) > int > tactic \\ 

219 
\end{mldecls} 

220 

221 
\begin{description} 

222 

39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

223 
\item Type \verbtactic represents tactics. The 
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

224 
wellformedness conditions described above need to be observed. See 
40802  225 
also \verb~~/src/Pure/General/seq.ML for the underlying 
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

226 
implementation of lazy sequences. 
30296  227 

39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

228 
\item Type \verbint > tactic represents tactics with 
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

229 
explicit subgoal addressing, with wellformedness conditions as 
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset

230 
described above. 
30296  231 

232 
\item \verbno_tac is a tactic that always fails, returning the 

233 
empty sequence. 

234 

235 
\item \verball_tac is a tactic that always succeeds, returning a 

236 
singleton sequence with unchanged goal state. 

237 

238 
\item \verbprint_tac~\isa{message} is like \verball_tac, but 

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

240 
channel. 

241 

242 
\item \verbPRIMITIVE~\isa{rule} turns a primitive inference rule 

243 
into a tactic with unique result. Exception \verbTHM is considered 

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

245 
exceptions are passed through. 

246 

40406  247 
\item \verbSUBGOAL~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ tactic{\isaliteral{29}{\isacharparenright}}} is the 
30296  248 
most basic form to produce a tactic with subgoal addressing. The 
249 
given abstraction over the subgoal term and subgoal number allows to 

250 
peek at the relevant information of the full goal state. The 

251 
subgoal range is checked as required above. 

252 

253 
\item \verbCSUBGOAL is similar to \verbSUBGOAL, but passes the 

254 
subgoal as \verbcterm instead of raw \verbterm. This 

255 
avoids expensive recertification in situations where the subgoal is 

256 
used directly for primitive inferences. 

257 

258 
\end{description}% 

259 
\end{isamarkuptext}% 

260 
\isamarkuptrue% 

261 
% 

262 
\endisatagmlref 

263 
{\isafoldmlref}% 

264 
% 

265 
\isadelimmlref 

266 
% 

267 
\endisadelimmlref 

268 
% 

269 
\isamarkupsubsection{Resolution and assumption tactics \label{sec:resolveassumetac}% 

270 
} 

271 
\isamarkuptrue% 

272 
% 

273 
\begin{isamarkuptext}% 

274 
\emph{Resolution} is the most basic mechanism for refining a 

275 
subgoal using a theorem as objectlevel rule. 

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

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

278 
finally deletes that assumption from any new subgoals. 

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

280 
destruction rules are first turned into canonical elimination 

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

40406  282 
without deleting the selected assumption. The \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f} 
30296  283 
naming convention is maintained for several different kinds of 
284 
resolution rules and tactics. 

285 

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

287 
against its conclusion. 

288 

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

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

291 
indirectly, due to instantiation of schematic variables. 

292 

293 
There are various sources of nondeterminism, the tactic result 

294 
sequence enumerates all possibilities of the following choices (if 

295 
applicable): 

296 

297 
\begin{enumerate} 

298 

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

300 

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

302 
the first premise of the rule; 

303 

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

305 
the rule. 

306 

307 
\end{enumerate} 

308 

309 
Recall that higherorder unification may produce multiple results 

310 
that are enumerated here.% 

311 
\end{isamarkuptext}% 

312 
\isamarkuptrue% 

313 
% 

314 
\isadelimmlref 

315 
% 

316 
\endisadelimmlref 

317 
% 

318 
\isatagmlref 

319 
% 

320 
\begin{isamarkuptext}% 

321 
\begin{mldecls} 

322 
\indexdef{}{ML}{resolve\_tac}\verbresolve_tac: thm list > int > tactic \\ 

323 
\indexdef{}{ML}{eresolve\_tac}\verberesolve_tac: thm list > int > tactic \\ 

324 
\indexdef{}{ML}{dresolve\_tac}\verbdresolve_tac: thm list > int > tactic \\ 

325 
\indexdef{}{ML}{forward\_tac}\verbforward_tac: thm list > int > tactic \\[1ex] 

326 
\indexdef{}{ML}{assume\_tac}\verbassume_tac: int > tactic \\ 

327 
\indexdef{}{ML}{eq\_assume\_tac}\verbeq_assume_tac: int > tactic \\[1ex] 

328 
\indexdef{}{ML}{match\_tac}\verbmatch_tac: thm list > int > tactic \\ 

329 
\indexdef{}{ML}{ematch\_tac}\verbematch_tac: thm list > int > tactic \\ 

330 
\indexdef{}{ML}{dmatch\_tac}\verbdmatch_tac: thm list > int > tactic \\ 

331 
\end{mldecls} 

332 

333 
\begin{description} 

334 

335 
\item \verbresolve_tac~\isa{thms\ i} refines the goal state 

336 
using the given theorems, which should normally be introduction 

337 
rules. The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's 

338 
premises. 

339 

340 
\item \verberesolve_tac~\isa{thms\ i} performs elimresolution 

46278  341 
with the given theorems, which are normally be elimination rules. 
342 

343 
Note that \verberesolve_tac [asm_rl] is equivalent to \verbassume_tac, which facilitates mixing of assumption steps with 

344 
genuine eliminations. 

30296  345 

346 
\item \verbdresolve_tac~\isa{thms\ i} performs 

347 
destructresolution with the given theorems, which should normally 

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

349 
applying one of the rules. 

350 

351 
\item \verbforward_tac is like \verbdresolve_tac except that the 

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

353 
assumption, adding the result as a new assumption. 

354 

355 
\item \verbassume_tac~\isa{i} attempts to solve subgoal \isa{i} 

356 
by assumption (modulo higherorder unification). 

357 

358 
\item \verbeq_assume_tac is similar to \verbassume_tac, but checks 

40406  359 
only for immediate \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}convertibility instead of using 
30296  360 
unification. It succeeds (with a unique next state) if one of the 
361 
assumptions is equal to the subgoal's conclusion. Since it does not 

362 
instantiate variables, it cannot make other subgoals unprovable. 

363 

364 
\item \verbmatch_tac, \verbematch_tac, and \verbdmatch_tac are 

365 
similar to \verbresolve_tac, \verberesolve_tac, and \verbdresolve_tac, respectively, but do not instantiate schematic 

366 
variables in the goal state. 

367 

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

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

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

371 
update the goal state. 

372 

373 
\end{description}% 

374 
\end{isamarkuptext}% 

375 
\isamarkuptrue% 

376 
% 

377 
\endisatagmlref 

378 
{\isafoldmlref}% 

379 
% 

380 
\isadelimmlref 

381 
% 

382 
\endisadelimmlref 

383 
% 

384 
\isamarkupsubsection{Explicit instantiation within a subgoal context% 

385 
} 

386 
\isamarkuptrue% 

387 
% 

388 
\begin{isamarkuptext}% 

389 
The main resolution tactics (\secref{sec:resolveassumetac}) 

390 
use higherorder unification, which works well in many practical 

391 
situations despite its daunting theoretical properties. 

392 
Nonetheless, there are important problem classes where unguided 

393 
higherorder unification is not so useful. This typically involves 

394 
rules like universal elimination, existential introduction, or 

395 
equational substitution. Here the unification problem involves 

40406  396 
fully flexible \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x} schemes, which are hard to manage 
30296  397 
without further hints. 
398 

40406  399 
By providing a (small) rigid term for \isa{{\isaliteral{3F}{\isacharquery}}x} explicitly, the 
400 
remaining unification problem is to assign a (large) term to \isa{{\isaliteral{3F}{\isacharquery}}P}, according to the shape of the given subgoal. This is 

30296  401 
sufficiently wellbehaved in most practical situations. 
402 

40406  403 
\medskip Isabelle provides separate versions of the standard \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f} resolution tactics that allow to provide explicit 
30296  404 
instantiations of unknowns of the given rule, wrt.\ terms that refer 
405 
to the implicit context of the selected subgoal. 

406 

40406  407 
An instantiation consists of a list of pairs of the form \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}, where \isa{{\isaliteral{3F}{\isacharquery}}x} is a schematic variable occurring in 
30296  408 
the given rule, and \isa{t} is a term from the current proof 
409 
context, augmented by the local goal parameters of the selected 

410 
subgoal; cf.\ the \isa{focus} operation described in 

411 
\secref{sec:variables}. 

412 

413 
Entering the syntactic context of a subgoal is a brittle operation, 

414 
because its exact form is somewhat accidental, and the choice of 

415 
bound variable names depends on the presence of other local and 

416 
global names. Explicit renaming of subgoal parameters prior to 

417 
explicit instantiation might help to achieve a bit more robustness. 

418 

40406  419 
Type instantiations may be given as well, via pairs like \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}. Type instantiations are distinguished from term 
30296  420 
instantiations by the syntactic form of the schematic variable. 
421 
Types are instantiated before terms are. Since term instantiation 

35001  422 
already performs simple typeinference, so explicit type 
30296  423 
instantiations are seldom necessary.% 
424 
\end{isamarkuptext}% 

425 
\isamarkuptrue% 

426 
% 

427 
\isadelimmlref 

428 
% 

429 
\endisadelimmlref 

430 
% 

431 
\isatagmlref 

432 
% 

433 
\begin{isamarkuptext}% 

434 
\begin{mldecls} 

435 
\indexdef{}{ML}{res\_inst\_tac}\verbres_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic \\ 

436 
\indexdef{}{ML}{eres\_inst\_tac}\verberes_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic \\ 

437 
\indexdef{}{ML}{dres\_inst\_tac}\verbdres_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic \\ 

46271  438 
\indexdef{}{ML}{forw\_inst\_tac}\verbforw_inst_tac: Proof.context > (indexname * string) list > thm > int > tactic \\ 
439 
\indexdef{}{ML}{subgoal\_tac}\verbsubgoal_tac: Proof.context > string > int > tactic \\ 

46277  440 
\indexdef{}{ML}{thin\_tac}\verbthin_tac: Proof.context > string > int > tactic \\ 
30296  441 
\indexdef{}{ML}{rename\_tac}\verbrename_tac: string list > int > tactic \\ 
442 
\end{mldecls} 

443 

444 
\begin{description} 

445 

446 
\item \verbres_inst_tac~\isa{ctxt\ insts\ thm\ i} instantiates the 

447 
rule \isa{thm} with the instantiations \isa{insts}, as described 

448 
above, and then performs resolution on subgoal \isa{i}. 

449 

450 
\item \verberes_inst_tac is like \verbres_inst_tac, but performs 

451 
elimresolution. 

452 

453 
\item \verbdres_inst_tac is like \verbres_inst_tac, but performs 

454 
destructresolution. 

455 

456 
\item \verbforw_inst_tac is like \verbdres_inst_tac except that 

457 
the selected assumption is not deleted. 

458 

46271  459 
\item \verbsubgoal_tac~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} adds the proposition 
460 
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as local premise to subgoal \isa{i}, and poses the 

461 
same as a new subgoal \isa{i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} (in the original context). 

462 

46277  463 
\item \verbthin_tac~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} deletes the specified 
464 
premise from subgoal \isa{i}. Note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain 

465 
schematic variables, to abbreviate the intended proposition; the 

466 
first matching subgoal premise will be deleted. Removing useless 

467 
premises from a subgoal increases its readability and can make 

468 
search tactics run faster. 

469 

30296  470 
\item \verbrename_tac~\isa{names\ i} renames the innermost 
471 
parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers). 

472 

35001  473 
\end{description} 
474 

475 
For historical reasons, the above instantiation tactics take 

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

477 
ML code. The slightly more advanced \verbSubgoal.FOCUS combinator 

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

479 
structure with explicit context management.% 

30296  480 
\end{isamarkuptext}% 
481 
\isamarkuptrue% 

482 
% 

483 
\endisatagmlref 

484 
{\isafoldmlref}% 

485 
% 

486 
\isadelimmlref 

487 
% 

488 
\endisadelimmlref 

489 
% 

46274  490 
\isamarkupsubsection{Rearranging goal states% 
491 
} 

492 
\isamarkuptrue% 

493 
% 

494 
\begin{isamarkuptext}% 

495 
In rare situations there is a need to rearrange goal states: 

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

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

498 
concrete presentation these conceptual sets of formulae.% 

499 
\end{isamarkuptext}% 

500 
\isamarkuptrue% 

501 
% 

502 
\isadelimmlref 

503 
% 

504 
\endisadelimmlref 

505 
% 

506 
\isatagmlref 

507 
% 

508 
\begin{isamarkuptext}% 

509 
\begin{mldecls} 

510 
\indexdef{}{ML}{rotate\_tac}\verbrotate_tac: int > int > tactic \\ 

46276  511 
\indexdef{}{ML}{distinct\_subgoals\_tac}\verbdistinct_subgoals_tac: tactic \\ 
512 
\indexdef{}{ML}{flexflex\_tac}\verbflexflex_tac: tactic \\ 

46274  513 
\end{mldecls} 
514 

515 
\begin{description} 

516 

517 
\item \verbrotate_tac~\isa{n\ i} rotates the premises of subgoal 

518 
\isa{i} by \isa{n} positions: from right to left if \isa{n} is 

519 
positive, and from left to right if \isa{n} is negative. 

520 

46276  521 
\item \verbdistinct_subgoals_tac removes duplicate subgoals from a 
522 
proof state. This is potentially inefficient. 

523 

524 
\item \verbflexflex_tac removes all flexflex pairs from the proof 

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

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

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

528 

529 
Flexflex constraints arise from difficult cases of higherorder 

530 
unification. To prevent this, use \verbres_inst_tac to instantiate 

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

532 
ignored; they often disappear as unknowns get instantiated. 

533 

46274  534 
\end{description}% 
535 
\end{isamarkuptext}% 

536 
\isamarkuptrue% 

537 
% 

538 
\endisatagmlref 

539 
{\isafoldmlref}% 

540 
% 

541 
\isadelimmlref 

542 
% 

543 
\endisadelimmlref 

544 
% 

30296  545 
\isamarkupsection{Tacticals \label{sec:tacticals}% 
546 
} 

547 
\isamarkuptrue% 

548 
% 

549 
\begin{isamarkuptext}% 

46258  550 
A \emph{tactical} is a functional combinator for building up 
551 
complex tactics from simpler ones. Common tacticals perform 

552 
sequential composition, disjunctive choice, iteration, or goal 

553 
addressing. Various search strategies may be expressed via 

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

554 
tacticals.% 
46258  555 
\end{isamarkuptext}% 
556 
\isamarkuptrue% 

557 
% 

558 
\isamarkupsubsection{Combining tactics% 

559 
} 

560 
\isamarkuptrue% 

561 
% 

562 
\begin{isamarkuptext}% 

563 
Sequential composition and alternative choices are the most 

564 
basic ways to combine tactics, similarly to ``\verb,'' and 

565 
``\verb\verb,,\verb'' in Isar method notation. This corresponds to 

46262  566 
\verbTHEN and \verbORELSE in ML, but there are further 
567 
possibilities for finetuning alternation of tactics such as \verbAPPEND. Further details become visible in ML due to explicit 

46258  568 
subgoal addressing.% 
30296  569 
\end{isamarkuptext}% 
570 
\isamarkuptrue% 

571 
% 

46258  572 
\isadelimmlref 
573 
% 

574 
\endisadelimmlref 

575 
% 

576 
\isatagmlref 

577 
% 

578 
\begin{isamarkuptext}% 

579 
\begin{mldecls} 

46262  580 
\indexdef{}{ML infix}{THEN}\verbinfix THEN: tactic * tactic > tactic \\ 
581 
\indexdef{}{ML infix}{ORELSE}\verbinfix ORELSE: tactic * tactic > tactic \\ 

582 
\indexdef{}{ML infix}{APPEND}\verbinfix APPEND: tactic * tactic > tactic \\ 

46258  583 
\indexdef{}{ML}{EVERY}\verbEVERY: tactic list > tactic \\ 
584 
\indexdef{}{ML}{FIRST}\verbFIRST: tactic list > tactic \\[0.5ex] 

585 

46262  586 
\indexdef{}{ML infix}{THEN'}\verbinfix THEN': ('a > tactic) * ('a > tactic) > 'a > tactic \\ 
587 
\indexdef{}{ML infix}{ORELSE'}\verbinfix ORELSE': ('a > tactic) * ('a > tactic) > 'a > tactic \\ 

588 
\indexdef{}{ML infix}{APPEND'}\verbinfix APPEND': ('a > tactic) * ('a > tactic) > 'a > tactic \\ 

46258  589 
\indexdef{}{ML}{EVERY'}\verbEVERY': ('a > tactic) list > 'a > tactic \\ 
590 
\indexdef{}{ML}{FIRST'}\verbFIRST': ('a > tactic) list > 'a > tactic \\ 

591 
\end{mldecls} 

592 

593 
\begin{description} 

594 

46262  595 
\item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verbTHEN~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential 
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

596 
composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

597 
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

598 
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{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

599 
states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

600 
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

601 
states. 
46258  602 

46262  603 
\item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verbORELSE~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice 
604 
between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it 

605 
tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if nonempty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic 

606 
choice: if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded 

607 
from the result. 

46258  608 

46262  609 
\item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verbAPPEND~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the 
610 
possible results of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike 

611 
\verbORELSE there is \emph{no commitment} to either tactic, so 

612 
\verbAPPEND helps to avoid incompleteness during search, at 

613 
the cost of potential inefficiencies. 

46258  614 

46262  615 
\item \verbEVERY~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verbTHEN~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verbTHEN~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. 
616 
Note that \verbEVERY [] is the same as \verball_tac: it always 

617 
succeeds. 

46258  618 

46262  619 
\item \verbFIRST~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verbORELSE~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verbORELSE~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \verbFIRST [] is the same as \verbno_tac: it 
620 
always fails. 

46258  621 

46264  622 
\item \verbTHEN' is the lifted version of \verbTHEN, for 
46266  623 
tactics with explicit subgoal addressing. So \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verbTHEN'~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verbTHEN~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}. 
46258  624 

46264  625 
The other primed tacticals work analogously. 
46258  626 

627 
\end{description}% 

628 
\end{isamarkuptext}% 

629 
\isamarkuptrue% 

630 
% 

631 
\endisatagmlref 

632 
{\isafoldmlref}% 

633 
% 

634 
\isadelimmlref 

635 
% 

636 
\endisadelimmlref 

637 
% 

46259  638 
\isamarkupsubsection{Repetition tacticals% 
639 
} 

640 
\isamarkuptrue% 

641 
% 

642 
\begin{isamarkuptext}% 

643 
These tacticals provide further control over repetition of 

644 
tactics, beyond the stylized forms of ``\verb?'' and 

645 
``\verb+'' in Isar method expressions.% 

646 
\end{isamarkuptext}% 

647 
\isamarkuptrue% 

648 
% 

649 
\isadelimmlref 

650 
% 

651 
\endisadelimmlref 

652 
% 

653 
\isatagmlref 

654 
% 

655 
\begin{isamarkuptext}% 

656 
\begin{mldecls} 

657 
\indexdef{}{ML}{TRY}\verbTRY: tactic > tactic \\ 

46266  658 
\indexdef{}{ML}{REPEAT}\verbREPEAT: tactic > tactic \\ 
659 
\indexdef{}{ML}{REPEAT1}\verbREPEAT1: tactic > tactic \\ 

46259  660 
\indexdef{}{ML}{REPEAT\_DETERM}\verbREPEAT_DETERM: tactic > tactic \\ 
661 
\indexdef{}{ML}{REPEAT\_DETERM\_N}\verbREPEAT_DETERM_N: int > tactic > tactic \\ 

662 
\end{mldecls} 

663 

664 
\begin{description} 

665 

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

666 
\item \verbTRY~\isa{tac} applies \isa{tac} to the goal 
46259  667 
state and returns the resulting sequence, if nonempty; otherwise it 
668 
returns the original state. Thus, it applies \isa{tac} at most 

669 
once. 

670 

46266  671 
Note that for tactics with subgoal addressing, the combinator can be 
672 
applied via functional composition: \verbTRY~\verbo~\isa{tac}. There is no need for \verbTRY'. 

46259  673 

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

674 
\item \verbREPEAT~\isa{tac} applies \isa{tac} to the goal 
46259  675 
state and, recursively, to each element of the resulting sequence. 
676 
The resulting sequence consists of those states that make \isa{tac} fail. Thus, it applies \isa{tac} as many times as 

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

678 
invocation of \isa{tac}. \verbREPEAT is more general than \verbREPEAT_DETERM, but requires more space. 

679 

680 
\item \verbREPEAT1~\isa{tac} is like \verbREPEAT~\isa{tac} 

681 
but it always applies \isa{tac} at least once, failing if this 

682 
is impossible. 

683 

46266  684 
\item \verbREPEAT_DETERM~\isa{tac} applies \isa{tac} to the 
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

685 
goal state and, recursively, to the head of the resulting sequence. 
46266  686 
It returns the first state to make \isa{tac} fail. It is 
687 
deterministic, discarding alternative outcomes. 

688 

689 
\item \verbREPEAT_DETERM_N~\isa{n\ tac} is like \verbREPEAT_DETERM~\isa{tac} but the number of repetitions is bound 

690 
by \isa{n} (where \verb~1 means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}). 

46259  691 

692 
\end{description}% 

693 
\end{isamarkuptext}% 

694 
\isamarkuptrue% 

695 
% 

696 
\endisatagmlref 

697 
{\isafoldmlref}% 

698 
% 

699 
\isadelimmlref 

700 
% 

701 
\endisadelimmlref 

702 
% 

703 
\isadelimmlex 

704 
% 

705 
\endisadelimmlex 

706 
% 

707 
\isatagmlex 

708 
% 

709 
\begin{isamarkuptext}% 

46260  710 
The basic tactics and tacticals considered above follow 
711 
some algebraic laws: 

712 

713 
\begin{itemize} 

714 

46262  715 
\item \verball_tac is the identity element of the tactical \verbTHEN. 
46260  716 

46262  717 
\item \verbno_tac is the identity element of \verbORELSE and 
718 
\verbAPPEND. Also, it is a zero element for \verbTHEN, 

719 
which means that \isa{tac}~\verbTHEN~\verbno_tac is 

720 
equivalent to \verbno_tac. 

46260  721 

722 
\item \verbTRY and \verbREPEAT can be expressed as (recursive) 

723 
functions over more basic combinators (ignoring some internal 

724 
implementation tricks): 

725 

726 
\end{itemize}% 

46259  727 
\end{isamarkuptext}% 
728 
\isamarkuptrue% 

729 
% 

730 
\endisatagmlex 

731 
{\isafoldmlex}% 

732 
% 

733 
\isadelimmlex 

734 
% 

735 
\endisadelimmlex 

736 
% 

737 
\isadelimML 

738 
% 

739 
\endisadelimML 

740 
% 

741 
\isatagML 

742 
\isacommand{ML}\isamarkupfalse% 

743 
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 

744 
\ \ fun\ TRY\ tac\ {\isaliteral{3D}{\isacharequal}}\ tac\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline 

745 
\ \ fun\ REPEAT\ tac\ st\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}\ st{\isaliteral{3B}{\isacharsemicolon}}\isanewline 

746 
{\isaliteral{2A7D}{\isacharverbatimclose}}% 

747 
\endisatagML 

748 
{\isafoldML}% 

749 
% 

750 
\isadelimML 

751 
% 

752 
\endisadelimML 

753 
% 

754 
\begin{isamarkuptext}% 

46262  755 
If \isa{tac} can return multiple outcomes then so can \verbREPEAT~\isa{tac}. \verbREPEAT uses \verbORELSE and not 
756 
\verbAPPEND, it applies \isa{tac} as many times as 

46259  757 
possible in each outcome. 
758 

759 
\begin{warn} 

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

760 
Note the explicit abstraction over the goal state in the ML 
46260  761 
definition of \verbREPEAT. Recursive tacticals must be coded in 
762 
this awkward fashion to avoid infinite recursion of eager functional 

763 
evaluation in Standard ML. The following attempt would make \verbREPEAT~\isa{tac} loop: 

46259  764 
\end{warn}% 
765 
\end{isamarkuptext}% 

766 
\isamarkuptrue% 

767 
% 

768 
\isadelimML 

769 
% 

770 
\endisadelimML 

771 
% 

772 
\isatagML 

773 
\isacommand{ML}\isamarkupfalse% 

774 
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline 

46260  775 
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}BAD\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ does\ not\ terminate{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline 
776 
\ \ fun\ REPEAT\ tac\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline 

46259  777 
{\isaliteral{2A7D}{\isacharverbatimclose}}% 
778 
\endisatagML 

779 
{\isafoldML}% 

780 
% 

781 
\isadelimML 

782 
% 

783 
\endisadelimML 

46263  784 
% 
46267  785 
\isamarkupsubsection{Applying tactics to subgoal ranges% 
46263  786 
} 
787 
\isamarkuptrue% 

788 
% 

789 
\begin{isamarkuptext}% 

790 
Tactics with explicit subgoal addressing 

791 
\verbint > tactic can be used together with tacticals that 

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

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

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

796 
Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals. Many of 

797 
these tacticals address subgoal ranges counting downwards from 

798 
\isa{n} towards \isa{{\isadigit{1}}}. This has the fortunate effect that 

799 
newly emerging subgoals are concatenated in the result, without 

800 
interfering each other. Nonetheless, there might be situations 

46266  801 
where a different order is desired.% 
46263  802 
\end{isamarkuptext}% 
803 
\isamarkuptrue% 

804 
% 

805 
\isadelimmlref 

806 
% 

807 
\endisadelimmlref 

808 
% 

809 
\isatagmlref 

810 
% 

811 
\begin{isamarkuptext}% 

812 
\begin{mldecls} 

813 
\indexdef{}{ML}{ALLGOALS}\verbALLGOALS: (int > tactic) > tactic \\ 

814 
\indexdef{}{ML}{SOMEGOAL}\verbSOMEGOAL: (int > tactic) > tactic \\ 

815 
\indexdef{}{ML}{FIRSTGOAL}\verbFIRSTGOAL: (int > tactic) > tactic \\ 

46267  816 
\indexdef{}{ML}{HEADGOAL}\verbHEADGOAL: (int > tactic) > tactic \\ 
46263  817 
\indexdef{}{ML}{REPEAT\_SOME}\verbREPEAT_SOME: (int > tactic) > tactic \\ 
818 
\indexdef{}{ML}{REPEAT\_FIRST}\verbREPEAT_FIRST: (int > tactic) > tactic \\ 

46267  819 
\indexdef{}{ML}{RANGE}\verbRANGE: (int > tactic) list > int > tactic \\ 
46263  820 
\end{mldecls} 
821 

822 
\begin{description} 

823 

824 
\item \verbALLGOALS~\isa{tac} is equivalent to \isa{tac\ n}~\verbTHEN~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verbTHEN~\isa{tac\ {\isadigit{1}}}. It 

825 
applies the \isa{tac} to all the subgoals, counting downwards. 

826 

827 
\item \verbSOMEGOAL~\isa{tac} is equivalent to \isa{tac\ n}~\verbORELSE~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verbORELSE~\isa{tac\ {\isadigit{1}}}. It 

828 
applies \isa{tac} to one subgoal, counting downwards. 

829 

830 
\item \verbFIRSTGOAL~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verbORELSE~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verbORELSE~\isa{tac\ n}. It 

831 
applies \isa{tac} to one subgoal, counting upwards. 

832 

46267  833 
\item \verbHEADGOAL~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}. 
834 
It applies \isa{tac} unconditionally to the first subgoal. 

835 

46263  836 
\item \verbREPEAT_SOME~\isa{tac} applies \isa{tac} once or 
837 
more to a subgoal, counting downwards. 

838 

839 
\item \verbREPEAT_FIRST~\isa{tac} applies \isa{tac} once or 

840 
more to a subgoal, counting upwards. 

841 

46267  842 
\item \verbRANGE~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to 
843 
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verbTHEN~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verbTHEN~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}. It applies the given list of tactics to the 

844 
corresponding range of subgoals, counting downwards. 

845 

46263  846 
\end{description}% 
847 
\end{isamarkuptext}% 

848 
\isamarkuptrue% 

849 
% 

850 
\endisatagmlref 

851 
{\isafoldmlref}% 

852 
% 

853 
\isadelimmlref 

854 
% 

855 
\endisadelimmlref 

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

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

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

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

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

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

862 
A predicate on theorems \verbthm > bool can test 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

863 
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

864 
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

865 
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

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

867 
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

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

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

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

871 
% 
46270  872 
\isadelimmlref 
873 
% 

874 
\endisadelimmlref 

875 
% 

876 
\isatagmlref 

877 
% 

878 
\begin{isamarkuptext}% 

879 
% 

880 
\end{isamarkuptext}% 

881 
\isamarkuptrue% 

882 
% 

883 
\endisatagmlref 

884 
{\isafoldmlref}% 

885 
% 

886 
\isadelimmlref 

887 
% 

888 
\endisadelimmlref 

889 
% 

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

890 
\isamarkupsubsubsection{Filtering a tactic's results% 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

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

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

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

897 
\indexdef{}{ML}{CHANGED}\verbCHANGED: tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

899 

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

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

901 

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

902 
\item \verbFILTER~\isa{sat\ tac} applies \isa{tac} to the 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

903 
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

904 
states that are satisfactory in the sense of \isa{sat}. 
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 
\item \verbCHANGED~\isa{tac} applies \isa{tac} to the goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

907 
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

908 
original state (according to \verbThm.eq_thm). Thus \verbCHANGED~\isa{tac} always has some effect on the state. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

909 

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

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

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

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

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

914 
\isamarkupsubsubsection{Depthfirst search% 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

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

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

920 
\indexdef{}{ML}{DEPTH\_FIRST}\verbDEPTH_FIRST: (thm > bool) > tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

921 
\indexdef{}{ML}{DEPTH\_SOLVE}\verbDEPTH_SOLVE: tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

922 
\indexdef{}{ML}{DEPTH\_SOLVE\_1}\verbDEPTH_SOLVE_1: tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

924 

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

925 
\begin{description} 
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 \verbDEPTH_FIRST~\isa{sat\ tac} returns the goal state if 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

929 
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

930 
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

931 
\isa{tac}~\verbTHEN~\verbDEPTH_FIRST~\isa{sat\ tac} to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

933 

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

934 
\item \verbDEPTH_SOLVE\isa{tac} uses \verbDEPTH_FIRST to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

936 

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

937 
\item \verbDEPTH_SOLVE_1~\isa{tac} uses \verbDEPTH_FIRST to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

938 
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

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

940 

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

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

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

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

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

945 
\isamarkupsubsubsection{Other search strategies% 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

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

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

951 
\indexdef{}{ML}{BREADTH\_FIRST}\verbBREADTH_FIRST: (thm > bool) > tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

952 
\indexdef{}{ML}{BEST\_FIRST}\verbBEST_FIRST: (thm > bool) * (thm > int) > tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

953 
\indexdef{}{ML}{THEN\_BEST\_FIRST}\verbTHEN_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

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

955 

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

956 
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

957 
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

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

959 

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

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

961 

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

962 
\item \verbBREADTH_FIRST~\isa{sat\ tac} uses breadthfirst 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

965 

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

966 
\item \verbBEST_FIRST~\isa{{\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} does a heuristic 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

970 
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

971 
then it returns them. Otherwise, \verbBEST_FIRST adds the new 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

973 

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

974 
The distance function is typically \verbsize_of_thm, which computes 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

975 
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

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

977 

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

978 
\item \verbTHEN_BEST_FIRST~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} is like 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

979 
\verbBEST_FIRST, except that the priority queue initially contains 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

980 
the result of applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}} to the goal state. This 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

981 
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

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

983 

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

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

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

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

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

988 
\isamarkupsubsubsection{Auxiliary tacticals for searching% 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

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

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

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

995 
\indexdef{}{ML}{IF\_UNSOLVED}\verbIF_UNSOLVED: tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

996 
\indexdef{}{ML}{SOLVE}\verbSOLVE: tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

997 
\indexdef{}{ML}{DETERM}\verbDETERM: tactic > tactic \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

999 

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

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

1001 

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

1002 
\item \verbCOND~\isa{sat\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

1004 
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{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

1005 
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is applied to a goal state. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1006 
However, both \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are evaluated 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

1008 

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

1009 
\item \verbIF_UNSOLVED~\isa{tac} applies \isa{tac} to the 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1010 
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

1011 
otherwise. Many common tactics, such as \verbresolve_tac, fail if 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1012 
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

1013 

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

1014 
\item \verbSOLVE~\isa{tac} applies \isa{tac} to the goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1015 
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

1016 

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

1017 
\item \verbDETERM~\isa{tac} applies \isa{tac} to the goal 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1018 
state and returns the head of the resulting sequence. \verbDETERM 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1019 
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

1020 

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

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

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

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

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

1025 
\isamarkupsubsubsection{Predicates and functions useful for searching% 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

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

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

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

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

1031 
\indexdef{}{ML}{has\_fewer\_prems}\verbhas_fewer_prems: int > thm > bool \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1032 
\indexdef{}{ML}{Thm.eq\_thm}\verbThm.eq_thm: thm * thm > bool \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1033 
\indexdef{}{ML}{Thm.eq\_thm\_prop}\verbThm.eq_thm_prop: thm * thm > bool \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1034 
\indexdef{}{ML}{size\_of\_thm}\verbsize_of_thm: thm > int \\ 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

1036 

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

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

1038 

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

1039 
\item \verbhas_fewer_prems~\isa{n\ thm} reports whether \isa{thm} has fewer than \isa{n} premises. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1040 

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

1041 
\item \verbThm.eq_thm~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal. Both theorems must have 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1042 
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

1043 
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

1044 
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

1045 

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

1046 
\item \verbThm.eq_thm_prop~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

1047 
the propositions of \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal. 
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset

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

1049 

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

1050 
\item \verbsize_of_thm~\isa{thm} computes the size of \isa{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

1051 
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

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

1053 

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

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

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

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

1057 
% 
30296  1058 
\isadelimtheory 
1059 
% 

1060 
\endisadelimtheory 

1061 
% 

1062 
\isatagtheory 

1063 
\isacommand{end}\isamarkupfalse% 

1064 
% 

1065 
\endisatagtheory 

1066 
{\isafoldtheory}% 

1067 
% 

1068 
\isadelimtheory 

1069 
% 

1070 
\endisadelimtheory 

1071 
\isanewline 

1072 
\end{isabellebody}% 

1073 
%%% Local Variables: 

1074 
%%% mode: latex 

1075 
%%% TeXmaster: "root" 

1076 
%%% End: 