src/Doc/Isar_Ref/Spec.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59785 4e6ab5831cc0
child 59901 840d03805755
permissions -rw-r--r--
tuned signature;
wenzelm@26869
     1
theory Spec
haftmann@59003
     2
imports Base Main "~~/src/Tools/Permanent_Interpretation"
wenzelm@26869
     3
begin
wenzelm@26869
     4
wenzelm@58618
     5
chapter \<open>Specifications\<close>
wenzelm@26869
     6
wenzelm@59781
     7
text \<open>The Isabelle/Isar theory format integrates specifications and proofs,
wenzelm@59781
     8
  with support for interactive development by continuous document editing.
wenzelm@59781
     9
  There is a separate document preparation system (see
wenzelm@59781
    10
  \chref{ch:document-prep}), for typesetting formal developments together
wenzelm@59781
    11
  with informal text. The resulting hyper-linked PDF documents can be used
wenzelm@59781
    12
  both for WWW presentation and printed copies.
wenzelm@29745
    13
wenzelm@29745
    14
  The Isar proof language (see \chref{ch:proofs}) is embedded into the
wenzelm@29745
    15
  theory language as a proper sub-language.  Proof mode is entered by
wenzelm@29745
    16
  stating some @{command theorem} or @{command lemma} at the theory
wenzelm@29745
    17
  level, and left again with the final conclusion (e.g.\ via @{command
wenzelm@59781
    18
  qed}).
wenzelm@58618
    19
\<close>
wenzelm@29745
    20
wenzelm@29745
    21
wenzelm@58618
    22
section \<open>Defining theories \label{sec:begin-thy}\<close>
wenzelm@26870
    23
wenzelm@58618
    24
text \<open>
wenzelm@26870
    25
  \begin{matharray}{rcl}
wenzelm@28761
    26
    @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
wenzelm@28761
    27
    @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
wenzelm@26870
    28
  \end{matharray}
wenzelm@26870
    29
wenzelm@59781
    30
  Isabelle/Isar theories are defined via theory files, which consist of an
wenzelm@59781
    31
  outermost sequence of definition--statement--proof elements. Some
wenzelm@59781
    32
  definitions are self-sufficient (e.g.\ @{command fun} in Isabelle/HOL),
wenzelm@59781
    33
  with foundational proofs performed internally. Other definitions require
wenzelm@59781
    34
  an explicit proof as justification (e.g.\ @{command function} and
wenzelm@59781
    35
  @{command termination} in Isabelle/HOL). Plain statements like @{command
wenzelm@59781
    36
  theorem} or @{command lemma} are merely a special case of that, defining a
wenzelm@59781
    37
  theorem from a given proposition and its proof.
wenzelm@26870
    38
wenzelm@59781
    39
  The theory body may be sub-structured by means of \emph{local theory
wenzelm@59781
    40
  targets}, such as @{command "locale"} and @{command "class"}. It is also
wenzelm@59781
    41
  possible to use @{command context}~@{keyword "begin"}~\dots~@{command end}
wenzelm@59781
    42
  blocks to delimited a local theory context: a \emph{named context} to
wenzelm@59781
    43
  augment a locale or class specification, or an \emph{unnamed context} to
wenzelm@59781
    44
  refer to local parameters and assumptions that are discharged later. See
wenzelm@59781
    45
  \secref{sec:target} for more details.
wenzelm@28745
    46
wenzelm@59781
    47
  \medskip A theory is commenced by the @{command "theory"} command, which
wenzelm@59781
    48
  indicates imports of previous theories, according to an acyclic
wenzelm@59781
    49
  foundational order. Before the initial @{command "theory"} command, there
wenzelm@59781
    50
  may be optional document header material (like @{command section} or
wenzelm@59781
    51
  @{command text}, see \secref{sec:markup}). The document header is outside
wenzelm@59781
    52
  of the formal theory context, though.
wenzelm@59781
    53
wenzelm@59781
    54
  A theory is concluded by a final @{command (global) "end"} command, one
wenzelm@59781
    55
  that does not belong to a local theory target. No further commands may
wenzelm@59781
    56
  follow such a global @{command (global) "end"}.
wenzelm@26870
    57
wenzelm@55112
    58
  @{rail \<open>
wenzelm@59781
    59
    @@{command theory} @{syntax name} imports? keywords? \<newline> @'begin'
wenzelm@26870
    60
    ;
wenzelm@47114
    61
    imports: @'imports' (@{syntax name} +)
wenzelm@47114
    62
    ;
wenzelm@50128
    63
    keywords: @'keywords' (keyword_decls + @'and')
wenzelm@50128
    64
    ;
wenzelm@50128
    65
    keyword_decls: (@{syntax string} +)
wenzelm@50128
    66
      ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
wenzelm@55112
    67
  \<close>}
wenzelm@26870
    68
wenzelm@28760
    69
  \begin{description}
wenzelm@26870
    70
wenzelm@28760
    71
  \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
wenzelm@28760
    72
  starts a new theory @{text A} based on the merge of existing
wenzelm@47114
    73
  theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.  Due to the possibility to import more
wenzelm@47114
    74
  than one ancestor, the resulting theory structure of an Isabelle
wenzelm@47114
    75
  session forms a directed acyclic graph (DAG).  Isabelle takes care
wenzelm@47114
    76
  that sources contributing to the development graph are always
wenzelm@47114
    77
  up-to-date: changed files are automatically rechecked whenever a
wenzelm@47114
    78
  theory header specification is processed.
wenzelm@47114
    79
wenzelm@59781
    80
  Empty imports are only allowed in the bootstrap process of the special
wenzelm@59781
    81
  theory @{theory Pure}, which is the start of any other formal development
wenzelm@59781
    82
  based on Isabelle. Regular user theories usually refer to some more
wenzelm@59781
    83
  complex entry point, such as theory @{theory Main} in Isabelle/HOL.
wenzelm@59781
    84
wenzelm@47114
    85
  The optional @{keyword_def "keywords"} specification declares outer
wenzelm@47114
    86
  syntax (\chref{ch:outer-syntax}) that is introduced in this theory
wenzelm@47114
    87
  later on (rare in end-user applications).  Both minor keywords and
wenzelm@47114
    88
  major keywords of the Isar command language need to be specified, in
wenzelm@47114
    89
  order to make parsing of proof documents work properly.  Command
wenzelm@47114
    90
  keywords need to be classified according to their structural role in
wenzelm@47114
    91
  the formal text.  Examples may be seen in Isabelle/HOL sources
wenzelm@58724
    92
  itself, such as @{keyword "keywords"}~@{verbatim \<open>"typedef"\<close>}
wenzelm@47114
    93
  @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
wenzelm@58724
    94
  \<open>"datatype"\<close>} @{text ":: thy_decl"} for theory-level declarations
wenzelm@47114
    95
  with and without proof, respectively.  Additional @{syntax tags}
wenzelm@47114
    96
  provide defaults for document preparation (\secref{sec:tags}).
wenzelm@50128
    97
wenzelm@59781
    98
  It is possible to specify an alternative completion via @{verbatim
wenzelm@59781
    99
  "=="}~@{text "text"}, while the default is the corresponding keyword name.
wenzelm@26870
   100
  
wenzelm@28760
   101
  \item @{command (global) "end"} concludes the current theory
wenzelm@47114
   102
  definition.  Note that some other commands, e.g.\ local theory
wenzelm@47114
   103
  targets @{command locale} or @{command class} may involve a
wenzelm@47114
   104
  @{keyword "begin"} that needs to be matched by @{command (local)
wenzelm@47114
   105
  "end"}, according to the usual rules for nested blocks.
wenzelm@27040
   106
wenzelm@28760
   107
  \end{description}
wenzelm@58618
   108
\<close>
wenzelm@27040
   109
wenzelm@27040
   110
wenzelm@58618
   111
section \<open>Local theory targets \label{sec:target}\<close>
wenzelm@27040
   112
wenzelm@58618
   113
text \<open>
wenzelm@47483
   114
  \begin{matharray}{rcll}
wenzelm@47483
   115
    @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
wenzelm@47483
   116
    @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
wenzelm@47483
   117
  \end{matharray}
wenzelm@47483
   118
wenzelm@59781
   119
  A local theory target is a specification context that is managed
wenzelm@59781
   120
  separately within the enclosing theory. Contexts may introduce parameters
wenzelm@59781
   121
  (fixed variables) and assumptions (hypotheses). Definitions and theorems
wenzelm@47482
   122
  depending on the context may be added incrementally later on.
wenzelm@47482
   123
wenzelm@47482
   124
  \emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or
wenzelm@47482
   125
  type classes (cf.\ \secref{sec:class}); the name ``@{text "-"}''
wenzelm@47482
   126
  signifies the global theory context.
wenzelm@47482
   127
wenzelm@47482
   128
  \emph{Unnamed contexts} may introduce additional parameters and
wenzelm@47482
   129
  assumptions, and results produced in the context are generalized
wenzelm@47482
   130
  accordingly.  Such auxiliary contexts may be nested within other
wenzelm@47482
   131
  targets, like @{command "locale"}, @{command "class"}, @{command
wenzelm@47482
   132
  "instantiation"}, @{command "overloading"}.
wenzelm@27040
   133
wenzelm@55112
   134
  @{rail \<open>
wenzelm@47484
   135
    @@{command context} @{syntax nameref} @'begin'
wenzelm@27040
   136
    ;
wenzelm@55112
   137
    @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
wenzelm@47484
   138
    ;
wenzelm@46999
   139
    @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
wenzelm@55112
   140
  \<close>}
wenzelm@27040
   141
wenzelm@28760
   142
  \begin{description}
wenzelm@27040
   143
  
wenzelm@47482
   144
  \item @{command "context"}~@{text "c \<BEGIN>"} opens a named
wenzelm@47482
   145
  context, by recommencing an existing locale or class @{text c}.
wenzelm@47482
   146
  Note that locale and class definitions allow to include the
wenzelm@47482
   147
  @{keyword "begin"} keyword as well, in order to continue the local
wenzelm@47482
   148
  theory immediately after the initial specification.
wenzelm@47482
   149
wenzelm@47484
   150
  \item @{command "context"}~@{text "bundles elements \<BEGIN>"} opens
wenzelm@47484
   151
  an unnamed context, by extending the enclosing global or local
wenzelm@47484
   152
  theory target by the given declaration bundles (\secref{sec:bundle})
wenzelm@47484
   153
  and context elements (@{text "\<FIXES>"}, @{text "\<ASSUMES>"}
wenzelm@47484
   154
  etc.).  This means any results stemming from definitions and proofs
wenzelm@47484
   155
  in the extended context will be exported into the enclosing target
wenzelm@47484
   156
  by lifting over extra parameters and premises.
wenzelm@27040
   157
  
wenzelm@47482
   158
  \item @{command (local) "end"} concludes the current local theory,
wenzelm@47482
   159
  according to the nesting of contexts.  Note that a global @{command
wenzelm@47482
   160
  (global) "end"} has a different meaning: it concludes the theory
wenzelm@47482
   161
  itself (\secref{sec:begin-thy}).
wenzelm@27040
   162
  
wenzelm@59783
   163
  \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
wenzelm@59783
   164
  theory command specifies an immediate target, e.g.\ ``@{command
wenzelm@59783
   165
  "definition"}~@{text "(\<IN> c)"}'' or ``@{command "theorem"}~@{text
wenzelm@59783
   166
  "(\<IN> c)"}''. This works both in a local or global theory context; the
wenzelm@59783
   167
  current target context will be suspended for this command only. Note that
wenzelm@59783
   168
  ``@{text "(\<IN> -)"}'' will always produce a global result independently
wenzelm@59783
   169
  of the current target context.
wenzelm@27040
   170
wenzelm@28760
   171
  \end{description}
wenzelm@27040
   172
wenzelm@59783
   173
  Any specification element that operates on @{text local_theory} according
wenzelm@59783
   174
  to this manual implicitly allows the above target syntax @{text
wenzelm@59783
   175
  "("}@{keyword "in"}~@{text "c)"}, but individual syntax diagrams omit that
wenzelm@59783
   176
  aspect for clarity.
wenzelm@59783
   177
wenzelm@59783
   178
  \medskip The exact meaning of results produced within a local theory
wenzelm@59783
   179
  context depends on the underlying target infrastructure (locale, type
wenzelm@59783
   180
  class etc.). The general idea is as follows, considering a context named
wenzelm@27040
   181
  @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
wenzelm@27040
   182
  
wenzelm@27040
   183
  Definitions are exported by introducing a global version with
wenzelm@27040
   184
  additional arguments; a syntactic abbreviation links the long form
wenzelm@27040
   185
  with the abstract version of the target context.  For example,
wenzelm@27040
   186
  @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
wenzelm@27040
   187
  level (for arbitrary @{text "?x"}), together with a local
wenzelm@27040
   188
  abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
wenzelm@27040
   189
  fixed parameter @{text x}).
wenzelm@27040
   190
wenzelm@27040
   191
  Theorems are exported by discharging the assumptions and
wenzelm@27040
   192
  generalizing the parameters of the context.  For example, @{text "a:
wenzelm@27040
   193
  B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
wenzelm@27040
   194
  @{text "?x"}.
wenzelm@59783
   195
\<close>
wenzelm@27040
   196
wenzelm@27040
   197
wenzelm@58618
   198
section \<open>Bundled declarations \label{sec:bundle}\<close>
wenzelm@47484
   199
wenzelm@58618
   200
text \<open>
wenzelm@47484
   201
  \begin{matharray}{rcl}
wenzelm@47484
   202
    @{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@47484
   203
    @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
wenzelm@47484
   204
    @{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
wenzelm@47484
   205
    @{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
wenzelm@47484
   206
    @{keyword_def "includes"} & : & syntax \\
wenzelm@47484
   207
  \end{matharray}
wenzelm@47484
   208
wenzelm@47484
   209
  The outer syntax of fact expressions (\secref{sec:syn-att}) involves
wenzelm@47484
   210
  theorems and attributes, which are evaluated in the context and
wenzelm@47484
   211
  applied to it.  Attributes may declare theorems to the context, as
wenzelm@47484
   212
  in @{text "this_rule [intro] that_rule [elim]"} for example.
wenzelm@47484
   213
  Configuration options (\secref{sec:config}) are special declaration
wenzelm@47484
   214
  attributes that operate on the context without a theorem, as in
wenzelm@47484
   215
  @{text "[[show_types = false]]"} for example.
wenzelm@47484
   216
wenzelm@47484
   217
  Expressions of this form may be defined as \emph{bundled
wenzelm@47484
   218
  declarations} in the context, and included in other situations later
wenzelm@47484
   219
  on.  Including declaration bundles augments a local context casually
wenzelm@47484
   220
  without logical dependencies, which is in contrast to locales and
wenzelm@47484
   221
  locale interpretation (\secref{sec:locale}).
wenzelm@47484
   222
wenzelm@55112
   223
  @{rail \<open>
wenzelm@59785
   224
    @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
wenzelm@47484
   225
    ;
wenzelm@47484
   226
    (@@{command include} | @@{command including}) (@{syntax nameref}+)
wenzelm@47484
   227
    ;
wenzelm@55112
   228
    @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
wenzelm@55112
   229
  \<close>}
wenzelm@47484
   230
wenzelm@47484
   231
  \begin{description}
wenzelm@47484
   232
wenzelm@47484
   233
  \item @{command bundle}~@{text "b = decls"} defines a bundle of
wenzelm@47484
   234
  declarations in the current context.  The RHS is similar to the one
wenzelm@47484
   235
  of the @{command declare} command.  Bundles defined in local theory
wenzelm@47484
   236
  targets are subject to transformations via morphisms, when moved
wenzelm@47484
   237
  into different application contexts; this works analogously to any
wenzelm@47484
   238
  other local theory specification.
wenzelm@47484
   239
wenzelm@47484
   240
  \item @{command print_bundles} prints the named bundles that are
wenzelm@47484
   241
  available in the current context.
wenzelm@47484
   242
wenzelm@47484
   243
  \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
wenzelm@47484
   244
  from the given bundles into the current proof body context.  This is
wenzelm@47484
   245
  analogous to @{command "note"} (\secref{sec:proof-facts}) with the
wenzelm@47484
   246
  expanded bundles.
wenzelm@47484
   247
wenzelm@47484
   248
  \item @{command including} is similar to @{command include}, but
wenzelm@47484
   249
  works in proof refinement (backward mode).  This is analogous to
wenzelm@47484
   250
  @{command "using"} (\secref{sec:proof-facts}) with the expanded
wenzelm@47484
   251
  bundles.
wenzelm@47484
   252
wenzelm@47484
   253
  \item @{keyword "includes"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is similar to
wenzelm@47484
   254
  @{command include}, but works in situations where a specification
wenzelm@47484
   255
  context is constructed, notably for @{command context} and long
wenzelm@47484
   256
  statements of @{command theorem} etc.
wenzelm@47484
   257
wenzelm@47484
   258
  \end{description}
wenzelm@47484
   259
wenzelm@47484
   260
  Here is an artificial example of bundling various configuration
wenzelm@58618
   261
  options:\<close>
wenzelm@47484
   262
wenzelm@53536
   263
bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
wenzelm@47484
   264
wenzelm@47484
   265
lemma "x = x"
wenzelm@47484
   266
  including trace by metis
wenzelm@47484
   267
wenzelm@47484
   268
wenzelm@58618
   269
section \<open>Term definitions \label{sec:term-definitions}\<close>
wenzelm@27040
   270
wenzelm@58618
   271
text \<open>
wenzelm@27040
   272
  \begin{matharray}{rcll}
wenzelm@28761
   273
    @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761
   274
    @{attribute_def "defn"} & : & @{text attribute} \\
wenzelm@51585
   275
    @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
wenzelm@28761
   276
    @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761
   277
    @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
wenzelm@27040
   278
  \end{matharray}
wenzelm@27040
   279
wenzelm@57487
   280
  Term definitions may either happen within the logic (as equational axioms
wenzelm@57487
   281
  of a certain form, see also see \secref{sec:consts}), or outside of it as
wenzelm@57487
   282
  rewrite system on abstract syntax. The second form is called
wenzelm@57487
   283
  ``abbreviation''.
wenzelm@27040
   284
wenzelm@55112
   285
  @{rail \<open>
wenzelm@59783
   286
    @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
wenzelm@27040
   287
    ;
wenzelm@59783
   288
    @@{command abbreviation} @{syntax mode}? \<newline>
wenzelm@42596
   289
      (decl @'where')? @{syntax prop}
wenzelm@27040
   290
    ;
wenzelm@27040
   291
wenzelm@42596
   292
    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
wenzelm@55112
   293
  \<close>}
wenzelm@27040
   294
wenzelm@28760
   295
  \begin{description}
wenzelm@27040
   296
  
wenzelm@28760
   297
  \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
wenzelm@27040
   298
  internal definition @{text "c \<equiv> t"} according to the specification
wenzelm@27040
   299
  given as @{text eq}, which is then turned into a proven fact.  The
wenzelm@27040
   300
  given proposition may deviate from internal meta-level equality
wenzelm@27040
   301
  according to the rewrite rules declared as @{attribute defn} by the
wenzelm@27040
   302
  object-logic.  This usually covers object-level equality @{text "x =
wenzelm@27040
   303
  y"} and equivalence @{text "A \<leftrightarrow> B"}.  End-users normally need not
wenzelm@27040
   304
  change the @{attribute defn} setup.
wenzelm@27040
   305
  
wenzelm@27040
   306
  Definitions may be presented with explicit arguments on the LHS, as
wenzelm@27040
   307
  well as additional conditions, e.g.\ @{text "f x y = t"} instead of
wenzelm@27040
   308
  @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
wenzelm@27040
   309
  unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
wenzelm@51585
   310
wenzelm@51585
   311
  \item @{command "print_defn_rules"} prints the definitional rewrite rules
wenzelm@51585
   312
  declared via @{attribute defn} in the current context.
wenzelm@51585
   313
wenzelm@28760
   314
  \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
wenzelm@28760
   315
  syntactic constant which is associated with a certain term according
wenzelm@28760
   316
  to the meta-level equality @{text eq}.
wenzelm@27040
   317
  
wenzelm@27040
   318
  Abbreviations participate in the usual type-inference process, but
wenzelm@27040
   319
  are expanded before the logic ever sees them.  Pretty printing of
wenzelm@27040
   320
  terms involves higher-order rewriting with rules stemming from
wenzelm@27040
   321
  reverted abbreviations.  This needs some care to avoid overlapping
wenzelm@27040
   322
  or looping syntactic replacements!
wenzelm@27040
   323
  
wenzelm@27040
   324
  The optional @{text mode} specification restricts output to a
wenzelm@27040
   325
  particular print mode; using ``@{text input}'' here achieves the
wenzelm@27040
   326
  effect of one-way abbreviations.  The mode may also include an
wenzelm@27040
   327
  ``@{keyword "output"}'' qualifier that affects the concrete syntax
wenzelm@27040
   328
  declared for abbreviations, cf.\ @{command "syntax"} in
wenzelm@27040
   329
  \secref{sec:syn-trans}.
wenzelm@27040
   330
  
wenzelm@28760
   331
  \item @{command "print_abbrevs"} prints all constant abbreviations
wenzelm@27040
   332
  of the current context.
wenzelm@27040
   333
  
wenzelm@28760
   334
  \end{description}
wenzelm@58618
   335
\<close>
wenzelm@27040
   336
wenzelm@27040
   337
wenzelm@58618
   338
section \<open>Axiomatizations \label{sec:axiomatizations}\<close>
wenzelm@57487
   339
wenzelm@58618
   340
text \<open>
wenzelm@57487
   341
  \begin{matharray}{rcll}
wenzelm@57487
   342
    @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
wenzelm@57487
   343
  \end{matharray}
wenzelm@57487
   344
wenzelm@57487
   345
  @{rail \<open>
wenzelm@57487
   346
    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
wenzelm@57487
   347
    ;
wenzelm@57487
   348
    specs: (@{syntax thmdecl}? @{syntax props} + @'and')
wenzelm@57487
   349
  \<close>}
wenzelm@57487
   350
wenzelm@57487
   351
  \begin{description}
wenzelm@57487
   352
wenzelm@57487
   353
  \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
wenzelm@57487
   354
  introduces several constants simultaneously and states axiomatic
wenzelm@57487
   355
  properties for these. The constants are marked as being specified once and
wenzelm@57487
   356
  for all, which prevents additional specifications for the same constants
wenzelm@57487
   357
  later on, but it is always possible do emit axiomatizations without
wenzelm@57487
   358
  referring to particular constants. Note that lack of precise dependency
wenzelm@57487
   359
  tracking of axiomatizations may disrupt the well-formedness of an
wenzelm@57487
   360
  otherwise definitional theory.
wenzelm@57487
   361
wenzelm@57487
   362
  Axiomatization is restricted to a global theory context: support for local
wenzelm@57487
   363
  theory targets \secref{sec:target} would introduce an extra dimension of
wenzelm@57487
   364
  uncertainty what the written specifications really are, and make it
wenzelm@57487
   365
  infeasible to argue why they are correct.
wenzelm@57487
   366
wenzelm@57487
   367
  Axiomatic specifications are required when declaring a new logical system
wenzelm@57487
   368
  within Isabelle/Pure, but in an application environment like Isabelle/HOL
wenzelm@57487
   369
  the user normally stays within definitional mechanisms provided by the
wenzelm@57487
   370
  logic and its libraries.
wenzelm@57487
   371
wenzelm@57487
   372
  \end{description}
wenzelm@58618
   373
\<close>
wenzelm@57487
   374
wenzelm@57487
   375
wenzelm@58618
   376
section \<open>Generic declarations\<close>
wenzelm@27040
   377
wenzelm@58618
   378
text \<open>
wenzelm@47483
   379
  \begin{matharray}{rcl}
wenzelm@47483
   380
    @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@47483
   381
    @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@47483
   382
    @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@47483
   383
  \end{matharray}
wenzelm@47483
   384
wenzelm@27040
   385
  Arbitrary operations on the background context may be wrapped-up as
wenzelm@27040
   386
  generic declaration elements.  Since the underlying concept of local
wenzelm@27040
   387
  theories may be subject to later re-interpretation, there is an
wenzelm@27040
   388
  additional dependency on a morphism that tells the difference of the
wenzelm@27040
   389
  original declaration context wrt.\ the application context
wenzelm@27040
   390
  encountered later on.  A fact declaration is an important special
wenzelm@27040
   391
  case: it consists of a theorem which is applied to the context by
wenzelm@27040
   392
  means of an attribute.
wenzelm@27040
   393
wenzelm@55112
   394
  @{rail \<open>
wenzelm@42596
   395
    (@@{command declaration} | @@{command syntax_declaration})
wenzelm@59783
   396
      ('(' @'pervasive' ')')? \<newline> @{syntax text}
wenzelm@27040
   397
    ;
wenzelm@59783
   398
    @@{command declare} (@{syntax thmrefs} + @'and')
wenzelm@55112
   399
  \<close>}
wenzelm@27040
   400
wenzelm@28760
   401
  \begin{description}
wenzelm@27040
   402
wenzelm@28760
   403
  \item @{command "declaration"}~@{text d} adds the declaration
wenzelm@27040
   404
  function @{text d} of ML type @{ML_type declaration}, to the current
wenzelm@27040
   405
  local theory under construction.  In later application contexts, the
wenzelm@27040
   406
  function is transformed according to the morphisms being involved in
wenzelm@27040
   407
  the interpretation hierarchy.
wenzelm@27040
   408
wenzelm@33516
   409
  If the @{text "(pervasive)"} option is given, the corresponding
wenzelm@33516
   410
  declaration is applied to all possible contexts involved, including
wenzelm@33516
   411
  the global background theory.
wenzelm@33516
   412
wenzelm@40784
   413
  \item @{command "syntax_declaration"} is similar to @{command
wenzelm@40784
   414
  "declaration"}, but is meant to affect only ``syntactic'' tools by
wenzelm@40784
   415
  convention (such as notation and type-checking information).
wenzelm@40784
   416
wenzelm@28760
   417
  \item @{command "declare"}~@{text thms} declares theorems to the
wenzelm@27040
   418
  current local theory context.  No theorem binding is involved here,
wenzelm@27040
   419
  unlike @{command "theorems"} or @{command "lemmas"} (cf.\
wenzelm@51313
   420
  \secref{sec:theorems}), so @{command "declare"} only has the effect
wenzelm@27040
   421
  of applying attributes as included in the theorem specification.
wenzelm@27040
   422
wenzelm@28760
   423
  \end{description}
wenzelm@58618
   424
\<close>
wenzelm@27040
   425
wenzelm@27040
   426
wenzelm@58618
   427
section \<open>Locales \label{sec:locale}\<close>
wenzelm@27040
   428
wenzelm@58618
   429
text \<open>
ballarin@54049
   430
  A locale is a functor that maps parameters (including implicit type
ballarin@54049
   431
  parameters) and a specification to a list of declarations.  The
ballarin@54049
   432
  syntax of locales is modeled after the Isar proof context commands
ballarin@54049
   433
  (cf.\ \secref{sec:proof-context}).
ballarin@54049
   434
ballarin@54049
   435
  Locale hierarchies are supported by maintaining a graph of
ballarin@54049
   436
  dependencies between locale instances in the global theory.
ballarin@54049
   437
  Dependencies may be introduced through import (where a locale is
ballarin@54049
   438
  defined as sublocale of the imported instances) or by proving that
ballarin@54049
   439
  an existing locale is a sublocale of one or several locale
ballarin@54049
   440
  instances.
ballarin@54049
   441
ballarin@54049
   442
  A locale may be opened with the purpose of appending to its list of
ballarin@54049
   443
  declarations (cf.\ \secref{sec:target}).  When opening a locale
ballarin@54049
   444
  declarations from all dependencies are collected and are presented
ballarin@54049
   445
  as a local theory.  In this process, which is called \emph{roundup},
ballarin@54049
   446
  redundant locale instances are omitted.  A locale instance is
ballarin@54049
   447
  redundant if it is subsumed by an instance encountered earlier.  A
ballarin@54049
   448
  more detailed description of this process is available elsewhere
wenzelm@58552
   449
  @{cite Ballarin2014}.
wenzelm@58618
   450
\<close>
wenzelm@27040
   451
wenzelm@27040
   452
wenzelm@58618
   453
subsection \<open>Locale expressions \label{sec:locale-expr}\<close>
ballarin@33846
   454
wenzelm@58618
   455
text \<open>
ballarin@54049
   456
  A \emph{locale expression} denotes a context composed of instances
ballarin@54049
   457
  of existing locales.  The context consists of the declaration
ballarin@54049
   458
  elements from the locale instances.  Redundant locale instances are
ballarin@54049
   459
  omitted according to roundup.
ballarin@33846
   460
wenzelm@55112
   461
  @{rail \<open>
wenzelm@59785
   462
    @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
ballarin@33846
   463
    ;
wenzelm@42617
   464
    instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
ballarin@33846
   465
    ;
wenzelm@42596
   466
    qualifier: @{syntax name} ('?' | '!')?
ballarin@33846
   467
    ;
wenzelm@42617
   468
    pos_insts: ('_' | @{syntax term})*
ballarin@33846
   469
    ;
wenzelm@42617
   470
    named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
wenzelm@55112
   471
  \<close>}
ballarin@33846
   472
ballarin@33846
   473
  A locale instance consists of a reference to a locale and either
ballarin@33846
   474
  positional or named parameter instantiations.  Identical
ballarin@54049
   475
  instantiations (that is, those that instantiate a parameter by itself)
wenzelm@40256
   476
  may be omitted.  The notation `@{text "_"}' enables to omit the
wenzelm@40256
   477
  instantiation for a parameter inside a positional instantiation.
ballarin@33846
   478
ballarin@33846
   479
  Terms in instantiations are from the context the locale expressions
ballarin@33846
   480
  is declared in.  Local names may be added to this context with the
ballarin@48824
   481
  optional @{keyword "for"} clause.  This is useful for shadowing names
ballarin@48824
   482
  bound in outer contexts, and for declaring syntax.  In addition,
ballarin@48824
   483
  syntax declarations from one instance are effective when parsing
ballarin@48824
   484
  subsequent instances of the same expression.
ballarin@33846
   485
ballarin@33846
   486
  Instances have an optional qualifier which applies to names in
ballarin@33846
   487
  declarations.  Names include local definitions and theorem names.
ballarin@33846
   488
  If present, the qualifier itself is either optional
ballarin@33846
   489
  (``\texttt{?}''), which means that it may be omitted on input of the
ballarin@33846
   490
  qualified name, or mandatory (``\texttt{!}'').  If neither
ballarin@33846
   491
  ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
ballarin@33846
   492
  is used.  For @{command "interpretation"} and @{command "interpret"}
ballarin@33846
   493
  the default is ``mandatory'', for @{command "locale"} and @{command
ballarin@54049
   494
  "sublocale"} the default is ``optional''.  Qualifiers play no role
ballarin@54049
   495
  in determining whether one locale instance subsumes another.
wenzelm@58618
   496
\<close>
ballarin@33846
   497
ballarin@33846
   498
wenzelm@58618
   499
subsection \<open>Locale declarations\<close>
wenzelm@27040
   500
wenzelm@58618
   501
text \<open>
wenzelm@27040
   502
  \begin{matharray}{rcl}
wenzelm@28761
   503
    @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
wenzelm@28761
   504
    @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
wenzelm@28761
   505
    @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
wenzelm@50716
   506
    @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
wenzelm@28761
   507
    @{method_def intro_locales} & : & @{text method} \\
wenzelm@28761
   508
    @{method_def unfold_locales} & : & @{text method} \\
wenzelm@27040
   509
  \end{matharray}
wenzelm@27040
   510
wenzelm@27040
   511
  \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
wenzelm@28787
   512
  \indexisarelem{defines}\indexisarelem{notes}
wenzelm@55112
   513
  @{rail \<open>
wenzelm@42596
   514
    @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
wenzelm@27040
   515
    ;
wenzelm@42596
   516
    @@{command print_locale} '!'? @{syntax nameref}
wenzelm@27040
   517
    ;
wenzelm@42617
   518
    @{syntax_def locale}: @{syntax context_elem}+ |
wenzelm@42617
   519
      @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
wenzelm@27040
   520
    ;
wenzelm@42617
   521
    @{syntax_def context_elem}:
wenzelm@59785
   522
      @'fixes' @{syntax "fixes"} |
wenzelm@42596
   523
      @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
wenzelm@42596
   524
      @'assumes' (@{syntax props} + @'and') |
wenzelm@42705
   525
      @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
wenzelm@42596
   526
      @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
wenzelm@55112
   527
  \<close>}
wenzelm@27040
   528
wenzelm@28760
   529
  \begin{description}
wenzelm@27040
   530
  
wenzelm@28760
   531
  \item @{command "locale"}~@{text "loc = import + body"} defines a
wenzelm@27040
   532
  new locale @{text loc} as a context consisting of a certain view of
wenzelm@27040
   533
  existing locales (@{text import}) plus some additional elements
wenzelm@27040
   534
  (@{text body}).  Both @{text import} and @{text body} are optional;
wenzelm@27040
   535
  the degenerate form @{command "locale"}~@{text loc} defines an empty
wenzelm@27040
   536
  locale, which may still be useful to collect declarations of facts
wenzelm@27040
   537
  later on.  Type-inference on locale expressions automatically takes
wenzelm@27040
   538
  care of the most general typing that the combined context elements
wenzelm@27040
   539
  may acquire.
wenzelm@27040
   540
ballarin@54049
   541
  The @{text import} consists of a locale expression; see
ballarin@54049
   542
  \secref{sec:proof-context} above.  Its @{keyword "for"} clause defines
ballarin@54049
   543
  the parameters of @{text import}.  These are parameters of
ballarin@54049
   544
  the defined locale.  Locale parameters whose instantiation is
ballarin@54049
   545
  omitted automatically extend the (possibly empty) @{keyword "for"}
ballarin@54049
   546
  clause: they are inserted at its beginning.  This means that these
ballarin@54049
   547
  parameters may be referred to from within the expression and also in
ballarin@54049
   548
  the subsequent context elements and provides a notational
ballarin@54049
   549
  convenience for the inheritance of parameters in locale
ballarin@33846
   550
  declarations.
wenzelm@27040
   551
ballarin@33846
   552
  The @{text body} consists of context elements.
wenzelm@27040
   553
wenzelm@28760
   554
  \begin{description}
wenzelm@27040
   555
wenzelm@28760
   556
  \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
wenzelm@27040
   557
  parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
wenzelm@27040
   558
  are optional).  The special syntax declaration ``@{text
wenzelm@51657
   559
  "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may
wenzelm@51657
   560
  be referenced implicitly in this context.
wenzelm@27040
   561
wenzelm@28760
   562
  \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
ballarin@33846
   563
  constraint @{text \<tau>} on the local parameter @{text x}.  This
ballarin@38110
   564
  element is deprecated.  The type constraint should be introduced in
ballarin@54049
   565
  the @{keyword "for"} clause or the relevant @{element "fixes"} element.
wenzelm@27040
   566
wenzelm@28760
   567
  \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
wenzelm@27040
   568
  introduces local premises, similar to @{command "assume"} within a
wenzelm@27040
   569
  proof (cf.\ \secref{sec:proof-context}).
wenzelm@27040
   570
wenzelm@28760
   571
  \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
wenzelm@27040
   572
  declared parameter.  This is similar to @{command "def"} within a
wenzelm@27040
   573
  proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
wenzelm@27040
   574
  takes an equational proposition instead of variable-term pair.  The
wenzelm@27040
   575
  left-hand side of the equation may have additional arguments, e.g.\
wenzelm@27040
   576
  ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
wenzelm@27040
   577
wenzelm@28760
   578
  \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
wenzelm@27040
   579
  reconsiders facts within a local context.  Most notably, this may
wenzelm@27040
   580
  include arbitrary declarations in any attribute specifications
wenzelm@27040
   581
  included here, e.g.\ a local @{attribute simp} rule.
wenzelm@27040
   582
ballarin@54049
   583
  \end{description}
wenzelm@27040
   584
ballarin@54049
   585
  Both @{element "assumes"} and @{element "defines"} elements
ballarin@54049
   586
  contribute to the locale specification.  When defining an operation
ballarin@54049
   587
  derived from the parameters, @{command "definition"}
wenzelm@57487
   588
  (\secref{sec:term-definitions}) is usually more appropriate.
wenzelm@27040
   589
  
wenzelm@27040
   590
  Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
wenzelm@27040
   591
  in the syntax of @{element "assumes"} and @{element "defines"} above
wenzelm@27040
   592
  are illegal in locale definitions.  In the long goal format of
wenzelm@27040
   593
  \secref{sec:goals}, term bindings may be included as expected,
wenzelm@27040
   594
  though.
wenzelm@27040
   595
  
ballarin@33846
   596
  \medskip Locale specifications are ``closed up'' by
wenzelm@27040
   597
  turning the given text into a predicate definition @{text
wenzelm@27040
   598
  loc_axioms} and deriving the original assumptions as local lemmas
wenzelm@27040
   599
  (modulo local definitions).  The predicate statement covers only the
wenzelm@27040
   600
  newly specified assumptions, omitting the content of included locale
wenzelm@27040
   601
  expressions.  The full cumulative view is only provided on export,
wenzelm@27040
   602
  involving another predicate @{text loc} that refers to the complete
wenzelm@27040
   603
  specification text.
wenzelm@27040
   604
  
wenzelm@27040
   605
  In any case, the predicate arguments are those locale parameters
ballarin@54049
   606
  that actually occur in the respective piece of text.  Also these
ballarin@54049
   607
  predicates operate at the meta-level in theory, but the locale
wenzelm@27040
   608
  packages attempts to internalize statements according to the
wenzelm@27040
   609
  object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
wenzelm@27040
   610
  @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
wenzelm@27040
   611
  \secref{sec:object-logic}).  Separate introduction rules @{text
wenzelm@27040
   612
  loc_axioms.intro} and @{text loc.intro} are provided as well.
wenzelm@27040
   613
  
ballarin@33867
   614
  \item @{command "print_locale"}~@{text "locale"} prints the
ballarin@33867
   615
  contents of the named locale.  The command omits @{element "notes"}
ballarin@33867
   616
  elements by default.  Use @{command "print_locale"}@{text "!"} to
ballarin@33867
   617
  have them included.
wenzelm@27040
   618
wenzelm@28760
   619
  \item @{command "print_locales"} prints the names of all locales
wenzelm@27040
   620
  of the current theory.
wenzelm@27040
   621
wenzelm@50716
   622
  \item @{command "locale_deps"} visualizes all locales and their
wenzelm@50716
   623
  relations as a Hasse diagram. This includes locales defined as type
ballarin@54049
   624
  classes (\secref{sec:class}).  See also @{command
ballarin@54049
   625
  "print_dependencies"} below.
wenzelm@50716
   626
wenzelm@28760
   627
  \item @{method intro_locales} and @{method unfold_locales}
wenzelm@27040
   628
  repeatedly expand all introduction rules of locale predicates of the
wenzelm@27040
   629
  theory.  While @{method intro_locales} only applies the @{text
ballarin@54049
   630
  loc.intro} introduction rules and therefore does not descend to
wenzelm@27040
   631
  assumptions, @{method unfold_locales} is more aggressive and applies
wenzelm@27040
   632
  @{text loc_axioms.intro} as well.  Both methods are aware of locale
wenzelm@28787
   633
  specifications entailed by the context, both from target statements,
wenzelm@28787
   634
  and from interpretations (see below).  New goals that are entailed
wenzelm@28787
   635
  by the current context are discharged automatically.
wenzelm@27040
   636
wenzelm@28760
   637
  \end{description}
wenzelm@58618
   638
\<close>
wenzelm@27040
   639
wenzelm@27040
   640
wenzelm@58618
   641
subsection \<open>Locale interpretation\<close>
wenzelm@27040
   642
wenzelm@58618
   643
text \<open>
wenzelm@27040
   644
  \begin{matharray}{rcl}
ballarin@53368
   645
    @{command_def "interpretation"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\
ballarin@33846
   646
    @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
ballarin@53368
   647
    @{command_def "sublocale"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\
ballarin@41435
   648
    @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
ballarin@33846
   649
    @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
wenzelm@27040
   650
  \end{matharray}
wenzelm@27040
   651
ballarin@54049
   652
  Locales may be instantiated, and the resulting instantiated
ballarin@54049
   653
  declarations added to the current context.  This requires proof (of
ballarin@54049
   654
  the instantiated specification) and is called \emph{locale
ballarin@54049
   655
  interpretation}.  Interpretation is possible in locales (@{command
ballarin@54049
   656
  "sublocale"}), global and local theories (@{command
ballarin@54049
   657
  "interpretation"}) and also within proof bodies (@{command
ballarin@48824
   658
  "interpret"}).
wenzelm@47483
   659
wenzelm@55112
   660
  @{rail \<open>
ballarin@53368
   661
    @@{command interpretation} @{syntax locale_expr} equations?
wenzelm@27040
   662
    ;
wenzelm@42617
   663
    @@{command interpret} @{syntax locale_expr} equations?
wenzelm@27040
   664
    ;
wenzelm@55029
   665
    @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
wenzelm@42704
   666
      equations?
ballarin@33846
   667
    ;
wenzelm@42617
   668
    @@{command print_dependencies} '!'? @{syntax locale_expr}
wenzelm@27040
   669
    ;
wenzelm@42596
   670
    @@{command print_interps} @{syntax nameref}
ballarin@41434
   671
    ;
wenzelm@42596
   672
wenzelm@42596
   673
    equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
wenzelm@55112
   674
  \<close>}
wenzelm@27040
   675
wenzelm@28760
   676
  \begin{description}
wenzelm@27040
   677
ballarin@33867
   678
  \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
ballarin@54049
   679
  interprets @{text expr} in a global or local theory.  The command
ballarin@54049
   680
  generates proof obligations for the instantiated specifications.
ballarin@54049
   681
  Once these are discharged by the user, instantiated declarations (in
ballarin@54049
   682
  particular, facts) are added to the theory in a post-processing
ballarin@54049
   683
  phase.
ballarin@53368
   684
ballarin@54049
   685
  The command is aware of interpretations that are already active.
ballarin@54049
   686
  Post-processing is achieved through a variant of roundup that takes
ballarin@54049
   687
  the interpretations of the current global or local theory into
ballarin@54049
   688
  account.  In order to simplify the proof obligations according to
ballarin@54049
   689
  existing interpretations use methods @{method intro_locales} or
ballarin@54049
   690
  @{method unfold_locales}.
ballarin@53368
   691
ballarin@53369
   692
  When adding declarations to locales, interpreted versions of these
ballarin@53369
   693
  declarations are added to the global theory for all interpretations
ballarin@53369
   694
  in the global theory as well. That is, interpretations in global
ballarin@53369
   695
  theories dynamically participate in any declarations added to
ballarin@54049
   696
  locales.
ballarin@54049
   697
ballarin@54049
   698
  In contrast, the lifetime of an interpretation in a local theory is
ballarin@54049
   699
  limited to the current context block.  At the closing @{command end}
ballarin@54049
   700
  of the block the interpretation and its declarations disappear.
ballarin@54049
   701
  This enables establishing facts based on interpretations without
ballarin@54049
   702
  creating permanent links to the interpreted locale instances, as
ballarin@54049
   703
  would be the case with @{command sublocale}.
ballarin@54049
   704
  While @{command "interpretation"}~@{text "(\<IN> c)
ballarin@54049
   705
  \<dots>"} is technically possible, it is not useful since its result is
ballarin@54049
   706
  discarded immediately.
ballarin@33846
   707
ballarin@48824
   708
  Free variables in the interpreted expression are allowed.  They are
ballarin@48824
   709
  turned into schematic variables in the generated declarations.  In
ballarin@48824
   710
  order to use a free variable whose name is already bound in the
ballarin@48824
   711
  context --- for example, because a constant of that name exists ---
ballarin@54049
   712
  add it to the @{keyword "for"} clause.
ballarin@48824
   713
ballarin@53370
   714
  The equations @{text eqns} yield \emph{rewrite morphisms}, which are
ballarin@53370
   715
  unfolded during post-processing and are useful for interpreting
ballarin@53370
   716
  concepts introduced through definitions.  The equations must be
ballarin@53370
   717
  proved.
wenzelm@27040
   718
ballarin@38110
   719
  \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
ballarin@38110
   720
  @{text expr} in the proof context and is otherwise similar to
ballarin@53370
   721
  interpretation in local theories.  Note that for @{command
ballarin@53370
   722
  "interpret"} the @{text eqns} should be
ballarin@41434
   723
  explicitly universally quantified.
ballarin@41434
   724
ballarin@41434
   725
  \item @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
ballarin@41434
   726
  eqns"}
ballarin@41434
   727
  interprets @{text expr} in the locale @{text name}.  A proof that
ballarin@41434
   728
  the specification of @{text name} implies the specification of
ballarin@41434
   729
  @{text expr} is required.  As in the localized version of the
ballarin@41434
   730
  theorem command, the proof is in the context of @{text name}.  After
ballarin@53370
   731
  the proof obligation has been discharged, the locale hierarchy is
ballarin@53370
   732
  changed as if @{text name} imported @{text expr} (hence the name
ballarin@53370
   733
  @{command "sublocale"}).  When the context of @{text name} is
ballarin@54049
   734
  subsequently entered, traversing the locale hierarchy will involve
ballarin@53370
   735
  the locale instances of @{text expr}, and their declarations will be
ballarin@53370
   736
  added to the context.  This makes @{command "sublocale"}
ballarin@53370
   737
  dynamic: extensions of a locale that is instantiated in @{text expr}
ballarin@53370
   738
  may take place after the @{command "sublocale"} declaration and
ballarin@53370
   739
  still become available in the context.  Circular @{command
ballarin@53370
   740
  "sublocale"} declarations are allowed as long as they do not lead to
ballarin@54049
   741
  infinite chains.
ballarin@41434
   742
ballarin@53368
   743
  If interpretations of @{text name} exist in the current global
ballarin@53368
   744
  theory, the command adds interpretations for @{text expr} as well,
ballarin@53368
   745
  with the same qualifier, although only for fragments of @{text expr}
ballarin@53368
   746
  that are not interpreted in the theory already.
ballarin@41434
   747
ballarin@53370
   748
  The equations @{text eqns} amend the morphism through
ballarin@53370
   749
  which @{text expr} is interpreted.  This enables mapping definitions
ballarin@53370
   750
  from the interpreted locales to entities of @{text name} and can
ballarin@54049
   751
  help break infinite chains induced by circular @{command
ballarin@54049
   752
  "sublocale"} declarations.
wenzelm@27040
   753
ballarin@53368
   754
  In a named context block the @{command sublocale} command may also
ballarin@53368
   755
  be used, but the locale argument must be omitted.  The command then
ballarin@53368
   756
  refers to the locale (or class) target of the context block.
haftmann@51747
   757
ballarin@41435
   758
  \item @{command "print_dependencies"}~@{text "expr"} is useful for
ballarin@54049
   759
  understanding the effect of an interpretation of @{text "expr"} in
ballarin@54049
   760
  the current context.  It lists all locale instances for which
ballarin@54049
   761
  interpretations would be added to the current context.  Variant
ballarin@54049
   762
  @{command "print_dependencies"}@{text "!"} does not generalize
ballarin@54049
   763
  parameters and assumes an empty context --- that is, it prints all
ballarin@54049
   764
  locale instances that would be considered for interpretation.  The
ballarin@54049
   765
  latter is useful for understanding the dependencies of a locale
ballarin@54049
   766
  expression.
ballarin@41435
   767
ballarin@33867
   768
  \item @{command "print_interps"}~@{text "locale"} lists all
ballarin@38110
   769
  interpretations of @{text "locale"} in the current theory or proof
ballarin@51565
   770
  context, including those due to a combination of an @{command
ballarin@38110
   771
  "interpretation"} or @{command "interpret"} and one or several
ballarin@38110
   772
  @{command "sublocale"} declarations.
ballarin@33867
   773
wenzelm@28760
   774
  \end{description}
wenzelm@27040
   775
wenzelm@27040
   776
  \begin{warn}
ballarin@54049
   777
    If a global theory inherits declarations (body elements) for a
ballarin@54049
   778
    locale from one parent and an interpretation of that locale from
ballarin@54049
   779
    another parent, the interpretation will not be applied to the
ballarin@54049
   780
    declarations.
ballarin@54049
   781
  \end{warn}
ballarin@54049
   782
ballarin@54049
   783
  \begin{warn}
wenzelm@27040
   784
    Since attributes are applied to interpreted theorems,
wenzelm@27040
   785
    interpretation may modify the context of common proof tools, e.g.\
ballarin@33867
   786
    the Simplifier or Classical Reasoner.  As the behavior of such
ballarin@33867
   787
    tools is \emph{not} stable under interpretation morphisms, manual
ballarin@33867
   788
    declarations might have to be added to the target context of the
ballarin@33867
   789
    interpretation to revert such declarations.
wenzelm@27040
   790
  \end{warn}
wenzelm@27040
   791
wenzelm@27040
   792
  \begin{warn}
haftmann@51747
   793
    An interpretation in a local theory or proof context may subsume previous
wenzelm@27040
   794
    interpretations.  This happens if the same specification fragment
wenzelm@27040
   795
    is interpreted twice and the instantiation of the second
wenzelm@27040
   796
    interpretation is more general than the interpretation of the
ballarin@33846
   797
    first.  The locale package does not attempt to remove subsumed
ballarin@33846
   798
    interpretations.
wenzelm@27040
   799
  \end{warn}
wenzelm@58618
   800
\<close>
wenzelm@27040
   801
wenzelm@27040
   802
haftmann@59003
   803
subsubsection \<open>Permanent locale interpretation\<close>
haftmann@59003
   804
haftmann@59003
   805
text \<open>
haftmann@59003
   806
  Permanent locale interpretation is a library extension on top
haftmann@59003
   807
  of @{command "interpretation"} and @{command "sublocale"}.  It is
haftmann@59003
   808
  available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}
haftmann@59003
   809
  and provides
haftmann@59003
   810
  \begin{enumerate}
haftmann@59003
   811
    \item a unified view on arbitrary suitable local theories as interpretation target; 
haftmann@59320
   812
    \item rewrite morphisms by means of \emph{rewrite definitions}. 
haftmann@59003
   813
  \end{enumerate}
haftmann@59003
   814
  
haftmann@59003
   815
  \begin{matharray}{rcl}
haftmann@59003
   816
    @{command_def "permanent_interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
haftmann@59003
   817
  \end{matharray}
haftmann@59003
   818
haftmann@59003
   819
  @{rail \<open>
haftmann@59003
   820
    @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
haftmann@59003
   821
      definitions? equations?
haftmann@59003
   822
    ;
haftmann@59003
   823
haftmann@59003
   824
    definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
haftmann@59003
   825
      @{syntax mixfix}? @'=' @{syntax term} + @'and');
haftmann@59003
   826
    equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
haftmann@59003
   827
  \<close>}
haftmann@59003
   828
haftmann@59003
   829
  \begin{description}
haftmann@59003
   830
haftmann@59003
   831
  \item @{command "permanent_interpretation"}~@{text "expr \<DEFINING> defs \<WHERE> eqns"}
haftmann@59003
   832
  interprets @{text expr} in the current local theory.  The command
haftmann@59003
   833
  generates proof obligations for the instantiated specifications.
haftmann@59003
   834
  Instantiated declarations (in particular, facts) are added to the
haftmann@59003
   835
  local theory's underlying target in a post-processing phase.  When
haftmann@59003
   836
  adding declarations to locales, interpreted versions of these
haftmann@59003
   837
  declarations are added to any target for all interpretations
haftmann@59003
   838
  in that target as well. That is, permanent interpretations
haftmann@59003
   839
  dynamically participate in any declarations added to
haftmann@59003
   840
  locales.
haftmann@59003
   841
  
haftmann@59003
   842
  The local theory's underlying target must explicitly support
haftmann@59003
   843
  permanent interpretations.  Prominent examples are global theories
haftmann@59003
   844
  (where @{command "permanent_interpretation"} is technically
haftmann@59003
   845
  corresponding to @{command "interpretation"}) and locales
haftmann@59003
   846
  (where @{command "permanent_interpretation"} is technically
haftmann@59003
   847
  corresponding to @{command "sublocale"}).  Unnamed contexts
haftmann@59320
   848
  (see \secref{sec:target}) are not admissible since they are
haftmann@59003
   849
  non-permanent due to their very nature.  
haftmann@59003
   850
haftmann@59003
   851
  In additions to \emph{rewrite morphisms} specified by @{text eqns},
haftmann@59320
   852
  also \emph{rewrite definitions} may be specified.  Semantically, a
haftmann@59320
   853
  rewrite definition
haftmann@59320
   854
  
haftmann@59320
   855
  \begin{itemize}
haftmann@59320
   856
  
haftmann@59320
   857
    \item produces a corresponding definition in
haftmann@59320
   858
      the local theory's underlying target \emph{and}
haftmann@59320
   859
    
haftmann@59320
   860
    \item augments the rewrite morphism with the equation
haftmann@59320
   861
      stemming from the symmetric of the corresponding definition.
haftmann@59003
   862
  
haftmann@59320
   863
  \end{itemize}
haftmann@59003
   864
  
haftmann@59320
   865
  This is technically different to to a naive combination
haftmann@59320
   866
  of a conventional definition and an explicit rewrite equation:
haftmann@59003
   867
  
haftmann@59320
   868
  \begin{itemize}
haftmann@59003
   869
  
haftmann@59320
   870
    \item Definitions are parsed in the syntactic interpretation
haftmann@59320
   871
      context, just like equations.
haftmann@59320
   872
  
haftmann@59320
   873
    \item The proof needs not consider the equations stemming from
haftmann@59003
   874
      definitions -- they are proved implicitly by construction.
haftmann@59003
   875
      
haftmann@59320
   876
  \end{itemize}
haftmann@59003
   877
  
haftmann@59320
   878
  Rewrite definitions yield a pattern for introducing new explicit
haftmann@59003
   879
  operations for existing terms after interpretation.
haftmann@59003
   880
  
haftmann@59003
   881
  \end{description}
haftmann@59003
   882
\<close>
haftmann@59003
   883
haftmann@59003
   884
wenzelm@58618
   885
section \<open>Classes \label{sec:class}\<close>
wenzelm@27040
   886
wenzelm@58618
   887
text \<open>
wenzelm@27040
   888
  \begin{matharray}{rcl}
wenzelm@28761
   889
    @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
wenzelm@28761
   890
    @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
wenzelm@28761
   891
    @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@42626
   892
    @{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
wenzelm@28761
   893
    @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761
   894
    @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
haftmann@29706
   895
    @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
wenzelm@28761
   896
    @{method_def intro_classes} & : & @{text method} \\
wenzelm@27040
   897
  \end{matharray}
wenzelm@27040
   898
wenzelm@47483
   899
  A class is a particular locale with \emph{exactly one} type variable
wenzelm@47483
   900
  @{text \<alpha>}.  Beyond the underlying locale, a corresponding type class
wenzelm@47483
   901
  is established which is interpreted logically as axiomatic type
wenzelm@58552
   902
  class @{cite "Wenzel:1997:TPHOL"} whose logical content are the
wenzelm@47483
   903
  assumptions of the locale.  Thus, classes provide the full
wenzelm@47483
   904
  generality of locales combined with the commodity of type classes
wenzelm@58552
   905
  (notably type-inference).  See @{cite "isabelle-classes"} for a short
wenzelm@47483
   906
  tutorial.
wenzelm@47483
   907
wenzelm@55112
   908
  @{rail \<open>
wenzelm@42704
   909
    @@{command class} class_spec @'begin'?
wenzelm@42704
   910
    ;
wenzelm@42704
   911
    class_spec: @{syntax name} '='
wenzelm@42617
   912
      ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
wenzelm@42704
   913
        @{syntax nameref} | (@{syntax context_elem}+))      
wenzelm@27040
   914
    ;
wenzelm@42596
   915
    @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
wenzelm@27040
   916
    ;
wenzelm@42704
   917
    @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
wenzelm@42704
   918
      @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
haftmann@31681
   919
    ;
wenzelm@59783
   920
    @@{command subclass} @{syntax nameref}
haftmann@58202
   921
    ;
haftmann@59422
   922
    @@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
haftmann@59422
   923
      ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
wenzelm@55112
   924
  \<close>}
wenzelm@27040
   925
wenzelm@28760
   926
  \begin{description}
wenzelm@27040
   927
wenzelm@28760
   928
  \item @{command "class"}~@{text "c = superclasses + body"} defines
wenzelm@27040
   929
  a new class @{text c}, inheriting from @{text superclasses}.  This
wenzelm@27040
   930
  introduces a locale @{text c} with import of all locales @{text
wenzelm@27040
   931
  superclasses}.
wenzelm@27040
   932
wenzelm@27040
   933
  Any @{element "fixes"} in @{text body} are lifted to the global
wenzelm@27040
   934
  theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
wenzelm@27040
   935
  f\<^sub>n"} of class @{text c}), mapping the local type parameter
wenzelm@27040
   936
  @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
wenzelm@27040
   937
wenzelm@27040
   938
  Likewise, @{element "assumes"} in @{text body} are also lifted,
wenzelm@27040
   939
  mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
wenzelm@27040
   940
  corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}.  The
wenzelm@27040
   941
  corresponding introduction rule is provided as @{text
wenzelm@27040
   942
  c_class_axioms.intro}.  This rule should be rarely needed directly
wenzelm@27040
   943
  --- the @{method intro_classes} method takes care of the details of
wenzelm@27040
   944
  class membership proofs.
wenzelm@27040
   945
wenzelm@28768
   946
  \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
haftmann@51747
   947
  \<BEGIN>"} opens a target (cf.\ \secref{sec:target}) which
wenzelm@28760
   948
  allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
wenzelm@28760
   949
  to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
wenzelm@28760
   950
  \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}.  A plain @{command "instance"} command in the
wenzelm@28760
   951
  target body poses a goal stating these type arities.  The target is
wenzelm@28760
   952
  concluded by an @{command_ref (local) "end"} command.
wenzelm@27040
   953
wenzelm@27040
   954
  Note that a list of simultaneous type constructors may be given;
haftmann@31914
   955
  this corresponds nicely to mutually recursive type definitions, e.g.\
wenzelm@27040
   956
  in Isabelle/HOL.
wenzelm@27040
   957
wenzelm@28760
   958
  \item @{command "instance"} in an instantiation target body sets
wenzelm@27040
   959
  up a goal stating the type arities claimed at the opening @{command
wenzelm@27040
   960
  "instantiation"}.  The proof would usually proceed by @{method
wenzelm@27040
   961
  intro_classes}, and then establish the characteristic theorems of
wenzelm@27040
   962
  the type classes involved.  After finishing the proof, the
wenzelm@27040
   963
  background theory will be augmented by the proven type arities.
wenzelm@27040
   964
haftmann@31681
   965
  On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
haftmann@31681
   966
  s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
webertj@37112
   967
  need to specify operations: one can continue with the
haftmann@31681
   968
  instantiation proof immediately.
haftmann@31681
   969
wenzelm@28760
   970
  \item @{command "subclass"}~@{text c} in a class context for class
wenzelm@27040
   971
  @{text d} sets up a goal stating that class @{text c} is logically
wenzelm@27040
   972
  contained in class @{text d}.  After finishing the proof, class
wenzelm@27040
   973
  @{text d} is proven to be subclass @{text c} and the locale @{text
wenzelm@27040
   974
  c} is interpreted into @{text d} simultaneously.
wenzelm@27040
   975
wenzelm@56594
   976
  A weakened form of this is available through a further variant of
haftmann@31681
   977
  @{command instance}:  @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
wenzelm@53015
   978
  a proof that class @{text "c\<^sub>2"} implies @{text "c\<^sub>1"} without reference
haftmann@31681
   979
  to the underlying locales;  this is useful if the properties to prove
wenzelm@56594
   980
  the logical connection are not sufficient on the locale level but on
haftmann@31681
   981
  the theory level.
haftmann@31681
   982
wenzelm@28760
   983
  \item @{command "print_classes"} prints all classes in the current
wenzelm@27040
   984
  theory.
wenzelm@27040
   985
haftmann@29706
   986
  \item @{command "class_deps"} visualizes all classes and their
haftmann@59422
   987
  subclass relations as a Hasse diagram.  An optional first argument
haftmann@59422
   988
  constrains the set of classes to all subclasses of at least one given
haftmann@59422
   989
  sort, an optional second rgument to all superclasses of at least one given
haftmann@59422
   990
  sort.
haftmann@29706
   991
wenzelm@28760
   992
  \item @{method intro_classes} repeatedly expands all class
wenzelm@27040
   993
  introduction rules of this theory.  Note that this method usually
wenzelm@27040
   994
  needs not be named explicitly, as it is already included in the
wenzelm@27040
   995
  default proof step (e.g.\ of @{command "proof"}).  In particular,
wenzelm@27040
   996
  instantiation of trivial (syntactic) classes may be performed by a
wenzelm@27040
   997
  single ``@{command ".."}'' proof step.
wenzelm@26870
   998
wenzelm@28760
   999
  \end{description}
wenzelm@58618
  1000
\<close>
wenzelm@26870
  1001
wenzelm@27040
  1002
wenzelm@58618
  1003
subsection \<open>The class target\<close>
wenzelm@27040
  1004
wenzelm@58618
  1005
text \<open>
wenzelm@27040
  1006
  %FIXME check
wenzelm@27040
  1007
wenzelm@27040
  1008
  A named context may refer to a locale (cf.\ \secref{sec:target}).
wenzelm@27040
  1009
  If this locale is also a class @{text c}, apart from the common
wenzelm@27040
  1010
  locale target behaviour the following happens.
wenzelm@27040
  1011
wenzelm@27040
  1012
  \begin{itemize}
wenzelm@27040
  1013
wenzelm@27040
  1014
  \item Local constant declarations @{text "g[\<alpha>]"} referring to the
wenzelm@27040
  1015
  local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
wenzelm@27040
  1016
  are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
wenzelm@27040
  1017
  referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
wenzelm@27040
  1018
wenzelm@27040
  1019
  \item Local theorem bindings are lifted as are assumptions.
wenzelm@27040
  1020
wenzelm@27040
  1021
  \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
wenzelm@27040
  1022
  global operations @{text "g[?\<alpha> :: c]"} uniformly.  Type inference
wenzelm@27040
  1023
  resolves ambiguities.  In rare cases, manual type annotations are
wenzelm@27040
  1024
  needed.
wenzelm@27040
  1025
  
wenzelm@27040
  1026
  \end{itemize}
wenzelm@58618
  1027
\<close>
wenzelm@27040
  1028
wenzelm@27040
  1029
wenzelm@58618
  1030
subsection \<open>Co-regularity of type classes and arities\<close>
haftmann@37768
  1031
wenzelm@58618
  1032
text \<open>The class relation together with the collection of
haftmann@37768
  1033
  type-constructor arities must obey the principle of
haftmann@37768
  1034
  \emph{co-regularity} as defined below.
haftmann@37768
  1035
haftmann@37768
  1036
  \medskip For the subsequent formulation of co-regularity we assume
haftmann@37768
  1037
  that the class relation is closed by transitivity and reflexivity.
haftmann@37768
  1038
  Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
haftmann@37768
  1039
  completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
haftmann@37768
  1040
  implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
haftmann@37768
  1041
haftmann@37768
  1042
  Treating sorts as finite sets of classes (meaning the intersection),
haftmann@37768
  1043
  the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
haftmann@37768
  1044
  follows:
haftmann@37768
  1045
  \[
haftmann@37768
  1046
    @{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"}
haftmann@37768
  1047
  \]
haftmann@37768
  1048
haftmann@37768
  1049
  This relation on sorts is further extended to tuples of sorts (of
haftmann@37768
  1050
  the same length) in the component-wise way.
haftmann@37768
  1051
haftmann@37768
  1052
  \smallskip Co-regularity of the class relation together with the
haftmann@37768
  1053
  arities relation means:
haftmann@37768
  1054
  \[
haftmann@37768
  1055
    @{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"}
haftmann@37768
  1056
  \]
haftmann@37768
  1057
  \noindent for all such arities.  In other words, whenever the result
haftmann@37768
  1058
  classes of some type-constructor arities are related, then the
haftmann@37768
  1059
  argument sorts need to be related in the same way.
haftmann@37768
  1060
haftmann@37768
  1061
  \medskip Co-regularity is a very fundamental property of the
haftmann@37768
  1062
  order-sorted algebra of types.  For example, it entails principle
wenzelm@58552
  1063
  types and most general unifiers, e.g.\ see @{cite "nipkow-prehofer"}.
wenzelm@58618
  1064
\<close>
haftmann@37768
  1065
haftmann@37768
  1066
wenzelm@58618
  1067
section \<open>Unrestricted overloading\<close>
wenzelm@27040
  1068
wenzelm@58618
  1069
text \<open>
wenzelm@47483
  1070
  \begin{matharray}{rcl}
wenzelm@47483
  1071
    @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
wenzelm@47483
  1072
  \end{matharray}
wenzelm@47483
  1073
wenzelm@27040
  1074
  Isabelle/Pure's definitional schemes support certain forms of
haftmann@31047
  1075
  overloading (see \secref{sec:consts}).  Overloading means that a
haftmann@31047
  1076
  constant being declared as @{text "c :: \<alpha> decl"} may be
haftmann@31047
  1077
  defined separately on type instances
haftmann@31047
  1078
  @{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
wenzelm@56594
  1079
  for each type constructor @{text t}.  At most occasions
wenzelm@27040
  1080
  overloading will be used in a Haskell-like fashion together with
wenzelm@27040
  1081
  type classes by means of @{command "instantiation"} (see
wenzelm@27040
  1082
  \secref{sec:class}).  Sometimes low-level overloading is desirable.
wenzelm@27040
  1083
  The @{command "overloading"} target provides a convenient view for
wenzelm@27040
  1084
  end-users.
wenzelm@27040
  1085
wenzelm@55112
  1086
  @{rail \<open>
wenzelm@42704
  1087
    @@{command overloading} ( spec + ) @'begin'
wenzelm@42704
  1088
    ;
wenzelm@42704
  1089
    spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
wenzelm@55112
  1090
  \<close>}
wenzelm@27040
  1091
wenzelm@28760
  1092
  \begin{description}
wenzelm@27040
  1093
wenzelm@28760
  1094
  \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
  1095
  opens a theory target (cf.\ \secref{sec:target}) which allows to
wenzelm@27040
  1096
  specify constants with overloaded definitions.  These are identified
wenzelm@28760
  1097
  by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
wenzelm@28760
  1098
  constants @{text "c\<^sub>i"} at particular type instances.  The
wenzelm@28760
  1099
  definitions themselves are established using common specification
wenzelm@28760
  1100
  tools, using the names @{text "x\<^sub>i"} as reference to the
wenzelm@28760
  1101
  corresponding constants.  The target is concluded by @{command
wenzelm@28760
  1102
  (local) "end"}.
wenzelm@27040
  1103
wenzelm@27040
  1104
  A @{text "(unchecked)"} option disables global dependency checks for
wenzelm@27040
  1105
  the corresponding definition, which is occasionally useful for
haftmann@31047
  1106
  exotic overloading (see \secref{sec:consts} for a precise description).
haftmann@31047
  1107
  It is at the discretion of the user to avoid
wenzelm@27040
  1108
  malformed theory specifications!
wenzelm@27040
  1109
wenzelm@28760
  1110
  \end{description}
wenzelm@58618
  1111
\<close>
wenzelm@27040
  1112
wenzelm@27040
  1113
wenzelm@58618
  1114
section \<open>Incorporating ML code \label{sec:ML}\<close>
wenzelm@27040
  1115
wenzelm@58618
  1116
text \<open>
wenzelm@27040
  1117
  \begin{matharray}{rcl}
wenzelm@56275
  1118
    @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@48890
  1119
    @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761
  1120
    @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761
  1121
    @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
wenzelm@28761
  1122
    @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
wenzelm@28761
  1123
    @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
wenzelm@28761
  1124
    @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@30461
  1125
    @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@57941
  1126
    @{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28760
  1127
  \end{matharray}
wenzelm@57478
  1128
  \begin{tabular}{rcll}
wenzelm@57478
  1129
    @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\
wenzelm@57478
  1130
    @{attribute_def ML_source_trace} & : & @{text attribute} & default @{text false} \\
wenzelm@57478
  1131
    @{attribute_def ML_exception_trace} & : & @{text attribute} & default @{text false} \\
wenzelm@57478
  1132
  \end{tabular}
wenzelm@28760
  1133
wenzelm@55112
  1134
  @{rail \<open>
wenzelm@56275
  1135
    (@@{command SML_file} | @@{command ML_file}) @{syntax name}
wenzelm@27040
  1136
    ;
wenzelm@42596
  1137
    (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
wenzelm@42596
  1138
      @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
wenzelm@27040
  1139
    ;
wenzelm@59783
  1140
    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
wenzelm@55112
  1141
  \<close>}
wenzelm@27040
  1142
wenzelm@28760
  1143
  \begin{description}
wenzelm@27040
  1144
wenzelm@56275
  1145
  \item @{command "SML_file"}~@{text "name"} reads and evaluates the
wenzelm@56275
  1146
  given Standard ML file.  Top-level SML bindings are stored within
wenzelm@56275
  1147
  the theory context; the initial environment is restricted to the
wenzelm@56275
  1148
  Standard ML implementation of Poly/ML, without the many add-ons of
wenzelm@56275
  1149
  Isabelle/ML.  Multiple @{command "SML_file"} commands may be used to
wenzelm@56275
  1150
  build larger Standard ML projects, independently of the regular
wenzelm@56275
  1151
  Isabelle/ML environment.
wenzelm@56275
  1152
wenzelm@48890
  1153
  \item @{command "ML_file"}~@{text "name"} reads and evaluates the
wenzelm@48890
  1154
  given ML file.  The current theory context is passed down to the ML
wenzelm@48890
  1155
  toplevel and may be modified, using @{ML "Context.>>"} or derived ML
wenzelm@48890
  1156
  commands.  Top-level ML bindings are stored within the (global or
wenzelm@48890
  1157
  local) theory context.
wenzelm@27040
  1158
  
wenzelm@48890
  1159
  \item @{command "ML"}~@{text "text"} is similar to @{command
wenzelm@48890
  1160
  "ML_file"}, but evaluates directly the given @{text "text"}.
wenzelm@28760
  1161
  Top-level ML bindings are stored within the (global or local) theory
wenzelm@28760
  1162
  context.
wenzelm@28281
  1163
wenzelm@28760
  1164
  \item @{command "ML_prf"} is analogous to @{command "ML"} but works
wenzelm@48890
  1165
  within a proof context.  Top-level ML bindings are stored within the
wenzelm@48890
  1166
  proof context in a purely sequential fashion, disregarding the
wenzelm@48890
  1167
  nested proof structure.  ML bindings introduced by @{command
wenzelm@48890
  1168
  "ML_prf"} are discarded at the end of the proof.
wenzelm@27040
  1169
wenzelm@28760
  1170
  \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
wenzelm@28760
  1171
  versions of @{command "ML"}, which means that the context may not be
wenzelm@28760
  1172
  updated.  @{command "ML_val"} echos the bindings produced at the ML
wenzelm@28760
  1173
  toplevel, but @{command "ML_command"} is silent.
wenzelm@27040
  1174
  
wenzelm@28760
  1175
  \item @{command "setup"}~@{text "text"} changes the current theory
wenzelm@27040
  1176
  context by applying @{text "text"}, which refers to an ML expression
wenzelm@30461
  1177
  of type @{ML_type "theory -> theory"}.  This enables to initialize
wenzelm@30461
  1178
  any object-logic specific tools and packages written in ML, for
wenzelm@30461
  1179
  example.
wenzelm@30461
  1180
wenzelm@30461
  1181
  \item @{command "local_setup"} is similar to @{command "setup"} for
wenzelm@30461
  1182
  a local theory context, and an ML expression of type @{ML_type
wenzelm@30461
  1183
  "local_theory -> local_theory"}.  This allows to
wenzelm@30461
  1184
  invoke local theory specification packages without going through
wenzelm@30461
  1185
  concrete outer syntax, for example.
wenzelm@28758
  1186
wenzelm@30526
  1187
  \item @{command "attribute_setup"}~@{text "name = text description"}
wenzelm@57941
  1188
  defines an attribute in the current context.  The given @{text
wenzelm@30526
  1189
  "text"} has to be an ML expression of type
wenzelm@30526
  1190
  @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
wenzelm@55837
  1191
  structure @{ML_structure Args} and @{ML_structure Attrib}.
wenzelm@30526
  1192
wenzelm@30526
  1193
  In principle, attributes can operate both on a given theorem and the
wenzelm@30526
  1194
  implicit context, although in practice only one is modified and the
wenzelm@30526
  1195
  other serves as parameter.  Here are examples for these two cases:
wenzelm@30526
  1196
wenzelm@30526
  1197
  \end{description}
wenzelm@58618
  1198
\<close>
wenzelm@30526
  1199
wenzelm@58619
  1200
  attribute_setup my_rule =
wenzelm@58619
  1201
    \<open>Attrib.thms >> (fn ths =>
wenzelm@42704
  1202
      Thm.rule_attribute
wenzelm@42704
  1203
        (fn context: Context.generic => fn th: thm =>
wenzelm@30526
  1204
          let val th' = th OF ths
wenzelm@58618
  1205
          in th' end))\<close>
wenzelm@30526
  1206
wenzelm@58619
  1207
  attribute_setup my_declaration =
wenzelm@58619
  1208
    \<open>Attrib.thms >> (fn ths =>
wenzelm@42704
  1209
      Thm.declaration_attribute
wenzelm@42704
  1210
        (fn th: thm => fn context: Context.generic =>
wenzelm@30526
  1211
          let val context' = context
wenzelm@58618
  1212
          in context' end))\<close>
wenzelm@30526
  1213
wenzelm@58618
  1214
text \<open>
wenzelm@57478
  1215
  \begin{description}
wenzelm@57478
  1216
wenzelm@57478
  1217
  \item @{attribute ML_print_depth} controls the printing depth of the ML
wenzelm@57478
  1218
  toplevel pretty printer; the precise effect depends on the ML compiler and
wenzelm@57478
  1219
  run-time system. Typically the limit should be less than 10. Bigger values
wenzelm@57478
  1220
  such as 100--1000 are occasionally useful for debugging.
wenzelm@57478
  1221
wenzelm@57478
  1222
  \item @{attribute ML_source_trace} indicates whether the source text that
wenzelm@57478
  1223
  is given to the ML compiler should be output: it shows the raw Standard ML
wenzelm@57478
  1224
  after expansion of Isabelle/ML antiquotations.
wenzelm@57478
  1225
wenzelm@57478
  1226
  \item @{attribute ML_exception_trace} indicates whether the ML run-time
wenzelm@57478
  1227
  system should print a detailed stack trace on exceptions. The result is
wenzelm@57478
  1228
  dependent on the particular ML compiler version. Note that after Poly/ML
wenzelm@57478
  1229
  5.3 some optimizations in the run-time systems may hinder exception
wenzelm@57478
  1230
  traces.
wenzelm@57478
  1231
wenzelm@57478
  1232
  The boundary for the exception trace is the current Isar command
wenzelm@57478
  1233
  transactions. It is occasionally better to insert the combinator @{ML
wenzelm@58552
  1234
  Runtime.exn_trace} into ML code for debugging @{cite
wenzelm@58552
  1235
  "isabelle-implementation"}, closer to the point where it actually
wenzelm@57478
  1236
  happens.
wenzelm@57478
  1237
wenzelm@57478
  1238
  \end{description}
wenzelm@58618
  1239
\<close>
wenzelm@57478
  1240
wenzelm@27040
  1241
wenzelm@58618
  1242
section \<open>Primitive specification elements\<close>
wenzelm@27040
  1243
wenzelm@58618
  1244
subsection \<open>Sorts\<close>
wenzelm@27040
  1245
wenzelm@58618
  1246
text \<open>
wenzelm@27040
  1247
  \begin{matharray}{rcll}
haftmann@37768
  1248
    @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
wenzelm@27040
  1249
  \end{matharray}
wenzelm@27040
  1250
wenzelm@55112
  1251
  @{rail \<open>
wenzelm@42596
  1252
    @@{command default_sort} @{syntax sort}
wenzelm@55112
  1253
  \<close>}
wenzelm@27040
  1254
wenzelm@28760
  1255
  \begin{description}
wenzelm@27040
  1256
wenzelm@36454
  1257
  \item @{command "default_sort"}~@{text s} makes sort @{text s} the
wenzelm@28767
  1258
  new default sort for any type variable that is given explicitly in
wenzelm@28767
  1259
  the text, but lacks a sort constraint (wrt.\ the current context).
wenzelm@28767
  1260
  Type variables generated by type inference are not affected.
wenzelm@28767
  1261
wenzelm@28767
  1262
  Usually the default sort is only changed when defining a new
wenzelm@28767
  1263
  object-logic.  For example, the default sort in Isabelle/HOL is
wenzelm@39831
  1264
  @{class type}, the class of all HOL types.
wenzelm@28767
  1265
wenzelm@28767
  1266
  When merging theories, the default sorts of the parents are
wenzelm@28767
  1267
  logically intersected, i.e.\ the representations as lists of classes
wenzelm@28767
  1268
  are joined.
wenzelm@27040
  1269
wenzelm@28760
  1270
  \end{description}
wenzelm@58618
  1271
\<close>
wenzelm@27040
  1272
wenzelm@27040
  1273
wenzelm@58618
  1274
subsection \<open>Types \label{sec:types-pure}\<close>
wenzelm@27040
  1275
wenzelm@58618
  1276
text \<open>
wenzelm@27040
  1277
  \begin{matharray}{rcll}
wenzelm@41249
  1278
    @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@35681
  1279
    @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@27040
  1280
  \end{matharray}
wenzelm@27040
  1281
wenzelm@55112
  1282
  @{rail \<open>
wenzelm@42596
  1283
    @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
wenzelm@27040
  1284
    ;
wenzelm@42596
  1285
    @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
wenzelm@55112
  1286
  \<close>}
wenzelm@27040
  1287
wenzelm@28760
  1288
  \begin{description}
wenzelm@27040
  1289
wenzelm@57487
  1290
  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
wenzelm@57487
  1291
  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type @{text
wenzelm@57487
  1292
  "\<tau>"}. Unlike the semantic type definitions in Isabelle/HOL, type synonyms
wenzelm@57487
  1293
  are merely syntactic abbreviations without any logical significance.
wenzelm@41249
  1294
  Internally, type synonyms are fully expanded.
wenzelm@27040
  1295
  
wenzelm@28760
  1296
  \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
wenzelm@28767
  1297
  type constructor @{text t}.  If the object-logic defines a base sort
wenzelm@28767
  1298
  @{text s}, then the constructor is declared to operate on that, via
wenzelm@55385
  1299
  the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
wenzelm@27040
  1300
wenzelm@28760
  1301
  \end{description}
wenzelm@57487
  1302
wenzelm@57487
  1303
  \begin{warn}
wenzelm@57487
  1304
  If you introduce a new type axiomatically, i.e.\ via @{command_ref
wenzelm@57487
  1305
  typedecl} and @{command_ref axiomatization}
wenzelm@57487
  1306
  (\secref{sec:axiomatizations}), the minimum requirement is that it has a
wenzelm@57487
  1307
  non-empty model, to avoid immediate collapse of the logical environment.
wenzelm@57487
  1308
  Moreover, one needs to demonstrate that the interpretation of such
wenzelm@57487
  1309
  free-form axiomatizations can coexist with other axiomatization schemes
wenzelm@57487
  1310
  for types, notably @{command_def typedef} in Isabelle/HOL
wenzelm@57487
  1311
  (\secref{sec:hol-typedef}), or any other extension that people might have
wenzelm@57487
  1312
  introduced elsewhere.
wenzelm@57487
  1313
  \end{warn}
wenzelm@58618
  1314
\<close>
wenzelm@27040
  1315
wenzelm@27040
  1316
wenzelm@58618
  1317
subsection \<open>Constants and definitions \label{sec:consts}\<close>
wenzelm@27040
  1318
wenzelm@58618
  1319
text \<open>
wenzelm@47483
  1320
  \begin{matharray}{rcl}
wenzelm@47483
  1321
    @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@47483
  1322
    @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@47483
  1323
  \end{matharray}
wenzelm@47483
  1324
wenzelm@27040
  1325
  Definitions essentially express abbreviations within the logic.  The
wenzelm@27040
  1326
  simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
wenzelm@27040
  1327
  c} is a newly declared constant.  Isabelle also allows derived forms
wenzelm@27040
  1328
  where the arguments of @{text c} appear on the left, abbreviating a
wenzelm@27040
  1329
  prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
wenzelm@27040
  1330
  written more conveniently as @{text "c x y \<equiv> t"}.  Moreover,
wenzelm@27040
  1331
  definitions may be weakened by adding arbitrary pre-conditions:
wenzelm@27040
  1332
  @{text "A \<Longrightarrow> c x y \<equiv> t"}.
wenzelm@27040
  1333
wenzelm@27040
  1334
  \medskip The built-in well-formedness conditions for definitional
wenzelm@27040
  1335
  specifications are:
wenzelm@27040
  1336
wenzelm@27040
  1337
  \begin{itemize}
wenzelm@27040
  1338
wenzelm@27040
  1339
  \item Arguments (on the left-hand side) must be distinct variables.
wenzelm@27040
  1340
wenzelm@27040
  1341
  \item All variables on the right-hand side must also appear on the
wenzelm@27040
  1342
  left-hand side.
wenzelm@27040
  1343
wenzelm@27040
  1344
  \item All type variables on the right-hand side must also appear on
wenzelm@27040
  1345
  the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
wenzelm@27040
  1346
  \<alpha> list)"} for example.
wenzelm@27040
  1347
wenzelm@27040
  1348
  \item The definition must not be recursive.  Most object-logics
wenzelm@27040
  1349
  provide definitional principles that can be used to express
wenzelm@27040
  1350
  recursion safely.
wenzelm@27040
  1351
wenzelm@27040
  1352
  \end{itemize}
wenzelm@27040
  1353
haftmann@31047
  1354
  The right-hand side of overloaded definitions may mention overloaded constants
wenzelm@27040
  1355
  recursively at type instances corresponding to the immediate
wenzelm@27040
  1356
  argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}.  Incomplete
wenzelm@27040
  1357
  specification patterns impose global constraints on all occurrences,
wenzelm@27040
  1358
  e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
wenzelm@27040
  1359
  corresponding occurrences on some right-hand side need to be an
wenzelm@27040
  1360
  instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
wenzelm@27040
  1361
wenzelm@55112
  1362
  @{rail \<open>
wenzelm@42596
  1363
    @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
wenzelm@27040
  1364
    ;
wenzelm@42704
  1365
    @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
wenzelm@42704
  1366
    ;
wenzelm@42704
  1367
    opt: '(' @'unchecked'? @'overloaded'? ')'
wenzelm@55112
  1368
  \<close>}
wenzelm@27040
  1369
wenzelm@28760
  1370
  \begin{description}
wenzelm@27040
  1371
wenzelm@28760
  1372
  \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
wenzelm@28760
  1373
  c} to have any instance of type scheme @{text \<sigma>}.  The optional
wenzelm@28760
  1374
  mixfix annotations may attach concrete syntax to the constants
wenzelm@28760
  1375
  declared.
wenzelm@27040
  1376
  
wenzelm@28760
  1377
  \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
wenzelm@27040
  1378
  as a definitional axiom for some existing constant.
wenzelm@27040
  1379
  
wenzelm@27040
  1380
  The @{text "(unchecked)"} option disables global dependency checks
wenzelm@27040
  1381
  for this definition, which is occasionally useful for exotic
wenzelm@27040
  1382
  overloading.  It is at the discretion of the user to avoid malformed
wenzelm@27040
  1383
  theory specifications!
wenzelm@27040
  1384
  
wenzelm@27040
  1385
  The @{text "(overloaded)"} option declares definitions to be
wenzelm@27040
  1386
  potentially overloaded.  Unless this option is given, a warning
wenzelm@27040
  1387
  message would be issued for any definitional equation with a more
wenzelm@27040
  1388
  special type than that of the corresponding constant declaration.
wenzelm@27040
  1389
  
wenzelm@28760
  1390
  \end{description}
wenzelm@58618
  1391
\<close>
wenzelm@27040
  1392
wenzelm@27040
  1393
wenzelm@58618
  1394
section \<open>Naming existing theorems \label{sec:theorems}\<close>
wenzelm@27040
  1395
wenzelm@58618
  1396
text \<open>
wenzelm@27040
  1397
  \begin{matharray}{rcll}
wenzelm@28761
  1398
    @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@28761
  1399
    @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@57946
  1400
    @{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
wenzelm@27040
  1401
  \end{matharray}
wenzelm@27040
  1402
wenzelm@55112
  1403
  @{rail \<open>
wenzelm@59785
  1404
    (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and')
wenzelm@59785
  1405
      @{syntax for_fixes}
wenzelm@57946
  1406
    ;
wenzelm@59785
  1407
    @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
wenzelm@55112
  1408
  \<close>}
wenzelm@27040
  1409
wenzelm@28760
  1410
  \begin{description}
wenzelm@27040
  1411
  
wenzelm@45600
  1412
  \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def
wenzelm@45600
  1413
  "for"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"} evaluates given facts (with attributes) in
wenzelm@45600
  1414
  the current context, which may be augmented by local variables.
wenzelm@45600
  1415
  Results are standardized before being stored, i.e.\ schematic
wenzelm@45600
  1416
  variables are renamed to enforce index @{text "0"} uniformly.
wenzelm@45600
  1417
wenzelm@45600
  1418
  \item @{command "theorems"} is the same as @{command "lemmas"}, but
wenzelm@45600
  1419
  marks the result as a different kind of facts.
wenzelm@27040
  1420
wenzelm@57946
  1421
  \item @{command "named_theorems"}~@{text "name description"} declares a
wenzelm@57946
  1422
  dynamic fact within the context. The same @{text name} is used to define
wenzelm@57946
  1423
  an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see
wenzelm@57946
  1424
  \secref{sec:simp-rules}) to maintain the content incrementally, in
wenzelm@57946
  1425
  canonical declaration order of the text structure.
wenzelm@57946
  1426
wenzelm@28760
  1427
  \end{description}
wenzelm@58618
  1428
\<close>
wenzelm@27040
  1429
wenzelm@27040
  1430
wenzelm@58618
  1431
section \<open>Oracles\<close>
wenzelm@27040
  1432
wenzelm@58618
  1433
text \<open>
wenzelm@47483
  1434
  \begin{matharray}{rcll}
wenzelm@47483
  1435
    @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
wenzelm@47483
  1436
  \end{matharray}
wenzelm@47483
  1437
wenzelm@47483
  1438
  Oracles allow Isabelle to take advantage of external reasoners such
wenzelm@47483
  1439
  as arithmetic decision procedures, model checkers, fast tautology
wenzelm@47483
  1440
  checkers or computer algebra systems.  Invoked as an oracle, an
wenzelm@47483
  1441
  external reasoner can create arbitrary Isabelle theorems.
wenzelm@28756
  1442
wenzelm@28756
  1443
  It is the responsibility of the user to ensure that the external
wenzelm@28756
  1444
  reasoner is as trustworthy as the application requires.  Another
wenzelm@28756
  1445
  typical source of errors is the linkup between Isabelle and the
wenzelm@28756
  1446
  external tool, not just its concrete implementation, but also the
wenzelm@28756
  1447
  required translation between two different logical environments.
wenzelm@28756
  1448
wenzelm@28756
  1449
  Isabelle merely guarantees well-formedness of the propositions being
wenzelm@28756
  1450
  asserted, and records within the internal derivation object how
wenzelm@28756
  1451
  presumed theorems depend on unproven suppositions.
wenzelm@28756
  1452
wenzelm@55112
  1453
  @{rail \<open>
wenzelm@42596
  1454
    @@{command oracle} @{syntax name} '=' @{syntax text}
wenzelm@55112
  1455
  \<close>}
wenzelm@27040
  1456
wenzelm@28760
  1457
  \begin{description}
wenzelm@27040
  1458
wenzelm@28760
  1459
  \item @{command "oracle"}~@{text "name = text"} turns the given ML
wenzelm@28290
  1460
  expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
wenzelm@28290
  1461
  ML function of type @{ML_text "'a -> thm"}, which is bound to the
wenzelm@28756
  1462
  global identifier @{ML_text name}.  This acts like an infinitary
wenzelm@28756
  1463
  specification of axioms!  Invoking the oracle only works within the
wenzelm@28756
  1464
  scope of the resulting theory.
wenzelm@27040
  1465
wenzelm@28760
  1466
  \end{description}
wenzelm@28756
  1467
wenzelm@40800
  1468
  See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
wenzelm@28756
  1469
  defining a new primitive rule as oracle, and turning it into a proof
wenzelm@28756
  1470
  method.
wenzelm@58618
  1471
\<close>
wenzelm@27040
  1472
wenzelm@27040
  1473
wenzelm@58618
  1474
section \<open>Name spaces\<close>
wenzelm@27040
  1475
wenzelm@58618
  1476
text \<open>
wenzelm@27040
  1477
  \begin{matharray}{rcl}
wenzelm@36177
  1478
    @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@36177
  1479
    @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@36177
  1480
    @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@36177
  1481
    @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
wenzelm@27040
  1482
  \end{matharray}
wenzelm@27040
  1483
wenzelm@55112
  1484
  @{rail \<open>
wenzelm@42596
  1485
    ( @{command hide_class} | @{command hide_type} |
wenzelm@42596
  1486
      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
wenzelm@55112
  1487
  \<close>}
wenzelm@27040
  1488
wenzelm@27040
  1489
  Isabelle organizes any kind of name declarations (of types,
wenzelm@27040
  1490
  constants, theorems etc.) by separate hierarchically structured name
wenzelm@27040
  1491
  spaces.  Normally the user does not have to control the behavior of
wenzelm@27040
  1492
  name spaces by hand, yet the following commands provide some way to
wenzelm@27040
  1493
  do so.
wenzelm@27040
  1494
wenzelm@28760
  1495
  \begin{description}
wenzelm@27040
  1496
wenzelm@36177
  1497
  \item @{command "hide_class"}~@{text names} fully removes class
wenzelm@36177
  1498
  declarations from a given name space; with the @{text "(open)"}
krauss@39977
  1499
  option, only the base name is hidden.
wenzelm@36177
  1500
wenzelm@27040
  1501
  Note that hiding name space accesses has no impact on logical
wenzelm@28756
  1502
  declarations --- they remain valid internally.  Entities that are no
wenzelm@27040
  1503
  longer accessible to the user are printed with the special qualifier
wenzelm@27040
  1504
  ``@{text "??"}'' prefixed to the full internal name.
wenzelm@27040
  1505
wenzelm@36177
  1506
  \item @{command "hide_type"}, @{command "hide_const"}, and @{command
wenzelm@36177
  1507
  "hide_fact"} are similar to @{command "hide_class"}, but hide types,
wenzelm@36177
  1508
  constants, and facts, respectively.
wenzelm@36177
  1509
  
wenzelm@28760
  1510
  \end{description}
wenzelm@58618
  1511
\<close>
wenzelm@27040
  1512
wenzelm@26869
  1513
end