1 (* testexamples for Poly, polynomials
2 author: Matthias Goldgruber 2003
3 (c) due to copyright terms
5 use"../smltest/IsacKnowledge/poly.sml";
7 ****************************************************************.*)
9 (******************************************************************
10 WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
11 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
12 *******************************************************************)
13 "-----------------------------------------------------------------";
14 "table of contents -----------------------------------------------";
15 "-----------------------------------------------------------------";
16 "-------- build Script Expand_binoms -----------------------------";
17 "-------- investigate new uniary minus ---------------------------";
18 "-------- Bsple aus Schalk I -------------------------------------";
19 "-------- Script 'simplification for_polynomials' ----------------";
20 "-------- check pbl 'polynomial simplification' -----------------";
21 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
22 "-------- norm_Poly NOT COMPLETE ---------------------------------";
23 "-------- ord_make_polynomial ------------------------------------";
24 "-----------------------------------------------------------------";
25 "-----------------------------------------------------------------";
26 "-----------------------------------------------------------------";
29 "-------- build Script Expand_binoms -----------------------------";
30 "-------- build Script Expand_binoms -----------------------------";
31 "-------- build Script Expand_binoms -----------------------------";
32 val scr_expand_binoms =
33 "Script Expand_binoms t_t =" ^
35 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
36 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
37 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
38 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
39 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
40 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
42 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
43 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
44 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
46 " (Try (Repeat (Calculate PLUS ))) @@ " ^
47 " (Try (Repeat (Calculate TIMES ))) @@ " ^
48 " (Try (Repeat (Calculate POWER))) @@ " ^
50 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
51 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
52 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
53 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
55 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
56 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
58 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
59 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
61 " (Try (Repeat (Calculate PLUS ))) @@ " ^
62 " (Try (Repeat (Calculate TIMES ))) @@ " ^
63 " (Try (Repeat (Calculate POWER)))) " ^
65 val scr_expand_binoms =
66 "Script Expand_binoms t_t = t_t";
68 val ---------------------------------------------- = "11111";
69 parse thy scr_expand_binoms;
70 val ---------------------------------------------- = "22222";
71 (*----------------------------------------------
73 "-------- investigate new uniary minus ---------------------------";
74 "-------- investigate new uniary minus ---------------------------";
75 "-------- investigate new uniary minus ---------------------------";
76 val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
79 *** Const ( Trueprop, bool => prop)
80 *** . Const ( op =, [real, real] => bool)
81 *** . . Const ( op -, [real, real] => real)
82 *** . . . Const ( 0, real)
83 *** . . . Var ((x, 0), real)
84 *** . . Const ( uminus, real => real)
85 *** . . . Var ((x, 0), real) *)
87 val t = (term_of o the o (parse thy)) "-1";
90 *** Free ( -1, real) *)
91 val t = (term_of o the o (parse thy)) "- 1";
94 *** Const ( uminus, real => real)
95 *** . Free ( 1, real) *)
97 val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
100 *** Free ( -x, real)*)
101 val t = (term_of o the o (parse thy)) "- x";
104 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
105 val t = (term_of o the o (parse thy)) "-(x)";
108 *** Free ( -x, real)*)
111 "-------- Bsple aus Schalk I -------------------------------------";
112 "-------- Bsple aus Schalk I -------------------------------------";
113 "-------- Bsple aus Schalk I -------------------------------------";
114 (*SPB Schalk I p.63 No.267b*)
116 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
117 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
119 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
121 else raise error "poly.sml: diff.behav. in make_polynomial 1";
123 (*SPB Schalk I p.63 No.275b*)
125 "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
126 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
129 "3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
130 \4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
132 else raise error "poly.sml: diff.behav. in make_polynomial 2";
134 (*SPB Schalk I p.63 No.279b*)
136 "(x-a)*(x-b)*(x-c)*(x-d)";
137 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
141 "a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4"
143 else raise error "poly.sml: diff.behav. in make_polynomial 3";
145 (*SPB Schalk I p.63 No.291*)
147 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
148 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
151 "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
153 else raise error "poly.sml: diff.behav. in make_polynomial 4";
155 (*SPB Schalk I p.64 No.295c*)
157 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
158 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
161 "169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
162 \ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
164 else raise error "poly.sml: diff.behav. in make_polynomial 5";
166 (*SPB Schalk I p.64 No.299a*)
169 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
172 "x ^^^ 2 + -1 * y ^^^ 2"
174 else raise error "poly.sml: diff.behav. in make_polynomial 6";
176 (*SPB Schalk I p.64 No.300c*)
178 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
179 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
182 "-1 + 9 * x ^^^ 4 * y ^^^ 2"
184 else raise error "poly.sml: diff.behav. in make_polynomial 7";
186 (*SPB Schalk I p.64 No.302*)
188 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
189 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
190 if term2str t = "0" then ()
191 else raise error "poly.sml: diff.behav. in make_polynomial 8";
192 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
195 (*SPB Schalk I p.64 No.306a*)
196 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
197 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
198 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
199 else raise error "poly.sml: diff.behav. in make_polynomial: not confluent \
200 \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";
203 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
204 the above resulted in the term below ... but reduces from then correctly*)
205 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
206 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
207 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
208 else raise error "poly.sml: diff.behav. in make_polynomial 9b";
210 (*SPB Schalk I p.64 No.296a*)
211 val t = str2term "(x - a)^^^3";
212 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
213 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
214 then () else raise error "poly.sml: diff.behav. in make_polynomial 10";
216 (*SPB Schalk I p.64 No.296c*)
217 val t = str2term "(-3*x - 4*y)^^^3";
218 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
220 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
221 then () else raise error "poly.sml: diff.behav. in make_polynomial 11";
223 (*SPB Schalk I p.62 No.242c*)
224 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
225 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
226 if (term2str t) = "1" then ()
227 else raise error "poly.sml: diff.behav. in make_polynomial 12";
229 (*SPB Schalk I p.60 No.209a*)
230 val t = str2term "a^^^(7-x) * a^^^x";
231 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
232 if term2str t = "a ^^^ 7" then ()
233 else raise error "poly.sml: diff.behav. in make_polynomial 13";
235 (*SPB Schalk I p.60 No.209d*)
236 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
237 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
238 if term2str t = "d ^^^ 3" then ()
239 else raise error "poly.sml: diff.behav. in make_polynomial 14";
242 (*---------------------------------------------------------------------*)
243 (*------------------ Bsple bei denen es Probleme gibt------------------*)
244 (*---------------------------------------------------------------------*)
246 (*Schalk I p.64 No.303*)
247 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
248 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
249 if term2str t = "1280 * b ^^^ 4" then ()
250 else raise error "poly.sml: diff.behav. in make_polynomial 14b";
251 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
254 (*--------------------------------------------------------------------*)
255 (*----------------------- Eigene Beispiele ---------------------------*)
256 (*--------------------------------------------------------------------*)
258 val t = str2term "a^^^2*a^^^(-2)";
259 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
260 if term2str t = "1" then ()
261 else raise error "poly.sml: diff.behav. in make_polynomial 15";
263 val t = str2term "a + a + a";
264 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
265 if term2str t = "3 * a" then ()
266 else raise error "poly.sml: diff.behav. in make_polynomial 16";
268 val t = str2term "a + b + b + b";
269 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
270 if term2str t = "a + 3 * b" then ()
271 else raise error "poly.sml: diff.behav. in make_polynomial 17";
273 val t = str2term "a^^^2*b*b^^^(-1)";
274 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
275 if term2str t = "a ^^^ 2" then ()
276 else raise error "poly.sml: diff.behav. in make_polynomial 18";
278 val t = str2term "a^^^2*a^^^(-2)";
279 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
280 if (term2str t) = "1" then ()
281 else raise error "poly.sml: diff.behav. in make_polynomial 19";
283 val t = str2term "b + a - b";
284 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
285 if (term2str t) = "a" then ()
286 else raise error "poly.sml: diff.behav. in make_polynomial 20";
288 val t = str2term "b * a * a";
289 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
290 if term2str t = "a ^^^ 2 * b" then ()
291 else raise error "poly.sml: diff.behav. in make_polynomial 21";
293 val t = str2term "(a^^^2)^^^3";
294 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
295 if term2str t = "a ^^^ 6" then ()
296 else raise error "poly.sml: diff.behav. in make_polynomial 22";
298 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
299 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
300 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
301 else raise error "poly.sml: diff.behav. in make_polynomial 23";
303 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
304 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
305 if (term2str t) = "a ^^^ 4" then ()
306 else raise error "poly.sml: diff.behav. in make_polynomial 24";
308 val t = str2term "a * b * b^^^(-1) + a";
309 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
310 if (term2str t) = "2 * a" then ()
311 else raise error "poly.sml: diff.behav. in make_polynomial 25";
313 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
314 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
315 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
316 then () else raise error "poly.sml: diff.behav. in make_polynomial 26";
319 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
321 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
322 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
324 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
325 then () else raise error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
326 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
327 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
329 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
330 then () else raise error "poly.sml: diff.behav. in make_polynomial 28";
332 "-------- Script 'simplification for_polynomials' ----------------";
333 "-------- Script 'simplification for_polynomials' ----------------";
334 "-------- Script 'simplification for_polynomials' ----------------";
336 "Script SimplifyScript (t_::real) = \
337 \ ((Rewrite_Set norm_Poly False) t_)";
338 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
342 "-------- check pbl 'polynomial simplification' -----------------";
343 "-------- check pbl 'polynomial simplification' -----------------";
344 "-------- check pbl 'polynomial simplification' -----------------";
345 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
346 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
349 case refine fmz ["polynomial","simplification"]of
350 [Matches (["polynomial", "simplification"], _)] => ()
351 | _ => raise error "poly.sml diff.behav. in check pbl, refine";
352 (*...if there is an error, then ...*)
356 val pbt = get_pbt ["polynomial","simplification"];
359 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
360 ... then trace_rewrite:*)
365 trace_rewrite:=false;
366 (*... if there is no rewrite, then there is something wrong with prls*)
370 val prls = (#prls o get_pbt) ["polynomial","simplification"];
372 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) \
373 \- (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
375 val SOME (t',_) = rewrite_set_ thy false prls t;
376 trace_rewrite:=false;
377 if t' = HOLogic.true_const then ()
378 else raise error "poly.sml: diff.behav. in check pbl 'polynomial..";
379 (*... if this works, but (*1*) does still NOT work, check types:*)
384 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
385 val wh = [False "(t_::real => real) (is_polyexp::real)"]
386 ......................^^^^^^^^^^^^...............^^^^*)
387 val Matches' _ = match_pbl fmz pbt;
391 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
392 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
393 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
394 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
395 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
398 ("Poly",["polynomial","simplification"],
399 ["simplification","for_polynomials"]);
400 val p = e_pos'; val c = [];
401 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
402 val (p,_,f,nxt,_,pt) = me nxt p c pt;
403 val (p,_,f,nxt,_,pt) = me nxt p c pt;
404 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
405 val (p,_,f,nxt,_,pt) = me nxt p c pt;
406 val (p,_,f,nxt,_,pt) = me nxt p c pt;
407 val (p,_,f,nxt,_,pt) = me nxt p c pt;
408 val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
410 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
411 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
413 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
414 then () else raise error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
417 "-------- interSteps for Schalk 299a -----------------------------";
418 "-------- interSteps for Schalk 299a -----------------------------";
419 "-------- interSteps for Schalk 299a -----------------------------";
422 [(["TERM ((x - y)*(x + y))", "normalform N"],
423 ("Poly",["polynomial","simplification"],
424 ["simplification","for_polynomials"]))];
427 autoCalculate 1 CompleteCalc;
428 val ((pt,p),_) = get_calc 1; show_pt pt;
430 interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
431 val ((pt,p),_) = get_calc 1; show_pt pt;
432 if existpt' ([1,1], Frm) pt then ()
433 else raise error "poly.sml: interSteps doesnt work again 1";
435 interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
436 val ((pt,p),_) = get_calc 1; show_pt pt;
437 if existpt' ([1,1,1], Frm) pt then ()
438 else raise error "poly.sml: interSteps doesnt work again 2";
441 "-------- norm_Poly NOT COMPLETE ---------------------------------";
442 "-------- norm_Poly NOT COMPLETE ---------------------------------";
443 "-------- norm_Poly NOT COMPLETE ---------------------------------";
445 val SOME (f',_) = rewrite_set_ thy false norm_Poly
446 (str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben")(*see poly.sml: -- norm_Poly NOT COMPLETE -- TODO MG*);
447 trace_rewrite:=false;
450 "-------- ord_make_polynomial ------------------------------------";
451 "-------- ord_make_polynomial ------------------------------------";
452 "-------- ord_make_polynomial ------------------------------------";
453 val t1 = str2term "2 * b + (3 * a + 3 * b)";
454 val t2 = str2term "3 * a + 3 * b + 2 * b";
456 if ord_make_polynomial true Poly.thy [] (t1, t2) then ()
457 else raise error "poly.sml: diff.behav. in ord_make_polynomial";
459 (*WN071202: ^^^ why then is there no rewriting ...*)
460 val term = str2term "2*b + (3*a + 3*b)";
461 val NONE = rewrite_set_ Isac.thy false order_add_mult term;
463 (*or why is there no rewriting this way...*)
464 val t1 = str2term "2 * b + (3 * a + 3 * b)";
465 val t2 = str2term "3 * a + (2 * b + 3 * b)";
468 ----------------------------------------------*)