# HG changeset patch # User wenzelm # Date 1156933719 -7200 # Node ID 9060c73a457867579c61f15cd33222e397efe008 # Parent 0eb5e30fd62008c2b22d76d16523a1eb62267a78 updated; diff -r 0eb5e30fd620 -r 9060c73a4578 doc-src/IsarImplementation/Thy/document/logic.tex --- a/doc-src/IsarImplementation/Thy/document/logic.tex Wed Aug 30 12:28:32 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex Wed Aug 30 12:28:39 2006 +0200 @@ -27,6 +27,15 @@ } \isamarkuptrue% % +\isamarkupsubsection{Variable names% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +FIXME% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Simply-typed lambda calculus% } \isamarkuptrue% diff -r 0eb5e30fd620 -r 9060c73a4578 doc-src/IsarImplementation/Thy/document/prelim.tex --- 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,,'', - -\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,,'' 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,,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' 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,,'', + +\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,,'' 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,,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' 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