isabelle-cookbook: comparison ProgTutorial/Advanced.thy

equal deleted inserted replaced

-:95b42288294e
+:438703674711
 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
-@{ML_matchresult_fake [gray, display]
+@{ML_response [gray, display]
 \<open>@{context}
 |> Variable.add_fixes ["x", "x"]\<close>
-\<open>ERROR: Duplicate fixed variable(s): "x"\<close>}
+\<open>Duplicate fixed variable(s): "x"\<close>}
 More importantly it also allows us to easily create fresh names for
 fixed variables.  For this you have to use the function @{ML_ind
 variant_fixes in Variable} from the structure @{ML_structure Variable}.
-@{ML_matchresult_fake [gray, display]
+@{ML_response [gray, display]
 \<open>@{context}
 |> Variable.variant_fixes ["y", "y", "z"]\<close>
-\<open>(["y", "ya", "z"], ...)\<close>}
+\<open>(["y", "ya", "z"],\<dots>\<close>}
 Now a fresh variant for the second occurence of \<open>y\<close> is created
 avoiding any clash. In this way we can also create fresh free variables
 that avoid any clashes with fixed variables. In Line~3 below we fix
 the variable \<open>x\<close> in the context \<open>ctxt1\<close>. Next we want to
 create two fresh variables of type @{typ nat} as variants of the
 string @{text [quotes] "x"} (Lines 6 and 7).
-@{ML_matchresult_fake [display, gray, linenos]
+@{ML_matchresult [display, gray, linenos]
 \<open>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\<close>
-\<open>([("x", "nat"), ("xa", "nat")],
+\<open>([("x", _), ("xa", _)],
-[("xa", "nat"), ("xb", "nat")])\<close>}
+[("xa", _), ("xb", _)])\<close>}
 As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,
 then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>
 and \<open>xb\<close> avoiding \<open>x\<close>, which was fixed in this context.
 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_structure Variable}.
-@{ML_matchresult_fake [gray, display]
+@{ML_matchresult [gray, display]
 \<open>let
 val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}
 val frees = replicate 2 ("x", @{typ nat})
 in
 Variable.variant_frees ctxt1 [] frees
 end\<close>
-\<open>[("xb", "nat"), ("xc", "nat")]\<close>}
+\<open>[("xb", _), ("xc", _)]\<close>}
 The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh
 variables, since \<open>x\<close> and \<open>xa\<close> 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
 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_structure Syntax}. Consider the following code:
-@{ML_matchresult_fake [gray, display]
+@{ML_response [gray, display]
 \<open>let
 val ctxt0 = @{context}
 val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0
 in
 (Syntax.read_term ctxt0 "x",
 with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a
 free variable of type @{typ nat} as previously declared. Which
 type the parsed term receives depends upon the last declaration that
 is made, as the next example illustrates.
-@{ML_matchresult_fake [gray, display]
+@{ML_response [gray, display]
 \<open>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",
 following code the function @{ML_ind make_thm in Skip_Proof} from the
 structure @{ML_structure Skip_Proof}. This function will turn an arbitray
 term, in our case @{term "P x y z x y z"}, into a theorem (disregarding
 whether it is actually provable).
-@{ML_matchresult_fake [display, gray]
+@{ML_response [display, gray]
 \<open>let
 val thy = @{theory}
 val ctxt0 = @{context}
 val (_, ctxt1) = Variable.add_fixes ["P", "x", "y", "z"] ctxt0
 val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z x y z"}
 that exporting from one to another is not just restricted to
 variables, but also works with assumptions. For this we can use the
 function @{ML_ind export in Assumption} from the structure
 @{ML_structure Assumption}. Consider the following code.
-@{ML_matchresult_fake [display, gray, linenos]
+@{ML_response [display, gray, linenos]
 \<open>let
 val ctxt0 = @{context}
 val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0
 val eq' = Thm.symmetric eq
 in
 The function @{ML_ind export in Proof_Context} from the structure
 @{ML_structure Proof_Context} combines both export functions from
 @{ML_structure Variable} and @{ML_structure Assumption}. This can be seen
 in the following example.
-@{ML_matchresult_fake [display, gray]
+@{ML_response [display, gray]
 \<open>let
 val ctxt0 = @{context}
 val ((fvs, [eq]), ctxt1) = ctxt0
 |> Variable.add_fixes ["x", "y"]
 ||>> Assumption.add_assumes [@{cprop "x \<equiv> y"}]
 val eq' = Thm.symmetric eq
 in
 Proof_Context.export ctxt1 ctxt0 [eq']
 end\<close>
-\<open>[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]\<close>}
+\<open>["?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x"]\<close>}
 \<close>
 text \<open>

changeset 572	438703674711
parent 569	f875a25aa72d