diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 18:27:40 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 22:55:49 2006 +0200 @@ -8,19 +8,20 @@ section {* Contexts \label{sec:context} *} text {* - A logical context represents the background that is taken for - granted when formulating statements and composing proofs. It acts - as a medium to produce formal content, depending on earlier material - (declarations, results etc.). + A logical context represents the background that is required for + formulating statements and composing proofs. It acts as a medium to + produce formal content, depending on earlier material (declarations, + results etc.). - In particular, derivations within the primitive Pure logic can be - described as a judgment @{text "\ \\<^sub>\ \"}, meaning that a + For example, derivations within the Isabelle/Pure logic can be + described as a judgment @{text "\ \\<^sub>\ \"}, which means that a proposition @{text "\"} is derivable from hypotheses @{text "\"} within the theory @{text "\"}. There are logical reasons for - keeping @{text "\"} and @{text "\"} separate: theories support type - constructors and schematic polymorphism of constants and axioms, - while the inner calculus of @{text "\ \ \"} is limited to Simple - Type Theory (with fixed type variables in the assumptions). + keeping @{text "\"} and @{text "\"} separate: theories can be + liberal about supporting type constructors and schematic + polymorphism of constants and axioms, while the inner calculus of + @{text "\ \ \"} is strictly limited to Simple Type Theory (with + fixed type variables in the assumptions). \medskip Contexts and derivations are linked by the following key principles: @@ -28,45 +29,46 @@ \begin{itemize} \item Transfer: monotonicity of derivations admits results to be - transferred into a larger context, i.e.\ @{text "\ \\<^sub>\ \"} - implies @{text "\' \\<^sub>\\<^sub>' \"} for contexts @{text "\' \ - \"} and @{text "\' \ \"}. + transferred into a \emph{larger} context, i.e.\ @{text "\ \\<^sub>\ + \"} implies @{text "\' \\<^sub>\\<^sub>' \"} for contexts @{text "\' + \ \"} and @{text "\' \ \"}. \item Export: discharge of hypotheses admits results to be exported - into a smaller context, i.e.\ @{text "\' \\<^sub>\ \"} implies - @{text "\ \\<^sub>\ \ \ \"} where @{text "\' \ \"} and @{text "\ = - \' - \"}. Note that @{text "\"} remains unchanged here, only the - @{text "\"} part is affected. + into a \emph{smaller} context, i.e.\ @{text "\' \\<^sub>\ \"} + implies @{text "\ \\<^sub>\ \ \ \"} where @{text "\' \ \"} and + @{text "\ = \' - \"}. Note that @{text "\"} remains unchanged here, + only the @{text "\"} part is affected. \end{itemize} - \medskip Isabelle/Isar provides two different notions of abstract - containers called \emph{theory context} and \emph{proof context}, - respectively. These model the main characteristics of the primitive - @{text "\"} and @{text "\"} above, without subscribing to any - particular kind of content yet. Instead, contexts merely impose a - certain policy of managing arbitrary \emph{context data}. The - system provides strongly typed mechanisms to declare new kinds of + \medskip By modeling the main characteristics of the primitive + @{text "\"} and @{text "\"} above, and abstracting over any + particular logical content, we arrive at the fundamental notions of + \emph{theory context} and \emph{proof context} in Isabelle/Isar. + These implement a certain policy to manage arbitrary \emph{context + data}. There is a strongly-typed mechanism to declare new kinds of data at compile time. - Thus the internal bootstrap process of Isabelle/Pure eventually - reaches a stage where certain data slots provide the logical content - of @{text "\"} and @{text "\"} sketched above, but this does not - stop there! Various additional data slots support all kinds of - mechanisms that are not necessarily part of the core logic. + The internal bootstrap process of Isabelle/Pure eventually reaches a + stage where certain data slots provide the logical content of @{text + "\"} and @{text "\"} sketched above, but this does not stop there! + Various additional data slots support all kinds of mechanisms that + are not necessarily part of the core logic. For example, there would be data for canonical introduction and elimination rules for arbitrary operators (depending on the object-logic and application), which enables users to perform - standard proof steps implicitly (cf.\ the @{text "rule"} method). + standard proof steps implicitly (cf.\ the @{text "rule"} method + \cite{isabelle-isar-ref}). - Isabelle is able to bring forth more and more concepts successively. - In particular, an object-logic like Isabelle/HOL continues the - Isabelle/Pure setup by adding specific components for automated - reasoning (classical reasoner, tableau prover, structured induction - etc.) and derived specification mechanisms (inductive predicates, - recursive functions etc.). All of this is based on the generic data - management by theory and proof contexts. + \medskip Thus Isabelle/Isar is able to bring forth more and more + concepts successively. In particular, an object-logic like + Isabelle/HOL continues the Isabelle/Pure setup by adding specific + components for automated reasoning (classical reasoner, tableau + prover, structured induction etc.) and derived specification + mechanisms (inductive predicates, recursive functions etc.). All of + this is ultimately based on the generic data management by theory + and proof contexts introduced here. *} @@ -75,31 +77,27 @@ text {* \glossary{Theory}{FIXME} - Each theory is explicitly named and holds a unique identifier. - There is a separate \emph{theory reference} for pointing backwards - to the enclosing theory context of derived entities. Theories are - related by a (nominal) sub-theory relation, which corresponds to the - canonical dependency graph: each theory is derived from a certain - sub-graph of ancestor theories. The @{text "merge"} of two theories - refers to the least upper bound, which actually degenerates into - absorption of one theory into the other, due to the nominal - sub-theory relation this. + A \emph{theory} is a data container with explicit named and unique + identifier. Theories are related by a (nominal) sub-theory + relation, which corresponds to the dependency graph of the original + construction; each theory is derived from a certain sub-graph of + ancestor theories. + + The @{text "merge"} operation produces the least upper bound of two + theories, which actually degenerates into absorption of one theory + into the other (due to the nominal sub-theory relation). The @{text "begin"} operation starts a new theory by importing several parent theories and entering a special @{text "draft"} mode, which is sustained until the final @{text "end"} operation. A draft - mode theory acts like a linear type, where updates invalidate - earlier drafts, but theory reference values will be propagated - automatically. Thus derived entities that ``belong'' to a draft - might be transferred spontaneously to a larger context. An - invalidated draft is called ``stale''. + theory acts like a linear type, where updates invalidate earlier + versions. An invalidated draft is called ``stale''. The @{text "checkpoint"} operation produces an intermediate stepping - stone that will survive the next update unscathed: both the original - and the changed theory remain valid and are related by the - sub-theory relation. Checkpointing essentially recovers purely - functional theory values, at the expense of some extra internal - bookkeeping. + stone that will survive the next update: both the original and the + changed theory remain valid and are related by the sub-theory + relation. Checkpointing essentially recovers purely functional + theory values, at the expense of some extra internal bookkeeping. The @{text "copy"} operation produces an auxiliary version that has the same data content, but is unrelated to the original: updates of @@ -107,11 +105,12 @@ relation hold. \medskip The example in \figref{fig:ex-theory} below shows a theory - graph derived from @{text "Pure"}. Theory @{text "Length"} imports - @{text "Nat"} and @{text "List"}. The theory body consists of a - sequence of updates, working mostly on drafts. Intermediate - checkpoints may occur as well, due to the history mechanism provided - by the Isar top-level, cf.\ \secref{sec:isar-toplevel}. + graph derived from @{text "Pure"}, with theory @{text "Length"} + importing @{text "Nat"} and @{text "List"}. The body of @{text + "Length"} consists of a sequence of updates, working mostly on + drafts. Intermediate checkpoints may occur as well, due to the + history mechanism provided by the Isar top-level, cf.\ + \secref{sec:isar-toplevel}. \begin{figure}[htb] \begin{center} @@ -132,9 +131,19 @@ & & $\vdots$~~ \\ & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\ \end{tabular} - \caption{Theory definition depending on ancestors}\label{fig:ex-theory} + \caption{A theory definition depending on ancestors}\label{fig:ex-theory} \end{center} \end{figure} + + \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. + + Derived entities may store a theory reference in order to indicate + the context they belong to. This implicitly assumes monotonic + reasoning, because the referenced context may become larger without + further notice. *} text %mlref {* @@ -151,9 +160,9 @@ \begin{description} - \item @{ML_type theory} represents theory contexts. This is a - linear type! Most operations destroy the old version, which then - becomes ``stale''. + \item @{ML_type theory} represents theory contexts. This is + essentially a linear type! Most operations destroy the original + version, which then becomes ``stale''. \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories according to the inherent graph structure of the @@ -169,18 +178,18 @@ update will result in two related, valid theories. \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text - "thy"} that holds a copy of the same data. The copy is not related - to the original, which is not touched at all. + "thy"} that holds a copy of the same data. The result is not + related to the original; the original is unchanched. - \item @{ML_type theory_ref} represents a sliding reference to a - valid theory --- updates on the original are propagated + \item @{ML_type theory_ref} represents a sliding reference to an + always valid theory; updates on the original are propagated automatically. \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type "theory"} and @{ML_type "theory_ref"}. As the referenced theory evolves monotonically over time, later invocations of @{ML - "Theory.deref"} may refer to larger contexts. + "Theory.deref"} may refer to a larger context. \end{description} *} @@ -198,28 +207,28 @@ A proof context is a container for pure data with a back-reference to the theory it belongs to. The @{text "init"} operation creates a - proof context derived from a given theory. Modifications to draft - theories are propagated to the proof context as usual, but there is - also an explicit @{text "transfer"} operation to force - resynchronization with more substantial updates to the underlying - theory. The actual context data does not require any special - bookkeeping, thanks to the lack of destructive features. + proof context from a given theory. Modifications to draft theories + are propagated to the proof context as usual, but there is also an + explicit @{text "transfer"} operation to force resynchronization + with more substantial updates to the underlying theory. The actual + context data does not require any special bookkeeping, thanks to the + lack of destructive features. Entities derived in a proof context need to record inherent logical requirements explicitly, since there is no separate context identification as for theories. For example, hypotheses used in - primitive derivations (cf.\ \secref{sec:thm}) are recorded + primitive derivations (cf.\ \secref{sec:thms}) are recorded separately within the sequent @{text "\ \ \"}, just to make double sure. Results could still leak into an alien proof context do to programming errors, but Isabelle/Isar includes some extra validity checks in critical positions, notably at the end of sub-proof. - Proof contexts may be produced in arbitrary ways, although the - common discipline is to follow block structure as a mental model: a - given context is extended consecutively, and results are exported - back into the original context. Note that the Isar proof states - model block-structured reasoning explicitly, using a stack of proof - contexts, cf.\ \secref{isar-proof-state}. + Proof contexts may be manipulated arbitrarily, although the common + discipline is to follow block structure as a mental model: a given + context is extended consecutively, and results are exported back + into the original context. Note that the Isar proof states model + block-structured reasoning explicitly, using a stack of proof + contexts internally, cf.\ \secref{sec:isar-proof-state}. *} text %mlref {* @@ -240,7 +249,8 @@ derived from @{text "thy"}, initializing all data. \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the - background theory from @{text "ctxt"}. + background theory from @{text "ctxt"}, dereferencing its internal + @{ML_type theory_ref}. \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the background theory of @{text "ctxt"} to the super theory @{text @@ -250,12 +260,11 @@ *} - -subsection {* Generic contexts *} +subsection {* Generic contexts \label{sec:generic-context} *} text {* A generic context is the disjoint sum of either a theory or proof - context. Occasionally, this simplifies uniform treatment of generic + context. Occasionally, this enables uniform treatment of generic context data, typically extra-logical information. Operations on generic contexts include the usual injections, partial selections, and combinators for lifting operations on either component of the @@ -263,8 +272,8 @@ Moreover, there are total operations @{text "theory_of"} and @{text "proof_of"} to convert a generic context into either kind: a theory - can always be selected, while a proof context may have to be - constructed by an ad-hoc @{text "init"} operation. + can always be selected from the sum, while a proof context might + have to be constructed by an ad-hoc @{text "init"} operation. *} text %mlref {* @@ -277,8 +286,8 @@ \begin{description} \item @{ML_type Context.generic} is the direct sum of @{ML_type - "theory"} and @{ML_type "Proof.context"}, with datatype constructors - @{ML "Context.Theory"} and @{ML "Context.Proof"}. + "theory"} and @{ML_type "Proof.context"}, with the datatype + constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}. \item @{ML Context.theory_of}~@{text "context"} always produces a theory from the generic @{text "context"}, using @{ML @@ -286,8 +295,8 @@ \item @{ML Context.proof_of}~@{text "context"} always produces a proof context from the generic @{text "context"}, using @{ML - "ProofContext.init"} as required. Note that this re-initializes the - context data with each invocation. + "ProofContext.init"} as required (note that this re-initializes the + context data with each invocation). \end{description} *} @@ -295,23 +304,23 @@ subsection {* Context data *} text {* - Both theory and proof contexts manage arbitrary data, which is the - main purpose of contexts in the first place. Data can be declared - incrementally at compile --- Isabelle/Pure and major object-logics - are bootstrapped that way. + The main purpose of theory and proof contexts is to manage arbitrary + data. New data types can be declared incrementally at compile time. + There are separate declaration mechanisms for any of the three kinds + of contexts: theory, proof, generic. \paragraph{Theory data} may refer to destructive entities, which are - maintained in correspondence to the linear evolution of theory - values, or explicit copies.\footnote{Most existing instances of - destructive theory data are merely historical relics (e.g.\ the - destructive theorem storage, and destructive hints for the - Simplifier and Classical rules).} A theory data declaration needs - to implement the following specification: + maintained in direct correspondence to the linear evolution of + theory values, including explicit copies.\footnote{Most existing + instances of destructive theory data are merely historical relics + (e.g.\ the destructive theorem storage, and destructive hints for + the Simplifier and Classical rules).} A theory data declaration + needs to implement the following specification (depending on type + @{text "T"}): \medskip \begin{tabular}{ll} @{text "name: string"} \\ - @{text "T"} & the ML type \\ @{text "empty: T"} & initial value \\ @{text "copy: T \ T"} & refresh impure data \\ @{text "extend: T \ T"} & re-initialize on import \\ @@ -326,27 +335,26 @@ should also include the functionality of @{text "copy"} for impure data. - \paragraph{Proof context data} is purely functional. It is declared - by implementing the following specification: + \paragraph{Proof context data} is purely functional. A declaration + needs to implement the following specification: \medskip \begin{tabular}{ll} @{text "name: string"} \\ - @{text "T"} & the ML type \\ @{text "init: theory \ T"} & produce initial value \\ @{text "print: T \ unit"} & diagnostic output \\ \end{tabular} \medskip \noindent The @{text "init"} operation is supposed to produce a pure - value from the given background theory. The rest is analogous to - (pure) theory data. + value from the given background theory. The remainder is analogous + to theory data. - \paragraph{Generic data} provides a hybrid interface for both kinds. - The declaration is essentially the same as for pure theory data, - without @{text "copy"} (it is always the identity). The @{text - "init"} operation for proof contexts selects the current data value - from the background theory. + \paragraph{Generic data} provides a hybrid interface for both theory + and proof data. The declaration is essentially the same as for + (pure) theory data, without @{text "copy"}, though. The @{text + "init"} operation for proof contexts merely selects the current data + value from the background theory. \bigskip In any case, a data declaration of type @{text "T"} results in the following interface: @@ -366,9 +374,9 @@ other operations provide access for the particular kind of context (theory, proof, or generic context). Note that this is a safe interface: there is no other way to access the corresponding data - slot within a context. By keeping these operations private, a - component may maintain abstract values authentically, without other - components interfering. + slot of a context. By keeping these operations private, a component + may maintain abstract values authentically, without other components + interfering. *} text %mlref {* @@ -382,8 +390,8 @@ \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for type @{ML_type theory} according to the specification provided as - argument structure. The result structure provides init and access - operations as described above. + argument structure. The resulting structure provides data init and + access operations as described above. \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for type @{ML_type Proof.context}. @@ -397,77 +405,95 @@ section {* Named entities *} -text {* 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 @{text "foo"} vs.\ theorem -@{text "foo"} vs.\ logical constant @{text "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. +text {* + By general convention, each kind of formal entities (logical + constant, type, type class, theorem, method etc.) lives in a + separate name space. It is usually clear from the syntactic context + of a name, which kind of entity it refers to. For example, proof + method @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical + constant @{text "foo"} are easily distinguished thanks to the design + of the concrete outer syntax. 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. + + Name spaces are organized uniformly, as a collection of qualified + names consisting of a sequence of basic name components separated by + dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"} + are examples for qualified names. -Each name space is organized as a collection of \emph{qualified -names}, which consist of a sequence of basic name components separated -by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "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. *} + Despite the independence of names of different kinds, certain naming + conventions may relate them to each other. For example, a constant + @{text "foo"} could be accompanied with theorems @{text + "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. The same + could happen for a type @{text "foo"}, but this is apt to cause + clashes in the theorem name space! To avoid this, there is an + additional convention to add a suffix that determines the original + kind. For example, constant @{text "foo"} could associated with + theorem @{text "foo.intro"}, type @{text "foo"} with theorem @{text + "foo_type.intro"}, and type class @{text "foo"} with @{text + "foo_class.intro"}. + + \medskip Name components are subdivided into \emph{symbols}, which + constitute the smallest textual unit in Isabelle --- raw characters + are normally not encountered. +*} subsection {* Strings of symbols *} -text {* Isabelle strings consist of a sequence of -symbols\glossary{Symbol}{The smallest 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 @{text "string"}, or represented as a list. Each symbol is in -itself a small string of the following form: +text {* + Isabelle strings consist of a sequence of + symbols\glossary{Symbol}{The smallest 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 @{text "string"}, or represented as a list. Each symbol + is in itself a small string of the following form: -\begin{enumerate} + \begin{enumerate} -\item either a singleton ASCII character ``@{text "c"}'' (with -character code 0--127), for example ``\verb,a,'', + \item either a singleton ASCII character ``@{text "c"}'' (with + character code 0--127), for example ``\verb,a,'', -\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'', -for example ``\verb,\,\verb,,'', + \item or a regular symbol ``\verb,\,\verb,<,@{text + "ident"}\verb,>,'', for example ``\verb,\,\verb,,'', -\item or a control symbol ``\verb,\,\verb,<^,@{text -"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'', + \item or a control symbol ``\verb,\,\verb,<^,@{text + "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'', -\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text -"\"}\verb,>,'' where ``@{text "\"}'' 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 raw control symbol ``\verb,\,\verb,<^raw:,@{text + "\"}\verb,>,'' where ``@{text "\"}'' 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,@{text -"nnn"}\verb,>, where @{text "nnn"} are digits, for example -``\verb,\,\verb,<^raw42>,''. + \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text + "nnn"}\verb,>, where @{text "nnn"} are digits, for example + ``\verb,\,\verb,<^raw42>,''. -\end{enumerate} + \end{enumerate} -The @{text "ident"} syntax for symbol names is @{text "letter (letter -| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text -"digit = 0..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. + The @{text "ident"} syntax for symbol names is @{text "letter + (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and + @{text "digit = 0..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 @{text -"\"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text -"\<^bold>\"}. + 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 @{text "\"}, and + ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text + "\<^bold>\"}. -\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. *} + \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 + Unicode/UCS data as well (using UTF-8 encoding). Unicode provides + its own collection of mathematical symbols, but there is no built-in + link to the ones of Isabelle. +*} text %mlref {* \begin{mldecls} @@ -476,34 +502,35 @@ @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\ @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\ @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\ - @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\ + @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex] @{index_ML_type "Symbol.sym"} \\ @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\ \end{mldecls} \begin{description} - \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type - is merely an alias for @{ML_type "string"}, but emphasizes the + \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 "Symbol.explode"}~@{text "s"} produces a symbol list from - the packed form usually encountered as user input. This function - replaces @{ML "String.explode"} for virtually all purposes of - manipulating text in Isabelle! Plain @{ML "implode"} may be used - for the reverse operation. + the packed form that is encountered in most practical situations. + This function supercedes @{ML "String.explode"} for virtually all + purposes of manipulating text in Isabelle! Plain @{ML "implode"} + may still be used for the reverse operation. \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML "Symbol.is_quasi"}, @{ML "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}. + conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}. \item @{ML_type "Symbol.sym"} is a concrete datatype that represents - the different kinds of symbols explicitly as @{ML "Symbol.Char"}, - @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}. + the different kinds of symbols explicitly with constructors @{ML + "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML + "Symbol.Raw"}. \item @{ML "Symbol.decode"} converts the string representation of a - symbol into the explicit datatype version. + symbol into the datatype version. \end{description} *} @@ -512,50 +539,27 @@ subsection {* Qualified names and name spaces *} text {* - FIXME - - 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 @{text "c"} - declared as part of a certain structure @{text "b"} (say a type - definition) in theory @{text "A"} will be named @{text "A.b.c"} - internally. - - \item + A \emph{qualified name} essentially consists of a non-empty list of + basic name components. The packad notation uses a dot as separator, + as in @{text "A.b"}, for example. The very last component is called + \emph{base} name, the remaining prefix \emph{qualifier} (which may + be empty). - \item - - \item - - \item - - \end{itemize} + A @{text "naming"} policy tells how to produce fully qualified names + from a given specification. The @{text "full"} operation applies + performs naming of a name; the policy is usually taken from the + context. For example, a common policy is to attach an implicit + prefix. - Names of different kinds of entities are basically independent, but - some practical naming conventions relate them to each other. For - example, a constant @{text "foo"} may be accompanied with theorems - @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. - The same may happen for a type @{text "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 @{text "foo"} is associated with theorem - @{text "foo.intro"}, type @{text "foo"} with theorem @{text - "foo_type.intro"}, and type class @{text "foo"} with @{text - "foo_class.intro"}. + A @{text "name space"} manages declarations of fully qualified + names. There are separate operations to @{text "declare"}, @{text + "intern"}, and @{text "extern"} names. + + FIXME *} +text %mlref FIXME + section {* Structured output *} @@ -567,7 +571,7 @@ text FIXME -subsection {* Print modes *} +subsection {* Print modes \label{sec:print-mode} *} text FIXME