--- a/doc-src/IsarImplementation/Thy/Logic.thy Thu Jan 28 22:19:27 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Thu Jan 28 22:38:11 2010 +0100
@@ -116,9 +116,9 @@
text %mlref {*
\begin{mldecls}
- @{index_ML_type class} \\
- @{index_ML_type sort} \\
- @{index_ML_type arity} \\
+ @{index_ML_type class: string} \\
+ @{index_ML_type sort: "class list"} \\
+ @{index_ML_type arity: "string * sort list * sort"} \\
@{index_ML_type typ} \\
@{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
@{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
@@ -136,15 +136,15 @@
\begin{description}
- \item @{ML_type class} represents type classes; this is an alias for
- @{ML_type string}.
+ \item @{ML_type class} represents type classes.
- \item @{ML_type sort} represents sorts; this is an alias for
- @{ML_type "class list"}.
+ \item @{ML_type sort} represents sorts, i.e.\ finite intersections
+ of classes. The empty list @{ML "[]: sort"} refers to the empty
+ class intersection, i.e.\ the ``full sort''.
- \item @{ML_type arity} represents type arities; this is an alias for
- triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
- (\<^vec>s)s"} described above.
+ \item @{ML_type arity} represents type arities. A triple @{text
+ "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> :: (\<^vec>s)s"} as
+ described above.
\item @{ML_type typ} represents types; this is a datatype with
constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jan 28 22:19:27 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jan 28 22:38:11 2010 +0100
@@ -73,41 +73,47 @@
subsection {* Theory context \label{sec:context-theory} *}
-text {*
- A \emph{theory} is a data container with explicit name and unique
- identifier. Theories are related by a (nominal) sub-theory
+text {* A \emph{theory} is a data container with explicit name 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).
+ ancestor theories. To this end, the system maintains a set of
+ symbolic ``identification stamps'' within each theory.
- 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
- theory acts like a linear type, where updates invalidate earlier
- versions. An invalidated draft is called ``stale''.
+ In order to avoid the full-scale overhead of explicit sub-theory
+ identification of arbitrary intermediate stages, a theory is
+ switched into @{text "draft"} mode under certain circumstances. A
+ draft theory acts like a linear type, where updates invalidate
+ earlier versions. An invalidated draft is called \emph{stale}.
- The @{text "checkpoint"} operation produces an intermediate stepping
- 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 "checkpoint"} operation produces a safe stepping stone
+ that will survive the next update without becoming stale: both the
+ old and the new 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
the copy do not affect the original, neither does the sub-theory
relation hold.
+ The @{text "merge"} operation produces the least upper bound of two
+ theories, which actually degenerates into absorption of one theory
+ into the other (according to the nominal sub-theory relation).
+
+ The @{text "begin"} operation starts a new theory by importing
+ several parent theories and entering a special mode of nameless
+ incremental updates, until the final @{text "end"} operation is
+ performed.
+
\medskip The example in \figref{fig:ex-theory} below shows a theory
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}.
+ drafts internally, while transaction boundaries of Isar top-level
+ commands (\secref{sec:isar-toplevel}) are guaranteed to be safe
+ checkpoints.
\begin{figure}[htb]
\begin{center}
@@ -147,9 +153,10 @@
\begin{mldecls}
@{index_ML_type theory} \\
@{index_ML Theory.subthy: "theory * theory -> bool"} \\
- @{index_ML Theory.merge: "theory * theory -> theory"} \\
@{index_ML Theory.checkpoint: "theory -> theory"} \\
@{index_ML Theory.copy: "theory -> theory"} \\
+ @{index_ML Theory.merge: "theory * theory -> theory"} \\
+ @{index_ML Theory.begin_theory: "string -> theory list -> theory"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type theory_ref} \\
@@ -160,25 +167,32 @@
\begin{description}
\item @{ML_type theory} represents theory contexts. This is
- essentially a linear type! Most operations destroy the original
- version, which then becomes ``stale''.
+ essentially a linear type, with explicit runtime checking! Most
+ internal theory 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
- construction. This sub-theory relation is a nominal approximation
- of inclusion (@{text "\<subseteq>"}) of the corresponding content.
-
- \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}
- absorbs one theory into the other. This fails for unrelated
- theories!
+ \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories
+ according to the intrinsic graph structure of the construction.
+ This sub-theory relation is a nominal approximation of inclusion
+ (@{text "\<subseteq>"}) of the corresponding content (according to the
+ semantics of the ML modules that implement the data).
\item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe
- stepping stone in the linear development of @{text "thy"}. The next
- update will result in two related, valid theories.
+ stepping stone in the linear development of @{text "thy"}. This
+ changes the old theory, but the next update will result in two
+ related, valid theories.
\item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text
- "thy"} with the same data. The result is not related to the
- original; the original is unchanged.
+ "thy"} with the same data. The copy is not related to the original,
+ but the original is unchanged.
+
+ \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} absorbs one theory
+ into the other, without changing @{text "thy\<^sub>1"} or @{text "thy\<^sub>2"}.
+ This version of ad-hoc theory merge fails for unrelated theories!
+
+ \item @{ML "Theory.begin_theory"}~@{text "name parents"} constructs
+ a new theory based on the given parents. This {\ML} function is
+ normally not invoked directly.
\item @{ML_type theory_ref} represents a sliding reference to an
always valid theory; updates on the original are propagated
@@ -198,31 +212,32 @@
subsection {* Proof context \label{sec:context-proof} *}
-text {*
- 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 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.
+text {* 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 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.
- Entities derived in a proof context need to record inherent logical
+ Entities derived in a proof context need to record logical
requirements explicitly, since there is no separate context
- identification as for theories. For example, hypotheses used in
- primitive derivations (cf.\ \secref{sec:thms}) are recorded
- separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double
- sure. Results could still leak into an alien proof context due to
- programming errors, but Isabelle/Isar includes some extra validity
- checks in critical positions, notably at the end of a sub-proof.
+ identification or symbolic inclusion as for theories. For example,
+ hypotheses used in primitive derivations (cf.\ \secref{sec:thms})
+ are recorded separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to
+ make double sure. Results could still leak into an alien proof
+ context due to programming errors, but Isabelle/Isar includes some
+ extra validity checks in critical positions, notably at the end of a
+ sub-proof.
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
+ into the original context. Note that an Isar proof state models
block-structured reasoning explicitly, using a stack of proof
- contexts internally.
+ contexts internally. For various technical reasons, the background
+ theory of an Isar proof state must not be changed while the proof is
+ still under construction!
*}
text %mlref {*
@@ -267,7 +282,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 from the sum, while a proof context might
- have to be constructed by an ad-hoc @{text "init"} operation.
+ have to be constructed by an ad-hoc @{text "init"} operation, which
+ incurs a small runtime overhead.
*}
text %mlref {*
@@ -319,6 +335,16 @@
\emph{any} theory that does not declare actual data content; @{text
"extend"} is acts like a unitary version of @{text "merge"}.
+ Implementing @{text "merge"} can be tricky. The general idea is
+ that @{text "merge (data\<^sub>1, data\<^sub>2)"} inserts those parts of @{text
+ "data\<^sub>2"} into @{text "data\<^sub>1"} that are not yet present, while
+ keeping the general order of things. The @{ML Library.merge}
+ function on plain lists may serve as canonical template.
+
+ Particularly note that shared parts of the data must not be
+ duplicated by naive concatenation, or a theory graph that is like a
+ chain of diamonds would cause an exponential blowup!
+
\paragraph{Proof context data} declarations need to implement the
following SML signature:
@@ -330,15 +356,18 @@
\medskip
\noindent The @{text "init"} operation is supposed to produce a pure
- value from the given background theory.
+ value from the given background theory and should be somehow
+ ``immediate''. Whenever a proof context is initialized, which
+ happens frequently, the the system invokes the @{text "init"}
+ operation of \emph{all} theory data slots ever declared.
\paragraph{Generic data} provides a hybrid interface for both theory
and proof data. The @{text "init"} operation for proof contexts is
predefined to select the current data value from the background
theory.
- \bigskip A data declaration of type @{text "T"} results in the
- following interface:
+ \bigskip Any of these data declaration over type @{text "T"} result
+ in an ML structure with the following signature:
\medskip
\begin{tabular}{ll}
@@ -348,12 +377,12 @@
\end{tabular}
\medskip
- \noindent These 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 of a context. By keeping these operations
- private, a component may maintain abstract values authentically,
- without other components interfering.
+ \noindent These other operations provide exclusive access for the
+ particular kind of context (theory, proof, or generic context).
+ This interface fully observes the ML discipline for types and
+ scopes: there is no other way to access the corresponding data slot
+ of a context. By keeping these operations private, an Isabelle/ML
+ module may maintain abstract values authentically.
*}
text %mlref {*
@@ -447,7 +476,7 @@
text %mlref {*
\begin{mldecls}
- @{index_ML_type "Symbol.symbol"} \\
+ @{index_ML_type "Symbol.symbol": string} \\
@{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
@{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
@{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
@@ -462,7 +491,7 @@
\begin{description}
\item @{ML_type "Symbol.symbol"} represents individual Isabelle
- symbols; this is an alias for @{ML_type "string"}.
+ symbols.
\item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
from the packed form. This function supercedes @{ML