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

doc-src/IsarRef/Thy/Proof.thy

author | noschinl |

Thu Oct 13 13:49:55 2011 +0200 (2011-10-13 ago) | |

changeset 45135 | 5ba2f065c6f7 |

parent 45103 | a45121ffcfcb |

child 46262 | 912b42e64fde |

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

tuned markup

1 theory Proof

2 imports Base Main

3 begin

5 chapter {* Proofs \label{ch:proofs} *}

7 text {*

8 Proof commands perform transitions of Isar/VM machine

9 configurations, which are block-structured, consisting of a stack of

10 nodes with three main components: logical proof context, current

11 facts, and open goals. Isar/VM transitions are typed according to

12 the following three different modes of operation:

14 \begin{description}

16 \item @{text "proof(prove)"} means that a new goal has just been

17 stated that is now to be \emph{proven}; the next command may refine

18 it by some proof method, and enter a sub-proof to establish the

19 actual result.

21 \item @{text "proof(state)"} is like a nested theory mode: the

22 context may be augmented by \emph{stating} additional assumptions,

23 intermediate results etc.

25 \item @{text "proof(chain)"} is intermediate between @{text

26 "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\

27 the contents of the special ``@{fact_ref this}'' register) have been

28 just picked up in order to be used when refining the goal claimed

29 next.

31 \end{description}

33 The proof mode indicator may be understood as an instruction to the

34 writer, telling what kind of operation may be performed next. The

35 corresponding typings of proof commands restricts the shape of

36 well-formed proof texts to particular command sequences. So dynamic

37 arrangements of commands eventually turn out as static texts of a

38 certain structure.

40 \Appref{ap:refcard} gives a simplified grammar of the (extensible)

41 language emerging that way from the different types of proof

42 commands. The main ideas of the overall Isar framework are

43 explained in \chref{ch:isar-framework}.

44 *}

47 section {* Proof structure *}

49 subsection {* Formal notepad *}

