# HG changeset patch # User wenzelm # Date 1157028835 -7200 # Node ID 5b75f1c4d7d6e5b0d9c979e318282932c2e30a1a # Parent 7e616709bca2b58a4e842cd4166bdead71e29968 more on contexts; diff -r 7e616709bca2 -r 5b75f1c4d7d6 doc-src/IsarImplementation/Thy/document/integration.tex --- a/doc-src/IsarImplementation/Thy/document/integration.tex Thu Aug 31 14:36:48 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex Thu Aug 31 14:53:55 2006 +0200 @@ -23,7 +23,7 @@ } \isamarkuptrue% % -\isamarkupsection{Isar toplevel% +\isamarkupsection{Isar toplevel \label{sec:isar-toplevel}% } \isamarkuptrue% % diff -r 7e616709bca2 -r 5b75f1c4d7d6 doc-src/IsarImplementation/Thy/document/prelim.tex --- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 14:36:48 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 14:53:55 2006 +0200 @@ -93,7 +93,9 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Each theory is explicitly named and holds a unique identifier. +\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 @@ -110,48 +112,49 @@ 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''. The \isa{copy} operation - produces an auxiliary version with 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. + invalidated draft is called ``stale''. - The example below shows a theory graph derived from \isa{Pure}. - Theory \isa{Length} imports \isa{Nat} and \isa{List}. - The linear draft mode is enabled during the ``\isa{{\isasymdots}}'' stage of - the theory body. + 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 + bookeeping. + + The \isa{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. - \bigskip + \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 toplevel, cf.\ \secref{sec:isar-toplevel}. + + \begin{figure}[htb] + \begin{center} \begin{tabular}{rcccl} - & & $Pure$ \\ - & & $\downarrow$ \\ - & & $FOL$ \\ + & & \isa{Pure} \\ + & & \isa{{\isasymdown}} \\ + & & \isa{FOL} \\ & $\swarrow$ & & $\searrow$ & \\ - $Nat$ & & & & $List$ \\ + $Nat$ & & & & \isa{List} \\ & $\searrow$ & & $\swarrow$ \\ - & & $Length$ \\ + & & \isa{Length} \\ & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\ & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\ & & $\vdots$~~ \\ + & & \isa{{\isasymbullet}}~~ \\ + & & $\vdots$~~ \\ + & & \isa{{\isasymbullet}}~~ \\ + & & $\vdots$~~ \\ & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\ \end{tabular} - - \medskip In practice, derived theory operations mostly operate - drafts, namely the body of the current portion of theory that the - user happens to be composing. - - \medskip There is also a builtin theory history mechanism that amends for - the destructive behaviour of theory drafts. The \isa{checkpoint} operation produces an intermediate stepping stone that - survives the next update unscathed: both the original and the - changed theory remain valid and are related by the sub-theory - relation. This recovering of pure theory values comes at the cost - of extra internal bookeeping. The cumulative effect of - checkpointing is purged by the \isa{finish} operation. - - History operations are usually managed by the system, e.g.\ notably - in the Isar transaction loop. - - \medskip - FIXME theory data% + \caption{Theory definition depending on ancestors}\label{fig:ex-theory} + \end{center} + \end{figure}% \end{isamarkuptext}% \isamarkuptrue% % @@ -162,7 +165,49 @@ \isatagmlref % \begin{isamarkuptext}% -% +\begin{mldecls} + \indexmltype{theory}\verb|type theory| \\ + \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\ + \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\ + \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\ + \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex] + \indexmltype{theory-ref}\verb|type theory_ref| \\ + \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\ + \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\ + \end{mldecls} + + \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.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} + compares theories according to the inherent graph structure of the + construction. This sub-theory relation is a nominal approximation + of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content. + + \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} + absorbs one theory into the other. This fails for unrelated + theories! + + \item \verb|Theory.checkpoint|~\isa{thy} produces a safe + 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_ref| represents a sliding reference to a + valid theory --- updates on the original are propagated + automatically. + + \item \verb|Theory.self_ref| and \verb|Theory.deref| 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. + + \end{description}% \end{isamarkuptext}% \isamarkuptrue% % @@ -178,35 +223,36 @@ \isamarkuptrue% % \begin{isamarkuptext}% -A proof context is an arbitrary container that is initialized from a - given theory. The result contains a back-reference to the theory it - belongs to, together with pure data. No further bookkeeping is - required here, thanks to the lack of destructive features. +\glossary{Proof context}{The static context of a structured proof, + acts like a local ``theory'' of the current portion of Isar proof + text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in + judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a + generic notion of introducing and discharging hypotheses. + Arbritrary auxiliary context data may be adjoined.} - There is no restriction on producing proof contexts, although the - usual discipline is to follow block structure as a mental model: a - given context is extended consecutively, results are exported back - into the original context. In particular, the concept of Isar proof - state models block-structured reasoning explicitly, using a stack of - proof contexts. + A proof context is a container for pure data with a back-reference + to the theory it belongs to. Modifications to draft theories are + propagated automatically as usual, but there is also an explicit + \isa{transfer} operation to resynchronize 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. - Due to the lack of identification and back-referencing, entities - derived in a proof context need to record inherent logical - requirements explicitly. For example, hypotheses used in a - derivation will be recorded separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double sure. Results could leak into an alien - proof context do to programming errors, but Isabelle/Isar - occasionally includes extra validity checks at the end of a - sub-proof. + 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 + 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. - \medskip - FIXME proof data - -\glossary{Proof context}{The static context of a structured proof, -acts like a local ``theory'' of the current portion of Isar proof -text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in -judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a -generic notion of introducing and discharging hypotheses. Arbritrary -auxiliary context data may be adjoined.}% + 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}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -255,6 +301,15 @@ % \endisadelimmlref % +\isamarkupsubsection{Context data% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Named entities% } \isamarkuptrue% @@ -355,11 +410,11 @@ is merely an alias for \verb|string|, but emphasizes the specific format encountered here. - \item \verb|Symbol.explode|~\isa{s} produces an actual 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 \isa{implode} may be - used for the reverse operation. + \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. \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 diff -r 7e616709bca2 -r 5b75f1c4d7d6 doc-src/IsarImplementation/Thy/integration.thy --- a/doc-src/IsarImplementation/Thy/integration.thy Thu Aug 31 14:36:48 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/integration.thy Thu Aug 31 14:53:55 2006 +0200 @@ -5,7 +5,7 @@ chapter {* System integration *} -section {* Isar toplevel *} +section {* Isar toplevel \label{sec:isar-toplevel} *} text {* The Isar toplevel may be considered the centeral hub of the Isabelle/Isar system, where all key components and sub-systems are diff -r 7e616709bca2 -r 5b75f1c4d7d6 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 14:36:48 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 14:53:55 2006 +0200 @@ -73,6 +73,8 @@ subsection {* Theory context \label{sec:context-theory} *} 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 @@ -90,89 +92,132 @@ 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''. The @{text "copy"} operation - produces an auxiliary version with 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. + invalidated draft is called ``stale''. - The example below shows a theory graph derived from @{text "Pure"}. - Theory @{text "Length"} imports @{text "Nat"} and @{text "List"}. - The linear draft mode is enabled during the ``@{text "\"}'' stage of - the theory body. + 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 + bookeeping. + + 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. - \bigskip + \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 toplevel, cf.\ \secref{sec:isar-toplevel}. + + \begin{figure}[htb] + \begin{center} \begin{tabular}{rcccl} - & & $Pure$ \\ - & & $\downarrow$ \\ - & & $FOL$ \\ + & & @{text "Pure"} \\ + & & @{text "\"} \\ + & & @{text "FOL"} \\ & $\swarrow$ & & $\searrow$ & \\ - $Nat$ & & & & $List$ \\ + $Nat$ & & & & @{text "List"} \\ & $\searrow$ & & $\swarrow$ \\ - & & $Length$ \\ + & & @{text "Length"} \\ & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\ & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\ & & $\vdots$~~ \\ + & & @{text "\"}~~ \\ + & & $\vdots$~~ \\ + & & @{text "\"}~~ \\ + & & $\vdots$~~ \\ & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\ \end{tabular} - - \medskip In practice, derived theory operations mostly operate - drafts, namely the body of the current portion of theory that the - user happens to be composing. - - \medskip There is also a builtin theory history mechanism that amends for - the destructive behaviour of theory drafts. The @{text - "checkpoint"} operation produces an intermediate stepping stone that - survives the next update unscathed: both the original and the - changed theory remain valid and are related by the sub-theory - relation. This recovering of pure theory values comes at the cost - of extra internal bookeeping. The cumulative effect of - checkpointing is purged by the @{text "finish"} operation. - - History operations are usually managed by the system, e.g.\ notably - in the Isar transaction loop. - - \medskip - FIXME theory data + \caption{Theory definition depending on ancestors}\label{fig:ex-theory} + \end{center} + \end{figure} *} text %mlref {* + \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"} \\[1ex] + @{index_ML_type theory_ref} \\ + @{index_ML Theory.self_ref: "theory -> theory_ref"} \\ + @{index_ML Theory.deref: "theory_ref -> theory"} \\ + \end{mldecls} + + \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 "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 "\"}) 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.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. + + \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. + + \item @{ML_type theory_ref} represents a sliding reference to a + valid theory --- updates on the original are propagated + automatically. + + \item @{ML "Theory.self_ref"} and @{ML "Theory.deref"} 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. + + \end{description} *} subsection {* Proof context \label{sec:context-proof} *} text {* - A proof context is an arbitrary container that is initialized from a - given theory. The result contains a back-reference to the theory it - belongs to, together with pure data. No further bookkeeping is - required here, thanks to the lack of destructive features. + \glossary{Proof context}{The static context of a structured proof, + acts like a local ``theory'' of the current portion of Isar proof + text, generalizes the idea of local hypotheses @{text "\"} in + judgments @{text "\ \ \"} of natural deduction calculi. There is a + generic notion of introducing and discharging hypotheses. + Arbritrary auxiliary context data may be adjoined.} - There is no restriction on producing proof contexts, although the - usual discipline is to follow block structure as a mental model: a - given context is extended consecutively, results are exported back - into the original context. In particular, the concept of Isar proof - state models block-structured reasoning explicitly, using a stack of - proof contexts. + A proof context is a container for pure data with a back-reference + to the theory it belongs to. Modifications to draft theories are + propagated automatically as usual, but there is also an explicit + @{text "transfer"} operation to resynchronize 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. - Due to the lack of identification and back-referencing, entities - derived in a proof context need to record inherent logical - requirements explicitly. For example, hypotheses used in a - derivation will be recorded separately within the sequent @{text "\ - \ \"}, just to make double sure. Results could leak into an alien - proof context do to programming errors, but Isabelle/Isar - occasionally includes extra validity checks at the end of a - sub-proof. + 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 + 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. - \medskip - FIXME proof data - -\glossary{Proof context}{The static context of a structured proof, -acts like a local ``theory'' of the current portion of Isar proof -text, generalizes the idea of local hypotheses @{text "\"} in -judgments @{text "\ \ \"} of natural deduction calculi. There is a -generic notion of introducing and discharging hypotheses. Arbritrary -auxiliary context data may be adjoined.} - + 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}. *} text %mlref {* FIXME *} @@ -185,6 +230,12 @@ text %mlref {* FIXME *} +subsection {* Context data *} + +text {* +*} + + section {* Named entities *} text {* Named entities of different kinds (logical constant, type, @@ -277,11 +328,11 @@ is merely an alias for @{ML_type "string"}, but emphasizes the specific format encountered here. - \item @{ML "Symbol.explode"}~@{text "s"} produces an actual 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 @{text "implode"} may be - used for the reverse operation. + \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. \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols