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