summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Implementation/Tactic.thy

author | wenzelm |

Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) | |

changeset 58957 | c9e744ea8a38 |

parent 58956 | a816aa3ff391 |

child 58963 | 26bf09b95dda |

permissions | -rw-r--r-- |

proper context for match_tac etc.;

1 theory Tactic

2 imports Base

3 begin

5 chapter \<open>Tactical reasoning\<close>

7 text \<open>Tactical reasoning works by refining an initial claim in a

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

13 "tactical"} is a combinator for composing tactics.\<close>

16 section \<open>Goals \label{sec:tactical-goals}\<close>

18 text \<open>

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''.

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 arbitrary-but-fixed 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 1--2 in practice.

39 The main conclusion @{text C} is internally marked as a protected

40 proposition, which is represented explicitly by the notation @{text

41 "#C"} here. This ensures that the decomposition into subgoals and

42 main conclusion is well-defined for arbitrarily structured claims.

44 \medskip Basic goal management is performed via the following

45 Isabelle/Pure rules:

47 \[

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

49 \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}

50 \]

52 \medskip The following low-level variants admit general reasoning

53 with protected propositions:

55 \[

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

57 \]

58 \[

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

60 \]

61 \<close>

63 text %mlref \<open>

64 \begin{mldecls}

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

66 @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\

67 @{index_ML Goal.protect: "int -> thm -> thm"} \\

68 @{index_ML Goal.conclude: "thm -> thm"} \\

69 \end{mldecls}

71 \begin{description}

73 \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from

74 the well-formed proposition @{text C}.

76 \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem

77 @{text "thm"} is a solved goal (no subgoals), and concludes the

78 result by removing the goal protection. The context is only

79 required for printing error messages.

81 \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement

82 of theorem @{text "thm"}. The parameter @{text n} indicates the

83 number of premises to be retained.

85 \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal

86 protection, even if there are pending subgoals.

88 \end{description}

89 \<close>

92 section \<open>Tactics\label{sec:tactics}\<close>

94 text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that

95 maps a given goal state (represented as a theorem, cf.\

96 \secref{sec:tactical-goals}) to a lazy sequence of potential

97 successor states. The underlying sequence implementation is lazy

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

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

100 nature of ML requires some care when working with low-level

101 sequence operations, to avoid duplicate or premature evaluation of

102 results. It also means that modified runtime behavior, such as

103 timeout, is very hard to achieve for general tactics.}

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

106 a compound tactic expression other tactics might be tried instead,

107 or the whole refinement step might fail outright, producing a

108 toplevel error message in the end. When implementing tactics from

109 scratch, one should take care to observe the basic protocol of

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

111 faults should emerge as exceptions.

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

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

115 combinators for building proof tools that involve search

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

118 \medskip As explained before, a goal state essentially consists of a

119 list of subgoals that imply the main goal (conclusion). Tactics may

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

121 must not change the main conclusion (apart from instantiating

122 schematic goal variables).

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

125 @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal

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

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

128 an exception!

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

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

132 be affected, apart from instantiating schematic variables ranging

133 over the whole goal state.

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

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

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

138 into unrelated subgoals that happen to come after the original

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

140 very common error when implementing tactics!

142 Tactics with internal subgoal addressing should expose the subgoal

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

144 subgoal 1 is not acceptable.

146 \medskip The main well-formedness conditions for proper tactics are

147 summarized as follows.

149 \begin{itemize}

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

152 serious faults may produce an exception.

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

155 instantiating schematic variables.

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

158 specifically on a selected subgoal (without bumping into unrelated

159 subgoals).

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

163 \end{itemize}

165 Some of these conditions are checked by higher-level goal

166 infrastructure (\secref{sec:struct-goals}); others are not checked

167 explicitly, and violating them merely results in ill-behaved tactics

168 experienced by the user (e.g.\ tactics that insist in being

169 applicable only to singleton goals, or prevent composition via

170 standard tacticals such as @{ML REPEAT}).

171 \<close>

173 text %mlref \<open>

174 \begin{mldecls}

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

176 @{index_ML no_tac: tactic} \\

177 @{index_ML all_tac: tactic} \\

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

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

180 @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\

181 @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\

182 @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\

183 @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\

184 \end{mldecls}

186 \begin{description}

188 \item Type @{ML_type tactic} represents tactics. The

189 well-formedness conditions described above need to be observed. See

190 also @{file "~~/src/Pure/General/seq.ML"} for the underlying

191 implementation of lazy sequences.

193 \item Type @{ML_type "int -> tactic"} represents tactics with

194 explicit subgoal addressing, with well-formedness conditions as

195 described above.

