Documented changes in induct, cases, and nominal_induct method.
5 chapter {* Proofs \label{ch:proofs} *}
8 Proof commands perform transitions of Isar/VM machine
9 configurations, which are block-structured, consisting of a stack of
10 nodes with three main components: logical proof context, current
11 facts, and open goals. Isar/VM transitions are typed according to
12 the following three different modes of operation:
16 \item @{text "proof(prove)"} means that a new goal has just been
17 stated that is now to be \emph{proven}; the next command may refine
18 it by some proof method, and enter a sub-proof to establish the
21 \item @{text "proof(state)"} is like a nested theory mode: the
22 context may be augmented by \emph{stating} additional assumptions,
23 intermediate results etc.
25 \item @{text "proof(chain)"} is intermediate between @{text
26 "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
27 the contents of the special ``@{fact_ref this}'' register) have been
28 just picked up in order to be used when refining the goal claimed
33 The proof mode indicator may be understood as an instruction to the
34 writer, telling what kind of operation may be performed next. The
35 corresponding typings of proof commands restricts the shape of
36 well-formed proof texts to particular command sequences. So dynamic
37 arrangements of commands eventually turn out as static texts of a
40 \Appref{ap:refcard} gives a simplified grammar of the (extensible)
41 language emerging that way from the different types of proof
42 commands. The main ideas of the overall Isar framework are
43 explained in \chref{ch:isar-framework}.
47 section {* Proof structure *}
49 subsection {* Example proofs *}
52 \begin{matharray}{rcl}
53 @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
58 \item @{command "example_proof"} opens an empty proof body. This
59 allows to experiment with Isar, without producing any persistent
62 Structurally, this is like a vacous @{command "lemma"} statement
63 followed by ``@{command "proof"}~@{text "-"}'', which means the
64 example proof may be closed by a regular @{command "qed"}, or
65 discontinued by @{command "oops"}.
71 subsection {* Blocks *}
74 \begin{matharray}{rcl}
75 @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
76 @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
77 @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
80 While Isar is inherently block-structured, opening and closing
81 blocks is mostly handled rather casually, with little explicit
82 user-intervention. Any local goal statement automatically opens
83 \emph{two} internal blocks, which are closed again when concluding
84 the sub-proof (by @{command "qed"} etc.). Sections of different
85 context within a sub-proof may be switched via @{command "next"},
86 which is just a single block-close followed by block-open again.
87 The effect of @{command "next"} is to reset the local proof context;
88 there is no goal focus involved here!
90 For slightly more advanced applications, there are explicit block
91 parentheses as well. These typically achieve a stronger forward
96 \item @{command "next"} switches to a fresh block within a
97 sub-proof, resetting the local context to the initial one.
99 \item @{command "{"} and @{command "}"} explicitly open and close
100 blocks. Any current facts pass through ``@{command "{"}''
101 unchanged, while ``@{command "}"}'' causes any result to be
102 \emph{exported} into the enclosing context. Thus fixed variables
103 are generalized, assumptions discharged, and local definitions
104 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
105 of @{command "assume"} and @{command "presume"} in this mode of
106 forward reasoning --- in contrast to plain backward reasoning with
107 the result exported at @{command "show"} time.
113 subsection {* Omitting proofs *}
116 \begin{matharray}{rcl}
117 @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\
120 The @{command "oops"} command discontinues the current proof
121 attempt, while considering the partial proof text as properly
122 processed. This is conceptually quite different from ``faking''
123 actual proofs via @{command_ref "sorry"} (see
124 \secref{sec:proof-steps}): @{command "oops"} does not observe the
125 proof structure at all, but goes back right to the theory level.
126 Furthermore, @{command "oops"} does not produce any result theorem
127 --- there is no intended claim to be able to complete the proof
130 A typical application of @{command "oops"} is to explain Isar proofs
131 \emph{within} the system itself, in conjunction with the document
132 preparation tools of Isabelle described in \chref{ch:document-prep}.
133 Thus partial or even wrong proof attempts can be discussed in a
134 logically sound manner. Note that the Isabelle {\LaTeX} macros can
135 be easily adapted to print something like ``@{text "\<dots>"}'' instead of
136 the keyword ``@{command "oops"}''.
138 \medskip The @{command "oops"} command is undo-able, unlike
139 @{command_ref "kill"} (see \secref{sec:history}). The effect is to
140 get back to the theory just before the opening of the proof.
144 section {* Statements *}
146 subsection {* Context elements \label{sec:proof-context} *}
149 \begin{matharray}{rcl}
150 @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
151 @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
152 @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
153 @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
156 The logical proof context consists of fixed variables and
157 assumptions. The former closely correspond to Skolem constants, or
158 meta-level universal quantification as provided by the Isabelle/Pure
159 logical framework. Introducing some \emph{arbitrary, but fixed}
160 variable via ``@{command "fix"}~@{text x}'' results in a local value
161 that may be used in the subsequent proof as any other variable or
162 constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
163 the context will be universally closed wrt.\ @{text x} at the
164 outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
165 form using Isabelle's meta-variables).
167 Similarly, introducing some assumption @{text \<chi>} has two effects.
168 On the one hand, a local theorem is created that may be used as a
169 fact in subsequent proof steps. On the other hand, any result
170 @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
171 the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
172 using such a result would basically introduce a new subgoal stemming
173 from the assumption. How this situation is handled depends on the
174 version of assumption command used: while @{command "assume"}
175 insists on solving the subgoal by unification with some premise of
176 the goal, @{command "presume"} leaves the subgoal unchanged in order
177 to be proved later by the user.
179 Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
180 t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
181 another version of assumption that causes any hypothetical equation
182 @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
183 exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
189 ('assume' | 'presume') (props + 'and')
193 def: thmdecl? \\ name ('==' | equiv) term termpat?
199 \item @{command "fix"}~@{text x} introduces a local variable @{text
200 x} that is \emph{arbitrary, but fixed.}
202 \item @{command "assume"}~@{text "a: \<phi>"} and @{command
203 "presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
204 assumption. Subsequent results applied to an enclosing goal (e.g.\
205 by @{command_ref "show"}) are handled as follows: @{command
206 "assume"} expects to be able to unify with existing premises in the
207 goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
209 Several lists of assumptions may be given (separated by
210 @{keyword_ref "and"}; the resulting list of current facts consists
211 of all of these concatenated.
213 \item @{command "def"}~@{text "x \<equiv> t"} introduces a local
214 (non-polymorphic) definition. In results exported from the context,
215 @{text x} is replaced by @{text t}. Basically, ``@{command
216 "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
217 x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
218 hypothetical equation solved by reflexivity.
220 The default name for the definitional equation is @{text x_def}.
221 Several simultaneous definitions may be given at the same time.
225 The special name @{fact_ref prems} refers to all assumptions of the
226 current context as a list of theorems. This feature should be used
227 with great care! It is better avoided in final proof texts.
231 subsection {* Term abbreviations \label{sec:term-abbrev} *}
234 \begin{matharray}{rcl}
235 @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
236 @{keyword_def "is"} & : & syntax \\
239 Abbreviations may be either bound by explicit @{command
240 "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
241 goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
242 p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
243 bind extra-logical term variables, which may be either named
244 schematic variables of the form @{text ?x}, or nameless dummies
245 ``@{variable _}'' (underscore). Note that in the @{command "let"}
246 form the patterns occur on the left-hand side, while the @{keyword
247 "is"} patterns are in postfix position.
249 Polymorphism of term bindings is handled in Hindley-Milner style,
250 similar to ML. Type variables referring to local assumptions or
251 open goal statements are \emph{fixed}, while those of finished
252 results or bound by @{command "let"} may occur in \emph{arbitrary}
253 instances later. Even though actual polymorphism should be rarely
254 used in practice, this mechanism is essential to achieve proper
255 incremental type-inference, as the user proceeds to build up the
256 Isar proof text from left to right.
258 \medskip Term abbreviations are quite different from local
259 definitions as introduced via @{command "def"} (see
260 \secref{sec:proof-context}). The latter are visible within the
261 logic as actual equations, while abbreviations disappear during the
262 input process just after type checking. Also note that @{command
263 "def"} does not support polymorphism.
266 'let' ((term + 'and') '=' term + 'and')
270 The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
271 or \railnonterm{proppat} (see \secref{sec:term-decls}).
275 \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
276 text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous
277 higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
279 \item @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but
280 matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement. Also
281 note that @{keyword "is"} is not a separate command, but part of
282 others (such as @{command "assume"}, @{command "have"} etc.).
286 Some \emph{implicit} term abbreviations\index{term abbreviations}
287 for goals and facts are available as well. For any open goal,
288 @{variable_ref thesis} refers to its object-level statement,
289 abstracted over any meta-level parameters (if present). Likewise,
290 @{variable_ref this} is bound for fact statements resulting from
291 assumptions or finished goals. In case @{variable this} refers to
292 an object-logic statement that is an application @{text "f t"}, then
293 @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
294 (three dots). The canonical application of this convenience are
295 calculational proofs (see \secref{sec:calculation}).
299 subsection {* Facts and forward chaining *}
302 \begin{matharray}{rcl}
303 @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
304 @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
305 @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
306 @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
307 @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
308 @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
311 New facts are established either by assumption or proof of local
312 statements. Any fact will usually be involved in further proofs,
313 either as explicit arguments of proof methods, or when forward
314 chaining towards the next goal via @{command "then"} (and variants);
315 @{command "from"} and @{command "with"} are composite forms
316 involving @{command "note"}. The @{command "using"} elements
317 augments the collection of used facts \emph{after} a goal has been
318 stated. Note that the special theorem name @{fact_ref this} refers
319 to the most recently established facts, but only \emph{before}
320 issuing a follow-up claim.
323 'note' (thmdef? thmrefs + 'and')
325 ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
331 \item @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
332 @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. Note that
333 attributes may be involved as well, both on the left and right hand
336 \item @{command "then"} indicates forward chaining by the current
337 facts in order to establish the goal to be claimed next. The
338 initial proof method invoked to refine that will be offered the
339 facts to do ``anything appropriate'' (see also
340 \secref{sec:proof-steps}). For example, method @{method_ref rule}
341 (see \secref{sec:pure-meth-att}) would typically do an elimination
342 rather than an introduction. Automatic methods usually insert the
343 facts into the goal state before operation. This provides a simple
344 scheme to control relevance of facts in automated proof search.
346 \item @{command "from"}~@{text b} abbreviates ``@{command
347 "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
348 equivalent to ``@{command "from"}~@{text this}''.
350 \item @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command
351 "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining
352 is from earlier facts together with the current ones.
354 \item @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being
355 currently indicated for use by a subsequent refinement step (such as
356 @{command_ref "apply"} or @{command_ref "proof"}).
358 \item @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally
359 similar to @{command "using"}, but unfolds definitional equations
360 @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.
364 Forward chaining with an empty list of theorems is the same as not
365 chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
366 effect apart from entering @{text "prove(chain)"} mode, since
367 @{fact_ref nothing} is bound to the empty list of theorems.
369 Basic proof methods (such as @{method_ref rule}) expect multiple
370 facts to be given in their proper order, corresponding to a prefix
371 of the premises of the rule involved. Note that positions may be
372 easily skipped using something like @{command "from"}~@{text "_
373 \<AND> a \<AND> b"}, for example. This involves the trivial rule
374 @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
375 ``@{fact_ref "_"}'' (underscore).
377 Automated methods (such as @{method simp} or @{method auto}) just
378 insert any given facts before their usual operation. Depending on
379 the kind of procedure involved, the order of facts is less
384 subsection {* Goals \label{sec:goals} *}
387 \begin{matharray}{rcl}
388 @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
389 @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
390 @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
391 @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
392 @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
393 @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
394 @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
395 @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
396 @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
397 @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
398 @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
401 From a theory context, proof mode is entered by an initial goal
402 command such as @{command "lemma"}, @{command "theorem"}, or
403 @{command "corollary"}. Within a proof, new claims may be
404 introduced locally as well; four variants are available here to
405 indicate whether forward chaining of facts should be performed
406 initially (via @{command_ref "then"}), and whether the final result
407 is meant to solve some pending goal.
409 Goals may consist of multiple statements, resulting in a list of
410 facts eventually. A pending multi-goal is internally represented as
411 a meta-level conjunction (@{text "&&&"}), which is usually
412 split into the corresponding number of sub-goals prior to an initial
413 method application, via @{command_ref "proof"}
414 (\secref{sec:proof-steps}) or @{command_ref "apply"}
415 (\secref{sec:tactic-commands}). The @{method_ref induct} method
416 covered in \secref{sec:cases-induct} acts on multiple claims
419 Claims at the theory level may be either in short or long form. A
420 short goal merely consists of several simultaneous propositions
421 (often just one). A long goal includes an explicit context
422 specification for the subsequent conclusion, involving local
423 parameters and assumptions. Here the role of each part of the
424 statement is explicitly marked by separate keywords (see also
425 \secref{sec:locale}); the local assumptions being introduced here
426 are available as @{fact_ref assms} in the proof. Moreover, there
427 are two kinds of conclusions: @{element_def "shows"} states several
428 simultaneous propositions (essentially a big conjunction), while
429 @{element_def "obtains"} claims several simultaneous simultaneous
430 contexts of (essentially a big disjunction of eliminated parameters
431 and assumptions, cf.\ \secref{sec:obtain}).
434 ('lemma' | 'theorem' | 'corollary' |
435 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
437 ('have' | 'show' | 'hence' | 'thus') goal
439 'print\_statement' modes? thmrefs
442 goal: (props + 'and')
444 longgoal: thmdecl? (contextelem *) conclusion
446 conclusion: 'shows' goal | 'obtains' (parname? case + '|')
448 case: (vars + 'and') 'where' (props + 'and')
454 \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
455 @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
456 \<phi>"} to be put back into the target context. An additional
457 \railnonterm{context} specification may build up an initial proof
458 context for the subsequent claim; this includes local definitions
459 and syntax as well, see the definition of @{syntax contextelem} in
462 \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
463 "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
464 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
465 being of a different kind. This discrimination acts like a formal
468 \item @{command "schematic_lemma"}, @{command "schematic_theorem"},
469 @{command "schematic_corollary"} are similar to @{command "lemma"},
470 @{command "theorem"}, @{command "corollary"}, respectively but allow
471 the statement to contain unbound schematic variables.
473 Under normal circumstances, an Isar proof text needs to specify
474 claims explicitly. Schematic goals are more like goals in Prolog,
475 where certain results are synthesized in the course of reasoning.
476 With schematic statements, the inherent compositionality of Isar
477 proofs is lost, which also impacts performance, because proof
478 checking is forced into sequential mode.
480 \item @{command "have"}~@{text "a: \<phi>"} claims a local goal,
481 eventually resulting in a fact within the current logical context.
482 This operation is completely independent of any pending sub-goals of
483 an enclosing goal statements, so @{command "have"} may be freely
484 used for experimental exploration of potential results within a
487 \item @{command "show"}~@{text "a: \<phi>"} is like @{command
488 "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
489 sub-goal for each one of the finished result, after having been
490 exported into the corresponding context (at the head of the
491 sub-proof of this @{command "show"} command).
493 To accommodate interactive debugging, resulting rules are printed
494 before being applied internally. Even more, interactive execution
495 of @{command "show"} predicts potential failure and displays the
496 resulting error as a warning beforehand. Watch out for the
499 %FIXME proper antiquitation
501 Problem! Local statement will fail to solve any pending goal
504 \item @{command "hence"} abbreviates ``@{command "then"}~@{command
505 "have"}'', i.e.\ claims a local goal to be proven by forward
506 chaining the current facts. Note that @{command "hence"} is also
507 equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
509 \item @{command "thus"} abbreviates ``@{command "then"}~@{command
510 "show"}''. Note that @{command "thus"} is also equivalent to
511 ``@{command "from"}~@{text this}~@{command "show"}''.
513 \item @{command "print_statement"}~@{text a} prints facts from the
514 current theory or proof context in long statement form, according to
515 the syntax for @{command "lemma"} given above.
519 Any goal statement causes some term abbreviations (such as
520 @{variable_ref "?thesis"}) to be bound automatically, see also
521 \secref{sec:term-abbrev}.
523 The optional case names of @{element_ref "obtains"} have a twofold
524 meaning: (1) during the of this claim they refer to the the local
525 context introductions, (2) the resulting rule is annotated
526 accordingly to support symbolic case splits when used with the
527 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
531 section {* Refinement steps *}
533 subsection {* Proof method expressions \label{sec:proof-meth} *}
536 Proof methods are either basic ones, or expressions composed of
537 methods via ``@{verbatim ","}'' (sequential composition),
538 ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
539 (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
540 "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
541 sub-goals, with default @{text "n = 1"}). In practice, proof
542 methods are usually just a comma separated list of
543 \railqtok{nameref}~\railnonterm{args} specifications. Note that
544 parentheses may be dropped for single method specifications (with no
547 \indexouternonterm{method}
549 method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
551 methods: (nameref args | method) + (',' | '|')
555 Proper Isar proof methods do \emph{not} admit arbitrary goal
556 addressing, but refer either to the first sub-goal or all sub-goals
557 uniformly. The goal restriction operator ``@{text "[n]"}''
558 evaluates a method expression within a sandbox consisting of the
559 first @{text n} sub-goals (which need to exist). For example, the
560 method ``@{text "simp_all[3]"}'' simplifies the first three
561 sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
562 new goals that emerge from applying rule @{text "foo"} to the
563 originally first one.
565 Improper methods, notably tactic emulations, offer a separate
566 low-level goal addressing scheme as explicit argument to the
567 individual tactic being involved. Here ``@{text "[!]"}'' refers to
568 all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
571 \indexouternonterm{goalspec}
573 goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
579 subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
582 \begin{matharray}{rcl}
583 @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\
584 @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\
585 @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
586 @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
587 @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
588 @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
591 Arbitrary goal refinement via tactics is considered harmful.
592 Structured proof composition in Isar admits proof methods to be
593 invoked in two places only.
597 \item An \emph{initial} refinement step @{command_ref
598 "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
599 of sub-goals that are to be solved later. Facts are passed to
600 @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
601 "proof(chain)"} mode.
603 \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
604 "m\<^sub>2"} is intended to solve remaining goals. No facts are
605 passed to @{text "m\<^sub>2"}.
609 The only other (proper) way to affect pending goals in a proof body
610 is by @{command_ref "show"}, which involves an explicit statement of
611 what is to be solved eventually. Thus we avoid the fundamental
612 problem of unstructured tactic scripts that consist of numerous
613 consecutive goal transformations, with invisible effects.
615 \medskip As a general rule of thumb for good proof style, initial
616 proof methods should either solve the goal completely, or constitute
617 some well-understood reduction to new sub-goals. Arbitrary
618 automatic proof tools that are prone leave a large number of badly
619 structured sub-goals are no help in continuing the proof document in
620 an intelligible manner.
622 Unless given explicitly by the user, the default initial method is
623 ``@{method_ref rule}'', which applies a single standard elimination
624 or introduction rule according to the topmost symbol involved.
625 There is no separate default terminal method. Any remaining goals
626 are always solved by assumption in the very last step.
635 ('.' | '..' | 'sorry')
641 \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof
642 method @{text "m\<^sub>1"}; facts for forward chaining are passed if so
643 indicated by @{text "proof(chain)"} mode.
645 \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by
646 proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.
647 If the goal had been @{text "show"} (or @{text "thus"}), some
648 pending sub-goal is solved as well by the rule resulting from the
649 result \emph{exported} into the enclosing goal context. Thus @{text
650 "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the
651 resulting rule does not fit to any pending goal\footnote{This
652 includes any additional ``strong'' assumptions as introduced by
653 @{command "assume"}.} of the enclosing context. Debugging such a
654 situation might involve temporarily changing @{command "show"} into
655 @{command "have"}, or weakening the local context by replacing
656 occurrences of @{command "assume"} by @{command "presume"}.
658 \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal
659 proof}\index{proof!terminal}; it abbreviates @{command
660 "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text "m\<^sub>2"}, but with
661 backtracking across both methods. Debugging an unsuccessful
662 @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its
663 definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even
664 @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
667 \item ``@{command ".."}'' is a \emph{default
668 proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
671 \item ``@{command "."}'' is a \emph{trivial
672 proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
675 \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
676 pretending to solve the pending claim without further ado. This
677 only works in interactive development, or if the @{ML
678 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
679 proofs are not the real thing. Internally, each theorem container
680 is tainted by an oracle invocation, which is indicated as ``@{text
681 "[!]"}'' in the printed result.
683 The most important application of @{command "sorry"} is to support
684 experimentation and top-down proof development.
690 subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
693 The following proof methods and attributes refer to basic logical
694 operations of Isar. Further methods and attributes are provided by
695 several generic and object-logic specific tools and packages (see
696 \chref{ch:gen-tools} and \chref{ch:hol}).
698 \begin{matharray}{rcl}
699 @{method_def "-"} & : & @{text method} \\
700 @{method_def "fact"} & : & @{text method} \\
701 @{method_def "assumption"} & : & @{text method} \\
702 @{method_def "this"} & : & @{text method} \\
703 @{method_def "rule"} & : & @{text method} \\
704 @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
705 @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
706 @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
707 @{attribute_def "rule"} & : & @{text attribute} \\[0.5ex]
708 @{attribute_def "OF"} & : & @{text attribute} \\
709 @{attribute_def "of"} & : & @{text attribute} \\
710 @{attribute_def "where"} & : & @{text attribute} \\
718 rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
720 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
726 'of' insts ('concl' ':' insts)?
728 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
734 \item ``@{method "-"}'' (minus) does nothing but insert the forward
735 chaining facts as premises into the goal. Note that command
736 @{command_ref "proof"} without any method actually performs a single
737 reduction step using the @{method_ref rule} method; thus a plain
738 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
739 "-"}'' rather than @{command "proof"} alone.
741 \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
742 @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
743 modulo unification of schematic type and term variables. The rule
744 structure is not taken into account, i.e.\ meta-level implication is
745 considered atomic. This is the same principle underlying literal
746 facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~@{text
747 "\<phi>"}~@{command "by"}~@{text fact}'' is equivalent to ``@{command
748 "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim "`"}'' provided that
749 @{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the
752 \item @{method assumption} solves some goal by a single assumption
753 step. All given facts are guaranteed to participate in the
754 refinement; this means there may be only 0 or 1 in the first place.
755 Recall that @{command "qed"} (\secref{sec:proof-steps}) already
756 concludes any remaining sub-goals by assumption, so structured
757 proofs usually need not quote the @{method assumption} method at
760 \item @{method this} applies all of the current facts directly as
761 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
762 "by"}~@{text this}''.
764 \item @{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
765 argument in backward manner; facts are used to reduce the rule
766 before applying it to the goal. Thus @{method rule} without facts
767 is plain introduction, while with facts it becomes elimination.
769 When no arguments are given, the @{method rule} method tries to pick
770 appropriate rules automatically, as declared in the current context
771 using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
772 @{attribute (Pure) dest} attributes (see below). This is the
773 default behavior of @{command "proof"} and ``@{command ".."}''
774 (double-dot) steps (see \secref{sec:proof-steps}).
776 \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
777 @{attribute (Pure) dest} declare introduction, elimination, and
778 destruct rules, to be used with method @{method rule}, and similar
779 tools. Note that the latter will ignore rules declared with
780 ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
782 The classical reasoner (see \secref{sec:classical}) introduces its
783 own variants of these attributes; use qualified names to access the
784 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
787 \item @{attribute rule}~@{text del} undeclares introduction,
788 elimination, or destruct rules.
790 \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
791 theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
792 (in parallel). This corresponds to the @{ML "op MRS"} operation in
793 ML, but note the reversed order. Positions may be effectively
794 skipped by including ``@{text _}'' (underscore) as argument.
796 \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
797 instantiation of term variables. The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
798 substituted for any schematic variables occurring in a theorem from
799 left to right; ``@{text _}'' (underscore) indicates to skip a
800 position. Arguments following a ``@{text "concl:"}'' specification
801 refer to positions of the conclusion of a rule.
803 \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
804 performs named instantiation of schematic type and term variables
805 occurring in a theorem. Schematic variables have to be specified on
806 the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may
807 be omitted if the variable name is a plain identifier without index.
808 As type instantiations are inferred from term instantiations,
809 explicit type instantiations are seldom necessary.
815 subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
818 The Isar provides separate commands to accommodate tactic-style
819 proof scripts within the same system. While being outside the
820 orthodox Isar proof language, these might come in handy for
821 interactive exploration and debugging, or even actual tactical proof
822 within new-style theories (to benefit from document preparation, for
823 example). See also \secref{sec:tactics} for actual tactics, that
824 have been encapsulated as proof methods. Proper proof methods may
825 be used in scripts, too.
827 \begin{matharray}{rcl}
828 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
829 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
830 @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
831 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
832 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
833 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
837 ( 'apply' | 'apply\_end' ) method
847 \item @{command "apply"}~@{text m} applies proof method @{text m} in
848 initial position, but unlike @{command "proof"} it retains ``@{text
849 "proof(prove)"}'' mode. Thus consecutive method applications may be
850 given just as in tactic scripts.
852 Facts are passed to @{text m} as indicated by the goal's
853 forward-chain mode, and are \emph{consumed} afterwards. Thus any
854 further @{command "apply"} command would always work in a purely
857 \item @{command "apply_end"}~@{text "m"} applies proof method @{text
858 m} as if in terminal position. Basically, this simulates a
859 multi-step tactic script for @{command "qed"}, but may be given
860 anywhere within the proof body.
862 No facts are passed to @{text m} here. Furthermore, the static
863 context is that of the enclosing goal (as for actual @{command
864 "qed"}). Thus the proof method may not refer to any assumptions
865 introduced in the current body, for example.
867 \item @{command "done"} completes a proof script, provided that the
868 current goal state is solved completely. Note that actual
869 structured proof commands (e.g.\ ``@{command "."}'' or @{command
870 "sorry"}) may be used to conclude proof scripts as well.
872 \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
873 shuffle the list of pending goals: @{command "defer"} puts off
874 sub-goal @{text n} to the end of the list (@{text "n = 1"} by
875 default), while @{command "prefer"} brings sub-goal @{text n} to the
878 \item @{command "back"} does back-tracking over the result sequence
879 of the latest proof command. Basically, any proof command may
880 return multiple results.
884 Any proper Isar proof method may be used with tactic script commands
885 such as @{command "apply"}. A few additional emulations of actual
886 tactics are provided as well; these would be never used in actual
887 structured proofs, of course.
891 subsection {* Defining proof methods *}
894 \begin{matharray}{rcl}
895 @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
899 'method\_setup' name '=' text text
905 \item @{command "method_setup"}~@{text "name = text description"}
906 defines a proof method in the current theory. The given @{text
907 "text"} has to be an ML expression of type
908 @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
909 basic parsers defined in structure @{ML_struct Args} and @{ML_struct
910 Attrib}. There are also combinators like @{ML METHOD} and @{ML
911 SIMPLE_METHOD} to turn certain tactic forms into official proof
912 methods; the primed versions refer to tactics with explicit goal
915 Here are some example method definitions:
920 method_setup my_method1 = {*
921 Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
922 *} "my first method (without any arguments)"
924 method_setup my_method2 = {*
925 Scan.succeed (fn ctxt: Proof.context =>
926 SIMPLE_METHOD' (fn i: int => no_tac))
927 *} "my second method (with context)"
929 method_setup my_method3 = {*
930 Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
931 SIMPLE_METHOD' (fn i: int => no_tac))
932 *} "my third method (with theorem arguments and context)"
935 section {* Generalized elimination \label{sec:obtain} *}
938 \begin{matharray}{rcl}
939 @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
940 @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
943 Generalized elimination means that additional elements with certain
944 properties may be introduced in the current context, by virtue of a
945 locally proven ``soundness statement''. Technically speaking, the
946 @{command "obtain"} language element is like a declaration of
947 @{command "fix"} and @{command "assume"} (see also see
948 \secref{sec:proof-context}), together with a soundness proof of its
949 additional claim. According to the nature of existential reasoning,
950 assumptions get eliminated from any result exported from the context
951 later, provided that the corresponding parameters do \emph{not}
952 occur in the conclusion.
955 'obtain' parname? (vars + 'and') 'where' (props + 'and')
957 'guess' (vars + 'and')
961 The derived Isar command @{command "obtain"} is defined as follows
962 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
963 facts indicated for forward chaining).
965 @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex]
966 \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
967 \quad @{command "proof"}~@{method succeed} \\
968 \qquad @{command "fix"}~@{text thesis} \\
969 \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
970 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
971 \quad\qquad @{command "apply"}~@{text -} \\
972 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
973 \quad @{command "qed"} \\
974 \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
977 Typically, the soundness proof is relatively straight-forward, often
978 just by canonical automated tools such as ``@{command "by"}~@{text
979 simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
980 ``@{text that}'' reduction above is declared as simplification and
983 In a sense, @{command "obtain"} represents at the level of Isar
984 proofs what would be meta-logical existential quantifiers and
985 conjunctions. This concept has a broad range of useful
986 applications, ranging from plain elimination (or introduction) of
987 object-level existential and conjunctions, to elimination over
988 results of symbolic evaluation of recursive definitions, for
989 example. Also note that @{command "obtain"} without parameters acts
990 much like @{command "have"}, where the result is treated as a
993 An alternative name to be used instead of ``@{text that}'' above may
994 be given in parentheses.
996 \medskip The improper variant @{command "guess"} is similar to
997 @{command "obtain"}, but derives the obtained statement from the
998 course of reasoning! The proof starts with a fixed goal @{text
999 thesis}. The subsequent proof may refine this to anything of the
1000 form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
1001 \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
1002 final goal state is then used as reduction rule for the obtain
1003 scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
1004 x\<^sub>m"} are marked as internal by default, which prevents the
1005 proof context from being polluted by ad-hoc variables. The variable
1006 names and type constraints given as arguments for @{command "guess"}
1007 specify a prefix of obtained parameters explicitly in the text.
1009 It is important to note that the facts introduced by @{command
1010 "obtain"} and @{command "guess"} may not be polymorphic: any
1011 type-variables occurring here are fixed in the present context!
1015 section {* Calculational reasoning \label{sec:calculation} *}
1018 \begin{matharray}{rcl}
1019 @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1020 @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
1021 @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1022 @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
1023 @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1024 @{attribute trans} & : & @{text attribute} \\
1025 @{attribute sym} & : & @{text attribute} \\
1026 @{attribute symmetric} & : & @{text attribute} \\
1029 Calculational proof is forward reasoning with implicit application
1030 of transitivity rules (such those of @{text "="}, @{text "\<le>"},
1031 @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
1032 @{fact_ref calculation} for accumulating results obtained by
1033 transitivity composed with the current result. Command @{command
1034 "also"} updates @{fact calculation} involving @{fact this}, while
1035 @{command "finally"} exhibits the final @{fact calculation} by
1036 forward chaining towards the next goal statement. Both commands
1037 require valid current facts, i.e.\ may occur only after commands
1038 that produce theorems such as @{command "assume"}, @{command
1039 "note"}, or some finished proof of @{command "have"}, @{command
1040 "show"} etc. The @{command "moreover"} and @{command "ultimately"}
1041 commands are similar to @{command "also"} and @{command "finally"},
1042 but only collect further results in @{fact calculation} without
1043 applying any rules yet.
1045 Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
1046 its canonical application with calculational proofs. It refers to
1047 the argument of the preceding statement. (The argument of a curried
1048 infix expression happens to be its right-hand side.)
1050 Isabelle/Isar calculations are implicitly subject to block structure
1051 in the sense that new threads of calculational reasoning are
1052 commenced for any new block (as opened by a local goal, for
1053 example). This means that, apart from being able to nest
1054 calculations, there is no separate \emph{begin-calculation} command
1057 \medskip The Isar calculation proof commands may be defined as
1058 follows:\footnote{We suppress internal bookkeeping such as proper
1059 handling of block-structure.}
1061 \begin{matharray}{rcl}
1062 @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
1063 @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
1064 @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
1065 @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
1066 @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
1070 ('also' | 'finally') ('(' thmrefs ')')?
1072 'trans' (() | 'add' | 'del')
1078 \item @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary
1079 @{fact calculation} register as follows. The first occurrence of
1080 @{command "also"} in some calculational thread initializes @{fact
1081 calculation} by @{fact this}. Any subsequent @{command "also"} on
1082 the same level of block-structure updates @{fact calculation} by
1083 some transitivity rule applied to @{fact calculation} and @{fact
1084 this} (in that order). Transitivity rules are picked from the
1085 current context, unless alternative rules are given as explicit
1088 \item @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact
1089 calculation} in the same way as @{command "also"}, and concludes the
1090 current calculational thread. The final result is exhibited as fact
1091 for forward chaining towards the next goal. Basically, @{command
1092 "finally"} just abbreviates @{command "also"}~@{command
1093 "from"}~@{fact calculation}. Typical idioms for concluding
1094 calculational proofs are ``@{command "finally"}~@{command
1095 "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
1096 "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
1098 \item @{command "moreover"} and @{command "ultimately"} are
1099 analogous to @{command "also"} and @{command "finally"}, but collect
1100 results only, without applying rules.
1102 \item @{command "print_trans_rules"} prints the list of transitivity
1103 rules (for calculational commands @{command "also"} and @{command
1104 "finally"}) and symmetry rules (for the @{attribute symmetric}
1105 operation and single step elimination patters) of the current
1108 \item @{attribute trans} declares theorems as transitivity rules.
1110 \item @{attribute sym} declares symmetry rules, as well as
1111 @{attribute "Pure.elim"}@{text "?"} rules.
1113 \item @{attribute symmetric} resolves a theorem with some rule
1114 declared as @{attribute sym} in the current context. For example,
1115 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
1116 swapped fact derived from that assumption.
1118 In structured proof texts it is often more appropriate to use an
1119 explicit single-step elimination proof, such as ``@{command
1120 "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
1121 "y = x"}~@{command ".."}''.
1127 section {* Proof by cases and induction \label{sec:cases-induct} *}
1129 subsection {* Rule contexts *}
1132 \begin{matharray}{rcl}
1133 @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1134 @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1135 @{attribute_def case_names} & : & @{text attribute} \\
1136 @{attribute_def case_conclusion} & : & @{text attribute} \\
1137 @{attribute_def params} & : & @{text attribute} \\
1138 @{attribute_def consumes} & : & @{text attribute} \\
1141 The puristic way to build up Isar proof contexts is by explicit
1142 language elements like @{command "fix"}, @{command "assume"},
1143 @{command "let"} (see \secref{sec:proof-context}). This is adequate
1144 for plain natural deduction, but easily becomes unwieldy in concrete
1145 verification tasks, which typically involve big induction rules with
1148 The @{command "case"} command provides a shorthand to refer to a
1149 local context symbolically: certain proof methods provide an
1150 environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
1151 x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
1152 "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
1153 "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
1154 \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably
1155 @{variable ?case} for the main conclusion.
1157 By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
1158 a case value is marked as hidden, i.e.\ there is no way to refer to
1159 such parameters in the subsequent proof text. After all, original
1160 rule parameters stem from somewhere outside of the current proof
1161 text. By using the explicit form ``@{command "case"}~@{text "(c
1162 y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to
1163 chose local names that fit nicely into the current context.
1165 \medskip It is important to note that proper use of @{command
1166 "case"} does not provide means to peek at the current goal state,
1167 which is not directly observable in Isar! Nonetheless, goal
1168 refinement commands do provide named cases @{text "goal\<^sub>i"}
1169 for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.
1170 Using this extra feature requires great care, because some bits of
1171 the internal tactical machinery intrude the proof text. In
1172 particular, parameter names stemming from the left-over of automated
1173 reasoning tools are usually quite unpredictable.
1175 Under normal circumstances, the text of cases emerge from standard
1176 elimination or induction rules, which in turn are derived from
1177 previous theory specifications in a canonical way (say from
1178 @{command "inductive"} definitions).
1180 \medskip Proper cases are only available if both the proof method
1181 and the rules involved support this. By using appropriate
1182 attributes, case names, conclusions, and parameters may be also
1183 declared by hand. Thus variant versions of rules that have been
1184 derived manually become ready to use in advanced case analysis
1188 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1190 caseref: nameref attributes?
1193 'case\_names' (name +)
1195 'case\_conclusion' name (name *)
1197 'params' ((name *) + 'and')
1205 \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
1206 context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
1207 appropriate proof method (such as @{method_ref cases} and
1208 @{method_ref induct}). The command ``@{command "case"}~@{text "(c
1209 x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
1210 x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.
1212 \item @{command "print_cases"} prints all local contexts of the
1213 current state, using Isar proof language notation.
1215 \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
1216 the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
1217 refers to the \emph{suffix} of the list of premises.
1219 \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
1220 names for the conclusions of a named premise @{text c}; here @{text
1221 "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula
1222 built by nesting a binary connective (e.g.\ @{text "\<or>"}).
1224 Note that proof methods such as @{method induct} and @{method
1225 coinduct} already provide a default name for the conclusion as a
1226 whole. The need to name subformulas only arises with cases that
1227 split into several sub-cases, as in common co-induction rules.
1229 \item @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames
1230 the innermost parameters of premises @{text "1, \<dots>, n"} of some
1231 theorem. An empty list of names may be given to skip positions,
1232 leaving the present parameters unchanged.
1234 Note that the default usage of case rules does \emph{not} directly
1235 expose parameters to the proof context.
1237 \item @{attribute consumes}~@{text n} declares the number of ``major
1238 premises'' of a rule, i.e.\ the number of facts to be consumed when
1239 it is applied by an appropriate proof method. The default value of
1240 @{attribute consumes} is @{text "n = 1"}, which is appropriate for
1241 the usual kind of cases and induction rules for inductive sets (cf.\
1242 \secref{sec:hol-inductive}). Rules without any @{attribute
1243 consumes} declaration given are treated as if @{attribute
1244 consumes}~@{text 0} had been specified.
1246 Note that explicit @{attribute consumes} declarations are only
1247 rarely needed; this is already taken care of automatically by the
1248 higher-level @{attribute cases}, @{attribute induct}, and
1249 @{attribute coinduct} declarations.
1255 subsection {* Proof methods *}
1258 \begin{matharray}{rcl}
1259 @{method_def cases} & : & @{text method} \\
1260 @{method_def induct} & : & @{text method} \\
1261 @{method_def coinduct} & : & @{text method} \\
1264 The @{method cases}, @{method induct}, and @{method coinduct}
1265 methods provide a uniform interface to common proof techniques over
1266 datatypes, inductive predicates (or sets), recursive functions etc.
1267 The corresponding rules may be specified and instantiated in a
1268 casual manner. Furthermore, these methods provide named local
1269 contexts that may be invoked via the @{command "case"} proof command
1270 within the subsequent proof text. This accommodates compact proof
1271 texts even when reasoning about large specifications.
1273 The @{method induct} method also provides some additional
1274 infrastructure in order to be applicable to structure statements
1275 (either using explicit meta-level connectives, or including facts
1276 and parameters separately). This avoids cumbersome encoding of
1277 ``strengthened'' inductive statements within the object-logic.
1280 'cases' '(no_simp)'? (insts * 'and') rule?
1282 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
1284 'coinduct' insts taking rule?
1287 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
1289 definst: name ('==' | equiv) term | '(' term ')' | inst
1291 definsts: ( definst *)
1293 arbitrary: 'arbitrary' ':' ((term *) 'and' +)
1295 taking: 'taking' ':' insts
1301 \item @{method cases}~@{text "insts R"} applies method @{method
1302 rule} with an appropriate case distinction theorem, instantiated to
1303 the subjects @{text insts}. Symbolic case names are bound according
1304 to the rule's local contexts.
1306 The rule is determined as follows, according to the facts and
1307 arguments passed to the @{method cases} method:
1310 \begin{tabular}{llll}
1311 facts & & arguments & rule \\\hline
1312 & @{method cases} & & classical case split \\
1313 & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
1314 @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
1315 @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1319 Several instantiations may be given, referring to the \emph{suffix}
1320 of premises of the case rule; within each premise, the \emph{prefix}
1321 of variables is instantiated. In most situations, only a single
1322 term needs to be specified; this refers to the first variable of the
1323 last premise (it is usually the same for all cases).
1324 The \texttt{no\_simp} option can be used to disable pre-simplification
1325 of cases (see the description of @{method induct} below for details).
1327 \item @{method induct}~@{text "insts R"} is analogous to the
1328 @{method cases} method, but refers to induction rules, which are
1329 determined as follows:
1332 \begin{tabular}{llll}
1333 facts & & arguments & rule \\\hline
1334 & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\
1335 @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
1336 @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1340 Several instantiations may be given, each referring to some part of
1341 a mutual inductive definition or datatype --- only related partial
1342 induction rules may be used together, though. Any of the lists of
1343 terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables
1344 present in the induction rule. This enables the writer to specify
1345 only induction variables, or both predicates and variables, for
1348 Instantiations may be definitional: equations @{text "x \<equiv> t"}
1349 introduce local definitions, which are inserted into the claim and
1350 discharged after applying the induction rule. Equalities reappear
1351 in the inductive cases, but have been transformed according to the
1352 induction principle being involved here. In order to achieve
1353 practically useful induction hypotheses, some variables occurring in
1354 @{text t} need to be fixed (see below).
1355 Instantiations of the form @{text t}, where @{text t} is not a variable,
1356 are taken as a shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is
1357 a fresh variable. If this is not intended, @{text t} has to be enclosed in
1359 By default, the equalities generated by definitional instantiations
1360 are pre-simplified using a specific set of rules, usually consisting
1361 of distinctness and injectivity theorems for datatypes. This pre-simplification
1362 may cause some of the parameters of an inductive case to disappear,
1363 or may even completely delete some of the inductive cases, if one of
1364 the equalities occurring in their premises can be simplified to @{text False}.
1365 The \texttt{no\_simp} option can be used to disable pre-simplification.
1366 Additional rules to be used in pre-simplification can be declared using the
1367 \texttt{induct\_simp} attribute.
1369 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
1370 specification generalizes variables @{text "x\<^sub>1, \<dots>,
1371 x\<^sub>m"} of the original goal before applying induction. Thus
1372 induction hypotheses may become sufficiently general to get the
1373 proof through. Together with definitional instantiations, one may
1374 effectively perform induction over expressions of a certain
1377 The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1378 specification provides additional instantiations of a prefix of
1379 pending variables in the rule. Such schematic induction rules
1380 rarely occur in practice, though.
1382 \item @{method coinduct}~@{text "inst R"} is analogous to the
1383 @{method induct} method, but refers to coinduction rules, which are
1384 determined as follows:
1387 \begin{tabular}{llll}
1388 goal & & arguments & rule \\\hline
1389 & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
1390 @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
1391 @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1394 Coinduction is the dual of induction. Induction essentially
1395 eliminates @{text "A x"} towards a generic result @{text "P x"},
1396 while coinduction introduces @{text "A x"} starting with @{text "B
1397 x"}, for a suitable ``bisimulation'' @{text B}. The cases of a
1398 coinduct rule are typically named after the predicates or sets being
1399 covered, while the conclusions consist of several alternatives being
1400 named after the individual destructor patterns.
1402 The given instantiation refers to the \emph{suffix} of variables
1403 occurring in the rule's major premise, or conclusion if unavailable.
1404 An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1405 specification may be required in order to specify the bisimulation
1406 to be used in the coinduction step.
1410 Above methods produce named local contexts, as determined by the
1411 instantiated rule as given in the text. Beyond that, the @{method
1412 induct} and @{method coinduct} methods guess further instantiations
1413 from the goal specification itself. Any persisting unresolved
1414 schematic variables of the resulting rule will render the the
1415 corresponding case invalid. The term binding @{variable ?case} for
1416 the conclusion will be provided with each case, provided that term
1419 The @{command "print_cases"} command prints all named cases present
1420 in the current proof state.
1422 \medskip Despite the additional infrastructure, both @{method cases}
1423 and @{method coinduct} merely apply a certain rule, after
1424 instantiation, while conforming due to the usual way of monotonic
1425 natural deduction: the context of a structured statement @{text
1426 "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}
1427 reappears unchanged after the case split.
1429 The @{method induct} method is fundamentally different in this
1430 respect: the meta-level structure is passed through the
1431 ``recursive'' course involved in the induction. Thus the original
1432 statement is basically replaced by separate copies, corresponding to
1433 the induction hypotheses and conclusion; the original goal context
1434 is no longer available. Thus local assumptions, fixed parameters
1435 and definitions effectively participate in the inductive rephrasing
1436 of the original statement.
1438 In induction proofs, local assumptions introduced by cases are split
1439 into two different kinds: @{text hyps} stemming from the rule and
1440 @{text prems} from the goal statement. This is reflected in the
1441 extracted cases accordingly, so invoking ``@{command "case"}~@{text
1442 c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
1443 as well as fact @{text c} to hold the all-inclusive list.
1445 \medskip Facts presented to either method are consumed according to
1446 the number of ``major premises'' of the rule involved, which is
1447 usually 0 for plain cases and induction rules of datatypes etc.\ and
1448 1 for rules of inductive predicates or sets and the like. The
1449 remaining facts are inserted into the goal verbatim before the
1450 actual @{text cases}, @{text induct}, or @{text coinduct} rule is
1455 subsection {* Declaring rules *}
1458 \begin{matharray}{rcl}
1459 @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1460 @{attribute_def cases} & : & @{text attribute} \\
1461 @{attribute_def induct} & : & @{text attribute} \\
1462 @{attribute_def coinduct} & : & @{text attribute} \\
1473 spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
1479 \item @{command "print_induct_rules"} prints cases and induct rules
1480 for predicates (or sets) and types of the current context.
1482 \item @{attribute cases}, @{attribute induct}, and @{attribute
1483 coinduct} (as attributes) declare rules for reasoning about
1484 (co)inductive predicates (or sets) and types, using the
1485 corresponding methods of the same name. Certain definitional
1486 packages of object-logics usually declare emerging cases and
1487 induction rules as expected, so users rarely need to intervene.
1489 Rules may be deleted via the @{text "del"} specification, which
1490 covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
1491 sub-categories simultaneously. For example, @{attribute
1492 cases}~@{text del} removes any @{attribute cases} rules declared for
1493 some type, predicate, or set.
1495 Manual rule declarations usually refer to the @{attribute
1496 case_names} and @{attribute params} attributes to adjust names of
1497 cases and parameters of a rule; the @{attribute consumes}
1498 declaration is taken care of automatically: @{attribute
1499 consumes}~@{text 0} is specified for ``type'' rules and @{attribute
1500 consumes}~@{text 1} for ``predicate'' / ``set'' rules.