Merge.
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' 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 \item @{command "declare"}~@{text thms} declares theorems to the
275 current local theory context. No theorem binding is involved here,
276 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
277 \secref{sec:axms-thms}), so @{command "declare"} only has the effect
278 of applying attributes as included in the theorem specification.
284 section {* Locales \label{sec:locale} *}
287 Locales are named local contexts, consisting of a list of
288 declaration elements that are modeled after the Isar proof context
289 commands (cf.\ \secref{sec:proof-context}).
293 subsection {* Locale specifications *}
296 \begin{matharray}{rcl}
297 @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
298 @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
299 @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
300 @{method_def intro_locales} & : & @{text method} \\
301 @{method_def unfold_locales} & : & @{text method} \\
304 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
305 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
306 \indexisarelem{defines}\indexisarelem{notes}
308 'locale' name ('=' localeexpr)? 'begin'?
310 'print\_locale' '!'? localeexpr
312 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
315 contextexpr: nameref | '(' contextexpr ')' |
316 (contextexpr (name mixfix? +)) | (contextexpr + '+')
318 contextelem: fixes | constrains | assumes | defines | notes
320 fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
322 constrains: 'constrains' (name '::' type + 'and')
324 assumes: 'assumes' (thmdecl? props + 'and')
326 defines: 'defines' (thmdecl? prop proppat? + 'and')
328 notes: 'notes' (thmdef? thmrefs + 'and')
334 \item @{command "locale"}~@{text "loc = import + body"} defines a
335 new locale @{text loc} as a context consisting of a certain view of
336 existing locales (@{text import}) plus some additional elements
337 (@{text body}). Both @{text import} and @{text body} are optional;
338 the degenerate form @{command "locale"}~@{text loc} defines an empty
339 locale, which may still be useful to collect declarations of facts
340 later on. Type-inference on locale expressions automatically takes
341 care of the most general typing that the combined context elements
344 The @{text import} consists of a structured context expression,
345 consisting of references to existing locales, renamed contexts, or
346 merged contexts. Renaming uses positional notation: @{text "c
347 x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed
348 parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>,
349 x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that
350 position. Renaming by default deletes concrete syntax, but new
351 syntax may by specified with a mixfix annotation. An exeption of
352 this rule is the special syntax declared with ``@{text
353 "(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it
354 be changed. Merging proceeds from left-to-right, suppressing any
355 duplicates stemming from different paths through the import
358 The @{text body} consists of basic context elements, further context
359 expressions may be included as well.
363 \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
364 parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
365 are optional). The special syntax declaration ``@{text
366 "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
367 implicitly in this context.
369 \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
370 constraint @{text \<tau>} on the local parameter @{text x}.
372 \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
373 introduces local premises, similar to @{command "assume"} within a
374 proof (cf.\ \secref{sec:proof-context}).
376 \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
377 declared parameter. This is similar to @{command "def"} within a
378 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
379 takes an equational proposition instead of variable-term pair. The
380 left-hand side of the equation may have additional arguments, e.g.\
381 ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
383 \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
384 reconsiders facts within a local context. Most notably, this may
385 include arbitrary declarations in any attribute specifications
386 included here, e.g.\ a local @{attribute simp} rule.
388 The initial @{text import} specification of a locale expression
389 maintains a dynamic relation to the locales being referenced
390 (benefiting from any later fact declarations in the obvious manner).
394 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
395 in the syntax of @{element "assumes"} and @{element "defines"} above
396 are illegal in locale definitions. In the long goal format of
397 \secref{sec:goals}, term bindings may be included as expected,
400 \medskip By default, locale specifications are ``closed up'' by
401 turning the given text into a predicate definition @{text
402 loc_axioms} and deriving the original assumptions as local lemmas
403 (modulo local definitions). The predicate statement covers only the
404 newly specified assumptions, omitting the content of included locale
405 expressions. The full cumulative view is only provided on export,
406 involving another predicate @{text loc} that refers to the complete
409 In any case, the predicate arguments are those locale parameters
410 that actually occur in the respective piece of text. Also note that
411 these predicates operate at the meta-level in theory, but the locale
412 packages attempts to internalize statements according to the
413 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
414 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
415 \secref{sec:object-logic}). Separate introduction rules @{text
416 loc_axioms.intro} and @{text loc.intro} are provided as well.
418 \item @{command "print_locale"}~@{text "import + body"} prints the
419 specified locale expression in a flattened form. The notable
420 special case @{command "print_locale"}~@{text loc} just prints the
421 contents of the named locale, but keep in mind that type-inference
422 will normalize type variables according to the usual alphabetical
423 order. The command omits @{element "notes"} elements by default.
424 Use @{command "print_locale"}@{text "!"} to get them included.
426 \item @{command "print_locales"} prints the names of all locales
427 of the current theory.
429 \item @{method intro_locales} and @{method unfold_locales}
430 repeatedly expand all introduction rules of locale predicates of the
431 theory. While @{method intro_locales} only applies the @{text
432 loc.intro} introduction rules and therefore does not decend to
433 assumptions, @{method unfold_locales} is more aggressive and applies
434 @{text loc_axioms.intro} as well. Both methods are aware of locale
435 specifications entailed by the context, both from target statements,
436 and from interpretations (see below). New goals that are entailed
437 by the current context are discharged automatically.
443 subsection {* Interpretation of locales *}
446 Locale expressions (more precisely, \emph{context expressions}) may
447 be instantiated, and the instantiated facts added to the current
448 context. This requires a proof of the instantiated specification
449 and is called \emph{locale interpretation}. Interpretation is
450 possible in theories and locales (command @{command
451 "interpretation"}) and also within a proof body (command @{command
454 \begin{matharray}{rcl}
455 @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
456 @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
459 \indexouternonterm{interp}
461 'interpretation' (interp | name ('<' | subseteq) contextexpr)
465 instantiation: ('[' (inst+) ']')?
467 interp: (name ':')? \\ (contextexpr instantiation |
468 name instantiation 'where' (thmdecl? prop + 'and'))
474 \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
476 The first form of @{command "interpretation"} interprets @{text
477 expr} in the theory. The instantiation is given as a list of terms
478 @{text insts} and is positional. All parameters must receive an
479 instantiation term --- with the exception of defined parameters.
480 These are, if omitted, derived from the defining equation and other
481 instantiations. Use ``@{text _}'' to omit an instantiation term.
483 The command generates proof obligations for the instantiated
484 specifications (assumes and defines elements). Once these are
485 discharged by the user, instantiated facts are added to the theory
486 in a post-processing phase.
488 Additional equations, which are unfolded in facts during
489 post-processing, may be given after the keyword @{keyword "where"}.
490 This is useful for interpreting concepts introduced through
491 definition specification elements. The equations must be proved.
492 Note that if equations are present, the context expression is
493 restricted to a locale name.
495 The command is aware of interpretations already active in the
496 theory, but does not simplify the goal automatically. In order to
497 simplify the proof obligations use methods @{method intro_locales}
498 or @{method unfold_locales}. Post-processing is not applied to
499 facts of interpretations that are already active. This avoids
500 duplication of interpreted facts, in particular. Note that, in the
501 case of a locale with import, parts of the interpretation may
502 already be active. The command will only process facts for new
505 The context expression may be preceded by a name, which takes effect
506 in the post-processing of facts. It is used to prefix fact names,
507 for example to avoid accidental hiding of other facts.
509 Adding facts to locales has the effect of adding interpreted facts
510 to the theory for all active interpretations also. That is,
511 interpretations dynamically participate in any facts added to
514 \item @{command "interpretation"}~@{text "name \<subseteq> expr"}
516 This form of the command interprets @{text expr} in the locale
517 @{text name}. It requires a proof that the specification of @{text
518 name} implies the specification of @{text expr}. As in the
519 localized version of the theorem command, the proof is in the
520 context of @{text name}. After the proof obligation has been
521 dischared, the facts of @{text expr} become part of locale @{text
522 name} as \emph{derived} context elements and are available when the
523 context @{text name} is subsequently entered. Note that, like
524 import, this is dynamic: facts added to a locale part of @{text
525 expr} after interpretation become also available in @{text name}.
526 Like facts of renamed context elements, facts obtained by
527 interpretation may be accessed by prefixing with the parameter
528 renaming (where the parameters are separated by ``@{text _}'').
530 Unlike interpretation in theories, instantiation is confined to the
531 renaming of parameters, which may be specified as part of the
532 context expression @{text expr}. Using defined parameters in @{text
533 name} one may achieve an effect similar to instantiation, though.
535 Only specification fragments of @{text expr} that are not already
536 part of @{text name} (be it imported, derived or a derived fragment
537 of the import) are considered by interpretation. This enables
538 circular interpretations.
540 If interpretations of @{text name} exist in the current theory, the
541 command adds interpretations for @{text expr} as well, with the same
542 prefix and attributes, although only for fragments of @{text expr}
543 that are not interpreted in the theory already.
545 \item @{command "interpret"}~@{text "expr insts \<WHERE> eqns"}
546 interprets @{text expr} in the proof context and is otherwise
547 similar to interpretation in theories.
552 Since attributes are applied to interpreted theorems,
553 interpretation may modify the context of common proof tools, e.g.\
554 the Simplifier or Classical Reasoner. Since the behavior of such
555 automated reasoning tools is \emph{not} stable under
556 interpretation morphisms, manual declarations might have to be
561 An interpretation in a theory may subsume previous
562 interpretations. This happens if the same specification fragment
563 is interpreted twice and the instantiation of the second
564 interpretation is more general than the interpretation of the
565 first. A warning is issued, since it is likely that these could
566 have been generalized in the first place. The locale package does
567 not attempt to remove subsumed interpretations.
572 section {* Classes \label{sec:class} *}
575 A class is a particular locale with \emph{exactly one} type variable
576 @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
577 is established which is interpreted logically as axiomatic type
578 class \cite{Wenzel:1997:TPHOL} whose logical content are the
579 assumptions of the locale. Thus, classes provide the full
580 generality of locales combined with the commodity of type classes
581 (notably type-inference). See \cite{isabelle-classes} for a short
584 \begin{matharray}{rcl}
585 @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
586 @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
587 @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
588 @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
589 @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
590 @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
591 @{method_def intro_classes} & : & @{text method} \\
595 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
598 'instantiation' (nameref + 'and') '::' arity 'begin'
602 'subclass' target? nameref
609 superclassexpr: nameref | (nameref '+' superclassexpr)
615 \item @{command "class"}~@{text "c = superclasses + body"} defines
616 a new class @{text c}, inheriting from @{text superclasses}. This
617 introduces a locale @{text c} with import of all locales @{text
620 Any @{element "fixes"} in @{text body} are lifted to the global
621 theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
622 f\<^sub>n"} of class @{text c}), mapping the local type parameter
623 @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
625 Likewise, @{element "assumes"} in @{text body} are also lifted,
626 mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
627 corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
628 corresponding introduction rule is provided as @{text
629 c_class_axioms.intro}. This rule should be rarely needed directly
630 --- the @{method intro_classes} method takes care of the details of
631 class membership proofs.
633 \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
634 \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
635 allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
636 to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
637 \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the
638 target body poses a goal stating these type arities. The target is
639 concluded by an @{command_ref (local) "end"} command.
641 Note that a list of simultaneous type constructors may be given;
642 this corresponds nicely to mutual recursive type definitions, e.g.\
645 \item @{command "instance"} in an instantiation target body sets
646 up a goal stating the type arities claimed at the opening @{command
647 "instantiation"}. The proof would usually proceed by @{method
648 intro_classes}, and then establish the characteristic theorems of
649 the type classes involved. After finishing the proof, the
650 background theory will be augmented by the proven type arities.
652 \item @{command "subclass"}~@{text c} in a class context for class
653 @{text d} sets up a goal stating that class @{text c} is logically
654 contained in class @{text d}. After finishing the proof, class
655 @{text d} is proven to be subclass @{text c} and the locale @{text
656 c} is interpreted into @{text d} simultaneously.
658 \item @{command "print_classes"} prints all classes in the current
661 \item @{command "class_deps"} visualizes all classes and their
662 subclass relations as a Hasse diagram.
664 \item @{method intro_classes} repeatedly expands all class
665 introduction rules of this theory. Note that this method usually
666 needs not be named explicitly, as it is already included in the
667 default proof step (e.g.\ of @{command "proof"}). In particular,
668 instantiation of trivial (syntactic) classes may be performed by a
669 single ``@{command ".."}'' proof step.
675 subsection {* The class target *}
680 A named context may refer to a locale (cf.\ \secref{sec:target}).
681 If this locale is also a class @{text c}, apart from the common
682 locale target behaviour the following happens.
686 \item Local constant declarations @{text "g[\<alpha>]"} referring to the
687 local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
688 are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
689 referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
691 \item Local theorem bindings are lifted as are assumptions.
693 \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
694 global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
695 resolves ambiguities. In rare cases, manual type annotations are
702 subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
705 \begin{matharray}{rcl}
706 @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
707 @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
710 Axiomatic type classes are Isabelle/Pure's primitive
711 \emph{definitional} interface to type classes. For practical
712 applications, you should consider using classes
713 (cf.~\secref{sec:classes}) which provide high level interface.
716 'axclass' classdecl (axmdecl prop +)
718 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
724 \item @{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n axms"} defines an
725 axiomatic type class as the intersection of existing classes, with
726 additional axioms holding. Class axioms may not contain more than
727 one type variable. The class axioms (with implicit sort constraints
728 added) are bound to the given names. Furthermore a class
729 introduction rule is generated (being bound as @{text
730 c_class.intro}); this rule is employed by method @{method
731 intro_classes} to support instantiation proofs of this class.
733 The ``class axioms'' (which are derived from the internal class
734 definition) are stored as theorems according to the given name
735 specifications; the name space prefix @{text "c_class"} is added
736 here. The full collection of these facts is also stored as @{text
739 \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
740 "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
741 relation or type arity. The proof would usually proceed by @{method
742 intro_classes}, and then establish the characteristic theorems of
743 the type classes involved. After finishing the proof, the theory
744 will be augmented by a type signature declaration corresponding to
745 the resulting theorem.
751 section {* Unrestricted overloading *}
754 Isabelle/Pure's definitional schemes support certain forms of
755 overloading (see \secref{sec:consts}). At most occassions
756 overloading will be used in a Haskell-like fashion together with
757 type classes by means of @{command "instantiation"} (see
758 \secref{sec:class}). Sometimes low-level overloading is desirable.
759 The @{command "overloading"} target provides a convenient view for
762 \begin{matharray}{rcl}
763 @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
768 ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
773 \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>"}
774 opens a theory target (cf.\ \secref{sec:target}) which allows to
775 specify constants with overloaded definitions. These are identified
776 by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
777 constants @{text "c\<^sub>i"} at particular type instances. The
778 definitions themselves are established using common specification
779 tools, using the names @{text "x\<^sub>i"} as reference to the
780 corresponding constants. The target is concluded by @{command
783 A @{text "(unchecked)"} option disables global dependency checks for
784 the corresponding definition, which is occasionally useful for
785 exotic overloading. It is at the discretion of the user to avoid
786 malformed theory specifications!
792 section {* Incorporating ML code \label{sec:ML} *}
795 \begin{matharray}{rcl}
796 @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
797 @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
798 @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
799 @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
800 @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
801 @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
805 @{index_ML bind_thms: "string * thm list -> unit"} \\
806 @{index_ML bind_thm: "string * thm -> unit"} \\
812 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
818 \item @{command "use"}~@{text "file"} reads and executes ML
819 commands from @{text "file"}. The current theory context is passed
820 down to the ML toplevel and may be modified, using @{ML [source=false]
821 "Context.>>"} or derived ML commands. The file name is checked with
822 the @{keyword_ref "uses"} dependency declaration given in the theory
823 header (see also \secref{sec:begin-thy}).
825 Top-level ML bindings are stored within the (global or local) theory
828 \item @{command "ML"}~@{text "text"} is similar to @{command "use"},
829 but executes ML commands directly from the given @{text "text"}.
830 Top-level ML bindings are stored within the (global or local) theory
833 \item @{command "ML_prf"} is analogous to @{command "ML"} but works
834 within a proof context.
836 Top-level ML bindings are stored within the proof context in a
837 purely sequential fashion, disregarding the nested proof structure.
838 ML bindings introduced by @{command "ML_prf"} are discarded at the
841 \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
842 versions of @{command "ML"}, which means that the context may not be
843 updated. @{command "ML_val"} echos the bindings produced at the ML
844 toplevel, but @{command "ML_command"} is silent.
846 \item @{command "setup"}~@{text "text"} changes the current theory
847 context by applying @{text "text"}, which refers to an ML expression
848 of type @{ML_type [source=false] "theory -> theory"}. This enables
849 to initialize any object-logic specific tools and packages written
852 \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
853 theorems produced in ML both in the theory context and the ML
854 toplevel, associating it with the provided name. Theorems are put
855 into a global ``standard'' format before being stored.
857 \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
864 section {* Primitive specification elements *}
866 subsection {* Type classes and sorts \label{sec:classes} *}
869 \begin{matharray}{rcll}
870 @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
871 @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
872 @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
873 @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
877 'classes' (classdecl +)
879 'classrel' (nameref ('<' | subseteq) nameref + 'and')
887 \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
888 @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
889 Isabelle implicitly maintains the transitive closure of the class
890 hierarchy. Cyclic class structures are not permitted.
892 \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
893 relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
894 This is done axiomatically! The @{command_ref "instance"} command
895 (see \secref{sec:axclass}) provides a way to introduce proven class
898 \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
899 new default sort for any type variable that is given explicitly in
900 the text, but lacks a sort constraint (wrt.\ the current context).
901 Type variables generated by type inference are not affected.
903 Usually the default sort is only changed when defining a new
904 object-logic. For example, the default sort in Isabelle/HOL is
905 @{text type}, the class of all HOL types. %FIXME sort antiq?
907 When merging theories, the default sorts of the parents are
908 logically intersected, i.e.\ the representations as lists of classes
911 \item @{command "class_deps"} visualizes the subclass relation,
912 using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
918 subsection {* Types and type abbreviations \label{sec:types-pure} *}
921 \begin{matharray}{rcll}
922 @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
923 @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
924 @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
928 'types' (typespec '=' type infix? +)
930 'typedecl' typespec infix?
932 'arities' (nameref '::' arity +)
938 \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
939 \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
940 @{text "\<tau>"}. Unlike actual type definitions, as are available in
941 Isabelle/HOL for example, type synonyms are merely syntactic
942 abbreviations without any logical significance. Internally, type
943 synonyms are fully expanded.
945 \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
946 type constructor @{text t}. If the object-logic defines a base sort
947 @{text s}, then the constructor is declared to operate on that, via
948 the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
951 \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
952 Isabelle's order-sorted signature of types by new type constructor
953 arities. This is done axiomatically! The @{command_ref "instance"}
954 command (see \secref{sec:axclass}) provides a way to introduce
961 subsection {* Co-regularity of type classes and arities *}
963 text {* The class relation together with the collection of
964 type-constructor arities must obey the principle of
965 \emph{co-regularity} as defined below.
967 \medskip For the subsequent formulation of co-regularity we assume
968 that the class relation is closed by transitivity and reflexivity.
969 Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
970 completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
971 implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
973 Treating sorts as finite sets of classes (meaning the intersection),
974 the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
977 @{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"}
980 This relation on sorts is further extended to tuples of sorts (of
981 the same length) in the component-wise way.
983 \smallskip Co-regularity of the class relation together with the
984 arities relation means:
986 @{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"}
988 \noindent for all such arities. In other words, whenever the result
989 classes of some type-constructor arities are related, then the
990 argument sorts need to be related in the same way.
992 \medskip Co-regularity is a very fundamental property of the
993 order-sorted algebra of types. For example, it entails principle
994 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
998 subsection {* Constants and definitions \label{sec:consts} *}
1001 Definitions essentially express abbreviations within the logic. The
1002 simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
1003 c} is a newly declared constant. Isabelle also allows derived forms
1004 where the arguments of @{text c} appear on the left, abbreviating a
1005 prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
1006 written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
1007 definitions may be weakened by adding arbitrary pre-conditions:
1008 @{text "A \<Longrightarrow> c x y \<equiv> t"}.
1010 \medskip The built-in well-formedness conditions for definitional
1015 \item Arguments (on the left-hand side) must be distinct variables.
1017 \item All variables on the right-hand side must also appear on the
1020 \item All type variables on the right-hand side must also appear on
1021 the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
1022 \<alpha> list)"} for example.
1024 \item The definition must not be recursive. Most object-logics
1025 provide definitional principles that can be used to express
1030 Overloading means that a constant being declared as @{text "c :: \<alpha>
1031 decl"} may be defined separately on type instances @{text "c ::
1032 (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
1033 t}. The right-hand side may mention overloaded constants
1034 recursively at type instances corresponding to the immediate
1035 argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
1036 specification patterns impose global constraints on all occurrences,
1037 e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
1038 corresponding occurrences on some right-hand side need to be an
1039 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1041 \begin{matharray}{rcl}
1042 @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
1043 @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
1044 @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
1048 'consts' ((name '::' type mixfix?) +)
1050 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
1055 'constdefs' structs? (constdecl? constdef +)
1058 structs: '(' 'structure' (vars + 'and') ')'
1060 constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
1062 constdef: thmdecl? prop
1068 \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
1069 c} to have any instance of type scheme @{text \<sigma>}. The optional
1070 mixfix annotations may attach concrete syntax to the constants
1073 \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
1074 as a definitional axiom for some existing constant.
1076 The @{text "(unchecked)"} option disables global dependency checks
1077 for this definition, which is occasionally useful for exotic
1078 overloading. It is at the discretion of the user to avoid malformed
1079 theory specifications!
1081 The @{text "(overloaded)"} option declares definitions to be
1082 potentially overloaded. Unless this option is given, a warning
1083 message would be issued for any definitional equation with a more
1084 special type than that of the corresponding constant declaration.
1086 \item @{command "constdefs"} combines constant declarations and
1087 definitions, with type-inference taking care of the most general
1088 typing of the given specification (the optional type constraint may
1089 refer to type-inference dummies ``@{text _}'' as usual). The
1090 resulting type declaration needs to agree with that of the
1091 specification; overloading is \emph{not} supported here!
1093 The constant name may be omitted altogether, if neither type nor
1094 syntax declarations are given. The canonical name of the
1095 definitional axiom for constant @{text c} will be @{text c_def},
1096 unless specified otherwise. Also note that the given list of
1097 specifications is processed in a strictly sequential manner, with
1098 type-checking being performed independently.
1100 An optional initial context of @{text "(structure)"} declarations
1101 admits use of indexed syntax, using the special symbol @{verbatim
1102 "\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
1103 particularly useful with locales (see also \secref{sec:locale}).
1109 section {* Axioms and theorems \label{sec:axms-thms} *}
1112 \begin{matharray}{rcll}
1113 @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1114 @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1115 @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1119 'axioms' (axmdecl prop +)
1121 ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
1127 \item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary
1128 statements as axioms of the meta-logic. In fact, axioms are
1129 ``axiomatic theorems'', and may be referred later just as any other
1132 Axioms are usually only introduced when declaring new logical
1133 systems. Everyday work is typically done the hard way, with proper
1134 definitions and proven theorems.
1136 \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} retrieves and stores
1137 existing facts in the theory context, or the specified target
1138 context (see also \secref{sec:target}). Typical applications would
1139 also involve attributes, to declare Simplifier rules, for example.
1141 \item @{command "theorems"} is essentially the same as @{command
1142 "lemmas"}, but marks the result as a different kind of facts.
1148 section {* Oracles *}
1150 text {* Oracles allow Isabelle to take advantage of external reasoners
1151 such as arithmetic decision procedures, model checkers, fast
1152 tautology checkers or computer algebra systems. Invoked as an
1153 oracle, an external reasoner can create arbitrary Isabelle theorems.
1155 It is the responsibility of the user to ensure that the external
1156 reasoner is as trustworthy as the application requires. Another
1157 typical source of errors is the linkup between Isabelle and the
1158 external tool, not just its concrete implementation, but also the
1159 required translation between two different logical environments.
1161 Isabelle merely guarantees well-formedness of the propositions being
1162 asserted, and records within the internal derivation object how
1163 presumed theorems depend on unproven suppositions.
1165 \begin{matharray}{rcl}
1166 @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
1170 'oracle' name '=' text
1176 \item @{command "oracle"}~@{text "name = text"} turns the given ML
1177 expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
1178 ML function of type @{ML_text "'a -> thm"}, which is bound to the
1179 global identifier @{ML_text name}. This acts like an infinitary
1180 specification of axioms! Invoking the oracle only works within the
1181 scope of the resulting theory.
1185 See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
1186 defining a new primitive rule as oracle, and turning it into a proof
1191 section {* Name spaces *}
1194 \begin{matharray}{rcl}
1195 @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
1196 @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
1197 @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
1201 'hide' ('(open)')? name (nameref + )
1205 Isabelle organizes any kind of name declarations (of types,
1206 constants, theorems etc.) by separate hierarchically structured name
1207 spaces. Normally the user does not have to control the behavior of
1208 name spaces by hand, yet the following commands provide some way to
1213 \item @{command "global"} and @{command "local"} change the current
1214 name declaration mode. Initially, theories start in @{command
1215 "local"} mode, causing all names to be automatically qualified by
1216 the theory name. Changing this to @{command "global"} causes all
1217 names to be declared without the theory prefix, until @{command
1218 "local"} is declared again.
1220 Note that global names are prone to get hidden accidently later,
1221 when qualified names of the same base name are introduced.
1223 \item @{command "hide"}~@{text "space names"} fully removes
1224 declarations from a given name space (which may be @{text "class"},
1225 @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
1226 "(open)"} option, only the base name is hidden. Global
1227 (unqualified) names may never be hidden.
1229 Note that hiding name space accesses has no impact on logical
1230 declarations --- they remain valid internally. Entities that are no
1231 longer accessible to the user are printed with the special qualifier
1232 ``@{text "??"}'' prefixed to the full internal name.