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