doc-src/IsarRef/Thy/document/Spec.tex
changeset 27042 8fcf19f2168b
parent 26902 8db1e960d636
child 27047 2dcdea037385
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 02 22:50:27 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Jun 02 22:50:29 2008 +0200
     1.3 @@ -32,21 +32,23 @@
     1.4  \begin{matharray}{rcl}
     1.5      \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\
     1.6      \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\
     1.7 -    \indexdef{}{command}{end}\hypertarget{command.end}{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\
     1.8 +    \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\
     1.9    \end{matharray}
    1.10  
    1.11 -  Isabelle/Isar theories are defined via theory, which contain both
    1.12 -  specifications and proofs; occasionally definitional mechanisms also
    1.13 -  require some explicit proof.
    1.14 +  Isabelle/Isar theories are defined via theory file, which contain
    1.15 +  both specifications and proofs; occasionally definitional mechanisms
    1.16 +  also require some explicit proof.  The theory body may be
    1.17 +  sub-structered by means of \emph{local theory} target mechanisms,
    1.18 +  notably \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}.
    1.19  
    1.20    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
    1.21    ones.  Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be
    1.22    an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is relevant to
    1.23    document preparation only; it acts very much like a special
    1.24 -  pre-theory markup command (cf.\ \secref{sec:markup-thy} and
    1.25 -  \secref{sec:markup-thy}).  The \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} command concludes a
    1.26 -  theory development; it has to be the very last command of any theory
    1.27 -  file loaded in batch-mode.
    1.28 +  pre-theory markup command (cf.\ \secref{sec:markup} and).  The
    1.29 +  \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command
    1.30 +  concludes a theory development; it has to be the very last command
    1.31 +  of any theory file loaded in batch-mode.
    1.32  
    1.33    \begin{rail}
    1.34      'header' text
    1.35 @@ -62,8 +64,7 @@
    1.36    \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
    1.37    markup just preceding the formal beginning of a theory.  In actual
    1.38    document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
    1.39 -  headings.  See also \secref{sec:markup-thy} and
    1.40 -  \secref{sec:markup-prf} for further markup commands.
    1.41 +  headings.  See also \secref{sec:markup} for further markup commands.
    1.42    
    1.43    \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
    1.44    merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
    1.45 @@ -82,13 +83,1255 @@
    1.46    text (typically via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} in the body text,
    1.47    see \secref{sec:ML}).
    1.48    
    1.49 -  \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory definition or
    1.50 -  context switch.
    1.51 +  \item [\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory
    1.52 +  definition.
    1.53 +
    1.54 +  \end{descr}%
    1.55 +\end{isamarkuptext}%
    1.56 +\isamarkuptrue%
    1.57 +%
    1.58 +\isamarkupsection{Local theory targets \label{sec:target}%
    1.59 +}
    1.60 +\isamarkuptrue%
    1.61 +%
    1.62 +\begin{isamarkuptext}%
    1.63 +A local theory target is a context managed separately within the
    1.64 +  enclosing theory.  Contexts may introduce parameters (fixed
    1.65 +  variables) and assumptions (hypotheses).  Definitions and theorems
    1.66 +  depending on the context may be added incrementally later on.  Named
    1.67 +  contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
    1.68 +  (cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
    1.69 +  global theory context.
    1.70 +
    1.71 +  \begin{matharray}{rcll}
    1.72 +    \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
    1.73 +    \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\
    1.74 +  \end{matharray}
    1.75 +
    1.76 +  \indexouternonterm{target}
    1.77 +  \begin{rail}
    1.78 +    'context' name 'begin'
    1.79 +    ;
    1.80 +
    1.81 +    target: '(' 'in' name ')'
    1.82 +    ;
    1.83 +  \end{rail}
    1.84 +
    1.85 +  \begin{descr}
    1.86 +  
    1.87 +  \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
    1.88 +  existing locale or class context \isa{c}.  Note that locale and
    1.89 +  class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}
    1.90 +  keyword as well, in order to continue the local theory immediately
    1.91 +  after the initial specification.
    1.92 +  
    1.93 +  \item [\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory
    1.94 +  and continues the enclosing global theory.  Note that a global
    1.95 +  \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
    1.96 +  theory itself (\secref{sec:begin-thy}).
    1.97 +  
    1.98 +  \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command
    1.99 +  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
   1.100 +  global theory context; the current target context will be suspended
   1.101 +  for this command only.  Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
   1.102 +  always produce a global result independently of the current target
   1.103 +  context.
   1.104 +
   1.105 +  \end{descr}
   1.106 +
   1.107 +  The exact meaning of results produced within a local theory context
   1.108 +  depends on the underlying target infrastructure (locale, type class
   1.109 +  etc.).  The general idea is as follows, considering a context named
   1.110 +  \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
   1.111 +  
   1.112 +  Definitions are exported by introducing a global version with
   1.113 +  additional arguments; a syntactic abbreviation links the long form
   1.114 +  with the abstract version of the target context.  For example,
   1.115 +  \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
   1.116 +  level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
   1.117 +  abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
   1.118 +  fixed parameter \isa{x}).
   1.119 +
   1.120 +  Theorems are exported by discharging the assumptions and
   1.121 +  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
   1.122 +  \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
   1.123 +\end{isamarkuptext}%
   1.124 +\isamarkuptrue%
   1.125 +%
   1.126 +\isamarkupsection{Basic specification elements%
   1.127 +}
   1.128 +\isamarkuptrue%
   1.129 +%
   1.130 +\begin{isamarkuptext}%
   1.131 +\begin{matharray}{rcll}
   1.132 +    \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
   1.133 +    \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.134 +    \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
   1.135 +    \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.136 +    \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} \\
   1.137 +    \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.138 +    \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.139 +  \end{matharray}
   1.140 +
   1.141 +  These specification mechanisms provide a slightly more abstract view
   1.142 +  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
   1.143 +  \secref{sec:axms-thms}).  In particular, type-inference is commonly
   1.144 +  available, and result names need not be given.
   1.145 +
   1.146 +  \begin{rail}
   1.147 +    'axiomatization' target? fixes? ('where' specs)?
   1.148 +    ;
   1.149 +    'definition' target? (decl 'where')? thmdecl? prop
   1.150 +    ;
   1.151 +    'abbreviation' target? mode? (decl 'where')? prop
   1.152 +    ;
   1.153 +    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
   1.154 +    ;
   1.155 +
   1.156 +    fixes: ((name ('::' type)? mixfix? | vars) + 'and')
   1.157 +    ;
   1.158 +    specs: (thmdecl? props + 'and')
   1.159 +    ;
   1.160 +    decl: name ('::' type)? mixfix?
   1.161 +    ;
   1.162 +  \end{rail}
   1.163 +
   1.164 +  \begin{descr}
   1.165 +  
   1.166 +  \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
   1.167 +  simultaneously and states axiomatic properties for these.  The
   1.168 +  constants are marked as being specified once and for all, which
   1.169 +  prevents additional specifications being issued later on.
   1.170 +  
   1.171 +  Note that axiomatic specifications are only appropriate when
   1.172 +  declaring a new logical system.  Normal applications should only use
   1.173 +  definitional mechanisms!
   1.174 +
   1.175 +  \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
   1.176 +  internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
   1.177 +  given as \isa{eq}, which is then turned into a proven fact.  The
   1.178 +  given proposition may deviate from internal meta-level equality
   1.179 +  according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
   1.180 +  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
   1.181 +  change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
   1.182 +  
   1.183 +  Definitions may be presented with explicit arguments on the LHS, as
   1.184 +  well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
   1.185 +  \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
   1.186 +  unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
   1.187 +  
   1.188 +  \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces
   1.189 +  a syntactic constant which is associated with a certain term
   1.190 +  according to the meta-level equality \isa{eq}.
   1.191 +  
   1.192 +  Abbreviations participate in the usual type-inference process, but
   1.193 +  are expanded before the logic ever sees them.  Pretty printing of
   1.194 +  terms involves higher-order rewriting with rules stemming from
   1.195 +  reverted abbreviations.  This needs some care to avoid overlapping
   1.196 +  or looping syntactic replacements!
   1.197 +  
   1.198 +  The optional \isa{mode} specification restricts output to a
   1.199 +  particular print mode; using ``\isa{input}'' here achieves the
   1.200 +  effect of one-way abbreviations.  The mode may also include an
   1.201 +  ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
   1.202 +  declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
   1.203 +  \secref{sec:syn-trans}.
   1.204 +  
   1.205 +  \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
   1.206 +  of the current context.
   1.207 +  
   1.208 +  \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
   1.209 +  syntax with an existing constant or fixed variable.  This is a
   1.210 +  robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
   1.211 +  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
   1.212 +  representation of the given entity is retrieved from the context.
   1.213 +  
   1.214 +  \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
   1.215 +  present context.
   1.216 +
   1.217 +  \end{descr}
   1.218 +
   1.219 +  All of these specifications support local theory targets (cf.\
   1.220 +  \secref{sec:target}).%
   1.221 +\end{isamarkuptext}%
   1.222 +\isamarkuptrue%
   1.223 +%
   1.224 +\isamarkupsection{Generic declarations%
   1.225 +}
   1.226 +\isamarkuptrue%
   1.227 +%
   1.228 +\begin{isamarkuptext}%
   1.229 +Arbitrary operations on the background context may be wrapped-up as
   1.230 +  generic declaration elements.  Since the underlying concept of local
   1.231 +  theories may be subject to later re-interpretation, there is an
   1.232 +  additional dependency on a morphism that tells the difference of the
   1.233 +  original declaration context wrt.\ the application context
   1.234 +  encountered later on.  A fact declaration is an important special
   1.235 +  case: it consists of a theorem which is applied to the context by
   1.236 +  means of an attribute.
   1.237 +
   1.238 +  \begin{matharray}{rcl}
   1.239 +    \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.240 +    \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\
   1.241 +  \end{matharray}
   1.242 +
   1.243 +  \begin{rail}
   1.244 +    'declaration' target? text
   1.245 +    ;
   1.246 +    'declare' target? (thmrefs + 'and')
   1.247 +    ;
   1.248 +  \end{rail}
   1.249 +
   1.250 +  \begin{descr}
   1.251 +
   1.252 +  \item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration
   1.253 +  function \isa{d} of ML type \verb|declaration|, to the current
   1.254 +  local theory under construction.  In later application contexts, the
   1.255 +  function is transformed according to the morphisms being involved in
   1.256 +  the interpretation hierarchy.
   1.257 +
   1.258 +  \item [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the
   1.259 +  current local theory context.  No theorem binding is involved here,
   1.260 +  unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
   1.261 +  \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
   1.262 +  of applying attributes as included in the theorem specification.
   1.263 +
   1.264 +  \end{descr}%
   1.265 +\end{isamarkuptext}%
   1.266 +\isamarkuptrue%
   1.267 +%
   1.268 +\isamarkupsection{Locales \label{sec:locale}%
   1.269 +}
   1.270 +\isamarkuptrue%
   1.271 +%
   1.272 +\begin{isamarkuptext}%
   1.273 +Locales are named local contexts, consisting of a list of
   1.274 +  declaration elements that are modeled after the Isar proof context
   1.275 +  commands (cf.\ \secref{sec:proof-context}).%
   1.276 +\end{isamarkuptext}%
   1.277 +\isamarkuptrue%
   1.278 +%
   1.279 +\isamarkupsubsection{Locale specifications%
   1.280 +}
   1.281 +\isamarkuptrue%
   1.282 +%
   1.283 +\begin{isamarkuptext}%
   1.284 +\begin{matharray}{rcl}
   1.285 +    \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
   1.286 +    \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} \\
   1.287 +    \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} \\
   1.288 +    \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
   1.289 +    \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
   1.290 +  \end{matharray}
   1.291 +
   1.292 +  \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
   1.293 +  \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   1.294 +  \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
   1.295 +  \begin{rail}
   1.296 +    'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
   1.297 +    ;
   1.298 +    'print\_locale' '!'? localeexpr
   1.299 +    ;
   1.300 +    localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
   1.301 +    ;
   1.302 +
   1.303 +    contextexpr: nameref | '(' contextexpr ')' |
   1.304 +    (contextexpr (name mixfix? +)) | (contextexpr + '+')
   1.305 +    ;
   1.306 +    contextelem: fixes | constrains | assumes | defines | notes
   1.307 +    ;
   1.308 +    fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
   1.309 +    ;
   1.310 +    constrains: 'constrains' (name '::' type + 'and')
   1.311 +    ;
   1.312 +    assumes: 'assumes' (thmdecl? props + 'and')
   1.313 +    ;
   1.314 +    defines: 'defines' (thmdecl? prop proppat? + 'and')
   1.315 +    ;
   1.316 +    notes: 'notes' (thmdef? thmrefs + 'and')
   1.317 +    ;
   1.318 +    includes: 'includes' contextexpr
   1.319 +    ;
   1.320 +  \end{rail}
   1.321 +
   1.322 +  \begin{descr}
   1.323 +  
   1.324 +  \item [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] defines a
   1.325 +  new locale \isa{loc} as a context consisting of a certain view of
   1.326 +  existing locales (\isa{import}) plus some additional elements
   1.327 +  (\isa{body}).  Both \isa{import} and \isa{body} are optional;
   1.328 +  the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
   1.329 +  locale, which may still be useful to collect declarations of facts
   1.330 +  later on.  Type-inference on locale expressions automatically takes
   1.331 +  care of the most general typing that the combined context elements
   1.332 +  may acquire.
   1.333 +
   1.334 +  The \isa{import} consists of a structured context expression,
   1.335 +  consisting of references to existing locales, renamed contexts, or
   1.336 +  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
   1.337 +  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
   1.338 +  position.  Renaming by default deletes concrete syntax, but new
   1.339 +  syntax may by specified with a mixfix annotation.  An exeption of
   1.340 +  this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
   1.341 +  be changed.  Merging proceeds from left-to-right, suppressing any
   1.342 +  duplicates stemming from different paths through the import
   1.343 +  hierarchy.
   1.344 +
   1.345 +  The \isa{body} consists of basic context elements, further context
   1.346 +  expressions may be included as well.
   1.347 +
   1.348 +  \begin{descr}
   1.349 +
   1.350 +  \item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local
   1.351 +  parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
   1.352 +  are optional).  The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
   1.353 +  implicitly in this context.
   1.354 +
   1.355 +  \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type
   1.356 +  constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
   1.357 +
   1.358 +  \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}]
   1.359 +  introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
   1.360 +  proof (cf.\ \secref{sec:proof-context}).
   1.361 +
   1.362 +  \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously
   1.363 +  declared parameter.  This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
   1.364 +  proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
   1.365 +  takes an equational proposition instead of variable-term pair.  The
   1.366 +  left-hand side of the equation may have additional arguments, e.g.\
   1.367 +  ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
   1.368 +
   1.369 +  \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
   1.370 +  reconsiders facts within a local context.  Most notably, this may
   1.371 +  include arbitrary declarations in any attribute specifications
   1.372 +  included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
   1.373 +
   1.374 +  \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
   1.375 +  in a statically scoped manner.  Only available in the long goal
   1.376 +  format of \secref{sec:goals}.
   1.377 +
   1.378 +  In contrast, the initial \isa{import} specification of a locale
   1.379 +  expression maintains a dynamic relation to the locales being
   1.380 +  referenced (benefiting from any later fact declarations in the
   1.381 +  obvious manner).
   1.382 +
   1.383 +  \end{descr}
   1.384 +  
   1.385 +  Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
   1.386 +  in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
   1.387 +  are illegal in locale definitions.  In the long goal format of
   1.388 +  \secref{sec:goals}, term bindings may be included as expected,
   1.389 +  though.
   1.390 +  
   1.391 +  \medskip By default, locale specifications are ``closed up'' by
   1.392 +  turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
   1.393 +  (modulo local definitions).  The predicate statement covers only the
   1.394 +  newly specified assumptions, omitting the content of included locale
   1.395 +  expressions.  The full cumulative view is only provided on export,
   1.396 +  involving another predicate \isa{loc} that refers to the complete
   1.397 +  specification text.
   1.398 +  
   1.399 +  In any case, the predicate arguments are those locale parameters
   1.400 +  that actually occur in the respective piece of text.  Also note that
   1.401 +  these predicates operate at the meta-level in theory, but the locale
   1.402 +  packages attempts to internalize statements according to the
   1.403 +  object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
   1.404 +  \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
   1.405 +  \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
   1.406 +  
   1.407 +  The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
   1.408 +  the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
   1.409 +  constructions.  Predicates are also omitted for empty specification
   1.410 +  texts.
   1.411 +
   1.412 +  \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
   1.413 +  specified locale expression in a flattened form.  The notable
   1.414 +  special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
   1.415 +  contents of the named locale, but keep in mind that type-inference
   1.416 +  will normalize type variables according to the usual alphabetical
   1.417 +  order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
   1.418 +  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
   1.419 +
   1.420 +  \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
   1.421 +  of the current theory.
   1.422 +
   1.423 +  \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
   1.424 +  repeatedly expand all introduction rules of locale predicates of the
   1.425 +  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
   1.426 +  assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
   1.427 +  \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale
   1.428 +  specifications entailed by the context, both from target and
   1.429 +  \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
   1.430 +  below).  New goals that are entailed by the current context are
   1.431 +  discharged automatically.
   1.432 +
   1.433 +  \end{descr}%
   1.434 +\end{isamarkuptext}%
   1.435 +\isamarkuptrue%
   1.436 +%
   1.437 +\isamarkupsubsection{Interpretation of locales%
   1.438 +}
   1.439 +\isamarkuptrue%
   1.440 +%
   1.441 +\begin{isamarkuptext}%
   1.442 +Locale expressions (more precisely, \emph{context expressions}) may
   1.443 +  be instantiated, and the instantiated facts added to the current
   1.444 +  context.  This requires a proof of the instantiated specification
   1.445 +  and is called \emph{locale interpretation}.  Interpretation is
   1.446 +  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}}}}).
   1.447 +
   1.448 +  \begin{matharray}{rcl}
   1.449 +    \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\
   1.450 +    \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   1.451 +    \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} \\
   1.452 +  \end{matharray}
   1.453 +
   1.454 +  \indexouternonterm{interp}
   1.455 +  \begin{rail}
   1.456 +    'interpretation' (interp | name ('<' | subseteq) contextexpr)
   1.457 +    ;
   1.458 +    'interpret' interp
   1.459 +    ;
   1.460 +    'print\_interps' '!'? name
   1.461 +    ;
   1.462 +    instantiation: ('[' (inst+) ']')?
   1.463 +    ;
   1.464 +    interp: thmdecl? \\ (contextexpr instantiation |
   1.465 +      name instantiation 'where' (thmdecl? prop + 'and'))
   1.466 +    ;
   1.467 +  \end{rail}
   1.468 +
   1.469 +  \begin{descr}
   1.470 +
   1.471 +  \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
   1.472 +
   1.473 +  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
   1.474 +  \isa{insts} and is positional.  All parameters must receive an
   1.475 +  instantiation term --- with the exception of defined parameters.
   1.476 +  These are, if omitted, derived from the defining equation and other
   1.477 +  instantiations.  Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
   1.478 +
   1.479 +  The command generates proof obligations for the instantiated
   1.480 +  specifications (assumes and defines elements).  Once these are
   1.481 +  discharged by the user, instantiated facts are added to the theory
   1.482 +  in a post-processing phase.
   1.483 +
   1.484 +  Additional equations, which are unfolded in facts during
   1.485 +  post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
   1.486 +  This is useful for interpreting concepts introduced through
   1.487 +  definition specification elements.  The equations must be proved.
   1.488 +  Note that if equations are present, the context expression is
   1.489 +  restricted to a locale name.
   1.490 +
   1.491 +  The command is aware of interpretations already active in the
   1.492 +  theory.  No proof obligations are generated for those, neither is
   1.493 +  post-processing applied to their facts.  This avoids duplication of
   1.494 +  interpreted facts, in particular.  Note that, in the case of a
   1.495 +  locale with import, parts of the interpretation may already be
   1.496 +  active.  The command will only generate proof obligations and
   1.497 +  process facts for new parts.
   1.498 +
   1.499 +  The context expression may be preceded by a name and/or attributes.
   1.500 +  These take effect in the post-processing of facts.  The name is used
   1.501 +  to prefix fact names, for example to avoid accidental hiding of
   1.502 +  other facts.  Attributes are applied after attributes of the
   1.503 +  interpreted facts.
   1.504 +
   1.505 +  Adding facts to locales has the effect of adding interpreted facts
   1.506 +  to the theory for all active interpretations also.  That is,
   1.507 +  interpretations dynamically participate in any facts added to
   1.508 +  locales.
   1.509 +
   1.510 +  \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]
   1.511 +
   1.512 +  This form of the command interprets \isa{expr} in the locale
   1.513 +  \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the
   1.514 +  localized version of the theorem command, the proof is in the
   1.515 +  context of \isa{name}.  After the proof obligation has been
   1.516 +  dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
   1.517 +  context \isa{name} is subsequently entered.  Note that, like
   1.518 +  import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
   1.519 +  Like facts of renamed context elements, facts obtained by
   1.520 +  interpretation may be accessed by prefixing with the parameter
   1.521 +  renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
   1.522 +
   1.523 +  Unlike interpretation in theories, instantiation is confined to the
   1.524 +  renaming of parameters, which may be specified as part of the
   1.525 +  context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
   1.526 +
   1.527 +  Only specification fragments of \isa{expr} that are not already
   1.528 +  part of \isa{name} (be it imported, derived or a derived fragment
   1.529 +  of the import) are considered by interpretation.  This enables
   1.530 +  circular interpretations.
   1.531 +
   1.532 +  If interpretations of \isa{name} exist in the current theory, the
   1.533 +  command adds interpretations for \isa{expr} as well, with the same
   1.534 +  prefix and attributes, although only for fragments of \isa{expr}
   1.535 +  that are not interpreted in the theory already.
   1.536 +
   1.537 +  \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
   1.538 +  interprets \isa{expr} in the proof context and is otherwise
   1.539 +  similar to interpretation in theories.
   1.540 +
   1.541 +  \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
   1.542 +  interpretations of a particular locale \isa{loc} that are active
   1.543 +  in the current context, either theory or proof context.  The
   1.544 +  exclamation point argument triggers printing of \emph{witness}
   1.545 +  theorems justifying interpretations.  These are normally omitted
   1.546 +  from the output.
   1.547 +  
   1.548 +  \end{descr}
   1.549 +
   1.550 +  \begin{warn}
   1.551 +    Since attributes are applied to interpreted theorems,
   1.552 +    interpretation may modify the context of common proof tools, e.g.\
   1.553 +    the Simplifier or Classical Reasoner.  Since the behavior of such
   1.554 +    automated reasoning tools is \emph{not} stable under
   1.555 +    interpretation morphisms, manual declarations might have to be
   1.556 +    issued.
   1.557 +  \end{warn}
   1.558 +
   1.559 +  \begin{warn}
   1.560 +    An interpretation in a theory may subsume previous
   1.561 +    interpretations.  This happens if the same specification fragment
   1.562 +    is interpreted twice and the instantiation of the second
   1.563 +    interpretation is more general than the interpretation of the
   1.564 +    first.  A warning is issued, since it is likely that these could
   1.565 +    have been generalized in the first place.  The locale package does
   1.566 +    not attempt to remove subsumed interpretations.
   1.567 +  \end{warn}%
   1.568 +\end{isamarkuptext}%
   1.569 +\isamarkuptrue%
   1.570 +%
   1.571 +\isamarkupsection{Classes \label{sec:class}%
   1.572 +}
   1.573 +\isamarkuptrue%
   1.574 +%
   1.575 +\begin{isamarkuptext}%
   1.576 +A class is a particular locale with \emph{exactly one} type variable
   1.577 +  \isa{{\isasymalpha}}.  Beyond the underlying locale, a corresponding type class
   1.578 +  is established which is interpreted logically as axiomatic type
   1.579 +  class \cite{Wenzel:1997:TPHOL} whose logical content are the
   1.580 +  assumptions of the locale.  Thus, classes provide the full
   1.581 +  generality of locales combined with the commodity of type classes
   1.582 +  (notably type-inference).  See \cite{isabelle-classes} for a short
   1.583 +  tutorial.
   1.584 +
   1.585 +  \begin{matharray}{rcl}
   1.586 +    \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
   1.587 +    \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
   1.588 +    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
   1.589 +    \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
   1.590 +    \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} \\
   1.591 +    \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
   1.592 +  \end{matharray}
   1.593 +
   1.594 +  \begin{rail}
   1.595 +    'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
   1.596 +      'begin'?
   1.597 +    ;
   1.598 +    'instantiation' (nameref + 'and') '::' arity 'begin'
   1.599 +    ;
   1.600 +    'instance'
   1.601 +    ;
   1.602 +    'subclass' target? nameref
   1.603 +    ;
   1.604 +    'print\_classes'
   1.605 +    ;
   1.606 +
   1.607 +    superclassexpr: nameref | (nameref '+' superclassexpr)
   1.608 +    ;
   1.609 +  \end{rail}
   1.610 +
   1.611 +  \begin{descr}
   1.612 +
   1.613 +  \item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines
   1.614 +  a new class \isa{c}, inheriting from \isa{superclasses}.  This
   1.615 +  introduces a locale \isa{c} with import of all locales \isa{superclasses}.
   1.616 +
   1.617 +  Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
   1.618 +  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
   1.619 +  \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
   1.620 +
   1.621 +  Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
   1.622 +  mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
   1.623 +  corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.  The
   1.624 +  corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}.  This rule should be rarely needed directly
   1.625 +  --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
   1.626 +  class membership proofs.
   1.627 +
   1.628 +  \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.\
   1.629 +  \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
   1.630 +  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
   1.631 +  in the target body poses a goal stating these type arities.  The
   1.632 +  target is concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
   1.633 +
   1.634 +  Note that a list of simultaneous type constructors may be given;
   1.635 +  this corresponds nicely to mutual recursive type definitions, e.g.\
   1.636 +  in Isabelle/HOL.
   1.637 +
   1.638 +  \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets
   1.639 +  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
   1.640 +  the type classes involved.  After finishing the proof, the
   1.641 +  background theory will be augmented by the proven type arities.
   1.642 +
   1.643 +  \item [\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c}] in a class context for class
   1.644 +  \isa{d} sets up a goal stating that class \isa{c} is logically
   1.645 +  contained in class \isa{d}.  After finishing the proof, class
   1.646 +  \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
   1.647 +
   1.648 +  \item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
   1.649 +  theory.
   1.650 +
   1.651 +  \item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
   1.652 +  introduction rules of this theory.  Note that this method usually
   1.653 +  needs not be named explicitly, as it is already included in the
   1.654 +  default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).  In particular,
   1.655 +  instantiation of trivial (syntactic) classes may be performed by a
   1.656 +  single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
   1.657  
   1.658    \end{descr}%
   1.659  \end{isamarkuptext}%
   1.660  \isamarkuptrue%
   1.661  %
   1.662 +\isamarkupsubsection{The class target%
   1.663 +}
   1.664 +\isamarkuptrue%
   1.665 +%
   1.666 +\begin{isamarkuptext}%
   1.667 +%FIXME check
   1.668 +
   1.669 +  A named context may refer to a locale (cf.\ \secref{sec:target}).
   1.670 +  If this locale is also a class \isa{c}, apart from the common
   1.671 +  locale target behaviour the following happens.
   1.672 +
   1.673 +  \begin{itemize}
   1.674 +
   1.675 +  \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
   1.676 +  local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
   1.677 +  are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
   1.678 +  referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
   1.679 +
   1.680 +  \item Local theorem bindings are lifted as are assumptions.
   1.681 +
   1.682 +  \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
   1.683 +  global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly.  Type inference
   1.684 +  resolves ambiguities.  In rare cases, manual type annotations are
   1.685 +  needed.
   1.686 +  
   1.687 +  \end{itemize}%
   1.688 +\end{isamarkuptext}%
   1.689 +\isamarkuptrue%
   1.690 +%
   1.691 +\isamarkupsection{Axiomatic type classes \label{sec:axclass}%
   1.692 +}
   1.693 +\isamarkuptrue%
   1.694 +%
   1.695 +\begin{isamarkuptext}%
   1.696 +\begin{warn}
   1.697 +  This describes the old interface to axiomatic type-classes in
   1.698 +  Isabelle.  See \secref{sec:class} for a more recent higher-level
   1.699 +  view on the same ideas.
   1.700 +  \end{warn}
   1.701 +
   1.702 +  \begin{matharray}{rcl}
   1.703 +    \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
   1.704 +    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
   1.705 +  \end{matharray}
   1.706 +
   1.707 +  Axiomatic type classes are Isabelle/Pure's primitive
   1.708 +  \emph{definitional} interface to type classes.  For practical
   1.709 +  applications, you should consider using classes
   1.710 +  (cf.~\secref{sec:classes}) which provide high level interface.
   1.711 +
   1.712 +  \begin{rail}
   1.713 +    'axclass' classdecl (axmdecl prop +)
   1.714 +    ;
   1.715 +    'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
   1.716 +    ;
   1.717 +  \end{rail}
   1.718 +
   1.719 +  \begin{descr}
   1.720 +  
   1.721 +  \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
   1.722 +  existing classes, with additional axioms holding.  Class axioms may
   1.723 +  not contain more than one type variable.  The class axioms (with
   1.724 +  implicit sort constraints added) are bound to the given names.
   1.725 +  Furthermore a class introduction rule is generated (being bound as
   1.726 +  \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.
   1.727 +  
   1.728 +  The ``class axioms'' are stored as theorems according to the given
   1.729 +  name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
   1.730 +  the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
   1.731 +  
   1.732 +  \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
   1.733 +  \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}}]
   1.734 +  setup a goal stating a class relation or type arity.  The proof
   1.735 +  would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
   1.736 +  the characteristic theorems of the type classes involved.  After
   1.737 +  finishing the proof, the theory will be augmented by a type
   1.738 +  signature declaration corresponding to the resulting theorem.
   1.739 +
   1.740 +  \end{descr}%
   1.741 +\end{isamarkuptext}%
   1.742 +\isamarkuptrue%
   1.743 +%
   1.744 +\isamarkupsection{Unrestricted overloading%
   1.745 +}
   1.746 +\isamarkuptrue%
   1.747 +%
   1.748 +\begin{isamarkuptext}%
   1.749 +Isabelle/Pure's definitional schemes support certain forms of
   1.750 +  overloading (see \secref{sec:consts}).  At most occassions
   1.751 +  overloading will be used in a Haskell-like fashion together with
   1.752 +  type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
   1.753 +  \secref{sec:class}).  Sometimes low-level overloading is desirable.
   1.754 +  The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
   1.755 +  end-users.
   1.756 +
   1.757 +  \begin{matharray}{rcl}
   1.758 +    \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
   1.759 +  \end{matharray}
   1.760 +
   1.761 +  \begin{rail}
   1.762 +    'overloading' \\
   1.763 +    ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
   1.764 +  \end{rail}
   1.765 +
   1.766 +  \begin{descr}
   1.767 +
   1.768 +  \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}}]
   1.769 +  opens a theory target (cf.\ \secref{sec:target}) which allows to
   1.770 +  specify constants with overloaded definitions.  These are identified
   1.771 +  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
   1.772 +  instances.  The definitions themselves are established using common
   1.773 +  specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as
   1.774 +  reference to the corresponding constants.  The target is concluded
   1.775 +  by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
   1.776 +
   1.777 +  A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
   1.778 +  the corresponding definition, which is occasionally useful for
   1.779 +  exotic overloading.  It is at the discretion of the user to avoid
   1.780 +  malformed theory specifications!
   1.781 +
   1.782 +  \end{descr}%
   1.783 +\end{isamarkuptext}%
   1.784 +\isamarkuptrue%
   1.785 +%
   1.786 +\isamarkupsection{Incorporating ML code \label{sec:ML}%
   1.787 +}
   1.788 +\isamarkuptrue%
   1.789 +%
   1.790 +\begin{isamarkuptext}%
   1.791 +\begin{matharray}{rcl}
   1.792 +    \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
   1.793 +    \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
   1.794 +    \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
   1.795 +    \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
   1.796 +    \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
   1.797 +    \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\
   1.798 +  \end{matharray}
   1.799 +
   1.800 +  \begin{rail}
   1.801 +    'use' name
   1.802 +    ;
   1.803 +    ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
   1.804 +    ;
   1.805 +    'method\_setup' name '=' text text
   1.806 +    ;
   1.807 +  \end{rail}
   1.808 +
   1.809 +  \begin{descr}
   1.810 +
   1.811 +  \item [\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML
   1.812 +  commands from \isa{{\isachardoublequote}file{\isachardoublequote}}.  The current theory context is passed
   1.813 +  down to the ML toplevel and may be modified, using \verb|"Context.>>"| or derived ML commands.  The file name is checked with
   1.814 +  the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
   1.815 +  header (see also \secref{sec:begin-thy}).
   1.816 +  
   1.817 +  \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}}.
   1.818 +
   1.819 +  \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
   1.820 +  diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context
   1.821 +  may not be updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
   1.822 +  at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
   1.823 +  
   1.824 +  \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
   1.825 +  context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
   1.826 +  of type \verb|"theory -> theory"|.  This enables to initialize
   1.827 +  any object-logic specific tools and packages written in ML, for
   1.828 +  example.
   1.829 +  
   1.830 +  \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
   1.831 +  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%
   1.832 +\verb|  Proof.context -> Proof.method"|.  Parsing concrete method syntax
   1.833 +  from \verb|Args.src| input can be quite tedious in general.  The
   1.834 +  following simple examples are for methods without any explicit
   1.835 +  arguments, or a list of theorems, respectively.
   1.836 +
   1.837 +%FIXME proper antiquotations
   1.838 +{\footnotesize
   1.839 +\begin{verbatim}
   1.840 + Method.no_args (Method.METHOD (fn facts => foobar_tac))
   1.841 + Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
   1.842 + Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
   1.843 + Method.thms_ctxt_args (fn thms => fn ctxt =>
   1.844 +    Method.METHOD (fn facts => foobar_tac))
   1.845 +\end{verbatim}
   1.846 +}
   1.847 +
   1.848 +  Note that mere tactic emulations may ignore the \isa{facts}
   1.849 +  parameter above.  Proper proof methods would do something
   1.850 +  appropriate with the list of current facts, though.  Single-rule
   1.851 +  methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
   1.852 +  using \verb|Method.insert_tac| before applying the main tactic.
   1.853 +
   1.854 +  \end{descr}%
   1.855 +\end{isamarkuptext}%
   1.856 +\isamarkuptrue%
   1.857 +%
   1.858 +\isamarkupsection{Primitive specification elements%
   1.859 +}
   1.860 +\isamarkuptrue%
   1.861 +%
   1.862 +\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
   1.863 +}
   1.864 +\isamarkuptrue%
   1.865 +%
   1.866 +\begin{isamarkuptext}%
   1.867 +\begin{matharray}{rcll}
   1.868 +    \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
   1.869 +    \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   1.870 +    \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
   1.871 +    \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
   1.872 +  \end{matharray}
   1.873 +
   1.874 +  \begin{rail}
   1.875 +    'classes' (classdecl +)
   1.876 +    ;
   1.877 +    'classrel' (nameref ('<' | subseteq) nameref + 'and')
   1.878 +    ;
   1.879 +    'defaultsort' sort
   1.880 +    ;
   1.881 +  \end{rail}
   1.882 +
   1.883 +  \begin{descr}
   1.884 +
   1.885 +  \item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]
   1.886 +  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.
   1.887 +
   1.888 +  \item [\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states
   1.889 +  subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and
   1.890 +  \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
   1.891 +  introduce proven class relations.
   1.892 +
   1.893 +  \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the
   1.894 +  new default sort for any type variables given without sort
   1.895 +  constraints.  Usually, the default sort would be only changed when
   1.896 +  defining a new object-logic.
   1.897 +
   1.898 +  \item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
   1.899 +  using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
   1.900 +
   1.901 +  \end{descr}%
   1.902 +\end{isamarkuptext}%
   1.903 +\isamarkuptrue%
   1.904 +%
   1.905 +\isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
   1.906 +}
   1.907 +\isamarkuptrue%
   1.908 +%
   1.909 +\begin{isamarkuptext}%
   1.910 +\begin{matharray}{rcll}
   1.911 +    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\
   1.912 +    \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\
   1.913 +    \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\
   1.914 +    \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   1.915 +  \end{matharray}
   1.916 +
   1.917 +  \begin{rail}
   1.918 +    'types' (typespec '=' type infix? +)
   1.919 +    ;
   1.920 +    'typedecl' typespec infix?
   1.921 +    ;
   1.922 +    'nonterminals' (name +)
   1.923 +    ;
   1.924 +    'arities' (nameref '::' arity +)
   1.925 +    ;
   1.926 +  \end{rail}
   1.927 +
   1.928 +  \begin{descr}
   1.929 +
   1.930 +  \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}}]
   1.931 +  introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}
   1.932 +  for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.  Unlike actual type definitions, as
   1.933 +  are available in Isabelle/HOL for example, type synonyms are just
   1.934 +  purely syntactic abbreviations without any logical significance.
   1.935 +  Internally, type synonyms are fully expanded.
   1.936 +  
   1.937 +  \item [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]
   1.938 +  declares a new type constructor \isa{t}, intended as an actual
   1.939 +  logical type (of the object-logic, if available).
   1.940 +
   1.941 +  \item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type
   1.942 +  constructors \isa{c} (without arguments) to act as purely
   1.943 +  syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
   1.944 +  syntax of terms or types.
   1.945 +
   1.946 +  \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
   1.947 +  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
   1.948 +  introduce proven type arities.
   1.949 +
   1.950 +  \end{descr}%
   1.951 +\end{isamarkuptext}%
   1.952 +\isamarkuptrue%
   1.953 +%
   1.954 +\isamarkupsubsection{Constants and definitions \label{sec:consts}%
   1.955 +}
   1.956 +\isamarkuptrue%
   1.957 +%
   1.958 +\begin{isamarkuptext}%
   1.959 +Definitions essentially express abbreviations within the logic.  The
   1.960 +  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
   1.961 +  where the arguments of \isa{c} appear on the left, abbreviating a
   1.962 +  prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
   1.963 +  written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.  Moreover,
   1.964 +  definitions may be weakened by adding arbitrary pre-conditions:
   1.965 +  \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
   1.966 +
   1.967 +  \medskip The built-in well-formedness conditions for definitional
   1.968 +  specifications are:
   1.969 +
   1.970 +  \begin{itemize}
   1.971 +
   1.972 +  \item Arguments (on the left-hand side) must be distinct variables.
   1.973 +
   1.974 +  \item All variables on the right-hand side must also appear on the
   1.975 +  left-hand side.
   1.976 +
   1.977 +  \item All type variables on the right-hand side must also appear on
   1.978 +  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.
   1.979 +
   1.980 +  \item The definition must not be recursive.  Most object-logics
   1.981 +  provide definitional principles that can be used to express
   1.982 +  recursion safely.
   1.983 +
   1.984 +  \end{itemize}
   1.985 +
   1.986 +  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
   1.987 +  recursively at type instances corresponding to the immediate
   1.988 +  argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}.  Incomplete
   1.989 +  specification patterns impose global constraints on all occurrences,
   1.990 +  e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
   1.991 +  corresponding occurrences on some right-hand side need to be an
   1.992 +  instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
   1.993 +
   1.994 +  \begin{matharray}{rcl}
   1.995 +    \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
   1.996 +    \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\
   1.997 +    \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isartrans{theory}{theory} \\
   1.998 +  \end{matharray}
   1.999 +
  1.1000 +  \begin{rail}
  1.1001 +    'consts' ((name '::' type mixfix?) +)
  1.1002 +    ;
  1.1003 +    'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
  1.1004 +    ;
  1.1005 +  \end{rail}
  1.1006 +
  1.1007 +  \begin{rail}
  1.1008 +    'constdefs' structs? (constdecl? constdef +)
  1.1009 +    ;
  1.1010 +
  1.1011 +    structs: '(' 'structure' (vars + 'and') ')'
  1.1012 +    ;
  1.1013 +    constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
  1.1014 +    ;
  1.1015 +    constdef: thmdecl? prop
  1.1016 +    ;
  1.1017 +  \end{rail}
  1.1018 +
  1.1019 +  \begin{descr}
  1.1020 +
  1.1021 +  \item [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant
  1.1022 +  \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}.  The
  1.1023 +  optional mixfix annotations may attach concrete syntax to the
  1.1024 +  constants declared.
  1.1025 +  
  1.1026 +  \item [\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn}
  1.1027 +  as a definitional axiom for some existing constant.
  1.1028 +  
  1.1029 +  The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
  1.1030 +  for this definition, which is occasionally useful for exotic
  1.1031 +  overloading.  It is at the discretion of the user to avoid malformed
  1.1032 +  theory specifications!
  1.1033 +  
  1.1034 +  The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
  1.1035 +  potentially overloaded.  Unless this option is given, a warning
  1.1036 +  message would be issued for any definitional equation with a more
  1.1037 +  special type than that of the corresponding constant declaration.
  1.1038 +  
  1.1039 +  \item [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}] provides a streamlined combination of
  1.1040 +  constants declarations and definitions: type-inference takes care of
  1.1041 +  the most general typing of the given specification (the optional
  1.1042 +  type constraint may refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual).  The resulting type declaration needs to agree with
  1.1043 +  that of the specification; overloading is \emph{not} supported here!
  1.1044 +  
  1.1045 +  The constant name may be omitted altogether, if neither type nor
  1.1046 +  syntax declarations are given.  The canonical name of the
  1.1047 +  definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
  1.1048 +  unless specified otherwise.  Also note that the given list of
  1.1049 +  specifications is processed in a strictly sequential manner, with
  1.1050 +  type-checking being performed independently.
  1.1051 +  
  1.1052 +  An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
  1.1053 +  admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'').  The latter concept is
  1.1054 +  particularly useful with locales (see also \S\ref{sec:locale}).
  1.1055 +
  1.1056 +  \end{descr}%
  1.1057 +\end{isamarkuptext}%
  1.1058 +\isamarkuptrue%
  1.1059 +%
  1.1060 +\isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
  1.1061 +}
  1.1062 +\isamarkuptrue%
  1.1063 +%
  1.1064 +\begin{isamarkuptext}%
  1.1065 +\begin{matharray}{rcll}
  1.1066 +    \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
  1.1067 +    \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
  1.1068 +    \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & isarkeep{local{\dsh}theory} \\
  1.1069 +  \end{matharray}
  1.1070 +
  1.1071 +  \begin{rail}
  1.1072 +    'axioms' (axmdecl prop +)
  1.1073 +    ;
  1.1074 +    ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
  1.1075 +    ;
  1.1076 +  \end{rail}
  1.1077 +
  1.1078 +  \begin{descr}
  1.1079 +  
  1.1080 +  \item [\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduces arbitrary
  1.1081 +  statements as axioms of the meta-logic.  In fact, axioms are
  1.1082 +  ``axiomatic theorems'', and may be referred later just as any other
  1.1083 +  theorem.
  1.1084 +  
  1.1085 +  Axioms are usually only introduced when declaring new logical
  1.1086 +  systems.  Everyday work is typically done the hard way, with proper
  1.1087 +  definitions and proven theorems.
  1.1088 +  
  1.1089 +  \item [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
  1.1090 +  retrieves and stores existing facts in the theory context, or the
  1.1091 +  specified target context (see also \secref{sec:target}).  Typical
  1.1092 +  applications would also involve attributes, to declare Simplifier
  1.1093 +  rules, for example.
  1.1094 +  
  1.1095 +  \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.
  1.1096 +
  1.1097 +  \end{descr}%
  1.1098 +\end{isamarkuptext}%
  1.1099 +\isamarkuptrue%
  1.1100 +%
  1.1101 +\isamarkupsection{Oracles%
  1.1102 +}
  1.1103 +\isamarkuptrue%
  1.1104 +%
  1.1105 +\begin{isamarkuptext}%
  1.1106 +\begin{matharray}{rcl}
  1.1107 +    \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
  1.1108 +  \end{matharray}
  1.1109 +
  1.1110 +  The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
  1.1111 +  type \verb|T| given by the user.  This acts like an infinitary
  1.1112 +  specification of axioms -- there is no internal check of the
  1.1113 +  correctness of the results!  The inference kernel records oracle
  1.1114 +  invocations within the internal derivation object of theorems, and
  1.1115 +  the pretty printer attaches ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results
  1.1116 +  that are not fully checked by Isabelle inferences.
  1.1117 +
  1.1118 +  \begin{rail}
  1.1119 +    'oracle' name '(' type ')' '=' text
  1.1120 +    ;
  1.1121 +  \end{rail}
  1.1122 +
  1.1123 +  \begin{descr}
  1.1124 +
  1.1125 +  \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
  1.1126 +  given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
  1.1127 +  \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
  1.1128 +  ML function of type
  1.1129 +  \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
  1.1130 +  bound to the global identifier \verb|name|.
  1.1131 +
  1.1132 +  \end{descr}%
  1.1133 +\end{isamarkuptext}%
  1.1134 +\isamarkuptrue%
  1.1135 +%
  1.1136 +\isamarkupsection{Name spaces%
  1.1137 +}
  1.1138 +\isamarkuptrue%
  1.1139 +%
  1.1140 +\begin{isamarkuptext}%
  1.1141 +\begin{matharray}{rcl}
  1.1142 +    \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\
  1.1143 +    \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\
  1.1144 +    \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isartrans{theory}{theory} \\
  1.1145 +  \end{matharray}
  1.1146 +
  1.1147 +  \begin{rail}
  1.1148 +    'hide' ('(open)')? name (nameref + )
  1.1149 +    ;
  1.1150 +  \end{rail}
  1.1151 +
  1.1152 +  Isabelle organizes any kind of name declarations (of types,
  1.1153 +  constants, theorems etc.) by separate hierarchically structured name
  1.1154 +  spaces.  Normally the user does not have to control the behavior of
  1.1155 +  name spaces by hand, yet the following commands provide some way to
  1.1156 +  do so.
  1.1157 +
  1.1158 +  \begin{descr}
  1.1159 +
  1.1160 +  \item [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the
  1.1161 +  current name declaration mode.  Initially, theories start in
  1.1162 +  \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically
  1.1163 +  qualified by the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}
  1.1164 +  causes all names to be declared without the theory prefix, until
  1.1165 +  \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
  1.1166 +  
  1.1167 +  Note that global names are prone to get hidden accidently later,
  1.1168 +  when qualified names of the same base name are introduced.
  1.1169 +  
  1.1170 +  \item [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes
  1.1171 +  declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
  1.1172 +  \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
  1.1173 +  (unqualified) names may never be hidden.
  1.1174 +  
  1.1175 +  Note that hiding name space accesses has no impact on logical
  1.1176 +  declarations -- they remain valid internally.  Entities that are no
  1.1177 +  longer accessible to the user are printed with the special qualifier
  1.1178 +  ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
  1.1179 +
  1.1180 +  \end{descr}%
  1.1181 +\end{isamarkuptext}%
  1.1182 +\isamarkuptrue%
  1.1183 +%
  1.1184 +\isamarkupsection{Syntax and translations \label{sec:syn-trans}%
  1.1185 +}
  1.1186 +\isamarkuptrue%
  1.1187 +%
  1.1188 +\begin{isamarkuptext}%
  1.1189 +\begin{matharray}{rcl}
  1.1190 +    \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\
  1.1191 +    \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
  1.1192 +    \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\
  1.1193 +    \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\
  1.1194 +  \end{matharray}
  1.1195 +
  1.1196 +  \begin{rail}
  1.1197 +    ('syntax' | 'no\_syntax') mode? (constdecl +)
  1.1198 +    ;
  1.1199 +    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
  1.1200 +    ;
  1.1201 +
  1.1202 +    mode: ('(' ( name | 'output' | name 'output' ) ')')
  1.1203 +    ;
  1.1204 +    transpat: ('(' nameref ')')? string
  1.1205 +    ;
  1.1206 +  \end{rail}
  1.1207 +
  1.1208 +  \begin{descr}
  1.1209 +  
  1.1210 +  \item [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to
  1.1211 +  \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical
  1.1212 +  signature extension is omitted.  Thus the context free grammar of
  1.1213 +  Isabelle's inner syntax may be augmented in arbitrary ways,
  1.1214 +  independently of the logic.  The \isa{mode} argument refers to the
  1.1215 +  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
  1.1216 +  input and output grammar.
  1.1217 +  
  1.1218 +  \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
  1.1219 +  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.
  1.1220 +  
  1.1221 +  \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic
  1.1222 +  translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
  1.1223 +  parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
  1.1224 +  Translation patterns may be prefixed by the syntactic category to be
  1.1225 +  used for parsing; the default is \isa{logic}.
  1.1226 +  
  1.1227 +  \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
  1.1228 +  translation rules, which are interpreted in the same manner as for
  1.1229 +  \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
  1.1230 +
  1.1231 +  \end{descr}%
  1.1232 +\end{isamarkuptext}%
  1.1233 +\isamarkuptrue%
  1.1234 +%
  1.1235 +\isamarkupsection{Syntax translation functions%
  1.1236 +}
  1.1237 +\isamarkuptrue%
  1.1238 +%
  1.1239 +\begin{isamarkuptext}%
  1.1240 +\begin{matharray}{rcl}
  1.1241 +    \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} \\
  1.1242 +    \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
  1.1243 +    \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
  1.1244 +    \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} \\
  1.1245 +    \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} \\
  1.1246 +    \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
  1.1247 +  \end{matharray}
  1.1248 +
  1.1249 +  \begin{rail}
  1.1250 +  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
  1.1251 +    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
  1.1252 +  ;
  1.1253 +
  1.1254 +  'token\_translation' text
  1.1255 +  ;
  1.1256 +  \end{rail}
  1.1257 +
  1.1258 +  Syntax translation functions written in ML admit almost arbitrary
  1.1259 +  manipulations of Isabelle's inner syntax.  Any of the above commands
  1.1260 +  have a single \railqtok{text} argument that refers to an ML
  1.1261 +  expression of appropriate type, which are as follows by default:
  1.1262 +
  1.1263 +%FIXME proper antiquotations
  1.1264 +\begin{ttbox}
  1.1265 +val parse_ast_translation   : (string * (ast list -> ast)) list
  1.1266 +val parse_translation       : (string * (term list -> term)) list
  1.1267 +val print_translation       : (string * (term list -> term)) list
  1.1268 +val typed_print_translation :
  1.1269 +  (string * (bool -> typ -> term list -> term)) list
  1.1270 +val print_ast_translation   : (string * (ast list -> ast)) list
  1.1271 +val token_translation       :
  1.1272 +  (string * string * (string -> string * real)) list
  1.1273 +\end{ttbox}
  1.1274 +
  1.1275 +  If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
  1.1276 +  translation functions may depend on the current theory or proof
  1.1277 +  context.  This allows to implement advanced syntax mechanisms, as
  1.1278 +  translations functions may refer to specific theory declarations or
  1.1279 +  auxiliary proof data.
  1.1280 +
  1.1281 +  See also \cite[\S8]{isabelle-ref} for more information on the
  1.1282 +  general concept of syntax transformations in Isabelle.
  1.1283 +
  1.1284 +%FIXME proper antiquotations
  1.1285 +\begin{ttbox}
  1.1286 +val parse_ast_translation:
  1.1287 +  (string * (Context.generic -> ast list -> ast)) list
  1.1288 +val parse_translation:
  1.1289 +  (string * (Context.generic -> term list -> term)) list
  1.1290 +val print_translation:
  1.1291 +  (string * (Context.generic -> term list -> term)) list
  1.1292 +val typed_print_translation:
  1.1293 +  (string * (Context.generic -> bool -> typ -> term list -> term)) list
  1.1294 +val print_ast_translation:
  1.1295 +  (string * (Context.generic -> ast list -> ast)) list
  1.1296 +\end{ttbox}%
  1.1297 +\end{isamarkuptext}%
  1.1298 +\isamarkuptrue%
  1.1299 +%
  1.1300  \isadelimtheory
  1.1301  %
  1.1302  \endisadelimtheory