# HG changeset patch # User wenzelm # Date 1157634986 -7200 # Node ID 121bc2135bd3a6a2fc834f18f0f58b396970be88 # Parent 6ac7a4fc32a0a0593e83c0e77b9287e4f8a5ba5b tuned; diff -r 6ac7a4fc32a0 -r 121bc2135bd3 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Wed Sep 06 22:48:36 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Thu Sep 07 15:16:26 2006 +0200 @@ -137,8 +137,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 @{text "end"} only. + drafts are propagated automatically. Dynamic updating stops after + an explicit @{text "end"} only. Derived entities may store a theory reference in order to indicate the context they belong to. This implicitly assumes monotonic @@ -408,12 +408,11 @@ text {* In principle, a name is just a string, but there are various - convention for encoding additional structure. - - For example, the string ``@{text "Foo.bar.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 ``@{text "\"}''). + convention for encoding additional structure. For example, ``@{text + "Foo.bar.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. *} @@ -425,28 +424,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 ``@{text "c"}'' (character code - 0--127), for example ``\verb,a,'', + \item a single ASCII character ``@{text "c"}'', for example + ``\verb,a,'', - \item regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'', + \item a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'', for example ``\verb,\,\verb,,'', - \item control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'', + \item a control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'', - \item raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,'' where - @{text text} is constists of printable characters excluding + \item a raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,'' + where @{text 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,@{text + \item a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text n}\verb,>, where @{text n} consists of digits, for example ``\verb,\,\verb,<^raw42>,''. @@ -457,15 +456,14 @@ A..Za..z"} and @{text "digit = 0..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 @@ -489,12 +487,11 @@ \begin{description} - \item @{ML_type "Symbol.symbol"} represents Isabelle symbols. This - type is an alias for @{ML_type "string"}, but emphasizes the - specific format encountered here. + \item @{ML_type "Symbol.symbol"} represents individual Isabelle + symbols; this is an alias for @{ML_type "string"}. \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list - from the packed form that. This function supercedes @{ML + from the packed form. This function supercedes @{ML "String.explode"} for virtually all purposes of manipulating text in Isabelle! @@ -504,8 +501,8 @@ \cite{isabelle-isar-ref}. \item @{ML_type "Symbol.sym"} is a concrete datatype that represents - the different kinds of symbols explicitly with constructors @{ML - "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML + the different kinds of symbols explicitly, with constructors @{ML + "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML "Symbol.Raw"}. \item @{ML "Symbol.decode"} converts the string representation of a @@ -529,27 +526,27 @@ @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text "foo___"}, 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 @{text "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 @{text + "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 @{text "declare"} operation. + \medskip Manipulating binding scopes often requires on-the-fly + renamings. A \emph{name context} contains a collection of already + used names. The @{text "declare"} operation adds names to the + context. - The @{text "invents"} operation derives a number of fresh names - derived from a given starting point. For example, three names - derived from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"}, - provided there are no clashes with already used names. + The @{text "invents"} operation derives a number of fresh names from + a given starting point. For example, the first three names derived + from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"}. The @{text "variants"} operation produces fresh names by - incrementing given names as to base-26 numbers (with digits @{text - "a..z"}). For example, name @{text "foo"} results in variants - @{text "fooa"}, @{text "foob"}, @{text "fooc"}, \dots, @{text - "fooaa"}, @{text "fooab"}, \dots; each renaming step picks the next - unused variant from this list. + incrementing tentative names as base-26 numbers (with digits @{text + "a..z"}) until all clashes are resolved. For example, name @{text + "foo"} results in variants @{text "fooa"}, @{text "foob"}, @{text + "fooc"}, \dots, @{text "fooaa"}, @{text "fooab"} etc.; each renaming + step picks the next unused variant from this sequence. *} text %mlref {* @@ -574,11 +571,14 @@ \item @{ML_type Name.context} represents the context of already used names; the initial value is @{ML "Name.context"}. - \item @{ML Name.declare}~@{text "name"} declares @{text "name"} as - being used. + \item @{ML Name.declare}~@{text "name"} enters a used name into the + context. - \item @{ML Name.invents}~@{text "context base n"} produces @{text - "n"} fresh names derived from @{text "base"}. + \item @{ML Name.invents}~@{text "context name n"} produces @{text + "n"} fresh names derived from @{text "name"}. + + \item @{ML Name.variants}~@{text "names context"} produces fresh + varians of @{text "names"}; the result is entered into the context. \end{description} *} @@ -588,16 +588,20 @@ text {* An \emph{indexed name} (or @{text "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 @{text "maxidx"} of the first collection, then - increment all indexes of the second collection by @{text "maxidx + - 1"}. Note that the maximum index of an empty collection is @{text - "-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 @{text "maxidx"} of the first + collection, then increment all indexes of the second collection by + @{text "maxidx + 1"}; the maximum index of an empty collection is + @{text "-1"}. - Isabelle syntax observes the following rules for representing an - indexname @{text "(x, i)"} as a packed string: + Occasionally, basic names and indexed names are injected into the + same pair type: the (improper) indexname @{text "(x, -1)"} is used + to encode basic names. + + \medskip Isabelle syntax observes the following rules for + representing an indexname @{text "(x, i)"} as a packed string: \begin{itemize} @@ -605,20 +609,15 @@ \item @{text "?xi"} if @{text "x"} does not end with a digit, - \item @{text "?x.i"} else. + \item @{text "?x.i"} otherwise. \end{itemize} - Occasionally, basic names and indexed names are injected into the - same pair type: the (improper) indexname @{text "(x, -1)"} is used - to encode basic names. - - \medskip Indexnames may acquire arbitrary large index numbers over - time. Results are usually normalized towards @{text "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 @{text - "?x.1, ?x.7, ?x.42"} then becomes @{text "?x, ?xa, ?xb"}. + Indexnames may acquire large index numbers over time. Results are + normalized towards @{text "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 + @{text "?x1, ?x7, ?x42"} becomes @{text "?x, ?xa, ?xb"}. *} text %mlref {* @@ -631,7 +630,7 @@ \item @{ML_type indexname} represents indexed names. This is an abbreviation for @{ML_type "string * int"}. The second component is usually non-negative, except for situations where @{text "(x, -1)"} - is used to embed plain names. + is used to embed basic names into this type. \end{description} *} @@ -641,62 +640,61 @@ text {* A \emph{qualified name} consists of a non-empty sequence of basic - name components. The packed representation a dot as separator, for - example in ``@{text "A.b.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, @{text "A.b.c"} may be understood - as a local entity @{text "c"} within a local structure @{text "b"} - of the enclosing structure @{text "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 ``@{text "A.b.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 ``@{text "A.b.c"}'' may be understood as a local entity @{text + "c"}, within a local structure @{text "b"}, within a global + structure @{text "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 @{text "naming"} policy tells how to turn a name specification into a fully qualified internal name (by the @{text - "full"} operation), and how to fully qualified names may be accessed - externally. For example, the default naming prefixes an implicit - path from the context: @{text "x"} is becomes @{text "path.x"} - internally; the standard accesses include @{text "x"}, @{text - "path.x"}, and further partial @{text "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. + "full"} operation), and how fully qualified names may be accessed + externally. For example, the default naming policy is to prefix an + implicit path: @{text "full x"} produces @{text "path.x"}, and the + standard accesses for @{text "path.x"} include both @{text "x"} and + @{text "path.x"}. Normally, the naming is implicit in the theory or + proof context; there are separate versions of the corresponding. \medskip A @{text "name space"} manages a collection of fully internalized names, together with a mapping between external names and internal names (in both directions). The corresponding @{text "intern"} and @{text "extern"} operations are mostly used for parsing and printing only! The @{text "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 @{text "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 @{text + "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 - @{text "c.intro"} and @{text "c.elim"} for theorems related to - constant @{text "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.\ @{text - "c_type.intro"} and @{text "c_class.intro"} for theorems related to - type @{text "c"} and class @{text "c"}, respectively. + to the name of the main logical entity involved, e.g.\ @{text + "c.intro"} for a canonical theorem related to constant @{text "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.\ @{text "c_type.intro"} + and @{text "c_class.intro"} for theorems related to type @{text "c"} + and class @{text "c"}, respectively. *} text %mlref {* \begin{mldecls} @{index_ML NameSpace.base: "string -> string"} \\ - @{index_ML NameSpace.drop_base: "string -> string"} \\ + @{index_ML NameSpace.drop_base: "string -> string"} \\ %FIXME qualifier @{index_ML NameSpace.append: "string -> string -> string"} \\ @{index_ML NameSpace.pack: "string list -> string"} \\ @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex] @@ -723,9 +721,9 @@ \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"} appends two qualified names. - \item @{ML NameSpace.pack}~@{text "name"} and @{text - "NameSpace.unpack"}~@{text "names"} convert between the packed - string representation and explicit list form of qualified names. + \item @{ML NameSpace.pack}~@{text "name"} and @{ML + NameSpace.unpack}~@{text "names"} convert between the packed string + representation and the explicit list form of qualified names. \item @{ML_type NameSpace.naming} represents the abstract concept of a naming policy. @@ -735,7 +733,7 @@ consisting of the theory name. \item @{ML NameSpace.add_path}~@{text "path naming"} augments the - naming policy by extending its path. + naming policy by extending its path component. \item @{ML NameSpace.full}@{text "naming name"} turns a name specification (usually a basic name) into the fully qualified @@ -744,26 +742,26 @@ \item @{ML_type NameSpace.T} represents name spaces. \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text - "(space\<^isub>1, space\<^isub>2)"} provide basic operations for - building name spaces in accordance to the usual theory data - management (\secref{sec:context-data}). + "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for + maintaining name spaces according to theory data management + (\secref{sec:context-data}). \item @{ML NameSpace.declare}~@{text "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 @{ML NameSpace.intern}~@{text "space name"} internalizes a (partially qualified) external name. - This operation is mostly for parsing. Note that fully qualified + This operation is mostly for parsing! Note that fully qualified names stemming from declarations are produced via @{ML - "NameSpace.full"} (or derivatives for @{ML_type theory} or @{ML_type - Proof.context}). + "NameSpace.full"} (or its derivatives for @{ML_type theory} and + @{ML_type Proof.context}). \item @{ML NameSpace.extern}~@{text "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 @{ML NameSpace.base}. \end{description} diff -r 6ac7a4fc32a0 -r 121bc2135bd3 doc-src/IsarImplementation/implementation.tex --- a/doc-src/IsarImplementation/implementation.tex Wed Sep 06 22:48:36 2006 +0200 +++ b/doc-src/IsarImplementation/implementation.tex Thu Sep 07 15:16:26 2006 +0200 @@ -32,7 +32,8 @@ We describe the key concepts underlying the Isabelle/Isar implementation, including ML references for the most important functions. The aim is to give some insight into the overall system - architecture, and provide clues on implementing user extensions. + architecture, and provide clues on implementing applications within + this framework. \end{abstract} \vspace*{2.5cm}