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