doc-src/IsarRef/Thy/Spec.thy
author wenzelm
Wed Mar 11 23:59:34 2009 +0100 (2009-03-11 ago)
changeset 30461 00323c45ea83
parent 30242 aea5d7fa7ef5
child 30526 7f9a9ec1c94d
permissions -rw-r--r--
added 'local_setup' command;
tuned;
     1 theory Spec
     2 imports Main
     3 begin
     4 
     5 chapter {* Theory specifications *}
     6 
     7 text {*
     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.
    14 
    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.
    22 *}
    23 
    24 
    25 section {* Defining theories \label{sec:begin-thy} *}
    26 
    27 text {*
    28   \begin{matharray}{rcl}
    29     @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
    30     @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
    31   \end{matharray}
    32 
    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"}.
    38 
    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
    45   \secref{sec:markup}.
    46 
    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
    51   admissible.
    52 
    53   \begin{rail}
    54     'theory' name 'imports' (name +) uses? 'begin'
    55     ;
    56 
    57     uses: 'uses' ((name | parname) +);
    58   \end{rail}
    59 
    60   \begin{description}
    61 
    62   \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
    63   starts a new theory @{text A} based on the merge of existing
    64   theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
    65   
    66   Due to the possibility to import more than one ancestor, the
    67   resulting theory structure of an Isabelle session forms a directed
    68   acyclic graph (DAG).  Isabelle's theory loader ensures that the
    69   sources contributing to the development graph are always up-to-date:
    70   changed files are automatically reloaded whenever a theory header
    71   specification is processed.
    72   
    73   The optional @{keyword_def "uses"} specification declares additional
    74   dependencies on extra files (usually ML sources).  Files will be
    75   loaded immediately (as ML), unless the name is parenthesized.  The
    76   latter case records a dependency that needs to be resolved later in
    77   the text, usually via explicit @{command_ref "use"} for ML files;
    78   other file formats require specific load commands defined by the
    79   corresponding tools or packages.
    80   
    81   \item @{command (global) "end"} concludes the current theory
    82   definition.  Note that local theory targets involve a local
    83   @{command (local) "end"}, which is clear from the nesting.
    84 
    85   \end{description}
    86 *}
    87 
    88 
    89 section {* Local theory targets \label{sec:target} *}
    90 
    91 text {*
    92   A local theory target is a context managed separately within the
    93   enclosing theory.  Contexts may introduce parameters (fixed
    94   variables) and assumptions (hypotheses).  Definitions and theorems
    95   depending on the context may be added incrementally later on.  Named
    96   contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
    97   (cf.\ \secref{sec:class}); the name ``@{text "-"}'' signifies the
    98   global theory context.
    99 
   100   \begin{matharray}{rcll}
   101     @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
   102     @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
   103   \end{matharray}
   104 
   105   \indexouternonterm{target}
   106   \begin{rail}
   107     'context' name 'begin'
   108     ;
   109 
   110     target: '(' 'in' name ')'
   111     ;
   112   \end{rail}
   113 
   114   \begin{description}
   115   
   116   \item @{command "context"}~@{text "c \<BEGIN>"} recommences an
   117   existing locale or class context @{text c}.  Note that locale and
   118   class definitions allow to include the @{keyword "begin"} keyword as
   119   well, in order to continue the local theory immediately after the
   120   initial specification.
   121   
   122   \item @{command (local) "end"} concludes the current local theory
   123   and continues the enclosing global theory.  Note that a global
   124   @{command (global) "end"} has a different meaning: it concludes the
   125   theory itself (\secref{sec:begin-thy}).
   126   
   127   \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
   128   local theory command specifies an immediate target, e.g.\
   129   ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
   130   "theorem"}~@{text "(\<IN> c) \<dots>"}''.  This works both in a local or
   131   global theory context; the current target context will be suspended
   132   for this command only.  Note that ``@{text "(\<IN> -)"}'' will
   133   always produce a global result independently of the current target
   134   context.
   135 
   136   \end{description}
   137 
   138   The exact meaning of results produced within a local theory context
   139   depends on the underlying target infrastructure (locale, type class
   140   etc.).  The general idea is as follows, considering a context named
   141   @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
   142   
   143   Definitions are exported by introducing a global version with
   144   additional arguments; a syntactic abbreviation links the long form
   145   with the abstract version of the target context.  For example,
   146   @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
   147   level (for arbitrary @{text "?x"}), together with a local
   148   abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
   149   fixed parameter @{text x}).
   150 
   151   Theorems are exported by discharging the assumptions and
   152   generalizing the parameters of the context.  For example, @{text "a:
   153   B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
   154   @{text "?x"}.
   155 *}
   156 
   157 
   158 section {* Basic specification elements *}
   159 
   160 text {*
   161   \begin{matharray}{rcll}
   162     @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
   163     @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   164     @{attribute_def "defn"} & : & @{text attribute} \\
   165     @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   166     @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
   167   \end{matharray}
   168 
   169   These specification mechanisms provide a slightly more abstract view
   170   than the underlying primitives of @{command "consts"}, @{command
   171   "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
   172   \secref{sec:axms-thms}).  In particular, type-inference is commonly
   173   available, and result names need not be given.
   174 
   175   \begin{rail}
   176     'axiomatization' target? fixes? ('where' specs)?
   177     ;
   178     'definition' target? (decl 'where')? thmdecl? prop
   179     ;
   180     'abbreviation' target? mode? (decl 'where')? prop
   181     ;
   182 
   183     fixes: ((name ('::' type)? mixfix? | vars) + 'and')
   184     ;
   185     specs: (thmdecl? props + 'and')
   186     ;
   187     decl: name ('::' type)? mixfix?
   188     ;
   189   \end{rail}
   190 
   191   \begin{description}
   192   
   193   \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
   194   introduces several constants simultaneously and states axiomatic
   195   properties for these.  The constants are marked as being specified
   196   once and for all, which prevents additional specifications being
   197   issued later on.
   198   
   199   Note that axiomatic specifications are only appropriate when
   200   declaring a new logical system; axiomatic specifications are
   201   restricted to global theory contexts.  Normal applications should
   202   only use definitional mechanisms!
   203 
   204   \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
   205   internal definition @{text "c \<equiv> t"} according to the specification
   206   given as @{text eq}, which is then turned into a proven fact.  The
   207   given proposition may deviate from internal meta-level equality
   208   according to the rewrite rules declared as @{attribute defn} by the
   209   object-logic.  This usually covers object-level equality @{text "x =
   210   y"} and equivalence @{text "A \<leftrightarrow> B"}.  End-users normally need not
   211   change the @{attribute defn} setup.
   212   
   213   Definitions may be presented with explicit arguments on the LHS, as
   214   well as additional conditions, e.g.\ @{text "f x y = t"} instead of
   215   @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
   216   unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
   217   
   218   \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
   219   syntactic constant which is associated with a certain term according
   220   to the meta-level equality @{text eq}.
   221   
   222   Abbreviations participate in the usual type-inference process, but
   223   are expanded before the logic ever sees them.  Pretty printing of
   224   terms involves higher-order rewriting with rules stemming from
   225   reverted abbreviations.  This needs some care to avoid overlapping
   226   or looping syntactic replacements!
   227   
   228   The optional @{text mode} specification restricts output to a
   229   particular print mode; using ``@{text input}'' here achieves the
   230   effect of one-way abbreviations.  The mode may also include an
   231   ``@{keyword "output"}'' qualifier that affects the concrete syntax
   232   declared for abbreviations, cf.\ @{command "syntax"} in
   233   \secref{sec:syn-trans}.
   234   
   235   \item @{command "print_abbrevs"} prints all constant abbreviations
   236   of the current context.
   237   
   238   \end{description}
   239 *}
   240 
   241 
   242 section {* Generic declarations *}
   243 
   244 text {*
   245   Arbitrary operations on the background context may be wrapped-up as
   246   generic declaration elements.  Since the underlying concept of local
   247   theories may be subject to later re-interpretation, there is an
   248   additional dependency on a morphism that tells the difference of the
   249   original declaration context wrt.\ the application context
   250   encountered later on.  A fact declaration is an important special
   251   case: it consists of a theorem which is applied to the context by
   252   means of an attribute.
   253 
   254   \begin{matharray}{rcl}
   255     @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   256     @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   257   \end{matharray}
   258 
   259   \begin{rail}
   260     'declaration' target? text
   261     ;
   262     'declare' target? (thmrefs + 'and')
   263     ;
   264   \end{rail}
   265 
   266   \begin{description}
   267 
   268   \item @{command "declaration"}~@{text d} adds the declaration
   269   function @{text d} of ML type @{ML_type declaration}, to the current
   270   local theory under construction.  In later application contexts, the
   271   function is transformed according to the morphisms being involved in
   272   the interpretation hierarchy.
   273 
   274   \item @{command "declare"}~@{text thms} declares theorems to the
   275   current local theory context.  No theorem binding is involved here,
   276   unlike @{command "theorems"} or @{command "lemmas"} (cf.\
   277   \secref{sec:axms-thms}), so @{command "declare"} only has the effect
   278   of applying attributes as included in the theorem specification.
   279 
   280   \end{description}
   281 *}
   282 
   283 
   284 section {* Locales \label{sec:locale} *}
   285 
   286 text {*
   287   Locales are named local contexts, consisting of a list of
   288   declaration elements that are modeled after the Isar proof context
   289   commands (cf.\ \secref{sec:proof-context}).
   290 *}
   291 
   292 
   293 subsection {* Locale specifications *}
   294 
   295 text {*
   296   \begin{matharray}{rcl}
   297     @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
   298     @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   299     @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   300     @{method_def intro_locales} & : & @{text method} \\
   301     @{method_def unfold_locales} & : & @{text method} \\
   302   \end{matharray}
   303 
   304   \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
   305   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   306   \indexisarelem{defines}\indexisarelem{notes}
   307   \begin{rail}
   308     'locale' name ('=' localeexpr)? 'begin'?
   309     ;
   310     'print\_locale' '!'? localeexpr
   311     ;
   312     localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
   313     ;
   314 
   315     contextexpr: nameref | '(' contextexpr ')' |
   316     (contextexpr (name mixfix? +)) | (contextexpr + '+')
   317     ;
   318     contextelem: fixes | constrains | assumes | defines | notes
   319     ;
   320     fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
   321     ;
   322     constrains: 'constrains' (name '::' type + 'and')
   323     ;
   324     assumes: 'assumes' (thmdecl? props + 'and')
   325     ;
   326     defines: 'defines' (thmdecl? prop proppat? + 'and')
   327     ;
   328     notes: 'notes' (thmdef? thmrefs + 'and')
   329     ;
   330   \end{rail}
   331 
   332   \begin{description}
   333   
   334   \item @{command "locale"}~@{text "loc = import + body"} defines a
   335   new locale @{text loc} as a context consisting of a certain view of
   336   existing locales (@{text import}) plus some additional elements
   337   (@{text body}).  Both @{text import} and @{text body} are optional;
   338   the degenerate form @{command "locale"}~@{text loc} defines an empty
   339   locale, which may still be useful to collect declarations of facts
   340   later on.  Type-inference on locale expressions automatically takes
   341   care of the most general typing that the combined context elements
   342   may acquire.
   343 
   344   The @{text import} consists of a structured context expression,
   345   consisting of references to existing locales, renamed contexts, or
   346   merged contexts.  Renaming uses positional notation: @{text "c
   347   x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed
   348   parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>,
   349   x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that
   350   position.  Renaming by default deletes concrete syntax, but new
   351   syntax may by specified with a mixfix annotation.  An exeption of
   352   this rule is the special syntax declared with ``@{text
   353   "(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it
   354   be changed.  Merging proceeds from left-to-right, suppressing any
   355   duplicates stemming from different paths through the import
   356   hierarchy.
   357 
   358   The @{text body} consists of basic context elements, further context
   359   expressions may be included as well.
   360 
   361   \begin{description}
   362 
   363   \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
   364   parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
   365   are optional).  The special syntax declaration ``@{text
   366   "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
   367   implicitly in this context.
   368 
   369   \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
   370   constraint @{text \<tau>} on the local parameter @{text x}.
   371 
   372   \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
   373   introduces local premises, similar to @{command "assume"} within a
   374   proof (cf.\ \secref{sec:proof-context}).
   375 
   376   \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
   377   declared parameter.  This is similar to @{command "def"} within a
   378   proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
   379   takes an equational proposition instead of variable-term pair.  The
   380   left-hand side of the equation may have additional arguments, e.g.\
   381   ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
   382 
   383   \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
   384   reconsiders facts within a local context.  Most notably, this may
   385   include arbitrary declarations in any attribute specifications
   386   included here, e.g.\ a local @{attribute simp} rule.
   387 
   388   The initial @{text import} specification of a locale expression
   389   maintains a dynamic relation to the locales being referenced
   390   (benefiting from any later fact declarations in the obvious manner).
   391 
   392   \end{description}
   393   
   394   Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
   395   in the syntax of @{element "assumes"} and @{element "defines"} above
   396   are illegal in locale definitions.  In the long goal format of
   397   \secref{sec:goals}, term bindings may be included as expected,
   398   though.
   399   
   400   \medskip By default, locale specifications are ``closed up'' by
   401   turning the given text into a predicate definition @{text
   402   loc_axioms} and deriving the original assumptions as local lemmas
   403   (modulo local definitions).  The predicate statement covers only the
   404   newly specified assumptions, omitting the content of included locale
   405   expressions.  The full cumulative view is only provided on export,
   406   involving another predicate @{text loc} that refers to the complete
   407   specification text.
   408   
   409   In any case, the predicate arguments are those locale parameters
   410   that actually occur in the respective piece of text.  Also note that
   411   these predicates operate at the meta-level in theory, but the locale
   412   packages attempts to internalize statements according to the
   413   object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
   414   @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
   415   \secref{sec:object-logic}).  Separate introduction rules @{text
   416   loc_axioms.intro} and @{text loc.intro} are provided as well.
   417   
   418   \item @{command "print_locale"}~@{text "import + body"} prints the
   419   specified locale expression in a flattened form.  The notable
   420   special case @{command "print_locale"}~@{text loc} just prints the
   421   contents of the named locale, but keep in mind that type-inference
   422   will normalize type variables according to the usual alphabetical
   423   order.  The command omits @{element "notes"} elements by default.
   424   Use @{command "print_locale"}@{text "!"} to get them included.
   425 
   426   \item @{command "print_locales"} prints the names of all locales
   427   of the current theory.
   428 
   429   \item @{method intro_locales} and @{method unfold_locales}
   430   repeatedly expand all introduction rules of locale predicates of the
   431   theory.  While @{method intro_locales} only applies the @{text
   432   loc.intro} introduction rules and therefore does not decend to
   433   assumptions, @{method unfold_locales} is more aggressive and applies
   434   @{text loc_axioms.intro} as well.  Both methods are aware of locale
   435   specifications entailed by the context, both from target statements,
   436   and from interpretations (see below).  New goals that are entailed
   437   by the current context are discharged automatically.
   438 
   439   \end{description}
   440 *}
   441 
   442 
   443 subsection {* Interpretation of locales *}
   444 
   445 text {*
   446   Locale expressions (more precisely, \emph{context expressions}) may
   447   be instantiated, and the instantiated facts added to the current
   448   context.  This requires a proof of the instantiated specification
   449   and is called \emph{locale interpretation}.  Interpretation is
   450   possible in theories and locales (command @{command
   451   "interpretation"}) and also within a proof body (command @{command
   452   "interpret"}).
   453 
   454   \begin{matharray}{rcl}
   455     @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   456     @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
   457   \end{matharray}
   458 
   459   \indexouternonterm{interp}
   460   \begin{rail}
   461     'interpretation' (interp | name ('<' | subseteq) contextexpr)
   462     ;
   463     'interpret' interp
   464     ;
   465     instantiation: ('[' (inst+) ']')?
   466     ;
   467     interp: (name ':')? \\ (contextexpr instantiation |
   468       name instantiation 'where' (thmdecl? prop + 'and'))
   469     ;
   470   \end{rail}
   471 
   472   \begin{description}
   473 
   474   \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
   475 
   476   The first form of @{command "interpretation"} interprets @{text
   477   expr} in the theory.  The instantiation is given as a list of terms
   478   @{text insts} and is positional.  All parameters must receive an
   479   instantiation term --- with the exception of defined parameters.
   480   These are, if omitted, derived from the defining equation and other
   481   instantiations.  Use ``@{text _}'' to omit an instantiation term.
   482 
   483   The command generates proof obligations for the instantiated
   484   specifications (assumes and defines elements).  Once these are
   485   discharged by the user, instantiated facts are added to the theory
   486   in a post-processing phase.
   487 
   488   Additional equations, which are unfolded in facts during
   489   post-processing, may be given after the keyword @{keyword "where"}.
   490   This is useful for interpreting concepts introduced through
   491   definition specification elements.  The equations must be proved.
   492   Note that if equations are present, the context expression is
   493   restricted to a locale name.
   494 
   495   The command is aware of interpretations already active in the
   496   theory, but does not simplify the goal automatically.  In order to
   497   simplify the proof obligations use methods @{method intro_locales}
   498   or @{method unfold_locales}.  Post-processing is not applied to
   499   facts of interpretations that are already active.  This avoids
   500   duplication of interpreted facts, in particular.  Note that, in the
   501   case of a locale with import, parts of the interpretation may
   502   already be active.  The command will only process facts for new
   503   parts.
   504 
   505   The context expression may be preceded by a name, which takes effect
   506   in the post-processing of facts.  It is used to prefix fact names,
   507   for example to avoid accidental hiding of other facts.
   508 
   509   Adding facts to locales has the effect of adding interpreted facts
   510   to the theory for all active interpretations also.  That is,
   511   interpretations dynamically participate in any facts added to
   512   locales.
   513 
   514   \item @{command "interpretation"}~@{text "name \<subseteq> expr"}
   515 
   516   This form of the command interprets @{text expr} in the locale
   517   @{text name}.  It requires a proof that the specification of @{text
   518   name} implies the specification of @{text expr}.  As in the
   519   localized version of the theorem command, the proof is in the
   520   context of @{text name}.  After the proof obligation has been
   521   dischared, the facts of @{text expr} become part of locale @{text
   522   name} as \emph{derived} context elements and are available when the
   523   context @{text name} is subsequently entered.  Note that, like
   524   import, this is dynamic: facts added to a locale part of @{text
   525   expr} after interpretation become also available in @{text name}.
   526   Like facts of renamed context elements, facts obtained by
   527   interpretation may be accessed by prefixing with the parameter
   528   renaming (where the parameters are separated by ``@{text _}'').
   529 
   530   Unlike interpretation in theories, instantiation is confined to the
   531   renaming of parameters, which may be specified as part of the
   532   context expression @{text expr}.  Using defined parameters in @{text
   533   name} one may achieve an effect similar to instantiation, though.
   534 
   535   Only specification fragments of @{text expr} that are not already
   536   part of @{text name} (be it imported, derived or a derived fragment
   537   of the import) are considered by interpretation.  This enables
   538   circular interpretations.
   539 
   540   If interpretations of @{text name} exist in the current theory, the
   541   command adds interpretations for @{text expr} as well, with the same
   542   prefix and attributes, although only for fragments of @{text expr}
   543   that are not interpreted in the theory already.
   544 
   545   \item @{command "interpret"}~@{text "expr insts \<WHERE> eqns"}
   546   interprets @{text expr} in the proof context and is otherwise
   547   similar to interpretation in theories.
   548 
   549   \end{description}
   550 
   551   \begin{warn}
   552     Since attributes are applied to interpreted theorems,
   553     interpretation may modify the context of common proof tools, e.g.\
   554     the Simplifier or Classical Reasoner.  Since the behavior of such
   555     automated reasoning tools is \emph{not} stable under
   556     interpretation morphisms, manual declarations might have to be
   557     issued.
   558   \end{warn}
   559 
   560   \begin{warn}
   561     An interpretation in a theory may subsume previous
   562     interpretations.  This happens if the same specification fragment
   563     is interpreted twice and the instantiation of the second
   564     interpretation is more general than the interpretation of the
   565     first.  A warning is issued, since it is likely that these could
   566     have been generalized in the first place.  The locale package does
   567     not attempt to remove subsumed interpretations.
   568   \end{warn}
   569 *}
   570 
   571 
   572 section {* Classes \label{sec:class} *}
   573 
   574 text {*
   575   A class is a particular locale with \emph{exactly one} type variable
   576   @{text \<alpha>}.  Beyond the underlying locale, a corresponding type class
   577   is established which is interpreted logically as axiomatic type
   578   class \cite{Wenzel:1997:TPHOL} whose logical content are the
   579   assumptions of the locale.  Thus, classes provide the full
   580   generality of locales combined with the commodity of type classes
   581   (notably type-inference).  See \cite{isabelle-classes} for a short
   582   tutorial.
   583 
   584   \begin{matharray}{rcl}
   585     @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
   586     @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
   587     @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   588     @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   589     @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   590     @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   591     @{method_def intro_classes} & : & @{text method} \\
   592   \end{matharray}
   593 
   594   \begin{rail}
   595     'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
   596       'begin'?
   597     ;
   598     'instantiation' (nameref + 'and') '::' arity 'begin'
   599     ;
   600     'instance'
   601     ;
   602     'subclass' target? nameref
   603     ;
   604     'print\_classes'
   605     ;
   606     'class\_deps'
   607     ;
   608 
   609     superclassexpr: nameref | (nameref '+' superclassexpr)
   610     ;
   611   \end{rail}
   612 
   613   \begin{description}
   614 
   615   \item @{command "class"}~@{text "c = superclasses + body"} defines
   616   a new class @{text c}, inheriting from @{text superclasses}.  This
   617   introduces a locale @{text c} with import of all locales @{text
   618   superclasses}.
   619 
   620   Any @{element "fixes"} in @{text body} are lifted to the global
   621   theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
   622   f\<^sub>n"} of class @{text c}), mapping the local type parameter
   623   @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
   624 
   625   Likewise, @{element "assumes"} in @{text body} are also lifted,
   626   mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
   627   corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}.  The
   628   corresponding introduction rule is provided as @{text
   629   c_class_axioms.intro}.  This rule should be rarely needed directly
   630   --- the @{method intro_classes} method takes care of the details of
   631   class membership proofs.
   632 
   633   \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
   634   \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
   635   allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
   636   to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
   637   \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}.  A plain @{command "instance"} command in the
   638   target body poses a goal stating these type arities.  The target is
   639   concluded by an @{command_ref (local) "end"} command.
   640 
   641   Note that a list of simultaneous type constructors may be given;
   642   this corresponds nicely to mutual recursive type definitions, e.g.\
   643   in Isabelle/HOL.
   644 
   645   \item @{command "instance"} in an instantiation target body sets
   646   up a goal stating the type arities claimed at the opening @{command
   647   "instantiation"}.  The proof would usually proceed by @{method
   648   intro_classes}, and then establish the characteristic theorems of
   649   the type classes involved.  After finishing the proof, the
   650   background theory will be augmented by the proven type arities.
   651 
   652   \item @{command "subclass"}~@{text c} in a class context for class
   653   @{text d} sets up a goal stating that class @{text c} is logically
   654   contained in class @{text d}.  After finishing the proof, class
   655   @{text d} is proven to be subclass @{text c} and the locale @{text
   656   c} is interpreted into @{text d} simultaneously.
   657 
   658   \item @{command "print_classes"} prints all classes in the current
   659   theory.
   660 
   661   \item @{command "class_deps"} visualizes all classes and their
   662   subclass relations as a Hasse diagram.
   663 
   664   \item @{method intro_classes} repeatedly expands all class
   665   introduction rules of this theory.  Note that this method usually
   666   needs not be named explicitly, as it is already included in the
   667   default proof step (e.g.\ of @{command "proof"}).  In particular,
   668   instantiation of trivial (syntactic) classes may be performed by a
   669   single ``@{command ".."}'' proof step.
   670 
   671   \end{description}
   672 *}
   673 
   674 
   675 subsection {* The class target *}
   676 
   677 text {*
   678   %FIXME check
   679 
   680   A named context may refer to a locale (cf.\ \secref{sec:target}).
   681   If this locale is also a class @{text c}, apart from the common
   682   locale target behaviour the following happens.
   683 
   684   \begin{itemize}
   685 
   686   \item Local constant declarations @{text "g[\<alpha>]"} referring to the
   687   local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
   688   are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
   689   referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
   690 
   691   \item Local theorem bindings are lifted as are assumptions.
   692 
   693   \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
   694   global operations @{text "g[?\<alpha> :: c]"} uniformly.  Type inference
   695   resolves ambiguities.  In rare cases, manual type annotations are
   696   needed.
   697   
   698   \end{itemize}
   699 *}
   700 
   701 
   702 subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
   703 
   704 text {*
   705   \begin{matharray}{rcl}
   706     @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
   707     @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   708   \end{matharray}
   709 
   710   Axiomatic type classes are Isabelle/Pure's primitive
   711   \emph{definitional} interface to type classes.  For practical
   712   applications, you should consider using classes
   713   (cf.~\secref{sec:classes}) which provide high level interface.
   714 
   715   \begin{rail}
   716     'axclass' classdecl (axmdecl prop +)
   717     ;
   718     'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
   719     ;
   720   \end{rail}
   721 
   722   \begin{description}
   723   
   724   \item @{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n axms"} defines an
   725   axiomatic type class as the intersection of existing classes, with
   726   additional axioms holding.  Class axioms may not contain more than
   727   one type variable.  The class axioms (with implicit sort constraints
   728   added) are bound to the given names.  Furthermore a class
   729   introduction rule is generated (being bound as @{text
   730   c_class.intro}); this rule is employed by method @{method
   731   intro_classes} to support instantiation proofs of this class.
   732   
   733   The ``class axioms'' (which are derived from the internal class
   734   definition) are stored as theorems according to the given name
   735   specifications; the name space prefix @{text "c_class"} is added
   736   here.  The full collection of these facts is also stored as @{text
   737   c_class.axioms}.
   738   
   739   \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
   740   "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
   741   relation or type arity.  The proof would usually proceed by @{method
   742   intro_classes}, and then establish the characteristic theorems of
   743   the type classes involved.  After finishing the proof, the theory
   744   will be augmented by a type signature declaration corresponding to
   745   the resulting theorem.
   746 
   747   \end{description}
   748 *}
   749 
   750 
   751 section {* Unrestricted overloading *}
   752 
   753 text {*
   754   Isabelle/Pure's definitional schemes support certain forms of
   755   overloading (see \secref{sec:consts}).  At most occassions
   756   overloading will be used in a Haskell-like fashion together with
   757   type classes by means of @{command "instantiation"} (see
   758   \secref{sec:class}).  Sometimes low-level overloading is desirable.
   759   The @{command "overloading"} target provides a convenient view for
   760   end-users.
   761 
   762   \begin{matharray}{rcl}
   763     @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
   764   \end{matharray}
   765 
   766   \begin{rail}
   767     'overloading' \\
   768     ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
   769   \end{rail}
   770 
   771   \begin{description}
   772 
   773   \item @{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}
   774   opens a theory target (cf.\ \secref{sec:target}) which allows to
   775   specify constants with overloaded definitions.  These are identified
   776   by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
   777   constants @{text "c\<^sub>i"} at particular type instances.  The
   778   definitions themselves are established using common specification
   779   tools, using the names @{text "x\<^sub>i"} as reference to the
   780   corresponding constants.  The target is concluded by @{command
   781   (local) "end"}.
   782 
   783   A @{text "(unchecked)"} option disables global dependency checks for
   784   the corresponding definition, which is occasionally useful for
   785   exotic overloading.  It is at the discretion of the user to avoid
   786   malformed theory specifications!
   787 
   788   \end{description}
   789 *}
   790 
   791 
   792 section {* Incorporating ML code \label{sec:ML} *}
   793 
   794 text {*
   795   \begin{matharray}{rcl}
   796     @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   797     @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   798     @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
   799     @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
   800     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
   801     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
   802     @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   803   \end{matharray}
   804 
   805   \begin{mldecls}
   806     @{index_ML bind_thms: "string * thm list -> unit"} \\
   807     @{index_ML bind_thm: "string * thm -> unit"} \\
   808   \end{mldecls}
   809 
   810   \begin{rail}
   811     'use' name
   812     ;
   813     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
   814     ;
   815   \end{rail}
   816 
   817   \begin{description}
   818 
   819   \item @{command "use"}~@{text "file"} reads and executes ML
   820   commands from @{text "file"}.  The current theory context is passed
   821   down to the ML toplevel and may be modified, using @{ML
   822   "Context.>>"} or derived ML commands.  The file name is checked with
   823   the @{keyword_ref "uses"} dependency declaration given in the theory
   824   header (see also \secref{sec:begin-thy}).
   825 
   826   Top-level ML bindings are stored within the (global or local) theory
   827   context.
   828   
   829   \item @{command "ML"}~@{text "text"} is similar to @{command "use"},
   830   but executes ML commands directly from the given @{text "text"}.
   831   Top-level ML bindings are stored within the (global or local) theory
   832   context.
   833 
   834   \item @{command "ML_prf"} is analogous to @{command "ML"} but works
   835   within a proof context.
   836 
   837   Top-level ML bindings are stored within the proof context in a
   838   purely sequential fashion, disregarding the nested proof structure.
   839   ML bindings introduced by @{command "ML_prf"} are discarded at the
   840   end of the proof.
   841 
   842   \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
   843   versions of @{command "ML"}, which means that the context may not be
   844   updated.  @{command "ML_val"} echos the bindings produced at the ML
   845   toplevel, but @{command "ML_command"} is silent.
   846   
   847   \item @{command "setup"}~@{text "text"} changes the current theory
   848   context by applying @{text "text"}, which refers to an ML expression
   849   of type @{ML_type "theory -> theory"}.  This enables to initialize
   850   any object-logic specific tools and packages written in ML, for
   851   example.
   852 
   853   \item @{command "local_setup"} is similar to @{command "setup"} for
   854   a local theory context, and an ML expression of type @{ML_type
   855   "local_theory -> local_theory"}.  This allows to
   856   invoke local theory specification packages without going through
   857   concrete outer syntax, for example.
   858 
   859   \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
   860   theorems produced in ML both in the theory context and the ML
   861   toplevel, associating it with the provided name.  Theorems are put
   862   into a global ``standard'' format before being stored.
   863 
   864   \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
   865   singleton theorem.
   866   
   867   \end{description}
   868 *}
   869 
   870 
   871 section {* Primitive specification elements *}
   872 
   873 subsection {* Type classes and sorts \label{sec:classes} *}
   874 
   875 text {*
   876   \begin{matharray}{rcll}
   877     @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
   878     @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   879     @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
   880     @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   881   \end{matharray}
   882 
   883   \begin{rail}
   884     'classes' (classdecl +)
   885     ;
   886     'classrel' (nameref ('<' | subseteq) nameref + 'and')
   887     ;
   888     'defaultsort' sort
   889     ;
   890   \end{rail}
   891 
   892   \begin{description}
   893 
   894   \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
   895   @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
   896   Isabelle implicitly maintains the transitive closure of the class
   897   hierarchy.  Cyclic class structures are not permitted.
   898 
   899   \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
   900   relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
   901   This is done axiomatically!  The @{command_ref "instance"} command
   902   (see \secref{sec:axclass}) provides a way to introduce proven class
   903   relations.
   904 
   905   \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
   906   new default sort for any type variable that is given explicitly in
   907   the text, but lacks a sort constraint (wrt.\ the current context).
   908   Type variables generated by type inference are not affected.
   909 
   910   Usually the default sort is only changed when defining a new
   911   object-logic.  For example, the default sort in Isabelle/HOL is
   912   @{text type}, the class of all HOL types.  %FIXME sort antiq?
   913 
   914   When merging theories, the default sorts of the parents are
   915   logically intersected, i.e.\ the representations as lists of classes
   916   are joined.
   917 
   918   \item @{command "class_deps"} visualizes the subclass relation,
   919   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
   920 
   921   \end{description}
   922 *}
   923 
   924 
   925 subsection {* Types and type abbreviations \label{sec:types-pure} *}
   926 
   927 text {*
   928   \begin{matharray}{rcll}
   929     @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
   930     @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
   931     @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   932   \end{matharray}
   933 
   934   \begin{rail}
   935     'types' (typespec '=' type infix? +)
   936     ;
   937     'typedecl' typespec infix?
   938     ;
   939     'arities' (nameref '::' arity +)
   940     ;
   941   \end{rail}
   942 
   943   \begin{description}
   944 
   945   \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
   946   \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
   947   @{text "\<tau>"}.  Unlike actual type definitions, as are available in
   948   Isabelle/HOL for example, type synonyms are merely syntactic
   949   abbreviations without any logical significance.  Internally, type
   950   synonyms are fully expanded.
   951   
   952   \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
   953   type constructor @{text t}.  If the object-logic defines a base sort
   954   @{text s}, then the constructor is declared to operate on that, via
   955   the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
   956   s)s"}.
   957 
   958   \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
   959   Isabelle's order-sorted signature of types by new type constructor
   960   arities.  This is done axiomatically!  The @{command_ref "instance"}
   961   command (see \secref{sec:axclass}) provides a way to introduce
   962   proven type arities.
   963 
   964   \end{description}
   965 *}
   966 
   967 
   968 subsection {* Co-regularity of type classes and arities *}
   969 
   970 text {* The class relation together with the collection of
   971   type-constructor arities must obey the principle of
   972   \emph{co-regularity} as defined below.
   973 
   974   \medskip For the subsequent formulation of co-regularity we assume
   975   that the class relation is closed by transitivity and reflexivity.
   976   Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
   977   completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
   978   implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
   979 
   980   Treating sorts as finite sets of classes (meaning the intersection),
   981   the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
   982   follows:
   983   \[
   984     @{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"}
   985   \]
   986 
   987   This relation on sorts is further extended to tuples of sorts (of
   988   the same length) in the component-wise way.
   989 
   990   \smallskip Co-regularity of the class relation together with the
   991   arities relation means:
   992   \[
   993     @{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"}
   994   \]
   995   \noindent for all such arities.  In other words, whenever the result
   996   classes of some type-constructor arities are related, then the
   997   argument sorts need to be related in the same way.
   998 
   999   \medskip Co-regularity is a very fundamental property of the
  1000   order-sorted algebra of types.  For example, it entails principle
  1001   types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
  1002 *}
  1003 
  1004 
  1005 subsection {* Constants and definitions \label{sec:consts} *}
  1006 
  1007 text {*
  1008   Definitions essentially express abbreviations within the logic.  The
  1009   simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
  1010   c} is a newly declared constant.  Isabelle also allows derived forms
  1011   where the arguments of @{text c} appear on the left, abbreviating a
  1012   prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
  1013   written more conveniently as @{text "c x y \<equiv> t"}.  Moreover,
  1014   definitions may be weakened by adding arbitrary pre-conditions:
  1015   @{text "A \<Longrightarrow> c x y \<equiv> t"}.
  1016 
  1017   \medskip The built-in well-formedness conditions for definitional
  1018   specifications are:
  1019 
  1020   \begin{itemize}
  1021 
  1022   \item Arguments (on the left-hand side) must be distinct variables.
  1023 
  1024   \item All variables on the right-hand side must also appear on the
  1025   left-hand side.
  1026 
  1027   \item All type variables on the right-hand side must also appear on
  1028   the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
  1029   \<alpha> list)"} for example.
  1030 
  1031   \item The definition must not be recursive.  Most object-logics
  1032   provide definitional principles that can be used to express
  1033   recursion safely.
  1034 
  1035   \end{itemize}
  1036 
  1037   Overloading means that a constant being declared as @{text "c :: \<alpha>
  1038   decl"} may be defined separately on type instances @{text "c ::
  1039   (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
  1040   t}.  The right-hand side may mention overloaded constants
  1041   recursively at type instances corresponding to the immediate
  1042   argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}.  Incomplete
  1043   specification patterns impose global constraints on all occurrences,
  1044   e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
  1045   corresponding occurrences on some right-hand side need to be an
  1046   instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
  1047 
  1048   \begin{matharray}{rcl}
  1049     @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
  1050     @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
  1051     @{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\
  1052   \end{matharray}
  1053 
  1054   \begin{rail}
  1055     'consts' ((name '::' type mixfix?) +)
  1056     ;
  1057     'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
  1058     ;
  1059   \end{rail}
  1060 
  1061   \begin{rail}
  1062     'constdefs' structs? (constdecl? constdef +)
  1063     ;
  1064 
  1065     structs: '(' 'structure' (vars + 'and') ')'
  1066     ;
  1067     constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
  1068     ;
  1069     constdef: thmdecl? prop
  1070     ;
  1071   \end{rail}
  1072 
  1073   \begin{description}
  1074 
  1075   \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
  1076   c} to have any instance of type scheme @{text \<sigma>}.  The optional
  1077   mixfix annotations may attach concrete syntax to the constants
  1078   declared.
  1079   
  1080   \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
  1081   as a definitional axiom for some existing constant.
  1082   
  1083   The @{text "(unchecked)"} option disables global dependency checks
  1084   for this definition, which is occasionally useful for exotic
  1085   overloading.  It is at the discretion of the user to avoid malformed
  1086   theory specifications!
  1087   
  1088   The @{text "(overloaded)"} option declares definitions to be
  1089   potentially overloaded.  Unless this option is given, a warning
  1090   message would be issued for any definitional equation with a more
  1091   special type than that of the corresponding constant declaration.
  1092   
  1093   \item @{command "constdefs"} combines constant declarations and
  1094   definitions, with type-inference taking care of the most general
  1095   typing of the given specification (the optional type constraint may
  1096   refer to type-inference dummies ``@{text _}'' as usual).  The
  1097   resulting type declaration needs to agree with that of the
  1098   specification; overloading is \emph{not} supported here!
  1099   
  1100   The constant name may be omitted altogether, if neither type nor
  1101   syntax declarations are given.  The canonical name of the
  1102   definitional axiom for constant @{text c} will be @{text c_def},
  1103   unless specified otherwise.  Also note that the given list of
  1104   specifications is processed in a strictly sequential manner, with
  1105   type-checking being performed independently.
  1106   
  1107   An optional initial context of @{text "(structure)"} declarations
  1108   admits use of indexed syntax, using the special symbol @{verbatim
  1109   "\<index>"} (printed as ``@{text "\<index>"}'').  The latter concept is
  1110   particularly useful with locales (see also \secref{sec:locale}).
  1111 
  1112   \end{description}
  1113 *}
  1114 
  1115 
  1116 section {* Axioms and theorems \label{sec:axms-thms} *}
  1117 
  1118 text {*
  1119   \begin{matharray}{rcll}
  1120     @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
  1121     @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
  1122     @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
  1123   \end{matharray}
  1124 
  1125   \begin{rail}
  1126     'axioms' (axmdecl prop +)
  1127     ;
  1128     ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
  1129     ;
  1130   \end{rail}
  1131 
  1132   \begin{description}
  1133   
  1134   \item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary
  1135   statements as axioms of the meta-logic.  In fact, axioms are
  1136   ``axiomatic theorems'', and may be referred later just as any other
  1137   theorem.
  1138   
  1139   Axioms are usually only introduced when declaring new logical
  1140   systems.  Everyday work is typically done the hard way, with proper
  1141   definitions and proven theorems.
  1142   
  1143   \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} retrieves and stores
  1144   existing facts in the theory context, or the specified target
  1145   context (see also \secref{sec:target}).  Typical applications would
  1146   also involve attributes, to declare Simplifier rules, for example.
  1147   
  1148   \item @{command "theorems"} is essentially the same as @{command
  1149   "lemmas"}, but marks the result as a different kind of facts.
  1150 
  1151   \end{description}
  1152 *}
  1153 
  1154 
  1155 section {* Oracles *}
  1156 
  1157 text {* Oracles allow Isabelle to take advantage of external reasoners
  1158   such as arithmetic decision procedures, model checkers, fast
  1159   tautology checkers or computer algebra systems.  Invoked as an
  1160   oracle, an external reasoner can create arbitrary Isabelle theorems.
  1161 
  1162   It is the responsibility of the user to ensure that the external
  1163   reasoner is as trustworthy as the application requires.  Another
  1164   typical source of errors is the linkup between Isabelle and the
  1165   external tool, not just its concrete implementation, but also the
  1166   required translation between two different logical environments.
  1167 
  1168   Isabelle merely guarantees well-formedness of the propositions being
  1169   asserted, and records within the internal derivation object how
  1170   presumed theorems depend on unproven suppositions.
  1171 
  1172   \begin{matharray}{rcl}
  1173     @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
  1174   \end{matharray}
  1175 
  1176   \begin{rail}
  1177     'oracle' name '=' text
  1178     ;
  1179   \end{rail}
  1180 
  1181   \begin{description}
  1182 
  1183   \item @{command "oracle"}~@{text "name = text"} turns the given ML
  1184   expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
  1185   ML function of type @{ML_text "'a -> thm"}, which is bound to the
  1186   global identifier @{ML_text name}.  This acts like an infinitary
  1187   specification of axioms!  Invoking the oracle only works within the
  1188   scope of the resulting theory.
  1189 
  1190   \end{description}
  1191 
  1192   See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
  1193   defining a new primitive rule as oracle, and turning it into a proof
  1194   method.
  1195 *}
  1196 
  1197 
  1198 section {* Name spaces *}
  1199 
  1200 text {*
  1201   \begin{matharray}{rcl}
  1202     @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
  1203     @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
  1204     @{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\
  1205   \end{matharray}
  1206 
  1207   \begin{rail}
  1208     'hide' ('(open)')? name (nameref + )
  1209     ;
  1210   \end{rail}
  1211 
  1212   Isabelle organizes any kind of name declarations (of types,
  1213   constants, theorems etc.) by separate hierarchically structured name
  1214   spaces.  Normally the user does not have to control the behavior of
  1215   name spaces by hand, yet the following commands provide some way to
  1216   do so.
  1217 
  1218   \begin{description}
  1219 
  1220   \item @{command "global"} and @{command "local"} change the current
  1221   name declaration mode.  Initially, theories start in @{command
  1222   "local"} mode, causing all names to be automatically qualified by
  1223   the theory name.  Changing this to @{command "global"} causes all
  1224   names to be declared without the theory prefix, until @{command
  1225   "local"} is declared again.
  1226   
  1227   Note that global names are prone to get hidden accidently later,
  1228   when qualified names of the same base name are introduced.
  1229   
  1230   \item @{command "hide"}~@{text "space names"} fully removes
  1231   declarations from a given name space (which may be @{text "class"},
  1232   @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
  1233   "(open)"} option, only the base name is hidden.  Global
  1234   (unqualified) names may never be hidden.
  1235   
  1236   Note that hiding name space accesses has no impact on logical
  1237   declarations --- they remain valid internally.  Entities that are no
  1238   longer accessible to the user are printed with the special qualifier
  1239   ``@{text "??"}'' prefixed to the full internal name.
  1240 
  1241   \end{description}
  1242 *}
  1243 
  1244 end