197 \item @{ML no_tac} is a tactic that always fails, returning the

198 empty sequence.

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

201 singleton sequence with unchanged goal state.

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

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

205 channel.

207 \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule

208 into a tactic with unique result. Exception @{ML THM} is considered

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

210 exceptions are passed through.

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

213 most basic form to produce a tactic with subgoal addressing. The

214 given abstraction over the subgoal term and subgoal number allows to

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

216 subgoal range is checked as required above.

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

219 subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This

220 avoids expensive re-certification in situations where the subgoal is

221 used directly for primitive inferences.

223 \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the

224 specified subgoal @{text "i"}. This rearranges subgoals and the

225 main goal protection (\secref{sec:tactical-goals}), while retaining

226 the syntactic context of the overall goal state (concerning

227 schematic variables etc.).

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

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

231 without changing the main goal protection.

233 \end{description}

234 \<close>

237 subsection \<open>Resolution and assumption tactics \label{sec:resolve-assume-tac}\<close>

239 text \<open>\emph{Resolution} is the most basic mechanism for refining a

240 subgoal using a theorem as object-level rule.

241 \emph{Elim-resolution} is particularly suited for elimination rules:

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

243 finally deletes that assumption from any new subgoals.

244 \emph{Destruct-resolution} is like elim-resolution, but the given

245 destruction rules are first turned into canonical elimination

246 format. \emph{Forward-resolution} is like destruct-resolution, but

247 without deleting the selected assumption. The @{text "r/e/d/f"}

248 naming convention is maintained for several different kinds of

249 resolution rules and tactics.

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

252 against its conclusion.

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

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

256 indirectly, due to instantiation of schematic variables.

258 There are various sources of non-determinism, the tactic result

259 sequence enumerates all possibilities of the following choices (if

260 applicable):

262 \begin{enumerate}

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

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

267 the first premise of the rule;

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

270 the rule.

272 \end{enumerate}

274 Recall that higher-order unification may produce multiple results

275 that are enumerated here.

276 \<close>

278 text %mlref \<open>

279 \begin{mldecls}

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

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

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

283 @{index_ML forward_tac: "thm list -> int -> tactic"} \\

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

285 @{index_ML assume_tac: "int -> tactic"} \\

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

287 @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\

288 @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\

289 @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\

290 @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\

291 \end{mldecls}

293 \begin{description}

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

296 using the given theorems, which should normally be introduction

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

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

299 premises.

301 \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution

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

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

305 assume_tac}, which facilitates mixing of assumption steps with

306 genuine eliminations.

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

309 destruct-resolution with the given theorems, which should normally

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

311 applying one of the rules.

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

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

315 assumption, adding the result as a new assumption.

317 \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state

318 by resolution or elim-resolution on each rule, as indicated by its

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

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

322 flag is @{text "false"} and elim-resolution if the flag is @{text

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

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

325 systematically in proof tools.

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

328 by assumption (modulo higher-order unification).

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

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

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

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

334 instantiate variables, it cannot make other subgoals unprovable.

336 \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML

337 bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},

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

339 not instantiate schematic variables in the goal state.%

340 \footnote{Strictly speaking, matching means to treat the unknowns in the goal

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

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

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

344 will fail even though an acceptable unifier exists.}

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

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

348 \end{description}

349 \<close>

352 subsection \<open>Explicit instantiation within a subgoal context\<close>

354 text \<open>The main resolution tactics (\secref{sec:resolve-assume-tac})

355 use higher-order unification, which works well in many practical

356 situations despite its daunting theoretical properties.

357 Nonetheless, there are important problem classes where unguided

358 higher-order unification is not so useful. This typically involves

359 rules like universal elimination, existential introduction, or

360 equational substitution. Here the unification problem involves

361 fully flexible @{text "?P ?x"} schemes, which are hard to manage

362 without further hints.

364 By providing a (small) rigid term for @{text "?x"} explicitly, the

365 remaining unification problem is to assign a (large) term to @{text

366 "?P"}, according to the shape of the given subgoal. This is

367 sufficiently well-behaved in most practical situations.

369 \medskip Isabelle provides separate versions of the standard @{text

370 "r/e/d/f"} resolution tactics that allow to provide explicit

371 instantiations of unknowns of the given rule, wrt.\ terms that refer

372 to the implicit context of the selected subgoal.

374 An instantiation consists of a list of pairs of the form @{text

375 "(?x, t)"}, where @{text ?x} is a schematic variable occurring in

376 the given rule, and @{text t} is a term from the current proof

377 context, augmented by the local goal parameters of the selected

378 subgoal; cf.\ the @{text "focus"} operation described in

