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