721 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
721 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
722 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")]; |
722 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")]; |
723 \<close> |
723 \<close> |
724 ML \<open> |
724 ML \<open> |
725 val expand = |
725 val expand = |
726 Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
726 Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
727 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [], |
727 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [], |
728 rules = [ |
728 rules = [ |
729 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
729 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
730 \<^rule_thm>\<open>distrib_left\<close> (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)], |
730 \<^rule_thm>\<open>distrib_left\<close> (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)], |
731 scr = Rule.Empty_Prog}; |
731 scr = Rule.Empty_Prog}; |
733 \<close> ML \<open> |
733 \<close> ML \<open> |
734 \<close> ML \<open>@{term "1 is_num"}\<close> |
734 \<close> ML \<open>@{term "1 is_num"}\<close> |
735 ML \<open> |
735 ML \<open> |
736 (* erls for calculate_Rational + etc *) |
736 (* erls for calculate_Rational + etc *) |
737 val powers_erls = |
737 val powers_erls = |
738 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
738 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
739 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
739 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
740 rules = [ |
740 rules = [ |
741 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"), |
741 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"), |
742 \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"), |
742 \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"), |
743 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
743 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
748 \<^rule_eval>\<open>plus_class.plus\<close> (eval_binop "#add_")], |
748 \<^rule_eval>\<open>plus_class.plus\<close> (eval_binop "#add_")], |
749 scr = Rule.Empty_Prog}; |
749 scr = Rule.Empty_Prog}; |
750 |
750 |
751 \<close> ML \<open> |
751 \<close> ML \<open> |
752 val discard_minus = |
752 val discard_minus = |
753 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
753 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
754 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
754 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
755 rules = [ |
755 rules = [ |
756 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*), |
756 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*), |
757 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)], |
757 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (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 = [], |
762 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
762 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
763 erls = powers_erls, srls = Rule_Set.Empty, |
763 erls = powers_erls, srls = Rule_Set.Empty, |
764 calc = [], errpatts = [], |
764 calc = [], errpatts = [], |
765 rules = [ |
765 rules = [ |
766 \<^rule_thm>\<open>real_plus_binom_pow4\<close>, (*"(a + b) \<up> 4 = ... "*) |
766 \<^rule_thm>\<open>real_plus_binom_pow4\<close>, (*"(a + b) \<up> 4 = ... "*) |
767 \<^rule_thm>\<open>real_plus_binom_pow5\<close>, (*"(a + b) \<up> 5 = ... "*) |
767 \<^rule_thm>\<open>real_plus_binom_pow5\<close>, (*"(a + b) \<up> 5 = ... "*) |
783 \<^rule_thm>\<open>realpow_minus_odd\<close> (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)], |
783 \<^rule_thm>\<open>realpow_minus_odd\<close> (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)], |
784 scr = Rule.Empty_Prog}; |
784 scr = Rule.Empty_Prog}; |
785 |
785 |
786 val expand_poly_rat_ = |
786 val expand_poly_rat_ = |
787 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [], |
787 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [], |
788 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
788 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
789 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [ |
789 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [ |
790 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""), |
790 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""), |
791 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"), |
791 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"), |
792 \<^rule_thm>\<open>not_false\<close>, |
792 \<^rule_thm>\<open>not_false\<close>, |
793 \<^rule_thm>\<open>not_true\<close> ], |
793 \<^rule_thm>\<open>not_true\<close> ], |
811 \<^rule_thm>\<open>realpow_minus_odd\<close> (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) ], |
811 \<^rule_thm>\<open>realpow_minus_odd\<close> (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) ], |
812 scr = Rule.Empty_Prog}; |
812 scr = Rule.Empty_Prog}; |
813 |
813 |
814 val simplify_power_ = |
814 val simplify_power_ = |
815 Rule_Def.Repeat{id = "simplify_power_", preconds = [], |
815 Rule_Def.Repeat{id = "simplify_power_", preconds = [], |
816 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
816 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
817 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
817 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
818 calc = [], errpatts = [], |
818 calc = [], errpatts = [], |
819 rules = [ |
819 rules = [ |
820 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen |
820 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen |
821 a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *) |
821 a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *) |
834 \<^rule_thm>\<open>realpow_pow\<close> (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)], |
834 \<^rule_thm>\<open>realpow_pow\<close> (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)], |
835 scr = Rule.Empty_Prog}; |
835 scr = Rule.Empty_Prog}; |
836 |
836 |
837 val calc_add_mult_pow_ = |
837 val calc_add_mult_pow_ = |
838 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [], |
838 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [], |
839 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
839 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
840 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty, |
840 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty, |
841 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
841 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
842 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
842 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
843 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
843 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
844 ], |
844 ], |
849 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
849 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
850 scr = Rule.Empty_Prog}; |
850 scr = Rule.Empty_Prog}; |
851 |
851 |
852 val reduce_012_mult_ = |
852 val reduce_012_mult_ = |
853 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [], |
853 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [], |
854 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
854 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
855 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
855 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
856 calc = [], errpatts = [], |
856 calc = [], errpatts = [], |
857 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *) |
857 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *) |
858 \<^rule_thm>\<open>mult_1_right\<close>, (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*) |
858 \<^rule_thm>\<open>mult_1_right\<close>, (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*) |
859 \<^rule_thm>\<open>realpow_zeroI\<close>, (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*) |
859 \<^rule_thm>\<open>realpow_zeroI\<close>, (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*) |
861 \<^rule_thm>\<open>realpow_eq_oneI\<close> (*"1 \<up> n = 1"*)], |
861 \<^rule_thm>\<open>realpow_eq_oneI\<close> (*"1 \<up> n = 1"*)], |
862 scr = Rule.Empty_Prog}; |
862 scr = Rule.Empty_Prog}; |
863 |
863 |
864 val collect_numerals_ = |
864 val collect_numerals_ = |
865 Rule_Def.Repeat{id = "collect_numerals_", preconds = [], |
865 Rule_Def.Repeat{id = "collect_numerals_", preconds = [], |
866 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
866 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
867 erls = Atools_erls, srls = Rule_Set.Empty, |
867 erls = Atools_erls, srls = Rule_Set.Empty, |
868 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")) |
868 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")) |
869 ], errpatts = [], |
869 ], errpatts = [], |
870 rules = [ |
870 rules = [ |
871 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
871 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
882 \<^rule_thm_sym>\<open>real_mult_2\<close> (*"z1 + z1 = 2 * z1"*)], |
882 \<^rule_thm_sym>\<open>real_mult_2\<close> (*"z1 + z1 = 2 * z1"*)], |
883 scr = Rule.Empty_Prog}; |
883 scr = Rule.Empty_Prog}; |
884 |
884 |
885 val reduce_012_ = |
885 val reduce_012_ = |
886 Rule_Def.Repeat{id = "reduce_012_", preconds = [], |
886 Rule_Def.Repeat{id = "reduce_012_", preconds = [], |
887 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
887 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
888 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [], |
888 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [], |
889 rules = [ |
889 rules = [ |
890 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
890 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
891 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
891 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
892 \<^rule_thm>\<open>mult_zero_right\<close>, (*"z * 0 = 0"*) |
892 \<^rule_thm>\<open>mult_zero_right\<close>, (*"z * 0 = 0"*) |
902 \<^rule_thm_sym>\<open>mult.assoc\<close> (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*) |
902 \<^rule_thm_sym>\<open>mult.assoc\<close> (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*) |
903 (*\<^rule_thm_sym>\<open>add.assoc\<close>*) (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)]; |
903 (*\<^rule_thm_sym>\<open>add.assoc\<close>*) (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)]; |
904 |
904 |
905 val expand_poly = |
905 val expand_poly = |
906 Rule_Def.Repeat{id = "expand_poly", preconds = [], |
906 Rule_Def.Repeat{id = "expand_poly", preconds = [], |
907 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
907 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
908 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
908 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
909 rules = [ |
909 rules = [ |
910 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
910 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
911 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
911 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
912 |
912 |
923 (*\<^rule_thm>\<open>real_diff_plus\<close>*) (*"a - b = a + -b"*)], |
923 (*\<^rule_thm>\<open>real_diff_plus\<close>*) (*"a - b = a + -b"*)], |
924 scr = Rule.Empty_Prog}; |
924 scr = Rule.Empty_Prog}; |
925 |
925 |
926 val simplify_power = |
926 val simplify_power = |
927 Rule_Def.Repeat{id = "simplify_power", preconds = [], |
927 Rule_Def.Repeat{id = "simplify_power", preconds = [], |
928 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
928 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
929 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
929 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
930 calc = [], errpatts = [], |
930 calc = [], errpatts = [], |
931 rules = [ |
931 rules = [ |
932 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
932 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
933 |
933 |
939 \<^rule_thm>\<open>realpow_eq_oneI\<close> (*"1 \<up> n = 1"*)], |
939 \<^rule_thm>\<open>realpow_eq_oneI\<close> (*"1 \<up> n = 1"*)], |
940 scr = Rule.Empty_Prog}; |
940 scr = Rule.Empty_Prog}; |
941 |
941 |
942 val collect_numerals = |
942 val collect_numerals = |
943 Rule_Def.Repeat{id = "collect_numerals", preconds = [], |
943 Rule_Def.Repeat{id = "collect_numerals", preconds = [], |
944 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
944 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
945 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty, |
945 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty, |
946 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
946 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
947 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
947 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
948 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
948 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
949 ], errpatts = [], |
949 ], errpatts = [], |
957 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
957 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
958 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
958 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
959 scr = Rule.Empty_Prog}; |
959 scr = Rule.Empty_Prog}; |
960 val reduce_012 = |
960 val reduce_012 = |
961 Rule_Def.Repeat{id = "reduce_012", preconds = [], |
961 Rule_Def.Repeat{id = "reduce_012", preconds = [], |
962 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
962 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
963 erls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [ |
963 erls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [ |
964 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
964 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"), |
965 \<^rule_thm>\<open>not_false\<close>, |
965 \<^rule_thm>\<open>not_false\<close>, |
966 \<^rule_thm>\<open>not_true\<close>], |
966 \<^rule_thm>\<open>not_true\<close>], |
967 srls = Rule_Set.Empty, calc = [], errpatts = [], |
967 srls = Rule_Set.Empty, calc = [], errpatts = [], |
987 ML \<open> |
987 ML \<open> |
988 (*MG.0401: termorders for multivariate polys dropped due to principal problems: |
988 (*MG.0401: termorders for multivariate polys dropped due to principal problems: |
989 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*) |
989 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*) |
990 val order_add_mult = |
990 val order_add_mult = |
991 Rule_Def.Repeat{id = "order_add_mult", preconds = [], |
991 Rule_Def.Repeat{id = "order_add_mult", preconds = [], |
992 rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>), |
992 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), |
993 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
993 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
994 calc = [], errpatts = [], |
994 calc = [], errpatts = [], |
995 rules = [ |
995 rules = [ |
996 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *) |
996 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *) |
997 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
997 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
1027 prepat = |
1027 prepat = |
1028 (* ?p matched with the current term gives an environment, |
1028 (* ?p matched with the current term gives an environment, |
1029 which evaluates (the instantiated) "?p is_multUnordered" to true *) |
1029 which evaluates (the instantiated) "?p is_multUnordered" to true *) |
1030 [([TermC.parse_patt \<^theory> "?p is_multUnordered"], |
1030 [([TermC.parse_patt \<^theory> "?p is_multUnordered"], |
1031 TermC.parse_patt \<^theory> "?p :: real")], |
1031 TermC.parse_patt \<^theory> "?p :: real")], |
1032 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1032 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1033 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty |
1033 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty |
1034 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")], |
1034 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")], |
1035 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
1035 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
1036 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1036 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1037 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
1037 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
1042 locate_rule = locate_rule, |
1042 locate_rule = locate_rule, |
1043 next_rule = next_rule, |
1043 next_rule = next_rule, |
1044 attach_form = attach_form}}; |
1044 attach_form = attach_form}}; |
1045 val order_mult_rls_ = |
1045 val order_mult_rls_ = |
1046 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [], |
1046 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [], |
1047 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1047 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1048 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
1048 erls = Rule_Set.empty,srls = Rule_Set.Empty, |
1049 calc = [], errpatts = [], |
1049 calc = [], errpatts = [], |
1050 rules = [ |
1050 rules = [ |
1051 Rule.Rls_ order_mult_], |
1051 Rule.Rls_ order_mult_], |
1052 scr = Rule.Empty_Prog}; |
1052 scr = Rule.Empty_Prog}; |
1067 die beide passen muessen, damit das Rule_Set.Rrls angewandt wird*) |
1067 die beide passen muessen, damit das Rule_Set.Rrls angewandt wird*) |
1068 ([TermC.parse_patt @{theory} "?p is_addUnordered"], |
1068 ([TermC.parse_patt @{theory} "?p is_addUnordered"], |
1069 TermC.parse_patt @{theory} "?p :: real" |
1069 TermC.parse_patt @{theory} "?p :: real" |
1070 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment |
1070 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment |
1071 fuer die Evaluation der Precondition "p is_addUnordered"*))], |
1071 fuer die Evaluation der Precondition "p is_addUnordered"*))], |
1072 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1072 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1073 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*) |
1073 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*) |
1074 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")], |
1074 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")], |
1075 calc = [ |
1075 calc = [ |
1076 ("PLUS" ,(\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
1076 ("PLUS" ,(\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
1077 ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1077 ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1085 next_rule = next_rule, |
1085 next_rule = next_rule, |
1086 attach_form = attach_form}}; |
1086 attach_form = attach_form}}; |
1087 |
1087 |
1088 val order_add_rls_ = |
1088 val order_add_rls_ = |
1089 Rule_Def.Repeat {id = "order_add_rls_", preconds = [], |
1089 Rule_Def.Repeat {id = "order_add_rls_", preconds = [], |
1090 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1090 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1091 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
1091 erls = Rule_Set.empty, srls = Rule_Set.Empty, |
1092 calc = [], errpatts = [], |
1092 calc = [], errpatts = [], |
1093 rules = [ |
1093 rules = [ |
1094 Rule.Rls_ order_add_], |
1094 Rule.Rls_ order_add_], |
1095 scr = Rule.Empty_Prog}; |
1095 scr = Rule.Empty_Prog}; |
1106 ML \<open> |
1106 ML \<open> |
1107 (*. see MG-DA.p.52ff .*) |
1107 (*. see MG-DA.p.52ff .*) |
1108 val make_polynomial(*MG.03, overwrites version from above, |
1108 val make_polynomial(*MG.03, overwrites version from above, |
1109 previously 'make_polynomial_'*) = |
1109 previously 'make_polynomial_'*) = |
1110 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list, |
1110 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list, |
1111 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1111 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1112 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [], |
1112 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [], |
1113 rules = [ |
1113 rules = [ |
1114 Rule.Rls_ discard_minus, |
1114 Rule.Rls_ discard_minus, |
1115 Rule.Rls_ expand_poly_, |
1115 Rule.Rls_ expand_poly_, |
1116 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1116 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1125 scr = Rule.Empty_Prog}; |
1125 scr = Rule.Empty_Prog}; |
1126 \<close> |
1126 \<close> |
1127 ML \<open> |
1127 ML \<open> |
1128 val norm_Poly(*=make_polynomial*) = |
1128 val norm_Poly(*=make_polynomial*) = |
1129 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list, |
1129 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list, |
1130 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1130 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1131 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1131 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1132 rules = [ |
1132 rules = [ |
1133 Rule.Rls_ discard_minus, |
1133 Rule.Rls_ discard_minus, |
1134 Rule.Rls_ expand_poly_, |
1134 Rule.Rls_ expand_poly_, |
1135 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1135 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1147 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1 |
1147 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1 |
1148 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*) |
1148 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*) |
1149 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*) |
1149 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*) |
1150 val make_rat_poly_with_parentheses = |
1150 val make_rat_poly_with_parentheses = |
1151 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list, |
1151 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list, |
1152 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
1152 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
1153 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1153 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
1154 rules = [ |
1154 rules = [ |
1155 Rule.Rls_ discard_minus, |
1155 Rule.Rls_ discard_minus, |
1156 Rule.Rls_ expand_poly_rat_,(*ignors rationals*) |
1156 Rule.Rls_ expand_poly_rat_,(*ignors rationals*) |
1157 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1157 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |