author wenzelm Thu, 07 Sep 2006 15:16:51 +0200 changeset 20490 e502690952be parent 20489 a684fc70d04e child 20491 98ba42f19995
updated;
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Sep 07 15:16:41 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Sep 07 15:16:51 2006 +0200
@@ -39,6 +39,19 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupchapter{Cookbook%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Defining a method that depends on declarations in the context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
%
\endisadelimtheory
--- 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
-  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

-  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
+  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
\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 @@
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.

-  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}%