--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Wed Aug 30 12:28:32 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Wed Aug 30 12:28:39 2006 +0200
@@ -23,233 +23,6 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Named entities%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Named entities of different kinds (logical constant, type,
-type class, theorem, method etc.) live in separate name spaces. It is
-usually clear from the occurrence of a name which kind of entity it
-refers to. For example, proof method \isa{foo} vs.\ theorem
-\isa{foo} vs.\ logical constant \isa{foo} are easily
-distinguished by means of the syntactic context. A notable exception
-are logical identifiers within a term (\secref{sec:terms}): constants,
-fixed variables, and bound variables all share the same identifier
-syntax, but are distinguished by their scope.
-
-Each name space is organized as a collection of \emph{qualified
-names}, which consist of a sequence of basic name components separated
-by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
-are examples for valid qualified names. Name components are
-subdivided into \emph{symbols}, which constitute the smallest textual
-unit in Isabelle --- raw characters are normally not encountered
-directly.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Strings of symbols%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle strings consist of a sequence of
-symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
-subsumes plain ASCII characters as well as an infinite collection of
-named symbols (for greek, math etc.).}, which are either packed as an
-actual \isa{string}, or represented as a list. Each symbol is in
-itself a small string of the following form:
-
-\begin{enumerate}
-
-\item either a singleton ASCII character ``\isa{c}'' (with
-character code 0--127), for example ``\verb,a,'',
-
-\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
-for example ``\verb,\,\verb,<alpha>,'',
-
-\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
-
-\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
-printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
-non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
-
-\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
-``\verb,\,\verb,<^raw42>,''.
-
-\end{enumerate}
-
-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 regular symbols and
-control symbols available, but a certain collection of standard
-symbols is treated specifically. For example,
-``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
-which means it may occur within regular Isabelle identifier syntax.
-
-Output of symbols depends on the print mode (\secref{sec:print-mode}).
-For example, the standard {\LaTeX} setup of the Isabelle document
-preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
-
-\medskip It is important to note that the character set underlying
-Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
-passed through transparently, Isabelle may easily process actual
-Unicode/UCS data (using the well-known UTF-8 encoding, for example).
-Unicode provides its own collection of mathematical symbols, but there
-is presently no link to Isabelle's named ones; both kinds of symbols
-coexist independently.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
- \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
- \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
- \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
- \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|Symbol.symbol| represents Isabelle symbols; this type
- is merely an alias for \verb|string|, but emphasizes the
- specific format encountered here.
-
- \item \verb|Symbol.explode|~\isa{s} produces an actual symbol
- list from the packed form usually encountered as user input. This
- function replaces \verb|String.explode| for virtually all purposes
- of manipulating text in Isabelle! Plain \isa{implode} may be
- used for the reverse operation.
-
- \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
- (both ASCII and several named ones) according to fixed syntactic
- convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
-
- \item \verb|Symbol.sym| is a concrete datatype that represents
- the different kinds of symbols explicitly as \verb|Symbol.Char|,
- \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
-
- \item \verb|Symbol.decode| converts the string representation of a
- symbol into the explicit datatype version.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsubsection{Simple names%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Qualified names and name spaces%
-}
-\isamarkuptrue%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
-\begin{isamarkuptext}%
-Qualified names are constructed according to implicit naming
-principles of the present context.
-
-
-The last component is called \emph{base name}; the remaining prefix of
-qualification may be empty.
-
-Some practical conventions help to organize named entities more
-systematically:
-
-\begin{itemize}
-
-\item Names are qualified first by the theory name, second by an
-optional ``structure''. For example, a constant \isa{c} declared
-as part of a certain structure \isa{b} (say a type definition) in
-theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
-
-\item
-
-\item
-
-\item
-
-\item
-
-\end{itemize}
-
-Names of different kinds of entities are basically independent, but
-some practical naming conventions relate them to each other. For
-example, a constant \isa{foo} may be accompanied with theorems
-\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The
-same may happen for a type \isa{foo}, which is then apt to cause
-clashes in the theorem name space! To avoid this, we occasionally
-follow an additional convention of suffixes that determine the
-original kind of entity that a name has been derived. For example,
-constant \isa{foo} is associated with 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}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isamarkupsection{Structured output%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Pretty printing%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Output channels%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Print modes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Contexts \label{sec:context}%
}
\isamarkuptrue%
@@ -482,6 +255,224 @@
%
\endisadelimmlref
%
+\isamarkupsection{Named entities%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Named entities of different kinds (logical constant, type,
+type class, theorem, method etc.) live in separate name spaces. It is
+usually clear from the occurrence of a name which kind of entity it
+refers to. For example, proof method \isa{foo} vs.\ theorem
+\isa{foo} vs.\ logical constant \isa{foo} are easily
+distinguished by means of the syntactic context. A notable exception
+are logical identifiers within a term (\secref{sec:terms}): constants,
+fixed variables, and bound variables all share the same identifier
+syntax, but are distinguished by their scope.
+
+Each name space is organized as a collection of \emph{qualified
+names}, which consist of a sequence of basic name components separated
+by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
+are examples for valid qualified names. Name components are
+subdivided into \emph{symbols}, which constitute the smallest textual
+unit in Isabelle --- raw characters are normally not encountered
+directly.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Strings of symbols%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle strings consist of a sequence of
+symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
+subsumes plain ASCII characters as well as an infinite collection of
+named symbols (for greek, math etc.).}, which are either packed as an
+actual \isa{string}, or represented as a list. Each symbol is in
+itself a small string of the following form:
+
+\begin{enumerate}
+
+\item either a singleton ASCII character ``\isa{c}'' (with
+character code 0--127), for example ``\verb,a,'',
+
+\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
+for example ``\verb,\,\verb,<alpha>,'',
+
+\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+
+\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
+printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
+non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+
+\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
+``\verb,\,\verb,<^raw42>,''.
+
+\end{enumerate}
+
+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 regular symbols and
+control symbols available, but a certain collection of standard
+symbols is treated specifically. For example,
+``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
+which means it may occur within regular Isabelle identifier syntax.
+
+Output of symbols depends on the print mode (\secref{sec:print-mode}).
+For example, the standard {\LaTeX} setup of the Isabelle document
+preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
+
+\medskip It is important to note that the character set underlying
+Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
+passed through transparently, Isabelle may easily process actual
+Unicode/UCS data (using the well-known UTF-8 encoding, for example).
+Unicode provides its own collection of mathematical symbols, but there
+is presently no link to Isabelle's named ones; both kinds of symbols
+coexist independently.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
+ \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
+ \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+ \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
+ \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Symbol.symbol| represents Isabelle symbols; this type
+ is merely an alias for \verb|string|, but emphasizes the
+ specific format encountered here.
+
+ \item \verb|Symbol.explode|~\isa{s} produces an actual symbol
+ list from the packed form usually encountered as user input. This
+ function replaces \verb|String.explode| for virtually all purposes
+ of manipulating text in Isabelle! Plain \isa{implode} may be
+ used for the reverse operation.
+
+ \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
+ (both ASCII and several named ones) according to fixed syntactic
+ convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
+
+ \item \verb|Symbol.sym| is a concrete datatype that represents
+ the different kinds of symbols explicitly as \verb|Symbol.Char|,
+ \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
+
+ \item \verb|Symbol.decode| converts the string representation of a
+ symbol into the explicit datatype version.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Qualified names and name spaces%
+}
+\isamarkuptrue%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isatagFIXME
+%
+\begin{isamarkuptext}%
+Qualified names are constructed according to implicit naming
+principles of the present context.
+
+
+The last component is called \emph{base name}; the remaining prefix of
+qualification may be empty.
+
+Some practical conventions help to organize named entities more
+systematically:
+
+\begin{itemize}
+
+\item Names are qualified first by the theory name, second by an
+optional ``structure''. For example, a constant \isa{c} declared
+as part of a certain structure \isa{b} (say a type definition) in
+theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
+
+\item
+
+\item
+
+\item
+
+\item
+
+\end{itemize}
+
+Names of different kinds of entities are basically independent, but
+some practical naming conventions relate them to each other. For
+example, a constant \isa{foo} may be accompanied with theorems
+\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The
+same may happen for a type \isa{foo}, which is then apt to cause
+clashes in the theorem name space! To avoid this, we occasionally
+follow an additional convention of suffixes that determine the
+original kind of entity that a name has been derived. For example,
+constant \isa{foo} is associated with 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}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagFIXME
+{\isafoldFIXME}%
+%
+\isadelimFIXME
+%
+\endisadelimFIXME
+%
+\isamarkupsection{Structured output%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Pretty printing%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Output channels%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Print modes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory