1 (* testexamples for Poly, polynomials |
1 (* Knowledge/poly.sml |
2 author: Matthias Goldgruber 2003 |
2 author: Matthias Goldgruber 2003 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 |
4 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
6 10 20 30 40 50 60 70 80 |
|
7 LEGEND: |
5 LEGEND: |
8 WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml' |
6 WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml' |
9 examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml' |
7 examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml' |
10 *) |
8 *) |
11 |
9 |
12 "--------------------------------------------------------"; |
10 "-----------------------------------------------------------------------------------------------"; |
13 "--------------------------------------------------------"; |
11 "-----------------------------------------------------------------------------------------------"; |
14 "table of contents --------------------------------------"; |
12 "table of contents -----------------------------------------------------------------------------"; |
15 "--------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------------------------"; |
16 "----------- fun is_polyexp --------------------------------------------------------------------"; |
14 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; |
17 "----------- fun has_degree_in -----------------------------------------------------------------"; |
15 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; |
18 "----------- fun mono_deg_in -------------------------------------------------------------------"; |
16 "-------- fun is_polyexp -----------------------------------------------------------------------"; |
19 "----------- fun mono_deg_in -------------------------------------------------------------------"; |
17 "-------- fun has_degree_in --------------------------------------------------------------------"; |
20 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------"; |
18 "-------- fun mono_deg_in ----------------------------------------------------------------------"; |
21 "-------- investigate (new 2002) uniary minus -----------"; |
19 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------"; |
22 "----------- fun sort_variables ----------------------------------------------------------------"; |
20 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------"; |
23 "-------- check make_polynomial with simple terms -------"; |
21 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
24 "-------- fun is_multUnordered --------------------------"; |
22 "-------- fun sort_variables -------------------------------------------------------------------"; |
25 "-------- examples from textbook Schalk I ---------------"; |
23 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------"; |
26 "-------- check pbl 'polynomial simplification' --------"; |
24 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------"; |
27 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------"; |
25 "-------- check make_polynomial with simple terms ----------------------------------------------"; |
28 "-------- interSteps for Schalk 299a --------------------"; |
26 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------"; |
29 "-------- norm_Poly NOT COMPLETE ------------------------"; |
27 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; |
30 "-------- ord_make_polynomial ---------------------------"; |
28 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------"; |
31 "--------------------------------------------------------"; |
29 "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; |
32 "--------------------------------------------------------"; |
30 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; |
33 "--------------------------------------------------------"; |
31 "-------- examples from textbook Schalk I ------------------------------------------------------"; |
34 |
32 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------"; |
35 |
33 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------"; |
36 "----------- fun is_polyexp --------------------------------------------------------------------"; |
34 "-------- check pbl 'polynomial simplification' -----------------------------------------------"; |
37 "----------- fun is_polyexp --------------------------------------------------------------------"; |
35 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------"; |
38 "----------- fun is_polyexp --------------------------------------------------------------------"; |
36 "-------- interSteps for Schalk 299a -----------------------------------------------------------"; |
39 val thy = @{theory Partial_Fractions}; |
37 "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------"; |
40 val ctxt = Proof_Context.init_global thy; |
38 "-------- ord_make_polynomial ------------------------------------------------------------------"; |
41 |
39 "-----------------------------------------------------------------------------------------------"; |
42 val t = (the o (parseNEW ctxt)) "x / x"; |
40 "-----------------------------------------------------------------------------------------------"; |
|
41 "-----------------------------------------------------------------------------------------------"; |
|
42 |
|
43 |
|
44 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; |
|
45 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; |
|
46 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------"; |
|
47 (* indentation indicates call hierarchy: |
|
48 "~~~~~ fun is_addUnordered |
|
49 "~~~~~~~ fun is_polyexp |
|
50 "~~~~~~~ fun sort_monoms |
|
51 "~~~~~~~~~ fun sort_monList |
|
52 "~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order |
|
53 "~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order |
|
54 "~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order |
|
55 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order |
|
56 "~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv |
|
57 "~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv |
|
58 "~~~~~~~~~~~~~~~ fun monom_degree : term list -> int |
|
59 "~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order |
|
60 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option |
|
61 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string |
|
62 "~~~~~ fun is_multUnordered |
|
63 "~~~~~~~ fun sort_variables |
|
64 "~~~~~~~~~ fun sort_varList |
|
65 "~~~~~~~~~~~ fun var_ord |
|
66 "~~~~~~~~~~~~~ fun get_basStr used twice --^^ |
|
67 "~~~~~~~~~~~~~ fun get_potStr used twice --^^ |
|
68 |
|
69 fun int_ord (i1, i2) = |
|
70 (@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)}; |
|
71 Int.compare (i1, i2) |
|
72 ); |
|
73 fun var_ord (a, b) = |
|
74 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", |
|
75 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; |
|
76 prod_ord string_ord string_ord |
|
77 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) |
|
78 ); |
|
79 fun var_ord_revPow (a, b: term) = |
|
80 (@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", |
|
81 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; |
|
82 prod_ord string_ord string_ord_rev |
|
83 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) |
|
84 ); |
|
85 fun sort_varList ts = |
|
86 (@{print} {a = "sort_varList", args = UnparseC.terms ts}; |
|
87 sort var_ord ts |
|
88 ); |
|
89 fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL) |
|
90 | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS) |
|
91 | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER) |
|
92 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) = |
|
93 (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")", |
|
94 is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"}; |
|
95 case (cond x, cond y) of |
|
96 (false, false) => |
|
97 (case elem_ord (x, y) of |
|
98 EQUAL => dict_cond_ord elem_ord cond (xs, ys) |
|
99 | ord => ord) |
|
100 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys) |
|
101 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys) |
|
102 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) |
|
103 ); |
|
104 fun compare_koeff_ord (xs, ys) = |
|
105 (@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")", |
|
106 sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"}; |
|
107 string_ord |
|
108 ((koeff2ordStr o get_koeff_of_mon) xs, |
|
109 (koeff2ordStr o get_koeff_of_mon) ys) |
|
110 ); |
|
111 fun var_ord (a,b: term) = |
|
112 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", |
|
113 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; |
|
114 prod_ord string_ord string_ord |
|
115 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) |
|
116 ); |
|
117 *) |
|
118 |
|
119 |
|
120 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; |
|
121 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; |
|
122 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------"; |
|
123 (* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls. |
|
124 |
|
125 sym_real_mult_minus1 = "- ?z = - 1 * ?z" *) |
|
126 @{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *) |
|
127 val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *) |
|
128 val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real"; |
|
129 |
|
130 val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac; |
|
131 if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("-1", _)*)) |
|
132 else error "thm - ?z = - 1 * ?z loops with new numerals"; |
|
133 |
|
134 |
|
135 "-------- fun is_polyexp -----------------------------------------------------------------------"; |
|
136 "-------- fun is_polyexp -----------------------------------------------------------------------"; |
|
137 "-------- fun is_polyexp -----------------------------------------------------------------------"; |
|
138 val t = TermC.str2term "x / x"; |
43 if is_polyexp t then error "NOT is_polyexp (x / x)" else (); |
139 if is_polyexp t then error "NOT is_polyexp (x / x)" else (); |
44 |
140 |
45 val t = (the o (parseNEW ctxt)) "-1 * A * 3"; |
141 val t = TermC.str2term "-1 * A * 3"; |
46 if is_polyexp t then () else error "is_polyexp (-1 * A * 3)"; |
142 if is_polyexp t then () else error "is_polyexp (-1 * A * 3)"; |
47 |
143 |
48 val t = (the o (parseNEW ctxt)) "-1 * AA * 3"; |
144 val t = TermC.str2term "-1 * AA * 3"; |
49 if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)"; |
145 if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)"; |
50 |
146 |
51 "----------- fun has_degree_in -----------------------------------------------------------------"; |
147 val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real"; |
52 "----------- fun has_degree_in -----------------------------------------------------------------"; |
148 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))"; |
53 "----------- fun has_degree_in -----------------------------------------------------------------"; |
149 |
|
150 "-------- fun has_degree_in --------------------------------------------------------------------"; |
|
151 "-------- fun has_degree_in --------------------------------------------------------------------"; |
|
152 "-------- fun has_degree_in --------------------------------------------------------------------"; |
54 val v = (Thm.term_of o the o (TermC.parse thy)) "x"; |
153 val v = (Thm.term_of o the o (TermC.parse thy)) "x"; |
55 val t = (Thm.term_of o the o (TermC.parse thy)) "1"; |
154 val t = (Thm.term_of o the o (TermC.parse thy)) "1"; |
56 if has_degree_in t v = 0 then () else error "has_degree_in (1) x"; |
155 if has_degree_in t v = 0 then () else error "has_degree_in (1) x"; |
57 |
156 |
58 val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; |
157 val v = (Thm.term_of o the o (TermC.parse thy)) "AA"; |
297 *** Free ( -x, real)*) |
387 *** Free ( -x, real)*) |
298 case t of |
388 case t of |
299 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () |
389 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () |
300 | _ => error "internal representation of \"-(x)\" changed"; |
390 | _ => error "internal representation of \"-(x)\" changed"; |
301 |
391 |
302 "-------- check make_polynomial with simple terms -------"; |
392 |
303 "-------- check make_polynomial with simple terms -------"; |
393 "-------- fun sort_variables -------------------------------------------------------------------"; |
304 "-------- check make_polynomial with simple terms -------"; |
394 "-------- fun sort_variables -------------------------------------------------------------------"; |
|
395 "-------- fun sort_variables -------------------------------------------------------------------"; |
|
396 if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then () |
|
397 else error "lexicographic order CHANGED"; |
|
398 |
|
399 (*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*) |
|
400 val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*) |
|
401 val t' = sort_variables t; |
|
402 if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then () |
|
403 else error "sort_variables 3 * b + a * 2 CHANGED"; |
|
404 |
|
405 "~~~~~~~ fun sort_variables , args:"; val (t) = (t); |
|
406 val ll = map monom2list (poly2list t); |
|
407 |
|
408 (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]"; |
|
409 (*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)], |
|
410 (*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)] |
|
411 (*+*) ] = map monom2list (poly2list t); |
|
412 |
|
413 val lls = map sort_varList ll; |
|
414 |
|
415 (*+*)case map sort_varList ll of |
|
416 (*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)], |
|
417 (*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)] |
|
418 (*+*) ] => () |
|
419 (*+*)| _ => error "map sort_varList CHANGED"; |
|
420 |
|
421 val T = type_of t; |
|
422 val ls = map (create_monom T) lls; |
|
423 |
|
424 (*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _), |
|
425 (*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls; |
|
426 |
|
427 (*+*)case map (create_monom T) lls of |
|
428 (*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _), |
|
429 (*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _) |
|
430 (*+*) ] => () |
|
431 (*+*)| _ => error "map (create_monom T) CHANGED"; |
|
432 |
|
433 val xxx = (*in*) create_polynom T ls (*end*); |
|
434 |
|
435 (*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then () |
|
436 (*+*)else error "create_polynom CHANGED"; |
|
437 (* done by rewriting> 2 * a + 3 * b ? *) |
|
438 |
|
439 (*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*) |
|
440 val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*) |
|
441 val t' = sort_variables t; |
|
442 if UnparseC.term t' = "3 * a + - 2 * a" then () |
|
443 else error "sort_variables 3 * a + - 2 * a CHANGED"; |
|
444 |
|
445 "~~~~~~~ fun sort_variables , args:"; val (t) = (t); |
|
446 val ll = map monom2list (poly2list t); |
|
447 |
|
448 (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)], |
|
449 (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*) |
|
450 (*+*) ] = map monom2list (poly2list t); |
|
451 |
|
452 val lls = map |
|
453 sort_varList ll; |
|
454 |
|
455 (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)], |
|
456 (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*) |
|
457 (*+*) ] = map sort_varList ll; |
|
458 |
|
459 map sort_varList ll; |
|
460 "~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll); |
|
461 val sorted = sort var_ord ts; |
|
462 |
|
463 (*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]" |
|
464 (*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED"; |
|
465 |
|
466 |
|
467 (*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2" |
|
468 (*+*)then () else error "get_basStr - 2 CHANGED"; |
|
469 (*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a" |
|
470 (*+*)then () else error "get_basStr a CHANGED"; |
|
471 |
|
472 |
|
473 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------"; |
|
474 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------"; |
|
475 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------"; |
|
476 (* indentation partially indicates call hierarchy: |
|
477 "~~~~~ fun is_addUnordered |
|
478 "~~~~~~~ fun is_polyexp |
|
479 "~~~~~~~ fun sort_monoms |
|
480 "~~~~~~~~~ fun sort_monList |
|
481 "~~~~~~~~~~~ fun koeff_degree_ord |
|
482 "~~~~~~~~~~~~~ fun degree_ord |
|
483 "~~~~~~~~~~~~~~~ fun dict_cond_ord |
|
484 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow |
|
485 "~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv |
|
486 "~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv |
|
487 "~~~~~~~~~~~~~~~ fun monom_degree |
|
488 "~~~~~~~~~~~~~ fun compare_koeff_ord |
|
489 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon |
|
490 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr |
|
491 "~~~~~ fun is_multUnordered |
|
492 "~~~~~~~ fun sort_variables |
|
493 "~~~~~~~~~ fun sort_varList |
|
494 "~~~~~~~~~~~ fun var_ord |
|
495 "~~~~~~~~~~~~~ fun get_basStr used twice --^^ |
|
496 "~~~~~~~~~~~~~ fun get_potStr used twice --^^ |
|
497 *) |
|
498 val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered"; |
|
499 |
|
500 eval_is_addUnordered "xxx" "yyy" t @{theory}; |
|
501 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _, |
|
502 (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) = |
|
503 ("xxx", "yyy", t, @{theory}); |
|
504 |
|
505 (*if*) is_addUnordered arg; |
|
506 "~~~~~ fun is_addUnordered , args:"; val (t) = (arg); |
|
507 ((is_polyexp t) andalso not (t = sort_monoms t)); |
|
508 |
|
509 (t = sort_monoms t); |
|
510 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t); |
|
511 val ll = map monom2list (poly2list t); |
|
512 val lls = |
|
513 |
|
514 sort_monList ll; |
|
515 "~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll); |
|
516 val xxx = |
|
517 |
|
518 sort koeff_degree_ord ll(*return value*); |
|
519 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll); |
|
520 koeff_degree_ord: term list * term list -> order; |
|
521 (*we check all elements at once..*) |
|
522 val eee1 = ll |> nth 1; |
|
523 val eee2 = ll |> nth 2; |
|
524 val eee3 = ll |> nth 3; |
|
525 val eee3 = ll |> nth 3; |
|
526 val eee4 = ll |> nth 4; |
|
527 |
|
528 if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED"; |
|
529 if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED"; |
|
530 if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED"; |
|
531 if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED"; |
|
532 |
|
533 if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED"; |
|
534 if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED"; |
|
535 if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED"; |
|
536 if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED"; |
|
537 |
|
538 if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED"; |
|
539 if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED"; |
|
540 if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED"; |
|
541 if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED"; |
|
542 |
|
543 if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED"; |
|
544 if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED"; |
|
545 if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED"; |
|
546 if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED"; |
|
547 |
|
548 if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED"; |
|
549 if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED"; |
|
550 if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED"; |
|
551 if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED"; |
|
552 |
|
553 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = (); |
|
554 degree_ord: term list * term list -> order; |
|
555 |
|
556 if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED"; |
|
557 if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED"; |
|
558 if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED"; |
|
559 if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED"; |
|
560 |
|
561 if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED"; |
|
562 if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED"; |
|
563 if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED"; |
|
564 if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED"; |
|
565 |
|
566 if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED"; |
|
567 if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED"; |
|
568 if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED"; |
|
569 if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED"; |
|
570 |
|
571 if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED"; |
|
572 if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED"; |
|
573 if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED"; |
|
574 if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED"; |
|
575 |
|
576 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = (); |
|
577 dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order; |
|
578 dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order; |
|
579 dict_cond_ord var_ord_revPow is_nums: term list * term list -> order; |
|
580 val xxx = dict_cond_ord var_ord_revPow is_nums; |
|
581 (* output from: |
|
582 fun var_ord_revPow (a,b: term) = |
|
583 (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"}; |
|
584 @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; |
|
585 prod_ord string_ord string_ord_rev |
|
586 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))); |
|
587 *) |
|
588 if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED"; |
|
589 if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED"; |
|
590 if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED"; |
|
591 if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED"; |
|
592 (*-------------------------------------------------------------------------------------*) |
|
593 if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED"; |
|
594 if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED"; |
|
595 if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED"; |
|
596 if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED"; |
|
597 (*-------------------------------------------------------------------------------------*) |
|
598 if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED"; |
|
599 if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED"; |
|
600 if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED"; |
|
601 if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED"; |
|
602 (*-------------------------------------------------------------------------------------*) |
|
603 if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED"; |
|
604 if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED"; |
|
605 if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED"; |
|
606 if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED"; |
|
607 (*-------------------------------------------------------------------------------------*) |
|
608 |
|
609 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = (); |
|
610 (* we check all at once//*) |
|
611 if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED"; |
|
612 if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED"; |
|
613 if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED"; |
|
614 if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED"; |
|
615 |
|
616 "~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = (); |
|
617 compare_koeff_ord: term list * term list -> order; |
|
618 (* we check all at once//*) |
|
619 if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED"; |
|
620 if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED"; |
|
621 if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED"; |
|
622 if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED"; |
|
623 |
|
624 if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED"; |
|
625 if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED"; |
|
626 if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED"; |
|
627 if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED"; |
|
628 |
|
629 if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED"; |
|
630 if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED"; |
|
631 if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED"; |
|
632 if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED"; |
|
633 |
|
634 if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED"; |
|
635 if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED"; |
|
636 if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED"; |
|
637 if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED"; |
|
638 |
|
639 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = (); |
|
640 get_koeff_of_mon: term list -> term option; |
|
641 |
|
642 val SOME xxx1 = get_koeff_of_mon eee1; |
|
643 val SOME xxx2 = get_koeff_of_mon eee2; |
|
644 val SOME xxx3 = get_koeff_of_mon eee3; |
|
645 val NONE = get_koeff_of_mon eee4; |
|
646 |
|
647 if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED"; |
|
648 if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED"; |
|
649 if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED"; |
|
650 |
|
651 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = (); |
|
652 koeff2ordStr: term option -> string; |
|
653 if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED"; |
|
654 if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED"; |
|
655 if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED"; |
|
656 if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED"; |
|
657 |
|
658 |
|
659 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------"; |
|
660 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------"; |
|
661 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------"; |
|
662 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y"; |
|
663 Rewrite.trace_on := false; |
|
664 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; |
|
665 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; |
|
666 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then () |
|
667 else error "poly.sml: diff.behav. in make_polynomial 23"; |
|
668 |
|
669 (** ) |
|
670 ## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y |
|
671 ### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y |
|
672 ###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered |
|
673 ####### try calc: "Poly.is_addUnordered" |
|
674 ######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*) |
|
675 True" (*isa2*) |
|
676 ####### calc. to: False (*isa*) |
|
677 True (*isa2*) |
|
678 ( **) |
|
679 if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then () |
|
680 else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*) |
|
681 "~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real"); |
|
682 ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*) |
|
683 |
|
684 (*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; |
|
685 |
|
686 (*+*) if t = sort_monoms t = false then () else error "sort_monoms 123"; |
|
687 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t); |
|
688 val ll = map monom2list (poly2list t); |
|
689 val lls = sort_monList ll; |
|
690 |
|
691 (*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*) |
|
692 (*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*) |
|
693 |
|
694 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = (); |
|
695 (* we check all elements at once..*) |
|
696 val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]"; |
|
697 val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]"; |
|
698 |
|
699 (*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED"; |
|
700 (*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED"; |
|
701 (*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*) |
|
702 (*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED"; |
|
703 (* isa -- isa2: |
|
704 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*) |
|
705 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*) |
|
706 (*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*) |
|
707 |
|
708 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*) |
|
709 |
|
710 (*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*) |
|
711 |
|
712 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*) |
|
713 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*) |
|
714 (*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*) |
|
715 val it = true: bool |
|
716 val it = true: bool |
|
717 val it = true: bool |
|
718 val it = true: bool*) |
|
719 |
|
720 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = (); |
|
721 (*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED"; |
|
722 (*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*) |
|
723 (*{a = "int_ord (4, 10003) = ", z = LESS} isa |
|
724 {a = "int_ord (4, 4) = ", z = EQUAL} isa2*) |
|
725 (*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*) |
|
726 (*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED"; |
|
727 (* isa -- isa2: |
|
728 (*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*) |
|
729 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) |
|
730 (*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*) |
|
731 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*) |
|
732 (*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*) |
|
733 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*) |
|
734 (*1*){a = "dict_cond_ord ([], [])"} (*isa*) |
|
735 |
|
736 (*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*) |
|
737 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) |
|
738 {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*) |
|
739 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*) |
|
740 |
|
741 (*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*) |
|
742 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) |
|
743 {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} |
|
744 (*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*) |
|
745 |
|
746 (*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*) |
|
747 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*) |
|
748 (*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*) |
|
749 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*) |
|
750 (*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*) |
|
751 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*) |
|
752 (*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*) |
|
753 |
|
754 val it = true: bool |
|
755 val it = false: bool |
|
756 val it = false: bool |
|
757 val it = true: bool |
|
758 *) |
|
759 |
|
760 (*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED"; |
|
761 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1); |
|
762 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* ) |
|
763 (*if*) (is_nums x) (*else*); |
|
764 val (Const ("Transcendental.powr", _) $ Free _ $ t) = |
|
765 (*case*) x (*of*); |
|
766 (*+*)UnparseC.term x = "x \<up> 2"; |
|
767 (*if*) TermC.is_num t (*then*); |
|
768 |
|
769 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs); |
|
770 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs); |
|
771 (*if*) (is_nums x) (*else*); |
|
772 val (Const ("Transcendental.powr", _) $ Free _ $ t) = |
|
773 (*case*) x (*of*); |
|
774 (*+*)UnparseC.term x = "y \<up> 2"; |
|
775 (*if*) TermC.is_num t (*then*); |
|
776 |
|
777 val return = |
|
778 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs); |
|
779 if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED"; |
|
780 ( *---------------------------------------------------------------------------------OPEN local/*) |
|
781 |
|
782 (*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then () |
|
783 else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED"; |
|
784 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2); |
|
785 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* ) |
|
786 (*if*) (is_nums x) (*else*); |
|
787 val (Const ("Transcendental.powr", _) $ Free _ $ t) = |
|
788 (*case*) x (*of*); |
|
789 (*+*)UnparseC.term x = "x \<up> 3"; |
|
790 (*if*) TermC.is_num t (*then*); |
|
791 |
|
792 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs); |
|
793 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs); |
|
794 (*if*) (is_nums x) (*else*); |
|
795 val _ = (*the default case*) |
|
796 (*case*) x (*of*); |
|
797 ( *---------------------------------------------------------------------------------OPEN local/*) |
|
798 |
|
799 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = (); |
|
800 val xxx = dict_cond_ord var_ord_revPow is_nums; |
|
801 (*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED"; |
|
802 (*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED"; |
|
803 (*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED"; |
|
804 (*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED"; |
|
805 |
|
806 |
|
807 "-------- check make_polynomial with simple terms ----------------------------------------------"; |
|
808 "-------- check make_polynomial with simple terms ----------------------------------------------"; |
|
809 "-------- check make_polynomial with simple terms ----------------------------------------------"; |
305 "----- check 1 ---"; |
810 "----- check 1 ---"; |
306 val t = TermC.str2term "2*3*a"; |
811 val t = TermC.str2term "2*3*a"; |
307 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; |
812 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; |
308 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1"; |
813 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1"; |
309 |
814 |
370 |
875 |
371 "----- rewrite_set_ STILL DIDN'T WORK"; |
876 "----- rewrite_set_ STILL DIDN'T WORK"; |
372 val SOME (t, _) = rewrite_set_ thy true order_mult_ t; |
877 val SOME (t, _) = rewrite_set_ thy true order_mult_ t; |
373 UnparseC.term t; |
878 UnparseC.term t; |
374 |
879 |
375 "-------- examples from textbook Schalk I ---------------"; |
880 |
376 "-------- examples from textbook Schalk I ---------------"; |
881 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; |
377 "-------- examples from textbook Schalk I ---------------"; |
882 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; |
|
883 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------"; |
|
884 val thy = @{theory "Isac_Knowledge"}; |
|
885 val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered"; |
|
886 |
|
887 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true |
|
888 (*+*) andalso not (is_multUnordered arg) |
|
889 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED"; |
|
890 |
|
891 case eval_is_multUnordered "xxx " "yyy " t thy of |
|
892 SOME |
|
893 ("xxx 3 * a + - 2 * a_", |
|
894 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ |
|
895 Const ("HOL.False", _))) => () |
|
896 (* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*) |
|
897 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; |
|
898 |
|
899 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False"; |
|
900 val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered"; |
|
901 |
|
902 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true |
|
903 (*+*) andalso not (is_multUnordered arg) |
|
904 (*+*)then () else error "sort_variables - 2 * a CHANGED"; |
|
905 |
|
906 case eval_is_multUnordered "xxx " "yyy " t thy of |
|
907 SOME |
|
908 ("xxx - 2 * a_", |
|
909 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ |
|
910 Const ("HOL.False", _))) => () |
|
911 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; |
|
912 |
|
913 "----- is_multUnordered --- (a) is_multUnordered = False"; |
|
914 val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered"; |
|
915 |
|
916 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true |
|
917 (*+*) andalso not (is_multUnordered arg) |
|
918 (*+*)then () else error "sort_variables a CHANGED"; |
|
919 |
|
920 case eval_is_multUnordered "xxx " "yyy " t thy of |
|
921 SOME |
|
922 ("xxx a_", |
|
923 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ |
|
924 Const ("HOL.False", _))) => () |
|
925 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; |
|
926 |
|
927 "----- is_multUnordered --- (- 2) is_multUnordered = False"; |
|
928 val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered"; |
|
929 |
|
930 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true |
|
931 (*+*) andalso not (is_multUnordered arg) |
|
932 (*+*)then () else error "sort_variables - 2 CHANGED"; |
|
933 |
|
934 case eval_is_multUnordered "xxx " "yyy " t thy of |
|
935 SOME |
|
936 ("xxx - 2_", |
|
937 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $ |
|
938 Const ("HOL.False", _))) => () |
|
939 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED"; |
|
940 |
|
941 |
|
942 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------"; |
|
943 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------"; |
|
944 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------"; |
|
945 (* ca.line 45 of Rewrite.trace_on: |
|
946 ## rls: order_mult_rls_ on: |
|
947 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 |
|
948 ### rls: order_mult_ on: |
|
949 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 |
|
950 ###### rls: Rule_Set.empty-is_multUnordered on: |
|
951 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered |
|
952 ####### try calc: "Poly.is_multUnordered" |
|
953 ######## eval asms: |
|
954 N:x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered = True" |
|
955 -------------------------------------------------------------------------------------------------== |
|
956 O:x \<up> 3 + 3 * x \<up> 2 * (-1 * a) + 3 * x * (-1 \<up> 2 * a \<up> 2) + -1 \<up> 3 * a \<up> 3 is_multUnordered = True" |
|
957 ####### calc. to: True |
|
958 ####### try calc: "Poly.is_multUnordered" |
|
959 ####### try calc: "Poly.is_multUnordered" |
|
960 ### rls: order_mult_ on: |
|
961 N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + 3 * (a \<up> 2 * (x * (- 1) \<up> 2)) + a \<up> 3 * (- 1) \<up> 3 |
|
962 --------+--------------------------+---------------------------------+---------------------------<> |
|
963 O:x \<up> 3 + -1 * (3 * (a * x \<up> 2)) + -1 \<up> 2 * (3 * (a \<up> 2 * x)) + -1 \<up> 3 * a \<up> 3 |
|
964 -------------------------------------------------------------------------------------------------<> |
|
965 *) |
|
966 val t = TermC.str2term "x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3"; |
|
967 (* |
|
968 "~~~~~ fun is_multUnordered |
|
969 "~~~~~~~ fun sort_variables |
|
970 "~~~~~~~~~ val sort_varList |
|
971 *) |
|
972 "~~~~~ fun is_multUnordered , args:"; val (t) = (t); |
|
973 is_polyexp t = true; |
|
974 |
|
975 val return = |
|
976 sort_variables t; |
|
977 (*+*)if UnparseC.term return = |
|
978 (*+*) "x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) +\n(- 1) \<up> 2 * (3 * (a \<up> 2 * x)) +\n(- 1) \<up> 3 * a \<up> 3" |
|
979 (*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED"; |
|
980 |
|
981 "~~~~~~~ fun sort_variables , args:"; val (t) = (t); |
|
982 val ll = map monom2list (poly2list t); |
|
983 val lls = map sort_varList ll; |
|
984 |
|
985 (*+*)val ori3 = nth 3 ll; |
|
986 (*+*)val mon3 = nth 3 lls; |
|
987 |
|
988 (*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll"; |
|
989 (*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll"; |
|
990 (*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll"; |
|
991 (*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll"; |
|
992 |
|
993 (*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls"; |
|
994 (*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls"; |
|
995 (*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls"; |
|
996 (*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls"; |
|
997 |
|
998 "~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3); |
|
999 (* Output below with: |
|
1000 val sort_varList = sort var_ord; |
|
1001 fun var_ord (a,b: term) = |
|
1002 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")", |
|
1003 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"}; |
|
1004 prod_ord string_ord string_ord |
|
1005 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)) |
|
1006 ); |
|
1007 *) |
|
1008 (*+*)val xxx = sort_varList ori3; |
|
1009 (* |
|
1010 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*) |
|
1011 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*) |
|
1012 |
|
1013 isa isa2 |
|
1014 {a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"} |
|
1015 {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"} |
|
1016 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} |
|
1017 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"} |
|
1018 {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} |
|
1019 {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"} |
|
1020 ^^^ ^^^ |
|
1021 |
|
1022 {a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"} |
|
1023 {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"} |
|
1024 ^^^ ^^^ |
|
1025 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} |
|
1026 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"} |
|
1027 {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} |
|
1028 {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"} |
|
1029 *) |
|
1030 |
|
1031 |
|
1032 "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; |
|
1033 "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; |
|
1034 "-------- fun is_multUnordered b * a * a ------------------------------------------------------"; |
|
1035 val t = TermC.str2term "b * a * a"; |
|
1036 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; |
|
1037 if UnparseC.term t = "a \<up> 2 * b" then () |
|
1038 else error "poly.sml: diff.behav. in make_polynomial 21"; |
|
1039 |
|
1040 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"}); |
|
1041 ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*) |
|
1042 |
|
1043 (*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED"; |
|
1044 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t); |
|
1045 (*if*) TermC.is_num num (*else*); |
|
1046 |
|
1047 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num); |
|
1048 (*if*) TermC.is_num num (*else*); |
|
1049 (*if*) TermC.is_variable num (*then*); |
|
1050 |
|
1051 val xxx = sort_variables t; |
|
1052 (*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED"; |
|
1053 |
|
1054 |
|
1055 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; |
|
1056 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; |
|
1057 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------"; |
|
1058 val t = TermC.str2term "2*3*a"; |
|
1059 val SOME (t', _) = rewrite_set_ thy false make_polynomial t; |
|
1060 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED"; |
|
1061 (* |
|
1062 ## try calc: "Groups.times_class.times" |
|
1063 ## rls: order_mult_rls_ on: 6 * a |
|
1064 ### rls: order_mult_ on: 6 * a |
|
1065 ###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered |
|
1066 ####### try calc: "Poly.is_multUnordered" |
|
1067 ######## eval asms: "6 * a is_multUnordered = True" (*isa*) |
|
1068 = False" (*isa2*) |
|
1069 ####### calc. to: True (*isa*) |
|
1070 False (*isa2*) |
|
1071 *) |
|
1072 val t = TermC.str2term "(6 * a) is_multUnordered"; |
|
1073 val SOME |
|
1074 (_, t') = |
|
1075 eval_is_multUnordered "xxx" () t @{theory}; |
|
1076 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () |
|
1077 (*+*)else error "6 * a is_multUnordered = False CHANGED"; |
|
1078 |
|
1079 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _, |
|
1080 (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory}); |
|
1081 (*if*) is_multUnordered arg (*else*); |
|
1082 |
|
1083 "~~~~~ fun is_multUnordered , args:"; val (t) = (arg); |
|
1084 val return = |
|
1085 ((is_polyexp t) andalso not (t = sort_variables t)); |
|
1086 |
|
1087 (*+*)return = false; (*isa*) |
|
1088 (*+*) is_polyexp t = true; (*isa*) |
|
1089 (*+*) not (t = sort_variables t) = false; (*isa*) |
|
1090 |
|
1091 val xxx = sort_variables t; |
|
1092 (*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED"; |
|
1093 |
|
1094 |
|
1095 "-------- examples from textbook Schalk I ------------------------------------------------------"; |
|
1096 "-------- examples from textbook Schalk I ------------------------------------------------------"; |
|
1097 "-------- examples from textbook Schalk I ------------------------------------------------------"; |
378 "-----SPB Schalk I p.63 No.267b ---"; |
1098 "-----SPB Schalk I p.63 No.267b ---"; |
379 (*associate poly* ) |
|
380 val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)"; |
1099 val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)"; |
381 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; |
1100 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t; |
382 if (UnparseC.term t) = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 + -8 * x \<up> 9" |
1101 if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9" |
383 then () else error "poly.sml: diff.behav. in make_polynomial 1"; |
1102 then () else error "poly.sml: diff.behav. in make_polynomial 1"; |
384 |
1103 |
385 "-----SPB Schalk I p.63 No.275b ---"; |
1104 "-----SPB Schalk I p.63 No.275b ---"; |
386 val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)"; |
1105 val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)"; |
387 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
1106 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
388 if (UnparseC.term t) = ("3 * x \<up> 4 + -2 * x \<up> 3 * y + -5 * x \<up> 2 * y \<up> 2 + " ^ |
1107 if UnparseC.term t = |
389 "4 * x * y \<up> 3 +\n-2 * y \<up> 4") |
1108 "3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4" |
390 then () else error "poly.sml: diff.behav. in make_polynomial 2"; |
1109 then () else error "poly.sml: diff.behav. in make_polynomial 2"; |
391 |
1110 |
392 "-----SPB Schalk I p.63 No.279b ---"; |
1111 "-----SPB Schalk I p.63 No.279b ---"; |
393 val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)"; |
1112 val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)"; |
394 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
1113 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
395 if (UnparseC.term t) = |
1114 if UnparseC.term t = |
396 ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x \<up> 2 +\n" ^ |
1115 ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^ |
397 "-1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n-1 * a * x \<up> 3 +\n" ^ |
1116 "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^ |
398 "-1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n-1 * b * x \<up> 3 +\n" ^ |
1117 "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^ |
399 "c * d * x \<up> 2 +\n-1 * c * x \<up> 3 +\n-1 * d * x \<up> 3 +\nx \<up> 4") |
1118 " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4") |
400 then () else error "poly.sml: diff.behav. in make_polynomial 3"; |
1119 then () else error "poly.sml: diff.behav. in make_polynomial 3"; |
401 ( *associate poly*) |
1120 (*associate poly*) |
402 |
1121 |
403 "-----SPB Schalk I p.63 No.291 ---"; |
1122 "-----SPB Schalk I p.63 No.291 ---"; |
404 val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))"; |
1123 val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))"; |
405 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
1124 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
406 if (UnparseC.term t) = "50 + -770 * x + 4520 * x \<up> 2 + -16320 * x \<up> 3 + -26880 * x \<up> 4" |
1125 if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4" |
407 then () else error "poly.sml: diff.behav. in make_polynomial 4"; |
1126 then () else error "poly.sml: diff.behav. in make_polynomial 4"; |
408 |
1127 |
409 (*associate poly* ) |
|
410 "-----SPB Schalk I p.64 No.295c ---"; |
1128 "-----SPB Schalk I p.64 No.295c ---"; |
411 val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2"; |
1129 val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2"; |
412 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
1130 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
413 if (UnparseC.term t) = ("169 * a \<up> 8 * b \<up> 18 * c \<up> 2 + -312 * a \<up> 7 * b \<up> 15 * c \<up> 10" ^ |
1131 if UnparseC.term t = |
414 " +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18") |
1132 "169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18" |
415 then ()else error "poly.sml: diff.behav. in make_polynomial 5"; |
1133 then ()else error "poly.sml: diff.behav. in make_polynomial 5"; |
416 ( *associate poly*) |
|
417 |
1134 |
418 "-----SPB Schalk I p.64 No.299a ---"; |
1135 "-----SPB Schalk I p.64 No.299a ---"; |
419 val t = TermC.str2term "(x - y)*(x + y)"; |
1136 val t = TermC.str2term "(x - y)*(x + y)"; |
420 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
1137 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
421 if (UnparseC.term t) = "x \<up> 2 + -1 * y \<up> 2" |
1138 if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2" |
422 then () else error "poly.sml: diff.behav. in make_polynomial 6"; |
1139 then () else error "poly.sml: diff.behav. in make_polynomial 6"; |
423 |
1140 |
424 "-----SPB Schalk I p.64 No.300c ---"; |
1141 "-----SPB Schalk I p.64 No.300c ---"; |
425 val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)"; |
1142 val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)"; |
426 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
1143 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
427 if (UnparseC.term t) = "-1 + 9 * x \<up> 4 * y \<up> 2" |
1144 if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2" |
428 then () else error "poly.sml: diff.behav. in make_polynomial 7"; |
1145 then () else error "poly.sml: diff.behav. in make_polynomial 7"; |
429 |
1146 |
430 "-----SPB Schalk I p.64 No.302 ---"; |
1147 "-----SPB Schalk I p.64 No.302 ---"; |
431 val t = TermC.str2term |
1148 val t = TermC.str2term |
432 "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)"; |
1149 "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)"; |