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

doc-src/IsarImplementation/Thy/Tactic.thy

author | wenzelm |

Wed Jan 25 18:18:59 2012 +0100 (2012-01-25) | |

changeset 46258 | 89ee3bc580a8 |

parent 40800 | 330eb65c9469 |

child 46259 | 6fab37137dcb |

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

updated THEN, ORELSE, APPEND, and derivatives;

discontinued obscure INTLEAVE;

discontinued obscure INTLEAVE;

1 theory Tactic

2 imports Base

3 begin

5 chapter {* Tactical reasoning *}

7 text {* 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. *}

16 section {* Goals \label{sec:tactical-goals} *}

18 text {*

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)"}]{@{text "#C"}}{@{text "C"}} \qquad

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

58 \]

59 *}

61 text %mlref {*

62 \begin{mldecls}

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

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

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

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

67 \end{mldecls}

69 \begin{description}

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

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

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

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

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

77 required for printing error messages.

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

80 of theorem @{text "thm"}.

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

83 protection, even if there are pending subgoals.

85 \end{description}

86 *}

89 section {* Tactics\label{sec:tactics} *}

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

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

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

94 successor states. The underlying sequence implementation is lazy

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

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

97 nature of SML requires some care when working with low-level

98 sequence operations, to avoid duplicate or premature evaluation of

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

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

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

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

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

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

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

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

108 faults should emerge as exceptions.

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

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

112 combinators for building proof tools that involve search

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

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

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

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

118 must not change the main conclusion (apart from instantiating

119 schematic goal variables).

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

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

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

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

125 an exception!

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

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

129 be affected, apart from instantiating schematic variables ranging

130 over the whole goal state.

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

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

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

135 into unrelated subgoals that happen to come after the original

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

137 very common error when implementing tactics!

139 Tactics with internal subgoal addressing should expose the subgoal

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

141 subgoal 1 is not acceptable.

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

144 summarized as follows.

146 \begin{itemize}

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

149 serious faults may produce an exception.

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

152 instantiating schematic variables.

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

155 specifically on a selected subgoal (without bumping into unrelated

156 subgoals).

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

160 \end{itemize}

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

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

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

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

166 applicable only to singleton goals, or prevent composition via

167 standard tacticals).

168 *}

170 text %mlref {*

171 \begin{mldecls}

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

173 @{index_ML no_tac: tactic} \\

174 @{index_ML all_tac: tactic} \\

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

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

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

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

179 \end{mldecls}

181 \begin{description}

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

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

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

186 implementation of lazy sequences.

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

189 explicit subgoal addressing, with well-formedness conditions as

190 described above.

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

193 empty sequence.

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

196 singleton sequence with unchanged goal state.

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

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

200 channel.

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

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

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

205 exceptions are passed through.

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

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

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

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

211 subgoal range is checked as required above.

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

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

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

216 used directly for primitive inferences.

218 \end{description}

219 *}

222 subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *}

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

225 subgoal using a theorem as object-level rule.

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

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

228 finally deletes that assumption from any new subgoals.

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

230 destruction rules are first turned into canonical elimination

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

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

233 naming convention is maintained for several different kinds of

234 resolution rules and tactics.

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

237 against its conclusion.

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

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

241 indirectly, due to instantiation of schematic variables.

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

244 sequence enumerates all possibilities of the following choices (if

245 applicable):

247 \begin{enumerate}

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

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

252 the first premise of the rule;

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

255 the rule.

257 \end{enumerate}

259 Recall that higher-order unification may produce multiple results

260 that are enumerated here.

261 *}

263 text %mlref {*

264 \begin{mldecls}

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

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

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

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

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

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

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

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

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

274 \end{mldecls}

276 \begin{description}

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

279 using the given theorems, which should normally be introduction

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

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

282 premises.

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

285 with the given theorems, which should normally be elimination rules.

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

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

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

290 applying one of the rules.

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

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

294 assumption, adding the result as a new assumption.

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

297 by assumption (modulo higher-order unification).

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

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

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

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

303 instantiate variables, it cannot make other subgoals unprovable.

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

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

307 dresolve_tac}, respectively, but do not instantiate schematic

308 variables in the goal state.

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

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

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

313 update the goal state.

315 \end{description}

316 *}

319 subsection {* Explicit instantiation within a subgoal context *}

321 text {* The main resolution tactics (\secref{sec:resolve-assume-tac})

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

323 situations despite its daunting theoretical properties.

324 Nonetheless, there are important problem classes where unguided

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

326 rules like universal elimination, existential introduction, or

327 equational substitution. Here the unification problem involves

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

329 without further hints.

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

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

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

334 sufficiently well-behaved in most practical situations.

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

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

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

339 to the implicit context of the selected subgoal.

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

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

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

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

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

346 \secref{sec:variables}.

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

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

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

351 global names. Explicit renaming of subgoal parameters prior to

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

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

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

356 instantiations by the syntactic form of the schematic variable.

357 Types are instantiated before terms are. Since term instantiation

358 already performs simple type-inference, so explicit type

359 instantiations are seldom necessary.

360 *}

362 text %mlref {*

363 \begin{mldecls}

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

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

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

367 @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex]

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

369 \end{mldecls}

371 \begin{description}

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

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

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

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

378 elim-resolution.

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

381 destruct-resolution.

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

384 the selected assumption is not deleted.

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

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

388 names} (which need to be distinct indentifiers).

390 \end{description}

392 For historical reasons, the above instantiation tactics take

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

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

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

396 structure with explicit context management.

397 *}

400 section {* Tacticals \label{sec:tacticals} *}

402 text {* A \emph{tactical} is a functional combinator for building up

403 complex tactics from simpler ones. Common tacticals perform

404 sequential composition, disjunctive choice, iteration, or goal

405 addressing. Various search strategies may be expressed via

406 tacticals.

408 \medskip The chapter on tacticals in old \cite{isabelle-ref} is

409 still applicable for further details. *}

412 subsection {* Combining tactics *}

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

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

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

417 @{text "THEN"} and @{text "ORELSE"} in ML, but there are further

418 possibilities for fine-tuning alternation of tactics such as @{text

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

420 subgoal addressing. *}

422 text %mlref {*

423 \begin{mldecls}

424 @{index_ML "op THEN": "tactic * tactic -> tactic"} \\

425 @{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\

426 @{index_ML "op APPEND": "tactic * tactic -> tactic"} \\

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

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

430 @{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\

431 @{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\

432 @{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\

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

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

435 @{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\

436 @{index_ML "FIRST1": "(int -> tactic) list -> tactic"} \\[0.5ex]

437 \end{mldecls}

439 \begin{description}

441 \item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of

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

443 returns all states reachable in two steps by applying @{text "tac\<^sub>1"}

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

445 proof state, getting a sequence of possible next states; then, it

446 applies @{text "tac\<^sub>2"} to each of these and concatenates the results

447 to produce again one flat sequence of states.

449 \item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text

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

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

452 then it uses @{text "tac\<^sub>2"}. This is a deterministic choice: if

453 @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the

454 result.

456 \item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results

457 of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike @{text "ORELSE"} there

458 is \emph{no commitment} to either tactic, so @{text "APPEND"} helps

459 to avoid incompleteness during search, at the cost of potential

460 inefficiencies.

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

463 \<dots> THEN tac\<^sub>n"}. Note that @{text "EVERY []"} is the same as @{ML

464 all_tac}: it always succeeds.

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

467 ORELSE \<dots> ORELSE tac\<^sub>n"}. Note that @{text "FIRST []"} is the same as

468 @{ML no_tac}: it always fails.

470 \item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are

471 lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text

472 "APPEND"}, for tactics with explicit subgoal addressing. This means

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

474 tac\<^sub>2 i)"} etc.

476 \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of

477 @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit

478 subgoal addressing.

480 \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions

481 of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1.

483 \end{description}

484 *}

486 end