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

src/Doc/Isar_Ref/Proof.thy

author | wenzelm |

Tue Apr 26 22:39:17 2016 +0200 (2016-04-26 ago) | |

changeset 63059 | 3f577308551e |

parent 63043 | 1a20fd9cf281 |

child 63094 | 056ea294c256 |

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

'obtain' supports structured statements (similar to 'define');

1 (*:maxLineLen=78:*)

3 theory Proof

4 imports Base Main

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 "fixes"}

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 "fixes"} + @'and')

171 @'where' (@{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" and "A x" for x\<close> is equivalent

193 to \<^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 \end{matharray}

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

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

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

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

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

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

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

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

296 claim.

298 @{rail \<open>

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

300 ;

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

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

303 \<close>}

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

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

307 both on the left and right hand sides.

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

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

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

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

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

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

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

316 relevance of facts in automated proof search.

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

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

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

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

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

324 with the current ones.

326 \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being currently

327 indicated for use by a subsequent refinement step (such as @{command_ref

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

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

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

332 goal state and facts.

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

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

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

338 empty list of theorems.

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

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

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

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

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

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

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

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

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

350 \<close>

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

355 text \<open>

356 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

367 \end{matharray}

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

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

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

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

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

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

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

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

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

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

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

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

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

384 long goal includes an explicit context specification for the subsequent

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

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

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

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

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

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

391 claims several simultaneous simultaneous contexts of (essentially a big

392 disjunction of eliminated parameters and assumptions, cf.\

393 \secref{sec:obtain}).

395 @{rail \<open>

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

397 @@{command proposition} | @@{command schematic_goal}) (stmt | statement)

398 ;

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

400 stmt cond_stmt @{syntax for_fixes}

401 ;

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

403 ;

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

406 ;

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

408 ;

409 statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>

410 conclusion

411 ;

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

413 ;

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

415 ;

416 @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'

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

418 \<close>}

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

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

422 context. An additional @{syntax context} specification may build up an

423 initial proof context for the subsequent claim; this includes local

424 definitions and syntax as well, see also @{syntax "includes"} in

425 \secref{sec:bundle} and @{syntax context_elem} in \secref{sec:locale}.

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

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

429 as a formal comment in the theory source.

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

432 the statement to contain unbound schematic variables.

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

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

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

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

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

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

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

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

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

444 potential results within a proof body.

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

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

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

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

451 To accommodate interactive debugging, resulting rules are printed before

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

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

454 warning beforehand. Watch out for the following message:

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

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

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

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

460 more orthogonal and improves readability and maintainability of proofs.

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

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

464 "lemma"} given above.

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

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

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

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

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

473 to the syntax of the statement.

474 \<close>

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

479 text \<open>

480 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

489 \end{matharray}

491 Calculational proof is forward reasoning with implicit application of

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

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

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

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

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

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

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

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

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

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

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

503 yet.

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

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

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

508 be its right-hand side.)

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

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

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

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

514 command required.

516 \<^medskip>

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

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

520 \begin{matharray}{rcl}

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

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

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

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

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

526 \end{matharray}

528 @{rail \<open>

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

530 ;

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

532 \<close>}

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

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

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

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

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

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

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

541 arguments.

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

544 same way as @{command "also"}, and concludes the current calculational

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

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

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

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

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

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

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

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

554 without applying rules.

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

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

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

559 elimination patters) of the current context.

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

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

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

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

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

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

569 assumption.

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

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

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

574 \<close>

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

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

581 text \<open>

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

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

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

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

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

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

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

589 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

590 to high).

592 @{rail \<open>

593 @{syntax_def method}:

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

595 ;

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

597 \<close>}

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

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

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

602 is known from ML tactics.

604 \<^medskip>

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

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

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

608 are presently exposed.

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

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

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

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

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

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

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

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

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

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

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

623 \<^medskip>

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

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

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

628 @{rail \<open>

629 @{syntax_def goal_spec}:

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

631 \<close>}

632 \<close>

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

637 text \<open>

638 \begin{matharray}{rcl}

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

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

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

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

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

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

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

646 \end{matharray}

648 Arbitrary goal refinement via tactics is considered harmful. Structured

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

650 only.

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

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

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

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

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

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

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

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

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

663 tactic scripts that consist of numerous consecutive goal transformations,

664 with invisible effects.

666 \<^medskip>

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

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

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

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

671 the proof document in an intelligible manner.

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

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

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

676 standard elimination or introduction rule according to the topmost logical

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

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

680 @{rail \<open>

681 @@{command proof} method?

682 ;

683 @@{command qed} method?

684 ;

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

686 ;

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

688 \<close>}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

709 to see the problem.

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

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

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

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

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

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

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

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

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

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

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

725 experimentation and top-down proof development.

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

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

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

730 environment.

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

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

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

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

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

738 \<close>

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

743 text \<open>

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

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

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

747 \partref{part:hol}).

749 \begin{matharray}{rcl}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

764 \end{matharray}

766 @{rail \<open>

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

768 ;

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

770 ;

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

772 ;

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

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

775 ;

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

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

778 ;

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

780 ;

781 @@{attribute OF} @{syntax thms}

782 ;

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

784 ;

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

786 \<close>}

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

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

790 Isabelle/Pure.

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

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

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

796 into the goal, and nothing else.

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

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

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

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

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

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

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

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

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

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

810 conclusion.

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

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

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

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

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

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

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

819 in the proof context.

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

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

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

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

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

826 assumption} method at all.

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

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

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

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

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

834 with facts it becomes elimination.

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

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

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

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

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

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

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

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

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

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

847 aggressively.

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

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

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

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

854 destruct rules.

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

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

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

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

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

861 functional application (modulo unification).

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

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

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

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

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

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

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

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

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

