diff -r c04001b3a753 -r 12afbf6eb7f9 doc-src/IsarRef/Spec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Spec.thy Tue Aug 28 12:45:49 2012 +0200 @@ -0,0 +1,1337 @@ +theory Spec +imports Base Main +begin + +chapter {* Specifications *} + +text {* + The Isabelle/Isar theory format integrates specifications and + proofs, supporting interactive development with unlimited undo + operation. There is an integrated document preparation system (see + \chref{ch:document-prep}), for typesetting formal developments + together with informal text. The resulting hyper-linked PDF + documents can be used both for WWW presentation and printed copies. + + The Isar proof language (see \chref{ch:proofs}) is embedded into the + theory language as a proper sub-language. Proof mode is entered by + stating some @{command theorem} or @{command lemma} at the theory + level, and left again with the final conclusion (e.g.\ via @{command + qed}). Some theory specification mechanisms also require a proof, + such as @{command typedef} in HOL, which demands non-emptiness of + the representing sets. +*} + + +section {* Defining theories \label{sec:begin-thy} *} + +text {* + \begin{matharray}{rcl} + @{command_def "theory"} & : & @{text "toplevel \ theory"} \\ + @{command_def (global) "end"} & : & @{text "theory \ toplevel"} \\ + \end{matharray} + + Isabelle/Isar theories are defined via theory files, which may + contain both specifications and proofs; occasionally definitional + mechanisms also require some explicit proof. The theory body may be + sub-structured by means of \emph{local theory targets}, such as + @{command "locale"} and @{command "class"}. + + The first proper command of a theory is @{command "theory"}, which + indicates imports of previous theories and optional dependencies on + other source files (usually in ML). Just preceding the initial + @{command "theory"} command there may be an optional @{command + "header"} declaration, which is only relevant to document + preparation: see also the other section markup commands in + \secref{sec:markup}. + + A theory is concluded by a final @{command (global) "end"} command, + one that does not belong to a local theory target. No further + commands may follow such a global @{command (global) "end"}, + although some user-interfaces might pretend that trailing input is + admissible. + + @{rail " + @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin' + ; + imports: @'imports' (@{syntax name} +) + ; + keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and') + ; + uses: @'uses' ((@{syntax name} | @{syntax parname}) +) + "} + + \begin{description} + + \item @{command "theory"}~@{text "A \ B\<^sub>1 \ B\<^sub>n \"} + starts a new theory @{text A} based on the merge of existing + theories @{text "B\<^sub>1 \ B\<^sub>n"}. Due to the possibility to import more + than one ancestor, the resulting theory structure of an Isabelle + session forms a directed acyclic graph (DAG). Isabelle takes care + that sources contributing to the development graph are always + up-to-date: changed files are automatically rechecked whenever a + theory header specification is processed. + + The optional @{keyword_def "keywords"} specification declares outer + syntax (\chref{ch:outer-syntax}) that is introduced in this theory + later on (rare in end-user applications). Both minor keywords and + major keywords of the Isar command language need to be specified, in + order to make parsing of proof documents work properly. Command + keywords need to be classified according to their structural role in + the formal text. Examples may be seen in Isabelle/HOL sources + itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""} + @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim + "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations + with and without proof, respectively. Additional @{syntax tags} + provide defaults for document preparation (\secref{sec:tags}). + + The optional @{keyword_def "uses"} specification declares additional + dependencies on external files (notably ML sources). Files will be + loaded immediately (as ML), unless the name is parenthesized. The + latter case records a dependency that needs to be resolved later in + the text, usually via explicit @{command_ref "use"} for ML files; + other file formats require specific load commands defined by the + corresponding tools or packages. + + \item @{command (global) "end"} concludes the current theory + definition. Note that some other commands, e.g.\ local theory + targets @{command locale} or @{command class} may involve a + @{keyword "begin"} that needs to be matched by @{command (local) + "end"}, according to the usual rules for nested blocks. + + \end{description} +*} + + +section {* Local theory targets \label{sec:target} *} + +text {* + \begin{matharray}{rcll} + @{command_def "context"} & : & @{text "theory \ local_theory"} \\ + @{command_def (local) "end"} & : & @{text "local_theory \ theory"} \\ + \end{matharray} + + A local theory target is a context managed separately within the + enclosing theory. Contexts may introduce parameters (fixed + variables) and assumptions (hypotheses). Definitions and theorems + depending on the context may be added incrementally later on. + + \emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or + type classes (cf.\ \secref{sec:class}); the name ``@{text "-"}'' + signifies the global theory context. + + \emph{Unnamed contexts} may introduce additional parameters and + assumptions, and results produced in the context are generalized + accordingly. Such auxiliary contexts may be nested within other + targets, like @{command "locale"}, @{command "class"}, @{command + "instantiation"}, @{command "overloading"}. + + @{rail " + @@{command context} @{syntax nameref} @'begin' + ; + @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin' + ; + @{syntax_def target}: '(' @'in' @{syntax nameref} ')' + "} + + \begin{description} + + \item @{command "context"}~@{text "c \"} opens a named + context, by recommencing an existing locale or class @{text c}. + Note that locale and class definitions allow to include the + @{keyword "begin"} keyword as well, in order to continue the local + theory immediately after the initial specification. + + \item @{command "context"}~@{text "bundles elements \"} opens + an unnamed context, by extending the enclosing global or local + theory target by the given declaration bundles (\secref{sec:bundle}) + and context elements (@{text "\"}, @{text "\"} + etc.). This means any results stemming from definitions and proofs + in the extended context will be exported into the enclosing target + by lifting over extra parameters and premises. + + \item @{command (local) "end"} concludes the current local theory, + according to the nesting of contexts. Note that a global @{command + (global) "end"} has a different meaning: it concludes the theory + itself (\secref{sec:begin-thy}). + + \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any + local theory command specifies an immediate target, e.g.\ + ``@{command "definition"}~@{text "(\ c) \"}'' or ``@{command + "theorem"}~@{text "(\ c) \"}''. This works both in a local or + global theory context; the current target context will be suspended + for this command only. Note that ``@{text "(\ -)"}'' will + always produce a global result independently of the current target + context. + + \end{description} + + The exact meaning of results produced within a local theory context + depends on the underlying target infrastructure (locale, type class + etc.). The general idea is as follows, considering a context named + @{text c} with parameter @{text x} and assumption @{text "A[x]"}. + + Definitions are exported by introducing a global version with + additional arguments; a syntactic abbreviation links the long form + with the abstract version of the target context. For example, + @{text "a \ t[x]"} becomes @{text "c.a ?x \ t[?x]"} at the theory + level (for arbitrary @{text "?x"}), together with a local + abbreviation @{text "c \ c.a x"} in the target context (for the + fixed parameter @{text x}). + + Theorems are exported by discharging the assumptions and + generalizing the parameters of the context. For example, @{text "a: + B[x]"} becomes @{text "c.a: A[?x] \ B[?x]"}, again for arbitrary + @{text "?x"}. + + \medskip The Isabelle/HOL library contains numerous applications of + locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}. An + example for an unnamed auxiliary contexts is given in @{file + "~~/src/HOL/Isar_Examples/Group_Context.thy"}. *} + + +section {* Bundled declarations \label{sec:bundle} *} + +text {* + \begin{matharray}{rcl} + @{command_def "bundle"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ + @{command_def "include"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "including"} & : & @{text "proof(prove) \ proof(prove)"} \\ + @{keyword_def "includes"} & : & syntax \\ + \end{matharray} + + The outer syntax of fact expressions (\secref{sec:syn-att}) involves + theorems and attributes, which are evaluated in the context and + applied to it. Attributes may declare theorems to the context, as + in @{text "this_rule [intro] that_rule [elim]"} for example. + Configuration options (\secref{sec:config}) are special declaration + attributes that operate on the context without a theorem, as in + @{text "[[show_types = false]]"} for example. + + Expressions of this form may be defined as \emph{bundled + declarations} in the context, and included in other situations later + on. Including declaration bundles augments a local context casually + without logical dependencies, which is in contrast to locales and + locale interpretation (\secref{sec:locale}). + + @{rail " + @@{command bundle} @{syntax target}? \\ + @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))? + ; + (@@{command include} | @@{command including}) (@{syntax nameref}+) + ; + @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+) + "} + + \begin{description} + + \item @{command bundle}~@{text "b = decls"} defines a bundle of + declarations in the current context. The RHS is similar to the one + of the @{command declare} command. Bundles defined in local theory + targets are subject to transformations via morphisms, when moved + into different application contexts; this works analogously to any + other local theory specification. + + \item @{command print_bundles} prints the named bundles that are + available in the current context. + + \item @{command include}~@{text "b\<^sub>1 \ b\<^sub>n"} includes the declarations + from the given bundles into the current proof body context. This is + analogous to @{command "note"} (\secref{sec:proof-facts}) with the + expanded bundles. + + \item @{command including} is similar to @{command include}, but + works in proof refinement (backward mode). This is analogous to + @{command "using"} (\secref{sec:proof-facts}) with the expanded + bundles. + + \item @{keyword "includes"}~@{text "b\<^sub>1 \ b\<^sub>n"} is similar to + @{command include}, but works in situations where a specification + context is constructed, notably for @{command context} and long + statements of @{command theorem} etc. + + \end{description} + + Here is an artificial example of bundling various configuration + options: *} + +bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]] + +lemma "x = x" + including trace by metis + + +section {* Basic specification elements *} + +text {* + \begin{matharray}{rcll} + @{command_def "axiomatization"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + @{command_def "definition"} & : & @{text "local_theory \ local_theory"} \\ + @{attribute_def "defn"} & : & @{text attribute} \\ + @{command_def "abbreviation"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ + \end{matharray} + + These specification mechanisms provide a slightly more abstract view + than the underlying primitives of @{command "consts"}, @{command + "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see + \secref{sec:axms-thms}). In particular, type-inference is commonly + available, and result names need not be given. + + @{rail " + @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)? + ; + @@{command definition} @{syntax target}? \\ + (decl @'where')? @{syntax thmdecl}? @{syntax prop} + ; + @@{command abbreviation} @{syntax target}? @{syntax mode}? \\ + (decl @'where')? @{syntax prop} + ; + + @{syntax_def \"fixes\"}: ((@{syntax name} ('::' @{syntax type})? + @{syntax mixfix}? | @{syntax vars}) + @'and') + ; + specs: (@{syntax thmdecl}? @{syntax props} + @'and') + ; + decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? + "} + + \begin{description} + + \item @{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m \ \\<^sub>1 \ \\<^sub>n"} + introduces several constants simultaneously and states axiomatic + properties for these. The constants are marked as being specified + once and for all, which prevents additional specifications being + issued later on. + + Note that axiomatic specifications are only appropriate when + declaring a new logical system; axiomatic specifications are + restricted to global theory contexts. Normal applications should + only use definitional mechanisms! + + \item @{command "definition"}~@{text "c \ eq"} produces an + internal definition @{text "c \ t"} according to the specification + given as @{text eq}, which is then turned into a proven fact. The + given proposition may deviate from internal meta-level equality + according to the rewrite rules declared as @{attribute defn} by the + object-logic. This usually covers object-level equality @{text "x = + y"} and equivalence @{text "A \ B"}. End-users normally need not + change the @{attribute defn} setup. + + Definitions may be presented with explicit arguments on the LHS, as + well as additional conditions, e.g.\ @{text "f x y = t"} instead of + @{text "f \ \x y. t"} and @{text "y \ 0 \ g x y = u"} instead of an + unrestricted @{text "g \ \x y. u"}. + + \item @{command "abbreviation"}~@{text "c \ eq"} introduces a + syntactic constant which is associated with a certain term according + to the meta-level equality @{text eq}. + + Abbreviations participate in the usual type-inference process, but + are expanded before the logic ever sees them. Pretty printing of + terms involves higher-order rewriting with rules stemming from + reverted abbreviations. This needs some care to avoid overlapping + or looping syntactic replacements! + + The optional @{text mode} specification restricts output to a + particular print mode; using ``@{text input}'' here achieves the + effect of one-way abbreviations. The mode may also include an + ``@{keyword "output"}'' qualifier that affects the concrete syntax + declared for abbreviations, cf.\ @{command "syntax"} in + \secref{sec:syn-trans}. + + \item @{command "print_abbrevs"} prints all constant abbreviations + of the current context. + + \end{description} +*} + + +section {* Generic declarations *} + +text {* + \begin{matharray}{rcl} + @{command_def "declaration"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "syntax_declaration"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "declare"} & : & @{text "local_theory \ local_theory"} \\ + \end{matharray} + + Arbitrary operations on the background context may be wrapped-up as + generic declaration elements. Since the underlying concept of local + theories may be subject to later re-interpretation, there is an + additional dependency on a morphism that tells the difference of the + original declaration context wrt.\ the application context + encountered later on. A fact declaration is an important special + case: it consists of a theorem which is applied to the context by + means of an attribute. + + @{rail " + (@@{command declaration} | @@{command syntax_declaration}) + ('(' @'pervasive' ')')? \\ @{syntax target}? @{syntax text} + ; + @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and') + "} + + \begin{description} + + \item @{command "declaration"}~@{text d} adds the declaration + function @{text d} of ML type @{ML_type declaration}, to the current + local theory under construction. In later application contexts, the + function is transformed according to the morphisms being involved in + the interpretation hierarchy. + + If the @{text "(pervasive)"} option is given, the corresponding + declaration is applied to all possible contexts involved, including + the global background theory. + + \item @{command "syntax_declaration"} is similar to @{command + "declaration"}, but is meant to affect only ``syntactic'' tools by + convention (such as notation and type-checking information). + + \item @{command "declare"}~@{text thms} declares theorems to the + current local theory context. No theorem binding is involved here, + unlike @{command "theorems"} or @{command "lemmas"} (cf.\ + \secref{sec:axms-thms}), so @{command "declare"} only has the effect + of applying attributes as included in the theorem specification. + + \end{description} +*} + + +section {* Locales \label{sec:locale} *} + +text {* + Locales are parametric named local contexts, consisting of a list of + declaration elements that are modeled after the Isar proof context + commands (cf.\ \secref{sec:proof-context}). +*} + + +subsection {* Locale expressions \label{sec:locale-expr} *} + +text {* + A \emph{locale expression} denotes a structured context composed of + instances of existing locales. The context consists of a list of + instances of declaration elements from the locales. Two locale + instances are equal if they are of the same locale and the + parameters are instantiated with equivalent terms. Declaration + elements from equal instances are never repeated, thus avoiding + duplicate declarations. More precisely, declarations from instances + that are subsumed by earlier instances are omitted. + + @{rail " + @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))? + ; + instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts) + ; + qualifier: @{syntax name} ('?' | '!')? + ; + pos_insts: ('_' | @{syntax term})* + ; + named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and') + "} + + A locale instance consists of a reference to a locale and either + positional or named parameter instantiations. Identical + instantiations (that is, those that instante a parameter by itself) + may be omitted. The notation `@{text "_"}' enables to omit the + instantiation for a parameter inside a positional instantiation. + + Terms in instantiations are from the context the locale expressions + is declared in. Local names may be added to this context with the + optional @{keyword "for"} clause. This is useful for shadowing names + bound in outer contexts, and for declaring syntax. In addition, + syntax declarations from one instance are effective when parsing + subsequent instances of the same expression. + + Instances have an optional qualifier which applies to names in + declarations. Names include local definitions and theorem names. + If present, the qualifier itself is either optional + (``\texttt{?}''), which means that it may be omitted on input of the + qualified name, or mandatory (``\texttt{!}''). If neither + ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default + is used. For @{command "interpretation"} and @{command "interpret"} + the default is ``mandatory'', for @{command "locale"} and @{command + "sublocale"} the default is ``optional''. +*} + + +subsection {* Locale declarations *} + +text {* + \begin{matharray}{rcl} + @{command_def "locale"} & : & @{text "theory \ local_theory"} \\ + @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{method_def intro_locales} & : & @{text method} \\ + @{method_def unfold_locales} & : & @{text method} \\ + \end{matharray} + + \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} + \indexisarelem{defines}\indexisarelem{notes} + @{rail " + @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? + ; + @@{command print_locale} '!'? @{syntax nameref} + ; + @{syntax_def locale}: @{syntax context_elem}+ | + @{syntax locale_expr} ('+' (@{syntax context_elem}+))? + ; + @{syntax_def context_elem}: + @'fixes' (@{syntax \"fixes\"} + @'and') | + @'constrains' (@{syntax name} '::' @{syntax type} + @'and') | + @'assumes' (@{syntax props} + @'and') | + @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') | + @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and') + "} + + \begin{description} + + \item @{command "locale"}~@{text "loc = import + body"} defines a + new locale @{text loc} as a context consisting of a certain view of + existing locales (@{text import}) plus some additional elements + (@{text body}). Both @{text import} and @{text body} are optional; + the degenerate form @{command "locale"}~@{text loc} defines an empty + locale, which may still be useful to collect declarations of facts + later on. Type-inference on locale expressions automatically takes + care of the most general typing that the combined context elements + may acquire. + + The @{text import} consists of a structured locale expression; see + \secref{sec:proof-context} above. Its for clause defines the local + parameters of the @{text import}. In addition, locale parameters + whose instantance is omitted automatically extend the (possibly + empty) for clause: they are inserted at its beginning. This means + that these parameters may be referred to from within the expression + and also in the subsequent context elements and provides a + notational convenience for the inheritance of parameters in locale + declarations. + + The @{text body} consists of context elements. + + \begin{description} + + \item @{element "fixes"}~@{text "x :: \ (mx)"} declares a local + parameter of type @{text \} and mixfix annotation @{text mx} (both + are optional). The special syntax declaration ``@{text + "(\)"}'' means that @{text x} may be referenced + implicitly in this context. + + \item @{element "constrains"}~@{text "x :: \"} introduces a type + constraint @{text \} on the local parameter @{text x}. This + element is deprecated. The type constraint should be introduced in + the for clause or the relevant @{element "fixes"} element. + + \item @{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"} + introduces local premises, similar to @{command "assume"} within a + proof (cf.\ \secref{sec:proof-context}). + + \item @{element "defines"}~@{text "a: x \ t"} defines a previously + declared parameter. This is similar to @{command "def"} within a + proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} + takes an equational proposition instead of variable-term pair. The + left-hand side of the equation may have additional arguments, e.g.\ + ``@{element "defines"}~@{text "f x\<^sub>1 \ x\<^sub>n \ t"}''. + + \item @{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} + reconsiders facts within a local context. Most notably, this may + include arbitrary declarations in any attribute specifications + included here, e.g.\ a local @{attribute simp} rule. + + The initial @{text import} specification of a locale expression + maintains a dynamic relation to the locales being referenced + (benefiting from any later fact declarations in the obvious manner). + + \end{description} + + Note that ``@{text "(\ p\<^sub>1 \ p\<^sub>n)"}'' patterns given + in the syntax of @{element "assumes"} and @{element "defines"} above + are illegal in locale definitions. In the long goal format of + \secref{sec:goals}, term bindings may be included as expected, + though. + + \medskip Locale specifications are ``closed up'' by + turning the given text into a predicate definition @{text + loc_axioms} and deriving the original assumptions as local lemmas + (modulo local definitions). The predicate statement covers only the + newly specified assumptions, omitting the content of included locale + expressions. The full cumulative view is only provided on export, + involving another predicate @{text loc} that refers to the complete + specification text. + + In any case, the predicate arguments are those locale parameters + that actually occur in the respective piece of text. Also note that + these predicates operate at the meta-level in theory, but the locale + packages attempts to internalize statements according to the + object-logic setup (e.g.\ replacing @{text \} by @{text \}, and + @{text "\"} by @{text "\"} in HOL; see also + \secref{sec:object-logic}). Separate introduction rules @{text + loc_axioms.intro} and @{text loc.intro} are provided as well. + + \item @{command "print_locale"}~@{text "locale"} prints the + contents of the named locale. The command omits @{element "notes"} + elements by default. Use @{command "print_locale"}@{text "!"} to + have them included. + + \item @{command "print_locales"} prints the names of all locales + of the current theory. + + \item @{method intro_locales} and @{method unfold_locales} + repeatedly expand all introduction rules of locale predicates of the + theory. While @{method intro_locales} only applies the @{text + loc.intro} introduction rules and therefore does not decend to + assumptions, @{method unfold_locales} is more aggressive and applies + @{text loc_axioms.intro} as well. Both methods are aware of locale + specifications entailed by the context, both from target statements, + and from interpretations (see below). New goals that are entailed + by the current context are discharged automatically. + + \end{description} +*} + + +subsection {* Locale interpretation *} + +text {* + \begin{matharray}{rcl} + @{command_def "interpretation"} & : & @{text "theory \ proof(prove)"} \\ + @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ + @{command_def "sublocale"} & : & @{text "theory \ proof(prove)"} \\ + @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + \end{matharray} + + Locale expressions may be instantiated, and the instantiated facts + added to the current context. This requires a proof of the + instantiated specification and is called \emph{locale + interpretation}. Interpretation is possible in locales (command + @{command "sublocale"}), theories (command @{command + "interpretation"}) and also within proof bodies (command @{command + "interpret"}). + + @{rail " + @@{command interpretation} @{syntax locale_expr} equations? + ; + @@{command interpret} @{syntax locale_expr} equations? + ; + @@{command sublocale} @{syntax nameref} ('<' | '\') @{syntax locale_expr} \\ + equations? + ; + @@{command print_dependencies} '!'? @{syntax locale_expr} + ; + @@{command print_interps} @{syntax nameref} + ; + + equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') + "} + + \begin{description} + + \item @{command "interpretation"}~@{text "expr \ eqns"} + interprets @{text expr} in the theory. The command generates proof + obligations for the instantiated specifications (assumes and defines + elements). Once these are discharged by the user, instantiated + facts are added to the theory in a post-processing phase. + + Free variables in the interpreted expression are allowed. They are + turned into schematic variables in the generated declarations. In + order to use a free variable whose name is already bound in the + context --- for example, because a constant of that name exists --- + it may be added to the @{keyword "for"} clause. + + Additional equations, which are unfolded during + post-processing, may be given after the keyword @{keyword "where"}. + This is useful for interpreting concepts introduced through + definitions. The equations must be proved. + + The command is aware of interpretations already active in the + theory, but does not simplify the goal automatically. In order to + simplify the proof obligations use methods @{method intro_locales} + or @{method unfold_locales}. Post-processing is not applied to + facts of interpretations that are already active. This avoids + duplication of interpreted facts, in particular. Note that, in the + case of a locale with import, parts of the interpretation may + already be active. The command will only process facts for new + parts. + + Adding facts to locales has the effect of adding interpreted facts + to the theory for all interpretations as well. That is, + interpretations dynamically participate in any facts added to + locales. Note that if a theory inherits additional facts for a + locale through one parent and an interpretation of that locale + through another parent, the additional facts will not be + interpreted. + + \item @{command "interpret"}~@{text "expr \ eqns"} interprets + @{text expr} in the proof context and is otherwise similar to + interpretation in theories. Note that rewrite rules given to + @{command "interpret"} after the @{keyword "where"} keyword should be + explicitly universally quantified. + + \item @{command "sublocale"}~@{text "name \ expr \ + eqns"} + interprets @{text expr} in the locale @{text name}. A proof that + the specification of @{text name} implies the specification of + @{text expr} is required. As in the localized version of the + theorem command, the proof is in the context of @{text name}. After + the proof obligation has been discharged, the facts of @{text expr} + become part of locale @{text name} as \emph{derived} context + elements and are available when the context @{text name} is + subsequently entered. Note that, like import, this is dynamic: + facts added to a locale part of @{text expr} after interpretation + become also available in @{text name}. + + Only specification fragments of @{text expr} that are not already + part of @{text name} (be it imported, derived or a derived fragment + of the import) are considered in this process. This enables + circular interpretations provided that no infinite chains are + generated in the locale hierarchy. + + If interpretations of @{text name} exist in the current theory, the + command adds interpretations for @{text expr} as well, with the same + qualifier, although only for fragments of @{text expr} that are not + interpreted in the theory already. + + Equations given after @{keyword "where"} amend the morphism through + which @{text expr} is interpreted. This enables to map definitions + from the interpreted locales to entities of @{text name}. This + feature is experimental. + + \item @{command "print_dependencies"}~@{text "expr"} is useful for + understanding the effect of an interpretation of @{text "expr"}. It + lists all locale instances for which interpretations would be added + to the current context. Variant @{command + "print_dependencies"}@{text "!"} prints all locale instances that + would be considered for interpretation, and would be interpreted in + an empty context (that is, without interpretations). + + \item @{command "print_interps"}~@{text "locale"} lists all + interpretations of @{text "locale"} in the current theory or proof + context, including those due to a combination of a @{command + "interpretation"} or @{command "interpret"} and one or several + @{command "sublocale"} declarations. + + \end{description} + + \begin{warn} + Since attributes are applied to interpreted theorems, + interpretation may modify the context of common proof tools, e.g.\ + the Simplifier or Classical Reasoner. As the behavior of such + tools is \emph{not} stable under interpretation morphisms, manual + declarations might have to be added to the target context of the + interpretation to revert such declarations. + \end{warn} + + \begin{warn} + An interpretation in a theory or proof context may subsume previous + interpretations. This happens if the same specification fragment + is interpreted twice and the instantiation of the second + interpretation is more general than the interpretation of the + first. The locale package does not attempt to remove subsumed + interpretations. + \end{warn} +*} + + +section {* Classes \label{sec:class} *} + +text {* + \begin{matharray}{rcl} + @{command_def "class"} & : & @{text "theory \ local_theory"} \\ + @{command_def "instantiation"} & : & @{text "theory \ local_theory"} \\ + @{command_def "instance"} & : & @{text "local_theory \ local_theory"} \\ + @{command "instance"} & : & @{text "theory \ proof(prove)"} \\ + @{command_def "subclass"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{method_def intro_classes} & : & @{text method} \\ + \end{matharray} + + A class is a particular locale with \emph{exactly one} type variable + @{text \}. Beyond the underlying locale, a corresponding type class + is established which is interpreted logically as axiomatic type + class \cite{Wenzel:1997:TPHOL} whose logical content are the + assumptions of the locale. Thus, classes provide the full + generality of locales combined with the commodity of type classes + (notably type-inference). See \cite{isabelle-classes} for a short + tutorial. + + @{rail " + @@{command class} class_spec @'begin'? + ; + class_spec: @{syntax name} '=' + ((@{syntax nameref} '+' (@{syntax context_elem}+)) | + @{syntax nameref} | (@{syntax context_elem}+)) + ; + @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin' + ; + @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} | + @{syntax nameref} ('<' | '\') @{syntax nameref} ) + ; + @@{command subclass} @{syntax target}? @{syntax nameref} + "} + + \begin{description} + + \item @{command "class"}~@{text "c = superclasses + body"} defines + a new class @{text c}, inheriting from @{text superclasses}. This + introduces a locale @{text c} with import of all locales @{text + superclasses}. + + Any @{element "fixes"} in @{text body} are lifted to the global + theory level (\emph{class operations} @{text "f\<^sub>1, \, + f\<^sub>n"} of class @{text c}), mapping the local type parameter + @{text \} to a schematic type variable @{text "?\ :: c"}. + + Likewise, @{element "assumes"} in @{text body} are also lifted, + mapping each local parameter @{text "f :: \[\]"} to its + corresponding global constant @{text "f :: \[?\ :: c]"}. The + corresponding introduction rule is provided as @{text + c_class_axioms.intro}. This rule should be rarely needed directly + --- the @{method intro_classes} method takes care of the details of + class membership proofs. + + \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n)s + \"} opens a theory target (cf.\ \secref{sec:target}) which + allows to specify class operations @{text "f\<^sub>1, \, f\<^sub>n"} corresponding + to sort @{text s} at the particular type instance @{text "(\\<^sub>1 :: s\<^sub>1, + \, \\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the + target body poses a goal stating these type arities. The target is + concluded by an @{command_ref (local) "end"} command. + + Note that a list of simultaneous type constructors may be given; + this corresponds nicely to mutually recursive type definitions, e.g.\ + in Isabelle/HOL. + + \item @{command "instance"} in an instantiation target body sets + up a goal stating the type arities claimed at the opening @{command + "instantiation"}. The proof would usually proceed by @{method + intro_classes}, and then establish the characteristic theorems of + the type classes involved. After finishing the proof, the + background theory will be augmented by the proven type arities. + + On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \, + s\<^sub>n)s"} provides a convenient way to instantiate a type class with no + need to specify operations: one can continue with the + instantiation proof immediately. + + \item @{command "subclass"}~@{text c} in a class context for class + @{text d} sets up a goal stating that class @{text c} is logically + contained in class @{text d}. After finishing the proof, class + @{text d} is proven to be subclass @{text c} and the locale @{text + c} is interpreted into @{text d} simultaneously. + + A weakend form of this is available through a further variant of + @{command instance}: @{command instance}~@{text "c\<^sub>1 \ c\<^sub>2"} opens + a proof that class @{text "c\<^isub>2"} implies @{text "c\<^isub>1"} without reference + to the underlying locales; this is useful if the properties to prove + the logical connection are not sufficent on the locale level but on + the theory level. + + \item @{command "print_classes"} prints all classes in the current + theory. + + \item @{command "class_deps"} visualizes all classes and their + subclass relations as a Hasse diagram. + + \item @{method intro_classes} repeatedly expands all class + introduction rules of this theory. Note that this method usually + needs not be named explicitly, as it is already included in the + default proof step (e.g.\ of @{command "proof"}). In particular, + instantiation of trivial (syntactic) classes may be performed by a + single ``@{command ".."}'' proof step. + + \end{description} +*} + + +subsection {* The class target *} + +text {* + %FIXME check + + A named context may refer to a locale (cf.\ \secref{sec:target}). + If this locale is also a class @{text c}, apart from the common + locale target behaviour the following happens. + + \begin{itemize} + + \item Local constant declarations @{text "g[\]"} referring to the + local type parameter @{text \} and local parameters @{text "f[\]"} + are accompanied by theory-level constants @{text "g[?\ :: c]"} + referring to theory-level class operations @{text "f[?\ :: c]"}. + + \item Local theorem bindings are lifted as are assumptions. + + \item Local syntax refers to local operations @{text "g[\]"} and + global operations @{text "g[?\ :: c]"} uniformly. Type inference + resolves ambiguities. In rare cases, manual type annotations are + needed. + + \end{itemize} +*} + + +subsection {* Co-regularity of type classes and arities *} + +text {* The class relation together with the collection of + type-constructor arities must obey the principle of + \emph{co-regularity} as defined below. + + \medskip For the subsequent formulation of co-regularity we assume + that the class relation is closed by transitivity and reflexivity. + Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is + completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \ c'"} + implies @{text "t :: (\<^vec>s)c'"} for all such declarations. + + Treating sorts as finite sets of classes (meaning the intersection), + the class relation @{text "c\<^sub>1 \ c\<^sub>2"} is extended to sorts as + follows: + \[ + @{text "s\<^sub>1 \ s\<^sub>2 \ \c\<^sub>2 \ s\<^sub>2. \c\<^sub>1 \ s\<^sub>1. c\<^sub>1 \ c\<^sub>2"} + \] + + This relation on sorts is further extended to tuples of sorts (of + the same length) in the component-wise way. + + \smallskip Co-regularity of the class relation together with the + arities relation means: + \[ + @{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \ t :: (\<^vec>s\<^sub>2)c\<^sub>2 \ c\<^sub>1 \ c\<^sub>2 \ \<^vec>s\<^sub>1 \ \<^vec>s\<^sub>2"} + \] + \noindent for all such arities. In other words, whenever the result + classes of some type-constructor arities are related, then the + argument sorts need to be related in the same way. + + \medskip Co-regularity is a very fundamental property of the + order-sorted algebra of types. For example, it entails principle + types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}. +*} + + +section {* Unrestricted overloading *} + +text {* + \begin{matharray}{rcl} + @{command_def "overloading"} & : & @{text "theory \ local_theory"} \\ + \end{matharray} + + Isabelle/Pure's definitional schemes support certain forms of + overloading (see \secref{sec:consts}). Overloading means that a + constant being declared as @{text "c :: \ decl"} may be + defined separately on type instances + @{text "c :: (\\<^sub>1, \, \\<^sub>n) t decl"} + for each type constructor @{text t}. At most occassions + overloading will be used in a Haskell-like fashion together with + type classes by means of @{command "instantiation"} (see + \secref{sec:class}). Sometimes low-level overloading is desirable. + The @{command "overloading"} target provides a convenient view for + end-users. + + @{rail " + @@{command overloading} ( spec + ) @'begin' + ; + spec: @{syntax name} ( '==' | '\' ) @{syntax term} ( '(' @'unchecked' ')' )? + "} + + \begin{description} + + \item @{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"} + opens a theory target (cf.\ \secref{sec:target}) which allows to + specify constants with overloaded definitions. These are identified + by an explicitly given mapping from variable names @{text "x\<^sub>i"} to + constants @{text "c\<^sub>i"} at particular type instances. The + definitions themselves are established using common specification + tools, using the names @{text "x\<^sub>i"} as reference to the + corresponding constants. The target is concluded by @{command + (local) "end"}. + + A @{text "(unchecked)"} option disables global dependency checks for + the corresponding definition, which is occasionally useful for + exotic overloading (see \secref{sec:consts} for a precise description). + It is at the discretion of the user to avoid + malformed theory specifications! + + \end{description} +*} + + +section {* Incorporating ML code \label{sec:ML} *} + +text {* + \begin{matharray}{rcl} + @{command_def "ML_file"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "ML"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "ML_prf"} & : & @{text "proof \ proof"} \\ + @{command_def "ML_val"} & : & @{text "any \"} \\ + @{command_def "ML_command"} & : & @{text "any \"} \\ + @{command_def "setup"} & : & @{text "theory \ theory"} \\ + @{command_def "local_setup"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "attribute_setup"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + @{rail " + @@{command ML_file} @{syntax name} + ; + (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | + @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} + ; + @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? + "} + + \begin{description} + + \item @{command "ML_file"}~@{text "name"} reads and evaluates the + given ML file. The current theory context is passed down to the ML + toplevel and may be modified, using @{ML "Context.>>"} or derived ML + commands. Top-level ML bindings are stored within the (global or + local) theory context. + + \item @{command "ML"}~@{text "text"} is similar to @{command + "ML_file"}, but evaluates directly the given @{text "text"}. + Top-level ML bindings are stored within the (global or local) theory + context. + + \item @{command "ML_prf"} is analogous to @{command "ML"} but works + within a proof context. Top-level ML bindings are stored within the + proof context in a purely sequential fashion, disregarding the + nested proof structure. ML bindings introduced by @{command + "ML_prf"} are discarded at the end of the proof. + + \item @{command "ML_val"} and @{command "ML_command"} are diagnostic + versions of @{command "ML"}, which means that the context may not be + updated. @{command "ML_val"} echos the bindings produced at the ML + toplevel, but @{command "ML_command"} is silent. + + \item @{command "setup"}~@{text "text"} changes the current theory + context by applying @{text "text"}, which refers to an ML expression + of type @{ML_type "theory -> theory"}. This enables to initialize + any object-logic specific tools and packages written in ML, for + example. + + \item @{command "local_setup"} is similar to @{command "setup"} for + a local theory context, and an ML expression of type @{ML_type + "local_theory -> local_theory"}. This allows to + invoke local theory specification packages without going through + concrete outer syntax, for example. + + \item @{command "attribute_setup"}~@{text "name = text description"} + defines an attribute in the current theory. The given @{text + "text"} has to be an ML expression of type + @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in + structure @{ML_struct Args} and @{ML_struct Attrib}. + + In principle, attributes can operate both on a given theorem and the + implicit context, although in practice only one is modified and the + other serves as parameter. Here are examples for these two cases: + + \end{description} +*} + + attribute_setup my_rule = {* + Attrib.thms >> (fn ths => + Thm.rule_attribute + (fn context: Context.generic => fn th: thm => + let val th' = th OF ths + in th' end)) *} + + attribute_setup my_declaration = {* + Attrib.thms >> (fn ths => + Thm.declaration_attribute + (fn th: thm => fn context: Context.generic => + let val context' = context + in context' end)) *} + + +section {* Primitive specification elements *} + +subsection {* Type classes and sorts \label{sec:classes} *} + +text {* + \begin{matharray}{rcll} + @{command_def "classes"} & : & @{text "theory \ theory"} \\ + @{command_def "classrel"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + @{command_def "default_sort"} & : & @{text "local_theory \ local_theory"} + \end{matharray} + + @{rail " + @@{command classes} (@{syntax classdecl} +) + ; + @@{command classrel} (@{syntax nameref} ('<' | '\') @{syntax nameref} + @'and') + ; + @@{command default_sort} @{syntax sort} + "} + + \begin{description} + + \item @{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"} declares class + @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \, c\<^sub>n"}. + Isabelle implicitly maintains the transitive closure of the class + hierarchy. Cyclic class structures are not permitted. + + \item @{command "classrel"}~@{text "c\<^sub>1 \ c\<^sub>2"} states subclass + relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}. + This is done axiomatically! The @{command_ref "subclass"} and + @{command_ref "instance"} commands (see \secref{sec:class}) provide + a way to introduce proven class relations. + + \item @{command "default_sort"}~@{text s} makes sort @{text s} the + new default sort for any type variable that is given explicitly in + the text, but lacks a sort constraint (wrt.\ the current context). + Type variables generated by type inference are not affected. + + Usually the default sort is only changed when defining a new + object-logic. For example, the default sort in Isabelle/HOL is + @{class type}, the class of all HOL types. + + When merging theories, the default sorts of the parents are + logically intersected, i.e.\ the representations as lists of classes + are joined. + + \end{description} +*} + + +subsection {* Types and type abbreviations \label{sec:types-pure} *} + +text {* + \begin{matharray}{rcll} + @{command_def "type_synonym"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "typedecl"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + \end{matharray} + + @{rail " + @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?) + ; + @@{command typedecl} @{syntax typespec} @{syntax mixfix}? + ; + @@{command arities} (@{syntax nameref} '::' @{syntax arity} +) + "} + + \begin{description} + + \item @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} + introduces a \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the + existing type @{text "\"}. Unlike actual type definitions, as are + available in Isabelle/HOL for example, type synonyms are merely + syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. + + \item @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} declares a new + type constructor @{text t}. If the object-logic defines a base sort + @{text s}, then the constructor is declared to operate on that, via + the axiomatic specification @{command arities}~@{text "t :: (s, \, + s)s"}. + + \item @{command "arities"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n)s"} augments + Isabelle's order-sorted signature of types by new type constructor + arities. This is done axiomatically! The @{command_ref "instantiation"} + target (see \secref{sec:class}) provides a way to introduce + proven type arities. + + \end{description} +*} + + +subsection {* Constants and definitions \label{sec:consts} *} + +text {* + \begin{matharray}{rcl} + @{command_def "consts"} & : & @{text "theory \ theory"} \\ + @{command_def "defs"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + Definitions essentially express abbreviations within the logic. The + simplest form of a definition is @{text "c :: \ \ t"}, where @{text + c} is a newly declared constant. Isabelle also allows derived forms + where the arguments of @{text c} appear on the left, abbreviating a + prefix of @{text \}-abstractions, e.g.\ @{text "c \ \x y. t"} may be + written more conveniently as @{text "c x y \ t"}. Moreover, + definitions may be weakened by adding arbitrary pre-conditions: + @{text "A \ c x y \ t"}. + + \medskip The built-in well-formedness conditions for definitional + specifications are: + + \begin{itemize} + + \item Arguments (on the left-hand side) must be distinct variables. + + \item All variables on the right-hand side must also appear on the + left-hand side. + + \item All type variables on the right-hand side must also appear on + the left-hand side; this prohibits @{text "0 :: nat \ length ([] :: + \ list)"} for example. + + \item The definition must not be recursive. Most object-logics + provide definitional principles that can be used to express + recursion safely. + + \end{itemize} + + The right-hand side of overloaded definitions may mention overloaded constants + recursively at type instances corresponding to the immediate + argument types @{text "\\<^sub>1, \, \\<^sub>n"}. Incomplete + specification patterns impose global constraints on all occurrences, + e.g.\ @{text "d :: \ \ \"} on the left-hand side means that all + corresponding occurrences on some right-hand side need to be an + instance of this, general @{text "d :: \ \ \"} will be disallowed. + + @{rail " + @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +) + ; + @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +) + ; + opt: '(' @'unchecked'? @'overloaded'? ')' + "} + + \begin{description} + + \item @{command "consts"}~@{text "c :: \"} declares constant @{text + c} to have any instance of type scheme @{text \}. The optional + mixfix annotations may attach concrete syntax to the constants + declared. + + \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn} + as a definitional axiom for some existing constant. + + The @{text "(unchecked)"} option disables global dependency checks + for this definition, which is occasionally useful for exotic + overloading. It is at the discretion of the user to avoid malformed + theory specifications! + + The @{text "(overloaded)"} option declares definitions to be + potentially overloaded. Unless this option is given, a warning + message would be issued for any definitional equation with a more + special type than that of the corresponding constant declaration. + + \end{description} +*} + + +section {* Axioms and theorems \label{sec:axms-thms} *} + +text {* + \begin{matharray}{rcll} + @{command_def "axioms"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + @{command_def "lemmas"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "theorems"} & : & @{text "local_theory \ local_theory"} \\ + \end{matharray} + + @{rail " + @@{command axioms} (@{syntax axmdecl} @{syntax prop} +) + ; + (@@{command lemmas} | @@{command theorems}) @{syntax target}? \\ + (@{syntax thmdef}? @{syntax thmrefs} + @'and') + (@'for' (@{syntax vars} + @'and'))? + "} + + \begin{description} + + \item @{command "axioms"}~@{text "a: \"} introduces arbitrary + statements as axioms of the meta-logic. In fact, axioms are + ``axiomatic theorems'', and may be referred later just as any other + theorem. + + Axioms are usually only introduced when declaring new logical + systems. Everyday work is typically done the hard way, with proper + definitions and proven theorems. + + \item @{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}~@{keyword_def + "for"}~@{text "x\<^sub>1 \ x\<^sub>m"} evaluates given facts (with attributes) in + the current context, which may be augmented by local variables. + Results are standardized before being stored, i.e.\ schematic + variables are renamed to enforce index @{text "0"} uniformly. + + \item @{command "theorems"} is the same as @{command "lemmas"}, but + marks the result as a different kind of facts. + + \end{description} +*} + + +section {* Oracles *} + +text {* + \begin{matharray}{rcll} + @{command_def "oracle"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + \end{matharray} + + Oracles allow Isabelle to take advantage of external reasoners such + as arithmetic decision procedures, model checkers, fast tautology + checkers or computer algebra systems. Invoked as an oracle, an + external reasoner can create arbitrary Isabelle theorems. + + It is the responsibility of the user to ensure that the external + reasoner is as trustworthy as the application requires. Another + typical source of errors is the linkup between Isabelle and the + external tool, not just its concrete implementation, but also the + required translation between two different logical environments. + + Isabelle merely guarantees well-formedness of the propositions being + asserted, and records within the internal derivation object how + presumed theorems depend on unproven suppositions. + + @{rail " + @@{command oracle} @{syntax name} '=' @{syntax text} + "} + + \begin{description} + + \item @{command "oracle"}~@{text "name = text"} turns the given ML + expression @{text "text"} of type @{ML_text "'a -> cterm"} into an + ML function of type @{ML_text "'a -> thm"}, which is bound to the + global identifier @{ML_text name}. This acts like an infinitary + specification of axioms! Invoking the oracle only works within the + scope of the resulting theory. + + \end{description} + + See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of + defining a new primitive rule as oracle, and turning it into a proof + method. +*} + + +section {* Name spaces *} + +text {* + \begin{matharray}{rcl} + @{command_def "hide_class"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_type"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_const"} & : & @{text "theory \ theory"} \\ + @{command_def "hide_fact"} & : & @{text "theory \ theory"} \\ + \end{matharray} + + @{rail " + ( @{command hide_class} | @{command hide_type} | + @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + ) + "} + + Isabelle organizes any kind of name declarations (of types, + constants, theorems etc.) by separate hierarchically structured name + spaces. Normally the user does not have to control the behavior of + name spaces by hand, yet the following commands provide some way to + do so. + + \begin{description} + + \item @{command "hide_class"}~@{text names} fully removes class + declarations from a given name space; with the @{text "(open)"} + option, only the base name is hidden. + + Note that hiding name space accesses has no impact on logical + declarations --- they remain valid internally. Entities that are no + longer accessible to the user are printed with the special qualifier + ``@{text "??"}'' prefixed to the full internal name. + + \item @{command "hide_type"}, @{command "hide_const"}, and @{command + "hide_fact"} are similar to @{command "hide_class"}, but hide types, + constants, and facts, respectively. + + \end{description} +*} + +end