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 {* Context elements \label{sec:proof-context} *}
48 \begin{matharray}{rcl}
49 @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
50 @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
51 @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
52 @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
55 The logical proof context consists of fixed variables and
56 assumptions. The former closely correspond to Skolem constants, or
57 meta-level universal quantification as provided by the Isabelle/Pure
58 logical framework. Introducing some \emph{arbitrary, but fixed}
59 variable via ``@{command "fix"}~@{text x}'' results in a local value
60 that may be used in the subsequent proof as any other variable or
61 constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
62 the context will be universally closed wrt.\ @{text x} at the
63 outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
64 form using Isabelle's meta-variables).
66 Similarly, introducing some assumption @{text \<chi>} has two effects.
67 On the one hand, a local theorem is created that may be used as a
68 fact in subsequent proof steps. On the other hand, any result
69 @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
70 the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
71 using such a result would basically introduce a new subgoal stemming
72 from the assumption. How this situation is handled depends on the
73 version of assumption command used: while @{command "assume"}
74 insists on solving the subgoal by unification with some premise of
75 the goal, @{command "presume"} leaves the subgoal unchanged in order
76 to be proved later by the user.
78 Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
79 t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
80 another version of assumption that causes any hypothetical equation
81 @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
82 exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
88 ('assume' | 'presume') (props + 'and')
92 def: thmdecl? \\ name ('==' | equiv) term termpat?
98 \item [@{command "fix"}~@{text x}] introduces a local variable
99 @{text x} that is \emph{arbitrary, but fixed.}
101 \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
102 "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
103 assumption. Subsequent results applied to an enclosing goal (e.g.\
104 by @{command_ref "show"}) are handled as follows: @{command
105 "assume"} expects to be able to unify with existing premises in the
106 goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
108 Several lists of assumptions may be given (separated by
109 @{keyword_ref "and"}; the resulting list of current facts consists
110 of all of these concatenated.
112 \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
113 (non-polymorphic) definition. In results exported from the context,
114 @{text x} is replaced by @{text t}. Basically, ``@{command
115 "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
116 x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
117 hypothetical equation solved by reflexivity.
119 The default name for the definitional equation is @{text x_def}.
120 Several simultaneous definitions may be given at the same time.
124 The special name @{fact_ref prems} refers to all assumptions of the
125 current context as a list of theorems. This feature should be used
126 with great care! It is better avoided in final proof texts.
130 section {* Facts and forward chaining *}
133 \begin{matharray}{rcl}
134 @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
135 @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
136 @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
137 @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
138 @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
139 @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
142 New facts are established either by assumption or proof of local
143 statements. Any fact will usually be involved in further proofs,
144 either as explicit arguments of proof methods, or when forward
145 chaining towards the next goal via @{command "then"} (and variants);
146 @{command "from"} and @{command "with"} are composite forms
147 involving @{command "note"}. The @{command "using"} elements
148 augments the collection of used facts \emph{after} a goal has been
149 stated. Note that the special theorem name @{fact_ref this} refers
150 to the most recently established facts, but only \emph{before}
151 issuing a follow-up claim.
154 'note' (thmdef? thmrefs + 'and')
156 ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
162 \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
163 recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
164 the result as @{text a}. Note that attributes may be involved as
165 well, both on the left and right hand sides.
167 \item [@{command "then"}] indicates forward chaining by the current
168 facts in order to establish the goal to be claimed next. The
169 initial proof method invoked to refine that will be offered the
170 facts to do ``anything appropriate'' (see also
171 \secref{sec:proof-steps}). For example, method @{method_ref rule}
172 (see \secref{sec:pure-meth-att}) would typically do an elimination
173 rather than an introduction. Automatic methods usually insert the
174 facts into the goal state before operation. This provides a simple
175 scheme to control relevance of facts in automated proof search.
177 \item [@{command "from"}~@{text b}] abbreviates ``@{command
178 "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
179 equivalent to ``@{command "from"}~@{text this}''.
181 \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
182 abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
183 this"}''; thus the forward chaining is from earlier facts together
184 with the current ones.
186 \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
187 the facts being currently indicated for use by a subsequent
188 refinement step (such as @{command_ref "apply"} or @{command_ref
191 \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
192 structurally similar to @{command "using"}, but unfolds definitional
193 equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
198 Forward chaining with an empty list of theorems is the same as not
199 chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
200 effect apart from entering @{text "prove(chain)"} mode, since
201 @{fact_ref nothing} is bound to the empty list of theorems.
203 Basic proof methods (such as @{method_ref rule}) expect multiple
204 facts to be given in their proper order, corresponding to a prefix
205 of the premises of the rule involved. Note that positions may be
206 easily skipped using something like @{command "from"}~@{text "_
207 \<AND> a \<AND> b"}, for example. This involves the trivial rule
208 @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
209 ``@{fact_ref "_"}'' (underscore).
211 Automated methods (such as @{method simp} or @{method auto}) just
212 insert any given facts before their usual operation. Depending on
213 the kind of procedure involved, the order of facts is less
218 section {* Goal statements \label{sec:goals} *}
221 \begin{matharray}{rcl}
222 @{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
223 @{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
224 @{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
225 @{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
226 @{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
227 @{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
228 @{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
229 @{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
232 From a theory context, proof mode is entered by an initial goal
233 command such as @{command "lemma"}, @{command "theorem"}, or
234 @{command "corollary"}. Within a proof, new claims may be
235 introduced locally as well; four variants are available here to
236 indicate whether forward chaining of facts should be performed
237 initially (via @{command_ref "then"}), and whether the final result
238 is meant to solve some pending goal.
240 Goals may consist of multiple statements, resulting in a list of
241 facts eventually. A pending multi-goal is internally represented as
242 a meta-level conjunction (printed as @{text "&&"}), which is usually
243 split into the corresponding number of sub-goals prior to an initial
244 method application, via @{command_ref "proof"}
245 (\secref{sec:proof-steps}) or @{command_ref "apply"}
246 (\secref{sec:tactic-commands}). The @{method_ref induct} method
247 covered in \secref{sec:cases-induct} acts on multiple claims
250 Claims at the theory level may be either in short or long form. A
251 short goal merely consists of several simultaneous propositions
252 (often just one). A long goal includes an explicit context
253 specification for the subsequent conclusion, involving local
254 parameters and assumptions. Here the role of each part of the
255 statement is explicitly marked by separate keywords (see also
256 \secref{sec:locale}); the local assumptions being introduced here
257 are available as @{fact_ref assms} in the proof. Moreover, there
258 are two kinds of conclusions: @{element_def "shows"} states several
259 simultaneous propositions (essentially a big conjunction), while
260 @{element_def "obtains"} claims several simultaneous simultaneous
261 contexts of (essentially a big disjunction of eliminated parameters
262 and assumptions, cf.\ \secref{sec:obtain}).
265 ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
267 ('have' | 'show' | 'hence' | 'thus') goal
269 'print\_statement' modes? thmrefs
272 goal: (props + 'and')
274 longgoal: thmdecl? (contextelem *) conclusion
276 conclusion: 'shows' goal | 'obtains' (parname? case + '|')
278 case: (vars + 'and') 'where' (props + 'and')
284 \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
285 @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
286 \<phi>"} to be put back into the target context. An additional
287 \railnonterm{context} specification may build up an initial proof
288 context for the subsequent claim; this includes local definitions
289 and syntax as well, see the definition of @{syntax contextelem} in
292 \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
293 "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
294 "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
295 being of a different kind. This discrimination acts like a formal
298 \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
299 eventually resulting in a fact within the current logical context.
300 This operation is completely independent of any pending sub-goals of
301 an enclosing goal statements, so @{command "have"} may be freely
302 used for experimental exploration of potential results within a
305 \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
306 "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
307 sub-goal for each one of the finished result, after having been
308 exported into the corresponding context (at the head of the
309 sub-proof of this @{command "show"} command).
311 To accommodate interactive debugging, resulting rules are printed
312 before being applied internally. Even more, interactive execution
313 of @{command "show"} predicts potential failure and displays the
314 resulting error as a warning beforehand. Watch out for the
317 %FIXME proper antiquitation
319 Problem! Local statement will fail to solve any pending goal
322 \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
323 "have"}'', i.e.\ claims a local goal to be proven by forward
324 chaining the current facts. Note that @{command "hence"} is also
325 equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
327 \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
328 "show"}''. Note that @{command "thus"} is also equivalent to
329 ``@{command "from"}~@{text this}~@{command "show"}''.
331 \item [@{command "print_statement"}~@{text a}] prints facts from the
332 current theory or proof context in long statement form, according to
333 the syntax for @{command "lemma"} given above.
337 Any goal statement causes some term abbreviations (such as
338 @{variable_ref "?thesis"}) to be bound automatically, see also
339 \secref{sec:term-abbrev}. Furthermore, the local context of a
340 (non-atomic) goal is provided via the @{case_ref rule_context} case.
342 The optional case names of @{element_ref "obtains"} have a twofold
343 meaning: (1) during the of this claim they refer to the the local
344 context introductions, (2) the resulting rule is annotated
345 accordingly to support symbolic case splits when used with the
346 @{method_ref cases} method (cf. \secref{sec:cases-induct}).
351 Isabelle/Isar suffers theory-level goal statements to contain
352 \emph{unbound schematic variables}, although this does not conform
353 to the aim of human-readable proof documents! The main problem
354 with schematic goals is that the actual outcome is usually hard to
355 predict, depending on the behavior of the proof methods applied
356 during the course of reasoning. Note that most semi-automated
357 methods heavily depend on several kinds of implicit rule
358 declarations within the current theory context. As this would
359 also result in non-compositional checking of sub-proofs,
360 \emph{local goals} are not allowed to be schematic at all.
361 Nevertheless, schematic goals do have their use in Prolog-style
362 interactive synthesis of proven results, usually by stepwise
363 refinement via emulation of traditional Isabelle tactic scripts
364 (see also \secref{sec:tactic-commands}). In any case, users
365 should know what they are doing.
370 section {* Initial and terminal proof steps \label{sec:proof-steps} *}
373 \begin{matharray}{rcl}
374 @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
375 @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
376 @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
377 @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
378 @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
379 @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
382 Arbitrary goal refinement via tactics is considered harmful.
383 Structured proof composition in Isar admits proof methods to be
384 invoked in two places only.
388 \item An \emph{initial} refinement step @{command_ref
389 "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
390 of sub-goals that are to be solved later. Facts are passed to
391 @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
392 "proof(chain)"} mode.
394 \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
395 "m\<^sub>2"} is intended to solve remaining goals. No facts are
396 passed to @{text "m\<^sub>2"}.
400 The only other (proper) way to affect pending goals in a proof body
401 is by @{command_ref "show"}, which involves an explicit statement of
402 what is to be solved eventually. Thus we avoid the fundamental
403 problem of unstructured tactic scripts that consist of numerous
404 consecutive goal transformations, with invisible effects.
406 \medskip As a general rule of thumb for good proof style, initial
407 proof methods should either solve the goal completely, or constitute
408 some well-understood reduction to new sub-goals. Arbitrary
409 automatic proof tools that are prone leave a large number of badly
410 structured sub-goals are no help in continuing the proof document in
411 an intelligible manner.
413 Unless given explicitly by the user, the default initial method is
414 ``@{method_ref rule}'', which applies a single standard elimination
415 or introduction rule according to the topmost symbol involved.
416 There is no separate default terminal method. Any remaining goals
417 are always solved by assumption in the very last step.
426 ('.' | '..' | 'sorry')
432 \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
433 proof method @{text "m\<^sub>1"}; facts for forward chaining are
434 passed if so indicated by @{text "proof(chain)"} mode.
436 \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
437 goals by proof method @{text "m\<^sub>2"} and concludes the
438 sub-proof by assumption. If the goal had been @{text "show"} (or
439 @{text "thus"}), some pending sub-goal is solved as well by the rule
440 resulting from the result \emph{exported} into the enclosing goal
441 context. Thus @{text "qed"} may fail for two reasons: either @{text
442 "m\<^sub>2"} fails, or the resulting rule does not fit to any
443 pending goal\footnote{This includes any additional ``strong''
444 assumptions as introduced by @{command "assume"}.} of the enclosing
445 context. Debugging such a situation might involve temporarily
446 changing @{command "show"} into @{command "have"}, or weakening the
447 local context by replacing occurrences of @{command "assume"} by
448 @{command "presume"}.
450 \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
451 \emph{terminal proof}\index{proof!terminal}; it abbreviates
452 @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
453 "m\<^sub>2"}, but with backtracking across both methods. Debugging
454 an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
455 command can be done by expanding its definition; in many cases
456 @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
457 "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
460 \item [``@{command ".."}''] is a \emph{default
461 proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
464 \item [``@{command "."}''] is a \emph{trivial
465 proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
468 \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
469 pretending to solve the pending claim without further ado. This
470 only works in interactive development, or if the @{ML
471 quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
472 proofs are not the real thing. Internally, each theorem container
473 is tainted by an oracle invocation, which is indicated as ``@{text
474 "[!]"}'' in the printed result.
476 The most important application of @{command "sorry"} is to support
477 experimentation and top-down proof development.
483 section {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
486 The following proof methods and attributes refer to basic logical
487 operations of Isar. Further methods and attributes are provided by
488 several generic and object-logic specific tools and packages (see
489 \chref{ch:gen-tools} and \chref{ch:hol}).
491 \begin{matharray}{rcl}
492 @{method_def "-"} & : & \isarmeth \\
493 @{method_def "fact"} & : & \isarmeth \\
494 @{method_def "assumption"} & : & \isarmeth \\
495 @{method_def "this"} & : & \isarmeth \\
496 @{method_def "rule"} & : & \isarmeth \\
497 @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
498 @{attribute_def "intro"} & : & \isaratt \\
499 @{attribute_def "elim"} & : & \isaratt \\
500 @{attribute_def "dest"} & : & \isaratt \\
501 @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
502 @{attribute_def "OF"} & : & \isaratt \\
503 @{attribute_def "of"} & : & \isaratt \\
504 @{attribute_def "where"} & : & \isaratt \\
512 'iprover' ('!' ?) (rulemod *)
514 rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
516 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
522 'of' insts ('concl' ':' insts)?
524 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
530 \item [``@{method "-"}'' (minus)] does nothing but insert the
531 forward chaining facts as premises into the goal. Note that command
532 @{command_ref "proof"} without any method actually performs a single
533 reduction step using the @{method_ref rule} method; thus a plain
534 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
535 "-"}'' rather than @{command "proof"} alone.
537 \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
538 some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
539 the current proof context) modulo unification of schematic type and
540 term variables. The rule structure is not taken into account, i.e.\
541 meta-level implication is considered atomic. This is the same
542 principle underlying literal facts (cf.\ \secref{sec:syn-att}):
543 ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
544 equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
545 "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
546 @{text "\<turnstile> \<phi>"} in the proof context.
548 \item [@{method assumption}] solves some goal by a single assumption
549 step. All given facts are guaranteed to participate in the
550 refinement; this means there may be only 0 or 1 in the first place.
551 Recall that @{command "qed"} (\secref{sec:proof-steps}) already
552 concludes any remaining sub-goals by assumption, so structured
553 proofs usually need not quote the @{method assumption} method at
556 \item [@{method this}] applies all of the current facts directly as
557 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
558 "by"}~@{text this}''.
560 \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
561 rule given as argument in backward manner; facts are used to reduce
562 the rule before applying it to the goal. Thus @{method rule}
563 without facts is plain introduction, while with facts it becomes
566 When no arguments are given, the @{method rule} method tries to pick
567 appropriate rules automatically, as declared in the current context
568 using the @{attribute intro}, @{attribute elim}, @{attribute dest}
569 attributes (see below). This is the default behavior of @{command
570 "proof"} and ``@{command ".."}'' (double-dot) steps (see
571 \secref{sec:proof-steps}).
573 \item [@{method iprover}] performs intuitionistic proof search,
574 depending on specifically declared rules from the context, or given
575 as explicit arguments. Chained facts are inserted into the goal
576 before commencing proof search; ``@{method iprover}@{text "!"}''
577 means to include the current @{fact prems} as well.
579 Rules need to be classified as @{attribute intro}, @{attribute
580 elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
581 refers to ``safe'' rules, which may be applied aggressively (without
582 considering back-tracking later). Rules declared with ``@{text
583 "?"}'' are ignored in proof search (the single-step @{method rule}
584 method still observes these). An explicit weight annotation may be
585 given as well; otherwise the number of rule premises will be taken
588 \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
589 declare introduction, elimination, and destruct rules, to be used
590 with the @{method rule} and @{method iprover} methods. Note that
591 the latter will ignore rules declared with ``@{text "?"}'', while
592 ``@{text "!"}'' are used most aggressively.
594 The classical reasoner (see \secref{sec:classical}) introduces its
595 own variants of these attributes; use qualified names to access the
596 present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
598 \item [@{attribute rule}~@{text del}] undeclares introduction,
599 elimination, or destruct rules.
601 \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
602 theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
603 (in parallel). This corresponds to the @{ML "op MRS"} operation in
604 ML, but note the reversed order. Positions may be effectively
605 skipped by including ``@{text _}'' (underscore) as argument.
607 \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
608 positional instantiation of term variables. The terms @{text
609 "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
610 variables occurring in a theorem from left to right; ``@{text _}''
611 (underscore) indicates to skip a position. Arguments following a
612 ``@{text "concl:"}'' specification refer to positions of the
613 conclusion of a rule.
615 \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
616 x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
617 type and term variables occurring in a theorem. Schematic variables
618 have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
619 The question mark may be omitted if the variable name is a plain
620 identifier without index. As type instantiations are inferred from
621 term instantiations, explicit type instantiations are seldom
628 section {* Term abbreviations \label{sec:term-abbrev} *}
631 \begin{matharray}{rcl}
632 @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
633 @{keyword_def "is"} & : & syntax \\
636 Abbreviations may be either bound by explicit @{command
637 "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
638 goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
639 p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
640 bind extra-logical term variables, which may be either named
641 schematic variables of the form @{text ?x}, or nameless dummies
642 ``@{variable _}'' (underscore). Note that in the @{command "let"}
643 form the patterns occur on the left-hand side, while the @{keyword
644 "is"} patterns are in postfix position.
646 Polymorphism of term bindings is handled in Hindley-Milner style,
647 similar to ML. Type variables referring to local assumptions or
648 open goal statements are \emph{fixed}, while those of finished
649 results or bound by @{command "let"} may occur in \emph{arbitrary}
650 instances later. Even though actual polymorphism should be rarely
651 used in practice, this mechanism is essential to achieve proper
652 incremental type-inference, as the user proceeds to build up the
653 Isar proof text from left to right.
655 \medskip Term abbreviations are quite different from local
656 definitions as introduced via @{command "def"} (see
657 \secref{sec:proof-context}). The latter are visible within the
658 logic as actual equations, while abbreviations disappear during the
659 input process just after type checking. Also note that @{command
660 "def"} does not support polymorphism.
663 'let' ((term + 'and') '=' term + 'and')
667 The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
668 or \railnonterm{proppat} (see \secref{sec:term-decls}).
672 \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
673 p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
674 "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
675 against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
677 \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
678 "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
679 preceding statement. Also note that @{keyword "is"} is not a
680 separate command, but part of others (such as @{command "assume"},
681 @{command "have"} etc.).
685 Some \emph{implicit} term abbreviations\index{term abbreviations}
686 for goals and facts are available as well. For any open goal,
687 @{variable_ref thesis} refers to its object-level statement,
688 abstracted over any meta-level parameters (if present). Likewise,
689 @{variable_ref this} is bound for fact statements resulting from
690 assumptions or finished goals. In case @{variable this} refers to
691 an object-logic statement that is an application @{text "f t"}, then
692 @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
693 (three dots). The canonical application of this convenience are
694 calculational proofs (see \secref{sec:calculation}).
698 section {* Block structure *}
701 \begin{matharray}{rcl}
702 @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
703 @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
704 @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
707 While Isar is inherently block-structured, opening and closing
708 blocks is mostly handled rather casually, with little explicit
709 user-intervention. Any local goal statement automatically opens
710 \emph{two} internal blocks, which are closed again when concluding
711 the sub-proof (by @{command "qed"} etc.). Sections of different
712 context within a sub-proof may be switched via @{command "next"},
713 which is just a single block-close followed by block-open again.
714 The effect of @{command "next"} is to reset the local proof context;
715 there is no goal focus involved here!
717 For slightly more advanced applications, there are explicit block
718 parentheses as well. These typically achieve a stronger forward
723 \item [@{command "next"}] switches to a fresh block within a
724 sub-proof, resetting the local context to the initial one.
726 \item [@{command "{"} and @{command "}"}] explicitly open and close
727 blocks. Any current facts pass through ``@{command "{"}''
728 unchanged, while ``@{command "}"}'' causes any result to be
729 \emph{exported} into the enclosing context. Thus fixed variables
730 are generalized, assumptions discharged, and local definitions
731 unfolded (cf.\ \secref{sec:proof-context}). There is no difference
732 of @{command "assume"} and @{command "presume"} in this mode of
733 forward reasoning --- in contrast to plain backward reasoning with
734 the result exported at @{command "show"} time.
740 section {* Emulating tactic scripts \label{sec:tactic-commands} *}
743 The Isar provides separate commands to accommodate tactic-style
744 proof scripts within the same system. While being outside the
745 orthodox Isar proof language, these might come in handy for
746 interactive exploration and debugging, or even actual tactical proof
747 within new-style theories (to benefit from document preparation, for
748 example). See also \secref{sec:tactics} for actual tactics, that
749 have been encapsulated as proof methods. Proper proof methods may
750 be used in scripts, too.
752 \begin{matharray}{rcl}
753 @{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
754 @{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
755 @{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
756 @{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
757 @{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
758 @{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
762 ( 'apply' | 'apply\_end' ) method
772 \item [@{command "apply"}~@{text m}] applies proof method @{text m}
773 in initial position, but unlike @{command "proof"} it retains
774 ``@{text "proof(prove)"}'' mode. Thus consecutive method
775 applications may be given just as in tactic scripts.
777 Facts are passed to @{text m} as indicated by the goal's
778 forward-chain mode, and are \emph{consumed} afterwards. Thus any
779 further @{command "apply"} command would always work in a purely
782 \item [@{command "apply_end"}~@{text "m"}] applies proof method
783 @{text m} as if in terminal position. Basically, this simulates a
784 multi-step tactic script for @{command "qed"}, but may be given
785 anywhere within the proof body.
787 No facts are passed to @{method m} here. Furthermore, the static
788 context is that of the enclosing goal (as for actual @{command
789 "qed"}). Thus the proof method may not refer to any assumptions
790 introduced in the current body, for example.
792 \item [@{command "done"}] completes a proof script, provided that
793 the current goal state is solved completely. Note that actual
794 structured proof commands (e.g.\ ``@{command "."}'' or @{command
795 "sorry"}) may be used to conclude proof scripts as well.
797 \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
798 n}] shuffle the list of pending goals: @{command "defer"} puts off
799 sub-goal @{text n} to the end of the list (@{text "n = 1"} by
800 default), while @{command "prefer"} brings sub-goal @{text n} to the
803 \item [@{command "back"}] does back-tracking over the result
804 sequence of the latest proof command. Basically, any proof command
805 may return multiple results.
809 Any proper Isar proof method may be used with tactic script commands
810 such as @{command "apply"}. A few additional emulations of actual
811 tactics are provided as well; these would be never used in actual
812 structured proofs, of course.
816 section {* Omitting proofs *}
819 \begin{matharray}{rcl}
820 @{command_def "oops"} & : & \isartrans{proof}{theory} \\
823 The @{command "oops"} command discontinues the current proof
824 attempt, while considering the partial proof text as properly
825 processed. This is conceptually quite different from ``faking''
826 actual proofs via @{command_ref "sorry"} (see
827 \secref{sec:proof-steps}): @{command "oops"} does not observe the
828 proof structure at all, but goes back right to the theory level.
829 Furthermore, @{command "oops"} does not produce any result theorem
830 --- there is no intended claim to be able to complete the proof
833 A typical application of @{command "oops"} is to explain Isar proofs
834 \emph{within} the system itself, in conjunction with the document
835 preparation tools of Isabelle described in \cite{isabelle-sys}.
836 Thus partial or even wrong proof attempts can be discussed in a
837 logically sound manner. Note that the Isabelle {\LaTeX} macros can
838 be easily adapted to print something like ``@{text "\<dots>"}'' instead of
839 the keyword ``@{command "oops"}''.
841 \medskip The @{command "oops"} command is undo-able, unlike
842 @{command_ref "kill"} (see \secref{sec:history}). The effect is to
843 get back to the theory just before the opening of the proof.
847 section {* Generalized elimination \label{sec:obtain} *}
850 \begin{matharray}{rcl}
851 @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
852 @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
855 Generalized elimination means that additional elements with certain
856 properties may be introduced in the current context, by virtue of a
857 locally proven ``soundness statement''. Technically speaking, the
858 @{command "obtain"} language element is like a declaration of
859 @{command "fix"} and @{command "assume"} (see also see
860 \secref{sec:proof-context}), together with a soundness proof of its
861 additional claim. According to the nature of existential reasoning,
862 assumptions get eliminated from any result exported from the context
863 later, provided that the corresponding parameters do \emph{not}
864 occur in the conclusion.
867 'obtain' parname? (vars + 'and') 'where' (props + 'and')
869 'guess' (vars + 'and')
873 The derived Isar command @{command "obtain"} is defined as follows
874 (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
875 facts indicated for forward chaining).
877 @{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]
878 \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"} \\
879 \quad @{command "proof"}~@{text succeed} \\
880 \qquad @{command "fix"}~@{text thesis} \\
881 \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"} \\
882 \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
883 \quad\qquad @{command "apply"}~@{text -} \\
884 \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
885 \quad @{command "qed"} \\
886 \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
889 Typically, the soundness proof is relatively straight-forward, often
890 just by canonical automated tools such as ``@{command "by"}~@{text
891 simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
892 ``@{text that}'' reduction above is declared as simplification and
895 In a sense, @{command "obtain"} represents at the level of Isar
896 proofs what would be meta-logical existential quantifiers and
897 conjunctions. This concept has a broad range of useful
898 applications, ranging from plain elimination (or introduction) of
899 object-level existential and conjunctions, to elimination over
900 results of symbolic evaluation of recursive definitions, for
901 example. Also note that @{command "obtain"} without parameters acts
902 much like @{command "have"}, where the result is treated as a
905 An alternative name to be used instead of ``@{text that}'' above may
906 be given in parentheses.
908 \medskip The improper variant @{command "guess"} is similar to
909 @{command "obtain"}, but derives the obtained statement from the
910 course of reasoning! The proof starts with a fixed goal @{text
911 thesis}. The subsequent proof may refine this to anything of the
912 form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
913 \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
914 final goal state is then used as reduction rule for the obtain
915 scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
916 x\<^sub>m"} are marked as internal by default, which prevents the
917 proof context from being polluted by ad-hoc variables. The variable
918 names and type constraints given as arguments for @{command "guess"}
919 specify a prefix of obtained parameters explicitly in the text.
921 It is important to note that the facts introduced by @{command
922 "obtain"} and @{command "guess"} may not be polymorphic: any
923 type-variables occurring here are fixed in the present context!
927 section {* Calculational reasoning \label{sec:calculation} *}
930 \begin{matharray}{rcl}
931 @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
932 @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
933 @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
934 @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
935 @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
936 @{attribute trans} & : & \isaratt \\
937 @{attribute sym} & : & \isaratt \\
938 @{attribute symmetric} & : & \isaratt \\
941 Calculational proof is forward reasoning with implicit application
942 of transitivity rules (such those of @{text "="}, @{text "\<le>"},
943 @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
944 @{fact_ref calculation} for accumulating results obtained by
945 transitivity composed with the current result. Command @{command
946 "also"} updates @{fact calculation} involving @{fact this}, while
947 @{command "finally"} exhibits the final @{fact calculation} by
948 forward chaining towards the next goal statement. Both commands
949 require valid current facts, i.e.\ may occur only after commands
950 that produce theorems such as @{command "assume"}, @{command
951 "note"}, or some finished proof of @{command "have"}, @{command
952 "show"} etc. The @{command "moreover"} and @{command "ultimately"}
953 commands are similar to @{command "also"} and @{command "finally"},
954 but only collect further results in @{fact calculation} without
955 applying any rules yet.
957 Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
958 its canonical application with calculational proofs. It refers to
959 the argument of the preceding statement. (The argument of a curried
960 infix expression happens to be its right-hand side.)
962 Isabelle/Isar calculations are implicitly subject to block structure
963 in the sense that new threads of calculational reasoning are
964 commenced for any new block (as opened by a local goal, for
965 example). This means that, apart from being able to nest
966 calculations, there is no separate \emph{begin-calculation} command
969 \medskip The Isar calculation proof commands may be defined as
970 follows:\footnote{We suppress internal bookkeeping such as proper
971 handling of block-structure.}
973 \begin{matharray}{rcl}
974 @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
975 @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
976 @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
977 @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
978 @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
982 ('also' | 'finally') ('(' thmrefs ')')?
984 'trans' (() | 'add' | 'del')
990 \item [@{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
991 maintains the auxiliary @{fact calculation} register as follows.
992 The first occurrence of @{command "also"} in some calculational
993 thread initializes @{fact calculation} by @{fact this}. Any
994 subsequent @{command "also"} on the same level of block-structure
995 updates @{fact calculation} by some transitivity rule applied to
996 @{fact calculation} and @{fact this} (in that order). Transitivity
997 rules are picked from the current context, unless alternative rules
998 are given as explicit arguments.
1000 \item [@{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
1001 maintaining @{fact calculation} in the same way as @{command
1002 "also"}, and concludes the current calculational thread. The final
1003 result is exhibited as fact for forward chaining towards the next
1004 goal. Basically, @{command "finally"} just abbreviates @{command
1005 "also"}~@{command "from"}~@{fact calculation}. Typical idioms for
1006 concluding calculational proofs are ``@{command "finally"}~@{command
1007 "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
1008 "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
1010 \item [@{command "moreover"} and @{command "ultimately"}] are
1011 analogous to @{command "also"} and @{command "finally"}, but collect
1012 results only, without applying rules.
1014 \item [@{command "print_trans_rules"}] prints the list of
1015 transitivity rules (for calculational commands @{command "also"} and
1016 @{command "finally"}) and symmetry rules (for the @{attribute
1017 symmetric} operation and single step elimination patters) of the
1020 \item [@{attribute trans}] declares theorems as transitivity rules.
1022 \item [@{attribute sym}] declares symmetry rules, as well as
1023 @{attribute "Pure.elim?"} rules.
1025 \item [@{attribute symmetric}] resolves a theorem with some rule
1026 declared as @{attribute sym} in the current context. For example,
1027 ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
1028 swapped fact derived from that assumption.
1030 In structured proof texts it is often more appropriate to use an
1031 explicit single-step elimination proof, such as ``@{command
1032 "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
1033 "y = x"}~@{command ".."}''.