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

src/Doc/Isar_Ref/Proof.thy

author | wenzelm |

Mon Oct 09 21:12:22 2017 +0200 (23 months ago) | |

changeset 66822 | 4642cf4a7ebb |

parent 64926 | 75ee8475c37e |

child 67119 | acb0807ddb56 |

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

tuned signature;

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 @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

132 \end{matharray}

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

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

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

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

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

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

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

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

142 Isabelle's meta-variables).

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

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

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

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

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

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

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

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

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

153 user.

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

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

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

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

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

161 @{rail \<open>

162 @@{command fix} @{syntax vars}

163 ;

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

165 ;

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

167 ;

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

169 ;

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

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

172 ;

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

174 ;

175 def: @{syntax thmdecl}? \<newline>

176 @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?

177 \<close>}

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

180 but fixed\<close>.

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

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

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

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

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

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

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

190 concatenated.

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

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

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

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

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

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

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

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

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

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

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

207 \<^medskip>

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

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

211 \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an

212 old form of \<^theory_text>\<open>define x where "x = t"\<close>.

213 \<close>

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

218 text \<open>

219 \begin{matharray}{rcl}

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

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

222 \end{matharray}

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

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

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

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

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

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

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

231 position.

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

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

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

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

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

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

239 proof text from left to right.

241 \<^medskip>

242 Term abbreviations are quite different from local definitions as introduced

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

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

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

246 "define"} does not support polymorphism.

248 @{rail \<open>

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

250 \<close>}

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

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

255 \<^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

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

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

259 \<^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>

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

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

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

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

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

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

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

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

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

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

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

272 \secref{sec:calculation}).

273 \<close>

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

278 text \<open>

279 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

288 \end{matharray}

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

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

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

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

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

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

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

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

298 claim.

300 @{rail \<open>

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

302 ;

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

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

305 ;

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

307 \<close>}

309 \<^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>,

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

311 both on the left and right hand sides.

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

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

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

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

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

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

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

320 relevance of facts in automated proof search.

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

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

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

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

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

328 with the current ones.

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

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

332 "proof"}).

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

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

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

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

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

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

341 explicitly.

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

344 facts of the goal state.

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

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

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

350 empty list of theorems.

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

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

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

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

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

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

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

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

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

362 \<close>

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

367 text \<open>

368 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

379 \end{matharray}

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

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

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

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

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

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

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

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

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

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

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

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

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

396 long goal includes an explicit context specification for the subsequent

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

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

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

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

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

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

403 claims several simultaneous simultaneous contexts of (essentially a big

404 disjunction of eliminated parameters and assumptions, cf.\

405 \secref{sec:obtain}).

407 @{rail \<open>

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

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

410 (long_statement | short_statement)

411 ;

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

413 stmt cond_stmt @{syntax for_fixes}

414 ;

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

416 ;

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

419 ;

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

421 ;

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

423 ;

424 long_statement: @{syntax thmdecl}? context conclusion

425 ;

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

427 ;

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

429 ;

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

431 ;

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

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

434 \<close>}

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

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

438 context.

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

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

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

443 in \secref{sec:locale}.

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

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

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

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

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

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

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

454 as a formal comment in the theory source.

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

457 the statement to contain unbound schematic variables.

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

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

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

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

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

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

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

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

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

469 potential results within a proof body.

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

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

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

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

476 To accommodate interactive debugging, resulting rules are printed before

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

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

479 warning beforehand. Watch out for the following message:

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

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

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

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

485 more orthogonal and improves readability and maintainability of proofs.

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

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

489 "lemma"} given above.

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

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

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

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

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

498 to the syntax of the statement.

499 \<close>

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

504 text \<open>

505 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

514 \end{matharray}

516 Calculational proof is forward reasoning with implicit application of

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

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

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

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

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

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

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

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

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

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

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

528 yet.

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

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

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

533 be its right-hand side.)

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

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

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

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

539 command required.

541 \<^medskip>

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

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

545 \begin{matharray}{rcl}

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

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

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

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

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

551 \end{matharray}

553 @{rail \<open>

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

555 ;

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

557 \<close>}

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

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

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

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

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

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

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

566 arguments.

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

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

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

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

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

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

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

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

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

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

579 without applying rules.

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

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

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

584 elimination patters) of the current context.

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

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

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

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

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

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

594 assumption.

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

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

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

599 \<close>

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

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

606 text \<open>

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

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

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

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

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

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

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

614 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

615 to high).

617 @{rail \<open>

618 @{syntax_def method}:

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

620 ;

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

622 \<close>}

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

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

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

627 is known from ML tactics.

629 \<^medskip>

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

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

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

633 are presently exposed.

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

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

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

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

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

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

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

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

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

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

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

648 \<^medskip>

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

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

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

653 @{rail \<open>

654 @{syntax_def goal_spec}:

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

656 \<close>}

657 \<close>

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

662 text \<open>

663 \begin{matharray}{rcl}

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

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

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

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

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

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

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

671 \end{matharray}

673 Arbitrary goal refinement via tactics is considered harmful. Structured

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

675 only.

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

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

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

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

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

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

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

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

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

688 tactic scripts that consist of numerous consecutive goal transformations,

689 with invisible effects.

691 \<^medskip>

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

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

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

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

696 the proof document in an intelligible manner.

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

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

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

701 standard elimination or introduction rule according to the topmost logical

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

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

705 @{rail \<open>

706 @@{command proof} method?

707 ;

708 @@{command qed} method?

709 ;

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

711 ;

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

713 \<close>}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

734 to see the problem.

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

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

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

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

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

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

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

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

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

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

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

750 experimentation and top-down proof development.

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

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

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

755 environment.

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

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

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

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

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

763 \<close>

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

768 text \<open>

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

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

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

772 \partref{part:hol}).

774 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

789 \end{matharray}

791 @{rail \<open>

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

793 ;

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

795 ;

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

797 ;

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

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

800 ;

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

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

803 ;

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

805 ;

806 @@{attribute OF} @{syntax thms}

807 ;

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

809 ;

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

811 \<close>}

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

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

815 Isabelle/Pure.

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

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

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

821 into the goal, and nothing else.

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

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

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

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

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

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

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

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

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

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

835 conclusion.

837 \<^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

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

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

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

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

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

843 "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>

844 in the proof context.

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

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

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

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

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

851 assumption} method at all.

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

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

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

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

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

859 with facts it becomes elimination.

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

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

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

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

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

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

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

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

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

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

872 aggressively.

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

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

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

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

879 destruct rules.

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

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

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

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

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

886 functional application (modulo unification).

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

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

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

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

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

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

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

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

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

899 (usually with some shifting of indices).

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

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

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

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

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

906 instantiations, explicit type instantiations are seldom necessary.

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

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

910 \<close>

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

915 text \<open>

916 \begin{matharray}{rcl}

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

918 \end{matharray}

920 @{rail \<open>

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

922 \<close>}

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

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

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

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

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

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

930 primed versions refer to tactics with explicit goal addressing.

932 Here are some example method definitions:

933 \<close>

935 (*<*)experiment begin(*>*)

936 method_setup my_method1 =

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

938 "my first method (without any arguments)"

940 method_setup my_method2 =

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

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

943 "my second method (with context)"

945 method_setup my_method3 =

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

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

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

949 (*<*)end(*>*)

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

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

956 text \<open>

957 \begin{matharray}{rcl}

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

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

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

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

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

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

964 \end{matharray}

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

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

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

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

970 involve big induction rules with several cases.

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

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

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

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

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

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

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

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

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

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

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

984 names that fit nicely into the current context.

986 \<^medskip>

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

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

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

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

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

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

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

994 quite unpredictable.

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

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

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

999 definitions).

1001 \<^medskip>

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

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

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

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

1006 advanced case analysis later.

1008 @{rail \<open>

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

1010 ;

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

1012 ;

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

1014 ;

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

1016 ;

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

1018 \<close>}

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

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

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

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

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

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

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

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

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

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

1032 using Isar proof language notation.

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

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

1036 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

1037 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

1038 right.

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

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

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

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

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

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

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

1048 as in common co-induction rules.

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

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

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

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

1055 parameters to the proof context.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1075 declarations.

1076 \<close>

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

1081 text \<open>

1082 \begin{matharray}{rcl}

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

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

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

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

1087 \end{matharray}

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

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

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

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

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

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

1095 This accommodates compact proof texts even when reasoning about large

1096 specifications.

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

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

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

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

1102 the object-logic.

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

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

1107 @{rail \<open>

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

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

1110 ;

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

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

1113 ;

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

1115 ;

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

1118 ;

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

1120 ;

1121 definsts: ( definst * )

1122 ;

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

1124 ;

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

1126 \<close>}

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

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

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

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

1133 passed to the @{method cases} method:

1135 \<^medskip>

1136 \begin{tabular}{llll}

1137 facts & & arguments & rule \\\hline

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

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

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

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

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

1143 \end{tabular}

1144 \<^medskip>

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

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

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

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

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

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

1152 for details).

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

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

1156 determined as follows:

1158 \<^medskip>

1159 \begin{tabular}{llll}

1160 facts & & arguments & rule \\\hline

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

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

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

1164 \end{tabular}

1165 \<^medskip>

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

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

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

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

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

1172 variables, for example.

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

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

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

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

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

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

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

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

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

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

1184 rules, usually consisting of distinctness and injectivity theorems for

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

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

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

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

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

1190 declared using the @{attribute_def induct_simp} attribute.

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

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

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

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

1196 proof through. Together with definitional instantiations, one may

1197 effectively perform induction over expressions of a certain structure.

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

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

1201 induction rules rarely occur in practice, though.

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

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

1206 \<^medskip>

1207 \begin{tabular}{llll}

1208 goal & & arguments & rule \\\hline

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

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

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

1212 \end{tabular}

1213 \<^medskip>

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

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

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

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

1219 the conclusions consist of several alternatives being named after the

1220 individual destructor patterns.

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

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

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

1225 the bisimulation to be used in the coinduction step.

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

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

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

1231 specification itself. Any persisting unresolved schematic variables of the

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

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

1234 case, provided that term is fully specified.

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

1237 current proof state.

1239 \<^medskip>

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

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

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

1243 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

1244 the case split.

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

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

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

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

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

1251 parameters and definitions effectively participate in the inductive

1252 rephrasing of the original statement.

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

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

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

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

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

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

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

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

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

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

1266 \<^medskip>

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

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

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

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

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

1272 applied.

1273 \<close>

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

1278 text \<open>

1279 \begin{matharray}{rcl}

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

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

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

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

1284 \end{matharray}

1286 @{rail \<open>

1287 @@{attribute cases} spec

1288 ;

1289 @@{attribute induct} spec

1290 ;

1291 @@{attribute coinduct} spec

1292 ;

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

1295 \<close>}

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

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

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

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

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

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

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

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

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

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

1309 predicate, or set.

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

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

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

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

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

1316 \<close>

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

1321 text \<open>

1322 \begin{matharray}{rcl}

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

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

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

1326 \end{matharray}

1328 Generalized elimination means that hypothetical parameters and premises may

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

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

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

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

1334 \<^medskip>

1335 \begin{tabular}{ll}

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

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

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

1339 \end{tabular}

1340 \<^medskip>

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

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

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

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

1347 @{rail \<open>

1348 @@{command consider} @{syntax obtain_clauses}

1349 ;

1350 @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>

1351 @'where' concl prems @{syntax for_fixes}

1352 ;

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

1354 ;

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

1356 ;

1357 @@{command guess} @{syntax vars}

1358 \<close>}

1360 \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)

1361 \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting

1362 into separate subgoals, such that each case involves new parameters and

1363 premises. After the proof is finished, the resulting rule may be used

1364 directly with the @{method cases} proof method (\secref{sec:cases-induct}),

1365 in order to perform actual case-splitting of the proof text via @{command

1366 case} and @{command next} as usual.

1368 Optional names in round parentheses refer to case names: in the proof of the

1369 rule this is a fact name, in the resulting rule it is used as annotation

1370 with the @{attribute_ref case_names} attribute.

1372 \<^medskip>

1373 Formally, the command @{command consider} is defined as derived Isar

1374 language element as follows:

1376 \begin{matharray}{l}

1377 @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]

1378 \quad @{command "have"}~\<open>[case_names a b \<dots>]: thesis\<close> \\

1379 \qquad \<open>\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\

1380 \qquad \<open>\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis\<close> \\

1381 \qquad \<open>\<AND> \<dots>\<close> \\

1382 \qquad \<open>\<FOR> thesis\<close> \\

1383 \qquad @{command "apply"}~\<open>(insert a b \<dots>)\<close> \\

1384 \end{matharray}

1386 See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal

1387 statements, as well as @{command print_statement} to print existing rules in

1388 a similar format.

1390 \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> states a

1391 generalized elimination rule with exactly one case. After the proof is

1392 finished, it is activated for the subsequent proof text: the context is

1393 augmented via @{command fix}~\<open>\<^vec>x\<close> @{command assume}~\<open>\<^vec>A

1394 \<^vec>x\<close>, with special provisions to export later results by discharging

1395 these assumptions again.

1397 Note that according to the parameter scopes within the elimination rule,

1398 results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the export

1399 will fail! This restriction conforms to the usual manner of existential

1400 reasoning in Natural Deduction.

1402 \<^medskip>

1403 Formally, the command @{command obtain} is defined as derived Isar language

1404 element as follows, using an instrumented variant of @{command assume}:

1406 \begin{matharray}{l}

1407 @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]

1408 \quad @{command "have"}~\<open>thesis\<close> \\

1409 \qquad \<open>\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\

1410 \qquad \<open>\<FOR> thesis\<close> \\

1411 \qquad @{command "apply"}~\<open>(insert that)\<close> \\

1412 \qquad \<open>\<langle>proof\<rangle>\<close> \\

1413 \quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\

1414 \end{matharray}

1416 \<^descr> @{command guess} is similar to @{command obtain}, but it derives the

1417 obtained context elements from the course of tactical reasoning in the

1418 proof. Thus it can considerably obscure the proof: it is classified as

1419 \<^emph>\<open>improper\<close>.

1421 A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The

1422 subsequent refinement steps may turn this to anything of the form

1423 \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new

1424 subgoals. The final goal state is then used as reduction rule for the obtain

1425 pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as

1426 internal by default, and thus inaccessible in the proof text. The variable

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

1428 a prefix of accessible parameters.

1431 In the proof of @{command consider} and @{command obtain} the local premises

1432 are always bound to the fact name @{fact_ref that}, according to structured

1433 Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).

1435 Facts that are established by @{command "obtain"} and @{command "guess"} may

1436 not be polymorphic: any type-variables occurring here are fixed in the

1437 present context. This is a natural consequence of the role of @{command fix}

1438 and @{command assume} in these constructs.

1439 \<close>

1441 end