5 chapter {* Theory specifications *}
8 The Isabelle/Isar theory format integrates specifications and
9 proofs, supporting interactive development with unlimited undo
10 operation. There is an integrated document preparation system (see
11 \chref{ch:document-prep}), for typesetting formal developments
12 together with informal text. The resulting hyper-linked PDF
13 documents can be used both for WWW presentation and printed copies.
15 The Isar proof language (see \chref{ch:proofs}) is embedded into the
16 theory language as a proper sub-language. Proof mode is entered by
17 stating some @{command theorem} or @{command lemma} at the theory
18 level, and left again with the final conclusion (e.g.\ via @{command
19 qed}). Some theory specification mechanisms also require a proof,
20 such as @{command typedef} in HOL, which demands non-emptiness of
21 the representing sets.
25 section {* Defining theories \label{sec:begin-thy} *}
28 \begin{matharray}{rcl}
29 @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
30 @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
33 Isabelle/Isar theories are defined via theory files, which may
34 contain both specifications and proofs; occasionally definitional
35 mechanisms also require some explicit proof. The theory body may be
36 sub-structured by means of \emph{local theory targets}, such as
37 @{command "locale"} and @{command "class"}.
39 The first proper command of a theory is @{command "theory"}, which
40 indicates imports of previous theories and optional dependencies on
41 other source files (usually in ML). Just preceding the initial
42 @{command "theory"} command there may be an optional @{command
43 "header"} declaration, which is only relevant to document
44 preparation: see also the other section markup commands in
47 A theory is concluded by a final @{command (global) "end"} command,
48 one that does not belong to a local theory target. No further
49 commands may follow such a global @{command (global) "end"},
50 although some user-interfaces might pretend that trailing input is
54 'theory' name 'imports' (name +) uses? 'begin'
57 uses: 'uses' ((name | parname) +);
62 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
63 starts a new theory @{text A} based on the merge of existing
64 theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
66 Due to the possibility to import more than one ancestor, the
67 resulting theory structure of an Isabelle session forms a directed
68 acyclic graph (DAG). Isabelle's theory loader ensures that the
69 sources contributing to the development graph are always up-to-date:
70 changed files are automatically reloaded whenever a theory header
71 specification is processed.
73 The optional @{keyword_def "uses"} specification declares additional
74 dependencies on extra files (usually ML sources). Files will be
75 loaded immediately (as ML), unless the name is parenthesized. The
76 latter case records a dependency that needs to be resolved later in
77 the text, usually via explicit @{command_ref "use"} for ML files;
78 other file formats require specific load commands defined by the
79 corresponding tools or packages.
81 \item @{command (global) "end"} concludes the current theory
82 definition. Note that local theory targets involve a local
83 @{command (local) "end"}, which is clear from the nesting.
89 section {* Local theory targets \label{sec:target} *}
92 A local theory target is a context managed separately within the
93 enclosing theory. Contexts may introduce parameters (fixed
94 variables) and assumptions (hypotheses). Definitions and theorems
95 depending on the context may be added incrementally later on. Named
96 contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
97 (cf.\ \secref{sec:class}); the name ``@{text "-"}'' signifies the
98 global theory context.
100 \begin{matharray}{rcll}
101 @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
102 @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
105 \indexouternonterm{target}
107 'context' name 'begin'
110 target: '(' 'in' name ')'
116 \item @{command "context"}~@{text "c \<BEGIN>"} recommences an
117 existing locale or class context @{text c}. Note that locale and
118 class definitions allow to include the @{keyword "begin"} keyword as
119 well, in order to continue the local theory immediately after the
120 initial specification.
122 \item @{command (local) "end"} concludes the current local theory
123 and continues the enclosing global theory. Note that a global
124 @{command (global) "end"} has a different meaning: it concludes the
125 theory itself (\secref{sec:begin-thy}).
127 \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
128 local theory command specifies an immediate target, e.g.\
129 ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
130 "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
131 global theory context; the current target context will be suspended
132 for this command only. Note that ``@{text "(\<IN> -)"}'' will
133 always produce a global result independently of the current target
138 The exact meaning of results produced within a local theory context
139 depends on the underlying target infrastructure (locale, type class
140 etc.). The general idea is as follows, considering a context named
141 @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
143 Definitions are exported by introducing a global version with
144 additional arguments; a syntactic abbreviation links the long form
145 with the abstract version of the target context. For example,
146 @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
147 level (for arbitrary @{text "?x"}), together with a local
148 abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
149 fixed parameter @{text x}).
151 Theorems are exported by discharging the assumptions and
152 generalizing the parameters of the context. For example, @{text "a:
153 B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
158 section {* Basic specification elements *}
161 \begin{matharray}{rcll}
162 @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
163 @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
164 @{attribute_def "defn"} & : & @{text attribute} \\
165 @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
166 @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
169 These specification mechanisms provide a slightly more abstract view
170 than the underlying primitives of @{command "consts"}, @{command
171 "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
172 \secref{sec:axms-thms}). In particular, type-inference is commonly
173 available, and result names need not be given.
176 'axiomatization' target? fixes? ('where' specs)?
178 'definition' target? (decl 'where')? thmdecl? prop
180 'abbreviation' target? mode? (decl 'where')? prop
183 fixes: ((name ('::' type)? mixfix? | vars) + 'and')
185 specs: (thmdecl? props + 'and')
187 decl: name ('::' type)? mixfix?
193 \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
194 introduces several constants simultaneously and states axiomatic
195 properties for these. The constants are marked as being specified
196 once and for all, which prevents additional specifications being
199 Note that axiomatic specifications are only appropriate when
200 declaring a new logical system; axiomatic specifications are
201 restricted to global theory contexts. Normal applications should
202 only use definitional mechanisms!
204 \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
205 internal definition @{text "c \<equiv> t"} according to the specification
206 given as @{text eq}, which is then turned into a proven fact. The
207 given proposition may deviate from internal meta-level equality
208 according to the rewrite rules declared as @{attribute defn} by the
209 object-logic. This usually covers object-level equality @{text "x =
210 y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
211 change the @{attribute defn} setup.
213 Definitions may be presented with explicit arguments on the LHS, as
214 well as additional conditions, e.g.\ @{text "f x y = t"} instead of
215 @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
216 unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
218 \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
219 syntactic constant which is associated with a certain term according
220 to the meta-level equality @{text eq}.
222 Abbreviations participate in the usual type-inference process, but
223 are expanded before the logic ever sees them. Pretty printing of
224 terms involves higher-order rewriting with rules stemming from
225 reverted abbreviations. This needs some care to avoid overlapping
226 or looping syntactic replacements!
228 The optional @{text mode} specification restricts output to a
229 particular print mode; using ``@{text input}'' here achieves the
230 effect of one-way abbreviations. The mode may also include an
231 ``@{keyword "output"}'' qualifier that affects the concrete syntax
232 declared for abbreviations, cf.\ @{command "syntax"} in
233 \secref{sec:syn-trans}.
235 \item @{command "print_abbrevs"} prints all constant abbreviations
236 of the current context.
242 section {* Generic declarations *}
245 Arbitrary operations on the background context may be wrapped-up as
246 generic declaration elements. Since the underlying concept of local
247 theories may be subject to later re-interpretation, there is an
248 additional dependency on a morphism that tells the difference of the
249 original declaration context wrt.\ the application context
250 encountered later on. A fact declaration is an important special
251 case: it consists of a theorem which is applied to the context by
252 means of an attribute.
254 \begin{matharray}{rcl}
255 @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
256 @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
260 'declaration' ('(pervasive)')? target? text
262 'declare' target? (thmrefs + 'and')
268 \item @{command "declaration"}~@{text d} adds the declaration
269 function @{text d} of ML type @{ML_type declaration}, to the current
270 local theory under construction. In later application contexts, the
271 function is transformed according to the morphisms being involved in
272 the interpretation hierarchy.
274 If the @{text "(pervasive)"} option is given, the corresponding
275 declaration is applied to all possible contexts involved, including
276 the global background theory.
278 \item @{command "declare"}~@{text thms} declares theorems to the
279 current local theory context. No theorem binding is involved here,
280 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
281 \secref{sec:axms-thms}), so @{command "declare"} only has the effect
282 of applying attributes as included in the theorem specification.
288 section {* Locales \label{sec:locale} *}
291 Locales are parametric named local contexts, consisting of a list of
292 declaration elements that are modeled after the Isar proof context
293 commands (cf.\ \secref{sec:proof-context}).
297 subsection {* Locale expressions \label{sec:locale-expr} *}
300 A \emph{locale expression} denotes a structured context composed of
301 instances of existing locales. The context consists of a list of
302 instances of declaration elements from the locales. Two locale
303 instances are equal if they are of the same locale and the
304 parameters are instantiated with equivalent terms. Declaration
305 elements from equal instances are never repeated, thus avoiding
306 duplicate declarations.
308 \indexouternonterm{localeexpr}
310 localeexpr: (instance + '+') ('for' (fixes + 'and'))?
312 instance: (qualifier ':')? nameref (posinsts | namedinsts)
314 qualifier: name ('?' | '!')?
316 posinsts: (term | '_')*
318 namedinsts: 'where' (name '=' term + 'and')
322 A locale instance consists of a reference to a locale and either
323 positional or named parameter instantiations. Identical
324 instantiations (that is, those that instante a parameter by itself)
325 may be omitted. The notation `\_' enables to omit the instantiation
326 for a parameter inside a positional instantiation.
328 Terms in instantiations are from the context the locale expressions
329 is declared in. Local names may be added to this context with the
330 optional for clause. In addition, syntax declarations from one
331 instance are effective when parsing subsequent instances of the same
334 Instances have an optional qualifier which applies to names in
335 declarations. Names include local definitions and theorem names.
336 If present, the qualifier itself is either optional
337 (``\texttt{?}''), which means that it may be omitted on input of the
338 qualified name, or mandatory (``\texttt{!}''). If neither
339 ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
340 is used. For @{command "interpretation"} and @{command "interpret"}
341 the default is ``mandatory'', for @{command "locale"} and @{command
342 "sublocale"} the default is ``optional''.
346 subsection {* Locale declarations *}
349 \begin{matharray}{rcl}
350 @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
351 @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
352 @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
353 @{method_def intro_locales} & : & @{text method} \\
354 @{method_def unfold_locales} & : & @{text method} \\
357 \indexouternonterm{contextelem}
358 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
359 \indexisarelem{defines}\indexisarelem{notes}
361 'locale' name ('=' locale)? 'begin'?
363 'print\_locale' '!'? nameref
365 locale: contextelem+ | localeexpr ('+' (contextelem+))?
368 'fixes' (fixes + 'and')
369 | 'constrains' (name '::' type + 'and')
370 | 'assumes' (props + 'and')
371 | 'defines' (thmdecl? prop proppat? + 'and')
372 | 'notes' (thmdef? thmrefs + 'and')
378 \item @{command "locale"}~@{text "loc = import + body"} defines a
379 new locale @{text loc} as a context consisting of a certain view of
380 existing locales (@{text import}) plus some additional elements
381 (@{text body}). Both @{text import} and @{text body} are optional;
382 the degenerate form @{command "locale"}~@{text loc} defines an empty
383 locale, which may still be useful to collect declarations of facts
384 later on. Type-inference on locale expressions automatically takes
385 care of the most general typing that the combined context elements
388 The @{text import} consists of a structured locale expression; see
389 \secref{sec:proof-context} above. Its for clause defines the local
390 parameters of the @{text import}. In addition, locale parameters
391 whose instantance is omitted automatically extend the (possibly
392 empty) for clause: they are inserted at its beginning. This means
393 that these parameters may be referred to from within the expression
394 and also in the subsequent context elements and provides a
395 notational convenience for the inheritance of parameters in locale
398 The @{text body} consists of context elements.
402 \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
403 parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
404 are optional). The special syntax declaration ``@{text
405 "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
406 implicitly in this context.
408 \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
409 constraint @{text \<tau>} on the local parameter @{text x}. This
410 element is deprecated. The type constraint should be introduced in
411 the for clause or the relevant @{element "fixes"} element.
413 \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
414 introduces local premises, similar to @{command "assume"} within a
415 proof (cf.\ \secref{sec:proof-context}).
417 \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
418 declared parameter. This is similar to @{command "def"} within a
419 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
420 takes an equational proposition instead of variable-term pair. The
421 left-hand side of the equation may have additional arguments, e.g.\
422 ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
424 \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
425 reconsiders facts within a local context. Most notably, this may
426 include arbitrary declarations in any attribute specifications
427 included here, e.g.\ a local @{attribute simp} rule.
429 The initial @{text import} specification of a locale expression
430 maintains a dynamic relation to the locales being referenced
431 (benefiting from any later fact declarations in the obvious manner).
435 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
436 in the syntax of @{element "assumes"} and @{element "defines"} above
437 are illegal in locale definitions. In the long goal format of
438 \secref{sec:goals}, term bindings may be included as expected,
441 \medskip Locale specifications are ``closed up'' by
442 turning the given text into a predicate definition @{text
443 loc_axioms} and deriving the original assumptions as local lemmas
444 (modulo local definitions). The predicate statement covers only the
445 newly specified assumptions, omitting the content of included locale
446 expressions. The full cumulative view is only provided on export,
447 involving another predicate @{text loc} that refers to the complete
450 In any case, the predicate arguments are those locale parameters
451 that actually occur in the respective piece of text. Also note that
452 these predicates operate at the meta-level in theory, but the locale
453 packages attempts to internalize statements according to the
454 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
455 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
456 \secref{sec:object-logic}). Separate introduction rules @{text
457 loc_axioms.intro} and @{text loc.intro} are provided as well.
459 \item @{command "print_locale"}~@{text "locale"} prints the
460 contents of the named locale. The command omits @{element "notes"}
461 elements by default. Use @{command "print_locale"}@{text "!"} to
464 \item @{command "print_locales"} prints the names of all locales
465 of the current theory.
467 \item @{method intro_locales} and @{method unfold_locales}
468 repeatedly expand all introduction rules of locale predicates of the
469 theory. While @{method intro_locales} only applies the @{text
470 loc.intro} introduction rules and therefore does not decend to
471 assumptions, @{method unfold_locales} is more aggressive and applies
472 @{text loc_axioms.intro} as well. Both methods are aware of locale
473 specifications entailed by the context, both from target statements,
474 and from interpretations (see below). New goals that are entailed
475 by the current context are discharged automatically.
481 subsection {* Locale interpretations *}
484 Locale expressions may be instantiated, and the instantiated facts
485 added to the current context. This requires a proof of the
486 instantiated specification and is called \emph{locale
487 interpretation}. Interpretation is possible in locales @{command
488 "sublocale"}, theories (command @{command "interpretation"}) and
489 also within a proof body (command @{command "interpret"}).
491 \begin{matharray}{rcl}
492 @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
493 @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
494 @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
495 @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
498 \indexouternonterm{interp}
500 'sublocale' nameref ('<' | subseteq) localeexpr
502 'interpretation' localeepxr equations?
504 'interpret' localeexpr equations?
506 'print\_interps' nameref
508 equations: 'where' (thmdecl? prop + 'and')
514 \item @{command "sublocale"}~@{text "name \<subseteq> expr"}
515 interprets @{text expr} in the locale @{text name}. A proof that
516 the specification of @{text name} implies the specification of
517 @{text expr} is required. As in the localized version of the
518 theorem command, the proof is in the context of @{text name}. After
519 the proof obligation has been dischared, the facts of @{text expr}
520 become part of locale @{text name} as \emph{derived} context
521 elements and are available when the context @{text name} is
522 subsequently entered. Note that, like import, this is dynamic:
523 facts added to a locale part of @{text expr} after interpretation
524 become also available in @{text name}.
526 Only specification fragments of @{text expr} that are not already
527 part of @{text name} (be it imported, derived or a derived fragment
528 of the import) are considered in this process. This enables
529 circular interpretations to the extent that no infinite chains are
530 generated in the locale hierarchy.
532 If interpretations of @{text name} exist in the current theory, the
533 command adds interpretations for @{text expr} as well, with the same
534 qualifier, although only for fragments of @{text expr} that are not
535 interpreted in the theory already.
537 \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
538 interprets @{text expr} in the theory. The command generates proof
539 obligations for the instantiated specifications (assumes and defines
540 elements). Once these are discharged by the user, instantiated
541 facts are added to the theory in a post-processing phase.
543 Additional equations, which are unfolded during
544 post-processing, may be given after the keyword @{keyword "where"}.
545 This is useful for interpreting concepts introduced through
546 definition specification elements. The equations must be proved.
548 The command is aware of interpretations already active in the
549 theory, but does not simplify the goal automatically. In order to
550 simplify the proof obligations use methods @{method intro_locales}
551 or @{method unfold_locales}. Post-processing is not applied to
552 facts of interpretations that are already active. This avoids
553 duplication of interpreted facts, in particular. Note that, in the
554 case of a locale with import, parts of the interpretation may
555 already be active. The command will only process facts for new
558 Adding facts to locales has the effect of adding interpreted facts
559 to the theory for all active interpretations also. That is,
560 interpretations dynamically participate in any facts added to
563 \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
564 @{text expr} in the proof context and is otherwise similar to
565 interpretation in theories. Note that rewrite rules given to
566 @{command "interpret"} should be explicitly universally quantified.
568 \item @{command "print_interps"}~@{text "locale"} lists all
569 interpretations of @{text "locale"} in the current theory or proof
570 context, including those due to a combination of a @{command
571 "interpretation"} or @{command "interpret"} and one or several
572 @{command "sublocale"} declarations.
577 Since attributes are applied to interpreted theorems,
578 interpretation may modify the context of common proof tools, e.g.\
579 the Simplifier or Classical Reasoner. As the behavior of such
580 tools is \emph{not} stable under interpretation morphisms, manual
581 declarations might have to be added to the target context of the
582 interpretation to revert such declarations.
586 An interpretation in a theory or proof context may subsume previous
587 interpretations. This happens if the same specification fragment
588 is interpreted twice and the instantiation of the second
589 interpretation is more general than the interpretation of the
590 first. The locale package does not attempt to remove subsumed
596 section {* Classes \label{sec:class} *}
599 A class is a particular locale with \emph{exactly one} type variable
600 @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
601 is established which is interpreted logically as axiomatic type
602 class \cite{Wenzel:1997:TPHOL} whose logical content are the
603 assumptions of the locale. Thus, classes provide the full
604 generality of locales combined with the commodity of type classes
605 (notably type-inference). See \cite{isabelle-classes} for a short
608 \begin{matharray}{rcl}
609 @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
610 @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
611 @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
612 @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
613 @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
614 @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
615 @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
616 @{method_def intro_classes} & : & @{text method} \\
620 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
623 'instantiation' (nameref + 'and') '::' arity 'begin'
627 'instance' (nameref + 'and') '::' arity
629 'subclass' target? nameref
631 'instance' nameref ('<' | subseteq) nameref
638 superclassexpr: nameref | (nameref '+' superclassexpr)
644 \item @{command "class"}~@{text "c = superclasses + body"} defines
645 a new class @{text c}, inheriting from @{text superclasses}. This
646 introduces a locale @{text c} with import of all locales @{text
649 Any @{element "fixes"} in @{text body} are lifted to the global
650 theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
651 f\<^sub>n"} of class @{text c}), mapping the local type parameter
652 @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
654 Likewise, @{element "assumes"} in @{text body} are also lifted,
655 mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
656 corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
657 corresponding introduction rule is provided as @{text
658 c_class_axioms.intro}. This rule should be rarely needed directly
659 --- the @{method intro_classes} method takes care of the details of
660 class membership proofs.
662 \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
663 \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
664 allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
665 to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
666 \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the
667 target body poses a goal stating these type arities. The target is
668 concluded by an @{command_ref (local) "end"} command.
670 Note that a list of simultaneous type constructors may be given;
671 this corresponds nicely to mutually recursive type definitions, e.g.\
674 \item @{command "instance"} in an instantiation target body sets
675 up a goal stating the type arities claimed at the opening @{command
676 "instantiation"}. The proof would usually proceed by @{method
677 intro_classes}, and then establish the characteristic theorems of
678 the type classes involved. After finishing the proof, the
679 background theory will be augmented by the proven type arities.
681 On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
682 s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
683 need to specify operations: one can continue with the
684 instantiation proof immediately.
686 \item @{command "subclass"}~@{text c} in a class context for class
687 @{text d} sets up a goal stating that class @{text c} is logically
688 contained in class @{text d}. After finishing the proof, class
689 @{text d} is proven to be subclass @{text c} and the locale @{text
690 c} is interpreted into @{text d} simultaneously.
692 A weakend form of this is available through a further variant of
693 @{command instance}: @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
694 a proof that class @{text "c\<^isub>2"} implies @{text "c\<^isub>1"} without reference
695 to the underlying locales; this is useful if the properties to prove
696 the logical connection are not sufficent on the locale level but on
699 \item @{command "print_classes"} prints all classes in the current
702 \item @{command "class_deps"} visualizes all classes and their
703 subclass relations as a Hasse diagram.
705 \item @{method intro_classes} repeatedly expands all class
706 introduction rules of this theory. Note that this method usually
707 needs not be named explicitly, as it is already included in the
708 default proof step (e.g.\ of @{command "proof"}). In particular,
709 instantiation of trivial (syntactic) classes may be performed by a
710 single ``@{command ".."}'' proof step.
716 subsection {* The class target *}
721 A named context may refer to a locale (cf.\ \secref{sec:target}).
722 If this locale is also a class @{text c}, apart from the common
723 locale target behaviour the following happens.
727 \item Local constant declarations @{text "g[\<alpha>]"} referring to the
728 local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
729 are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
730 referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
732 \item Local theorem bindings are lifted as are assumptions.
734 \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
735 global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
736 resolves ambiguities. In rare cases, manual type annotations are
743 subsection {* Co-regularity of type classes and arities *}
745 text {* The class relation together with the collection of
746 type-constructor arities must obey the principle of
747 \emph{co-regularity} as defined below.
749 \medskip For the subsequent formulation of co-regularity we assume
750 that the class relation is closed by transitivity and reflexivity.
751 Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
752 completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
753 implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
755 Treating sorts as finite sets of classes (meaning the intersection),
756 the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
759 @{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"}
762 This relation on sorts is further extended to tuples of sorts (of
763 the same length) in the component-wise way.
765 \smallskip Co-regularity of the class relation together with the
766 arities relation means:
768 @{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"}
770 \noindent for all such arities. In other words, whenever the result
771 classes of some type-constructor arities are related, then the
772 argument sorts need to be related in the same way.
774 \medskip Co-regularity is a very fundamental property of the
775 order-sorted algebra of types. For example, it entails principle
776 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
780 section {* Unrestricted overloading *}
783 Isabelle/Pure's definitional schemes support certain forms of
784 overloading (see \secref{sec:consts}). Overloading means that a
785 constant being declared as @{text "c :: \<alpha> decl"} may be
786 defined separately on type instances
787 @{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
788 for each type constructor @{text t}. At most occassions
789 overloading will be used in a Haskell-like fashion together with
790 type classes by means of @{command "instantiation"} (see
791 \secref{sec:class}). Sometimes low-level overloading is desirable.
792 The @{command "overloading"} target provides a convenient view for
795 \begin{matharray}{rcl}
796 @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
801 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
806 \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>"}
807 opens a theory target (cf.\ \secref{sec:target}) which allows to
808 specify constants with overloaded definitions. These are identified
809 by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
810 constants @{text "c\<^sub>i"} at particular type instances. The
811 definitions themselves are established using common specification
812 tools, using the names @{text "x\<^sub>i"} as reference to the
813 corresponding constants. The target is concluded by @{command
816 A @{text "(unchecked)"} option disables global dependency checks for
817 the corresponding definition, which is occasionally useful for
818 exotic overloading (see \secref{sec:consts} for a precise description).
819 It is at the discretion of the user to avoid
820 malformed theory specifications!
826 section {* Incorporating ML code \label{sec:ML} *}
829 \begin{matharray}{rcl}
830 @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
831 @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
832 @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
833 @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
834 @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
835 @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
836 @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
837 @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
841 @{index_ML bind_thms: "string * thm list -> unit"} \\
842 @{index_ML bind_thm: "string * thm -> unit"} \\
848 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
850 'attribute\_setup' name '=' text text
856 \item @{command "use"}~@{text "file"} reads and executes ML
857 commands from @{text "file"}. The current theory context is passed
858 down to the ML toplevel and may be modified, using @{ML
859 "Context.>>"} or derived ML commands. The file name is checked with
860 the @{keyword_ref "uses"} dependency declaration given in the theory
861 header (see also \secref{sec:begin-thy}).
863 Top-level ML bindings are stored within the (global or local) theory
866 \item @{command "ML"}~@{text "text"} is similar to @{command "use"},
867 but executes ML commands directly from the given @{text "text"}.
868 Top-level ML bindings are stored within the (global or local) theory
871 \item @{command "ML_prf"} is analogous to @{command "ML"} but works
872 within a proof context.
874 Top-level ML bindings are stored within the proof context in a
875 purely sequential fashion, disregarding the nested proof structure.
876 ML bindings introduced by @{command "ML_prf"} are discarded at the
879 \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
880 versions of @{command "ML"}, which means that the context may not be
881 updated. @{command "ML_val"} echos the bindings produced at the ML
882 toplevel, but @{command "ML_command"} is silent.
884 \item @{command "setup"}~@{text "text"} changes the current theory
885 context by applying @{text "text"}, which refers to an ML expression
886 of type @{ML_type "theory -> theory"}. This enables to initialize
887 any object-logic specific tools and packages written in ML, for
890 \item @{command "local_setup"} is similar to @{command "setup"} for
891 a local theory context, and an ML expression of type @{ML_type
892 "local_theory -> local_theory"}. This allows to
893 invoke local theory specification packages without going through
894 concrete outer syntax, for example.
896 \item @{command "attribute_setup"}~@{text "name = text description"}
897 defines an attribute in the current theory. The given @{text
898 "text"} has to be an ML expression of type
899 @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
900 structure @{ML_struct Args} and @{ML_struct Attrib}.
902 In principle, attributes can operate both on a given theorem and the
903 implicit context, although in practice only one is modified and the
904 other serves as parameter. Here are examples for these two cases:
909 attribute_setup my_rule = {*
910 Attrib.thms >> (fn ths =>
911 Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
912 let val th' = th OF ths
913 in th' end)) *} "my rule"
915 attribute_setup my_declaration = {*
916 Attrib.thms >> (fn ths =>
917 Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
918 let val context' = context
919 in context' end)) *} "my declaration"
924 \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
925 theorems produced in ML both in the theory context and the ML
926 toplevel, associating it with the provided name. Theorems are put
927 into a global ``standard'' format before being stored.
929 \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
936 section {* Primitive specification elements *}
938 subsection {* Type classes and sorts \label{sec:classes} *}
941 \begin{matharray}{rcll}
942 @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
943 @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
944 @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
948 'classes' (classdecl +)
950 'classrel' (nameref ('<' | subseteq) nameref + 'and')
958 \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
959 @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
960 Isabelle implicitly maintains the transitive closure of the class
961 hierarchy. Cyclic class structures are not permitted.
963 \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
964 relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
965 This is done axiomatically! The @{command_ref "subclass"} and
966 @{command_ref "instance"} commands (see \secref{sec:class}) provide
967 a way to introduce proven class relations.
969 \item @{command "default_sort"}~@{text s} makes sort @{text s} the
970 new default sort for any type variable that is given explicitly in
971 the text, but lacks a sort constraint (wrt.\ the current context).
972 Type variables generated by type inference are not affected.
974 Usually the default sort is only changed when defining a new
975 object-logic. For example, the default sort in Isabelle/HOL is
976 @{text type}, the class of all HOL types. %FIXME sort antiq?
978 When merging theories, the default sorts of the parents are
979 logically intersected, i.e.\ the representations as lists of classes
986 subsection {* Types and type abbreviations \label{sec:types-pure} *}
989 \begin{matharray}{rcll}
990 @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
991 @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
992 @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
996 'types' (typespec '=' type mixfix? +)
998 'typedecl' typespec mixfix?
1000 'arities' (nameref '::' arity +)
1006 \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
1007 \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
1008 @{text "\<tau>"}. Unlike actual type definitions, as are available in
1009 Isabelle/HOL for example, type synonyms are merely syntactic
1010 abbreviations without any logical significance. Internally, type
1011 synonyms are fully expanded.
1013 \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
1014 type constructor @{text t}. If the object-logic defines a base sort
1015 @{text s}, then the constructor is declared to operate on that, via
1016 the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
1019 \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
1020 Isabelle's order-sorted signature of types by new type constructor
1021 arities. This is done axiomatically! The @{command_ref "instantiation"}
1022 target (see \secref{sec:class}) provides a way to introduce
1023 proven type arities.
1029 subsection {* Constants and definitions \label{sec:consts} *}
1032 Definitions essentially express abbreviations within the logic. The
1033 simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
1034 c} is a newly declared constant. Isabelle also allows derived forms
1035 where the arguments of @{text c} appear on the left, abbreviating a
1036 prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
1037 written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
1038 definitions may be weakened by adding arbitrary pre-conditions:
1039 @{text "A \<Longrightarrow> c x y \<equiv> t"}.
1041 \medskip The built-in well-formedness conditions for definitional
1046 \item Arguments (on the left-hand side) must be distinct variables.
1048 \item All variables on the right-hand side must also appear on the
1051 \item All type variables on the right-hand side must also appear on
1052 the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
1053 \<alpha> list)"} for example.
1055 \item The definition must not be recursive. Most object-logics
1056 provide definitional principles that can be used to express
1061 The right-hand side of overloaded definitions may mention overloaded constants
1062 recursively at type instances corresponding to the immediate
1063 argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
1064 specification patterns impose global constraints on all occurrences,
1065 e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
1066 corresponding occurrences on some right-hand side need to be an
1067 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1069 \begin{matharray}{rcl}
1070 @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
1071 @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
1075 'consts' ((name '::' type mixfix?) +)
1077 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1083 \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
1084 c} to have any instance of type scheme @{text \<sigma>}. The optional
1085 mixfix annotations may attach concrete syntax to the constants
1088 \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
1089 as a definitional axiom for some existing constant.
1091 The @{text "(unchecked)"} option disables global dependency checks
1092 for this definition, which is occasionally useful for exotic
1093 overloading. It is at the discretion of the user to avoid malformed
1094 theory specifications!
1096 The @{text "(overloaded)"} option declares definitions to be
1097 potentially overloaded. Unless this option is given, a warning
1098 message would be issued for any definitional equation with a more
1099 special type than that of the corresponding constant declaration.
1105 section {* Axioms and theorems \label{sec:axms-thms} *}
1108 \begin{matharray}{rcll}
1109 @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1110 @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1111 @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1115 'axioms' (axmdecl prop +)
1117 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1123 \item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary
1124 statements as axioms of the meta-logic. In fact, axioms are
1125 ``axiomatic theorems'', and may be referred later just as any other
1128 Axioms are usually only introduced when declaring new logical
1129 systems. Everyday work is typically done the hard way, with proper
1130 definitions and proven theorems.
1132 \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} retrieves and stores
1133 existing facts in the theory context, or the specified target
1134 context (see also \secref{sec:target}). Typical applications would
1135 also involve attributes, to declare Simplifier rules, for example.
1137 \item @{command "theorems"} is essentially the same as @{command
1138 "lemmas"}, but marks the result as a different kind of facts.
1144 section {* Oracles *}
1146 text {* Oracles allow Isabelle to take advantage of external reasoners
1147 such as arithmetic decision procedures, model checkers, fast
1148 tautology checkers or computer algebra systems. Invoked as an
1149 oracle, an external reasoner can create arbitrary Isabelle theorems.
1151 It is the responsibility of the user to ensure that the external
1152 reasoner is as trustworthy as the application requires. Another
1153 typical source of errors is the linkup between Isabelle and the
1154 external tool, not just its concrete implementation, but also the
1155 required translation between two different logical environments.
1157 Isabelle merely guarantees well-formedness of the propositions being
1158 asserted, and records within the internal derivation object how
1159 presumed theorems depend on unproven suppositions.
1161 \begin{matharray}{rcl}
1162 @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
1166 'oracle' name '=' text
1172 \item @{command "oracle"}~@{text "name = text"} turns the given ML
1173 expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
1174 ML function of type @{ML_text "'a -> thm"}, which is bound to the
1175 global identifier @{ML_text name}. This acts like an infinitary
1176 specification of axioms! Invoking the oracle only works within the
1177 scope of the resulting theory.
1181 See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
1182 defining a new primitive rule as oracle, and turning it into a proof
1187 section {* Name spaces *}
1190 \begin{matharray}{rcl}
1191 @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
1192 @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
1193 @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
1194 @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
1198 ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
1202 Isabelle organizes any kind of name declarations (of types,
1203 constants, theorems etc.) by separate hierarchically structured name
1204 spaces. Normally the user does not have to control the behavior of
1205 name spaces by hand, yet the following commands provide some way to
1210 \item @{command "hide_class"}~@{text names} fully removes class
1211 declarations from a given name space; with the @{text "(open)"}
1212 option, only the base name is hidden. Global (unqualified) names
1213 may never be hidden.
1215 Note that hiding name space accesses has no impact on logical
1216 declarations --- they remain valid internally. Entities that are no
1217 longer accessible to the user are printed with the special qualifier
1218 ``@{text "??"}'' prefixed to the full internal name.
1220 \item @{command "hide_type"}, @{command "hide_const"}, and @{command
1221 "hide_fact"} are similar to @{command "hide_class"}, but hide types,
1222 constants, and facts, respectively.