21 |
21 |
22 |
22 |
23 "----------- inst_bdv --------------------------------------------"; |
23 "----------- inst_bdv --------------------------------------------"; |
24 "----------- inst_bdv --------------------------------------------"; |
24 "----------- inst_bdv --------------------------------------------"; |
25 "----------- inst_bdv --------------------------------------------"; |
25 "----------- inst_bdv --------------------------------------------"; |
26 if string_of_thm (num_str @{d1_isolate_add2) = |
26 if string_of_thm (num_str @{thm d1_isolate_add2}) = |
27 "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then () |
27 "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then () |
28 else raise error "term_G.sml d1_isolate_add2"; |
28 else raise error "term_G.sml d1_isolate_add2"; |
29 val subst = [(str2term "bdv", str2term "x")]; |
29 val subst = [(str2term "bdv", str2term "x")]; |
30 val t = (norm o #prop o rep_thm) (num_str @{d1_isolate_add2); |
30 val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2}); |
31 val t' = inst_bdv subst t; |
31 val t' = inst_bdv subst t; |
32 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then () |
32 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then () |
33 else raise error "term_G.sml inst_bdv 1"; |
33 else raise error "term_G.sml inst_bdv 1"; |
34 |
34 |
35 if string_of_thm (num_str @{separate_bdvs_add) = |
35 if string_of_thm (num_str @{thm separate_bdvs_add}) = |
36 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\ |
36 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\ |
37 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then () |
37 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then () |
38 else raise error "term_G.sml separate_bdvs_add"; |
38 else raise error "term_G.sml separate_bdvs_add"; |
39 val subst = [(str2term"bdv_1",str2term"c"), |
39 val subst = [(str2term"bdv_1",str2term"c"), |
40 (str2term"bdv_2",str2term"c_2"), |
40 (str2term"bdv_2",str2term"c_2"), |
41 (str2term"bdv_3",str2term"c_3"), |
41 (str2term"bdv_3",str2term"c_3"), |
42 (str2term"bdv_4",str2term"c_4")]; |
42 (str2term"bdv_4",str2term"c_4")]; |
43 val t = (norm o #prop o rep_thm) (num_str @{separate_bdvs_add); |
43 val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add}); |
44 val t' = inst_bdv subst t; |
44 val t' = inst_bdv subst t; |
45 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\ |
45 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\ |
46 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then () |
46 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then () |
47 else raise error "term_G.sml inst_bdv 2"; |
47 else raise error "term_G.sml inst_bdv 2"; |
48 |
48 |
84 handle MATCH => ([(* (Term.indexname * Term.typ) *)], |
84 handle MATCH => ([(* (Term.indexname * Term.typ) *)], |
85 [(* (Term.indexname * Term.term) *)]); |
85 [(* (Term.indexname * Term.term) *)]); |
86 Pattern.MATCH; |
86 Pattern.MATCH; |
87 |
87 |
88 (*ML {**) |
88 (*ML {**) |
89 val thy = @{theory Complex_Main}; |
89 val thy = @{theory "Complex_Main"}; |
90 val PARSE = Syntax.read_term_global thy; |
90 val PARSE = Syntax.read_term_global thy; |
91 val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real"); |
91 val (pa, tm) = (PARSE "a + b::real", PARSE "x + 2*z::real"); |
92 "-------"; |
92 "-------"; |
93 val (tye, tme) = |
93 val (tye, tme) = |
94 (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv); |
94 (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv); |
109 (*smltest/IsacKnowledge/polyeq.sml: |
109 (*smltest/IsacKnowledge/polyeq.sml: |
110 Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*) |
110 Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*) |
111 (*smltest/ME/ptyps.sml: |
111 (*smltest/ME/ptyps.sml: |
112 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*) |
112 |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*) |
113 (*ML {**) |
113 (*ML {**) |
114 val thy = @{theory Complex_Main}; |
114 val thy = @{theory "Complex_Main"}; |
115 "----- test 1"; |
115 "----- test 1"; |
116 val pa = Logic.varify @{term "a = (0::real)"}; |
116 val pa = Logic.varify @{term "a = (0::real)"}; |
117 "----- test 1 true"; |
117 "----- test 1 true"; |
118 val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; |
118 val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"}; |
119 if matches thy tm pa then () |
119 if matches thy tm pa then () |