tuned;
authorwenzelm
Tue Sep 05 16:42:32 2006 +0200 (2006-09-05)
changeset 20477e623b0e30541
parent 20476 6d3f144cc1bd
child 20478 de1bd9717d6c
tuned;
doc-src/IsarImplementation/Thy/document/isar.tex
doc-src/IsarImplementation/Thy/document/locale.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/locale.thy
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/unused.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/isar.tex	Tue Sep 05 16:42:32 2006 +0200
     1.3 @@ -0,0 +1,82 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{isar}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +\isanewline
    1.10 +\isanewline
    1.11 +\isanewline
    1.12 +%
    1.13 +\endisadelimtheory
    1.14 +%
    1.15 +\isatagtheory
    1.16 +\isacommand{theory}\isamarkupfalse%
    1.17 +\ isar\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    1.18 +\endisatagtheory
    1.19 +{\isafoldtheory}%
    1.20 +%
    1.21 +\isadelimtheory
    1.22 +%
    1.23 +\endisadelimtheory
    1.24 +%
    1.25 +\isamarkupchapter{Isar proof texts%
    1.26 +}
    1.27 +\isamarkuptrue%
    1.28 +%
    1.29 +\isamarkupsection{Proof states \label{sec:isar-proof-state}%
    1.30 +}
    1.31 +\isamarkuptrue%
    1.32 +%
    1.33 +\begin{isamarkuptext}%
    1.34 +FIXME
    1.35 +
    1.36 +\glossary{Proof state}{The whole configuration of a structured proof,
    1.37 +consisting of a \seeglossary{proof context} and an optional
    1.38 +\seeglossary{structured goal}.  Internally, an Isar proof state is
    1.39 +organized as a stack to accomodate block structure of proof texts.
    1.40 +For historical reasons, a low-level \seeglossary{tactical goal} is
    1.41 +occasionally called ``proof state'' as well.}
    1.42 +
    1.43 +\glossary{Structured goal}{FIXME}
    1.44 +
    1.45 +\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
    1.46 +\end{isamarkuptext}%
    1.47 +\isamarkuptrue%
    1.48 +%
    1.49 +\isamarkupsection{Proof methods%
    1.50 +}
    1.51 +\isamarkuptrue%
    1.52 +%
    1.53 +\begin{isamarkuptext}%
    1.54 +FIXME%
    1.55 +\end{isamarkuptext}%
    1.56 +\isamarkuptrue%
    1.57 +%
    1.58 +\isamarkupsection{Attributes%
    1.59 +}
    1.60 +\isamarkuptrue%
    1.61 +%
    1.62 +\begin{isamarkuptext}%
    1.63 +FIXME ?!%
    1.64 +\end{isamarkuptext}%
    1.65 +\isamarkuptrue%
    1.66 +%
    1.67 +\isadelimtheory
    1.68 +%
    1.69 +\endisadelimtheory
    1.70 +%
    1.71 +\isatagtheory
    1.72 +\isacommand{end}\isamarkupfalse%
    1.73 +%
    1.74 +\endisatagtheory
    1.75 +{\isafoldtheory}%
    1.76 +%
    1.77 +\isadelimtheory
    1.78 +%
    1.79 +\endisadelimtheory
    1.80 +\isanewline
    1.81 +\end{isabellebody}%
    1.82 +%%% Local Variables:
    1.83 +%%% mode: latex
    1.84 +%%% TeX-master: "root"
    1.85 +%%% End:
     2.1 --- a/doc-src/IsarImplementation/Thy/document/locale.tex	Tue Sep 05 16:42:23 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/locale.tex	Tue Sep 05 16:42:32 2006 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{Localized theory specifications%
     2.8 +\isamarkupsection{Local theories%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 05 16:42:23 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 05 16:42:32 2006 +0200
     3.3 @@ -23,15 +23,6 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsection{Names%
     3.8 -}
     3.9 -\isamarkuptrue%
    3.10 -%
    3.11 -\begin{isamarkuptext}%
    3.12 -FIXME%
    3.13 -\end{isamarkuptext}%
    3.14 -\isamarkuptrue%
    3.15 -%
    3.16  \isamarkupsection{Types \label{sec:types}%
    3.17  }
    3.18  \isamarkuptrue%
    3.19 @@ -76,6 +67,15 @@
    3.20  \end{isamarkuptext}%
    3.21  \isamarkuptrue%
    3.22  %
    3.23 +\isamarkupsection{Proof terms%
    3.24 +}
    3.25 +\isamarkuptrue%
    3.26 +%
    3.27 +\begin{isamarkuptext}%
    3.28 +FIXME%
    3.29 +\end{isamarkuptext}%
    3.30 +\isamarkuptrue%
    3.31 +%
    3.32  \isamarkupsection{Theorems \label{sec:thms}%
    3.33  }
    3.34  \isamarkuptrue%
    3.35 @@ -155,7 +155,7 @@
    3.36  \end{isamarkuptext}%
    3.37  \isamarkuptrue%
    3.38  %
    3.39 -\isamarkupsection{Low-level specifications%
    3.40 +\isamarkupsection{Raw theories%
    3.41  }
    3.42  \isamarkuptrue%
    3.43  %
     4.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Tue Sep 05 16:42:23 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Tue Sep 05 16:42:32 2006 +0200
     4.3 @@ -357,7 +357,7 @@
     4.4  %
     4.5  \endisadelimmlref
     4.6  %
     4.7 -\isamarkupsubsection{Context data%
     4.8 +\isamarkupsubsection{Context data \label{sec:context-data}%
     4.9  }
    4.10  \isamarkuptrue%
    4.11  %
    4.12 @@ -473,124 +473,78 @@
    4.13  %
    4.14  \endisadelimmlref
    4.15  %
    4.16 -\isamarkupsection{Name spaces%
    4.17 +\isamarkupsection{Names%
    4.18  }
    4.19  \isamarkuptrue%
    4.20  %
    4.21 -\isadelimFIXME
    4.22 -%
    4.23 -\endisadelimFIXME
    4.24 -%
    4.25 -\isatagFIXME
    4.26 -%
    4.27  \begin{isamarkuptext}%
    4.28 -FIXME tune
    4.29 +In principle, a name is just a string, but there are various
    4.30 +  convention for encoding additional structure.
    4.31  
    4.32 -  By general convention, each kind of formal entities (logical
    4.33 -  constant, type, type class, theorem, method etc.) lives in a
    4.34 -  separate name space.  It is usually clear from the syntactic context
    4.35 -  of a name, which kind of entity it refers to.  For example, proof
    4.36 -  method \isa{foo} vs.\ theorem \isa{foo} vs.\ logical
    4.37 -  constant \isa{foo} are easily distinguished thanks to the design
    4.38 -  of the concrete outer syntax.  A notable exception are logical
    4.39 -  identifiers within a term (\secref{sec:terms}): constants, fixed
    4.40 -  variables, and bound variables all share the same identifier syntax,
    4.41 -  but are distinguished by their scope.
    4.42 -
    4.43 -  Name spaces are organized uniformly, as a collection of qualified
    4.44 -  names consisting of a sequence of basic name components separated by
    4.45 -  dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
    4.46 -  are examples for qualified names.
    4.47 -
    4.48 -  Despite the independence of names of different kinds, certain naming
    4.49 -  conventions may relate them to each other.  For example, a constant
    4.50 -  \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The same
    4.51 -  could happen for a type \isa{foo}, but this is apt to cause
    4.52 -  clashes in the theorem name space!  To avoid this, there is an
    4.53 -  additional convention to add a suffix that determines the original
    4.54 -  kind.  For example, constant \isa{foo} could associated with
    4.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}.
    4.56 -
    4.57 -  \medskip Name components are subdivided into \emph{symbols}, which
    4.58 -  constitute the smallest textual unit in Isabelle --- raw characters
    4.59 -  are normally not encountered.%
    4.60 +  For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
    4.61 +  qualified name.  The most basic constituents of names may have their
    4.62 +  own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
    4.63 +  considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
    4.64  \end{isamarkuptext}%
    4.65  \isamarkuptrue%
    4.66  %
    4.67 -\endisatagFIXME
    4.68 -{\isafoldFIXME}%
    4.69 -%
    4.70 -\isadelimFIXME
    4.71 -%
    4.72 -\endisadelimFIXME
    4.73 -%
    4.74  \isamarkupsubsection{Strings of symbols%
    4.75  }
    4.76  \isamarkuptrue%
    4.77  %
    4.78 -\isadelimFIXME
    4.79 -%
    4.80 -\endisadelimFIXME
    4.81 -%
    4.82 -\isatagFIXME
    4.83 -%
    4.84  \begin{isamarkuptext}%
    4.85 -FIXME tune
    4.86 +\glossary{Symbol}{The smallest unit of text in Isabelle, subsumes
    4.87 +  plain ASCII characters as well as an infinite collection of named
    4.88 +  symbols (for greek, math etc.).}
    4.89  
    4.90 -  Isabelle strings consist of a sequence of
    4.91 -  symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
    4.92 -  subsumes plain ASCII characters as well as an infinite collection of
    4.93 -  named symbols (for greek, math etc.).}, which are either packed as
    4.94 -  an actual \isa{string}, or represented as a list.  Each symbol
    4.95 -  is in itself a small string of the following form:
    4.96 +  A \emph{symbol} constitutes the smallest textual unit in Isabelle
    4.97 +  --- raw characters are normally not encountered.  Isabelle strings
    4.98 +  consist of a sequence of symbols, represented as a packed string or
    4.99 +  a list of symbols.  Each symbol is in itself a small string, which
   4.100 +  is of one of the following forms:
   4.101  
   4.102    \begin{enumerate}
   4.103  
   4.104 -  \item either a singleton ASCII character ``\isa{c}'' (with
   4.105 -  character code 0--127), for example ``\verb,a,'',
   4.106 +  \item singleton ASCII character ``\isa{c}'' (character code
   4.107 +  0--127), for example ``\verb,a,'',
   4.108  
   4.109 -  \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
   4.110 +  \item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
   4.111 +  for example ``\verb,\,\verb,<alpha>,'',
   4.112  
   4.113 -  \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   4.114 +  \item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
   4.115 +  for example ``\verb,\,\verb,<^bold>,'',
   4.116  
   4.117 -  \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
   4.118 -  character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
   4.119 -  character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   4.120 +  \item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
   4.121 +  \isa{text} is constists of printable characters excluding
   4.122 +  ``\verb,.,'' and ``\verb,>,'', for example
   4.123 +  ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   4.124  
   4.125 -  \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
   4.126 +  \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
   4.127    ``\verb,\,\verb,<^raw42>,''.
   4.128  
   4.129    \end{enumerate}
   4.130  
   4.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
   4.132 -  \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}.  There are infinitely many regular symbols
   4.133 -  and control symbols available, but a certain collection of standard
   4.134 -  symbols is treated specifically.  For example,
   4.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
   4.136 +  regular symbols and control symbols, but a fixed collection of
   4.137 +  standard symbols is treated specifically.  For example,
   4.138    ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   4.139    which means it may occur within regular Isabelle identifier syntax.
   4.140  
   4.141 -  Output of symbols depends on the print mode
   4.142 -  (\secref{sec:print-mode}).  For example, the standard {\LaTeX} setup
   4.143 -  of the Isabelle document preparation system would present
   4.144 -  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
   4.145 -  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
   4.146 +  Note that the character set underlying Isabelle symbols is plain
   4.147 +  7-bit ASCII.  Since 8-bit characters are passed through
   4.148 +  transparently, Isabelle may process Unicode/UCS data (in UTF-8
   4.149 +  encoding) as well.  Unicode provides its own collection of
   4.150 +  mathematical symbols, but there is no built-in link to the ones of
   4.151 +  Isabelle.
   4.152  
   4.153 -  \medskip It is important to note that the character set underlying
   4.154 -  Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   4.155 -  passed through transparently, Isabelle may easily process
   4.156 -  Unicode/UCS data as well (using UTF-8 encoding).  Unicode provides
   4.157 -  its own collection of mathematical symbols, but there is no built-in
   4.158 -  link to the ones of Isabelle.%
   4.159 +  \medskip Output of Isabelle symbols depends on the print mode
   4.160 +  (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the
   4.161 +  Isabelle document preparation system would present
   4.162 +  ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
   4.163 +  ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
   4.164  \end{isamarkuptext}%
   4.165  \isamarkuptrue%
   4.166  %
   4.167 -\endisatagFIXME
   4.168 -{\isafoldFIXME}%
   4.169 -%
   4.170 -\isadelimFIXME
   4.171 -%
   4.172 -\endisadelimFIXME
   4.173 -%
   4.174  \isadelimmlref
   4.175  %
   4.176  \endisadelimmlref
   4.177 @@ -615,15 +569,13 @@
   4.178    type is an alias for \verb|string|, but emphasizes the
   4.179    specific format encountered here.
   4.180  
   4.181 -  \item \verb|Symbol.explode|~\isa{s} produces a symbol list from
   4.182 -  the packed form that is encountered in most practical situations.
   4.183 -  This function supercedes \verb|String.explode| for virtually all
   4.184 -  purposes of manipulating text in Isabelle!  Plain \verb|implode|
   4.185 -  may still be used for the reverse operation.
   4.186 +  \item \verb|Symbol.explode|~\isa{str} produces a symbol list
   4.187 +  from the packed form that.  This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
   4.188 +  Isabelle!
   4.189  
   4.190 -  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
   4.191 -  (both ASCII and several named ones) according to fixed syntactic
   4.192 -  conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
   4.193 +  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
   4.194 +  symbols according to fixed syntactic conventions of Isabelle, cf.\
   4.195 +  \cite{isabelle-isar-ref}.
   4.196  
   4.197    \item \verb|Symbol.sym| is a concrete datatype that represents
   4.198    the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
   4.199 @@ -642,45 +594,43 @@
   4.200  %
   4.201  \endisadelimmlref
   4.202  %
   4.203 -\isamarkupsubsection{Qualified names%
   4.204 +\isamarkupsubsection{Basic names \label{sec:basic-names}%
   4.205  }
   4.206  \isamarkuptrue%
   4.207  %
   4.208 -\isadelimFIXME
   4.209 -%
   4.210 -\endisadelimFIXME
   4.211 -%
   4.212 -\isatagFIXME
   4.213 -%
   4.214  \begin{isamarkuptext}%
   4.215 -FIXME tune
   4.216 +A \emph{basic name} essentially consists of a single Isabelle
   4.217 +  identifier.  There are conventions to mark separate classes of basic
   4.218 +  names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
   4.219 +  underscore means \emph{internal name}, two underscores means
   4.220 +  \emph{Skolem name}, three underscores means \emph{internal Skolem
   4.221 +  name}.
   4.222 +
   4.223 +  For example, the basic name \isa{foo} has the internal version
   4.224 +  \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
   4.225  
   4.226 -  A \emph{qualified name} essentially consists of a non-empty list of
   4.227 -  basic name components.  The packad notation uses a dot as separator,
   4.228 -  as in \isa{A{\isachardot}b}, for example.  The very last component is called
   4.229 -  \emph{base} name, the remaining prefix \emph{qualifier} (which may
   4.230 -  be empty).
   4.231 +  Such special versions are required for bookkeeping of names that are
   4.232 +  apart from anything that may appear in the text given by the user.
   4.233 +  In particular, system generated variables in high-level Isar proof
   4.234 +  contexts are usually marked as internal, which prevents mysterious
   4.235 +  name references such as \isa{xaa} in the text.
   4.236 +
   4.237 +  \medskip Basic manipulations of binding scopes requires names to be
   4.238 +  modified.  A \emph{name context} contains a collection of already
   4.239 +  used names, which is maintained by the \isa{declare} operation.
   4.240  
   4.241 -  A \isa{naming} policy tells how to produce fully qualified names
   4.242 -  from a given specification.  The \isa{full} operation applies
   4.243 -  performs naming of a name; the policy is usually taken from the
   4.244 -  context.  For example, a common policy is to attach an implicit
   4.245 -  prefix.
   4.246 +  The \isa{invents} operation derives a number of fresh names
   4.247 +  derived from a given starting point.  For example, three names
   4.248 +  derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
   4.249 +  provided there are no clashes with already used names.
   4.250  
   4.251 -  A \isa{name\ space} manages declarations of fully qualified
   4.252 -  names.  There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
   4.253 -
   4.254 -  FIXME%
   4.255 +  The \isa{variants} operation produces fresh names by
   4.256 +  incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}).  For example, name \isa{foo} results in variants
   4.257 +  \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
   4.258 +  unused variant from this list.%
   4.259  \end{isamarkuptext}%
   4.260  \isamarkuptrue%
   4.261  %
   4.262 -\endisatagFIXME
   4.263 -{\isafoldFIXME}%
   4.264 -%
   4.265 -\isadelimFIXME
   4.266 -%
   4.267 -\endisadelimFIXME
   4.268 -%
   4.269  \isadelimmlref
   4.270  %
   4.271  \endisadelimmlref
   4.272 @@ -688,7 +638,99 @@
   4.273  \isatagmlref
   4.274  %
   4.275  \begin{isamarkuptext}%
   4.276 -FIXME%
   4.277 +\begin{mldecls}
   4.278 +  \indexml{Name.internal}\verb|Name.internal: string -> string| \\
   4.279 +  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
   4.280 +  \indexmltype{Name.context}\verb|type Name.context| \\
   4.281 +  \indexml{Name.context}\verb|Name.context: Name.context| \\
   4.282 +  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
   4.283 +  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
   4.284 +  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
   4.285 +  \end{mldecls}
   4.286 +
   4.287 +  \begin{description}
   4.288 +
   4.289 +  \item \verb|Name.internal|~\isa{name} produces an internal name
   4.290 +  by adding one underscore.
   4.291 +
   4.292 +  \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
   4.293 +  adding two underscores.
   4.294 +
   4.295 +  \item \verb|Name.context| represents the context of already used
   4.296 +  names; the initial value is \verb|Name.context|.
   4.297 +
   4.298 +  \item \verb|Name.declare|~\isa{name} declares \isa{name} as
   4.299 +  being used.
   4.300 +
   4.301 +  \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
   4.302 +
   4.303 +  \end{description}%
   4.304 +\end{isamarkuptext}%
   4.305 +\isamarkuptrue%
   4.306 +%
   4.307 +\endisatagmlref
   4.308 +{\isafoldmlref}%
   4.309 +%
   4.310 +\isadelimmlref
   4.311 +%
   4.312 +\endisadelimmlref
   4.313 +%
   4.314 +\isamarkupsubsection{Indexed names%
   4.315 +}
   4.316 +\isamarkuptrue%
   4.317 +%
   4.318 +\begin{isamarkuptext}%
   4.319 +An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
   4.320 +  name with a natural number.  This representation allows efficient
   4.321 +  renaming by incrementing the second component only.  To rename two
   4.322 +  collections of indexnames apart from each other, first determine the
   4.323 +  maximum index \isa{maxidx} of the first collection, then
   4.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}}}.
   4.325 +
   4.326 +  Isabelle syntax observes the following rules for representing an
   4.327 +  indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
   4.328 +
   4.329 +  \begin{itemize}
   4.330 +
   4.331 +  \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
   4.332 +
   4.333 +  \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
   4.334 +
   4.335 +  \item \isa{{\isacharquery}x{\isachardot}i} else.
   4.336 +
   4.337 +  \end{itemize}
   4.338 +
   4.339 +  Occasionally, basic names and indexed names are injected into the
   4.340 +  same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
   4.341 +  to encode basic names.
   4.342 +
   4.343 +  \medskip Indexnames may acquire arbitrary large index numbers over
   4.344 +  time.  Results are usually normalized towards \isa{{\isadigit{0}}} at certain
   4.345 +  checkpoints, such that the very end of a proof.  This works by
   4.346 +  producing variants of the corresponding basic names
   4.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}.%
   4.348 +\end{isamarkuptext}%
   4.349 +\isamarkuptrue%
   4.350 +%
   4.351 +\isadelimmlref
   4.352 +%
   4.353 +\endisadelimmlref
   4.354 +%
   4.355 +\isatagmlref
   4.356 +%
   4.357 +\begin{isamarkuptext}%
   4.358 +\begin{mldecls}
   4.359 +  \indexmltype{indexname}\verb|type indexname| \\
   4.360 +  \end{mldecls}
   4.361 +
   4.362 +  \begin{description}
   4.363 +
   4.364 +  \item \verb|indexname| represents indexed names.  This is an
   4.365 +  abbreviation for \verb|string * int|.  The second component is
   4.366 +  usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
   4.367 +  is used to embed plain names.
   4.368 +
   4.369 +  \end{description}%
   4.370  \end{isamarkuptext}%
   4.371  \isamarkuptrue%
   4.372  %
   4.373 @@ -699,36 +741,153 @@
   4.374  %
   4.375  \endisadelimmlref
   4.376  %
   4.377 -\isamarkupsection{Structured output%
   4.378 -}
   4.379 -\isamarkuptrue%
   4.380 -%
   4.381 -\isamarkupsubsection{Pretty printing%
   4.382 +\isamarkupsubsection{Qualified names and name spaces%
   4.383  }
   4.384  \isamarkuptrue%
   4.385  %
   4.386  \begin{isamarkuptext}%
   4.387 -FIXME%
   4.388 +A \emph{qualified name} consists of a non-empty sequence of basic
   4.389 +  name components.  The packed representation a dot as separator, for
   4.390 +  example in ``\isa{A{\isachardot}b{\isachardot}c}''.  The last component is called
   4.391 +  \emph{base} name, the remaining prefix \emph{qualifier} (which may
   4.392 +  be empty).
   4.393 +
   4.394 +  The empty name is commonly used as an indication of unnamed
   4.395 +  entities, if this makes any sense.  The operations on qualified
   4.396 +  names are smart enough to pass through such improper names
   4.397 +  unchanged.
   4.398 +
   4.399 +  The basic idea of qualified names is to encode a hierarchically
   4.400 +  structured name spaces by recording the access path as part of the
   4.401 +  name.  For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
   4.402 +  entity \isa{c} within a local structure \isa{b} of the
   4.403 +  enclosing structure \isa{A}.  Typically, name space hierarchies
   4.404 +  consist of 1--3 levels, but this need not be always so.
   4.405 +
   4.406 +  \medskip A \isa{naming} policy tells how to turn a name
   4.407 +  specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
   4.408 +  externally.
   4.409 +
   4.410 +  For example, the default naming prefixes an implicit path from the
   4.411 +  context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
   4.412 +  standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
   4.413 +  partial \isa{path} specifications.
   4.414 +
   4.415 +  Normally, the naming is implicit in the theory or proof context.
   4.416 +  There are separate versions of the corresponding operations for these
   4.417 +  context types.
   4.418 +
   4.419 +  \medskip A \isa{name\ space} manages a collection of fully
   4.420 +  internalized names, together with a mapping between external names
   4.421 +  and internal names (in both directions).  The corresponding \isa{intern} and \isa{extern} operations are mostly used for
   4.422 +  parsing and printing only!  The \isa{declare} operation augments
   4.423 +  a name space according to a given naming policy.
   4.424 +
   4.425 +  By general convention, there are separate name spaces for each kind
   4.426 +  of formal entity, such as logical constant, type, type class,
   4.427 +  theorem etc.  It is usually clear from the occurrence in concrete
   4.428 +  syntax (or from the scope) which kind of entity a name refers to.
   4.429 +
   4.430 +  For example, the very same name \isa{c} may be used uniformly
   4.431 +  for a constant, type, type class, which are from separate syntactic
   4.432 +  categories.  There is a common convention to name theorems
   4.433 +  systematically, according to the name of the main logical entity
   4.434 +  being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
   4.435 +  theorems related to constant \isa{c}.
   4.436 +
   4.437 +  This technique of mapping names from one space into another requires
   4.438 +  some care in order to avoid conflicts.  In particular, theorem names
   4.439 +  derived from type or class names are better suffixed in addition to
   4.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
   4.441 +  \isa{c}, respectively.%
   4.442  \end{isamarkuptext}%
   4.443  \isamarkuptrue%
   4.444  %
   4.445 -\isamarkupsubsection{Output channels%
   4.446 -}
   4.447 -\isamarkuptrue%
   4.448 +\isadelimmlref
   4.449 +%
   4.450 +\endisadelimmlref
   4.451 +%
   4.452 +\isatagmlref
   4.453  %
   4.454  \begin{isamarkuptext}%
   4.455 -FIXME%
   4.456 +\begin{mldecls}
   4.457 +  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
   4.458 +  \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
   4.459 +  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
   4.460 +  \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
   4.461 +  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
   4.462 +  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   4.463 +  \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
   4.464 +  \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
   4.465 +  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
   4.466 +  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
   4.467 +  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
   4.468 +  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
   4.469 +  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
   4.470 +  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
   4.471 +  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
   4.472 +  \end{mldecls}
   4.473 +
   4.474 +  \begin{description}
   4.475 +
   4.476 +  \item \verb|NameSpace.base|~\isa{name} returns the base name of a
   4.477 +  qualified name.
   4.478 +
   4.479 +  \item \verb|NameSpace.drop_base|~\isa{name} returns the qualifier
   4.480 +  of a qualified name.
   4.481 +
   4.482 +  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
   4.483 +  appends two qualified names.
   4.484 +
   4.485 +  \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
   4.486 +  string representation and explicit list form of qualified names.
   4.487 +
   4.488 +  \item \verb|NameSpace.naming| represents the abstract concept of
   4.489 +  a naming policy.
   4.490 +
   4.491 +  \item \verb|NameSpace.default_naming| is the default naming policy.
   4.492 +  In a theory context, this is usually augmented by a path prefix
   4.493 +  consisting of the theory name.
   4.494 +
   4.495 +  \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
   4.496 +  naming policy by extending its path.
   4.497 +
   4.498 +  \item \verb|NameSpace.full|\isa{naming\ name} turns a name
   4.499 +  specification (usually a basic name) into the fully qualified
   4.500 +  internal version, according to the given naming policy.
   4.501 +
   4.502 +  \item \verb|NameSpace.T| represents name spaces.
   4.503 +
   4.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
   4.505 +  building name spaces in accordance to the usual theory data
   4.506 +  management (\secref{sec:context-data}).
   4.507 +
   4.508 +  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
   4.509 +  fully qualified name into the name space, with partial accesses
   4.510 +  being derived from the given policy.
   4.511 +
   4.512 +  \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
   4.513 +  (partially qualified) external name.
   4.514 +
   4.515 +  This operation is mostly for parsing.  Note that fully qualified
   4.516 +  names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
   4.517 +
   4.518 +  \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
   4.519 +  (fully qualified) internal name.
   4.520 +
   4.521 +  This operation is mostly for printing.  Note unqualified names are
   4.522 +  produced via \verb|NameSpace.base|.
   4.523 +
   4.524 +  \end{description}%
   4.525  \end{isamarkuptext}%
   4.526  \isamarkuptrue%
   4.527  %
   4.528 -\isamarkupsubsection{Print modes \label{sec:print-mode}%
   4.529 -}
   4.530 -\isamarkuptrue%
   4.531 +\endisatagmlref
   4.532 +{\isafoldmlref}%
   4.533  %
   4.534 -\begin{isamarkuptext}%
   4.535 -FIXME%
   4.536 -\end{isamarkuptext}%
   4.537 -\isamarkuptrue%
   4.538 +\isadelimmlref
   4.539 +%
   4.540 +\endisadelimmlref
   4.541  %
   4.542  \isadelimtheory
   4.543  %
     5.1 --- a/doc-src/IsarImplementation/Thy/locale.thy	Tue Sep 05 16:42:23 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/locale.thy	Tue Sep 05 16:42:32 2006 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  text FIXME
     5.5  
     5.6  
     5.7 -section {* Localized theory specifications *}
     5.8 +section {* Local theories *}
     5.9  
    5.10  text {*
    5.11    FIXME
     6.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 16:42:23 2006 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 16:42:32 2006 +0200
     6.3 @@ -5,11 +5,6 @@
     6.4  
     6.5  chapter {* Primitive logic \label{ch:logic} *}
     6.6  
     6.7 -section {* Names *}
     6.8 -
     6.9 -text FIXME
    6.10 -
    6.11 -
    6.12  section {* Types \label{sec:types} *}
    6.13  
    6.14  text {*
    6.15 @@ -52,6 +47,13 @@
    6.16  *}
    6.17  
    6.18  
    6.19 +section {* Proof terms *}
    6.20 +
    6.21 +text {*
    6.22 +  FIXME
    6.23 +*}
    6.24 +
    6.25 +
    6.26  section {* Theorems \label{sec:thms} *}
    6.27  
    6.28  text {*
    6.29 @@ -122,7 +124,7 @@
    6.30  text FIXME
    6.31  
    6.32  
    6.33 -section {* Low-level specifications *}
    6.34 +section {* Raw theories *}
    6.35  
    6.36  text {*
    6.37  
     7.1 --- a/doc-src/IsarImplementation/Thy/unused.thy	Tue Sep 05 16:42:23 2006 +0200
     7.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy	Tue Sep 05 16:42:32 2006 +0200
     7.3 @@ -1,3 +1,16 @@
     7.4 +section {* Structured output *}
     7.5 +
     7.6 +subsection {* Pretty printing *}
     7.7 +
     7.8 +text FIXME
     7.9 +
    7.10 +subsection {* Output channels *}
    7.11 +
    7.12 +text FIXME
    7.13 +
    7.14 +subsection {* Print modes \label{sec:print-mode} *}
    7.15 +
    7.16 +text FIXME
    7.17  
    7.18  text {*
    7.19