1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Aug 04 15:38:42 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Aug 04 16:48:37 2022 +0200
1.3 @@ -708,18 +708,18 @@
1.4 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls [
1.5 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.6 \<^rule_thm>\<open>real_unari_minus\<close>,
1.7 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.8 - \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
1.9 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.10 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
1.11 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.12 + \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
1.13 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.14 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
1.15
1.16 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [
1.17 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.18 \<^rule_thm>\<open>real_unari_minus\<close>,
1.19 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.20 - \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
1.21 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.22 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
1.23 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.24 + \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
1.25 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.26 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
1.27 \<close>
1.28 ML \<open>
1.29 val expand =
1.30 @@ -745,7 +745,7 @@
1.31 \<^rule_eval>\<open>ord_class.less\<close> (Prog_Expr.eval_equ "#less_"),
1.32 \<^rule_thm>\<open>not_false\<close>,
1.33 \<^rule_thm>\<open>not_true\<close>,
1.34 - \<^rule_eval>\<open>plus_class.plus\<close> (eval_binop "#add_")],
1.35 + \<^rule_eval>\<open>plus_class.plus\<close> (Calc_Binop.numeric "#add_")],
1.36 scr = Rule.Empty_Prog};
1.37
1.38 \<close> ML \<open>
1.39 @@ -838,15 +838,15 @@
1.40 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
1.41 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.42 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
1.43 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.44 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.45 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
1.46 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1.47 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1.48 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
1.49 ],
1.50 errpatts = [],
1.51 rules = [
1.52 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.53 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.54 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
1.55 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.56 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.57 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
1.58 scr = Rule.Empty_Prog};
1.59
1.60 val reduce_012_mult_ =
1.61 @@ -865,7 +865,7 @@
1.62 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
1.63 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.64 erls = Atools_erls, srls = Rule_Set.Empty,
1.65 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
1.66 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"))
1.67 ], errpatts = [],
1.68 rules = [
1.69 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
1.70 @@ -874,7 +874,7 @@
1.71 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1.72 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
1.73
1.74 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.75 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.76
1.77 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
1.78 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.79 @@ -943,9 +943,9 @@
1.80 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
1.81 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.82 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
1.83 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.84 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.85 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
1.86 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1.87 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1.88 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
1.89 ], errpatts = [],
1.90 rules =[
1.91 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
1.92 @@ -953,9 +953,9 @@
1.93 (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.94 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1.95 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
1.96 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.97 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.98 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
1.99 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.100 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.101 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
1.102 scr = Rule.Empty_Prog};
1.103 val reduce_012 =
1.104 Rule_Def.Repeat{id = "reduce_012", preconds = [],
1.105 @@ -1032,10 +1032,10 @@
1.106 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.107 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.108 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
1.109 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.110 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.111 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1.112 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1.113 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
1.114 - ("POWER" , (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))],
1.115 + ("POWER" , (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))],
1.116 errpatts = [],
1.117 scr = Rule.Rfuns {init_state = init_state,
1.118 normal_form = normal_form,
1.119 @@ -1073,10 +1073,10 @@
1.120 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
1.121 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
1.122 calc = [
1.123 - ("PLUS" ,(\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.124 - ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.125 + ("PLUS" ,(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1.126 + ("TIMES" ,(\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1.127 ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
1.128 - ("POWER" ,(\<^const_name>\<open>realpow\<close> , eval_binop "#power_"))],
1.129 + ("POWER" ,(\<^const_name>\<open>realpow\<close> , Calc_Binop.numeric "#power_"))],
1.130 errpatts = [],
1.131 scr = Rule.Rfuns {
1.132 init_state = init_state,
1.133 @@ -1113,7 +1113,7 @@
1.134 rules = [
1.135 Rule.Rls_ discard_minus,
1.136 Rule.Rls_ expand_poly_,
1.137 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.138 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.139 Rule.Rls_ order_mult_rls_,
1.140 Rule.Rls_ simplify_power_,
1.141 Rule.Rls_ calc_add_mult_pow_,
1.142 @@ -1132,7 +1132,7 @@
1.143 rules = [
1.144 Rule.Rls_ discard_minus,
1.145 Rule.Rls_ expand_poly_,
1.146 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.147 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.148 Rule.Rls_ order_mult_rls_,
1.149 Rule.Rls_ simplify_power_,
1.150 Rule.Rls_ calc_add_mult_pow_,
1.151 @@ -1154,7 +1154,7 @@
1.152 rules = [
1.153 Rule.Rls_ discard_minus,
1.154 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1.155 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.156 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.157 Rule.Rls_ order_mult_rls_,
1.158 Rule.Rls_ simplify_power_,
1.159 Rule.Rls_ calc_add_mult_pow_,
1.160 @@ -1171,9 +1171,9 @@
1.161 val rev_rew_p =
1.162 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1.163 erls = Atools_erls, srls = Rule_Set.Empty,
1.164 - calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.165 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.166 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))*)
1.167 + calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1.168 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1.169 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))*)
1.170 ], errpatts = [],
1.171 rules = [
1.172 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1.173 @@ -1189,9 +1189,9 @@
1.174 Rule.Rls_ order_mult_rls_,
1.175 (*Rule.Rls_ order_add_rls_,*)
1.176
1.177 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.178 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.179 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
1.180 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.181 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.182 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
1.183
1.184 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
1.185 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
1.186 @@ -1204,9 +1204,9 @@
1.187
1.188 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
1.189
1.190 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.191 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.192 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
1.193 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.194 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.195 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
1.196
1.197 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
1.198 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
1.199 @@ -1256,9 +1256,9 @@
1.200 val expand_binoms =
1.201 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.202 erls = Atools_erls, srls = Rule_Set.Empty,
1.203 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.204 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.205 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
1.206 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1.207 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1.208 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
1.209 ], errpatts = [],
1.210 rules = [
1.211 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
1.212 @@ -1285,9 +1285,9 @@
1.213 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
1.214 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
1.215
1.216 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.217 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.218 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
1.219 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.220 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.221 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
1.222 (*\<^rule_thm>\<open>mult.commute\<close>,
1.223 (*AC-rewriting*)
1.224 \<^rule_thm>\<open>real_mult_left_commute\<close>,
1.225 @@ -1307,9 +1307,9 @@
1.226 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1.227 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
1.228
1.229 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
1.230 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
1.231 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
1.232 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.233 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1.234 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
1.235 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})};
1.236 \<close>
1.237