211 (*. a 'monomial t in variable v' is a term t with |
211 (*. a 'monomial t in variable v' is a term t with |
212 either (1) v NOT existent in t, or (2) v contained in t, |
212 either (1) v NOT existent in t, or (2) v contained in t, |
213 if (1) then degree 0 |
213 if (1) then degree 0 |
214 if (2) then v is a factor on the very right, ev. with exponent.*) |
214 if (2) then v is a factor on the very right, ev. with exponent.*) |
215 fun factor_right_deg (*case 2*) |
215 fun factor_right_deg (*case 2*) |
216 (t as Const ("op *",_) $ t1 $ |
216 (t as Const ("Groups.times_class.times",_) $ t1 $ |
217 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v = |
217 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v = |
218 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE |
218 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE |
219 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v = |
219 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v = |
220 if (vv = v) then SOME (int_of_str' d) else NONE |
220 if (vv = v) then SOME (int_of_str' d) else NONE |
221 | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v = |
221 | factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v = |
222 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE |
222 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE |
223 | factor_right_deg vv v = |
223 | factor_right_deg vv v = |
224 if (vv = v) then SOME 1 else NONE; |
224 if (vv = v) then SOME 1 else NONE; |
225 fun mono_deg_in m v = |
225 fun mono_deg_in m v = |
226 if coeff_in m v then (*case 1*) SOME 0 |
226 if coeff_in m v then (*case 1*) SOME 0 |
399 append_rls "Poly_erls" Atools_erls |
399 append_rls "Poly_erls" Atools_erls |
400 [ Calc ("op =",eval_equal "#equal_"), |
400 [ Calc ("op =",eval_equal "#equal_"), |
401 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
401 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
402 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
402 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
403 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
403 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
404 Calc ("op *",eval_binop "#mult_"), |
404 Calc ("Groups.times_class.times",eval_binop "#mult_"), |
405 Calc ("Atools.pow" ,eval_binop "#power_") |
405 Calc ("Atools.pow" ,eval_binop "#power_") |
406 ]; |
406 ]; |
407 |
407 |
408 val poly_crls = |
408 val poly_crls = |
409 append_rls "poly_crls" Atools_crls |
409 append_rls "poly_crls" Atools_crls |
410 [ Calc ("op =",eval_equal "#equal_"), |
410 [ Calc ("op =",eval_equal "#equal_"), |
411 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
411 Thm ("real_unari_minus",num_str @{thm real_unari_minus}), |
412 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
412 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
413 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
413 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
414 Calc ("op *",eval_binop "#mult_"), |
414 Calc ("Groups.times_class.times",eval_binop "#mult_"), |
415 Calc ("Atools.pow" ,eval_binop "#power_") |
415 Calc ("Atools.pow" ,eval_binop "#power_") |
416 ]; |
416 ]; |
417 |
417 |
418 local (*. for make_polynomial .*) |
418 local (*. for make_polynomial .*) |
419 |
419 |
553 (*.the expression contains + - * ^ only ? |
553 (*.the expression contains + - * ^ only ? |
554 this is weaker than 'is_polynomial' !.*) |
554 this is weaker than 'is_polynomial' !.*) |
555 fun is_polyexp (Free _) = true |
555 fun is_polyexp (Free _) = true |
556 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true |
556 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true |
557 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true |
557 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true |
558 | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true |
558 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true |
559 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true |
559 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true |
560 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
560 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
561 ((is_polyexp t1) andalso (is_polyexp t2)) |
561 ((is_polyexp t1) andalso (is_polyexp t2)) |
562 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = |
562 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = |
563 ((is_polyexp t1) andalso (is_polyexp t2)) |
563 ((is_polyexp t1) andalso (is_polyexp t2)) |
564 | is_polyexp (Const ("op *",_) $ t1 $ t2) = |
564 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = |
565 ((is_polyexp t1) andalso (is_polyexp t2)) |
565 ((is_polyexp t1) andalso (is_polyexp t2)) |
566 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) = |
566 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) = |
567 ((is_polyexp t1) andalso (is_polyexp t2)) |
567 ((is_polyexp t1) andalso (is_polyexp t2)) |
568 | is_polyexp _ = false; |
568 | is_polyexp _ = false; |
569 |
569 |
657 val calc_add_mult_pow_ = |
657 val calc_add_mult_pow_ = |
658 Rls{id = "calc_add_mult_pow_", preconds = [], |
658 Rls{id = "calc_add_mult_pow_", preconds = [], |
659 rew_ord = ("dummy_ord", dummy_ord), |
659 rew_ord = ("dummy_ord", dummy_ord), |
660 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
660 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
661 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
661 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
662 ("TIMES" , ("op *", eval_binop "#mult_")), |
662 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
663 ("POWER", ("Atools.pow", eval_binop "#power_")) |
663 ("POWER", ("Atools.pow", eval_binop "#power_")) |
664 ], |
664 ], |
665 (*asm_thm = [],*) |
665 (*asm_thm = [],*) |
666 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
666 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
667 Calc ("op *", eval_binop "#mult_"), |
667 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
668 Calc ("Atools.pow", eval_binop "#power_") |
668 Calc ("Atools.pow", eval_binop "#power_") |
669 ], scr = EmptyScr}:rls; |
669 ], scr = EmptyScr}:rls; |
670 |
670 |
671 val reduce_012_mult_ = |
671 val reduce_012_mult_ = |
672 Rls{id = "reduce_012_mult_", preconds = [], |
672 Rls{id = "reduce_012_mult_", preconds = [], |
750 val collect_numerals_left = |
750 val collect_numerals_left = |
751 Rls{id = "collect_numerals", preconds = [], |
751 Rls{id = "collect_numerals", preconds = [], |
752 rew_ord = ("dummy_ord", dummy_ord), |
752 rew_ord = ("dummy_ord", dummy_ord), |
753 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
753 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
754 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
754 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
755 ("TIMES" , ("op *", eval_binop "#mult_")), |
755 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
756 ("POWER", ("Atools.pow", eval_binop "#power_")) |
756 ("POWER", ("Atools.pow", eval_binop "#power_")) |
757 ], |
757 ], |
758 (*asm_thm = [],*) |
758 (*asm_thm = [],*) |
759 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), |
759 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), |
760 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
760 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
878 val collect_numerals = |
878 val collect_numerals = |
879 Rls{id = "collect_numerals", preconds = [], |
879 Rls{id = "collect_numerals", preconds = [], |
880 rew_ord = ("dummy_ord", dummy_ord), |
880 rew_ord = ("dummy_ord", dummy_ord), |
881 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
881 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
882 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
882 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
883 ("TIMES" , ("op *", eval_binop "#mult_")), |
883 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
884 ("POWER", ("Atools.pow", eval_binop "#power_")) |
884 ("POWER", ("Atools.pow", eval_binop "#power_")) |
885 ], |
885 ], |
886 (*asm_thm = [],*) |
886 (*asm_thm = [],*) |
887 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), |
887 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}), |
888 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
888 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
892 Thm ("real_one_collect",num_str @{thm real_one_collect}), |
892 Thm ("real_one_collect",num_str @{thm real_one_collect}), |
893 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
893 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
894 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
894 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
895 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
895 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
896 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
896 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
897 Calc ("op *", eval_binop "#mult_"), |
897 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
898 Calc ("Atools.pow", eval_binop "#power_") |
898 Calc ("Atools.pow", eval_binop "#power_") |
899 ], scr = EmptyScr}:rls; |
899 ], scr = EmptyScr}:rls; |
900 val reduce_012 = |
900 val reduce_012 = |
901 Rls{id = "reduce_012", preconds = [], |
901 Rls{id = "reduce_012", preconds = [], |
902 rew_ord = ("dummy_ord", dummy_ord), |
902 rew_ord = ("dummy_ord", dummy_ord), |
1023 |
1023 |
1024 val expand_binoms = |
1024 val expand_binoms = |
1025 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), |
1025 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), |
1026 erls = Atools_erls, srls = Erls, |
1026 erls = Atools_erls, srls = Erls, |
1027 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1027 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1028 ("TIMES" , ("op *", eval_binop "#mult_")), |
1028 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1029 ("POWER", ("Atools.pow", eval_binop "#power_")) |
1029 ("POWER", ("Atools.pow", eval_binop "#power_")) |
1030 ], |
1030 ], |
1031 rules = [Thm ("real_plus_binom_pow2", |
1031 rules = [Thm ("real_plus_binom_pow2", |
1032 num_str @{thm real_plus_binom_pow2}), |
1032 num_str @{thm real_plus_binom_pow2}), |
1033 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*) |
1033 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*) |
1078 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), |
1078 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), |
1079 (*"0 * z = 0"*) |
1079 (*"0 * z = 0"*) |
1080 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*) |
1080 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*) |
1081 |
1081 |
1082 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1082 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1083 Calc ("op *", eval_binop "#mult_"), |
1083 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1084 Calc ("Atools.pow", eval_binop "#power_"), |
1084 Calc ("Atools.pow", eval_binop "#power_"), |
1085 (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}), |
1085 (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}), |
1086 (*AC-rewriting*) |
1086 (*AC-rewriting*) |
1087 Thm ("real_mult_left_commute", |
1087 Thm ("real_mult_left_commute", |
1088 num_str @{thm real_mult_left_commute}), |
1088 num_str @{thm real_mult_left_commute}), |
1113 Thm ("real_one_collect_assoc", |
1113 Thm ("real_one_collect_assoc", |
1114 num_str @{thm real_one_collect_assoc}), |
1114 num_str @{thm real_one_collect_assoc}), |
1115 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
1115 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
1116 |
1116 |
1117 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1117 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1118 Calc ("op *", eval_binop "#mult_"), |
1118 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1119 Calc ("Atools.pow", eval_binop "#power_") |
1119 Calc ("Atools.pow", eval_binop "#power_") |
1120 ], |
1120 ], |
1121 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms) |
1121 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms) |
1122 }:rls; |
1122 }:rls; |
1123 |
1123 |
1130 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
1130 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
1131 (poly2list t1) @ (poly2list t2) |
1131 (poly2list t1) @ (poly2list t2) |
1132 | poly2list t = [t]; |
1132 | poly2list t = [t]; |
1133 |
1133 |
1134 (* Monom --> Liste von Variablen *) |
1134 (* Monom --> Liste von Variablen *) |
1135 fun monom2list (Const ("op *",_) $ t1 $ t2) = |
1135 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) = |
1136 (monom2list t1) @ (monom2list t2) |
1136 (monom2list t1) @ (monom2list t2) |
1137 | monom2list t = [t]; |
1137 | monom2list t = [t]; |
1138 |
1138 |
1139 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *) |
1139 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *) |
1140 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str |
1140 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str |
1276 val sort_monList = sort simple_ord; *) |
1276 val sort_monList = sort simple_ord; *) |
1277 |
1277 |
1278 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt |
1278 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt |
1279 (mit gewuenschtem Typen T) *) |
1279 (mit gewuenschtem Typen T) *) |
1280 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T); |
1280 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T); |
1281 fun mult T = Const ("op *", [T,T] ---> T); |
1281 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T); |
1282 fun binop op_ t1 t2 = op_ $ t1 $ t2; |
1282 fun binop op_ t1 t2 = op_ $ t1 $ t2; |
1283 fun create_prod T (a,b) = binop (mult T) a b; |
1283 fun create_prod T (a,b) = binop (mult T) a b; |
1284 fun create_sum T (a,b) = binop (plus T) a b; |
1284 fun create_sum T (a,b) = binop (plus T) a b; |
1285 |
1285 |
1286 (* löscht letztes Element einer Liste *) |
1286 (* löscht letztes Element einer Liste *) |
1351 rew_ord = ("dummy_ord", dummy_ord), |
1351 rew_ord = ("dummy_ord", dummy_ord), |
1352 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*) |
1352 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*) |
1353 [Calc ("Poly.is'_multUnordered", |
1353 [Calc ("Poly.is'_multUnordered", |
1354 eval_is_multUnordered "")], |
1354 eval_is_multUnordered "")], |
1355 calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")), |
1355 calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")), |
1356 ("TIMES" , ("op *" , eval_binop "#mult_")), |
1356 ("TIMES" , ("Groups.times_class.times" , eval_binop "#mult_")), |
1357 ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")), |
1357 ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")), |
1358 ("POWER" , ("Atools.pow", eval_binop "#power_"))], |
1358 ("POWER" , ("Atools.pow", eval_binop "#power_"))], |
1359 scr=Rfuns {init_state = init_state, |
1359 scr=Rfuns {init_state = init_state, |
1360 normal_form = normal_form, |
1360 normal_form = normal_form, |
1361 locate_rule = locate_rule, |
1361 locate_rule = locate_rule, |
1404 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*) |
1404 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*) |
1405 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "") |
1405 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "") |
1406 (*WN.18.6.03 definiert in thy, |
1406 (*WN.18.6.03 definiert in thy, |
1407 evaluiert prepat*)], |
1407 evaluiert prepat*)], |
1408 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
1408 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
1409 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
1409 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")), |
1410 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), |
1410 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")), |
1411 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
1411 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
1412 (*asm_thm=[],*) |
1412 (*asm_thm=[],*) |
1413 scr=Rfuns {init_state = init_state, |
1413 scr=Rfuns {init_state = init_state, |
1414 normal_form = normal_form, |
1414 normal_form = normal_form, |
1431 Seq {id = "make_polynomial", preconds = []:term list, |
1431 Seq {id = "make_polynomial", preconds = []:term list, |
1432 rew_ord = ("dummy_ord", dummy_ord), |
1432 rew_ord = ("dummy_ord", dummy_ord), |
1433 erls = Atools_erls, srls = Erls,calc = [], |
1433 erls = Atools_erls, srls = Erls,calc = [], |
1434 rules = [Rls_ discard_minus, |
1434 rules = [Rls_ discard_minus, |
1435 Rls_ expand_poly_, |
1435 Rls_ expand_poly_, |
1436 Calc ("op *", eval_binop "#mult_"), |
1436 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1437 Rls_ order_mult_rls_, |
1437 Rls_ order_mult_rls_, |
1438 Rls_ simplify_power_, |
1438 Rls_ simplify_power_, |
1439 Rls_ calc_add_mult_pow_, |
1439 Rls_ calc_add_mult_pow_, |
1440 Rls_ reduce_012_mult_, |
1440 Rls_ reduce_012_mult_, |
1441 Rls_ order_add_rls_, |
1441 Rls_ order_add_rls_, |
1449 Seq {id = "norm_Poly", preconds = []:term list, |
1449 Seq {id = "norm_Poly", preconds = []:term list, |
1450 rew_ord = ("dummy_ord", dummy_ord), |
1450 rew_ord = ("dummy_ord", dummy_ord), |
1451 erls = Atools_erls, srls = Erls, calc = [], |
1451 erls = Atools_erls, srls = Erls, calc = [], |
1452 rules = [Rls_ discard_minus, |
1452 rules = [Rls_ discard_minus, |
1453 Rls_ expand_poly_, |
1453 Rls_ expand_poly_, |
1454 Calc ("op *", eval_binop "#mult_"), |
1454 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1455 Rls_ order_mult_rls_, |
1455 Rls_ order_mult_rls_, |
1456 Rls_ simplify_power_, |
1456 Rls_ simplify_power_, |
1457 Rls_ calc_add_mult_pow_, |
1457 Rls_ calc_add_mult_pow_, |
1458 Rls_ reduce_012_mult_, |
1458 Rls_ reduce_012_mult_, |
1459 Rls_ order_add_rls_, |
1459 Rls_ order_add_rls_, |
1471 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list, |
1471 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list, |
1472 rew_ord = ("dummy_ord", dummy_ord), |
1472 rew_ord = ("dummy_ord", dummy_ord), |
1473 erls = Atools_erls, srls = Erls, calc = [], |
1473 erls = Atools_erls, srls = Erls, calc = [], |
1474 rules = [Rls_ discard_minus, |
1474 rules = [Rls_ discard_minus, |
1475 Rls_ expand_poly_rat_,(*ignors rationals*) |
1475 Rls_ expand_poly_rat_,(*ignors rationals*) |
1476 Calc ("op *", eval_binop "#mult_"), |
1476 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1477 Rls_ order_mult_rls_, |
1477 Rls_ order_mult_rls_, |
1478 Rls_ simplify_power_, |
1478 Rls_ simplify_power_, |
1479 Rls_ calc_add_mult_pow_, |
1479 Rls_ calc_add_mult_pow_, |
1480 Rls_ reduce_012_mult_, |
1480 Rls_ reduce_012_mult_, |
1481 Rls_ order_add_rls_, |
1481 Rls_ order_add_rls_, |
1490 compare expand_binoms.*) |
1490 compare expand_binoms.*) |
1491 val rev_rew_p = |
1491 val rev_rew_p = |
1492 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI), |
1492 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI), |
1493 erls = Atools_erls, srls = Erls, |
1493 erls = Atools_erls, srls = Erls, |
1494 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1494 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1495 ("TIMES" , ("op *", eval_binop "#mult_")), |
1495 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1496 ("POWER", ("Atools.pow", eval_binop "#power_"))*) |
1496 ("POWER", ("Atools.pow", eval_binop "#power_"))*) |
1497 ], |
1497 ], |
1498 rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}), |
1498 rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}), |
1499 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*) |
1499 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*) |
1500 Thm ("real_plus_binom_times1" ,num_str @{thm real_plus_binom_times1}), |
1500 Thm ("real_plus_binom_times1" ,num_str @{thm real_plus_binom_times1}), |
1513 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*) |
1513 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*) |
1514 Rls_ order_mult_rls_, |
1514 Rls_ order_mult_rls_, |
1515 (*Rls_ order_add_rls_,*) |
1515 (*Rls_ order_add_rls_,*) |
1516 |
1516 |
1517 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1517 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1518 Calc ("op *", eval_binop "#mult_"), |
1518 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1519 Calc ("Atools.pow", eval_binop "#power_"), |
1519 Calc ("Atools.pow", eval_binop "#power_"), |
1520 |
1520 |
1521 Thm ("sym_realpow_twoI", |
1521 Thm ("sym_realpow_twoI", |
1522 num_str (@{thm realpow_twoI} RS @{thm sym})), |
1522 num_str (@{thm realpow_twoI} RS @{thm sym})), |
1523 (*"r1 * r1 = r1 ^^^ 2"*) |
1523 (*"r1 * r1 = r1 ^^^ 2"*) |
1539 |
1539 |
1540 Thm ("realpow_multI", num_str @{thm realpow_multI}), |
1540 Thm ("realpow_multI", num_str @{thm realpow_multI}), |
1541 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
1541 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
1542 |
1542 |
1543 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1543 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1544 Calc ("op *", eval_binop "#mult_"), |
1544 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
1545 Calc ("Atools.pow", eval_binop "#power_"), |
1545 Calc ("Atools.pow", eval_binop "#power_"), |
1546 |
1546 |
1547 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*) |
1547 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*) |
1548 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),(*"0 * z = 0"*) |
1548 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),(*"0 * z = 0"*) |
1549 Thm ("add_0_left",num_str @{thm add_0_left})(*0 + z = z*) |
1549 Thm ("add_0_left",num_str @{thm add_0_left})(*0 + z = z*) |