doc-src/IsarRef/Thy/document/Spec.tex
author blanchet
Wed Mar 04 11:05:29 2009 +0100 (2009-03-04 ago)
changeset 30242 aea5d7fa7ef5
parent 30240 5b25fee0362c
parent 30121 5c7bcb296600
child 30463 f1cb00030d4f
permissions -rw-r--r--
Merge.
     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   \end{matharray}
   811 
   812   \begin{mldecls}
   813     \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
   814     \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
   815   \end{mldecls}
   816 
   817   \begin{rail}
   818     'use' name
   819     ;
   820     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
   821     ;
   822   \end{rail}
   823 
   824   \begin{description}
   825 
   826   \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML
   827   commands from \isa{{\isachardoublequote}file{\isachardoublequote}}.  The current theory context is passed
   828   down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands.  The file name is checked with
   829   the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
   830   header (see also \secref{sec:begin-thy}).
   831 
   832   Top-level ML bindings are stored within the (global or local) theory
   833   context.
   834   
   835   \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
   836   but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
   837   Top-level ML bindings are stored within the (global or local) theory
   838   context.
   839 
   840   \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
   841   within a proof context.
   842 
   843   Top-level ML bindings are stored within the proof context in a
   844   purely sequential fashion, disregarding the nested proof structure.
   845   ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the
   846   end of the proof.
   847 
   848   \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic
   849   versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
   850   updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML
   851   toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
   852   
   853   \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
   854   context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
   855   of type \verb|theory -> theory|.  This enables
   856   to initialize any object-logic specific tools and packages written
   857   in ML, for example.
   858 
   859   \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
   860   theorems produced in ML both in the theory context and the ML
   861   toplevel, associating it with the provided name.  Theorems are put
   862   into a global ``standard'' format before being stored.
   863 
   864   \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
   865   singleton theorem.
   866   
   867   \end{description}%
   868 \end{isamarkuptext}%
   869 \isamarkuptrue%
   870 %
   871 \isamarkupsection{Primitive specification elements%
   872 }
   873 \isamarkuptrue%
   874 %
   875 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
   876 }
   877 \isamarkuptrue%
   878 %
   879 \begin{isamarkuptext}%
   880 \begin{matharray}{rcll}
   881     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   882     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   883     \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   884     \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}} \\
   885   \end{matharray}
   886 
   887   \begin{rail}
   888     'classes' (classdecl +)
   889     ;
   890     'classrel' (nameref ('<' | subseteq) nameref + 'and')
   891     ;
   892     'defaultsort' sort
   893     ;
   894   \end{rail}
   895 
   896   \begin{description}
   897 
   898   \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
   899   \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.
   900   Isabelle implicitly maintains the transitive closure of the class
   901   hierarchy.  Cyclic class structures are not permitted.
   902 
   903   \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
   904   relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
   905   This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
   906   (see \secref{sec:axclass}) provides a way to introduce proven class
   907   relations.
   908 
   909   \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
   910   new default sort for any type variable that is given explicitly in
   911   the text, but lacks a sort constraint (wrt.\ the current context).
   912   Type variables generated by type inference are not affected.
   913 
   914   Usually the default sort is only changed when defining a new
   915   object-logic.  For example, the default sort in Isabelle/HOL is
   916   \isa{type}, the class of all HOL types.  %FIXME sort antiq?
   917 
   918   When merging theories, the default sorts of the parents are
   919   logically intersected, i.e.\ the representations as lists of classes
   920   are joined.
   921 
   922   \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation,
   923   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
   924 
   925   \end{description}%
   926 \end{isamarkuptext}%
   927 \isamarkuptrue%
   928 %
   929 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
   930 }
   931 \isamarkuptrue%
   932 %
   933 \begin{isamarkuptext}%
   934 \begin{matharray}{rcll}
   935     \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   936     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   937     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   938   \end{matharray}
   939 
   940   \begin{rail}
   941     'types' (typespec '=' type infix? +)
   942     ;
   943     'typedecl' typespec infix?
   944     ;
   945     'arities' (nameref '::' arity +)
   946     ;
   947   \end{rail}
   948 
   949   \begin{description}
   950 
   951   \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
   952   \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type
   953   \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.  Unlike actual type definitions, as are available in
   954   Isabelle/HOL for example, type synonyms are merely syntactic
   955   abbreviations without any logical significance.  Internally, type
   956   synonyms are fully expanded.
   957   
   958   \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
   959   type constructor \isa{t}.  If the object-logic defines a base sort
   960   \isa{s}, then the constructor is declared to operate on that, via
   961   the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.
   962 
   963   \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
   964   Isabelle's order-sorted signature of types by new type constructor
   965   arities.  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
   966   command (see \secref{sec:axclass}) provides a way to introduce
   967   proven type arities.
   968 
   969   \end{description}%
   970 \end{isamarkuptext}%
   971 \isamarkuptrue%
   972 %
   973 \isamarkupsubsection{Co-regularity of type classes and arities%
   974 }
   975 \isamarkuptrue%
   976 %
   977 \begin{isamarkuptext}%
   978 The class relation together with the collection of
   979   type-constructor arities must obey the principle of
   980   \emph{co-regularity} as defined below.
   981 
   982   \medskip For the subsequent formulation of co-regularity we assume
   983   that the class relation is closed by transitivity and reflexivity.
   984   Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is
   985   completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}
   986   implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.
   987 
   988   Treating sorts as finite sets of classes (meaning the intersection),
   989   the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as
   990   follows:
   991   \[
   992     \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}}
   993   \]
   994 
   995   This relation on sorts is further extended to tuples of sorts (of
   996   the same length) in the component-wise way.
   997 
   998   \smallskip Co-regularity of the class relation together with the
   999   arities relation means:
  1000   \[
  1001     \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}}
  1002   \]
  1003   \noindent for all such arities.  In other words, whenever the result
  1004   classes of some type-constructor arities are related, then the
  1005   argument sorts need to be related in the same way.
  1006 
  1007   \medskip Co-regularity is a very fundamental property of the
  1008   order-sorted algebra of types.  For example, it entails principle
  1009   types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
  1010 \end{isamarkuptext}%
  1011 \isamarkuptrue%
  1012 %
  1013 \isamarkupsubsection{Constants and definitions \label{sec:consts}%
  1014 }
  1015 \isamarkuptrue%
  1016 %
  1017 \begin{isamarkuptext}%
  1018 Definitions essentially express abbreviations within the logic.  The
  1019   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
  1020   where the arguments of \isa{c} appear on the left, abbreviating a
  1021   prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
  1022   written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.  Moreover,
  1023   definitions may be weakened by adding arbitrary pre-conditions:
  1024   \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
  1025 
  1026   \medskip The built-in well-formedness conditions for definitional
  1027   specifications are:
  1028 
  1029   \begin{itemize}
  1030 
  1031   \item Arguments (on the left-hand side) must be distinct variables.
  1032 
  1033   \item All variables on the right-hand side must also appear on the
  1034   left-hand side.
  1035 
  1036   \item All type variables on the right-hand side must also appear on
  1037   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.
  1038 
  1039   \item The definition must not be recursive.  Most object-logics
  1040   provide definitional principles that can be used to express
  1041   recursion safely.
  1042 
  1043   \end{itemize}
  1044 
  1045   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
  1046   recursively at type instances corresponding to the immediate
  1047   argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}.  Incomplete
  1048   specification patterns impose global constraints on all occurrences,
  1049   e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
  1050   corresponding occurrences on some right-hand side need to be an
  1051   instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
  1052 
  1053   \begin{matharray}{rcl}
  1054     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1055     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1056     \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1057   \end{matharray}
  1058 
  1059   \begin{rail}
  1060     'consts' ((name '::' type mixfix?) +)
  1061     ;
  1062     'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
  1063     ;
  1064   \end{rail}
  1065 
  1066   \begin{rail}
  1067     'constdefs' structs? (constdecl? constdef +)
  1068     ;
  1069 
  1070     structs: '(' 'structure' (vars + 'and') ')'
  1071     ;
  1072     constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
  1073     ;
  1074     constdef: thmdecl? prop
  1075     ;
  1076   \end{rail}
  1077 
  1078   \begin{description}
  1079 
  1080   \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
  1081   mixfix annotations may attach concrete syntax to the constants
  1082   declared.
  1083   
  1084   \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}
  1085   as a definitional axiom for some existing constant.
  1086   
  1087   The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
  1088   for this definition, which is occasionally useful for exotic
  1089   overloading.  It is at the discretion of the user to avoid malformed
  1090   theory specifications!
  1091   
  1092   The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
  1093   potentially overloaded.  Unless this option is given, a warning
  1094   message would be issued for any definitional equation with a more
  1095   special type than that of the corresponding constant declaration.
  1096   
  1097   \item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and
  1098   definitions, with type-inference taking care of the most general
  1099   typing of the given specification (the optional type constraint may
  1100   refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual).  The
  1101   resulting type declaration needs to agree with that of the
  1102   specification; overloading is \emph{not} supported here!
  1103   
  1104   The constant name may be omitted altogether, if neither type nor
  1105   syntax declarations are given.  The canonical name of the
  1106   definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
  1107   unless specified otherwise.  Also note that the given list of
  1108   specifications is processed in a strictly sequential manner, with
  1109   type-checking being performed independently.
  1110   
  1111   An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
  1112   admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'').  The latter concept is
  1113   particularly useful with locales (see also \secref{sec:locale}).
  1114 
  1115   \end{description}%
  1116 \end{isamarkuptext}%
  1117 \isamarkuptrue%
  1118 %
  1119 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
  1120 }
  1121 \isamarkuptrue%
  1122 %
  1123 \begin{isamarkuptext}%
  1124 \begin{matharray}{rcll}
  1125     \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
  1126     \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
  1127     \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
  1128   \end{matharray}
  1129 
  1130   \begin{rail}
  1131     'axioms' (axmdecl prop +)
  1132     ;
  1133     ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
  1134     ;
  1135   \end{rail}
  1136 
  1137   \begin{description}
  1138   
  1139   \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary
  1140   statements as axioms of the meta-logic.  In fact, axioms are
  1141   ``axiomatic theorems'', and may be referred later just as any other
  1142   theorem.
  1143   
  1144   Axioms are usually only introduced when declaring new logical
  1145   systems.  Everyday work is typically done the hard way, with proper
  1146   definitions and proven theorems.
  1147   
  1148   \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores
  1149   existing facts in the theory context, or the specified target
  1150   context (see also \secref{sec:target}).  Typical applications would
  1151   also involve attributes, to declare Simplifier rules, for example.
  1152   
  1153   \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.
  1154 
  1155   \end{description}%
  1156 \end{isamarkuptext}%
  1157 \isamarkuptrue%
  1158 %
  1159 \isamarkupsection{Oracles%
  1160 }
  1161 \isamarkuptrue%
  1162 %
  1163 \begin{isamarkuptext}%
  1164 Oracles allow Isabelle to take advantage of external reasoners
  1165   such as arithmetic decision procedures, model checkers, fast
  1166   tautology checkers or computer algebra systems.  Invoked as an
  1167   oracle, an external reasoner can create arbitrary Isabelle theorems.
  1168 
  1169   It is the responsibility of the user to ensure that the external
  1170   reasoner is as trustworthy as the application requires.  Another
  1171   typical source of errors is the linkup between Isabelle and the
  1172   external tool, not just its concrete implementation, but also the
  1173   required translation between two different logical environments.
  1174 
  1175   Isabelle merely guarantees well-formedness of the propositions being
  1176   asserted, and records within the internal derivation object how
  1177   presumed theorems depend on unproven suppositions.
  1178 
  1179   \begin{matharray}{rcl}
  1180     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1181   \end{matharray}
  1182 
  1183   \begin{rail}
  1184     'oracle' name '=' text
  1185     ;
  1186   \end{rail}
  1187 
  1188   \begin{description}
  1189 
  1190   \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML
  1191   expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
  1192   ML function of type \verb|'a -> thm|, which is bound to the
  1193   global identifier \verb|name|.  This acts like an infinitary
  1194   specification of axioms!  Invoking the oracle only works within the
  1195   scope of the resulting theory.
  1196 
  1197   \end{description}
  1198 
  1199   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
  1200   defining a new primitive rule as oracle, and turning it into a proof
  1201   method.%
  1202 \end{isamarkuptext}%
  1203 \isamarkuptrue%
  1204 %
  1205 \isamarkupsection{Name spaces%
  1206 }
  1207 \isamarkuptrue%
  1208 %
  1209 \begin{isamarkuptext}%
  1210 \begin{matharray}{rcl}
  1211     \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1212     \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1213     \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
  1214   \end{matharray}
  1215 
  1216   \begin{rail}
  1217     'hide' ('(open)')? name (nameref + )
  1218     ;
  1219   \end{rail}
  1220 
  1221   Isabelle organizes any kind of name declarations (of types,
  1222   constants, theorems etc.) by separate hierarchically structured name
  1223   spaces.  Normally the user does not have to control the behavior of
  1224   name spaces by hand, yet the following commands provide some way to
  1225   do so.
  1226 
  1227   \begin{description}
  1228 
  1229   \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
  1230   name declaration mode.  Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
  1231   the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
  1232   names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
  1233   
  1234   Note that global names are prone to get hidden accidently later,
  1235   when qualified names of the same base name are introduced.
  1236   
  1237   \item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes
  1238   declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
  1239   \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
  1240   (unqualified) names may never be hidden.
  1241   
  1242   Note that hiding name space accesses has no impact on logical
  1243   declarations --- they remain valid internally.  Entities that are no
  1244   longer accessible to the user are printed with the special qualifier
  1245   ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
  1246 
  1247   \end{description}%
  1248 \end{isamarkuptext}%
  1249 \isamarkuptrue%
  1250 %
  1251 \isadelimtheory
  1252 %
  1253 \endisadelimtheory
  1254 %
  1255 \isatagtheory
  1256 \isacommand{end}\isamarkupfalse%
  1257 %
  1258 \endisatagtheory
  1259 {\isafoldtheory}%
  1260 %
  1261 \isadelimtheory
  1262 %
  1263 \endisadelimtheory
  1264 \isanewline
  1265 \end{isabellebody}%
  1266 %%% Local Variables:
  1267 %%% mode: latex
  1268 %%% TeX-master: "root"
  1269 %%% End: