# HG changeset patch # User Christian Urban # Date 1321028824 0 # Node ID f3f24874e8becc4aec3102bbf9af77d026707a8d # Parent 743020b817af91fedbc91ebe8ac64d89e4ddbab5 more on contexts diff -r 743020b817af -r f3f24874e8be ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Thu Nov 10 19:25:25 2011 +0000 +++ b/ProgTutorial/Advanced.thy Fri Nov 11 16:27:04 2011 +0000 @@ -101,7 +101,7 @@ @{text "> \"BAR\" :: \"'a\""} \end{isabelle} - you can see that you do \emph{not} obtain a constant of type @{typ nat}, but a free + you can see that you do \emph{not} obtain the expected constant of type @{typ nat}, but a free variable (printed in blue) of polymorphic type. The problem is that the ML-expression above did not ``register'' the declaration with the current theory. This is what the command \isacommand{setup} is for. The constant is properly @@ -143,7 +143,7 @@ in thy end"}~@{text "\"}\isanewline - @{text "> ERROR \"Stale theory encountered\""} + @{text "> ERROR: \"Stale theory encountered\""} \end{graybox} \end{isabelle} @@ -194,7 +194,7 @@ were already made. *} -section {* Contexts (TBD) *} +section {* Contexts *} text {* Contexts are arguably more important than theories, even though they only @@ -243,10 +243,11 @@ txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) text {* - 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. - This means the curly-braces act as opening and closing statements for a context. - The above proof corresoponds roughly to the following ML-code. + 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 *} ML{*val ctxt0 = @{context}; @@ -256,38 +257,133 @@ 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 @{text "(x, y, z, w)"} using the function @{ML_ind pretty_term}. + 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. -*} -ML {* -let - val trm = @{term "(x, y, z, w)"} + \begin{isabelle} + \begin{graybox} + @{ML "let + val trm = @{term \"(x, y, z, w)\"} in pwriteln (Pretty.chunks [ pretty_term ctxt0 trm, pretty_term ctxt1 trm, pretty_term ctxt2 trm ]) +end"}\\ + \setlength{\fboxsep}{0mm} + @{text ">"}~@{text "("}\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}\\ + @{text ">"}~@{text "("}\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~% + \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}\\ + @{text ">"}~@{text "("}\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~% + \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~% + \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~% + \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"} + \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 + 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 + free variables as being alien or faulty. 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 + + @{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 + clashes. 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 + val ctxt0 = @{context} + val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0 + val frees = replicate 2 (\"x\", @{typ nat}) +in + (Variable.variant_frees ctxt0 [] frees, + 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}, + 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 + 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} + val frees = replicate 2 (\"x\", @{typ nat}) +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 + 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: + + @{ML_response_fake [gray, display] + "let + val ctxt0 = @{context} + val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0 +in + (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 + with a default polymorphic type, but in the second case 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. + + @{ML_response_fake [gray, display] + "let + val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context} + val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1 +in + (Syntax.read_term ctxt1 \"x\", + Syntax.read_term ctxt2 \"x\") +end" + "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"} + +*} + +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 +in + singleton (Proof_Context.export ctxt1 ctxt0) foo_thm end *} +text {* -text {* - 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 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 is that the context contains the information - which variables are fixed, and designates all other free variables as being alien or faulty. - While this seems like a minor feat, the concept of making the context aware of - fixed variables is actually quite useful. For example it prevents us from fixing a - variable twice - - @{ML_response_fake [gray, display] - "@{context} -|> Variable.add_fixes [\"x\", \"y\"] -||>> Variable.add_fixes [\"x\", \"y\"]" - "Duplicate fixed variable(s): \"x\""} *} diff -r 743020b817af -r f3f24874e8be progtutorial.pdf Binary file progtutorial.pdf has changed