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