# HG changeset patch # User wenzelm # Date 1157635011 -7200 # Node ID e502690952be7ff3fca89b0f3b62bf753f8e3ca3 # Parent a684fc70d04e5899138aa588ae57d2ec200cc776 updated; diff -r a684fc70d04e -r e502690952be doc-src/IsarImplementation/Thy/document/ML.tex --- 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% +% \isadelimtheory % \endisadelimtheory diff -r a684fc70d04e -r e502690952be doc-src/IsarImplementation/Thy/document/prelim.tex --- 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,,'' 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,,'' 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,,'', - \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,,'' is classified as a (non-ASCII) letter, - which means it may occur within regular Isabelle identifier syntax. + ``\verb,\,\verb,,'' 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}%