434 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*) |
434 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*) |
435 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}), |
435 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}), |
436 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
436 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
437 |
437 |
438 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}), |
438 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}), |
439 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
439 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*) |
440 |
440 |
441 Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}), |
441 Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}), |
442 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*) |
442 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*) |
443 Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}), |
443 Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}), |
444 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*) |
444 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*) |
616 contains absolute minimum of thms for context in norm_Rational .*) |
616 contains absolute minimum of thms for context in norm_Rational .*) |
617 val powers = prep_rls'( |
617 val powers = prep_rls'( |
618 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
618 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
619 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
619 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
620 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}), |
620 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}), |
621 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
621 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
622 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}), |
622 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}), |
623 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
623 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
624 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}), |
624 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}), |
625 (*"r ^^^ 1 = r"*) |
625 (*"r \<up> 1 = r"*) |
626 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}), |
626 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}), |
627 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*) |
627 (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*) |
628 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}), |
628 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}), |
629 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*) |
629 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) |
630 |
630 |
631 (*----- collect atoms over * -----*) |
631 (*----- collect atoms over * -----*) |
632 Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}), |
632 Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}), |
633 (*"r is_atom ==> r * r = r ^^^ 2"*) |
633 (*"r is_atom ==> r * r = r \<up> 2"*) |
634 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}), |
634 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}), |
635 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*) |
635 (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*) |
636 Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}), |
636 Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}), |
637 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*) |
637 (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*) |
638 |
638 |
639 (*----- distribute none-atoms -----*) |
639 (*----- distribute none-atoms -----*) |
640 Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}), |
640 Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}), |
641 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*) |
641 (*"[| 1 < n; not(r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*) |
642 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}), |
642 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}), |
643 (*"1 ^^^ n = 1"*) |
643 (*"1 \<up> n = 1"*) |
644 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_") |
644 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_") |
645 ], |
645 ], |
646 scr = Rule.Empty_Prog |
646 scr = Rule.Empty_Prog |
647 }); |
647 }); |
648 (*.contains absolute minimum of thms for context in norm_Rational.*) |
648 (*.contains absolute minimum of thms for context in norm_Rational.*) |
654 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
654 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
655 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}), |
655 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}), |
656 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
656 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2], |
657 otherwise inv.to a / b / c = ...*) |
657 otherwise inv.to a / b / c = ...*) |
658 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}), |
658 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}), |
659 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much |
659 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much |
660 and does not commute a / b * c ^^^ 2 !*) |
660 and does not commute a / b * c \<up> 2 !*) |
661 |
661 |
662 Rule.Thm ("divide_divide_eq_right", |
662 Rule.Thm ("divide_divide_eq_right", |
663 ThmC.numerals_to_Free @{thm divide_divide_eq_right}), |
663 ThmC.numerals_to_Free @{thm divide_divide_eq_right}), |
664 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
664 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
665 Rule.Thm ("divide_divide_eq_left", |
665 Rule.Thm ("divide_divide_eq_left", |
808 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}), |
808 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}), |
809 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
809 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
810 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
810 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
811 |
811 |
812 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}) |
812 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}) |
813 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
813 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*) |
814 ], |
814 ], |
815 scr = Rule.Empty_Prog}); |
815 scr = Rule.Empty_Prog}); |
816 |
816 |
817 val rat_reduce_1 = prep_rls'( |
817 val rat_reduce_1 = prep_rls'( |
818 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
818 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |