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