# HG changeset patch # User wenzelm # Date 1286451541 -3600 # Node ID bf164c153d107c58e5ad186ce842fc1b930d7697 # Parent cd691e2c7a1ac2f368cc33d88041d092e5a3a817 minor tuning and updating; diff -r cd691e2c7a1a -r bf164c153d10 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Fri Oct 01 17:23:26 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Thu Oct 07 12:39:01 2010 +0100 @@ -552,12 +552,14 @@ @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\ @{index_ML Thm.add_axiom: "binding * term -> theory -> (string * thm) * theory"} \\ - @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory - -> (string * ('a -> thm)) * theory"} \\ - @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> (string * thm) * theory"} \\ + @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> + (string * ('a -> thm)) * theory"} \\ + @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> + (string * thm) * theory"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\ + @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> + theory -> theory"} \\ \end{mldecls} \begin{description} diff -r cd691e2c7a1a -r bf164c153d10 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Fri Oct 01 17:23:26 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Oct 07 12:39:01 2010 +0100 @@ -140,13 +140,13 @@ \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. Dynamic updating stops after - an explicit @{text "end"} only. + drafts are propagated automatically. Dynamic updating stops when + the next @{text "checkpoint"} is reached. 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. + the formal context from which they are derived. This implicitly + assumes monotonic reasoning, because the referenced context may + become larger without further notice. *} text %mlref {* @@ -167,9 +167,11 @@ \begin{description} \item @{ML_type theory} represents theory contexts. This is - essentially a linear type, with explicit runtime checking! Most - internal theory operations destroy the original version, which then - becomes ``stale''. + essentially a linear type, with explicit runtime checking. + Primitive theory operations destroy the original version, which then + becomes ``stale''. This can be prevented by explicit checkpointing, + which the system does at least at the boundary of toplevel command + transactions \secref{sec:isar-toplevel}. \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories according to the intrinsic graph structure of the construction. @@ -213,8 +215,8 @@ 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. + back-reference to the theory from which it is derived. 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 @@ -359,15 +361,20 @@ 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. + operation of \emph{all} theory data slots ever declared. This also + means that one needs to be economic about the total number of proof + data declarations in the system, i.e.\ each ML module should declare + at most one, sometimes two data slots for its internal use. + Repeated data declarations to simulate a record type should be + avoided! \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 Any of these data declaration over type @{text "T"} result - in an ML structure with the following signature: + \bigskip Any of the above data declarations over type @{text "T"} + result in an ML structure with the following signature: \medskip \begin{tabular}{ll} @@ -379,10 +386,10 @@ \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. + This interface 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 {* @@ -442,23 +449,26 @@ val get = Terms.get; fun add raw_t thy = - let val t = Sign.cert_term thy raw_t - in Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy end; + let + val t = Sign.cert_term thy raw_t; + in + Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy + end; end; *} -text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient - representation of a set of terms: all operations are linear in the - number of stored elements. Here we assume that our users do not - care about the declaration order, since that data structure forces - its own arrangement of elements. +text {* \noindent We use @{ML_type "term Ord_List.T"} for reasonably + efficient representation of a set of terms: all operations are + linear in the number of stored elements. Here we assume that users + of this module do not care about the declaration order, since that + data structure forces its own arrangement of elements. Observe how the @{verbatim merge} operation joins the data slots of the two constituents: @{ML Ord_List.union} prevents duplication of common data from different branches, thus avoiding the danger of - exponential blowup. (Plain list append etc.\ must never be used for - theory data merges.) + exponential blowup. Plain list append etc.\ must never be used for + theory data merges! \medskip Our intended invariant is achieved as follows: \begin{enumerate} @@ -479,7 +489,7 @@ type-inference via @{ML Syntax.check_term} (cf.\ \secref{sec:term-check}) is not necessarily monotonic wrt.\ the background theory, since constraints of term constants can be - strengthened by later declarations, for example. + modified by later declarations, for example. In most cases, user-space context data does not have to take such invariants too seriously. The situation is different in the @@ -598,12 +608,11 @@ symbols. \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list - from the packed form. This function supercedes @{ML + from the packed form. This function supersedes @{ML "String.explode"} for virtually all purposes of manipulating text in Isabelle!\footnote{The runtime overhead for exploded strings is mainly that of the list structure: individual symbols that happen to - be a singleton string --- which is the most common case --- do not - require extra memory in Poly/ML.} + be a singleton string do not require extra memory in Poly/ML.} \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard diff -r cd691e2c7a1a -r bf164c153d10 doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Fri Oct 01 17:23:26 2010 +0200 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Thu Oct 07 12:39:01 2010 +0100 @@ -146,7 +146,7 @@ *} text %mlex {* The following example (in theory @{theory Pure}) shows - how to work with fixed term and type parameters work with + how to work with fixed term and type parameters and with type-inference. *} @@ -185,15 +185,14 @@ ctxt0 |> Variable.variant_fixes ["x", "x", "x"]; *} -text {* \noindent Subsequent ML code can now work with the invented +text {* \noindent The following ML code can now work with the invented names of @{verbatim x1}, @{verbatim x2}, @{verbatim x3}, without depending on the details on the system policy for introducing these variants. Recall that within a proof body the system always invents fresh ``skolem constants'', e.g.\ as follows: *} -lemma "PROP XXX" -proof - +example_proof ML_prf %"ML" {* val ctxt0 = @{context}; @@ -381,10 +380,14 @@ text %mlref {* \begin{mldecls} - @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ + @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) -> + Proof.context -> int -> tactic"} \\ + @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) -> + Proof.context -> int -> tactic"} \\ + @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) -> + Proof.context -> int -> tactic"} \\ + @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) -> + Proof.context -> int -> tactic"} \\ \end{mldecls} \begin{mldecls} @@ -394,8 +397,8 @@ ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Obtain.result: "(Proof.context -> tactic) -> - thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\ + @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list -> + Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\ \end{mldecls} \begin{description}