19 "----------- inst_bdv -----------------------------------"; |
19 "----------- inst_bdv -----------------------------------"; |
20 "----------- inst_bdv -----------------------------------"; |
20 "----------- inst_bdv -----------------------------------"; |
21 "----------- inst_bdv -----------------------------------"; |
21 "----------- inst_bdv -----------------------------------"; |
22 if (term2str o prop_of o num_str) @{thm d1_isolate_add2} = |
22 if (term2str o prop_of o num_str) @{thm d1_isolate_add2} = |
23 "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then () |
23 "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then () |
24 else raise error "termC.sml d1_isolate_add2"; |
24 else error "termC.sml d1_isolate_add2"; |
25 val subst = [(str2term "bdv", str2term "x")]; |
25 val subst = [(str2term "bdv", str2term "x")]; |
26 val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2}); |
26 val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2}); |
27 val t' = inst_bdv subst t; |
27 val t' = inst_bdv subst t; |
28 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then () |
28 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then () |
29 else raise error "termC.sml inst_bdv 1"; |
29 else error "termC.sml inst_bdv 1"; |
30 |
30 |
31 if string_of_thm (num_str @{thm separate_bdvs_add}) = |
31 if string_of_thm (num_str @{thm separate_bdvs_add}) = |
32 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\ |
32 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\ |
33 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then () |
33 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then () |
34 else raise error "termC.sml separate_bdvs_add"; |
34 else error "termC.sml separate_bdvs_add"; |
35 val subst = [(str2term"bdv_1",str2term"c"), |
35 val subst = [(str2term"bdv_1",str2term"c"), |
36 (str2term"bdv_2",str2term"c_2"), |
36 (str2term"bdv_2",str2term"c_2"), |
37 (str2term"bdv_3",str2term"c_3"), |
37 (str2term"bdv_3",str2term"c_3"), |
38 (str2term"bdv_4",str2term"c_4")]; |
38 (str2term"bdv_4",str2term"c_4")]; |
39 val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add}); |
39 val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add}); |
40 val t' = inst_bdv subst t; |
40 val t' = inst_bdv subst t; |
41 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\ |
41 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\ |
42 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then () |
42 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then () |
43 else raise error "termC.sml inst_bdv 2"; |
43 else error "termC.sml inst_bdv 2"; |
44 |
44 |
45 |
45 |
46 "----------- subst_atomic_all ---------------------------"; |
46 "----------- subst_atomic_all ---------------------------"; |
47 "----------- subst_atomic_all ---------------------------"; |
47 "----------- subst_atomic_all ---------------------------"; |
48 "----------- subst_atomic_all ---------------------------"; |
48 "----------- subst_atomic_all ---------------------------"; |
50 val env = [(str2term"vs_::real list",str2term"[c, c_2]"), |
50 val env = [(str2term"vs_::real list",str2term"[c, c_2]"), |
51 (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")]; |
51 (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")]; |
52 val (all_Free_subst, t') = subst_atomic_all env t; |
52 val (all_Free_subst, t') = subst_atomic_all env t; |
53 if all_Free_subst andalso |
53 if all_Free_subst andalso |
54 term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then () |
54 term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then () |
55 else raise error "termC.sml subst_atomic_all should be 'true'"; |
55 else error "termC.sml subst_atomic_all should be 'true'"; |
56 |
56 |
57 |
57 |
58 val (all_Free_subst, t') = subst_atomic_all (tl env) t; |
58 val (all_Free_subst, t') = subst_atomic_all (tl env) t; |
59 if not all_Free_subst andalso |
59 if not all_Free_subst andalso |
60 term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then () |
60 term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then () |
61 else raise error "termC.sml subst_atomic_all should be 'false'"; |
61 else error "termC.sml subst_atomic_all should be 'false'"; |
62 ===== inhibit exn ============================================================*) |
62 ===== inhibit exn ============================================================*) |
63 |
63 |
64 |
64 |
65 "----------- Pattern.match ------------------------------"; |
65 "----------- Pattern.match ------------------------------"; |
66 "----------- Pattern.match ------------------------------"; |
66 "----------- Pattern.match ------------------------------"; |