--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Sep 07 15:16:41 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Sep 07 15:16:51 2006 +0200
@@ -155,8 +155,8 @@
\medskip There is a separate notion of \emph{theory reference} for
maintaining a live link to an evolving theory context: updates on
- drafts are propagated automatically. The dynamic stops after an
- explicit \isa{end} only.
+ drafts are propagated automatically. Dynamic updating stops after
+ an explicit \isa{end} only.
Derived entities may store a theory reference in order to indicate
the context they belong to. This implicitly assumes monotonic
@@ -479,12 +479,10 @@
%
\begin{isamarkuptext}%
In principle, a name is just a string, but there are various
- convention for encoding additional structure.
-
- For example, the string ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a
- qualified name. The most basic constituents of names may have their
- own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
- considered as a single symbol (printed as ``\isa{{\isasymalpha}}'').%
+ convention for encoding additional structure. For example, ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a qualified name consisting of
+ three basic name components. The individual constituents of a name
+ may have further substructure, e.g.\ the string
+ ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -498,28 +496,28 @@
symbols (for greek, math etc.).}
A \emph{symbol} constitutes the smallest textual unit in Isabelle
- --- raw characters are normally not encountered. Isabelle strings
- consist of a sequence of symbols, represented as a packed string or
- a list of symbols. Each symbol is in itself a small string, which
- is of one of the following forms:
+ --- raw characters are normally not encountered at all. Isabelle
+ strings consist of a sequence of symbols, represented as a packed
+ string or a list of strings. Each symbol is in itself a small
+ string, which has either one of the following forms:
\begin{enumerate}
- \item singleton ASCII character ``\isa{c}'' (character code
- 0--127), for example ``\verb,a,'',
+ \item a single ASCII character ``\isa{c}'', for example
+ ``\verb,a,'',
- \item regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
+ \item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
- \item control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
+ \item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<^bold>,'',
- \item raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,'' where
- \isa{text} is constists of printable characters excluding
+ \item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''
+ where \isa{text} constists of printable characters excluding
``\verb,.,'' and ``\verb,>,'', for example
``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
- \item numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
+ \item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
``\verb,\,\verb,<^raw42>,''.
\end{enumerate}
@@ -527,15 +525,14 @@
\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
regular symbols and control symbols, but a fixed 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.
+ ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
+ may occur within regular Isabelle identifiers.
- Note that the character set underlying Isabelle symbols is plain
- 7-bit ASCII. Since 8-bit characters are passed through
- transparently, Isabelle may process Unicode/UCS data (in UTF-8
- encoding) as well. Unicode provides its own collection of
- mathematical symbols, but there is no built-in link to the ones of
- Isabelle.
+ Since the character set underlying Isabelle symbols is 7-bit ASCII
+ and 8-bit characters are passed through transparently, Isabelle may
+ also process Unicode/UCS data in UTF-8 encoding. Unicode provides
+ its own collection of mathematical symbols, but there is no built-in
+ link to the standard collection of Isabelle.
\medskip Output of Isabelle symbols depends on the print mode
(\secref{FIXME}). For example, the standard {\LaTeX} setup of the
@@ -565,12 +562,11 @@
\begin{description}
- \item \verb|Symbol.symbol| represents Isabelle symbols. This
- type is an alias for \verb|string|, but emphasizes the
- specific format encountered here.
+ \item \verb|Symbol.symbol| represents individual Isabelle
+ symbols; this is an alias for \verb|string|.
\item \verb|Symbol.explode|~\isa{str} produces a symbol list
- from the packed form that. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
+ from the packed form. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
Isabelle!
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
@@ -578,7 +574,7 @@
\cite{isabelle-isar-ref}.
\item \verb|Symbol.sym| is a concrete datatype that represents
- the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
+ the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
symbol into the datatype version.
@@ -609,25 +605,23 @@
For example, the basic name \isa{foo} has the internal version
\isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
- Such special versions are required for bookkeeping of names that are
- apart from anything that may appear in the text given by the user.
- In particular, system generated variables in high-level Isar proof
- contexts are usually marked as internal, which prevents mysterious
- name references such as \isa{xaa} in the text.
+ These special versions provide copies of the basic name space, apart
+ from anything that normally appears in the user text. For example,
+ system generated variables in Isar proof contexts are usually marked
+ as internal, which prevents mysterious name references like \isa{xaa} to appear in the text.
- \medskip Basic manipulations of binding scopes requires names to be
- modified. A \emph{name context} contains a collection of already
- used names, which is maintained by the \isa{declare} operation.
+ \medskip Manipulating binding scopes often requires on-the-fly
+ renamings. A \emph{name context} contains a collection of already
+ used names. The \isa{declare} operation adds names to the
+ context.
- The \isa{invents} operation derives a number of fresh names
- derived from a given starting point. For example, three names
- derived from \isa{a} are \isa{a}, \isa{b}, \isa{c},
- provided there are no clashes with already used names.
+ The \isa{invents} operation derives a number of fresh names from
+ a given starting point. For example, the first three names derived
+ from \isa{a} are \isa{a}, \isa{b}, \isa{c}.
The \isa{variants} operation produces fresh names by
- incrementing given names as to base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}). For example, name \isa{foo} results in variants
- \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab}, \dots; each renaming step picks the next
- unused variant from this list.%
+ incrementing tentative names as base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}) until all clashes are resolved. For example, name \isa{foo} results in variants \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab} etc.; each renaming
+ step picks the next unused variant from this sequence.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -659,10 +653,13 @@
\item \verb|Name.context| represents the context of already used
names; the initial value is \verb|Name.context|.
- \item \verb|Name.declare|~\isa{name} declares \isa{name} as
- being used.
+ \item \verb|Name.declare|~\isa{name} enters a used name into the
+ context.
- \item \verb|Name.invents|~\isa{context\ base\ n} produces \isa{n} fresh names derived from \isa{base}.
+ \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
+
+ \item \verb|Name.variants|~\isa{names\ context} produces fresh
+ varians of \isa{names}; the result is entered into the context.
\end{description}%
\end{isamarkuptext}%
@@ -681,14 +678,20 @@
%
\begin{isamarkuptext}%
An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
- name with a natural number. This representation allows efficient
- renaming by incrementing the second component only. To rename two
- collections of indexnames apart from each other, first determine the
- maximum index \isa{maxidx} of the first collection, then
- 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}}}.
+ name and a natural number. This representation allows efficient
+ renaming by incrementing the second component only. The canonical
+ way to rename two collections of indexnames apart from each other is
+ this: determine the maximum index \isa{maxidx} of the first
+ collection, then increment all indexes of the second collection by
+ \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}; the maximum index of an empty collection is
+ \isa{{\isacharminus}{\isadigit{1}}}.
- Isabelle syntax observes the following rules for representing an
- indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
+ Occasionally, basic names and indexed names are injected into the
+ same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
+ to encode basic names.
+
+ \medskip Isabelle syntax observes the following rules for
+ representing an indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
\begin{itemize}
@@ -696,19 +699,15 @@
\item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
- \item \isa{{\isacharquery}x{\isachardot}i} else.
+ \item \isa{{\isacharquery}x{\isachardot}i} otherwise.
\end{itemize}
- Occasionally, basic names and indexed names are injected into the
- same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
- to encode basic names.
-
- \medskip Indexnames may acquire arbitrary large index numbers over
- time. Results are usually normalized towards \isa{{\isadigit{0}}} at certain
- checkpoints, such that the very end of a proof. This works by
- producing variants of the corresponding basic names
- (\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}.%
+ Indexnames may acquire large index numbers over time. Results are
+ normalized towards \isa{{\isadigit{0}}} at certain checkpoints, notably at
+ the end of a proof. This works by producing variants of the
+ corresponding basic name components. For example, the collection
+ \isa{{\isacharquery}x{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isadigit{4}}{\isadigit{2}}} becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -728,7 +727,7 @@
\item \verb|indexname| represents indexed names. This is an
abbreviation for \verb|string * int|. The second component is
usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
- is used to embed plain names.
+ is used to embed basic names into this type.
\end{description}%
\end{isamarkuptext}%
@@ -747,52 +746,50 @@
%
\begin{isamarkuptext}%
A \emph{qualified name} consists of a non-empty sequence of basic
- name components. The packed representation a dot as separator, for
- example in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called
- \emph{base} name, the remaining prefix \emph{qualifier} (which may
- be empty). The basic idea of qualified names is to encode a
- hierarchically structured name spaces by recording the access path
- as part of the name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood
- as a local entity \isa{c} within a local structure \isa{b}
- of the enclosing structure \isa{A}. Typically, name space
- hierarchies consist of 1--3 levels, but this need not be always so.
+ name components. The packed representation uses a dot as separator,
+ as in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called \emph{base}
+ name, the remaining prefix \emph{qualifier} (which may be empty).
+ The idea of qualified names is to encode nested structures by
+ recording the access paths as qualifiers. For example, an item
+ named ``\isa{A{\isachardot}b{\isachardot}c}'' may be understood as a local entity \isa{c}, within a local structure \isa{b}, within a global
+ structure \isa{A}. Typically, name space hierarchies consist of
+ 1--2 levels of qualification, but this need not be always so.
The empty name is commonly used as an indication of unnamed
- entities, if this makes any sense. The operations on qualified
- names are smart enough to pass through such improper names
+ entities, whenever this makes any sense. The basic operations on
+ qualified names are smart enough to pass through such improper names
unchanged.
\medskip A \isa{naming} policy tells how to turn a name
- specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
- externally. For example, the default naming prefixes an implicit
- path from the context: \isa{x} is becomes \isa{path{\isachardot}x}
- internally; the standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further partial \isa{path} specifications.
- Normally, the naming is implicit in the theory or proof context.
- There are separate versions of the corresponding operations for
- these context types.
+ specification into a fully qualified internal name (by the \isa{full} operation), and how fully qualified names may be accessed
+ externally. For example, the default naming policy is to prefix an
+ implicit path: \isa{full\ x} produces \isa{path{\isachardot}x}, and the
+ standard accesses for \isa{path{\isachardot}x} include both \isa{x} and
+ \isa{path{\isachardot}x}. Normally, the naming is implicit in the theory or
+ proof context; there are separate versions of the corresponding.
\medskip A \isa{name\ space} manages a collection of fully
internalized names, together with a mapping between external names
and internal names (in both directions). The corresponding \isa{intern} and \isa{extern} operations are mostly used for
parsing and printing only! The \isa{declare} operation augments
- a name space according to a given naming policy.
+ a name space according to the accesses determined by the naming
+ policy.
- By general convention, there are separate name spaces for each kind
- of formal entity, such as logical constant, type, type class,
- theorem etc. It is usually clear from the occurrence in concrete
- syntax (or from the scope) which kind of entity a name refers to.
- For example, the very same name \isa{c} may be used uniformly
- for a constant, type, type class, which are from separate syntactic
- categories.
+ \medskip As a general principle, there is a separate name space for
+ each kind of formal entity, e.g.\ logical constant, type
+ constructor, type class, theorem. It is usually clear from the
+ occurrence in concrete syntax (or from the scope) which kind of
+ entity a name refers to. For example, the very same name \isa{c} may be used uniformly for a constant, type constructor, and
+ type class.
There are common schemes to name theorems systematically, according
- to the name of the main logical entity being involved, such as
- \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for theorems related to
- constant \isa{c}. This technique of mapping names from one
- space into another requires some care in order to avoid conflicts.
- In particular, theorem names derived from type or class names are
- better suffixed in addition to 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 \isa{c}, respectively.%
+ to the name of the main logical entity involved, e.g.\ \isa{c{\isachardot}intro} for a canonical theorem related to constant \isa{c}.
+ This technique of mapping names from one space into another requires
+ some care in order to avoid conflicts. In particular, theorem names
+ derived from a type constructor or type class are better suffixed in
+ addition to 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 \isa{c}, respectively.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -805,7 +802,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\
- \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\
+ \indexml{NameSpace.drop-base}\verb|NameSpace.drop_base: string -> string| \\ %FIXME qualifier
\indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
\indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
\indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
@@ -832,8 +829,8 @@
\item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
appends two qualified names.
- \item \verb|NameSpace.pack|~\isa{name} and \isa{NameSpace{\isachardot}unpack}~\isa{names} convert between the packed
- string representation and explicit list form of qualified names.
+ \item \verb|NameSpace.pack|~\isa{name} and \verb|NameSpace.unpack|~\isa{names} convert between the packed string
+ representation and the explicit list form of qualified names.
\item \verb|NameSpace.naming| represents the abstract concept of
a naming policy.
@@ -843,7 +840,7 @@
consisting of the theory name.
\item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
- naming policy by extending its path.
+ naming policy by extending its path component.
\item \verb|NameSpace.full|\isa{naming\ name} turns a name
specification (usually a basic name) into the fully qualified
@@ -851,24 +848,25 @@
\item \verb|NameSpace.T| represents name spaces.
- \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} provide basic operations for
- building name spaces in accordance to the usual theory data
- management (\secref{sec:context-data}).
+ \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
+ maintaining name spaces according to theory data management
+ (\secref{sec:context-data}).
\item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
- fully qualified name into the name space, with partial accesses
- being derived from the given policy.
+ fully qualified name into the name space, with external accesses
+ determined by the naming policy.
\item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
(partially qualified) external name.
- This operation is mostly for parsing. Note that fully qualified
- names stemming from declarations are produced via \verb|NameSpace.full| (or derivatives for \verb|theory| or \verb|Proof.context|).
+ This operation is mostly for parsing! Note that fully qualified
+ names stemming from declarations are produced via \verb|NameSpace.full| (or its derivatives for \verb|theory| and
+ \verb|Proof.context|).
\item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
(fully qualified) internal name.
- This operation is mostly for printing. Note unqualified names are
+ This operation is mostly for printing! Note unqualified names are
produced via \verb|NameSpace.base|.
\end{description}%