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