# HG changeset patch # User Christian Urban # Date 1321098339 0 # Node ID 80eb66aefc665e25281423110347e6ee89e3c57f # Parent f3f24874e8becc4aec3102bbf9af77d026707a8d tuned diff -r f3f24874e8be -r 80eb66aefc66 ProgTutorial/Advanced.thy --- 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 "\ \ \"}, not \isacommand{ML}~@{text "\ \ \"}. 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 diff -r f3f24874e8be -r 80eb66aefc66 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Fri Nov 11 16:27:04 2011 +0000 +++ b/ProgTutorial/First_Steps.thy Sat Nov 12 11:45:39 2011 +0000 @@ -669,13 +669,13 @@ ML{*val (((one_def, two_def), three_def), ctxt') = @{context} - |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) + |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*} text {* - where we make three definitions, namely @{term "one \ 1::nat"}, @{term "two \ 2::nat"} - and @{term "three \ 3::nat"}. The point of this code is that we augment the initial + where we make three definitions, namely @{term "One \ 1::nat"}, @{term "Two \ 2::nat"} + and @{term "Three \ 3::nat"}. The point of this code is that we augment the initial context with the definitions. The result we are interested in is the augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing information about the definitions---the function @{ML_ind add_def in Local_Defs} returns diff -r f3f24874e8be -r 80eb66aefc66 progtutorial.pdf Binary file progtutorial.pdf has changed