neuper@37906
|
1 |
(* tests on rewrite orders
|
neuper@37906
|
2 |
author Matthias Goldgruber 2003
|
neuper@37906
|
3 |
|
neuper@37906
|
4 |
WN0509 do not use this file anymore, since orders require thy:
|
neuper@37906
|
5 |
do tests in the smltest/IsacKnowledge/file.sml
|
neuper@37906
|
6 |
where file.ML defines the respective order !
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
use"../smltest/IsacKnowledge/termorder.sml";
|
neuper@37906
|
9 |
*)
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
(*MK die ersten Tests*)
|
neuper@37906
|
13 |
val substa = [(e_term, (term_of o the o (parse thy)) "a")];
|
neuper@37906
|
14 |
val substb = [(e_term, (term_of o the o (parse thy)) "b")];
|
neuper@37906
|
15 |
val substx = [(e_term, (term_of o the o (parse thy)) "x")];
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
val x1 = (term_of o the o (parse thy)) "a + b + x";
|
neuper@37906
|
18 |
val x2 = (term_of o the o (parse thy)) "a + x + b";
|
neuper@37906
|
19 |
val x3 = (term_of o the o (parse thy)) "a + x + b";
|
neuper@37906
|
20 |
val x4 = (term_of o the o (parse thy)) "x + a + b";
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
|
neuper@37906
|
23 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #1";
|
neuper@37906
|
24 |
|
neuper@37906
|
25 |
if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
|
neuper@37906
|
26 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #2";
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
|
neuper@37906
|
29 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #3";
|
neuper@37906
|
30 |
|
neuper@37906
|
31 |
val aa = (term_of o the o (parse thy)) "-1 * a * x";
|
neuper@37906
|
32 |
val bb = (term_of o the o (parse thy)) "x^^^3";
|
neuper@37906
|
33 |
ord_make_polynomial_in true thy substx (aa, bb);
|
neuper@37906
|
34 |
true; (* => LESS *)
|
neuper@37906
|
35 |
|
neuper@37906
|
36 |
val aa = (term_of o the o (parse thy)) "-1 * a * x";
|
neuper@37906
|
37 |
val bb = (term_of o the o (parse thy)) "x^^^3";
|
neuper@37906
|
38 |
ord_make_polynomial_in true thy substa (aa, bb);
|
neuper@37906
|
39 |
false; (* => GREATER *)
|
neuper@37906
|
40 |
|
neuper@37906
|
41 |
(*und nach dem Re-engineering der Termorders in den 'rulesets'
|
neuper@37906
|
42 |
kannst Du die 'gr"osste' Variable frei w"ahlen: *)
|
neuper@37906
|
43 |
val bdv= (term_of o the o (parse thy)) "bdv";
|
neuper@37906
|
44 |
val x = (term_of o the o (parse thy)) "x";
|
neuper@37906
|
45 |
val a = (term_of o the o (parse thy)) "a";
|
neuper@37906
|
46 |
val b = (term_of o the o (parse thy)) "b";
|
neuper@37926
|
47 |
val SOME (t',_) =
|
neuper@37906
|
48 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
|
neuper@37906
|
49 |
if term2str t' = "b + x + a" then ()
|
neuper@37906
|
50 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #11";
|
neuper@37906
|
51 |
|
neuper@37926
|
52 |
val NONE =
|
neuper@37906
|
53 |
rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
|
neuper@37906
|
54 |
term2str t';
|
neuper@37906
|
55 |
"a + x + b";
|
neuper@37906
|
56 |
|
neuper@37926
|
57 |
val SOME (t',_) =
|
neuper@37906
|
58 |
rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
|
neuper@37906
|
59 |
if term2str t' = "a + b + x" then ()
|
neuper@37906
|
60 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #13";
|
neuper@37906
|
61 |
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
|
neuper@37906
|
65 |
val ppp = (term_of o the o (parse thy)) ppp';
|
neuper@37926
|
66 |
val SOME (t',_) =
|
neuper@37906
|
67 |
rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
|
neuper@37906
|
68 |
(*MG 2003...
|
neuper@37906
|
69 |
term2str t';
|
neuper@37906
|
70 |
"(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
|
neuper@37906
|
71 |
if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
|
neuper@37906
|
72 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #14";
|
neuper@37906
|
73 |
|
neuper@37926
|
74 |
val SOME (t',_) =
|
neuper@37906
|
75 |
rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp';
|
neuper@37906
|
76 |
(*MG 2003...
|
neuper@37906
|
77 |
"(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
|
neuper@37906
|
78 |
if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
|
neuper@37906
|
79 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #15";
|
neuper@37906
|
80 |
|
neuper@37906
|
81 |
val ttt' = "(3*x + 5)/18";
|
neuper@37906
|
82 |
val ttt = (term_of o the o (parse thy)) ttt';
|
neuper@37926
|
83 |
val SOME (uuu,_) =
|
neuper@37906
|
84 |
rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
|
neuper@37906
|
85 |
if term2str uuu = "(5 + 3 * x) / 18" then ()
|
neuper@37906
|
86 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #16";
|
neuper@37906
|
87 |
|
neuper@37926
|
88 |
val SOME (uuu,_) =
|
neuper@37906
|
89 |
rewrite_set_ thy false make_polynomial ttt;
|
neuper@37906
|
90 |
if term2str uuu = "(5 + 3 * x) / 18" then ()
|
neuper@37906
|
91 |
else raise error "termorder.sml diff.behav ord_make_polynomial_in #16";
|
neuper@37906
|
92 |
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
|
neuper@37906
|
95 |
|
neuper@37906
|
96 |
(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
|
neuper@37906
|
97 |
|
neuper@37906
|
98 |
(*Aufgabe zum Einstieg in die Arbeit...*)
|
neuper@37906
|
99 |
val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
|
neuper@37906
|
100 |
(*ein 'ruleset' aus Poly.ML wird angewandt...*)
|
neuper@37926
|
101 |
val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
|
neuper@37906
|
102 |
term2str t;
|
neuper@37906
|
103 |
"a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
|
neuper@37926
|
104 |
val SOME (t,_) =
|
neuper@37906
|
105 |
rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
|
neuper@37906
|
106 |
term2str t;
|
neuper@37906
|
107 |
"x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
|
neuper@37906
|
108 |
(* bei Verwendung von "size_of-term" nach MG :*)
|
neuper@37906
|
109 |
(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
|
neuper@37906
|
110 |
|
neuper@37906
|
111 |
(*wir holen 'a' wieder aus der Klammerung heraus...*)
|
neuper@37926
|
112 |
val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
|
neuper@37906
|
113 |
term2str t;
|
neuper@37906
|
114 |
"x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
|
neuper@37906
|
115 |
(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
|
neuper@37906
|
116 |
|
neuper@37926
|
117 |
val SOME (t,_) =
|
neuper@37906
|
118 |
rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
|
neuper@37906
|
119 |
term2str t;
|
neuper@37906
|
120 |
"x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
|
neuper@37906
|
121 |
(*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
|
neuper@37906
|
122 |
"x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
|
neuper@37906
|
123 |
|
neuper@37906
|
124 |
(*das rewriting l"asst sich beobachten mit
|
neuper@37906
|
125 |
trace_rewrite:=true;
|
neuper@37906
|
126 |
*)
|
neuper@37906
|
127 |
|
neuper@37906
|
128 |
|
neuper@37906
|
129 |
|
neuper@37906
|
130 |
"------15.11.02 --------------------------";
|
neuper@37906
|
131 |
val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
|
neuper@37906
|
132 |
val bdv = (term_of o the o (parse thy)) "bdv";
|
neuper@37906
|
133 |
val a = (term_of o the o (parse thy)) "a";
|
neuper@37906
|
134 |
|
neuper@37906
|
135 |
trace_rewrite:=true;
|
neuper@37906
|
136 |
(* Anwenden einer Regelmenge aus Termorder.ML: *)
|
neuper@37926
|
137 |
val SOME (t,_) =
|
neuper@37906
|
138 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
neuper@37906
|
139 |
term2str t;
|
neuper@37926
|
140 |
val SOME (t,_) =
|
neuper@37906
|
141 |
rewrite_set_ thy false discard_parentheses t;
|
neuper@37906
|
142 |
term2str t;
|
neuper@37906
|
143 |
"1 + b * x + x * a";
|
neuper@37906
|
144 |
|
neuper@37906
|
145 |
val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
|
neuper@37926
|
146 |
val SOME (t,_) =
|
neuper@37906
|
147 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
neuper@37906
|
148 |
term2str t;
|
neuper@37926
|
149 |
val SOME (t,_) =
|
neuper@37906
|
150 |
rewrite_set_ thy false discard_parentheses t;
|
neuper@37906
|
151 |
term2str t;
|
neuper@37906
|
152 |
"1 + (x + b * x) * a + a ^^^ 2";
|
neuper@37906
|
153 |
|
neuper@37906
|
154 |
val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
|
neuper@37926
|
155 |
val SOME (t,_) =
|
neuper@37906
|
156 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
neuper@37906
|
157 |
term2str t;
|
neuper@37926
|
158 |
val SOME (t,_) =
|
neuper@37906
|
159 |
rewrite_set_ thy false discard_parentheses t;
|
neuper@37906
|
160 |
term2str t;
|
neuper@37906
|
161 |
"1 + b * a + (7 + x) * a ^^^ 2";
|
neuper@37906
|
162 |
|
neuper@37906
|
163 |
(* MG2003
|
neuper@37906
|
164 |
Atools.thy grundlegende Algebra
|
neuper@37906
|
165 |
Poly.thy Polynome
|
neuper@37906
|
166 |
Rational.thy Br"uche
|
neuper@37906
|
167 |
Root.thy Wurzeln
|
neuper@37906
|
168 |
RootRat.thy Wurzen + Br"uche
|
neuper@37906
|
169 |
Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
|
neuper@37906
|
170 |
|
neuper@37906
|
171 |
cd"knowledge";
|
neuper@37906
|
172 |
remove_thy"Termorder";
|
neuper@37906
|
173 |
use_thy"Isac";
|
neuper@37906
|
174 |
|
neuper@37906
|
175 |
get_thm Termorder.thy "bdv_n_collect";
|
neuper@37906
|
176 |
get_thm Isac.thy "bdv_n_collect";
|
neuper@37906
|
177 |
|
neuper@37906
|
178 |
*)
|
neuper@37906
|
179 |
val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
|
neuper@37926
|
180 |
val SOME (t,_) =
|
neuper@37906
|
181 |
rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
|
neuper@37906
|
182 |
term2str t;
|
neuper@37926
|
183 |
val SOME (t,_) =
|
neuper@37906
|
184 |
rewrite_set_ thy false discard_parentheses t;
|
neuper@37906
|
185 |
term2str t;
|
neuper@37906
|
186 |
"(7 + x) * a ^^^ 2";
|
neuper@37906
|
187 |
|
neuper@37906
|
188 |
val t = (term_of o the o (parse Termorder.thy)) "Pi";
|
neuper@37906
|
189 |
|
neuper@37906
|
190 |
val t = (term_of o the o (parseold thy)) "7";
|
neuper@37906
|
191 |
|
neuper@37906
|
192 |
----------------------------------------------------------------------*)
|