src/Doc/Implementation/Prelim.thy
author wenzelm
Mon, 20 Jul 2020 23:45:29 +0200
changeset 72290 efb7fd4a6d1f
parent 69609 ff784d5a5bfb
permissions -rw-r--r--
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory; explicitly check for extend as identity;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61580
diff changeset
     1
(*:maxLineLen=78:*)
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61580
diff changeset
     2
29755
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 29581
diff changeset
     3
theory Prelim
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 29581
diff changeset
     4
imports Base
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 29581
diff changeset
     5
begin
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
     7
chapter \<open>Preliminaries\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
     9
section \<open>Contexts \label{sec:context}\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
    11
text \<open>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    12
  A logical context represents the background that is required for formulating
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    13
  statements and composing proofs. It acts as a medium to produce formal
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    14
  content, depending on earlier material (declarations, results etc.).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    16
  For example, derivations within the Isabelle/Pure logic can be described as
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    17
  a judgment \<open>\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>\<close>, which means that a proposition \<open>\<phi>\<close> is derivable from
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    18
  hypotheses \<open>\<Gamma>\<close> within the theory \<open>\<Theta>\<close>. There are logical reasons for keeping
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    19
  \<open>\<Theta>\<close> and \<open>\<Gamma>\<close> separate: theories can be liberal about supporting type
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    20
  constructors and schematic polymorphism of constants and axioms, while the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    21
  inner calculus of \<open>\<Gamma> \<turnstile> \<phi>\<close> is strictly limited to Simple Type Theory (with
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    22
  fixed type variables in the assumptions).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    23
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
    24
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    25
  Contexts and derivations are linked by the following key principles:
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
    26
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    27
  \<^item> Transfer: monotonicity of derivations admits results to be transferred
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    28
  into a \<^emph>\<open>larger\<close> context, i.e.\ \<open>\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>\<close> implies \<open>\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>\<close> for contexts
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    29
  \<open>\<Theta>' \<supseteq> \<Theta>\<close> and \<open>\<Gamma>' \<supseteq> \<Gamma>\<close>.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    30
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    31
  \<^item> Export: discharge of hypotheses admits results to be exported into a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    32
  \<^emph>\<open>smaller\<close> context, i.e.\ \<open>\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>\<close> implies \<open>\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>\<close> where \<open>\<Gamma>' \<supseteq> \<Gamma>\<close>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    33
  and \<open>\<Delta> = \<Gamma>' - \<Gamma>\<close>. Note that \<open>\<Theta>\<close> remains unchanged here, only the \<open>\<Gamma>\<close> part is
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    34
  affected.
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
    35
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    36
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
    37
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    38
  By modeling the main characteristics of the primitive \<open>\<Theta>\<close> and \<open>\<Gamma>\<close> above, and
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    39
  abstracting over any particular logical content, we arrive at the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    40
  fundamental notions of \<^emph>\<open>theory context\<close> and \<^emph>\<open>proof context\<close> in
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    41
  Isabelle/Isar. These implement a certain policy to manage arbitrary
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    42
  \<^emph>\<open>context data\<close>. There is a strongly-typed mechanism to declare new kinds of
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
    43
  data at compile time.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    44
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    45
  The internal bootstrap process of Isabelle/Pure eventually reaches a stage
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    46
  where certain data slots provide the logical content of \<open>\<Theta>\<close> and \<open>\<Gamma>\<close> sketched
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    47
  above, but this does not stop there! Various additional data slots support
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    48
  all kinds of mechanisms that are not necessarily part of the core logic.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    49
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    50
  For example, there would be data for canonical introduction and elimination
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    51
  rules for arbitrary operators (depending on the object-logic and
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    52
  application), which enables users to perform standard proof steps implicitly
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    53
  (cf.\ the \<open>rule\<close> method @{cite "isabelle-isar-ref"}).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    54
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
    55
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    56
  Thus Isabelle/Isar is able to bring forth more and more concepts
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    57
  successively. In particular, an object-logic like Isabelle/HOL continues the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    58
  Isabelle/Pure setup by adding specific components for automated reasoning
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    59
  (classical reasoner, tableau prover, structured induction etc.) and derived
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    60
  specification mechanisms (inductive predicates, recursive functions etc.).
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    61
  All of this is ultimately based on the generic data management by theory and
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    62
  proof contexts introduced here.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
    63
\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    64
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    65
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
    66
subsection \<open>Theory context \label{sec:context-theory}\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    67
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    68
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    69
  A \<^emph>\<open>theory\<close> is a data container with explicit name and unique identifier.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    70
  Theories are related by a (nominal) sub-theory relation, which corresponds
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    71
  to the dependency graph of the original construction; each theory is derived
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    72
  from a certain sub-graph of ancestor theories. To this end, the system
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    73
  maintains a set of symbolic ``identification stamps'' within each theory.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    74
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    75
  The \<open>begin\<close> operation starts a new theory by importing several parent
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    76
  theories (with merged contents) and entering a special mode of nameless
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    77
  incremental updates, until the final \<open>end\<close> operation is performed.
34921
008126f730a0 formal markup of type aliases;
wenzelm
parents: 33524
diff changeset
    78
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
    79
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    80
  The example in \figref{fig:ex-theory} below shows a theory graph derived
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    81
  from \<open>Pure\<close>, with theory \<open>Length\<close> importing \<open>Nat\<close> and \<open>List\<close>. The body of
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    82
  \<open>Length\<close> consists of a sequence of updates, resulting in locally a linear
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
    83
  sub-theory relation for each intermediate step.
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
    84
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
    85
  \begin{figure}[htb]
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
    86
  \begin{center}
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
    87
  \begin{tabular}{rcccl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    88
        &            & \<open>Pure\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    89
        &            & \<open>\<down>\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    90
        &            & \<open>FOL\<close> \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
        & $\swarrow$ &              & $\searrow$ & \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    92
  \<open>Nat\<close> &    &              &            & \<open>List\<close> \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    93
        & $\searrow$ &              & $\swarrow$ \\
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
    94
        &            & \<open>Length\<close> \\
26864
1417e704d724 replaced macros by antiquotations;
wenzelm
parents: 24137
diff changeset
    95
        &            & \multicolumn{3}{l}{~~@{keyword "begin"}} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    96
        &            & $\vdots$~~ \\
26864
1417e704d724 replaced macros by antiquotations;
wenzelm
parents: 24137
diff changeset
    97
        &            & \multicolumn{3}{l}{~~@{command "end"}} \\
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
    98
  \end{tabular}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    99
  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   100
  \end{center}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   101
  \end{figure}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   102
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   103
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   104
  Derived formal entities may retain a reference to the background theory in
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   105
  order to indicate the formal context from which they were produced. This
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   106
  provides an immutable certificate of the background theory.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   107
\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   108
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   109
text %mlref \<open>
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   110
  \begin{mldecls}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   111
  @{index_ML_type theory} \\
60948
b710a5087116 prefer theory_id operations;
wenzelm
parents: 59902
diff changeset
   112
  @{index_ML Context.eq_thy: "theory * theory -> bool"} \\
b710a5087116 prefer theory_id operations;
wenzelm
parents: 59902
diff changeset
   113
  @{index_ML Context.subthy: "theory * theory -> bool"} \\
48930
10b89c127153 updated Theory.begin_theory;
wenzelm
parents: 47174
diff changeset
   114
  @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
39837
eacb7825025d cover some more theory operations;
wenzelm
parents: 39833
diff changeset
   115
  @{index_ML Theory.parents_of: "theory -> theory list"} \\
eacb7825025d cover some more theory operations;
wenzelm
parents: 39833
diff changeset
   116
  @{index_ML Theory.ancestors_of: "theory -> theory list"} \\
20547
wenzelm
parents: 20530
diff changeset
   117
  \end{mldecls}
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   118
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   119
  \<^descr> Type \<^ML_type>\<open>theory\<close> represents theory contexts.
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   120
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   121
  \<^descr> \<^ML>\<open>Context.eq_thy\<close>~\<open>(thy\<^sub>1, thy\<^sub>2)\<close> check strict identity of two
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   122
  theories.
39837
eacb7825025d cover some more theory operations;
wenzelm
parents: 39833
diff changeset
   123
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   124
  \<^descr> \<^ML>\<open>Context.subthy\<close>~\<open>(thy\<^sub>1, thy\<^sub>2)\<close> compares theories according to the
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   125
  intrinsic graph structure of the construction. This sub-theory relation is a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   126
  nominal approximation of inclusion (\<open>\<subseteq>\<close>) of the corresponding content
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   127
  (according to the semantics of the ML modules that implement the data).
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   128
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   129
  \<^descr> \<^ML>\<open>Theory.begin_theory\<close>~\<open>name parents\<close> constructs a new theory based
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   130
  on the given parents. This ML function is normally not invoked directly.
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   131
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   132
  \<^descr> \<^ML>\<open>Theory.parents_of\<close>~\<open>thy\<close> returns the direct ancestors of \<open>thy\<close>.
39837
eacb7825025d cover some more theory operations;
wenzelm
parents: 39833
diff changeset
   133
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   134
  \<^descr> \<^ML>\<open>Theory.ancestors_of\<close>~\<open>thy\<close> returns all ancestors of \<open>thy\<close> (not
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   135
  including \<open>thy\<close> itself).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   136
\<close>
20430
wenzelm
parents: 20429
diff changeset
   137
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   138
text %mlantiq \<open>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   139
  \begin{matharray}{rcl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   140
  @{ML_antiquotation_def "theory"} & : & \<open>ML_antiquotation\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   141
  @{ML_antiquotation_def "theory_context"} & : & \<open>ML_antiquotation\<close> \\
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   142
  \end{matharray}
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   143
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   144
  \<^rail>\<open>
67146
909dcdec2122 more embedded cartouche arguments;
wenzelm
parents: 62969
diff changeset
   145
  @@{ML_antiquotation theory} embedded?
51686
532e0ac5a66d added ML antiquotation @{theory_context};
wenzelm
parents: 48992
diff changeset
   146
  ;
67146
909dcdec2122 more embedded cartouche arguments;
wenzelm
parents: 62969
diff changeset
   147
  @@{ML_antiquotation theory_context} embedded
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   148
  \<close>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   149
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   150
  \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   151
  abstract value.
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   152
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   153
  \<^descr> \<open>@{theory A}\<close> refers to an explicitly named ancestor theory \<open>A\<close> of the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   154
  background theory of the current context --- as abstract value.
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   155
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   156
  \<^descr> \<open>@{theory_context A}\<close> is similar to \<open>@{theory A}\<close>, but presents the result
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   157
  as initial \<^ML_type>\<open>Proof.context\<close> (see also \<^ML>\<open>Proof_Context.init_global\<close>).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   158
\<close>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   159
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   160
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   161
subsection \<open>Proof context \label{sec:context-proof}\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   162
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   163
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   164
  A proof context is a container for pure data that refers to the theory from
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   165
  which it is derived. The \<open>init\<close> operation creates a proof context from a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   166
  given theory. There is an explicit \<open>transfer\<close> operation to force
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   167
  resynchronization with updates to the background theory -- this is rarely
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   168
  required in practice.
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
   169
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   170
  Entities derived in a proof context need to record logical requirements
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   171
  explicitly, since there is no separate context identification or symbolic
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   172
  inclusion as for theories. For example, hypotheses used in primitive
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   173
  derivations (cf.\ \secref{sec:thms}) are recorded separately within the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   174
  sequent \<open>\<Gamma> \<turnstile> \<phi>\<close>, just to make double sure. Results could still leak into an
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   175
  alien proof context due to programming errors, but Isabelle/Isar includes
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   176
  some extra validity checks in critical positions, notably at the end of a
34921
008126f730a0 formal markup of type aliases;
wenzelm
parents: 33524
diff changeset
   177
  sub-proof.
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
   178
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   179
  Proof contexts may be manipulated arbitrarily, although the common
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   180
  discipline is to follow block structure as a mental model: a given context
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   181
  is extended consecutively, and results are exported back into the original
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   182
  context. Note that an Isar proof state models block-structured reasoning
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   183
  explicitly, using a stack of proof contexts internally. For various
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   184
  technical reasons, the background theory of an Isar proof state must not be
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   185
  changed while the proof is still under construction!
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   186
\<close>
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   187
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   188
text %mlref \<open>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   189
  \begin{mldecls}
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   190
  @{index_ML_type Proof.context} \\
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   191
  @{index_ML Proof_Context.init_global: "theory -> Proof.context"} \\
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   192
  @{index_ML Proof_Context.theory_of: "Proof.context -> theory"} \\
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   193
  @{index_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   194
  \end{mldecls}
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   195
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   196
  \<^descr> Type \<^ML_type>\<open>Proof.context\<close> represents proof contexts.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   197
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   198
  \<^descr> \<^ML>\<open>Proof_Context.init_global\<close>~\<open>thy\<close> produces a proof context derived
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   199
  from \<open>thy\<close>, initializing all data.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   200
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   201
  \<^descr> \<^ML>\<open>Proof_Context.theory_of\<close>~\<open>ctxt\<close> selects the background theory from
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   202
  \<open>ctxt\<close>.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   203
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   204
  \<^descr> \<^ML>\<open>Proof_Context.transfer\<close>~\<open>thy ctxt\<close> promotes the background theory of
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   205
  \<open>ctxt\<close> to the super theory \<open>thy\<close>.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   206
\<close>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   207
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   208
text %mlantiq \<open>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   209
  \begin{matharray}{rcl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   210
  @{ML_antiquotation_def "context"} & : & \<open>ML_antiquotation\<close> \\
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   211
  \end{matharray}
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   212
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   213
  \<^descr> \<open>@{context}\<close> refers to \<^emph>\<open>the\<close> context at compile-time --- as abstract
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   214
  value. Independently of (local) theory or proof mode, this always produces a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   215
  meaningful result.
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   216
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   217
  This is probably the most common antiquotation in interactive
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   218
  experimentation with ML inside Isar.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   219
\<close>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   220
20430
wenzelm
parents: 20429
diff changeset
   221
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   222
subsection \<open>Generic contexts \label{sec:generic-context}\<close>
20429
116255c9209b more on contexts;
wenzelm
parents: 20214
diff changeset
   223
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   224
text \<open>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   225
  A generic context is the disjoint sum of either a theory or proof context.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   226
  Occasionally, this enables uniform treatment of generic context data,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   227
  typically extra-logical information. Operations on generic contexts include
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   228
  the usual injections, partial selections, and combinators for lifting
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   229
  operations on either component of the disjoint sum.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   230
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   231
  Moreover, there are total operations \<open>theory_of\<close> and \<open>proof_of\<close> to convert a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   232
  generic context into either kind: a theory can always be selected from the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   233
  sum, while a proof context might have to be constructed by an ad-hoc \<open>init\<close>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   234
  operation, which incurs a small runtime overhead.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   235
\<close>
20430
wenzelm
parents: 20429
diff changeset
   236
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   237
text %mlref \<open>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   238
  \begin{mldecls}
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   239
  @{index_ML_type Context.generic} \\
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   240
  @{index_ML Context.theory_of: "Context.generic -> theory"} \\
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   241
  @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   242
  \end{mldecls}
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   243
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   244
  \<^descr> Type \<^ML_type>\<open>Context.generic\<close> is the direct sum of \<^ML_type>\<open>theory\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   245
  and \<^ML_type>\<open>Proof.context\<close>, with the datatype constructors \<^ML>\<open>Context.Theory\<close> and \<^ML>\<open>Context.Proof\<close>.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   246
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   247
  \<^descr> \<^ML>\<open>Context.theory_of\<close>~\<open>context\<close> always produces a theory from the
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   248
  generic \<open>context\<close>, using \<^ML>\<open>Proof_Context.theory_of\<close> as required.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   249
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   250
  \<^descr> \<^ML>\<open>Context.proof_of\<close>~\<open>context\<close> always produces a proof context from the
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   251
  generic \<open>context\<close>, using \<^ML>\<open>Proof_Context.init_global\<close> as required (note
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   252
  that this re-initializes the context data with each invocation).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   253
\<close>
20437
wenzelm
parents: 20430
diff changeset
   254
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   255
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   256
subsection \<open>Context data \label{sec:context-data}\<close>
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   257
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   258
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   259
  The main purpose of theory and proof contexts is to manage arbitrary (pure)
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   260
  data. New data types can be declared incrementally at compile time. There
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   261
  are separate declaration mechanisms for any of the three kinds of contexts:
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   262
  theory, proof, generic.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   263
\<close>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   264
61506
wenzelm
parents: 61503
diff changeset
   265
paragraph \<open>Theory data\<close>
wenzelm
parents: 61503
diff changeset
   266
text \<open>declarations need to implement the following ML signature:
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   267
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   268
  \<^medskip>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   269
  \begin{tabular}{ll}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   270
  \<open>\<type> T\<close> & representing type \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   271
  \<open>\<val> empty: T\<close> & empty default value \\
72290
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   272
  \<open>\<val> extend: T \<rightarrow> T\<close> & obsolete (identity function) \\
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   273
  \<open>\<val> merge: T \<times> T \<rightarrow> T\<close> & merge data \\
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   274
  \end{tabular}
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   275
  \<^medskip>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   276
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   277
  The \<open>empty\<close> value acts as initial default for \<^emph>\<open>any\<close> theory that does not
72290
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   278
  declare actual data content; \<open>extend\<close> is obsolete: it needs to be the
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   279
  identity function.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   280
72290
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   281
  The \<open>merge\<close> operation needs to join the data from two theories in a
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   282
  conservative manner. The standard scheme for \<open>merge (data\<^sub>1, data\<^sub>2)\<close>
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   283
  inserts those parts of \<open>data\<^sub>2\<close> into \<open>data\<^sub>1\<close> that are not yet present,
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   284
  while keeping the general order of things. The \<^ML>\<open>Library.merge\<close>
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   285
  function on plain lists may serve as canonical template. Particularly note
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   286
  that shared parts of the data must not be duplicated by naive concatenation,
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   287
  or a theory graph that resembles a chain of diamonds would cause an
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   288
  exponential blowup!
34921
008126f730a0 formal markup of type aliases;
wenzelm
parents: 33524
diff changeset
   289
72290
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   290
  Sometimes, the data consists of a single item that cannot be ``merged'' in a
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   291
  sensible manner. Then the standard scheme degenerates to the projection to
efb7fd4a6d1f subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
wenzelm
parents: 69609
diff changeset
   292
  \<open>data\<^sub>1\<close>, ignoring \<open>data\<^sub>2\<close> outright.
61506
wenzelm
parents: 61503
diff changeset
   293
\<close>
34921
008126f730a0 formal markup of type aliases;
wenzelm
parents: 33524
diff changeset
   294
61506
wenzelm
parents: 61503
diff changeset
   295
paragraph \<open>Proof context data\<close>
wenzelm
parents: 61503
diff changeset
   296
text \<open>declarations need to implement the following ML signature:
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   297
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   298
  \<^medskip>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   299
  \begin{tabular}{ll}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   300
  \<open>\<type> T\<close> & representing type \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   301
  \<open>\<val> init: theory \<rightarrow> T\<close> & produce initial value \\
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   302
  \end{tabular}
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   303
  \<^medskip>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   304
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   305
  The \<open>init\<close> operation is supposed to produce a pure value from the given
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   306
  background theory and should be somehow ``immediate''. Whenever a proof
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   307
  context is initialized, which happens frequently, the the system invokes the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   308
  \<open>init\<close> operation of \<^emph>\<open>all\<close> theory data slots ever declared. This also means
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   309
  that one needs to be economic about the total number of proof data
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   310
  declarations in the system, i.e.\ each ML module should declare at most one,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   311
  sometimes two data slots for its internal use. Repeated data declarations to
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   312
  simulate a record type should be avoided!
61506
wenzelm
parents: 61503
diff changeset
   313
\<close>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   314
61506
wenzelm
parents: 61503
diff changeset
   315
paragraph \<open>Generic data\<close>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   316
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   317
  provides a hybrid interface for both theory and proof data. The \<open>init\<close>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   318
  operation for proof contexts is predefined to select the current data value
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   319
  from the background theory.
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   320
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   321
  \<^bigskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   322
  Any of the above data declarations over type \<open>T\<close> result in an ML structure
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   323
  with the following signature:
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   324
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   325
  \<^medskip>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   326
  \begin{tabular}{ll}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   327
  \<open>get: context \<rightarrow> T\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   328
  \<open>put: T \<rightarrow> context \<rightarrow> context\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   329
  \<open>map: (T \<rightarrow> T) \<rightarrow> context \<rightarrow> context\<close> \\
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   330
  \end{tabular}
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   331
  \<^medskip>
20449
f8a7a8236c68 more stuff;
wenzelm
parents: 20447
diff changeset
   332
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   333
  These other operations provide exclusive access for the particular kind of
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   334
  context (theory, proof, or generic context). This interface observes the ML
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   335
  discipline for types and scopes: there is no other way to access the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   336
  corresponding data slot of a context. By keeping these operations private,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   337
  an Isabelle/ML module may maintain abstract values authentically.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   338
\<close>
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   339
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   340
text %mlref \<open>
20450
wenzelm
parents: 20449
diff changeset
   341
  \begin{mldecls}
33524
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33174
diff changeset
   342
  @{index_ML_functor Theory_Data} \\
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33174
diff changeset
   343
  @{index_ML_functor Proof_Data} \\
a08e6c1cbc04 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents: 33174
diff changeset
   344
  @{index_ML_functor Generic_Data} \\
20450
wenzelm
parents: 20449
diff changeset
   345
  \end{mldecls}
wenzelm
parents: 20449
diff changeset
   346
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   347
  \<^descr> \<^ML_functor>\<open>Theory_Data\<close>\<open>(spec)\<close> declares data for type \<^ML_type>\<open>theory\<close>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   348
  according to the specification provided as argument structure. The resulting
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   349
  structure provides data init and access operations as described above.
20450
wenzelm
parents: 20449
diff changeset
   350
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   351
  \<^descr> \<^ML_functor>\<open>Proof_Data\<close>\<open>(spec)\<close> is analogous to \<^ML_functor>\<open>Theory_Data\<close>
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   352
  for type \<^ML_type>\<open>Proof.context\<close>.
20450
wenzelm
parents: 20449
diff changeset
   353
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   354
  \<^descr> \<^ML_functor>\<open>Generic_Data\<close>\<open>(spec)\<close> is analogous to \<^ML_functor>\<open>Theory_Data\<close> for type \<^ML_type>\<open>Context.generic\<close>. \<close>
20450
wenzelm
parents: 20449
diff changeset
   355
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   356
text %mlex \<open>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   357
  The following artificial example demonstrates theory data: we maintain a set
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   358
  of terms that are supposed to be wellformed wrt.\ the enclosing theory. The
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   359
  public interface is as follows:
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   360
\<close>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   361
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   362
ML \<open>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   363
  signature WELLFORMED_TERMS =
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   364
  sig
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   365
    val get: theory -> term list
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   366
    val add: term -> theory -> theory
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   367
  end;
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   368
\<close>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   369
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   370
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   371
  The implementation uses private theory data internally, and only exposes an
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   372
  operation that involves explicit argument checking wrt.\ the given theory.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   373
\<close>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   374
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   375
ML \<open>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   376
  structure Wellformed_Terms: WELLFORMED_TERMS =
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   377
  struct
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   378
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   379
  structure Terms = Theory_Data
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   380
  (
39687
4e9b6ada3a21 modernized structure Ord_List;
wenzelm
parents: 37533
diff changeset
   381
    type T = term Ord_List.T;
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   382
    val empty = [];
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   383
    val extend = I;
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   384
    fun merge (ts1, ts2) =
39687
4e9b6ada3a21 modernized structure Ord_List;
wenzelm
parents: 37533
diff changeset
   385
      Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39857
diff changeset
   386
  );
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   387
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   388
  val get = Terms.get;
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   389
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   390
  fun add raw_t thy =
39821
bf164c153d10 minor tuning and updating;
wenzelm
parents: 39687
diff changeset
   391
    let
bf164c153d10 minor tuning and updating;
wenzelm
parents: 39687
diff changeset
   392
      val t = Sign.cert_term thy raw_t;
bf164c153d10 minor tuning and updating;
wenzelm
parents: 39687
diff changeset
   393
    in
bf164c153d10 minor tuning and updating;
wenzelm
parents: 39687
diff changeset
   394
      Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy
bf164c153d10 minor tuning and updating;
wenzelm
parents: 39687
diff changeset
   395
    end;
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   396
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   397
  end;
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   398
\<close>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   399
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   400
text \<open>
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   401
  Type \<^ML_type>\<open>term Ord_List.T\<close> is used for reasonably efficient
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   402
  representation of a set of terms: all operations are linear in the number of
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   403
  stored elements. Here we assume that users of this module do not care about
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   404
  the declaration order, since that data structure forces its own arrangement
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   405
  of elements.
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   406
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   407
  Observe how the \<^ML_text>\<open>merge\<close> operation joins the data slots of the two
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   408
  constituents: \<^ML>\<open>Ord_List.union\<close> prevents duplication of common data from
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   409
  different branches, thus avoiding the danger of exponential blowup. Plain
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   410
  list append etc.\ must never be used for theory data merges!
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   411
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   412
  \<^medskip>
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   413
  Our intended invariant is achieved as follows:
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   414
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   415
    \<^enum> \<^ML>\<open>Wellformed_Terms.add\<close> only admits terms that have passed the \<^ML>\<open>Sign.cert_term\<close> check of the given theory at that point.
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   416
  
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   417
    \<^enum> Wellformedness in the sense of \<^ML>\<open>Sign.cert_term\<close> is monotonic wrt.\
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   418
    the sub-theory relation. So our data can move upwards in the hierarchy
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   419
    (via extension or merges), and maintain wellformedness without further
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   420
    checks.
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   421
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   422
  Note that all basic operations of the inference kernel (which includes \<^ML>\<open>Sign.cert_term\<close>) observe this monotonicity principle, but other user-space
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   423
  tools don't. For example, fully-featured type-inference via \<^ML>\<open>Syntax.check_term\<close> (cf.\ \secref{sec:term-check}) is not necessarily
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   424
  monotonic wrt.\ the background theory, since constraints of term constants
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   425
  can be modified by later declarations, for example.
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   426
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   427
  In most cases, user-space context data does not have to take such invariants
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   428
  too seriously. The situation is different in the implementation of the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   429
  inference kernel itself, which uses the very same data mechanisms for types,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   430
  constants, axioms etc.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   431
\<close>
34928
c4cd36411983 moved examples to proper place;
wenzelm
parents: 34927
diff changeset
   432
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20437
diff changeset
   433
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   434
subsection \<open>Configuration options \label{sec:config-options}\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   435
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   436
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   437
  A \<^emph>\<open>configuration option\<close> is a named optional value of some basic type
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   438
  (Boolean, integer, string) that is stored in the context. It is a simple
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   439
  application of general context data (\secref{sec:context-data}) that is
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   440
  sufficiently common to justify customized setup, which includes some
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   441
  concrete declarations for end-users using existing notation for attributes
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   442
  (cf.\ \secref{sec:attributes}).
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   443
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   444
  For example, the predefined configuration option @{attribute show_types}
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   445
  controls output of explicit type constraints for variables in printed terms
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   446
  (cf.\ \secref{sec:read-print}). Its value can be modified within Isar text
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   447
  like this:
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   448
\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   449
59902
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   450
experiment
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   451
begin
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   452
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   453
declare [[show_types = false]]
61580
c49a8ebd30cc isabelle update_cartouches -c;
wenzelm
parents: 61506
diff changeset
   454
  \<comment> \<open>declaration within (local) theory context\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   455
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40628
diff changeset
   456
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40628
diff changeset
   457
begin
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   458
  note [[show_types = true]]
61580
c49a8ebd30cc isabelle update_cartouches -c;
wenzelm
parents: 61506
diff changeset
   459
    \<comment> \<open>declaration within proof (forward mode)\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   460
  term x
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   461
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   462
  have "x = x"
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   463
    using [[show_types = false]]
61580
c49a8ebd30cc isabelle update_cartouches -c;
wenzelm
parents: 61506
diff changeset
   464
      \<comment> \<open>declaration within proof (backward mode)\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   465
    ..
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40628
diff changeset
   466
end
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   467
59902
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   468
end
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   469
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   470
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   471
  Configuration options that are not set explicitly hold a default value that
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   472
  can depend on the application context. This allows to retrieve the value
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   473
  from another slot within the context, or fall back on a global preference
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   474
  mechanism, for example.
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   475
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   476
  The operations to declare configuration options and get/map their values are
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   477
  modeled as direct replacements for historic global references, only that the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   478
  context is made explicit. This allows easy configuration of tools, without
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   479
  relying on the execution order as required for old-style mutable
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   480
  references.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   481
\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   482
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   483
text %mlref \<open>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   484
  \begin{mldecls}
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   485
  @{index_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   486
  @{index_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   487
  @{index_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) ->
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   488
  bool Config.T"} \\
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   489
  @{index_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) ->
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   490
  int Config.T"} \\
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   491
  @{index_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) ->
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   492
  real Config.T"} \\
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   493
  @{index_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) ->
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   494
  string Config.T"} \\
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   495
  \end{mldecls}
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   496
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   497
  \<^descr> \<^ML>\<open>Config.get\<close>~\<open>ctxt config\<close> gets the value of \<open>config\<close> in the given
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   498
  context.
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   499
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   500
  \<^descr> \<^ML>\<open>Config.map\<close>~\<open>config f ctxt\<close> updates the context by updating the value
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   501
  of \<open>config\<close>.
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   502
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   503
  \<^descr> \<open>config =\<close>~\<^ML>\<open>Attrib.setup_config_bool\<close>~\<open>name default\<close> creates a named
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   504
  configuration option of type \<^ML_type>\<open>bool\<close>, with the given \<open>default\<close>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   505
  depending on the application context. The resulting \<open>config\<close> can be used to
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   506
  get/map its value in a given context. There is an implicit update of the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   507
  background theory that registers the option as attribute with some concrete
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   508
  syntax.
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   509
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   510
  \<^descr> \<^ML>\<open>Attrib.config_int\<close>, \<^ML>\<open>Attrib.config_real\<close>, and \<^ML>\<open>Attrib.config_string\<close> work like \<^ML>\<open>Attrib.config_bool\<close>, but for types
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   511
  \<^ML_type>\<open>int\<close> and \<^ML_type>\<open>string\<close>, respectively.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   512
\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   513
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   514
text %mlex \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   515
  The following example shows how to declare and use a Boolean configuration
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   516
  option called \<open>my_flag\<close> with constant default value \<^ML>\<open>false\<close>.
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   517
\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   518
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   519
ML \<open>
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   520
  val my_flag =
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   521
    Attrib.setup_config_bool \<^binding>\<open>my_flag\<close> (K false)
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   522
\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   523
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   524
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   525
  Now the user can refer to @{attribute my_flag} in declarations, while ML
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   526
  tools can retrieve the current value from the context via \<^ML>\<open>Config.get\<close>.
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   527
\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   528
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   529
ML_val \<open>\<^assert> (Config.get \<^context> my_flag = false)\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   530
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   531
declare [[my_flag = true]]
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   532
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   533
ML_val \<open>\<^assert> (Config.get \<^context> my_flag = true)\<close>
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   534
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40628
diff changeset
   535
notepad
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40628
diff changeset
   536
begin
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   537
  {
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   538
    note [[my_flag = false]]
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   539
    ML_val \<open>\<^assert> (Config.get \<^context> my_flag = false)\<close>
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   540
  }
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   541
  ML_val \<open>\<^assert> (Config.get \<^context> my_flag = true)\<close>
40964
482a8334ee9e prefer 'notepad' over 'example_proof';
wenzelm
parents: 40628
diff changeset
   542
end
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   543
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   544
text \<open>
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   545
  Here is another example involving ML type \<^ML_type>\<open>real\<close> (floating-point
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   546
  numbers).
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   547
\<close>
40291
012ed4426fda support for real valued configuration options;
wenzelm
parents: 40241
diff changeset
   548
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   549
ML \<open>
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42510
diff changeset
   550
  val airspeed_velocity =
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   551
    Attrib.setup_config_real \<^binding>\<open>airspeed_velocity\<close> (K 0.0)
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   552
\<close>
40291
012ed4426fda support for real valued configuration options;
wenzelm
parents: 40241
diff changeset
   553
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40291
diff changeset
   554
declare [[airspeed_velocity = 10]]
40291
012ed4426fda support for real valued configuration options;
wenzelm
parents: 40241
diff changeset
   555
declare [[airspeed_velocity = 9.9]]
012ed4426fda support for real valued configuration options;
wenzelm
parents: 40241
diff changeset
   556
39865
a724b90f951e more on "Configuration options";
wenzelm
parents: 39864
diff changeset
   557
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   558
section \<open>Names \label{sec:names}\<close>
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   559
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   560
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   561
  In principle, a name is just a string, but there are various conventions for
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   562
  representing additional structure. For example, ``\<open>Foo.bar.baz\<close>'' is
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   563
  considered as a long name consisting of qualifier \<open>Foo.bar\<close> and base name
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   564
  \<open>baz\<close>. The individual constituents of a name may have further substructure,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   565
  e.g.\ the string ``\<^verbatim>\<open>\<alpha>\<close>'' encodes as a single symbol (\secref{sec:symbols}).
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   566
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   567
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   568
  Subsequently, we shall introduce specific categories of names. Roughly
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   569
  speaking these correspond to logical entities as follows:
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   570
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   571
  \<^item> Basic names (\secref{sec:basic-name}): free and bound variables.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   572
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   573
  \<^item> Indexed names (\secref{sec:indexname}): schematic variables.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   574
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   575
  \<^item> Long names (\secref{sec:long-name}): constants of any kind (type
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   576
  constructors, term constants, other concepts defined in user space). Such
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   577
  entities are typically managed via name spaces (\secref{sec:name-space}).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   578
\<close>
20437
wenzelm
parents: 20430
diff changeset
   579
wenzelm
parents: 20430
diff changeset
   580
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   581
subsection \<open>Basic names \label{sec:basic-name}\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   582
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   583
text \<open>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   584
  A \<^emph>\<open>basic name\<close> essentially consists of a single Isabelle identifier. There
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   585
  are conventions to mark separate classes of basic names, by attaching a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   586
  suffix of underscores: one underscore means \<^emph>\<open>internal name\<close>, two
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   587
  underscores means \<^emph>\<open>Skolem name\<close>, three underscores means \<^emph>\<open>internal Skolem
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   588
  name\<close>.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   589
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   590
  For example, the basic name \<open>foo\<close> has the internal version \<open>foo_\<close>, with
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   591
  Skolem versions \<open>foo__\<close> and \<open>foo___\<close>, respectively.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   592
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   593
  These special versions provide copies of the basic name space, apart from
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   594
  anything that normally appears in the user text. For example, system
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   595
  generated variables in Isar proof contexts are usually marked as internal,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   596
  which prevents mysterious names like \<open>xaa\<close> to appear in human-readable text.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   597
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   598
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   599
  Manipulating binding scopes often requires on-the-fly renamings. A \<^emph>\<open>name
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   600
  context\<close> contains a collection of already used names. The \<open>declare\<close>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   601
  operation adds names to the context.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   602
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   603
  The \<open>invents\<close> operation derives a number of fresh names from a given
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   604
  starting point. For example, the first three names derived from \<open>a\<close> are \<open>a\<close>,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   605
  \<open>b\<close>, \<open>c\<close>.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   606
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   607
  The \<open>variants\<close> operation produces fresh names by incrementing tentative
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   608
  names as base-26 numbers (with digits \<open>a..z\<close>) until all clashes are
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   609
  resolved. For example, name \<open>foo\<close> results in variants \<open>fooa\<close>, \<open>foob\<close>,
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   610
  \<open>fooc\<close>, \dots, \<open>fooaa\<close>, \<open>fooab\<close> etc.; each renaming step picks the next
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   611
  unused variant from this sequence.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   612
\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   613
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   614
text %mlref \<open>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   615
  \begin{mldecls}
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   616
  @{index_ML Name.internal: "string -> string"} \\
20547
wenzelm
parents: 20530
diff changeset
   617
  @{index_ML Name.skolem: "string -> string"} \\
wenzelm
parents: 20530
diff changeset
   618
  \end{mldecls}
wenzelm
parents: 20530
diff changeset
   619
  \begin{mldecls}
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   620
  @{index_ML_type Name.context} \\
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   621
  @{index_ML Name.context: Name.context} \\
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   622
  @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   623
  @{index_ML Name.invent: "Name.context -> string -> int -> string list"} \\
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 42616
diff changeset
   624
  @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   625
  \end{mldecls}
34926
19294b07e445 Variable.names_of;
wenzelm
parents: 34925
diff changeset
   626
  \begin{mldecls}
19294b07e445 Variable.names_of;
wenzelm
parents: 34925
diff changeset
   627
  @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\
19294b07e445 Variable.names_of;
wenzelm
parents: 34925
diff changeset
   628
  \end{mldecls}
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   629
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   630
  \<^descr> \<^ML>\<open>Name.internal\<close>~\<open>name\<close> produces an internal name by adding one
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   631
  underscore.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   632
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   633
  \<^descr> \<^ML>\<open>Name.skolem\<close>~\<open>name\<close> produces a Skolem name by adding two underscores.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   634
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   635
  \<^descr> Type \<^ML_type>\<open>Name.context\<close> represents the context of already used names;
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   636
  the initial value is \<^ML>\<open>Name.context\<close>.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   637
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   638
  \<^descr> \<^ML>\<open>Name.declare\<close>~\<open>name\<close> enters a used name into the context.
20437
wenzelm
parents: 20430
diff changeset
   639
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   640
  \<^descr> \<^ML>\<open>Name.invent\<close>~\<open>context name n\<close> produces \<open>n\<close> fresh names derived from
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   641
  \<open>name\<close>.
20488
wenzelm
parents: 20479
diff changeset
   642
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   643
  \<^descr> \<^ML>\<open>Name.variant\<close>~\<open>name context\<close> produces a fresh variant of \<open>name\<close>; the
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   644
  result is declared to the context.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   645
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   646
  \<^descr> \<^ML>\<open>Variable.names_of\<close>~\<open>ctxt\<close> retrieves the context of declared type and
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   647
  term variable names. Projecting a proof context down to a primitive name
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   648
  context is occasionally useful when invoking lower-level operations. Regular
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   649
  management of ``fresh variables'' is done by suitable operations of
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   650
  structure \<^ML_structure>\<open>Variable\<close>, which is also able to provide an
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   651
  official status of ``locally fixed variable'' within the logical environment
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   652
  (cf.\ \secref{sec:variables}).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   653
\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   654
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   655
text %mlex \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   656
  The following simple examples demonstrate how to produce fresh names from
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   657
  the initial \<^ML>\<open>Name.context\<close>.
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   658
\<close>
39857
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   659
59902
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   660
ML_val \<open>
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   661
  val list1 = Name.invent Name.context "a" 5;
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   662
  \<^assert> (list1 = ["a", "b", "c", "d", "e"]);
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   663
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   664
  val list2 =
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 42616
diff changeset
   665
    #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context);
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   666
  \<^assert> (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   667
\<close>
39857
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   668
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   669
text \<open>
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   670
  \<^medskip>
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   671
  The same works relatively to the formal context as follows.\<close>
39857
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   672
59902
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   673
experiment fixes a b c :: 'a
39857
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   674
begin
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   675
59902
6afbe5a99139 misc tuning -- keep name space more clean;
wenzelm
parents: 59859
diff changeset
   676
ML_val \<open>
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   677
  val names = Variable.names_of \<^context>;
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   678
43329
84472e198515 tuned signature: Name.invent and Name.invent_names;
wenzelm
parents: 43326
diff changeset
   679
  val list1 = Name.invent names "a" 5;
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   680
  \<^assert> (list1 = ["d", "e", "f", "g", "h"]);
39866
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   681
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents: 39865
diff changeset
   682
  val list2 =
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 42616
diff changeset
   683
    #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] names);
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   684
  \<^assert> (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]);
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   685
\<close>
39857
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   686
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   687
end
ea93e088398d more examples;
wenzelm
parents: 39846
diff changeset
   688
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   689
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   690
subsection \<open>Indexed names \label{sec:indexname}\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   691
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   692
text \<open>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   693
  An \<^emph>\<open>indexed name\<close> (or \<open>indexname\<close>) is a pair of a basic name and a natural
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   694
  number. This representation allows efficient renaming by incrementing the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   695
  second component only. The canonical way to rename two collections of
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   696
  indexnames apart from each other is this: determine the maximum index
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   697
  \<open>maxidx\<close> of the first collection, then increment all indexes of the second
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   698
  collection by \<open>maxidx + 1\<close>; the maximum index of an empty collection is
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   699
  \<open>-1\<close>.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   700
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   701
  Occasionally, basic names are injected into the same pair type of indexed
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   702
  names: then \<open>(x, -1)\<close> is used to encode the basic name \<open>x\<close>.
20488
wenzelm
parents: 20479
diff changeset
   703
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   704
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   705
  Isabelle syntax observes the following rules for representing an indexname
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   706
  \<open>(x, i)\<close> as a packed string:
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   707
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   708
    \<^item> \<open>?x\<close> if \<open>x\<close> does not end with a digit and \<open>i = 0\<close>,
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   709
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   710
    \<^item> \<open>?xi\<close> if \<open>x\<close> does not end with a digit,
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   711
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   712
    \<^item> \<open>?x.i\<close> otherwise.
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20452
diff changeset
   713
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   714
  Indexnames may acquire large index numbers after several maxidx shifts have
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   715
  been applied. Results are usually normalized towards \<open>0\<close> at certain
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   716
  checkpoints, notably at the end of a proof. This works by producing variants
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   717
  of the corresponding basic name components. For example, the collection
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   718
  \<open>?x1, ?x7, ?x42\<close> becomes \<open>?x, ?xa, ?xb\<close>.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   719
\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   720
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   721
text %mlref \<open>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   722
  \begin{mldecls}
39861
b8d89db3e238 use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents: 39857
diff changeset
   723
  @{index_ML_type indexname: "string * int"} \\
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   724
  \end{mldecls}
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   725
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   726
  \<^descr> Type \<^ML_type>\<open>indexname\<close> represents indexed names. This is an
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   727
  abbreviation for \<^ML_type>\<open>string * int\<close>. The second component is usually
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   728
  non-negative, except for situations where \<open>(x, -1)\<close> is used to inject basic
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   729
  names into this type. Other negative indexes should not be used.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   730
\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   731
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   732
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   733
subsection \<open>Long names \label{sec:long-name}\<close>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   734
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   735
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   736
  A \<^emph>\<open>long name\<close> consists of a sequence of non-empty name components. The
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   737
  packed representation uses a dot as separator, as in ``\<open>A.b.c\<close>''. The last
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   738
  component is called \<^emph>\<open>base name\<close>, the remaining prefix is called
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   739
  \<^emph>\<open>qualifier\<close> (which may be empty). The qualifier can be understood as the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   740
  access path to the named entity while passing through some nested
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   741
  block-structure, although our free-form long names do not really enforce any
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   742
  strict discipline.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   743
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   744
  For example, an item named ``\<open>A.b.c\<close>'' may be understood as a local entity
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   745
  \<open>c\<close>, within a local structure \<open>b\<close>, within a global structure \<open>A\<close>. In
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   746
  practice, long names usually represent 1--3 levels of qualification. User ML
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   747
  code should not make any assumptions about the particular structure of long
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   748
  names!
20437
wenzelm
parents: 20430
diff changeset
   749
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   750
  The empty name is commonly used as an indication of unnamed entities, or
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   751
  entities that are not entered into the corresponding name space, whenever
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   752
  this makes any sense. The basic operations on long names map empty names
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   753
  again to empty names.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   754
\<close>
20437
wenzelm
parents: 20430
diff changeset
   755
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   756
text %mlref \<open>
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   757
  \begin{mldecls}
30365
790129514c2d adapted to structure Long_Name;
wenzelm
parents: 30281
diff changeset
   758
  @{index_ML Long_Name.base_name: "string -> string"} \\
790129514c2d adapted to structure Long_Name;
wenzelm
parents: 30281
diff changeset
   759
  @{index_ML Long_Name.qualifier: "string -> string"} \\
790129514c2d adapted to structure Long_Name;
wenzelm
parents: 30281
diff changeset
   760
  @{index_ML Long_Name.append: "string -> string -> string"} \\
790129514c2d adapted to structure Long_Name;
wenzelm
parents: 30281
diff changeset
   761
  @{index_ML Long_Name.implode: "string list -> string"} \\
790129514c2d adapted to structure Long_Name;
wenzelm
parents: 30281
diff changeset
   762
  @{index_ML Long_Name.explode: "string -> string list"} \\
20547
wenzelm
parents: 20530
diff changeset
   763
  \end{mldecls}
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   764
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   765
  \<^descr> \<^ML>\<open>Long_Name.base_name\<close>~\<open>name\<close> returns the base name of a long name.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   766
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   767
  \<^descr> \<^ML>\<open>Long_Name.qualifier\<close>~\<open>name\<close> returns the qualifier of a long name.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   768
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   769
  \<^descr> \<^ML>\<open>Long_Name.append\<close>~\<open>name\<^sub>1 name\<^sub>2\<close> appends two long names.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   770
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   771
  \<^descr> \<^ML>\<open>Long_Name.implode\<close>~\<open>names\<close> and \<^ML>\<open>Long_Name.explode\<close>~\<open>name\<close> convert
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   772
  between the packed string representation and the explicit list form of long
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   773
  names.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   774
\<close>
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   775
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   776
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   777
subsection \<open>Name spaces \label{sec:name-space}\<close>
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   778
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   779
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   780
  A \<open>name space\<close> manages a collection of long names, together with a mapping
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   781
  between partially qualified external names and fully qualified internal
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   782
  names (in both directions). Note that the corresponding \<open>intern\<close> and
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   783
  \<open>extern\<close> operations are mostly used for parsing and printing only! The
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   784
  \<open>declare\<close> operation augments a name space according to the accesses
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   785
  determined by a given binding, and a naming policy from the context.
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   786
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   787
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   788
  A \<open>binding\<close> specifies details about the prospective long name of a newly
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   789
  introduced formal entity. It consists of a base name, prefixes for
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   790
  qualification (separate ones for system infrastructure and user-space
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   791
  mechanisms), a slot for the original source position, and some additional
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   792
  flags.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   793
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   794
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   795
  A \<open>naming\<close> provides some additional details for producing a long name from a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   796
  binding. Normally, the naming is implicit in the theory or proof context.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   797
  The \<open>full\<close> operation (and its variants for different context types) produces
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   798
  a fully qualified internal name to be entered into a name space. The main
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   799
  equation of this ``chemical reaction'' when binding new entities in a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   800
  context is as follows:
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   801
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   802
  \<^medskip>
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   803
  \begin{tabular}{l}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   804
  \<open>binding + naming \<longrightarrow> long name + name space accesses\<close>
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   805
  \end{tabular}
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   806
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   807
  \<^bigskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   808
  As a general principle, there is a separate name space for each kind of
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   809
  formal entity, e.g.\ fact, logical constant, type constructor, type class.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   810
  It is usually clear from the occurrence in concrete syntax (or from the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   811
  scope) which kind of entity a name refers to. For example, the very same
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   812
  name \<open>c\<close> may be used uniformly for a constant, type constructor, and type
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   813
  class.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   814
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   815
  There are common schemes to name derived entities systematically according
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   816
  to the name of the main logical entity involved, e.g.\ fact \<open>c.intro\<close> for a
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   817
  canonical introduction rule related to constant \<open>c\<close>. This technique of
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   818
  mapping names from one space into another requires some care in order to
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   819
  avoid conflicts. In particular, theorem names derived from a type
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   820
  constructor or type class should get an additional suffix in addition to the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   821
  usual qualification. This leads to the following conventions for derived
39839
08f59175e541 misc tuning;
wenzelm
parents: 39837
diff changeset
   822
  names:
08f59175e541 misc tuning;
wenzelm
parents: 39837
diff changeset
   823
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   824
  \<^medskip>
39839
08f59175e541 misc tuning;
wenzelm
parents: 39837
diff changeset
   825
  \begin{tabular}{ll}
08f59175e541 misc tuning;
wenzelm
parents: 39837
diff changeset
   826
  logical entity & fact name \\\hline
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   827
  constant \<open>c\<close> & \<open>c.intro\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   828
  type \<open>c\<close> & \<open>c_type.intro\<close> \\
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   829
  class \<open>c\<close> & \<open>c_class.intro\<close> \\
39839
08f59175e541 misc tuning;
wenzelm
parents: 39837
diff changeset
   830
  \end{tabular}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   831
\<close>
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   832
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   833
text %mlref \<open>
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   834
  \begin{mldecls}
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   835
  @{index_ML_type binding} \\
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   836
  @{index_ML Binding.empty: binding} \\
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   837
  @{index_ML Binding.name: "string -> binding"} \\
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   838
  @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   839
  @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 58742
diff changeset
   840
  @{index_ML Binding.concealed: "binding -> binding"} \\
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 43329
diff changeset
   841
  @{index_ML Binding.print: "binding -> string"} \\
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   842
  \end{mldecls}
20547
wenzelm
parents: 20530
diff changeset
   843
  \begin{mldecls}
33174
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   844
  @{index_ML_type Name_Space.naming} \\
58668
1891f17c6124 tuned signature;
wenzelm
parents: 58618
diff changeset
   845
  @{index_ML Name_Space.global_naming: Name_Space.naming} \\
33174
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   846
  @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   847
  @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\
20547
wenzelm
parents: 20530
diff changeset
   848
  \end{mldecls}
wenzelm
parents: 20530
diff changeset
   849
  \begin{mldecls}
33174
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   850
  @{index_ML_type Name_Space.T} \\
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   851
  @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   852
  @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
47174
b9b2e183e94d updated Sign.add_type, Name_Space.declare;
wenzelm
parents: 46484
diff changeset
   853
  @{index_ML Name_Space.declare: "Context.generic -> bool ->
b9b2e183e94d updated Sign.add_type, Name_Space.declare;
wenzelm
parents: 46484
diff changeset
   854
  binding -> Name_Space.T -> string * Name_Space.T"} \\
33174
1f2051f41335 adjusted to changes in corresponding ML code
haftmann
parents: 30365
diff changeset
   855
  @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 40964
diff changeset
   856
  @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   857
  @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   858
  \end{mldecls}
20437
wenzelm
parents: 20430
diff changeset
   859
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   860
  \<^descr> Type \<^ML_type>\<open>binding\<close> represents the abstract concept of name bindings.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   861
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   862
  \<^descr> \<^ML>\<open>Binding.empty\<close> is the empty binding.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   863
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   864
  \<^descr> \<^ML>\<open>Binding.name\<close>~\<open>name\<close> produces a binding with base name \<open>name\<close>. Note
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   865
  that this lacks proper source position information; see also the ML
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   866
  antiquotation @{ML_antiquotation binding}.
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   867
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   868
  \<^descr> \<^ML>\<open>Binding.qualify\<close>~\<open>mandatory name binding\<close> prefixes qualifier \<open>name\<close>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   869
  to \<open>binding\<close>. The \<open>mandatory\<close> flag tells if this name component always needs
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   870
  to be given in name space accesses --- this is mostly \<open>false\<close> in practice.
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   871
  Note that this part of qualification is typically used in derived
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   872
  specification mechanisms.
20437
wenzelm
parents: 20430
diff changeset
   873
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   874
  \<^descr> \<^ML>\<open>Binding.prefix\<close> is similar to \<^ML>\<open>Binding.qualify\<close>, but affects the
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   875
  system prefix. This part of extra qualification is typically used in the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   876
  infrastructure for modular specifications, notably ``local theory targets''
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   877
  (see also \chref{ch:local-theory}).
20437
wenzelm
parents: 20430
diff changeset
   878
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   879
  \<^descr> \<^ML>\<open>Binding.concealed\<close>~\<open>binding\<close> indicates that the binding shall refer
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   880
  to an entity that serves foundational purposes only. This flag helps to mark
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   881
  implementation details of specification mechanism etc. Other tools should
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   882
  not depend on the particulars of concealed entities (cf.\ \<^ML>\<open>Name_Space.is_concealed\<close>).
34927
c4c02ac736a6 more details on long names, binding/naming, name space;
wenzelm
parents: 34926
diff changeset
   883
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   884
  \<^descr> \<^ML>\<open>Binding.print\<close>~\<open>binding\<close> produces a string representation for
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   885
  human-readable output, together with some formal markup that might get used
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   886
  in GUI front-ends, for example.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   887
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   888
  \<^descr> Type \<^ML_type>\<open>Name_Space.naming\<close> represents the abstract concept of a
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   889
  naming policy.
20437
wenzelm
parents: 20430
diff changeset
   890
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   891
  \<^descr> \<^ML>\<open>Name_Space.global_naming\<close> is the default naming policy: it is global
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   892
  and lacks any path prefix. In a regular theory context this is augmented by
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   893
  a path prefix consisting of the theory name.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   894
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   895
  \<^descr> \<^ML>\<open>Name_Space.add_path\<close>~\<open>path naming\<close> augments the naming policy by
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   896
  extending its path component.
20437
wenzelm
parents: 20430
diff changeset
   897
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   898
  \<^descr> \<^ML>\<open>Name_Space.full_name\<close>~\<open>naming binding\<close> turns a name binding (usually
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   899
  a basic name) into the fully qualified internal name, according to the given
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   900
  naming policy.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   901
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   902
  \<^descr> Type \<^ML_type>\<open>Name_Space.T\<close> represents name spaces.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   903
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   904
  \<^descr> \<^ML>\<open>Name_Space.empty\<close>~\<open>kind\<close> and \<^ML>\<open>Name_Space.merge\<close>~\<open>(space\<^sub>1,
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   905
  space\<^sub>2)\<close> are the canonical operations for maintaining name spaces according
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   906
  to theory data management (\secref{sec:context-data}); \<open>kind\<close> is a formal
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   907
  comment to characterize the purpose of a name space.
20437
wenzelm
parents: 20430
diff changeset
   908
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   909
  \<^descr> \<^ML>\<open>Name_Space.declare\<close>~\<open>context strict binding space\<close> enters a name
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   910
  binding as fully qualified internal name into the name space, using the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   911
  naming of the context.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   912
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   913
  \<^descr> \<^ML>\<open>Name_Space.intern\<close>~\<open>space name\<close> internalizes a (partially qualified)
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   914
  external name.
20437
wenzelm
parents: 20430
diff changeset
   915
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   916
  This operation is mostly for parsing! Note that fully qualified names
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   917
  stemming from declarations are produced via \<^ML>\<open>Name_Space.full_name\<close> and
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   918
  \<^ML>\<open>Name_Space.declare\<close> (or their derivatives for \<^ML_type>\<open>theory\<close> and
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   919
  \<^ML_type>\<open>Proof.context\<close>).
20437
wenzelm
parents: 20430
diff changeset
   920
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   921
  \<^descr> \<^ML>\<open>Name_Space.extern\<close>~\<open>ctxt space name\<close> externalizes a (fully qualified)
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   922
  internal name.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   923
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   924
  This operation is mostly for printing! User code should not rely on the
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   925
  precise result too much.
20476
6d3f144cc1bd more on names;
wenzelm
parents: 20475
diff changeset
   926
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   927
  \<^descr> \<^ML>\<open>Name_Space.is_concealed\<close>~\<open>space name\<close> indicates whether \<open>name\<close> refers
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   928
  to a strictly private entity that other tools are supposed to ignore!
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   929
\<close>
30272
2d612824e642 regenerated document;
wenzelm
parents: 30270
diff changeset
   930
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   931
text %mlantiq \<open>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   932
  \begin{matharray}{rcl}
61493
0debd22f0c0e isabelle update_cartouches -t;
wenzelm
parents: 61477
diff changeset
   933
  @{ML_antiquotation_def "binding"} & : & \<open>ML_antiquotation\<close> \\
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   934
  \end{matharray}
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   935
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   936
  \<^rail>\<open>
67146
909dcdec2122 more embedded cartouche arguments;
wenzelm
parents: 62969
diff changeset
   937
  @@{ML_antiquotation binding} embedded
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   938
  \<close>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   939
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   940
  \<^descr> \<open>@{binding name}\<close> produces a binding with base name \<open>name\<close> and the source
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   941
  position taken from the concrete syntax of this antiquotation. In many
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   942
  situations this is more appropriate than the more basic \<^ML>\<open>Binding.name\<close>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   943
  function.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   944
\<close>
39832
1080dee73a53 various concrete ML antiquotations;
wenzelm
parents: 39825
diff changeset
   945
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   946
text %mlex \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   947
  The following example yields the source position of some concrete binding
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   948
  inlined into the text:
58618
782f0b662cae more cartouches;
wenzelm
parents: 58555
diff changeset
   949
\<close>
39833
6d54a48c859d more examples;
wenzelm
parents: 39832
diff changeset
   950
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   951
ML_val \<open>Binding.pos_of \<^binding>\<open>here\<close>\<close>
39833
6d54a48c859d more examples;
wenzelm
parents: 39832
diff changeset
   952
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   953
text \<open>
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   954
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   955
  That position can be also printed in a message as follows:
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   956
\<close>
39833
6d54a48c859d more examples;
wenzelm
parents: 39832
diff changeset
   957
58742
bb55a3530709 tuned spacing;
wenzelm
parents: 58723
diff changeset
   958
ML_command
bb55a3530709 tuned spacing;
wenzelm
parents: 58723
diff changeset
   959
  \<open>writeln
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   960
    ("Look here" ^ Position.here (Binding.pos_of \<^binding>\<open>here\<close>))\<close>
39833
6d54a48c859d more examples;
wenzelm
parents: 39832
diff changeset
   961
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   962
text \<open>
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   963
  This illustrates a key virtue of formalized bindings as opposed to raw
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   964
  specifications of base names: the system can use this additional information
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   965
  for feedback given to the user (error messages etc.).
56071
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 55837
diff changeset
   966
61416
b9a3324e4e62 more symbols;
wenzelm
parents: 61046
diff changeset
   967
  \<^medskip>
61854
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   968
  The following example refers to its source position directly, which is
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   969
  occasionally useful for experimentation and diagnostic purposes:
38b049cd3aad tuned whitespace;
wenzelm
parents: 61656
diff changeset
   970
\<close>
56071
2ffdedb0c044 added ML antiquotation @{here};
wenzelm
parents: 55837
diff changeset
   971
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69298
diff changeset
   972
ML_command \<open>warning ("Look here" ^ Position.here \<^here>)\<close>
39833
6d54a48c859d more examples;
wenzelm
parents: 39832
diff changeset
   973
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   974
end