3 \def\isabellecontext{Generic}%
12 \isacommand{theory}\isamarkupfalse%
14 \isakeyword{imports}\ CPure\isanewline
23 \isamarkupchapter{Generic tools and packages \label{ch:gen-tools}%
27 \isamarkupsection{Specification commands%
31 \isamarkupsubsection{Derived specifications%
35 \begin{isamarkuptext}%
36 \begin{matharray}{rcll}
37 \indexdef{}{command}{axiomatization}\mbox{\isa{\isacommand{axiomatization}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
38 \indexdef{}{command}{definition}\mbox{\isa{\isacommand{definition}}} & : & \isarkeep{local{\dsh}theory} \\
39 \indexdef{}{attribute}{defn}\mbox{\isa{defn}} & : & \isaratt \\
40 \indexdef{}{command}{abbreviation}\mbox{\isa{\isacommand{abbreviation}}} & : & \isarkeep{local{\dsh}theory} \\
41 \indexdef{}{command}{print-abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
42 \indexdef{}{command}{notation}\mbox{\isa{\isacommand{notation}}} & : & \isarkeep{local{\dsh}theory} \\
43 \indexdef{}{command}{no-notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
46 These specification mechanisms provide a slightly more abstract view
47 than the underlying primitives of \mbox{\isa{\isacommand{consts}}}, \mbox{\isa{\isacommand{defs}}} (see \secref{sec:consts}), and \mbox{\isa{\isacommand{axioms}}} (see
48 \secref{sec:axms-thms}). In particular, type-inference is commonly
49 available, and result names need not be given.
52 'axiomatization' target? fixes? ('where' specs)?
54 'definition' target? (decl 'where')? thmdecl? prop
56 'abbreviation' target? mode? (decl 'where')? prop
58 ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
61 fixes: ((name ('::' type)? mixfix? | vars) + 'and')
63 specs: (thmdecl? props + 'and')
65 decl: name ('::' type)? mixfix?
71 \item [\mbox{\isa{\isacommand{axiomatization}}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}] introduces several constants
72 simultaneously and states axiomatic properties for these. The
73 constants are marked as being specified once and for all, which
74 prevents additional specifications being issued later on.
76 Note that axiomatic specifications are only appropriate when
77 declaring a new logical system. Normal applications should only use
78 definitional mechanisms!
80 \item [\mbox{\isa{\isacommand{definition}}}~\isa{c\ {\isasymWHERE}\ eq}] produces an
81 internal definition \isa{c\ {\isasymequiv}\ t} according to the specification
82 given as \isa{eq}, which is then turned into a proven fact. The
83 given proposition may deviate from internal meta-level equality
84 according to the rewrite rules declared as \mbox{\isa{defn}} by the
85 object-logic. This typically covers object-level equality \isa{x\ {\isacharequal}\ t} and equivalence \isa{A\ {\isasymleftrightarrow}\ B}. End-users normally need not
86 change the \mbox{\isa{defn}} setup.
88 Definitions may be presented with explicit arguments on the LHS, as
89 well as additional conditions, e.g.\ \isa{f\ x\ y\ {\isacharequal}\ t} instead of
90 \isa{f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t} and \isa{y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u} instead of an
91 unrestricted \isa{g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u}.
93 \item [\mbox{\isa{\isacommand{abbreviation}}}~\isa{c\ {\isasymWHERE}\ eq}] introduces
94 a syntactic constant which is associated with a certain term
95 according to the meta-level equality \isa{eq}.
97 Abbreviations participate in the usual type-inference process, but
98 are expanded before the logic ever sees them. Pretty printing of
99 terms involves higher-order rewriting with rules stemming from
100 reverted abbreviations. This needs some care to avoid overlapping
101 or looping syntactic replacements!
103 The optional \isa{mode} specification restricts output to a
104 particular print mode; using ``\isa{input}'' here achieves the
105 effect of one-way abbreviations. The mode may also include an
106 ``\mbox{\isa{\isakeyword{output}}}'' qualifier that affects the concrete syntax
107 declared for abbreviations, cf.\ \mbox{\isa{\isacommand{syntax}}} in
108 \secref{sec:syn-trans}.
110 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}] prints all constant abbreviations
111 of the current context.
113 \item [\mbox{\isa{\isacommand{notation}}}~\isa{c\ {\isacharparenleft}mx{\isacharparenright}}] associates mixfix
114 syntax with an existing constant or fixed variable. This is a
115 robust interface to the underlying \mbox{\isa{\isacommand{syntax}}} primitive
116 (\secref{sec:syn-trans}). Type declaration and internal syntactic
117 representation of the given entity is retrieved from the context.
119 \item [\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}] is similar to \mbox{\isa{\isacommand{notation}}}, but removes the specified syntax annotation from the
124 All of these specifications support local theory targets (cf.\
125 \secref{sec:target}).%
129 \isamarkupsubsection{Generic declarations%
133 \begin{isamarkuptext}%
134 Arbitrary operations on the background context may be wrapped-up as
135 generic declaration elements. Since the underlying concept of local
136 theories may be subject to later re-interpretation, there is an
137 additional dependency on a morphism that tells the difference of the
138 original declaration context wrt.\ the application context
139 encountered later on. A fact declaration is an important special
140 case: it consists of a theorem which is applied to the context by
141 means of an attribute.
143 \begin{matharray}{rcl}
144 \indexdef{}{command}{declaration}\mbox{\isa{\isacommand{declaration}}} & : & \isarkeep{local{\dsh}theory} \\
145 \indexdef{}{command}{declare}\mbox{\isa{\isacommand{declare}}} & : & \isarkeep{local{\dsh}theory} \\
149 'declaration' target? text
151 'declare' target? (thmrefs + 'and')
157 \item [\mbox{\isa{\isacommand{declaration}}}~\isa{d}] adds the declaration
158 function \isa{d} of ML type \verb|declaration|, to the current
159 local theory under construction. In later application contexts, the
160 function is transformed according to the morphisms being involved in
161 the interpretation hierarchy.
163 \item [\mbox{\isa{\isacommand{declare}}}~\isa{thms}] declares theorems to the
164 current local theory context. No theorem binding is involved here,
165 unlike \mbox{\isa{\isacommand{theorems}}} or \mbox{\isa{\isacommand{lemmas}}} (cf.\
166 \secref{sec:axms-thms}), so \mbox{\isa{\isacommand{declare}}} only has the effect
167 of applying attributes as included in the theorem specification.
173 \isamarkupsubsection{Local theory targets \label{sec:target}%
177 \begin{isamarkuptext}%
178 A local theory target is a context managed separately within the
179 enclosing theory. Contexts may introduce parameters (fixed
180 variables) and assumptions (hypotheses). Definitions and theorems
181 depending on the context may be added incrementally later on. Named
182 contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
183 (cf.\ \secref{sec:class}); the name ``\isa{{\isacharminus}}'' signifies the
184 global theory context.
186 \begin{matharray}{rcll}
187 \indexdef{}{command}{context}\mbox{\isa{\isacommand{context}}} & : & \isartrans{theory}{local{\dsh}theory} \\
188 \indexdef{}{command}{end}\mbox{\isa{\isacommand{end}}} & : & \isartrans{local{\dsh}theory}{theory} \\
191 \indexouternonterm{target}
193 'context' name 'begin'
196 target: '(' 'in' name ')'
202 \item [\mbox{\isa{\isacommand{context}}}~\isa{c\ {\isasymBEGIN}}] recommences an
203 existing locale or class context \isa{c}. Note that locale and
204 class definitions allow to include the \indexref{}{keyword}{begin}\mbox{\isa{\isakeyword{begin}}}
205 keyword as well, in order to continue the local theory immediately
206 after the initial specification.
208 \item [\mbox{\isa{\isacommand{end}}}] concludes the current local theory and
209 continues the enclosing global theory. Note that a non-local
210 \mbox{\isa{\isacommand{end}}} has a different meaning: it concludes the theory
211 itself (\secref{sec:begin-thy}).
213 \item [\isa{{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}}] given after any local theory command
214 specifies an immediate target, e.g.\ ``\mbox{\isa{\isacommand{definition}}}~\isa{{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}}'' or ``\mbox{\isa{\isacommand{theorem}}}~\isa{{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}}''. This works both in a local or
215 global theory context; the current target context will be suspended
216 for this command only. Note that \isa{{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}} will always
217 produce a global result independently of the current target context.
221 The exact meaning of results produced within a local theory context
222 depends on the underlying target infrastructure (locale, type class
223 etc.). The general idea is as follows, considering a context named
224 \isa{c} with parameter \isa{x} and assumption \isa{A{\isacharbrackleft}x{\isacharbrackright}}.
226 Definitions are exported by introducing a global version with
227 additional arguments; a syntactic abbreviation links the long form
228 with the abstract version of the target context. For example,
229 \isa{a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}} becomes \isa{c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}} at the theory
230 level (for arbitrary \isa{{\isacharquery}x}), together with a local
231 abbreviation \isa{c\ {\isasymequiv}\ c{\isachardot}a\ x} in the target context (for the
232 fixed parameter \isa{x}).
234 Theorems are exported by discharging the assumptions and
235 generalizing the parameters of the context. For example, \isa{a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}} becomes \isa{c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}} (again for arbitrary
236 \isa{{\isacharquery}x}).%
240 \isamarkupsubsection{Locales \label{sec:locale}%
244 \begin{isamarkuptext}%
245 Locales are named local contexts, consisting of a list of
246 declaration elements that are modeled after the Isar proof context
247 commands (cf.\ \secref{sec:proof-context}).%
251 \isamarkupsubsubsection{Locale specifications%
255 \begin{isamarkuptext}%
256 \begin{matharray}{rcl}
257 \indexdef{}{command}{locale}\mbox{\isa{\isacommand{locale}}} & : & \isartrans{theory}{local{\dsh}theory} \\
258 \indexdef{}{command}{print-locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
259 \indexdef{}{command}{print-locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
260 \indexdef{}{method}{intro-locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
261 \indexdef{}{method}{unfold-locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
264 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
265 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
266 \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
268 'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
270 'print\_locale' '!'? localeexpr
272 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
275 contextexpr: nameref | '(' contextexpr ')' |
276 (contextexpr (name mixfix? +)) | (contextexpr + '+')
278 contextelem: fixes | constrains | assumes | defines | notes
280 fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
282 constrains: 'constrains' (name '::' type + 'and')
284 assumes: 'assumes' (thmdecl? props + 'and')
286 defines: 'defines' (thmdecl? prop proppat? + 'and')
288 notes: 'notes' (thmdef? thmrefs + 'and')
290 includes: 'includes' contextexpr
296 \item [\mbox{\isa{\isacommand{locale}}}~\isa{loc\ {\isacharequal}\ import\ {\isacharplus}\ body}] defines a
297 new locale \isa{loc} as a context consisting of a certain view of
298 existing locales (\isa{import}) plus some additional elements
299 (\isa{body}). Both \isa{import} and \isa{body} are optional;
300 the degenerate form \mbox{\isa{\isacommand{locale}}}~\isa{loc} defines an empty
301 locale, which may still be useful to collect declarations of facts
302 later on. Type-inference on locale expressions automatically takes
303 care of the most general typing that the combined context elements
306 The \isa{import} consists of a structured context expression,
307 consisting of references to existing locales, renamed contexts, or
308 merged contexts. Renaming uses positional notation: \isa{c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n} means that (a prefix of) the fixed
309 parameters of context \isa{c} are named \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
310 position. Renaming by default deletes concrete syntax, but new
311 syntax may by specified with a mixfix annotation. An exeption of
312 this rule is the special syntax declared with ``\isa{{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}}'' (see below), which is neither deleted nor can it
313 be changed. Merging proceeds from left-to-right, suppressing any
314 duplicates stemming from different paths through the import
317 The \isa{body} consists of basic context elements, further context
318 expressions may be included as well.
322 \item [\mbox{\isa{fixes}}~\isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}}] declares a local
323 parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
324 are optional). The special syntax declaration ``\isa{{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}}'' means that \isa{x} may be referenced
325 implicitly in this context.
327 \item [\mbox{\isa{constrains}}~\isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}] introduces a type
328 constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
330 \item [\mbox{\isa{assumes}}~\isa{a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}]
331 introduces local premises, similar to \mbox{\isa{\isacommand{assume}}} within a
332 proof (cf.\ \secref{sec:proof-context}).
334 \item [\mbox{\isa{defines}}~\isa{a{\isacharcolon}\ x\ {\isasymequiv}\ t}] defines a previously
335 declared parameter. This is close to \mbox{\isa{\isacommand{def}}} within a
336 proof (cf.\ \secref{sec:proof-context}), but \mbox{\isa{defines}}
337 takes an equational proposition instead of variable-term pair. The
338 left-hand side of the equation may have additional arguments, e.g.\
339 ``\mbox{\isa{defines}}~\isa{f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t}''.
341 \item [\mbox{\isa{notes}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}]
342 reconsiders facts within a local context. Most notably, this may
343 include arbitrary declarations in any attribute specifications
344 included here, e.g.\ a local \mbox{\isa{simp}} rule.
346 \item [\mbox{\isa{includes}}~\isa{c}] copies the specified context
347 in a statically scoped manner. Only available in the long goal
348 format of \secref{sec:goals}.
350 In contrast, the initial \isa{import} specification of a locale
351 expression maintains a dynamic relation to the locales being
352 referenced (benefiting from any later fact declarations in the
357 Note that ``\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}'' patterns given
358 in the syntax of \mbox{\isa{assumes}} and \mbox{\isa{defines}} above
359 are illegal in locale definitions. In the long goal format of
360 \secref{sec:goals}, term bindings may be included as expected,
363 \medskip By default, locale specifications are ``closed up'' by
364 turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
365 (modulo local definitions). The predicate statement covers only the
366 newly specified assumptions, omitting the content of included locale
367 expressions. The full cumulative view is only provided on export,
368 involving another predicate \isa{loc} that refers to the complete
371 In any case, the predicate arguments are those locale parameters
372 that actually occur in the respective piece of text. Also note that
373 these predicates operate at the meta-level in theory, but the locale
374 packages attempts to internalize statements according to the
375 object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
376 \isa{{\isasymLongrightarrow}} by \isa{{\isasymlongrightarrow}} in HOL; see also
377 \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
379 The \isa{{\isacharparenleft}open{\isacharparenright}} option of a locale specification prevents both
380 the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
381 constructions. Predicates are also omitted for empty specification
384 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{import\ {\isacharplus}\ body}] prints the
385 specified locale expression in a flattened form. The notable
386 special case \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}~\isa{loc} just prints the
387 contents of the named locale, but keep in mind that type-inference
388 will normalize type variables according to the usual alphabetical
389 order. The command omits \mbox{\isa{notes}} elements by default.
390 Use \mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isacharbang}} to get them included.
392 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}] prints the names of all locales
393 of the current theory.
395 \item [\mbox{\isa{intro{\isacharunderscore}locales}} and \mbox{\isa{unfold{\isacharunderscore}locales}}]
396 repeatedly expand all introduction rules of locale predicates of the
397 theory. While \mbox{\isa{intro{\isacharunderscore}locales}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
398 assumptions, \mbox{\isa{unfold{\isacharunderscore}locales}} is more aggressive and applies
399 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale
400 specifications entailed by the context, both from target and
401 \mbox{\isa{includes}} statements, and from interpretations (see
402 below). New goals that are entailed by the current context are
403 discharged automatically.
409 \isamarkupsubsubsection{Interpretation of locales%
413 \begin{isamarkuptext}%
414 Locale expressions (more precisely, \emph{context expressions}) may
415 be instantiated, and the instantiated facts added to the current
416 context. This requires a proof of the instantiated specification
417 and is called \emph{locale interpretation}. Interpretation is
418 possible in theories and locales (command \mbox{\isa{\isacommand{interpretation}}}) and also within a proof body (\mbox{\isa{\isacommand{interpret}}}).
420 \begin{matharray}{rcl}
421 \indexdef{}{command}{interpretation}\mbox{\isa{\isacommand{interpretation}}} & : & \isartrans{theory}{proof(prove)} \\
422 \indexdef{}{command}{interpret}\mbox{\isa{\isacommand{interpret}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
423 \indexdef{}{command}{print-interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
426 \indexouternonterm{interp}
428 'interpretation' (interp | name ('<' | subseteq) contextexpr)
432 'print\_interps' '!'? name
434 instantiation: ('[' (inst+) ']')?
436 interp: thmdecl? \\ (contextexpr instantiation |
437 name instantiation 'where' (thmdecl? prop + 'and'))
443 \item [\mbox{\isa{\isacommand{interpretation}}}~\isa{expr\ insts\ {\isasymWHERE}\ eqns}]
445 The first form of \mbox{\isa{\isacommand{interpretation}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms
446 \isa{insts} and is positional. All parameters must receive an
447 instantiation term --- with the exception of defined parameters.
448 These are, if omitted, derived from the defining equation and other
449 instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
450 Free variables are automatically generalized.
452 The command generates proof obligations for the instantiated
453 specifications (assumes and defines elements). Once these are
454 discharged by the user, instantiated facts are added to the theory
455 in a post-processing phase.
457 Additional equations, which are unfolded in facts during
458 post-processing, may be given after the keyword \mbox{\isa{\isakeyword{where}}}.
459 This is useful for interpreting concepts introduced through
460 definition specification elements. The equations must be proved.
461 Note that if equations are present, the context expression is
462 restricted to a locale name.
464 The command is aware of interpretations already active in the
465 theory. No proof obligations are generated for those, neither is
466 post-processing applied to their facts. This avoids duplication of
467 interpreted facts, in particular. Note that, in the case of a
468 locale with import, parts of the interpretation may already be
469 active. The command will only generate proof obligations and
470 process facts for new parts.
472 The context expression may be preceded by a name and/or attributes.
473 These take effect in the post-processing of facts. The name is used
474 to prefix fact names, for example to avoid accidental hiding of
475 other facts. Attributes are applied after attributes of the
478 Adding facts to locales has the effect of adding interpreted facts
479 to the theory for all active interpretations also. That is,
480 interpretations dynamically participate in any facts added to
483 \item [\mbox{\isa{\isacommand{interpretation}}}~\isa{name\ {\isasymsubseteq}\ expr}]
485 This form of the command interprets \isa{expr} in the locale
486 \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the
487 localized version of the theorem command, the proof is in the
488 context of \isa{name}. After the proof obligation has been
489 dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
490 context \isa{name} is subsequently entered. Note that, like
491 import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
492 Like facts of renamed context elements, facts obtained by
493 interpretation may be accessed by prefixing with the parameter
494 renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
496 Unlike interpretation in theories, instantiation is confined to the
497 renaming of parameters, which may be specified as part of the
498 context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
500 Only specification fragments of \isa{expr} that are not already
501 part of \isa{name} (be it imported, derived or a derived fragment
502 of the import) are considered by interpretation. This enables
503 circular interpretations.
505 If interpretations of \isa{name} exist in the current theory, the
506 command adds interpretations for \isa{expr} as well, with the same
507 prefix and attributes, although only for fragments of \isa{expr}
508 that are not interpreted in the theory already.
510 \item [\mbox{\isa{\isacommand{interpret}}}~\isa{expr\ insts\ {\isasymWHERE}\ eqns}]
511 interprets \isa{expr} in the proof context and is otherwise
512 similar to interpretation in theories. Free variables in
513 instantiations are not generalized, however.
515 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}~\isa{loc}] prints the
516 interpretations of a particular locale \isa{loc} that are active
517 in the current context, either theory or proof context. The
518 exclamation point argument triggers printing of \emph{witness}
519 theorems justifying interpretations. These are normally omitted
525 Since attributes are applied to interpreted theorems,
526 interpretation may modify the context of common proof tools, e.g.\
527 the Simplifier or Classical Reasoner. Since the behavior of such
528 automated reasoning tools is \emph{not} stable under
529 interpretation morphisms, manual declarations might have to be
534 An interpretation in a theory may subsume previous
535 interpretations. This happens if the same specification fragment
536 is interpreted twice and the instantiation of the second
537 interpretation is more general than the interpretation of the
538 first. A warning is issued, since it is likely that these could
539 have been generalized in the first place. The locale package does
540 not attempt to remove subsumed interpretations.
545 \isamarkupsubsection{Classes \label{sec:class}%
549 \begin{isamarkuptext}%
550 A class is a particular locale with \emph{exactly one} type variable
551 \isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class
552 is established which is interpreted logically as axiomatic type
553 class \cite{Wenzel:1997:TPHOL} whose logical content are the
554 assumptions of the locale. Thus, classes provide the full
555 generality of locales combined with the commodity of type classes
556 (notably type-inference). See \cite{isabelle-classes} for a short
559 \begin{matharray}{rcl}
560 \indexdef{}{command}{class}\mbox{\isa{\isacommand{class}}} & : & \isartrans{theory}{local{\dsh}theory} \\
561 \indexdef{}{command}{instantiation}\mbox{\isa{\isacommand{instantiation}}} & : & \isartrans{theory}{local{\dsh}theory} \\
562 \indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
563 \indexdef{}{command}{subclass}\mbox{\isa{\isacommand{subclass}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
564 \indexdef{}{command}{print-classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
565 \indexdef{}{method}{intro-classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
569 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
572 'instantiation' (nameref + 'and') '::' arity 'begin'
576 'subclass' target? nameref
581 superclassexpr: nameref | (nameref '+' superclassexpr)
587 \item [\mbox{\isa{\isacommand{class}}}~\isa{c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body}] defines
588 a new class \isa{c}, inheriting from \isa{superclasses}. This
589 introduces a locale \isa{c} with import of all locales \isa{superclasses}.
591 Any \mbox{\isa{fixes}} in \isa{body} are lifted to the global
592 theory level (\emph{class operations} \isa{f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n} of class \isa{c}), mapping the local type parameter
593 \isa{{\isasymalpha}} to a schematic type variable \isa{{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c}.
595 Likewise, \mbox{\isa{assumes}} in \isa{body} are also lifted,
596 mapping each local parameter \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} to its
597 corresponding global constant \isa{f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}}. The
598 corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly
599 --- the \mbox{\isa{intro{\isacharunderscore}classes}} method takes care of the details of
600 class membership proofs.
602 \item [\mbox{\isa{\isacommand{instantiation}}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}}] opens a theory target (cf.\
603 \secref{sec:target}) which allows to specify class operations \isa{f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n} corresponding to sort \isa{s} at the
604 particular type instance \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t}. An plain \mbox{\isa{\isacommand{instance}}} command
605 in the target body poses a goal stating these type arities. The
606 target is concluded by an \indexref{}{command}{end}\mbox{\isa{\isacommand{end}}} command.
608 Note that a list of simultaneous type constructors may be given;
609 this corresponds nicely to mutual recursive type definitions, e.g.\
612 \item [\mbox{\isa{\isacommand{instance}}}] in an instantiation target body sets
613 up a goal stating the type arities claimed at the opening \mbox{\isa{\isacommand{instantiation}}}. The proof would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish the characteristic theorems of
614 the type classes involved. After finishing the proof, the
615 background theory will be augmented by the proven type arities.
617 \item [\mbox{\isa{\isacommand{subclass}}}~\isa{c}] in a class context for class
618 \isa{d} sets up a goal stating that class \isa{c} is logically
619 contained in class \isa{d}. After finishing the proof, class
620 \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
622 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}] prints all classes in the current
625 \item [\mbox{\isa{intro{\isacharunderscore}classes}}] repeatedly expands all class
626 introduction rules of this theory. Note that this method usually
627 needs not be named explicitly, as it is already included in the
628 default proof step (e.g.\ of \mbox{\isa{\isacommand{proof}}}). In particular,
629 instantiation of trivial (syntactic) classes may be performed by a
630 single ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' proof step.
636 \isamarkupsubsubsection{The class target%
640 \begin{isamarkuptext}%
643 A named context may refer to a locale (cf.\ \secref{sec:target}).
644 If this locale is also a class \isa{c}, apart from the common
645 locale target behaviour the following happens.
649 \item Local constant declarations \isa{g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} referring to the
650 local type parameter \isa{{\isasymalpha}} and local parameters \isa{f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}
651 are accompanied by theory-level constants \isa{g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}}
652 referring to theory-level class operations \isa{f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}}.
654 \item Local theorem bindings are lifted as are assumptions.
656 \item Local syntax refers to local operations \isa{g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} and
657 global operations \isa{g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}} uniformly. Type inference
658 resolves ambiguities. In rare cases, manual type annotations are
665 \isamarkupsubsection{Axiomatic type classes \label{sec:axclass}%
669 \begin{isamarkuptext}%
670 \begin{matharray}{rcl}
671 \indexdef{}{command}{axclass}\mbox{\isa{\isacommand{axclass}}} & : & \isartrans{theory}{theory} \\
672 \indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{theory}{proof(prove)} \\
675 Axiomatic type classes are Isabelle/Pure's primitive
676 \emph{definitional} interface to type classes. For practical
677 applications, you should consider using classes
678 (cf.~\secref{sec:classes}) which provide high level interface.
681 'axclass' classdecl (axmdecl prop +)
683 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
689 \item [\mbox{\isa{\isacommand{axclass}}}~\isa{c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms}] defines an axiomatic type class as the intersection of
690 existing classes, with additional axioms holding. Class axioms may
691 not contain more than one type variable. The class axioms (with
692 implicit sort constraints added) are bound to the given names.
693 Furthermore a class introduction rule is generated (being bound as
694 \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \mbox{\isa{intro{\isacharunderscore}classes}} to support instantiation proofs of this class.
696 The ``class axioms'' are stored as theorems according to the given
697 name specifications, adding \isa{c{\isacharunderscore}class} as name space prefix;
698 the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
700 \item [\mbox{\isa{\isacommand{instance}}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}} and
701 \mbox{\isa{\isacommand{instance}}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s}]
702 setup a goal stating a class relation or type arity. The proof
703 would usually proceed by \mbox{\isa{intro{\isacharunderscore}classes}}, and then establish
704 the characteristic theorems of the type classes involved. After
705 finishing the proof, the theory will be augmented by a type
706 signature declaration corresponding to the resulting theorem.
712 \isamarkupsubsection{Arbitrary overloading%
716 \begin{isamarkuptext}%
717 Isabelle/Pure's definitional schemes support certain forms of
718 overloading (see \secref{sec:consts}). At most occassions
719 overloading will be used in a Haskell-like fashion together with
720 type classes by means of \mbox{\isa{\isacommand{instantiation}}} (see
721 \secref{sec:class}). Sometimes low-level overloading is desirable.
722 The \mbox{\isa{\isacommand{overloading}}} target provides a convenient view for
725 \begin{matharray}{rcl}
726 \indexdef{}{command}{overloading}\mbox{\isa{\isacommand{overloading}}} & : & \isartrans{theory}{local{\dsh}theory} \\
731 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
736 \item [\mbox{\isa{\isacommand{overloading}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n{\isacharbraceright}\ {\isasymBEGIN}}]
737 opens a theory target (cf.\ \secref{sec:target}) which allows to
738 specify constants with overloaded definitions. These are identified
739 by an explicitly given mapping from variable names \isa{x\isactrlsub i} to constants \isa{c\isactrlsub i} at particular type
740 instances. The definitions themselves are established using common
741 specification tools, using the names \isa{x\isactrlsub i} as
742 reference to the corresponding constants. The target is concluded
743 by \mbox{\isa{\isacommand{end}}}.
745 A \isa{{\isacharparenleft}unchecked{\isacharparenright}} option disables global dependency checks for
746 the corresponding definition, which is occasionally useful for
747 exotic overloading. It is at the discretion of the user to avoid
748 malformed theory specifications!
754 \isamarkupsubsection{Configuration options%
758 \begin{isamarkuptext}%
759 Isabelle/Pure maintains a record of named configuration options
760 within the theory or proof context, with values of type \verb|bool|, \verb|int|, or \verb|string|. Tools may declare
761 options in ML, and then refer to these values (relative to the
762 context). Thus global reference variables are easily avoided. The
763 user may change the value of a configuration option by means of an
764 associated attribute of the same name. This form of context
765 declaration works particularly well with commands such as \mbox{\isa{\isacommand{declare}}} or \mbox{\isa{\isacommand{using}}}.
767 For historical reasons, some tools cannot take the full proof
768 context into account and merely refer to the background theory.
769 This is accommodated by configuration options being declared as
770 ``global'', which may not be changed within a local context.
772 \begin{matharray}{rcll}
773 \indexdef{}{command}{print-configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
777 name ('=' ('true' | 'false' | int | name))?
782 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}}] prints the available
783 configuration options, with names, types, and current values.
785 \item [\isa{name\ {\isacharequal}\ value}] as an attribute expression modifies
786 the named option, with the syntax of the value depending on the
787 option's type. For \verb|bool| the default value is \isa{true}. Any attempt to change a global option in a local context is
794 \isamarkupsection{Derived proof schemes%
798 \isamarkupsubsection{Generalized elimination \label{sec:obtain}%
802 \begin{isamarkuptext}%
803 \begin{matharray}{rcl}
804 \indexdef{}{command}{obtain}\mbox{\isa{\isacommand{obtain}}} & : & \isartrans{proof(state)}{proof(prove)} \\
805 \indexdef{}{command}{guess}\mbox{\isa{\isacommand{guess}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isartrans{proof(state)}{proof(prove)} \\
808 Generalized elimination means that additional elements with certain
809 properties may be introduced in the current context, by virtue of a
810 locally proven ``soundness statement''. Technically speaking, the
811 \mbox{\isa{\isacommand{obtain}}} language element is like a declaration of
812 \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} (see also see
813 \secref{sec:proof-context}), together with a soundness proof of its
814 additional claim. According to the nature of existential reasoning,
815 assumptions get eliminated from any result exported from the context
816 later, provided that the corresponding parameters do \emph{not}
817 occur in the conclusion.
820 'obtain' parname? (vars + 'and') 'where' (props + 'and')
822 'guess' (vars + 'and')
826 The derived Isar command \mbox{\isa{\isacommand{obtain}}} is defined as follows
827 (where \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k} shall refer to (optional)
828 facts indicated for forward chaining).
830 \isa{{\isasymlangle}facts\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}} \\
831 \mbox{\isa{\isacommand{obtain}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}} \\[1ex]
832 \quad \mbox{\isa{\isacommand{have}}}~\isa{{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis} \\
833 \quad \mbox{\isa{\isacommand{proof}}}~\isa{succeed} \\
834 \qquad \mbox{\isa{\isacommand{fix}}}~\isa{thesis} \\
835 \qquad \mbox{\isa{\isacommand{assume}}}~\isa{that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis} \\
836 \qquad \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}~\isa{thesis} \\
837 \quad\qquad \mbox{\isa{\isacommand{apply}}}~\isa{{\isacharminus}} \\
838 \quad\qquad \mbox{\isa{\isacommand{using}}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}} \\
839 \quad \mbox{\isa{\isacommand{qed}}} \\
840 \quad \mbox{\isa{\isacommand{fix}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}~\mbox{\isa{\isacommand{assume}}}\isa{\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n} \\
843 Typically, the soundness proof is relatively straight-forward, often
844 just by canonical automated tools such as ``\mbox{\isa{\isacommand{by}}}~\isa{simp}'' or ``\mbox{\isa{\isacommand{by}}}~\isa{blast}''. Accordingly, the
845 ``\isa{that}'' reduction above is declared as simplification and
848 In a sense, \mbox{\isa{\isacommand{obtain}}} represents at the level of Isar
849 proofs what would be meta-logical existential quantifiers and
850 conjunctions. This concept has a broad range of useful
851 applications, ranging from plain elimination (or introduction) of
852 object-level existential and conjunctions, to elimination over
853 results of symbolic evaluation of recursive definitions, for
854 example. Also note that \mbox{\isa{\isacommand{obtain}}} without parameters acts
855 much like \mbox{\isa{\isacommand{have}}}, where the result is treated as a
858 An alternative name to be used instead of ``\isa{that}'' above may
859 be given in parentheses.
861 \medskip The improper variant \mbox{\isa{\isacommand{guess}}} is similar to
862 \mbox{\isa{\isacommand{obtain}}}, but derives the obtained statement from the
863 course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
864 form like \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis}, but must not introduce new subgoals. The
865 final goal state is then used as reduction rule for the obtain
866 scheme described above. Obtained parameters \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m} are marked as internal by default, which prevents the
867 proof context from being polluted by ad-hoc variables. The variable
868 names and type constraints given as arguments for \mbox{\isa{\isacommand{guess}}}
869 specify a prefix of obtained parameters explicitly in the text.
871 It is important to note that the facts introduced by \mbox{\isa{\isacommand{obtain}}} and \mbox{\isa{\isacommand{guess}}} may not be polymorphic: any
872 type-variables occurring here are fixed in the present context!%
876 \isamarkupsubsection{Calculational reasoning \label{sec:calculation}%
880 \begin{isamarkuptext}%
881 \begin{matharray}{rcl}
882 \indexdef{}{command}{also}\mbox{\isa{\isacommand{also}}} & : & \isartrans{proof(state)}{proof(state)} \\
883 \indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
884 \indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
885 \indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
886 \indexdef{}{command}{print-trans-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
887 \mbox{\isa{trans}} & : & \isaratt \\
888 \mbox{\isa{sym}} & : & \isaratt \\
889 \mbox{\isa{symmetric}} & : & \isaratt \\
892 Calculational proof is forward reasoning with implicit application
893 of transitivity rules (such those of \isa{{\isacharequal}}, \isa{{\isasymle}},
894 \isa{{\isacharless}}). Isabelle/Isar maintains an auxiliary fact register
895 \indexref{}{fact}{calculation}\mbox{\isa{calculation}} for accumulating results obtained by
896 transitivity composed with the current result. Command \mbox{\isa{\isacommand{also}}} updates \mbox{\isa{calculation}} involving \mbox{\isa{this}}, while
897 \mbox{\isa{\isacommand{finally}}} exhibits the final \mbox{\isa{calculation}} by
898 forward chaining towards the next goal statement. Both commands
899 require valid current facts, i.e.\ may occur only after commands
900 that produce theorems such as \mbox{\isa{\isacommand{assume}}}, \mbox{\isa{\isacommand{note}}}, or some finished proof of \mbox{\isa{\isacommand{have}}}, \mbox{\isa{\isacommand{show}}} etc. The \mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}
901 commands are similar to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}},
902 but only collect further results in \mbox{\isa{calculation}} without
903 applying any rules yet.
905 Also note that the implicit term abbreviation ``\isa{{\isasymdots}}'' has
906 its canonical application with calculational proofs. It refers to
907 the argument of the preceding statement. (The argument of a curried
908 infix expression happens to be its right-hand side.)
910 Isabelle/Isar calculations are implicitly subject to block structure
911 in the sense that new threads of calculational reasoning are
912 commenced for any new block (as opened by a local goal, for
913 example). This means that, apart from being able to nest
914 calculations, there is no separate \emph{begin-calculation} command
917 \medskip The Isar calculation proof commands may be defined as
918 follows:\footnote{We suppress internal bookkeeping such as proper
919 handling of block-structure.}
921 \begin{matharray}{rcl}
922 \mbox{\isa{\isacommand{also}}}\isa{\isactrlsub {\isadigit{0}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ this} \\
923 \mbox{\isa{\isacommand{also}}}\isa{\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}} \\[0.5ex]
924 \mbox{\isa{\isacommand{finally}}} & \equiv & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
925 \mbox{\isa{\isacommand{moreover}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{calculation\ {\isacharequal}\ calculation\ this} \\
926 \mbox{\isa{\isacommand{ultimately}}} & \equiv & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\
930 ('also' | 'finally') ('(' thmrefs ')')?
932 'trans' (() | 'add' | 'del')
938 \item [\mbox{\isa{\isacommand{also}}}~\isa{{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}}]
939 maintains the auxiliary \mbox{\isa{calculation}} register as follows.
940 The first occurrence of \mbox{\isa{\isacommand{also}}} in some calculational
941 thread initializes \mbox{\isa{calculation}} by \mbox{\isa{this}}. Any
942 subsequent \mbox{\isa{\isacommand{also}}} on the same level of block-structure
943 updates \mbox{\isa{calculation}} by some transitivity rule applied to
944 \mbox{\isa{calculation}} and \mbox{\isa{this}} (in that order). Transitivity
945 rules are picked from the current context, unless alternative rules
946 are given as explicit arguments.
948 \item [\mbox{\isa{\isacommand{finally}}}~\isa{{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}}]
949 maintaining \mbox{\isa{calculation}} in the same way as \mbox{\isa{\isacommand{also}}}, and concludes the current calculational thread. The final
950 result is exhibited as fact for forward chaining towards the next
951 goal. Basically, \mbox{\isa{\isacommand{finally}}} just abbreviates \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\mbox{\isa{calculation}}. Typical idioms for
952 concluding calculational proofs are ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{show}}}~\isa{{\isacharquery}thesis}~\mbox{\isa{\isacommand{{\isachardot}}}}'' and ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{{\isachardot}}}}''.
954 \item [\mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}] are
955 analogous to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}}, but collect
956 results only, without applying rules.
958 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}] prints the list of
959 transitivity rules (for calculational commands \mbox{\isa{\isacommand{also}}} and
960 \mbox{\isa{\isacommand{finally}}}) and symmetry rules (for the \mbox{\isa{symmetric}} operation and single step elimination patters) of the
963 \item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
965 \item [\mbox{\isa{sym}}] declares symmetry rules, as well as
966 \mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
968 \item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
969 declared as \mbox{\isa{sym}} in the current context. For example,
970 ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y}'' produces a
971 swapped fact derived from that assumption.
973 In structured proof texts it is often more appropriate to use an
974 explicit single-step elimination proof, such as ``\mbox{\isa{\isacommand{assume}}}~\isa{x\ {\isacharequal}\ y}~\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}~\isa{y\ {\isacharequal}\ x}~\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''.
980 \isamarkupsection{Proof tools%
984 \isamarkupsubsection{Miscellaneous methods and attributes \label{sec:misc-meth-att}%
988 \begin{isamarkuptext}%
989 \begin{matharray}{rcl}
990 \indexdef{}{method}{unfold}\mbox{\isa{unfold}} & : & \isarmeth \\
991 \indexdef{}{method}{fold}\mbox{\isa{fold}} & : & \isarmeth \\
992 \indexdef{}{method}{insert}\mbox{\isa{insert}} & : & \isarmeth \\[0.5ex]
993 \indexdef{}{method}{erule}\mbox{\isa{erule}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
994 \indexdef{}{method}{drule}\mbox{\isa{drule}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
995 \indexdef{}{method}{frule}\mbox{\isa{frule}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
996 \indexdef{}{method}{succeed}\mbox{\isa{succeed}} & : & \isarmeth \\
997 \indexdef{}{method}{fail}\mbox{\isa{fail}} & : & \isarmeth \\
1001 ('fold' | 'unfold' | 'insert') thmrefs
1003 ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
1009 \item [\mbox{\isa{unfold}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n} and \mbox{\isa{fold}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] expand (or fold back) the
1010 given definitions throughout all goals; any chained facts provided
1011 are inserted into the goal and subject to rewriting as well.
1013 \item [\mbox{\isa{insert}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] inserts
1014 theorems as facts into all goals of the proof state. Note that
1015 current facts indicated for forward chaining are ignored.
1017 \item [\mbox{\isa{erule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}, \mbox{\isa{drule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}, and \mbox{\isa{frule}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] are similar to the basic \mbox{\isa{rule}}
1018 method (see \secref{sec:pure-meth-att}), but apply rules by
1019 elim-resolution, destruct-resolution, and forward-resolution,
1020 respectively \cite{isabelle-ref}. The optional natural number
1021 argument (default 0) specifies additional assumption steps to be
1024 Note that these methods are improper ones, mainly serving for
1025 experimentation and tactic script emulation. Different modes of
1026 basic rule application are usually expressed in Isar at the proof
1027 language level, rather than via implicit proof state manipulations.
1028 For example, a proper single-step elimination would be done using
1029 the plain \mbox{\isa{rule}} method, with forward chaining of current
1032 \item [\mbox{\isa{succeed}}] yields a single (unchanged) result; it is
1033 the identity of the ``\isa{{\isacharcomma}}'' method combinator (cf.\
1034 \secref{sec:syn-meth}).
1036 \item [\mbox{\isa{fail}}] yields an empty result sequence; it is the
1037 identity of the ``\isa{{\isacharbar}}'' method combinator (cf.\
1038 \secref{sec:syn-meth}).
1042 \begin{matharray}{rcl}
1043 \indexdef{}{attribute}{tagged}\mbox{\isa{tagged}} & : & \isaratt \\
1044 \indexdef{}{attribute}{untagged}\mbox{\isa{untagged}} & : & \isaratt \\[0.5ex]
1045 \indexdef{}{attribute}{THEN}\mbox{\isa{THEN}} & : & \isaratt \\
1046 \indexdef{}{attribute}{COMP}\mbox{\isa{COMP}} & : & \isaratt \\[0.5ex]
1047 \indexdef{}{attribute}{unfolded}\mbox{\isa{unfolded}} & : & \isaratt \\
1048 \indexdef{}{attribute}{folded}\mbox{\isa{folded}} & : & \isaratt \\[0.5ex]
1049 \indexdef{}{attribute}{rotated}\mbox{\isa{rotated}} & : & \isaratt \\
1050 \indexdef{Pure}{attribute}{elim-format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
1051 \indexdef{}{attribute}{standard}\mbox{\isa{standard}}\isa{\isactrlsup {\isacharasterisk}} & : & \isaratt \\
1052 \indexdef{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{\isactrlsup {\isacharasterisk}} & : & \isaratt \\
1060 ('THEN' | 'COMP') ('[' nat ']')? thmref
1062 ('unfolded' | 'folded') thmrefs
1069 \item [\mbox{\isa{tagged}}~\isa{name\ arg} and \mbox{\isa{untagged}}~\isa{name}] add and remove \emph{tags} of some theorem.
1070 Tags may be any list of string pairs that serve as formal comment.
1071 The first string is considered the tag name, the second its
1072 argument. Note that \mbox{\isa{untagged}} removes any tags of the
1075 \item [\mbox{\isa{THEN}}~\isa{a} and \mbox{\isa{COMP}}~\isa{a}]
1076 compose rules by resolution. \mbox{\isa{THEN}} resolves with the
1077 first premise of \isa{a} (an alternative position may be also
1078 specified); the \mbox{\isa{COMP}} version skips the automatic
1079 lifting process that is normally intended (cf.\ \verb|op RS| and
1080 \verb|op COMP| in \cite[\S5]{isabelle-ref}).
1082 \item [\mbox{\isa{unfolded}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n} and
1083 \mbox{\isa{folded}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] expand and fold
1084 back again the given definitions throughout a rule.
1086 \item [\mbox{\isa{rotated}}~\isa{n}] rotate the premises of a
1087 theorem by \isa{n} (default 1).
1089 \item [\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}] turns a destruction rule into
1090 elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
1092 Note that the Classical Reasoner (\secref{sec:classical}) provides
1093 its own version of this operation.
1095 \item [\mbox{\isa{standard}}] puts a theorem into the standard form
1096 of object-rules at the outermost theory level. Note that this
1097 operation violates the local proof context (including active
1100 \item [\mbox{\isa{no{\isacharunderscore}vars}}] replaces schematic variables by free
1101 ones; this is mainly for tuning output of pretty printed theorems.
1104 \end{isamarkuptext}%
1107 \isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
1111 \begin{isamarkuptext}%
1112 The following improper proof methods emulate traditional tactics.
1113 These admit direct access to the goal state, which is normally
1114 considered harmful! In particular, this may involve both numbered
1115 goal addressing (default 1), and dynamic instantiation within the
1116 scope of some subgoal.
1119 Dynamic instantiations refer to universally quantified parameters
1120 of a subgoal (the dynamic context) rather than fixed variables and
1121 term abbreviations of a (static) Isar context.
1124 Tactic emulation methods, unlike their ML counterparts, admit
1125 simultaneous instantiation from both dynamic and static contexts.
1126 If names occur in both contexts goal parameters hide locally fixed
1127 variables. Likewise, schematic variables refer to term
1128 abbreviations, if present in the static context. Otherwise the
1129 schematic variable is interpreted as a schematic variable and left
1130 to be solved by unification with certain parts of the subgoal.
1132 Note that the tactic emulation proof methods in Isabelle/Isar are
1133 consistently named \isa{foo{\isacharunderscore}tac}. Note also that variable names
1134 occurring on left hand sides of instantiations must be preceded by a
1135 question mark if they coincide with a keyword or contain dots. This
1136 is consistent with the attribute \mbox{\isa{where}} (see
1137 \secref{sec:pure-meth-att}).
1139 \begin{matharray}{rcl}
1140 \indexdef{}{method}{rule-tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1141 \indexdef{}{method}{erule-tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1142 \indexdef{}{method}{drule-tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1143 \indexdef{}{method}{frule-tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1144 \indexdef{}{method}{cut-tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1145 \indexdef{}{method}{thin-tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1146 \indexdef{}{method}{subgoal-tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1147 \indexdef{}{method}{rename-tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1148 \indexdef{}{method}{rotate-tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1149 \indexdef{}{method}{tactic}\mbox{\isa{tactic}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1153 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
1154 ( insts thmref | thmrefs )
1156 'subgoal\_tac' goalspec? (prop +)
1158 'rename\_tac' goalspec? (name +)
1160 'rotate\_tac' goalspec? int?
1165 insts: ((name '=' term) + 'and') 'in'
1171 \item [\mbox{\isa{rule{\isacharunderscore}tac}} etc.] do resolution of rules with explicit
1172 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}).
1174 Multiple rules may be only given if there is no instantiation; then
1175 \mbox{\isa{rule{\isacharunderscore}tac}} is the same as \verb|resolve_tac| in ML (see
1176 \cite[\S3]{isabelle-ref}).
1178 \item [\mbox{\isa{cut{\isacharunderscore}tac}}] inserts facts into the proof state as
1179 assumption of a subgoal, see also \verb|cut_facts_tac| in
1180 \cite[\S3]{isabelle-ref}. Note that the scope of schematic
1181 variables is spread over the main goal statement. Instantiations
1182 may be given as well, see also ML tactic \verb|cut_inst_tac| in
1183 \cite[\S3]{isabelle-ref}.
1185 \item [\mbox{\isa{thin{\isacharunderscore}tac}}~\isa{{\isasymphi}}] deletes the specified
1186 assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic
1187 variables. See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
1189 \item [\mbox{\isa{subgoal{\isacharunderscore}tac}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an
1190 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
1192 \item [\mbox{\isa{rename{\isacharunderscore}tac}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n}] renames
1193 parameters of a goal according to the list \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n}, which refers to the \emph{suffix} of variables.
1195 \item [\mbox{\isa{rotate{\isacharunderscore}tac}}~\isa{n}] rotates the assumptions of a
1196 goal by \isa{n} positions: from right to left if \isa{n} is
1197 positive, and from left to right if \isa{n} is negative; the
1198 default value is 1. See also \verb|rotate_tac| in
1199 \cite[\S3]{isabelle-ref}.
1201 \item [\mbox{\isa{tactic}}~\isa{text}] produces a proof method from
1202 any ML text of type \verb|tactic|. Apart from the usual ML
1203 environment and the current implicit theory context, the ML code may
1204 refer to the following locally bound values:
1207 {\footnotesize\begin{verbatim}
1208 val ctxt : Proof.context
1209 val facts : thm list
1210 val thm : string -> thm
1211 val thms : string -> thm list
1214 Here \verb|ctxt| refers to the current proof context, \verb|facts| indicates any current facts for forward-chaining, and \verb|thm|~/~\verb|thms| retrieve named facts (including global theorems)
1218 \end{isamarkuptext}%
1221 \isamarkupsubsection{The Simplifier \label{sec:simplifier}%
1225 \isamarkupsubsubsection{Simplification methods%
1229 \begin{isamarkuptext}%
1230 \begin{matharray}{rcl}
1231 \indexdef{}{method}{simp}\mbox{\isa{simp}} & : & \isarmeth \\
1232 \indexdef{}{method}{simp-all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
1235 \indexouternonterm{simpmod}
1237 ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
1240 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')'
1242 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
1243 'split' (() | 'add' | 'del')) ':' thmrefs
1249 \item [\mbox{\isa{simp}}] invokes the Simplifier, after declaring
1250 additional rules according to the arguments given. Note that the
1251 \railtterm{only} modifier first removes all other rewrite rules,
1252 congruences, and looper tactics (including splits), and then behaves
1253 like \railtterm{add}.
1255 \medskip The \railtterm{cong} modifiers add or delete Simplifier
1256 congruence rules (see also \cite{isabelle-ref}), the default is to
1259 \medskip The \railtterm{split} modifiers add or delete rules for the
1260 Splitter (see also \cite{isabelle-ref}), the default is to add.
1261 This works only if the Simplifier method has been properly setup to
1262 include the Splitter (all major object logics such HOL, HOLCF, FOL,
1263 ZF do this already).
1265 \item [\mbox{\isa{simp{\isacharunderscore}all}}] is similar to \mbox{\isa{simp}}, but acts on
1266 all goals (backwards from the last to the first one).
1270 By default the Simplifier methods take local assumptions fully into
1271 account, using equational assumptions in the subsequent
1272 normalization process, or simplifying assumptions themselves (cf.\
1273 \verb|asm_full_simp_tac| in \cite[\S10]{isabelle-ref}). In
1274 structured proofs this is usually quite well behaved in practice:
1275 just the local premises of the actual goal are involved, additional
1276 facts may be inserted via explicit forward-chaining (via \mbox{\isa{\isacommand{then}}}, \mbox{\isa{\isacommand{from}}}, \mbox{\isa{\isacommand{using}}} etc.). The full
1277 context of premises is only included if the ``\isa{{\isacharbang}}'' (bang)
1278 argument is given, which should be used with some care, though.
1280 Additional Simplifier options may be specified to tune the behavior
1281 further (mostly for unstructured scripts with many accidental local
1282 facts): ``\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}'' means assumptions are ignored
1283 completely (cf.\ \verb|simp_tac|), ``\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}'' means
1284 assumptions are used in the simplification of the conclusion but are
1285 not themselves simplified (cf.\ \verb|asm_simp_tac|), and ``\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}'' means assumptions are simplified but are not used
1286 in the simplification of each other or the conclusion (cf.\ \verb|full_simp_tac|). For compatibility reasons, there is also an option
1287 ``\isa{{\isacharparenleft}asm{\isacharunderscore}lr{\isacharparenright}}'', which means that an assumption is only used
1288 for simplifying assumptions which are to the right of it (cf.\ \verb|asm_lr_simp_tac|).
1290 Giving an option ``\isa{{\isacharparenleft}depth{\isacharunderscore}limit{\isacharcolon}\ n{\isacharparenright}}'' limits the number of
1291 recursive invocations of the simplifier during conditional
1294 \medskip The Splitter package is usually configured to work as part
1295 of the Simplifier. The effect of repeatedly applying \verb|split_tac| can be simulated by ``\isa{{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}}''. There is also a separate \isa{split}
1296 method available for single-step case splitting.%
1297 \end{isamarkuptext}%
1300 \isamarkupsubsubsection{Declaring rules%
1304 \begin{isamarkuptext}%
1305 \begin{matharray}{rcl}
1306 \indexdef{}{command}{print-simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
1307 \indexdef{}{attribute}{simp}\mbox{\isa{simp}} & : & \isaratt \\
1308 \indexdef{}{attribute}{cong}\mbox{\isa{cong}} & : & \isaratt \\
1309 \indexdef{}{attribute}{split}\mbox{\isa{split}} & : & \isaratt \\
1313 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
1319 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}] prints the collection of rules
1320 declared to the Simplifier, which is also known as ``simpset''
1321 internally \cite{isabelle-ref}.
1323 \item [\mbox{\isa{simp}}] declares simplification rules.
1325 \item [\mbox{\isa{cong}}] declares congruence rules.
1327 \item [\mbox{\isa{split}}] declares case split rules.
1330 \end{isamarkuptext}%
1333 \isamarkupsubsubsection{Simplification procedures%
1337 \begin{isamarkuptext}%
1338 \begin{matharray}{rcl}
1339 \indexdef{}{command}{simproc-setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
1340 simproc & : & \isaratt \\
1344 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
1347 'simproc' (('add' ':')? | 'del' ':') (name+)
1353 \item [\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}] defines a named simplification
1354 procedure that is invoked by the Simplifier whenever any of the
1355 given term patterns match the current redex. The implementation,
1356 which is provided as ML source text, needs to be of type \verb|morphism -> simpset -> cterm -> thm option|, where the \verb|cterm| represents the current redex \isa{r} and the result is
1357 supposed to be some proven rewrite rule \isa{r\ {\isasymequiv}\ r{\isacharprime}} (or a
1358 generalized version), or \verb|NONE| to indicate failure. The
1359 \verb|simpset| argument holds the full context of the current
1360 Simplifier invocation, including the actual Isar proof context. The
1361 \verb|morphism| informs about the difference of the original
1362 compilation context wrt.\ the one of the actual application later
1363 on. The optional \mbox{\isa{\isakeyword{identifier}}} specifies theorems that
1364 represent the logical content of the abstract theory of this
1367 Morphisms and identifiers are only relevant for simprocs that are
1368 defined within a local target context, e.g.\ in a locale.
1370 \item [\isa{simproc\ add{\isacharcolon}\ name} and \isa{simproc\ del{\isacharcolon}\ name}]
1371 add or delete named simprocs to the current Simplifier context. The
1372 default is to add a simproc. Note that \mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}}
1373 already adds the new simproc to the subsequent context.
1376 \end{isamarkuptext}%
1379 \isamarkupsubsubsection{Forward simplification%
1383 \begin{isamarkuptext}%
1384 \begin{matharray}{rcl}
1385 \indexdef{}{attribute}{simplified}\mbox{\isa{simplified}} & : & \isaratt \\
1389 'simplified' opt? thmrefs?
1392 opt: '(' (noasm | noasmsimp | noasmuse) ')'
1398 \item [\mbox{\isa{simplified}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}]
1399 causes a theorem to be simplified, either by exactly the specified
1400 rules \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n}, or the implicit Simplifier
1401 context if no arguments are given. The result is fully simplified
1402 by default, including assumptions and conclusion; the options \isa{no{\isacharunderscore}asm} etc.\ tune the Simplifier in the same way as the for the
1405 Note that forward simplification restricts the simplifier to its
1406 most basic operation of term rewriting; solver and looper tactics
1407 \cite{isabelle-ref} are \emph{not} involved here. The \isa{simplified} attribute should be only rarely required under normal
1411 \end{isamarkuptext}%
1414 \isamarkupsubsubsection{Low-level equational reasoning%
1418 \begin{isamarkuptext}%
1419 \begin{matharray}{rcl}
1420 \indexdef{}{method}{subst}\mbox{\isa{subst}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1421 \indexdef{}{method}{hypsubst}\mbox{\isa{hypsubst}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1422 \indexdef{}{method}{split}\mbox{\isa{split}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarmeth \\
1426 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
1428 'split' ('(' 'asm' ')')? thmrefs
1432 These methods provide low-level facilities for equational reasoning
1433 that are intended for specialized applications only. Normally,
1434 single step calculations would be performed in a structured text
1435 (see also \secref{sec:calculation}), while the Simplifier methods
1436 provide the canonical way for automated normalization (see
1437 \secref{sec:simplifier}).
1441 \item [\mbox{\isa{subst}}~\isa{eq}] performs a single substitution
1442 step using rule \isa{eq}, which may be either a meta or object
1445 \item [\mbox{\isa{subst}}~\isa{{\isacharparenleft}asm{\isacharparenright}\ eq}] substitutes in an
1448 \item [\mbox{\isa{subst}}~\isa{{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq}] performs several
1449 substitutions in the conclusion. The numbers \isa{i} to \isa{j}
1450 indicate the positions to substitute at. Positions are ordered from
1451 the top of the term tree moving down from left to right. For
1452 example, in \isa{{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}} there are three positions
1453 where commutativity of \isa{{\isacharplus}} is applicable: 1 refers to the
1454 whole term, 2 to \isa{a\ {\isacharplus}\ b} and 3 to \isa{c\ {\isacharplus}\ d}.
1456 If the positions in the list \isa{{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}} are non-overlapping
1457 (e.g.\ \isa{{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}} in \isa{{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}}) you may
1458 assume all substitutions are performed simultaneously. Otherwise
1459 the behaviour of \isa{subst} is not specified.
1461 \item [\mbox{\isa{subst}}~\isa{{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq}] performs the
1462 substitutions in the assumptions. Positions \isa{{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}}
1463 refer to assumption 1, positions \isa{i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}}
1464 to assumption 2, and so on.
1466 \item [\mbox{\isa{hypsubst}}] performs substitution using some
1467 assumption; this only works for equations of the form \isa{x\ {\isacharequal}\ t} where \isa{x} is a free or bound variable.
1469 \item [\mbox{\isa{split}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] performs
1470 single-step case splitting using the given rules. By default,
1471 splitting is performed in the conclusion of a goal; the \isa{{\isacharparenleft}asm{\isacharparenright}} option indicates to operate on assumptions instead.
1473 Note that the \mbox{\isa{simp}} method already involves repeated
1474 application of split rules as declared in the current context.
1477 \end{isamarkuptext}%
1480 \isamarkupsubsection{The Classical Reasoner \label{sec:classical}%
1484 \isamarkupsubsubsection{Basic methods%
1488 \begin{isamarkuptext}%
1489 \begin{matharray}{rcl}
1490 \indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\
1491 \indexdef{}{method}{contradiction}\mbox{\isa{contradiction}} & : & \isarmeth \\
1492 \indexdef{}{method}{intro}\mbox{\isa{intro}} & : & \isarmeth \\
1493 \indexdef{}{method}{elim}\mbox{\isa{elim}} & : & \isarmeth \\
1497 ('rule' | 'intro' | 'elim') thmrefs?
1503 \item [\mbox{\isa{rule}}] as offered by the Classical Reasoner is a
1504 refinement over the primitive one (see \secref{sec:pure-meth-att}).
1505 Both versions essentially work the same, but the classical version
1506 observes the classical rule context in addition to that of
1509 Common object logics (HOL, ZF, etc.) declare a rich collection of
1510 classical rules (even if these would qualify as intuitionistic
1511 ones), but only few declarations to the rule context of
1512 Isabelle/Pure (\secref{sec:pure-meth-att}).
1514 \item [\mbox{\isa{contradiction}}] solves some goal by contradiction,
1515 deriving any result from both \isa{{\isasymnot}\ A} and \isa{A}. Chained
1516 facts, which are guaranteed to participate, may appear in either
1519 \item [\mbox{\isa{intro}} and \mbox{\isa{elim}}] repeatedly refine
1520 some goal by intro- or elim-resolution, after having inserted any
1521 chained facts. Exactly the rules given as arguments are taken into
1522 account; this allows fine-tuned decomposition of a proof problem, in
1523 contrast to common automated tools.
1526 \end{isamarkuptext}%
1529 \isamarkupsubsubsection{Automated methods%
1533 \begin{isamarkuptext}%
1534 \begin{matharray}{rcl}
1535 \indexdef{}{method}{blast}\mbox{\isa{blast}} & : & \isarmeth \\
1536 \indexdef{}{method}{fast}\mbox{\isa{fast}} & : & \isarmeth \\
1537 \indexdef{}{method}{slow}\mbox{\isa{slow}} & : & \isarmeth \\
1538 \indexdef{}{method}{best}\mbox{\isa{best}} & : & \isarmeth \\
1539 \indexdef{}{method}{safe}\mbox{\isa{safe}} & : & \isarmeth \\
1540 \indexdef{}{method}{clarify}\mbox{\isa{clarify}} & : & \isarmeth \\
1543 \indexouternonterm{clamod}
1545 'blast' ('!' ?) nat? (clamod *)
1547 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
1550 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
1556 \item [\mbox{\isa{blast}}] refers to the classical tableau prover (see
1557 \verb|blast_tac| in \cite[\S11]{isabelle-ref}). The optional
1558 argument specifies a user-supplied search bound (default 20).
1560 \item [\mbox{\isa{fast}}, \mbox{\isa{slow}}, \mbox{\isa{best}}, \mbox{\isa{safe}}, and \mbox{\isa{clarify}}] refer to the generic classical
1561 reasoner. See \verb|fast_tac|, \verb|slow_tac|, \verb|best_tac|, \verb|safe_tac|, and \verb|clarify_tac| in \cite[\S11]{isabelle-ref} for
1566 Any of the above methods support additional modifiers of the context
1567 of classical rules. Their semantics is analogous to the attributes
1568 given before. Facts provided by forward chaining are inserted into
1569 the goal before commencing proof search. The ``\isa{{\isacharbang}}''~argument causes the full context of assumptions to be
1571 \end{isamarkuptext}%
1574 \isamarkupsubsubsection{Combined automated methods \label{sec:clasimp}%
1578 \begin{isamarkuptext}%
1579 \begin{matharray}{rcl}
1580 \indexdef{}{method}{auto}\mbox{\isa{auto}} & : & \isarmeth \\
1581 \indexdef{}{method}{force}\mbox{\isa{force}} & : & \isarmeth \\
1582 \indexdef{}{method}{clarsimp}\mbox{\isa{clarsimp}} & : & \isarmeth \\
1583 \indexdef{}{method}{fastsimp}\mbox{\isa{fastsimp}} & : & \isarmeth \\
1584 \indexdef{}{method}{slowsimp}\mbox{\isa{slowsimp}} & : & \isarmeth \\
1585 \indexdef{}{method}{bestsimp}\mbox{\isa{bestsimp}} & : & \isarmeth \\
1588 \indexouternonterm{clasimpmod}
1590 'auto' '!'? (nat nat)? (clasimpmod *)
1592 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
1595 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
1596 ('cong' | 'split') (() | 'add' | 'del') |
1597 'iff' (((() | 'add') '?'?) | 'del') |
1598 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
1603 \item [\mbox{\isa{auto}}, \mbox{\isa{force}}, \mbox{\isa{clarsimp}}, \mbox{\isa{fastsimp}}, \mbox{\isa{slowsimp}}, and \mbox{\isa{bestsimp}}] provide
1604 access to Isabelle's combined simplification and classical reasoning
1605 tactics. These correspond to \verb|auto_tac|, \verb|force_tac|, \verb|clarsimp_tac|, and Classical Reasoner tactics with the Simplifier
1606 added as wrapper, see \cite[\S11]{isabelle-ref} for more
1607 information. The modifier arguments correspond to those given in
1608 \secref{sec:simplifier} and \secref{sec:classical}. Just note that
1609 the ones related to the Simplifier are prefixed by \railtterm{simp}
1612 Facts provided by forward chaining are inserted into the goal before
1613 doing the search. The ``\isa{{\isacharbang}}'' argument causes the full
1614 context of assumptions to be included as well.
1617 \end{isamarkuptext}%
1620 \isamarkupsubsubsection{Declaring rules%
1624 \begin{isamarkuptext}%
1625 \begin{matharray}{rcl}
1626 \indexdef{}{command}{print-claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
1627 \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
1628 \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
1629 \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
1630 \indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\
1631 \indexdef{}{attribute}{iff}\mbox{\isa{iff}} & : & \isaratt \\
1635 ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
1639 'iff' (((() | 'add') '?'?) | 'del')
1645 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}] prints the collection of rules
1646 declared to the Classical Reasoner, which is also known as
1647 ``claset'' internally \cite{isabelle-ref}.
1649 \item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}]
1650 declare introduction, elimination, and destruction rules,
1651 respectively. By default, rules are considered as \emph{unsafe}
1652 (i.e.\ not applied blindly without backtracking), while ``\isa{{\isacharbang}}'' classifies as \emph{safe}. Rule declarations marked by
1653 ``\isa{{\isacharquery}}'' coincide with those of Isabelle/Pure, cf.\
1654 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
1655 of the \mbox{\isa{rule}} method). The optional natural number
1656 specifies an explicit weight argument, which is ignored by automated
1657 tools, but determines the search order of single rule steps.
1659 \item [\mbox{\isa{rule}}~\isa{del}] deletes introduction,
1660 elimination, or destruction rules from the context.
1662 \item [\mbox{\isa{iff}}] declares logical equivalences to the
1663 Simplifier and the Classical reasoner at the same time.
1664 Non-conditional rules result in a ``safe'' introduction and
1665 elimination pair; conditional ones are considered ``unsafe''. Rules
1666 with negative conclusion are automatically inverted (using \isa{{\isasymnot}} elimination internally).
1668 The ``\isa{{\isacharquery}}'' version of \mbox{\isa{iff}} declares rules to
1669 the Isabelle/Pure context only, and omits the Simplifier
1673 \end{isamarkuptext}%
1676 \isamarkupsubsubsection{Classical operations%
1680 \begin{isamarkuptext}%
1681 \begin{matharray}{rcl}
1682 \indexdef{}{attribute}{swapped}\mbox{\isa{swapped}} & : & \isaratt \\
1687 \item [\mbox{\isa{swapped}}] turns an introduction rule into an
1688 elimination, by resolving with the classical swap principle \isa{{\isacharparenleft}{\isasymnot}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ B{\isacharparenright}}.
1691 \end{isamarkuptext}%
1694 \isamarkupsubsection{Proof by cases and induction \label{sec:cases-induct}%
1698 \isamarkupsubsubsection{Rule contexts%
1702 \begin{isamarkuptext}%
1703 \begin{matharray}{rcl}
1704 \indexdef{}{command}{case}\mbox{\isa{\isacommand{case}}} & : & \isartrans{proof(state)}{proof(state)} \\
1705 \indexdef{}{command}{print-cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{proof} \\
1706 \indexdef{}{attribute}{case-names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
1707 \indexdef{}{attribute}{case-conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
1708 \indexdef{}{attribute}{params}\mbox{\isa{params}} & : & \isaratt \\
1709 \indexdef{}{attribute}{consumes}\mbox{\isa{consumes}} & : & \isaratt \\
1712 The puristic way to build up Isar proof contexts is by explicit
1713 language elements like \mbox{\isa{\isacommand{fix}}}, \mbox{\isa{\isacommand{assume}}},
1714 \mbox{\isa{\isacommand{let}}} (see \secref{sec:proof-context}). This is adequate
1715 for plain natural deduction, but easily becomes unwieldy in concrete
1716 verification tasks, which typically involve big induction rules with
1719 The \mbox{\isa{\isacommand{case}}} command provides a shorthand to refer to a
1720 local context symbolically: certain proof methods provide an
1721 environment of named ``cases'' of the form \isa{c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n}; the effect of
1722 ``\mbox{\isa{\isacommand{case}}}\isa{c}'' is then equivalent to ``\mbox{\isa{\isacommand{fix}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}~\mbox{\isa{\isacommand{assume}}}~\isa{c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}''. Term bindings may be
1723 covered as well, notably \mbox{\isa{{\isacharquery}case}} for the main conclusion.
1725 By default, the ``terminology'' \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m} of
1726 a case value is marked as hidden, i.e.\ there is no way to refer to
1727 such parameters in the subsequent proof text. After all, original
1728 rule parameters stem from somewhere outside of the current proof
1729 text. By using the explicit form ``\mbox{\isa{\isacommand{case}}}~\isa{{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}}'' instead, the proof author is able to
1730 chose local names that fit nicely into the current context.
1732 \medskip It is important to note that proper use of \mbox{\isa{\isacommand{case}}} does not provide means to peek at the current goal state,
1733 which is not directly observable in Isar! Nonetheless, goal
1734 refinement commands do provide named cases \isa{goal\isactrlsub i}
1735 for each subgoal \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n} of the resulting goal state.
1736 Using this extra feature requires great care, because some bits of
1737 the internal tactical machinery intrude the proof text. In
1738 particular, parameter names stemming from the left-over of automated
1739 reasoning tools are usually quite unpredictable.
1741 Under normal circumstances, the text of cases emerge from standard
1742 elimination or induction rules, which in turn are derived from
1743 previous theory specifications in a canonical way (say from
1744 \mbox{\isa{\isacommand{inductive}}} definitions).
1746 \medskip Proper cases are only available if both the proof method
1747 and the rules involved support this. By using appropriate
1748 attributes, case names, conclusions, and parameters may be also
1749 declared by hand. Thus variant versions of rules that have been
1750 derived manually become ready to use in advanced case analysis
1754 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1756 caseref: nameref attributes?
1759 'case\_names' (name +)
1761 'case\_conclusion' name (name *)
1763 'params' ((name *) + 'and')
1771 \item [\mbox{\isa{\isacommand{case}}}~\isa{{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}}]
1772 invokes a named local context \isa{c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m}, as provided by an appropriate
1773 proof method (such as \indexref{}{method}{cases}\mbox{\isa{cases}} and \indexref{}{method}{induct}\mbox{\isa{induct}}).
1774 The command ``\mbox{\isa{\isacommand{case}}}~\isa{{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}~\mbox{\isa{\isacommand{assume}}}~\isa{c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n}''.
1776 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}] prints all local contexts of the
1777 current state, using Isar proof language notation.
1779 \item [\mbox{\isa{case{\isacharunderscore}names}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k}]
1780 declares names for the local contexts of premises of a theorem;
1781 \isa{c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k} refers to the \emph{suffix} of the
1784 \item [\mbox{\isa{case{\isacharunderscore}conclusion}}~\isa{c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k}] declares names for the conclusions of a named premise
1785 \isa{c}; here \isa{d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k} refers to the
1786 prefix of arguments of a logical formula built by nesting a binary
1787 connective (e.g.\ \isa{{\isasymor}}).
1789 Note that proof methods such as \mbox{\isa{induct}} and \mbox{\isa{coinduct}} already provide a default name for the conclusion as a
1790 whole. The need to name subformulas only arises with cases that
1791 split into several sub-cases, as in common co-induction rules.
1793 \item [\mbox{\isa{params}}~\isa{p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n}] renames the innermost parameters of
1794 premises \isa{{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n} of some theorem. An empty list of names
1795 may be given to skip positions, leaving the present parameters
1798 Note that the default usage of case rules does \emph{not} directly
1799 expose parameters to the proof context.
1801 \item [\mbox{\isa{consumes}}~\isa{n}] declares the number of
1802 ``major premises'' of a rule, i.e.\ the number of facts to be
1803 consumed when it is applied by an appropriate proof method. The
1804 default value of \mbox{\isa{consumes}} is \isa{n\ {\isacharequal}\ {\isadigit{1}}}, which is
1805 appropriate for the usual kind of cases and induction rules for
1806 inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
1807 \mbox{\isa{consumes}} declaration given are treated as if
1808 \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} had been specified.
1810 Note that explicit \mbox{\isa{consumes}} declarations are only
1811 rarely needed; this is already taken care of automatically by the
1812 higher-level \mbox{\isa{cases}}, \mbox{\isa{induct}}, and
1813 \mbox{\isa{coinduct}} declarations.
1816 \end{isamarkuptext}%
1819 \isamarkupsubsubsection{Proof methods%
1823 \begin{isamarkuptext}%
1824 \begin{matharray}{rcl}
1825 \indexdef{}{method}{cases}\mbox{\isa{cases}} & : & \isarmeth \\
1826 \indexdef{}{method}{induct}\mbox{\isa{induct}} & : & \isarmeth \\
1827 \indexdef{}{method}{coinduct}\mbox{\isa{coinduct}} & : & \isarmeth \\
1830 The \mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}
1831 methods provide a uniform interface to common proof techniques over
1832 datatypes, inductive predicates (or sets), recursive functions etc.
1833 The corresponding rules may be specified and instantiated in a
1834 casual manner. Furthermore, these methods provide named local
1835 contexts that may be invoked via the \mbox{\isa{\isacommand{case}}} proof command
1836 within the subsequent proof text. This accommodates compact proof
1837 texts even when reasoning about large specifications.
1839 The \mbox{\isa{induct}} method also provides some additional
1840 infrastructure in order to be applicable to structure statements
1841 (either using explicit meta-level connectives, or including facts
1842 and parameters separately). This avoids cumbersome encoding of
1843 ``strengthened'' inductive statements within the object-logic.
1846 'cases' (insts * 'and') rule?
1848 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
1850 'coinduct' insts taking rule?
1853 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
1855 definst: name ('==' | equiv) term | inst
1857 definsts: ( definst *)
1859 arbitrary: 'arbitrary' ':' ((term *) 'and' +)
1861 taking: 'taking' ':' insts
1867 \item [\mbox{\isa{cases}}~\isa{insts\ R}] applies method \mbox{\isa{rule}} with an appropriate case distinction theorem, instantiated to
1868 the subjects \isa{insts}. Symbolic case names are bound according
1869 to the rule's local contexts.
1871 The rule is determined as follows, according to the facts and
1872 arguments passed to the \mbox{\isa{cases}} method:
1875 \begin{tabular}{llll}
1876 facts & & arguments & rule \\\hline
1877 & \mbox{\isa{cases}} & & classical case split \\
1878 & \mbox{\isa{cases}} & \isa{t} & datatype exhaustion (type of \isa{t}) \\
1879 \isa{{\isasymturnstile}\ A\ t} & \mbox{\isa{cases}} & \isa{{\isasymdots}} & inductive predicate/set elimination (of \isa{A}) \\
1880 \isa{{\isasymdots}} & \mbox{\isa{cases}} & \isa{{\isasymdots}\ rule{\isacharcolon}\ R} & explicit rule \isa{R} \\
1884 Several instantiations may be given, referring to the \emph{suffix}
1885 of premises of the case rule; within each premise, the \emph{prefix}
1886 of variables is instantiated. In most situations, only a single
1887 term needs to be specified; this refers to the first variable of the
1888 last premise (it is usually the same for all cases).
1890 \item [\mbox{\isa{induct}}~\isa{insts\ R}] is analogous to the
1891 \mbox{\isa{cases}} method, but refers to induction rules, which are
1892 determined as follows:
1895 \begin{tabular}{llll}
1896 facts & & arguments & rule \\\hline
1897 & \mbox{\isa{induct}} & \isa{P\ x\ {\isasymdots}} & datatype induction (type of \isa{x}) \\
1898 \isa{{\isasymturnstile}\ A\ x} & \mbox{\isa{induct}} & \isa{{\isasymdots}} & predicate/set induction (of \isa{A}) \\
1899 \isa{{\isasymdots}} & \mbox{\isa{induct}} & \isa{{\isasymdots}\ rule{\isacharcolon}\ R} & explicit rule \isa{R} \\
1903 Several instantiations may be given, each referring to some part of
1904 a mutual inductive definition or datatype --- only related partial
1905 induction rules may be used together, though. Any of the lists of
1906 terms \isa{P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}} refers to the \emph{suffix} of variables
1907 present in the induction rule. This enables the writer to specify
1908 only induction variables, or both predicates and variables, for
1911 Instantiations may be definitional: equations \isa{x\ {\isasymequiv}\ t}
1912 introduce local definitions, which are inserted into the claim and
1913 discharged after applying the induction rule. Equalities reappear
1914 in the inductive cases, but have been transformed according to the
1915 induction principle being involved here. In order to achieve
1916 practically useful induction hypotheses, some variables occurring in
1917 \isa{t} need to be fixed (see below).
1919 The optional ``\isa{arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}''
1920 specification generalizes variables \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m} of the original goal before applying induction. Thus
1921 induction hypotheses may become sufficiently general to get the
1922 proof through. Together with definitional instantiations, one may
1923 effectively perform induction over expressions of a certain
1926 The optional ``\isa{taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}''
1927 specification provides additional instantiations of a prefix of
1928 pending variables in the rule. Such schematic induction rules
1929 rarely occur in practice, though.
1931 \item [\mbox{\isa{coinduct}}~\isa{inst\ R}] is analogous to the
1932 \mbox{\isa{induct}} method, but refers to coinduction rules, which are
1933 determined as follows:
1936 \begin{tabular}{llll}
1937 goal & & arguments & rule \\\hline
1938 & \mbox{\isa{coinduct}} & \isa{x\ {\isasymdots}} & type coinduction (type of \isa{x}) \\
1939 \isa{A\ x} & \mbox{\isa{coinduct}} & \isa{{\isasymdots}} & predicate/set coinduction (of \isa{A}) \\
1940 \isa{{\isasymdots}} & \mbox{\isa{coinduct}} & \isa{{\isasymdots}\ R} & explicit rule \isa{R} \\
1943 Coinduction is the dual of induction. Induction essentially
1944 eliminates \isa{A\ x} towards a generic result \isa{P\ x},
1945 while coinduction introduces \isa{A\ x} starting with \isa{B\ x}, for a suitable ``bisimulation'' \isa{B}. The cases of a
1946 coinduct rule are typically named after the predicates or sets being
1947 covered, while the conclusions consist of several alternatives being
1948 named after the individual destructor patterns.
1950 The given instantiation refers to the \emph{suffix} of variables
1951 occurring in the rule's major premise, or conclusion if unavailable.
1952 An additional ``\isa{taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}''
1953 specification may be required in order to specify the bisimulation
1954 to be used in the coinduction step.
1958 Above methods produce named local contexts, as determined by the
1959 instantiated rule as given in the text. Beyond that, the \mbox{\isa{induct}} and \mbox{\isa{coinduct}} methods guess further instantiations
1960 from the goal specification itself. Any persisting unresolved
1961 schematic variables of the resulting rule will render the the
1962 corresponding case invalid. The term binding \mbox{\isa{{\isacharquery}case}} for
1963 the conclusion will be provided with each case, provided that term
1966 The \mbox{\isa{\isacommand{print{\isacharunderscore}cases}}} command prints all named cases present
1967 in the current proof state.
1969 \medskip Despite the additional infrastructure, both \mbox{\isa{cases}}
1970 and \mbox{\isa{coinduct}} merely apply a certain rule, after
1971 instantiation, while conforming due to the usual way of monotonic
1972 natural deduction: the context of a structured statement \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}}
1973 reappears unchanged after the case split.
1975 The \mbox{\isa{induct}} method is fundamentally different in this
1976 respect: the meta-level structure is passed through the
1977 ``recursive'' course involved in the induction. Thus the original
1978 statement is basically replaced by separate copies, corresponding to
1979 the induction hypotheses and conclusion; the original goal context
1980 is no longer available. Thus local assumptions, fixed parameters
1981 and definitions effectively participate in the inductive rephrasing
1982 of the original statement.
1984 In induction proofs, local assumptions introduced by cases are split
1985 into two different kinds: \isa{hyps} stemming from the rule and
1986 \isa{prems} from the goal statement. This is reflected in the
1987 extracted cases accordingly, so invoking ``\mbox{\isa{\isacommand{case}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
1988 as well as fact \isa{c} to hold the all-inclusive list.
1990 \medskip Facts presented to either method are consumed according to
1991 the number of ``major premises'' of the rule involved, which is
1992 usually 0 for plain cases and induction rules of datatypes etc.\ and
1993 1 for rules of inductive predicates or sets and the like. The
1994 remaining facts are inserted into the goal verbatim before the
1995 actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
1997 \end{isamarkuptext}%
2000 \isamarkupsubsubsection{Declaring rules%
2004 \begin{isamarkuptext}%
2005 \begin{matharray}{rcl}
2006 \indexdef{}{command}{print-induct-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{\isactrlsup {\isacharasterisk}} & : & \isarkeep{theory~|~proof} \\
2007 \indexdef{}{attribute}{cases}\mbox{\isa{cases}} & : & \isaratt \\
2008 \indexdef{}{attribute}{induct}\mbox{\isa{induct}} & : & \isaratt \\
2009 \indexdef{}{attribute}{coinduct}\mbox{\isa{coinduct}} & : & \isaratt \\
2020 spec: ('type' | 'pred' | 'set') ':' nameref
2026 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}] prints cases and induct
2027 rules for predicates (or sets) and types of the current context.
2029 \item [\mbox{\isa{cases}}, \mbox{\isa{induct}}, and \mbox{\isa{coinduct}}] (as attributes) augment the corresponding context of
2030 rules for reasoning about (co)inductive predicates (or sets) and
2031 types, using the corresponding methods of the same name. Certain
2032 definitional packages of object-logics usually declare emerging
2033 cases and induction rules as expected, so users rarely need to
2036 Manual rule declarations usually refer to the \mbox{\isa{case{\isacharunderscore}names}} and \mbox{\isa{params}} attributes to adjust names of
2037 cases and parameters of a rule; the \mbox{\isa{consumes}}
2038 declaration is taken care of automatically: \mbox{\isa{consumes}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \mbox{\isa{consumes}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
2041 \end{isamarkuptext}%
2049 \isacommand{end}\isamarkupfalse%
2059 %%% Local Variables:
2061 %%% TeX-master: "root"