1.1 --- a/src/Tools/isac/IsacKnowledge/Poly.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,147 +0,0 @@
1.4 -(* WN.020812: theorems in the Reals,
1.5 - necessary for special rule sets, in addition to Isabelle2002.
1.6 - !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.7 - !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
1.8 - !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.9 - xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
1.10 - changed by: Richard Lang 020912
1.11 -*)
1.12 -
1.13 -(*
1.14 - use_thy"IsacKnowledge/Poly";
1.15 - use_thy"Poly";
1.16 - use_thy_only"IsacKnowledge/Poly";
1.17 -
1.18 - remove_thy"Poly";
1.19 - use_thy"IsacKnowledge/Isac";
1.20 -
1.21 -
1.22 - use"ROOT.ML";
1.23 - cd"IsacKnowledge";
1.24 - *)
1.25 -
1.26 -Poly = Simplify +
1.27 -
1.28 -(*-------------------- consts-----------------------------------------------*)
1.29 -consts
1.30 -
1.31 - is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
1.32 - is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
1.33 - has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
1.34 - is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
1.35 -
1.36 - is'_multUnordered :: "real => bool" ("_ is'_multUnordered")
1.37 - is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
1.38 - is'_polyexp :: "real => bool" ("_ is'_polyexp")
1.39 -
1.40 - Expand'_binoms
1.41 - :: "['y, \
1.42 - \ 'y] => 'y"
1.43 - ("((Script Expand'_binoms (_ =))// \
1.44 - \ (_))" 9)
1.45 -
1.46 -(*-------------------- rules------------------------------------------------*)
1.47 -rules (*.not contained in Isabelle2002,
1.48 - stated as axioms, TODO: prove as theorems;
1.49 - theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
1.50 -
1.51 - realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
1.52 - realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
1.53 - realpow_addI_assoc_l "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
1.54 - realpow_addI_assoc_r "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
1.55 -
1.56 - realpow_oneI "r ^^^ 1 = r"
1.57 - realpow_zeroI "r ^^^ 0 = 1"
1.58 - realpow_eq_oneI "1 ^^^ n = 1"
1.59 - realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
1.60 - realpow_multI_poly "[| r is_polyexp; s is_polyexp |] ==> \
1.61 - \(r * s) ^^^ n = r ^^^ n * s ^^^ n"
1.62 - realpow_minus_oneI "-1 ^^^ (2 * n) = 1"
1.63 -
1.64 - realpow_twoI "r ^^^ 2 = r * r"
1.65 - realpow_twoI_assoc_l "r * (r * s) = r ^^^ 2 * s"
1.66 - realpow_twoI_assoc_r "s * r * r = s * r ^^^ 2"
1.67 - realpow_two_atom "r is_atom ==> r * r = r ^^^ 2"
1.68 - realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)"
1.69 - realpow_plus_1_assoc_l "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
1.70 - realpow_plus_1_assoc_l2 "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
1.71 - realpow_plus_1_assoc_r "s * r * r ^^^ m = s * r ^^^ (1 + m)"
1.72 - realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
1.73 - realpow_def_atom "[| Not (r is_atom); 1 < n |] \
1.74 - \ ==> r ^^^ n = r * r ^^^ (n + -1)"
1.75 - realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
1.76 -
1.77 -
1.78 - realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n"
1.79 - realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
1.80 -
1.81 -
1.82 -(* RL 020914 *)
1.83 - real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
1.84 - real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
1.85 - real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
1.86 - real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
1.87 - real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
1.88 - real_plus_binom_pow3_poly "[| a is_polyexp; b is_polyexp |] ==> \
1.89 - \(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
1.90 - real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
1.91 - real_minus_binom_pow3_p "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 + -1*b^^^3"
1.92 -(* real_plus_binom_pow "[| n is_const; 3 < n |] ==> \
1.93 - \(a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
1.94 - real_plus_binom_pow4 "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)"
1.95 - real_plus_binom_pow4_poly "[| a is_polyexp; b is_polyexp |] ==> \
1.96 - \(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)"
1.97 - real_plus_binom_pow5 "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
1.98 -
1.99 - real_plus_binom_pow5_poly "[| a is_polyexp; b is_polyexp |] ==> \
1.100 - \(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
1.101 -
1.102 - real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*)
1.103 - real_diff_minus "a - b = a + -1 * b"
1.104 - real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
1.105 - real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
1.106 - (*WN071229 changed for Schaerding -----vvv*)
1.107 - (*real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
1.108 - real_plus_binom_pow2 "(a + b)^^^2 = (a + b) * (a + b)"
1.109 - (*WN071229 changed for Schaerding -----^^^*)
1.110 - real_plus_binom_pow2_poly "[| a is_polyexp; b is_polyexp |] ==> \
1.111 - \(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
1.112 - real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
1.113 - real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
1.114 - real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
1.115 - real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
1.116 - real_plus_minus_binom1_p_p "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
1.117 - real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
1.118 - real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
1.119 - real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
1.120 - real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
1.121 - real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
1.122 -
1.123 - real_num_collect "[| l is_const; m is_const |] ==> \
1.124 - \l * n + m * n = (l + m) * n"
1.125 -(* FIXME.MG.0401: replace 'real_num_collect_assoc'
1.126 - by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
1.127 - real_num_collect_assoc "[| l is_const; m is_const |] ==> \
1.128 - \l * n + (m * n + k) = (l + m) * n + k"
1.129 - real_num_collect_assoc_l "[| l is_const; m is_const |] ==> \
1.130 - \l * n + (m * n + k) = (l + m)
1.131 - * n + k"
1.132 - real_num_collect_assoc_r "[| l is_const; m is_const |] ==> \
1.133 - \(k + m * n) + l * n = k + (l + m) * n"
1.134 - real_one_collect "m is_const ==> n + m * n = (1 + m) * n"
1.135 -(* FIXME.MG.0401: replace 'real_one_collect_assoc'
1.136 - by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
1.137 - real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
1.138 -
1.139 - real_one_collect_assoc_l "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
1.140 - real_one_collect_assoc_r "m is_const ==>(k + n) + m * n = k + (1 + m) * n"
1.141 -
1.142 -(* FIXME.MG.0401: replace 'real_mult_2_assoc'
1.143 - by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
1.144 - real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k"
1.145 - real_mult_2_assoc_l "z1 + (z1 + k) = 2 * z1 + k"
1.146 - real_mult_2_assoc_r "(k + z1) + z1 = k + 2 * z1"
1.147 -
1.148 - real_add_mult_distrib_poly "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
1.149 - real_add_mult_distrib2_poly "w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
1.150 -end