doc-src/IsarRef/Thy/document/Spec.tex
author wenzelm
Thu Mar 12 00:02:30 2009 +0100 (2009-03-12)
changeset 30463 f1cb00030d4f
parent 30242 aea5d7fa7ef5
child 30527 fae488569faf
permissions -rw-r--r--
updated generated files;
     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' 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   \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
   295   current local theory context.  No theorem binding is involved here,
   296   unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
   297   \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
   298   of applying attributes as included in the theorem specification.
   299 
   300   \end{description}%
   301 \end{isamarkuptext}%
   302 \isamarkuptrue%
   303 %
   304 \isamarkupsection{Locales \label{sec:locale}%
   305 }
   306 \isamarkuptrue%
   307 %
   308 \begin{isamarkuptext}%
   309 Locales are named local contexts, consisting of a list of
   310   declaration elements that are modeled after the Isar proof context
   311   commands (cf.\ \secref{sec:proof-context}).%
   312 \end{isamarkuptext}%
   313 \isamarkuptrue%
   314 %
   315 \isamarkupsubsection{Locale specifications%
   316 }
   317 \isamarkuptrue%
   318 %
   319 \begin{isamarkuptext}%
   320 \begin{matharray}{rcl}
   321     \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   322     \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}} \\
   323     \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}} \\
   324     \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isa{method} \\
   325     \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\
   326   \end{matharray}
   327 
   328   \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
   329   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   330   \indexisarelem{defines}\indexisarelem{notes}
   331   \begin{rail}
   332     'locale' name ('=' localeexpr)? 'begin'?
   333     ;
   334     'print\_locale' '!'? localeexpr
   335     ;
   336     localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
   337     ;
   338 
   339     contextexpr: nameref | '(' contextexpr ')' |
   340     (contextexpr (name mixfix? +)) | (contextexpr + '+')
   341     ;
   342     contextelem: fixes | constrains | assumes | defines | notes
   343     ;
   344     fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
   345     ;
   346     constrains: 'constrains' (name '::' type + 'and')
   347     ;
   348     assumes: 'assumes' (thmdecl? props + 'and')
   349     ;
   350     defines: 'defines' (thmdecl? prop proppat? + 'and')
   351     ;
   352     notes: 'notes' (thmdef? thmrefs + 'and')
   353     ;
   354   \end{rail}
   355 
   356   \begin{description}
   357   
   358   \item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}} defines a
   359   new locale \isa{loc} as a context consisting of a certain view of
   360   existing locales (\isa{import}) plus some additional elements
   361   (\isa{body}).  Both \isa{import} and \isa{body} are optional;
   362   the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
   363   locale, which may still be useful to collect declarations of facts
   364   later on.  Type-inference on locale expressions automatically takes
   365   care of the most general typing that the combined context elements
   366   may acquire.
   367 
   368   The \isa{import} consists of a structured context expression,
   369   consisting of references to existing locales, renamed contexts, or
   370   merged contexts.  Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
   371   parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
   372   position.  Renaming by default deletes concrete syntax, but new
   373   syntax may by specified with a mixfix annotation.  An exeption of
   374   this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
   375   be changed.  Merging proceeds from left-to-right, suppressing any
   376   duplicates stemming from different paths through the import
   377   hierarchy.
   378 
   379   The \isa{body} consists of basic context elements, further context
   380   expressions may be included as well.
   381 
   382   \begin{description}
   383 
   384   \item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares a local
   385   parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
   386   are optional).  The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
   387   implicitly in this context.
   388 
   389   \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type
   390   constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
   391 
   392   \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}
   393   introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
   394   proof (cf.\ \secref{sec:proof-context}).
   395 
   396   \item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} defines a previously
   397   declared parameter.  This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
   398   proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
   399   takes an equational proposition instead of variable-term pair.  The
   400   left-hand side of the equation may have additional arguments, e.g.\
   401   ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
   402 
   403   \item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}
   404   reconsiders facts within a local context.  Most notably, this may
   405   include arbitrary declarations in any attribute specifications
   406   included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
   407 
   408   The initial \isa{import} specification of a locale expression
   409   maintains a dynamic relation to the locales being referenced
   410   (benefiting from any later fact declarations in the obvious manner).
   411 
   412   \end{description}
   413   
   414   Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
   415   in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
   416   are illegal in locale definitions.  In the long goal format of
   417   \secref{sec:goals}, term bindings may be included as expected,
   418   though.
   419   
   420   \medskip By default, locale specifications are ``closed up'' by
   421   turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
   422   (modulo local definitions).  The predicate statement covers only the
   423   newly specified assumptions, omitting the content of included locale
   424   expressions.  The full cumulative view is only provided on export,
   425   involving another predicate \isa{loc} that refers to the complete
   426   specification text.
   427   
   428   In any case, the predicate arguments are those locale parameters
   429   that actually occur in the respective piece of text.  Also note that
   430   these predicates operate at the meta-level in theory, but the locale
   431   packages attempts to internalize statements according to the
   432   object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
   433   \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
   434   \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
   435   
   436   \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
   437   specified locale expression in a flattened form.  The notable
   438   special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
   439   contents of the named locale, but keep in mind that type-inference
   440   will normalize type variables according to the usual alphabetical
   441   order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
   442   Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
   443 
   444   \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
   445   of the current theory.
   446 
   447   \item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}
   448   repeatedly expand all introduction rules of locale predicates of the
   449   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
   450   assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
   451   \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale
   452   specifications entailed by the context, both from target statements,
   453   and from interpretations (see below).  New goals that are entailed
   454   by the current context are discharged automatically.
   455 
   456   \end{description}%
   457 \end{isamarkuptext}%
   458 \isamarkuptrue%
   459 %
   460 \isamarkupsubsection{Interpretation of locales%
   461 }
   462 \isamarkuptrue%
   463 %
   464 \begin{isamarkuptext}%
   465 Locale expressions (more precisely, \emph{context expressions}) may
   466   be instantiated, and the instantiated facts added to the current
   467   context.  This requires a proof of the instantiated specification
   468   and is called \emph{locale interpretation}.  Interpretation is
   469   possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
   470 
   471   \begin{matharray}{rcl}
   472     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   473     \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   474   \end{matharray}
   475 
   476   \indexouternonterm{interp}
   477   \begin{rail}
   478     'interpretation' (interp | name ('<' | subseteq) contextexpr)
   479     ;
   480     'interpret' interp
   481     ;
   482     instantiation: ('[' (inst+) ']')?
   483     ;
   484     interp: (name ':')? \\ (contextexpr instantiation |
   485       name instantiation 'where' (thmdecl? prop + 'and'))
   486     ;
   487   \end{rail}
   488 
   489   \begin{description}
   490 
   491   \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
   492 
   493   The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory.  The instantiation is given as a list of terms
   494   \isa{insts} and is positional.  All parameters must receive an
   495   instantiation term --- with the exception of defined parameters.
   496   These are, if omitted, derived from the defining equation and other
   497   instantiations.  Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
   498 
   499   The command generates proof obligations for the instantiated
   500   specifications (assumes and defines elements).  Once these are
   501   discharged by the user, instantiated facts are added to the theory
   502   in a post-processing phase.
   503 
   504   Additional equations, which are unfolded in facts during
   505   post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
   506   This is useful for interpreting concepts introduced through
   507   definition specification elements.  The equations must be proved.
   508   Note that if equations are present, the context expression is
   509   restricted to a locale name.
   510 
   511   The command is aware of interpretations already active in the
   512   theory, but does not simplify the goal automatically.  In order to
   513   simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}
   514   or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}.  Post-processing is not applied to
   515   facts of interpretations that are already active.  This avoids
   516   duplication of interpreted facts, in particular.  Note that, in the
   517   case of a locale with import, parts of the interpretation may
   518   already be active.  The command will only process facts for new
   519   parts.
   520 
   521   The context expression may be preceded by a name, which takes effect
   522   in the post-processing of facts.  It is used to prefix fact names,
   523   for example to avoid accidental hiding of other facts.
   524 
   525   Adding facts to locales has the effect of adding interpreted facts
   526   to the theory for all active interpretations also.  That is,
   527   interpretations dynamically participate in any facts added to
   528   locales.
   529 
   530   \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
   531 
   532   This form of the command interprets \isa{expr} in the locale
   533   \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the
   534   localized version of the theorem command, the proof is in the
   535   context of \isa{name}.  After the proof obligation has been
   536   dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
   537   context \isa{name} is subsequently entered.  Note that, like
   538   import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
   539   Like facts of renamed context elements, facts obtained by
   540   interpretation may be accessed by prefixing with the parameter
   541   renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
   542 
   543   Unlike interpretation in theories, instantiation is confined to the
   544   renaming of parameters, which may be specified as part of the
   545   context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
   546 
   547   Only specification fragments of \isa{expr} that are not already
   548   part of \isa{name} (be it imported, derived or a derived fragment
   549   of the import) are considered by interpretation.  This enables
   550   circular interpretations.
   551 
   552   If interpretations of \isa{name} exist in the current theory, the
   553   command adds interpretations for \isa{expr} as well, with the same
   554   prefix and attributes, although only for fragments of \isa{expr}
   555   that are not interpreted in the theory already.
   556 
   557   \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
   558   interprets \isa{expr} in the proof context and is otherwise
   559   similar to interpretation in theories.
   560 
   561   \end{description}
   562 
   563   \begin{warn}
   564     Since attributes are applied to interpreted theorems,
   565     interpretation may modify the context of common proof tools, e.g.\
   566     the Simplifier or Classical Reasoner.  Since the behavior of such
   567     automated reasoning tools is \emph{not} stable under
   568     interpretation morphisms, manual declarations might have to be
   569     issued.
   570   \end{warn}
   571 
   572   \begin{warn}
   573     An interpretation in a theory may subsume previous
   574     interpretations.  This happens if the same specification fragment
   575     is interpreted twice and the instantiation of the second
   576     interpretation is more general than the interpretation of the
   577     first.  A warning is issued, since it is likely that these could
   578     have been generalized in the first place.  The locale package does
   579     not attempt to remove subsumed interpretations.
   580   \end{warn}%
   581 \end{isamarkuptext}%
   582 \isamarkuptrue%
   583 %
   584 \isamarkupsection{Classes \label{sec:class}%
   585 }
   586 \isamarkuptrue%
   587 %
   588 \begin{isamarkuptext}%
   589 A class is a particular locale with \emph{exactly one} type variable
   590   \isa{{\isasymalpha}}.  Beyond the underlying locale, a corresponding type class
   591   is established which is interpreted logically as axiomatic type
   592   class \cite{Wenzel:1997:TPHOL} whose logical content are the
   593   assumptions of the locale.  Thus, classes provide the full
   594   generality of locales combined with the commodity of type classes
   595   (notably type-inference).  See \cite{isabelle-classes} for a short
   596   tutorial.
   597 
   598   \begin{matharray}{rcl}
   599     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   600     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   601     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   602     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   603     \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}} \\
   604     \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}} \\
   605     \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\
   606   \end{matharray}
   607 
   608   \begin{rail}
   609     'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
   610       'begin'?
   611     ;
   612     'instantiation' (nameref + 'and') '::' arity 'begin'
   613     ;
   614     'instance'
   615     ;
   616     'subclass' target? nameref
   617     ;
   618     'print\_classes'
   619     ;
   620     'class\_deps'
   621     ;
   622 
   623     superclassexpr: nameref | (nameref '+' superclassexpr)
   624     ;
   625   \end{rail}
   626 
   627   \begin{description}
   628 
   629   \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}} defines
   630   a new class \isa{c}, inheriting from \isa{superclasses}.  This
   631   introduces a locale \isa{c} with import of all locales \isa{superclasses}.
   632 
   633   Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
   634   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
   635   \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
   636 
   637   Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
   638   mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
   639   corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.  The
   640   corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}.  This rule should be rarely needed directly
   641   --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
   642   class membership proofs.
   643 
   644   \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
   645   allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding
   646   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
   647   target body poses a goal stating these type arities.  The target is
   648   concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
   649 
   650   Note that a list of simultaneous type constructors may be given;
   651   this corresponds nicely to mutual recursive type definitions, e.g.\
   652   in Isabelle/HOL.
   653 
   654   \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
   655   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
   656   the type classes involved.  After finishing the proof, the
   657   background theory will be augmented by the proven type arities.
   658 
   659   \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
   660   \isa{d} sets up a goal stating that class \isa{c} is logically
   661   contained in class \isa{d}.  After finishing the proof, class
   662   \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
   663 
   664   \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
   665   theory.
   666 
   667   \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes all classes and their
   668   subclass relations as a Hasse diagram.
   669 
   670   \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class
   671   introduction rules of this theory.  Note that this method usually
   672   needs not be named explicitly, as it is already included in the
   673   default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).  In particular,
   674   instantiation of trivial (syntactic) classes may be performed by a
   675   single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
   676 
   677   \end{description}%
   678 \end{isamarkuptext}%
   679 \isamarkuptrue%
   680 %
   681 \isamarkupsubsection{The class target%
   682 }
   683 \isamarkuptrue%
   684 %
   685 \begin{isamarkuptext}%
   686 %FIXME check
   687 
   688   A named context may refer to a locale (cf.\ \secref{sec:target}).
   689   If this locale is also a class \isa{c}, apart from the common
   690   locale target behaviour the following happens.
   691 
   692   \begin{itemize}
   693 
   694   \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
   695   local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
   696   are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
   697   referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
   698 
   699   \item Local theorem bindings are lifted as are assumptions.
   700 
   701   \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
   702   global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly.  Type inference
   703   resolves ambiguities.  In rare cases, manual type annotations are
   704   needed.
   705   
   706   \end{itemize}%
   707 \end{isamarkuptext}%
   708 \isamarkuptrue%
   709 %
   710 \isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
   711 }
   712 \isamarkuptrue%
   713 %
   714 \begin{isamarkuptext}%
   715 \begin{matharray}{rcl}
   716     \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   717     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
   718   \end{matharray}
   719 
   720   Axiomatic type classes are Isabelle/Pure's primitive
   721   \emph{definitional} interface to type classes.  For practical
   722   applications, you should consider using classes
   723   (cf.~\secref{sec:classes}) which provide high level interface.
   724 
   725   \begin{rail}
   726     'axclass' classdecl (axmdecl prop +)
   727     ;
   728     'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
   729     ;
   730   \end{rail}
   731 
   732   \begin{description}
   733   
   734   \item \hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}} defines an
   735   axiomatic type class as the intersection of existing classes, with
   736   additional axioms holding.  Class axioms may not contain more than
   737   one type variable.  The class axioms (with implicit sort constraints
   738   added) are bound to the given names.  Furthermore a class
   739   introduction rule is generated (being bound as \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
   740   
   741   The ``class axioms'' (which are derived from the internal class
   742   definition) are stored as theorems according to the given name
   743   specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added
   744   here.  The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
   745   
   746   \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and \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}} setup a goal stating a class
   747   relation or type arity.  The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
   748   the type classes involved.  After finishing the proof, the theory
   749   will be augmented by a type signature declaration corresponding to
   750   the resulting theorem.
   751 
   752   \end{description}%
   753 \end{isamarkuptext}%
   754 \isamarkuptrue%
   755 %
   756 \isamarkupsection{Unrestricted overloading%
   757 }
   758 \isamarkuptrue%
   759 %
   760 \begin{isamarkuptext}%
   761 Isabelle/Pure's definitional schemes support certain forms of
   762   overloading (see \secref{sec:consts}).  At most occassions
   763   overloading will be used in a Haskell-like fashion together with
   764   type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
   765   \secref{sec:class}).  Sometimes low-level overloading is desirable.
   766   The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
   767   end-users.
   768 
   769   \begin{matharray}{rcl}
   770     \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   771   \end{matharray}
   772 
   773   \begin{rail}
   774     'overloading' \\
   775     ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
   776   \end{rail}
   777 
   778   \begin{description}
   779 
   780   \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}}
   781   opens a theory target (cf.\ \secref{sec:target}) which allows to
   782   specify constants with overloaded definitions.  These are identified
   783   by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to
   784   constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances.  The
   785   definitions themselves are established using common specification
   786   tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the
   787   corresponding constants.  The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
   788 
   789   A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
   790   the corresponding definition, which is occasionally useful for
   791   exotic overloading.  It is at the discretion of the user to avoid
   792   malformed theory specifications!
   793 
   794   \end{description}%
   795 \end{isamarkuptext}%
   796 \isamarkuptrue%
   797 %
   798 \isamarkupsection{Incorporating ML code \label{sec:ML}%
   799 }
   800 \isamarkuptrue%
   801 %
   802 \begin{isamarkuptext}%
   803 \begin{matharray}{rcl}
   804     \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   805     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   806     \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
   807     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   808     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   809     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   810     \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}} \\
   811   \end{matharray}
   812 
   813   \begin{mldecls}
   814     \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
   815     \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   816   \end{mldecls}
   817 
   818   \begin{rail}
   819     'use' name
   820     ;
   821     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
   822     ;
   823   \end{rail}
   824 
   825   \begin{description}
   826 
   827   \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML
   828   commands from \isa{{\isachardoublequote}file{\isachardoublequote}}.  The current theory context is passed
   829   down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands.  The file name is checked with
   830   the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
   831   header (see also \secref{sec:begin-thy}).
   832 
   833   Top-level ML bindings are stored within the (global or local) theory
   834   context.
   835   
   836   \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
   837   but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
   838   Top-level ML bindings are stored within the (global or local) theory
   839   context.
   840 
   841   \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
   842   within a proof context.
   843 
   844   Top-level ML bindings are stored within the proof context in a
   845   purely sequential fashion, disregarding the nested proof structure.
   846   ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the
   847   end of the proof.
   848 
   849   \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic
   850   versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
   851   updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML
   852   toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
   853   
   854   \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
   855   context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
   856   of type \verb|theory -> theory|.  This enables to initialize
   857   any object-logic specific tools and packages written in ML, for
   858   example.
   859 
   860   \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
   861   a local theory context, and an ML expression of type \verb|local_theory -> local_theory|.  This allows to
   862   invoke local theory specification packages without going through
   863   concrete outer syntax, for example.
   864 
   865   \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
   866   theorems produced in ML both in the theory context and the ML
   867   toplevel, associating it with the provided name.  Theorems are put
   868   into a global ``standard'' format before being stored.
   869 
   870   \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
   871   singleton theorem.
   872   
   873   \end{description}%
   874 \end{isamarkuptext}%
   875 \isamarkuptrue%
   876 %
   877 \isamarkupsection{Primitive specification elements%
   878 }
   879 \isamarkuptrue%
   880 %
   881 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
   882 }
   883 \isamarkuptrue%
   884 %
   885 \begin{isamarkuptext}%
   886 \begin{matharray}{rcll}
   887     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   888     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   889     \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   890     \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}} \\
   891   \end{matharray}
   892 
   893   \begin{rail}
   894     'classes' (classdecl +)
   895     ;
   896     'classrel' (nameref ('<' | subseteq) nameref + 'and')
   897     ;
   898     'defaultsort' sort
   899     ;
   900   \end{rail}
   901 
   902   \begin{description}
   903 
   904   \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
   905   \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.
   906   Isabelle implicitly maintains the transitive closure of the class
   907   hierarchy.  Cyclic class structures are not permitted.
   908 
   909   \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
   910   relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
   911   This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
   912   (see \secref{sec:axclass}) provides a way to introduce proven class
   913   relations.
   914 
   915   \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
   916   new default sort for any type variable that is given explicitly in
   917   the text, but lacks a sort constraint (wrt.\ the current context).
   918   Type variables generated by type inference are not affected.
   919 
   920   Usually the default sort is only changed when defining a new
   921   object-logic.  For example, the default sort in Isabelle/HOL is
   922   \isa{type}, the class of all HOL types.  %FIXME sort antiq?
   923 
   924   When merging theories, the default sorts of the parents are
   925   logically intersected, i.e.\ the representations as lists of classes
   926   are joined.
   927 
   928   \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation,
   929   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
   930 
   931   \end{description}%
   932 \end{isamarkuptext}%
   933 \isamarkuptrue%
   934 %
   935 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
   936 }
   937 \isamarkuptrue%
   938 %
   939 \begin{isamarkuptext}%
   940 \begin{matharray}{rcll}
   941     \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   942     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   943     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   944   \end{matharray}
   945 
   946   \begin{rail}
   947     'types' (typespec '=' type infix? +)
   948     ;
   949     'typedecl' typespec infix?
   950     ;
   951     'arities' (nameref '::' arity +)
   952     ;
   953   \end{rail}
   954 
   955   \begin{description}
   956 
   957   \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
   958   \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type
   959   \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.  Unlike actual type definitions, as are available in
   960   Isabelle/HOL for example, type synonyms are merely syntactic
   961   abbreviations without any logical significance.  Internally, type
   962   synonyms are fully expanded.
   963   
   964   \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
   965   type constructor \isa{t}.  If the object-logic defines a base sort
   966   \isa{s}, then the constructor is declared to operate on that, via
   967   the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.
   968 
   969   \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
   970   Isabelle's order-sorted signature of types by new type constructor
   971   arities.  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
   972   command (see \secref{sec:axclass}) provides a way to introduce
   973   proven type arities.
   974 
   975   \end{description}%
   976 \end{isamarkuptext}%
   977 \isamarkuptrue%
   978 %
   979 \isamarkupsubsection{Co-regularity of type classes and arities%
   980 }
   981 \isamarkuptrue%
   982 %
   983 \begin{isamarkuptext}%
   984 The class relation together with the collection of
   985   type-constructor arities must obey the principle of
   986   \emph{co-regularity} as defined below.
   987 
   988   \medskip For the subsequent formulation of co-regularity we assume
   989   that the class relation is closed by transitivity and reflexivity.
   990   Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is
   991   completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}
   992   implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.
   993 
   994   Treating sorts as finite sets of classes (meaning the intersection),
   995   the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as
   996   follows:
   997   \[
   998     \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}}
   999   \]
  1000 
  1001   This relation on sorts is further extended to tuples of sorts (of
  1002   the same length) in the component-wise way.
  1003 
  1004   \smallskip Co-regularity of the class relation together with the
  1005   arities relation means:
  1006   \[
  1007     \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}}
  1008   \]
  1009   \noindent for all such arities.  In other words, whenever the result
  1010   classes of some type-constructor arities are related, then the
  1011   argument sorts need to be related in the same way.
  1012 
  1013   \medskip Co-regularity is a very fundamental property of the
  1014   order-sorted algebra of types.  For example, it entails principle
  1015   types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
  1016 \end{isamarkuptext}%
  1017 \isamarkuptrue%
  1018 %
  1019 \isamarkupsubsection{Constants and definitions \label{sec:consts}%
  1020 }
  1021 \isamarkuptrue%
  1022 %
  1023 \begin{isamarkuptext}%
  1024 Definitions essentially express abbreviations within the logic.  The
  1025   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
  1026   where the arguments of \isa{c} appear on the left, abbreviating a
  1027   prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
  1028   written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.  Moreover,
  1029   definitions may be weakened by adding arbitrary pre-conditions:
  1030   \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
  1031 
  1032   \medskip The built-in well-formedness conditions for definitional
  1033   specifications are:
  1034 
  1035   \begin{itemize}
  1036 
  1037   \item Arguments (on the left-hand side) must be distinct variables.
  1038 
  1039   \item All variables on the right-hand side must also appear on the
  1040   left-hand side.
  1041 
  1042   \item All type variables on the right-hand side must also appear on
  1043   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.
  1044 
  1045   \item The definition must not be recursive.  Most object-logics
  1046   provide definitional principles that can be used to express
  1047   recursion safely.
  1048 
  1049   \end{itemize}
  1050 
  1051   Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}.  The right-hand side may mention overloaded constants
  1052   recursively at type instances corresponding to the immediate
  1053   argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}.  Incomplete
  1054   specification patterns impose global constraints on all occurrences,
  1055   e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
  1056   corresponding occurrences on some right-hand side need to be an
  1057   instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
  1058 
  1059   \begin{matharray}{rcl}
  1060     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1061     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1062     \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1063   \end{matharray}
  1064 
  1065   \begin{rail}
  1066     'consts' ((name '::' type mixfix?) +)
  1067     ;
  1068     'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
  1069     ;
  1070   \end{rail}
  1071 
  1072   \begin{rail}
  1073     'constdefs' structs? (constdecl? constdef +)
  1074     ;
  1075 
  1076     structs: '(' 'structure' (vars + 'and') ')'
  1077     ;
  1078     constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
  1079     ;
  1080     constdef: thmdecl? prop
  1081     ;
  1082   \end{rail}
  1083 
  1084   \begin{description}
  1085 
  1086   \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
  1087   mixfix annotations may attach concrete syntax to the constants
  1088   declared.
  1089   
  1090   \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}
  1091   as a definitional axiom for some existing constant.
  1092   
  1093   The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
  1094   for this definition, which is occasionally useful for exotic
  1095   overloading.  It is at the discretion of the user to avoid malformed
  1096   theory specifications!
  1097   
  1098   The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
  1099   potentially overloaded.  Unless this option is given, a warning
  1100   message would be issued for any definitional equation with a more
  1101   special type than that of the corresponding constant declaration.
  1102   
  1103   \item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and
  1104   definitions, with type-inference taking care of the most general
  1105   typing of the given specification (the optional type constraint may
  1106   refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual).  The
  1107   resulting type declaration needs to agree with that of the
  1108   specification; overloading is \emph{not} supported here!
  1109   
  1110   The constant name may be omitted altogether, if neither type nor
  1111   syntax declarations are given.  The canonical name of the
  1112   definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
  1113   unless specified otherwise.  Also note that the given list of
  1114   specifications is processed in a strictly sequential manner, with
  1115   type-checking being performed independently.
  1116   
  1117   An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
  1118   admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'').  The latter concept is
  1119   particularly useful with locales (see also \secref{sec:locale}).
  1120 
  1121   \end{description}%
  1122 \end{isamarkuptext}%
  1123 \isamarkuptrue%
  1124 %
  1125 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
  1126 }
  1127 \isamarkuptrue%
  1128 %
  1129 \begin{isamarkuptext}%
  1130 \begin{matharray}{rcll}
  1131     \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
  1132     \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
  1133     \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
  1134   \end{matharray}
  1135 
  1136   \begin{rail}
  1137     'axioms' (axmdecl prop +)
  1138     ;
  1139     ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
  1140     ;
  1141   \end{rail}
  1142 
  1143   \begin{description}
  1144   
  1145   \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary
  1146   statements as axioms of the meta-logic.  In fact, axioms are
  1147   ``axiomatic theorems'', and may be referred later just as any other
  1148   theorem.
  1149   
  1150   Axioms are usually only introduced when declaring new logical
  1151   systems.  Everyday work is typically done the hard way, with proper
  1152   definitions and proven theorems.
  1153   
  1154   \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores
  1155   existing facts in the theory context, or the specified target
  1156   context (see also \secref{sec:target}).  Typical applications would
  1157   also involve attributes, to declare Simplifier rules, for example.
  1158   
  1159   \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.
  1160 
  1161   \end{description}%
  1162 \end{isamarkuptext}%
  1163 \isamarkuptrue%
  1164 %
  1165 \isamarkupsection{Oracles%
  1166 }
  1167 \isamarkuptrue%
  1168 %
  1169 \begin{isamarkuptext}%
  1170 Oracles allow Isabelle to take advantage of external reasoners
  1171   such as arithmetic decision procedures, model checkers, fast
  1172   tautology checkers or computer algebra systems.  Invoked as an
  1173   oracle, an external reasoner can create arbitrary Isabelle theorems.
  1174 
  1175   It is the responsibility of the user to ensure that the external
  1176   reasoner is as trustworthy as the application requires.  Another
  1177   typical source of errors is the linkup between Isabelle and the
  1178   external tool, not just its concrete implementation, but also the
  1179   required translation between two different logical environments.
  1180 
  1181   Isabelle merely guarantees well-formedness of the propositions being
  1182   asserted, and records within the internal derivation object how
  1183   presumed theorems depend on unproven suppositions.
  1184 
  1185   \begin{matharray}{rcl}
  1186     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1187   \end{matharray}
  1188 
  1189   \begin{rail}
  1190     'oracle' name '=' text
  1191     ;
  1192   \end{rail}
  1193 
  1194   \begin{description}
  1195 
  1196   \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML
  1197   expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
  1198   ML function of type \verb|'a -> thm|, which is bound to the
  1199   global identifier \verb|name|.  This acts like an infinitary
  1200   specification of axioms!  Invoking the oracle only works within the
  1201   scope of the resulting theory.
  1202 
  1203   \end{description}
  1204 
  1205   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
  1206   defining a new primitive rule as oracle, and turning it into a proof
  1207   method.%
  1208 \end{isamarkuptext}%
  1209 \isamarkuptrue%
  1210 %
  1211 \isamarkupsection{Name spaces%
  1212 }
  1213 \isamarkuptrue%
  1214 %
  1215 \begin{isamarkuptext}%
  1216 \begin{matharray}{rcl}
  1217     \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1218     \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1219     \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1220   \end{matharray}
  1221 
  1222   \begin{rail}
  1223     'hide' ('(open)')? name (nameref + )
  1224     ;
  1225   \end{rail}
  1226 
  1227   Isabelle organizes any kind of name declarations (of types,
  1228   constants, theorems etc.) by separate hierarchically structured name
  1229   spaces.  Normally the user does not have to control the behavior of
  1230   name spaces by hand, yet the following commands provide some way to
  1231   do so.
  1232 
  1233   \begin{description}
  1234 
  1235   \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
  1236   name declaration mode.  Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
  1237   the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
  1238   names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
  1239   
  1240   Note that global names are prone to get hidden accidently later,
  1241   when qualified names of the same base name are introduced.
  1242   
  1243   \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
  1244   declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
  1245   \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden.  Global
  1246   (unqualified) names may never be hidden.
  1247   
  1248   Note that hiding name space accesses has no impact on logical
  1249   declarations --- they remain valid internally.  Entities that are no
  1250   longer accessible to the user are printed with the special qualifier
  1251   ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
  1252 
  1253   \end{description}%
  1254 \end{isamarkuptext}%
  1255 \isamarkuptrue%
  1256 %
  1257 \isadelimtheory
  1258 %
  1259 \endisadelimtheory
  1260 %
  1261 \isatagtheory
  1262 \isacommand{end}\isamarkupfalse%
  1263 %
  1264 \endisatagtheory
  1265 {\isafoldtheory}%
  1266 %
  1267 \isadelimtheory
  1268 %
  1269 \endisadelimtheory
  1270 \isanewline
  1271 \end{isabellebody}%
  1272 %%% Local Variables:
  1273 %%% mode: latex
  1274 %%% TeX-master: "root"
  1275 %%% End: