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