18 val x2 = (term_of o the o (parse thy)) "a + x + b"; |
18 val x2 = (term_of o the o (parse thy)) "a + x + b"; |
19 val x3 = (term_of o the o (parse thy)) "a + x + b"; |
19 val x3 = (term_of o the o (parse thy)) "a + x + b"; |
20 val x4 = (term_of o the o (parse thy)) "x + a + b"; |
20 val x4 = (term_of o the o (parse thy)) "x + a + b"; |
21 |
21 |
22 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () |
22 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () |
23 else raise error "termorder.sml diff.behav ord_make_polynomial_in #1"; |
23 else error "termorder.sml diff.behav ord_make_polynomial_in #1"; |
24 |
24 |
25 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () |
25 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () |
26 else raise error "termorder.sml diff.behav ord_make_polynomial_in #2"; |
26 else error "termorder.sml diff.behav ord_make_polynomial_in #2"; |
27 |
27 |
28 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () |
28 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () |
29 else raise error "termorder.sml diff.behav ord_make_polynomial_in #3"; |
29 else error "termorder.sml diff.behav ord_make_polynomial_in #3"; |
30 |
30 |
31 val aa = (term_of o the o (parse thy)) "-1 * a * x"; |
31 val aa = (term_of o the o (parse thy)) "-1 * a * x"; |
32 val bb = (term_of o the o (parse thy)) "x^^^3"; |
32 val bb = (term_of o the o (parse thy)) "x^^^3"; |
33 ord_make_polynomial_in true thy substx (aa, bb); |
33 ord_make_polynomial_in true thy substx (aa, bb); |
34 true; (* => LESS *) |
34 true; (* => LESS *) |
45 val a = (term_of o the o (parse thy)) "a"; |
45 val a = (term_of o the o (parse thy)) "a"; |
46 val b = (term_of o the o (parse thy)) "b"; |
46 val b = (term_of o the o (parse thy)) "b"; |
47 val SOME (t',_) = |
47 val SOME (t',_) = |
48 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; |
48 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; |
49 if term2str t' = "b + x + a" then () |
49 if term2str t' = "b + x + a" then () |
50 else raise error "termorder.sml diff.behav ord_make_polynomial_in #11"; |
50 else error "termorder.sml diff.behav ord_make_polynomial_in #11"; |
51 |
51 |
52 val NONE = |
52 val NONE = |
53 rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; |
53 rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; |
54 term2str t'; |
54 term2str t'; |
55 "a + x + b"; |
55 "a + x + b"; |
56 |
56 |
57 val SOME (t',_) = |
57 val SOME (t',_) = |
58 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; |
58 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; |
59 if term2str t' = "a + b + x" then () |
59 if term2str t' = "a + b + x" then () |
60 else raise error "termorder.sml diff.behav ord_make_polynomial_in #13"; |
60 else error "termorder.sml diff.behav ord_make_polynomial_in #13"; |
61 |
61 |
62 |
62 |
63 |
63 |
64 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2"; |
64 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2"; |
65 val ppp = (term_of o the o (parse thy)) ppp'; |
65 val ppp = (term_of o the o (parse thy)) ppp'; |
67 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; |
67 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; |
68 (*MG 2003... |
68 (*MG 2003... |
69 term2str t'; |
69 term2str t'; |
70 "(-6) + (-5 * x + (-15 * x ^^^ 2))";*) |
70 "(-6) + (-5 * x + (-15 * x ^^^ 2))";*) |
71 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
71 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
72 else raise error "termorder.sml diff.behav ord_make_polynomial_in #14"; |
72 else error "termorder.sml diff.behav ord_make_polynomial_in #14"; |
73 |
73 |
74 val SOME (t',_) = |
74 val SOME (t',_) = |
75 rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp'; |
75 rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp'; |
76 (*MG 2003... |
76 (*MG 2003... |
77 "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) |
77 "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) |
78 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
78 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
79 else raise error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
79 else error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
80 |
80 |
81 val ttt' = "(3*x + 5)/18"; |
81 val ttt' = "(3*x + 5)/18"; |
82 val ttt = (term_of o the o (parse thy)) ttt'; |
82 val ttt = (term_of o the o (parse thy)) ttt'; |
83 val SOME (uuu,_) = |
83 val SOME (uuu,_) = |
84 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; |
84 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; |
85 if term2str uuu = "(5 + 3 * x) / 18" then () |
85 if term2str uuu = "(5 + 3 * x) / 18" then () |
86 else raise error "termorder.sml diff.behav ord_make_polynomial_in #16"; |
86 else error "termorder.sml diff.behav ord_make_polynomial_in #16"; |
87 |
87 |
88 val SOME (uuu,_) = |
88 val SOME (uuu,_) = |
89 rewrite_set_ thy false make_polynomial ttt; |
89 rewrite_set_ thy false make_polynomial ttt; |
90 if term2str uuu = "(5 + 3 * x) / 18" then () |
90 if term2str uuu = "(5 + 3 * x) / 18" then () |
91 else raise error "termorder.sml diff.behav ord_make_polynomial_in #16"; |
91 else error "termorder.sml diff.behav ord_make_polynomial_in #16"; |
92 |
92 |
93 |
93 |
94 |
94 |
95 |
95 |
96 (*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML |
96 (*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML |