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