isabelle-cookbook: comparison ProgTutorial/Advanced.thy

equal deleted inserted replaced

-:76c632c05949
+:7294b1b839a8
 *}
 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 \<Rightarrow> 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"
 val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)
 in
 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. 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}
 @{ML "let
 val trm = @{term \"(x, y, z, w)\"}
 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.  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}
 |> Variable.add_fixes [\"x\", \"x\"]"
 "ERROR: Duplicate fixed variable(s): \"x\""}
 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
 val ctxt0 = @{context}
 val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
 Variable.variant_frees ctxt1 [] frees
 end"
 "[(\"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, since @{text x} and @{text xa} occur in the term we declared.
-variables; it just makes them ``known'' to the context. This is helpful when
+Note that @{ML_ind declare_term in Variable} does not fix the
-parsing terms using the function @{ML_ind read_term in Syntax} from the
+variables; it just makes them ``known'' to the context. You can see
-structure @{ML_struct Syntax}. Consider the following code:
+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
 val ctxt0 = @{context}
 val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
 Syntax.read_term ctxt2 \"x\")
 end"
 "(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}
 \begin{linenos}
 @{ML "let
 @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%
 @{text "?x ?y ?z"}
 \end{graybox}
 \end{isabelle}
-In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in context @{text ctxt1}.
+In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in
-The function @{ML_ind export_terms in Variable} from the @{ML_struct Variable} can be used
+context @{text ctxt1}.  The function @{ML_ind export_terms in
-to ``transfer'' terms between contexts. Transferring means to turn all (free) variables that
+Variable} from the @{ML_struct Variable} can be used to ``transfer''
-are fixed in one context, but not in the other, into schematic variables. In our example
+terms between contexts. Transferring means to turn all (free)
-we are transferring the term @{text "P x y z"} from context @{text "ctxt1"} into @{text "ctxt0"}
+variables that are fixed in one context, but not in the other, into
-which means @{term x}, @{term y} and @{term z} become schematic variables (as can be seen
+schematic variables. In our example, we are transferring the term
-by the leading question mark). Note that the variable @{text P} stays a free variable, since
+@{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"},
-it not fixed in @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does not
+which means @{term x}, @{term y} and @{term z} become schematic
-know about it. Note also that in Line 6 we had to use the function @{ML_ind singleton},
+variables (as can be seen by the leading question marks). Note that
-because the function @{ML_ind export_terms in Variable} normally works over lists of terms.
+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.
-ML {*
-let
+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 (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0
-val foo_trm = @{term "P x y z"}
+val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
 in
-singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
+singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-|> pretty_term ctxt1
+end"
-|> pwriteln
+"> P ?x ?y ?z ?x ?y ?z"}
-end
+*}
-*}
 ML {*
 let
 val thy = @{theory}
 val ctxt0 = @{context}
 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
-*}
 text {*
 *}

changeset 498	7294b1b839a8
parent 497	76c632c05949
child 499	42bac8b16951