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 {* Blocks *}
52 \begin{matharray}{rcl}
53 @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
54 @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
55 @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
58 While Isar is inherently block-structured, opening and closing
59 blocks is mostly handled rather casually, with little explicit
60 user-intervention. Any local goal statement automatically opens
61 \emph{two} internal blocks, which are closed again when concluding
62 the sub-proof (by @{command "qed"} etc.). Sections of different
63 context within a sub-proof may be switched via @{command "next"},
64 which is just a single block-close followed by block-open again.
65 The effect of @{command "next"} is to reset the local proof context;
66 there is no goal focus involved here!
68 For slightly more advanced applications, there are explicit block
69 parentheses as well. These typically achieve a stronger forward
74 \item @{command "next"} switches to a fresh block within a
75 sub-proof, resetting the local context to the initial one.
77 \item @{command "{"} and @{command "}"} explicitly open and close
78 blocks. Any current facts pass through ``@{command "{"}''
79 unchanged, while ``@{command "}"}'' causes any result to be
80 \emph{exported} into the enclosing context. Thus fixed variables
81 are generalized, assumptions discharged, and local definitions
82 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
83 of @{command "assume"} and @{command "presume"} in this mode of
84 forward reasoning --- in contrast to plain backward reasoning with
85 the result exported at @{command "show"} time.
91 subsection {* Omitting proofs *}
94 \begin{matharray}{rcl}
95 @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\
98 The @{command "oops"} command discontinues the current proof
99 attempt, while considering the partial proof text as properly
100 processed. This is conceptually quite different from ``faking''
101 actual proofs via @{command_ref "sorry"} (see
102 \secref{sec:proof-steps}): @{command "oops"} does not observe the
103 proof structure at all, but goes back right to the theory level.
104 Furthermore, @{command "oops"} does not produce any result theorem
105 --- there is no intended claim to be able to complete the proof
108 A typical application of @{command "oops"} is to explain Isar proofs
109 \emph{within} the system itself, in conjunction with the document
110 preparation tools of Isabelle described in \chref{ch:document-prep}.
111 Thus partial or even wrong proof attempts can be discussed in a
112 logically sound manner. Note that the Isabelle {\LaTeX} macros can
113 be easily adapted to print something like ``@{text "\<dots>"}'' instead of
114 the keyword ``@{command "oops"}''.
116 \medskip The @{command "oops"} command is undo-able, unlike
117 @{command_ref "kill"} (see \secref{sec:history}). The effect is to
118 get back to the theory just before the opening of the proof.
122 section {* Statements *}
124 subsection {* Context elements \label{sec:proof-context} *}
127 \begin{matharray}{rcl}
128 @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
129 @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
130 @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
131 @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
134 The logical proof context consists of fixed variables and
135 assumptions. The former closely correspond to Skolem constants, or
136 meta-level universal quantification as provided by the Isabelle/Pure
137 logical framework. Introducing some \emph{arbitrary, but fixed}
138 variable via ``@{command "fix"}~@{text x}'' results in a local value
139 that may be used in the subsequent proof as any other variable or
140 constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
141 the context will be universally closed wrt.\ @{text x} at the
142 outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
143 form using Isabelle's meta-variables).
145 Similarly, introducing some assumption @{text \<chi>} has two effects.
146 On the one hand, a local theorem is created that may be used as a
147 fact in subsequent proof steps. On the other hand, any result
148 @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
149 the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
150 using such a result would basically introduce a new subgoal stemming
151 from the assumption. How this situation is handled depends on the
152 version of assumption command used: while @{command "assume"}
153 insists on solving the subgoal by unification with some premise of
154 the goal, @{command "presume"} leaves the subgoal unchanged in order
155 to be proved later by the user.
157 Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
158 t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
159 another version of assumption that causes any hypothetical equation
160 @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
161 exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
167 ('assume' | 'presume') (props + 'and')
171 def: thmdecl? \\ name ('==' | equiv) term termpat?
177 \item @{command "fix"}~@{text x} introduces a local variable @{text
178 x} that is \emph{arbitrary, but fixed.}
180 \item @{command "assume"}~@{text "a: \<phi>"} and @{command
181 "presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
182 assumption. Subsequent results applied to an enclosing goal (e.g.\
183 by @{command_ref "show"}) are handled as follows: @{command
184 "assume"} expects to be able to unify with existing premises in the
185 goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
187 Several lists of assumptions may be given (separated by
188 @{keyword_ref "and"}; the resulting list of current facts consists
189 of all of these concatenated.
191 \item @{command "def"}~@{text "x \<equiv> t"} introduces a local
192 (non-polymorphic) definition. In results exported from the context,
193 @{text x} is replaced by @{text t}. Basically, ``@{command
194 "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
195 x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
196 hypothetical equation solved by reflexivity.
198 The default name for the definitional equation is @{text x_def}.
199 Several simultaneous definitions may be given at the same time.
203 The special name @{fact_ref prems} refers to all assumptions of the
204 current context as a list of theorems. This feature should be used
205 with great care! It is better avoided in final proof texts.
209 subsection {* Term abbreviations \label{sec:term-abbrev} *}
212 \begin{matharray}{rcl}
213 @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
214 @{keyword_def "is"} & : & syntax \\
217 Abbreviations may be either bound by explicit @{command
218 "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
219 goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
220 p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
221 bind extra-logical term variables, which may be either named
222 schematic variables of the form @{text ?x}, or nameless dummies
223 ``@{variable _}'' (underscore). Note that in the @{command "let"}
224 form the patterns occur on the left-hand side, while the @{keyword
225 "is"} patterns are in postfix position.
227 Polymorphism of term bindings is handled in Hindley-Milner style,
228 similar to ML. Type variables referring to local assumptions or
229 open goal statements are \emph{fixed}, while those of finished
230 results or bound by @{command "let"} may occur in \emph{arbitrary}
231 instances later. Even though actual polymorphism should be rarely
232 used in practice, this mechanism is essential to achieve proper
233 incremental type-inference, as the user proceeds to build up the
234 Isar proof text from left to right.
236 \medskip Term abbreviations are quite different from local
237 definitions as introduced via @{command "def"} (see
238 \secref{sec:proof-context}). The latter are visible within the
239 logic as actual equations, while abbreviations disappear during the
240 input process just after type checking. Also note that @{command
241 "def"} does not support polymorphism.
244 'let' ((term + 'and') '=' term + 'and')
248 The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
249 or \railnonterm{proppat} (see \secref{sec:term-decls}).
253 \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
254 text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous
255 higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
257 \item @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but
258 matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement. Also
259 note that @{keyword "is"} is not a separate command, but part of
260 others (such as @{command "assume"}, @{command "have"} etc.).
264 Some \emph{implicit} term abbreviations\index{term abbreviations}
265 for goals and facts are available as well. For any open goal,
266 @{variable_ref thesis} refers to its object-level statement,
267 abstracted over any meta-level parameters (if present). Likewise,
268 @{variable_ref this} is bound for fact statements resulting from
269 assumptions or finished goals. In case @{variable this} refers to
270 an object-logic statement that is an application @{text "f t"}, then
271 @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
272 (three dots). The canonical application of this convenience are
273 calculational proofs (see \secref{sec:calculation}).
277 subsection {* Facts and forward chaining *}
280 \begin{matharray}{rcl}
281 @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
282 @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
283 @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
284 @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
285 @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
286 @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
289 New facts are established either by assumption or proof of local
290 statements. Any fact will usually be involved in further proofs,
291 either as explicit arguments of proof methods, or when forward
292 chaining towards the next goal via @{command "then"} (and variants);
293 @{command "from"} and @{command "with"} are composite forms
294 involving @{command "note"}. The @{command "using"} elements
295 augments the collection of used facts \emph{after} a goal has been
296 stated. Note that the special theorem name @{fact_ref this} refers
297 to the most recently established facts, but only \emph{before}
298 issuing a follow-up claim.
301 'note' (thmdef? thmrefs + 'and')
303 ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
309 \item @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
310 @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. Note that
311 attributes may be involved as well, both on the left and right hand
314 \item @{command "then"} indicates forward chaining by the current
315 facts in order to establish the goal to be claimed next. The
316 initial proof method invoked to refine that will be offered the
317 facts to do ``anything appropriate'' (see also
318 \secref{sec:proof-steps}). For example, method @{method_ref rule}
319 (see \secref{sec:pure-meth-att}) would typically do an elimination
320 rather than an introduction. Automatic methods usually insert the
321 facts into the goal state before operation. This provides a simple
322 scheme to control relevance of facts in automated proof search.
324 \item @{command "from"}~@{text b} abbreviates ``@{command
325 "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
326 equivalent to ``@{command "from"}~@{text this}''.
328 \item @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command
329 "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining
330 is from earlier facts together with the current ones.
332 \item @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being
333 currently indicated for use by a subsequent refinement step (such as
334 @{command_ref "apply"} or @{command_ref "proof"}).
336 \item @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally
337 similar to @{command "using"}, but unfolds definitional equations
338 @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.
342 Forward chaining with an empty list of theorems is the same as not
343 chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
344 effect apart from entering @{text "prove(chain)"} mode, since
345 @{fact_ref nothing} is bound to the empty list of theorems.
347 Basic proof methods (such as @{method_ref rule}) expect multiple
348 facts to be given in their proper order, corresponding to a prefix
349 of the premises of the rule involved. Note that positions may be
350 easily skipped using something like @{command "from"}~@{text "_
351 \<AND> a \<AND> b"}, for example. This involves the trivial rule
352 @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
353 ``@{fact_ref "_"}'' (underscore).
355 Automated methods (such as @{method simp} or @{method auto}) just
356 insert any given facts before their usual operation. Depending on
357 the kind of procedure involved, the order of facts is less
362 subsection {* Goals \label{sec:goals} *}
365 \begin{matharray}{rcl}
366 @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
367 @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
368 @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
369 @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
370 @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
371 @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
372 @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
373 @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
376 From a theory context, proof mode is entered by an initial goal
377 command such as @{command "lemma"}, @{command "theorem"}, or
378 @{command "corollary"}. Within a proof, new claims may be
379 introduced locally as well; four variants are available here to
380 indicate whether forward chaining of facts should be performed
381 initially (via @{command_ref "then"}), and whether the final result
382 is meant to solve some pending goal.
384 Goals may consist of multiple statements, resulting in a list of
385 facts eventually. A pending multi-goal is internally represented as
386 a meta-level conjunction (@{text "&&&"}), which is usually
387 split into the corresponding number of sub-goals prior to an initial
388 method application, via @{command_ref "proof"}
389 (\secref{sec:proof-steps}) or @{command_ref "apply"}
390 (\secref{sec:tactic-commands}). The @{method_ref induct} method
391 covered in \secref{sec:cases-induct} acts on multiple claims
394 Claims at the theory level may be either in short or long form. A
395 short goal merely consists of several simultaneous propositions
396 (often just one). A long goal includes an explicit context
397 specification for the subsequent conclusion, involving local
398 parameters and assumptions. Here the role of each part of the
399 statement is explicitly marked by separate keywords (see also
400 \secref{sec:locale}); the local assumptions being introduced here
401 are available as @{fact_ref assms} in the proof. Moreover, there
402 are two kinds of conclusions: @{element_def "shows"} states several
403 simultaneous propositions (essentially a big conjunction), while
404 @{element_def "obtains"} claims several simultaneous simultaneous
405 contexts of (essentially a big disjunction of eliminated parameters
406 and assumptions, cf.\ \secref{sec:obtain}).
409 ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
411 ('have' | 'show' | 'hence' | 'thus') goal
413 'print\_statement' modes? thmrefs
416 goal: (props + 'and')
418 longgoal: thmdecl? (contextelem *) conclusion
420 conclusion: 'shows' goal | 'obtains' (parname? case + '|')
422 case: (vars + 'and') 'where' (props + 'and')
428 \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
429 @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
430 \<phi>"} to be put back into the target context. An additional
431 \railnonterm{context} specification may build up an initial proof
432 context for the subsequent claim; this includes local definitions
433 and syntax as well, see the definition of @{syntax contextelem} in
436 \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
437 "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
438 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
439 being of a different kind. This discrimination acts like a formal
442 \item @{command "have"}~@{text "a: \<phi>"} claims a local goal,
443 eventually resulting in a fact within the current logical context.
444 This operation is completely independent of any pending sub-goals of
445 an enclosing goal statements, so @{command "have"} may be freely
446 used for experimental exploration of potential results within a
449 \item @{command "show"}~@{text "a: \<phi>"} is like @{command
450 "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
451 sub-goal for each one of the finished result, after having been
452 exported into the corresponding context (at the head of the
453 sub-proof of this @{command "show"} command).
455 To accommodate interactive debugging, resulting rules are printed
456 before being applied internally. Even more, interactive execution
457 of @{command "show"} predicts potential failure and displays the
458 resulting error as a warning beforehand. Watch out for the
461 %FIXME proper antiquitation
463 Problem! Local statement will fail to solve any pending goal
466 \item @{command "hence"} abbreviates ``@{command "then"}~@{command
467 "have"}'', i.e.\ claims a local goal to be proven by forward
468 chaining the current facts. Note that @{command "hence"} is also
469 equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
471 \item @{command "thus"} abbreviates ``@{command "then"}~@{command
472 "show"}''. Note that @{command "thus"} is also equivalent to
473 ``@{command "from"}~@{text this}~@{command "show"}''.
475 \item @{command "print_statement"}~@{text a} prints facts from the
476 current theory or proof context in long statement form, according to
477 the syntax for @{command "lemma"} given above.
481 Any goal statement causes some term abbreviations (such as
482 @{variable_ref "?thesis"}) to be bound automatically, see also
483 \secref{sec:term-abbrev}.
485 The optional case names of @{element_ref "obtains"} have a twofold
486 meaning: (1) during the of this claim they refer to the the local
487 context introductions, (2) the resulting rule is annotated
488 accordingly to support symbolic case splits when used with the
489 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
494 Isabelle/Isar suffers theory-level goal statements to contain
495 \emph{unbound schematic variables}, although this does not conform
496 to the aim of human-readable proof documents! The main problem
497 with schematic goals is that the actual outcome is usually hard to
498 predict, depending on the behavior of the proof methods applied
499 during the course of reasoning. Note that most semi-automated
500 methods heavily depend on several kinds of implicit rule
501 declarations within the current theory context. As this would
502 also result in non-compositional checking of sub-proofs,
503 \emph{local goals} are not allowed to be schematic at all.
504 Nevertheless, schematic goals do have their use in Prolog-style
505 interactive synthesis of proven results, usually by stepwise
506 refinement via emulation of traditional Isabelle tactic scripts
507 (see also \secref{sec:tactic-commands}). In any case, users
508 should know what they are doing.
513 section {* Refinement steps *}
515 subsection {* Proof method expressions \label{sec:proof-meth} *}
518 Proof methods are either basic ones, or expressions composed of
519 methods via ``@{verbatim ","}'' (sequential composition),
520 ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
521 (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
522 "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
523 sub-goals, with default @{text "n = 1"}). In practice, proof
524 methods are usually just a comma separated list of
525 \railqtok{nameref}~\railnonterm{args} specifications. Note that
526 parentheses may be dropped for single method specifications (with no
529 \indexouternonterm{method}
531 method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
533 methods: (nameref args | method) + (',' | '|')
537 Proper Isar proof methods do \emph{not} admit arbitrary goal
538 addressing, but refer either to the first sub-goal or all sub-goals
539 uniformly. The goal restriction operator ``@{text "[n]"}''
540 evaluates a method expression within a sandbox consisting of the
541 first @{text n} sub-goals (which need to exist). For example, the
542 method ``@{text "simp_all[3]"}'' simplifies the first three
543 sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
544 new goals that emerge from applying rule @{text "foo"} to the
545 originally first one.
547 Improper methods, notably tactic emulations, offer a separate
548 low-level goal addressing scheme as explicit argument to the
549 individual tactic being involved. Here ``@{text "[!]"}'' refers to
550 all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
553 \indexouternonterm{goalspec}
555 goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
561 subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
564 \begin{matharray}{rcl}
565 @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\
566 @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\
567 @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
568 @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
569 @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
570 @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
573 Arbitrary goal refinement via tactics is considered harmful.
574 Structured proof composition in Isar admits proof methods to be
575 invoked in two places only.
579 \item An \emph{initial} refinement step @{command_ref
580 "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
581 of sub-goals that are to be solved later. Facts are passed to
582 @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
583 "proof(chain)"} mode.
585 \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
586 "m\<^sub>2"} is intended to solve remaining goals. No facts are
587 passed to @{text "m\<^sub>2"}.
591 The only other (proper) way to affect pending goals in a proof body
592 is by @{command_ref "show"}, which involves an explicit statement of
593 what is to be solved eventually. Thus we avoid the fundamental
594 problem of unstructured tactic scripts that consist of numerous
595 consecutive goal transformations, with invisible effects.
597 \medskip As a general rule of thumb for good proof style, initial
598 proof methods should either solve the goal completely, or constitute
599 some well-understood reduction to new sub-goals. Arbitrary
600 automatic proof tools that are prone leave a large number of badly
601 structured sub-goals are no help in continuing the proof document in
602 an intelligible manner.
604 Unless given explicitly by the user, the default initial method is
605 ``@{method_ref rule}'', which applies a single standard elimination
606 or introduction rule according to the topmost symbol involved.
607 There is no separate default terminal method. Any remaining goals
608 are always solved by assumption in the very last step.
617 ('.' | '..' | 'sorry')
623 \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof
624 method @{text "m\<^sub>1"}; facts for forward chaining are passed if so
625 indicated by @{text "proof(chain)"} mode.
627 \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by
628 proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.
629 If the goal had been @{text "show"} (or @{text "thus"}), some
630 pending sub-goal is solved as well by the rule resulting from the
631 result \emph{exported} into the enclosing goal context. Thus @{text
632 "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the
633 resulting rule does not fit to any pending goal\footnote{This
634 includes any additional ``strong'' assumptions as introduced by
635 @{command "assume"}.} of the enclosing context. Debugging such a
636 situation might involve temporarily changing @{command "show"} into
637 @{command "have"}, or weakening the local context by replacing
638 occurrences of @{command "assume"} by @{command "presume"}.
640 \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal
641 proof}\index{proof!terminal}; it abbreviates @{command
642 "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text "m\<^sub>2"}, but with
643 backtracking across both methods. Debugging an unsuccessful
644 @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its
645 definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even
646 @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
649 \item ``@{command ".."}'' is a \emph{default
650 proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
653 \item ``@{command "."}'' is a \emph{trivial
654 proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
657 \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
658 pretending to solve the pending claim without further ado. This
659 only works in interactive development, or if the @{ML
660 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
661 proofs are not the real thing. Internally, each theorem container
662 is tainted by an oracle invocation, which is indicated as ``@{text
663 "[!]"}'' in the printed result.
665 The most important application of @{command "sorry"} is to support
666 experimentation and top-down proof development.
672 subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
675 The following proof methods and attributes refer to basic logical
676 operations of Isar. Further methods and attributes are provided by
677 several generic and object-logic specific tools and packages (see
678 \chref{ch:gen-tools} and \chref{ch:hol}).
680 \begin{matharray}{rcl}
681 @{method_def "-"} & : & @{text method} \\
682 @{method_def "fact"} & : & @{text method} \\
683 @{method_def "assumption"} & : & @{text method} \\
684 @{method_def "this"} & : & @{text method} \\
685 @{method_def "rule"} & : & @{text method} \\
686 @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
687 @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
688 @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
689 @{attribute_def "rule"} & : & @{text attribute} \\[0.5ex]
690 @{attribute_def "OF"} & : & @{text attribute} \\
691 @{attribute_def "of"} & : & @{text attribute} \\
692 @{attribute_def "where"} & : & @{text attribute} \\
700 rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
702 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
708 'of' insts ('concl' ':' insts)?
710 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
716 \item ``@{method "-"}'' (minus) does nothing but insert the forward
717 chaining facts as premises into the goal. Note that command
718 @{command_ref "proof"} without any method actually performs a single
719 reduction step using the @{method_ref rule} method; thus a plain
720 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
721 "-"}'' rather than @{command "proof"} alone.
723 \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
724 @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
725 modulo unification of schematic type and term variables. The rule
726 structure is not taken into account, i.e.\ meta-level implication is
727 considered atomic. This is the same principle underlying literal
728 facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~@{text
729 "\<phi>"}~@{command "by"}~@{text fact}'' is equivalent to ``@{command
730 "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim "`"}'' provided that
731 @{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the
734 \item @{method assumption} solves some goal by a single assumption
735 step. All given facts are guaranteed to participate in the
736 refinement; this means there may be only 0 or 1 in the first place.
737 Recall that @{command "qed"} (\secref{sec:proof-steps}) already
738 concludes any remaining sub-goals by assumption, so structured
739 proofs usually need not quote the @{method assumption} method at
742 \item @{method this} applies all of the current facts directly as
743 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
744 "by"}~@{text this}''.
746 \item @{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
747 argument in backward manner; facts are used to reduce the rule
748 before applying it to the goal. Thus @{method rule} without facts
749 is plain introduction, while with facts it becomes elimination.
751 When no arguments are given, the @{method rule} method tries to pick
752 appropriate rules automatically, as declared in the current context
753 using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
754 @{attribute (Pure) dest} attributes (see below). This is the
755 default behavior of @{command "proof"} and ``@{command ".."}''
756 (double-dot) steps (see \secref{sec:proof-steps}).
758 \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
759 @{attribute (Pure) dest} declare introduction, elimination, and
760 destruct rules, to be used with method @{method rule}, and similar
761 tools. Note that the latter will ignore rules declared with
762 ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
764 The classical reasoner (see \secref{sec:classical}) introduces its
765 own variants of these attributes; use qualified names to access the
766 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
769 \item @{attribute rule}~@{text del} undeclares introduction,
770 elimination, or destruct rules.
772 \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
773 theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
774 (in parallel). This corresponds to the @{ML "op MRS"} operation in
775 ML, but note the reversed order. Positions may be effectively
776 skipped by including ``@{text _}'' (underscore) as argument.
778 \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
779 instantiation of term variables. The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
780 substituted for any schematic variables occurring in a theorem from
781 left to right; ``@{text _}'' (underscore) indicates to skip a
782 position. Arguments following a ``@{text "concl:"}'' specification
783 refer to positions of the conclusion of a rule.
785 \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
786 performs named instantiation of schematic type and term variables
787 occurring in a theorem. Schematic variables have to be specified on
788 the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may
789 be omitted if the variable name is a plain identifier without index.
790 As type instantiations are inferred from term instantiations,
791 explicit type instantiations are seldom necessary.
797 subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
800 The Isar provides separate commands to accommodate tactic-style
801 proof scripts within the same system. While being outside the
802 orthodox Isar proof language, these might come in handy for
803 interactive exploration and debugging, or even actual tactical proof
804 within new-style theories (to benefit from document preparation, for
805 example). See also \secref{sec:tactics} for actual tactics, that
806 have been encapsulated as proof methods. Proper proof methods may
807 be used in scripts, too.
809 \begin{matharray}{rcl}
810 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
811 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
812 @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
813 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
814 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
815 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
819 ( 'apply' | 'apply\_end' ) method
829 \item @{command "apply"}~@{text m} applies proof method @{text m} in
830 initial position, but unlike @{command "proof"} it retains ``@{text
831 "proof(prove)"}'' mode. Thus consecutive method applications may be
832 given just as in tactic scripts.
834 Facts are passed to @{text m} as indicated by the goal's
835 forward-chain mode, and are \emph{consumed} afterwards. Thus any
836 further @{command "apply"} command would always work in a purely
839 \item @{command "apply_end"}~@{text "m"} applies proof method @{text
840 m} as if in terminal position. Basically, this simulates a
841 multi-step tactic script for @{command "qed"}, but may be given
842 anywhere within the proof body.
844 No facts are passed to @{text m} here. Furthermore, the static
845 context is that of the enclosing goal (as for actual @{command
846 "qed"}). Thus the proof method may not refer to any assumptions
847 introduced in the current body, for example.
849 \item @{command "done"} completes a proof script, provided that the
850 current goal state is solved completely. Note that actual
851 structured proof commands (e.g.\ ``@{command "."}'' or @{command
852 "sorry"}) may be used to conclude proof scripts as well.
854 \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
855 shuffle the list of pending goals: @{command "defer"} puts off
856 sub-goal @{text n} to the end of the list (@{text "n = 1"} by
857 default), while @{command "prefer"} brings sub-goal @{text n} to the
860 \item @{command "back"} does back-tracking over the result sequence
861 of the latest proof command. Basically, any proof command may
862 return multiple results.
866 Any proper Isar proof method may be used with tactic script commands
867 such as @{command "apply"}. A few additional emulations of actual
868 tactics are provided as well; these would be never used in actual
869 structured proofs, of course.
873 subsection {* Defining proof methods *}
876 \begin{matharray}{rcl}
877 @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
881 'method\_setup' name '=' text text
887 \item @{command "method_setup"}~@{text "name = text description"}
888 defines a proof method in the current theory. The given @{text
889 "text"} has to be an ML expression of type @{ML_type "Args.src ->
890 Proof.context -> Proof.method"}. Parsing concrete method syntax
891 from @{ML_type Args.src} input can be quite tedious in general. The
892 following simple examples are for methods without any explicit
893 arguments, or a list of theorems, respectively.
895 %FIXME proper antiquotations
898 Method.no_args (Method.METHOD (fn facts => foobar_tac))
899 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
900 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
901 Method.thms_ctxt_args (fn thms => fn ctxt =>
902 Method.METHOD (fn facts => foobar_tac))
906 Note that mere tactic emulations may ignore the @{text facts}
907 parameter above. Proper proof methods would do something
908 appropriate with the list of current facts, though. Single-rule
909 methods usually do strict forward-chaining (e.g.\ by using @{ML
910 Drule.multi_resolves}), while automatic ones just insert the facts
911 using @{ML Method.insert_tac} before applying the main tactic.
917 section {* Generalized elimination \label{sec:obtain} *}
920 \begin{matharray}{rcl}
921 @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
922 @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
925 Generalized elimination means that additional elements with certain
926 properties may be introduced in the current context, by virtue of a
927 locally proven ``soundness statement''. Technically speaking, the
928 @{command "obtain"} language element is like a declaration of
929 @{command "fix"} and @{command "assume"} (see also see
930 \secref{sec:proof-context}), together with a soundness proof of its
931 additional claim. According to the nature of existential reasoning,
932 assumptions get eliminated from any result exported from the context
933 later, provided that the corresponding parameters do \emph{not}
934 occur in the conclusion.
937 'obtain' parname? (vars + 'and') 'where' (props + 'and')
939 'guess' (vars + 'and')
943 The derived Isar command @{command "obtain"} is defined as follows
944 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
945 facts indicated for forward chaining).
947 @{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]
948 \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"} \\
949 \quad @{command "proof"}~@{method succeed} \\
950 \qquad @{command "fix"}~@{text thesis} \\
951 \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"} \\
952 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
953 \quad\qquad @{command "apply"}~@{text -} \\
954 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
955 \quad @{command "qed"} \\
956 \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
959 Typically, the soundness proof is relatively straight-forward, often
960 just by canonical automated tools such as ``@{command "by"}~@{text
961 simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
962 ``@{text that}'' reduction above is declared as simplification and
965 In a sense, @{command "obtain"} represents at the level of Isar
966 proofs what would be meta-logical existential quantifiers and
967 conjunctions. This concept has a broad range of useful
968 applications, ranging from plain elimination (or introduction) of
969 object-level existential and conjunctions, to elimination over
970 results of symbolic evaluation of recursive definitions, for
971 example. Also note that @{command "obtain"} without parameters acts
972 much like @{command "have"}, where the result is treated as a
975 An alternative name to be used instead of ``@{text that}'' above may
976 be given in parentheses.
978 \medskip The improper variant @{command "guess"} is similar to
979 @{command "obtain"}, but derives the obtained statement from the
980 course of reasoning! The proof starts with a fixed goal @{text
981 thesis}. The subsequent proof may refine this to anything of the
982 form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
983 \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
984 final goal state is then used as reduction rule for the obtain
985 scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
986 x\<^sub>m"} are marked as internal by default, which prevents the
987 proof context from being polluted by ad-hoc variables. The variable
988 names and type constraints given as arguments for @{command "guess"}
989 specify a prefix of obtained parameters explicitly in the text.
991 It is important to note that the facts introduced by @{command
992 "obtain"} and @{command "guess"} may not be polymorphic: any
993 type-variables occurring here are fixed in the present context!
997 section {* Calculational reasoning \label{sec:calculation} *}
1000 \begin{matharray}{rcl}
1001 @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1002 @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
1003 @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1004 @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
1005 @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1006 @{attribute trans} & : & @{text attribute} \\
1007 @{attribute sym} & : & @{text attribute} \\
1008 @{attribute symmetric} & : & @{text attribute} \\
1011 Calculational proof is forward reasoning with implicit application
1012 of transitivity rules (such those of @{text "="}, @{text "\<le>"},
1013 @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
1014 @{fact_ref calculation} for accumulating results obtained by
1015 transitivity composed with the current result. Command @{command
1016 "also"} updates @{fact calculation} involving @{fact this}, while
1017 @{command "finally"} exhibits the final @{fact calculation} by
1018 forward chaining towards the next goal statement. Both commands
1019 require valid current facts, i.e.\ may occur only after commands
1020 that produce theorems such as @{command "assume"}, @{command
1021 "note"}, or some finished proof of @{command "have"}, @{command
1022 "show"} etc. The @{command "moreover"} and @{command "ultimately"}
1023 commands are similar to @{command "also"} and @{command "finally"},
1024 but only collect further results in @{fact calculation} without
1025 applying any rules yet.
1027 Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
1028 its canonical application with calculational proofs. It refers to
1029 the argument of the preceding statement. (The argument of a curried
1030 infix expression happens to be its right-hand side.)
1032 Isabelle/Isar calculations are implicitly subject to block structure
1033 in the sense that new threads of calculational reasoning are
1034 commenced for any new block (as opened by a local goal, for
1035 example). This means that, apart from being able to nest
1036 calculations, there is no separate \emph{begin-calculation} command
1039 \medskip The Isar calculation proof commands may be defined as
1040 follows:\footnote{We suppress internal bookkeeping such as proper
1041 handling of block-structure.}
1043 \begin{matharray}{rcl}
1044 @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
1045 @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
1046 @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
1047 @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
1048 @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
1052 ('also' | 'finally') ('(' thmrefs ')')?
1054 'trans' (() | 'add' | 'del')
1060 \item @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary
1061 @{fact calculation} register as follows. The first occurrence of
1062 @{command "also"} in some calculational thread initializes @{fact
1063 calculation} by @{fact this}. Any subsequent @{command "also"} on
1064 the same level of block-structure updates @{fact calculation} by
1065 some transitivity rule applied to @{fact calculation} and @{fact
1066 this} (in that order). Transitivity rules are picked from the
1067 current context, unless alternative rules are given as explicit
1070 \item @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact
1071 calculation} in the same way as @{command "also"}, and concludes the
1072 current calculational thread. The final result is exhibited as fact
1073 for forward chaining towards the next goal. Basically, @{command
1074 "finally"} just abbreviates @{command "also"}~@{command
1075 "from"}~@{fact calculation}. Typical idioms for concluding
1076 calculational proofs are ``@{command "finally"}~@{command
1077 "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
1078 "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
1080 \item @{command "moreover"} and @{command "ultimately"} are
1081 analogous to @{command "also"} and @{command "finally"}, but collect
1082 results only, without applying rules.
1084 \item @{command "print_trans_rules"} prints the list of transitivity
1085 rules (for calculational commands @{command "also"} and @{command
1086 "finally"}) and symmetry rules (for the @{attribute symmetric}
1087 operation and single step elimination patters) of the current
1090 \item @{attribute trans} declares theorems as transitivity rules.
1092 \item @{attribute sym} declares symmetry rules, as well as
1093 @{attribute "Pure.elim"}@{text "?"} rules.
1095 \item @{attribute symmetric} resolves a theorem with some rule
1096 declared as @{attribute sym} in the current context. For example,
1097 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
1098 swapped fact derived from that assumption.
1100 In structured proof texts it is often more appropriate to use an
1101 explicit single-step elimination proof, such as ``@{command
1102 "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
1103 "y = x"}~@{command ".."}''.
1109 section {* Proof by cases and induction \label{sec:cases-induct} *}
1111 subsection {* Rule contexts *}
1114 \begin{matharray}{rcl}
1115 @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1116 @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1117 @{attribute_def case_names} & : & @{text attribute} \\
1118 @{attribute_def case_conclusion} & : & @{text attribute} \\
1119 @{attribute_def params} & : & @{text attribute} \\
1120 @{attribute_def consumes} & : & @{text attribute} \\
1123 The puristic way to build up Isar proof contexts is by explicit
1124 language elements like @{command "fix"}, @{command "assume"},
1125 @{command "let"} (see \secref{sec:proof-context}). This is adequate
1126 for plain natural deduction, but easily becomes unwieldy in concrete
1127 verification tasks, which typically involve big induction rules with
1130 The @{command "case"} command provides a shorthand to refer to a
1131 local context symbolically: certain proof methods provide an
1132 environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
1133 x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
1134 "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
1135 "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
1136 \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably
1137 @{variable ?case} for the main conclusion.
1139 By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
1140 a case value is marked as hidden, i.e.\ there is no way to refer to
1141 such parameters in the subsequent proof text. After all, original
1142 rule parameters stem from somewhere outside of the current proof
1143 text. By using the explicit form ``@{command "case"}~@{text "(c
1144 y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to
1145 chose local names that fit nicely into the current context.
1147 \medskip It is important to note that proper use of @{command
1148 "case"} does not provide means to peek at the current goal state,
1149 which is not directly observable in Isar! Nonetheless, goal
1150 refinement commands do provide named cases @{text "goal\<^sub>i"}
1151 for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.
1152 Using this extra feature requires great care, because some bits of
1153 the internal tactical machinery intrude the proof text. In
1154 particular, parameter names stemming from the left-over of automated
1155 reasoning tools are usually quite unpredictable.
1157 Under normal circumstances, the text of cases emerge from standard
1158 elimination or induction rules, which in turn are derived from
1159 previous theory specifications in a canonical way (say from
1160 @{command "inductive"} definitions).
1162 \medskip Proper cases are only available if both the proof method
1163 and the rules involved support this. By using appropriate
1164 attributes, case names, conclusions, and parameters may be also
1165 declared by hand. Thus variant versions of rules that have been
1166 derived manually become ready to use in advanced case analysis
1170 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1172 caseref: nameref attributes?
1175 'case\_names' (name +)
1177 'case\_conclusion' name (name *)
1179 'params' ((name *) + 'and')
1187 \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
1188 context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
1189 appropriate proof method (such as @{method_ref cases} and
1190 @{method_ref induct}). The command ``@{command "case"}~@{text "(c
1191 x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
1192 x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.
1194 \item @{command "print_cases"} prints all local contexts of the
1195 current state, using Isar proof language notation.
1197 \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
1198 the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
1199 refers to the \emph{suffix} of the list of premises.
1201 \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
1202 names for the conclusions of a named premise @{text c}; here @{text
1203 "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula
1204 built by nesting a binary connective (e.g.\ @{text "\<or>"}).
1206 Note that proof methods such as @{method induct} and @{method
1207 coinduct} already provide a default name for the conclusion as a
1208 whole. The need to name subformulas only arises with cases that
1209 split into several sub-cases, as in common co-induction rules.
1211 \item @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames
1212 the innermost parameters of premises @{text "1, \<dots>, n"} of some
1213 theorem. An empty list of names may be given to skip positions,
1214 leaving the present parameters unchanged.
1216 Note that the default usage of case rules does \emph{not} directly
1217 expose parameters to the proof context.
1219 \item @{attribute consumes}~@{text n} declares the number of ``major
1220 premises'' of a rule, i.e.\ the number of facts to be consumed when
1221 it is applied by an appropriate proof method. The default value of
1222 @{attribute consumes} is @{text "n = 1"}, which is appropriate for
1223 the usual kind of cases and induction rules for inductive sets (cf.\
1224 \secref{sec:hol-inductive}). Rules without any @{attribute
1225 consumes} declaration given are treated as if @{attribute
1226 consumes}~@{text 0} had been specified.
1228 Note that explicit @{attribute consumes} declarations are only
1229 rarely needed; this is already taken care of automatically by the
1230 higher-level @{attribute cases}, @{attribute induct}, and
1231 @{attribute coinduct} declarations.
1237 subsection {* Proof methods *}
1240 \begin{matharray}{rcl}
1241 @{method_def cases} & : & @{text method} \\
1242 @{method_def induct} & : & @{text method} \\
1243 @{method_def coinduct} & : & @{text method} \\
1246 The @{method cases}, @{method induct}, and @{method coinduct}
1247 methods provide a uniform interface to common proof techniques over
1248 datatypes, inductive predicates (or sets), recursive functions etc.
1249 The corresponding rules may be specified and instantiated in a
1250 casual manner. Furthermore, these methods provide named local
1251 contexts that may be invoked via the @{command "case"} proof command
1252 within the subsequent proof text. This accommodates compact proof
1253 texts even when reasoning about large specifications.
1255 The @{method induct} method also provides some additional
1256 infrastructure in order to be applicable to structure statements
1257 (either using explicit meta-level connectives, or including facts
1258 and parameters separately). This avoids cumbersome encoding of
1259 ``strengthened'' inductive statements within the object-logic.
1262 'cases' (insts * 'and') rule?
1264 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
1266 'coinduct' insts taking rule?
1269 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
1271 definst: name ('==' | equiv) term | inst
1273 definsts: ( definst *)
1275 arbitrary: 'arbitrary' ':' ((term *) 'and' +)
1277 taking: 'taking' ':' insts
1283 \item @{method cases}~@{text "insts R"} applies method @{method
1284 rule} with an appropriate case distinction theorem, instantiated to
1285 the subjects @{text insts}. Symbolic case names are bound according
1286 to the rule's local contexts.
1288 The rule is determined as follows, according to the facts and
1289 arguments passed to the @{method cases} method:
1292 \begin{tabular}{llll}
1293 facts & & arguments & rule \\\hline
1294 & @{method cases} & & classical case split \\
1295 & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
1296 @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
1297 @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1301 Several instantiations may be given, referring to the \emph{suffix}
1302 of premises of the case rule; within each premise, the \emph{prefix}
1303 of variables is instantiated. In most situations, only a single
1304 term needs to be specified; this refers to the first variable of the
1305 last premise (it is usually the same for all cases).
1307 \item @{method induct}~@{text "insts R"} is analogous to the
1308 @{method cases} method, but refers to induction rules, which are
1309 determined as follows:
1312 \begin{tabular}{llll}
1313 facts & & arguments & rule \\\hline
1314 & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\
1315 @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
1316 @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1320 Several instantiations may be given, each referring to some part of
1321 a mutual inductive definition or datatype --- only related partial
1322 induction rules may be used together, though. Any of the lists of
1323 terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables
1324 present in the induction rule. This enables the writer to specify
1325 only induction variables, or both predicates and variables, for
1328 Instantiations may be definitional: equations @{text "x \<equiv> t"}
1329 introduce local definitions, which are inserted into the claim and
1330 discharged after applying the induction rule. Equalities reappear
1331 in the inductive cases, but have been transformed according to the
1332 induction principle being involved here. In order to achieve
1333 practically useful induction hypotheses, some variables occurring in
1334 @{text t} need to be fixed (see below).
1336 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
1337 specification generalizes variables @{text "x\<^sub>1, \<dots>,
1338 x\<^sub>m"} of the original goal before applying induction. Thus
1339 induction hypotheses may become sufficiently general to get the
1340 proof through. Together with definitional instantiations, one may
1341 effectively perform induction over expressions of a certain
1344 The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1345 specification provides additional instantiations of a prefix of
1346 pending variables in the rule. Such schematic induction rules
1347 rarely occur in practice, though.
1349 \item @{method coinduct}~@{text "inst R"} is analogous to the
1350 @{method induct} method, but refers to coinduction rules, which are
1351 determined as follows:
1354 \begin{tabular}{llll}
1355 goal & & arguments & rule \\\hline
1356 & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
1357 @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
1358 @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1361 Coinduction is the dual of induction. Induction essentially
1362 eliminates @{text "A x"} towards a generic result @{text "P x"},
1363 while coinduction introduces @{text "A x"} starting with @{text "B
1364 x"}, for a suitable ``bisimulation'' @{text B}. The cases of a
1365 coinduct rule are typically named after the predicates or sets being
1366 covered, while the conclusions consist of several alternatives being
1367 named after the individual destructor patterns.
1369 The given instantiation refers to the \emph{suffix} of variables
1370 occurring in the rule's major premise, or conclusion if unavailable.
1371 An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1372 specification may be required in order to specify the bisimulation
1373 to be used in the coinduction step.
1377 Above methods produce named local contexts, as determined by the
1378 instantiated rule as given in the text. Beyond that, the @{method
1379 induct} and @{method coinduct} methods guess further instantiations
1380 from the goal specification itself. Any persisting unresolved
1381 schematic variables of the resulting rule will render the the
1382 corresponding case invalid. The term binding @{variable ?case} for
1383 the conclusion will be provided with each case, provided that term
1386 The @{command "print_cases"} command prints all named cases present
1387 in the current proof state.
1389 \medskip Despite the additional infrastructure, both @{method cases}
1390 and @{method coinduct} merely apply a certain rule, after
1391 instantiation, while conforming due to the usual way of monotonic
1392 natural deduction: the context of a structured statement @{text
1393 "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}
1394 reappears unchanged after the case split.
1396 The @{method induct} method is fundamentally different in this
1397 respect: the meta-level structure is passed through the
1398 ``recursive'' course involved in the induction. Thus the original
1399 statement is basically replaced by separate copies, corresponding to
1400 the induction hypotheses and conclusion; the original goal context
1401 is no longer available. Thus local assumptions, fixed parameters
1402 and definitions effectively participate in the inductive rephrasing
1403 of the original statement.
1405 In induction proofs, local assumptions introduced by cases are split
1406 into two different kinds: @{text hyps} stemming from the rule and
1407 @{text prems} from the goal statement. This is reflected in the
1408 extracted cases accordingly, so invoking ``@{command "case"}~@{text
1409 c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
1410 as well as fact @{text c} to hold the all-inclusive list.
1412 \medskip Facts presented to either method are consumed according to
1413 the number of ``major premises'' of the rule involved, which is
1414 usually 0 for plain cases and induction rules of datatypes etc.\ and
1415 1 for rules of inductive predicates or sets and the like. The
1416 remaining facts are inserted into the goal verbatim before the
1417 actual @{text cases}, @{text induct}, or @{text coinduct} rule is
1422 subsection {* Declaring rules *}
1425 \begin{matharray}{rcl}
1426 @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1427 @{attribute_def cases} & : & @{text attribute} \\
1428 @{attribute_def induct} & : & @{text attribute} \\
1429 @{attribute_def coinduct} & : & @{text attribute} \\
1440 spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
1446 \item @{command "print_induct_rules"} prints cases and induct rules
1447 for predicates (or sets) and types of the current context.
1449 \item @{attribute cases}, @{attribute induct}, and @{attribute
1450 coinduct} (as attributes) declare rules for reasoning about
1451 (co)inductive predicates (or sets) and types, using the
1452 corresponding methods of the same name. Certain definitional
1453 packages of object-logics usually declare emerging cases and
1454 induction rules as expected, so users rarely need to intervene.
1456 Rules may be deleted via the @{text "del"} specification, which
1457 covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
1458 sub-categories simultaneously. For example, @{attribute
1459 cases}~@{text del} removes any @{attribute cases} rules declared for
1460 some type, predicate, or set.
1462 Manual rule declarations usually refer to the @{attribute
1463 case_names} and @{attribute params} attributes to adjust names of
1464 cases and parameters of a rule; the @{attribute consumes}
1465 declaration is taken care of automatically: @{attribute
1466 consumes}~@{text 0} is specified for ``type'' rules and @{attribute
1467 consumes}~@{text 1} for ``predicate'' / ``set'' rules.