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