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