175 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
175 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
176 fun is_polyrat_in t v = |
176 fun is_polyrat_in t v = |
177 let fun coeff_in c v = member op = (vars c) v; |
177 let fun coeff_in c v = member op = (vars c) v; |
178 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:") |
178 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:") |
179 (* at the moment there is no term like this, but ....*) |
179 (* at the moment there is no term like this, but ....*) |
180 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = |
180 | finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v = |
181 not(coeff_in b v) |
181 not(coeff_in b v) |
182 | finddivide (_ $ t1 $ t2) v = |
182 | finddivide (_ $ t1 $ t2) v = |
183 (finddivide t1 v) orelse (finddivide t2 v) |
183 (finddivide t1 v) orelse (finddivide t2 v) |
184 | finddivide (_ $ t1) v = (finddivide t1 v) |
184 | finddivide (_ $ t1) v = (finddivide t1 v) |
185 | finddivide _ _ = false; |
185 | finddivide _ _ = false; |
248 val t = (term_of o the o (parse thy)) "ab - (a*b)*x"; |
248 val t = (term_of o the o (parse thy)) "ab - (a*b)*x"; |
249 mono_deg_in t v; |
249 mono_deg_in t v; |
250 (*val it = NONE*) |
250 (*val it = NONE*) |
251 ------------------------------------------------------------------*) |
251 ------------------------------------------------------------------*) |
252 fun expand_deg_in t v = |
252 fun expand_deg_in t v = |
253 let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) = |
253 let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
254 (case mono_deg_in t2 v of (* $ is left associative*) |
254 (case mono_deg_in t2 v of (* $ is left associative*) |
255 SOME d' => edi d' d' t1 |
255 SOME d' => edi d' d' t1 |
256 | NONE => NONE) |
256 | NONE => NONE) |
257 | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) = |
257 | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = |
258 (case mono_deg_in t2 v of |
258 (case mono_deg_in t2 v of |
259 SOME d' => edi d' d' t1 |
259 SOME d' => edi d' d' t1 |
260 | NONE => NONE) |
260 | NONE => NONE) |
261 | edi d dmax (Const ("op -",_) $ t1 $ t2) = |
261 | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = |
262 (case mono_deg_in t2 v of |
262 (case mono_deg_in t2 v of |
263 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
263 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
264 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) |
264 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) |
265 then edi d' dmax t1 else NONE |
265 then edi d' dmax t1 else NONE |
266 | NONE => NONE) |
266 | NONE => NONE) |
267 | edi d dmax (Const ("op +",_) $ t1 $ t2) = |
267 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
268 (case mono_deg_in t2 v of |
268 (case mono_deg_in t2 v of |
269 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
269 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
270 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) |
270 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) |
271 then edi d' dmax t1 else NONE |
271 then edi d' dmax t1 else NONE |
272 | NONE => NONE) |
272 | NONE => NONE) |
295 (*SOME 1*) |
295 (*SOME 1*) |
296 val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2"; |
296 val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2"; |
297 expand_deg_in t v; |
297 expand_deg_in t v; |
298 -------------------------------------------------------------------*) |
298 -------------------------------------------------------------------*) |
299 fun poly_deg_in t v = |
299 fun poly_deg_in t v = |
300 let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) = |
300 let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
301 (case mono_deg_in t2 v of (* $ is left associative*) |
301 (case mono_deg_in t2 v of (* $ is left associative*) |
302 SOME d' => edi d' d' t1 |
302 SOME d' => edi d' d' t1 |
303 | NONE => NONE) |
303 | NONE => NONE) |
304 | edi d dmax (Const ("op +",_) $ t1 $ t2) = |
304 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = |
305 (case mono_deg_in t2 v of |
305 (case mono_deg_in t2 v of |
306 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
306 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
307 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) |
307 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) |
308 then edi d' dmax t1 else NONE |
308 then edi d' dmax t1 else NONE |
309 | NONE => NONE) |
309 | NONE => NONE) |
397 (*.for evaluation of conditions in rewrite rules.*) |
397 (*.for evaluation of conditions in rewrite rules.*) |
398 val Poly_erls = |
398 val Poly_erls = |
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 ("op +",eval_binop "#add_"), |
402 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
403 Calc ("op -",eval_binop "#sub_"), |
403 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
404 Calc ("op *",eval_binop "#mult_"), |
404 Calc ("op *",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 ("op +",eval_binop "#add_"), |
412 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
413 Calc ("op -",eval_binop "#sub_"), |
413 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
414 Calc ("op *",eval_binop "#mult_"), |
414 Calc ("op *",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 .*) |
551 ], scr = EmptyScr}:rls; |
551 ], scr = EmptyScr}:rls; |
552 |
552 |
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 ("op +",_) $ Free _ $ Free _) = true |
556 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true |
557 | is_polyexp (Const ("op -",_) $ 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 ("op *",_) $ 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 ("op +",_) $ 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 ("op -",_) $ 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 ("op *",_) $ 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)) |
656 |
656 |
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" , ("op +", eval_binop "#add_")), |
661 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
662 ("TIMES" , ("op *", eval_binop "#mult_")), |
662 ("TIMES" , ("op *", 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 ("op +", eval_binop "#add_"), |
666 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
667 Calc ("op *", eval_binop "#mult_"), |
667 Calc ("op *", 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_ = |
687 |
687 |
688 val collect_numerals_ = |
688 val collect_numerals_ = |
689 Rls{id = "collect_numerals_", preconds = [], |
689 Rls{id = "collect_numerals_", preconds = [], |
690 rew_ord = ("dummy_ord", dummy_ord), |
690 rew_ord = ("dummy_ord", dummy_ord), |
691 erls = Atools_erls, srls = Erls, |
691 erls = Atools_erls, srls = Erls, |
692 calc = [("PLUS" , ("op +", eval_binop "#add_")) |
692 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")) |
693 ], |
693 ], |
694 rules = |
694 rules = |
695 [Thm ("real_num_collect",num_str @{thm real_num_collect}), |
695 [Thm ("real_num_collect",num_str @{thm real_num_collect}), |
696 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
696 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
697 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}), |
697 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}), |
700 Thm ("real_one_collect",num_str @{thm real_one_collect}), |
700 Thm ("real_one_collect",num_str @{thm real_one_collect}), |
701 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
701 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
702 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}), |
702 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}), |
703 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*) |
703 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*) |
704 |
704 |
705 Calc ("op +", eval_binop "#add_"), |
705 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
706 |
706 |
707 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
707 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
708 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
708 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
709 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}), |
709 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}), |
710 (*"(k + z1) + z1 = k + 2 * z1"*) |
710 (*"(k + z1) + z1 = k + 2 * z1"*) |
749 (*MG.0401 ev. for use in rls with ordered rewriting ? |
749 (*MG.0401 ev. for use in rls with ordered rewriting ? |
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" , ("op +", eval_binop "#add_")), |
754 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
755 ("TIMES" , ("op *", eval_binop "#mult_")), |
755 ("TIMES" , ("op *", 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}), |
764 Thm ("real_one_collect",num_str @{thm real_one_collect}), |
764 Thm ("real_one_collect",num_str @{thm real_one_collect}), |
765 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
765 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
766 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
766 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}), |
767 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*) |
767 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*) |
768 |
768 |
769 Calc ("op +", eval_binop "#add_"), |
769 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
770 |
770 |
771 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*) |
771 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*) |
772 Thm ("sym_real_mult_2", |
772 Thm ("sym_real_mult_2", |
773 num_str (@{thm real_mult_2} RS @{thm sym})), |
773 num_str (@{thm real_mult_2} RS @{thm sym})), |
774 (*"z1 + z1 = 2 * z1"*) |
774 (*"z1 + z1 = 2 * z1"*) |
877 ], scr = EmptyScr}:rls; |
877 ], scr = EmptyScr}:rls; |
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" , ("op +", eval_binop "#add_")), |
882 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
883 ("TIMES" , ("op *", eval_binop "#mult_")), |
883 ("TIMES" , ("op *", 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}), |
891 l * n + (m * n + k) = (l + m) * n + k"*) |
891 l * n + (m * n + k) = (l + m) * n + k"*) |
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 ("op +", eval_binop "#add_"), |
896 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
897 Calc ("op *", eval_binop "#mult_"), |
897 Calc ("op *", 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 = [], |
1022 " t_t)"; |
1022 " t_t)"; |
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" , ("op +", eval_binop "#add_")), |
1027 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1028 ("TIMES" , ("op *", eval_binop "#mult_")), |
1028 ("TIMES" , ("op *", 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}), |
1077 (*"1 * z = z"*) |
1077 (*"1 * z = z"*) |
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 ("op +", eval_binop "#add_"), |
1082 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1083 Calc ("op *", eval_binop "#mult_"), |
1083 Calc ("op *", 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", |
1112 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
1112 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
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 ("op +", eval_binop "#add_"), |
1117 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1118 Calc ("op *", eval_binop "#mult_"), |
1118 Calc ("op *", 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; |
1125 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**) |
1125 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**) |
1126 |
1126 |
1127 (*FIXME.0401: make SML-order local to make_polynomial(_) *) |
1127 (*FIXME.0401: make SML-order local to make_polynomial(_) *) |
1128 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *) |
1128 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *) |
1129 (* Polynom --> List von Monomen *) |
1129 (* Polynom --> List von Monomen *) |
1130 fun poly2list (Const ("op +",_) $ 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 ("op *",_) $ t1 $ t2) = |
1275 |
1275 |
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 ("op +", [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 ("op *", [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 |
1350 parse_patt thy "?p" )], |
1350 parse_patt thy "?p" )], |
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" , ("op +" , eval_binop "#add_")), |
1355 calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")), |
1356 ("TIMES" , ("op *" , eval_binop "#mult_")), |
1356 ("TIMES" , ("op *" , eval_binop "#mult_")), |
1357 ("DIVIDE", ("HOL.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, |
1362 next_rule = next_rule, |
1362 next_rule = next_rule, |
1403 rew_ord = ("dummy_ord", dummy_ord), |
1403 rew_ord = ("dummy_ord", dummy_ord), |
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" ,("op +" ,eval_binop "#add_")), |
1408 calc = [("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")), |
1409 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
1409 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
1410 ("DIVIDE" ,("HOL.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, |
1415 locate_rule = locate_rule, |
1415 locate_rule = locate_rule, |
1489 (*.a minimal ruleset for reverse rewriting of factions [2]; |
1489 (*.a minimal ruleset for reverse rewriting of factions [2]; |
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" , ("op +", eval_binop "#add_")), |
1494 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1495 ("TIMES" , ("op *", eval_binop "#mult_")), |
1495 ("TIMES" , ("op *", 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*) |
1512 Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}), |
1512 Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}), |
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 ("op +", eval_binop "#add_"), |
1517 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1518 Calc ("op *", eval_binop "#mult_"), |
1518 Calc ("op *", 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})), |
1538 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
1538 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
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 ("op +", eval_binop "#add_"), |
1543 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
1544 Calc ("op *", eval_binop "#mult_"), |
1544 Calc ("op *", 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"*) |