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

src/Doc/Isar_Ref/Proof.thy

author | wenzelm |

Sun Dec 03 13:22:09 2017 +0100 (17 months ago) | |

changeset 67119 | acb0807ddb56 |

parent 64926 | 75ee8475c37e |

child 69597 | ff784d5a5bfb |

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

discontinued old 'def' command;

1 (*:maxLineLen=78:*)

3 theory Proof

4 imports Main Base

5 begin

7 chapter \<open>Proofs \label{ch:proofs}\<close>

9 text \<open>

10 Proof commands perform transitions of Isar/VM machine configurations, which

11 are block-structured, consisting of a stack of nodes with three main

12 components: logical proof context, current facts, and open goals. Isar/VM

13 transitions are typed according to the following three different modes of

14 operation:

16 \<^descr> \<open>proof(prove)\<close> means that a new goal has just been stated that is now to

17 be \<^emph>\<open>proven\<close>; the next command may refine it by some proof method, and

18 enter a sub-proof to establish the actual result.

20 \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the context may be

21 augmented by \<^emph>\<open>stating\<close> additional assumptions, intermediate results etc.

23 \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and

24 \<open>proof(prove)\<close>: existing facts (i.e.\ the contents of the special

25 @{fact_ref this} register) have been just picked up in order to be used

26 when refining the goal claimed next.

28 The proof mode indicator may be understood as an instruction to the writer,

29 telling what kind of operation may be performed next. The corresponding

30 typings of proof commands restricts the shape of well-formed proof texts to

31 particular command sequences. So dynamic arrangements of commands eventually

32 turn out as static texts of a certain structure.

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

35 emerging that way from the different types of proof commands. The main ideas

36 of the overall Isar framework are explained in \chref{ch:isar-framework}.

37 \<close>

40 section \<open>Proof structure\<close>

42 subsection \<open>Formal notepad\<close>

44 text \<open>

45 \begin{matharray}{rcl}

46 @{command_def "notepad"} & : & \<open>local_theory \<rightarrow> proof(state)\<close> \\

47 \end{matharray}

49 @{rail \<open>

50 @@{command notepad} @'begin'

51 ;

52 @@{command end}

53 \<close>}

55 \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without any

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

57 persistent result. The notepad is closed by @{command "end"}.

58 \<close>

61 subsection \<open>Blocks\<close>

63 text \<open>

64 \begin{matharray}{rcl}

