doc-src/IsarImplementation/Thy/document/prelim.tex
author wenzelm
Tue Sep 05 16:42:32 2006 +0200 (2006-09-05 ago)
changeset 20477 e623b0e30541
parent 20475 a04bf731ceb6
child 20481 c96f80442ce6
permissions -rw-r--r--
tuned;
wenzelm@18537
     1
%
wenzelm@18537
     2
\begin{isabellebody}%
wenzelm@18537
     3
\def\isabellecontext{prelim}%
wenzelm@18537
     4
%
wenzelm@18537
     5
\isadelimtheory
wenzelm@18537
     6
\isanewline
wenzelm@18537
     7
\isanewline
wenzelm@18537
     8
\isanewline
wenzelm@18537
     9
%
wenzelm@18537
    10
\endisadelimtheory
wenzelm@18537
    11
%
wenzelm@18537
    12
\isatagtheory
wenzelm@18537
    13
\isacommand{theory}\isamarkupfalse%
wenzelm@18537
    14
\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
wenzelm@18537
    15
\endisatagtheory
wenzelm@18537
    16
{\isafoldtheory}%
wenzelm@18537
    17
%
wenzelm@18537
    18
\isadelimtheory
wenzelm@18537
    19
%
wenzelm@18537
    20
\endisadelimtheory
wenzelm@18537
    21
%
wenzelm@18537
    22
\isamarkupchapter{Preliminaries%
wenzelm@18537
    23
}
wenzelm@18537
    24
\isamarkuptrue%
wenzelm@18537
    25
%
wenzelm@20429
    26
\isamarkupsection{Contexts \label{sec:context}%
wenzelm@18537
    27
}
wenzelm@18537
    28
\isamarkuptrue%
wenzelm@18537
    29
%
wenzelm@18537
    30
\begin{isamarkuptext}%
wenzelm@20451
    31
A logical context represents the background that is required for
wenzelm@20451
    32
  formulating statements and composing proofs.  It acts as a medium to
wenzelm@20451
    33
  produce formal content, depending on earlier material (declarations,
wenzelm@20451
    34
  results etc.).
wenzelm@18537
    35
wenzelm@20451
    36
  For example, derivations within the Isabelle/Pure logic can be
wenzelm@20451
    37
  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
wenzelm@20429
    38
  proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
wenzelm@20429
    39
  within the theory \isa{{\isasymTheta}}.  There are logical reasons for
wenzelm@20451
    40
  keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
wenzelm@20451
    41
  liberal about supporting type constructors and schematic
wenzelm@20451
    42
  polymorphism of constants and axioms, while the inner calculus of
wenzelm@20451
    43
  \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with
wenzelm@20451
    44
  fixed type variables in the assumptions).
wenzelm@18537
    45
wenzelm@20429
    46
  \medskip Contexts and derivations are linked by the following key
wenzelm@20429
    47
  principles:
wenzelm@20429
    48
wenzelm@20429
    49
  \begin{itemize}
wenzelm@20429
    50
wenzelm@20429
    51
  \item Transfer: monotonicity of derivations admits results to be
wenzelm@20451
    52
  transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
wenzelm@20429
    53
wenzelm@20429
    54
  \item Export: discharge of hypotheses admits results to be exported
wenzelm@20451
    55
  into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
wenzelm@20451
    56
  implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
wenzelm@20451
    57
  \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}.  Note that \isa{{\isasymTheta}} remains unchanged here,
wenzelm@20451
    58
  only the \isa{{\isasymGamma}} part is affected.
wenzelm@18537
    59
wenzelm@20429
    60
  \end{itemize}
wenzelm@18537
    61
wenzelm@20451
    62
  \medskip By modeling the main characteristics of the primitive
wenzelm@20451
    63
  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any
wenzelm@20451
    64
  particular logical content, we arrive at the fundamental notions of
wenzelm@20451
    65
  \emph{theory context} and \emph{proof context} in Isabelle/Isar.
wenzelm@20451
    66
  These implement a certain policy to manage arbitrary \emph{context
wenzelm@20451
    67
  data}.  There is a strongly-typed mechanism to declare new kinds of
wenzelm@20429
    68
  data at compile time.
wenzelm@18537
    69
wenzelm@20451
    70
  The internal bootstrap process of Isabelle/Pure eventually reaches a
wenzelm@20451
    71
  stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!
wenzelm@20451
    72
  Various additional data slots support all kinds of mechanisms that
wenzelm@20451
    73
  are not necessarily part of the core logic.
wenzelm@18537
    74
wenzelm@20429
    75
  For example, there would be data for canonical introduction and
wenzelm@20429
    76
  elimination rules for arbitrary operators (depending on the
wenzelm@20429
    77
  object-logic and application), which enables users to perform
wenzelm@20451
    78
  standard proof steps implicitly (cf.\ the \isa{rule} method
wenzelm@20451
    79
  \cite{isabelle-isar-ref}).
wenzelm@18537
    80
wenzelm@20451
    81
  \medskip Thus Isabelle/Isar is able to bring forth more and more
wenzelm@20451
    82
  concepts successively.  In particular, an object-logic like
wenzelm@20451
    83
  Isabelle/HOL continues the Isabelle/Pure setup by adding specific
wenzelm@20451
    84
  components for automated reasoning (classical reasoner, tableau
wenzelm@20451
    85
  prover, structured induction etc.) and derived specification
wenzelm@20451
    86
  mechanisms (inductive predicates, recursive functions etc.).  All of
wenzelm@20451
    87
  this is ultimately based on the generic data management by theory
wenzelm@20451
    88
  and proof contexts introduced here.%
wenzelm@18537
    89
\end{isamarkuptext}%
wenzelm@18537
    90
\isamarkuptrue%
wenzelm@18537
    91
%
wenzelm@18537
    92
\isamarkupsubsection{Theory context \label{sec:context-theory}%
wenzelm@18537
    93
}
wenzelm@18537
    94
\isamarkuptrue%
wenzelm@18537
    95
%
wenzelm@18537
    96
\begin{isamarkuptext}%
wenzelm@20447
    97
\glossary{Theory}{FIXME}
wenzelm@20447
    98
wenzelm@20451
    99
  A \emph{theory} is a data container with explicit named and unique
wenzelm@20451
   100
  identifier.  Theories are related by a (nominal) sub-theory
wenzelm@20451
   101
  relation, which corresponds to the dependency graph of the original
wenzelm@20451
   102
  construction; each theory is derived from a certain sub-graph of
wenzelm@20451
   103
  ancestor theories.
wenzelm@20451
   104
