# HG changeset patch # User Christian Urban # Date 1321272105 0 # Node ID 7294b1b839a831c4b8d2f0147a476e5e7e63d395 # Parent 76c632c05949702f7776d3e28ab6d2110bd2041c tuned diff -r 76c632c05949 -r 7294b1b839a8 ProgTutorial/Advanced.thy --- 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 \ 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 {* diff -r 76c632c05949 -r 7294b1b839a8 progtutorial.pdf Binary file progtutorial.pdf has changed