1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Jul 26 16:50:27 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Jul 27 09:30:15 2011 +0200
1.3 @@ -27,111 +27,111 @@
1.4 (_))" 9)
1.5
1.6 (*-------------------- rules------------------------------------------------*)
1.7 -axiomatization where (*.not contained in Isabelle2002,
1.8 +axioms(*axiomatization where*) (*.not contained in Isabelle2002,
1.9 stated as axioms, TODO: prove as theorems;
1.10 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
1.11
1.12 - realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
1.13 - realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
1.14 - realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
1.15 - realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
1.16 + realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" (*and*)
1.17 + realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" (*and*)
1.18 + realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" (*and*)
1.19 + realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" (*and*)
1.20
1.21 - realpow_oneI: "r ^^^ 1 = r" and
1.22 - realpow_zeroI: "r ^^^ 0 = 1" and
1.23 - realpow_eq_oneI: "1 ^^^ n = 1" and
1.24 - realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
1.25 + realpow_oneI: "r ^^^ 1 = r" (*and*)
1.26 + realpow_zeroI: "r ^^^ 0 = 1" (*and*)
1.27 + realpow_eq_oneI: "1 ^^^ n = 1" (*and*)
1.28 + realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" (*and*)
1.29 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
1.30 - (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
1.31 - realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" and
1.32 + (r * s) ^^^ n = r ^^^ n * s ^^^ n" (*and*)
1.33 + realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" (*and*)
1.34
1.35 - realpow_twoI: "r ^^^ 2 = r * r" and
1.36 - realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
1.37 - realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
1.38 - realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
1.39 - realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
1.40 - realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
1.41 - realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
1.42 - realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
1.43 - realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
1.44 + realpow_twoI: "r ^^^ 2 = r * r" (*and*)
1.45 + realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" (*and*)
1.46 + realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" (*and*)
1.47 + realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" (*and*)
1.48 + realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" (*and*)
1.49 + realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" (*and*)
1.50 + realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" (*and*)
1.51 + realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" (*and*)
1.52 + realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" (*and*)
1.53 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
1.54 - ==> r ^^^ n = r * r ^^^ (n + -1)" and
1.55 - realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
1.56 + ==> r ^^^ n = r * r ^^^ (n + -1)" (*and*)
1.57 + realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" (*and*)
1.58
1.59
1.60 - realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
1.61 - realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
1.62 + realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" (*and*)
1.63 + realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" (*and*)
1.64
1.65
1.66 (* RL 020914 *)
1.67 - real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
1.68 - real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
1.69 - real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
1.70 - real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
1.71 - real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
1.72 + real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" (*and*)
1.73 + real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" (*and*)
1.74 + real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" (*and*)
1.75 + real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" (*and*)
1.76 + real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" (*and*)
1.77 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
1.78 - (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
1.79 - real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
1.80 + (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" (*and*)
1.81 + real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" (*and*)
1.82 real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
1.83 - -1*b^^^3" and
1.84 + -1*b^^^3" (*and*)
1.85 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
1.86 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
1.87 real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
1.88 - *(a + b)" and
1.89 + *(a + b)" (*and*)
1.90 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
1.91 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
1.92 - *(a + b)" and
1.93 + *(a + b)" (*and*)
1.94 real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
1.95 - *(a^^^2 + 2*a*b + b^^^2)" and
1.96 + *(a^^^2 + 2*a*b + b^^^2)" (*and*)
1.97 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
1.98 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
1.99 - + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
1.100 - real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
1.101 - real_diff_minus: "a - b = a + -1 * b" and
1.102 - real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
1.103 - real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
1.104 + + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" (*and*)
1.105 + real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) (*and*)
1.106 + real_diff_minus: "a - b = a + -1 * b" (*and*)
1.107 + real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" (*and*)
1.108 + real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" (*and*)
1.109 (*WN071229 changed for Schaerding -----vvv*)
1.110 (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.111 - real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
1.112 + real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" (*and*)
1.113 (*WN071229 changed for Schaerding -----^^^*)
1.114 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
1.115 - (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
1.116 - real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
1.117 - real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
1.118 - real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
1.119 - real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
1.120 - real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
1.121 - real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
1.122 - real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
1.123 - real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
1.124 - real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
1.125 - real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
1.126 + (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" (*and*)
1.127 + real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" (*and*)
1.128 + real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" (*and*)
1.129 + real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" (*and*)
1.130 + real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" (*and*)
1.131 + real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" (*and*)
1.132 + real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" (*and*)
1.133 + real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" (*and*)
1.134 + real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" (*and*)
1.135 + real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" (*and*)
1.136 + real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" (*and*)
1.137
1.138 real_num_collect: "[| l is_const; m is_const |] ==>
1.139 - l * n + m * n = (l + m) * n" and
1.140 + l * n + m * n = (l + m) * n" (*and*)
1.141 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
1.142 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
1.143 real_num_collect_assoc: "[| l is_const; m is_const |] ==>
1.144 - l * n + (m * n + k) = (l + m) * n + k" and
1.145 + l * n + (m * n + k) = (l + m) * n + k" (*and*)
1.146 real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
1.147 l * n + (m * n + k) = (l + m)
1.148 - * n + k" and
1.149 + * n + k" (*and*)
1.150 real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
1.151 - (k + m * n) + l * n = k + (l + m) * n" and
1.152 - real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
1.153 + (k + m * n) + l * n = k + (l + m) * n" (*and*)
1.154 + real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" (*and*)
1.155 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
1.156 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
1.157 - real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
1.158 + real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" (*and*)
1.159
1.160 - real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
1.161 - real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
1.162 + real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" (*and*)
1.163 + real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" (*and*)
1.164
1.165 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
1.166 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
1.167 - real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
1.168 - real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
1.169 - real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
1.170 + real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" (*and*)
1.171 + real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" (*and*)
1.172 + real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" (*and*)
1.173
1.174 - real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
1.175 + real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" (*and*)
1.176 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
1.177
1.178 text {* remark on 'polynomials'