1 (* tests on rewrite orders
2 author Matthias Goldgruber 2003
4 WN0509 do not use this file anymore, since orders require thy:
5 do tests in the smltest/IsacKnowledge/file.sml
6 where file.ML defines the respective order !
8 use"../smltest/IsacKnowledge/termorder.sml";
12 (*MK die ersten Tests*)
13 val substa = [(e_term, (term_of o the o (parse thy)) "a")];
14 val substb = [(e_term, (term_of o the o (parse thy)) "b")];
15 val substx = [(e_term, (term_of o the o (parse thy)) "x")];
17 val x1 = (term_of o the o (parse thy)) "a + b + x";
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";
20 val x4 = (term_of o the o (parse thy)) "x + a + b";
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";
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";
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";
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";
33 ord_make_polynomial_in true thy substx (aa, bb);
36 val aa = (term_of o the o (parse thy)) "-1 * a * x";
37 val bb = (term_of o the o (parse thy)) "x^^^3";
38 ord_make_polynomial_in true thy substa (aa, bb);
39 false; (* => GREATER *)
41 (*und nach dem Re-engineering der Termorders in den 'rulesets'
42 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
43 val bdv= (term_of o the o (parse thy)) "bdv";
44 val x = (term_of o the o (parse thy)) "x";
45 val a = (term_of o the o (parse thy)) "a";
46 val b = (term_of o the o (parse thy)) "b";
48 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
49 if term2str t' = "b + x + a" then ()
50 else raise error "termorder.sml diff.behav ord_make_polynomial_in #11";
53 rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
58 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
59 if term2str t' = "a + b + x" then ()
60 else raise error "termorder.sml diff.behav ord_make_polynomial_in #13";
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';
67 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
70 "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
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";
75 rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp';
77 "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
78 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
79 else raise error "termorder.sml diff.behav ord_make_polynomial_in #15";
81 val ttt' = "(3*x + 5)/18";
82 val ttt = (term_of o the o (parse thy)) ttt';
84 rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
85 if term2str uuu = "(5 + 3 * x) / 18" then ()
86 else raise error "termorder.sml diff.behav ord_make_polynomial_in #16";
89 rewrite_set_ thy false make_polynomial ttt;
90 if term2str uuu = "(5 + 3 * x) / 18" then ()
91 else raise error "termorder.sml diff.behav ord_make_polynomial_in #16";
96 (*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
98 (*Aufgabe zum Einstieg in die Arbeit...*)
99 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
100 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
101 val Some (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
103 "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
105 rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
107 "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
108 (* bei Verwendung von "size_of-term" nach MG :*)
109 (*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
111 (*wir holen 'a' wieder aus der Klammerung heraus...*)
112 val Some (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
114 "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
115 (* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
118 rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
120 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
121 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
122 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
124 (*das rewriting l"asst sich beobachten mit
130 "------15.11.02 --------------------------";
131 val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
132 val bdv = (term_of o the o (parse thy)) "bdv";
133 val a = (term_of o the o (parse thy)) "a";
136 (* Anwenden einer Regelmenge aus Termorder.ML: *)
138 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
141 rewrite_set_ thy false discard_parentheses t;
145 val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
147 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
150 rewrite_set_ thy false discard_parentheses t;
152 "1 + (x + b * x) * a + a ^^^ 2";
154 val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
156 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
159 rewrite_set_ thy false discard_parentheses t;
161 "1 + b * a + (7 + x) * a ^^^ 2";
164 Atools.thy grundlegende Algebra
168 RootRat.thy Wurzen + Br"uche
169 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
172 remove_thy"Termorder";
175 get_thm Termorder.thy "bdv_n_collect";
176 get_thm Isac.thy "bdv_n_collect";
179 val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
181 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
184 rewrite_set_ thy false discard_parentheses t;
188 val t = (term_of o the o (parse Termorder.thy)) "Pi";
190 val t = (term_of o the o (parseold thy)) "7";
192 ----------------------------------------------------------------------*)