--- 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 "\<verbclose>"}\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\""}
*}