65 @{command_def "next"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

66 @{command_def "{"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

67 @{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

68 \end{matharray}

70 While Isar is inherently block-structured, opening and closing blocks is

71 mostly handled rather casually, with little explicit user-intervention. Any

72 local goal statement automatically opens \<^emph>\<open>two\<close> internal blocks, which are

73 closed again when concluding the sub-proof (by @{command "qed"} etc.).

74 Sections of different context within a sub-proof may be switched via

75 @{command "next"}, which is just a single block-close followed by block-open

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

77 there is no goal focus involved here!

79 For slightly more advanced applications, there are explicit block

80 parentheses as well. These typically achieve a stronger forward style of

81 reasoning.

83 \<^descr> @{command "next"} switches to a fresh block within a sub-proof, resetting

84 the local context to the initial one.

86 \<^descr> @{command "{"} and @{command "}"} explicitly open and close blocks. Any

87 current facts pass through ``@{command "{"}'' unchanged, while ``@{command

88 "}"}'' causes any result to be \<^emph>\<open>exported\<close> into the enclosing context. Thus

89 fixed variables are generalized, assumptions discharged, and local

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

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

92 forward reasoning --- in contrast to plain backward reasoning with the

93 result exported at @{command "show"} time.

94 \<close>

97 subsection \<open>Omitting proofs\<close>

99 text \<open>

100 \begin{matharray}{rcl}

101 @{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\

102 \end{matharray}

104 The @{command "oops"} command discontinues the current proof attempt, while

105 considering the partial proof text as properly processed. This is

106 conceptually quite different from ``faking'' actual proofs via @{command_ref

107 "sorry"} (see \secref{sec:proof-steps}): @{command "oops"} does not observe

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

109 Furthermore, @{command "oops"} does not produce any result theorem --- there

110 is no intended claim to be able to complete the proof in any way.

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

113 \<^emph>\<open>within\<close> the system itself, in conjunction with the document preparation

114 tools of Isabelle described in \chref{ch:document-prep}. Thus partial or

115 even wrong proof attempts can be discussed in a logically sound manner. Note

116 that the Isabelle {\LaTeX} macros can be easily adapted to print something

117 like ``\<open>\<dots>\<close>'' instead of the keyword ``@{command "oops"}''.

118 \<close>

121 section \<open>Statements\<close>

123 subsection \<open>Context elements \label{sec:proof-context}\<close>

125 text \<open>

126 \begin{matharray}{rcl}

127 @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

128 @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

129 @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

130 @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

131 \end{matharray}

133 The logical proof context consists of fixed variables and assumptions. The

134 former closely correspond to Skolem constants, or meta-level universal

135 quantification as provided by the Isabelle/Pure logical framework.

136 Introducing some \<^emph>\<open>arbitrary, but fixed\<close> variable via ``@{command

137 "fix"}~\<open>x\<close>'' results in a local value that may be used in the subsequent

138 proof as any other variable or constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close>

139 exported from the context will be universally closed wrt.\ \<open>x\<close> at the

140 outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal form using

141 Isabelle's meta-variables).

143 Similarly, introducing some assumption \<open>\<chi>\<close> has two effects. On the one hand,

144 a local theorem is created that may be used as a fact in subsequent proof

145 steps. On the other hand, any result \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context

146 becomes conditional wrt.\ the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an

147 enclosing goal using such a result would basically introduce a new subgoal

148 stemming from the assumption. How this situation is handled depends on the

149 version of assumption command used: while @{command "assume"} insists on

150 solving the subgoal by unification with some premise of the goal, @{command

151 "presume"} leaves the subgoal unchanged in order to be proved later by the

152 user.

154 Local definitions, introduced by ``\<^theory_text>\<open>define x where x = t\<close>'', are achieved

155 by combining ``@{command "fix"}~\<open>x\<close>'' with another version of assumption

156 that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the

157 reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>

158 \<phi>[t]\<close>.

160 @{rail \<open>

161 @@{command fix} @{syntax vars}

162 ;

163 (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}

164 ;

165 concl: (@{syntax props} + @'and')

166 ;

167 prems: (@'if' (@{syntax props'} + @'and'))?

168 ;

169 @@{command define} @{syntax vars} @'where'

170 (@{syntax props} + @'and') @{syntax for_fixes}

171 \<close>}

173 \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,

174 but fixed\<close>.

176 \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command "presume"}~\<open>a: \<phi>\<close> introduce a

177 local fact \<open>\<phi> \<turnstile> \<phi>\<close> by assumption. Subsequent results applied to an enclosing

178 goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command

179 "assume"} expects to be able to unify with existing premises in the goal,

180 while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.

182 Several lists of assumptions may be given (separated by @{keyword_ref

183 "and"}; the resulting list of current facts consists of all of these

184 concatenated.

186 A structured assumption like \<^theory_text>\<open>assume "B x" if "A x" for x\<close> is equivalent to

187 \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a

188 for-context only effects propositions according to actual use of variables.

190 \<^descr> \<^theory_text>\<open>define x where "x = t"\<close> introduces a local (non-polymorphic) definition.

191 In results that are exported from the context, \<open>x\<close> is replaced by \<open>t\<close>.

193 Internally, equational assumptions are added to the context in Pure form,

194 using \<open>x \<equiv> t\<close> instead of \<open>x = t\<close> or \<open>x \<longleftrightarrow> t\<close> from the object-logic. When

195 exporting results from the context, \<open>x\<close> is generalized and the assumption

196 discharged by reflexivity, causing the replacement by \<open>t\<close>.

198 The default name for the definitional fact is \<open>x_def\<close>. Several simultaneous

199 definitions may be given as well, with a collective default name.

201 \<^medskip>

202 It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f

203 :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.

204 \<close>

207 subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close>

209 text \<open>

210 \begin{matharray}{rcl}

211 @{command_def "let"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

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

213 \end{matharray}

215 Abbreviations may be either bound by explicit @{command "let"}~\<open>p \<equiv> t\<close>

216 statements, or by annotating assumptions or goal statements with a list of

217 patterns ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is

218 invoked to bind extra-logical term variables, which may be either named

219 schematic variables of the form \<open>?x\<close>, or nameless dummies ``@{variable _}''

220 (underscore). Note that in the @{command "let"} form the patterns occur on

221 the left-hand side, while the @{keyword "is"} patterns are in postfix

222 position.

224 Polymorphism of term bindings is handled in Hindley-Milner style, similar to

225 ML. Type variables referring to local assumptions or open goal statements

226 are \<^emph>\<open>fixed\<close>, while those of finished results or bound by @{command "let"}

227 may occur in \<^emph>\<open>arbitrary\<close> instances later. Even though actual polymorphism

228 should be rarely used in practice, this mechanism is essential to achieve

229 proper incremental type-inference, as the user proceeds to build up the Isar

230 proof text from left to right.

232 \<^medskip>

233 Term abbreviations are quite different from local definitions as introduced

234 via @{command "define"} (see \secref{sec:proof-context}). The latter are

235 visible within the logic as actual equations, while abbreviations disappear

236 during the input process just after type checking. Also note that @{command

237 "define"} does not support polymorphism.

239 @{rail \<open>

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

241 \<close>}

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

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

246 \<^descr> \<^theory_text>\<open>let p\<^sub>1 = t\<^sub>1 and \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables in patterns

247 \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against terms \<open>t\<^sub>1, \<dots>,

248 t\<^sub>n\<close>.

250 \<^descr> \<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close>

251 against the preceding statement. Also note that @{keyword "is"} is not a

252 separate command, but part of others (such as @{command "assume"},

253 @{command "have"} etc.).

255 Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} for goals and

256 facts are available as well. For any open goal, @{variable_ref thesis}

257 refers to its object-level statement, abstracted over any meta-level

258 parameters (if present). Likewise, @{variable_ref this} is bound for fact

259 statements resulting from assumptions or finished goals. In case @{variable

260 this} refers to an object-logic statement that is an application \<open>f t\<close>, then

261 \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}'' (three dots).

262 The canonical application of this convenience are calculational proofs (see

263 \secref{sec:calculation}).

264 \<close>

267 subsection \<open>Facts and forward chaining \label{sec:proof-facts}\<close>

269 text \<open>

270 \begin{matharray}{rcl}

271 @{command_def "note"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

272 @{command_def "then"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

273 @{command_def "from"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

274 @{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

275 @{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

276 @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

277 @{method_def "use"} & : & \<open>method\<close> \\

278 @{fact_def "method_facts"} & : & \<open>fact\<close> \\

279 \end{matharray}

281 New facts are established either by assumption or proof of local statements.

282 Any fact will usually be involved in further proofs, either as explicit

283 arguments of proof methods, or when forward chaining towards the next goal

284 via @{command "then"} (and variants); @{command "from"} and @{command

285 "with"} are composite forms involving @{command "note"}. The @{command

286 "using"} elements augments the collection of used facts \<^emph>\<open>after\<close> a goal has

287 been stated. Note that the special theorem name @{fact_ref this} refers to

288 the most recently established facts, but only \<^emph>\<open>before\<close> issuing a follow-up

289 claim.

291 @{rail \<open>

292 @@{command note} (@{syntax thmdef}? @{syntax thms} + @'and')

293 ;

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

295 (@{syntax thms} + @'and')

296 ;

297 @{method use} @{syntax thms} @'in' @{syntax method}

298 \<close>}

300 \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,

301 binding the result as \<open>a\<close>. Note that attributes may be involved as well,

302 both on the left and right hand sides.

304 \<^descr> @{command "then"} indicates forward chaining by the current facts in order

305 to establish the goal to be claimed next. The initial proof method invoked

306 to refine that will be offered the facts to do ``anything appropriate'' (see

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

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

309 than an introduction. Automatic methods usually insert the facts into the

310 goal state before operation. This provides a simple scheme to control

311 relevance of facts in automated proof search.

313 \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command "note"}~\<open>b\<close>~@{command

314 "then"}''; thus @{command "then"} is equivalent to ``@{command

315 "from"}~\<open>this\<close>''.

317 \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n

318 \<AND> this\<close>''; thus the forward chaining is from earlier facts together

319 with the current ones.

321 \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts to be used by a

322 subsequent refinement step (such as @{command_ref "apply"} or @{command_ref

323 "proof"}).

325 \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command

326 "using"}, but unfolds definitional equations \<open>b\<^sub>1 \<dots> b\<^sub>n\<close> throughout the goal

327 state and facts. See also the proof method @{method_ref unfold}.

329 \<^descr> \<^theory_text>\<open>(use b\<^sub>1 \<dots> b\<^sub>n in method)\<close> uses the facts in the given method

330 expression. The facts provided by the proof state (via @{command "using"}

331 etc.) are ignored, but it is possible to refer to @{fact method_facts}

332 explicitly.

334 \<^descr> @{fact method_facts} is a dynamic fact that refers to the currently used

335 facts of the goal state.

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

339 at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no effect apart from

340 entering \<open>prove(chain)\<close> mode, since @{fact_ref nothing} is bound to the

341 empty list of theorems.

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

344 facts to be given in their proper order, corresponding to a prefix of the

345 premises of the rule involved. Note that positions may be easily skipped

346 using something like @{command "from"}~\<open>_ \<AND> a \<AND> b\<close>, for example.

347 This involves the trivial rule \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in

348 Isabelle/Pure as ``@{fact_ref "_"}'' (underscore).

350 Automated methods (such as @{method simp} or @{method auto}) just insert any

351 given facts before their usual operation. Depending on the kind of procedure

352 involved, the order of facts is less significant here.

353 \<close>

356 subsection \<open>Goals \label{sec:goals}\<close>

358 text \<open>

359 \begin{matharray}{rcl}

360 @{command_def "lemma"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

361 @{command_def "theorem"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

362 @{command_def "corollary"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

363 @{command_def "proposition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

364 @{command_def "schematic_goal"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

365 @{command_def "have"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

366 @{command_def "show"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

367 @{command_def "hence"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\

368 @{command_def "thus"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\

369 @{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

370 \end{matharray}

372 From a theory context, proof mode is entered by an initial goal command such

373 as @{command "lemma"}. Within a proof context, new claims may be introduced

374 locally; there are variants to interact with the overall proof structure

375 specifically, such as @{command have} or @{command show}.

377 Goals may consist of multiple statements, resulting in a list of facts

378 eventually. A pending multi-goal is internally represented as a meta-level

379 conjunction (\<open>&&&\<close>), which is usually split into the corresponding number of

380 sub-goals prior to an initial method application, via @{command_ref "proof"}

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

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

383 \secref{sec:cases-induct} acts on multiple claims simultaneously.

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

386 merely consists of several simultaneous propositions (often just one). A

387 long goal includes an explicit context specification for the subsequent

388 conclusion, involving local parameters and assumptions. Here the role of

389 each part of the statement is explicitly marked by separate keywords (see

390 also \secref{sec:locale}); the local assumptions being introduced here are

391 available as @{fact_ref assms} in the proof. Moreover, there are two kinds

392 of conclusions: @{element_def "shows"} states several simultaneous

393 propositions (essentially a big conjunction), while @{element_def "obtains"}

394 claims several simultaneous simultaneous contexts of (essentially a big

395 disjunction of eliminated parameters and assumptions, cf.\

396 \secref{sec:obtain}).

398 @{rail \<open>

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

400 @@{command proposition} | @@{command schematic_goal})

401 (long_statement | short_statement)

402 ;

403 (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})

404 stmt cond_stmt @{syntax for_fixes}

405 ;

406 @@{command print_statement} @{syntax modes}? @{syntax thms}

407 ;

409 stmt: (@{syntax props} + @'and')

410 ;

411 cond_stmt: ((@'if' | @'when') stmt)?

412 ;

413 short_statement: stmt (@'if' stmt)? @{syntax for_fixes}

414 ;

415 long_statement: @{syntax thmdecl}? context conclusion

416 ;

417 context: (@{syntax_ref "includes"}?) (@{syntax context_elem} *)

418 ;

419 conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}

420 ;

421 @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')

422 ;

423 @{syntax_def obtain_case}: @{syntax vars} @'where'

424 (@{syntax thmdecl}? (@{syntax prop}+) + @'and')

425 \<close>}

427 \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,

428 eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target

429 context.

431 A @{syntax long_statement} may build up an initial proof context for the

432 subsequent claim, potentially including local definitions and syntax; see

433 also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem}

434 in \secref{sec:locale}.

436 A @{syntax short_statement} consists of propositions as conclusion, with an

437 option context of premises and parameters, via \<^verbatim>\<open>if\<close>/\<^verbatim>\<open>for\<close> in postfix

438 notation, corresponding to \<^verbatim>\<open>assumes\<close>/\<^verbatim>\<open>fixes\<close> in the long prefix notation.

440 Local premises (if present) are called ``\<open>assms\<close>'' for @{syntax

441 long_statement}, and ``\<open>that\<close>'' for @{syntax short_statement}.

443 \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}

444 are the same as @{command "lemma"}. The different command names merely serve

445 as a formal comment in the theory source.

447 \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"}, but allows

448 the statement to contain unbound schematic variables.

450 Under normal circumstances, an Isar proof text needs to specify claims

451 explicitly. Schematic goals are more like goals in Prolog, where certain

452 results are synthesized in the course of reasoning. With schematic

453 statements, the inherent compositionality of Isar proofs is lost, which also

454 impacts performance, because proof checking is forced into sequential mode.

456 \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal, eventually resulting in a

457 fact within the current logical context. This operation is completely

458 independent of any pending sub-goals of an enclosing goal statements, so

459 @{command "have"} may be freely used for experimental exploration of

460 potential results within a proof body.

462 \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command "have"}~\<open>a: \<phi>\<close> plus a second

463 stage to refine some pending sub-goal for each one of the finished result,

464 after having been exported into the corresponding context (at the head of

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

467 To accommodate interactive debugging, resulting rules are printed before

468 being applied internally. Even more, interactive execution of @{command

469 "show"} predicts potential failure and displays the resulting error as a

470 warning beforehand. Watch out for the following message:

471 @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}

473 \<^descr> @{command "hence"} expands to ``@{command "then"}~@{command "have"}'' and

474 @{command "thus"} expands to ``@{command "then"}~@{command "show"}''. These

475 conflations are left-over from early history of Isar. The expanded syntax is

476 more orthogonal and improves readability and maintainability of proofs.

478 \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the current theory or

479 proof context in long statement form, according to the syntax for @{command

480 "lemma"} given above.

483 Any goal statement causes some term abbreviations (such as @{variable_ref

484 "?thesis"}) to be bound automatically, see also \secref{sec:term-abbrev}.

486 Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref

487 "when"} define the special fact @{fact_ref that} to refer to these

488 assumptions in the proof body. The user may provide separate names according

489 to the syntax of the statement.

490 \<close>

493 section \<open>Calculational reasoning \label{sec:calculation}\<close>

495 text \<open>

496 \begin{matharray}{rcl}

497 @{command_def "also"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

498 @{command_def "finally"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

499 @{command_def "moreover"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

500 @{command_def "ultimately"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\

501 @{command_def "print_trans_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

502 @{attribute trans} & : & \<open>attribute\<close> \\

503 @{attribute sym} & : & \<open>attribute\<close> \\

504 @{attribute symmetric} & : & \<open>attribute\<close> \\

505 \end{matharray}

507 Calculational proof is forward reasoning with implicit application of

508 transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>, \<open><\<close>). Isabelle/Isar maintains an

509 auxiliary fact register @{fact_ref calculation} for accumulating results

510 obtained by transitivity composed with the current result. Command @{command

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

512 "finally"} exhibits the final @{fact calculation} by forward chaining

513 towards the next goal statement. Both commands require valid current facts,

514 i.e.\ may occur only after commands that produce theorems such as @{command

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

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

517 commands are similar to @{command "also"} and @{command "finally"}, but only

518 collect further results in @{fact calculation} without applying any rules

519 yet.

521 Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has its canonical

522 application with calculational proofs. It refers to the argument of the

523 preceding statement. (The argument of a curried infix expression happens to

524 be its right-hand side.)

526 Isabelle/Isar calculations are implicitly subject to block structure in the

527 sense that new threads of calculational reasoning are commenced for any new

528 block (as opened by a local goal, for example). This means that, apart from

529 being able to nest calculations, there is no separate \<^emph>\<open>begin-calculation\<close>

530 command required.

532 \<^medskip>

533 The Isar calculation proof commands may be defined as follows:\<^footnote>\<open>We suppress

534 internal bookkeeping such as proper handling of block-structure.\<close>

536 \begin{matharray}{rcl}

537 @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\

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

539 @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]

540 @{command "moreover"} & \equiv & @{command "note"}~\<open>calculation = calculation this\<close> \\

541 @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\

542 \end{matharray}

544 @{rail \<open>

545 (@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?

546 ;

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

548 \<close>}

550 \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary @{fact

551 calculation} register as follows. The first occurrence of @{command "also"}

552 in some calculational thread initializes @{fact calculation} by @{fact

553 this}. Any subsequent @{command "also"} on the same level of block-structure

554 updates @{fact calculation} by some transitivity rule applied to @{fact

555 calculation} and @{fact this} (in that order). Transitivity rules are picked

556 from the current context, unless alternative rules are given as explicit

557 arguments.

559 \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains @{fact calculation} in the

560 same way as @{command "also"} and then concludes the current calculational

561 thread. The final result is exhibited as fact for forward chaining towards

562 the next goal. Basically, @{command "finally"} abbreviates @{command

563 "also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding

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

565 "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command "finally"}~@{command

566 "have"}~\<open>\<phi>\<close>~@{command "."}''.

568 \<^descr> @{command "moreover"} and @{command "ultimately"} are analogous to

569 @{command "also"} and @{command "finally"}, but collect results only,

570 without applying rules.

572 \<^descr> @{command "print_trans_rules"} prints the list of transitivity rules (for

573 calculational commands @{command "also"} and @{command "finally"}) and

574 symmetry rules (for the @{attribute symmetric} operation and single step

575 elimination patters) of the current context.

577 \<^descr> @{attribute trans} declares theorems as transitivity rules.

579 \<^descr> @{attribute sym} declares symmetry rules, as well as @{attribute

580 "Pure.elim"}\<open>?\<close> rules.

582 \<^descr> @{attribute symmetric} resolves a theorem with some rule declared as

583 @{attribute sym} in the current context. For example, ``@{command

584 "assume"}~\<open>[symmetric]: x = y\<close>'' produces a swapped fact derived from that

585 assumption.

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

588 single-step elimination proof, such as ``@{command "assume"}~\<open>x =

589 y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.

590 \<close>

593 section \<open>Refinement steps\<close>

595 subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>

597 text \<open>

598 Proof methods are either basic ones, or expressions composed of methods via

599 ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural composition),

600 ``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least

601 once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,

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

603 name}~@{syntax args} specifications. Note that parentheses may be dropped

604 for single method specifications (with no arguments). The syntactic

605 precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low

606 to high).

608 @{rail \<open>

609 @{syntax_def method}:

610 (@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')

611 ;

612 methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')

613 \<close>}

615 Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer

616 to the first subgoal or to all subgoals uniformly. Nonetheless, the

617 subsequent mechanisms allow to imitate the effect of subgoal addressing that

618 is known from ML tactics.

620 \<^medskip>

621 Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a way that

622 certain subgoals are exposed, and other subgoals are ``parked'' elsewhere.

623 Thus a proof method has no other chance than to operate on the subgoals that

624 are presently exposed.

626 Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is

627 applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied

628 consecutively with restriction to each subgoal that has newly emerged due to

629 \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator @{ML_op THEN_ALL_NEW} in

630 Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule

631 r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.

633 Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the

634 first \<open>n\<close> subgoals (which need to exist), with default \<open>n = 1\<close>. For example,

635 the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals,

636 while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from

637 applying rule \<open>r\<close> to the originally first one.

639 \<^medskip>

640 Improper methods, notably tactic emulations, offer low-level goal addressing

641 as explicit argument to the individual tactic being involved. Here ``\<open>[!]\<close>''

642 refers to all goals, and ``\<open>[n-]\<close>'' to all goals starting from \<open>n\<close>.

644 @{rail \<open>

645 @{syntax_def goal_spec}:

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

647 \<close>}

648 \<close>

651 subsection \<open>Initial and terminal proof steps \label{sec:proof-steps}\<close>

653 text \<open>

654 \begin{matharray}{rcl}

655 @{command_def "proof"} & : & \<open>proof(prove) \<rightarrow> proof(state)\<close> \\

656 @{command_def "qed"} & : & \<open>proof(state) \<rightarrow> proof(state) | local_theory | theory\<close> \\

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

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

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

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

661 @{method_def standard} & : & \<open>method\<close> \\

662 \end{matharray}

664 Arbitrary goal refinement via tactics is considered harmful. Structured

665 proof composition in Isar admits proof methods to be invoked in two places

666 only.

668 \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref "proof"}~\<open>m\<^sub>1\<close> reduces a

669 newly stated goal to a number of sub-goals that are to be solved later.

670 Facts are passed to \<open>m\<^sub>1\<close> for forward chaining, if so indicated by

671 \<open>proof(chain)\<close> mode.

673 \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to

674 solve remaining goals. No facts are passed to \<open>m\<^sub>2\<close>.

676 The only other (proper) way to affect pending goals in a proof body is by

677 @{command_ref "show"}, which involves an explicit statement of what is to be

678 solved eventually. Thus we avoid the fundamental problem of unstructured

679 tactic scripts that consist of numerous consecutive goal transformations,

680 with invisible effects.

682 \<^medskip>

683 As a general rule of thumb for good proof style, initial proof methods

684 should either solve the goal completely, or constitute some well-understood

685 reduction to new sub-goals. Arbitrary automatic proof tools that are prone

686 leave a large number of badly structured sub-goals are no help in continuing

687 the proof document in an intelligible manner.

689 Unless given explicitly by the user, the default initial method is @{method

690 standard}, which subsumes at least @{method_ref (Pure) rule} or its

691 classical variant @{method_ref (HOL) rule}. These methods apply a single

692 standard elimination or introduction rule according to the topmost logical

693 connective involved. There is no separate default terminal method. Any

694 remaining goals are always solved by assumption in the very last step.

696 @{rail \<open>

697 @@{command proof} method?

698 ;

699 @@{command qed} method?

700 ;

701 @@{command "by"} method method?

702 ;

703 (@@{command "."} | @@{command ".."} | @@{command sorry})

704 \<close>}

706 \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof method \<open>m\<^sub>1\<close>; facts for

707 forward chaining are passed if so indicated by \<open>proof(chain)\<close> mode.

709 \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by proof method \<open>m\<^sub>2\<close>

710 and concludes the sub-proof by assumption. If the goal had been \<open>show\<close>, some

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

712 \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail for two

713 reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to any

714 pending goal\<^footnote>\<open>This includes any additional ``strong'' assumptions as

715 introduced by @{command "assume"}.\<close> of the enclosing context. Debugging such

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

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

718 of @{command "assume"} by @{command "presume"}.

720 \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal proof\<close>\index{proof!terminal}; it

721 abbreviates @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with

722 backtracking across both methods. Debugging an unsuccessful @{command

723 "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its definition; in many

724 cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient

725 to see the problem.

727 \<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard proof\<close>\index{proof!standard}; it

728 abbreviates @{command "by"}~\<open>standard\<close>.

730 \<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial proof\<close>\index{proof!trivial}; it

731 abbreviates @{command "by"}~\<open>this\<close>.

733 \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to

734 solve the pending claim without further ado. This only works in interactive

735 development, or if the @{attribute quick_and_dirty} is enabled. Facts

736 emerging from fake proofs are not the real thing. Internally, the derivation

737 object is tainted by an oracle invocation, which may be inspected via the

738 theorem status @{cite "isabelle-implementation"}.

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

741 experimentation and top-down proof development.

743 \<^descr> @{method standard} refers to the default refinement step of some Isar

744 language elements (notably @{command proof} and ``@{command ".."}''). It is

745 \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the application

746 environment.

748 In Isabelle/Pure, @{method standard} performs elementary introduction~/

749 elimination steps (@{method_ref (Pure) rule}), introduction of type classes

750 (@{method_ref intro_classes}) and locales (@{method_ref intro_locales}).

752 In Isabelle/HOL, @{method standard} also takes classical rules into account

753 (cf.\ \secref{sec:classical}).

754 \<close>

757 subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close>

759 text \<open>

760 The following proof methods and attributes refer to basic logical operations

761 of Isar. Further methods and attributes are provided by several generic and

762 object-logic specific tools and packages (see \chref{ch:gen-tools} and

763 \partref{part:hol}).

765 \begin{matharray}{rcl}

766 @{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]

767 @{method_def "-"} & : & \<open>method\<close> \\

768 @{method_def "goal_cases"} & : & \<open>method\<close> \\

769 @{method_def "fact"} & : & \<open>method\<close> \\

770 @{method_def "assumption"} & : & \<open>method\<close> \\

771 @{method_def "this"} & : & \<open>method\<close> \\

772 @{method_def (Pure) "rule"} & : & \<open>method\<close> \\

773 @{attribute_def (Pure) "intro"} & : & \<open>attribute\<close> \\

774 @{attribute_def (Pure) "elim"} & : & \<open>attribute\<close> \\

775 @{attribute_def (Pure) "dest"} & : & \<open>attribute\<close> \\

776 @{attribute_def (Pure) "rule"} & : & \<open>attribute\<close> \\[0.5ex]

777 @{attribute_def "OF"} & : & \<open>attribute\<close> \\

778 @{attribute_def "of"} & : & \<open>attribute\<close> \\

779 @{attribute_def "where"} & : & \<open>attribute\<close> \\

780 \end{matharray}

782 @{rail \<open>

783 @@{method goal_cases} (@{syntax name}*)

784 ;

785 @@{method fact} @{syntax thms}?

786 ;

787 @@{method (Pure) rule} @{syntax thms}?

788 ;

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

790 ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}

791 ;

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

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

794 ;

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

796 ;

797 @@{attribute OF} @{syntax thms}

798 ;

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

800 ;

801 @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}

802 \<close>}

804 \<^descr> @{command "print_rules"} prints rules declared via attributes @{attribute

805 (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of

806 Isabelle/Pure.

808 See also the analogous @{command "print_claset"} command for similar rule

809 declarations of the classical reasoner (\secref{sec:classical}).

811 \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as premises

812 into the goal, and nothing else.

814 Note that command @{command_ref "proof"} without any method actually

815 performs a single reduction step using the @{method_ref (Pure) rule} method;

816 thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command "proof"}~\<open>-\<close>''

817 rather than @{command "proof"} alone.

819 \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals into cases

820 within the context (see also \secref{sec:cases-induct}). The specified case

821 names are used if present; otherwise cases are numbered starting from 1.

823 Invoking cases in the subsequent proof body via the @{command_ref case}

824 command will @{command fix} goal parameters, @{command assume} goal

825 premises, and @{command let} variable @{variable_ref ?case} refer to the

826 conclusion.

828 \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or

829 implicitly from the current proof context) modulo unification of schematic

830 type and term variables. The rule structure is not taken into account, i.e.\

831 meta-level implication is considered atomic. This is the same principle

832 underlying literal facts (cf.\ \secref{sec:syn-att}): ``@{command

833 "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command

834 "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close>

835 in the proof context.

837 \<^descr> @{method assumption} solves some goal by a single assumption step. All

838 given facts are guaranteed to participate in the refinement; this means

839 there may be only 0 or 1 in the first place. Recall that @{command "qed"}

840 (\secref{sec:proof-steps}) already concludes any remaining sub-goals by

841 assumption, so structured proofs usually need not quote the @{method

842 assumption} method at all.

844 \<^descr> @{method this} applies all of the current facts directly as rules. Recall

845 that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~\<open>this\<close>''.

847 \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as argument in

848 backward manner; facts are used to reduce the rule before applying it to the

849 goal. Thus @{method (Pure) rule} without facts is plain introduction, while

850 with facts it becomes elimination.

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

853 appropriate rules automatically, as declared in the current context using

854 the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)

855 dest} attributes (see below). This is included in the standard behaviour of

856 @{command "proof"} and ``@{command ".."}'' (double-dot) steps (see

857 \secref{sec:proof-steps}).

859 \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute

860 (Pure) dest} declare introduction, elimination, and destruct rules, to be

861 used with method @{method (Pure) rule}, and similar tools. Note that the

862 latter will ignore rules declared with ``\<open>?\<close>'', while ``\<open>!\<close>'' are used most

863 aggressively.

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

866 variants of these attributes; use qualified names to access the present

867 versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}.

869 \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction, elimination, or

870 destruct rules.

872 \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all of the given rules

873 \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left order, which means that premises

874 stemming from the \<open>a\<^sub>i\<close> emerge in parallel in the result, without

875 interfering with each other. In many practical situations, the \<open>a\<^sub>i\<close> do not

876 have premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually read as

877 functional application (modulo unification).

879 Argument positions may be effectively skipped by using ``\<open>_\<close>'' (underscore),

880 which refers to the propositional identity rule in the Pure theory.

882 \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional instantiation of term

883 variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are substituted for any schematic

884 variables occurring in a theorem from left to right; ``\<open>_\<close>'' (underscore)

885 indicates to skip a position. Arguments following a ``\<open>concl:\<close>''

886 specification refer to positions of the conclusion of a rule.

888 An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified:

889 the instantiated theorem is exported, and these variables become schematic

890 (usually with some shifting of indices).

892 \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close> performs named

893 instantiation of schematic type and term variables occurring in a theorem.

894 Schematic variables have to be specified on the left-hand side (e.g.\

895 \<open>?x1.3\<close>). The question mark may be omitted if the variable name is a plain

896 identifier without index. As type instantiations are inferred from term

897 instantiations, explicit type instantiations are seldom necessary.

899 An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified

900 as for @{attribute "of"} above.

901 \<close>

904 subsection \<open>Defining proof methods\<close>

906 text \<open>

907 \begin{matharray}{rcl}

908 @{command_def "method_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

909 \end{matharray}

911 @{rail \<open>

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

913 \<close>}

915 \<^descr> @{command "method_setup"}~\<open>name = text description\<close> defines a proof method

916 in the current context. The given \<open>text\<close> has to be an ML expression of type

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

918 parsers defined in structure @{ML_structure Args} and @{ML_structure

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

920 SIMPLE_METHOD} to turn certain tactic forms into official proof methods; the

921 primed versions refer to tactics with explicit goal addressing.

923 Here are some example method definitions:

924 \<close>

926 (*<*)experiment begin(*>*)

927 method_setup my_method1 =

928 \<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close>

929 "my first method (without any arguments)"

931 method_setup my_method2 =

932 \<open>Scan.succeed (fn ctxt: Proof.context =>

933 SIMPLE_METHOD' (fn i: int => no_tac))\<close>

934 "my second method (with context)"

936 method_setup my_method3 =

937 \<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>

938 SIMPLE_METHOD' (fn i: int => no_tac))\<close>

939 "my third method (with theorem arguments and context)"

940 (*<*)end(*>*)

943 section \<open>Proof by cases and induction \label{sec:cases-induct}\<close>

945 subsection \<open>Rule contexts\<close>

947 text \<open>

948 \begin{matharray}{rcl}

949 @{command_def "case"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

950 @{command_def "print_cases"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

951 @{attribute_def case_names} & : & \<open>attribute\<close> \\

952 @{attribute_def case_conclusion} & : & \<open>attribute\<close> \\

953 @{attribute_def params} & : & \<open>attribute\<close> \\

954 @{attribute_def consumes} & : & \<open>attribute\<close> \\

955 \end{matharray}

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

958 elements like @{command "fix"}, @{command "assume"}, @{command "let"} (see

959 \secref{sec:proof-context}). This is adequate for plain natural deduction,

960 but easily becomes unwieldy in concrete verification tasks, which typically

961 involve big induction rules with several cases.

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

964 context symbolically: certain proof methods provide an environment of named

965 ``cases'' of the form \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of

966 ``@{command "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots>

967 x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Term bindings may be covered as

968 well, notably @{variable ?case} for the main conclusion.

970 By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of a case value is marked as

971 hidden, i.e.\ there is no way to refer to such parameters in the subsequent

972 proof text. After all, original rule parameters stem from somewhere outside

973 of the current proof text. By using the explicit form ``@{command

974 "case"}~\<open>(c y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to chose local

975 names that fit nicely into the current context.

977 \<^medskip>

978 It is important to note that proper use of @{command "case"} does not

979 provide means to peek at the current goal state, which is not directly

980 observable in Isar! Nonetheless, goal refinement commands do provide named

981 cases \<open>goal\<^sub>i\<close> for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.

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

983 internal tactical machinery intrude the proof text. In particular, parameter

984 names stemming from the left-over of automated reasoning tools are usually

985 quite unpredictable.

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

988 elimination or induction rules, which in turn are derived from previous

989 theory specifications in a canonical way (say from @{command "inductive"}

990 definitions).

992 \<^medskip>

993 Proper cases are only available if both the proof method and the rules

994 involved support this. By using appropriate attributes, case names,

995 conclusions, and parameters may be also declared by hand. Thus variant

996 versions of rules that have been derived manually become ready to use in

997 advanced case analysis later.

999 @{rail \<open>

1000 @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')

1001 ;

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

1003 ;

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

1005 ;

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

1007 ;

1008 @@{attribute consumes} @{syntax int}?

1009 \<close>}

1011 \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local context \<open>c:

1012 x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an appropriate proof method (such

1013 as @{method_ref cases} and @{method_ref induct}). The command ``@{command

1014 "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>'' abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots>

1015 x\<^sub>m\<close>~@{command "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by

1016 the prefix \<open>a\<close>, and all such facts are collectively bound to the name \<open>a\<close>.

1018 The fact name is specification \<open>a\<close> is optional, the default is to re-use

1019 \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same as @{command

1020 "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.

1022 \<^descr> @{command "print_cases"} prints all local contexts of the current state,

1023 using Isar proof language notation.

1025 \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for the local contexts

1026 of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close> refers to the \<^emph>\<open>prefix\<close> of the list

1027 of premises. Each of the cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where

1028 the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close> from left to

1029 right.

1031 \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares names for the

1032 conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix

1033 of arguments of a logical formula built by nesting a binary connective

1034 (e.g.\ \<open>\<or>\<close>).

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

1037 already provide a default name for the conclusion as a whole. The need to

1038 name subformulas only arises with cases that split into several sub-cases,

1039 as in common co-induction rules.

1041 \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames the innermost

1042 parameters of premises \<open>1, \<dots>, n\<close> of some theorem. An empty list of names may

1043 be given to skip positions, leaving the present parameters unchanged.

1045 Note that the default usage of case rules does \<^emph>\<open>not\<close> directly expose

1046 parameters to the proof context.

1048 \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major premises'' of a

1049 rule, i.e.\ the number of facts to be consumed when it is applied by an

1050 appropriate proof method. The default value of @{attribute consumes} is \<open>n =

1051 1\<close>, which is appropriate for the usual kind of cases and induction rules for

1052 inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any

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

1054 consumes}~\<open>0\<close> had been specified.

1056 A negative \<open>n\<close> is interpreted relatively to the total number of premises of

1057 the rule in the target context. Thus its absolute value specifies the

1058 remaining number of premises, after subtracting the prefix of major premises

1059 as indicated above. This form of declaration has the technical advantage of

1060 being stable under more morphisms, notably those that export the result from

1061 a nested @{command_ref context} with additional assumptions.

1063 Note that explicit @{attribute consumes} declarations are only rarely

1064 needed; this is already taken care of automatically by the higher-level

1065 @{attribute cases}, @{attribute induct}, and @{attribute coinduct}

1066 declarations.

1067 \<close>

1070 subsection \<open>Proof methods\<close>

1072 text \<open>

1073 \begin{matharray}{rcl}

1074 @{method_def cases} & : & \<open>method\<close> \\

1075 @{method_def induct} & : & \<open>method\<close> \\

1076 @{method_def induction} & : & \<open>method\<close> \\

1077 @{method_def coinduct} & : & \<open>method\<close> \\

1078 \end{matharray}

1080 The @{method cases}, @{method induct}, @{method induction}, and @{method

1081 coinduct} methods provide a uniform interface to common proof techniques

1082 over datatypes, inductive predicates (or sets), recursive functions etc. The

1083 corresponding rules may be specified and instantiated in a casual manner.

1084 Furthermore, these methods provide named local contexts that may be invoked

1085 via the @{command "case"} proof command within the subsequent proof text.

1086 This accommodates compact proof texts even when reasoning about large

1087 specifications.

1089 The @{method induct} method also provides some additional infrastructure in

1090 order to be applicable to structure statements (either using explicit

1091 meta-level connectives, or including facts and parameters separately). This

1092 avoids cumbersome encoding of ``strengthened'' inductive statements within

1093 the object-logic.

1095 Method @{method induction} differs from @{method induct} only in the names

1096 of the facts in the local context invoked by the @{command "case"} command.

1098 @{rail \<open>

1099 @@{method cases} ('(' 'no_simp' ')')? \<newline>

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

1101 ;

1102 (@@{method induct} | @@{method induction})

1103 ('(' 'no_simp' ')')? (definsts * @'and') \<newline> arbitrary? taking? rule?

1104 ;

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

1106 ;

1108 rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)

1109 ;

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

1111 ;

1112 definsts: ( definst * )

1113 ;

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

1115 ;

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

1117 \<close>}

1119 \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method rule} with an

1120 appropriate case distinction theorem, instantiated to the subjects \<open>insts\<close>.

1121 Symbolic case names are bound according to the rule's local contexts.

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

1124 passed to the @{method cases} method:

1126 \<^medskip>

1127 \begin{tabular}{llll}

1128 facts & & arguments & rule \\\hline

1129 \<open>\<turnstile> R\<close> & @{method cases} & & implicit rule \<open>R\<close> \\

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

1131 & @{method cases} & \<open>t\<close> & datatype exhaustion (type of \<open>t\<close>) \\

1132 \<open>\<turnstile> A t\<close> & @{method cases} & \<open>\<dots>\<close> & inductive predicate/set elimination (of \<open>A\<close>) \\

1133 \<open>\<dots>\<close> & @{method cases} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\

1134 \end{tabular}

1135 \<^medskip>

1137 Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close> of premises

1138 of the case rule; within each premise, the \<^emph>\<open>prefix\<close> of variables is

1139 instantiated. In most situations, only a single term needs to be specified;

1140 this refers to the first variable of the last premise (it is usually the

1141 same for all cases). The \<open>(no_simp)\<close> option can be used to disable

1142 pre-simplification of cases (see the description of @{method induct} below

1143 for details).

1145 \<^descr> @{method induct}~\<open>insts R\<close> and @{method induction}~\<open>insts R\<close> are analogous

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

1147 determined as follows:

1149 \<^medskip>

1150 \begin{tabular}{llll}

1151 facts & & arguments & rule \\\hline

1152 & @{method induct} & \<open>P x\<close> & datatype induction (type of \<open>x\<close>) \\

1153 \<open>\<turnstile> A x\<close> & @{method induct} & \<open>\<dots>\<close> & predicate/set induction (of \<open>A\<close>) \\

1154 \<open>\<dots>\<close> & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\

1155 \end{tabular}

1156 \<^medskip>

1158 Several instantiations may be given, each referring to some part of a mutual

1159 inductive definition or datatype --- only related partial induction rules

1160 may be used together, though. Any of the lists of terms \<open>P, x, \<dots>\<close> refers to

1161 the \<^emph>\<open>suffix\<close> of variables present in the induction rule. This enables the

1162 writer to specify only induction variables, or both predicates and

1163 variables, for example.

1165 Instantiations may be definitional: equations \<open>x \<equiv> t\<close> introduce local

1166 definitions, which are inserted into the claim and discharged after applying

1167 the induction rule. Equalities reappear in the inductive cases, but have

1168 been transformed according to the induction principle being involved here.

1169 In order to achieve practically useful induction hypotheses, some variables

1170 occurring in \<open>t\<close> need to be fixed (see below). Instantiations of the form

1171 \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv> t\<close>,

1172 where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be

1173 enclosed in parentheses. By default, the equalities generated by

1174 definitional instantiations are pre-simplified using a specific set of

1175 rules, usually consisting of distinctness and injectivity theorems for

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

1177 inductive case to disappear, or may even completely delete some of the

1178 inductive cases, if one of the equalities occurring in their premises can be

1179 simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable

1180 pre-simplification. Additional rules to be used in pre-simplification can be

1181 declared using the @{attribute_def induct_simp} attribute.

1183 The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables

1184 \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can

1185 separate variables by ``\<open>and\<close>'' to generalize them in other goals then the

1186 first. Thus induction hypotheses may become sufficiently general to get the

1187 proof through. Together with definitional instantiations, one may

1188 effectively perform induction over expressions of a certain structure.

1190 The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional

1191 instantiations of a prefix of pending variables in the rule. Such schematic

1192 induction rules rarely occur in practice, though.

1194 \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the @{method induct} method,

1195 but refers to coinduction rules, which are determined as follows:

1197 \<^medskip>

1198 \begin{tabular}{llll}

1199 goal & & arguments & rule \\\hline

1200 & @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\

1201 \<open>A x\<close> & @{method coinduct} & \<open>\<dots>\<close> & predicate/set coinduction (of \<open>A\<close>) \\

1202 \<open>\<dots>\<close> & @{method coinduct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\

1203 \end{tabular}

1204 \<^medskip>

1206 Coinduction is the dual of induction. Induction essentially eliminates \<open>A x\<close>

1207 towards a generic result \<open>P x\<close>, while coinduction introduces \<open>A x\<close> starting

1208 with \<open>B x\<close>, for a suitable ``bisimulation'' \<open>B\<close>. The cases of a coinduct

1209 rule are typically named after the predicates or sets being covered, while

1210 the conclusions consist of several alternatives being named after the

1211 individual destructor patterns.

1213 The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables occurring in

1214 the rule's major premise, or conclusion if unavailable. An additional

1215 ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification may be required in order to specify

1216 the bisimulation to be used in the coinduction step.

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

1220 instantiated rule as given in the text. Beyond that, the @{method induct}

1221 and @{method coinduct} methods guess further instantiations from the goal

1222 specification itself. Any persisting unresolved schematic variables of the

1223 resulting rule will render the the corresponding case invalid. The term

1224 binding @{variable ?case} for the conclusion will be provided with each

1225 case, provided that term is fully specified.

1227 The @{command "print_cases"} command prints all named cases present in the

1228 current proof state.

1230 \<^medskip>

1231 Despite the additional infrastructure, both @{method cases} and @{method

1232 coinduct} merely apply a certain rule, after instantiation, while conforming

1233 due to the usual way of monotonic natural deduction: the context of a

1234 structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close> reappears unchanged after

1235 the case split.

1237 The @{method induct} method is fundamentally different in this respect: the

1238 meta-level structure is passed through the ``recursive'' course involved in

1239 the induction. Thus the original statement is basically replaced by separate

1240 copies, corresponding to the induction hypotheses and conclusion; the

1241 original goal context is no longer available. Thus local assumptions, fixed

1242 parameters and definitions effectively participate in the inductive

1243 rephrasing of the original statement.

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

1246 into two different kinds: \<open>hyps\<close> stemming from the rule and \<open>prems\<close> from the

1247 goal statement. This is reflected in the extracted cases accordingly, so

1248 invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and

1249 \<open>c.prems\<close>, as well as fact \<open>c\<close> to hold the all-inclusive list.

1251 In @{method induction} proofs, local assumptions introduced by cases are

1252 split into three different kinds: \<open>IH\<close>, the induction hypotheses, \<open>hyps\<close>,

1253 the remaining hypotheses stemming from the rule, and \<open>prems\<close>, the

1254 assumptions from the goal statement. The names are \<open>c.IH\<close>, \<open>c.hyps\<close> and

1255 \<open>c.prems\<close>, as above.

1257 \<^medskip>

1258 Facts presented to either method are consumed according to the number of

1259 ``major premises'' of the rule involved, which is usually 0 for plain cases

1260 and induction rules of datatypes etc.\ and 1 for rules of inductive

1261 predicates or sets and the like. The remaining facts are inserted into the

1262 goal verbatim before the actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is

1263 applied.

1264 \<close>

1267 subsection \<open>Declaring rules\<close>

1269 text \<open>

1270 \begin{matharray}{rcl}

1271 @{command_def "print_induct_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

1272 @{attribute_def cases} & : & \<open>attribute\<close> \\

1273 @{attribute_def induct} & : & \<open>attribute\<close> \\

1274 @{attribute_def coinduct} & : & \<open>attribute\<close> \\

1275 \end{matharray}

1277 @{rail \<open>

1278 @@{attribute cases} spec

1279 ;

1280 @@{attribute induct} spec

1281 ;

1282 @@{attribute coinduct} spec

1283 ;

1285 spec: (('type' | 'pred' | 'set') ':' @{syntax name}) | 'del'

1286 \<close>}

1288 \<^descr> @{command "print_induct_rules"} prints cases and induct rules for

1289 predicates (or sets) and types of the current context.

1291 \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute coinduct} (as

1292 attributes) declare rules for reasoning about (co)inductive predicates (or

1293 sets) and types, using the corresponding methods of the same name. Certain

1294 definitional packages of object-logics usually declare emerging cases and

1295 induction rules as expected, so users rarely need to intervene.

1297 Rules may be deleted via the \<open>del\<close> specification, which covers all of the

1298 \<open>type\<close>/\<open>pred\<close>/\<open>set\<close> sub-categories simultaneously. For example, @{attribute

1299 cases}~\<open>del\<close> removes any @{attribute cases} rules declared for some type,

1300 predicate, or set.

1302 Manual rule declarations usually refer to the @{attribute case_names} and

1303 @{attribute params} attributes to adjust names of cases and parameters of a

1304 rule; the @{attribute consumes} declaration is taken care of automatically:

1305 @{attribute consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute

1306 consumes}~\<open>1\<close> for ``predicate'' / ``set'' rules.

1307 \<close>

1310 section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close>

1312 text \<open>

1313 \begin{matharray}{rcl}

1314 @{command_def "consider"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

1315 @{command_def "obtain"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

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

1317 \end{matharray}

1319 Generalized elimination means that hypothetical parameters and premises may

1320 be introduced in the current context, potentially with a split into cases.

1321 This works by virtue of a locally proven rule that establishes the soundness

1322 of this temporary context extension. As representative examples, one may

1323 think of standard rules from Isabelle/HOL like this:

1325 \<^medskip>

1326 \begin{tabular}{ll}

1327 \<open>\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\

1328 \<open>A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\

1329 \<open>A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\

1330 \end{tabular}

1331 \<^medskip>

1333 In general, these particular rules and connectives need to get involved at

1334 all: this concept works directly in Isabelle/Pure via Isar commands defined

1335 below. In particular, the logic of elimination and case splitting is

1336 delegated to an Isar proof, which often involves automated tools.

1338 @{rail \<open>

1339 @@{command consider} @{syntax obtain_clauses}

1340 ;

1341 @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>

1342 @'where' concl prems @{syntax for_fixes}

1343 ;

1344 concl: (@{syntax props} + @'and')

1345 ;

1346 prems: (@'if' (@{syntax props'} + @'and'))?

1347 ;

1348 @@{command guess} @{syntax vars}

1349 \<close>}

1351 \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)

1352 \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting

1353 into separate subgoals, such that each case involves new parameters and

1354 premises. After the proof is finished, the resulting rule may be used

1355 directly with the @{method cases} proof method (\secref{sec:cases-induct}),

1356 in order to perform actual case-splitting of the proof text via @{command

1357 case} and @{command next} as usual.

1359 Optional names in round parentheses refer to case names: in the proof of the

1360 rule this is a fact name, in the resulting rule it is used as annotation

1361 with the @{attribute_ref case_names} attribute.

1363 \<^medskip>

1364 Formally, the command @{command consider} is defined as derived Isar

1365 language element as follows:

1367 \begin{matharray}{l}

1368 @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]

1369 \quad @{command "have"}~\<open>[case_names a b \<dots>]: thesis\<close> \\

1370 \qquad \<open>\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\

1371 \qquad \<open>\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis\<close> \\

1372 \qquad \<open>\<AND> \<dots>\<close> \\

1373 \qquad \<open>\<FOR> thesis\<close> \\

1374 \qquad @{command "apply"}~\<open>(insert a b \<dots>)\<close> \\

1375 \end{matharray}

1377 See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal

1378 statements, as well as @{command print_statement} to print existing rules in

1379 a similar format.

1381 \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> states a

1382 generalized elimination rule with exactly one case. After the proof is

1383 finished, it is activated for the subsequent proof text: the context is

1384 augmented via @{command fix}~\<open>\<^vec>x\<close> @{command assume}~\<open>\<^vec>A

1385 \<^vec>x\<close>, with special provisions to export later results by discharging

1386 these assumptions again.

1388 Note that according to the parameter scopes within the elimination rule,

1389 results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the export

1390 will fail! This restriction conforms to the usual manner of existential

1391 reasoning in Natural Deduction.

1393 \<^medskip>

1394 Formally, the command @{command obtain} is defined as derived Isar language

1395 element as follows, using an instrumented variant of @{command assume}:

1397 \begin{matharray}{l}

1398 @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]

1399 \quad @{command "have"}~\<open>thesis\<close> \\

1400 \qquad \<open>\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\

1401 \qquad \<open>\<FOR> thesis\<close> \\

1402 \qquad @{command "apply"}~\<open>(insert that)\<close> \\

1403 \qquad \<open>\<langle>proof\<rangle>\<close> \\

1404 \quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\

1405 \end{matharray}

1407 \<^descr> @{command guess} is similar to @{command obtain}, but it derives the

1408 obtained context elements from the course of tactical reasoning in the

1409 proof. Thus it can considerably obscure the proof: it is classified as

1410 \<^emph>\<open>improper\<close>.

1412 A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The

1413 subsequent refinement steps may turn this to anything of the form

1414 \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new

1415 subgoals. The final goal state is then used as reduction rule for the obtain

1416 pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as

1417 internal by default, and thus inaccessible in the proof text. The variable

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

1419 a prefix of accessible parameters.

1422 In the proof of @{command consider} and @{command obtain} the local premises

1423 are always bound to the fact name @{fact_ref that}, according to structured

1424 Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).

1426 Facts that are established by @{command "obtain"} and @{command "guess"} may

1427 not be polymorphic: any type-variables occurring here are fixed in the

1428 present context. This is a natural consequence of the role of @{command fix}

1429 and @{command assume} in these constructs.

1430 \<close>

1432 end