51 text {*

52 \begin{matharray}{rcl}

53 @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\

54 \end{matharray}

56 @{rail "

57 @@{command notepad} @'begin'

58 ;

59 @@{command end}

60 "}

62 \begin{description}

64 \item @{command "notepad"}~@{keyword "begin"} opens a proof state

65 without any goal statement. This allows to experiment with Isar,

66 without producing any persistent result.

68 The notepad can be closed by @{command "end"} or discontinued by

69 @{command "oops"}.

71 \end{description}

72 *}

75 subsection {* Blocks *}

77 text {*

78 \begin{matharray}{rcl}

79 @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

80 @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

81 @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

82 \end{matharray}

84 While Isar is inherently block-structured, opening and closing

85 blocks is mostly handled rather casually, with little explicit

86 user-intervention. Any local goal statement automatically opens

87 \emph{two} internal blocks, which are closed again when concluding

88 the sub-proof (by @{command "qed"} etc.). Sections of different

89 context within a sub-proof may be switched via @{command "next"},

90 which is just a single block-close followed by block-open again.

91 The effect of @{command "next"} is to reset the local proof context;

92 there is no goal focus involved here!

94 For slightly more advanced applications, there are explicit block

95 parentheses as well. These typically achieve a stronger forward

96 style of reasoning.

98 \begin{description}

100 \item @{command "next"} switches to a fresh block within a

101 sub-proof, resetting the local context to the initial one.

103 \item @{command "{"} and @{command "}"} explicitly open and close

104 blocks. Any current facts pass through ``@{command "{"}''

105 unchanged, while ``@{command "}"}'' causes any result to be

106 \emph{exported} into the enclosing context. Thus fixed variables

107 are generalized, assumptions discharged, and local definitions

108 unfolded (cf.\ \secref{sec:proof-context}). There is no difference

109 of @{command "assume"} and @{command "presume"} in this mode of

110 forward reasoning --- in contrast to plain backward reasoning with

111 the result exported at @{command "show"} time.

113 \end{description}

114 *}

117 subsection {* Omitting proofs *}

119 text {*

120 \begin{matharray}{rcl}

121 @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\

122 \end{matharray}

124 The @{command "oops"} command discontinues the current proof

125 attempt, while considering the partial proof text as properly

126 processed. This is conceptually quite different from ``faking''

127 actual proofs via @{command_ref "sorry"} (see

128 \secref{sec:proof-steps}): @{command "oops"} does not observe the

129 proof structure at all, but goes back right to the theory level.

130 Furthermore, @{command "oops"} does not produce any result theorem

131 --- there is no intended claim to be able to complete the proof

132 in any way.

134 A typical application of @{command "oops"} is to explain Isar proofs

135 \emph{within} the system itself, in conjunction with the document

136 preparation tools of Isabelle described in \chref{ch:document-prep}.

137 Thus partial or even wrong proof attempts can be discussed in a

138 logically sound manner. Note that the Isabelle {\LaTeX} macros can

139 be easily adapted to print something like ``@{text "\<dots>"}'' instead of

140 the keyword ``@{command "oops"}''.

142 \medskip The @{command "oops"} command is undo-able, unlike

143 @{command_ref "kill"} (see \secref{sec:history}). The effect is to

144 get back to the theory just before the opening of the proof.

145 *}

148 section {* Statements *}

150 subsection {* Context elements \label{sec:proof-context} *}

152 text {*

153 \begin{matharray}{rcl}

154 @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

155 @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

156 @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

157 @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

158 \end{matharray}

160 The logical proof context consists of fixed variables and

161 assumptions. The former closely correspond to Skolem constants, or

162 meta-level universal quantification as provided by the Isabelle/Pure

163 logical framework. Introducing some \emph{arbitrary, but fixed}

164 variable via ``@{command "fix"}~@{text x}'' results in a local value

165 that may be used in the subsequent proof as any other variable or

166 constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from

167 the context will be universally closed wrt.\ @{text x} at the

168 outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal

169 form using Isabelle's meta-variables).

171 Similarly, introducing some assumption @{text \<chi>} has two effects.

172 On the one hand, a local theorem is created that may be used as a

173 fact in subsequent proof steps. On the other hand, any result

174 @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\

175 the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal

176 using such a result would basically introduce a new subgoal stemming

177 from the assumption. How this situation is handled depends on the

178 version of assumption command used: while @{command "assume"}

179 insists on solving the subgoal by unification with some premise of

180 the goal, @{command "presume"} leaves the subgoal unchanged in order

181 to be proved later by the user.

183 Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>

184 t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with

185 another version of assumption that causes any hypothetical equation

186 @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,

187 exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>

188 \<phi>[t]"}.

190 @{rail "

191 @@{command fix} (@{syntax vars} + @'and')

192 ;

193 (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')

194 ;

195 @@{command def} (def + @'and')

196 ;

197 def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?

198 "}

200 \begin{description}

202 \item @{command "fix"}~@{text x} introduces a local variable @{text

203 x} that is \emph{arbitrary, but fixed.}

205 \item @{command "assume"}~@{text "a: \<phi>"} and @{command

206 "presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by

207 assumption. Subsequent results applied to an enclosing goal (e.g.\

208 by @{command_ref "show"}) are handled as follows: @{command

209 "assume"} expects to be able to unify with existing premises in the

210 goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.

212 Several lists of assumptions may be given (separated by

213 @{keyword_ref "and"}; the resulting list of current facts consists

214 of all of these concatenated.

216 \item @{command "def"}~@{text "x \<equiv> t"} introduces a local

217 (non-polymorphic) definition. In results exported from the context,

218 @{text x} is replaced by @{text t}. Basically, ``@{command

219 "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text

220 x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting

221 hypothetical equation solved by reflexivity.

223 The default name for the definitional equation is @{text x_def}.

224 Several simultaneous definitions may be given at the same time.

226 \end{description}

228 The special name @{fact_ref prems} refers to all assumptions of the

229 current context as a list of theorems. This feature should be used

230 with great care! It is better avoided in final proof texts.

231 *}

234 subsection {* Term abbreviations \label{sec:term-abbrev} *}

236 text {*

237 \begin{matharray}{rcl}

238 @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

239 @{keyword_def "is"} & : & syntax \\

240 \end{matharray}

242 Abbreviations may be either bound by explicit @{command

243 "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or

244 goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>

245 p\<^sub>n)"}''. In both cases, higher-order matching is invoked to

246 bind extra-logical term variables, which may be either named

247 schematic variables of the form @{text ?x}, or nameless dummies

248 ``@{variable _}'' (underscore). Note that in the @{command "let"}

249 form the patterns occur on the left-hand side, while the @{keyword

250 "is"} patterns are in postfix position.

252 Polymorphism of term bindings is handled in Hindley-Milner style,

253 similar to ML. Type variables referring to local assumptions or

254 open goal statements are \emph{fixed}, while those of finished

255 results or bound by @{command "let"} may occur in \emph{arbitrary}

256 instances later. Even though actual polymorphism should be rarely

257 used in practice, this mechanism is essential to achieve proper

258 incremental type-inference, as the user proceeds to build up the

259 Isar proof text from left to right.

261 \medskip Term abbreviations are quite different from local

262 definitions as introduced via @{command "def"} (see

263 \secref{sec:proof-context}). The latter are visible within the

264 logic as actual equations, while abbreviations disappear during the

265 input process just after type checking. Also note that @{command

266 "def"} does not support polymorphism.

268 @{rail "

269 @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')

270 "}

272 The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or

273 @{syntax prop_pat} (see \secref{sec:term-decls}).

275 \begin{description}

277 \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any

278 text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous

279 higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.

281 \item @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but

282 matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement. Also

283 note that @{keyword "is"} is not a separate command, but part of

284 others (such as @{command "assume"}, @{command "have"} etc.).

286 \end{description}

288 Some \emph{implicit} term abbreviations\index{term abbreviations}

289 for goals and facts are available as well. For any open goal,

290 @{variable_ref thesis} refers to its object-level statement,

291 abstracted over any meta-level parameters (if present). Likewise,

292 @{variable_ref this} is bound for fact statements resulting from

293 assumptions or finished goals. In case @{variable this} refers to

294 an object-logic statement that is an application @{text "f t"}, then

295 @{text t} is bound to the special text variable ``@{variable "\<dots>"}''

296 (three dots). The canonical application of this convenience are

297 calculational proofs (see \secref{sec:calculation}).

298 *}

301 subsection {* Facts and forward chaining *}

303 text {*

304 \begin{matharray}{rcl}

305 @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

306 @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

307 @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

308 @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

309 @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

310 @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

311 \end{matharray}

313 New facts are established either by assumption or proof of local

314 statements. Any fact will usually be involved in further proofs,

315 either as explicit arguments of proof methods, or when forward

316 chaining towards the next goal via @{command "then"} (and variants);

317 @{command "from"} and @{command "with"} are composite forms

318 involving @{command "note"}. The @{command "using"} elements

319 augments the collection of used facts \emph{after} a goal has been

320 stated. Note that the special theorem name @{fact_ref this} refers

321 to the most recently established facts, but only \emph{before}

322 issuing a follow-up claim.

324 @{rail "

325 @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')

326 ;

327 (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})

328 (@{syntax thmrefs} + @'and')

329 "}

331 \begin{description}

333 \item @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts

334 @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. Note that

335 attributes may be involved as well, both on the left and right hand

336 sides.

338 \item @{command "then"} indicates forward chaining by the current

339 facts in order to establish the goal to be claimed next. The

340 initial proof method invoked to refine that will be offered the

341 facts to do ``anything appropriate'' (see also

342 \secref{sec:proof-steps}). For example, method @{method (Pure) rule}

343 (see \secref{sec:pure-meth-att}) would typically do an elimination

344 rather than an introduction. Automatic methods usually insert the

345 facts into the goal state before operation. This provides a simple

346 scheme to control relevance of facts in automated proof search.

348 \item @{command "from"}~@{text b} abbreviates ``@{command

349 "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is

350 equivalent to ``@{command "from"}~@{text this}''.

352 \item @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command

353 "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining

354 is from earlier facts together with the current ones.

356 \item @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being

357 currently indicated for use by a subsequent refinement step (such as

358 @{command_ref "apply"} or @{command_ref "proof"}).

360 \item @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally

361 similar to @{command "using"}, but unfolds definitional equations

362 @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.

364 \end{description}

366 Forward chaining with an empty list of theorems is the same as not

367 chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no

368 effect apart from entering @{text "prove(chain)"} mode, since

369 @{fact_ref nothing} is bound to the empty list of theorems.

371 Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple

372 facts to be given in their proper order, corresponding to a prefix

373 of the premises of the rule involved. Note that positions may be

374 easily skipped using something like @{command "from"}~@{text "_

375 \<AND> a \<AND> b"}, for example. This involves the trivial rule

376 @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as

377 ``@{fact_ref "_"}'' (underscore).

379 Automated methods (such as @{method simp} or @{method auto}) just

380 insert any given facts before their usual operation. Depending on

381 the kind of procedure involved, the order of facts is less

382 significant here.

383 *}

386 subsection {* Goals \label{sec:goals} *}

388 text {*

389 \begin{matharray}{rcl}

390 @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

391 @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

392 @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

393 @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

394 @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

395 @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

396 @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

397 @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

398 @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\

399 @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\

400 @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

401 \end{matharray}

403 From a theory context, proof mode is entered by an initial goal

404 command such as @{command "lemma"}, @{command "theorem"}, or

405 @{command "corollary"}. Within a proof, new claims may be

406 introduced locally as well; four variants are available here to

407 indicate whether forward chaining of facts should be performed

408 initially (via @{command_ref "then"}), and whether the final result

409 is meant to solve some pending goal.

411 Goals may consist of multiple statements, resulting in a list of

412 facts eventually. A pending multi-goal is internally represented as

413 a meta-level conjunction (@{text "&&&"}), which is usually

414 split into the corresponding number of sub-goals prior to an initial

415 method application, via @{command_ref "proof"}

416 (\secref{sec:proof-steps}) or @{command_ref "apply"}

417 (\secref{sec:tactic-commands}). The @{method_ref induct} method

418 covered in \secref{sec:cases-induct} acts on multiple claims

419 simultaneously.

421 Claims at the theory level may be either in short or long form. A

422 short goal merely consists of several simultaneous propositions

423 (often just one). A long goal includes an explicit context

424 specification for the subsequent conclusion, involving local

425 parameters and assumptions. Here the role of each part of the

426 statement is explicitly marked by separate keywords (see also

427 \secref{sec:locale}); the local assumptions being introduced here

428 are available as @{fact_ref assms} in the proof. Moreover, there

429 are two kinds of conclusions: @{element_def "shows"} states several

430 simultaneous propositions (essentially a big conjunction), while

431 @{element_def "obtains"} claims several simultaneous simultaneous

432 contexts of (essentially a big disjunction of eliminated parameters

433 and assumptions, cf.\ \secref{sec:obtain}).

435 @{rail "

436 (@@{command lemma} | @@{command theorem} | @@{command corollary} |

437 @@{command schematic_lemma} | @@{command schematic_theorem} |

438 @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)

439 ;

440 (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal

441 ;

442 @@{command print_statement} @{syntax modes}? @{syntax thmrefs}

443 ;

445 goal: (@{syntax props} + @'and')

446 ;

447 longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion

448 ;

449 conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')

450 ;

451 case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')

452 "}

454 \begin{description}

456 \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with

457 @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>

458 \<phi>"} to be put back into the target context. An additional @{syntax

459 context} specification may build up an initial proof context for the

460 subsequent claim; this includes local definitions and syntax as

461 well, see the definition of @{syntax context_elem} in

462 \secref{sec:locale}.

464 \item @{command "theorem"}~@{text "a: \<phi>"} and @{command

465 "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command

466 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as

467 being of a different kind. This discrimination acts like a formal

468 comment.

470 \item @{command "schematic_lemma"}, @{command "schematic_theorem"},

471 @{command "schematic_corollary"} are similar to @{command "lemma"},

472 @{command "theorem"}, @{command "corollary"}, respectively but allow

473 the statement to contain unbound schematic variables.

475 Under normal circumstances, an Isar proof text needs to specify

476 claims explicitly. Schematic goals are more like goals in Prolog,

477 where certain results are synthesized in the course of reasoning.

478 With schematic statements, the inherent compositionality of Isar

479 proofs is lost, which also impacts performance, because proof

480 checking is forced into sequential mode.

482 \item @{command "have"}~@{text "a: \<phi>"} claims a local goal,

483 eventually resulting in a fact within the current logical context.

484 This operation is completely independent of any pending sub-goals of

485 an enclosing goal statements, so @{command "have"} may be freely

486 used for experimental exploration of potential results within a

487 proof body.

489 \item @{command "show"}~@{text "a: \<phi>"} is like @{command

490 "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending

491 sub-goal for each one of the finished result, after having been

492 exported into the corresponding context (at the head of the

493 sub-proof of this @{command "show"} command).

495 To accommodate interactive debugging, resulting rules are printed

496 before being applied internally. Even more, interactive execution

497 of @{command "show"} predicts potential failure and displays the

498 resulting error as a warning beforehand. Watch out for the

499 following message:

501 %FIXME proper antiquitation

502 \begin{ttbox}

503 Problem! Local statement will fail to solve any pending goal

504 \end{ttbox}

506 \item @{command "hence"} abbreviates ``@{command "then"}~@{command

507 "have"}'', i.e.\ claims a local goal to be proven by forward

508 chaining the current facts. Note that @{command "hence"} is also

509 equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.

511 \item @{command "thus"} abbreviates ``@{command "then"}~@{command

512 "show"}''. Note that @{command "thus"} is also equivalent to

513 ``@{command "from"}~@{text this}~@{command "show"}''.

515 \item @{command "print_statement"}~@{text a} prints facts from the

516 current theory or proof context in long statement form, according to

517 the syntax for @{command "lemma"} given above.

519 \end{description}

521 Any goal statement causes some term abbreviations (such as

522 @{variable_ref "?thesis"}) to be bound automatically, see also

523 \secref{sec:term-abbrev}.

525 The optional case names of @{element_ref "obtains"} have a twofold

526 meaning: (1) during the of this claim they refer to the the local

527 context introductions, (2) the resulting rule is annotated

528 accordingly to support symbolic case splits when used with the

529 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).

530 *}

533 section {* Refinement steps *}

535 subsection {* Proof method expressions \label{sec:proof-meth} *}

537 text {* Proof methods are either basic ones, or expressions composed

538 of methods via ``@{verbatim ","}'' (sequential composition),

539 ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''

540 (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim

541 "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}

542 sub-goals, with default @{text "n = 1"}). In practice, proof

543 methods are usually just a comma separated list of @{syntax

544 nameref}~@{syntax args} specifications. Note that parentheses may

545 be dropped for single method specifications (with no arguments).

547 @{rail "

548 @{syntax_def method}:

549 (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')

550 ;

551 methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|')

552 "}

554 Proper Isar proof methods do \emph{not} admit arbitrary goal

555 addressing, but refer either to the first sub-goal or all sub-goals

556 uniformly. The goal restriction operator ``@{text "[n]"}''

557 evaluates a method expression within a sandbox consisting of the

558 first @{text n} sub-goals (which need to exist). For example, the

559 method ``@{text "simp_all[3]"}'' simplifies the first three

560 sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all

561 new goals that emerge from applying rule @{text "foo"} to the

562 originally first one.

564 Improper methods, notably tactic emulations, offer a separate

565 low-level goal addressing scheme as explicit argument to the

566 individual tactic being involved. Here ``@{text "[!]"}'' refers to

567 all goals, and ``@{text "[n-]"}'' to all goals starting from @{text

568 "n"}.

570 @{rail "

571 @{syntax_def goal_spec}:

572 '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'

573 "}

574 *}

577 subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}

579 text {*

580 \begin{matharray}{rcl}

581 @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\

582 @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\

583 @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

584 @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

585 @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

586 @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

587 \end{matharray}

589 Arbitrary goal refinement via tactics is considered harmful.

590 Structured proof composition in Isar admits proof methods to be

591 invoked in two places only.

593 \begin{enumerate}

595 \item An \emph{initial} refinement step @{command_ref

596 "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number

597 of sub-goals that are to be solved later. Facts are passed to

598 @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text

599 "proof(chain)"} mode.

601 \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text

602 "m\<^sub>2"} is intended to solve remaining goals. No facts are

603 passed to @{text "m\<^sub>2"}.

605 \end{enumerate}

607 The only other (proper) way to affect pending goals in a proof body

608 is by @{command_ref "show"}, which involves an explicit statement of

609 what is to be solved eventually. Thus we avoid the fundamental

610 problem of unstructured tactic scripts that consist of numerous

611 consecutive goal transformations, with invisible effects.

613 \medskip As a general rule of thumb for good proof style, initial

614 proof methods should either solve the goal completely, or constitute

615 some well-understood reduction to new sub-goals. Arbitrary

616 automatic proof tools that are prone leave a large number of badly

617 structured sub-goals are no help in continuing the proof document in

618 an intelligible manner.

620 Unless given explicitly by the user, the default initial method is

621 @{method_ref (Pure) rule} (or its classical variant @{method_ref

622 rule}), which applies a single standard elimination or introduction

623 rule according to the topmost symbol involved. There is no separate

624 default terminal method. Any remaining goals are always solved by

625 assumption in the very last step.

627 @{rail "

628 @@{command proof} method?

629 ;

630 @@{command qed} method?

631 ;

632 @@{command \"by\"} method method?

633 ;

634 (@@{command \".\"} | @@{command \"..\"} | @@{command sorry})

635 "}

637 \begin{description}

639 \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof

640 method @{text "m\<^sub>1"}; facts for forward chaining are passed if so

641 indicated by @{text "proof(chain)"} mode.

643 \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by

644 proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.

645 If the goal had been @{text "show"} (or @{text "thus"}), some

646 pending sub-goal is solved as well by the rule resulting from the

647 result \emph{exported} into the enclosing goal context. Thus @{text

648 "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the

649 resulting rule does not fit to any pending goal\footnote{This

650 includes any additional ``strong'' assumptions as introduced by

651 @{command "assume"}.} of the enclosing context. Debugging such a

652 situation might involve temporarily changing @{command "show"} into

653 @{command "have"}, or weakening the local context by replacing

654 occurrences of @{command "assume"} by @{command "presume"}.

656 \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal

657 proof}\index{proof!terminal}; it abbreviates @{command

658 "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with

659 backtracking across both methods. Debugging an unsuccessful

660 @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its

661 definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even

662 @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the

663 problem.

665 \item ``@{command ".."}'' is a \emph{default

666 proof}\index{proof!default}; it abbreviates @{command "by"}~@{text

667 "rule"}.

669 \item ``@{command "."}'' is a \emph{trivial

670 proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text

671 "this"}.

673 \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}

674 pretending to solve the pending claim without further ado. This

675 only works in interactive development, or if the @{ML

676 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake

677 proofs are not the real thing. Internally, each theorem container

678 is tainted by an oracle invocation, which is indicated as ``@{text

679 "[!]"}'' in the printed result.

681 The most important application of @{command "sorry"} is to support

682 experimentation and top-down proof development.

684 \end{description}

685 *}

688 subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}

690 text {*

691 The following proof methods and attributes refer to basic logical

692 operations of Isar. Further methods and attributes are provided by

693 several generic and object-logic specific tools and packages (see

694 \chref{ch:gen-tools} and \chref{ch:hol}).

696 \begin{matharray}{rcl}

697 @{method_def "-"} & : & @{text method} \\

698 @{method_def "fact"} & : & @{text method} \\

699 @{method_def "assumption"} & : & @{text method} \\

700 @{method_def "this"} & : & @{text method} \\

701 @{method_def (Pure) "rule"} & : & @{text method} \\

702 @{attribute_def (Pure) "intro"} & : & @{text attribute} \\

703 @{attribute_def (Pure) "elim"} & : & @{text attribute} \\

704 @{attribute_def (Pure) "dest"} & : & @{text attribute} \\

705 @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]

706 @{attribute_def "OF"} & : & @{text attribute} \\

707 @{attribute_def "of"} & : & @{text attribute} \\

708 @{attribute_def "where"} & : & @{text attribute} \\

709 \end{matharray}

711 @{rail "

712 @@{method fact} @{syntax thmrefs}?

713 ;

714 @@{method (Pure) rule} @{syntax thmrefs}?

715 ;

716 rulemod: ('intro' | 'elim' | 'dest')

717 ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}

718 ;

719 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})

720 ('!' | () | '?') @{syntax nat}?

721 ;

722 @@{attribute (Pure) rule} 'del'

723 ;

724 @@{attribute OF} @{syntax thmrefs}

725 ;

726 @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?

727 ;

728 @@{attribute \"where\"}

729 ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='

730 (@{syntax type} | @{syntax term}) * @'and')

731 "}

733 \begin{description}

735 \item ``@{method "-"}'' (minus) does nothing but insert the forward

736 chaining facts as premises into the goal. Note that command

737 @{command_ref "proof"} without any method actually performs a single

738 reduction step using the @{method_ref (Pure) rule} method; thus a plain

739 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text

740 "-"}'' rather than @{command "proof"} alone.

742 \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from

743 @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)

744 modulo unification of schematic type and term variables. The rule

745 structure is not taken into account, i.e.\ meta-level implication is

746 considered atomic. This is the same principle underlying literal

747 facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~@{text

748 "\<phi>"}~@{command "by"}~@{text fact}'' is equivalent to ``@{command

749 "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim "`"}'' provided that

750 @{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the

751 proof context.

753 \item @{method assumption} solves some goal by a single assumption

754 step. All given facts are guaranteed to participate in the

755 refinement; this means there may be only 0 or 1 in the first place.

756 Recall that @{command "qed"} (\secref{sec:proof-steps}) already

757 concludes any remaining sub-goals by assumption, so structured

758 proofs usually need not quote the @{method assumption} method at

759 all.

761 \item @{method this} applies all of the current facts directly as

762 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command

763 "by"}~@{text this}''.

765 \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as

766 argument in backward manner; facts are used to reduce the rule

767 before applying it to the goal. Thus @{method (Pure) rule} without facts

768 is plain introduction, while with facts it becomes elimination.

770 When no arguments are given, the @{method (Pure) rule} method tries to pick

771 appropriate rules automatically, as declared in the current context

772 using the @{attribute (Pure) intro}, @{attribute (Pure) elim},

773 @{attribute (Pure) dest} attributes (see below). This is the

774 default behavior of @{command "proof"} and ``@{command ".."}''

775 (double-dot) steps (see \secref{sec:proof-steps}).

777 \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and

778 @{attribute (Pure) dest} declare introduction, elimination, and

779 destruct rules, to be used with method @{method (Pure) rule}, and similar

780 tools. Note that the latter will ignore rules declared with

781 ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.

783 The classical reasoner (see \secref{sec:classical}) introduces its

784 own variants of these attributes; use qualified names to access the

785 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)

786 "Pure.intro"}.

788 \item @{attribute (Pure) rule}~@{text del} undeclares introduction,

789 elimination, or destruct rules.

791 \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some

792 theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}

793 (in parallel). This corresponds to the @{ML "op MRS"} operation in

794 ML, but note the reversed order. Positions may be effectively

795 skipped by including ``@{text _}'' (underscore) as argument.

797 \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional

798 instantiation of term variables. The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are

799 substituted for any schematic variables occurring in a theorem from

800 left to right; ``@{text _}'' (underscore) indicates to skip a

801 position. Arguments following a ``@{text "concl:"}'' specification

802 refer to positions of the conclusion of a rule.

804 \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}

805 performs named instantiation of schematic type and term variables

806 occurring in a theorem. Schematic variables have to be specified on

807 the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may

808 be omitted if the variable name is a plain identifier without index.

809 As type instantiations are inferred from term instantiations,

810 explicit type instantiations are seldom necessary.

812 \end{description}

813 *}

816 subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}

818 text {*

819 The Isar provides separate commands to accommodate tactic-style

820 proof scripts within the same system. While being outside the

821 orthodox Isar proof language, these might come in handy for

822 interactive exploration and debugging, or even actual tactical proof

823 within new-style theories (to benefit from document preparation, for

824 example). See also \secref{sec:tactics} for actual tactics, that

825 have been encapsulated as proof methods. Proper proof methods may

826 be used in scripts, too.

828 \begin{matharray}{rcl}

829 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

830 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

831 @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

832 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

833 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

834 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\

835 \end{matharray}

837 @{rail "

838 ( @@{command apply} | @@{command apply_end} ) @{syntax method}

839 ;

840 @@{command defer} @{syntax nat}?

841 ;

842 @@{command prefer} @{syntax nat}

843 "}

845 \begin{description}

847 \item @{command "apply"}~@{text m} applies proof method @{text m} in

848 initial position, but unlike @{command "proof"} it retains ``@{text

849 "proof(prove)"}'' mode. Thus consecutive method applications may be

850 given just as in tactic scripts.

852 Facts are passed to @{text m} as indicated by the goal's

853 forward-chain mode, and are \emph{consumed} afterwards. Thus any

854 further @{command "apply"} command would always work in a purely

855 backward manner.

857 \item @{command "apply_end"}~@{text "m"} applies proof method @{text

858 m} as if in terminal position. Basically, this simulates a

859 multi-step tactic script for @{command "qed"}, but may be given

860 anywhere within the proof body.

862 No facts are passed to @{text m} here. Furthermore, the static

863 context is that of the enclosing goal (as for actual @{command

864 "qed"}). Thus the proof method may not refer to any assumptions

865 introduced in the current body, for example.

867 \item @{command "done"} completes a proof script, provided that the

868 current goal state is solved completely. Note that actual

869 structured proof commands (e.g.\ ``@{command "."}'' or @{command

870 "sorry"}) may be used to conclude proof scripts as well.

872 \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}

873 shuffle the list of pending goals: @{command "defer"} puts off

874 sub-goal @{text n} to the end of the list (@{text "n = 1"} by

875 default), while @{command "prefer"} brings sub-goal @{text n} to the

876 front.

878 \item @{command "back"} does back-tracking over the result sequence

879 of the latest proof command. Basically, any proof command may

880 return multiple results.

882 \end{description}

884 Any proper Isar proof method may be used with tactic script commands

885 such as @{command "apply"}. A few additional emulations of actual

886 tactics are provided as well; these would be never used in actual

887 structured proofs, of course.

888 *}

891 subsection {* Defining proof methods *}

893 text {*

894 \begin{matharray}{rcl}

895 @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\

896 \end{matharray}

898 @{rail "

899 @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?

900 ;

901 "}

903 \begin{description}

905 \item @{command "method_setup"}~@{text "name = text description"}

906 defines a proof method in the current theory. The given @{text

907 "text"} has to be an ML expression of type

908 @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\

909 basic parsers defined in structure @{ML_struct Args} and @{ML_struct

910 Attrib}. There are also combinators like @{ML METHOD} and @{ML

911 SIMPLE_METHOD} to turn certain tactic forms into official proof

912 methods; the primed versions refer to tactics with explicit goal

913 addressing.

915 Here are some example method definitions:

917 \end{description}

918 *}

920 method_setup my_method1 = {*

921 Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))

922 *} "my first method (without any arguments)"

924 method_setup my_method2 = {*

925 Scan.succeed (fn ctxt: Proof.context =>

926 SIMPLE_METHOD' (fn i: int => no_tac))

927 *} "my second method (with context)"

929 method_setup my_method3 = {*

930 Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>

931 SIMPLE_METHOD' (fn i: int => no_tac))

932 *} "my third method (with theorem arguments and context)"

935 section {* Generalized elimination \label{sec:obtain} *}

937 text {*

938 \begin{matharray}{rcl}

939 @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

940 @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\

941 \end{matharray}

943 Generalized elimination means that additional elements with certain

944 properties may be introduced in the current context, by virtue of a

945 locally proven ``soundness statement''. Technically speaking, the

946 @{command "obtain"} language element is like a declaration of

947 @{command "fix"} and @{command "assume"} (see also see

948 \secref{sec:proof-context}), together with a soundness proof of its

949 additional claim. According to the nature of existential reasoning,

950 assumptions get eliminated from any result exported from the context

951 later, provided that the corresponding parameters do \emph{not}

952 occur in the conclusion.

954 @{rail "

955 @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')

956 @'where' (@{syntax props} + @'and')

957 ;

958 @@{command guess} (@{syntax vars} + @'and')

959 "}

961 The derived Isar command @{command "obtain"} is defined as follows

962 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)

963 facts indicated for forward chaining).

964 \begin{matharray}{l}

965 @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex]

966 \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\

967 \quad @{command "proof"}~@{method succeed} \\

968 \qquad @{command "fix"}~@{text thesis} \\

969 \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\

970 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\

971 \quad\qquad @{command "apply"}~@{text -} \\

972 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\

973 \quad @{command "qed"} \\

974 \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\

975 \end{matharray}

977 Typically, the soundness proof is relatively straight-forward, often

978 just by canonical automated tools such as ``@{command "by"}~@{text

979 simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the

980 ``@{text that}'' reduction above is declared as simplification and

981 introduction rule.

983 In a sense, @{command "obtain"} represents at the level of Isar

984 proofs what would be meta-logical existential quantifiers and

985 conjunctions. This concept has a broad range of useful

986 applications, ranging from plain elimination (or introduction) of

987 object-level existential and conjunctions, to elimination over

988 results of symbolic evaluation of recursive definitions, for

989 example. Also note that @{command "obtain"} without parameters acts

990 much like @{command "have"}, where the result is treated as a

991 genuine assumption.

993 An alternative name to be used instead of ``@{text that}'' above may

994 be given in parentheses.

996 \medskip The improper variant @{command "guess"} is similar to

997 @{command "obtain"}, but derives the obtained statement from the

998 course of reasoning! The proof starts with a fixed goal @{text

999 thesis}. The subsequent proof may refine this to anything of the

1000 form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>

1001 \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The

1002 final goal state is then used as reduction rule for the obtain

1003 scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,

1004 x\<^sub>m"} are marked as internal by default, which prevents the

1005 proof context from being polluted by ad-hoc variables. The variable

1006 names and type constraints given as arguments for @{command "guess"}

1007 specify a prefix of obtained parameters explicitly in the text.

1009 It is important to note that the facts introduced by @{command

1010 "obtain"} and @{command "guess"} may not be polymorphic: any

1011 type-variables occurring here are fixed in the present context!

1012 *}

1015 section {* Calculational reasoning \label{sec:calculation} *}

1017 text {*

1018 \begin{matharray}{rcl}

1019 @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

1020 @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

1021 @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

1022 @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

1023 @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

1024 @{attribute trans} & : & @{text attribute} \\

1025 @{attribute sym} & : & @{text attribute} \\

1026 @{attribute symmetric} & : & @{text attribute} \\

1027 \end{matharray}

1029 Calculational proof is forward reasoning with implicit application

1030 of transitivity rules (such those of @{text "="}, @{text "\<le>"},

1031 @{text "<"}). Isabelle/Isar maintains an auxiliary fact register

1032 @{fact_ref calculation} for accumulating results obtained by

1033 transitivity composed with the current result. Command @{command

1034 "also"} updates @{fact calculation} involving @{fact this}, while

1035 @{command "finally"} exhibits the final @{fact calculation} by

1036 forward chaining towards the next goal statement. Both commands

1037 require valid current facts, i.e.\ may occur only after commands

1038 that produce theorems such as @{command "assume"}, @{command

1039 "note"}, or some finished proof of @{command "have"}, @{command

1040 "show"} etc. The @{command "moreover"} and @{command "ultimately"}

1041 commands are similar to @{command "also"} and @{command "finally"},

1042 but only collect further results in @{fact calculation} without

1043 applying any rules yet.

1045 Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has

1046 its canonical application with calculational proofs. It refers to

1047 the argument of the preceding statement. (The argument of a curried

1048 infix expression happens to be its right-hand side.)

1050 Isabelle/Isar calculations are implicitly subject to block structure

1051 in the sense that new threads of calculational reasoning are

1052 commenced for any new block (as opened by a local goal, for

1053 example). This means that, apart from being able to nest

1054 calculations, there is no separate \emph{begin-calculation} command

1055 required.

1057 \medskip The Isar calculation proof commands may be defined as

1058 follows:\footnote{We suppress internal bookkeeping such as proper

1059 handling of block-structure.}

1061 \begin{matharray}{rcl}

1062 @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\

1063 @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]

1064 @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]

1065 @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\

1066 @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\

1067 \end{matharray}

1069 @{rail "

1070 (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?

1071 ;

1072 @@{attribute trans} (() | 'add' | 'del')

1073 "}

1075 \begin{description}

1077 \item @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary

1078 @{fact calculation} register as follows. The first occurrence of

1079 @{command "also"} in some calculational thread initializes @{fact

1080 calculation} by @{fact this}. Any subsequent @{command "also"} on

1081 the same level of block-structure updates @{fact calculation} by

1082 some transitivity rule applied to @{fact calculation} and @{fact

1083 this} (in that order). Transitivity rules are picked from the

1084 current context, unless alternative rules are given as explicit

1085 arguments.

1087 \item @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact

1088 calculation} in the same way as @{command "also"}, and concludes the

1089 current calculational thread. The final result is exhibited as fact

1090 for forward chaining towards the next goal. Basically, @{command

1091 "finally"} just abbreviates @{command "also"}~@{command

1092 "from"}~@{fact calculation}. Typical idioms for concluding

1093 calculational proofs are ``@{command "finally"}~@{command

1094 "show"}~@{text ?thesis}~@{command "."}'' and ``@{command

1095 "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.

1097 \item @{command "moreover"} and @{command "ultimately"} are

1098 analogous to @{command "also"} and @{command "finally"}, but collect

1099 results only, without applying rules.

1101 \item @{command "print_trans_rules"} prints the list of transitivity

1102 rules (for calculational commands @{command "also"} and @{command

1103 "finally"}) and symmetry rules (for the @{attribute symmetric}

1104 operation and single step elimination patters) of the current

1105 context.

1107 \item @{attribute trans} declares theorems as transitivity rules.

1109 \item @{attribute sym} declares symmetry rules, as well as

1110 @{attribute "Pure.elim"}@{text "?"} rules.

1112 \item @{attribute symmetric} resolves a theorem with some rule

1113 declared as @{attribute sym} in the current context. For example,

1114 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a

1115 swapped fact derived from that assumption.

1117 In structured proof texts it is often more appropriate to use an

1118 explicit single-step elimination proof, such as ``@{command

1119 "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text

1120 "y = x"}~@{command ".."}''.

1122 \end{description}

1123 *}

1126 section {* Proof by cases and induction \label{sec:cases-induct} *}

1128 subsection {* Rule contexts *}

1130 text {*

1131 \begin{matharray}{rcl}

1132 @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

1133 @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

1134 @{attribute_def case_names} & : & @{text attribute} \\

1135 @{attribute_def case_conclusion} & : & @{text attribute} \\

1136 @{attribute_def params} & : & @{text attribute} \\

1137 @{attribute_def consumes} & : & @{text attribute} \\

1138 \end{matharray}

1140 The puristic way to build up Isar proof contexts is by explicit

1141 language elements like @{command "fix"}, @{command "assume"},

1142 @{command "let"} (see \secref{sec:proof-context}). This is adequate

1143 for plain natural deduction, but easily becomes unwieldy in concrete

1144 verification tasks, which typically involve big induction rules with

1145 several cases.

1147 The @{command "case"} command provides a shorthand to refer to a

1148 local context symbolically: certain proof methods provide an

1149 environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,

1150 x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command

1151 "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text

1152 "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>

1153 \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably

1154 @{variable ?case} for the main conclusion.

1156 By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of

1157 a case value is marked as hidden, i.e.\ there is no way to refer to

1158 such parameters in the subsequent proof text. After all, original

1159 rule parameters stem from somewhere outside of the current proof

1160 text. By using the explicit form ``@{command "case"}~@{text "(c

1161 y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to

1162 chose local names that fit nicely into the current context.

1164 \medskip It is important to note that proper use of @{command

1165 "case"} does not provide means to peek at the current goal state,

1166 which is not directly observable in Isar! Nonetheless, goal

1167 refinement commands do provide named cases @{text "goal\<^sub>i"}

1168 for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.

1169 Using this extra feature requires great care, because some bits of

1170 the internal tactical machinery intrude the proof text. In

1171 particular, parameter names stemming from the left-over of automated

1172 reasoning tools are usually quite unpredictable.

1174 Under normal circumstances, the text of cases emerge from standard

1175 elimination or induction rules, which in turn are derived from

1176 previous theory specifications in a canonical way (say from

1177 @{command "inductive"} definitions).

1179 \medskip Proper cases are only available if both the proof method

1180 and the rules involved support this. By using appropriate

1181 attributes, case names, conclusions, and parameters may be also

1182 declared by hand. Thus variant versions of rules that have been

1183 derived manually become ready to use in advanced case analysis

1184 later.

1186 @{rail "

1187 @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')')

1188 ;

1189 caseref: nameref attributes?

1190 ;

1192 @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)

1193 ;

1194 @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )

1195 ;

1196 @@{attribute params} ((@{syntax name} * ) + @'and')

1197 ;

1198 @@{attribute consumes} @{syntax nat}?

1199 "}

1201 \begin{description}

1203 \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local

1204 context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an

1205 appropriate proof method (such as @{method_ref cases} and

1206 @{method_ref induct}). The command ``@{command "case"}~@{text "(c

1207 x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>

1208 x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.

1210 \item @{command "print_cases"} prints all local contexts of the

1211 current state, using Isar proof language notation.

1213 \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for

1214 the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}

1215 refers to the \emph{prefix} of the list of premises. Each of the

1216 cases @{text "c\<^isub>i"} can be of the form @{text "c[h\<^isub>1 \<dots> h\<^isub>n]"} where

1217 the @{text "h\<^isub>1 \<dots> h\<^isub>n"} are the names of the hypotheses in case @{text "c\<^isub>i"}

1218 from left to right.

1220 \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares

1221 names for the conclusions of a named premise @{text c}; here @{text

1222 "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula

1223 built by nesting a binary connective (e.g.\ @{text "\<or>"}).

1225 Note that proof methods such as @{method induct} and @{method

1226 coinduct} already provide a default name for the conclusion as a

1227 whole. The need to name subformulas only arises with cases that

1228 split into several sub-cases, as in common co-induction rules.

1230 \item @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames

1231 the innermost parameters of premises @{text "1, \<dots>, n"} of some

1232 theorem. An empty list of names may be given to skip positions,

1233 leaving the present parameters unchanged.

1235 Note that the default usage of case rules does \emph{not} directly

1236 expose parameters to the proof context.

1238 \item @{attribute consumes}~@{text n} declares the number of ``major

1239 premises'' of a rule, i.e.\ the number of facts to be consumed when

1240 it is applied by an appropriate proof method. The default value of

1241 @{attribute consumes} is @{text "n = 1"}, which is appropriate for

1242 the usual kind of cases and induction rules for inductive sets (cf.\

1243 \secref{sec:hol-inductive}). Rules without any @{attribute

1244 consumes} declaration given are treated as if @{attribute

1245 consumes}~@{text 0} had been specified.

1247 Note that explicit @{attribute consumes} declarations are only

1248 rarely needed; this is already taken care of automatically by the

1249 higher-level @{attribute cases}, @{attribute induct}, and

1250 @{attribute coinduct} declarations.

1252 \end{description}

1253 *}

1256 subsection {* Proof methods *}

1258 text {*

1259 \begin{matharray}{rcl}

1260 @{method_def cases} & : & @{text method} \\

1261 @{method_def induct} & : & @{text method} \\

1262 @{method_def induction} & : & @{text method} \\

1263 @{method_def coinduct} & : & @{text method} \\

1264 \end{matharray}

1266 The @{method cases}, @{method induct}, @{method induction},

1267 and @{method coinduct}

1268 methods provide a uniform interface to common proof techniques over

1269 datatypes, inductive predicates (or sets), recursive functions etc.

1270 The corresponding rules may be specified and instantiated in a

1271 casual manner. Furthermore, these methods provide named local

1272 contexts that may be invoked via the @{command "case"} proof command

1273 within the subsequent proof text. This accommodates compact proof

1274 texts even when reasoning about large specifications.

1276 The @{method induct} method also provides some additional

1277 infrastructure in order to be applicable to structure statements

1278 (either using explicit meta-level connectives, or including facts

1279 and parameters separately). This avoids cumbersome encoding of

1280 ``strengthened'' inductive statements within the object-logic.

1282 Method @{method induction} differs from @{method induct} only in

1283 the names of the facts in the local context invoked by the @{command "case"}

1284 command.

1286 @{rail "

1287 @@{method cases} ('(' 'no_simp' ')')? \\

1288 (@{syntax insts} * @'and') rule?

1289 ;

1290 (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?

1291 ;

1292 @@{method coinduct} @{syntax insts} taking rule?

1293 ;

1295 rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)

1296 ;

1297 definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}

1298 ;

1299 definsts: ( definst * )

1300 ;

1301 arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)

1302 ;

1303 taking: 'taking' ':' @{syntax insts}

1304 "}

1306 \begin{description}

1308 \item @{method cases}~@{text "insts R"} applies method @{method

1309 rule} with an appropriate case distinction theorem, instantiated to

1310 the subjects @{text insts}. Symbolic case names are bound according

1311 to the rule's local contexts.

1313 The rule is determined as follows, according to the facts and

1314 arguments passed to the @{method cases} method:

1316 \medskip

1317 \begin{tabular}{llll}

1318 facts & & arguments & rule \\\hline

1319 & @{method cases} & & classical case split \\

1320 & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\

1321 @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\

1322 @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\

1323 \end{tabular}

1324 \medskip

1326 Several instantiations may be given, referring to the \emph{suffix}

1327 of premises of the case rule; within each premise, the \emph{prefix}

1328 of variables is instantiated. In most situations, only a single

1329 term needs to be specified; this refers to the first variable of the

1330 last premise (it is usually the same for all cases). The @{text

1331 "(no_simp)"} option can be used to disable pre-simplification of

1332 cases (see the description of @{method induct} below for details).

1334 \item @{method induct}~@{text "insts R"} and

1335 @{method induction}~@{text "insts R"} are analogous to the

1336 @{method cases} method, but refer to induction rules, which are

1337 determined as follows:

1339 \medskip

1340 \begin{tabular}{llll}

1341 facts & & arguments & rule \\\hline

1342 & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\

1343 @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\

1344 @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\

1345 \end{tabular}

1346 \medskip

1348 Several instantiations may be given, each referring to some part of

1349 a mutual inductive definition or datatype --- only related partial

1350 induction rules may be used together, though. Any of the lists of

1351 terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables

1352 present in the induction rule. This enables the writer to specify

1353 only induction variables, or both predicates and variables, for

1354 example.

1356 Instantiations may be definitional: equations @{text "x \<equiv> t"}

1357 introduce local definitions, which are inserted into the claim and

1358 discharged after applying the induction rule. Equalities reappear

1359 in the inductive cases, but have been transformed according to the

1360 induction principle being involved here. In order to achieve

1361 practically useful induction hypotheses, some variables occurring in

1362 @{text t} need to be fixed (see below). Instantiations of the form

1363 @{text t}, where @{text t} is not a variable, are taken as a

1364 shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh

1365 variable. If this is not intended, @{text t} has to be enclosed in

1366 parentheses. By default, the equalities generated by definitional

1367 instantiations are pre-simplified using a specific set of rules,

1368 usually consisting of distinctness and injectivity theorems for

1369 datatypes. This pre-simplification may cause some of the parameters

1370 of an inductive case to disappear, or may even completely delete

1371 some of the inductive cases, if one of the equalities occurring in

1372 their premises can be simplified to @{text False}. The @{text

1373 "(no_simp)"} option can be used to disable pre-simplification.

1374 Additional rules to be used in pre-simplification can be declared

1375 using the @{attribute_def induct_simp} attribute.

1377 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''

1378 specification generalizes variables @{text "x\<^sub>1, \<dots>,

1379 x\<^sub>m"} of the original goal before applying induction. One can

1380 separate variables by ``@{text "and"}'' to generalize them in other

1381 goals then the first. Thus induction hypotheses may become

1382 sufficiently general to get the proof through. Together with

1383 definitional instantiations, one may effectively perform induction

1384 over expressions of a certain structure.

1386 The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''

1387 specification provides additional instantiations of a prefix of

1388 pending variables in the rule. Such schematic induction rules

1389 rarely occur in practice, though.

1391 \item @{method coinduct}~@{text "inst R"} is analogous to the

1392 @{method induct} method, but refers to coinduction rules, which are

1393 determined as follows:

1395 \medskip

1396 \begin{tabular}{llll}

1397 goal & & arguments & rule \\\hline

1398 & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\

1399 @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\

1400 @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\

1401 \end{tabular}

1403 Coinduction is the dual of induction. Induction essentially

1404 eliminates @{text "A x"} towards a generic result @{text "P x"},

1405 while coinduction introduces @{text "A x"} starting with @{text "B

1406 x"}, for a suitable ``bisimulation'' @{text B}. The cases of a

1407 coinduct rule are typically named after the predicates or sets being

1408 covered, while the conclusions consist of several alternatives being

1409 named after the individual destructor patterns.

1411 The given instantiation refers to the \emph{suffix} of variables

1412 occurring in the rule's major premise, or conclusion if unavailable.

1413 An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''

1414 specification may be required in order to specify the bisimulation

1415 to be used in the coinduction step.

1417 \end{description}

1419 Above methods produce named local contexts, as determined by the

1420 instantiated rule as given in the text. Beyond that, the @{method

1421 induct} and @{method coinduct} methods guess further instantiations

1422 from the goal specification itself. Any persisting unresolved

1423 schematic variables of the resulting rule will render the the

1424 corresponding case invalid. The term binding @{variable ?case} for

1425 the conclusion will be provided with each case, provided that term

1426 is fully specified.

1428 The @{command "print_cases"} command prints all named cases present

1429 in the current proof state.

1431 \medskip Despite the additional infrastructure, both @{method cases}

1432 and @{method coinduct} merely apply a certain rule, after

1433 instantiation, while conforming due to the usual way of monotonic

1434 natural deduction: the context of a structured statement @{text

1435 "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}

1436 reappears unchanged after the case split.

1438 The @{method induct} method is fundamentally different in this

1439 respect: the meta-level structure is passed through the

1440 ``recursive'' course involved in the induction. Thus the original

1441 statement is basically replaced by separate copies, corresponding to

1442 the induction hypotheses and conclusion; the original goal context

1443 is no longer available. Thus local assumptions, fixed parameters

1444 and definitions effectively participate in the inductive rephrasing

1445 of the original statement.

1447 In @{method induct} proofs, local assumptions introduced by cases are split

1448 into two different kinds: @{text hyps} stemming from the rule and

1449 @{text prems} from the goal statement. This is reflected in the

1450 extracted cases accordingly, so invoking ``@{command "case"}~@{text

1451 c}'' will provide separate facts @{text c.hyps} and @{text c.prems},

1452 as well as fact @{text c} to hold the all-inclusive list.

1454 In @{method induction} proofs, local assumptions introduced by cases are

1455 split into three different kinds: @{text IH}, the induction hypotheses,

1456 @{text hyps}, the remaining hypotheses stemming from the rule, and

1457 @{text prems}, the assumptions from the goal statement. The names are

1458 @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.

1461 \medskip Facts presented to either method are consumed according to

1462 the number of ``major premises'' of the rule involved, which is

1463 usually 0 for plain cases and induction rules of datatypes etc.\ and

1464 1 for rules of inductive predicates or sets and the like. The

1465 remaining facts are inserted into the goal verbatim before the

1466 actual @{text cases}, @{text induct}, or @{text coinduct} rule is

1467 applied.

1468 *}

1471 subsection {* Declaring rules *}

1473 text {*

1474 \begin{matharray}{rcl}

1475 @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

1476 @{attribute_def cases} & : & @{text attribute} \\

1477 @{attribute_def induct} & : & @{text attribute} \\

1478 @{attribute_def coinduct} & : & @{text attribute} \\

1479 \end{matharray}

1481 @{rail "

1482 @@{attribute cases} spec

1483 ;

1484 @@{attribute induct} spec

1485 ;

1486 @@{attribute coinduct} spec

1487 ;

1489 spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'

1490 "}

1492 \begin{description}

1494 \item @{command "print_induct_rules"} prints cases and induct rules

1495 for predicates (or sets) and types of the current context.

1497 \item @{attribute cases}, @{attribute induct}, and @{attribute

1498 coinduct} (as attributes) declare rules for reasoning about

1499 (co)inductive predicates (or sets) and types, using the

1500 corresponding methods of the same name. Certain definitional

1501 packages of object-logics usually declare emerging cases and

1502 induction rules as expected, so users rarely need to intervene.

1504 Rules may be deleted via the @{text "del"} specification, which

1505 covers all of the @{text "type"}/@{text "pred"}/@{text "set"}

1506 sub-categories simultaneously. For example, @{attribute

1507 cases}~@{text del} removes any @{attribute cases} rules declared for

1508 some type, predicate, or set.

1510 Manual rule declarations usually refer to the @{attribute

1511 case_names} and @{attribute params} attributes to adjust names of

1512 cases and parameters of a rule; the @{attribute consumes}

1513 declaration is taken care of automatically: @{attribute

1514 consumes}~@{text 0} is specified for ``type'' rules and @{attribute

1515 consumes}~@{text 1} for ``predicate'' / ``set'' rules.

1517 \end{description}

1518 *}

1520 end