5 chapter {* 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 @@{command theory} @{syntax name} imports keywords? \<newline> @'begin'
56 imports: @'imports' (@{syntax name} +)
58 keywords: @'keywords' (keyword_decls + @'and')
60 keyword_decls: (@{syntax string} +)
61 ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
66 \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
67 starts a new theory @{text A} based on the merge of existing
68 theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. Due to the possibility to import more
69 than one ancestor, the resulting theory structure of an Isabelle
70 session forms a directed acyclic graph (DAG). Isabelle takes care
71 that sources contributing to the development graph are always
72 up-to-date: changed files are automatically rechecked whenever a
73 theory header specification is processed.
75 The optional @{keyword_def "keywords"} specification declares outer
76 syntax (\chref{ch:outer-syntax}) that is introduced in this theory
77 later on (rare in end-user applications). Both minor keywords and
78 major keywords of the Isar command language need to be specified, in
79 order to make parsing of proof documents work properly. Command
80 keywords need to be classified according to their structural role in
81 the formal text. Examples may be seen in Isabelle/HOL sources
82 itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
83 @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
84 "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
85 with and without proof, respectively. Additional @{syntax tags}
86 provide defaults for document preparation (\secref{sec:tags}).
88 It is possible to specify an alternative completion via @{text "==
89 text"}, while the default is the corresponding keyword name.
91 \item @{command (global) "end"} concludes the current theory
92 definition. Note that some other commands, e.g.\ local theory
93 targets @{command locale} or @{command class} may involve a
94 @{keyword "begin"} that needs to be matched by @{command (local)
95 "end"}, according to the usual rules for nested blocks.
101 section {* Local theory targets \label{sec:target} *}
104 \begin{matharray}{rcll}
105 @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
106 @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
109 A local theory target is a context managed separately within the
110 enclosing theory. Contexts may introduce parameters (fixed
111 variables) and assumptions (hypotheses). Definitions and theorems
112 depending on the context may be added incrementally later on.
114 \emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or
115 type classes (cf.\ \secref{sec:class}); the name ``@{text "-"}''
116 signifies the global theory context.
118 \emph{Unnamed contexts} may introduce additional parameters and
119 assumptions, and results produced in the context are generalized
120 accordingly. Such auxiliary contexts may be nested within other
121 targets, like @{command "locale"}, @{command "class"}, @{command
122 "instantiation"}, @{command "overloading"}.
125 @@{command context} @{syntax nameref} @'begin'
127 @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
129 @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
134 \item @{command "context"}~@{text "c \<BEGIN>"} opens a named
135 context, by recommencing an existing locale or class @{text c}.
136 Note that locale and class definitions allow to include the
137 @{keyword "begin"} keyword as well, in order to continue the local
138 theory immediately after the initial specification.
140 \item @{command "context"}~@{text "bundles elements \<BEGIN>"} opens
141 an unnamed context, by extending the enclosing global or local
142 theory target by the given declaration bundles (\secref{sec:bundle})
143 and context elements (@{text "\<FIXES>"}, @{text "\<ASSUMES>"}
144 etc.). This means any results stemming from definitions and proofs
145 in the extended context will be exported into the enclosing target
146 by lifting over extra parameters and premises.
148 \item @{command (local) "end"} concludes the current local theory,
149 according to the nesting of contexts. Note that a global @{command
150 (global) "end"} has a different meaning: it concludes the theory
151 itself (\secref{sec:begin-thy}).
153 \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
154 local theory command specifies an immediate target, e.g.\
155 ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
156 "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
157 global theory context; the current target context will be suspended
158 for this command only. Note that ``@{text "(\<IN> -)"}'' will
159 always produce a global result independently of the current target
164 The exact meaning of results produced within a local theory context
165 depends on the underlying target infrastructure (locale, type class
166 etc.). The general idea is as follows, considering a context named
167 @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
169 Definitions are exported by introducing a global version with
170 additional arguments; a syntactic abbreviation links the long form
171 with the abstract version of the target context. For example,
172 @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
173 level (for arbitrary @{text "?x"}), together with a local
174 abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
175 fixed parameter @{text x}).
177 Theorems are exported by discharging the assumptions and
178 generalizing the parameters of the context. For example, @{text "a:
179 B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
182 \medskip The Isabelle/HOL library contains numerous applications of
183 locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}. An
184 example for an unnamed auxiliary contexts is given in @{file
185 "~~/src/HOL/Isar_Examples/Group_Context.thy"}. *}
188 section {* Bundled declarations \label{sec:bundle} *}
191 \begin{matharray}{rcl}
192 @{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
193 @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
194 @{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
195 @{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
196 @{keyword_def "includes"} & : & syntax \\
199 The outer syntax of fact expressions (\secref{sec:syn-att}) involves
200 theorems and attributes, which are evaluated in the context and
201 applied to it. Attributes may declare theorems to the context, as
202 in @{text "this_rule [intro] that_rule [elim]"} for example.
203 Configuration options (\secref{sec:config}) are special declaration
204 attributes that operate on the context without a theorem, as in
205 @{text "[[show_types = false]]"} for example.
207 Expressions of this form may be defined as \emph{bundled
208 declarations} in the context, and included in other situations later
209 on. Including declaration bundles augments a local context casually
210 without logical dependencies, which is in contrast to locales and
211 locale interpretation (\secref{sec:locale}).
214 @@{command bundle} @{syntax target}? \<newline>
215 @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
217 (@@{command include} | @@{command including}) (@{syntax nameref}+)
219 @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
224 \item @{command bundle}~@{text "b = decls"} defines a bundle of
225 declarations in the current context. The RHS is similar to the one
226 of the @{command declare} command. Bundles defined in local theory
227 targets are subject to transformations via morphisms, when moved
228 into different application contexts; this works analogously to any
229 other local theory specification.
231 \item @{command print_bundles} prints the named bundles that are
232 available in the current context.
234 \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
235 from the given bundles into the current proof body context. This is
236 analogous to @{command "note"} (\secref{sec:proof-facts}) with the
239 \item @{command including} is similar to @{command include}, but
240 works in proof refinement (backward mode). This is analogous to
241 @{command "using"} (\secref{sec:proof-facts}) with the expanded
244 \item @{keyword "includes"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is similar to
245 @{command include}, but works in situations where a specification
246 context is constructed, notably for @{command context} and long
247 statements of @{command theorem} etc.
251 Here is an artificial example of bundling various configuration
254 bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
257 including trace by metis
260 section {* Term definitions \label{sec:term-definitions} *}
263 \begin{matharray}{rcll}
264 @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
265 @{attribute_def "defn"} & : & @{text attribute} \\
266 @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
267 @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
268 @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
271 Term definitions may either happen within the logic (as equational axioms
272 of a certain form, see also see \secref{sec:consts}), or outside of it as
273 rewrite system on abstract syntax. The second form is called
277 @@{command definition} @{syntax target}? \<newline>
278 (decl @'where')? @{syntax thmdecl}? @{syntax prop}
280 @@{command abbreviation} @{syntax target}? @{syntax mode}? \<newline>
281 (decl @'where')? @{syntax prop}
284 decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
289 \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
290 internal definition @{text "c \<equiv> t"} according to the specification
291 given as @{text eq}, which is then turned into a proven fact. The
292 given proposition may deviate from internal meta-level equality
293 according to the rewrite rules declared as @{attribute defn} by the
294 object-logic. This usually covers object-level equality @{text "x =
295 y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
296 change the @{attribute defn} setup.
298 Definitions may be presented with explicit arguments on the LHS, as
299 well as additional conditions, e.g.\ @{text "f x y = t"} instead of
300 @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
301 unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
303 \item @{command "print_defn_rules"} prints the definitional rewrite rules
304 declared via @{attribute defn} in the current context.
306 \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
307 syntactic constant which is associated with a certain term according
308 to the meta-level equality @{text eq}.
310 Abbreviations participate in the usual type-inference process, but
311 are expanded before the logic ever sees them. Pretty printing of
312 terms involves higher-order rewriting with rules stemming from
313 reverted abbreviations. This needs some care to avoid overlapping
314 or looping syntactic replacements!
316 The optional @{text mode} specification restricts output to a
317 particular print mode; using ``@{text input}'' here achieves the
318 effect of one-way abbreviations. The mode may also include an
319 ``@{keyword "output"}'' qualifier that affects the concrete syntax
320 declared for abbreviations, cf.\ @{command "syntax"} in
321 \secref{sec:syn-trans}.
323 \item @{command "print_abbrevs"} prints all constant abbreviations
324 of the current context.
330 section {* Axiomatizations \label{sec:axiomatizations} *}
333 \begin{matharray}{rcll}
334 @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
338 @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
341 @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
342 @{syntax mixfix}? | @{syntax vars}) + @'and')
344 specs: (@{syntax thmdecl}? @{syntax props} + @'and')
349 \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
350 introduces several constants simultaneously and states axiomatic
351 properties for these. The constants are marked as being specified once and
352 for all, which prevents additional specifications for the same constants
353 later on, but it is always possible do emit axiomatizations without
354 referring to particular constants. Note that lack of precise dependency
355 tracking of axiomatizations may disrupt the well-formedness of an
356 otherwise definitional theory.
358 Axiomatization is restricted to a global theory context: support for local
359 theory targets \secref{sec:target} would introduce an extra dimension of
360 uncertainty what the written specifications really are, and make it
361 infeasible to argue why they are correct.
363 Axiomatic specifications are required when declaring a new logical system
364 within Isabelle/Pure, but in an application environment like Isabelle/HOL
365 the user normally stays within definitional mechanisms provided by the
366 logic and its libraries.
372 section {* Generic declarations *}
375 \begin{matharray}{rcl}
376 @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
377 @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
378 @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
381 Arbitrary operations on the background context may be wrapped-up as
382 generic declaration elements. Since the underlying concept of local
383 theories may be subject to later re-interpretation, there is an
384 additional dependency on a morphism that tells the difference of the
385 original declaration context wrt.\ the application context
386 encountered later on. A fact declaration is an important special
387 case: it consists of a theorem which is applied to the context by
388 means of an attribute.
391 (@@{command declaration} | @@{command syntax_declaration})
392 ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
394 @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
399 \item @{command "declaration"}~@{text d} adds the declaration
400 function @{text d} of ML type @{ML_type declaration}, to the current
401 local theory under construction. In later application contexts, the
402 function is transformed according to the morphisms being involved in
403 the interpretation hierarchy.
405 If the @{text "(pervasive)"} option is given, the corresponding
406 declaration is applied to all possible contexts involved, including
407 the global background theory.
409 \item @{command "syntax_declaration"} is similar to @{command
410 "declaration"}, but is meant to affect only ``syntactic'' tools by
411 convention (such as notation and type-checking information).
413 \item @{command "declare"}~@{text thms} declares theorems to the
414 current local theory context. No theorem binding is involved here,
415 unlike @{command "theorems"} or @{command "lemmas"} (cf.\
416 \secref{sec:theorems}), so @{command "declare"} only has the effect
417 of applying attributes as included in the theorem specification.
423 section {* Locales \label{sec:locale} *}
426 A locale is a functor that maps parameters (including implicit type
427 parameters) and a specification to a list of declarations. The
428 syntax of locales is modeled after the Isar proof context commands
429 (cf.\ \secref{sec:proof-context}).
431 Locale hierarchies are supported by maintaining a graph of
432 dependencies between locale instances in the global theory.
433 Dependencies may be introduced through import (where a locale is
434 defined as sublocale of the imported instances) or by proving that
435 an existing locale is a sublocale of one or several locale
438 A locale may be opened with the purpose of appending to its list of
439 declarations (cf.\ \secref{sec:target}). When opening a locale
440 declarations from all dependencies are collected and are presented
441 as a local theory. In this process, which is called \emph{roundup},
442 redundant locale instances are omitted. A locale instance is
443 redundant if it is subsumed by an instance encountered earlier. A
444 more detailed description of this process is available elsewhere
449 subsection {* Locale expressions \label{sec:locale-expr} *}
452 A \emph{locale expression} denotes a context composed of instances
453 of existing locales. The context consists of the declaration
454 elements from the locale instances. Redundant locale instances are
455 omitted according to roundup.
458 @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax "fixes"} + @'and'))?
460 instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
462 qualifier: @{syntax name} ('?' | '!')?
464 pos_insts: ('_' | @{syntax term})*
466 named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
469 A locale instance consists of a reference to a locale and either
470 positional or named parameter instantiations. Identical
471 instantiations (that is, those that instantiate a parameter by itself)
472 may be omitted. The notation `@{text "_"}' enables to omit the
473 instantiation for a parameter inside a positional instantiation.
475 Terms in instantiations are from the context the locale expressions
476 is declared in. Local names may be added to this context with the
477 optional @{keyword "for"} clause. This is useful for shadowing names
478 bound in outer contexts, and for declaring syntax. In addition,
479 syntax declarations from one instance are effective when parsing
480 subsequent instances of the same expression.
482 Instances have an optional qualifier which applies to names in
483 declarations. Names include local definitions and theorem names.
484 If present, the qualifier itself is either optional
485 (``\texttt{?}''), which means that it may be omitted on input of the
486 qualified name, or mandatory (``\texttt{!}''). If neither
487 ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
488 is used. For @{command "interpretation"} and @{command "interpret"}
489 the default is ``mandatory'', for @{command "locale"} and @{command
490 "sublocale"} the default is ``optional''. Qualifiers play no role
491 in determining whether one locale instance subsumes another.
495 subsection {* Locale declarations *}
498 \begin{matharray}{rcl}
499 @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
500 @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
501 @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
502 @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
503 @{method_def intro_locales} & : & @{text method} \\
504 @{method_def unfold_locales} & : & @{text method} \\
507 \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
508 \indexisarelem{defines}\indexisarelem{notes}
510 @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
512 @@{command print_locale} '!'? @{syntax nameref}
514 @{syntax_def locale}: @{syntax context_elem}+ |
515 @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
517 @{syntax_def context_elem}:
518 @'fixes' (@{syntax "fixes"} + @'and') |
519 @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
520 @'assumes' (@{syntax props} + @'and') |
521 @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
522 @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
527 \item @{command "locale"}~@{text "loc = import + body"} defines a
528 new locale @{text loc} as a context consisting of a certain view of
529 existing locales (@{text import}) plus some additional elements
530 (@{text body}). Both @{text import} and @{text body} are optional;
531 the degenerate form @{command "locale"}~@{text loc} defines an empty
532 locale, which may still be useful to collect declarations of facts
533 later on. Type-inference on locale expressions automatically takes
534 care of the most general typing that the combined context elements
537 The @{text import} consists of a locale expression; see
538 \secref{sec:proof-context} above. Its @{keyword "for"} clause defines
539 the parameters of @{text import}. These are parameters of
540 the defined locale. Locale parameters whose instantiation is
541 omitted automatically extend the (possibly empty) @{keyword "for"}
542 clause: they are inserted at its beginning. This means that these
543 parameters may be referred to from within the expression and also in
544 the subsequent context elements and provides a notational
545 convenience for the inheritance of parameters in locale
548 The @{text body} consists of context elements.
552 \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
553 parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
554 are optional). The special syntax declaration ``@{text
555 "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may
556 be referenced implicitly in this context.
558 \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
559 constraint @{text \<tau>} on the local parameter @{text x}. This
560 element is deprecated. The type constraint should be introduced in
561 the @{keyword "for"} clause or the relevant @{element "fixes"} element.
563 \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
564 introduces local premises, similar to @{command "assume"} within a
565 proof (cf.\ \secref{sec:proof-context}).
567 \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
568 declared parameter. This is similar to @{command "def"} within a
569 proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
570 takes an equational proposition instead of variable-term pair. The
571 left-hand side of the equation may have additional arguments, e.g.\
572 ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
574 \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
575 reconsiders facts within a local context. Most notably, this may
576 include arbitrary declarations in any attribute specifications
577 included here, e.g.\ a local @{attribute simp} rule.
581 Both @{element "assumes"} and @{element "defines"} elements
582 contribute to the locale specification. When defining an operation
583 derived from the parameters, @{command "definition"}
584 (\secref{sec:term-definitions}) is usually more appropriate.
586 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
587 in the syntax of @{element "assumes"} and @{element "defines"} above
588 are illegal in locale definitions. In the long goal format of
589 \secref{sec:goals}, term bindings may be included as expected,
592 \medskip Locale specifications are ``closed up'' by
593 turning the given text into a predicate definition @{text
594 loc_axioms} and deriving the original assumptions as local lemmas
595 (modulo local definitions). The predicate statement covers only the
596 newly specified assumptions, omitting the content of included locale
597 expressions. The full cumulative view is only provided on export,
598 involving another predicate @{text loc} that refers to the complete
601 In any case, the predicate arguments are those locale parameters
602 that actually occur in the respective piece of text. Also these
603 predicates operate at the meta-level in theory, but the locale
604 packages attempts to internalize statements according to the
605 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
606 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
607 \secref{sec:object-logic}). Separate introduction rules @{text
608 loc_axioms.intro} and @{text loc.intro} are provided as well.
610 \item @{command "print_locale"}~@{text "locale"} prints the
611 contents of the named locale. The command omits @{element "notes"}
612 elements by default. Use @{command "print_locale"}@{text "!"} to
615 \item @{command "print_locales"} prints the names of all locales
616 of the current theory.
618 \item @{command "locale_deps"} visualizes all locales and their
619 relations as a Hasse diagram. This includes locales defined as type
620 classes (\secref{sec:class}). See also @{command
621 "print_dependencies"} below.
623 \item @{method intro_locales} and @{method unfold_locales}
624 repeatedly expand all introduction rules of locale predicates of the
625 theory. While @{method intro_locales} only applies the @{text
626 loc.intro} introduction rules and therefore does not descend to
627 assumptions, @{method unfold_locales} is more aggressive and applies
628 @{text loc_axioms.intro} as well. Both methods are aware of locale
629 specifications entailed by the context, both from target statements,
630 and from interpretations (see below). New goals that are entailed
631 by the current context are discharged automatically.
637 subsection {* Locale interpretation *}
640 \begin{matharray}{rcl}
641 @{command_def "interpretation"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\
642 @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
643 @{command_def "sublocale"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\
644 @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
645 @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
648 Locales may be instantiated, and the resulting instantiated
649 declarations added to the current context. This requires proof (of
650 the instantiated specification) and is called \emph{locale
651 interpretation}. Interpretation is possible in locales (@{command
652 "sublocale"}), global and local theories (@{command
653 "interpretation"}) and also within proof bodies (@{command
657 @@{command interpretation} @{syntax locale_expr} equations?
659 @@{command interpret} @{syntax locale_expr} equations?
661 @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
664 @@{command print_dependencies} '!'? @{syntax locale_expr}
666 @@{command print_interps} @{syntax nameref}
669 equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
674 \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
675 interprets @{text expr} in a global or local theory. The command
676 generates proof obligations for the instantiated specifications.
677 Once these are discharged by the user, instantiated declarations (in
678 particular, facts) are added to the theory in a post-processing
681 The command is aware of interpretations that are already active.
682 Post-processing is achieved through a variant of roundup that takes
683 the interpretations of the current global or local theory into
684 account. In order to simplify the proof obligations according to
685 existing interpretations use methods @{method intro_locales} or
686 @{method unfold_locales}.
688 When adding declarations to locales, interpreted versions of these
689 declarations are added to the global theory for all interpretations
690 in the global theory as well. That is, interpretations in global
691 theories dynamically participate in any declarations added to
694 In contrast, the lifetime of an interpretation in a local theory is
695 limited to the current context block. At the closing @{command end}
696 of the block the interpretation and its declarations disappear.
697 This enables establishing facts based on interpretations without
698 creating permanent links to the interpreted locale instances, as
699 would be the case with @{command sublocale}.
700 While @{command "interpretation"}~@{text "(\<IN> c)
701 \<dots>"} is technically possible, it is not useful since its result is
702 discarded immediately.
704 Free variables in the interpreted expression are allowed. They are
705 turned into schematic variables in the generated declarations. In
706 order to use a free variable whose name is already bound in the
707 context --- for example, because a constant of that name exists ---
708 add it to the @{keyword "for"} clause.
710 The equations @{text eqns} yield \emph{rewrite morphisms}, which are
711 unfolded during post-processing and are useful for interpreting
712 concepts introduced through definitions. The equations must be
715 \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
716 @{text expr} in the proof context and is otherwise similar to
717 interpretation in local theories. Note that for @{command
718 "interpret"} the @{text eqns} should be
719 explicitly universally quantified.
721 \item @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
723 interprets @{text expr} in the locale @{text name}. A proof that
724 the specification of @{text name} implies the specification of
725 @{text expr} is required. As in the localized version of the
726 theorem command, the proof is in the context of @{text name}. After
727 the proof obligation has been discharged, the locale hierarchy is
728 changed as if @{text name} imported @{text expr} (hence the name
729 @{command "sublocale"}). When the context of @{text name} is
730 subsequently entered, traversing the locale hierarchy will involve
731 the locale instances of @{text expr}, and their declarations will be
732 added to the context. This makes @{command "sublocale"}
733 dynamic: extensions of a locale that is instantiated in @{text expr}
734 may take place after the @{command "sublocale"} declaration and
735 still become available in the context. Circular @{command
736 "sublocale"} declarations are allowed as long as they do not lead to
739 If interpretations of @{text name} exist in the current global
740 theory, the command adds interpretations for @{text expr} as well,
741 with the same qualifier, although only for fragments of @{text expr}
742 that are not interpreted in the theory already.
744 The equations @{text eqns} amend the morphism through
745 which @{text expr} is interpreted. This enables mapping definitions
746 from the interpreted locales to entities of @{text name} and can
747 help break infinite chains induced by circular @{command
748 "sublocale"} declarations.
750 In a named context block the @{command sublocale} command may also
751 be used, but the locale argument must be omitted. The command then
752 refers to the locale (or class) target of the context block.
754 \item @{command "print_dependencies"}~@{text "expr"} is useful for
755 understanding the effect of an interpretation of @{text "expr"} in
756 the current context. It lists all locale instances for which
757 interpretations would be added to the current context. Variant
758 @{command "print_dependencies"}@{text "!"} does not generalize
759 parameters and assumes an empty context --- that is, it prints all
760 locale instances that would be considered for interpretation. The
761 latter is useful for understanding the dependencies of a locale
764 \item @{command "print_interps"}~@{text "locale"} lists all
765 interpretations of @{text "locale"} in the current theory or proof
766 context, including those due to a combination of an @{command
767 "interpretation"} or @{command "interpret"} and one or several
768 @{command "sublocale"} declarations.
773 If a global theory inherits declarations (body elements) for a
774 locale from one parent and an interpretation of that locale from
775 another parent, the interpretation will not be applied to the
780 Since attributes are applied to interpreted theorems,
781 interpretation may modify the context of common proof tools, e.g.\
782 the Simplifier or Classical Reasoner. As the behavior of such
783 tools is \emph{not} stable under interpretation morphisms, manual
784 declarations might have to be added to the target context of the
785 interpretation to revert such declarations.
789 An interpretation in a local theory or proof context may subsume previous
790 interpretations. This happens if the same specification fragment
791 is interpreted twice and the instantiation of the second
792 interpretation is more general than the interpretation of the
793 first. The locale package does not attempt to remove subsumed
799 section {* Classes \label{sec:class} *}
802 \begin{matharray}{rcl}
803 @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
804 @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
805 @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
806 @{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
807 @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
808 @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
809 @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
810 @{method_def intro_classes} & : & @{text method} \\
813 A class is a particular locale with \emph{exactly one} type variable
814 @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
815 is established which is interpreted logically as axiomatic type
816 class \cite{Wenzel:1997:TPHOL} whose logical content are the
817 assumptions of the locale. Thus, classes provide the full
818 generality of locales combined with the commodity of type classes
819 (notably type-inference). See \cite{isabelle-classes} for a short
823 @@{command class} class_spec @'begin'?
825 class_spec: @{syntax name} '='
826 ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
827 @{syntax nameref} | (@{syntax context_elem}+))
829 @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
831 @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
832 @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
834 @@{command subclass} @{syntax target}? @{syntax nameref}
839 \item @{command "class"}~@{text "c = superclasses + body"} defines
840 a new class @{text c}, inheriting from @{text superclasses}. This
841 introduces a locale @{text c} with import of all locales @{text
844 Any @{element "fixes"} in @{text body} are lifted to the global
845 theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
846 f\<^sub>n"} of class @{text c}), mapping the local type parameter
847 @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
849 Likewise, @{element "assumes"} in @{text body} are also lifted,
850 mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
851 corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
852 corresponding introduction rule is provided as @{text
853 c_class_axioms.intro}. This rule should be rarely needed directly
854 --- the @{method intro_classes} method takes care of the details of
855 class membership proofs.
857 \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
858 \<BEGIN>"} opens a target (cf.\ \secref{sec:target}) which
859 allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
860 to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
861 \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the
862 target body poses a goal stating these type arities. The target is
863 concluded by an @{command_ref (local) "end"} command.
865 Note that a list of simultaneous type constructors may be given;
866 this corresponds nicely to mutually recursive type definitions, e.g.\
869 \item @{command "instance"} in an instantiation target body sets
870 up a goal stating the type arities claimed at the opening @{command
871 "instantiation"}. The proof would usually proceed by @{method
872 intro_classes}, and then establish the characteristic theorems of
873 the type classes involved. After finishing the proof, the
874 background theory will be augmented by the proven type arities.
876 On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
877 s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
878 need to specify operations: one can continue with the
879 instantiation proof immediately.
881 \item @{command "subclass"}~@{text c} in a class context for class
882 @{text d} sets up a goal stating that class @{text c} is logically
883 contained in class @{text d}. After finishing the proof, class
884 @{text d} is proven to be subclass @{text c} and the locale @{text
885 c} is interpreted into @{text d} simultaneously.
887 A weakened form of this is available through a further variant of
888 @{command instance}: @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
889 a proof that class @{text "c\<^sub>2"} implies @{text "c\<^sub>1"} without reference
890 to the underlying locales; this is useful if the properties to prove
891 the logical connection are not sufficient on the locale level but on
894 \item @{command "print_classes"} prints all classes in the current
897 \item @{command "class_deps"} visualizes all classes and their
898 subclass relations as a Hasse diagram.
900 \item @{method intro_classes} repeatedly expands all class
901 introduction rules of this theory. Note that this method usually
902 needs not be named explicitly, as it is already included in the
903 default proof step (e.g.\ of @{command "proof"}). In particular,
904 instantiation of trivial (syntactic) classes may be performed by a
905 single ``@{command ".."}'' proof step.
911 subsection {* The class target *}
916 A named context may refer to a locale (cf.\ \secref{sec:target}).
917 If this locale is also a class @{text c}, apart from the common
918 locale target behaviour the following happens.
922 \item Local constant declarations @{text "g[\<alpha>]"} referring to the
923 local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
924 are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
925 referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
927 \item Local theorem bindings are lifted as are assumptions.
929 \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
930 global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
931 resolves ambiguities. In rare cases, manual type annotations are
938 subsection {* Co-regularity of type classes and arities *}
940 text {* The class relation together with the collection of
941 type-constructor arities must obey the principle of
942 \emph{co-regularity} as defined below.
944 \medskip For the subsequent formulation of co-regularity we assume
945 that the class relation is closed by transitivity and reflexivity.
946 Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
947 completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
948 implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
950 Treating sorts as finite sets of classes (meaning the intersection),
951 the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
954 @{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"}
957 This relation on sorts is further extended to tuples of sorts (of
958 the same length) in the component-wise way.
960 \smallskip Co-regularity of the class relation together with the
961 arities relation means:
963 @{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"}
965 \noindent for all such arities. In other words, whenever the result
966 classes of some type-constructor arities are related, then the
967 argument sorts need to be related in the same way.
969 \medskip Co-regularity is a very fundamental property of the
970 order-sorted algebra of types. For example, it entails principle
971 types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
975 section {* Unrestricted overloading *}
978 \begin{matharray}{rcl}
979 @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
982 Isabelle/Pure's definitional schemes support certain forms of
983 overloading (see \secref{sec:consts}). Overloading means that a
984 constant being declared as @{text "c :: \<alpha> decl"} may be
985 defined separately on type instances
986 @{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
987 for each type constructor @{text t}. At most occasions
988 overloading will be used in a Haskell-like fashion together with
989 type classes by means of @{command "instantiation"} (see
990 \secref{sec:class}). Sometimes low-level overloading is desirable.
991 The @{command "overloading"} target provides a convenient view for
995 @@{command overloading} ( spec + ) @'begin'
997 spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
1002 \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>"}
1003 opens a theory target (cf.\ \secref{sec:target}) which allows to
1004 specify constants with overloaded definitions. These are identified
1005 by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
1006 constants @{text "c\<^sub>i"} at particular type instances. The
1007 definitions themselves are established using common specification
1008 tools, using the names @{text "x\<^sub>i"} as reference to the
1009 corresponding constants. The target is concluded by @{command
1012 A @{text "(unchecked)"} option disables global dependency checks for
1013 the corresponding definition, which is occasionally useful for
1014 exotic overloading (see \secref{sec:consts} for a precise description).
1015 It is at the discretion of the user to avoid
1016 malformed theory specifications!
1022 section {* Incorporating ML code \label{sec:ML} *}
1025 \begin{matharray}{rcl}
1026 @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
1027 @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1028 @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1029 @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
1030 @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
1031 @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
1032 @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
1033 @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1034 @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
1036 \begin{tabular}{rcll}
1037 @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
1038 @{attribute_def ML_source_trace} & : & @{text attribute} & default @{text false} \\
1039 @{attribute_def ML_exception_trace} & : & @{text attribute} & default @{text false} \\
1043 (@@{command SML_file} | @@{command ML_file}) @{syntax name}
1045 (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
1046 @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
1048 @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
1053 \item @{command "SML_file"}~@{text "name"} reads and evaluates the
1054 given Standard ML file. Top-level SML bindings are stored within
1055 the theory context; the initial environment is restricted to the
1056 Standard ML implementation of Poly/ML, without the many add-ons of
1057 Isabelle/ML. Multiple @{command "SML_file"} commands may be used to
1058 build larger Standard ML projects, independently of the regular
1059 Isabelle/ML environment.
1061 \item @{command "ML_file"}~@{text "name"} reads and evaluates the
1062 given ML file. The current theory context is passed down to the ML
1063 toplevel and may be modified, using @{ML "Context.>>"} or derived ML
1064 commands. Top-level ML bindings are stored within the (global or
1065 local) theory context.
1067 \item @{command "ML"}~@{text "text"} is similar to @{command
1068 "ML_file"}, but evaluates directly the given @{text "text"}.
1069 Top-level ML bindings are stored within the (global or local) theory
1072 \item @{command "ML_prf"} is analogous to @{command "ML"} but works
1073 within a proof context. Top-level ML bindings are stored within the
1074 proof context in a purely sequential fashion, disregarding the
1075 nested proof structure. ML bindings introduced by @{command
1076 "ML_prf"} are discarded at the end of the proof.
1078 \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
1079 versions of @{command "ML"}, which means that the context may not be
1080 updated. @{command "ML_val"} echos the bindings produced at the ML
1081 toplevel, but @{command "ML_command"} is silent.
1083 \item @{command "setup"}~@{text "text"} changes the current theory
1084 context by applying @{text "text"}, which refers to an ML expression
1085 of type @{ML_type "theory -> theory"}. This enables to initialize
1086 any object-logic specific tools and packages written in ML, for
1089 \item @{command "local_setup"} is similar to @{command "setup"} for
1090 a local theory context, and an ML expression of type @{ML_type
1091 "local_theory -> local_theory"}. This allows to
1092 invoke local theory specification packages without going through
1093 concrete outer syntax, for example.
1095 \item @{command "attribute_setup"}~@{text "name = text description"}
1096 defines an attribute in the current theory. The given @{text
1097 "text"} has to be an ML expression of type
1098 @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
1099 structure @{ML_structure Args} and @{ML_structure Attrib}.
1101 In principle, attributes can operate both on a given theorem and the
1102 implicit context, although in practice only one is modified and the
1103 other serves as parameter. Here are examples for these two cases:
1108 attribute_setup my_rule = {*
1109 Attrib.thms >> (fn ths =>
1111 (fn context: Context.generic => fn th: thm =>
1112 let val th' = th OF ths
1115 attribute_setup my_declaration = {*
1116 Attrib.thms >> (fn ths =>
1117 Thm.declaration_attribute
1118 (fn th: thm => fn context: Context.generic =>
1119 let val context' = context
1120 in context' end)) *}
1125 \item @{attribute ML_print_depth} controls the printing depth of the ML
1126 toplevel pretty printer; the precise effect depends on the ML compiler and
1127 run-time system. Typically the limit should be less than 10. Bigger values
1128 such as 100--1000 are occasionally useful for debugging.
1130 \item @{attribute ML_source_trace} indicates whether the source text that
1131 is given to the ML compiler should be output: it shows the raw Standard ML
1132 after expansion of Isabelle/ML antiquotations.
1134 \item @{attribute ML_exception_trace} indicates whether the ML run-time
1135 system should print a detailed stack trace on exceptions. The result is
1136 dependent on the particular ML compiler version. Note that after Poly/ML
1137 5.3 some optimizations in the run-time systems may hinder exception
1140 The boundary for the exception trace is the current Isar command
1141 transactions. It is occasionally better to insert the combinator @{ML
1142 Runtime.exn_trace} into ML code for debugging
1143 \cite{isabelle-implementation}, closer to the point where it actually
1150 section {* Primitive specification elements *}
1152 subsection {* Sorts *}
1155 \begin{matharray}{rcll}
1156 @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
1160 @@{command default_sort} @{syntax sort}
1165 \item @{command "default_sort"}~@{text s} makes sort @{text s} the
1166 new default sort for any type variable that is given explicitly in
1167 the text, but lacks a sort constraint (wrt.\ the current context).
1168 Type variables generated by type inference are not affected.
1170 Usually the default sort is only changed when defining a new
1171 object-logic. For example, the default sort in Isabelle/HOL is
1172 @{class type}, the class of all HOL types.
1174 When merging theories, the default sorts of the parents are
1175 logically intersected, i.e.\ the representations as lists of classes
1182 subsection {* Types \label{sec:types-pure} *}
1185 \begin{matharray}{rcll}
1186 @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1187 @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1191 @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
1193 @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
1198 \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
1199 \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type @{text
1200 "\<tau>"}. Unlike the semantic type definitions in Isabelle/HOL, type synonyms
1201 are merely syntactic abbreviations without any logical significance.
1202 Internally, type synonyms are fully expanded.
1204 \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
1205 type constructor @{text t}. If the object-logic defines a base sort
1206 @{text s}, then the constructor is declared to operate on that, via
1207 the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
1212 If you introduce a new type axiomatically, i.e.\ via @{command_ref
1213 typedecl} and @{command_ref axiomatization}
1214 (\secref{sec:axiomatizations}), the minimum requirement is that it has a
1215 non-empty model, to avoid immediate collapse of the logical environment.
1216 Moreover, one needs to demonstrate that the interpretation of such
1217 free-form axiomatizations can coexist with other axiomatization schemes
1218 for types, notably @{command_def typedef} in Isabelle/HOL
1219 (\secref{sec:hol-typedef}), or any other extension that people might have
1220 introduced elsewhere.
1225 subsection {* Constants and definitions \label{sec:consts} *}
1228 \begin{matharray}{rcl}
1229 @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
1230 @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
1233 Definitions essentially express abbreviations within the logic. The
1234 simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
1235 c} is a newly declared constant. Isabelle also allows derived forms
1236 where the arguments of @{text c} appear on the left, abbreviating a
1237 prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
1238 written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
1239 definitions may be weakened by adding arbitrary pre-conditions:
1240 @{text "A \<Longrightarrow> c x y \<equiv> t"}.
1242 \medskip The built-in well-formedness conditions for definitional
1247 \item Arguments (on the left-hand side) must be distinct variables.
1249 \item All variables on the right-hand side must also appear on the
1252 \item All type variables on the right-hand side must also appear on
1253 the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
1254 \<alpha> list)"} for example.
1256 \item The definition must not be recursive. Most object-logics
1257 provide definitional principles that can be used to express
1262 The right-hand side of overloaded definitions may mention overloaded constants
1263 recursively at type instances corresponding to the immediate
1264 argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
1265 specification patterns impose global constraints on all occurrences,
1266 e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
1267 corresponding occurrences on some right-hand side need to be an
1268 instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
1271 @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
1273 @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
1275 opt: '(' @'unchecked'? @'overloaded'? ')'
1280 \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
1281 c} to have any instance of type scheme @{text \<sigma>}. The optional
1282 mixfix annotations may attach concrete syntax to the constants
1285 \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
1286 as a definitional axiom for some existing constant.
1288 The @{text "(unchecked)"} option disables global dependency checks
1289 for this definition, which is occasionally useful for exotic
1290 overloading. It is at the discretion of the user to avoid malformed
1291 theory specifications!
1293 The @{text "(overloaded)"} option declares definitions to be
1294 potentially overloaded. Unless this option is given, a warning
1295 message would be issued for any definitional equation with a more
1296 special type than that of the corresponding constant declaration.
1302 section {* Naming existing theorems \label{sec:theorems} *}
1305 \begin{matharray}{rcll}
1306 @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1307 @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
1311 (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
1312 (@{syntax thmdef}? @{syntax thmrefs} + @'and')
1313 (@'for' (@{syntax vars} + @'and'))?
1318 \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def
1319 "for"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"} evaluates given facts (with attributes) in
1320 the current context, which may be augmented by local variables.
1321 Results are standardized before being stored, i.e.\ schematic
1322 variables are renamed to enforce index @{text "0"} uniformly.
1324 \item @{command "theorems"} is the same as @{command "lemmas"}, but
1325 marks the result as a different kind of facts.
1331 section {* Oracles *}
1334 \begin{matharray}{rcll}
1335 @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
1338 Oracles allow Isabelle to take advantage of external reasoners such
1339 as arithmetic decision procedures, model checkers, fast tautology
1340 checkers or computer algebra systems. Invoked as an oracle, an
1341 external reasoner can create arbitrary Isabelle theorems.
1343 It is the responsibility of the user to ensure that the external
1344 reasoner is as trustworthy as the application requires. Another
1345 typical source of errors is the linkup between Isabelle and the
1346 external tool, not just its concrete implementation, but also the
1347 required translation between two different logical environments.
1349 Isabelle merely guarantees well-formedness of the propositions being
1350 asserted, and records within the internal derivation object how
1351 presumed theorems depend on unproven suppositions.
1354 @@{command oracle} @{syntax name} '=' @{syntax text}
1359 \item @{command "oracle"}~@{text "name = text"} turns the given ML
1360 expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
1361 ML function of type @{ML_text "'a -> thm"}, which is bound to the
1362 global identifier @{ML_text name}. This acts like an infinitary
1363 specification of axioms! Invoking the oracle only works within the
1364 scope of the resulting theory.
1368 See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
1369 defining a new primitive rule as oracle, and turning it into a proof
1374 section {* Name spaces *}
1377 \begin{matharray}{rcl}
1378 @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
1379 @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
1380 @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
1381 @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
1385 ( @{command hide_class} | @{command hide_type} |
1386 @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
1389 Isabelle organizes any kind of name declarations (of types,
1390 constants, theorems etc.) by separate hierarchically structured name
1391 spaces. Normally the user does not have to control the behavior of
1392 name spaces by hand, yet the following commands provide some way to
1397 \item @{command "hide_class"}~@{text names} fully removes class
1398 declarations from a given name space; with the @{text "(open)"}
1399 option, only the base name is hidden.
1401 Note that hiding name space accesses has no impact on logical
1402 declarations --- they remain valid internally. Entities that are no
1403 longer accessible to the user are printed with the special qualifier
1404 ``@{text "??"}'' prefixed to the full internal name.
1406 \item @{command "hide_type"}, @{command "hide_const"}, and @{command
1407 "hide_fact"} are similar to @{command "hide_class"}, but hide types,
1408 constants, and facts, respectively.