1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 18:06:27 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 18:22:07 2021 +0200
1.3 @@ -745,11 +745,9 @@
1.4 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,
1.5 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
1.6
1.7 - Rule.Thm ("real_add_mult_distrib_poly",
1.8 - ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}),
1.9 + \<^rule_thm>\<open>real_add_mult_distrib_poly\<close>,
1.10 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.11 - Rule.Thm("real_add_mult_distrib2_poly",
1.12 - ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}),
1.13 + \<^rule_thm>\<open>real_add_mult_distrib2_poly\<close>,
1.14 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.15
1.16 \<^rule_thm>\<open>realpow_multI_poly\<close>,
1.17 @@ -773,12 +771,10 @@
1.18
1.19 \<^rule_thm>\<open>realpow_plus_1\<close>,
1.20 (*"r * r \<up> n = r \<up> (n + 1)"*)
1.21 - Rule.Thm ("realpow_plus_1_assoc_l",
1.22 - ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
1.23 + \<^rule_thm>\<open>realpow_plus_1_assoc_l\<close>,
1.24 (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)
1.25 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)
1.26 - Rule.Thm ("realpow_plus_1_assoc_l2",
1.27 - ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
1.28 + \<^rule_thm>\<open>realpow_plus_1_assoc_l2\<close>,
1.29 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
1.30
1.31 \<^rule_thm_sym>\<open>realpow_addI\<close>,
1.32 @@ -895,11 +891,9 @@
1.33 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
1.34 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>,
1.35 (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
1.36 - Rule.Thm ("real_plus_minus_binom1_p",
1.37 - ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
1.38 + \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>,
1.39 (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
1.40 - Rule.Thm ("real_plus_minus_binom2_p",
1.41 - ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
1.42 + \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>,
1.43 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
1.44
1.45 \<^rule_thm>\<open>minus_minus\<close>,
1.46 @@ -909,8 +903,7 @@
1.47 \<^rule_thm_sym>\<open>real_mult_minus1\<close>
1.48 (*- ?z = "-1 * ?z"*)
1.49
1.50 - (*Rule.Thm ("real_minus_add_distrib",
1.51 - ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
1.52 + (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)
1.53 (*"- (?x + ?y) = - ?x + - ?y"*)
1.54 (*\<^rule_thm>\<open>real_diff_plus\<close>*)
1.55 (*"a - b = a + -b"*)
1.56 @@ -968,11 +961,9 @@
1.57 (*"1 * z = z"*)
1.58 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
1.59 (*"-1 * z = - z"*)
1.60 - Rule.Thm ("minus_mult_left",
1.61 - ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
1.62 + Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
1.63 (*- (?x * ?y) = "- ?x * ?y"*)
1.64 - (*Rule.Thm ("real_minus_mult_cancel",
1.65 - ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
1.66 + (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
1.67 (*"- ?x * - ?y = ?x * ?y"*)---*)
1.68 \<^rule_thm>\<open>mult_zero_left\<close>,
1.69 (*"0 * z = 0"*)
1.70 @@ -1289,23 +1280,17 @@
1.71 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.72 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
1.73 ], errpatts = [],
1.74 - rules = [Rule.Thm ("real_plus_binom_pow2",
1.75 - ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
1.76 + rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,
1.77 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
1.78 - Rule.Thm ("real_plus_binom_times",
1.79 - ThmC.numerals_to_Free @{thm real_plus_binom_times}),
1.80 + \<^rule_thm>\<open>real_plus_binom_times\<close>,
1.81 (*"(a + b)*(a + b) = ...*)
1.82 - Rule.Thm ("real_minus_binom_pow2",
1.83 - ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
1.84 + \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
1.85 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
1.86 - Rule.Thm ("real_minus_binom_times",
1.87 - ThmC.numerals_to_Free @{thm real_minus_binom_times}),
1.88 + \<^rule_thm>\<open>real_minus_binom_times\<close>,
1.89 (*"(a - b)*(a - b) = ...*)
1.90 - Rule.Thm ("real_plus_minus_binom1",
1.91 - ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
1.92 + \<^rule_thm>\<open>real_plus_minus_binom1\<close>,
1.93 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
1.94 - Rule.Thm ("real_plus_minus_binom2",
1.95 - ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
1.96 + \<^rule_thm>\<open>real_plus_minus_binom2\<close>,
1.97 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
1.98 (*RL 020915*)
1.99 \<^rule_thm>\<open>real_pp_binom_times\<close>,
1.100 @@ -1320,8 +1305,7 @@
1.101 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
1.102 \<^rule_thm>\<open>real_plus_binom_pow3\<close>,
1.103 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
1.104 - Rule.Thm ("real_minus_binom_pow3",
1.105 - ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
1.106 + \<^rule_thm>\<open>real_minus_binom_pow3\<close>,
1.107 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
1.108
1.109
1.110 @@ -1345,8 +1329,7 @@
1.111 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
1.112 (*\<^rule_thm>\<open>mult.commute\<close>,
1.113 (*AC-rewriting*)
1.114 - Rule.Thm ("real_mult_left_commute",
1.115 - ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1.116 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
1.117 \<^rule_thm>\<open>mult.assoc\<close>,
1.118 \<^rule_thm>\<open>add.commute\<close>,
1.119 \<^rule_thm>\<open>add.left_commute\<close>,
1.120 @@ -1363,14 +1346,12 @@
1.121
1.122 \<^rule_thm>\<open>real_num_collect\<close>,
1.123 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
1.124 - Rule.Thm ("real_num_collect_assoc",
1.125 - ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
1.126 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
1.127 (*"[| l is_const; m is_const |] ==>
1.128 l * n + (m * n + k) = (l + m) * n + k"*)
1.129 \<^rule_thm>\<open>real_one_collect\<close>,
1.130 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.131 - Rule.Thm ("real_one_collect_assoc",
1.132 - ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
1.133 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
1.134 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.135
1.136 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),