706 |
706 |
707 (*.for evaluation of conditions in rewrite rules.*) |
707 (*.for evaluation of conditions in rewrite rules.*) |
708 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls [ |
708 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls [ |
709 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"), |
709 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"), |
710 \<^rule_thm>\<open>real_unari_minus\<close>, |
710 \<^rule_thm>\<open>real_unari_minus\<close>, |
711 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
711 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
712 \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"), |
712 \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"), |
713 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
713 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
714 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")]; |
714 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")]; |
715 |
715 |
716 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [ |
716 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [ |
717 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"), |
717 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"), |
718 \<^rule_thm>\<open>real_unari_minus\<close>, |
718 \<^rule_thm>\<open>real_unari_minus\<close>, |
719 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
719 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
720 \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"), |
720 \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"), |
721 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
721 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
722 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")]; |
722 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#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.function_empty), |
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 = [], |
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_"), |
744 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"), |
744 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"), |
745 \<^rule_eval>\<open>ord_class.less\<close> (Prog_Expr.eval_equ "#less_"), |
745 \<^rule_eval>\<open>ord_class.less\<close> (Prog_Expr.eval_equ "#less_"), |
746 \<^rule_thm>\<open>not_false\<close>, |
746 \<^rule_thm>\<open>not_false\<close>, |
747 \<^rule_thm>\<open>not_true\<close>, |
747 \<^rule_thm>\<open>not_true\<close>, |
748 \<^rule_eval>\<open>plus_class.plus\<close> (eval_binop "#add_")], |
748 \<^rule_eval>\<open>plus_class.plus\<close> (Calc_Binop.numeric "#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.function_empty), |
753 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
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.function_empty), |
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>, Calc_Binop.numeric "#add_")), |
842 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
842 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")), |
843 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
843 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_")) |
844 ], |
844 ], |
845 errpatts = [], |
845 errpatts = [], |
846 rules = [ |
846 rules = [ |
847 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
847 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
848 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
848 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
849 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
849 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#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.function_empty), |
854 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
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.function_empty), |
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>, Calc_Binop.numeric "#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"*) |
872 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>, |
872 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>, |
873 (*"[| l is_num; m is_num |] ==> (k + m * n) + l * n = k + (l + m)*n"*) |
873 (*"[| l is_num; m is_num |] ==> (k + m * n) + l * n = k + (l + m)*n"*) |
874 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
874 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
875 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*) |
875 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*) |
876 |
876 |
877 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
877 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
878 |
878 |
879 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen |
879 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen |
880 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
880 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
881 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*) |
881 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*) |
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"*)], |
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.function_empty), |
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>, Calc_Binop.numeric "#add_")), |
947 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
947 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")), |
948 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
948 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_")) |
949 ], errpatts = [], |
949 ], errpatts = [], |
950 rules =[ |
950 rules =[ |
951 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
951 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*) |
952 \<^rule_thm>\<open>real_num_collect_assoc\<close>, |
952 \<^rule_thm>\<open>real_num_collect_assoc\<close>, |
953 (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
953 (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
954 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
954 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
955 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
955 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
956 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
956 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
957 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
957 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
958 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
958 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#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.function_empty), |
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 [ |
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.function_empty), |
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>, Calc_Binop.numeric "#add_")), |
1036 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1036 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#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")), |
1038 ("POWER" , (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))], |
1038 ("POWER" , (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))], |
1039 errpatts = [], |
1039 errpatts = [], |
1040 scr = Rule.Rfuns {init_state = init_state, |
1040 scr = Rule.Rfuns {init_state = init_state, |
1041 normal_form = normal_form, |
1041 normal_form = normal_form, |
1042 locate_rule = locate_rule, |
1042 locate_rule = locate_rule, |
1043 next_rule = next_rule, |
1043 next_rule = next_rule, |
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.function_empty), |
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>, Calc_Binop.numeric "#add_")), |
1077 ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1077 ("TIMES" ,(\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")), |
1078 ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
1078 ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")), |
1079 ("POWER" ,(\<^const_name>\<open>realpow\<close> , eval_binop "#power_"))], |
1079 ("POWER" ,(\<^const_name>\<open>realpow\<close> , Calc_Binop.numeric "#power_"))], |
1080 errpatts = [], |
1080 errpatts = [], |
1081 scr = Rule.Rfuns { |
1081 scr = Rule.Rfuns { |
1082 init_state = init_state, |
1082 init_state = init_state, |
1083 normal_form = normal_form, |
1083 normal_form = normal_form, |
1084 locate_rule = locate_rule, |
1084 locate_rule = locate_rule, |
1111 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
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> (Calc_Binop.numeric "#mult_"), |
1117 Rule.Rls_ order_mult_rls_, |
1117 Rule.Rls_ order_mult_rls_, |
1118 Rule.Rls_ simplify_power_, |
1118 Rule.Rls_ simplify_power_, |
1119 Rule.Rls_ calc_add_mult_pow_, |
1119 Rule.Rls_ calc_add_mult_pow_, |
1120 Rule.Rls_ reduce_012_mult_, |
1120 Rule.Rls_ reduce_012_mult_, |
1121 Rule.Rls_ order_add_rls_, |
1121 Rule.Rls_ order_add_rls_, |
1130 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
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> (Calc_Binop.numeric "#mult_"), |
1136 Rule.Rls_ order_mult_rls_, |
1136 Rule.Rls_ order_mult_rls_, |
1137 Rule.Rls_ simplify_power_, |
1137 Rule.Rls_ simplify_power_, |
1138 Rule.Rls_ calc_add_mult_pow_, |
1138 Rule.Rls_ calc_add_mult_pow_, |
1139 Rule.Rls_ reduce_012_mult_, |
1139 Rule.Rls_ reduce_012_mult_, |
1140 Rule.Rls_ order_add_rls_, |
1140 Rule.Rls_ order_add_rls_, |
1152 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
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> (Calc_Binop.numeric "#mult_"), |
1158 Rule.Rls_ order_mult_rls_, |
1158 Rule.Rls_ order_mult_rls_, |
1159 Rule.Rls_ simplify_power_, |
1159 Rule.Rls_ simplify_power_, |
1160 Rule.Rls_ calc_add_mult_pow_, |
1160 Rule.Rls_ calc_add_mult_pow_, |
1161 Rule.Rls_ reduce_012_mult_, |
1161 Rule.Rls_ reduce_012_mult_, |
1162 Rule.Rls_ order_add_rls_, |
1162 Rule.Rls_ order_add_rls_, |
1169 (*.a minimal ruleset for reverse rewriting of factions [2]; |
1169 (*.a minimal ruleset for reverse rewriting of factions [2]; |
1170 compare expand_binoms.*) |
1170 compare expand_binoms.*) |
1171 val rev_rew_p = |
1171 val rev_rew_p = |
1172 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI), |
1172 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI), |
1173 erls = Atools_erls, srls = Rule_Set.Empty, |
1173 erls = Atools_erls, srls = Rule_Set.Empty, |
1174 calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
1174 calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")), |
1175 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1175 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")), |
1176 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))*) |
1176 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))*) |
1177 ], errpatts = [], |
1177 ], errpatts = [], |
1178 rules = [ |
1178 rules = [ |
1179 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*) |
1179 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*) |
1180 \<^rule_thm>\<open>real_plus_binom_times1\<close>, (*"(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2"*) |
1180 \<^rule_thm>\<open>real_plus_binom_times1\<close>, (*"(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2"*) |
1181 \<^rule_thm>\<open>real_plus_binom_times2\<close>, (*"(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 2"*) |
1181 \<^rule_thm>\<open>real_plus_binom_times2\<close>, (*"(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 2"*) |
1187 |
1187 |
1188 \<^rule_thm>\<open>mult.assoc\<close>, (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*) |
1188 \<^rule_thm>\<open>mult.assoc\<close>, (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*) |
1189 Rule.Rls_ order_mult_rls_, |
1189 Rule.Rls_ order_mult_rls_, |
1190 (*Rule.Rls_ order_add_rls_,*) |
1190 (*Rule.Rls_ order_add_rls_,*) |
1191 |
1191 |
1192 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1192 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
1193 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1193 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
1194 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"), |
1194 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"), |
1195 |
1195 |
1196 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
1196 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*) |
1197 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*) |
1197 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*) |
1198 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
1198 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*) |
1199 |
1199 |
1202 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
1202 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
1203 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
1203 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
1204 |
1204 |
1205 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
1205 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*) |
1206 |
1206 |
1207 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1207 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
1208 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1208 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
1209 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"), |
1209 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"), |
1210 |
1210 |
1211 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
1211 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
1212 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
1212 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
1213 \<^rule_thm>\<open>add_0_left\<close> (*0 + z = z*) |
1213 \<^rule_thm>\<open>add_0_left\<close> (*0 + z = z*) |
1214 |
1214 |
1254 term)" |
1254 term)" |
1255 ML \<open> |
1255 ML \<open> |
1256 val expand_binoms = |
1256 val expand_binoms = |
1257 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), |
1257 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), |
1258 erls = Atools_erls, srls = Rule_Set.Empty, |
1258 erls = Atools_erls, srls = Rule_Set.Empty, |
1259 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), |
1259 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")), |
1260 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")), |
1260 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")), |
1261 ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_")) |
1261 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_")) |
1262 ], errpatts = [], |
1262 ], errpatts = [], |
1263 rules = [ |
1263 rules = [ |
1264 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
1264 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*) |
1265 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*) |
1265 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*) |
1266 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*) |
1266 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*) |
1283 *) |
1283 *) |
1284 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
1284 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*) |
1285 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
1285 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*) |
1286 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
1286 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*) |
1287 |
1287 |
1288 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1288 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
1289 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1289 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
1290 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"), |
1290 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"), |
1291 (*\<^rule_thm>\<open>mult.commute\<close>, |
1291 (*\<^rule_thm>\<open>mult.commute\<close>, |
1292 (*AC-rewriting*) |
1292 (*AC-rewriting*) |
1293 \<^rule_thm>\<open>real_mult_left_commute\<close>, |
1293 \<^rule_thm>\<open>real_mult_left_commute\<close>, |
1294 \<^rule_thm>\<open>mult.assoc\<close>, |
1294 \<^rule_thm>\<open>mult.assoc\<close>, |
1295 \<^rule_thm>\<open>add.commute\<close>, |
1295 \<^rule_thm>\<open>add.commute\<close>, |
1305 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*) |
1305 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*) |
1306 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
1306 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
1307 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
1307 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*) |
1308 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
1308 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*) |
1309 |
1309 |
1310 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), |
1310 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), |
1311 \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"), |
1311 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"), |
1312 \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")], |
1312 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")], |
1313 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})}; |
1313 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})}; |
1314 \<close> |
1314 \<close> |
1315 |
1315 |
1316 subsection \<open>add to Know_Store\<close> |
1316 subsection \<open>add to Know_Store\<close> |
1317 subsubsection \<open>rule-sets\<close> |
1317 subsubsection \<open>rule-sets\<close> |