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