isabelle-cookbook: comparison ProgTutorial/Advanced.thy

equal deleted inserted replaced

-:f3f24874e8be
+:80eb66aefc66
 txt_raw {*\mbox{}\\[-7mm]*}
 ML_prf {* Variable.dest_fixes @{context} *}
 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
 @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes
 a context and returns all its currently fixed variable (names). That
 text {*
 Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables;
 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};
 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;
 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*}
 text {*
 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}
 @{ML "let
 val trm = @{term \"(x, y, z, w)\"}
 \end{graybox}
 \end{isabelle}
 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
 are printed as expected. The point of this example is that the context
 contains the information which variables are fixed, and designates all other
 @{ML_response_fake [gray, display]
 "@{context}
 |> Variable.add_fixes [\"x\", \"x\"]"
 "ERROR: Duplicate fixed variable(s): \"x\""}
-But it also allows us to easily create fresh free variables avoiding any
+More importantly 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
+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"}.
 @{ML_response_fake [display, gray, linenos]
 "let
 Variable.variant_frees ctxt1 [] frees)
 end"
 "([(\"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
+Often one has the problem that given some terms, create fresh variables
-avoiding any variable occuring in those terms. For this you can use the
+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]
 "let
 val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
 in
 Variable.variant_frees ctxt1 [] frees
 end"
 "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
-The result is @{text xb} and @{text xc} for the names of the freshh variables. This
+The result is @{text xb} and @{text xc} for the names of the fresh
-is also important when parsing terms, for example with the function
+variables. Note that @{ML_ind declare_term in Variable} does not fix the
-@{ML_ind read_term in Syntax} from the structure @{ML_struct Syntax}. Consider
+variables; it just makes them ``known'' to the context. This is helpful when
-the following code:
+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
 val ctxt0 = @{context}
 val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
 (Syntax.read_term ctxt0 \"x\",
 Syntax.read_term ctxt1 \"x\")
 end"
 "(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
-Parsing the string in the first context results in a free variable
+Parsing the string in the context @{text "ctxt0"} results in a free variable
-with a default polymorphic type, but in the second case we obtain a
+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
+type the parsed term receives depends upon the last declaration that
-is made as the next example illustrates.
+is made, as the next example illustrates.
 @{ML_response_fake [gray, display]
 "let
 val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
 val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
 (Syntax.read_term ctxt1 \"x\",
 Syntax.read_term ctxt2 \"x\")
 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
 *}

changeset 496	80eb66aefc66
parent 495	f3f24874e8be
child 497	76c632c05949