--- a/ProgTutorial/Advanced.thy Sat Nov 12 20:28:30 2011 +0000
+++ b/ProgTutorial/Advanced.thy Mon Nov 14 12:01:45 2011 +0000
@@ -161,7 +161,7 @@
setup %graylinenos {* fn thy =>
let
val tmp_thy = Theory.copy thy
- val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)
+ val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn)
val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
val trm2 = Syntax.read_term_global thy "FOO baz"
@@ -259,7 +259,7 @@
specified by strings. Let us come back to the point about printing terms. Consider
printing out the term \mbox{@{text "(x, y, z, w)"}} using our function @{ML_ind pretty_term}.
This function takes a term and a context as argument. Notice how the printing
- of the term changes with which context is used.
+ of the term changes according to which context is used.
\begin{isabelle}
\begin{graybox}
@@ -298,7 +298,7 @@
free variables as being alien or faulty. Therefore the highlighting.
While this seems like a minor detail, the concept of making the context aware
of fixed variables is actually quite useful. For example it prevents us from
- fixing a variable twice
+ fixing a variable twice.
@{ML_response_fake [gray, display]
"@{context}
@@ -308,7 +308,7 @@
More importantly it also allows us to easily create fresh free variables avoiding any
clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context
@{text ctxt1}. Next we want to create two fresh variables of type @{typ nat}
- as variants of the string @{text [quotes] "x"}.
+ as variants of the string @{text [quotes] "x"} (Lines 6 and 7).
@{ML_response_fake [display, gray, linenos]
"let
@@ -340,10 +340,31 @@
"[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
The result is @{text xb} and @{text xc} for the names of the fresh
- variables. Note that @{ML_ind declare_term in Variable} does not fix the
- variables; it just makes them ``known'' to the context. This is helpful when
- parsing terms using the function @{ML_ind read_term in Syntax} from the
- structure @{ML_struct Syntax}. Consider the following code:
+ variables, since @{text x} and @{text xa} occur in the term we declared.
+ Note that @{ML_ind declare_term in Variable} does not fix the
+ variables; it just makes them ``known'' to the context. You can see
+ that if you print out a declared term.
+
+ \begin{isabelle}
+ \begin{graybox}
+ @{ML "let
+ val trm = @{term \"P x y z\"}
+ val ctxt1 = Variable.declare_term trm @{context}
+in
+ pwriteln (pretty_term ctxt1 trm)
+end"}\\
+ \setlength{\fboxsep}{0mm}
+ @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%
+ \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}~%
+ \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}~%
+ \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}
+ \end{graybox}
+ \end{isabelle}
+
+ All variables are highligted, indicating that they are not
+ fixed. However, declaring a term is helpful when parsing terms using
+ the function @{ML_ind read_term in Syntax} from the structure
+ @{ML_struct Syntax}. Consider the following code:
@{ML_response_fake [gray, display]
"let
@@ -372,7 +393,7 @@
"(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
The most useful feature of contexts is that one can export terms and theorems
- between contexts. Let us consider first the case of terms.
+ between them. Let us show this first in the case of terms.
\begin{isabelle}
\begin{graybox}
@@ -393,31 +414,40 @@
\end{graybox}
\end{isabelle}
- In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in context @{text ctxt1}.
- The function @{ML_ind export_terms in Variable} from the @{ML_struct Variable} can be used
- to ``transfer'' terms between contexts. Transferring means to turn all (free) variables that
- are fixed in one context, but not in the other, into schematic variables. In our example
- we are transferring the term @{text "P x y z"} from context @{text "ctxt1"} into @{text "ctxt0"}
- which means @{term x}, @{term y} and @{term z} become schematic variables (as can be seen
- by the leading question mark). Note that the variable @{text P} stays a free variable, since
- it not fixed in @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does not
- know about it. Note also that in Line 6 we had to use the function @{ML_ind singleton},
- because the function @{ML_ind export_terms in Variable} normally works over lists of terms.
-
-
+ In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in
+ context @{text ctxt1}. The function @{ML_ind export_terms in
+ Variable} from the @{ML_struct Variable} can be used to ``transfer''
+ terms between contexts. Transferring means to turn all (free)
+ variables that are fixed in one context, but not in the other, into
+ schematic variables. In our example, we are transferring the term
+ @{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"},
+ which means @{term x}, @{term y} and @{term z} become schematic
+ variables (as can be seen by the leading question marks). Note that
+ the variable @{text P} stays a free variable, since it not fixed in
+ @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does
+ not know about it. Note also that in Line 6 we had to use the
+ function @{ML_ind singleton}, because the function @{ML_ind
+ export_terms in Variable} normally works over lists of terms.
+
+ The case of transferring theorems is even more useful. The reason is
+ that the generalisation of fixed variables to schematic variables is
+ not trivial. For illustration purposes we use in the following code
+ the function @{ML_ind make_thm in Skip_Proof} from the structure
+ @{ML_struct Skip_Proof} in order to turn an arbitray term into a
+ theorem.
+
+ @{ML_response_fake [display, gray]
+ "let
+ val thy = @{theory}
+ val ctxt0 = @{context}
+ val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0
+ val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
+in
+ singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
+end"
+ "> P ?x ?y ?z ?x ?y ?z"}
*}
-ML {*
-let
- val ctxt0 = @{context}
- val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
- val foo_trm = @{term "P x y z"}
-in
- singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
- |> pretty_term ctxt1
- |> pwriteln
-end
-*}
ML {*
let
@@ -430,16 +460,6 @@
end
*}
-ML {*
-let
- val thy = @{theory}
- val ctxt0 = @{context}
- val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
- val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
-in
- singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end
-*}
text {*