wenzelm@20451
   105
  The \isa{merge} operation produces the least upper bound of two
wenzelm@20451
   106
  theories, which actually degenerates into absorption of one theory
wenzelm@20451
   107
  into the other (due to the nominal sub-theory relation).
wenzelm@18537
   108
wenzelm@20429
   109
  The \isa{begin} operation starts a new theory by importing
wenzelm@20429
   110
  several parent theories and entering a special \isa{draft} mode,
wenzelm@20429
   111
  which is sustained until the final \isa{end} operation.  A draft
wenzelm@20451
   112
  theory acts like a linear type, where updates invalidate earlier
wenzelm@20451
   113
  versions.  An invalidated draft is called ``stale''.
wenzelm@20429
   114
wenzelm@20447
   115
  The \isa{checkpoint} operation produces an intermediate stepping
wenzelm@20451
   116
  stone that will survive the next update: both the original and the
wenzelm@20451
   117
  changed theory remain valid and are related by the sub-theory
wenzelm@20451
   118
  relation.  Checkpointing essentially recovers purely functional
wenzelm@20451
   119
  theory values, at the expense of some extra internal bookkeeping.
wenzelm@20447
   120
wenzelm@20447
   121
  The \isa{copy} operation produces an auxiliary version that has
wenzelm@20447
   122
  the same data content, but is unrelated to the original: updates of
wenzelm@20447
   123
  the copy do not affect the original, neither does the sub-theory
wenzelm@20447
   124
  relation hold.
wenzelm@20429
   125
wenzelm@20447
   126
  \medskip The example in \figref{fig:ex-theory} below shows a theory
wenzelm@20451
   127
  graph derived from \isa{Pure}, with theory \isa{Length}
wenzelm@20451
   128
  importing \isa{Nat} and \isa{List}.  The body of \isa{Length} consists of a sequence of updates, working mostly on
wenzelm@20451
   129
  drafts.  Intermediate checkpoints may occur as well, due to the
wenzelm@20451
   130
  history mechanism provided by the Isar top-level, cf.\
wenzelm@20451
   131
  \secref{sec:isar-toplevel}.
wenzelm@20447
   132
wenzelm@20447
   133
  \begin{figure}[htb]
wenzelm@20447
   134
  \begin{center}
wenzelm@20429
   135
  \begin{tabular}{rcccl}
wenzelm@20447
   136
        &            & \isa{Pure} \\
wenzelm@20447
   137
        &            & \isa{{\isasymdown}} \\
wenzelm@20447
   138
        &            & \isa{FOL} \\
wenzelm@18537
   139
        & $\swarrow$ &              & $\searrow$ & \\
wenzelm@20447
   140
  $Nat$ &            &              &            & \isa{List} \\
wenzelm@18537
   141
        & $\searrow$ &              & $\swarrow$ \\
wenzelm@20447
   142
        &            & \isa{Length} \\
wenzelm@18537
   143
        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
wenzelm@18537
   144
        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
wenzelm@18537
   145
        &            & $\vdots$~~ \\
wenzelm@20447
   146
        &            & \isa{{\isasymbullet}}~~ \\
wenzelm@20447
   147
        &            & $\vdots$~~ \\
wenzelm@20447
   148
        &            & \isa{{\isasymbullet}}~~ \\
wenzelm@20447
   149
        &            & $\vdots$~~ \\
wenzelm@18537
   150
        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
wenzelm@20429
   151
  \end{tabular}
wenzelm@20451
   152
  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
wenzelm@20447
   153
  \end{center}
wenzelm@20451
   154
  \end{figure}
wenzelm@20451
   155
wenzelm@20451
   156
  \medskip There is a separate notion of \emph{theory reference} for
wenzelm@20451
   157
  maintaining a live link to an evolving theory context: updates on
wenzelm@20451
   158
  drafts are propagated automatically.  The dynamic stops after an
wenzelm@20451
   159
  explicit \isa{end} only.
wenzelm@20451
   160
wenzelm@20451
   161
  Derived entities may store a theory reference in order to indicate
wenzelm@20451
   162
  the context they belong to.  This implicitly assumes monotonic
wenzelm@20451
   163
  reasoning, because the referenced context may become larger without
wenzelm@20451
   164
  further notice.%
wenzelm@18537
   165
\end{isamarkuptext}%
wenzelm@18537
   166
\isamarkuptrue%
wenzelm@18537
   167
%
wenzelm@20430
   168
\isadelimmlref
wenzelm@20430
   169
%
wenzelm@20430
   170
\endisadelimmlref
wenzelm@20430
   171
%
wenzelm@20430
   172
\isatagmlref
wenzelm@20430
   173
%
wenzelm@20430
   174
\begin{isamarkuptext}%
wenzelm@20447
   175
\begin{mldecls}
wenzelm@20447
   176
  \indexmltype{theory}\verb|type theory| \\
wenzelm@20447
   177
  \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
wenzelm@20447
   178
  \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
wenzelm@20447
   179
  \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
wenzelm@20447
   180
  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
wenzelm@20447
   181
  \indexmltype{theory-ref}\verb|type theory_ref| \\
wenzelm@20447
   182
  \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
wenzelm@20447
   183
  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
wenzelm@20447
   184
  \end{mldecls}
wenzelm@20447
   185
wenzelm@20447
   186
  \begin{description}
wenzelm@20447
   187
wenzelm@20451
   188
  \item \verb|theory| represents theory contexts.  This is
wenzelm@20451
   189
  essentially a linear type!  Most operations destroy the original
wenzelm@20451
   190
  version, which then becomes ``stale''.
wenzelm@20447
   191
wenzelm@20447
   192
  \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
wenzelm@20447
   193
  compares theories according to the inherent graph structure of the
wenzelm@20447
   194
  construction.  This sub-theory relation is a nominal approximation
wenzelm@20447
   195
  of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
wenzelm@20447
   196
wenzelm@20447
   197
  \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
wenzelm@20447
   198
  absorbs one theory into the other.  This fails for unrelated
wenzelm@20447
   199
  theories!
wenzelm@20447
   200
wenzelm@20447
   201
  \item \verb|Theory.checkpoint|~\isa{thy} produces a safe
wenzelm@20447
   202
  stepping stone in the linear development of \isa{thy}.  The next
wenzelm@20447
   203
  update will result in two related, valid theories.
wenzelm@20447
   204
wenzelm@20451
   205
  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The result is not
wenzelm@20451
   206
  related to the original; the original is unchanched.
wenzelm@20447
   207
wenzelm@20451
   208
  \item \verb|theory_ref| represents a sliding reference to an
wenzelm@20451
   209
  always valid theory; updates on the original are propagated
wenzelm@20447
   210
  automatically.
wenzelm@20447
   211
wenzelm@20449
   212
  \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|.  As the referenced theory
wenzelm@20451
   213
  evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
wenzelm@20447
   214
wenzelm@20447
   215
  \end{description}%
wenzelm@20430
   216
\end{isamarkuptext}%
wenzelm@20430
   217
\isamarkuptrue%
wenzelm@20430
   218
%
wenzelm@20430
   219
\endisatagmlref
wenzelm@20430
   220
{\isafoldmlref}%
wenzelm@20430
   221
%
wenzelm@20430
   222
\isadelimmlref
wenzelm@20430
   223
%
wenzelm@20430
   224
\endisadelimmlref
wenzelm@20430
   225
%
wenzelm@18537
   226
\isamarkupsubsection{Proof context \label{sec:context-proof}%
wenzelm@18537
   227
}
wenzelm@18537
   228
\isamarkuptrue%
wenzelm@18537
   229
%
wenzelm@18537
   230
\begin{isamarkuptext}%
wenzelm@20447
   231
\glossary{Proof context}{The static context of a structured proof,
wenzelm@20447
   232
  acts like a local ``theory'' of the current portion of Isar proof
wenzelm@20447
   233
  text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
wenzelm@20447
   234
  judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi.  There is a
wenzelm@20447
   235
  generic notion of introducing and discharging hypotheses.
wenzelm@20447
   236
  Arbritrary auxiliary context data may be adjoined.}
wenzelm@20429
   237
wenzelm@20447
   238
  A proof context is a container for pure data with a back-reference
wenzelm@20449
   239
  to the theory it belongs to.  The \isa{init} operation creates a
wenzelm@20451
   240
  proof context from a given theory.  Modifications to draft theories
wenzelm@20451
   241
  are propagated to the proof context as usual, but there is also an
wenzelm@20451
   242
  explicit \isa{transfer} operation to force resynchronization
wenzelm@20451
   243
  with more substantial updates to the underlying theory.  The actual
wenzelm@20451
   244
  context data does not require any special bookkeeping, thanks to the
wenzelm@20451
   245
  lack of destructive features.
wenzelm@20429
   246
wenzelm@20447
   247
  Entities derived in a proof context need to record inherent logical
wenzelm@20447
   248
  requirements explicitly, since there is no separate context
wenzelm@20447
   249
  identification as for theories.  For example, hypotheses used in
wenzelm@20451
   250
  primitive derivations (cf.\ \secref{sec:thms}) are recorded
wenzelm@20447
   251
  separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
wenzelm@20447
   252
  sure.  Results could still leak into an alien proof context do to
wenzelm@20447
   253
  programming errors, but Isabelle/Isar includes some extra validity
wenzelm@20447
   254
  checks in critical positions, notably at the end of sub-proof.
wenzelm@20429
   255
wenzelm@20451
   256
  Proof contexts may be manipulated arbitrarily, although the common
wenzelm@20451
   257
  discipline is to follow block structure as a mental model: a given
wenzelm@20451
   258
  context is extended consecutively, and results are exported back
wenzelm@20451
   259
  into the original context.  Note that the Isar proof states model
wenzelm@20451
   260
  block-structured reasoning explicitly, using a stack of proof
wenzelm@20451
   261
  contexts internally, cf.\ \secref{sec:isar-proof-state}.%
wenzelm@18537
   262
\end{isamarkuptext}%
wenzelm@18537
   263
\isamarkuptrue%
wenzelm@18537
   264
%
wenzelm@20430
   265
\isadelimmlref
wenzelm@20430
   266
%
wenzelm@20430
   267
\endisadelimmlref
wenzelm@20430
   268
%
wenzelm@20430
   269
\isatagmlref
wenzelm@20430
   270
%
wenzelm@20430
   271
\begin{isamarkuptext}%
wenzelm@20449
   272
\begin{mldecls}
wenzelm@20449
   273
  \indexmltype{Proof.context}\verb|type Proof.context| \\
wenzelm@20449
   274
  \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
wenzelm@20449
   275
  \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
wenzelm@20449
   276
  \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
wenzelm@20449
   277
  \end{mldecls}
wenzelm@20449
   278
wenzelm@20449
   279
  \begin{description}
wenzelm@20449
   280
wenzelm@20449
   281
  \item \verb|Proof.context| represents proof contexts.  Elements
wenzelm@20449
   282
  of this type are essentially pure values, with a sliding reference
wenzelm@20449
   283
  to the background theory.
wenzelm@20449
   284
wenzelm@20449
   285
  \item \verb|ProofContext.init|~\isa{thy} produces a proof context
wenzelm@20449
   286
  derived from \isa{thy}, initializing all data.
wenzelm@20449
   287
wenzelm@20449
   288
  \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
wenzelm@20451
   289
  background theory from \isa{ctxt}, dereferencing its internal
wenzelm@20451
   290
  \verb|theory_ref|.
wenzelm@20449
   291
wenzelm@20449
   292
  \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
wenzelm@20449
   293
  background theory of \isa{ctxt} to the super theory \isa{thy}.
wenzelm@20449
   294
wenzelm@20449
   295
  \end{description}%
wenzelm@20430
   296
\end{isamarkuptext}%
wenzelm@20430
   297
\isamarkuptrue%
wenzelm@20430
   298
%
wenzelm@20430
   299
\endisatagmlref
wenzelm@20430
   300
{\isafoldmlref}%
wenzelm@20430
   301
%
wenzelm@20430
   302
\isadelimmlref
wenzelm@20430
   303
%
wenzelm@20430
   304
\endisadelimmlref
wenzelm@20430
   305
%
wenzelm@20451
   306
\isamarkupsubsection{Generic contexts \label{sec:generic-context}%
wenzelm@20429
   307
}
wenzelm@20429
   308
\isamarkuptrue%
wenzelm@20429
   309
%
wenzelm@20430
   310
\begin{isamarkuptext}%
wenzelm@20449
   311
A generic context is the disjoint sum of either a theory or proof
wenzelm@20451
   312
  context.  Occasionally, this enables uniform treatment of generic
wenzelm@20450
   313
  context data, typically extra-logical information.  Operations on
wenzelm@20449
   314
  generic contexts include the usual injections, partial selections,
wenzelm@20449
   315
  and combinators for lifting operations on either component of the
wenzelm@20449
   316
  disjoint sum.
wenzelm@20449
   317
wenzelm@20449
   318
  Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
