1 (* testexamples for Poly, polynomials
2 author: Matthias Goldgruber 2003
3 (c) due to copyright terms
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
8 (*******************************************************************************
9 WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
10 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
11 *******************************************************************************)
12 "--------------------------------------------------------";
13 "--------------------------------------------------------";
14 "table of contents --------------------------------------";
15 "--------------------------------------------------------";
16 "-------- check is'_polyexp is_polyexp ------------------";
17 "-------- build Script Expand_binoms --------------------";
18 "-------- investigate (new) uniary minus ----------------";
19 "-------- check make_polynomial with simple terms -------";
20 "-------- fun is_multUnordered --------------------------";
21 "-------- examples from textbook Schalk I ---------------";
22 "-------- Script 'simplification for_polynomials' -------";
23 "-------- check pbl 'polynomial simplification' --------";
24 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
25 "-------- interSteps for Schalk 299a --------------------";
26 "-------- norm_Poly NOT COMPLETE ------------------------";
27 "-------- ord_make_polynomial ---------------------------";
28 "--------------------------------------------------------";
29 "--------------------------------------------------------";
30 "--------------------------------------------------------";
33 "-------- check is'_polyexp is_polyexp ------------------";
34 "-------- check is'_polyexp is_polyexp ------------------";
35 "-------- check is'_polyexp is_polyexp ------------------";
36 if is_polyexp @{term "x / x"}
37 then error "poly.sml: check is'_polyexp is_polyexp" else ();
40 "-------- build Script Expand_binoms -----------------------------";
41 "-------- build Script Expand_binoms -----------------------------";
42 "-------- build Script Expand_binoms -----------------------------";
43 val scr_expand_binoms =
44 "Script Expand_binoms t_t =" ^
46 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
47 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
48 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
49 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
50 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
51 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
53 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
54 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
55 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
57 " (Try (Repeat (Calculate PLUS ))) @@ " ^
58 " (Try (Repeat (Calculate TIMES ))) @@ " ^
59 " (Try (Repeat (Calculate POWER))) @@ " ^
61 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
62 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
63 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
64 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
66 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
67 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
69 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
70 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
72 " (Try (Repeat (Calculate PLUS ))) @@ " ^
73 " (Try (Repeat (Calculate TIMES ))) @@ " ^
74 " (Try (Repeat (Calculate POWER)))) " ^
77 val scr_expand_binoms =
78 "Script Expand_binoms t_t = t_t";
80 parse thy scr_expand_binoms;
83 "-------- investigate (new) uniary minus ----------------";
84 "-------- investigate (new) uniary minus ----------------";
85 "-------- investigate (new) uniary minus ----------------";
86 val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
89 *** Const ( Trueprop, bool => prop)
90 *** . Const ( op =, [real, real] => bool)
91 *** . . Const ( op -, [real, real] => real)
92 *** . . . Const ( 0, real)
93 *** . . . Var ((x, 0), real)
94 *** . . Const ( uminus, real => real)
95 *** . . . Var ((x, 0), real) *)
97 val t = (term_of o the o (parse thy)) "-1";
100 *** Free ( -1, real) *)
101 val t = (term_of o the o (parse thy)) "- 1";
104 *** Const ( uminus, real => real)
105 *** . Free ( 1, real) *)
107 val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
110 *** Free ( -x, real)*)
111 val t = (term_of o the o (parse thy)) "- x";
114 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
115 val t = (term_of o the o (parse thy)) "-(x)";
118 *** Free ( -x, real)*)
120 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
121 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
123 "-------- check make_polynomial with simple terms -------";
124 "-------- check make_polynomial with simple terms -------";
125 "-------- check make_polynomial with simple terms -------";
127 val t = str2term "2*3*a";
128 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
129 if term2str t = "6 * a" then () else error "check make_polynomial 1";
132 val t = str2term "2*a + 3*a";
133 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
134 if term2str t = "5 * a" then () else error "check make_polynomial 2";
137 val t = str2term "2*a + 3*a + 3*a";
138 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
139 if term2str t = "8 * a" then () else error "check make_polynomial 3";
142 val t = str2term "3*a - 2*a";
143 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
144 if term2str t = "a" then () else error "check make_polynomial 4";
147 val t = str2term "4*(3*a - 2*a)";
148 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
149 if term2str t = "4 * a" then () else error "check make_polynomial 5";
152 val t = str2term "4*(3*a^^^2 - 2*a^^^2)";
153 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
154 if term2str t = "4 * a ^^^ 2" then () else error "check make_polynomial 6";
157 "-------- fun is_multUnordered --------------------------";
158 "-------- fun is_multUnordered --------------------------";
159 "-------- fun is_multUnordered --------------------------";
160 val thy = theory "Isac";
161 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
162 val t = str2term "x^^^2 * x";
163 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
164 if term2str t' = "x * x ^^^ 2" then ()
165 else error "poly.sml Poly.is'_multUnordered doesn't work";
167 (* 100928 trace_rewrite shows the first occurring difference in 267b:
168 ### rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
170 ###### rls: e_rls-is_multUnordered on: p is_multUnordered
171 ####### try calc: Poly.is'_multUnordered'
172 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
174 val t = str2term "5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))";
176 "----- is_multUnordered ---";
177 val tsort = sort_variables t;
178 term2str tsort = "2 * (5 * (x ^^^ 2 * x ^^^ 7)) + 3 * (5 * x ^^^ 2) + 6 * x ^^^ 7 + 9 +\n-1 * (3 * (6 * (x ^^^ 4 * x ^^^ 5))) +\n-1 * (-1 * (3 * x ^^^ 5)) +\n-48 * x ^^^ 4 +\n8";
181 is_polyexp t andalso not (t = sort_variables t);
182 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
184 "----- eval_is_multUnordered ---";
185 val tm = str2term "(5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))) is_multUnordered";
186 case eval_is_multUnordered "testid" "" tm thy of
187 SOME (_, Const ("Trueprop", _) $
189 (Const ("Poly.is'_multUnordered", _) $ _) $
190 Const ("True", _))) => ()
191 | _ => error "poly.sml diff. eval_is_multUnordered";
193 "----- rewrite_set_ STILL DIDN'T WORK";
194 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
198 "-------- examples from textbook Schalk I ---------------";
199 "-------- examples from textbook Schalk I ---------------";
200 "-------- examples from textbook Schalk I ---------------";
201 "-----SPB Schalk I p.63 No.267b ---";
202 trace_rewrite := true; tracing "-----SPB Schalk I p.63 No.267b ---begin";
204 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
205 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
207 trace_rewrite := false; tracing "-----SPB Schalk I p.63 No.267b ---end";
209 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
211 else error "poly.sml: diff.behav. in make_polynomial 1";
213 "-----SPB Schalk I p.63 No.275b ---";
215 "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
216 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
219 "3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
220 \4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
222 else error "poly.sml: diff.behav. in make_polynomial 2";
224 "-----SPB Schalk I p.63 No.279b ---";
226 "(x-a)*(x-b)*(x-c)*(x-d)";
227 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
231 "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"
233 else error "poly.sml: diff.behav. in make_polynomial 3";
235 "-----SPB Schalk I p.63 No.291 ---";
237 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
238 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
241 "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
243 else error "poly.sml: diff.behav. in make_polynomial 4";
245 "-----SPB Schalk I p.64 No.295c ---";
247 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
248 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
251 "169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
252 \ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
254 else error "poly.sml: diff.behav. in make_polynomial 5";
256 "-----SPB Schalk I p.64 No.299a ---";
259 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
262 if (term2str t) = "x ^^^ 2 + -1 * y ^^^ 2" then ()
263 else error "poly.sml: diff.behav. in make_polynomial 6";
266 "-----SPB Schalk I p.64 No.300c ---";
268 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
269 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
272 "-1 + 9 * x ^^^ 4 * y ^^^ 2"
274 else error "poly.sml: diff.behav. in make_polynomial 7";
276 "-----SPB Schalk I p.64 No.302 ---";
278 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
279 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
280 if term2str t = "0" then ()
281 else error "poly.sml: diff.behav. in make_polynomial 8";
282 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
285 "-----SPB Schalk I p.64 No.306a ---";
286 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
287 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
288 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
289 else error "poly.sml: diff.behav. in make_polynomial: not confluent \
290 \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";
293 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
294 the above resulted in the term below ... but reduces from then correctly*)
295 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
296 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
297 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
298 else error "poly.sml: diff.behav. in make_polynomial 9b";
300 "-----SPB Schalk I p.64 No.296a ---";
301 val t = str2term "(x - a)^^^3";
302 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
303 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
304 then () else error "poly.sml: diff.behav. in make_polynomial 10";
306 "-----SPB Schalk I p.64 No.296c ---";
307 val t = str2term "(-3*x - 4*y)^^^3";
308 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
310 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
311 then () else error "poly.sml: diff.behav. in make_polynomial 11";
313 "-----SPB Schalk I p.62 No.242c ---";
314 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
315 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
316 if (term2str t) = "1" then ()
317 else error "poly.sml: diff.behav. in make_polynomial 12";
319 "-----SPB Schalk I p.60 No.209a ---";
320 val t = str2term "a^^^(7-x) * a^^^x";
321 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
322 if term2str t = "a ^^^ 7" then ()
323 else error "poly.sml: diff.behav. in make_polynomial 13";
325 "-----SPB Schalk I p.60 No.209d ---";
326 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
327 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
328 if term2str t = "d ^^^ 3" then ()
329 else error "poly.sml: diff.behav. in make_polynomial 14";
331 (*---------------------------------------------------------------------*)
332 (*------------------ Bsple bei denen es Probleme gibt------------------*)
333 (*---------------------------------------------------------------------*)
335 "-----Schalk I p.64 No.303 ---";
336 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)";
337 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
338 if term2str t = "1280 * b ^^^ 4" then ()
339 else error "poly.sml: diff.behav. in make_polynomial 14b";
340 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
343 (*--------------------------------------------------------------------*)
344 (*----------------------- Eigene Beispiele ---------------------------*)
345 (*--------------------------------------------------------------------*)
347 val t = str2term "a^^^2*a^^^(-2)";
348 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
349 if term2str t = "1" then ()
350 else error "poly.sml: diff.behav. in make_polynomial 15";
352 val t = str2term "a + a + a";
353 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
354 if term2str t = "3 * a" then ()
355 else error "poly.sml: diff.behav. in make_polynomial 16";
357 val t = str2term "a + b + b + b";
358 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
359 if term2str t = "a + 3 * b" then ()
360 else error "poly.sml: diff.behav. in make_polynomial 17";
362 val t = str2term "a^^^2*b*b^^^(-1)";
363 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
364 if term2str t = "a ^^^ 2" then ()
365 else error "poly.sml: diff.behav. in make_polynomial 18";
367 val t = str2term "a^^^2*a^^^(-2)";
368 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
369 if (term2str t) = "1" then ()
370 else error "poly.sml: diff.behav. in make_polynomial 19";
372 val t = str2term "b + a - b";
373 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
374 if (term2str t) = "a" then ()
375 else error "poly.sml: diff.behav. in make_polynomial 20";
377 val t = str2term "b * a * a";
378 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
379 if term2str t = "a ^^^ 2 * b" then ()
380 else error "poly.sml: diff.behav. in make_polynomial 21";
382 val t = str2term "(a^^^2)^^^3";
383 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
384 if term2str t = "a ^^^ 6" then ()
385 else error "poly.sml: diff.behav. in make_polynomial 22";
387 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
388 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
389 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
390 else error "poly.sml: diff.behav. in make_polynomial 23";
392 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
393 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
394 if (term2str t) = "a ^^^ 4" then ()
395 else error "poly.sml: diff.behav. in make_polynomial 24";
397 val t = str2term "a * b * b^^^(-1) + a";
398 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
399 if (term2str t) = "2 * a" then ()
400 else error "poly.sml: diff.behav. in make_polynomial 25";
402 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
403 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
404 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
405 then () else error "poly.sml: diff.behav. in make_polynomial 26";
408 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
410 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
411 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
413 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
414 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
415 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
416 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
418 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
419 then () else error "poly.sml: diff.behav. in make_polynomial 28";
421 "-------- Script 'simplification for_polynomials' -------";
422 "-------- Script 'simplification for_polynomials' -------";
423 "-------- Script 'simplification for_polynomials' -------";
425 "Script SimplifyScript (t_t::real) = \
426 \ ((Rewrite_Set norm_Poly False) t_t)";
427 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
431 "-------- check pbl 'polynomial simplification' --------";
432 "-------- check pbl 'polynomial simplification' --------";
433 "-------- check pbl 'polynomial simplification' --------";
434 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
435 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
438 (*===== inhibit exn ============================================================
441 case refine fmz ["polynomial","simplification"]of
442 [Matches (["polynomial", "simplification"], _)] => ()
443 | _ => error "poly.sml diff.behav. in check pbl, refine";
444 (*...if there is an error, then ...*)
448 val pbt = get_pbt ["polynomial","simplification"];
451 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
452 ... then trace_rewrite:*)
457 trace_rewrite:=false;
458 (*... if there is no rewrite, then there is something wrong with prls*)
462 val prls = (#prls o get_pbt) ["polynomial","simplification"];
464 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) \
465 \- (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
467 val SOME (t',_) = rewrite_set_ thy false prls t;
468 trace_rewrite:=false;
469 if t' = HOLogic.true_const then ()
470 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
471 (*... if this works, but (*1*) does still NOT work, check types:*)
476 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
477 val wh = [False "(t_::real => real) (is_polyexp::real)"]
478 ......................^^^^^^^^^^^^...............^^^^*)
479 val Matches' _ = match_pbl fmz pbt;
483 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
484 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
485 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
486 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
487 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
490 ("Poly",["polynomial","simplification"],
491 ["simplification","for_polynomials"]);
492 val p = e_pos'; val c = [];
493 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
494 val (p,_,f,nxt,_,pt) = me nxt p c pt;
495 val (p,_,f,nxt,_,pt) = me nxt p c pt;
496 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
497 val (p,_,f,nxt,_,pt) = me nxt p c pt;
498 val (p,_,f,nxt,_,pt) = me nxt p c pt;
499 val (p,_,f,nxt,_,pt) = me nxt p c pt;
500 val (p,_,f,nxt,_,pt) = me nxt p c pt;
501 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
502 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
503 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
505 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
506 then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
509 "-------- interSteps for Schalk 299a --------------------";
510 "-------- interSteps for Schalk 299a --------------------";
511 "-------- interSteps for Schalk 299a --------------------";
514 [(["TERM ((x - y)*(x + y))", "normalform N"],
515 ("Poly",["polynomial","simplification"],
516 ["simplification","for_polynomials"]))];
519 autoCalculate 1 CompleteCalc;
520 val ((pt,p),_) = get_calc 1; show_pt pt;
522 interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
523 val ((pt,p),_) = get_calc 1; show_pt pt;
524 if existpt' ([1,1], Frm) pt then ()
525 else error "poly.sml: interSteps doesnt work again 1";
527 interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
528 val ((pt,p),_) = get_calc 1; show_pt pt;
529 if existpt' ([1,1,1], Frm) pt then ()
530 else error "poly.sml: interSteps doesnt work again 2";
533 "-------- norm_Poly NOT COMPLETE ------------------------";
534 "-------- norm_Poly NOT COMPLETE ------------------------";
535 "-------- norm_Poly NOT COMPLETE ------------------------";
537 val SOME (f',_) = rewrite_set_ thy false norm_Poly
538 (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*);
539 trace_rewrite:=false;
543 "-------- ord_make_polynomial ---------------------------";
544 "-------- ord_make_polynomial ---------------------------";
545 "-------- ord_make_polynomial ---------------------------";
546 val t1 = str2term "2 * b + (3 * a + 3 * b)";
547 val t2 = str2term "3 * a + 3 * b + 2 * b";
549 if ord_make_polynomial true Poly.thy [] (t1, t2) then ()
550 else error "poly.sml: diff.behav. in ord_make_polynomial";
552 (*WN071202: ^^^ why then is there no rewriting ...*)
553 val term = str2term "2*b + (3*a + 3*b)";
554 val NONE = rewrite_set_ Isac.thy false order_add_mult term;
556 (*or why is there no rewriting this way...*)
557 val t1 = str2term "2 * b + (3 * a + 3 * b)";
558 val t2 = str2term "3 * a + (2 * b + 3 * b)";
560 ===== inhibit exn ?===========================================================*)
563 (*========== inhibit exn =======================================================
564 ============ inhibit exn =====================================================*)
566 (*========== inhibit exn ?======================================================
567 ============ inhibit exn ?====================================================*)
569 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
570 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)