10 Proof commands perform transitions of Isar/VM machine
11 configurations, which are block-structured, consisting of a stack of
12 nodes with three main components: logical proof context, current
13 facts, and open goals. Isar/VM transitions are \emph{typed}
14 according to the following three different modes of operation:
18 \item [@{text "proof(prove)"}] means that a new goal has just been
19 stated that is now to be \emph{proven}; the next command may refine
20 it by some proof method, and enter a sub-proof to establish the
23 \item [@{text "proof(state)"}] is like a nested theory mode: the
24 context may be augmented by \emph{stating} additional assumptions,
25 intermediate results etc.
27 \item [@{text "proof(chain)"}] is intermediate between @{text
28 "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
29 the contents of the special ``@{fact_ref this}'' register) have been
30 just picked up in order to be used when refining the goal claimed
35 The proof mode indicator may be read as a verb telling the writer
36 what kind of operation may be performed next. The corresponding
37 typings of proof commands restricts the shape of well-formed proof
38 texts to particular command sequences. So dynamic arrangements of
39 commands eventually turn out as static texts of a certain structure.
40 \Appref{ap:refcard} gives a simplified grammar of the overall
41 (extensible) language emerging that way.
45 section {* Statements *}
47 subsection {* Context elements \label{sec:proof-context} *}
50 \begin{matharray}{rcl}
51 @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
52 @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
53 @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
54 @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
57 The logical proof context consists of fixed variables and
58 assumptions. The former closely correspond to Skolem constants, or
59 meta-level universal quantification as provided by the Isabelle/Pure
60 logical framework. Introducing some \emph{arbitrary, but fixed}
61 variable via ``@{command "fix"}~@{text x}'' results in a local value
62 that may be used in the subsequent proof as any other variable or
63 constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
64 the context will be universally closed wrt.\ @{text x} at the
65 outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
66 form using Isabelle's meta-variables).
68 Similarly, introducing some assumption @{text \<chi>} has two effects.
69 On the one hand, a local theorem is created that may be used as a
70 fact in subsequent proof steps. On the other hand, any result
71 @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
72 the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
73 using such a result would basically introduce a new subgoal stemming
74 from the assumption. How this situation is handled depends on the
75 version of assumption command used: while @{command "assume"}
76 insists on solving the subgoal by unification with some premise of
77 the goal, @{command "presume"} leaves the subgoal unchanged in order
78 to be proved later by the user.
80 Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
81 t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
82 another version of assumption that causes any hypothetical equation
83 @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
84 exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
90 ('assume' | 'presume') (props + 'and')
94 def: thmdecl? \\ name ('==' | equiv) term termpat?
100 \item [@{command "fix"}~@{text x}] introduces a local variable
101 @{text x} that is \emph{arbitrary, but fixed.}
103 \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
104 "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
105 assumption. Subsequent results applied to an enclosing goal (e.g.\
106 by @{command_ref "show"}) are handled as follows: @{command
107 "assume"} expects to be able to unify with existing premises in the
108 goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
110 Several lists of assumptions may be given (separated by
111 @{keyword_ref "and"}; the resulting list of current facts consists
112 of all of these concatenated.
114 \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
115 (non-polymorphic) definition. In results exported from the context,
116 @{text x} is replaced by @{text t}. Basically, ``@{command
117 "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
118 x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
119 hypothetical equation solved by reflexivity.
121 The default name for the definitional equation is @{text x_def}.
122 Several simultaneous definitions may be given at the same time.
126 The special name @{fact_ref prems} refers to all assumptions of the
127 current context as a list of theorems. This feature should be used
128 with great care! It is better avoided in final proof texts.
132 subsection {* Term abbreviations \label{sec:term-abbrev} *}
135 \begin{matharray}{rcl}
136 @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
137 @{keyword_def "is"} & : & syntax \\
140 Abbreviations may be either bound by explicit @{command
141 "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
142 goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
143 p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
144 bind extra-logical term variables, which may be either named
145 schematic variables of the form @{text ?x}, or nameless dummies
146 ``@{variable _}'' (underscore). Note that in the @{command "let"}
147 form the patterns occur on the left-hand side, while the @{keyword
148 "is"} patterns are in postfix position.
150 Polymorphism of term bindings is handled in Hindley-Milner style,
151 similar to ML. Type variables referring to local assumptions or
152 open goal statements are \emph{fixed}, while those of finished
153 results or bound by @{command "let"} may occur in \emph{arbitrary}
154 instances later. Even though actual polymorphism should be rarely
155 used in practice, this mechanism is essential to achieve proper
156 incremental type-inference, as the user proceeds to build up the
157 Isar proof text from left to right.
159 \medskip Term abbreviations are quite different from local
160 definitions as introduced via @{command "def"} (see
161 \secref{sec:proof-context}). The latter are visible within the
162 logic as actual equations, while abbreviations disappear during the
163 input process just after type checking. Also note that @{command
164 "def"} does not support polymorphism.
167 'let' ((term + 'and') '=' term + 'and')
171 The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
172 or \railnonterm{proppat} (see \secref{sec:term-decls}).
176 \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
177 p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
178 "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
179 against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
181 \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
182 "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
183 preceding statement. Also note that @{keyword "is"} is not a
184 separate command, but part of others (such as @{command "assume"},
185 @{command "have"} etc.).
189 Some \emph{implicit} term abbreviations\index{term abbreviations}
190 for goals and facts are available as well. For any open goal,
191 @{variable_ref thesis} refers to its object-level statement,
192 abstracted over any meta-level parameters (if present). Likewise,
193 @{variable_ref this} is bound for fact statements resulting from
194 assumptions or finished goals. In case @{variable this} refers to
195 an object-logic statement that is an application @{text "f t"}, then
196 @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
197 (three dots). The canonical application of this convenience are
198 calculational proofs (see \secref{sec:calculation}).
202 subsection {* Facts and forward chaining *}
205 \begin{matharray}{rcl}
206 @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
207 @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
208 @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
209 @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
210 @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
211 @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
214 New facts are established either by assumption or proof of local
215 statements. Any fact will usually be involved in further proofs,
216 either as explicit arguments of proof methods, or when forward
217 chaining towards the next goal via @{command "then"} (and variants);
218 @{command "from"} and @{command "with"} are composite forms
219 involving @{command "note"}. The @{command "using"} elements
220 augments the collection of used facts \emph{after} a goal has been
221 stated. Note that the special theorem name @{fact_ref this} refers
222 to the most recently established facts, but only \emph{before}
223 issuing a follow-up claim.
226 'note' (thmdef? thmrefs + 'and')
228 ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
234 \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
235 recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
236 the result as @{text a}. Note that attributes may be involved as
237 well, both on the left and right hand sides.
239 \item [@{command "then"}] indicates forward chaining by the current
240 facts in order to establish the goal to be claimed next. The
241 initial proof method invoked to refine that will be offered the
242 facts to do ``anything appropriate'' (see also
243 \secref{sec:proof-steps}). For example, method @{method_ref rule}
244 (see \secref{sec:pure-meth-att}) would typically do an elimination
245 rather than an introduction. Automatic methods usually insert the
246 facts into the goal state before operation. This provides a simple
247 scheme to control relevance of facts in automated proof search.
249 \item [@{command "from"}~@{text b}] abbreviates ``@{command
250 "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
251 equivalent to ``@{command "from"}~@{text this}''.
253 \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
254 abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
255 this"}''; thus the forward chaining is from earlier facts together
256 with the current ones.
258 \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
259 the facts being currently indicated for use by a subsequent
260 refinement step (such as @{command_ref "apply"} or @{command_ref
263 \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
264 structurally similar to @{command "using"}, but unfolds definitional
265 equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
270 Forward chaining with an empty list of theorems is the same as not
271 chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
272 effect apart from entering @{text "prove(chain)"} mode, since
273 @{fact_ref nothing} is bound to the empty list of theorems.
275 Basic proof methods (such as @{method_ref rule}) expect multiple
276 facts to be given in their proper order, corresponding to a prefix
277 of the premises of the rule involved. Note that positions may be
278 easily skipped using something like @{command "from"}~@{text "_
279 \<AND> a \<AND> b"}, for example. This involves the trivial rule
280 @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
281 ``@{fact_ref "_"}'' (underscore).
283 Automated methods (such as @{method simp} or @{method auto}) just
284 insert any given facts before their usual operation. Depending on
285 the kind of procedure involved, the order of facts is less
290 subsection {* Goals \label{sec:goals} *}
293 \begin{matharray}{rcl}
294 @{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
295 @{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
296 @{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
297 @{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
298 @{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
299 @{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
300 @{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
301 @{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
304 From a theory context, proof mode is entered by an initial goal
305 command such as @{command "lemma"}, @{command "theorem"}, or
306 @{command "corollary"}. Within a proof, new claims may be
307 introduced locally as well; four variants are available here to
308 indicate whether forward chaining of facts should be performed
309 initially (via @{command_ref "then"}), and whether the final result
310 is meant to solve some pending goal.
312 Goals may consist of multiple statements, resulting in a list of
313 facts eventually. A pending multi-goal is internally represented as
314 a meta-level conjunction (printed as @{text "&&"}), which is usually
315 split into the corresponding number of sub-goals prior to an initial
316 method application, via @{command_ref "proof"}
317 (\secref{sec:proof-steps}) or @{command_ref "apply"}
318 (\secref{sec:tactic-commands}). The @{method_ref induct} method
319 covered in \secref{sec:cases-induct} acts on multiple claims
322 Claims at the theory level may be either in short or long form. A
323 short goal merely consists of several simultaneous propositions
324 (often just one). A long goal includes an explicit context
325 specification for the subsequent conclusion, involving local
326 parameters and assumptions. Here the role of each part of the
327 statement is explicitly marked by separate keywords (see also
328 \secref{sec:locale}); the local assumptions being introduced here
329 are available as @{fact_ref assms} in the proof. Moreover, there
330 are two kinds of conclusions: @{element_def "shows"} states several
331 simultaneous propositions (essentially a big conjunction), while
332 @{element_def "obtains"} claims several simultaneous simultaneous
333 contexts of (essentially a big disjunction of eliminated parameters
334 and assumptions, cf.\ \secref{sec:obtain}).
337 ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
339 ('have' | 'show' | 'hence' | 'thus') goal
341 'print\_statement' modes? thmrefs
344 goal: (props + 'and')
346 longgoal: thmdecl? (contextelem *) conclusion
348 conclusion: 'shows' goal | 'obtains' (parname? case + '|')
350 case: (vars + 'and') 'where' (props + 'and')
356 \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
357 @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
358 \<phi>"} to be put back into the target context. An additional
359 \railnonterm{context} specification may build up an initial proof
360 context for the subsequent claim; this includes local definitions
361 and syntax as well, see the definition of @{syntax contextelem} in
364 \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
365 "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
366 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
367 being of a different kind. This discrimination acts like a formal
370 \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
371 eventually resulting in a fact within the current logical context.
372 This operation is completely independent of any pending sub-goals of
373 an enclosing goal statements, so @{command "have"} may be freely
374 used for experimental exploration of potential results within a
377 \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
378 "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
379 sub-goal for each one of the finished result, after having been
380 exported into the corresponding context (at the head of the
381 sub-proof of this @{command "show"} command).
383 To accommodate interactive debugging, resulting rules are printed
384 before being applied internally. Even more, interactive execution
385 of @{command "show"} predicts potential failure and displays the
386 resulting error as a warning beforehand. Watch out for the
389 %FIXME proper antiquitation
391 Problem! Local statement will fail to solve any pending goal
394 \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
395 "have"}'', i.e.\ claims a local goal to be proven by forward
396 chaining the current facts. Note that @{command "hence"} is also
397 equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
399 \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
400 "show"}''. Note that @{command "thus"} is also equivalent to
401 ``@{command "from"}~@{text this}~@{command "show"}''.
403 \item [@{command "print_statement"}~@{text a}] prints facts from the
404 current theory or proof context in long statement form, according to
405 the syntax for @{command "lemma"} given above.
409 Any goal statement causes some term abbreviations (such as
410 @{variable_ref "?thesis"}) to be bound automatically, see also
411 \secref{sec:term-abbrev}.
413 The optional case names of @{element_ref "obtains"} have a twofold
414 meaning: (1) during the of this claim they refer to the the local
415 context introductions, (2) the resulting rule is annotated
416 accordingly to support symbolic case splits when used with the
417 @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
422 Isabelle/Isar suffers theory-level goal statements to contain
423 \emph{unbound schematic variables}, although this does not conform
424 to the aim of human-readable proof documents! The main problem
425 with schematic goals is that the actual outcome is usually hard to
426 predict, depending on the behavior of the proof methods applied
427 during the course of reasoning. Note that most semi-automated
428 methods heavily depend on several kinds of implicit rule
429 declarations within the current theory context. As this would
430 also result in non-compositional checking of sub-proofs,
431 \emph{local goals} are not allowed to be schematic at all.
432 Nevertheless, schematic goals do have their use in Prolog-style
433 interactive synthesis of proven results, usually by stepwise
434 refinement via emulation of traditional Isabelle tactic scripts
435 (see also \secref{sec:tactic-commands}). In any case, users
436 should know what they are doing.
441 section {* Refinement steps *}
443 subsection {* Proof method expressions \label{sec:proof-meth} *}
446 Proof methods are either basic ones, or expressions composed of
447 methods via ``@{verbatim ","}'' (sequential composition),
448 ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
449 (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
450 "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
451 sub-goals, with default @{text "n = 1"}). In practice, proof
452 methods are usually just a comma separated list of
453 \railqtok{nameref}~\railnonterm{args} specifications. Note that
454 parentheses may be dropped for single method specifications (with no
457 \indexouternonterm{method}
459 method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
461 methods: (nameref args | method) + (',' | '|')
465 Proper Isar proof methods do \emph{not} admit arbitrary goal
466 addressing, but refer either to the first sub-goal or all sub-goals
467 uniformly. The goal restriction operator ``@{text "[n]"}''
468 evaluates a method expression within a sandbox consisting of the
469 first @{text n} sub-goals (which need to exist). For example, the
470 method ``@{text "simp_all[3]"}'' simplifies the first three
471 sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
472 new goals that emerge from applying rule @{text "foo"} to the
473 originally first one.
475 Improper methods, notably tactic emulations, offer a separate
476 low-level goal addressing scheme as explicit argument to the
477 individual tactic being involved. Here ``@{text "[!]"}'' refers to
478 all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
481 \indexouternonterm{goalspec}
483 goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
489 subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
492 \begin{matharray}{rcl}
493 @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
494 @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
495 @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
496 @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
497 @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
498 @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
501 Arbitrary goal refinement via tactics is considered harmful.
502 Structured proof composition in Isar admits proof methods to be
503 invoked in two places only.
507 \item An \emph{initial} refinement step @{command_ref
508 "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
509 of sub-goals that are to be solved later. Facts are passed to
510 @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
511 "proof(chain)"} mode.
513 \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
514 "m\<^sub>2"} is intended to solve remaining goals. No facts are
515 passed to @{text "m\<^sub>2"}.
519 The only other (proper) way to affect pending goals in a proof body
520 is by @{command_ref "show"}, which involves an explicit statement of
521 what is to be solved eventually. Thus we avoid the fundamental
522 problem of unstructured tactic scripts that consist of numerous
523 consecutive goal transformations, with invisible effects.
525 \medskip As a general rule of thumb for good proof style, initial
526 proof methods should either solve the goal completely, or constitute
527 some well-understood reduction to new sub-goals. Arbitrary
528 automatic proof tools that are prone leave a large number of badly
529 structured sub-goals are no help in continuing the proof document in
530 an intelligible manner.
532 Unless given explicitly by the user, the default initial method is
533 ``@{method_ref rule}'', which applies a single standard elimination
534 or introduction rule according to the topmost symbol involved.
535 There is no separate default terminal method. Any remaining goals
536 are always solved by assumption in the very last step.
545 ('.' | '..' | 'sorry')
551 \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
552 proof method @{text "m\<^sub>1"}; facts for forward chaining are
553 passed if so indicated by @{text "proof(chain)"} mode.
555 \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
556 goals by proof method @{text "m\<^sub>2"} and concludes the
557 sub-proof by assumption. If the goal had been @{text "show"} (or
558 @{text "thus"}), some pending sub-goal is solved as well by the rule
559 resulting from the result \emph{exported} into the enclosing goal
560 context. Thus @{text "qed"} may fail for two reasons: either @{text
561 "m\<^sub>2"} fails, or the resulting rule does not fit to any
562 pending goal\footnote{This includes any additional ``strong''
563 assumptions as introduced by @{command "assume"}.} of the enclosing
564 context. Debugging such a situation might involve temporarily
565 changing @{command "show"} into @{command "have"}, or weakening the
566 local context by replacing occurrences of @{command "assume"} by
567 @{command "presume"}.
569 \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
570 \emph{terminal proof}\index{proof!terminal}; it abbreviates
571 @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
572 "m\<^sub>2"}, but with backtracking across both methods. Debugging
573 an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
574 command can be done by expanding its definition; in many cases
575 @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
576 "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
579 \item [``@{command ".."}''] is a \emph{default
580 proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
583 \item [``@{command "."}''] is a \emph{trivial
584 proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
587 \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
588 pretending to solve the pending claim without further ado. This
589 only works in interactive development, or if the @{ML
590 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
591 proofs are not the real thing. Internally, each theorem container
592 is tainted by an oracle invocation, which is indicated as ``@{text
593 "[!]"}'' in the printed result.
595 The most important application of @{command "sorry"} is to support
596 experimentation and top-down proof development.
602 subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
605 The following proof methods and attributes refer to basic logical
606 operations of Isar. Further methods and attributes are provided by
607 several generic and object-logic specific tools and packages (see
608 \chref{ch:gen-tools} and \chref{ch:hol}).
610 \begin{matharray}{rcl}
611 @{method_def "-"} & : & \isarmeth \\
612 @{method_def "fact"} & : & \isarmeth \\
613 @{method_def "assumption"} & : & \isarmeth \\
614 @{method_def "this"} & : & \isarmeth \\
615 @{method_def "rule"} & : & \isarmeth \\
616 @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
617 @{attribute_def (Pure) "intro"} & : & \isaratt \\
618 @{attribute_def (Pure) "elim"} & : & \isaratt \\
619 @{attribute_def (Pure) "dest"} & : & \isaratt \\
620 @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
621 @{attribute_def "OF"} & : & \isaratt \\
622 @{attribute_def "of"} & : & \isaratt \\
623 @{attribute_def "where"} & : & \isaratt \\
631 'iprover' ('!' ?) (rulemod *)
633 rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
635 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
641 'of' insts ('concl' ':' insts)?
643 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
649 \item [``@{method "-"}'' (minus)] does nothing but insert the
650 forward chaining facts as premises into the goal. Note that command
651 @{command_ref "proof"} without any method actually performs a single
652 reduction step using the @{method_ref rule} method; thus a plain
653 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
654 "-"}'' rather than @{command "proof"} alone.
656 \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
657 some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
658 the current proof context) modulo unification of schematic type and
659 term variables. The rule structure is not taken into account, i.e.\
660 meta-level implication is considered atomic. This is the same
661 principle underlying literal facts (cf.\ \secref{sec:syn-att}):
662 ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
663 equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
664 "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
665 @{text "\<turnstile> \<phi>"} in the proof context.
667 \item [@{method assumption}] solves some goal by a single assumption
668 step. All given facts are guaranteed to participate in the
669 refinement; this means there may be only 0 or 1 in the first place.
670 Recall that @{command "qed"} (\secref{sec:proof-steps}) already
671 concludes any remaining sub-goals by assumption, so structured
672 proofs usually need not quote the @{method assumption} method at
675 \item [@{method this}] applies all of the current facts directly as
676 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
677 "by"}~@{text this}''.
679 \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
680 rule given as argument in backward manner; facts are used to reduce
681 the rule before applying it to the goal. Thus @{method rule}
682 without facts is plain introduction, while with facts it becomes
685 When no arguments are given, the @{method rule} method tries to pick
686 appropriate rules automatically, as declared in the current context
687 using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
688 @{attribute (Pure) dest} attributes (see below). This is the
689 default behavior of @{command "proof"} and ``@{command ".."}''
690 (double-dot) steps (see \secref{sec:proof-steps}).
692 \item [@{method iprover}] performs intuitionistic proof search,
693 depending on specifically declared rules from the context, or given
694 as explicit arguments. Chained facts are inserted into the goal
695 before commencing proof search; ``@{method iprover}@{text "!"}''
696 means to include the current @{fact prems} as well.
698 Rules need to be classified as @{attribute (Pure) intro},
699 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
700 ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
701 applied aggressively (without considering back-tracking later).
702 Rules declared with ``@{text "?"}'' are ignored in proof search (the
703 single-step @{method rule} method still observes these). An
704 explicit weight annotation may be given as well; otherwise the
705 number of rule premises will be taken into account here.
707 \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and
708 @{attribute (Pure) dest}] declare introduction, elimination, and
709 destruct rules, to be used with the @{method rule} and @{method
710 iprover} methods. Note that the latter will ignore rules declared
711 with ``@{text "?"}'', while ``@{text "!"}'' are used most
714 The classical reasoner (see \secref{sec:classical}) introduces its
715 own variants of these attributes; use qualified names to access the
716 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
719 \item [@{attribute rule}~@{text del}] undeclares introduction,
720 elimination, or destruct rules.
722 \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
723 theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
724 (in parallel). This corresponds to the @{ML "op MRS"} operation in
725 ML, but note the reversed order. Positions may be effectively
726 skipped by including ``@{text _}'' (underscore) as argument.
728 \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
729 positional instantiation of term variables. The terms @{text
730 "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
731 variables occurring in a theorem from left to right; ``@{text _}''
732 (underscore) indicates to skip a position. Arguments following a
733 ``@{text "concl:"}'' specification refer to positions of the
734 conclusion of a rule.
736 \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
737 x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
738 type and term variables occurring in a theorem. Schematic variables
739 have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
740 The question mark may be omitted if the variable name is a plain
741 identifier without index. As type instantiations are inferred from
742 term instantiations, explicit type instantiations are seldom
749 subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
752 The Isar provides separate commands to accommodate tactic-style
753 proof scripts within the same system. While being outside the
754 orthodox Isar proof language, these might come in handy for
755 interactive exploration and debugging, or even actual tactical proof
756 within new-style theories (to benefit from document preparation, for
757 example). See also \secref{sec:tactics} for actual tactics, that
758 have been encapsulated as proof methods. Proper proof methods may
759 be used in scripts, too.
761 \begin{matharray}{rcl}
762 @{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
763 @{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
764 @{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
765 @{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
766 @{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
767 @{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
771 ( 'apply' | 'apply\_end' ) method
781 \item [@{command "apply"}~@{text m}] applies proof method @{text m}
782 in initial position, but unlike @{command "proof"} it retains
783 ``@{text "proof(prove)"}'' mode. Thus consecutive method
784 applications may be given just as in tactic scripts.
786 Facts are passed to @{text m} as indicated by the goal's
787 forward-chain mode, and are \emph{consumed} afterwards. Thus any
788 further @{command "apply"} command would always work in a purely
791 \item [@{command "apply_end"}~@{text "m"}] applies proof method
792 @{text m} as if in terminal position. Basically, this simulates a
793 multi-step tactic script for @{command "qed"}, but may be given
794 anywhere within the proof body.
796 No facts are passed to @{text m} here. Furthermore, the static
797 context is that of the enclosing goal (as for actual @{command
798 "qed"}). Thus the proof method may not refer to any assumptions
799 introduced in the current body, for example.
801 \item [@{command "done"}] completes a proof script, provided that
802 the current goal state is solved completely. Note that actual
803 structured proof commands (e.g.\ ``@{command "."}'' or @{command
804 "sorry"}) may be used to conclude proof scripts as well.
806 \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
807 n}] shuffle the list of pending goals: @{command "defer"} puts off
808 sub-goal @{text n} to the end of the list (@{text "n = 1"} by
809 default), while @{command "prefer"} brings sub-goal @{text n} to the
812 \item [@{command "back"}] does back-tracking over the result
813 sequence of the latest proof command. Basically, any proof command
814 may return multiple results.
818 Any proper Isar proof method may be used with tactic script commands
819 such as @{command "apply"}. A few additional emulations of actual
820 tactics are provided as well; these would be never used in actual
821 structured proofs, of course.
825 section {* Block structure *}
828 \begin{matharray}{rcl}
829 @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
830 @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
831 @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
834 While Isar is inherently block-structured, opening and closing
835 blocks is mostly handled rather casually, with little explicit
836 user-intervention. Any local goal statement automatically opens
837 \emph{two} internal blocks, which are closed again when concluding
838 the sub-proof (by @{command "qed"} etc.). Sections of different
839 context within a sub-proof may be switched via @{command "next"},
840 which is just a single block-close followed by block-open again.
841 The effect of @{command "next"} is to reset the local proof context;
842 there is no goal focus involved here!
844 For slightly more advanced applications, there are explicit block
845 parentheses as well. These typically achieve a stronger forward
850 \item [@{command "next"}] switches to a fresh block within a
851 sub-proof, resetting the local context to the initial one.
853 \item [@{command "{"} and @{command "}"}] explicitly open and close
854 blocks. Any current facts pass through ``@{command "{"}''
855 unchanged, while ``@{command "}"}'' causes any result to be
856 \emph{exported} into the enclosing context. Thus fixed variables
857 are generalized, assumptions discharged, and local definitions
858 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
859 of @{command "assume"} and @{command "presume"} in this mode of
860 forward reasoning --- in contrast to plain backward reasoning with
861 the result exported at @{command "show"} time.
867 section {* Omitting proofs *}
870 \begin{matharray}{rcl}
871 @{command_def "oops"} & : & \isartrans{proof}{theory} \\
874 The @{command "oops"} command discontinues the current proof
875 attempt, while considering the partial proof text as properly
876 processed. This is conceptually quite different from ``faking''
877 actual proofs via @{command_ref "sorry"} (see
878 \secref{sec:proof-steps}): @{command "oops"} does not observe the
879 proof structure at all, but goes back right to the theory level.
880 Furthermore, @{command "oops"} does not produce any result theorem
881 --- there is no intended claim to be able to complete the proof
884 A typical application of @{command "oops"} is to explain Isar proofs
885 \emph{within} the system itself, in conjunction with the document
886 preparation tools of Isabelle described in \cite{isabelle-sys}.
887 Thus partial or even wrong proof attempts can be discussed in a
888 logically sound manner. Note that the Isabelle {\LaTeX} macros can
889 be easily adapted to print something like ``@{text "\<dots>"}'' instead of
890 the keyword ``@{command "oops"}''.
892 \medskip The @{command "oops"} command is undo-able, unlike
893 @{command_ref "kill"} (see \secref{sec:history}). The effect is to
894 get back to the theory just before the opening of the proof.
898 section {* Generalized elimination \label{sec:obtain} *}
901 \begin{matharray}{rcl}
902 @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
903 @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
906 Generalized elimination means that additional elements with certain
907 properties may be introduced in the current context, by virtue of a
908 locally proven ``soundness statement''. Technically speaking, the
909 @{command "obtain"} language element is like a declaration of
910 @{command "fix"} and @{command "assume"} (see also see
911 \secref{sec:proof-context}), together with a soundness proof of its
912 additional claim. According to the nature of existential reasoning,
913 assumptions get eliminated from any result exported from the context
914 later, provided that the corresponding parameters do \emph{not}
915 occur in the conclusion.
918 'obtain' parname? (vars + 'and') 'where' (props + 'and')
920 'guess' (vars + 'and')
924 The derived Isar command @{command "obtain"} is defined as follows
925 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
926 facts indicated for forward chaining).
928 @{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]
929 \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"} \\
930 \quad @{command "proof"}~@{text succeed} \\
931 \qquad @{command "fix"}~@{text thesis} \\
932 \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"} \\
933 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
934 \quad\qquad @{command "apply"}~@{text -} \\
935 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
936 \quad @{command "qed"} \\
937 \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
940 Typically, the soundness proof is relatively straight-forward, often
941 just by canonical automated tools such as ``@{command "by"}~@{text
942 simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
943 ``@{text that}'' reduction above is declared as simplification and
946 In a sense, @{command "obtain"} represents at the level of Isar
947 proofs what would be meta-logical existential quantifiers and
948 conjunctions. This concept has a broad range of useful
949 applications, ranging from plain elimination (or introduction) of
950 object-level existential and conjunctions, to elimination over
951 results of symbolic evaluation of recursive definitions, for
952 example. Also note that @{command "obtain"} without parameters acts
953 much like @{command "have"}, where the result is treated as a
956 An alternative name to be used instead of ``@{text that}'' above may
957 be given in parentheses.
959 \medskip The improper variant @{command "guess"} is similar to
960 @{command "obtain"}, but derives the obtained statement from the
961 course of reasoning! The proof starts with a fixed goal @{text
962 thesis}. The subsequent proof may refine this to anything of the
963 form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
964 \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
965 final goal state is then used as reduction rule for the obtain
966 scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
967 x\<^sub>m"} are marked as internal by default, which prevents the
968 proof context from being polluted by ad-hoc variables. The variable
969 names and type constraints given as arguments for @{command "guess"}
970 specify a prefix of obtained parameters explicitly in the text.
972 It is important to note that the facts introduced by @{command
973 "obtain"} and @{command "guess"} may not be polymorphic: any
974 type-variables occurring here are fixed in the present context!
978 section {* Calculational reasoning \label{sec:calculation} *}
981 \begin{matharray}{rcl}
982 @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
983 @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
984 @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
985 @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
986 @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
987 @{attribute trans} & : & \isaratt \\
988 @{attribute sym} & : & \isaratt \\
989 @{attribute symmetric} & : & \isaratt \\
992 Calculational proof is forward reasoning with implicit application
993 of transitivity rules (such those of @{text "="}, @{text "\<le>"},
994 @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
995 @{fact_ref calculation} for accumulating results obtained by
996 transitivity composed with the current result. Command @{command
997 "also"} updates @{fact calculation} involving @{fact this}, while
998 @{command "finally"} exhibits the final @{fact calculation} by
999 forward chaining towards the next goal statement. Both commands
1000 require valid current facts, i.e.\ may occur only after commands
1001 that produce theorems such as @{command "assume"}, @{command
1002 "note"}, or some finished proof of @{command "have"}, @{command
1003 "show"} etc. The @{command "moreover"} and @{command "ultimately"}
1004 commands are similar to @{command "also"} and @{command "finally"},
1005 but only collect further results in @{fact calculation} without
1006 applying any rules yet.
1008 Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
1009 its canonical application with calculational proofs. It refers to
1010 the argument of the preceding statement. (The argument of a curried
1011 infix expression happens to be its right-hand side.)
1013 Isabelle/Isar calculations are implicitly subject to block structure
1014 in the sense that new threads of calculational reasoning are
1015 commenced for any new block (as opened by a local goal, for
1016 example). This means that, apart from being able to nest
1017 calculations, there is no separate \emph{begin-calculation} command
1020 \medskip The Isar calculation proof commands may be defined as
1021 follows:\footnote{We suppress internal bookkeeping such as proper
1022 handling of block-structure.}
1024 \begin{matharray}{rcl}
1025 @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
1026 @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
1027 @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
1028 @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
1029 @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
1033 ('also' | 'finally') ('(' thmrefs ')')?
1035 'trans' (() | 'add' | 'del')
1041 \item [@{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
1042 maintains the auxiliary @{fact calculation} register as follows.
1043 The first occurrence of @{command "also"} in some calculational
1044 thread initializes @{fact calculation} by @{fact this}. Any
1045 subsequent @{command "also"} on the same level of block-structure
1046 updates @{fact calculation} by some transitivity rule applied to
1047 @{fact calculation} and @{fact this} (in that order). Transitivity
1048 rules are picked from the current context, unless alternative rules
1049 are given as explicit arguments.
1051 \item [@{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
1052 maintaining @{fact calculation} in the same way as @{command
1053 "also"}, and concludes the current calculational thread. The final
1054 result is exhibited as fact for forward chaining towards the next
1055 goal. Basically, @{command "finally"} just abbreviates @{command
1056 "also"}~@{command "from"}~@{fact calculation}. Typical idioms for
1057 concluding calculational proofs are ``@{command "finally"}~@{command
1058 "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
1059 "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
1061 \item [@{command "moreover"} and @{command "ultimately"}] are
1062 analogous to @{command "also"} and @{command "finally"}, but collect
1063 results only, without applying rules.
1065 \item [@{command "print_trans_rules"}] prints the list of
1066 transitivity rules (for calculational commands @{command "also"} and
1067 @{command "finally"}) and symmetry rules (for the @{attribute
1068 symmetric} operation and single step elimination patters) of the
1071 \item [@{attribute trans}] declares theorems as transitivity rules.
1073 \item [@{attribute sym}] declares symmetry rules, as well as
1074 @{attribute "Pure.elim"}@{text "?"} rules.
1076 \item [@{attribute symmetric}] resolves a theorem with some rule
1077 declared as @{attribute sym} in the current context. For example,
1078 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
1079 swapped fact derived from that assumption.
1081 In structured proof texts it is often more appropriate to use an
1082 explicit single-step elimination proof, such as ``@{command
1083 "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
1084 "y = x"}~@{command ".."}''.
1090 section {* Proof by cases and induction \label{sec:cases-induct} *}
1092 subsection {* Rule contexts *}
1095 \begin{matharray}{rcl}
1096 @{command_def "case"} & : & \isartrans{proof(state)}{proof(state)} \\
1097 @{command_def "print_cases"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
1098 @{attribute_def case_names} & : & \isaratt \\
1099 @{attribute_def case_conclusion} & : & \isaratt \\
1100 @{attribute_def params} & : & \isaratt \\
1101 @{attribute_def consumes} & : & \isaratt \\
1104 The puristic way to build up Isar proof contexts is by explicit
1105 language elements like @{command "fix"}, @{command "assume"},
1106 @{command "let"} (see \secref{sec:proof-context}). This is adequate
1107 for plain natural deduction, but easily becomes unwieldy in concrete
1108 verification tasks, which typically involve big induction rules with
1111 The @{command "case"} command provides a shorthand to refer to a
1112 local context symbolically: certain proof methods provide an
1113 environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
1114 x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
1115 "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
1116 "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
1117 \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably
1118 @{variable ?case} for the main conclusion.
1120 By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
1121 a case value is marked as hidden, i.e.\ there is no way to refer to
1122 such parameters in the subsequent proof text. After all, original
1123 rule parameters stem from somewhere outside of the current proof
1124 text. By using the explicit form ``@{command "case"}~@{text "(c
1125 y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to
1126 chose local names that fit nicely into the current context.
1128 \medskip It is important to note that proper use of @{command
1129 "case"} does not provide means to peek at the current goal state,
1130 which is not directly observable in Isar! Nonetheless, goal
1131 refinement commands do provide named cases @{text "goal\<^sub>i"}
1132 for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.
1133 Using this extra feature requires great care, because some bits of
1134 the internal tactical machinery intrude the proof text. In
1135 particular, parameter names stemming from the left-over of automated
1136 reasoning tools are usually quite unpredictable.
1138 Under normal circumstances, the text of cases emerge from standard
1139 elimination or induction rules, which in turn are derived from
1140 previous theory specifications in a canonical way (say from
1141 @{command "inductive"} definitions).
1143 \medskip Proper cases are only available if both the proof method
1144 and the rules involved support this. By using appropriate
1145 attributes, case names, conclusions, and parameters may be also
1146 declared by hand. Thus variant versions of rules that have been
1147 derived manually become ready to use in advanced case analysis
1151 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1153 caseref: nameref attributes?
1156 'case\_names' (name +)
1158 'case\_conclusion' name (name *)
1160 'params' ((name *) + 'and')
1168 \item [@{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"}]
1169 invokes a named local context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m,
1170 \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an appropriate
1171 proof method (such as @{method_ref cases} and @{method_ref induct}).
1172 The command ``@{command "case"}~@{text "(c x\<^sub>1 \<dots>
1173 x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
1174 x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
1177 \item [@{command "print_cases"}] prints all local contexts of the
1178 current state, using Isar proof language notation.
1180 \item [@{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"}]
1181 declares names for the local contexts of premises of a theorem;
1182 @{text "c\<^sub>1, \<dots>, c\<^sub>k"} refers to the \emph{suffix} of the
1185 \item [@{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots>
1186 d\<^sub>k"}] declares names for the conclusions of a named premise
1187 @{text c}; here @{text "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the
1188 prefix of arguments of a logical formula built by nesting a binary
1189 connective (e.g.\ @{text "\<or>"}).
1191 Note that proof methods such as @{method induct} and @{method
1192 coinduct} already provide a default name for the conclusion as a
1193 whole. The need to name subformulas only arises with cases that
1194 split into several sub-cases, as in common co-induction rules.
1196 \item [@{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots>
1197 q\<^sub>1 \<dots> q\<^sub>n"}] renames the innermost parameters of
1198 premises @{text "1, \<dots>, n"} of some theorem. An empty list of names
1199 may be given to skip positions, leaving the present parameters
1202 Note that the default usage of case rules does \emph{not} directly
1203 expose parameters to the proof context.
1205 \item [@{attribute consumes}~@{text n}] declares the number of
1206 ``major premises'' of a rule, i.e.\ the number of facts to be
1207 consumed when it is applied by an appropriate proof method. The
1208 default value of @{attribute consumes} is @{text "n = 1"}, which is
1209 appropriate for the usual kind of cases and induction rules for
1210 inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
1211 @{attribute consumes} declaration given are treated as if
1212 @{attribute consumes}~@{text 0} had been specified.
1214 Note that explicit @{attribute consumes} declarations are only
1215 rarely needed; this is already taken care of automatically by the
1216 higher-level @{attribute cases}, @{attribute induct}, and
1217 @{attribute coinduct} declarations.
1223 subsection {* Proof methods *}
1226 \begin{matharray}{rcl}
1227 @{method_def cases} & : & \isarmeth \\
1228 @{method_def induct} & : & \isarmeth \\
1229 @{method_def coinduct} & : & \isarmeth \\
1232 The @{method cases}, @{method induct}, and @{method coinduct}
1233 methods provide a uniform interface to common proof techniques over
1234 datatypes, inductive predicates (or sets), recursive functions etc.
1235 The corresponding rules may be specified and instantiated in a
1236 casual manner. Furthermore, these methods provide named local
1237 contexts that may be invoked via the @{command "case"} proof command
1238 within the subsequent proof text. This accommodates compact proof
1239 texts even when reasoning about large specifications.
1241 The @{method induct} method also provides some additional
1242 infrastructure in order to be applicable to structure statements
1243 (either using explicit meta-level connectives, or including facts
1244 and parameters separately). This avoids cumbersome encoding of
1245 ``strengthened'' inductive statements within the object-logic.
1248 'cases' (insts * 'and') rule?
1250 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
1252 'coinduct' insts taking rule?
1255 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
1257 definst: name ('==' | equiv) term | inst
1259 definsts: ( definst *)
1261 arbitrary: 'arbitrary' ':' ((term *) 'and' +)
1263 taking: 'taking' ':' insts
1269 \item [@{method cases}~@{text "insts R"}] applies method @{method
1270 rule} with an appropriate case distinction theorem, instantiated to
1271 the subjects @{text insts}. Symbolic case names are bound according
1272 to the rule's local contexts.
1274 The rule is determined as follows, according to the facts and
1275 arguments passed to the @{method cases} method:
1278 \begin{tabular}{llll}
1279 facts & & arguments & rule \\\hline
1280 & @{method cases} & & classical case split \\
1281 & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
1282 @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
1283 @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1287 Several instantiations may be given, referring to the \emph{suffix}
1288 of premises of the case rule; within each premise, the \emph{prefix}
1289 of variables is instantiated. In most situations, only a single
1290 term needs to be specified; this refers to the first variable of the
1291 last premise (it is usually the same for all cases).
1293 \item [@{method induct}~@{text "insts R"}] is analogous to the
1294 @{method cases} method, but refers to induction rules, which are
1295 determined as follows:
1298 \begin{tabular}{llll}
1299 facts & & arguments & rule \\\hline
1300 & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\
1301 @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
1302 @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1306 Several instantiations may be given, each referring to some part of
1307 a mutual inductive definition or datatype --- only related partial
1308 induction rules may be used together, though. Any of the lists of
1309 terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables
1310 present in the induction rule. This enables the writer to specify
1311 only induction variables, or both predicates and variables, for
1314 Instantiations may be definitional: equations @{text "x \<equiv> t"}
1315 introduce local definitions, which are inserted into the claim and
1316 discharged after applying the induction rule. Equalities reappear
1317 in the inductive cases, but have been transformed according to the
1318 induction principle being involved here. In order to achieve
1319 practically useful induction hypotheses, some variables occurring in
1320 @{text t} need to be fixed (see below).
1322 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
1323 specification generalizes variables @{text "x\<^sub>1, \<dots>,
1324 x\<^sub>m"} of the original goal before applying induction. Thus
1325 induction hypotheses may become sufficiently general to get the
1326 proof through. Together with definitional instantiations, one may
1327 effectively perform induction over expressions of a certain
1330 The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1331 specification provides additional instantiations of a prefix of
1332 pending variables in the rule. Such schematic induction rules
1333 rarely occur in practice, though.
1335 \item [@{method coinduct}~@{text "inst R"}] is analogous to the
1336 @{method induct} method, but refers to coinduction rules, which are
1337 determined as follows:
1340 \begin{tabular}{llll}
1341 goal & & arguments & rule \\\hline
1342 & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
1343 @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
1344 @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
1347 Coinduction is the dual of induction. Induction essentially
1348 eliminates @{text "A x"} towards a generic result @{text "P x"},
1349 while coinduction introduces @{text "A x"} starting with @{text "B
1350 x"}, for a suitable ``bisimulation'' @{text B}. The cases of a
1351 coinduct rule are typically named after the predicates or sets being
1352 covered, while the conclusions consist of several alternatives being
1353 named after the individual destructor patterns.
1355 The given instantiation refers to the \emph{suffix} of variables
1356 occurring in the rule's major premise, or conclusion if unavailable.
1357 An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
1358 specification may be required in order to specify the bisimulation
1359 to be used in the coinduction step.
1363 Above methods produce named local contexts, as determined by the
1364 instantiated rule as given in the text. Beyond that, the @{method
1365 induct} and @{method coinduct} methods guess further instantiations
1366 from the goal specification itself. Any persisting unresolved
1367 schematic variables of the resulting rule will render the the
1368 corresponding case invalid. The term binding @{variable ?case} for
1369 the conclusion will be provided with each case, provided that term
1372 The @{command "print_cases"} command prints all named cases present
1373 in the current proof state.
1375 \medskip Despite the additional infrastructure, both @{method cases}
1376 and @{method coinduct} merely apply a certain rule, after
1377 instantiation, while conforming due to the usual way of monotonic
1378 natural deduction: the context of a structured statement @{text
1379 "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}
1380 reappears unchanged after the case split.
1382 The @{method induct} method is fundamentally different in this
1383 respect: the meta-level structure is passed through the
1384 ``recursive'' course involved in the induction. Thus the original
1385 statement is basically replaced by separate copies, corresponding to
1386 the induction hypotheses and conclusion; the original goal context
1387 is no longer available. Thus local assumptions, fixed parameters
1388 and definitions effectively participate in the inductive rephrasing
1389 of the original statement.
1391 In induction proofs, local assumptions introduced by cases are split
1392 into two different kinds: @{text hyps} stemming from the rule and
1393 @{text prems} from the goal statement. This is reflected in the
1394 extracted cases accordingly, so invoking ``@{command "case"}~@{text
1395 c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
1396 as well as fact @{text c} to hold the all-inclusive list.
1398 \medskip Facts presented to either method are consumed according to
1399 the number of ``major premises'' of the rule involved, which is
1400 usually 0 for plain cases and induction rules of datatypes etc.\ and
1401 1 for rules of inductive predicates or sets and the like. The
1402 remaining facts are inserted into the goal verbatim before the
1403 actual @{text cases}, @{text induct}, or @{text coinduct} rule is
1408 subsection {* Declaring rules *}
1411 \begin{matharray}{rcl}
1412 @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1413 @{attribute_def cases} & : & \isaratt \\
1414 @{attribute_def induct} & : & \isaratt \\
1415 @{attribute_def coinduct} & : & \isaratt \\
1426 spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
1432 \item [@{command "print_induct_rules"}] prints cases and induct
1433 rules for predicates (or sets) and types of the current context.
1435 \item [@{attribute cases}, @{attribute induct}, and @{attribute
1436 coinduct}] (as attributes) declare rules for reasoning about
1437 (co)inductive predicates (or sets) and types, using the
1438 corresponding methods of the same name. Certain definitional
1439 packages of object-logics usually declare emerging cases and
1440 induction rules as expected, so users rarely need to intervene.
1442 Rules may be deleted via the @{text "del"} specification, which
1443 covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
1444 sub-categories simultaneously. For example, @{attribute
1445 cases}~@{text del} removes any @{attribute cases} rules declared for
1446 some type, predicate, or set.
1448 Manual rule declarations usually refer to the @{attribute
1449 case_names} and @{attribute params} attributes to adjust names of
1450 cases and parameters of a rule; the @{attribute consumes}
1451 declaration is taken care of automatically: @{attribute
1452 consumes}~@{text 0} is specified for ``type'' rules and @{attribute
1453 consumes}~@{text 1} for ``predicate'' / ``set'' rules.