wenzelm@20451
   319
  can always be selected from the sum, while a proof context might
wenzelm@20451
   320
  have to be constructed by an ad-hoc \isa{init} operation.%
wenzelm@20430
   321
\end{isamarkuptext}%
wenzelm@20430
   322
\isamarkuptrue%
wenzelm@20430
   323
%
wenzelm@20430
   324
\isadelimmlref
wenzelm@20430
   325
%
wenzelm@20430
   326
\endisadelimmlref
wenzelm@20430
   327
%
wenzelm@20430
   328
\isatagmlref
wenzelm@20430
   329
%
wenzelm@20430
   330
\begin{isamarkuptext}%
wenzelm@20449
   331
\begin{mldecls}
wenzelm@20449
   332
  \indexmltype{Context.generic}\verb|type Context.generic| \\
wenzelm@20449
   333
  \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
wenzelm@20449
   334
  \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
wenzelm@20449
   335
  \end{mldecls}
wenzelm@20449
   336
wenzelm@20449
   337
  \begin{description}
wenzelm@20449
   338
wenzelm@20451
   339
  \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
wenzelm@20451
   340
  constructors \verb|Context.Theory| and \verb|Context.Proof|.
wenzelm@20449
   341
wenzelm@20449
   342
  \item \verb|Context.theory_of|~\isa{context} always produces a
wenzelm@20449
   343
  theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
wenzelm@20449
   344
wenzelm@20449
   345
  \item \verb|Context.proof_of|~\isa{context} always produces a
wenzelm@20451
   346
  proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
wenzelm@20451
   347
  context data with each invocation).
wenzelm@20449
   348
wenzelm@20449
   349
  \end{description}%
wenzelm@20430
   350
\end{isamarkuptext}%
wenzelm@20430
   351
\isamarkuptrue%
wenzelm@20430
   352
%
wenzelm@20430
   353
\endisatagmlref
wenzelm@20430
   354
{\isafoldmlref}%
wenzelm@20430
   355
%
wenzelm@20430
   356
\isadelimmlref
wenzelm@20430
   357
%
wenzelm@20430
   358
\endisadelimmlref
wenzelm@20430
   359
%
wenzelm@20477
   360
\isamarkupsubsection{Context data \label{sec:context-data}%
wenzelm@20447
   361
}
wenzelm@20447
   362
\isamarkuptrue%
wenzelm@20447
   363
%
wenzelm@20447
   364
\begin{isamarkuptext}%
wenzelm@20451
   365
The main purpose of theory and proof contexts is to manage arbitrary
wenzelm@20451
   366
  data.  New data types can be declared incrementally at compile time.
wenzelm@20451
   367
  There are separate declaration mechanisms for any of the three kinds
wenzelm@20451
   368
  of contexts: theory, proof, generic.
wenzelm@20449
   369
wenzelm@20449
   370
  \paragraph{Theory data} may refer to destructive entities, which are
wenzelm@20451
   371
  maintained in direct correspondence to the linear evolution of
wenzelm@20451
   372
  theory values, including explicit copies.\footnote{Most existing
wenzelm@20451
   373
  instances of destructive theory data are merely historical relics
wenzelm@20451
   374
  (e.g.\ the destructive theorem storage, and destructive hints for
wenzelm@20451
   375
  the Simplifier and Classical rules).}  A theory data declaration
wenzelm@20451
   376
  needs to implement the following specification (depending on type
wenzelm@20451
   377
  \isa{T}):
wenzelm@20449
   378
wenzelm@20449
   379
  \medskip
wenzelm@20449
   380
  \begin{tabular}{ll}
wenzelm@20449
   381
  \isa{name{\isacharcolon}\ string} \\
wenzelm@20449
   382
  \isa{empty{\isacharcolon}\ T} & initial value \\
wenzelm@20449
   383
  \isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
wenzelm@20449
   384
  \isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
wenzelm@20449
   385
  \isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
wenzelm@20449
   386
  \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
wenzelm@20449
   387
  \end{tabular}
wenzelm@20449
   388
  \medskip
wenzelm@20449
   389
wenzelm@20449
   390
  \noindent The \isa{name} acts as a comment for diagnostic
wenzelm@20449
   391
  messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both
wenzelm@20449
   392
  should also include the functionality of \isa{copy} for impure
wenzelm@20449
   393
  data.
wenzelm@20449
   394
wenzelm@20451
   395
  \paragraph{Proof context data} is purely functional.  A declaration
wenzelm@20451
   396
  needs to implement the following specification:
wenzelm@20449
   397
wenzelm@20449
   398
  \medskip
wenzelm@20449
   399
  \begin{tabular}{ll}
wenzelm@20449
   400
  \isa{name{\isacharcolon}\ string} \\
wenzelm@20449
   401
  \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
wenzelm@20449
   402
  \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
wenzelm@20449
   403
  \end{tabular}
wenzelm@20449
   404
  \medskip
wenzelm@20449
   405
wenzelm@20449
   406
  \noindent The \isa{init} operation is supposed to produce a pure
wenzelm@20451
   407
  value from the given background theory.  The remainder is analogous
wenzelm@20451
   408
  to theory data.
wenzelm@20449
   409
wenzelm@20451
   410
  \paragraph{Generic data} provides a hybrid interface for both theory
wenzelm@20451
   411
  and proof data.  The declaration is essentially the same as for
wenzelm@20451
   412
  (pure) theory data, without \isa{copy}, though.  The \isa{init} operation for proof contexts merely selects the current data
wenzelm@20451
   413
  value from the background theory.
wenzelm@20449
   414
wenzelm@20449
   415
  \bigskip In any case, a data declaration of type \isa{T} results
wenzelm@20449
   416
  in the following interface:
wenzelm@20449
   417
wenzelm@20449
   418
  \medskip
wenzelm@20449
   419
  \begin{tabular}{ll}
wenzelm@20449
   420
  \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
wenzelm@20449
   421
  \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
wenzelm@20449
   422
  \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
wenzelm@20449
   423
  \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
wenzelm@20449
   424
  \isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit}
wenzelm@20449
   425
  \end{tabular}
wenzelm@20449
   426
  \medskip
wenzelm@20449
   427
wenzelm@20449
   428
  \noindent Here \isa{init} needs to be applied to the current
wenzelm@20449
   429
  theory context once, in order to register the initial setup.  The
wenzelm@20449
   430
  other operations provide access for the particular kind of context
wenzelm@20449
   431
  (theory, proof, or generic context).  Note that this is a safe
wenzelm@20449
   432
  interface: there is no other way to access the corresponding data
wenzelm@20451
   433
  slot of a context.  By keeping these operations private, a component
wenzelm@20451
   434
  may maintain abstract values authentically, without other components
wenzelm@20451
   435
  interfering.%
wenzelm@20447
   436
\end{isamarkuptext}%
wenzelm@20447
   437
\isamarkuptrue%
wenzelm@20447
   438
%
wenzelm@20450
   439
\isadelimmlref
wenzelm@20450
   440
%
wenzelm@20450
   441
\endisadelimmlref
wenzelm@20450
   442
%
wenzelm@20450
   443
\isatagmlref
wenzelm@20450
   444
%
wenzelm@20450
   445
\begin{isamarkuptext}%
wenzelm@20450
   446
\begin{mldecls}
wenzelm@20450
   447
  \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
wenzelm@20450
   448
  \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
wenzelm@20450
   449
  \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
wenzelm@20450
   450
  \end{mldecls}
wenzelm@20450
   451
wenzelm@20450
   452
  \begin{description}
wenzelm@20450
   453
wenzelm@20450
   454
  \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
wenzelm@20450
   455
  type \verb|theory| according to the specification provided as
wenzelm@20451
   456
  argument structure.  The resulting structure provides data init and
wenzelm@20451
   457
  access operations as described above.
wenzelm@20450
   458
wenzelm@20471
   459
  \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
wenzelm@20471
   460
  \verb|TheoryDataFun| for type \verb|Proof.context|.
wenzelm@20450
   461
wenzelm@20471
   462
  \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
wenzelm@20471
   463
  \verb|TheoryDataFun| for type \verb|Context.generic|.
wenzelm@20450
   464
wenzelm@20450
   465
  \end{description}%
wenzelm@20450
   466
\end{isamarkuptext}%
wenzelm@20450
   467
\isamarkuptrue%
wenzelm@20450
   468
%
wenzelm@20450
   469
\endisatagmlref
wenzelm@20450
   470
{\isafoldmlref}%
wenzelm@20450
   471
%
wenzelm@20450
   472
\isadelimmlref
wenzelm@20450
   473
%
wenzelm@20450
   474
\endisadelimmlref
wenzelm@20450
   475
%
wenzelm@20477
   476
\isamarkupsection{Names%
wenzelm@20438
   477
}
wenzelm@20438
   478
\isamarkuptrue%
wenzelm@20438
   479
%
wenzelm@20438
   480
\begin{isamarkuptext}%
wenzelm@20477
   481
In principle, a name is just a string, but there are various
wenzelm@20477
   482
  convention for encoding additional structure.
wenzelm@20471
   483
wenzelm@20477
   484
  For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
wenzelm@20477
   485
  qualified name.  The most basic constituents of names may have their
wenzelm@20477
   486
  own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
wenzelm@20477
   487
  considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
wenzelm@20438
   488
\end{isamarkuptext}%
wenzelm@20438
   489
\isamarkuptrue%
wenzelm@20438
   490
%
wenzelm@20438
   491
\isamarkupsubsection{Strings of symbols%
wenzelm@20438
   492
}
wenzelm@20438
   493
\isamarkuptrue%
wenzelm@20438
   494
%
wenzelm@20438
   495
\begin{isamarkuptext}%
wenzelm@20477
   496
\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
wenzelm@20477
   497
  plain ASCII characters as well as an infinite collection of named
wenzelm@20477
   498
  symbols (for greek, math etc.).}
wenzelm@20471
   499
wenzelm@20477
   500
  A \emph{symbol} constitutes the smallest textual unit in Isabelle
wenzelm@20477
   501
  --- raw characters are normally not encountered.  Isabelle strings
wenzelm@20477
   502
  consist of a sequence of symbols, represented as a packed string or
wenzelm@20477
   503
  a list of symbols.  Each symbol is in itself a small string, which
wenzelm@20477
   504
  is of one of the following forms:
wenzelm@20438
   505
wenzelm@20451
   506
  \begin{enumerate}
wenzelm@20451
   507
wenzelm@20477
   508
  \item singleton ASCII character ``\isa{c}'' (character code
wenzelm@20477
   509
  0--127), for example ``\verb,a,'',
wenzelm@20438
   510
wenzelm@20477
   511
  \item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
wenzelm@20477
   512
  for example ``\verb,\,\verb,<alpha>,'',
wenzelm@20438
   513
wenzelm@20477
   514
  \item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
wenzelm@20477
   515
  for example ``\verb,\,\verb,<^bold>,'',
wenzelm@20438
   516
wenzelm@20477
   517
  \item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
wenzelm@20477
   518
  \isa{text} is constists of printable characters excluding
wenzelm@20477
   519
  ``\verb,.,'' and ``\verb,>,'', for example
wenzelm@20477
   520
  ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
wenzelm@20438
   521
wenzelm@20477
   522
  \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
wenzelm@20451
   523
  ``\verb,\,\verb,<^raw42>,''.
wenzelm@20438
   524
wenzelm@20451
   525
  \end{enumerate}
wenzelm@20438
   526
wenzelm@20477
   527
  \noindent The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many
wenzelm@20477
   528
  regular symbols and control symbols, but a fixed collection of
wenzelm@20477
   529
  standard symbols is treated specifically.  For example,
wenzelm@20451
   530
  ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
wenzelm@20451
   531
  which means it may occur within regular Isabelle identifier syntax.
wenzelm@20438
   532
wenzelm@20477
   533
  Note that the character set underlying Isabelle symbols is plain
wenzelm@20477
   534
  7-bit ASCII.  Since 8-bit characters are passed through
wenzelm@20477
   535
  transparently, Isabelle may process Unicode/UCS data (in UTF-8
wenzelm@20477
   536
  encoding) as well.  Unicode provides its own collection of
wenzelm@20477
   537
  mathematical symbols, but there is no built-in link to the ones of
wenzelm@20477
   538
  Isabelle.
wenzelm@20438
   539
wenzelm@20477
   540
  \medskip Output of Isabelle symbols depends on the print mode
wenzelm@20477
   541
  (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the
wenzelm@20477
   542
  Isabelle document preparation system would present
wenzelm@20477
   543
  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
wenzelm@20477
   544
  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
wenzelm@20438
   545
\end{isamarkuptext}%
wenzelm@20438
   546
\isamarkuptrue%
wenzelm@20438
   547
%
wenzelm@20438
   548
\isadelimmlref
wenzelm@20438
   549
%
wenzelm@20438
   550
\endisadelimmlref
wenzelm@20438
   551
%
wenzelm@20438
   552
\isatagmlref
wenzelm@20438
   553
%
wenzelm@20438
   554
\begin{isamarkuptext}%
wenzelm@20438
   555
\begin{mldecls}
wenzelm@20438
   556
  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
wenzelm@20438
   557
  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
wenzelm@20438
   558
  \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
wenzelm@20438
   559
  \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
wenzelm@20438
   560
  \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
wenzelm@20451
   561
  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
wenzelm@20438
   562
  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
wenzelm@20438
   563
  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
wenzelm@20438
   564
  \end{mldecls}
wenzelm@20438
   565
wenzelm@20438
   566
  \begin{description}
wenzelm@20438
   567
wenzelm@20451
   568
  \item \verb|Symbol.symbol| represents Isabelle symbols.  This
wenzelm@20451
   569
  type is an alias for \verb|string|, but emphasizes the
wenzelm@20438
   570
  specific format encountered here.
wenzelm@20438
   571
wenzelm@20477
   572
  \item \verb|Symbol.explode|~\isa{str} produces a symbol list
wenzelm@20477
   573
  from the packed form that.  This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
wenzelm@20477
   574
  Isabelle!
wenzelm@20438
   575
wenzelm@20477
   576
  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
wenzelm@20477
   577
  symbols according to fixed syntactic conventions of Isabelle, cf.\
wenzelm@20477
   578
  \cite{isabelle-isar-ref}.
wenzelm@20438
   579
wenzelm@20438
   580
  \item \verb|Symbol.sym| is a concrete datatype that represents
wenzelm@20451
   581
  the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
wenzelm@20438
   582
wenzelm@20438
   583
  \item \verb|Symbol.decode| converts the string representation of a
wenzelm@20451
   584
  symbol into the datatype version.
wenzelm@20438
   585
wenzelm@20438
   586
  \end{description}%
wenzelm@20438
   587
\end{isamarkuptext}%
wenzelm@20438
   588
\isamarkuptrue%
wenzelm@20438
   589
%
wenzelm@20438
   590
\endisatagmlref
wenzelm@20438
   591
{\isafoldmlref}%
wenzelm@20438
   592
%
wenzelm@20438
   593
\isadelimmlref
wenzelm@20438
   594
%
wenzelm@20438
   595
\endisadelimmlref
wenzelm@20438
   596
%
wenzelm@20477
   597
\isamarkupsubsection{Basic names \label{sec:basic-names}%
wenzelm@20438
   598
}
wenzelm@20438
   599
\isamarkuptrue%
wenzelm@20438
   600
%
wenzelm@20438
   601
\begin{isamarkuptext}%
wenzelm@20477
   602
A \emph{basic name} essentially consists of a single Isabelle
wenzelm@20477
   603
  identifier.  There are conventions to mark separate classes of basic
wenzelm@20477
   604
  names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
wenzelm@20477
   605
  underscore means \emph{internal name}, two underscores means
wenzelm@20477
   606
  \emph{Skolem name}, three underscores means \emph{internal Skolem
wenzelm@20477
   607
  name}.
wenzelm@20477
   608
wenzelm@20477
   609
  For example, the basic name \isa{foo} has the internal version
wenzelm@20477
   610
  \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
wenzelm@20471
   611
wenzelm@20477
   612
  Such special versions are required for bookkeeping of names that are
wenzelm@20477
   613
  apart from anything that may appear in the text given by the user.
wenzelm@20477
   614
  In particular, system generated variables in high-level Isar proof
wenzelm@20477
   615
  contexts are usually marked as internal, which prevents mysterious
wenzelm@20477
   616
  name references such as \isa{xaa} in the text.
wenzelm@20477
   617
wenzelm@20477
   618
  \medskip Basic manipulations of binding scopes requires names to be
wenzelm@20477
   619
  modified.  A \emph{name context} contains a collection of already
wenzelm@20477
   620
  used names, which is maintained by the \isa{declare} operation.
wenzelm@20438
   621
wenzelm@20477
   622
  The \isa{invents} operation derives a number of fresh names
wenzelm@20477
   623
  derived from a given starting point.  For example, three names
wenzelm@20477
   624
  derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
wenzelm@20477
   625
  provided there are no clashes with already used names.
wenzelm@20438
   626
wenzelm@20477
   627
  The \isa{variants} operation produces fresh names by
wenzelm@20477
   628
  incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}).  For example, name \isa{foo} results in variants
wenzelm@20477
   629
  \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
wenzelm@20477
   630
  unused variant from this list.%
wenzelm@20438
   631
\end{isamarkuptext}%
wenzelm@20438
   632
\isamarkuptrue%
wenzelm@20438
   633
%
wenzelm@20451
   634
\isadelimmlref
wenzelm@20451
   635
%
wenzelm@20451
   636
\endisadelimmlref
wenzelm@20451
   637
%
wenzelm@20451
   638
\isatagmlref
wenzelm@20451
   639
%
wenzelm@20451
   640
\begin{isamarkuptext}%
wenzelm@20477
   641
\begin{mldecls}
wenzelm@20477
   642
  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
wenzelm@20477
   643
  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
wenzelm@20477
   644
  \indexmltype{Name.context}\verb|type Name.context| \\
wenzelm@20477
   645
  \indexml{Name.context}\verb|Name.context: Name.context| \\
wenzelm@20477
   646
  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
wenzelm@20477
   647
  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
wenzelm@20477
   648
  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
wenzelm@20477
   649
  \end{mldecls}
wenzelm@20477
   650
wenzelm@20477
   651
  \begin{description}
wenzelm@20477
   652
wenzelm@20477
   653
  \item \verb|Name.internal|~\isa{name} produces an internal name
wenzelm@20477
   654
  by adding one underscore.
wenzelm@20477
   655
wenzelm@20477
   656
  \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
wenzelm@20477
   657
  adding two underscores.
wenzelm@20477
   658
wenzelm@20477
   659
  \item \verb|Name.context| represents the context of already used
wenzelm@20477
   660
  names; the initial value is \verb|Name.context|.
wenzelm@20477
   661
wenzelm@20477
   662
  \item \verb|Name.declare|~\isa{name} declares \isa{name} as
wenzelm@20477
   663
  being used.
wenzelm@20477
   664
wenzelm@20477
   665
  \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
wenzelm@20477
   666
wenzelm@20477
   667
  \end{description}%
wenzelm@20477
   668
\end{isamarkuptext}%
wenzelm@20477
   669
\isamarkuptrue%
wenzelm@20477
   670
%
wenzelm@20477
   671
\endisatagmlref
wenzelm@20477
   672
{\isafoldmlref}%
wenzelm@20477
   673
%
wenzelm@20477
   674
\isadelimmlref
wenzelm@20477
   675
%
wenzelm@20477
   676
\endisadelimmlref
wenzelm@20477
   677
%
wenzelm@20477
   678
\isamarkupsubsection{Indexed names%
wenzelm@20477
   679
}
wenzelm@20477
   680
\isamarkuptrue%
wenzelm@20477
   681
%
wenzelm@20477
   682
\begin{isamarkuptext}%
wenzelm@20477
   683
An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
wenzelm@20477
   684
  name with a natural number.  This representation allows efficient
wenzelm@20477
   685
  renaming by incrementing the second component only.  To rename two
wenzelm@20477
   686
  collections of indexnames apart from each other, first determine the
wenzelm@20477
   687
  maximum index \isa{maxidx} of the first collection, then
wenzelm@20477
   688
  increment all indexes of the second collection by \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}.  Note that the maximum index of an empty collection is \isa{{\isacharminus}{\isadigit{1}}}.
wenzelm@20477
   689
wenzelm@20477
   690
  Isabelle syntax observes the following rules for representing an
wenzelm@20477
   691
  indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
wenzelm@20477
   692
wenzelm@20477
   693
  \begin{itemize}
wenzelm@20477
   694
wenzelm@20477
   695
  \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
wenzelm@20477
   696
wenzelm@20477
   697
  \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
wenzelm@20477
   698
wenzelm@20477
   699
  \item \isa{{\isacharquery}x{\isachardot}i} else.
wenzelm@20477
   700
wenzelm@20477
   701
  \end{itemize}
wenzelm@20477
   702
wenzelm@20477
   703
  Occasionally, basic names and indexed names are injected into the
wenzelm@20477
   704
  same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
wenzelm@20477
   705
  to encode basic names.
wenzelm@20477
   706
wenzelm@20477
   707
  \medskip Indexnames may acquire arbitrary large index numbers over
wenzelm@20477
   708
  time.  Results are usually normalized towards \isa{{\isadigit{0}}} at certain
wenzelm@20477
   709
  checkpoints, such that the very end of a proof.  This works by
wenzelm@20477
   710
  producing variants of the corresponding basic names
wenzelm@20477
   711
  (\secref{sec:basic-names}).  For example, the collection \isa{{\isacharquery}x{\isachardot}{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{4}}{\isadigit{2}}} then becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
wenzelm@20477
   712
\end{isamarkuptext}%
wenzelm@20477
   713
\isamarkuptrue%
wenzelm@20477
   714
%
wenzelm@20477
   715
\isadelimmlref
wenzelm@20477
   716
%
wenzelm@20477
   717
\endisadelimmlref
wenzelm@20477
   718
%
wenzelm@20477
   719
\isatagmlref
wenzelm@20477
   720
%
wenzelm@20477
   721
\begin{isamarkuptext}%
wenzelm@20477
   722
\begin{mldecls}
wenzelm@20477
   723
  \indexmltype{indexname}\verb|type indexname| \\
wenzelm@20477
   724
  \end{mldecls}
wenzelm@20477
   725
wenzelm@20477
   726
  \begin{description}
wenzelm@20477
   727
wenzelm@20477
   728
  \item \verb|indexname| represents indexed names.  This is an
wenzelm@20477
   729
  abbreviation for \verb|string * int|.  The second component is
wenzelm@20477
   730
  usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
wenzelm@20477
   731
  is used to embed plain names.
wenzelm@20477
   732
wenzelm@20477
   733
  \end{description}%
wenzelm@20451
   734
\end{isamarkuptext}%
wenzelm@20451
   735
\isamarkuptrue%
wenzelm@20451
   736
%
wenzelm@20451
   737
\endisatagmlref
wenzelm@20451
   738
{\isafoldmlref}%
wenzelm@20451
   739
%
wenzelm@20451
   740
\isadelimmlref
wenzelm@20451
   741
%
wenzelm@20451
   742
\endisadelimmlref
wenzelm@20451
   743
%
wenzelm@20477
   744
\isamarkupsubsection{Qualified names and name spaces%
wenzelm@20438
   745
}
wenzelm@20438
   746
\isamarkuptrue%
wenzelm@20438
   747
%
wenzelm@20438
   748
\begin{isamarkuptext}%
wenzelm@20477
   749
A \emph{qualified name} consists of a non-empty sequence of basic
wenzelm@20477
   750
  name components.  The packed representation a dot as separator, for
wenzelm@20477
   751
  example in ``\isa{A{\isachardot}b{\isachardot}c}''.  The last component is called
wenzelm@20477
   752
  \emph{base} name, the remaining prefix \emph{qualifier} (which may
wenzelm@20477
   753
  be empty).
wenzelm@20477
   754
wenzelm@20477
   755
  The empty name is commonly used as an indication of unnamed
wenzelm@20477
   756
  entities, if this makes any sense.  The operations on qualified
wenzelm@20477
   757
  names are smart enough to pass through such improper names
wenzelm@20477
   758
  unchanged.
wenzelm@20477
   759
wenzelm@20477
   760
  The basic idea of qualified names is to encode a hierarchically
wenzelm@20477
   761
  structured name spaces by recording the access path as part of the
wenzelm@20477
   762
  name.  For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
wenzelm@20477
   763
  entity \isa{c} within a local structure \isa{b} of the
wenzelm@20477
   764
  enclosing structure \isa{A}.  Typically, name space hierarchies
wenzelm@20477
   765
  consist of 1--3 levels, but this need not be always so.
wenzelm@20477
   766
wenzelm@20477
   767
  \medskip A \isa{naming} policy tells how to turn a name
wenzelm@20477
   768
  specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
wenzelm@20477
   769
  externally.
wenzelm@20477
   770
wenzelm@20477
   771
  For example, the default naming prefixes an implicit path from the
wenzelm@20477
   772
  context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
wenzelm@20477
   773
  standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
wenzelm@20477
   774
  partial \isa{path} specifications.
wenzelm@20477
   775
wenzelm@20477
   776
  Normally, the naming is implicit in the theory or proof context.
wenzelm@20477
   777
  There are separate versions of the corresponding operations for these
wenzelm@20477
   778
  context types.
wenzelm@20477
   779
wenzelm@20477
   780
  \medskip A \isa{name\ space} manages a collection of fully
wenzelm@20477
   781
  internalized names, together with a mapping between external names
wenzelm@20477
   782
  and internal names (in both directions).  The corresponding \isa{intern} and \isa{extern} operations are mostly used for
wenzelm@20477
   783
  parsing and printing only!  The \isa{declare} operation augments
