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