737 rules = |
737 rules = |
738 [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), |
738 [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), |
739 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), |
739 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), |
740 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"), |
740 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"), |
741 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
741 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
742 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), |
742 Rule.Thm ("not_false", @{thm not_false}), |
743 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), |
743 Rule.Thm ("not_true", @{thm not_true}), |
744 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_") |
744 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_") |
745 ], |
745 ], |
746 scr = Rule.Empty_Prog |
746 scr = Rule.Empty_Prog |
747 }; |
747 }; |
748 |
748 |
751 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
751 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
752 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
752 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
753 rules = |
753 rules = |
754 [\<^rule_thm>\<open>real_diff_minus\<close>, |
754 [\<^rule_thm>\<open>real_diff_minus\<close>, |
755 (*"a - b = a + -1 * b"*) |
755 (*"a - b = a + -1 * b"*) |
756 Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})) |
756 Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})) |
757 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)], |
757 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)], |
758 scr = Rule.Empty_Prog}; |
758 scr = Rule.Empty_Prog}; |
759 |
759 |
760 val expand_poly_ = |
760 val expand_poly_ = |
761 Rule_Def.Repeat{id = "expand_poly_", preconds = [], |
761 Rule_Def.Repeat{id = "expand_poly_", preconds = [], |
788 \<^rule_thm>\<open>realpow_multI\<close>, |
788 \<^rule_thm>\<open>realpow_multI\<close>, |
789 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
789 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
790 \<^rule_thm>\<open>realpow_pow\<close>, |
790 \<^rule_thm>\<open>realpow_pow\<close>, |
791 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
791 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
792 (**) |
792 (**) |
793 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}), |
793 Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}), |
794 (*"n is_even ==> (- r) \<up> n = r \<up> n"*) |
794 (*"n is_even ==> (- r) \<up> n = r \<up> n"*) |
795 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}) |
795 Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd}) |
796 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) |
796 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) |
797 (**) |
797 (**) |
798 ], scr = Rule.Empty_Prog}; |
798 ], scr = Rule.Empty_Prog}; |
799 |
799 |
800 val expand_poly_rat_ = |
800 val expand_poly_rat_ = |
801 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [], |
801 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [], |
802 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
802 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
803 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty |
803 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty |
804 [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""), |
804 [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""), |
805 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"), |
805 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"), |
806 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), |
806 Rule.Thm ("not_false", @{thm not_false}), |
807 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}) |
807 Rule.Thm ("not_true", @{thm not_true}) |
808 ], |
808 ], |
809 srls = Rule_Set.Empty, |
809 srls = Rule_Set.Empty, |
810 calc = [], errpatts = [], |
810 calc = [], errpatts = [], |
811 rules = |
811 rules = |
812 [\<^rule_thm>\<open>real_plus_binom_pow4_poly\<close>, |
812 [\<^rule_thm>\<open>real_plus_binom_pow4_poly\<close>, |
830 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
830 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
831 |
831 |
832 \<^rule_thm>\<open>realpow_multI_poly\<close>, |
832 \<^rule_thm>\<open>realpow_multI_poly\<close>, |
833 (*"[| r is_polyexp; s is_polyexp |] ==> |
833 (*"[| r is_polyexp; s is_polyexp |] ==> |
834 (r * s) \<up> n = r \<up> n * s \<up> n"*) |
834 (r * s) \<up> n = r \<up> n * s \<up> n"*) |
835 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}), |
835 Rule.Thm ("realpow_pow", @{thm realpow_pow}), |
836 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
836 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*) |
837 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}), |
837 Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}), |
838 (*"n is_even ==> (- r) \<up> n = r \<up> n"*) |
838 (*"n is_even ==> (- r) \<up> n = r \<up> n"*) |
839 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}) |
839 Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd}) |
840 (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) |
840 (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) |
841 ], scr = Rule.Empty_Prog}; |
841 ], scr = Rule.Empty_Prog}; |
842 |
842 |
843 val simplify_power_ = |
843 val simplify_power_ = |
844 Rule_Def.Repeat{id = "simplify_power_", preconds = [], |
844 Rule_Def.Repeat{id = "simplify_power_", preconds = [], |
960 val expand_poly = |
960 val expand_poly = |
961 Rule_Def.Repeat{id = "expand_poly", preconds = [], |
961 Rule_Def.Repeat{id = "expand_poly", preconds = [], |
962 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
962 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
963 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
963 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
964 rules = |
964 rules = |
965 [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}), |
965 [Rule.Thm ("distrib_right" , @{thm distrib_right}), |
966 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
966 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
967 \<^rule_thm>\<open>distrib_left\<close>, |
967 \<^rule_thm>\<open>distrib_left\<close>, |
968 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
968 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
969 (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1), |
969 (*Rule.Thm ("distrib_right1", @{thm distrib_right}1), |
970 ....... 18.3.03 undefined???*) |
970 ....... 18.3.03 undefined???*) |
971 |
971 |
972 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
972 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, |
973 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*) |
973 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*) |
974 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>, |
974 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>, |
980 |
980 |
981 \<^rule_thm>\<open>minus_minus\<close>, |
981 \<^rule_thm>\<open>minus_minus\<close>, |
982 (*"- (- ?z) = ?z"*) |
982 (*"- (- ?z) = ?z"*) |
983 \<^rule_thm>\<open>real_diff_minus\<close>, |
983 \<^rule_thm>\<open>real_diff_minus\<close>, |
984 (*"a - b = a + -1 * b"*) |
984 (*"a - b = a + -1 * b"*) |
985 Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})) |
985 Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})) |
986 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*) |
986 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*) |
987 |
987 |
988 (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*) |
988 (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*) |
989 (*"- (?x + ?y) = - ?x + - ?y"*) |
989 (*"- (?x + ?y) = - ?x + - ?y"*) |
990 (*\<^rule_thm>\<open>real_diff_plus\<close>*) |
990 (*\<^rule_thm>\<open>real_diff_plus\<close>*) |
1041 calc = [], errpatts = [], |
1041 calc = [], errpatts = [], |
1042 rules = [\<^rule_thm>\<open>mult_1_left\<close>, |
1042 rules = [\<^rule_thm>\<open>mult_1_left\<close>, |
1043 (*"1 * z = z"*) |
1043 (*"1 * z = z"*) |
1044 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*) |
1044 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*) |
1045 (*"-1 * z = - z"*) |
1045 (*"-1 * z = - z"*) |
1046 Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})), |
1046 Rule.Thm ("minus_mult_left", (@{thm minus_mult_left} RS @{thm sym})), |
1047 (*- (?x * ?y) = "- ?x * ?y"*) |
1047 (*- (?x * ?y) = "- ?x * ?y"*) |
1048 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, |
1048 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, |
1049 (*"- ?x * - ?y = ?x * ?y"*)---*) |
1049 (*"- ?x * - ?y = ?x * ?y"*)---*) |
1050 \<^rule_thm>\<open>mult_zero_left\<close>, |
1050 \<^rule_thm>\<open>mult_zero_left\<close>, |
1051 (*"0 * z = 0"*) |
1051 (*"0 * z = 0"*) |