doc-src/IsarImplementation/Thy/document/prelim.tex
author wenzelm
Tue Sep 05 16:42:32 2006 +0200 (2006-09-05 ago)
changeset 20477 e623b0e30541
parent 20475 a04bf731ceb6
child 20481 c96f80442ce6
permissions -rw-r--r--
tuned;
     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   $Nat$ &            &              &            & \isa{List} \\
   141         & $\searrow$ &              & $\swarrow$ \\
   142         &            & \isa{Length} \\
   143         &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
   144         &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
   145         &            & $\vdots$~~ \\
   146         &            & \isa{{\isasymbullet}}~~ \\
   147         &            & $\vdots$~~ \\
   148         &            & \isa{{\isasymbullet}}~~ \\
   149         &            & $\vdots$~~ \\
   150         &            & \multicolumn{3}{l}{~~$\isarkeyword{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.  The dynamic stops after an
   159   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| \\[1ex]
   181   \indexmltype{theory-ref}\verb|type theory_ref| \\
   182   \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
   183   \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
   184   \end{mldecls}
   185 
   186   \begin{description}
   187 
   188   \item \verb|theory| represents theory contexts.  This is
   189   essentially a linear type!  Most operations destroy the original
   190   version, which then becomes ``stale''.
   191 
   192   \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
   193   compares theories according to the inherent graph structure of the
   194   construction.  This sub-theory relation is a nominal approximation
   195   of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
   196 
   197   \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
   198   absorbs one theory into the other.  This fails for unrelated
   199   theories!
   200 
   201   \item \verb|Theory.checkpoint|~\isa{thy} produces a safe
   202   stepping stone in the linear development of \isa{thy}.  The next
   203   update will result in two related, valid theories.
   204 
   205   \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The result is not
   206   related to the original; the original is unchanched.
   207 
   208   \item \verb|theory_ref| represents a sliding reference to an
   209   always valid theory; updates on the original are propagated
   210   automatically.
   211 
   212   \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|.  As the referenced theory
   213   evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
   214 
   215   \end{description}%
   216 \end{isamarkuptext}%
   217 \isamarkuptrue%
   218 %
   219 \endisatagmlref
   220 {\isafoldmlref}%
   221 %
   222 \isadelimmlref
   223 %
   224 \endisadelimmlref
   225 %
   226 \isamarkupsubsection{Proof context \label{sec:context-proof}%
   227 }
   228 \isamarkuptrue%
   229 %
   230 \begin{isamarkuptext}%
   231 \glossary{Proof context}{The static context of a structured proof,
   232   acts like a local ``theory'' of the current portion of Isar proof
   233   text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
   234   judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi.  There is a
   235   generic notion of introducing and discharging hypotheses.
   236   Arbritrary auxiliary context data may be adjoined.}
   237 
   238   A proof context is a container for pure data with a back-reference
   239   to the theory it belongs to.  The \isa{init} operation creates a
   240   proof context from a given theory.  Modifications to draft theories
   241   are propagated to the proof context as usual, but there is also an
   242   explicit \isa{transfer} operation to force resynchronization
   243   with more substantial updates to the underlying theory.  The actual
   244   context data does not require any special bookkeeping, thanks to the
   245   lack of destructive features.
   246 
   247   Entities derived in a proof context need to record inherent logical
   248   requirements explicitly, since there is no separate context
   249   identification as for theories.  For example, hypotheses used in
   250   primitive derivations (cf.\ \secref{sec:thms}) are recorded
   251   separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
   252   sure.  Results could still leak into an alien proof context do to
   253   programming errors, but Isabelle/Isar includes some extra validity
   254   checks in critical positions, notably at the end of sub-proof.
   255 
   256   Proof contexts may be manipulated arbitrarily, although the common
   257   discipline is to follow block structure as a mental model: a given
   258   context is extended consecutively, and results are exported back
   259   into the original context.  Note that the Isar proof states model
   260   block-structured reasoning explicitly, using a stack of proof
   261   contexts internally, cf.\ \secref{sec:isar-proof-state}.%
   262 \end{isamarkuptext}%
   263 \isamarkuptrue%
   264 %
   265 \isadelimmlref
   266 %
   267 \endisadelimmlref
   268 %
   269 \isatagmlref
   270 %
   271 \begin{isamarkuptext}%
   272 \begin{mldecls}
   273   \indexmltype{Proof.context}\verb|type Proof.context| \\
   274   \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
   275   \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
   276   \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
   277   \end{mldecls}
   278 
   279   \begin{description}
   280 
   281   \item \verb|Proof.context| represents proof contexts.  Elements
   282   of this type are essentially pure values, with a sliding reference
   283   to the background theory.
   284 
   285   \item \verb|ProofContext.init|~\isa{thy} produces a proof context
   286   derived from \isa{thy}, initializing all data.
   287 
   288   \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
   289   background theory from \isa{ctxt}, dereferencing its internal
   290   \verb|theory_ref|.
   291 
   292   \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
   293   background theory of \isa{ctxt} to the super theory \isa{thy}.
   294 
   295   \end{description}%
   296 \end{isamarkuptext}%
   297 \isamarkuptrue%
   298 %
   299 \endisatagmlref
   300 {\isafoldmlref}%
   301 %
   302 \isadelimmlref
   303 %
   304 \endisadelimmlref
   305 %
   306 \isamarkupsubsection{Generic contexts \label{sec:generic-context}%
   307 }
   308 \isamarkuptrue%
   309 %
   310 \begin{isamarkuptext}%
   311 A generic context is the disjoint sum of either a theory or proof
   312   context.  Occasionally, this enables uniform treatment of generic
   313   context data, typically extra-logical information.  Operations on
   314   generic contexts include the usual injections, partial selections,
   315   and combinators for lifting operations on either component of the
   316   disjoint sum.
   317 
   318   Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
   319   can always be selected from the sum, while a proof context might
   320   have to be constructed by an ad-hoc \isa{init} operation.%
   321 \end{isamarkuptext}%
   322 \isamarkuptrue%
   323 %
   324 \isadelimmlref
   325 %
   326 \endisadelimmlref
   327 %
   328 \isatagmlref
   329 %
   330 \begin{isamarkuptext}%
   331 \begin{mldecls}
   332   \indexmltype{Context.generic}\verb|type Context.generic| \\
   333   \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
   334   \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
   335   \end{mldecls}
   336 
   337   \begin{description}
   338 
   339   \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
   340   constructors \verb|Context.Theory| and \verb|Context.Proof|.
   341 
   342   \item \verb|Context.theory_of|~\isa{context} always produces a
   343   theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
   344 
   345   \item \verb|Context.proof_of|~\isa{context} always produces a
   346   proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
   347   context data with each invocation).
   348 
   349   \end{description}%
   350 \end{isamarkuptext}%
   351 \isamarkuptrue%
   352 %
   353 \endisatagmlref
   354 {\isafoldmlref}%
   355 %
   356 \isadelimmlref
   357 %
   358 \endisadelimmlref
   359 %
   360 \isamarkupsubsection{Context data \label{sec:context-data}%
   361 }
   362 \isamarkuptrue%
   363 %
   364 \begin{isamarkuptext}%
   365 The main purpose of theory and proof contexts is to manage arbitrary
   366   data.  New data types can be declared incrementally at compile time.
   367   There are separate declaration mechanisms for any of the three kinds
   368   of contexts: theory, proof, generic.
   369 
   370   \paragraph{Theory data} may refer to destructive entities, which are
   371   maintained in direct correspondence to the linear evolution of
   372   theory values, including explicit copies.\footnote{Most existing
   373   instances of destructive theory data are merely historical relics
   374   (e.g.\ the destructive theorem storage, and destructive hints for
   375   the Simplifier and Classical rules).}  A theory data declaration
   376   needs to implement the following specification (depending on type
   377   \isa{T}):
   378 
   379   \medskip
   380   \begin{tabular}{ll}
   381   \isa{name{\isacharcolon}\ string} \\
   382   \isa{empty{\isacharcolon}\ T} & initial value \\
   383   \isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
   384   \isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
   385   \isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
   386   \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
   387   \end{tabular}
   388   \medskip
   389 
   390   \noindent The \isa{name} acts as a comment for diagnostic
   391   messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both
   392   should also include the functionality of \isa{copy} for impure
   393   data.
   394 
   395   \paragraph{Proof context data} is purely functional.  A declaration
   396   needs to implement the following specification:
   397 
   398   \medskip
   399   \begin{tabular}{ll}
   400   \isa{name{\isacharcolon}\ string} \\
   401   \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
   402   \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
   403   \end{tabular}
   404   \medskip
   405 
   406   \noindent The \isa{init} operation is supposed to produce a pure
   407   value from the given background theory.  The remainder is analogous
   408   to theory data.
   409 
   410   \paragraph{Generic data} provides a hybrid interface for both theory
   411   and proof data.  The declaration is essentially the same as for
   412   (pure) theory data, without \isa{copy}, though.  The \isa{init} operation for proof contexts merely selects the current data
   413   value from the background theory.
   414 
   415   \bigskip In any case, a data declaration of type \isa{T} results
   416   in the following interface:
   417 
   418   \medskip
   419   \begin{tabular}{ll}
   420   \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
   421   \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
   422   \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
   423   \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
   424   \isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit}
   425   \end{tabular}
   426   \medskip
   427 
   428   \noindent Here \isa{init} needs to be applied to the current
   429   theory context once, in order to register the initial setup.  The
   430   other operations provide access for the particular kind of context
   431   (theory, proof, or generic context).  Note that this is a safe
   432   interface: there is no other way to access the corresponding data
   433   slot of a context.  By keeping these operations private, a component
   434   may maintain abstract values authentically, without other components
   435   interfering.%
   436 \end{isamarkuptext}%
   437 \isamarkuptrue%
   438 %
   439 \isadelimmlref
   440 %
   441 \endisadelimmlref
   442 %
   443 \isatagmlref
   444 %
   445 \begin{isamarkuptext}%
   446 \begin{mldecls}
   447   \indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
   448   \indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
   449   \indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
   450   \end{mldecls}
   451 
   452   \begin{description}
   453 
   454   \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
   455   type \verb|theory| according to the specification provided as
   456   argument structure.  The resulting structure provides data init and
   457   access operations as described above.
   458 
   459   \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
   460   \verb|TheoryDataFun| for type \verb|Proof.context|.
   461 
   462   \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
   463   \verb|TheoryDataFun| for type \verb|Context.generic|.
   464 
   465   \end{description}%
   466 \end{isamarkuptext}%
   467 \isamarkuptrue%
   468 %
   469 \endisatagmlref
   470 {\isafoldmlref}%
   471 %
   472 \isadelimmlref
   473 %
   474 \endisadelimmlref
   475 %
   476 \isamarkupsection{Names%
   477 }
   478 \isamarkuptrue%
   479 %
   480 \begin{isamarkuptext}%
   481 In principle, a name is just a string, but there are various
   482   convention for encoding additional structure.
   483 
   484   For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
   485   qualified name.  The most basic constituents of names may have their
   486   own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
   487   considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
   488 \end{isamarkuptext}%
   489 \isamarkuptrue%
   490 %
   491 \isamarkupsubsection{Strings of symbols%
   492 }
   493 \isamarkuptrue%
   494 %
   495 \begin{isamarkuptext}%
   496 \glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
   497   plain ASCII characters as well as an infinite collection of named
   498   symbols (for greek, math etc.).}
   499 
   500   A \emph{symbol} constitutes the smallest textual unit in Isabelle
   501   --- raw characters are normally not encountered.  Isabelle strings
   502   consist of a sequence of symbols, represented as a packed string or
   503   a list of symbols.  Each symbol is in itself a small string, which
   504   is of one of the following forms:
   505 
   506   \begin{enumerate}
   507 
   508   \item singleton ASCII character ``\isa{c}'' (character code
   509   0--127), for example ``\verb,a,'',
   510 
   511   \item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
   512   for example ``\verb,\,\verb,<alpha>,'',
   513 
   514   \item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
   515   for example ``\verb,\,\verb,<^bold>,'',
   516 
   517   \item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
   518   \isa{text} is constists of printable characters excluding
   519   ``\verb,.,'' and ``\verb,>,'', for example
   520   ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   521 
   522   \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
   523   ``\verb,\,\verb,<^raw42>,''.
   524 
   525   \end{enumerate}
   526 
   527   \noindent The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many
   528   regular symbols and control symbols, but a fixed collection of
   529   standard symbols is treated specifically.  For example,
   530   ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   531   which means it may occur within regular Isabelle identifier syntax.
   532 
   533   Note that the character set underlying Isabelle symbols is plain
   534   7-bit ASCII.  Since 8-bit characters are passed through
   535   transparently, Isabelle may process Unicode/UCS data (in UTF-8
   536   encoding) as well.  Unicode provides its own collection of
   537   mathematical symbols, but there is no built-in link to the ones of
   538   Isabelle.
   539 
   540   \medskip Output of Isabelle symbols depends on the print mode
   541   (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the
   542   Isabelle document preparation system would present
   543   ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
   544   ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
   545 \end{isamarkuptext}%
   546 \isamarkuptrue%
   547 %
   548 \isadelimmlref
   549 %
   550 \endisadelimmlref
   551 %
   552 \isatagmlref
   553 %
   554 \begin{isamarkuptext}%
   555 \begin{mldecls}
   556   \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
   557   \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
   558   \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   559   \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   560   \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
   561   \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
   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 Isabelle symbols.  This
   569   type is an alias for \verb|string|, but emphasizes the
   570   specific format encountered here.
   571 
   572   \item \verb|Symbol.explode|~\isa{str} produces a symbol list
   573   from the packed form that.  This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
   574   Isabelle!
   575 
   576   \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
   577   symbols according to fixed syntactic conventions of Isabelle, cf.\
   578   \cite{isabelle-isar-ref}.
   579 
   580   \item \verb|Symbol.sym| is a concrete datatype that represents
   581   the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
   582 
   583   \item \verb|Symbol.decode| converts the string representation of a
   584   symbol into the datatype version.
   585 
   586   \end{description}%
   587 \end{isamarkuptext}%
   588 \isamarkuptrue%
   589 %
   590 \endisatagmlref
   591 {\isafoldmlref}%
   592 %
   593 \isadelimmlref
   594 %
   595 \endisadelimmlref
   596 %
   597 \isamarkupsubsection{Basic names \label{sec:basic-names}%
   598 }
   599 \isamarkuptrue%
   600 %
   601 \begin{isamarkuptext}%
   602 A \emph{basic name} essentially consists of a single Isabelle
   603   identifier.  There are conventions to mark separate classes of basic
   604   names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
   605   underscore means \emph{internal name}, two underscores means
   606   \emph{Skolem name}, three underscores means \emph{internal Skolem
   607   name}.
   608 
   609   For example, the basic name \isa{foo} has the internal version
   610   \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
   611 
   612   Such special versions are required for bookkeeping of names that are
   613   apart from anything that may appear in the text given by the user.
   614   In particular, system generated variables in high-level Isar proof
   615   contexts are usually marked as internal, which prevents mysterious
   616   name references such as \isa{xaa} in the text.
   617 
   618   \medskip Basic manipulations of binding scopes requires names to be
   619   modified.  A \emph{name context} contains a collection of already
   620   used names, which is maintained by the \isa{declare} operation.
   621 
   622   The \isa{invents} operation derives a number of fresh names
   623   derived from a given starting point.  For example, three names
   624   derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
   625   provided there are no clashes with already used names.
   626 
   627   The \isa{variants} operation produces fresh names by
   628   incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}).  For example, name \isa{foo} results in variants
   629   \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
   630   unused variant from this list.%
   631 \end{isamarkuptext}%
   632 \isamarkuptrue%
   633 %
   634 \isadelimmlref
   635 %
   636 \endisadelimmlref
   637 %
   638 \isatagmlref
   639 %
   640 \begin{isamarkuptext}%
   641 \begin{mldecls}
   642   \indexml{Name.internal}\verb|Name.internal: string -> string| \\
   643   \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
   644   \indexmltype{Name.context}\verb|type Name.context| \\
   645   \indexml{Name.context}\verb|Name.context: Name.context| \\
   646   \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
   647   \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
   648   \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
   649   \end{mldecls}
   650 
   651   \begin{description}
   652 
   653   \item \verb|Name.internal|~\isa{name} produces an internal name
   654   by adding one underscore.
   655 
   656   \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
   657   adding two underscores.
   658 
   659   \item \verb|Name.context| represents the context of already used
   660   names; the initial value is \verb|Name.context|.
   661 
   662   \item \verb|Name.declare|~\isa{name} declares \isa{name} as
   663   being used.
   664 
   665   \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
   666 
   667   \end{description}%
   668 \end{isamarkuptext}%
   669 \isamarkuptrue%
   670 %
   671 \endisatagmlref
   672 {\isafoldmlref}%
   673 %
   674 \isadelimmlref
   675 %
   676 \endisadelimmlref
   677 %
   678 \isamarkupsubsection{Indexed names%
   679 }
   680 \isamarkuptrue%
   681 %
   682 \begin{isamarkuptext}%
   683 An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
   684   name with a natural number.  This representation allows efficient
   685   renaming by incrementing the second component only.  To rename two
   686   collections of indexnames apart from each other, first determine the
   687   maximum index \isa{maxidx} of the first collection, then
   688   increment all indexes of the second collection by \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}.  Note that the maximum index of an empty collection is \isa{{\isacharminus}{\isadigit{1}}}.
   689 
   690   Isabelle syntax observes the following rules for representing an
   691   indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
   692 
   693   \begin{itemize}
   694 
   695   \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
   696 
   697   \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
   698 
   699   \item \isa{{\isacharquery}x{\isachardot}i} else.
   700 
   701   \end{itemize}
   702 
   703   Occasionally, basic names and indexed names are injected into the
   704   same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
   705   to encode basic names.
   706 
   707   \medskip Indexnames may acquire arbitrary large index numbers over
   708   time.  Results are usually normalized towards \isa{{\isadigit{0}}} at certain
   709   checkpoints, such that the very end of a proof.  This works by
   710   producing variants of the corresponding basic names
   711   (\secref{sec:basic-names}).  For example, the collection \isa{{\isacharquery}x{\isachardot}{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isachardot}{\isadigit{4}}{\isadigit{2}}} then becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
   712 \end{isamarkuptext}%
   713 \isamarkuptrue%
   714 %
   715 \isadelimmlref
   716 %
   717 \endisadelimmlref
   718 %
   719 \isatagmlref
   720 %
   721 \begin{isamarkuptext}%
   722 \begin{mldecls}
   723   \indexmltype{indexname}\verb|type indexname| \\
   724   \end{mldecls}
   725 
   726   \begin{description}
   727 
   728   \item \verb|indexname| represents indexed names.  This is an
   729   abbreviation for \verb|string * int|.  The second component is
   730   usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
   731   is used to embed plain names.
   732 
   733   \end{description}%
   734 \end{isamarkuptext}%
   735 \isamarkuptrue%
   736 %
   737 \endisatagmlref
   738 {\isafoldmlref}%
   739 %
   740 \isadelimmlref
   741 %
   742 \endisadelimmlref
   743 %
   744 \isamarkupsubsection{Qualified names and name spaces%
   745 }
   746 \isamarkuptrue%
   747 %
   748 \begin{isamarkuptext}%
   749 A \emph{qualified name} consists of a non-empty sequence of basic
   750   name components.  The packed representation a dot as separator, for
   751   example in ``\isa{A{\isachardot}b{\isachardot}c}''.  The last component is called
   752   \emph{base} name, the remaining prefix \emph{qualifier} (which may
   753   be empty).
   754 
   755   The empty name is commonly used as an indication of unnamed
   756   entities, if this makes any sense.  The operations on qualified
   757   names are smart enough to pass through such improper names
   758   unchanged.
   759 
   760   The basic idea of qualified names is to encode a hierarchically
   761   structured name spaces by recording the access path as part of the
   762   name.  For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
   763   entity \isa{c} within a local structure \isa{b} of the
   764   enclosing structure \isa{A}.  Typically, name space hierarchies
   765   consist of 1--3 levels, but this need not be always so.
   766 
   767   \medskip A \isa{naming} policy tells how to turn a name
   768   specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
   769   externally.
   770 
   771   For example, the default naming prefixes an implicit path from the
   772   context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
   773   standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
   774   partial \isa{path} specifications.
   775 
   776   Normally, the naming is implicit in the theory or proof context.
   777   There are separate versions of the corresponding operations for these
   778   context types.
   779 
   780   \medskip A \isa{name\ space} manages a collection of fully
   781   internalized names, together with a mapping between external names
   782   and internal names (in both directions).  The corresponding \isa{intern} and \isa{extern} operations are mostly used for
   783   parsing and printing only!  The \isa{declare} operation augments
   784   a name space according to a given naming policy.
   785 
   786   By general convention, there are separate name spaces for each kind
   787   of formal entity, such as logical constant, type, type class,
   788   theorem etc.  It is usually clear from the occurrence in concrete
   789   syntax (or from the scope) which kind of entity a name refers to.
   790 
   791   For example, the very same name \isa{c} may be used uniformly
   792   for a constant, type, type class, which are from separate syntactic
   793   categories.  There is a common convention to name theorems
   794   systematically, according to the name of the main logical entity
   795   being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
   796   theorems related to constant \isa{c}.
   797 
   798   This technique of mapping names from one space into another requires
   799   some care in order to avoid conflicts.  In particular, theorem names
   800   derived from type or class names are better suffixed in addition to
   801   the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
   802   \isa{c}, respectively.%
   803 \end{isamarkuptext}%
   804 \isamarkuptrue%
   805 %
   806 \isadelimmlref
   807 %
   808 \endisadelimmlref
   809 %
   810 \isatagmlref
   811 %
   812 \begin{isamarkuptext}%
   813 \begin{mldecls}
   814   \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
   815   \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
   816   \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
   817   \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
   818   \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
   819   \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   820   \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
   821   \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
   822   \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
   823   \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
   824   \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
   825   \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
   826   \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
   827   \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
   828   \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
   829   \end{mldecls}
   830 
   831   \begin{description}
   832 
   833   \item \verb|NameSpace.base|~\isa{name} returns the base name of a
   834   qualified name.
   835 
   836   \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
   837   of a qualified name.
   838 
   839   \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
   840   appends two qualified names.
   841 
   842   \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
   843   string representation and explicit list form of qualified names.
   844 
   845   \item \verb|NameSpace.naming| represents the abstract concept of
   846   a naming policy.
   847 
   848   \item \verb|NameSpace.default_naming| is the default naming policy.
   849   In a theory context, this is usually augmented by a path prefix
   850   consisting of the theory name.
   851 
   852   \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
   853   naming policy by extending its path.
   854 
   855   \item \verb|NameSpace.full|\isa{naming\ name} turns a name
   856   specification (usually a basic name) into the fully qualified
   857   internal version, according to the given naming policy.
   858 
   859   \item \verb|NameSpace.T| represents name spaces.
   860 
   861   \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
   862   building name spaces in accordance to the usual theory data
   863   management (\secref{sec:context-data}).
   864 
   865   \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
   866   fully qualified name into the name space, with partial accesses
   867   being derived from the given policy.
   868 
   869   \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
   870   (partially qualified) external name.
   871 
   872   This operation is mostly for parsing.  Note that fully qualified
   873   names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \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: