34 "----------- fun eval_ist_monom ----------------------------------"; |
34 "----------- fun eval_ist_monom ----------------------------------"; |
35 "----------- fun eval_ist_monom ----------------------------------"; |
35 "----------- fun eval_ist_monom ----------------------------------"; |
36 ist_monom (str2term "12"); |
36 ist_monom (str2term "12"); |
37 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of |
37 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of |
38 SOME ("12 ist_monom = True", _) => () |
38 SOME ("12 ist_monom = True", _) => () |
39 | _ => raise error "polyminus.sml: 12 ist_monom = True"; |
39 | _ => error "polyminus.sml: 12 ist_monom = True"; |
40 |
40 |
41 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of |
41 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of |
42 SOME ("a ist_monom = True", _) => () |
42 SOME ("a ist_monom = True", _) => () |
43 | _ => raise error "polyminus.sml: a ist_monom = True"; |
43 | _ => error "polyminus.sml: a ist_monom = True"; |
44 |
44 |
45 case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of |
45 case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of |
46 SOME ("3 * a ist_monom = True", _) => () |
46 SOME ("3 * a ist_monom = True", _) => () |
47 | _ => raise error "polyminus.sml: 3 * a ist_monom = True"; |
47 | _ => error "polyminus.sml: 3 * a ist_monom = True"; |
48 |
48 |
49 case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of |
49 case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of |
50 SOME ("a ^^^ 2 ist_monom = True", _) => () |
50 SOME ("a ^^^ 2 ist_monom = True", _) => () |
51 | _ => raise error "polyminus.sml: a^^^2 ist_monom = True"; |
51 | _ => error "polyminus.sml: a^^^2 ist_monom = True"; |
52 |
52 |
53 case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of |
53 case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of |
54 SOME ("3 * a ^^^ 2 ist_monom = True", _) => () |
54 SOME ("3 * a ^^^ 2 ist_monom = True", _) => () |
55 | _ => raise error "polyminus.sml: 3*a^^^2 ist_monom = True"; |
55 | _ => error "polyminus.sml: 3*a^^^2 ist_monom = True"; |
56 |
56 |
57 case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of |
57 case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of |
58 SOME ("a * b ist_monom = True", _) => () |
58 SOME ("a * b ist_monom = True", _) => () |
59 | _ => raise error "polyminus.sml: a*b ist_monom = True"; |
59 | _ => error "polyminus.sml: a*b ist_monom = True"; |
60 |
60 |
61 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of |
61 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of |
62 SOME ("3 * a * b ist_monom = True", _) => () |
62 SOME ("3 * a * b ist_monom = True", _) => () |
63 | _ => raise error "polyminus.sml: 3*a*b ist_monom = True"; |
63 | _ => error "polyminus.sml: 3*a*b ist_monom = True"; |
64 |
64 |
65 |
65 |
66 "----------- watch order_add_mult -------------------------------"; |
66 "----------- watch order_add_mult -------------------------------"; |
67 "----------- watch order_add_mult -------------------------------"; |
67 "----------- watch order_add_mult -------------------------------"; |
68 "----------- watch order_add_mult -------------------------------"; |
68 "----------- watch order_add_mult -------------------------------"; |
103 "----- but we do not want the parentheses at right; thus: cond.rew."; |
103 "----- but we do not want the parentheses at right; thus: cond.rew."; |
104 "WN0712707 complicated monomials do not yet work ..."; |
104 "WN0712707 complicated monomials do not yet work ..."; |
105 val t = str2term "((5*a + 4*d) + 3*c) + 2*b"; |
105 val t = str2term "((5*a + 4*d) + 3*c) + 2*b"; |
106 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
106 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
107 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then () |
107 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then () |
108 else raise error "polyminus.sml: order_add_mult changed"; |
108 else error "polyminus.sml: order_add_mult changed"; |
109 |
109 |
110 "----- here we see rew_sub going into subterm with ord.rew...."; |
110 "----- here we see rew_sub going into subterm with ord.rew...."; |
111 val od = ord_make_polynomial false Poly.thy; |
111 val od = ord_make_polynomial false Poly.thy; |
112 val t = str2term "b + a + c + d"; |
112 val t = str2term "b + a + c + d"; |
113 val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t; |
113 val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t; |
128 str2term "aaa"; |
128 str2term "aaa"; |
129 str2term "222 * aaa"; |
129 str2term "222 * aaa"; |
130 (* |
130 (* |
131 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of |
131 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of |
132 SOME ("12 kleiner 9 = False", _) => () |
132 SOME ("12 kleiner 9 = False", _) => () |
133 | _ => raise error "polyminus.sml: 12 kleiner 9 = False"; |
133 | _ => error "polyminus.sml: 12 kleiner 9 = False"; |
134 *) |
134 *) |
135 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of |
135 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of |
136 SOME ("a kleiner b = True", _) => () |
136 SOME ("a kleiner b = True", _) => () |
137 | _ => raise error "polyminus.sml: a kleiner b = True"; |
137 | _ => error "polyminus.sml: a kleiner b = True"; |
138 |
138 |
139 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of |
139 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of |
140 SOME ("10 * g kleiner f = False", _) => () |
140 SOME ("10 * g kleiner f = False", _) => () |
141 | _ => raise error "polyminus.sml: 10 * g kleiner f = False"; |
141 | _ => error "polyminus.sml: 10 * g kleiner f = False"; |
142 |
142 |
143 case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of |
143 case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of |
144 SOME ("a ^^^ 2 kleiner b = True", _) => () |
144 SOME ("a ^^^ 2 kleiner b = True", _) => () |
145 | _ => raise error "polyminus.sml: a ^^^ 2 kleiner b = True"; |
145 | _ => error "polyminus.sml: a ^^^ 2 kleiner b = True"; |
146 |
146 |
147 case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of |
147 case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of |
148 SOME ("3 * a ^^^ 2 kleiner b = True", _) => () |
148 SOME ("3 * a ^^^ 2 kleiner b = True", _) => () |
149 | _ => raise error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True"; |
149 | _ => error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True"; |
150 |
150 |
151 case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of |
151 case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of |
152 SOME ("a * b kleiner c = True", _) => () |
152 SOME ("a * b kleiner c = True", _) => () |
153 | _ => raise error "polyminus.sml: a * b kleiner b = True"; |
153 | _ => error "polyminus.sml: a * b kleiner b = True"; |
154 |
154 |
155 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of |
155 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of |
156 SOME ("3 * a * b kleiner c = True", _) => () |
156 SOME ("3 * a * b kleiner c = True", _) => () |
157 | _ => raise error "polyminus.sml: 3 * a * b kleiner b = True"; |
157 | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; |
158 |
158 |
159 |
159 |
160 |
160 |
161 "----- compare tausche_plus with real_num_collect"; |
161 "----- compare tausche_plus with real_num_collect"; |
162 val od = dummy_ord; |
162 val od = dummy_ord; |
163 |
163 |
164 val erls = erls_ordne_alphabetisch; |
164 val erls = erls_ordne_alphabetisch; |
165 val t = str2term "b + a"; |
165 val t = str2term "b + a"; |
166 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
166 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
167 if term2str t = "a + b" then () |
167 if term2str t = "a + b" then () |
168 else raise error "polyminus.sml: ordne_alphabetisch1 b + a"; |
168 else error "polyminus.sml: ordne_alphabetisch1 b + a"; |
169 |
169 |
170 val erls = Atools_erls; |
170 val erls = Atools_erls; |
171 val t = str2term "2*a + 3*a"; |
171 val t = str2term "2*a + 3*a"; |
172 val SOME (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t; |
172 val SOME (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t; |
173 |
173 |
175 trace_rewrite:=true; |
175 trace_rewrite:=true; |
176 val erls = erls_ordne_alphabetisch; |
176 val erls = erls_ordne_alphabetisch; |
177 val t = str2term "b + a"; |
177 val t = str2term "b + a"; |
178 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
178 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
179 if term2str t = "a + b" then () |
179 if term2str t = "a + b" then () |
180 else raise error "polyminus.sml: ordne_alphabetisch a + b"; |
180 else error "polyminus.sml: ordne_alphabetisch a + b"; |
181 |
181 |
182 val t = str2term "2*b + a"; |
182 val t = str2term "2*b + a"; |
183 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
183 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
184 if term2str t = "a + 2 * b" then () |
184 if term2str t = "a + 2 * b" then () |
185 else raise error "polyminus.sml: ordne_alphabetisch a + 2 * b"; |
185 else error "polyminus.sml: ordne_alphabetisch a + 2 * b"; |
186 |
186 |
187 val t = str2term "a + c + b"; |
187 val t = str2term "a + c + b"; |
188 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
188 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
189 if term2str t = "a + b + c" then () |
189 if term2str t = "a + b + c" then () |
190 else raise error "polyminus.sml: ordne_alphabetisch a + b + c"; |
190 else error "polyminus.sml: ordne_alphabetisch a + b + c"; |
191 |
191 |
192 "----- rewrite goes into subterms"; |
192 "----- rewrite goes into subterms"; |
193 val t = str2term "a + c + b + d"; |
193 val t = str2term "a + c + b + d"; |
194 val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t; |
194 val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t; |
195 if term2str t = "a + b + c + d" then () |
195 if term2str t = "a + b + c + d" then () |
196 else raise error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; |
196 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; |
197 |
197 |
198 val t = str2term "a + c + d + b"; |
198 val t = str2term "a + c + d + b"; |
199 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
199 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
200 if term2str t = "a + b + c + d" then () |
200 if term2str t = "a + b + c + d" then () |
201 else raise error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; |
201 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; |
202 |
202 |
203 "----- here we see rew_sub going into subterm with cond.rew...."; |
203 "----- here we see rew_sub going into subterm with cond.rew...."; |
204 val t = str2term "b + a + c + d"; |
204 val t = str2term "b + a + c + d"; |
205 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
205 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
206 if term2str t = "a + b + c + d" then () |
206 if term2str t = "a + b + c + d" then () |
207 else raise error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; |
207 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; |
208 |
208 |
209 "----- compile rls for the most complicated terms"; |
209 "----- compile rls for the most complicated terms"; |
210 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
210 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
211 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; |
211 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; |
212 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; |
212 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; |
213 if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" |
213 if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" |
214 then () else raise error "polyminus.sml: ordne_alphabetisch finished"; |
214 then () else error "polyminus.sml: ordne_alphabetisch finished"; |
215 |
215 |
216 |
216 |
217 "----------- build fasse_zusammen --------------------------------"; |
217 "----------- build fasse_zusammen --------------------------------"; |
218 "----------- build fasse_zusammen --------------------------------"; |
218 "----------- build fasse_zusammen --------------------------------"; |
219 "----------- build fasse_zusammen --------------------------------"; |
219 "----------- build fasse_zusammen --------------------------------"; |
220 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; |
220 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; |
221 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t; |
221 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t; |
222 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then () |
222 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then () |
223 else raise error "polyminus.sml: fasse_zusammen finished"; |
223 else error "polyminus.sml: fasse_zusammen finished"; |
224 |
224 |
225 "----------- build verschoenere ----------------------------------"; |
225 "----------- build verschoenere ----------------------------------"; |
226 "----------- build verschoenere ----------------------------------"; |
226 "----------- build verschoenere ----------------------------------"; |
227 "----------- build verschoenere ----------------------------------"; |
227 "----------- build verschoenere ----------------------------------"; |
228 val t = str2term "3 + -2 * e + 2 * f + 2 * g"; |
228 val t = str2term "3 + -2 * e + 2 * f + 2 * g"; |
229 val SOME (t,_) = rewrite_set_ thy false verschoenere t; |
229 val SOME (t,_) = rewrite_set_ thy false verschoenere t; |
230 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then () |
230 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then () |
231 else raise error "polyminus.sml: verschoenere 3 + -2 * e ..."; |
231 else error "polyminus.sml: verschoenere 3 + -2 * e ..."; |
232 |
232 |
233 trace_rewrite:=true; |
233 trace_rewrite:=true; |
234 trace_rewrite:=false; |
234 trace_rewrite:=false; |
235 |
235 |
236 "----------- met simplification for_polynomials with_minus -------"; |
236 "----------- met simplification for_polynomials with_minus -------"; |
347 val ((pt,p),_) = get_calc 1; term2str (get_obj g_res pt (fst p)); |
347 val ((pt,p),_) = get_calc 1; term2str (get_obj g_res pt (fst p)); |
348 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same, |
348 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same, |
349 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*) |
349 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*) |
350 val ((pt,p),_) = get_calc 1; |
350 val ((pt,p),_) = get_calc 1; |
351 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11" |
351 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11" |
352 then () else raise error "polyminus.sml: Probe 11 = 11"; |
352 then () else error "polyminus.sml: Probe 11 = 11"; |
353 show_pt pt; |
353 show_pt pt; |
354 |
354 |
355 |
355 |
356 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
356 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
357 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
357 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |