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