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