379 \secref{sec:variables}.

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

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

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

384 global names. Explicit renaming of subgoal parameters prior to

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

387 Type instantiations may be given as well, via pairs like @{text

388 "(?'a, \<tau>)"}. Type instantiations are distinguished from term

389 instantiations by the syntactic form of the schematic variable.

390 Types are instantiated before terms are. Since term instantiation

391 already performs simple type-inference, so explicit type

392 instantiations are seldom necessary.

393 \<close>

395 text %mlref \<open>

396 \begin{mldecls}

397 @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

398 @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

399 @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

400 @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\

401 @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\

402 @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\

403 @{index_ML rename_tac: "string list -> int -> tactic"} \\

404 \end{mldecls}

406 \begin{description}

408 \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the

409 rule @{text thm} with the instantiations @{text insts}, as described

410 above, and then performs resolution on subgoal @{text i}.

412 \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs

413 elim-resolution.

415 \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs

416 destruct-resolution.

418 \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that

419 the selected assumption is not deleted.

421 \item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition

422 @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the

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

425 \item @{ML thin_tac}~@{text "ctxt \<phi> i"} deletes the specified

426 premise from subgoal @{text i}. Note that @{text \<phi>} may contain

427 schematic variables, to abbreviate the intended proposition; the

428 first matching subgoal premise will be deleted. Removing useless

429 premises from a subgoal increases its readability and can make

430 search tactics run faster.

432 \item @{ML rename_tac}~@{text "names i"} renames the innermost

433 parameters of subgoal @{text i} according to the provided @{text

434 names} (which need to be distinct identifiers).

436 \end{description}

438 For historical reasons, the above instantiation tactics take

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

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

441 of \secref{sec:struct-goals} allows to refer to internal goal

442 structure with explicit context management.

443 \<close>

446 subsection \<open>Rearranging goal states\<close>

448 text \<open>In rare situations there is a need to rearrange goal states:

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

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

451 concrete presentation these conceptual sets of formulae.\<close>

453 text %mlref \<open>

454 \begin{mldecls}

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

456 @{index_ML distinct_subgoals_tac: tactic} \\

457 @{index_ML flexflex_tac: "Proof.context -> tactic"} \\

458 \end{mldecls}

460 \begin{description}

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

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

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

466 \item @{ML distinct_subgoals_tac} removes duplicate subgoals from a

467 proof state. This is potentially inefficient.

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

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

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

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

474 Flex-flex constraints arise from difficult cases of higher-order

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

476 some variables in a rule. Normally flex-flex constraints can be

477 ignored; they often disappear as unknowns get instantiated.

479 \end{description}

480 \<close>

483 subsection \<open>Raw composition: resolution without lifting\<close>

485 text \<open>

486 Raw composition of two rules means resolving them without prior

487 lifting or renaming of unknowns. This low-level operation, which

488 underlies the resolution tactics, may occasionally be useful for

489 special effects. Schematic variables are not renamed by default, so

490 beware of clashes!

491 \<close>

493 text %mlref \<open>

494 \begin{mldecls}

495 @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\

496 @{index_ML Drule.compose: "thm * int * thm -> thm"} \\

497 @{index_ML_op COMP: "thm * thm -> thm"} \\

498 \end{mldecls}

500 \begin{description}

502 \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal

503 @{text "i"} using @{text "rule"}, without lifting. The @{text

504 "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where

505 @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the

506 number of new subgoals. If @{text "flag"} is @{text "true"} then it

507 performs elim-resolution --- it solves the first premise of @{text

508 "rule"} by assumption and deletes that assumption.

510 \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},

511 regarded as an atomic formula, to solve premise @{text "i"} of

512 @{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text

513 "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. The unique @{text "s"} that

514 unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>

515 \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}. Multiple results are considered as

516 error (exception @{ML THM}).

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

519 (thm\<^sub>1, 1, thm\<^sub>2)"}.

521 \end{description}

523 \begin{warn}

524 These low-level operations are stepping outside the structure

525 imposed by regular rule resolution. Used without understanding of

526 the consequences, they may produce results that cause problems with

527 standard rules and tactics later on.

528 \end{warn}

529 \<close>

532 section \<open>Tacticals \label{sec:tacticals}\<close>

534 text \<open>A \emph{tactical} is a functional combinator for building up

535 complex tactics from simpler ones. Common tacticals perform

536 sequential composition, disjunctive choice, iteration, or goal

537 addressing. Various search strategies may be expressed via

538 tacticals.

539 \<close>

542 subsection \<open>Combining tactics\<close>

544 text \<open>Sequential composition and alternative choices are the most

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

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