wenzelm@20477
   784
  a name space according to a given naming policy.
wenzelm@20477
   785
wenzelm@20477
   786
  By general convention, there are separate name spaces for each kind
wenzelm@20477
   787
  of formal entity, such as logical constant, type, type class,
wenzelm@20477
   788
  theorem etc.  It is usually clear from the occurrence in concrete
wenzelm@20477
   789
  syntax (or from the scope) which kind of entity a name refers to.
wenzelm@20477
   790
wenzelm@20477
   791
  For example, the very same name \isa{c} may be used uniformly
wenzelm@20477
   792
  for a constant, type, type class, which are from separate syntactic
wenzelm@20477
   793
  categories.  There is a common convention to name theorems
wenzelm@20477
   794
  systematically, according to the name of the main logical entity
wenzelm@20477
   795
  being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
wenzelm@20477
   796
  theorems related to constant \isa{c}.
wenzelm@20477
   797
wenzelm@20477
   798
  This technique of mapping names from one space into another requires
wenzelm@20477
   799
  some care in order to avoid conflicts.  In particular, theorem names
wenzelm@20477
   800
  derived from type or class names are better suffixed in addition to
wenzelm@20477
   801
  the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
wenzelm@20477
   802
  \isa{c}, respectively.%
wenzelm@20438
   803
\end{isamarkuptext}%
wenzelm@20438
   804
\isamarkuptrue%
wenzelm@20438
   805
%
wenzelm@20477
   806
\isadelimmlref
wenzelm@20477
   807
%
wenzelm@20477
   808
\endisadelimmlref
wenzelm@20477
   809
%
wenzelm@20477
   810
\isatagmlref
wenzelm@20438
   811
%
wenzelm@20438
   812
\begin{isamarkuptext}%
wenzelm@20477
   813
\begin{mldecls}
wenzelm@20477
   814
  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
wenzelm@20477
   815
  \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
wenzelm@20477
   816
  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
wenzelm@20477
   817
  \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
wenzelm@20477
   818
  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
wenzelm@20477
   819
  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
wenzelm@20477
   820
  \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
wenzelm@20477
   821
  \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
wenzelm@20477
   822
  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
wenzelm@20477
   823
  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
wenzelm@20477
   824
  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
wenzelm@20477
   825
  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
wenzelm@20477
   826
  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
wenzelm@20477
   827
  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
wenzelm@20477
   828
  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
wenzelm@20477
   829
  \end{mldecls}
wenzelm@20477
   830
wenzelm@20477
   831
  \begin{description}
wenzelm@20477
   832
wenzelm@20477
   833
  \item \verb|NameSpace.base|~\isa{name} returns the base name of a
wenzelm@20477
   834
  qualified name.
wenzelm@20477
   835
wenzelm@20477
   836
  \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
wenzelm@20477
   837
  of a qualified name.
wenzelm@20477
   838
wenzelm@20477
   839
  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
wenzelm@20477
   840
  appends two qualified names.
wenzelm@20477
   841
wenzelm@20477
   842
  \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
wenzelm@20477
   843
  string representation and explicit list form of qualified names.
wenzelm@20477
   844
wenzelm@20477
   845
  \item \verb|NameSpace.naming| represents the abstract concept of
wenzelm@20477
   846
  a naming policy.
wenzelm@20477
   847
wenzelm@20477
   848
  \item \verb|NameSpace.default_naming| is the default naming policy.
wenzelm@20477
   849
  In a theory context, this is usually augmented by a path prefix
wenzelm@20477
   850
  consisting of the theory name.
wenzelm@20477
   851
wenzelm@20477
   852
  \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
wenzelm@20477
   853
  naming policy by extending its path.
wenzelm@20477
   854
wenzelm@20477
   855
  \item \verb|NameSpace.full|\isa{naming\ name} turns a name
wenzelm@20477
   856
  specification (usually a basic name) into the fully qualified
wenzelm@20477
   857
  internal version, according to the given naming policy.
wenzelm@20477
   858
wenzelm@20477
   859
  \item \verb|NameSpace.T| represents name spaces.
wenzelm@20477
   860
wenzelm@20477
   861
  \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
wenzelm@20477
   862
  building name spaces in accordance to the usual theory data
wenzelm@20477
   863
  management (\secref{sec:context-data}).
wenzelm@20477
   864
wenzelm@20477
   865
  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
wenzelm@20477
   866
  fully qualified name into the name space, with partial accesses
wenzelm@20477
   867
  being derived from the given policy.
wenzelm@20477
   868
wenzelm@20477
   869
  \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
wenzelm@20477
   870
  (partially qualified) external name.
wenzelm@20477
   871
wenzelm@20477
   872
  This operation is mostly for parsing.  Note that fully qualified
wenzelm@20477
   873
  names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
wenzelm@20477
   874
wenzelm@20477
   875
  \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
wenzelm@20477
   876
  (fully qualified) internal name.
wenzelm@20477
   877
wenzelm@20477
   878
  This operation is mostly for printing.  Note unqualified names are
wenzelm@20477
   879
  produced via \verb|NameSpace.base|.
wenzelm@20477
   880
wenzelm@20477
   881
  \end{description}%
wenzelm@20438
   882
\end{isamarkuptext}%
wenzelm@20438
   883
\isamarkuptrue%
wenzelm@20438
   884
%
wenzelm@20477
   885
\endisatagmlref
wenzelm@20477
   886
{\isafoldmlref}%
wenzelm@20438
   887
%
wenzelm@20477
   888
\isadelimmlref
wenzelm@20477
   889
%
wenzelm@20477
   890
\endisadelimmlref
wenzelm@20438
   891
%
wenzelm@18537
   892
\isadelimtheory
wenzelm@18537
   893
%
wenzelm@18537
   894
\endisadelimtheory
wenzelm@18537
   895
%
wenzelm@18537
   896
\isatagtheory
wenzelm@18537
   897
\isacommand{end}\isamarkupfalse%
wenzelm@18537
   898
%
wenzelm@18537
   899
\endisatagtheory
wenzelm@18537
   900
{\isafoldtheory}%
wenzelm@18537
   901
%
wenzelm@18537
   902
\isadelimtheory
wenzelm@18537
   903
%
wenzelm@18537
   904
\endisadelimtheory
wenzelm@18537
   905
\isanewline
wenzelm@18537
   906
\end{isabellebody}%
wenzelm@18537
   907
%%% Local Variables:
wenzelm@18537
   908
%%% mode: latex
wenzelm@18537
   909
%%% TeX-master: "root"
wenzelm@18537
   910
%%% End: