--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 22:55:49 2006 +0200
@@ -28,19 +28,20 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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 \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
+ For example, derivations within the Isabelle/Pure logic can be
+ described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
within the theory \isa{{\isasymTheta}}. There are logical reasons for
- keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories support type
- constructors and schematic polymorphism of constants and axioms,
- while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
- Type Theory (with fixed type variables in the assumptions).
+ keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
+ liberal about supporting type constructors and schematic
+ polymorphism of constants and axioms, while the inner calculus of
+ \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} 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:
@@ -48,43 +49,43 @@
\begin{itemize}
\item Transfer: monotonicity of derivations admits results to be
- transferred into a larger context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
- implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
+ transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
\item Export: discharge of hypotheses admits results to be exported
- into a smaller context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies
- \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here, only the
- \isa{{\isasymGamma}} part is affected.
+ into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
+ implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
+ \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here,
+ only the \isa{{\isasymGamma}} 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
- \isa{{\isasymTheta}} and \isa{{\isasymGamma}} 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
+ \isa{{\isasymTheta}} and \isa{{\isasymGamma}} 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 \isa{{\isasymTheta}} and \isa{{\isasymGamma}} 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 \isa{{\isasymTheta}} and \isa{{\isasymGamma}} 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 \isa{rule} method).
+ standard proof steps implicitly (cf.\ the \isa{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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -95,31 +96,27 @@
\begin{isamarkuptext}%
\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 \isa{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 \isa{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 \isa{begin} operation starts a new theory by importing
several parent theories and entering a special \isa{draft} mode,
which is sustained until the final \isa{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 \isa{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 \isa{copy} operation produces an auxiliary version that has
the same data content, but is unrelated to the original: updates of
@@ -127,11 +124,11 @@
relation hold.
\medskip The example in \figref{fig:ex-theory} below shows a theory
- graph derived from \isa{Pure}. Theory \isa{Length} imports
- \isa{Nat} and \isa{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 \isa{Pure}, with theory \isa{Length}
+ importing \isa{Nat} and \isa{List}. The body of \isa{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}
@@ -152,9 +149,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}%
+ \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 \isa{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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -178,9 +185,9 @@
\begin{description}
- \item \verb|theory| represents theory contexts. This is a
- linear type! Most operations destroy the old version, which then
- becomes ``stale''.
+ \item \verb|theory| represents theory contexts. This is
+ essentially a linear type! Most operations destroy the original
+ version, which then becomes ``stale''.
\item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
compares theories according to the inherent graph structure of the
@@ -195,15 +202,15 @@
stepping stone in the linear development of \isa{thy}. The next
update will result in two related, valid theories.
- \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The copy is not related
- to the original, which is not touched at all.
+ \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The result is not
+ related to the original; the original is unchanched.
- \item \verb|theory_ref| represents a sliding reference to a
- valid theory --- updates on the original are propagated
+ \item \verb|theory_ref| represents a sliding reference to an
+ always valid theory; updates on the original are propagated
automatically.
\item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|. As the referenced theory
- evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to larger contexts.
+ evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
\end{description}%
\end{isamarkuptext}%
@@ -230,28 +237,28 @@
A proof context is a container for pure data with a back-reference
to the theory it belongs to. The \isa{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 \isa{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 \isa{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 \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, 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}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -279,7 +286,8 @@
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
- background theory from \isa{ctxt}.
+ background theory from \isa{ctxt}, dereferencing its internal
+ \verb|theory_ref|.
\item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
background theory of \isa{ctxt} to the super theory \isa{thy}.
@@ -295,21 +303,21 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Generic contexts%
+\isamarkupsubsection{Generic contexts \label{sec:generic-context}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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
disjoint sum.
Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}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 \isa{init} operation.%
+ can always be selected from the sum, while a proof context might
+ have to be constructed by an ad-hoc \isa{init} operation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -328,15 +336,15 @@
\begin{description}
- \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with datatype constructors
- \verb|Context.Theory| and \verb|Context.Proof|.
+ \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
+ constructors \verb|Context.Theory| and \verb|Context.Proof|.
\item \verb|Context.theory_of|~\isa{context} always produces a
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
- proof context from the generic \isa{context}, using \verb|ProofContext.init| as required. Note that this re-initializes the
- context data with each invocation.
+ proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
+ context data with each invocation).
\end{description}%
\end{isamarkuptext}%
@@ -354,23 +362,23 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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
+ \isa{T}):
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
- \isa{T} & the ML type \\
\isa{empty{\isacharcolon}\ T} & initial value \\
\isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
\isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
@@ -384,26 +392,25 @@
should also include the functionality of \isa{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}
\isa{name{\isacharcolon}\ string} \\
- \isa{T} & the ML type \\
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
\isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
\end{tabular}
\medskip
\noindent The \isa{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 \isa{copy} (it is always the identity). The \isa{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 \isa{copy}, though. The \isa{init} operation for proof contexts merely selects the current data
+ value from the background theory.
\bigskip In any case, a data declaration of type \isa{T} results
in the following interface:
@@ -423,9 +430,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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -446,8 +453,8 @@
\item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
type \verb|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 \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
type \verb|Proof.context|.
@@ -471,23 +478,34 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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 \isa{foo} vs.\ theorem
-\isa{foo} vs.\ logical constant \isa{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.
+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 \isa{foo} vs.\ theorem \isa{foo} vs.\ logical
+ constant \isa{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.
-Each name space is organized as a collection of \emph{qualified
-names}, which consist of a sequence of basic name components separated
-by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{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.%
+ Name spaces are organized uniformly, as a collection of qualified
+ names consisting of a sequence of basic name components separated by
+ dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
+ are examples for qualified names.
+
+ Despite the independence of names of different kinds, certain naming
+ conventions may relate them to each other. For example, a constant
+ \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The same
+ could happen for a type \isa{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 \isa{foo} could associated with
+ theorem \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.
+
+ \medskip Name components are subdivided into \emph{symbols}, which
+ constitute the smallest textual unit in Isabelle --- raw characters
+ are normally not encountered.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -497,48 +515,49 @@
%
\begin{isamarkuptext}%
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 \isa{string}, or represented as a list. Each symbol is in
-itself a small string of the following form:
+ 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 \isa{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 ``\isa{c}'' (with
+ character code 0--127), for example ``\verb,a,'',
-\item either a singleton ASCII character ``\isa{c}'' (with
-character code 0--127), for example ``\verb,a,'',
+ \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
-\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
-for example ``\verb,\,\verb,<alpha>,'',
+ \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
-\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+ \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' 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:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' 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,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
+ ``\verb,\,\verb,<^raw42>,''.
-\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
-``\verb,\,\verb,<^raw42>,''.
-
-\end{enumerate}
+ \end{enumerate}
-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 available, but a certain 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.
+ 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 available, but a certain 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.
-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,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
+ 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,<alpha>,'' as \isa{{\isasymalpha}}, and
+ ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
-\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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -555,33 +574,32 @@
\indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
\indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
\indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
\indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
\indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
\end{mldecls}
\begin{description}
- \item \verb|Symbol.symbol| represents Isabelle symbols; this type
- is merely an alias for \verb|string|, but emphasizes the
+ \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.explode|~\isa{s} produces a symbol list from
- the packed form usually encountered as user input. This function
- replaces \verb|String.explode| for virtually all purposes of
- manipulating text in Isabelle! Plain \verb|implode| may be used
- for the reverse operation.
+ the packed form that is encountered in most practical situations.
+ This function supercedes \verb|String.explode| for virtually all
+ purposes of manipulating text in Isabelle! Plain \verb|implode|
+ may still be used for the reverse operation.
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|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 \verb|Symbol.sym| is a concrete datatype that represents
- the different kinds of symbols explicitly as \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|, or \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
- symbol into the explicit datatype version.
+ symbol into the datatype version.
\end{description}%
\end{isamarkuptext}%
@@ -599,49 +617,43 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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 \isa{c}
- declared as part of a certain structure \isa{b} (say a type
- definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
- internally.
+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 \isa{A{\isachardot}b}, for example. The very last component is called
+ \emph{base} name, the remaining prefix \emph{qualifier} (which may
+ be empty).
- \item
-
- \item
-
- \item
-
- \item
-
- \end{itemize}
+ A \isa{naming} policy tells how to produce fully qualified names
+ from a given specification. The \isa{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 \isa{foo} may be accompanied with theorems
- \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
- The same may happen for a type \isa{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 \isa{foo} is associated with theorem
- \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
+ A \isa{name\ space} manages declarations of fully qualified
+ names. There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
+
+ FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsection{Structured output%
}
\isamarkuptrue%
@@ -664,7 +676,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Print modes%
+\isamarkupsubsection{Print modes \label{sec:print-mode}%
}
\isamarkuptrue%
%