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