diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/Poly.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,147 @@ +(* WN.020812: theorems in the Reals, + necessary for special rule sets, in addition to Isabelle2002. + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!! + !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002 + changed by: Richard Lang 020912 +*) + +(* + use_thy"Knowledge/Poly"; + use_thy"Poly"; + use_thy_only"Knowledge/Poly"; + + remove_thy"Poly"; + use_thy"Knowledge/Isac"; + + + use"ROOT.ML"; + cd"IsacKnowledge"; + *) + +Poly = Simplify + + +(*-------------------- consts-----------------------------------------------*) +consts + + is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _") + is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *) + has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *) + is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*) + + is'_multUnordered :: "real => bool" ("_ is'_multUnordered") + is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*) + is'_polyexp :: "real => bool" ("_ is'_polyexp") + + Expand'_binoms + :: "['y, \ + \ 'y] => 'y" + ("((Script Expand'_binoms (_ =))// \ + \ (_))" 9) + +(*-------------------- rules------------------------------------------------*) +rules (*.not contained in Isabelle2002, + stated as axioms, TODO: prove as theorems; + theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*) + + realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)" + realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m" + realpow_addI_assoc_l "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" + realpow_addI_assoc_r "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" + + realpow_oneI "r ^^^ 1 = r" + realpow_zeroI "r ^^^ 0 = 1" + realpow_eq_oneI "1 ^^^ n = 1" + realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n" + realpow_multI_poly "[| r is_polyexp; s is_polyexp |] ==> \ + \(r * s) ^^^ n = r ^^^ n * s ^^^ n" + realpow_minus_oneI "-1 ^^^ (2 * n) = 1" + + realpow_twoI "r ^^^ 2 = r * r" + realpow_twoI_assoc_l "r * (r * s) = r ^^^ 2 * s" + realpow_twoI_assoc_r "s * r * r = s * r ^^^ 2" + realpow_two_atom "r is_atom ==> r * r = r ^^^ 2" + realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)" + realpow_plus_1_assoc_l "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" + realpow_plus_1_assoc_l2 "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" + realpow_plus_1_assoc_r "s * r * r ^^^ m = s * r ^^^ (1 + m)" + realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" + realpow_def_atom "[| Not (r is_atom); 1 < n |] \ + \ ==> r ^^^ n = r * r ^^^ (n + -1)" + realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" + + + realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n" + realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" + + +(* RL 020914 *) + real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d" + real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d" + real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d" + real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d" + real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" + real_plus_binom_pow3_poly "[| a is_polyexp; b is_polyexp |] ==> \ + \(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" + real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" + real_minus_binom_pow3_p "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 + -1*b^^^3" +(* real_plus_binom_pow "[| n is_const; 3 < n |] ==> \ + \(a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *) + real_plus_binom_pow4 "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)" + real_plus_binom_pow4_poly "[| a is_polyexp; b is_polyexp |] ==> \ + \(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)" + 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)" + + real_plus_binom_pow5_poly "[| a is_polyexp; b is_polyexp |] ==> \ + \(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" + + real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*) + real_diff_minus "a - b = a + -1 * b" + real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" + real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" + (*WN071229 changed for Schaerding -----vvv*) + (*real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*) + real_plus_binom_pow2 "(a + b)^^^2 = (a + b) * (a + b)" + (*WN071229 changed for Schaerding -----^^^*) + real_plus_binom_pow2_poly "[| a is_polyexp; b is_polyexp |] ==> \ + \(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" + real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" + real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" + real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2" + real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2" + real_plus_minus_binom1_p_p "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" + real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2" + real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2" + real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" + real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" + real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" + + real_num_collect "[| l is_const; m is_const |] ==> \ + \l * n + m * n = (l + m) * n" +(* FIXME.MG.0401: replace 'real_num_collect_assoc' + by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *) + real_num_collect_assoc "[| l is_const; m is_const |] ==> \ + \l * n + (m * n + k) = (l + m) * n + k" + real_num_collect_assoc_l "[| l is_const; m is_const |] ==> \ + \l * n + (m * n + k) = (l + m) + * n + k" + real_num_collect_assoc_r "[| l is_const; m is_const |] ==> \ + \(k + m * n) + l * n = k + (l + m) * n" + real_one_collect "m is_const ==> n + m * n = (1 + m) * n" +(* FIXME.MG.0401: replace 'real_one_collect_assoc' + by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *) + real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m)* n + k" + + real_one_collect_assoc_l "m is_const ==> n + (m * n + k) = (1 + m) * n + k" + real_one_collect_assoc_r "m is_const ==>(k + n) + m * n = k + (1 + m) * n" + +(* FIXME.MG.0401: replace 'real_mult_2_assoc' + by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *) + real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k" + real_mult_2_assoc_l "z1 + (z1 + k) = 2 * z1 + k" + real_mult_2_assoc_r "(k + z1) + z1 = k + 2 * z1" + + real_add_mult_distrib_poly "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" + real_add_mult_distrib2_poly "w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2" +end