src/Doc/Isar_Ref/Spec.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 66757 e32750d7acb4
child 66916 aca50a1572c5
permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Spec
     4   imports Main Base
     5 begin
     6 
     7 chapter \<open>Specifications\<close>
     8 
     9 text \<open>
    10   The Isabelle/Isar theory format integrates specifications and proofs, with
    11   support for interactive development by continuous document editing. There is
    12   a separate document preparation system (see \chref{ch:document-prep}), for
    13   typesetting formal developments together with informal text. The resulting
    14   hyper-linked PDF documents can be used both for WWW presentation and printed
    15   copies.
    16 
    17   The Isar proof language (see \chref{ch:proofs}) is embedded into the theory
    18   language as a proper sub-language. Proof mode is entered by stating some
    19   \<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> at the theory level, and left again with the final
    20   conclusion (e.g.\ via \<^theory_text>\<open>qed\<close>).
    21 \<close>
    22 
    23 
    24 section \<open>Defining theories \label{sec:begin-thy}\<close>
    25 
    26 text \<open>
    27   \begin{matharray}{rcl}
    28     @{command_def "theory"} & : & \<open>toplevel \<rightarrow> theory\<close> \\
    29     @{command_def (global) "end"} & : & \<open>theory \<rightarrow> toplevel\<close> \\
    30     @{command_def "thy_deps"}\<open>\<^sup>*\<close> & : & \<open>theory \<rightarrow>\<close> \\
    31   \end{matharray}
    32 
    33   Isabelle/Isar theories are defined via theory files, which consist of an
    34   outermost sequence of definition--statement--proof elements. Some
    35   definitions are self-sufficient (e.g.\ \<^theory_text>\<open>fun\<close> in Isabelle/HOL), with
    36   foundational proofs performed internally. Other definitions require an
    37   explicit proof as justification (e.g.\ \<^theory_text>\<open>function\<close> and \<^theory_text>\<open>termination\<close> in
    38   Isabelle/HOL). Plain statements like \<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> are merely a
    39   special case of that, defining a theorem from a given proposition and its
    40   proof.
    41 
    42   The theory body may be sub-structured by means of \<^emph>\<open>local theory targets\<close>,
    43   such as \<^theory_text>\<open>locale\<close> and \<^theory_text>\<open>class\<close>. It is also possible to use \<^theory_text>\<open>context begin \<dots>
    44   end\<close> blocks to delimited a local theory context: a \<^emph>\<open>named context\<close> to
    45   augment a locale or class specification, or an \<^emph>\<open>unnamed context\<close> to refer
    46   to local parameters and assumptions that are discharged later. See
    47   \secref{sec:target} for more details.
    48 
    49   \<^medskip>
    50   A theory is commenced by the \<^theory_text>\<open>theory\<close> command, which indicates imports of
    51   previous theories, according to an acyclic foundational order. Before the
    52   initial \<^theory_text>\<open>theory\<close> command, there may be optional document header material
    53   (like \<^theory_text>\<open>section\<close> or \<^theory_text>\<open>text\<close>, see \secref{sec:markup}). The document header
    54   is outside of the formal theory context, though.
    55 
    56   A theory is concluded by a final @{command (global) "end"} command, one that
    57   does not belong to a local theory target. No further commands may follow
    58   such a global @{command (global) "end"}.
    59 
    60   @{rail \<open>
    61     @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \<newline>
    62       keywords? abbrevs? @'begin'
    63     ;
    64     keywords: @'keywords' (keyword_decls + @'and')
    65     ;
    66     keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
    67     ;
    68     abbrevs: @'abbrevs' ((text '=' text) +)
    69     ;
    70     @@{command thy_deps} (thy_bounds thy_bounds?)?
    71     ;
    72     thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')'
    73   \<close>}
    74 
    75   \<^descr> \<^theory_text>\<open>theory A imports B\<^sub>1 \<dots> B\<^sub>n begin\<close> starts a new theory \<open>A\<close> based on the
    76   merge of existing theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>. Due to the possibility to import
    77   more than one ancestor, the resulting theory structure of an Isabelle
    78   session forms a directed acyclic graph (DAG). Isabelle takes care that
    79   sources contributing to the development graph are always up-to-date: changed
    80   files are automatically rechecked whenever a theory header specification is
    81   processed.
    82 
    83   Empty imports are only allowed in the bootstrap process of the special
    84   theory @{theory Pure}, which is the start of any other formal development
    85   based on Isabelle. Regular user theories usually refer to some more complex
    86   entry point, such as theory @{theory Main} in Isabelle/HOL.
    87 
    88   The @{keyword_def "keywords"} specification declares outer syntax
    89   (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare
    90   in end-user applications). Both minor keywords and major keywords of the
    91   Isar command language need to be specified, in order to make parsing of
    92   proof documents work properly. Command keywords need to be classified
    93   according to their structural role in the formal text. Examples may be seen
    94   in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close>
    95   \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for
    96   theory-level declarations with and without proof, respectively. Additional
    97   @{syntax tags} provide defaults for document preparation
    98   (\secref{sec:tags}).
    99 
   100   The @{keyword_def "abbrevs"} specification declares additional abbreviations
   101   for syntactic completion. The default for a new keyword is just its name,
   102   but completion may be avoided by defining @{keyword "abbrevs"} with empty
   103   text.
   104 
   105   \<^descr> @{command (global) "end"} concludes the current theory definition. Note
   106   that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
   107   may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "end"},
   108   according to the usual rules for nested blocks.
   109 
   110   \<^descr> \<^theory_text>\<open>thy_deps\<close> visualizes the theory hierarchy as a directed acyclic graph.
   111   By default, all imported theories are shown. This may be restricted by
   112   specifying bounds wrt. the theory inclusion relation.
   113 \<close>
   114 
   115 
   116 section \<open>Local theory targets \label{sec:target}\<close>
   117 
   118 text \<open>
   119   \begin{matharray}{rcll}
   120     @{command_def "context"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   121     @{command_def (local) "end"} & : & \<open>local_theory \<rightarrow> theory\<close> \\
   122     @{keyword_def "private"} \\
   123     @{keyword_def "qualified"} \\
   124   \end{matharray}
   125 
   126   A local theory target is a specification context that is managed separately
   127   within the enclosing theory. Contexts may introduce parameters (fixed
   128   variables) and assumptions (hypotheses). Definitions and theorems depending
   129   on the context may be added incrementally later on.
   130 
   131   \<^emph>\<open>Named contexts\<close> refer to locales (cf.\ \secref{sec:locale}) or type
   132   classes (cf.\ \secref{sec:class}); the name ``\<open>-\<close>'' signifies the global
   133   theory context.
   134 
   135   \<^emph>\<open>Unnamed contexts\<close> may introduce additional parameters and assumptions, and
   136   results produced in the context are generalized accordingly. Such auxiliary
   137   contexts may be nested within other targets, like \<^theory_text>\<open>locale\<close>, \<^theory_text>\<open>class\<close>,
   138   \<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>.
   139 
   140   @{rail \<open>
   141     @@{command context} @{syntax name} @'begin'
   142     ;
   143     @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
   144     ;
   145     @{syntax_def target}: '(' @'in' @{syntax name} ')'
   146   \<close>}
   147 
   148   \<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing
   149   locale or class \<open>c\<close>. Note that locale and class definitions allow to include
   150   the \<^theory_text>\<open>begin\<close> keyword as well, in order to continue the local theory
   151   immediately after the initial specification.
   152 
   153   \<^descr> \<^theory_text>\<open>context bundles elements begin\<close> opens an unnamed context, by extending
   154   the enclosing global or local theory target by the given declaration bundles
   155   (\secref{sec:bundle}) and context elements (\<^theory_text>\<open>fixes\<close>, \<^theory_text>\<open>assumes\<close> etc.). This
   156   means any results stemming from definitions and proofs in the extended
   157   context will be exported into the enclosing target by lifting over extra
   158   parameters and premises.
   159 
   160   \<^descr> @{command (local) "end"} concludes the current local theory, according to
   161   the nesting of contexts. Note that a global @{command (global) "end"} has a
   162   different meaning: it concludes the theory itself (\secref{sec:begin-thy}).
   163 
   164   \<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be given as modifiers before any local
   165   theory command. This restricts name space accesses to the local scope, as
   166   determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outside its scope,
   167   a \<^theory_text>\<open>private\<close> name is inaccessible, and a \<^theory_text>\<open>qualified\<close> name is only
   168   accessible with some qualification.
   169 
   170   Neither a global \<^theory_text>\<open>theory\<close> nor a \<^theory_text>\<open>locale\<close> target provides a local scope by
   171   itself: an extra unnamed context is required to use \<^theory_text>\<open>private\<close> or
   172   \<^theory_text>\<open>qualified\<close> here.
   173 
   174   \<^descr> \<open>(\<close>@{keyword_def "in"}~\<open>c)\<close> given after any local theory command specifies
   175   an immediate target, e.g.\ ``\<^theory_text>\<open>definition (in c)\<close>'' or
   176   ``\<^theory_text>\<open>theorem (in c)\<close>''. This works both in a local or global theory context;
   177   the current target context will be suspended for this command only. Note
   178   that ``\<^theory_text>\<open>(in -)\<close>'' will always produce a global result independently of the
   179   current target context.
   180 
   181 
   182   Any specification element that operates on \<open>local_theory\<close> according to this
   183   manual implicitly allows the above target syntax \<^theory_text>\<open>(in c)\<close>, but individual
   184   syntax diagrams omit that aspect for clarity.
   185 
   186   \<^medskip>
   187   The exact meaning of results produced within a local theory context depends
   188   on the underlying target infrastructure (locale, type class etc.). The
   189   general idea is as follows, considering a context named \<open>c\<close> with parameter
   190   \<open>x\<close> and assumption \<open>A[x]\<close>.
   191 
   192   Definitions are exported by introducing a global version with additional
   193   arguments; a syntactic abbreviation links the long form with the abstract
   194   version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
   195   t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local
   196   abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the fixed parameter
   197   \<open>x\<close>).
   198 
   199   Theorems are exported by discharging the assumptions and generalizing the
   200   parameters of the context. For example, \<open>a: B[x]\<close> becomes \<open>c.a: A[?x] \<Longrightarrow>
   201   B[?x]\<close>, again for arbitrary \<open>?x\<close>.
   202 \<close>
   203 
   204 
   205 section \<open>Bundled declarations \label{sec:bundle}\<close>
   206 
   207 text \<open>
   208   \begin{matharray}{rcl}
   209     @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   210     @{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   211     @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   212     @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   213     @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
   214     @{keyword_def "includes"} & : & syntax \\
   215   \end{matharray}
   216 
   217   The outer syntax of fact expressions (\secref{sec:syn-att}) involves
   218   theorems and attributes, which are evaluated in the context and applied to
   219   it. Attributes may declare theorems to the context, as in \<open>this_rule [intro]
   220   that_rule [elim]\<close> for example. Configuration options (\secref{sec:config})
   221   are special declaration attributes that operate on the context without a
   222   theorem, as in \<open>[[show_types = false]]\<close> for example.
   223 
   224   Expressions of this form may be defined as \<^emph>\<open>bundled declarations\<close> in the
   225   context, and included in other situations later on. Including declaration
   226   bundles augments a local context casually without logical dependencies,
   227   which is in contrast to locales and locale interpretation
   228   (\secref{sec:locale}).
   229 
   230   @{rail \<open>
   231     @@{command bundle} @{syntax name}
   232       ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
   233     ;
   234     @@{command print_bundles} ('!'?)
   235     ;
   236     (@@{command include} | @@{command including}) (@{syntax name}+)
   237     ;
   238     @{syntax_def "includes"}: @'includes' (@{syntax name}+)
   239   \<close>}
   240 
   241   \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
   242   context. The RHS is similar to the one of the \<^theory_text>\<open>declare\<close> command. Bundles
   243   defined in local theory targets are subject to transformations via
   244   morphisms, when moved into different application contexts; this works
   245   analogously to any other local theory specification.
   246 
   247   \<^descr> \<^theory_text>\<open>bundle b begin body end\<close> defines a bundle of declarations from the
   248   \<open>body\<close> of local theory specifications. It may consist of commands that are
   249   technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declaration\<close>, which also includes
   250   \<^theory_text>\<open>notation\<close>, for example. Named fact declarations like ``\<^theory_text>\<open>lemmas a [simp] =
   251   b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name
   252   bindings are not recorded in the bundle.
   253 
   254   \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
   255   current context; the ``\<open>!\<close>'' option indicates extra verbosity.
   256 
   257   \<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in
   258   the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
   259   (\secref{sec:theorems}) with the expanded bundles.
   260 
   261   \<^descr> \<^theory_text>\<open>include\<close> is similar to \<^theory_text>\<open>unbundle\<close>, but works in a proof body (forward
   262   mode). This is analogous to \<^theory_text>\<open>note\<close> (\secref{sec:proof-facts}) with the
   263   expanded bundles.
   264 
   265   \<^descr> \<^theory_text>\<open>including\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement
   266   (backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts})
   267   with the expanded bundles.
   268 
   269   \<^descr> \<^theory_text>\<open>includes b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but works in situations
   270   where a specification context is constructed, notably for \<^theory_text>\<open>context\<close> and
   271   long statements of \<^theory_text>\<open>theorem\<close> etc.
   272 
   273 
   274   Here is an artificial example of bundling various configuration options:
   275 \<close>
   276 
   277 (*<*)experiment begin(*>*)
   278 bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
   279 
   280 lemma "x = x"
   281   including trace by metis
   282 (*<*)end(*>*)
   283 
   284 
   285 section \<open>Term definitions \label{sec:term-definitions}\<close>
   286 
   287 text \<open>
   288   \begin{matharray}{rcll}
   289     @{command_def "definition"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   290     @{attribute_def "defn"} & : & \<open>attribute\<close> \\
   291     @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   292     @{command_def "abbreviation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   293     @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   294   \end{matharray}
   295 
   296   Term definitions may either happen within the logic (as equational axioms of
   297   a certain form (see also \secref{sec:overloading}), or outside of it as
   298   rewrite system on abstract syntax. The second form is called
   299   ``abbreviation''.
   300 
   301   @{rail \<open>
   302     @@{command definition} decl? definition
   303     ;
   304     @@{command abbreviation} @{syntax mode}? decl? abbreviation
   305     ;
   306     @@{command print_abbrevs} ('!'?)
   307     ;
   308     decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
   309     ;
   310     definition: @{syntax thmdecl}? @{syntax prop}
   311       @{syntax spec_prems} @{syntax for_fixes}
   312     ;
   313     abbreviation: @{syntax prop} @{syntax for_fixes}
   314   \<close>}
   315 
   316   \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according
   317   to the specification given as \<open>eq\<close>, which is then turned into a proven fact.
   318   The given proposition may deviate from internal meta-level equality
   319   according to the rewrite rules declared as @{attribute defn} by the
   320   object-logic. This usually covers object-level equality \<open>x = y\<close> and
   321   equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{attribute
   322   defn} setup.
   323 
   324   Definitions may be presented with explicit arguments on the LHS, as well as
   325   additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0
   326   \<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.
   327 
   328   \<^descr> \<^theory_text>\<open>print_defn_rules\<close> prints the definitional rewrite rules declared via
   329   @{attribute defn} in the current context.
   330 
   331   \<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant which is
   332   associated with a certain term according to the meta-level equality \<open>eq\<close>.
   333 
   334   Abbreviations participate in the usual type-inference process, but are
   335   expanded before the logic ever sees them. Pretty printing of terms involves
   336   higher-order rewriting with rules stemming from reverted abbreviations. This
   337   needs some care to avoid overlapping or looping syntactic replacements!
   338 
   339   The optional \<open>mode\<close> specification restricts output to a particular print
   340   mode; using ``\<open>input\<close>'' here achieves the effect of one-way abbreviations.
   341   The mode may also include an ``\<^theory_text>\<open>output\<close>'' qualifier that affects the
   342   concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in
   343   \secref{sec:syn-trans}.
   344 
   345   \<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the current context;
   346   the ``\<open>!\<close>'' option indicates extra verbosity.
   347 \<close>
   348 
   349 
   350 section \<open>Axiomatizations \label{sec:axiomatizations}\<close>
   351 
   352 text \<open>
   353   \begin{matharray}{rcll}
   354     @{command_def "axiomatization"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\
   355   \end{matharray}
   356 
   357   @{rail \<open>
   358     @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)?
   359     ;
   360     axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
   361       @{syntax spec_prems} @{syntax for_fixes}
   362   \<close>}
   363 
   364   \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
   365   simultaneously and states axiomatic properties for these. The constants are
   366   marked as being specified once and for all, which prevents additional
   367   specifications for the same constants later on, but it is always possible do
   368   emit axiomatizations without referring to particular constants. Note that
   369   lack of precise dependency tracking of axiomatizations may disrupt the
   370   well-formedness of an otherwise definitional theory.
   371 
   372   Axiomatization is restricted to a global theory context: support for local
   373   theory targets \secref{sec:target} would introduce an extra dimension of
   374   uncertainty what the written specifications really are, and make it
   375   infeasible to argue why they are correct.
   376 
   377   Axiomatic specifications are required when declaring a new logical system
   378   within Isabelle/Pure, but in an application environment like Isabelle/HOL
   379   the user normally stays within definitional mechanisms provided by the logic
   380   and its libraries.
   381 \<close>
   382 
   383 
   384 section \<open>Generic declarations\<close>
   385 
   386 text \<open>
   387   \begin{matharray}{rcl}
   388     @{command_def "declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   389     @{command_def "syntax_declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   390     @{command_def "declare"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   391   \end{matharray}
   392 
   393   Arbitrary operations on the background context may be wrapped-up as generic
   394   declaration elements. Since the underlying concept of local theories may be
   395   subject to later re-interpretation, there is an additional dependency on a
   396   morphism that tells the difference of the original declaration context wrt.\
   397   the application context encountered later on. A fact declaration is an
   398   important special case: it consists of a theorem which is applied to the
   399   context by means of an attribute.
   400 
   401   @{rail \<open>
   402     (@@{command declaration} | @@{command syntax_declaration})
   403       ('(' @'pervasive' ')')? \<newline> @{syntax text}
   404     ;
   405     @@{command declare} (@{syntax thms} + @'and')
   406   \<close>}
   407 
   408   \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type @{ML_type
   409   declaration}, to the current local theory under construction. In later
   410   application contexts, the function is transformed according to the morphisms
   411   being involved in the interpretation hierarchy.
   412 
   413   If the \<^theory_text>\<open>(pervasive)\<close> option is given, the corresponding declaration is
   414   applied to all possible contexts involved, including the global background
   415   theory.
   416 
   417   \<^descr> \<^theory_text>\<open>syntax_declaration\<close> is similar to \<^theory_text>\<open>declaration\<close>, but is meant to affect
   418   only ``syntactic'' tools by convention (such as notation and type-checking
   419   information).
   420 
   421   \<^descr> \<^theory_text>\<open>declare thms\<close> declares theorems to the current local theory context. No
   422   theorem binding is involved here, unlike \<^theory_text>\<open>lemmas\<close> (cf.\
   423   \secref{sec:theorems}), so \<^theory_text>\<open>declare\<close> only has the effect of applying
   424   attributes as included in the theorem specification.
   425 \<close>
   426 
   427 
   428 section \<open>Locales \label{sec:locale}\<close>
   429 
   430 text \<open>
   431   A locale is a functor that maps parameters (including implicit type
   432   parameters) and a specification to a list of declarations. The syntax of
   433   locales is modeled after the Isar proof context commands (cf.\
   434   \secref{sec:proof-context}).
   435 
   436   Locale hierarchies are supported by maintaining a graph of dependencies
   437   between locale instances in the global theory. Dependencies may be
   438   introduced through import (where a locale is defined as sublocale of the
   439   imported instances) or by proving that an existing locale is a sublocale of
   440   one or several locale instances.
   441 
   442   A locale may be opened with the purpose of appending to its list of
   443   declarations (cf.\ \secref{sec:target}). When opening a locale declarations
   444   from all dependencies are collected and are presented as a local theory. In
   445   this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are
   446   omitted. A locale instance is redundant if it is subsumed by an instance
   447   encountered earlier. A more detailed description of this process is
   448   available elsewhere @{cite Ballarin2014}.
   449 \<close>
   450 
   451 
   452 subsection \<open>Locale expressions \label{sec:locale-expr}\<close>
   453 
   454 text \<open>
   455   A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing
   456   locales. The context consists of the declaration elements from the locale
   457   instances. Redundant locale instances are omitted according to roundup.
   458 
   459   @{rail \<open>
   460     @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
   461     ;
   462     instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts)
   463     ;
   464     qualifier: @{syntax name} ('?')?
   465     ;
   466     pos_insts: ('_' | @{syntax term})*
   467     ;
   468     named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
   469   \<close>}
   470 
   471   A locale instance consists of a reference to a locale and either positional
   472   or named parameter instantiations. Identical instantiations (that is, those
   473   that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>''
   474   enables to omit the instantiation for a parameter inside a positional
   475   instantiation.
   476 
   477   Terms in instantiations are from the context the locale expressions is
   478   declared in. Local names may be added to this context with the optional
   479   \<^theory_text>\<open>for\<close> clause. This is useful for shadowing names bound in outer contexts,
   480   and for declaring syntax. In addition, syntax declarations from one instance
   481   are effective when parsing subsequent instances of the same expression.
   482 
   483   Instances have an optional qualifier which applies to names in declarations.
   484   Names include local definitions and theorem names. If present, the qualifier
   485   itself is either mandatory (default) or non-mandatory (when followed by
   486   ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.
   487   Qualifiers only affect name spaces; they play no role in determining whether
   488   one locale instance subsumes another.
   489 \<close>
   490 
   491 
   492 subsection \<open>Locale declarations\<close>
   493 
   494 text \<open>
   495   \begin{matharray}{rcl}
   496     @{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   497     @{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   498     @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   499     @{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   500     @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   501     @{method_def intro_locales} & : & \<open>method\<close> \\
   502     @{method_def unfold_locales} & : & \<open>method\<close> \\
   503   \end{matharray}
   504 
   505   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   506   \indexisarelem{defines}\indexisarelem{notes}
   507   @{rail \<open>
   508     @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
   509     ;
   510     @@{command experiment} (@{syntax context_elem}*) @'begin'
   511     ;
   512     @@{command print_locale} '!'? @{syntax name}
   513     ;
   514     @@{command print_locales} ('!'?)
   515     ;
   516     @{syntax_def locale}: @{syntax context_elem}+ |
   517       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
   518     ;
   519     @{syntax_def context_elem}:
   520       @'fixes' @{syntax vars} |
   521       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
   522       @'assumes' (@{syntax props} + @'and') |
   523       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
   524       @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
   525   \<close>}
   526 
   527   \<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context
   528   consisting of a certain view of existing locales (\<open>import\<close>) plus some
   529   additional elements (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional; the
   530   degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may still be
   531   useful to collect declarations of facts later on. Type-inference on locale
   532   expressions automatically takes care of the most general typing that the
   533   combined context elements may acquire.
   534 
   535   The \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}
   536   above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are
   537   parameters of the defined locale. Locale parameters whose instantiation is
   538   omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: they are
   539   inserted at its beginning. This means that these parameters may be referred
   540   to from within the expression and also in the subsequent context elements
   541   and provides a notational convenience for the inheritance of parameters in
   542   locale declarations.
   543 
   544   The \<open>body\<close> consists of context elements.
   545 
   546     \<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<open>\<tau>\<close>
   547     and mixfix annotation \<open>mx\<close> (both are optional). The special syntax
   548     declaration ``\<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\<close> may be
   549     referenced implicitly in this context.
   550 
   551     \<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type constraint \<open>\<tau>\<close> on the
   552     local parameter \<open>x\<close>. This element is deprecated. The type constraint
   553     should be introduced in the \<^theory_text>\<open>for\<close> clause or the relevant @{element
   554     "fixes"} element.
   555 
   556     \<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces local premises, similar
   557     to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}).
   558 
   559     \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parameter.
   560     This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\
   561     \secref{sec:proof-context}), but @{element "defines"} is restricted to
   562     Pure equalities and the defined variable needs to be declared beforehand
   563     via @{element "fixes"}. The left-hand side of the equation may have
   564     additional arguments, e.g.\ ``@{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>'',
   565     which need to be free in the context.
   566 
   567     \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a local
   568     context. Most notably, this may include arbitrary declarations in any
   569     attribute specifications included here, e.g.\ a local @{attribute simp}
   570     rule.
   571 
   572   Both @{element "assumes"} and @{element "defines"} elements contribute to
   573   the locale specification. When defining an operation derived from the
   574   parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more
   575   appropriate.
   576 
   577   Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element
   578   "assumes"} and @{element "defines"} above are illegal in locale definitions.
   579   In the long goal format of \secref{sec:goals}, term bindings may be included
   580   as expected, though.
   581 
   582   \<^medskip>
   583   Locale specifications are ``closed up'' by turning the given text into a
   584   predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as
   585   local lemmas (modulo local definitions). The predicate statement covers only
   586   the newly specified assumptions, omitting the content of included locale
   587   expressions. The full cumulative view is only provided on export, involving
   588   another predicate \<open>loc\<close> that refers to the complete specification text.
   589 
   590   In any case, the predicate arguments are those locale parameters that
   591   actually occur in the respective piece of text. Also these predicates
   592   operate at the meta-level in theory, but the locale packages attempts to
   593   internalize statements according to the object-logic setup (e.g.\ replacing
   594   \<open>\<And>\<close> by \<open>\<forall>\<close>, and \<open>\<Longrightarrow>\<close> by \<open>\<longrightarrow>\<close> in HOL; see also \secref{sec:object-logic}).
   595   Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided
   596   as well.
   597 
   598   \<^descr> \<^theory_text>\<open>experiment exprs begin\<close> opens an anonymous locale context with private
   599   naming policy. Specifications in its body are inaccessible from outside.
   600   This is useful to perform experiments, without polluting the name space.
   601 
   602   \<^descr> \<^theory_text>\<open>print_locale locale\<close> prints the contents of the named locale. The
   603   command omits @{element "notes"} elements by default. Use \<^theory_text>\<open>print_locale!\<close>
   604   to have them included.
   605 
   606   \<^descr> \<^theory_text>\<open>print_locales\<close> prints the names of all locales of the current theory;
   607   the ``\<open>!\<close>'' option indicates extra verbosity.
   608 
   609   \<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations as a Hasse
   610   diagram. This includes locales defined as type classes (\secref{sec:class}).
   611   See also \<^theory_text>\<open>print_dependencies\<close> below.
   612 
   613   \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all
   614   introduction rules of locale predicates of the theory. While @{method
   615   intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore
   616   does not descend to assumptions, @{method unfold_locales} is more aggressive
   617   and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale
   618   specifications entailed by the context, both from target statements, and
   619   from interpretations (see below). New goals that are entailed by the current
   620   context are discharged automatically.
   621 \<close>
   622 
   623 
   624 subsection \<open>Locale interpretation\<close>
   625 
   626 text \<open>
   627   \begin{matharray}{rcl}
   628     @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
   629     @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
   630     @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
   631     @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
   632     @{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   633     @{command_def "print_interps"}\<open>\<^sup>*\<close> & :  & \<open>context \<rightarrow>\<close> \\
   634   \end{matharray}
   635 
   636   Locales may be instantiated, and the resulting instantiated declarations
   637   added to the current context. This requires proof (of the instantiated
   638   specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is
   639   possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), within proof
   640   bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>global_interpretation\<close>) and
   641   into locales (\<^theory_text>\<open>sublocale\<close>).
   642 
   643   @{rail \<open>
   644     @@{command interpretation} @{syntax locale_expr} equations?
   645     ;
   646     @@{command interpret} @{syntax locale_expr} equations?
   647     ;
   648     @@{command global_interpretation} @{syntax locale_expr} \<newline>
   649       definitions? equations?
   650     ;
   651     @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
   652       definitions? equations?
   653     ;
   654     @@{command print_dependencies} '!'? @{syntax locale_expr}
   655     ;
   656     @@{command print_interps} @{syntax name}
   657     ;
   658 
   659     definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
   660       @{syntax mixfix}? @'=' @{syntax term} + @'and');
   661 
   662     equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
   663   \<close>}
   664 
   665   The core of each interpretation command is a locale expression \<open>expr\<close>; the
   666   command generates proof obligations for the instantiated specifications.
   667   Once these are discharged by the user, instantiated declarations (in
   668   particular, facts) are added to the context in a post-processing phase, in a
   669   manner specific to each command.
   670 
   671   Interpretation commands are aware of interpretations that are already
   672   active: post-processing is achieved through a variant of roundup that takes
   673   interpretations of the current global or local theory into account. In order
   674   to simplify the proof obligations according to existing interpretations use
   675   methods @{method intro_locales} or @{method unfold_locales}.
   676 
   677   Given equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is
   678   interpreted, adding rewrite rules. This is particularly useful for
   679   interpreting concepts introduced through definitions. The equations must be
   680   proved the user.
   681 
   682   Given definitions \<open>defs\<close> produce corresponding definitions in the local
   683   theory's underlying target \<^emph>\<open>and\<close> amend the morphism with the equations
   684   stemming from the symmetric of those definitions. Hence these need not be
   685   proved explicitly the user. Such rewrite definitions are a even more useful
   686   device for interpreting concepts introduced through definitions, but they
   687   are only supported for interpretation commands operating in a local theory
   688   whose implementing target actually supports this.  Note that despite
   689   the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
   690   are processed sequentially without mutual recursion.
   691 
   692   \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
   693   such that its lifetime is limited to the current context block (e.g. a
   694   locale or unnamed context). At the closing @{command end} of the block the
   695   interpretation and its declarations disappear. Hence facts based on
   696   interpretation can be established without creating permanent links to the
   697   interpreted locale instances, as would be the case with @{command
   698   sublocale}.
   699 
   700   When used on the level of a global theory, there is no end of a current
   701   context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to
   702   \<^theory_text>\<open>global_interpretation\<close> then.
   703 
   704   \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> into a proof context:
   705   the interpretation and its declarations disappear when closing the current
   706   proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
   707   universally quantified.
   708 
   709   \<^descr> \<^theory_text>\<open>global_interpretation defines defs rewrites eqns\<close> interprets \<open>expr\<close>
   710   into a global theory.
   711 
   712   When adding declarations to locales, interpreted versions of these
   713   declarations are added to the global theory for all interpretations in the
   714   global theory as well. That is, interpretations into global theories
   715   dynamically participate in any declarations added to locales.
   716 
   717   Free variables in the interpreted expression are allowed. They are turned
   718   into schematic variables in the generated declarations. In order to use a
   719   free variable whose name is already bound in the context --- for example,
   720   because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
   721 
   722   \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> defines defs expr rewrites eqns\<close> interprets \<open>expr\<close>
   723   into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
   724   specification of \<open>expr\<close> is required. As in the localized version of the
   725   theorem command, the proof is in the context of \<open>name\<close>. After the proof
   726   obligation has been discharged, the locale hierarchy is changed as if \<open>name\<close>
   727   imported \<open>expr\<close> (hence the name \<^theory_text>\<open>sublocale\<close>). When the context of \<open>name\<close> is
   728   subsequently entered, traversing the locale hierarchy will involve the
   729   locale instances of \<open>expr\<close>, and their declarations will be added to the
   730   context. This makes \<^theory_text>\<open>sublocale\<close> dynamic: extensions of a locale that is
   731   instantiated in \<open>expr\<close> may take place after the \<^theory_text>\<open>sublocale\<close> declaration and
   732   still become available in the context. Circular \<^theory_text>\<open>sublocale\<close> declarations
   733   are allowed as long as they do not lead to infinite chains.
   734 
   735   If interpretations of \<open>name\<close> exist in the current global theory, the command
   736   adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
   737   only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
   738 
   739   Using equations \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break infinite
   740   chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
   741 
   742   In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
   743   locale argument must be omitted. The command then refers to the locale (or
   744   class) target of the context block.
   745 
   746   \<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an
   747   interpretation of \<open>expr\<close> in the current context. It lists all locale
   748   instances for which interpretations would be added to the current context.
   749   Variant \<^theory_text>\<open>print_dependencies!\<close> does not generalize parameters and assumes an
   750   empty context --- that is, it prints all locale instances that would be
   751   considered for interpretation. The latter is useful for understanding the
   752   dependencies of a locale expression.
   753 
   754   \<^descr> \<^theory_text>\<open>print_interps locale\<close> lists all interpretations of \<open>locale\<close> in the
   755   current theory or proof context, including those due to a combination of an
   756   \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
   757   declarations.
   758 
   759   \begin{warn}
   760     If a global theory inherits declarations (body elements) for a locale from
   761     one parent and an interpretation of that locale from another parent, the
   762     interpretation will not be applied to the declarations.
   763   \end{warn}
   764 
   765   \begin{warn}
   766     Since attributes are applied to interpreted theorems, interpretation may
   767     modify the context of common proof tools, e.g.\ the Simplifier or
   768     Classical Reasoner. As the behaviour of such tools is \<^emph>\<open>not\<close> stable under
   769     interpretation morphisms, manual declarations might have to be added to
   770     the target context of the interpretation to revert such declarations.
   771   \end{warn}
   772 
   773   \begin{warn}
   774     An interpretation in a local theory or proof context may subsume previous
   775     interpretations. This happens if the same specification fragment is
   776     interpreted twice and the instantiation of the second interpretation is
   777     more general than the interpretation of the first. The locale package does
   778     not attempt to remove subsumed interpretations.
   779   \end{warn}
   780 
   781   \begin{warn}
   782     Due to a technical limitation, the specific context of a interpretation
   783     given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
   784     \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
   785     explicit sort constraints and quantified term variables.
   786   \end{warn}
   787 
   788   \begin{warn}
   789     While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
   790     its result is discarded immediately.
   791   \end{warn}
   792 \<close>
   793 
   794 
   795 section \<open>Classes \label{sec:class}\<close>
   796 
   797 text \<open>
   798   \begin{matharray}{rcl}
   799     @{command_def "class"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   800     @{command_def "instantiation"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   801     @{command_def "instance"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   802     @{command "instance"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
   803     @{command_def "subclass"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   804     @{command_def "print_classes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   805     @{command_def "class_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   806     @{method_def intro_classes} & : & \<open>method\<close> \\
   807   \end{matharray}
   808 
   809   A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. Beyond
   810   the underlying locale, a corresponding type class is established which is
   811   interpreted logically as axiomatic type class @{cite "Wenzel:1997:TPHOL"}
   812   whose logical content are the assumptions of the locale. Thus, classes
   813   provide the full generality of locales combined with the commodity of type
   814   classes (notably type-inference). See @{cite "isabelle-classes"} for a short
   815   tutorial.
   816 
   817   @{rail \<open>
   818     @@{command class} class_spec @'begin'?
   819     ;
   820     class_spec: @{syntax name} '='
   821       ((@{syntax name} '+' (@{syntax context_elem}+)) |
   822         @{syntax name} | (@{syntax context_elem}+))
   823     ;
   824     @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'
   825     ;
   826     @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} |
   827       @{syntax name} ('<' | '\<subseteq>') @{syntax name} )
   828     ;
   829     @@{command subclass} @{syntax name}
   830     ;
   831     @@{command class_deps} (class_bounds class_bounds?)?
   832     ;
   833     class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
   834   \<close>}
   835 
   836   \<^descr> \<^theory_text>\<open>class c = superclasses + body\<close> defines a new class \<open>c\<close>, inheriting from
   837   \<open>superclasses\<close>. This introduces a locale \<open>c\<close> with import of all locales
   838   \<open>superclasses\<close>.
   839 
   840   Any @{element "fixes"} in \<open>body\<close> are lifted to the global theory level
   841   (\<^emph>\<open>class operations\<close> \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> of class \<open>c\<close>), mapping the local type
   842   parameter \<open>\<alpha>\<close> to a schematic type variable \<open>?\<alpha> :: c\<close>.
   843 
   844   Likewise, @{element "assumes"} in \<open>body\<close> are also lifted, mapping each local
   845   parameter \<open>f :: \<tau>[\<alpha>]\<close> to its corresponding global constant \<open>f :: \<tau>[?\<alpha> ::
   846   c]\<close>. The corresponding introduction rule is provided as
   847   \<open>c_class_axioms.intro\<close>. This rule should be rarely needed directly --- the
   848   @{method intro_classes} method takes care of the details of class membership
   849   proofs.
   850 
   851   \<^descr> \<^theory_text>\<open>instantiation t :: (s\<^sub>1, \<dots>, s\<^sub>n)s begin\<close> opens a target (cf.\
   852   \secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close>
   853   corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,
   854   \<alpha>\<^sub>n :: s\<^sub>n) t\<close>. A plain \<^theory_text>\<open>instance\<close> command in the target body poses a goal
   855   stating these type arities. The target is concluded by an @{command_ref
   856   (local) "end"} command.
   857 
   858   Note that a list of simultaneous type constructors may be given; this
   859   corresponds nicely to mutually recursive type definitions, e.g.\ in
   860   Isabelle/HOL.
   861 
   862   \<^descr> \<^theory_text>\<open>instance\<close> in an instantiation target body sets up a goal stating the
   863   type arities claimed at the opening \<^theory_text>\<open>instantiation\<close>. The proof would
   864   usually proceed by @{method intro_classes}, and then establish the
   865   characteristic theorems of the type classes involved. After finishing the
   866   proof, the background theory will be augmented by the proven type arities.
   867 
   868   On the theory level, \<^theory_text>\<open>instance t :: (s\<^sub>1, \<dots>, s\<^sub>n)s\<close> provides a convenient
   869   way to instantiate a type class with no need to specify operations: one can
   870   continue with the instantiation proof immediately.
   871 
   872   \<^descr> \<^theory_text>\<open>subclass c\<close> in a class context for class \<open>d\<close> sets up a goal stating that
   873   class \<open>c\<close> is logically contained in class \<open>d\<close>. After finishing the proof,
   874   class \<open>d\<close> is proven to be subclass \<open>c\<close> and the locale \<open>c\<close> is interpreted
   875   into \<open>d\<close> simultaneously.
   876 
   877   A weakened form of this is available through a further variant of @{command
   878   instance}: \<^theory_text>\<open>instance c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens a proof that class \<open>c\<^sub>2\<close> implies
   879   \<open>c\<^sub>1\<close> without reference to the underlying locales; this is useful if the
   880   properties to prove the logical connection are not sufficient on the locale
   881   level but on the theory level.
   882 
   883   \<^descr> \<^theory_text>\<open>print_classes\<close> prints all classes in the current theory.
   884 
   885   \<^descr> \<^theory_text>\<open>class_deps\<close> visualizes classes and their subclass relations as a
   886   directed acyclic graph. By default, all classes from the current theory
   887   context are show. This may be restricted by optional bounds as follows:
   888   \<^theory_text>\<open>class_deps upper\<close> or \<^theory_text>\<open>class_deps upper lower\<close>. A class is visualized, iff
   889   it is a subclass of some sort from \<open>upper\<close> and a superclass of some sort
   890   from \<open>lower\<close>.
   891 
   892   \<^descr> @{method intro_classes} repeatedly expands all class introduction rules of
   893   this theory. Note that this method usually needs not be named explicitly, as
   894   it is already included in the default proof step (e.g.\ of \<^theory_text>\<open>proof\<close>). In
   895   particular, instantiation of trivial (syntactic) classes may be performed by
   896   a single ``\<^theory_text>\<open>..\<close>'' proof step.
   897 \<close>
   898 
   899 
   900 subsection \<open>The class target\<close>
   901 
   902 text \<open>
   903   %FIXME check
   904 
   905   A named context may refer to a locale (cf.\ \secref{sec:target}). If this
   906   locale is also a class \<open>c\<close>, apart from the common locale target behaviour
   907   the following happens.
   908 
   909     \<^item> Local constant declarations \<open>g[\<alpha>]\<close> referring to the local type parameter
   910     \<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close> are accompanied by theory-level constants
   911     \<open>g[?\<alpha> :: c]\<close> referring to theory-level class operations \<open>f[?\<alpha> :: c]\<close>.
   912 
   913     \<^item> Local theorem bindings are lifted as are assumptions.
   914 
   915     \<^item> Local syntax refers to local operations \<open>g[\<alpha>]\<close> and global operations
   916     \<open>g[?\<alpha> :: c]\<close> uniformly. Type inference resolves ambiguities. In rare
   917     cases, manual type annotations are needed.
   918 \<close>
   919 
   920 
   921 subsection \<open>Co-regularity of type classes and arities\<close>
   922 
   923 text \<open>
   924   The class relation together with the collection of type-constructor arities
   925   must obey the principle of \<^emph>\<open>co-regularity\<close> as defined below.
   926 
   927   \<^medskip>
   928   For the subsequent formulation of co-regularity we assume that the class
   929   relation is closed by transitivity and reflexivity. Moreover the collection
   930   of arities \<open>t :: (\<^vec>s)c\<close> is completed such that \<open>t :: (\<^vec>s)c\<close> and
   931   \<open>c \<subseteq> c'\<close> implies \<open>t :: (\<^vec>s)c'\<close> for all such declarations.
   932 
   933   Treating sorts as finite sets of classes (meaning the intersection), the
   934   class relation \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is extended to sorts as follows:
   935   \[
   936     \<open>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\<close>
   937   \]
   938 
   939   This relation on sorts is further extended to tuples of sorts (of the same
   940   length) in the component-wise way.
   941 
   942   \<^medskip>
   943   Co-regularity of the class relation together with the arities relation
   944   means:
   945   \[
   946     \<open>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\<close>
   947   \]
   948   for all such arities. In other words, whenever the result classes of some
   949   type-constructor arities are related, then the argument sorts need to be
   950   related in the same way.
   951 
   952   \<^medskip>
   953   Co-regularity is a very fundamental property of the order-sorted algebra of
   954   types. For example, it entails principle types and most general unifiers,
   955   e.g.\ see @{cite "nipkow-prehofer"}.
   956 \<close>
   957 
   958 
   959 section \<open>Overloaded constant definitions \label{sec:overloading}\<close>
   960 
   961 text \<open>
   962   Definitions essentially express abbreviations within the logic. The simplest
   963   form of a definition is \<open>c :: \<sigma> \<equiv> t\<close>, where \<open>c\<close> is a new constant and \<open>t\<close> is
   964   a closed term that does not mention \<open>c\<close>. Moreover, so-called \<^emph>\<open>hidden
   965   polymorphism\<close> is excluded: all type variables in \<open>t\<close> need to occur in its
   966   type \<open>\<sigma>\<close>.
   967 
   968   \<^emph>\<open>Overloading\<close> means that a constant being declared as \<open>c :: \<alpha> decl\<close> may be
   969   defined separately on type instances \<open>c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n)\<kappa> decl\<close> for each
   970   type constructor \<open>\<kappa>\<close>. At most occasions overloading will be used in a
   971   Haskell-like fashion together with type classes by means of \<^theory_text>\<open>instantiation\<close>
   972   (see \secref{sec:class}). Sometimes low-level overloading is desirable; this
   973   is supported by \<^theory_text>\<open>consts\<close> and \<^theory_text>\<open>overloading\<close> explained below.
   974 
   975   The right-hand side of overloaded definitions may mention overloaded
   976   constants recursively at type instances corresponding to the immediate
   977   argument types \<open>\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n\<close>. Incomplete specification patterns impose
   978   global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand
   979   side means that all corresponding occurrences on some right-hand side need
   980   to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. Full
   981   details are given by Kun\v{c}ar @{cite "Kuncar:2015"}.
   982 
   983   \<^medskip>
   984   The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<close> target provide a convenient
   985   interface for end-users. Regular specification elements such as @{command
   986   definition}, @{command inductive}, @{command function} may be used in the
   987   body. It is also possible to use \<^theory_text>\<open>consts c :: \<sigma>\<close> with later \<^theory_text>\<open>overloading c
   988   \<equiv> c :: \<sigma>\<close> to keep the declaration and definition of a constant separate.
   989 
   990   \begin{matharray}{rcl}
   991     @{command_def "consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
   992     @{command_def "overloading"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
   993   \end{matharray}
   994 
   995   @{rail \<open>
   996     @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
   997     ;
   998     @@{command overloading} ( spec + ) @'begin'
   999     ;
  1000     spec: @{syntax name} ( '\<equiv>' | '==' ) @{syntax term} ( '(' @'unchecked' ')' )?
  1001   \<close>}
  1002 
  1003   \<^descr> \<^theory_text>\<open>consts c :: \<sigma>\<close> declares constant \<open>c\<close> to have any instance of type scheme
  1004   \<open>\<sigma>\<close>. The optional mixfix annotations may attach concrete syntax to the
  1005   constants declared.
  1006 
  1007   \<^descr> \<^theory_text>\<open>overloading x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n begin \<dots> end\<close> defines
  1008   a theory target (cf.\ \secref{sec:target}) which allows to specify already
  1009   declared constants via definitions in the body. These are identified by an
  1010   explicitly given mapping from variable names \<open>x\<^sub>i\<close> to constants \<open>c\<^sub>i\<close> at
  1011   particular type instances. The definitions themselves are established using
  1012   common specification tools, using the names \<open>x\<^sub>i\<close> as reference to the
  1013   corresponding constants.
  1014 
  1015   Option \<^theory_text>\<open>(unchecked)\<close> disables global dependency checks for the
  1016   corresponding definition, which is occasionally useful for exotic
  1017   overloading; this is a form of axiomatic specification. It is at the
  1018   discretion of the user to avoid malformed theory specifications!
  1019 \<close>
  1020 
  1021 
  1022 subsubsection \<open>Example\<close>
  1023 
  1024 consts Length :: "'a \<Rightarrow> nat"
  1025 
  1026 overloading
  1027   Length\<^sub>0 \<equiv> "Length :: unit \<Rightarrow> nat"
  1028   Length\<^sub>1 \<equiv> "Length :: 'a \<times> unit \<Rightarrow> nat"
  1029   Length\<^sub>2 \<equiv> "Length :: 'a \<times> 'b \<times> unit \<Rightarrow> nat"
  1030   Length\<^sub>3 \<equiv> "Length :: 'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat"
  1031 begin
  1032 
  1033 fun Length\<^sub>0 :: "unit \<Rightarrow> nat" where "Length\<^sub>0 () = 0"
  1034 fun Length\<^sub>1 :: "'a \<times> unit \<Rightarrow> nat" where "Length\<^sub>1 (a, ()) = 1"
  1035 fun Length\<^sub>2 :: "'a \<times> 'b \<times> unit \<Rightarrow> nat" where "Length\<^sub>2 (a, b, ()) = 2"
  1036 fun Length\<^sub>3 :: "'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" where "Length\<^sub>3 (a, b, c, ()) = 3"
  1037 
  1038 end
  1039 
  1040 lemma "Length (a, b, c, ()) = 3" by simp
  1041 lemma "Length ((a, b), (c, d), ()) = 2" by simp
  1042 lemma "Length ((a, b, c, d, e), ()) = 1" by simp
  1043 
  1044 
  1045 section \<open>Incorporating ML code \label{sec:ML}\<close>
  1046 
  1047 text \<open>
  1048   \begin{matharray}{rcl}
  1049     @{command_def "SML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1050     @{command_def "SML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1051     @{command_def "SML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1052     @{command_def "ML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1053     @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1054     @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1055     @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1056     @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
  1057     @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\
  1058     @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\
  1059     @{command_def "setup"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1060     @{command_def "local_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1061     @{command_def "attribute_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1062   \end{matharray}
  1063   \begin{tabular}{rcll}
  1064     @{attribute_def ML_print_depth} & : & \<open>attribute\<close> & default 10 \\
  1065     @{attribute_def ML_source_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
  1066     @{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
  1067     @{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
  1068     @{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
  1069   \end{tabular}
  1070 
  1071   @{rail \<open>
  1072     (@@{command SML_file} |
  1073       @@{command SML_file_debug} |
  1074       @@{command SML_file_no_debug} |
  1075       @@{command ML_file} |
  1076       @@{command ML_file_debug} |
  1077       @@{command ML_file_no_debug}) @{syntax name} ';'?
  1078     ;
  1079     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
  1080       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
  1081     ;
  1082     @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
  1083   \<close>}
  1084 
  1085   \<^descr> \<^theory_text>\<open>SML_file name\<close> reads and evaluates the given Standard ML file. Top-level
  1086   SML bindings are stored within the (global or local) theory context; the
  1087   initial environment is restricted to the Standard ML implementation of
  1088   Poly/ML, without the many add-ons of Isabelle/ML. Multiple \<^theory_text>\<open>SML_file\<close>
  1089   commands may be used to build larger Standard ML projects, independently of
  1090   the regular Isabelle/ML environment.
  1091 
  1092   \<^descr> \<^theory_text>\<open>ML_file name\<close> reads and evaluates the given ML file. The current theory
  1093   context is passed down to the ML toplevel and may be modified, using @{ML
  1094   "Context.>>"} or derived ML commands. Top-level ML bindings are stored
  1095   within the (global or local) theory context.
  1096 
  1097   \<^descr> \<^theory_text>\<open>SML_file_debug\<close>, \<^theory_text>\<open>SML_file_no_debug\<close>, \<^theory_text>\<open>ML_file_debug\<close>, and
  1098   \<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while
  1099   the given file is compiled.
  1100 
  1101   \<^descr> \<^theory_text>\<open>ML text\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given
  1102   \<open>text\<close>. Top-level ML bindings are stored within the (global or local) theory
  1103   context.
  1104 
  1105   \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
  1106   Top-level ML bindings are stored within the proof context in a purely
  1107   sequential fashion, disregarding the nested proof structure. ML bindings
  1108   introduced by \<^theory_text>\<open>ML_prf\<close> are discarded at the end of the proof.
  1109 
  1110   \<^descr> \<^theory_text>\<open>ML_val\<close> and \<^theory_text>\<open>ML_command\<close> are diagnostic versions of \<^theory_text>\<open>ML\<close>, which means
  1111   that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced
  1112   at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent.
  1113 
  1114   \<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>,
  1115   which refers to an ML expression of type @{ML_type "theory -> theory"}. This
  1116   enables to initialize any object-logic specific tools and packages written
  1117   in ML, for example.
  1118 
  1119   \<^descr> \<^theory_text>\<open>local_setup\<close> is similar to \<^theory_text>\<open>setup\<close> for a local theory context, and an
  1120   ML expression of type @{ML_type "local_theory -> local_theory"}. This allows
  1121   to invoke local theory specification packages without going through concrete
  1122   outer syntax, for example.
  1123 
  1124   \<^descr> \<^theory_text>\<open>attribute_setup name = "text" description\<close> defines an attribute in the
  1125   current context. The given \<open>text\<close> has to be an ML expression of type
  1126   @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
  1127   structure @{ML_structure Args} and @{ML_structure Attrib}.
  1128 
  1129   In principle, attributes can operate both on a given theorem and the
  1130   implicit context, although in practice only one is modified and the other
  1131   serves as parameter. Here are examples for these two cases:
  1132 \<close>
  1133 
  1134 (*<*)experiment begin(*>*)
  1135         attribute_setup my_rule =
  1136           \<open>Attrib.thms >> (fn ths =>
  1137             Thm.rule_attribute ths
  1138               (fn context: Context.generic => fn th: thm =>
  1139                 let val th' = th OF ths
  1140                 in th' end))\<close>
  1141 
  1142         attribute_setup my_declaration =
  1143           \<open>Attrib.thms >> (fn ths =>
  1144             Thm.declaration_attribute
  1145               (fn th: thm => fn context: Context.generic =>
  1146                 let val context' = context
  1147                 in context' end))\<close>
  1148 (*<*)end(*>*)
  1149 
  1150 text \<open>
  1151   \<^descr> @{attribute ML_print_depth} controls the printing depth of the ML toplevel
  1152   pretty printer. Typically the limit should be less than 10. Bigger values
  1153   such as 100--1000 are occasionally useful for debugging.
  1154 
  1155   \<^descr> @{attribute ML_source_trace} indicates whether the source text that is
  1156   given to the ML compiler should be output: it shows the raw Standard ML
  1157   after expansion of Isabelle/ML antiquotations.
  1158 
  1159   \<^descr> @{attribute ML_debugger} controls compilation of sources with or without
  1160   debugging information. The global system option @{system_option_ref
  1161   ML_debugger} does the same when building a session image. It is also
  1162   possible use commands like \<^theory_text>\<open>ML_file_debug\<close> etc. The ML debugger is
  1163   explained further in @{cite "isabelle-jedit"}.
  1164 
  1165   \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system
  1166   should print a detailed stack trace on exceptions. The result is dependent
  1167   on various ML compiler optimizations. The boundary for the exception trace
  1168   is the current Isar command transactions: it is occasionally better to
  1169   insert the combinator @{ML Runtime.exn_trace} into ML code for debugging
  1170   @{cite "isabelle-implementation"}, closer to the point where it actually
  1171   happens.
  1172 
  1173   \<^descr> @{attribute ML_exception_debugger} controls detailed exception trace via
  1174   the Poly/ML debugger, at the cost of extra compile-time and run-time
  1175   overhead. Relevant ML modules need to be compiled beforehand with debugging
  1176   enabled, see @{attribute ML_debugger} above.
  1177 \<close>
  1178 
  1179 
  1180 section \<open>External file dependencies\<close>
  1181 
  1182 text \<open>
  1183   \begin{matharray}{rcl}
  1184     @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
  1185   \end{matharray}
  1186 
  1187   @{rail \<open>@@{command external_file} @{syntax name} ';'?\<close>}
  1188 
  1189   \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
  1190   name, such that the Isabelle build process knows about it (see also @{cite
  1191   "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via @{ML
  1192   File.read}, without specific management by the Prover IDE.
  1193 \<close>
  1194 
  1195 
  1196 
  1197 section \<open>Primitive specification elements\<close>
  1198 
  1199 subsection \<open>Sorts\<close>
  1200 
  1201 text \<open>
  1202   \begin{matharray}{rcll}
  1203     @{command_def "default_sort"} & : & \<open>local_theory \<rightarrow> local_theory\<close>
  1204   \end{matharray}
  1205 
  1206   @{rail \<open>
  1207     @@{command default_sort} @{syntax sort}
  1208   \<close>}
  1209 
  1210   \<^descr> \<^theory_text>\<open>default_sort s\<close> makes sort \<open>s\<close> the new default sort for any type
  1211   variable that is given explicitly in the text, but lacks a sort constraint
  1212   (wrt.\ the current context). Type variables generated by type inference are
  1213   not affected.
  1214 
  1215   Usually the default sort is only changed when defining a new object-logic.
  1216   For example, the default sort in Isabelle/HOL is @{class type}, the class of
  1217   all HOL types.
  1218 
  1219   When merging theories, the default sorts of the parents are logically
  1220   intersected, i.e.\ the representations as lists of classes are joined.
  1221 \<close>
  1222 
  1223 
  1224 subsection \<open>Types \label{sec:types-pure}\<close>
  1225 
  1226 text \<open>
  1227   \begin{matharray}{rcll}
  1228     @{command_def "type_synonym"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1229     @{command_def "typedecl"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1230   \end{matharray}
  1231 
  1232   @{rail \<open>
  1233     @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
  1234     ;
  1235     @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
  1236   \<close>}
  1237 
  1238   \<^descr> \<^theory_text>\<open>type_synonym (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>\<close> introduces a \<^emph>\<open>type synonym\<close> \<open>(\<alpha>\<^sub>1, \<dots>,
  1239   \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in
  1240   Isabelle/HOL, type synonyms are merely syntactic abbreviations without any
  1241   logical significance. Internally, type synonyms are fully expanded.
  1242 
  1243   \<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the
  1244   object-logic defines a base sort \<open>s\<close>, then the constructor is declared to
  1245   operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.
  1246 
  1247 
  1248   \begin{warn}
  1249     If you introduce a new type axiomatically, i.e.\ via @{command_ref
  1250     typedecl} and @{command_ref axiomatization}
  1251     (\secref{sec:axiomatizations}), the minimum requirement is that it has a
  1252     non-empty model, to avoid immediate collapse of the logical environment.
  1253     Moreover, one needs to demonstrate that the interpretation of such
  1254     free-form axiomatizations can coexist with other axiomatization schemes
  1255     for types, notably @{command_def typedef} in Isabelle/HOL
  1256     (\secref{sec:hol-typedef}), or any other extension that people might have
  1257     introduced elsewhere.
  1258   \end{warn}
  1259 \<close>
  1260 
  1261 
  1262 section \<open>Naming existing theorems \label{sec:theorems}\<close>
  1263 
  1264 text \<open>
  1265   \begin{matharray}{rcll}
  1266     @{command_def "lemmas"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1267     @{command_def "named_theorems"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1268   \end{matharray}
  1269 
  1270   @{rail \<open>
  1271     @@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and')
  1272       @{syntax for_fixes}
  1273     ;
  1274     @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
  1275   \<close>}
  1276 
  1277   \<^descr> \<^theory_text>\<open>lemmas a = b\<^sub>1 \<dots> b\<^sub>n\<close>~@{keyword_def "for"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close> evaluates given
  1278   facts (with attributes) in the current context, which may be augmented by
  1279   local variables. Results are standardized before being stored, i.e.\
  1280   schematic variables are renamed to enforce index \<open>0\<close> uniformly.
  1281 
  1282   \<^descr> \<^theory_text>\<open>named_theorems name description\<close> declares a dynamic fact within the
  1283   context. The same \<open>name\<close> is used to define an attribute with the usual
  1284   \<open>add\<close>/\<open>del\<close> syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the
  1285   content incrementally, in canonical declaration order of the text structure.
  1286 \<close>
  1287 
  1288 
  1289 section \<open>Oracles\<close>
  1290 
  1291 text \<open>
  1292   \begin{matharray}{rcll}
  1293     @{command_def "oracle"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\
  1294   \end{matharray}
  1295 
  1296   Oracles allow Isabelle to take advantage of external reasoners such as
  1297   arithmetic decision procedures, model checkers, fast tautology checkers or
  1298   computer algebra systems. Invoked as an oracle, an external reasoner can
  1299   create arbitrary Isabelle theorems.
  1300 
  1301   It is the responsibility of the user to ensure that the external reasoner is
  1302   as trustworthy as the application requires. Another typical source of errors
  1303   is the linkup between Isabelle and the external tool, not just its concrete
  1304   implementation, but also the required translation between two different
  1305   logical environments.
  1306 
  1307   Isabelle merely guarantees well-formedness of the propositions being
  1308   asserted, and records within the internal derivation object how presumed
  1309   theorems depend on unproven suppositions.
  1310 
  1311   @{rail \<open>
  1312     @@{command oracle} @{syntax name} '=' @{syntax text}
  1313   \<close>}
  1314 
  1315   \<^descr> \<^theory_text>\<open>oracle name = "text"\<close> turns the given ML expression \<open>text\<close> of type
  1316   @{ML_text "'a -> cterm"} into an ML function of type @{ML_text "'a -> thm"},
  1317   which is bound to the global identifier @{ML_text name}. This acts like an
  1318   infinitary specification of axioms! Invoking the oracle only works within
  1319   the scope of the resulting theory.
  1320 
  1321 
  1322   See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
  1323   primitive rule as oracle, and turning it into a proof method.
  1324 \<close>
  1325 
  1326 
  1327 section \<open>Name spaces\<close>
  1328 
  1329 text \<open>
  1330   \begin{matharray}{rcl}
  1331     @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1332     @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  1333     @{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1334     @{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1335     @{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1336     @{command_def "hide_fact"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1337   \end{matharray}
  1338 
  1339   @{rail \<open>
  1340     (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}
  1341     ;
  1342     (@{command hide_class} | @{command hide_type} |
  1343       @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )
  1344   \<close>}
  1345 
  1346   Isabelle organizes any kind of name declarations (of types, constants,
  1347   theorems etc.) by separate hierarchically structured name spaces. Normally
  1348   the user does not have to control the behaviour of name spaces by hand, yet
  1349   the following commands provide some way to do so.
  1350 
  1351   \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type
  1352   constructors, respectively. This allows adhoc changes to name-space
  1353   accesses.
  1354 
  1355   \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.
  1356 
  1357   \<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name
  1358   space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.
  1359 
  1360   Note that hiding name space accesses has no impact on logical declarations
  1361   --- they remain valid internally. Entities that are no longer accessible to
  1362   the user are printed with the special qualifier ``\<open>??\<close>'' prefixed to the
  1363   full internal name.
  1364 
  1365   \<^descr> \<^theory_text>\<open>hide_type\<close>, \<^theory_text>\<open>hide_const\<close>, and \<^theory_text>\<open>hide_fact\<close> are similar to
  1366   \<^theory_text>\<open>hide_class\<close>, but hide types, constants, and facts, respectively.
  1367 \<close>
  1368 
  1369 end