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 {* Formal notepad *}
52 \begin{matharray}{rcl}
53 @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
57 @@{command notepad} @'begin'
64 \item @{command "notepad"}~@{keyword "begin"} opens a proof state
65 without any goal statement. This allows to experiment with Isar,
66 without producing any persistent result.
68 The notepad can be closed by @{command "end"} or discontinued by
75 subsection {* Blocks *}
78 \begin{matharray}{rcl}
79 @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
80 @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
81 @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
84 While Isar is inherently block-structured, opening and closing
85 blocks is mostly handled rather casually, with little explicit
86 user-intervention. Any local goal statement automatically opens
87 \emph{two} internal blocks, which are closed again when concluding
88 the sub-proof (by @{command "qed"} etc.). Sections of different
89 context within a sub-proof may be switched via @{command "next"},
90 which is just a single block-close followed by block-open again.
91 The effect of @{command "next"} is to reset the local proof context;
92 there is no goal focus involved here!
94 For slightly more advanced applications, there are explicit block
95 parentheses as well. These typically achieve a stronger forward
100 \item @{command "next"} switches to a fresh block within a
101 sub-proof, resetting the local context to the initial one.
103 \item @{command "{"} and @{command "}"} explicitly open and close
104 blocks. Any current facts pass through ``@{command "{"}''
105 unchanged, while ``@{command "}"}'' causes any result to be
106 \emph{exported} into the enclosing context. Thus fixed variables
107 are generalized, assumptions discharged, and local definitions
108 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
109 of @{command "assume"} and @{command "presume"} in this mode of
110 forward reasoning --- in contrast to plain backward reasoning with
111 the result exported at @{command "show"} time.
117 subsection {* Omitting proofs *}
120 \begin{matharray}{rcl}
121 @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\
124 The @{command "oops"} command discontinues the current proof
125 attempt, while considering the partial proof text as properly
126 processed. This is conceptually quite different from ``faking''
127 actual proofs via @{command_ref "sorry"} (see
128 \secref{sec:proof-steps}): @{command "oops"} does not observe the
129 proof structure at all, but goes back right to the theory level.
130 Furthermore, @{command "oops"} does not produce any result theorem
131 --- there is no intended claim to be able to complete the proof
134 A typical application of @{command "oops"} is to explain Isar proofs
135 \emph{within} the system itself, in conjunction with the document
136 preparation tools of Isabelle described in \chref{ch:document-prep}.
137 Thus partial or even wrong proof attempts can be discussed in a
138 logically sound manner. Note that the Isabelle {\LaTeX} macros can
139 be easily adapted to print something like ``@{text "\<dots>"}'' instead of
140 the keyword ``@{command "oops"}''.
142 \medskip The @{command "oops"} command is undo-able, unlike
143 @{command_ref "kill"} (see \secref{sec:history}). The effect is to
144 get back to the theory just before the opening of the proof.
148 section {* Statements *}
150 subsection {* Context elements \label{sec:proof-context} *}
153 \begin{matharray}{rcl}
154 @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
155 @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
156 @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
157 @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
160 The logical proof context consists of fixed variables and
161 assumptions. The former closely correspond to Skolem constants, or
162 meta-level universal quantification as provided by the Isabelle/Pure
163 logical framework. Introducing some \emph{arbitrary, but fixed}
164 variable via ``@{command "fix"}~@{text x}'' results in a local value
165 that may be used in the subsequent proof as any other variable or
166 constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
167 the context will be universally closed wrt.\ @{text x} at the
168 outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
169 form using Isabelle's meta-variables).
171 Similarly, introducing some assumption @{text \<chi>} has two effects.
172 On the one hand, a local theorem is created that may be used as a
173 fact in subsequent proof steps. On the other hand, any result
174 @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
175 the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
176 using such a result would basically introduce a new subgoal stemming
177 from the assumption. How this situation is handled depends on the
178 version of assumption command used: while @{command "assume"}
179 insists on solving the subgoal by unification with some premise of
180 the goal, @{command "presume"} leaves the subgoal unchanged in order
181 to be proved later by the user.
183 Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
184 t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
185 another version of assumption that causes any hypothetical equation
186 @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
187 exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
191 @@{command fix} (@{syntax vars} + @'and')
193 (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
195 @@{command def} (def + @'and')
197 def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
202 \item @{command "fix"}~@{text x} introduces a local variable @{text
203 x} that is \emph{arbitrary, but fixed.}
205 \item @{command "assume"}~@{text "a: \<phi>"} and @{command
206 "presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
207 assumption. Subsequent results applied to an enclosing goal (e.g.\
208 by @{command_ref "show"}) are handled as follows: @{command
209 "assume"} expects to be able to unify with existing premises in the
210 goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
212 Several lists of assumptions may be given (separated by
213 @{keyword_ref "and"}; the resulting list of current facts consists
214 of all of these concatenated.
216 \item @{command "def"}~@{text "x \<equiv> t"} introduces a local
217 (non-polymorphic) definition. In results exported from the context,
218 @{text x} is replaced by @{text t}. Basically, ``@{command
219 "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
220 x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
221 hypothetical equation solved by reflexivity.
223 The default name for the definitional equation is @{text x_def}.
224 Several simultaneous definitions may be given at the same time.
228 The special name @{fact_ref prems} refers to all assumptions of the
229 current context as a list of theorems. This feature should be used
230 with great care! It is better avoided in final proof texts.
234 subsection {* Term abbreviations \label{sec:term-abbrev} *}
237 \begin{matharray}{rcl}
238 @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
239 @{keyword_def "is"} & : & syntax \\
242 Abbreviations may be either bound by explicit @{command
243 "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
244 goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
245 p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
246 bind extra-logical term variables, which may be either named
247 schematic variables of the form @{text ?x}, or nameless dummies
248 ``@{variable _}'' (underscore). Note that in the @{command "let"}
249 form the patterns occur on the left-hand side, while the @{keyword
250 "is"} patterns are in postfix position.
252 Polymorphism of term bindings is handled in Hindley-Milner style,
253 similar to ML. Type variables referring to local assumptions or
254 open goal statements are \emph{fixed}, while those of finished
255 results or bound by @{command "let"} may occur in \emph{arbitrary}
256 instances later. Even though actual polymorphism should be rarely
257 used in practice, this mechanism is essential to achieve proper
258 incremental type-inference, as the user proceeds to build up the
259 Isar proof text from left to right.
261 \medskip Term abbreviations are quite different from local
262 definitions as introduced via @{command "def"} (see
263 \secref{sec:proof-context}). The latter are visible within the
264 logic as actual equations, while abbreviations disappear during the
265 input process just after type checking. Also note that @{command
266 "def"} does not support polymorphism.
269 @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
272 The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
273 @{syntax prop_pat} (see \secref{sec:term-decls}).
277 \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
278 text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous
279 higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
281 \item @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but
282 matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement. Also
283 note that @{keyword "is"} is not a separate command, but part of
284 others (such as @{command "assume"}, @{command "have"} etc.).
288 Some \emph{implicit} term abbreviations\index{term abbreviations}
289 for goals and facts are available as well. For any open goal,
290 @{variable_ref thesis} refers to its object-level statement,
291 abstracted over any meta-level parameters (if present). Likewise,
292 @{variable_ref this} is bound for fact statements resulting from
293 assumptions or finished goals. In case @{variable this} refers to
294 an object-logic statement that is an application @{text "f t"}, then
295 @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
296 (three dots). The canonical application of this convenience are
297 calculational proofs (see \secref{sec:calculation}).
301 subsection {* Facts and forward chaining *}
304 \begin{matharray}{rcl}
305 @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
306 @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
307 @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
308 @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
309 @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
310 @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
313 New facts are established either by assumption or proof of local
314 statements. Any fact will usually be involved in further proofs,
315 either as explicit arguments of proof methods, or when forward
316 chaining towards the next goal via @{command "then"} (and variants);
317 @{command "from"} and @{command "with"} are composite forms
318 involving @{command "note"}. The @{command "using"} elements
319 augments the collection of used facts \emph{after} a goal has been
320 stated. Note that the special theorem name @{fact_ref this} refers
321 to the most recently established facts, but only \emph{before}
322 issuing a follow-up claim.
325 @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
327 (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
328 (@{syntax thmrefs} + @'and')
333 \item @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
334 @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. Note that
335 attributes may be involved as well, both on the left and right hand
338 \item @{command "then"} indicates forward chaining by the current
339 facts in order to establish the goal to be claimed next. The
340 initial proof method invoked to refine that will be offered the
341 facts to do ``anything appropriate'' (see also
342 \secref{sec:proof-steps}). For example, method @{method (Pure) rule}
343 (see \secref{sec:pure-meth-att}) would typically do an elimination
344 rather than an introduction. Automatic methods usually insert the
345 facts into the goal state before operation. This provides a simple
346 scheme to control relevance of facts in automated proof search.
348 \item @{command "from"}~@{text b} abbreviates ``@{command
349 "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
350 equivalent to ``@{command "from"}~@{text this}''.
352 \item @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command
353 "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining
354 is from earlier facts together with the current ones.
356 \item @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being
357 currently indicated for use by a subsequent refinement step (such as
358 @{command_ref "apply"} or @{command_ref "proof"}).
360 \item @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally
361 similar to @{command "using"}, but unfolds definitional equations
362 @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.
366 Forward chaining with an empty list of theorems is the same as not
367 chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
368 effect apart from entering @{text "prove(chain)"} mode, since
369 @{fact_ref nothing} is bound to the empty list of theorems.
371 Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
372 facts to be given in their proper order, corresponding to a prefix
373 of the premises of the rule involved. Note that positions may be
374 easily skipped using something like @{command "from"}~@{text "_
375 \<AND> a \<AND> b"}, for example. This involves the trivial rule
376 @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
377 ``@{fact_ref "_"}'' (underscore).
379 Automated methods (such as @{method simp} or @{method auto}) just
380 insert any given facts before their usual operation. Depending on
381 the kind of procedure involved, the order of facts is less
386 subsection {* Goals \label{sec:goals} *}
389 \begin{matharray}{rcl}
390 @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
391 @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
392 @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
393 @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
394 @{command_def "schematic_theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
395 @{command_def "schematic_corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
396 @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
397 @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
398 @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
399 @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
400 @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
403 From a theory context, proof mode is entered by an initial goal
404 command such as @{command "lemma"}, @{command "theorem"}, or
405 @{command "corollary"}. Within a proof, new claims may be
406 introduced locally as well; four variants are available here to
407 indicate whether forward chaining of facts should be performed
408 initially (via @{command_ref "then"}), and whether the final result
409 is meant to solve some pending goal.
411 Goals may consist of multiple statements, resulting in a list of
412 facts eventually. A pending multi-goal is internally represented as
413 a meta-level conjunction (@{text "&&&"}), which is usually
414 split into the corresponding number of sub-goals prior to an initial
415 method application, via @{command_ref "proof"}
416 (\secref{sec:proof-steps}) or @{command_ref "apply"}
417 (\secref{sec:tactic-commands}). The @{method_ref induct} method
418 covered in \secref{sec:cases-induct} acts on multiple claims
421 Claims at the theory level may be either in short or long form. A
422 short goal merely consists of several simultaneous propositions
423 (often just one). A long goal includes an explicit context
424 specification for the subsequent conclusion, involving local
425 parameters and assumptions. Here the role of each part of the
426 statement is explicitly marked by separate keywords (see also
427 \secref{sec:locale}); the local assumptions being introduced here
428 are available as @{fact_ref assms} in the proof. Moreover, there
429 are two kinds of conclusions: @{element_def "shows"} states several
430 simultaneous propositions (essentially a big conjunction), while
431 @{element_def "obtains"} claims several simultaneous simultaneous
432 contexts of (essentially a big disjunction of eliminated parameters
433 and assumptions, cf.\ \secref{sec:obtain}).
436 (@@{command lemma} | @@{command theorem} | @@{command corollary} |
437 @@{command schematic_lemma} | @@{command schematic_theorem} |
438 @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)
440 (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
442 @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
445 goal: (@{syntax props} + @'and')
447 longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
449 conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
451 case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
456 \item @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
457 @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
458 \<phi>"} to be put back into the target context. An additional @{syntax
459 context} specification may build up an initial proof context for the
460 subsequent claim; this includes local definitions and syntax as
461 well, see the definition of @{syntax context_elem} in
464 \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
465 "corollary"}~@{text "a: \<phi>"} are essentially the same as @{command
466 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
467 being of a different kind. This discrimination acts like a formal
470 \item @{command "schematic_lemma"}, @{command "schematic_theorem"},
471 @{command "schematic_corollary"} are similar to @{command "lemma"},
472 @{command "theorem"}, @{command "corollary"}, respectively but allow
473 the statement to contain unbound schematic variables.
475 Under normal circumstances, an Isar proof text needs to specify
476 claims explicitly. Schematic goals are more like goals in Prolog,
477 where certain results are synthesized in the course of reasoning.
478 With schematic statements, the inherent compositionality of Isar
479 proofs is lost, which also impacts performance, because proof
480 checking is forced into sequential mode.
482 \item @{command "have"}~@{text "a: \<phi>"} claims a local goal,
483 eventually resulting in a fact within the current logical context.
484 This operation is completely independent of any pending sub-goals of
485 an enclosing goal statements, so @{command "have"} may be freely
486 used for experimental exploration of potential results within a
489 \item @{command "show"}~@{text "a: \<phi>"} is like @{command
490 "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
491 sub-goal for each one of the finished result, after having been
492 exported into the corresponding context (at the head of the
493 sub-proof of this @{command "show"} command).
495 To accommodate interactive debugging, resulting rules are printed
496 before being applied internally. Even more, interactive execution
497 of @{command "show"} predicts potential failure and displays the
498 resulting error as a warning beforehand. Watch out for the
501 %FIXME proper antiquitation
503 Problem! Local statement will fail to solve any pending goal
506 \item @{command "hence"} abbreviates ``@{command "then"}~@{command
507 "have"}'', i.e.\ claims a local goal to be proven by forward
508 chaining the current facts. Note that @{command "hence"} is also
509 equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
511 \item @{command "thus"} abbreviates ``@{command "then"}~@{command
512 "show"}''. Note that @{command "thus"} is also equivalent to
513 ``@{command "from"}~@{text this}~@{command "show"}''.
515 \item @{command "print_statement"}~@{text a} prints facts from the
516 current theory or proof context in long statement form, according to
517 the syntax for @{command "lemma"} given above.
521 Any goal statement causes some term abbreviations (such as
522 @{variable_ref "?thesis"}) to be bound automatically, see also
523 \secref{sec:term-abbrev}.
525 The optional case names of @{element_ref "obtains"} have a twofold
526 meaning: (1) during the of this claim they refer to the the local
527 context introductions, (2) the resulting rule is annotated
528 accordingly to support symbolic case splits when used with the
529 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
533 section {* Refinement steps *}
535 subsection {* Proof method expressions \label{sec:proof-meth} *}
537 text {* Proof methods are either basic ones, or expressions composed
538 of methods via ``@{verbatim ","}'' (sequential composition),
539 ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
540 (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
541 "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
542 sub-goals, with default @{text "n = 1"}). In practice, proof
543 methods are usually just a comma separated list of @{syntax
544 nameref}~@{syntax args} specifications. Note that parentheses may
545 be dropped for single method specifications (with no arguments).
548 @{syntax_def method}:
549 (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
551 methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|')
554 Proper Isar proof methods do \emph{not} admit arbitrary goal
555 addressing, but refer either to the first sub-goal or all sub-goals
556 uniformly. The goal restriction operator ``@{text "[n]"}''
557 evaluates a method expression within a sandbox consisting of the
558 first @{text n} sub-goals (which need to exist). For example, the
559 method ``@{text "simp_all[3]"}'' simplifies the first three
560 sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
561 new goals that emerge from applying rule @{text "foo"} to the
562 originally first one.
564 Improper methods, notably tactic emulations, offer a separate
565 low-level goal addressing scheme as explicit argument to the
566 individual tactic being involved. Here ``@{text "[!]"}'' refers to
567 all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
571 @{syntax_def goal_spec}:
572 '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
577 subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
580 \begin{matharray}{rcl}
581 @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\
582 @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\
583 @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
584 @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
585 @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
586 @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
589 Arbitrary goal refinement via tactics is considered harmful.
590 Structured proof composition in Isar admits proof methods to be
591 invoked in two places only.
595 \item An \emph{initial} refinement step @{command_ref
596 "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
597 of sub-goals that are to be solved later. Facts are passed to
598 @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
599 "proof(chain)"} mode.
601 \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
602 "m\<^sub>2"} is intended to solve remaining goals. No facts are
603 passed to @{text "m\<^sub>2"}.
607 The only other (proper) way to affect pending goals in a proof body
608 is by @{command_ref "show"}, which involves an explicit statement of
609 what is to be solved eventually. Thus we avoid the fundamental
610 problem of unstructured tactic scripts that consist of numerous
611 consecutive goal transformations, with invisible effects.
613 \medskip As a general rule of thumb for good proof style, initial
614 proof methods should either solve the goal completely, or constitute
615 some well-understood reduction to new sub-goals. Arbitrary
616 automatic proof tools that are prone leave a large number of badly
617 structured sub-goals are no help in continuing the proof document in
618 an intelligible manner.
620 Unless given explicitly by the user, the default initial method is
621 @{method_ref (Pure) rule} (or its classical variant @{method_ref
622 rule}), which applies a single standard elimination or introduction
623 rule according to the topmost symbol involved. There is no separate
624 default terminal method. Any remaining goals are always solved by
625 assumption in the very last step.
628 @@{command proof} method?
630 @@{command qed} method?
632 @@{command \"by\"} method method?
634 (@@{command \".\"} | @@{command \"..\"} | @@{command sorry})
639 \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof
640 method @{text "m\<^sub>1"}; facts for forward chaining are passed if so
641 indicated by @{text "proof(chain)"} mode.
643 \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by
644 proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.
645 If the goal had been @{text "show"} (or @{text "thus"}), some
646 pending sub-goal is solved as well by the rule resulting from the
647 result \emph{exported} into the enclosing goal context. Thus @{text
648 "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the
649 resulting rule does not fit to any pending goal\footnote{This
650 includes any additional ``strong'' assumptions as introduced by
651 @{command "assume"}.} of the enclosing context. Debugging such a
652 situation might involve temporarily changing @{command "show"} into
653 @{command "have"}, or weakening the local context by replacing
654 occurrences of @{command "assume"} by @{command "presume"}.
656 \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal
657 proof}\index{proof!terminal}; it abbreviates @{command
658 "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text "m\<^sub>2"}, but with
659 backtracking across both methods. Debugging an unsuccessful
660 @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its
661 definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even
662 @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
665 \item ``@{command ".."}'' is a \emph{default
666 proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
669 \item ``@{command "."}'' is a \emph{trivial
670 proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
673 \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
674 pretending to solve the pending claim without further ado. This
675 only works in interactive development, or if the @{ML
676 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
677 proofs are not the real thing. Internally, each theorem container
678 is tainted by an oracle invocation, which is indicated as ``@{text
679 "[!]"}'' in the printed result.
681 The most important application of @{command "sorry"} is to support
682 experimentation and top-down proof development.
688 subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
691 The following proof methods and attributes refer to basic logical
692 operations of Isar. Further methods and attributes are provided by
693 several generic and object-logic specific tools and packages (see
694 \chref{ch:gen-tools} and \chref{ch:hol}).
696 \begin{matharray}{rcl}
697 @{method_def "-"} & : & @{text method} \\
698 @{method_def "fact"} & : & @{text method} \\
699 @{method_def "assumption"} & : & @{text method} \\
700 @{method_def "this"} & : & @{text method} \\
701 @{method_def (Pure) "rule"} & : & @{text method} \\
702 @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
703 @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
704 @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
705 @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]
706 @{attribute_def "OF"} & : & @{text attribute} \\
707 @{attribute_def "of"} & : & @{text attribute} \\
708 @{attribute_def "where"} & : & @{text attribute} \\
712 @@{method fact} @{syntax thmrefs}?
714 @@{method (Pure) rule} @{syntax thmrefs}?
716 rulemod: ('intro' | 'elim' | 'dest')
717 ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
719 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
720 ('!' | () | '?') @{syntax nat}?
722 @@{attribute (Pure) rule} 'del'
724 @@{attribute OF} @{syntax thmrefs}
726 @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
728 @@{attribute \"where\"}
729 ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
730 (@{syntax type} | @{syntax term}) * @'and')
735 \item ``@{method "-"}'' (minus) does nothing but insert the forward
736 chaining facts as premises into the goal. Note that command
737 @{command_ref "proof"} without any method actually performs a single
738 reduction step using the @{method_ref (Pure) rule} method; thus a plain
739 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
740 "-"}'' rather than @{command "proof"} alone.
742 \item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
743 @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
744 modulo unification of schematic type and term variables. The rule
745 structure is not taken into account, i.e.\ meta-level implication is
746 considered atomic. This is the same principle underlying literal
747 facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~@{text
748 "\<phi>"}~@{command "by"}~@{text fact}'' is equivalent to ``@{command
749 "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim "`"}'' provided that
750 @{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the
753 \item @{method assumption} solves some goal by a single assumption
754 step. All given facts are guaranteed to participate in the
755 refinement; this means there may be only 0 or 1 in the first place.
756 Recall that @{command "qed"} (\secref{sec:proof-steps}) already
757 concludes any remaining sub-goals by assumption, so structured
758 proofs usually need not quote the @{method assumption} method at
761 \item @{method this} applies all of the current facts directly as
762 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
763 "by"}~@{text this}''.
765 \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
766 argument in backward manner; facts are used to reduce the rule
767 before applying it to the goal. Thus @{method (Pure) rule} without facts
768 is plain introduction, while with facts it becomes elimination.
770 When no arguments are given, the @{method (Pure) rule} method tries to pick
771 appropriate rules automatically, as declared in the current context
772 using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
773 @{attribute (Pure) dest} attributes (see below). This is the
774 default behavior of @{command "proof"} and ``@{command ".."}''
775 (double-dot) steps (see \secref{sec:proof-steps}).
777 \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
778 @{attribute (Pure) dest} declare introduction, elimination, and
779 destruct rules, to be used with method @{method (Pure) rule}, and similar
780 tools. Note that the latter will ignore rules declared with
781 ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
783 The classical reasoner (see \secref{sec:classical}) introduces its
784 own variants of these attributes; use qualified names to access the
785 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
788 \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
789 elimination, or destruct rules.
791 \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
792 theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
793 (in parallel). This corresponds to the @{ML "op MRS"} operation in
794 ML, but note the reversed order. Positions may be effectively
795 skipped by including ``@{text _}'' (underscore) as argument.
797 \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
798 instantiation of term variables. The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
799 substituted for any schematic variables occurring in a theorem from
800 left to right; ``@{text _}'' (underscore) indicates to skip a
801 position. Arguments following a ``@{text "concl:"}'' specification
802 refer to positions of the conclusion of a rule.
804 \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
805 performs named instantiation of schematic type and term variables
806 occurring in a theorem. Schematic variables have to be specified on
807 the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may
808 be omitted if the variable name is a plain identifier without index.
809 As type instantiations are inferred from term instantiations,
810 explicit type instantiations are seldom necessary.
816 subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
819 The Isar provides separate commands to accommodate tactic-style
820 proof scripts within the same system. While being outside the
821 orthodox Isar proof language, these might come in handy for
822 interactive exploration and debugging, or even actual tactical proof
823 within new-style theories (to benefit from document preparation, for
824 example). See also \secref{sec:tactics} for actual tactics, that
825 have been encapsulated as proof methods. Proper proof methods may
826 be used in scripts, too.
828 \begin{matharray}{rcl}
829 @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
830 @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
831 @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
832 @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
833 @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
834 @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
838 ( @@{command apply} | @@{command apply_end} ) @{syntax method}
840 @@{command defer} @{syntax nat}?
842 @@{command prefer} @{syntax nat}
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 @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax 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 @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')
956 @'where' (@{syntax props} + @'and')
958 @@{command guess} (@{syntax 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 (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?
1072 @@{attribute trans} (() | 'add' | 'del')
1077 \item @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary
1078 @{fact calculation} register as follows. The first occurrence of
1079 @{command "also"} in some calculational thread initializes @{fact
1080 calculation} by @{fact this}. Any subsequent @{command "also"} on
1081 the same level of block-structure updates @{fact calculation} by
1082 some transitivity rule applied to @{fact calculation} and @{fact
1083 this} (in that order). Transitivity rules are picked from the
1084 current context, unless alternative rules are given as explicit
1087 \item @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact
1088 calculation} in the same way as @{command "also"}, and concludes the
1089 current calculational thread. The final result is exhibited as fact
1090 for forward chaining towards the next goal. Basically, @{command
1091 "finally"} just abbreviates @{command "also"}~@{command
1092 "from"}~@{fact calculation}. Typical idioms for concluding
1093 calculational proofs are ``@{command "finally"}~@{command
1094 "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
1095 "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
1097 \item @{command "moreover"} and @{command "ultimately"} are
1098 analogous to @{command "also"} and @{command "finally"}, but collect
1099 results only, without applying rules.
1101 \item @{command "print_trans_rules"} prints the list of transitivity
1102 rules (for calculational commands @{command "also"} and @{command
1103 "finally"}) and symmetry rules (for the @{attribute symmetric}
1104 operation and single step elimination patters) of the current
1107 \item @{attribute trans} declares theorems as transitivity rules.
1109 \item @{attribute sym} declares symmetry rules, as well as
1110 @{attribute "Pure.elim"}@{text "?"} rules.
1112 \item @{attribute symmetric} resolves a theorem with some rule
1113 declared as @{attribute sym} in the current context. For example,
1114 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
1115 swapped fact derived from that assumption.
1117 In structured proof texts it is often more appropriate to use an
1118 explicit single-step elimination proof, such as ``@{command
1119 "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
1120 "y = x"}~@{command ".."}''.
1126 section {* Proof by cases and induction \label{sec:cases-induct} *}
1128 subsection {* Rule contexts *}
1131 \begin{matharray}{rcl}
1132 @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
1133 @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1134 @{attribute_def case_names} & : & @{text attribute} \\
1135 @{attribute_def case_conclusion} & : & @{text attribute} \\
1136 @{attribute_def params} & : & @{text attribute} \\
1137 @{attribute_def consumes} & : & @{text attribute} \\
1140 The puristic way to build up Isar proof contexts is by explicit
1141 language elements like @{command "fix"}, @{command "assume"},
1142 @{command "let"} (see \secref{sec:proof-context}). This is adequate
1143 for plain natural deduction, but easily becomes unwieldy in concrete
1144 verification tasks, which typically involve big induction rules with
1147 The @{command "case"} command provides a shorthand to refer to a
1148 local context symbolically: certain proof methods provide an
1149 environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
1150 x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
1151 "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
1152 "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
1153 \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably
1154 @{variable ?case} for the main conclusion.
1156 By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
1157 a case value is marked as hidden, i.e.\ there is no way to refer to
1158 such parameters in the subsequent proof text. After all, original
1159 rule parameters stem from somewhere outside of the current proof
1160 text. By using the explicit form ``@{command "case"}~@{text "(c
1161 y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to
1162 chose local names that fit nicely into the current context.
1164 \medskip It is important to note that proper use of @{command
1165 "case"} does not provide means to peek at the current goal state,
1166 which is not directly observable in Isar! Nonetheless, goal
1167 refinement commands do provide named cases @{text "goal\<^sub>i"}
1168 for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.
1169 Using this extra feature requires great care, because some bits of
1170 the internal tactical machinery intrude the proof text. In
1171 particular, parameter names stemming from the left-over of automated
1172 reasoning tools are usually quite unpredictable.
1174 Under normal circumstances, the text of cases emerge from standard
1175 elimination or induction rules, which in turn are derived from
1176 previous theory specifications in a canonical way (say from
1177 @{command "inductive"} definitions).
1179 \medskip Proper cases are only available if both the proof method
1180 and the rules involved support this. By using appropriate
1181 attributes, case names, conclusions, and parameters may be also
1182 declared by hand. Thus variant versions of rules that have been
1183 derived manually become ready to use in advanced case analysis
1187 @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')')
1189 caseref: nameref attributes?
1192 @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
1194 @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
1196 @@{attribute params} ((@{syntax name} * ) + @'and')
1198 @@{attribute consumes} @{syntax nat}?
1203 \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
1204 context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
1205 appropriate proof method (such as @{method_ref cases} and
1206 @{method_ref induct}). The command ``@{command "case"}~@{text "(c
1207 x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
1208 x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.
1210 \item @{command "print_cases"} prints all local contexts of the
1211 current state, using Isar proof language notation.
1213 \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
1214 the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
1215 refers to the \emph{prefix} of the list of premises. Each of the
1216 cases @{text "c\<^isub>i"} can be of the form @{text "c[h\<^isub>1 \<dots> h\<^isub>n]"} where
1217 the @{text "h\<^isub>1 \<dots> h\<^isub>n"} are the names of the hypotheses in case @{text "c\<^isub>i"}
1220 \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
1221 names for the conclusions of a named premise @{text c}; here @{text
1222 "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula
1223 built by nesting a binary connective (e.g.\ @{text "\<or>"}).
1225 Note that proof methods such as @{method induct} and @{method
1226 coinduct} already provide a default name for the conclusion as a
1227 whole. The need to name subformulas only arises with cases that
1228 split into several sub-cases, as in common co-induction rules.
1230 \item @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames
1231 the innermost parameters of premises @{text "1, \<dots>, n"} of some
1232 theorem. An empty list of names may be given to skip positions,
1233 leaving the present parameters unchanged.
1235 Note that the default usage of case rules does \emph{not} directly
1236 expose parameters to the proof context.
1238 \item @{attribute consumes}~@{text n} declares the number of ``major
1239 premises'' of a rule, i.e.\ the number of facts to be consumed when
1240 it is applied by an appropriate proof method. The default value of
1241 @{attribute consumes} is @{text "n = 1"}, which is appropriate for
1242 the usual kind of cases and induction rules for inductive sets (cf.\
1243 \secref{sec:hol-inductive}). Rules without any @{attribute
1244 consumes} declaration given are treated as if @{attribute
1245 consumes}~@{text 0} had been specified.
1247 Note that explicit @{attribute consumes} declarations are only
1248 rarely needed; this is already taken care of automatically by the
1249 higher-level @{attribute cases}, @{attribute induct}, and
1250 @{attribute coinduct} declarations.
1256 subsection {* Proof methods *}
1259 \begin{matharray}{rcl}
1260 @{method_def cases} & : & @{text method} \\
1261 @{method_def induct} & : & @{text method} \\
1262 @{method_def induction} & : & @{text method} \\
1263 @{method_def coinduct} & : & @{text method} \\
1266 The @{method cases}, @{method induct}, @{method induction},
1267 and @{method coinduct}
1268 methods provide a uniform interface to common proof techniques over
1269 datatypes, inductive predicates (or sets), recursive functions etc.
1270 The corresponding rules may be specified and instantiated in a
1271 casual manner. Furthermore, these methods provide named local
1272 contexts that may be invoked via the @{command "case"} proof command
1273 within the subsequent proof text. This accommodates compact proof
1274 texts even when reasoning about large specifications.
1276 The @{method induct} method also provides some additional
1277 infrastructure in order to be applicable to structure statements
1278 (either using explicit meta-level connectives, or including facts
1279 and parameters separately). This avoids cumbersome encoding of
1280 ``strengthened'' inductive statements within the object-logic.
1282 Method @{method induction} differs from @{method induct} only in
1283 the names of the facts in the local context invoked by the @{command "case"}
1287 @@{method cases} ('(' 'no_simp' ')')? \\
1288 (@{syntax insts} * @'and') rule?
1290 (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
1292 @@{method coinduct} @{syntax insts} taking rule?
1295 rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
1297 definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}
1299 definsts: ( definst * )
1301 arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
1303 taking: 'taking' ':' @{syntax insts}
1308 \item @{method cases}~@{text "insts R"} applies method @{method
1309 rule} with an appropriate case distinction theorem, instantiated to
1310 the subjects @{text insts}. Symbolic case names are bound according
1311 to the rule's local contexts.
1313 The rule is determined as follows, according to the facts and
1314 arguments passed to the @{method cases} method:
1317 \begin{tabular}{llll}
1318 facts & & arguments & rule \\\hline
1319 & @{method cases} & & classical case split \\
1320 & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
1321 @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
1322 @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1326 Several instantiations may be given, referring to the \emph{suffix}
1327 of premises of the case rule; within each premise, the \emph{prefix}
1328 of variables is instantiated. In most situations, only a single
1329 term needs to be specified; this refers to the first variable of the
1330 last premise (it is usually the same for all cases). The @{text
1331 "(no_simp)"} option can be used to disable pre-simplification of
1332 cases (see the description of @{method induct} below for details).
1334 \item @{method induct}~@{text "insts R"} and
1335 @{method induction}~@{text "insts R"} are analogous to the
1336 @{method cases} method, but refer to induction rules, which are
1337 determined as follows:
1340 \begin{tabular}{llll}
1341 facts & & arguments & rule \\\hline
1342 & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\
1343 @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
1344 @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1348 Several instantiations may be given, each referring to some part of
1349 a mutual inductive definition or datatype --- only related partial
1350 induction rules may be used together, though. Any of the lists of
1351 terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables
1352 present in the induction rule. This enables the writer to specify
1353 only induction variables, or both predicates and variables, for
1356 Instantiations may be definitional: equations @{text "x \<equiv> t"}
1357 introduce local definitions, which are inserted into the claim and
1358 discharged after applying the induction rule. Equalities reappear
1359 in the inductive cases, but have been transformed according to the
1360 induction principle being involved here. In order to achieve
1361 practically useful induction hypotheses, some variables occurring in
1362 @{text t} need to be fixed (see below). Instantiations of the form
1363 @{text t}, where @{text t} is not a variable, are taken as a
1364 shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh
1365 variable. If this is not intended, @{text t} has to be enclosed in
1366 parentheses. By default, the equalities generated by definitional
1367 instantiations are pre-simplified using a specific set of rules,
1368 usually consisting of distinctness and injectivity theorems for
1369 datatypes. This pre-simplification may cause some of the parameters
1370 of an inductive case to disappear, or may even completely delete
1371 some of the inductive cases, if one of the equalities occurring in
1372 their premises can be simplified to @{text False}. The @{text
1373 "(no_simp)"} option can be used to disable pre-simplification.
1374 Additional rules to be used in pre-simplification can be declared
1375 using the @{attribute_def induct_simp} attribute.
1377 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
1378 specification generalizes variables @{text "x\<^sub>1, \<dots>,
1379 x\<^sub>m"} of the original goal before applying induction. One can
1380 separate variables by ``@{text "and"}'' to generalize them in other
1381 goals then the first. Thus induction hypotheses may become
1382 sufficiently general to get the proof through. Together with
1383 definitional instantiations, one may effectively perform induction
1384 over expressions of a certain structure.
1386 The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1387 specification provides additional instantiations of a prefix of
1388 pending variables in the rule. Such schematic induction rules
1389 rarely occur in practice, though.
1391 \item @{method coinduct}~@{text "inst R"} is analogous to the
1392 @{method induct} method, but refers to coinduction rules, which are
1393 determined as follows:
1396 \begin{tabular}{llll}
1397 goal & & arguments & rule \\\hline
1398 & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
1399 @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
1400 @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1403 Coinduction is the dual of induction. Induction essentially
1404 eliminates @{text "A x"} towards a generic result @{text "P x"},
1405 while coinduction introduces @{text "A x"} starting with @{text "B
1406 x"}, for a suitable ``bisimulation'' @{text B}. The cases of a
1407 coinduct rule are typically named after the predicates or sets being
1408 covered, while the conclusions consist of several alternatives being
1409 named after the individual destructor patterns.
1411 The given instantiation refers to the \emph{suffix} of variables
1412 occurring in the rule's major premise, or conclusion if unavailable.
1413 An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1414 specification may be required in order to specify the bisimulation
1415 to be used in the coinduction step.
1419 Above methods produce named local contexts, as determined by the
1420 instantiated rule as given in the text. Beyond that, the @{method
1421 induct} and @{method coinduct} methods guess further instantiations
1422 from the goal specification itself. Any persisting unresolved
1423 schematic variables of the resulting rule will render the the
1424 corresponding case invalid. The term binding @{variable ?case} for
1425 the conclusion will be provided with each case, provided that term
1428 The @{command "print_cases"} command prints all named cases present
1429 in the current proof state.
1431 \medskip Despite the additional infrastructure, both @{method cases}
1432 and @{method coinduct} merely apply a certain rule, after
1433 instantiation, while conforming due to the usual way of monotonic
1434 natural deduction: the context of a structured statement @{text
1435 "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}
1436 reappears unchanged after the case split.
1438 The @{method induct} method is fundamentally different in this
1439 respect: the meta-level structure is passed through the
1440 ``recursive'' course involved in the induction. Thus the original
1441 statement is basically replaced by separate copies, corresponding to
1442 the induction hypotheses and conclusion; the original goal context
1443 is no longer available. Thus local assumptions, fixed parameters
1444 and definitions effectively participate in the inductive rephrasing
1445 of the original statement.
1447 In @{method induct} proofs, local assumptions introduced by cases are split
1448 into two different kinds: @{text hyps} stemming from the rule and
1449 @{text prems} from the goal statement. This is reflected in the
1450 extracted cases accordingly, so invoking ``@{command "case"}~@{text
1451 c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
1452 as well as fact @{text c} to hold the all-inclusive list.
1454 In @{method induction} proofs, local assumptions introduced by cases are
1455 split into three different kinds: @{text IH}, the induction hypotheses,
1456 @{text hyps}, the remaining hypotheses stemming from the rule, and
1457 @{text prems}, the assumptions from the goal statement. The names are
1458 @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
1461 \medskip Facts presented to either method are consumed according to
1462 the number of ``major premises'' of the rule involved, which is
1463 usually 0 for plain cases and induction rules of datatypes etc.\ and
1464 1 for rules of inductive predicates or sets and the like. The
1465 remaining facts are inserted into the goal verbatim before the
1466 actual @{text cases}, @{text induct}, or @{text coinduct} rule is
1471 subsection {* Declaring rules *}
1474 \begin{matharray}{rcl}
1475 @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
1476 @{attribute_def cases} & : & @{text attribute} \\
1477 @{attribute_def induct} & : & @{text attribute} \\
1478 @{attribute_def coinduct} & : & @{text attribute} \\
1482 @@{attribute cases} spec
1484 @@{attribute induct} spec
1486 @@{attribute coinduct} spec
1489 spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
1494 \item @{command "print_induct_rules"} prints cases and induct rules
1495 for predicates (or sets) and types of the current context.
1497 \item @{attribute cases}, @{attribute induct}, and @{attribute
1498 coinduct} (as attributes) declare rules for reasoning about
1499 (co)inductive predicates (or sets) and types, using the
1500 corresponding methods of the same name. Certain definitional
1501 packages of object-logics usually declare emerging cases and
1502 induction rules as expected, so users rarely need to intervene.
1504 Rules may be deleted via the @{text "del"} specification, which
1505 covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
1506 sub-categories simultaneously. For example, @{attribute
1507 cases}~@{text del} removes any @{attribute cases} rules declared for
1508 some type, predicate, or set.
1510 Manual rule declarations usually refer to the @{attribute
1511 case_names} and @{attribute params} attributes to adjust names of
1512 cases and parameters of a rule; the @{attribute consumes}
1513 declaration is taken care of automatically: @{attribute
1514 consumes}~@{text 0} is specified for ``type'' rules and @{attribute
1515 consumes}~@{text 1} for ``predicate'' / ``set'' rules.