547 @{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further

548 possibilities for fine-tuning alternation of tactics such as @{ML_op

549 "APPEND"}. Further details become visible in ML due to explicit

550 subgoal addressing.

551 \<close>

553 text %mlref \<open>

554 \begin{mldecls}

555 @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\

556 @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\

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

558 @{index_ML "EVERY": "tactic list -> tactic"} \\

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

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

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

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

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

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

566 \end{mldecls}

568 \begin{description}

570 \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential

571 composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal

572 state, it returns all states reachable in two steps by applying

573 @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it applies @{text

574 "tac\<^sub>1"} to the goal state, getting a sequence of possible next

575 states; then, it applies @{text "tac\<^sub>2"} to each of these and

576 concatenates the results to produce again one flat sequence of

577 states.

579 \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice

580 between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it

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

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

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

584 from the result.

586 \item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the

587 possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike

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

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

590 the cost of potential inefficiencies.

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

593 "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.

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

595 succeeds.

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

598 "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text

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

600 always fails.

602 \item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for

603 tactics with explicit subgoal addressing. So @{text

604 "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text

605 "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.

607 The other primed tacticals work analogously.

609 \end{description}

610 \<close>

613 subsection \<open>Repetition tacticals\<close>

615 text \<open>These tacticals provide further control over repetition of

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

617 ``@{verbatim "+"}'' in Isar method expressions.\<close>

619 text %mlref \<open>

620 \begin{mldecls}

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

622 @{index_ML "REPEAT": "tactic -> tactic"} \\

623 @{index_ML "REPEAT1": "tactic -> tactic"} \\

624 @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\

625 @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\

626 \end{mldecls}

628 \begin{description}

630 \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal

631 state and returns the resulting sequence, if non-empty; otherwise it

632 returns the original state. Thus, it applies @{text "tac"} at most

633 once.

635 Note that for tactics with subgoal addressing, the combinator can be

636 applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text

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

639 \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal

640 state and, recursively, to each element of the resulting sequence.

641 The resulting sequence consists of those states that make @{text

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

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

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

645 REPEAT_DETERM}, but requires more space.

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

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

649 is impossible.

651 \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the

652 goal state and, recursively, to the head of the resulting sequence.

653 It returns the first state to make @{text "tac"} fail. It is

654 deterministic, discarding alternative outcomes.

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

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

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

660 \end{description}

661 \<close>

663 text %mlex \<open>The basic tactics and tacticals considered above follow

664 some algebraic laws:

666 \begin{itemize}

668 \item @{ML all_tac} is the identity element of the tactical @{ML_op

669 "THEN"}.

671 \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and

672 @{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"},

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

674 equivalent to @{ML no_tac}.

676 \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)

677 functions over more basic combinators (ignoring some internal

678 implementation tricks):

680 \end{itemize}

681 \<close>

683 ML \<open>

684 fun TRY tac = tac ORELSE all_tac;

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

686 \<close>

688 text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML

689 REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML_op "ORELSE"} and not

690 @{ML_op "APPEND"}, it applies @{text "tac"} as many times as

691 possible in each outcome.

693 \begin{warn}

694 Note the explicit abstraction over the goal state in the ML

695 definition of @{ML REPEAT}. Recursive tacticals must be coded in

696 this awkward fashion to avoid infinite recursion of eager functional

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

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

699 \end{warn}

700 \<close>

702 ML \<open>

703 (*BAD -- does not terminate!*)

704 fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;

705 \<close>

708 subsection \<open>Applying tactics to subgoal ranges\<close>

710 text \<open>Tactics with explicit subgoal addressing

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

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

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

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

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

717 these tacticals address subgoal ranges counting downwards from

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

719 newly emerging subgoals are concatenated in the result, without

720 interfering each other. Nonetheless, there might be situations

721 where a different order is desired.\<close>

723 text %mlref \<open>

724 \begin{mldecls}

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

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

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

728 @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\

729 @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\

730 @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\

731 @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\

732 \end{mldecls}

734 \begin{description}

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

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

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

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

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

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

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

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

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

748 \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.

749 It applies @{text "tac"} unconditionally to the first subgoal.

751 \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or

752 more to a subgoal, counting downwards.

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

755 more to a subgoal, counting upwards.

757 \item @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to

758 @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op

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

760 corresponding range of subgoals, counting downwards.

762 \end{description}

763 \<close>

766 subsection \<open>Control and search tacticals\<close>

768 text \<open>A predicate on theorems @{ML_type "thm -> bool"} can test

769 whether a goal state enjoys some desirable property --- such as

770 having no subgoals. Tactics that search for satisfactory goal

771 states are easy to express. The main search procedures,

772 depth-first, breadth-first and best-first, are provided as

773 tacticals. They generate the search tree by repeatedly applying a

774 given tactic.\<close>

777 text %mlref ""

779 subsubsection \<open>Filtering a tactic's results\<close>

781 text \<open>

782 \begin{mldecls}

783 @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\

784 @{index_ML CHANGED: "tactic -> tactic"} \\

785 \end{mldecls}

787 \begin{description}

789 \item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the

790 goal state and returns a sequence consisting of those result goal

791 states that are satisfactory in the sense of @{text "sat"}.

793 \item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal

794 state and returns precisely those states that differ from the

795 original state (according to @{ML Thm.eq_thm}). Thus @{ML

796 CHANGED}~@{text "tac"} always has some effect on the state.

798 \end{description}

799 \<close>

802 subsubsection \<open>Depth-first search\<close>

804 text \<open>

805 \begin{mldecls}

806 @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\

807 @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\

808 @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\

809 \end{mldecls}

811 \begin{description}

813 \item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if

814 @{text "sat"} returns true. Otherwise it applies @{text "tac"},

815 then recursively searches from each element of the resulting

816 sequence. The code uses a stack for efficiency, in effect applying

817 @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to

818 the state.

820 \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to

821 search for states having no subgoals.

823 \item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to

824 search for states having fewer subgoals than the given state. Thus,

825 it insists upon solving at least one subgoal.

827 \end{description}

828 \<close>

831 subsubsection \<open>Other search strategies\<close>

833 text \<open>

834 \begin{mldecls}

835 @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\

836 @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\

837 @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\

838 \end{mldecls}

840 These search strategies will find a solution if one exists.

841 However, they do not enumerate all solutions; they terminate after

842 the first satisfactory result from @{text "tac"}.

844 \begin{description}

846 \item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first

847 search to find states for which @{text "sat"} is true. For most

848 applications, it is too slow.

850 \item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic

851 search, using @{text "dist"} to estimate the distance from a

852 satisfactory state (in the sense of @{text "sat"}). It maintains a

853 list of states ordered by distance. It applies @{text "tac"} to the

854 head of this list; if the result contains any satisfactory states,

855 then it returns them. Otherwise, @{ML BEST_FIRST} adds the new

856 states to the list, and continues.

858 The distance function is typically @{ML size_of_thm}, which computes

859 the size of the state. The smaller the state, the fewer and simpler

860 subgoals it has.

862 \item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like

863 @{ML BEST_FIRST}, except that the priority queue initially contains

864 the result of applying @{text "tac\<^sub>0"} to the goal state. This

865 tactical permits separate tactics for starting the search and

866 continuing the search.

868 \end{description}

869 \<close>

872 subsubsection \<open>Auxiliary tacticals for searching\<close>

874 text \<open>

875 \begin{mldecls}

876 @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\

877 @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\

878 @{index_ML SOLVE: "tactic -> tactic"} \\

879 @{index_ML DETERM: "tactic -> tactic"} \\

880 \end{mldecls}

882 \begin{description}

884 \item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to

885 the goal state if it satisfies predicate @{text "sat"}, and applies

886 @{text "tac\<^sub>2"}. It is a conditional tactical in that only one of

887 @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.

888 However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated

889 because ML uses eager evaluation.

891 \item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the

892 goal state if it has any subgoals, and simply returns the goal state

893 otherwise. Many common tactics, such as @{ML resolve_tac}, fail if

894 applied to a goal state that has no subgoals.

896 \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal

897 state and then fails iff there are subgoals left.

899 \item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal

900 state and returns the head of the resulting sequence. @{ML DETERM}

901 limits the search space by making its argument deterministic.

903 \end{description}

904 \<close>

907 subsubsection \<open>Predicates and functions useful for searching\<close>

909 text \<open>

910 \begin{mldecls}

911 @{index_ML has_fewer_prems: "int -> thm -> bool"} \\

912 @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\

913 @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\

914 @{index_ML size_of_thm: "thm -> int"} \\

915 \end{mldecls}

917 \begin{description}

919 \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text

920 "thm"} has fewer than @{text "n"} premises.

922 \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text

923 "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the

924 same conclusions, the same set of hypotheses, and the same set of sort

925 hypotheses. Names of bound variables are ignored as usual.

927 \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether

928 the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.

929 Names of bound variables are ignored.

931 \item @{ML size_of_thm}~@{text "thm"} computes the size of @{text

932 "thm"}, namely the number of variables, constants and abstractions

933 in its conclusion. It may serve as a distance function for

934 @{ML BEST_FIRST}.

936 \end{description}

937 \<close>

939 end