7 chapter {* Theory specifications *}
9 section {* Defining theories \label{sec:begin-thy} *}
12 \begin{matharray}{rcl}
13 @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
14 @{command_def (global) "end"} & : & \isartrans{theory}{toplevel} \\
17 Isabelle/Isar theories are defined via theory files, which may
18 contain both specifications and proofs; occasionally definitional
19 mechanisms also require some explicit proof. The theory body may be
20 sub-structured by means of \emph{local theory targets}, such as
21 @{command "locale"} and @{command "class"}.
23 The first proper command of a theory is @{command "theory"}, which
24 indicates imports of previous theories and optional dependencies on
25 other source files (usually in ML). Just preceding the initial
26 @{command "theory"} command there may be an optional @{command
27 "header"} declaration, which is only relevant to document
28 preparation: see also the other section markup commands in
31 A theory is concluded by a final @{command (global) "end"} command,
32 one that does not belong to a local theory target. No further
33 commands may follow such a global @{command (global) "end"},
34 although some user-interfaces might pretend that trailing input is
38 'theory' name 'imports' (name +) uses? 'begin'
41 uses: 'uses' ((name | parname) +);
46 \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
47 B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
48 merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
50 Due to the possibility to import more than one ancestor, the
51 resulting theory structure of an Isabelle session forms a directed
52 acyclic graph (DAG). Isabelle's theory loader ensures that the
53 sources contributing to the development graph are always up-to-date:
54 changed files are automatically reloaded whenever a theory header
55 specification is processed.
57 The optional @{keyword_def "uses"} specification declares additional
58 dependencies on extra files (usually ML sources). Files will be
59 loaded immediately (as ML), unless the name is parenthesized. The
60 latter case records a dependency that needs to be resolved later in
61 the text, usually via explicit @{command_ref "use"} for ML files;
62 other file formats require specific load commands defined by the
63 corresponding tools or packages.
65 \item [@{command (global) "end"}] concludes the current theory
66 definition. Note that local theory targets involve a local
67 @{command (local) "end"}, which is clear from the nesting.
73 section {* Local theory targets \label{sec:target} *}
76 A local theory target is a context managed separately within the
77 enclosing theory. Contexts may introduce parameters (fixed
78 variables) and assumptions (hypotheses). Definitions and theorems
79 depending on the context may be added incrementally later on. Named
80 contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
81 (cf.\ \secref{sec:class}); the name ``@{text "-"}'' signifies the
82 global theory context.
84 \begin{matharray}{rcll}
85 @{command_def "context"} & : & \isartrans{theory}{local{\dsh}theory} \\
86 @{command_def (local) "end"} & : & \isartrans{local{\dsh}theory}{theory} \\
89 \indexouternonterm{target}
91 'context' name 'begin'
94 target: '(' 'in' name ')'
100 \item [@{command "context"}~@{text "c \<BEGIN>"}] recommences an
101 existing locale or class context @{text c}. Note that locale and
102 class definitions allow to include the @{keyword "begin"} keyword as
103 well, in order to continue the local theory immediately after the
104 initial specification.
106 \item [@{command (local) "end"}] concludes the current local theory
107 and continues the enclosing global theory. Note that a global
108 @{command (global) "end"} has a different meaning: it concludes the
109 theory itself (\secref{sec:begin-thy}).
111 \item [@{text "(\<IN> c)"}] given after any local theory command
112 specifies an immediate target, e.g.\ ``@{command
113 "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
114 "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
115 global theory context; the current target context will be suspended
116 for this command only. Note that ``@{text "(\<IN> -)"}'' will
117 always produce a global result independently of the current target
122 The exact meaning of results produced within a local theory context
123 depends on the underlying target infrastructure (locale, type class
124 etc.). The general idea is as follows, considering a context named
125 @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
127 Definitions are exported by introducing a global version with
128 additional arguments; a syntactic abbreviation links the long form
129 with the abstract version of the target context. For example,
130 @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
131 level (for arbitrary @{text "?x"}), together with a local
132 abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
133 fixed parameter @{text x}).
135 Theorems are exported by discharging the assumptions and
136 generalizing the parameters of the context. For example, @{text "a:
137 B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
142 section {* Basic specification elements *}
145 \begin{matharray}{rcll}
146 @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\
147 @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\
148 @{attribute_def "defn"} & : & \isaratt \\
149 @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\
150 @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
151 @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\
152 @{command_def "no_notation"} & : & \isarkeep{local{\dsh}theory} \\
155 These specification mechanisms provide a slightly more abstract view
156 than the underlying primitives of @{command "consts"}, @{command
157 "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
158 \secref{sec:axms-thms}). In particular, type-inference is commonly
159 available, and result names need not be given.
162 'axiomatization' target? fixes? ('where' specs)?
164 'definition' target? (decl 'where')? thmdecl? prop
166 'abbreviation' target? mode? (decl 'where')? prop
168 ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
171 fixes: ((name ('::' type)? mixfix? | vars) + 'and')
173 specs: (thmdecl? props + 'and')
175 decl: name ('::' type)? mixfix?
181 \item [@{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m
182 \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}] introduces several constants
183 simultaneously and states axiomatic properties for these. The
184 constants are marked as being specified once and for all, which
185 prevents additional specifications being issued later on.
187 Note that axiomatic specifications are only appropriate when
188 declaring a new logical system; axiomatic specifications are
189 restricted to global theory contexts. Normal applications should
190 only use definitional mechanisms!
192 \item [@{command "definition"}~@{text "c \<WHERE> eq"}] produces an
193 internal definition @{text "c \<equiv> t"} according to the specification
194 given as @{text eq}, which is then turned into a proven fact. The
195 given proposition may deviate from internal meta-level equality
196 according to the rewrite rules declared as @{attribute defn} by the
197 object-logic. This usually covers object-level equality @{text "x =
198 y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
199 change the @{attribute defn} setup.
201 Definitions may be presented with explicit arguments on the LHS, as
202 well as additional conditions, e.g.\ @{text "f x y = t"} instead of
203 @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
204 unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
206 \item [@{command "abbreviation"}~@{text "c \<WHERE> eq"}] introduces
207 a syntactic constant which is associated with a certain term
208 according to the meta-level equality @{text eq}.
210 Abbreviations participate in the usual type-inference process, but
211 are expanded before the logic ever sees them. Pretty printing of
212 terms involves higher-order rewriting with rules stemming from
213 reverted abbreviations. This needs some care to avoid overlapping
214 or looping syntactic replacements!
216 The optional @{text mode} specification restricts output to a
217 particular print mode; using ``@{text input}'' here achieves the
218 effect of one-way abbreviations. The mode may also include an
219 ``@{keyword "output"}'' qualifier that affects the concrete syntax
220 declared for abbreviations, cf.\ @{command "syntax"} in
221 \secref{sec:syn-trans}.
223 \item [@{command "print_abbrevs"}] prints all constant abbreviations
224 of the current context.
226 \item [@{command "notation"}~@{text "c (mx)"}] associates mixfix
227 syntax with an existing constant or fixed variable. This is a
228 robust interface to the underlying @{command "syntax"} primitive
229 (\secref{sec:syn-trans}). Type declaration and internal syntactic
230 representation of the given entity is retrieved from the context.
232 \item [@{command "no_notation"}] is similar to @{command
233 "notation"}, but removes the specified syntax annotation from the
238 All of these specifications support local theory targets (cf.\
239 \secref{sec:target}).
243 section {* Generic declarations *}
246 Arbitrary operations on the background context may be wrapped-up as
247 generic declaration elements. Since the underlying concept of local
248 theories may be subject to later re-interpretation, there is an
249 additional dependency on a morphism that tells the difference of the
250 original declaration context wrt.\ the application context
251 encountered later on. A fact declaration is an important special
252 case: it consists of a theorem which is applied to the context by
253 means of an attribute.
255 \begin{matharray}{rcl}
256 @{command_def "declaration"} & : & \isarkeep{local{\dsh}theory} \\
257 @{command_def "declare"} & : & \isarkeep{local{\dsh}theory} \\
261 'declaration' target? text
263 'declare' target? (thmrefs + 'and')
269 \item [@{command "declaration"}~@{text d}] adds the declaration
270 function @{text d} of ML type @{ML_type declaration}, to the current
271 local theory under construction. In later application contexts, the
272 function is transformed according to the morphisms being involved in
273 the interpretation hierarchy.
275 \item [@{command "declare"}~@{text thms}] declares theorems to the
276 current local theory context. No theorem binding is involved here,
277 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
278 \secref{sec:axms-thms}), so @{command "declare"} only has the effect
279 of applying attributes as included in the theorem specification.
285 section {* Locales \label{sec:locale} *}
288 Locales are named local contexts, consisting of a list of
289 declaration elements that are modeled after the Isar proof context
290 commands (cf.\ \secref{sec:proof-context}).
294 subsection {* Locale specifications *}
297 \begin{matharray}{rcl}
298 @{command_def "locale"} & : & \isartrans{theory}{local{\dsh}theory} \\
299 @{command_def "print_locale"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
300 @{command_def "print_locales"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
301 @{method_def intro_locales} & : & \isarmeth \\
302 @{method_def unfold_locales} & : & \isarmeth \\
305 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
306 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
307 \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
309 'locale' name ('=' localeexpr)? 'begin'?
311 'print\_locale' '!'? localeexpr
313 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
316 contextexpr: nameref | '(' contextexpr ')' |
317 (contextexpr (name mixfix? +)) | (contextexpr + '+')
319 contextelem: fixes | constrains | assumes | defines | notes
321 fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
323 constrains: 'constrains' (name '::' type + 'and')
325 assumes: 'assumes' (thmdecl? props + 'and')
327 defines: 'defines' (thmdecl? prop proppat? + 'and')
329 notes: 'notes' (thmdef? thmrefs + 'and')
331 includes: 'includes' contextexpr
337 \item [@{command "locale"}~@{text "loc = import + body"}] defines a
338 new locale @{text loc} as a context consisting of a certain view of
339 existing locales (@{text import}) plus some additional elements
340 (@{text body}). Both @{text import} and @{text body} are optional;
341 the degenerate form @{command "locale"}~@{text loc} defines an empty
342 locale, which may still be useful to collect declarations of facts
343 later on. Type-inference on locale expressions automatically takes
344 care of the most general typing that the combined context elements
347 The @{text import} consists of a structured context expression,
348 consisting of references to existing locales, renamed contexts, or
349 merged contexts. Renaming uses positional notation: @{text "c
350 x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed
351 parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>,
352 x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that
353 position. Renaming by default deletes concrete syntax, but new
354 syntax may by specified with a mixfix annotation. An exeption of
355 this rule is the special syntax declared with ``@{text
356 "(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it
357 be changed. Merging proceeds from left-to-right, suppressing any
358 duplicates stemming from different paths through the import
361 The @{text body} consists of basic context elements, further context
362 expressions may be included as well.
366 \item [@{element "fixes"}~@{text "x :: \<tau> (mx)"}] declares a local
367 parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
368 are optional). The special syntax declaration ``@{text
369 "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
370 implicitly in this context.
372 \item [@{element "constrains"}~@{text "x :: \<tau>"}] introduces a type
373 constraint @{text \<tau>} on the local parameter @{text x}.
375 \item [@{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}]
376 introduces local premises, similar to @{command "assume"} within a
377 proof (cf.\ \secref{sec:proof-context}).
379 \item [@{element "defines"}~@{text "a: x \<equiv> t"}] defines a previously
380 declared parameter. This is similar to @{command "def"} within a
381 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
382 takes an equational proposition instead of variable-term pair. The
383 left-hand side of the equation may have additional arguments, e.g.\
384 ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
386 \item [@{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
387 reconsiders facts within a local context. Most notably, this may
388 include arbitrary declarations in any attribute specifications
389 included here, e.g.\ a local @{attribute simp} rule.
391 The initial @{text import} specification of a locale
392 expression maintains a dynamic relation to the locales being
393 referenced (benefiting from any later fact declarations in the
398 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
399 in the syntax of @{element "assumes"} and @{element "defines"} above
400 are illegal in locale definitions. In the long goal format of
401 \secref{sec:goals}, term bindings may be included as expected,
404 \medskip By default, locale specifications are ``closed up'' by
405 turning the given text into a predicate definition @{text
406 loc_axioms} and deriving the original assumptions as local lemmas
407 (modulo local definitions). The predicate statement covers only the
408 newly specified assumptions, omitting the content of included locale
409 expressions. The full cumulative view is only provided on export,
410 involving another predicate @{text loc} that refers to the complete
413 In any case, the predicate arguments are those locale parameters
414 that actually occur in the respective piece of text. Also note that
415 these predicates operate at the meta-level in theory, but the locale
416 packages attempts to internalize statements according to the
417 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
418 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
419 \secref{sec:object-logic}). Separate introduction rules @{text
420 loc_axioms.intro} and @{text loc.intro} are provided as well.
422 \item [@{command "print_locale"}~@{text "import + body"}] prints the
423 specified locale expression in a flattened form. The notable
424 special case @{command "print_locale"}~@{text loc} just prints the
425 contents of the named locale, but keep in mind that type-inference
426 will normalize type variables according to the usual alphabetical
427 order. The command omits @{element "notes"} elements by default.
428 Use @{command "print_locale"}@{text "!"} to get them included.
430 \item [@{command "print_locales"}] prints the names of all locales
431 of the current theory.
433 \item [@{method intro_locales} and @{method unfold_locales}]
434 repeatedly expand all introduction rules of locale predicates of the
435 theory. While @{method intro_locales} only applies the @{text
436 loc.intro} introduction rules and therefore does not decend to
437 assumptions, @{method unfold_locales} is more aggressive and applies
438 @{text loc_axioms.intro} as well. Both methods are aware of locale
439 specifications entailed by the context, both from target statements,
440 and from interpretations (see below). New goals that are entailed
441 by the current context are discharged automatically.
447 subsection {* Interpretation of locales *}
450 Locale expressions (more precisely, \emph{context expressions}) may
451 be instantiated, and the instantiated facts added to the current
452 context. This requires a proof of the instantiated specification
453 and is called \emph{locale interpretation}. Interpretation is
454 possible in theories and locales (command @{command
455 "interpretation"}) and also within a proof body (command @{command
458 \begin{matharray}{rcl}
459 @{command_def "interpretation"} & : & \isartrans{theory}{proof(prove)} \\
460 @{command_def "interpret"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
461 @{command_def "print_interps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
464 \indexouternonterm{interp}
466 'interpretation' (interp | name ('<' | subseteq) contextexpr)
470 'print\_interps' '!'? name
472 instantiation: ('[' (inst+) ']')?
474 interp: (name ':')? \\ (contextexpr instantiation |
475 name instantiation 'where' (thmdecl? prop + 'and'))
481 \item [@{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}]
483 The first form of @{command "interpretation"} interprets @{text
484 expr} in the theory. The instantiation is given as a list of terms
485 @{text insts} and is positional. All parameters must receive an
486 instantiation term --- with the exception of defined parameters.
487 These are, if omitted, derived from the defining equation and other
488 instantiations. Use ``@{text _}'' to omit an instantiation term.
490 The command generates proof obligations for the instantiated
491 specifications (assumes and defines elements). Once these are
492 discharged by the user, instantiated facts are added to the theory
493 in a post-processing phase.
495 Additional equations, which are unfolded in facts during
496 post-processing, may be given after the keyword @{keyword "where"}.
497 This is useful for interpreting concepts introduced through
498 definition specification elements. The equations must be proved.
499 Note that if equations are present, the context expression is
500 restricted to a locale name.
502 The command is aware of interpretations already active in the
503 theory, but does not simplify the goal automatically. In order to
504 simplify the proof obligations use methods @{method intro_locales}
505 or @{method unfold_locales}. Post-processing is not applied to
506 facts of interpretations that are already active. This avoids
507 duplication of interpreted facts, in particular. Note that, in the
508 case of a locale with import, parts of the interpretation may
509 already be active. The command will only process facts for new
512 The context expression may be preceded by a name, which takes effect
513 in the post-processing of facts. It is used to prefix fact names,
514 for example to avoid accidental hiding of other facts.
516 Adding facts to locales has the effect of adding interpreted facts
517 to the theory for all active interpretations also. That is,
518 interpretations dynamically participate in any facts added to
521 \item [@{command "interpretation"}~@{text "name \<subseteq> expr"}]
523 This form of the command interprets @{text expr} in the locale
524 @{text name}. It requires a proof that the specification of @{text
525 name} implies the specification of @{text expr}. As in the
526 localized version of the theorem command, the proof is in the
527 context of @{text name}. After the proof obligation has been
528 dischared, the facts of @{text expr} become part of locale @{text
529 name} as \emph{derived} context elements and are available when the
530 context @{text name} is subsequently entered. Note that, like
531 import, this is dynamic: facts added to a locale part of @{text
532 expr} after interpretation become also available in @{text name}.
533 Like facts of renamed context elements, facts obtained by
534 interpretation may be accessed by prefixing with the parameter
535 renaming (where the parameters are separated by ``@{text _}'').
537 Unlike interpretation in theories, instantiation is confined to the
538 renaming of parameters, which may be specified as part of the
539 context expression @{text expr}. Using defined parameters in @{text
540 name} one may achieve an effect similar to instantiation, though.
542 Only specification fragments of @{text expr} that are not already
543 part of @{text name} (be it imported, derived or a derived fragment
544 of the import) are considered by interpretation. This enables
545 circular interpretations.
547 If interpretations of @{text name} exist in the current theory, the
548 command adds interpretations for @{text expr} as well, with the same
549 prefix and attributes, although only for fragments of @{text expr}
550 that are not interpreted in the theory already.
552 \item [@{command "interpret"}~@{text "expr insts \<WHERE> eqns"}]
553 interprets @{text expr} in the proof context and is otherwise
554 similar to interpretation in theories.
556 \item [@{command "print_interps"}~@{text loc}] prints the
557 interpretations of a particular locale @{text loc} that are active
558 in the current context, either theory or proof context. The
559 exclamation point argument triggers printing of \emph{witness}
560 theorems justifying interpretations. These are normally omitted
566 Since attributes are applied to interpreted theorems,
567 interpretation may modify the context of common proof tools, e.g.\
568 the Simplifier or Classical Reasoner. Since the behavior of such
569 automated reasoning tools is \emph{not} stable under
570 interpretation morphisms, manual declarations might have to be
575 An interpretation in a theory may subsume previous
576 interpretations. This happens if the same specification fragment
577 is interpreted twice and the instantiation of the second
578 interpretation is more general than the interpretation of the
579 first. A warning is issued, since it is likely that these could
580 have been generalized in the first place. The locale package does
581 not attempt to remove subsumed interpretations.
586 section {* Classes \label{sec:class} *}
589 A class is a particular locale with \emph{exactly one} type variable
590 @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
591 is established which is interpreted logically as axiomatic type
592 class \cite{Wenzel:1997:TPHOL} whose logical content are the
593 assumptions of the locale. Thus, classes provide the full
594 generality of locales combined with the commodity of type classes
595 (notably type-inference). See \cite{isabelle-classes} for a short
598 \begin{matharray}{rcl}
599 @{command_def "class"} & : & \isartrans{theory}{local{\dsh}theory} \\
600 @{command_def "instantiation"} & : & \isartrans{theory}{local{\dsh}theory} \\
601 @{command_def "instance"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
602 @{command_def "subclass"} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
603 @{command_def "print_classes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
604 @{method_def intro_classes} & : & \isarmeth \\
608 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
611 'instantiation' (nameref + 'and') '::' arity 'begin'
615 'subclass' target? nameref
620 superclassexpr: nameref | (nameref '+' superclassexpr)
626 \item [@{command "class"}~@{text "c = superclasses + body"}] defines
627 a new class @{text c}, inheriting from @{text superclasses}. This
628 introduces a locale @{text c} with import of all locales @{text
631 Any @{element "fixes"} in @{text body} are lifted to the global
632 theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
633 f\<^sub>n"} of class @{text c}), mapping the local type parameter
634 @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
636 Likewise, @{element "assumes"} in @{text body} are also lifted,
637 mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
638 corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
639 corresponding introduction rule is provided as @{text
640 c_class_axioms.intro}. This rule should be rarely needed directly
641 --- the @{method intro_classes} method takes care of the details of
642 class membership proofs.
644 \item [@{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>,
645 s\<^sub>n) s \<BEGIN>"}] opens a theory target (cf.\
646 \secref{sec:target}) which allows to specify class operations @{text
647 "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding to sort @{text s} at the
648 particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,
649 \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command
650 in the target body poses a goal stating these type arities. The
651 target is concluded by an @{command_ref (local) "end"} command.
653 Note that a list of simultaneous type constructors may be given;
654 this corresponds nicely to mutual recursive type definitions, e.g.\
657 \item [@{command "instance"}] in an instantiation target body sets
658 up a goal stating the type arities claimed at the opening @{command
659 "instantiation"}. The proof would usually proceed by @{method
660 intro_classes}, and then establish the characteristic theorems of
661 the type classes involved. After finishing the proof, the
662 background theory will be augmented by the proven type arities.
664 \item [@{command "subclass"}~@{text c}] in a class context for class
665 @{text d} sets up a goal stating that class @{text c} is logically
666 contained in class @{text d}. After finishing the proof, class
667 @{text d} is proven to be subclass @{text c} and the locale @{text
668 c} is interpreted into @{text d} simultaneously.
670 \item [@{command "print_classes"}] prints all classes in the current
673 \item [@{method intro_classes}] repeatedly expands all class
674 introduction rules of this theory. Note that this method usually
675 needs not be named explicitly, as it is already included in the
676 default proof step (e.g.\ of @{command "proof"}). In particular,
677 instantiation of trivial (syntactic) classes may be performed by a
678 single ``@{command ".."}'' proof step.
684 subsection {* The class target *}
689 A named context may refer to a locale (cf.\ \secref{sec:target}).
690 If this locale is also a class @{text c}, apart from the common
691 locale target behaviour the following happens.
695 \item Local constant declarations @{text "g[\<alpha>]"} referring to the
696 local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
697 are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
698 referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
700 \item Local theorem bindings are lifted as are assumptions.
702 \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
703 global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
704 resolves ambiguities. In rare cases, manual type annotations are
711 subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
714 \begin{matharray}{rcl}
715 @{command_def "axclass"} & : & \isartrans{theory}{theory} \\
716 @{command_def "instance"} & : & \isartrans{theory}{proof(prove)} \\
719 Axiomatic type classes are Isabelle/Pure's primitive
720 \emph{definitional} interface to type classes. For practical
721 applications, you should consider using classes
722 (cf.~\secref{sec:classes}) which provide high level interface.
725 'axclass' classdecl (axmdecl prop +)
727 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
733 \item [@{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n
734 axms"}] defines an axiomatic type class as the intersection of
735 existing classes, with additional axioms holding. Class axioms may
736 not contain more than one type variable. The class axioms (with
737 implicit sort constraints added) are bound to the given names.
738 Furthermore a class introduction rule is generated (being bound as
739 @{text c_class.intro}); this rule is employed by method @{method
740 intro_classes} to support instantiation proofs of this class.
742 The ``class axioms'' are stored as theorems according to the given
743 name specifications, adding @{text "c_class"} as name space prefix;
744 the same facts are also stored collectively as @{text
747 \item [@{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and
748 @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"}]
749 setup a goal stating a class relation or type arity. The proof
750 would usually proceed by @{method intro_classes}, and then establish
751 the characteristic theorems of the type classes involved. After
752 finishing the proof, the theory will be augmented by a type
753 signature declaration corresponding to the resulting theorem.
759 section {* Unrestricted overloading *}
762 Isabelle/Pure's definitional schemes support certain forms of
763 overloading (see \secref{sec:consts}). At most occassions
764 overloading will be used in a Haskell-like fashion together with
765 type classes by means of @{command "instantiation"} (see
766 \secref{sec:class}). Sometimes low-level overloading is desirable.
767 The @{command "overloading"} target provides a convenient view for
770 \begin{matharray}{rcl}
771 @{command_def "overloading"} & : & \isartrans{theory}{local{\dsh}theory} \\
776 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
781 \item [@{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 ::
782 \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}]
783 opens a theory target (cf.\ \secref{sec:target}) which allows to
784 specify constants with overloaded definitions. These are identified
785 by an explicitly given mapping from variable names @{text
786 "x\<^sub>i"} to constants @{text "c\<^sub>i"} at particular type
787 instances. The definitions themselves are established using common
788 specification tools, using the names @{text "x\<^sub>i"} as
789 reference to the corresponding constants. The target is concluded
790 by @{command (local) "end"}.
792 A @{text "(unchecked)"} option disables global dependency checks for
793 the corresponding definition, which is occasionally useful for
794 exotic overloading. It is at the discretion of the user to avoid
795 malformed theory specifications!
801 section {* Incorporating ML code \label{sec:ML} *}
804 \begin{matharray}{rcl}
805 @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
806 @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
807 @{command_def "ML_prf"} & : & \isarkeep{proof} \\
808 @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
809 @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
810 @{command_def "setup"} & : & \isartrans{theory}{theory} \\
816 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
822 \item [@{command "use"}~@{text "file"}] reads and executes ML
823 commands from @{text "file"}. The current theory context is passed
824 down to the ML toplevel and may be modified, using @{ML [source=false]
825 "Context.>>"} or derived ML commands. The file name is checked with
826 the @{keyword_ref "uses"} dependency declaration given in the theory
827 header (see also \secref{sec:begin-thy}).
829 Top-level ML bindings are stored within the (global or local) theory
832 \item [@{command "ML"}~@{text "text"}] is similar to @{command
833 "use"}, but executes ML commands directly from the given @{text
834 "text"}. Top-level ML bindings are stored within the (global or
835 local) theory context.
837 \item [@{command "ML_prf"}] is analogous to @{command "ML"} but
838 works within a proof context.
840 Top-level ML bindings are stored within the proof context in a
841 purely sequential fashion, disregarding the nested proof structure.
842 ML bindings introduced by @{command "ML_prf"} are discarded at the
845 \item [@{command "ML_val"} and @{command "ML_command"}] are
846 diagnostic versions of @{command "ML"}, which means that the context
847 may not be updated. @{command "ML_val"} echos the bindings produced
848 at the ML toplevel, but @{command "ML_command"} is silent.
850 \item [@{command "setup"}~@{text "text"}] changes the current theory
851 context by applying @{text "text"}, which refers to an ML expression
852 of type @{ML_type [source=false] "theory -> theory"}. This enables
853 to initialize any object-logic specific tools and packages written
860 section {* Primitive specification elements *}
862 subsection {* Type classes and sorts \label{sec:classes} *}
865 \begin{matharray}{rcll}
866 @{command_def "classes"} & : & \isartrans{theory}{theory} \\
867 @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
868 @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
869 @{command_def "class_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
873 'classes' (classdecl +)
875 'classrel' (nameref ('<' | subseteq) nameref + 'and')
883 \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
884 declares class @{text c} to be a subclass of existing classes @{text
885 "c\<^sub>1, \<dots>, c\<^sub>n"}. Cyclic class structures are not permitted.
887 \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states
888 subclass relations between existing classes @{text "c\<^sub>1"} and
889 @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref
890 "instance"} command (see \secref{sec:axclass}) provides a way to
891 introduce proven class relations.
893 \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the
894 new default sort for any type variables given without sort
895 constraints. Usually, the default sort would be only changed when
896 defining a new object-logic.
898 \item [@{command "class_deps"}] visualizes the subclass relation,
899 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
905 subsection {* Types and type abbreviations \label{sec:types-pure} *}
908 \begin{matharray}{rcll}
909 @{command_def "types"} & : & \isartrans{theory}{theory} \\
910 @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
911 @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
912 @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
916 'types' (typespec '=' type infix? +)
918 'typedecl' typespec infix?
920 'nonterminals' (name +)
922 'arities' (nameref '::' arity +)
928 \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
929 introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
930 for existing type @{text "\<tau>"}. Unlike actual type definitions, as
931 are available in Isabelle/HOL for example, type synonyms are just
932 purely syntactic abbreviations without any logical significance.
933 Internally, type synonyms are fully expanded.
935 \item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]
936 declares a new type constructor @{text t}, intended as an actual
937 logical type (of the object-logic, if available).
939 \item [@{command "nonterminals"}~@{text c}] declares type
940 constructors @{text c} (without arguments) to act as purely
941 syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
942 syntax of terms or types.
944 \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)
945 s"}] augments Isabelle's order-sorted signature of types by new type
946 constructor arities. This is done axiomatically! The @{command_ref
947 "instance"} command (see \S\ref{sec:axclass}) provides a way to
948 introduce proven type arities.
954 subsection {* Constants and definitions \label{sec:consts} *}
957 Definitions essentially express abbreviations within the logic. The
958 simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
959 c} is a newly declared constant. Isabelle also allows derived forms
960 where the arguments of @{text c} appear on the left, abbreviating a
961 prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
962 written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
963 definitions may be weakened by adding arbitrary pre-conditions:
964 @{text "A \<Longrightarrow> c x y \<equiv> t"}.
966 \medskip The built-in well-formedness conditions for definitional
971 \item Arguments (on the left-hand side) must be distinct variables.
973 \item All variables on the right-hand side must also appear on the
976 \item All type variables on the right-hand side must also appear on
977 the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
978 \<alpha> list)"} for example.
980 \item The definition must not be recursive. Most object-logics
981 provide definitional principles that can be used to express
986 Overloading means that a constant being declared as @{text "c :: \<alpha>
987 decl"} may be defined separately on type instances @{text "c ::
988 (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
989 t}. The right-hand side may mention overloaded constants
990 recursively at type instances corresponding to the immediate
991 argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
992 specification patterns impose global constraints on all occurrences,
993 e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
994 corresponding occurrences on some right-hand side need to be an
995 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
997 \begin{matharray}{rcl}
998 @{command_def "consts"} & : & \isartrans{theory}{theory} \\
999 @{command_def "defs"} & : & \isartrans{theory}{theory} \\
1000 @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
1004 'consts' ((name '::' type mixfix?) +)
1006 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1011 'constdefs' structs? (constdecl? constdef +)
1014 structs: '(' 'structure' (vars + 'and') ')'
1016 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1018 constdef: thmdecl? prop
1024 \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
1025 @{text c} to have any instance of type scheme @{text \<sigma>}. The
1026 optional mixfix annotations may attach concrete syntax to the
1029 \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}
1030 as a definitional axiom for some existing constant.
1032 The @{text "(unchecked)"} option disables global dependency checks
1033 for this definition, which is occasionally useful for exotic
1034 overloading. It is at the discretion of the user to avoid malformed
1035 theory specifications!
1037 The @{text "(overloaded)"} option declares definitions to be
1038 potentially overloaded. Unless this option is given, a warning
1039 message would be issued for any definitional equation with a more
1040 special type than that of the corresponding constant declaration.
1042 \item [@{command "constdefs"}] provides a streamlined combination of
1043 constants declarations and definitions: type-inference takes care of
1044 the most general typing of the given specification (the optional
1045 type constraint may refer to type-inference dummies ``@{text
1046 _}'' as usual). The resulting type declaration needs to agree with
1047 that of the specification; overloading is \emph{not} supported here!
1049 The constant name may be omitted altogether, if neither type nor
1050 syntax declarations are given. The canonical name of the
1051 definitional axiom for constant @{text c} will be @{text c_def},
1052 unless specified otherwise. Also note that the given list of
1053 specifications is processed in a strictly sequential manner, with
1054 type-checking being performed independently.
1056 An optional initial context of @{text "(structure)"} declarations
1057 admits use of indexed syntax, using the special symbol @{verbatim
1058 "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
1059 particularly useful with locales (see also \S\ref{sec:locale}).
1065 section {* Axioms and theorems \label{sec:axms-thms} *}
1068 \begin{matharray}{rcll}
1069 @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
1070 @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
1071 @{command_def "theorems"} & : & \isarkeep{local{\dsh}theory} \\
1075 'axioms' (axmdecl prop +)
1077 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1083 \item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary
1084 statements as axioms of the meta-logic. In fact, axioms are
1085 ``axiomatic theorems'', and may be referred later just as any other
1088 Axioms are usually only introduced when declaring new logical
1089 systems. Everyday work is typically done the hard way, with proper
1090 definitions and proven theorems.
1092 \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
1093 retrieves and stores existing facts in the theory context, or the
1094 specified target context (see also \secref{sec:target}). Typical
1095 applications would also involve attributes, to declare Simplifier
1098 \item [@{command "theorems"}] is essentially the same as @{command
1099 "lemmas"}, but marks the result as a different kind of facts.
1105 section {* Oracles *}
1107 text {* Oracles allow Isabelle to take advantage of external reasoners
1108 such as arithmetic decision procedures, model checkers, fast
1109 tautology checkers or computer algebra systems. Invoked as an
1110 oracle, an external reasoner can create arbitrary Isabelle theorems.
1112 It is the responsibility of the user to ensure that the external
1113 reasoner is as trustworthy as the application requires. Another
1114 typical source of errors is the linkup between Isabelle and the
1115 external tool, not just its concrete implementation, but also the
1116 required translation between two different logical environments.
1118 Isabelle merely guarantees well-formedness of the propositions being
1119 asserted, and records within the internal derivation object how
1120 presumed theorems depend on unproven suppositions.
1122 \begin{matharray}{rcl}
1123 @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
1127 'oracle' name '=' text
1133 \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
1134 expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
1135 ML function of type @{ML_text "'a -> thm"}, which is bound to the
1136 global identifier @{ML_text name}. This acts like an infinitary
1137 specification of axioms! Invoking the oracle only works within the
1138 scope of the resulting theory.
1142 See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
1143 defining a new primitive rule as oracle, and turning it into a proof
1148 section {* Name spaces *}
1151 \begin{matharray}{rcl}
1152 @{command_def "global"} & : & \isartrans{theory}{theory} \\
1153 @{command_def "local"} & : & \isartrans{theory}{theory} \\
1154 @{command_def "hide"} & : & \isartrans{theory}{theory} \\
1158 'hide' ('(open)')? name (nameref + )
1162 Isabelle organizes any kind of name declarations (of types,
1163 constants, theorems etc.) by separate hierarchically structured name
1164 spaces. Normally the user does not have to control the behavior of
1165 name spaces by hand, yet the following commands provide some way to
1170 \item [@{command "global"} and @{command "local"}] change the
1171 current name declaration mode. Initially, theories start in
1172 @{command "local"} mode, causing all names to be automatically
1173 qualified by the theory name. Changing this to @{command "global"}
1174 causes all names to be declared without the theory prefix, until
1175 @{command "local"} is declared again.
1177 Note that global names are prone to get hidden accidently later,
1178 when qualified names of the same base name are introduced.
1180 \item [@{command "hide"}~@{text "space names"}] fully removes
1181 declarations from a given name space (which may be @{text "class"},
1182 @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
1183 "(open)"} option, only the base name is hidden. Global
1184 (unqualified) names may never be hidden.
1186 Note that hiding name space accesses has no impact on logical
1187 declarations --- they remain valid internally. Entities that are no
1188 longer accessible to the user are printed with the special qualifier
1189 ``@{text "??"}'' prefixed to the full internal name.
1195 section {* Syntax and translations \label{sec:syn-trans} *}
1198 \begin{matharray}{rcl}
1199 @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
1200 @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
1201 @{command_def "translations"} & : & \isartrans{theory}{theory} \\
1202 @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
1206 ('syntax' | 'no\_syntax') mode? (constdecl +)
1208 ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
1211 mode: ('(' ( name | 'output' | name 'output' ) ')')
1213 transpat: ('(' nameref ')')? string
1219 \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to
1220 @{command "consts"}~@{text decls}, except that the actual logical
1221 signature extension is omitted. Thus the context free grammar of
1222 Isabelle's inner syntax may be augmented in arbitrary ways,
1223 independently of the logic. The @{text mode} argument refers to the
1224 print mode that the grammar rules belong; unless the @{keyword_ref
1225 "output"} indicator is given, all productions are added both to the
1226 input and output grammar.
1228 \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes
1229 grammar declarations (and translations) resulting from @{text
1230 decls}, which are interpreted in the same manner as for @{command
1233 \item [@{command "translations"}~@{text rules}] specifies syntactic
1234 translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
1235 parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
1236 Translation patterns may be prefixed by the syntactic category to be
1237 used for parsing; the default is @{text logic}.
1239 \item [@{command "no_translations"}~@{text rules}] removes syntactic
1240 translation rules, which are interpreted in the same manner as for
1241 @{command "translations"} above.
1247 section {* Syntax translation functions *}
1250 \begin{matharray}{rcl}
1251 @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
1252 @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
1253 @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
1254 @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
1255 @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
1259 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
1260 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
1264 Syntax translation functions written in ML admit almost arbitrary
1265 manipulations of Isabelle's inner syntax. Any of the above commands
1266 have a single \railqtok{text} argument that refers to an ML
1267 expression of appropriate type, which are as follows by default:
1269 %FIXME proper antiquotations
1271 val parse_ast_translation : (string * (ast list -> ast)) list
1272 val parse_translation : (string * (term list -> term)) list
1273 val print_translation : (string * (term list -> term)) list
1274 val typed_print_translation :
1275 (string * (bool -> typ -> term list -> term)) list
1276 val print_ast_translation : (string * (ast list -> ast)) list
1279 If the @{text "(advanced)"} option is given, the corresponding
1280 translation functions may depend on the current theory or proof
1281 context. This allows to implement advanced syntax mechanisms, as
1282 translations functions may refer to specific theory declarations or
1283 auxiliary proof data.
1285 See also \cite[\S8]{isabelle-ref} for more information on the
1286 general concept of syntax transformations in Isabelle.
1288 %FIXME proper antiquotations
1290 val parse_ast_translation:
1291 (string * (Proof.context -> ast list -> ast)) list
1292 val parse_translation:
1293 (string * (Proof.context -> term list -> term)) list
1294 val print_translation:
1295 (string * (Proof.context -> term list -> term)) list
1296 val typed_print_translation:
1297 (string * (Proof.context -> bool -> typ -> term list -> term)) list
1298 val print_ast_translation:
1299 (string * (Proof.context -> ast list -> ast)) list