2 \chapter{Generic tools and packages}\label{ch:gen-tools}
4 \section{Theory specification commands}
6 \subsection{Axiomatic type classes}\label{sec:axclass}
8 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
10 \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
11 \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
12 intro_classes & : & \isarmeth \\
15 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
16 interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
17 may make use of this light-weight mechanism of abstract theories
18 \cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type
19 classes in Isabelle \cite{isabelle-axclass} that is part of the standard
20 Isabelle documentation.
23 'axclass' classdecl (axmdecl prop +)
25 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
31 \item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
32 the intersection of existing classes, with additional axioms holding. Class
33 axioms may not contain more than one type variable. The class axioms (with
34 implicit sort constraints added) are bound to the given names. Furthermore
35 a class introduction rule is generated (being bound as
36 $c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to
37 support instantiation proofs of this class.
39 The ``axioms'' are stored as theorems according to the given name
40 specifications, adding the class name $c$ as name space prefix; the same
41 facts are also stored collectively as $c_class{\dtt}axioms$.
43 \item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
44 goal stating a class relation or type arity. The proof would usually
45 proceed by $intro_classes$, and then establish the characteristic theorems
46 of the type classes involved. After finishing the proof, the theory will be
47 augmented by a type signature declaration corresponding to the resulting
50 \item [$intro_classes$] repeatedly expands all class introduction rules of
51 this theory. Note that this method usually needs not be named explicitly,
52 as it is already included in the default proof step (of $\PROOFNAME$ etc.).
53 In particular, instantiation of trivial (syntactic) classes may be performed
54 by a single ``$\DDOT$'' proof step.
59 \subsection{Locales and local contexts}\label{sec:locale}
61 Locales are named local contexts, consisting of a list of declaration elements
62 that are modeled after the Isar proof context commands (cf.\
63 \S\ref{sec:proof-context}).
66 \subsubsection{Localized commands}
68 Existing locales may be augmented later on by adding new facts. Note that the
69 actual context definition may not be changed! Several theory commands that
70 produce facts in some way are available in ``localized'' versions, referring
71 to a named locale instead of the global theory context.
73 \indexouternonterm{locale}
75 locale: '(' 'in' name ')'
79 Emerging facts of localized commands are stored in two versions, both in the
80 target locale and the theory (after export). The latter view produces a
81 qualified binding, using the locale name as a name space prefix.
83 For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from
84 the locale context of $loc$ and augments its body by an appropriate
85 ``$\isarkeyword{notes}$'' element (see below). The exported view of $a$,
86 after discharging the locale context, is stored as $loc{.}a$ within the global
87 theory. A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' works similarly,
88 only that the fact emerges through the subsequent proof, which may refer to
89 the full infrastructure of the locale context (covering local parameters with
90 typing and concrete syntax, assumptions, definitions etc.). Most notably,
91 fact declarations of the locale are active during the proof as well (e.g.\
94 As a general principle, results exported from a locale context acquire
95 additional premises according to the specification. Usually this is only a
96 single predicate according to the standard ``closed'' view of locale
100 \subsubsection{Locale specifications}
102 \indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales}
103 \begin{matharray}{rcl}
104 \isarcmd{locale} & : & \isarkeep{theory} \\
105 \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\
106 \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\
109 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
111 \railalias{printlocale}{print\_locale}
112 \railterm{printlocale}
115 'locale' ('(open)')? name ('=' localeexpr)?
117 printlocale '!'? localeexpr
119 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
122 contextexpr: nameref | '(' contextexpr ')' |
123 (contextexpr (name mixfix? +)) | (contextexpr + '+')
125 contextelem: fixes | constrains | assumes | defines | notes | includes
127 fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
129 constrains: 'constrains' (name '::' type + 'and')
131 assumes: 'assumes' (thmdecl? props + 'and')
133 defines: 'defines' (thmdecl? prop proppat? + 'and')
135 notes: 'notes' (thmdef? thmrefs + 'and')
137 includes: 'includes' contextexpr
143 \item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context
144 consisting of a certain view of existing locales ($import$) plus some
145 additional elements ($body$). Both $import$ and $body$ are optional; the
146 degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
147 useful to collect declarations of facts later on. Type-inference on locale
148 expressions automatically takes care of the most general typing that the
149 combined context elements may acquire.
151 The $import$ consists of a structured context expression, consisting of
152 references to existing locales, renamed contexts, or merged contexts.
153 Renaming uses positional notation: $c~\vec x$ means that (a prefix of) the
154 fixed parameters of context $c$ are named according to $\vec x$; a
155 ``\texttt{_}'' (underscore) \indexisarthm{_@\texttt{_}} means to skip that
156 position. Renaming by default deletes existing syntax. Optionally,
157 new syntax may by specified with a mixfix annotation. Note that the
158 special syntax declared with ``$(structure)$'' (see below) is
159 neither deleted nor can it be changed.
160 Merging proceeds from left-to-right, suppressing any duplicates stemming
161 from different paths through the import hierarchy.
163 The $body$ consists of basic context elements, further context expressions
164 may be included as well.
168 \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$
169 and mixfix annotation $mx$ (both are optional). The special syntax
170 declaration ``$(structure)$'' means that $x$ may be referenced
171 implicitly in this context.
173 \item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$
174 on the local parameter $x$.
176 \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
177 $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
179 \item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter.
180 This is close to $\DEFNAME$ within a proof (cf.\
181 \S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational
182 proposition instead of variable-term pair. The left-hand side of the
183 equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x
186 \item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context. Most
187 notably, this may include arbitrary declarations in any attribute
188 specifications included here, e.g.\ a local $simp$ rule.
190 \item [$\INCLUDES{c}$] copies the specified context in a statically scoped
191 manner. Only available in the long goal format of \S\ref{sec:goals}.
193 In contrast, the initial $import$ specification of a locale expression
194 maintains a dynamic relation to the locales being referenced (benefiting
195 from any later fact declarations in the obvious manner).
198 Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and
199 $\DEFINESNAME$ above are illegal in locale definitions. In the long goal
200 format of \S\ref{sec:goals}, term bindings may be included as expected,
203 \medskip By default, locale specifications are ``closed up'' by turning the
204 given text into a predicate definition $loc_axioms$ and deriving the
205 original assumptions as local lemmas (modulo local definitions). The
206 predicate statement covers only the newly specified assumptions, omitting
207 the content of included locale expressions. The full cumulative view is
208 only provided on export, involving another predicate $loc$ that refers to
209 the complete specification text.
211 In any case, the predicate arguments are those locale parameters that
212 actually occur in the respective piece of text. Also note that these
213 predicates operate at the meta-level in theory, but the locale packages
214 attempts to internalize statements according to the object-logic setup
215 (e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see
216 also \S\ref{sec:object-logic}). Separate introduction rules
217 $loc_axioms.intro$ and $loc.intro$ are declared as well.
219 The $(open)$ option of a locale specification prevents both the current
220 $loc_axioms$ and cumulative $loc$ predicate constructions. Predicates are
221 also omitted for empty specification texts.
223 \item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale
224 expression in a flattened form. The notable special case
225 $\isarkeyword{print_locale}~loc$ just prints the contents of the named
226 locale, but keep in mind that type-inference will normalize type variables
227 according to the usual alphabetical order. The command omits
228 $\isarkeyword{notes}$ elements by default. Use
229 $\isarkeyword{print_locale}!$ to get them included.
231 \item [$\isarkeyword{print_locales}$] prints the names of all locales of the
237 \subsubsection{Interpretation of locales}
239 Locale expressions (more precisely, \emph{context expressions}) may be
240 instantiated, and the instantiated facts added to the current context.
241 This requires a proof of the instantiated specification and is called
242 \emph{locale interpretation}. Interpretation is possible in theories
244 (command $\isarcmd{interpretation}$) and also in proof contexts
245 ($\isarcmd{interpret}$).
247 \indexisarcmd{interpretation}\indexisarcmd{interpret}
248 \indexisarcmd{print-interps}
249 \begin{matharray}{rcl}
250 \isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\
251 \isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
252 \isarcmd{print_interps}^* & : & \isarkeep{theory~|~proof} \\
255 \indexouternonterm{interp}
257 \railalias{printinterps}{print\_interps}
258 \railterm{printinterps}
261 'interpretation' (interp | name ('<' | subseteq) contextexp)
265 printinterps '!'? name
267 interp: thmdecl? contextexpr ('[' (inst+) ']')?
274 \item [$\isarcmd{interpretation}~expr~insts$]
276 The first form of $\isarcmd{interpretation}$ interprets $expr$
277 in the theory. The instantiation is given as a list of
278 terms $insts$ and is positional.
279 All parameters must receive an instantiation term --- with the
280 exception of defined parameters. These are, if omitted, derived
281 from the defining equation and other instantiations. Use ``\_'' to
282 omit an instantiation term. Free variables are automatically
285 The command generates proof obligations for the instantiated
286 specifications (assumes and defines elements). Once these are
287 discharged by the user, instantiated facts are added to the theory in
288 a post-processing phase.
290 The command is aware of interpretations already active in the
291 theory. No proof obligations are generated for those, neither is
292 post-processing applied to their facts. This avoids duplication of
293 interpreted facts, in particular. Note that, in the case of a
294 locale with import, parts of the interpretation may already be
295 active. The command will only generate proof obligations and add
298 The context expression may be preceded by a name and/or attributes.
299 These take effect in the post-processing of facts. The name is used
300 to prefix fact names, for example to avoid accidental hiding of
301 other facts. Attributes are applied after attributes of the
304 Adding facts to locales has the
305 effect of adding interpreted facts to the theory for all active
306 interpretations also. That is, interpretations dynamically
307 participate in any facts added to locales.
309 \item [$\isarcmd{interpretation}~name~\subseteq~expr$]
311 This form of the command interprets $expr$ in the locale $name$. It
312 requires a proof that the specification of $name$ implies the
313 specification of $expr$. As in the localized version of the theorem
314 command, the proof is in the context of $name$. After the proof
315 obligation has been dischared, the facts of $expr$
316 become part of locale $name$ as \emph{derived} context elements and
317 are available when the context $name$ is subsequently entered.
318 Note that, like import, this is dynamic: facts added to a locale
319 part of $expr$ after interpretation become also available in
321 of renamed context elements, facts obtained by interpretation may be
322 accessed by prefixing with the parameter renaming (where the parameters
323 are separated by `\_').
325 Unlike interpretation in theories, instantiation is confined to the
326 renaming of parameters, which may be specified as part of the context
327 expression $expr$. Using defined parameters in $name$ one may
328 achieve an effect similar to instantiation, though.
330 Only specification fragments of $expr$ that are not already part of
331 $name$ (be it imported, derived or a derived fragment of the import)
332 are considered by interpretation. This enables circular
335 If interpretations of $name$ exist in the current theory, the
336 command adds interpretations for $expr$ as well, with the same
337 prefix and attributes, although only for fragments of $expr$ that
338 are not interpreted in the theory already.
340 \item [$\isarcmd{interpret}~expr~insts$]
341 interprets $expr$ in the proof context and is otherwise similar to
342 interpretation in theories. Free variables in instantiations are not
343 generalized, however.
345 \item [$\isarcmd{print_interps}~loc$]
346 prints the interpretations of a particular locale $loc$ that are
347 active in the current context, either theory or proof context. The
348 exclamation point argument causes triggers printing of
349 \emph{witness} theorems justifying interpretations. These are
350 normally omitted from the output.
356 Since attributes are applied to interpreted theorems, interpretation
357 may modify the current simpset and claset. Take this into
358 account when choosing attributes for local theorems.
362 An interpretation in a theory may subsume previous interpretations.
363 This happens if the same specification fragment is interpreted twice
364 and the instantiation of the second interpretation is more general
365 than the interpretation of the first. A warning
366 is issued, since it is likely that these could have been generalized
367 in the first place. The locale package does not attempt to remove
368 subsumed interpretations. This situation is normally harmless, but
369 note that $blast$ gets confused by the presence of multiple axclass
374 \section{Derived proof schemes}
376 \subsection{Generalized elimination}\label{sec:obtain}
378 \indexisarcmd{obtain}\indexisarcmd{guess}
379 \begin{matharray}{rcl}
380 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
381 \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\
384 Generalized elimination means that additional elements with certain properties
385 may be introduced in the current context, by virtue of a locally proven
386 ``soundness statement''. Technically speaking, the $\OBTAINNAME$ language
387 element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
388 \S\ref{sec:proof-context}), together with a soundness proof of its additional
389 claim. According to the nature of existential reasoning, assumptions get
390 eliminated from any result exported from the context later, provided that the
391 corresponding parameters do \emph{not} occur in the conclusion.
394 'obtain' (vars + 'and') 'where' (props + 'and')
396 'guess' (vars + 'and')
400 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
401 shall refer to (optional) facts indicated for forward chaining.
403 \langle facts~\vec b\rangle \\
404 \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
405 \quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\
406 \quad \PROOF{succeed} \\
407 \qquad \FIX{thesis} \\
408 \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
409 \qquad \THUS{}{thesis} \\
410 \quad\qquad \APPLY{-} \\
411 \quad\qquad \USING{\vec b}~~\langle proof\rangle \\
413 \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
416 Typically, the soundness proof is relatively straight-forward, often just by
417 canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
418 Accordingly, the ``$that$'' reduction above is declared as simplification and
421 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
422 meta-logical existential quantifiers and conjunctions. This concept has a
423 broad range of useful applications, ranging from plain elimination (or
424 introduction) of object-level existential and conjunctions, to elimination
425 over results of symbolic evaluation of recursive definitions, for example.
426 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
427 where the result is treated as a genuine assumption.
431 The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but
432 derives the obtained statement from the course of reasoning! The proof starts
433 with a fixed goal $thesis$. The subsequent proof may refine this to anything
434 of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce
435 new subgoals. The final goal state is then used as reduction rule for the
436 obtain scheme described above. Obtained parameters $\vec x$ are marked as
437 internal by default, which prevents the proof context from being polluted by
438 ad-hoc variables. The variable names and type constraints given as arguments
439 for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly
442 It is important to note that the facts introduced by $\OBTAINNAME$ and
443 $\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring
444 here are fixed in the present context!
447 \subsection{Calculational reasoning}\label{sec:calculation}
449 \indexisarcmd{also}\indexisarcmd{finally}
450 \indexisarcmd{moreover}\indexisarcmd{ultimately}
451 \indexisarcmd{print-trans-rules}
452 \indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric}
453 \begin{matharray}{rcl}
454 \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
455 \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
456 \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
457 \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
458 \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\
459 trans & : & \isaratt \\
460 sym & : & \isaratt \\
461 symmetric & : & \isaratt \\
464 Calculational proof is forward reasoning with implicit application of
465 transitivity rules (such those of $=$, $\leq$, $<$). Isabelle/Isar maintains
466 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
467 results obtained by transitivity composed with the current result. Command
468 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
469 final $calculation$ by forward chaining towards the next goal statement. Both
470 commands require valid current facts, i.e.\ may occur only after commands that
471 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
472 $\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are
473 similar to $\ALSO$ and $\FINALLY$, but only collect further results in
474 $calculation$ without applying any rules yet.
476 Also note that the implicit term abbreviation ``$\dots$'' has its canonical
477 application with calculational proofs. It refers to the argument of the
478 preceding statement. (The argument of a curried infix expression happens to be
479 its right-hand side.)
481 Isabelle/Isar calculations are implicitly subject to block structure in the
482 sense that new threads of calculational reasoning are commenced for any new
483 block (as opened by a local goal, for example). This means that, apart from
484 being able to nest calculations, there is no separate \emph{begin-calculation}
489 The Isar calculation proof commands may be defined as follows:\footnote{We
490 suppress internal bookkeeping such as proper handling of block-structure.}
491 \begin{matharray}{rcl}
492 \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
493 \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
494 \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
495 \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
496 \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
500 ('also' | 'finally') ('(' thmrefs ')')?
502 'trans' (() | 'add' | 'del')
508 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
509 follows. The first occurrence of $\ALSO$ in some calculational thread
510 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
511 level of block-structure updates $calculation$ by some transitivity rule
512 applied to $calculation$ and $this$ (in that order). Transitivity rules are
513 picked from the current context, unless alternative rules are given as
516 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
517 $\ALSO$, and concludes the current calculational thread. The final result
518 is exhibited as fact for forward chaining towards the next goal. Basically,
519 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that
520 ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
521 ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
522 calculational proofs.
524 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
525 but collect results only, without applying rules.
527 \item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
528 rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules
529 (for the $symmetric$ operation and single step elimination patters) of the
532 \item [$trans$] declares theorems as transitivity rules.
534 \item [$sym$] declares symmetry rules.
536 \item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the
537 current context. For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a
538 swapped fact derived from that assumption.
540 In structured proof texts it is often more appropriate to use an explicit
541 single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
542 x}~\DDOT$''. The very same rules known to $symmetric$ are declared as
548 \section{Proof tools}
550 \subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
552 \indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
553 \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
554 \indexisarmeth{fail}\indexisarmeth{succeed}
555 \begin{matharray}{rcl}
556 unfold & : & \isarmeth \\
557 fold & : & \isarmeth \\
558 insert & : & \isarmeth \\[0.5ex]
559 erule^* & : & \isarmeth \\
560 drule^* & : & \isarmeth \\
561 frule^* & : & \isarmeth \\
562 succeed & : & \isarmeth \\
563 fail & : & \isarmeth \\
567 ('fold' | 'unfold' | 'insert') thmrefs
569 ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
575 \item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
576 given meta-level definitions throughout all goals; any chained facts
577 provided are inserted into the goal and subject to rewriting as well.
579 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
580 state. Note that current facts indicated for forward chaining are ignored.
582 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
583 basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
584 elim-resolution, destruct-resolution, and forward-resolution, respectively
585 \cite{isabelle-ref}. The optional natural number argument (default $0$)
586 specifies additional assumption steps to be performed here.
588 Note that these methods are improper ones, mainly serving for
589 experimentation and tactic script emulation. Different modes of basic rule
590 application are usually expressed in Isar at the proof language level,
591 rather than via implicit proof state manipulations. For example, a proper
592 single-step elimination would be done using the plain $rule$ method, with
593 forward chaining of current facts.
595 \item [$succeed$] yields a single (unchanged) result; it is the identity of
596 the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
598 \item [$fail$] yields an empty result sequence; it is the identity of the
599 ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
603 \indexisaratt{tagged}\indexisaratt{untagged}
604 \indexisaratt{THEN}\indexisaratt{COMP}
605 \indexisaratt{unfolded}\indexisaratt{folded}
606 \indexisaratt{standard}\indexisarattof{Pure}{elim-format}
607 \indexisaratt{no-vars}
608 \begin{matharray}{rcl}
609 tagged & : & \isaratt \\
610 untagged & : & \isaratt \\[0.5ex]
611 THEN & : & \isaratt \\
612 COMP & : & \isaratt \\[0.5ex]
613 unfolded & : & \isaratt \\
614 folded & : & \isaratt \\[0.5ex]
615 elim_format & : & \isaratt \\
616 standard^* & : & \isaratt \\
617 no_vars^* & : & \isaratt \\
625 ('THEN' | 'COMP') ('[' nat ']')? thmref
627 ('unfolded' | 'folded') thmrefs
633 \item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
634 theorem. Tags may be any list of strings that serve as comment for some
635 tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
636 result). The first string is considered the tag name, the rest its
637 arguments. Note that untag removes any tags of the same name.
639 \item [$THEN~a$ and $COMP~a$] compose rules by resolution. $THEN$ resolves
640 with the first premise of $a$ (an alternative position may be also
641 specified); the $COMP$ version skips the automatic lifting process that is
642 normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
643 \cite[\S5]{isabelle-ref}).
645 \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
646 given meta-level definitions throughout a rule.
648 \item [$elim_format$] turns a destruction rule into elimination rule format,
649 by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
652 Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
653 version of this operation.
655 \item [$standard$] puts a theorem into the standard form of object-rules at
656 the outermost theory level. Note that this operation violates the local
657 proof context (including active locales).
659 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
660 for tuning output of pretty printed theorems.
665 \subsection{Further tactic emulations}\label{sec:tactics}
667 The following improper proof methods emulate traditional tactics. These admit
668 direct access to the goal state, which is normally considered harmful! In
669 particular, this may involve both numbered goal addressing (default 1), and
670 dynamic instantiation within the scope of some subgoal.
673 Dynamic instantiations refer to universally quantified parameters of
674 a subgoal (the dynamic context) rather than fixed variables and term
675 abbreviations of a (static) Isar context.
678 Tactic emulation methods, unlike their ML counterparts, admit
679 simultaneous instantiation from both dynamic and static contexts. If
680 names occur in both contexts goal parameters hide locally fixed
681 variables. Likewise, schematic variables refer to term abbreviations,
682 if present in the static context. Otherwise the schematic variable is
683 interpreted as a schematic variable and left to be solved by unification
684 with certain parts of the subgoal.
686 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
687 named $foo_tac$. Note also that variable names occurring on left hand sides
688 of instantiations must be preceded by a question mark if they coincide with
689 a keyword or contain dots.
690 This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
692 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
693 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
694 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
695 \indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
696 \indexisarmeth{rotate-tac}\indexisarmeth{tactic}
697 \begin{matharray}{rcl}
698 rule_tac^* & : & \isarmeth \\
699 erule_tac^* & : & \isarmeth \\
700 drule_tac^* & : & \isarmeth \\
701 frule_tac^* & : & \isarmeth \\
702 cut_tac^* & : & \isarmeth \\
703 thin_tac^* & : & \isarmeth \\
704 subgoal_tac^* & : & \isarmeth \\
705 rename_tac^* & : & \isarmeth \\
706 rotate_tac^* & : & \isarmeth \\
707 tactic^* & : & \isarmeth \\
710 \railalias{ruletac}{rule\_tac}
713 \railalias{eruletac}{erule\_tac}
716 \railalias{druletac}{drule\_tac}
719 \railalias{fruletac}{frule\_tac}
722 \railalias{cuttac}{cut\_tac}
725 \railalias{thintac}{thin\_tac}
728 \railalias{subgoaltac}{subgoal\_tac}
729 \railterm{subgoaltac}
731 \railalias{renametac}{rename\_tac}
734 \railalias{rotatetac}{rotate\_tac}
738 ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
739 ( insts thmref | thmrefs )
741 subgoaltac goalspec? (prop +)
743 renametac goalspec? (name +)
745 rotatetac goalspec? int?
750 insts: ((name '=' term) + 'and') 'in'
756 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
757 This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
758 \cite[\S3]{isabelle-ref}).
760 Multiple rules may be only given if there is no instantiation; then
761 $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
762 \cite[\S3]{isabelle-ref}).
764 \item [$cut_tac$] inserts facts into the proof state as assumption of a
765 subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note
766 that the scope of schematic variables is spread over the main goal
767 statement. Instantiations may be given as well, see also ML tactic
768 \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
770 \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
771 that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in
772 \cite[\S3]{isabelle-ref}.
774 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See
775 also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
776 \cite[\S3]{isabelle-ref}.
778 \item [$rename_tac~\vec x$] renames parameters of a goal according to the list
779 $\vec x$, which refers to the \emph{suffix} of variables.
781 \item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
782 from right to left if $n$ is positive, and from left to right if $n$ is
783 negative; the default value is $1$. See also \texttt{rotate_tac} in
784 \cite[\S3]{isabelle-ref}.
786 \item [$tactic~text$] produces a proof method from any ML text of type
787 \texttt{tactic}. Apart from the usual ML environment and the current
788 implicit theory context, the ML code may refer to the following locally
791 {\footnotesize\begin{verbatim}
792 val ctxt : Proof.context
794 val thm : string -> thm
795 val thms : string -> thm list
797 Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
798 indicates any current facts for forward-chaining, and
799 \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
800 theorems) from the context.
804 \subsection{The Simplifier}\label{sec:simplifier}
806 \subsubsection{Simplification methods}
808 \indexisarmeth{simp}\indexisarmeth{simp-all}
809 \begin{matharray}{rcl}
810 simp & : & \isarmeth \\
811 simp_all & : & \isarmeth \\
814 \railalias{simpall}{simp\_all}
817 \railalias{noasm}{no\_asm}
820 \railalias{noasmsimp}{no\_asm\_simp}
823 \railalias{noasmuse}{no\_asm\_use}
826 \railalias{asmlr}{asm\_lr}
829 \indexouternonterm{simpmod}
831 ('simp' | simpall) ('!' ?) opt? (simpmod *)
834 opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')'
836 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
837 'split' (() | 'add' | 'del')) ':' thmrefs
843 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
844 according to the arguments given. Note that the \railtterm{only} modifier
845 first removes all other rewrite rules, congruences, and looper tactics
846 (including splits), and then behaves like \railtterm{add}.
848 \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
849 rules (see also \cite{isabelle-ref}), the default is to add.
851 \medskip The \railtterm{split} modifiers add or delete rules for the
852 Splitter (see also \cite{isabelle-ref}), the default is to add. This works
853 only if the Simplifier method has been properly setup to include the
854 Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
856 \item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from
857 the last to the first one).
861 By default the Simplifier methods take local assumptions fully into account,
862 using equational assumptions in the subsequent normalization process, or
863 simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in
864 \cite[\S10]{isabelle-ref}). In structured proofs this is usually quite well
865 behaved in practice: just the local premises of the actual goal are involved,
866 additional facts may be inserted via explicit forward-chaining (using $\THEN$,
867 $\FROMNAME$ etc.). The full context of assumptions is only included if the
868 ``$!$'' (bang) argument is given, which should be used with some care, though.
870 Additional Simplifier options may be specified to tune the behavior further
871 (mostly for unstructured scripts with many accidental local facts):
872 ``$(no_asm)$'' means assumptions are ignored completely (cf.\
873 \texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the
874 simplification of the conclusion but are not themselves simplified (cf.\
875 \texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are
876 simplified but are not used in the simplification of each other or the
877 conclusion (cf.\ \texttt{full_simp_tac}).
878 For compatibility reasons, there is also an option ``$(asm_lr)$'',
879 which means that an assumption is only used for simplifying assumptions
880 which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}).
884 The Splitter package is usually configured to work as part of the Simplifier.
885 The effect of repeatedly applying \texttt{split_tac} can be simulated by
886 ``$(simp~only\colon~split\colon~\vec a)$''. There is also a separate $split$
887 method available for single-step case splitting.
890 \subsubsection{Declaring rules}
892 \indexisarcmd{print-simpset}
893 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
894 \begin{matharray}{rcl}
895 \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\
896 simp & : & \isaratt \\
897 cong & : & \isaratt \\
898 split & : & \isaratt \\
902 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
908 \item [$\isarcmd{print_simpset}$] prints the collection of rules declared to
909 the Simplifier, which is also known as ``simpset'' internally
910 \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
912 \item [$simp$] declares simplification rules.
914 \item [$cong$] declares congruence rules.
916 \item [$split$] declares case split rules.
921 \subsubsection{Forward simplification}
923 \indexisaratt{simplified}
924 \begin{matharray}{rcl}
925 simplified & : & \isaratt \\
929 'simplified' opt? thmrefs?
932 opt: '(' (noasm | noasmsimp | noasmuse) ')'
938 \item [$simplified~\vec a$] causes a theorem to be simplified, either by
939 exactly the specified rules $\vec a$, or the implicit Simplifier context if
940 no arguments are given. The result is fully simplified by default,
941 including assumptions and conclusion; the options $no_asm$ etc.\ tune the
942 Simplifier in the same way as the for the $simp$ method.
944 Note that forward simplification restricts the simplifier to its most basic
945 operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
946 are \emph{not} involved here. The $simplified$ attribute should be only
947 rarely required under normal circumstances.
952 \subsubsection{Low-level equational reasoning}
954 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
955 \begin{matharray}{rcl}
956 subst^* & : & \isarmeth \\
957 hypsubst^* & : & \isarmeth \\
958 split^* & : & \isarmeth \\
962 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
964 'split' ('(' 'asm' ')')? thmrefs
968 These methods provide low-level facilities for equational reasoning that are
969 intended for specialized applications only. Normally, single step
970 calculations would be performed in a structured text (see also
971 \S\ref{sec:calculation}), while the Simplifier methods provide the canonical
972 way for automated normalization (see \S\ref{sec:simplifier}).
976 \item [$subst~eq$] performs a single substitution step using rule $eq$, which
977 may be either a meta or object equality.
979 \item [$subst~(asm)~eq$] substitutes in an assumption.
981 \item [$subst~(i \dots j)~eq$] performs several substitutions in the
982 conclusion. The numbers $i$ to $j$ indicate the positions to substitute at.
983 Positions are ordered from the top of the term tree moving down from left to
984 right. For example, in $(a+b)+(c+d)$ there are three positions where
985 commutativity of $+$ is applicable: 1 refers to the whole term, 2 to $a+b$
986 and 3 to $c+d$. If the positions in the list $(i \dots j)$ are
987 non-overlapping (e.g. $(2~3)$ in $(a+b)+(c+d)$) you may assume all
988 substitutions are performed simultaneously. Otherwise the behaviour of
989 $subst$ is not specified.
991 \item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the
992 assumptions. Positions $1 \dots i@1$ refer
993 to assumption 1, positions $i@1+1 \dots i@2$ to assumption 2, and so on.
995 \item [$hypsubst$] performs substitution using some assumption; this only
996 works for equations of the form $x = t$ where $x$ is a free or bound
999 \item [$split~\vec a$] performs single-step case splitting using rules $thms$.
1000 By default, splitting is performed in the conclusion of a goal; the $asm$
1001 option indicates to operate on assumptions instead.
1003 Note that the $simp$ method already involves repeated application of split
1004 rules as declared in the current context.
1008 \subsection{The Classical Reasoner}\label{sec:classical}
1010 \subsubsection{Basic methods}
1012 \indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
1013 \indexisarmeth{intro}\indexisarmeth{elim}
1014 \begin{matharray}{rcl}
1015 rule & : & \isarmeth \\
1016 contradiction & : & \isarmeth \\
1017 intro & : & \isarmeth \\
1018 elim & : & \isarmeth \\
1022 ('rule' | 'intro' | 'elim') thmrefs?
1028 \item [$rule$] as offered by the classical reasoner is a refinement over the
1029 primitive one (see \S\ref{sec:pure-meth-att}). Both versions essentially
1030 work the same, but the classical version observes the classical rule context
1031 in addition to that of Isabelle/Pure.
1033 Common object logics (HOL, ZF, etc.) declare a rich collection of classical
1034 rules (even if these would qualify as intuitionistic ones), but only few
1035 declarations to the rule context of Isabelle/Pure
1036 (\S\ref{sec:pure-meth-att}).
1038 \item [$contradiction$] solves some goal by contradiction, deriving any result
1039 from both $\neg A$ and $A$. Chained facts, which are guaranteed to
1040 participate, may appear in either order.
1042 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
1043 elim-resolution, after having inserted any chained facts. Exactly the rules
1044 given as arguments are taken into account; this allows fine-tuned
1045 decomposition of a proof problem, in contrast to common automated tools.
1050 \subsubsection{Automated methods}
1052 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
1053 \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
1054 \begin{matharray}{rcl}
1055 blast & : & \isarmeth \\
1056 fast & : & \isarmeth \\
1057 slow & : & \isarmeth \\
1058 best & : & \isarmeth \\
1059 safe & : & \isarmeth \\
1060 clarify & : & \isarmeth \\
1063 \indexouternonterm{clamod}
1065 'blast' ('!' ?) nat? (clamod *)
1067 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
1070 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
1075 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
1076 in \cite[\S11]{isabelle-ref}). The optional argument specifies a
1077 user-supplied search bound (default 20).
1078 \item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
1079 classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac},
1080 \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
1081 \cite[\S11]{isabelle-ref} for more information.
1084 Any of the above methods support additional modifiers of the context of
1085 classical rules. Their semantics is analogous to the attributes given before.
1086 Facts provided by forward chaining are inserted into the goal before
1087 commencing proof search. The ``!''~argument causes the full context of
1088 assumptions to be included as well.
1091 \subsubsection{Combined automated methods}\label{sec:clasimp}
1093 \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
1094 \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
1095 \begin{matharray}{rcl}
1096 auto & : & \isarmeth \\
1097 force & : & \isarmeth \\
1098 clarsimp & : & \isarmeth \\
1099 fastsimp & : & \isarmeth \\
1100 slowsimp & : & \isarmeth \\
1101 bestsimp & : & \isarmeth \\
1104 \indexouternonterm{clasimpmod}
1106 'auto' '!'? (nat nat)? (clasimpmod *)
1108 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
1111 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
1112 ('cong' | 'split') (() | 'add' | 'del') |
1113 'iff' (((() | 'add') '?'?) | 'del') |
1114 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
1118 \item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
1119 provide access to Isabelle's combined simplification and classical reasoning
1120 tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac},
1121 \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
1122 added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The
1123 modifier arguments correspond to those given in \S\ref{sec:simplifier} and
1124 \S\ref{sec:classical}. Just note that the ones related to the Simplifier
1125 are prefixed by \railtterm{simp} here.
1127 Facts provided by forward chaining are inserted into the goal before doing
1128 the search. The ``!''~argument causes the full context of assumptions to be
1133 \subsubsection{Declaring rules}
1135 \indexisarcmd{print-claset}
1136 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
1137 \indexisaratt{iff}\indexisaratt{rule}
1138 \begin{matharray}{rcl}
1139 \isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\
1140 intro & : & \isaratt \\
1141 elim & : & \isaratt \\
1142 dest & : & \isaratt \\
1143 rule & : & \isaratt \\
1144 iff & : & \isaratt \\
1148 ('intro' | 'elim' | 'dest') ('!' | () | '?')
1152 'iff' (((() | 'add') '?'?) | 'del')
1158 \item [$\isarcmd{print_claset}$] prints the collection of rules declared to
1159 the Classical Reasoner, which is also known as ``simpset'' internally
1160 \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
1162 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
1163 destruction rules, respectively. By default, rules are considered as
1164 \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
1165 single ``!'' classifies as \emph{safe}. Rule declarations marked by ``?''
1166 coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\
1167 are only applied in single steps of the $rule$ method).
1169 \item [$rule~del$] deletes introduction, elimination, or destruction rules from
1172 \item [$iff$] declares logical equivalences to the Simplifier and the
1173 Classical reasoner at the same time. Non-conditional rules result in a
1174 ``safe'' introduction and elimination pair; conditional ones are considered
1175 ``unsafe''. Rules with negative conclusion are automatically inverted
1176 (using $\neg$ elimination internally).
1178 The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only,
1179 and omits the Simplifier declaration.
1184 \subsubsection{Classical operations}
1186 \indexisaratt{elim-format}\indexisaratt{swapped}
1188 \begin{matharray}{rcl}
1189 elim_format & : & \isaratt \\
1190 swapped & : & \isaratt \\
1195 \item [$elim_format$] turns a destruction rule into elimination rule format;
1196 this operation is similar to the the intuitionistic version
1197 (\S\ref{sec:misc-meth-att}), but each premise of the resulting rule acquires
1198 an additional local fact of the negated main thesis; according to the
1199 classical principle $(\neg A \Imp A) \Imp A$.
1201 \item [$swapped$] turns an introduction rule into an elimination, by resolving
1202 with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.
1207 \subsection{Proof by cases and induction}\label{sec:cases-induct}
1209 \subsubsection{Rule contexts}
1211 \indexisarcmd{case}\indexisarcmd{print-cases}
1212 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
1213 \begin{matharray}{rcl}
1214 \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
1215 \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
1216 case_names & : & \isaratt \\
1217 params & : & \isaratt \\
1218 consumes & : & \isaratt \\
1221 Basically, Isar proof contexts are built up explicitly using commands like
1222 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical
1223 verification tasks this can become hard to manage, though. In particular, a
1224 large number of local contexts may emerge from case analysis or induction over
1225 inductive sets and types.
1229 The $\CASENAME$ command provides a shorthand to refer to certain parts of
1230 logical context symbolically. Proof methods may provide an environment of
1231 named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of
1232 ``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term
1233 bindings may be covered as well, such as $\Var{case}$ for the intended
1236 Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$)
1237 are marked as hidden. Using the explicit form ``$\CASE{(c~\vec x)}$'' enables
1238 proof writers to choose their own names for the subsequent proof text.
1242 It is important to note that $\CASENAME$ does \emph{not} provide direct means
1243 to peek at the current goal state, which is generally considered
1244 non-observable in Isar. The text of the cases basically emerge from standard
1245 elimination or induction rules, which in turn are derived from previous theory
1246 specifications in a canonical way (say from $\isarkeyword{inductive}$
1249 Named cases may be exhibited in the current proof context only if both the
1250 proof method and the rules involved support this. Case names and parameters
1251 of basic rules may be declared by hand as well, by using appropriate
1252 attributes. Thus variant versions of rules that have been derived manually
1253 may be used in advanced case analysis later.
1255 \railalias{casenames}{case\_names}
1256 \railterm{casenames}
1259 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1261 caseref: nameref attributes?
1266 'params' ((name *) + 'and')
1274 \item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x,
1275 \vec \phi$, as provided by an appropriate proof method (such as $cases$ and
1276 $induct$, see \S\ref{sec:cases-induct-meth}). The command ``$\CASE{(c~\vec
1277 x)}$'' abbreviates ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''.
1279 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
1280 state, using Isar proof language notation. This is a diagnostic command;
1281 $undo$ does not apply.
1283 \item [$case_names~\vec c$] declares names for the local contexts of premises
1284 of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
1287 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
1288 premises $1, \dots, n$ of some theorem. An empty list of names may be given
1289 to skip positions, leaving the present parameters unchanged.
1291 Note that the default usage of case rules does \emph{not} directly expose
1292 parameters to the proof context (see also \S\ref{sec:cases-induct-meth}).
1294 \item [$consumes~n$] declares the number of ``major premises'' of a rule,
1295 i.e.\ the number of facts to be consumed when it is applied by an
1296 appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default
1297 value of $consumes$ is $n = 1$, which is appropriate for the usual kind of
1298 cases and induction rules for inductive sets (cf.\
1299 \S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given
1300 are treated as if $consumes~0$ had been specified.
1302 Note that explicit $consumes$ declarations are only rarely needed; this is
1303 already taken care of automatically by the higher-level $cases$ and $induct$
1304 declarations, see also \S\ref{sec:cases-induct-att}.
1309 \subsubsection{Proof methods}\label{sec:cases-induct-meth}
1311 \indexisarmeth{cases}\indexisarmeth{induct}
1312 \begin{matharray}{rcl}
1313 cases & : & \isarmeth \\
1314 induct & : & \isarmeth \\
1317 The $cases$ and $induct$ methods provide a uniform interface to case analysis
1318 and induction over datatypes, inductive sets, and recursive functions. The
1319 corresponding rules may be specified and instantiated in a casual manner.
1320 Furthermore, these methods provide named local contexts that may be invoked
1321 via the $\CASENAME$ proof command within the subsequent proof text. This
1322 accommodates compact proof texts even when reasoning about large
1331 spec: open? args rule?
1333 open: '(' 'open' ')'
1335 args: (insts * 'and')
1337 rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
1343 \item [$cases~insts~R$] applies method $rule$ with an appropriate case
1344 distinction theorem, instantiated to the subjects $insts$. Symbolic case
1345 names are bound according to the rule's local contexts.
1347 The rule is determined as follows, according to the facts and arguments
1348 passed to the $cases$ method:
1349 \begin{matharray}{llll}
1350 \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
1351 & cases & & \Text{classical case split} \\
1352 & cases & t & \Text{datatype exhaustion (type of $t$)} \\
1353 \edrv a \in A & cases & \dots & \Text{inductive set elimination (of $A$)} \\
1354 \dots & cases & \dots ~ R & \Text{explicit rule $R$} \\
1357 Several instantiations may be given, referring to the \emph{suffix} of
1358 premises of the case rule; within each premise, the \emph{prefix} of
1359 variables is instantiated. In most situations, only a single term needs to
1360 be specified; this refers to the first variable of the last premise (it is
1361 usually the same for all cases).
1363 The ``$(open)$'' option causes the parameters of the new local contexts to
1364 be exposed to the current proof context. Thus local variables stemming from
1365 distant parts of the theory development may be introduced in an implicit
1366 manner, which can be quite confusing to the reader. Furthermore, this
1367 option may cause unwanted hiding of existing local variables, resulting in
1368 less robust proof texts.
1370 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
1371 induction rules, which are determined as follows:
1372 \begin{matharray}{llll}
1373 \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
1374 & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
1375 \edrv x \in A & induct & \dots & \Text{set induction (of $A$)} \\
1376 \dots & induct & \dots ~ R & \Text{explicit rule $R$} \\
1379 Several instantiations may be given, each referring to some part of a mutual
1380 inductive definition or datatype --- only related partial induction rules
1381 may be used together, though. Any of the lists of terms $P, x, \dots$
1382 refers to the \emph{suffix} of variables present in the induction rule.
1383 This enables the writer to specify only induction variables, or both
1384 predicates and variables, for example.
1386 The ``$(open)$'' option works the same way as for $cases$.
1390 Above methods produce named local contexts, as determined by the instantiated
1391 rule as specified in the text. Beyond that, the $induct$ method guesses
1392 further instantiations from the goal specification itself. Any persisting
1393 unresolved schematic variables of the resulting rule will render the the
1394 corresponding case invalid. The term binding $\Var{case}$\indexisarvar{case}
1395 for the conclusion will be provided with each case, provided that term is
1398 The $\isarkeyword{print_cases}$ command prints all named cases present in the
1399 current proof state.
1403 It is important to note that there is a fundamental difference of the $cases$
1404 and $induct$ methods in handling of non-atomic goal statements: $cases$ just
1405 applies a certain rule in backward fashion, splitting the result into new
1406 goals with the local contexts being augmented in a purely monotonic manner.
1408 In contrast, $induct$ passes the full goal statement through the
1409 ``recursive'' course involved in the induction. Thus the original statement
1410 is basically replaced by separate copies, corresponding to the induction
1411 hypotheses and conclusion; the original goal context is no longer available.
1412 This behavior allows \emph{strengthened induction predicates} to be expressed
1413 concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp
1414 \psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive''
1415 assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs
1416 ``$\FIX{\vec x}$''. Also note that local definitions may be expressed as
1417 $\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
1420 In induction proofs, local assumptions introduced by cases are split into two
1421 different kinds: $hyps$ stemming from the rule and $prems$ from the goal
1422 statement. This is reflected in the extracted cases accordingly, so invoking
1423 ``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and
1424 $c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list.
1428 Facts presented to either method are consumed according to the number of
1429 ``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}),
1430 which is usually $0$ for plain cases and induction rules of datatypes etc.\
1431 and $1$ for rules of inductive sets and the like. The remaining facts are
1432 inserted into the goal verbatim before the actual $cases$ or $induct$ rule is
1433 applied (thus facts may be even passed through an induction).
1436 \subsubsection{Declaring rules}\label{sec:cases-induct-att}
1438 \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
1439 \begin{matharray}{rcl}
1440 \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
1441 cases & : & \isaratt \\
1442 induct & : & \isaratt \\
1451 spec: ('type' | 'set') ':' nameref
1457 \item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
1458 sets and types of the current context.
1460 \item [$cases$ and $induct$] (as attributes) augment the corresponding context
1461 of rules for reasoning about inductive sets and types, using the
1462 corresponding methods of the same name. Certain definitional packages of
1463 object-logics usually declare emerging cases and induction rules as
1464 expected, so users rarely need to intervene.
1466 Manual rule declarations usually include the the $case_names$ and $ps$
1467 attributes to adjust names of cases and parameters of a rule (see
1468 \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of
1469 automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
1474 %%% Local Variables:
1476 %%% TeX-master: "isar-ref"