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