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