5 chapter {* Theory specifications *}
7 section {* Defining theories \label{sec:begin-thy} *}
10 \begin{matharray}{rcl}
11 @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
12 @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
15 Isabelle/Isar theories are defined via theory files, which may
16 contain both specifications and proofs; occasionally definitional
17 mechanisms also require some explicit proof. The theory body may be
18 sub-structured by means of \emph{local theory targets}, such as
19 @{command "locale"} and @{command "class"}.
21 The first proper command of a theory is @{command "theory"}, which
22 indicates imports of previous theories and optional dependencies on
23 other source files (usually in ML). Just preceding the initial
24 @{command "theory"} command there may be an optional @{command
25 "header"} declaration, which is only relevant to document
26 preparation: see also the other section markup commands in
29 A theory is concluded by a final @{command (global) "end"} command,
30 one that does not belong to a local theory target. No further
31 commands may follow such a global @{command (global) "end"},
32 although some user-interfaces might pretend that trailing input is
36 'theory' name 'imports' (name +) uses? 'begin'
39 uses: 'uses' ((name | parname) +);
44 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
45 starts a new theory @{text A} based on the merge of existing
46 theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
48 Due to the possibility to import more than one ancestor, the
49 resulting theory structure of an Isabelle session forms a directed
50 acyclic graph (DAG). Isabelle's theory loader ensures that the
51 sources contributing to the development graph are always up-to-date:
52 changed files are automatically reloaded whenever a theory header
53 specification is processed.
55 The optional @{keyword_def "uses"} specification declares additional
56 dependencies on extra files (usually ML sources). Files will be
57 loaded immediately (as ML), unless the name is parenthesized. The
58 latter case records a dependency that needs to be resolved later in
59 the text, usually via explicit @{command_ref "use"} for ML files;
60 other file formats require specific load commands defined by the
61 corresponding tools or packages.
63 \item @{command (global) "end"} concludes the current theory
64 definition. Note that local theory targets involve a local
65 @{command (local) "end"}, which is clear from the nesting.
71 section {* Local theory targets \label{sec:target} *}
74 A local theory target is a context managed separately within the
75 enclosing theory. Contexts may introduce parameters (fixed
76 variables) and assumptions (hypotheses). Definitions and theorems
77 depending on the context may be added incrementally later on. Named
78 contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
79 (cf.\ \secref{sec:class}); the name ``@{text "-"}'' signifies the
80 global theory context.
82 \begin{matharray}{rcll}
83 @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
84 @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
87 \indexouternonterm{target}
89 'context' name 'begin'
92 target: '(' 'in' name ')'
98 \item @{command "context"}~@{text "c \<BEGIN>"} recommences an
99 existing locale or class context @{text c}. Note that locale and
100 class definitions allow to include the @{keyword "begin"} keyword as
101 well, in order to continue the local theory immediately after the
102 initial specification.
104 \item @{command (local) "end"} concludes the current local theory
105 and continues the enclosing global theory. Note that a global
106 @{command (global) "end"} has a different meaning: it concludes the
107 theory itself (\secref{sec:begin-thy}).
109 \item @{text "(\<IN> c)"} given after any local theory command
110 specifies an immediate target, e.g.\ ``@{command
111 "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
112 "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
113 global theory context; the current target context will be suspended
114 for this command only. Note that ``@{text "(\<IN> -)"}'' will
115 always produce a global result independently of the current target
120 The exact meaning of results produced within a local theory context
121 depends on the underlying target infrastructure (locale, type class
122 etc.). The general idea is as follows, considering a context named
123 @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
125 Definitions are exported by introducing a global version with
126 additional arguments; a syntactic abbreviation links the long form
127 with the abstract version of the target context. For example,
128 @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
129 level (for arbitrary @{text "?x"}), together with a local
130 abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
131 fixed parameter @{text x}).
133 Theorems are exported by discharging the assumptions and
134 generalizing the parameters of the context. For example, @{text "a:
135 B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
140 section {* Basic specification elements *}
143 \begin{matharray}{rcll}
144 @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
145 @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
146 @{attribute_def "defn"} & : & @{text attribute} \\
147 @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
148 @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
151 These specification mechanisms provide a slightly more abstract view
152 than the underlying primitives of @{command "consts"}, @{command
153 "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
154 \secref{sec:axms-thms}). In particular, type-inference is commonly
155 available, and result names need not be given.
158 'axiomatization' target? fixes? ('where' specs)?
160 'definition' target? (decl 'where')? thmdecl? prop
162 'abbreviation' target? mode? (decl 'where')? prop
165 fixes: ((name ('::' type)? mixfix? | vars) + 'and')
167 specs: (thmdecl? props + 'and')
169 decl: name ('::' type)? mixfix?
175 \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
176 introduces several constants simultaneously and states axiomatic
177 properties for these. The constants are marked as being specified
178 once and for all, which prevents additional specifications being
181 Note that axiomatic specifications are only appropriate when
182 declaring a new logical system; axiomatic specifications are
183 restricted to global theory contexts. Normal applications should
184 only use definitional mechanisms!
186 \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
187 internal definition @{text "c \<equiv> t"} according to the specification
188 given as @{text eq}, which is then turned into a proven fact. The
189 given proposition may deviate from internal meta-level equality
190 according to the rewrite rules declared as @{attribute defn} by the
191 object-logic. This usually covers object-level equality @{text "x =
192 y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
193 change the @{attribute defn} setup.
195 Definitions may be presented with explicit arguments on the LHS, as
196 well as additional conditions, e.g.\ @{text "f x y = t"} instead of
197 @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
198 unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
200 \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
201 syntactic constant which is associated with a certain term according
202 to the meta-level equality @{text eq}.
204 Abbreviations participate in the usual type-inference process, but
205 are expanded before the logic ever sees them. Pretty printing of
206 terms involves higher-order rewriting with rules stemming from
207 reverted abbreviations. This needs some care to avoid overlapping
208 or looping syntactic replacements!
210 The optional @{text mode} specification restricts output to a
211 particular print mode; using ``@{text input}'' here achieves the
212 effect of one-way abbreviations. The mode may also include an
213 ``@{keyword "output"}'' qualifier that affects the concrete syntax
214 declared for abbreviations, cf.\ @{command "syntax"} in
215 \secref{sec:syn-trans}.
217 \item @{command "print_abbrevs"} prints all constant abbreviations
218 of the current context.
224 section {* Generic declarations *}
227 Arbitrary operations on the background context may be wrapped-up as
228 generic declaration elements. Since the underlying concept of local
229 theories may be subject to later re-interpretation, there is an
230 additional dependency on a morphism that tells the difference of the
231 original declaration context wrt.\ the application context
232 encountered later on. A fact declaration is an important special
233 case: it consists of a theorem which is applied to the context by
234 means of an attribute.
236 \begin{matharray}{rcl}
237 @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
238 @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
242 'declaration' target? text
244 'declare' target? (thmrefs + 'and')
250 \item @{command "declaration"}~@{text d} adds the declaration
251 function @{text d} of ML type @{ML_type declaration}, to the current
252 local theory under construction. In later application contexts, the
253 function is transformed according to the morphisms being involved in
254 the interpretation hierarchy.
256 \item @{command "declare"}~@{text thms} declares theorems to the
257 current local theory context. No theorem binding is involved here,
258 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
259 \secref{sec:axms-thms}), so @{command "declare"} only has the effect
260 of applying attributes as included in the theorem specification.
266 section {* Locales \label{sec:locale} *}
269 Locales are named local contexts, consisting of a list of
270 declaration elements that are modeled after the Isar proof context
271 commands (cf.\ \secref{sec:proof-context}).
275 subsection {* Locale specifications *}
278 \begin{matharray}{rcl}
279 @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
280 @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
281 @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
282 @{method_def intro_locales} & : & @{text method} \\
283 @{method_def unfold_locales} & : & @{text method} \\
286 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
287 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
288 \indexisarelem{defines}\indexisarelem{notes}
290 'locale' name ('=' localeexpr)? 'begin'?
292 'print\_locale' '!'? localeexpr
294 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
297 contextexpr: nameref | '(' contextexpr ')' |
298 (contextexpr (name mixfix? +)) | (contextexpr + '+')
300 contextelem: fixes | constrains | assumes | defines | notes
302 fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
304 constrains: 'constrains' (name '::' type + 'and')
306 assumes: 'assumes' (thmdecl? props + 'and')
308 defines: 'defines' (thmdecl? prop proppat? + 'and')
310 notes: 'notes' (thmdef? thmrefs + 'and')
316 \item @{command "locale"}~@{text "loc = import + body"} defines a
317 new locale @{text loc} as a context consisting of a certain view of
318 existing locales (@{text import}) plus some additional elements
319 (@{text body}). Both @{text import} and @{text body} are optional;
320 the degenerate form @{command "locale"}~@{text loc} defines an empty
321 locale, which may still be useful to collect declarations of facts
322 later on. Type-inference on locale expressions automatically takes
323 care of the most general typing that the combined context elements
326 The @{text import} consists of a structured context expression,
327 consisting of references to existing locales, renamed contexts, or
328 merged contexts. Renaming uses positional notation: @{text "c
329 x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed
330 parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>,
331 x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that
332 position. Renaming by default deletes concrete syntax, but new
333 syntax may by specified with a mixfix annotation. An exeption of
334 this rule is the special syntax declared with ``@{text
335 "(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it
336 be changed. Merging proceeds from left-to-right, suppressing any
337 duplicates stemming from different paths through the import
340 The @{text body} consists of basic context elements, further context
341 expressions may be included as well.
345 \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
346 parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
347 are optional). The special syntax declaration ``@{text
348 "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
349 implicitly in this context.
351 \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
352 constraint @{text \<tau>} on the local parameter @{text x}.
354 \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
355 introduces local premises, similar to @{command "assume"} within a
356 proof (cf.\ \secref{sec:proof-context}).
358 \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
359 declared parameter. This is similar to @{command "def"} within a
360 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
361 takes an equational proposition instead of variable-term pair. The
362 left-hand side of the equation may have additional arguments, e.g.\
363 ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
365 \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
366 reconsiders facts within a local context. Most notably, this may
367 include arbitrary declarations in any attribute specifications
368 included here, e.g.\ a local @{attribute simp} rule.
370 The initial @{text import} specification of a locale expression
371 maintains a dynamic relation to the locales being referenced
372 (benefiting from any later fact declarations in the obvious manner).
376 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
377 in the syntax of @{element "assumes"} and @{element "defines"} above
378 are illegal in locale definitions. In the long goal format of
379 \secref{sec:goals}, term bindings may be included as expected,
382 \medskip By default, locale specifications are ``closed up'' by
383 turning the given text into a predicate definition @{text
384 loc_axioms} and deriving the original assumptions as local lemmas
385 (modulo local definitions). The predicate statement covers only the
386 newly specified assumptions, omitting the content of included locale
387 expressions. The full cumulative view is only provided on export,
388 involving another predicate @{text loc} that refers to the complete
391 In any case, the predicate arguments are those locale parameters
392 that actually occur in the respective piece of text. Also note that
393 these predicates operate at the meta-level in theory, but the locale
394 packages attempts to internalize statements according to the
395 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
396 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
397 \secref{sec:object-logic}). Separate introduction rules @{text
398 loc_axioms.intro} and @{text loc.intro} are provided as well.
400 \item @{command "print_locale"}~@{text "import + body"} prints the
401 specified locale expression in a flattened form. The notable
402 special case @{command "print_locale"}~@{text loc} just prints the
403 contents of the named locale, but keep in mind that type-inference
404 will normalize type variables according to the usual alphabetical
405 order. The command omits @{element "notes"} elements by default.
406 Use @{command "print_locale"}@{text "!"} to get them included.
408 \item @{command "print_locales"} prints the names of all locales
409 of the current theory.
411 \item @{method intro_locales} and @{method unfold_locales}
412 repeatedly expand all introduction rules of locale predicates of the
413 theory. While @{method intro_locales} only applies the @{text
414 loc.intro} introduction rules and therefore does not decend to
415 assumptions, @{method unfold_locales} is more aggressive and applies
416 @{text loc_axioms.intro} as well. Both methods are aware of locale
417 specifications entailed by the context, both from target statements,
418 and from interpretations (see below). New goals that are entailed
419 by the current context are discharged automatically.
425 subsection {* Interpretation of locales *}
428 Locale expressions (more precisely, \emph{context expressions}) may
429 be instantiated, and the instantiated facts added to the current
430 context. This requires a proof of the instantiated specification
431 and is called \emph{locale interpretation}. Interpretation is
432 possible in theories and locales (command @{command
433 "interpretation"}) and also within a proof body (command @{command
436 \begin{matharray}{rcl}
437 @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
438 @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
441 \indexouternonterm{interp}
443 'interpretation' (interp | name ('<' | subseteq) contextexpr)
447 instantiation: ('[' (inst+) ']')?
449 interp: (name ':')? \\ (contextexpr instantiation |
450 name instantiation 'where' (thmdecl? prop + 'and'))
456 \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
458 The first form of @{command "interpretation"} interprets @{text
459 expr} in the theory. The instantiation is given as a list of terms
460 @{text insts} and is positional. All parameters must receive an
461 instantiation term --- with the exception of defined parameters.
462 These are, if omitted, derived from the defining equation and other
463 instantiations. Use ``@{text _}'' to omit an instantiation term.
465 The command generates proof obligations for the instantiated
466 specifications (assumes and defines elements). Once these are
467 discharged by the user, instantiated facts are added to the theory
468 in a post-processing phase.
470 Additional equations, which are unfolded in facts during
471 post-processing, may be given after the keyword @{keyword "where"}.
472 This is useful for interpreting concepts introduced through
473 definition specification elements. The equations must be proved.
474 Note that if equations are present, the context expression is
475 restricted to a locale name.
477 The command is aware of interpretations already active in the
478 theory, but does not simplify the goal automatically. In order to
479 simplify the proof obligations use methods @{method intro_locales}
480 or @{method unfold_locales}. Post-processing is not applied to
481 facts of interpretations that are already active. This avoids
482 duplication of interpreted facts, in particular. Note that, in the
483 case of a locale with import, parts of the interpretation may
484 already be active. The command will only process facts for new
487 The context expression may be preceded by a name, which takes effect
488 in the post-processing of facts. It is used to prefix fact names,
489 for example to avoid accidental hiding of other facts.
491 Adding facts to locales has the effect of adding interpreted facts
492 to the theory for all active interpretations also. That is,
493 interpretations dynamically participate in any facts added to
496 \item @{command "interpretation"}~@{text "name \<subseteq> expr"}
498 This form of the command interprets @{text expr} in the locale
499 @{text name}. It requires a proof that the specification of @{text
500 name} implies the specification of @{text expr}. As in the
501 localized version of the theorem command, the proof is in the
502 context of @{text name}. After the proof obligation has been
503 dischared, the facts of @{text expr} become part of locale @{text
504 name} as \emph{derived} context elements and are available when the
505 context @{text name} is subsequently entered. Note that, like
506 import, this is dynamic: facts added to a locale part of @{text
507 expr} after interpretation become also available in @{text name}.
508 Like facts of renamed context elements, facts obtained by
509 interpretation may be accessed by prefixing with the parameter
510 renaming (where the parameters are separated by ``@{text _}'').
512 Unlike interpretation in theories, instantiation is confined to the
513 renaming of parameters, which may be specified as part of the
514 context expression @{text expr}. Using defined parameters in @{text
515 name} one may achieve an effect similar to instantiation, though.
517 Only specification fragments of @{text expr} that are not already
518 part of @{text name} (be it imported, derived or a derived fragment
519 of the import) are considered by interpretation. This enables
520 circular interpretations.
522 If interpretations of @{text name} exist in the current theory, the
523 command adds interpretations for @{text expr} as well, with the same
524 prefix and attributes, although only for fragments of @{text expr}
525 that are not interpreted in the theory already.
527 \item @{command "interpret"}~@{text "expr insts \<WHERE> eqns"}
528 interprets @{text expr} in the proof context and is otherwise
529 similar to interpretation in theories.
534 Since attributes are applied to interpreted theorems,
535 interpretation may modify the context of common proof tools, e.g.\
536 the Simplifier or Classical Reasoner. Since the behavior of such
537 automated reasoning tools is \emph{not} stable under
538 interpretation morphisms, manual declarations might have to be
543 An interpretation in a theory may subsume previous
544 interpretations. This happens if the same specification fragment
545 is interpreted twice and the instantiation of the second
546 interpretation is more general than the interpretation of the
547 first. A warning is issued, since it is likely that these could
548 have been generalized in the first place. The locale package does
549 not attempt to remove subsumed interpretations.
554 section {* Classes \label{sec:class} *}
557 A class is a particular locale with \emph{exactly one} type variable
558 @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
559 is established which is interpreted logically as axiomatic type
560 class \cite{Wenzel:1997:TPHOL} whose logical content are the
561 assumptions of the locale. Thus, classes provide the full
562 generality of locales combined with the commodity of type classes
563 (notably type-inference). See \cite{isabelle-classes} for a short
566 \begin{matharray}{rcl}
567 @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
568 @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
569 @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
570 @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
571 @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
572 @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
573 @{method_def intro_classes} & : & @{text method} \\
577 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
580 'instantiation' (nameref + 'and') '::' arity 'begin'
584 'subclass' target? nameref
591 superclassexpr: nameref | (nameref '+' superclassexpr)
597 \item @{command "class"}~@{text "c = superclasses + body"} defines
598 a new class @{text c}, inheriting from @{text superclasses}. This
599 introduces a locale @{text c} with import of all locales @{text
602 Any @{element "fixes"} in @{text body} are lifted to the global
603 theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
604 f\<^sub>n"} of class @{text c}), mapping the local type parameter
605 @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
607 Likewise, @{element "assumes"} in @{text body} are also lifted,
608 mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
609 corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
610 corresponding introduction rule is provided as @{text
611 c_class_axioms.intro}. This rule should be rarely needed directly
612 --- the @{method intro_classes} method takes care of the details of
613 class membership proofs.
615 \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
616 \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
617 allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
618 to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
619 \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the
620 target body poses a goal stating these type arities. The target is
621 concluded by an @{command_ref (local) "end"} command.
623 Note that a list of simultaneous type constructors may be given;
624 this corresponds nicely to mutual recursive type definitions, e.g.\
627 \item @{command "instance"} in an instantiation target body sets
628 up a goal stating the type arities claimed at the opening @{command
629 "instantiation"}. The proof would usually proceed by @{method
630 intro_classes}, and then establish the characteristic theorems of
631 the type classes involved. After finishing the proof, the
632 background theory will be augmented by the proven type arities.
634 \item @{command "subclass"}~@{text c} in a class context for class
635 @{text d} sets up a goal stating that class @{text c} is logically
636 contained in class @{text d}. After finishing the proof, class
637 @{text d} is proven to be subclass @{text c} and the locale @{text
638 c} is interpreted into @{text d} simultaneously.
640 \item @{command "print_classes"} prints all classes in the current
643 \item @{command "class_deps"} visualizes all classes and their
644 subclass relations as a Hasse diagram.
646 \item @{method intro_classes} repeatedly expands all class
647 introduction rules of this theory. Note that this method usually
648 needs not be named explicitly, as it is already included in the
649 default proof step (e.g.\ of @{command "proof"}). In particular,
650 instantiation of trivial (syntactic) classes may be performed by a
651 single ``@{command ".."}'' proof step.
657 subsection {* The class target *}
662 A named context may refer to a locale (cf.\ \secref{sec:target}).
663 If this locale is also a class @{text c}, apart from the common
664 locale target behaviour the following happens.
668 \item Local constant declarations @{text "g[\<alpha>]"} referring to the
669 local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
670 are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
671 referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
673 \item Local theorem bindings are lifted as are assumptions.
675 \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
676 global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
677 resolves ambiguities. In rare cases, manual type annotations are
684 subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
687 \begin{matharray}{rcl}
688 @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
689 @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
692 Axiomatic type classes are Isabelle/Pure's primitive
693 \emph{definitional} interface to type classes. For practical
694 applications, you should consider using classes
695 (cf.~\secref{sec:classes}) which provide high level interface.
698 'axclass' classdecl (axmdecl prop +)
700 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
706 \item @{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n axms"} defines an
707 axiomatic type class as the intersection of existing classes, with
708 additional axioms holding. Class axioms may not contain more than
709 one type variable. The class axioms (with implicit sort constraints
710 added) are bound to the given names. Furthermore a class
711 introduction rule is generated (being bound as @{text
712 c_class.intro}); this rule is employed by method @{method
713 intro_classes} to support instantiation proofs of this class.
715 The ``class axioms'' (which are derived from the internal class
716 definition) are stored as theorems according to the given name
717 specifications; the name space prefix @{text "c_class"} is added
718 here. The full collection of these facts is also stored as @{text
721 \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
722 "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
723 relation or type arity. The proof would usually proceed by @{method
724 intro_classes}, and then establish the characteristic theorems of
725 the type classes involved. After finishing the proof, the theory
726 will be augmented by a type signature declaration corresponding to
727 the resulting theorem.
733 section {* Unrestricted overloading *}
736 Isabelle/Pure's definitional schemes support certain forms of
737 overloading (see \secref{sec:consts}). At most occassions
738 overloading will be used in a Haskell-like fashion together with
739 type classes by means of @{command "instantiation"} (see
740 \secref{sec:class}). Sometimes low-level overloading is desirable.
741 The @{command "overloading"} target provides a convenient view for
744 \begin{matharray}{rcl}
745 @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
750 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
755 \item @{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}
756 opens a theory target (cf.\ \secref{sec:target}) which allows to
757 specify constants with overloaded definitions. These are identified
758 by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
759 constants @{text "c\<^sub>i"} at particular type instances. The
760 definitions themselves are established using common specification
761 tools, using the names @{text "x\<^sub>i"} as reference to the
762 corresponding constants. The target is concluded by @{command
765 A @{text "(unchecked)"} option disables global dependency checks for
766 the corresponding definition, which is occasionally useful for
767 exotic overloading. It is at the discretion of the user to avoid
768 malformed theory specifications!
774 section {* Incorporating ML code \label{sec:ML} *}
777 \begin{matharray}{rcl}
778 @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
779 @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
780 @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
781 @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
782 @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
783 @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
787 @{index_ML bind_thms: "string * thm list -> unit"} \\
788 @{index_ML bind_thm: "string * thm -> unit"} \\
794 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
800 \item @{command "use"}~@{text "file"} reads and executes ML
801 commands from @{text "file"}. The current theory context is passed
802 down to the ML toplevel and may be modified, using @{ML [source=false]
803 "Context.>>"} or derived ML commands. The file name is checked with
804 the @{keyword_ref "uses"} dependency declaration given in the theory
805 header (see also \secref{sec:begin-thy}).
807 Top-level ML bindings are stored within the (global or local) theory
810 \item @{command "ML"}~@{text "text"} is similar to @{command "use"},
811 but executes ML commands directly from the given @{text "text"}.
812 Top-level ML bindings are stored within the (global or local) theory
815 \item @{command "ML_prf"} is analogous to @{command "ML"} but works
816 within a proof context.
818 Top-level ML bindings are stored within the proof context in a
819 purely sequential fashion, disregarding the nested proof structure.
820 ML bindings introduced by @{command "ML_prf"} are discarded at the
823 \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
824 versions of @{command "ML"}, which means that the context may not be
825 updated. @{command "ML_val"} echos the bindings produced at the ML
826 toplevel, but @{command "ML_command"} is silent.
828 \item @{command "setup"}~@{text "text"} changes the current theory
829 context by applying @{text "text"}, which refers to an ML expression
830 of type @{ML_type [source=false] "theory -> theory"}. This enables
831 to initialize any object-logic specific tools and packages written
834 \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
835 theorems produced in ML both in the theory context and the ML
836 toplevel, associating it with the provided name. Theorems are put
837 into a global ``standard'' format before being stored.
839 \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
846 section {* Primitive specification elements *}
848 subsection {* Type classes and sorts \label{sec:classes} *}
851 \begin{matharray}{rcll}
852 @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
853 @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
854 @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
855 @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
859 'classes' (classdecl +)
861 'classrel' (nameref ('<' | subseteq) nameref + 'and')
869 \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
870 @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
871 Isabelle implicitly maintains the transitive closure of the class
872 hierarchy. Cyclic class structures are not permitted.
874 \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
875 relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
876 This is done axiomatically! The @{command_ref "instance"} command
877 (see \secref{sec:axclass}) provides a way to introduce proven class
880 \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
881 new default sort for any type variable that is given explicitly in
882 the text, but lacks a sort constraint (wrt.\ the current context).
883 Type variables generated by type inference are not affected.
885 Usually the default sort is only changed when defining a new
886 object-logic. For example, the default sort in Isabelle/HOL is
887 @{text type}, the class of all HOL types. %FIXME sort antiq?
889 When merging theories, the default sorts of the parents are
890 logically intersected, i.e.\ the representations as lists of classes
893 \item @{command "class_deps"} visualizes the subclass relation,
894 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
900 subsection {* Types and type abbreviations \label{sec:types-pure} *}
903 \begin{matharray}{rcll}
904 @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
905 @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
906 @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
910 'types' (typespec '=' type infix? +)
912 'typedecl' typespec infix?
914 'arities' (nameref '::' arity +)
920 \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
921 \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
922 @{text "\<tau>"}. Unlike actual type definitions, as are available in
923 Isabelle/HOL for example, type synonyms are merely syntactic
924 abbreviations without any logical significance. Internally, type
925 synonyms are fully expanded.
927 \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
928 type constructor @{text t}. If the object-logic defines a base sort
929 @{text s}, then the constructor is declared to operate on that, via
930 the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
933 \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
934 Isabelle's order-sorted signature of types by new type constructor
935 arities. This is done axiomatically! The @{command_ref "instance"}
936 command (see \secref{sec:axclass}) provides a way to introduce
943 subsection {* Co-regularity of type classes and arities *}
945 text {* The class relation together with the collection of
946 type-constructor arities must obey the principle of
947 \emph{co-regularity} as defined below.
949 \medskip For the subsequent formulation of co-regularity we assume
950 that the class relation is closed by transitivity and reflexivity.
951 Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
952 completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
953 implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
955 Treating sorts as finite sets of classes (meaning the intersection),
956 the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
959 @{text "s\<^sub>1 \<subseteq> s\<^sub>2 \<equiv> \<forall>c\<^sub>2 \<in> s\<^sub>2. \<exists>c\<^sub>1 \<in> s\<^sub>1. c\<^sub>1 \<subseteq> c\<^sub>2"}
962 This relation on sorts is further extended to tuples of sorts (of
963 the same length) in the component-wise way.
965 \smallskip Co-regularity of the class relation together with the
966 arities relation means:
968 @{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2"}
970 \noindent for all such arities. In other words, whenever the result
971 classes of some type-constructor arities are related, then the
972 argument sorts need to be related in the same way.
974 \medskip Co-regularity is a very fundamental property of the
975 order-sorted algebra of types. For example, it entails principle
976 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
980 subsection {* Constants and definitions \label{sec:consts} *}
983 Definitions essentially express abbreviations within the logic. The
984 simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
985 c} is a newly declared constant. Isabelle also allows derived forms
986 where the arguments of @{text c} appear on the left, abbreviating a
987 prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
988 written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
989 definitions may be weakened by adding arbitrary pre-conditions:
990 @{text "A \<Longrightarrow> c x y \<equiv> t"}.
992 \medskip The built-in well-formedness conditions for definitional
997 \item Arguments (on the left-hand side) must be distinct variables.
999 \item All variables on the right-hand side must also appear on the
1002 \item All type variables on the right-hand side must also appear on
1003 the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
1004 \<alpha> list)"} for example.
1006 \item The definition must not be recursive. Most object-logics
1007 provide definitional principles that can be used to express
1012 Overloading means that a constant being declared as @{text "c :: \<alpha>
1013 decl"} may be defined separately on type instances @{text "c ::
1014 (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
1015 t}. The right-hand side may mention overloaded constants
1016 recursively at type instances corresponding to the immediate
1017 argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
1018 specification patterns impose global constraints on all occurrences,
1019 e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
1020 corresponding occurrences on some right-hand side need to be an
1021 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1023 \begin{matharray}{rcl}
1024 @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
1025 @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
1026 @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
1030 'consts' ((name '::' type mixfix?) +)
1032 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1037 'constdefs' structs? (constdecl? constdef +)
1040 structs: '(' 'structure' (vars + 'and') ')'
1042 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1044 constdef: thmdecl? prop
1050 \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
1051 c} to have any instance of type scheme @{text \<sigma>}. The optional
1052 mixfix annotations may attach concrete syntax to the constants
1055 \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
1056 as a definitional axiom for some existing constant.
1058 The @{text "(unchecked)"} option disables global dependency checks
1059 for this definition, which is occasionally useful for exotic
1060 overloading. It is at the discretion of the user to avoid malformed
1061 theory specifications!
1063 The @{text "(overloaded)"} option declares definitions to be
1064 potentially overloaded. Unless this option is given, a warning
1065 message would be issued for any definitional equation with a more
1066 special type than that of the corresponding constant declaration.
1068 \item @{command "constdefs"} combines constant declarations and
1069 definitions, with type-inference taking care of the most general
1070 typing of the given specification (the optional type constraint may
1071 refer to type-inference dummies ``@{text _}'' as usual). The
1072 resulting type declaration needs to agree with that of the
1073 specification; overloading is \emph{not} supported here!
1075 The constant name may be omitted altogether, if neither type nor
1076 syntax declarations are given. The canonical name of the
1077 definitional axiom for constant @{text c} will be @{text c_def},
1078 unless specified otherwise. Also note that the given list of
1079 specifications is processed in a strictly sequential manner, with
1080 type-checking being performed independently.
1082 An optional initial context of @{text "(structure)"} declarations
1083 admits use of indexed syntax, using the special symbol @{verbatim
1084 "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
1085 particularly useful with locales (see also \secref{sec:locale}).
1091 section {* Axioms and theorems \label{sec:axms-thms} *}
1094 \begin{matharray}{rcll}
1095 @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1096 @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1097 @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1101 'axioms' (axmdecl prop +)
1103 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1109 \item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary
1110 statements as axioms of the meta-logic. In fact, axioms are
1111 ``axiomatic theorems'', and may be referred later just as any other
1114 Axioms are usually only introduced when declaring new logical
1115 systems. Everyday work is typically done the hard way, with proper
1116 definitions and proven theorems.
1118 \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} retrieves and stores
1119 existing facts in the theory context, or the specified target
1120 context (see also \secref{sec:target}). Typical applications would
1121 also involve attributes, to declare Simplifier rules, for example.
1123 \item @{command "theorems"} is essentially the same as @{command
1124 "lemmas"}, but marks the result as a different kind of facts.
1130 section {* Oracles *}
1132 text {* Oracles allow Isabelle to take advantage of external reasoners
1133 such as arithmetic decision procedures, model checkers, fast
1134 tautology checkers or computer algebra systems. Invoked as an
1135 oracle, an external reasoner can create arbitrary Isabelle theorems.
1137 It is the responsibility of the user to ensure that the external
1138 reasoner is as trustworthy as the application requires. Another
1139 typical source of errors is the linkup between Isabelle and the
1140 external tool, not just its concrete implementation, but also the
1141 required translation between two different logical environments.
1143 Isabelle merely guarantees well-formedness of the propositions being
1144 asserted, and records within the internal derivation object how
1145 presumed theorems depend on unproven suppositions.
1147 \begin{matharray}{rcl}
1148 @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
1152 'oracle' name '=' text
1158 \item @{command "oracle"}~@{text "name = text"} turns the given ML
1159 expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
1160 ML function of type @{ML_text "'a -> thm"}, which is bound to the
1161 global identifier @{ML_text name}. This acts like an infinitary
1162 specification of axioms! Invoking the oracle only works within the
1163 scope of the resulting theory.
1167 See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
1168 defining a new primitive rule as oracle, and turning it into a proof
1173 section {* Name spaces *}
1176 \begin{matharray}{rcl}
1177 @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
1178 @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
1179 @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
1183 'hide' ('(open)')? name (nameref + )
1187 Isabelle organizes any kind of name declarations (of types,
1188 constants, theorems etc.) by separate hierarchically structured name
1189 spaces. Normally the user does not have to control the behavior of
1190 name spaces by hand, yet the following commands provide some way to
1195 \item @{command "global"} and @{command "local"} change the current
1196 name declaration mode. Initially, theories start in @{command
1197 "local"} mode, causing all names to be automatically qualified by
1198 the theory name. Changing this to @{command "global"} causes all
1199 names to be declared without the theory prefix, until @{command
1200 "local"} is declared again.
1202 Note that global names are prone to get hidden accidently later,
1203 when qualified names of the same base name are introduced.
1205 \item @{command "hide"}~@{text "space names"} fully removes
1206 declarations from a given name space (which may be @{text "class"},
1207 @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
1208 "(open)"} option, only the base name is hidden. Global
1209 (unqualified) names may never be hidden.
1211 Note that hiding name space accesses has no impact on logical
1212 declarations --- they remain valid internally. Entities that are no
1213 longer accessible to the user are printed with the special qualifier
1214 ``@{text "??"}'' prefixed to the full internal name.