--- a/ProgTutorial/Advanced.thy Fri Nov 11 16:27:04 2011 +0000
+++ b/ProgTutorial/Advanced.thy Sat Nov 12 11:45:39 2011 +0000
@@ -216,7 +216,7 @@
txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
text {*
- The interesting point in this proof is that we injected ML-code before and after
+ The interesting point is that we injected ML-code before and after
the variables are fixed. For this remember that ML-code inside a proof
needs to be enclosed inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"},
not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function
@@ -247,7 +247,7 @@
the second time we get only the fixes variables @{text x} and @{text y} as answer, since
@{text z} and @{text w} are not anymore in the scope of the context.
This means the curly-braces act on the Isabelle level as opening and closing statements
- for a context. The above proof fragment corresoponds roughly to the following ML-code
+ for a context. The above proof fragment corresponds roughly to the following ML-code
*}
ML{*val ctxt0 = @{context};
@@ -258,7 +258,8 @@
where the function @{ML_ind add_fixes in Variable} fixes a list of variables
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.
+ This function takes a term and a context as argument. Notice how the printing
+ of the term changes with which context is used.
\begin{isabelle}
\begin{graybox}
@@ -288,7 +289,7 @@
The term we are printing is in all three cases the same---a tuple containing
- four free variables. As you can see in case of @{ML "ctxt0"}, however, all
+ four free variables. As you can see, however, in case of @{ML "ctxt0"} all
variables are highlighted indicating a problem, while in case of @{ML
"ctxt1"} @{text x} and @{text y} are printed as normal (blue) free
variables, but not @{text z} and @{text w}. In the last case all variables
@@ -304,8 +305,8 @@
|> Variable.add_fixes [\"x\", \"x\"]"
"ERROR: Duplicate fixed variable(s): \"x\""}
- But it also allows us to easily create fresh free variables avoiding any
- clashes. In Line~3 below we fix the variable @{text x} in the context
+ 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"}.
@@ -321,12 +322,12 @@
"([(\"x\", \"nat\"), (\"xa\", \"nat\")],
[(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
- As can be seen, if we create the fresh variables with the context @{text ctxt0},
+ As you can see, if we create the fresh variables with the context @{text ctxt0},
then we obtain @{text "x"} and @{text "xa"}; but in @{text ctxt1} we obtain @{text "xa"}
and @{text "xb"} avoiding @{text x}, which was fixed in this context.
- Often one has the situation that given some terms, create fresh variables
- avoiding any variable occuring in those terms. For this you can use the
+ Often one has the problem that given some terms, create fresh variables
+ avoiding any variable occurring in those terms. For this you can use the
function @{ML_ind declare_term in Variable} from the structure @{ML_struct Variable}.
@{ML_response_fake [gray, display]
@@ -338,10 +339,11 @@
end"
"[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
- The result is @{text xb} and @{text xc} for the names of the freshh variables. This
- is also important when parsing terms, for example with the function
- @{ML_ind read_term in Syntax} from the structure @{ML_struct Syntax}. Consider
- the following code:
+ 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:
@{ML_response_fake [gray, display]
"let
@@ -353,11 +355,11 @@
end"
"(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
- Parsing the string in the first context results in a free variable
- with a default polymorphic type, but in the second case we obtain a
+ Parsing the string in the context @{text "ctxt0"} results in a free variable
+ with a default polymorphic type, but in case of @{text "ctxt1"} we obtain a
free variable of type @{typ nat} as previously declared. Which
- type the parsed term receives depends on the last declaration that
- is made as the next example illustrates.
+ type the parsed term receives depends upon the last declaration that
+ is made, as the next example illustrates.
@{ML_response_fake [gray, display]
"let
@@ -369,14 +371,39 @@
end"
"(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
+ The most useful feature of contexts is that one can export, for example,
+ terms between contexts.
*}
ML {*
let
val ctxt0 = @{context}
- val trm = @{prop "P x y z"}
- val foo_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt0) trm
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
+ 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
+*}
+
+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