874 (usually with some shifting of indices).

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

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

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

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

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

881 instantiations, explicit type instantiations are seldom necessary.

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

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

885 \<close>

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

890 text \<open>

891 \begin{matharray}{rcl}

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

893 \end{matharray}

895 @{rail \<open>

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

897 \<close>}

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

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

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

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

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

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

905 primed versions refer to tactics with explicit goal addressing.

907 Here are some example method definitions:

908 \<close>

910 (*<*)experiment begin(*>*)

911 method_setup my_method1 =

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

913 "my first method (without any arguments)"

915 method_setup my_method2 =

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

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

918 "my second method (with context)"

920 method_setup my_method3 =

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

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

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

924 (*<*)end(*>*)

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

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

931 text \<open>

932 \begin{matharray}{rcl}

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

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

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

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

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

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

939 \end{matharray}

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

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

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

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

945 involve big induction rules with several cases.

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

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

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

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

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

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

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

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

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

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

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

959 names that fit nicely into the current context.

961 \<^medskip>

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

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

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

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

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

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

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

969 quite unpredictable.

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

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

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

974 definitions).

976 \<^medskip>

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

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

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

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

981 advanced case analysis later.

983 @{rail \<open>

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

985 ;

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

987 ;

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

989 ;

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

991 ;

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

993 \<close>}

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

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

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

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

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

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

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

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

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

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

1007 using Isar proof language notation.

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

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

1011 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

1012 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

1013 right.

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

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

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

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

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

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

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

1023 as in common co-induction rules.

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

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

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

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

1030 parameters to the proof context.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1050 declarations.

1051 \<close>

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

1056 text \<open>

1057 \begin{matharray}{rcl}

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

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

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

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

1062 \end{matharray}

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

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

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

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

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

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

1070 This accommodates compact proof texts even when reasoning about large

1071 specifications.

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

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

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

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

1077 the object-logic.

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

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

1082 @{rail \<open>

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

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

1085 ;

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

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

1088 ;

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

1090 ;

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

1093 ;

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

1095 ;

1096 definsts: ( definst * )

1097 ;

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

1099 ;

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

1101 \<close>}

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

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

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

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

1108 passed to the @{method cases} method:

1110 \<^medskip>

1111 \begin{tabular}{llll}

1112 facts & & arguments & rule \\\hline

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

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

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

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

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

1118 \end{tabular}

1119 \<^medskip>

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

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

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

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

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

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

1127 for details).

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

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

1131 determined as follows:

1133 \<^medskip>

1134 \begin{tabular}{llll}

1135 facts & & arguments & rule \\\hline

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

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

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

1139 \end{tabular}

1140 \<^medskip>

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

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

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

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

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

1147 variables, for example.

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

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

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

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

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

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

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

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

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

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

1159 rules, usually consisting of distinctness and injectivity theorems for

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

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

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

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

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

1165 declared using the @{attribute_def induct_simp} attribute.

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

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

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

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

1171 proof through. Together with definitional instantiations, one may

1172 effectively perform induction over expressions of a certain structure.

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

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

1176 induction rules rarely occur in practice, though.

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

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

1181 \<^medskip>

1182 \begin{tabular}{llll}

1183 goal & & arguments & rule \\\hline

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

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

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

1187 \end{tabular}

1188 \<^medskip>

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

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

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

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

1194 the conclusions consist of several alternatives being named after the

1195 individual destructor patterns.

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

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

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

1200 the bisimulation to be used in the coinduction step.

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

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

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

1206 specification itself. Any persisting unresolved schematic variables of the

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

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

1209 case, provided that term is fully specified.

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

1212 current proof state.

1214 \<^medskip>

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

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

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

1218 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

1219 the case split.

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

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

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

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

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

1226 parameters and definitions effectively participate in the inductive

1227 rephrasing of the original statement.

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

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

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

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

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

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

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

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

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

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

1241 \<^medskip>

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

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

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

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

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

1247 applied.

1248 \<close>

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

1253 text \<open>

1254 \begin{matharray}{rcl}

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

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

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

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

1259 \end{matharray}

1261 @{rail \<open>

1262 @@{attribute cases} spec

1263 ;

1264 @@{attribute induct} spec

1265 ;

1266 @@{attribute coinduct} spec

1267 ;

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

1270 \<close>}

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

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

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

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

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

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

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

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

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

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

1284 predicate, or set.

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

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

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

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

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

1291 \<close>

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

1296 text \<open>

1297 \begin{matharray}{rcl}

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

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

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

1301 \end{matharray}

1303 Generalized elimination means that hypothetical parameters and premises may

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

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

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

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

1309 \<^medskip>

1310 \begin{tabular}{ll}

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

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

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

1314 \end{tabular}

1315 \<^medskip>

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

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

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

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

1322 @{rail \<open>

1323 @@{command consider} @{syntax obtain_clauses}

1324 ;

1325 @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>

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

1327 ;

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

1329 ;

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

1331 ;

1332 @@{command guess} (@{syntax "fixes"} + @'and')

1333 \<close>}

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

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

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

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

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

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

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

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

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

1345 with the @{attribute_ref case_names} attribute.

1347 \<^medskip>

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

1349 language element as follows:

1351 \begin{matharray}{l}

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

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

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

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

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

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

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

1359 \end{matharray}

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

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

1363 a similar format.

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

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

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

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

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

1370 these assumptions again.

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

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

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

1375 reasoning in Natural Deduction.

1377 \<^medskip>

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

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

1381 \begin{matharray}{l}

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

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

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

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

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

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

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

1389 \end{matharray}

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

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

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

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

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

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

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

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

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

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

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

1403 a prefix of accessible parameters.

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

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

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

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

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

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

1413 and @{command assume} in these constructs.

1414 \<close>

1416 end