doc-src/IsarImplementation/Thy/document/prelim.tex
changeset 20477 e623b0e30541
parent 20475 a04bf731ceb6
child 20481 c96f80442ce6
     1.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Tue Sep 05 16:42:23 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Tue Sep 05 16:42:32 2006 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4  %
     1.5  \endisadelimmlref
     1.6  %
     1.7 -\isamarkupsubsection{Context data%
     1.8 +\isamarkupsubsection{Context data \label{sec:context-data}%
     1.9  }
    1.10  \isamarkuptrue%
    1.11  %
    1.12 @@ -473,124 +473,78 @@
    1.13  %
    1.14  \endisadelimmlref
    1.15  %
    1.16 -\isamarkupsection{Name spaces%
    1.17 +\isamarkupsection{Names%
    1.18  }
    1.19  \isamarkuptrue%
    1.20  %
    1.21 -\isadelimFIXME
    1.22 -%
    1.23 -\endisadelimFIXME
    1.24 -%
    1.25 -\isatagFIXME
    1.26 -%
    1.27  \begin{isamarkuptext}%
    1.28 -FIXME tune
    1.29 +In principle, a name is just a string, but there are various
    1.30 +  convention for encoding additional structure.
    1.31  
    1.32 -  By general convention, each kind of formal entities (logical
    1.33 -  constant, type, type class, theorem, method etc.) lives in a
    1.34 -  separate name space.  It is usually clear from the syntactic context
    1.35 -  of a name, which kind of entity it refers to.  For example, proof
    1.36 -  method \isa{foo} vs.\ theorem \isa{foo} vs.\ logical
    1.37 -  constant \isa{foo} are easily distinguished thanks to the design
    1.38 -  of the concrete outer syntax.  A notable exception are logical
    1.39 -  identifiers within a term (\secref{sec:terms}): constants, fixed
    1.40 -  variables, and bound variables all share the same identifier syntax,
    1.41 -  but are distinguished by their scope.
    1.42 -
    1.43 -  Name spaces are organized uniformly, as a collection of qualified
    1.44 -  names consisting of a sequence of basic name components separated by
    1.45 -  dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
    1.46 -  are examples for qualified names.
    1.47 -
    1.48 -  Despite the independence of names of different kinds, certain naming
    1.49 -  conventions may relate them to each other.  For example, a constant
    1.50 -  \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The same
    1.51 -  could happen for a type \isa{foo}, but this is apt to cause
    1.52 -  clashes in the theorem name space!  To avoid this, there is an
    1.53 -  additional convention to add a suffix that determines the original
    1.54 -  kind.  For example, constant \isa{foo} could associated with
    1.55 -  theorem \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.
    1.56 -
    1.57 -  \medskip Name components are subdivided into \emph{symbols}, which
    1.58 -  constitute the smallest textual unit in Isabelle --- raw characters
    1.59 -  are normally not encountered.%
    1.60 +  For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
    1.61 +  qualified name.  The most basic constituents of names may have their
    1.62 +  own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
    1.63 +  considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
    1.64  \end{isamarkuptext}%
    1.65  \isamarkuptrue%
    1.66  %
    1.67 -\endisatagFIXME
    1.68 -{\isafoldFIXME}%
    1.69 -%
    1.70 -\isadelimFIXME
    1.71 -%
    1.72 -\endisadelimFIXME
    1.73 -%
    1.74  \isamarkupsubsection{Strings of symbols%
    1.75  }
    1.76  \isamarkuptrue%
    1.77  %
    1.78 -\isadelimFIXME
    1.79 -%
    1.80 -\endisadelimFIXME
    1.81 -%
    1.82 -\isatagFIXME
    1.83 -%
    1.84  \begin{isamarkuptext}%
    1.85 -FIXME tune
    1.86 +\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
    1.87 +  plain ASCII characters as well as an infinite collection of named
    1.88 +  symbols (for greek, math etc.).}
    1.89  
    1.90 -  Isabelle strings consist of a sequence of
    1.91 -  symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
    1.92 -  subsumes plain ASCII characters as well as an infinite collection of
    1.93 -  named symbols (for greek, math etc.).}, which are either packed as
    1.94 -  an actual \isa{string}, or represented as a list.  Each symbol
    1.95 -  is in itself a small string of the following form:
    1.96 +  A \emph{symbol} constitutes the smallest textual unit in Isabelle
    1.97 +  --- raw characters are normally not encountered.  Isabelle strings
    1.98 +  consist of a sequence of symbols, represented as a packed string or
    1.99 +  a list of symbols.  Each symbol is in itself a small string, which
   1.100 +  is of one of the following forms:
   1.101  
   1.102    \begin{enumerate}
   1.103  
   1.104 -  \item either a singleton ASCII character ``\isa{c}'' (with
   1.105 -  character code 0--127), for example ``\verb,a,'',
   1.106 +  \item singleton ASCII character ``\isa{c}'' (character code
   1.107 +  0--127), for example ``\verb,a,'',
   1.108  
   1.109 -  \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
   1.110 +  \item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
   1.111 +  for example ``\verb,\,\verb,<alpha>,'',
   1.112  
   1.113 -  \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   1.114 +  \item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
   1.115 +  for example ``\verb,\,\verb,<^bold>,'',
   1.116  
   1.117 -  \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
   1.118 -  character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
   1.119 -  character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   1.120 +  \item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
   1.121 +  \isa{text} is constists of printable characters excluding
   1.122 +  ``\verb,.,'' and ``\verb,>,'', for example
   1.123 +  ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   1.124  
   1.125 -  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
   1.126 +  \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
   1.127    ``\verb,\,\verb,<^raw42>,''.
   1.128  
   1.129    \end{enumerate}
   1.130  
   1.131 -  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
   1.132 -  \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many regular symbols
   1.133 -  and control symbols available, but a certain collection of standard
   1.134 -  symbols is treated specifically.  For example,
   1.135 +  \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
   1.136 +  regular symbols and control symbols, but a fixed collection of
   1.137 +  standard symbols is treated specifically.  For example,
   1.138    ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   1.139    which means it may occur within regular Isabelle identifier syntax.
   1.140  
   1.141 -  Output of symbols depends on the print mode
   1.142 -  (\secref{sec:print-mode}).  For example, the standard {\LaTeX} setup
   1.143 -  of the Isabelle document preparation system would present
   1.144 -  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
   1.145 -  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
   1.146 +  Note that the character set underlying Isabelle symbols is plain
   1.147 +  7-bit ASCII.  Since 8-bit characters are passed through
   1.148 +  transparently, Isabelle may process Unicode/UCS data (in UTF-8
   1.149 +  encoding) as well.  Unicode provides its own collection of
   1.150 +  mathematical symbols, but there is no built-in link to the ones of
   1.151 +  Isabelle.
   1.152  
   1.153 -  \medskip It is important to note that the character set underlying
   1.154 -  Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   1.155 -  passed through transparently, Isabelle may easily process
   1.156 -  Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides
   1.157 -  its own collection of mathematical symbols, but there is no built-in
   1.158 -  link to the ones of Isabelle.%
   1.159 +  \medskip Output of Isabelle symbols depends on the print mode
   1.160 +  (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the
   1.161 +  Isabelle document preparation system would present
   1.162 +  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
   1.163 +  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
   1.164  \end{isamarkuptext}%
   1.165  \isamarkuptrue%
   1.166  %
   1.167 -\endisatagFIXME
   1.168 -{\isafoldFIXME}%
   1.169 -%
   1.170 -\isadelimFIXME
   1.171 -%
   1.172 -\endisadelimFIXME
   1.173 -%
   1.174  \isadelimmlref
   1.175  %
   1.176  \endisadelimmlref
   1.177 @@ -615,15 +569,13 @@
   1.178    type is an alias for \verb|string|, but emphasizes the
   1.179    specific format encountered here.
   1.180  
   1.181 -  \item \verb|Symbol.explode|~\isa{s} produces a symbol list from
   1.182 -  the packed form that is encountered in most practical situations.
   1.183 -  This function supercedes \verb|String.explode| for virtually all
   1.184 -  purposes of manipulating text in Isabelle!  Plain \verb|implode|
   1.185 -  may still be used for the reverse operation.
   1.186 +  \item \verb|Symbol.explode|~\isa{str} produces a symbol list
   1.187 +  from the packed form that.  This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
   1.188 +  Isabelle!
   1.189  
   1.190 -  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
   1.191 -  (both ASCII and several named ones) according to fixed syntactic
   1.192 -  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
   1.193 +  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
   1.194 +  symbols according to fixed syntactic conventions of Isabelle, cf.\
   1.195 +  \cite{isabelle-isar-ref}.
   1.196  
   1.197    \item \verb|Symbol.sym| is a concrete datatype that represents
   1.198    the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
   1.199 @@ -642,45 +594,43 @@
   1.200  %
   1.201  \endisadelimmlref
   1.202  %
   1.203 -\isamarkupsubsection{Qualified names%
   1.204 +\isamarkupsubsection{Basic names \label{sec:basic-names}%
   1.205  }
   1.206  \isamarkuptrue%
   1.207  %
   1.208 -\isadelimFIXME
   1.209 -%
   1.210 -\endisadelimFIXME
   1.211 -%
   1.212 -\isatagFIXME
   1.213 -%
   1.214  \begin{isamarkuptext}%
   1.215 -FIXME tune
   1.216 +A \emph{basic name} essentially consists of a single Isabelle
   1.217 +  identifier.  There are conventions to mark separate classes of basic
   1.218 +  names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
   1.219 +  underscore means \emph{internal name}, two underscores means
   1.220 +  \emph{Skolem name}, three underscores means \emph{internal Skolem
   1.221 +  name}.
   1.222 +
   1.223 +  For example, the basic name \isa{foo} has the internal version
   1.224 +  \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
   1.225  
   1.226 -  A \emph{qualified name} essentially consists of a non-empty list of
   1.227 -  basic name components.  The packad notation uses a dot as separator,
   1.228 -  as in \isa{A{\isachardot}b}, for example.  The very last component is called
   1.229 -  \emph{base} name, the remaining prefix \emph{qualifier} (which may
   1.230 -  be empty).
   1.231 +  Such special versions are required for bookkeeping of names that are
   1.232 +  apart from anything that may appear in the text given by the user.
   1.233 +  In particular, system generated variables in high-level Isar proof
   1.234 +  contexts are usually marked as internal, which prevents mysterious
   1.235 +  name references such as \isa{xaa} in the text.
   1.236 +
   1.237 +  \medskip Basic manipulations of binding scopes requires names to be
   1.238 +  modified.  A \emph{name context} contains a collection of already
   1.239 +  used names, which is maintained by the \isa{declare} operation.
   1.240  
   1.241 -  A \isa{naming} policy tells how to produce fully qualified names
   1.242 -  from a given specification.  The \isa{full} operation applies
   1.243 -  performs naming of a name; the policy is usually taken from the
   1.244 -  context.  For example, a common policy is to attach an implicit
   1.245 -  prefix.
   1.246 +  The \isa{invents} operation derives a number of fresh names
   1.247 +  derived from a given starting point.  For example, three names
   1.248 +  derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
   1.249 +  provided there are no clashes with already used names.
   1.250  
   1.251 -  A \isa{name\ space} manages declarations of fully qualified
   1.252 -  names.  There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
   1.253 -
   1.254 -  FIXME%
   1.255 +  The \isa{variants} operation produces fresh names by
   1.256 +  incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}).  For example, name \isa{foo} results in variants
   1.257 +  \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
   1.258 +  unused variant from this list.%
   1.259  \end{isamarkuptext}%
   1.260  \isamarkuptrue%
   1.261  %
   1.262 -\endisatagFIXME
   1.263 -{\isafoldFIXME}%
   1.264 -%
   1.265 -\isadelimFIXME
   1.266 -%
   1.267 -\endisadelimFIXME
   1.268 -%
   1.269  \isadelimmlref
   1.270  %
   1.271  \endisadelimmlref
   1.272 @@ -688,7 +638,99 @@
   1.273  \isatagmlref
   1.274  %
   1.275  \begin{isamarkuptext}%
   1.276 -FIXME%
   1.277 +\begin{mldecls}
   1.278 +  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
   1.279 +  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
   1.280 +  \indexmltype{Name.context}\verb|type Name.context| \\
   1.281 +  \indexml{Name.context}\verb|Name.context: Name.context| \\
   1.282 +  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
   1.283 +  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
   1.284 +  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
   1.285 +  \end{mldecls}
   1.286 +
   1.287 +  \begin{description}
   1.288 +
   1.289 +  \item \verb|Name.internal|~\isa{name} produces an internal name
   1.290 +  by adding one underscore.
   1.291 +
   1.292 +  \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
   1.293 +  adding two underscores.
   1.294 +
   1.295 +  \item \verb|Name.context| represents the context of already used
   1.296 +  names; the initial value is \verb|Name.context|.
   1.297 +
   1.298 +  \item \verb|Name.declare|~\isa{name} declares \isa{name} as
   1.299 +  being used.
   1.300 +
   1.301 +  \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
   1.302 +
   1.303 +  \end{description}%
   1.304 +\end{isamarkuptext}%
   1.305 +\isamarkuptrue%
   1.306 +%
   1.307 +\endisatagmlref
   1.308 +{\isafoldmlref}%
   1.309 +%
   1.310 +\isadelimmlref
   1.311 +%
   1.312 +\endisadelimmlref
   1.313 +%
   1.314 +\isamarkupsubsection{Indexed names%
   1.315 +}
   1.316 +\isamarkuptrue%
   1.317 +%
   1.318 +\begin{isamarkuptext}%
   1.319 +An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
   1.320 +  name with a natural number.  This representation allows efficient
   1.321 +  renaming by incrementing the second component only.  To rename two
   1.322 +  collections of indexnames apart from each other, first determine the
   1.323 +  maximum index \isa{maxidx} of the first collection, then
   1.324 +  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}}}.
   1.325 +
   1.326 +  Isabelle syntax observes the following rules for representing an
   1.327 +  indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
   1.328 +
   1.329 +  \begin{itemize}
   1.330 +
   1.331 +  \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
   1.332 +
   1.333 +  \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
   1.334 +
   1.335 +  \item \isa{{\isacharquery}x{\isachardot}i} else.
   1.336 +
   1.337 +  \end{itemize}
   1.338 +
   1.339 +  Occasionally, basic names and indexed names are injected into the
   1.340 +  same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
   1.341 +  to encode basic names.
   1.342 +
   1.343 +  \medskip Indexnames may acquire arbitrary large index numbers over
   1.344 +  time.  Results are usually normalized towards \isa{{\isadigit{0}}} at certain
   1.345 +  checkpoints, such that the very end of a proof.  This works by
   1.346 +  producing variants of the corresponding basic names
   1.347 +  (\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}.%
   1.348 +\end{isamarkuptext}%
   1.349 +\isamarkuptrue%
   1.350 +%
   1.351 +\isadelimmlref
   1.352 +%
   1.353 +\endisadelimmlref
   1.354 +%
   1.355 +\isatagmlref
   1.356 +%
   1.357 +\begin{isamarkuptext}%
   1.358 +\begin{mldecls}
   1.359 +  \indexmltype{indexname}\verb|type indexname| \\
   1.360 +  \end{mldecls}
   1.361 +
   1.362 +  \begin{description}
   1.363 +
   1.364 +  \item \verb|indexname| represents indexed names.  This is an
   1.365 +  abbreviation for \verb|string * int|.  The second component is
   1.366 +  usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
   1.367 +  is used to embed plain names.
   1.368 +
   1.369 +  \end{description}%
   1.370  \end{isamarkuptext}%
   1.371  \isamarkuptrue%
   1.372  %
   1.373 @@ -699,36 +741,153 @@
   1.374  %
   1.375  \endisadelimmlref
   1.376  %
   1.377 -\isamarkupsection{Structured output%
   1.378 -}
   1.379 -\isamarkuptrue%
   1.380 -%
   1.381 -\isamarkupsubsection{Pretty printing%
   1.382 +\isamarkupsubsection{Qualified names and name spaces%
   1.383  }
   1.384  \isamarkuptrue%
   1.385  %
   1.386  \begin{isamarkuptext}%
   1.387 -FIXME%
   1.388 +A \emph{qualified name} consists of a non-empty sequence of basic
   1.389 +  name components.  The packed representation a dot as separator, for
   1.390 +  example in ``\isa{A{\isachardot}b{\isachardot}c}''.  The last component is called
   1.391 +  \emph{base} name, the remaining prefix \emph{qualifier} (which may
   1.392 +  be empty).
   1.393 +
   1.394 +  The empty name is commonly used as an indication of unnamed
   1.395 +  entities, if this makes any sense.  The operations on qualified
   1.396 +  names are smart enough to pass through such improper names
   1.397 +  unchanged.
   1.398 +
   1.399 +  The basic idea of qualified names is to encode a hierarchically
   1.400 +  structured name spaces by recording the access path as part of the
   1.401 +  name.  For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
   1.402 +  entity \isa{c} within a local structure \isa{b} of the
   1.403 +  enclosing structure \isa{A}.  Typically, name space hierarchies
   1.404 +  consist of 1--3 levels, but this need not be always so.
   1.405 +
   1.406 +  \medskip A \isa{naming} policy tells how to turn a name
   1.407 +  specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
   1.408 +  externally.
   1.409 +
   1.410 +  For example, the default naming prefixes an implicit path from the
   1.411 +  context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
   1.412 +  standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
   1.413 +  partial \isa{path} specifications.
   1.414 +
   1.415 +  Normally, the naming is implicit in the theory or proof context.
   1.416 +  There are separate versions of the corresponding operations for these
   1.417 +  context types.
   1.418 +
   1.419 +  \medskip A \isa{name\ space} manages a collection of fully
   1.420 +  internalized names, together with a mapping between external names
   1.421 +  and internal names (in both directions).  The corresponding \isa{intern} and \isa{extern} operations are mostly used for
   1.422 +  parsing and printing only!  The \isa{declare} operation augments
   1.423 +  a name space according to a given naming policy.
   1.424 +
   1.425 +  By general convention, there are separate name spaces for each kind
   1.426 +  of formal entity, such as logical constant, type, type class,
   1.427 +  theorem etc.  It is usually clear from the occurrence in concrete
   1.428 +  syntax (or from the scope) which kind of entity a name refers to.
   1.429 +
   1.430 +  For example, the very same name \isa{c} may be used uniformly
   1.431 +  for a constant, type, type class, which are from separate syntactic
   1.432 +  categories.  There is a common convention to name theorems
   1.433 +  systematically, according to the name of the main logical entity
   1.434 +  being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
   1.435 +  theorems related to constant \isa{c}.
   1.436 +
   1.437 +  This technique of mapping names from one space into another requires
   1.438 +  some care in order to avoid conflicts.  In particular, theorem names
   1.439 +  derived from type or class names are better suffixed in addition to
   1.440 +  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
   1.441 +  \isa{c}, respectively.%
   1.442  \end{isamarkuptext}%
   1.443  \isamarkuptrue%
   1.444  %
   1.445 -\isamarkupsubsection{Output channels%
   1.446 -}
   1.447 -\isamarkuptrue%
   1.448 +\isadelimmlref
   1.449 +%
   1.450 +\endisadelimmlref
   1.451 +%
   1.452 +\isatagmlref
   1.453  %
   1.454  \begin{isamarkuptext}%
   1.455 -FIXME%
   1.456 +\begin{mldecls}
   1.457 +  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
   1.458 +  \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
   1.459 +  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
   1.460 +  \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
   1.461 +  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
   1.462 +  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   1.463 +  \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
   1.464 +  \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
   1.465 +  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
   1.466 +  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
   1.467 +  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
   1.468 +  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
   1.469 +  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
   1.470 +  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
   1.471 +  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
   1.472 +  \end{mldecls}
   1.473 +
   1.474 +  \begin{description}
   1.475 +
   1.476 +  \item \verb|NameSpace.base|~\isa{name} returns the base name of a
   1.477 +  qualified name.
   1.478 +
   1.479 +  \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
   1.480 +  of a qualified name.
   1.481 +
   1.482 +  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
   1.483 +  appends two qualified names.
   1.484 +
   1.485 +  \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
   1.486 +  string representation and explicit list form of qualified names.
   1.487 +
   1.488 +  \item \verb|NameSpace.naming| represents the abstract concept of
   1.489 +  a naming policy.
   1.490 +
   1.491 +  \item \verb|NameSpace.default_naming| is the default naming policy.
   1.492 +  In a theory context, this is usually augmented by a path prefix
   1.493 +  consisting of the theory name.
   1.494 +
   1.495 +  \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
   1.496 +  naming policy by extending its path.
   1.497 +
   1.498 +  \item \verb|NameSpace.full|\isa{naming\ name} turns a name
   1.499 +  specification (usually a basic name) into the fully qualified
   1.500 +  internal version, according to the given naming policy.
   1.501 +
   1.502 +  \item \verb|NameSpace.T| represents name spaces.
   1.503 +
   1.504 +  \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
   1.505 +  building name spaces in accordance to the usual theory data
   1.506 +  management (\secref{sec:context-data}).
   1.507 +
   1.508 +  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
   1.509 +  fully qualified name into the name space, with partial accesses
   1.510 +  being derived from the given policy.
   1.511 +
   1.512 +  \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
   1.513 +  (partially qualified) external name.
   1.514 +
   1.515 +  This operation is mostly for parsing.  Note that fully qualified
   1.516 +  names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
   1.517 +
   1.518 +  \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
   1.519 +  (fully qualified) internal name.
   1.520 +
   1.521 +  This operation is mostly for printing.  Note unqualified names are
   1.522 +  produced via \verb|NameSpace.base|.
   1.523 +
   1.524 +  \end{description}%
   1.525  \end{isamarkuptext}%
   1.526  \isamarkuptrue%
   1.527  %
   1.528 -\isamarkupsubsection{Print modes \label{sec:print-mode}%
   1.529 -}
   1.530 -\isamarkuptrue%
   1.531 +\endisatagmlref
   1.532 +{\isafoldmlref}%
   1.533  %
   1.534 -\begin{isamarkuptext}%
   1.535 -FIXME%
   1.536 -\end{isamarkuptext}%
   1.537 -\isamarkuptrue%
   1.538 +\isadelimmlref
   1.539 +%
   1.540 +\endisadelimmlref
   1.541  %
   1.542  \isadelimtheory
   1.543  %