# HG changeset patch # User paulson # Date 1073641578 -3600 # Node ID 744c868ee0b7cd8d6919384603b0a642d369cd4f # Parent 1fff56703e29dad1eed35a6b1167c6cb1257069e Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Complex/CLim.ML Fri Jan 09 10:46:18 2004 +0100 @@ -852,13 +852,10 @@ Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"; by (asm_full_simp_tac - (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff, - complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym, + (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff, + minus_mult_right, complex_add_mult_distrib2 RS sym, complex_diff_def] - delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym] - delsimps [times_divide_eq_right, minus_mult_right RS sym] - -) 1); + delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1); by (etac (NSCLIM_const RS NSCLIM_mult) 1); qed "NSCDERIV_cmult"; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Complex/Complex.thy Fri Jan 09 10:46:18 2004 +0100 @@ -577,119 +577,8 @@ qed -lemma complex_mult_minus_one: "-(1::complex) * z = -z" -apply (simp (no_asm)) -done -declare complex_mult_minus_one [simp] - -lemma complex_mult_minus_one_right: "z * -(1::complex) = -z" -apply (subst complex_mult_commute) -apply (simp (no_asm)) -done -declare complex_mult_minus_one_right [simp] - -lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)" -apply (simp (no_asm)) -done -declare complex_minus_mult_cancel [simp] - lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)" -apply (simp (no_asm)) -done - - -lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)" -apply auto -apply (drule_tac f = "%x. x*inverse c" in arg_cong) -apply (simp add: complex_mult_ac) -done - -lemma complex_mult_right_cancel: "(c::complex) ~= 0 ==> (a*c=b*c) = (a=b)" -apply safe -apply (drule_tac f = "%x. x*inverse c" in arg_cong) -apply (simp add: complex_mult_ac) -done - -lemma complex_inverse_not_zero: "z ~= 0 ==> inverse(z::complex) ~= 0" -apply safe -apply (frule complex_mult_right_cancel [THEN iffD2]) -apply (erule_tac [2] V = "inverse z = 0" in thin_rl) -apply (assumption, auto) -done -declare complex_inverse_not_zero [simp] - -lemma complex_mult_not_zero: "!!x. [| x ~= 0; y ~= (0::complex) |] ==> x * y ~= 0" -apply safe -apply (drule_tac f = "%z. inverse x*z" in arg_cong) -apply (simp add: complex_mult_assoc [symmetric]) -done - -lemmas complex_mult_not_zeroE = complex_mult_not_zero [THEN notE, standard] - -lemma complex_inverse_inverse: "inverse(inverse (x::complex)) = x" -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "inverse x" in complex_mult_right_cancel [THEN iffD1]) -apply (erule complex_inverse_not_zero) -apply (auto dest: complex_inverse_not_zero) -done -declare complex_inverse_inverse [simp] - -lemma complex_inverse_one: "inverse(1::complex) = 1" -apply (unfold complex_one_def) -apply (simp (no_asm) add: complex_inverse) -done -declare complex_inverse_one [simp] - -lemma complex_minus_inverse: "inverse(-x) = -inverse(x::complex)" -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "-x" in complex_mult_right_cancel [THEN iffD1], force) -apply (subst complex_mult_inv_left, auto) -done - -lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)" -apply (rule inverse_mult_distrib) -done - - -subsection{*Division*} - -(*adding some of these theorems to simpset as for reals: - not 100% convinced for some*) - -lemma complex_times_divide1_eq: "(x::complex) * (y/z) = (x*y)/z" -apply (simp (no_asm) add: complex_divide_def complex_mult_assoc) -done - -lemma complex_times_divide2_eq: "(y/z) * (x::complex) = (y*x)/z" -apply (simp (no_asm) add: complex_divide_def complex_mult_ac) -done - -declare complex_times_divide1_eq [simp] complex_times_divide2_eq [simp] - -lemma complex_divide_divide1_eq: "(x::complex) / (y/z) = (x*z)/y" -apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_ac) -done - -lemma complex_divide_divide2_eq: "((x::complex) / y) / z = x/(y*z)" -apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_assoc) -done - -declare complex_divide_divide1_eq [simp] complex_divide_divide2_eq [simp] - -(** As with multiplication, pull minus signs OUT of the / operator **) - -lemma complex_minus_divide_eq: "(-x) / (y::complex) = - (x/y)" -apply (simp (no_asm) add: complex_divide_def) -done -declare complex_minus_divide_eq [simp] - -lemma complex_divide_minus_eq: "(x / -(y::complex)) = - (x/y)" -apply (simp (no_asm) add: complex_divide_def complex_minus_inverse) -done -declare complex_divide_minus_eq [simp] - -lemma complex_add_divide_distrib: "(x+y)/(z::complex) = x/z + y/z" -apply (simp (no_asm) add: complex_divide_def complex_add_mult_distrib) +apply (simp) done subsection{*Embedding Properties for @{term complex_of_real} Map*} @@ -713,7 +602,8 @@ done declare complex_of_real_zero [simp] -lemma complex_of_real_eq_iff: "(complex_of_real x = complex_of_real y) = (x = y)" +lemma complex_of_real_eq_iff: + "(complex_of_real x = complex_of_real y) = (x = y)" by (auto dest: inj_complex_of_real [THEN injD]) declare complex_of_real_eq_iff [iff] @@ -721,22 +611,25 @@ apply (simp (no_asm) add: complex_of_real_def complex_minus) done -lemma complex_of_real_inverse: "complex_of_real(inverse x) = inverse(complex_of_real x)" -apply (case_tac "x=0") -apply (simp add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) +lemma complex_of_real_inverse: + "complex_of_real(inverse x) = inverse(complex_of_real x)" +apply (case_tac "x=0", simp) apply (simp add: complex_inverse complex_of_real_def real_divide_def inverse_mult_distrib real_power_two) done -lemma complex_of_real_add: "complex_of_real x + complex_of_real y = complex_of_real (x + y)" +lemma complex_of_real_add: + "complex_of_real x + complex_of_real y = complex_of_real (x + y)" apply (simp (no_asm) add: complex_add complex_of_real_def) done -lemma complex_of_real_diff: "complex_of_real x - complex_of_real y = complex_of_real (x - y)" +lemma complex_of_real_diff: + "complex_of_real x - complex_of_real y = complex_of_real (x - y)" apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add) done -lemma complex_of_real_mult: "complex_of_real x * complex_of_real y = complex_of_real (x * y)" +lemma complex_of_real_mult: + "complex_of_real x * complex_of_real y = complex_of_real (x * y)" apply (simp (no_asm) add: complex_mult complex_of_real_def) done @@ -764,19 +657,18 @@ done declare complex_mod_zero [simp] -lemma complex_mod_one: "cmod(1) = 1" -by (unfold cmod_def, simp) -declare complex_mod_one [simp] +lemma complex_mod_one [simp]: "cmod(1) = 1" +by (simp add: cmod_def real_power_two) lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x" -apply (unfold complex_of_real_def) -apply (simp (no_asm) add: complex_mod) +apply (simp add: complex_of_real_def real_power_two complex_mod) done declare complex_mod_complex_of_real [simp] -lemma complex_of_real_abs: "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" -apply (simp (no_asm)) -done +lemma complex_of_real_abs: + "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" +by (simp) + subsection{*Conjugation is an Automorphism*} @@ -801,7 +693,8 @@ done declare complex_cnj_cnj [simp] -lemma complex_cnj_complex_of_real: "cnj (complex_of_real x) = complex_of_real x" +lemma complex_cnj_complex_of_real: + "cnj (complex_of_real x) = complex_of_real x" apply (unfold complex_of_real_def) apply (simp (no_asm) add: complex_cnj) done @@ -884,12 +777,6 @@ subsection{*Algebra*} -lemma complex_mult_zero_iff: "(x*y = (0::complex)) = (x = 0 | y = 0)" -apply auto -apply (auto intro: ccontr dest: complex_mult_not_zero) -done -declare complex_mult_zero_iff [iff] - lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))" apply (unfold complex_zero_def) apply (rule_tac z = x in eq_Abs_complex) @@ -913,13 +800,6 @@ subsection{*Modulus*} -(* -Goal "[| sqrt(x) = 0; 0 <= x |] ==> x = 0" -by (auto_tac (claset() addIs [real_sqrt_eq_zero_cancel], - simpset())); -qed "real_sqrt_eq_zero_cancel2"; -*) - lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)" apply (rule_tac z = x in eq_Abs_complex) apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def real_power_two) @@ -960,7 +840,7 @@ apply (rule_tac z = x in eq_Abs_complex) apply (rule_tac z = y in eq_Abs_complex) apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc) -apply (rule_tac n = 1 in realpow_Suc_cancel_eq) +apply (rule_tac n = 1 in power_inject_base) apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc) apply (auto simp add: real_diff_def real_power_two right_distrib left_distrib add_ac mult_ac) done @@ -1087,7 +967,7 @@ lemma complex_inverse_divide: "inverse(x/y) = y/(x::complex)" apply (unfold complex_divide_def) -apply (auto simp add: complex_inverse_distrib complex_mult_commute) +apply (auto simp add: inverse_mult_distrib complex_mult_commute) done declare complex_inverse_divide [simp] @@ -1105,7 +985,7 @@ lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0" apply (induct_tac "n") -apply (auto simp add: complex_mult_not_zero) +apply (auto simp add: ) done declare complexpow_not_zero [simp] declare complexpow_not_zero [intro] @@ -1135,7 +1015,7 @@ lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n" apply (induct_tac "n") -apply (auto simp add: complex_inverse_distrib) +apply (auto simp add: inverse_mult_distrib) done (*---------------------------------------------------------------------------*) @@ -1383,21 +1263,22 @@ by (unfold rcis_def cis_def, auto) declare Re_rcis [simp] -lemma Im_complex_polar: "Im(complex_of_real r * - (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * sin a" -apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac) -done -declare Im_complex_polar [simp] +lemma Im_complex_polar [simp]: + "Im(complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = + r * sin a" +by (auto simp add: complex_add_mult_distrib2 complex_of_real_mult mult_ac) -lemma Im_rcis: "Im(rcis r a) = r * sin a" +lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" by (unfold rcis_def cis_def, auto) -declare Im_rcis [simp] -lemma complex_mod_complex_polar: "cmod (complex_of_real r * - (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r" -apply (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult right_distrib [symmetric] realpow_mult complex_mult_ac mult_ac simp del: realpow_Suc) -done -declare complex_mod_complex_polar [simp] +lemma complex_mod_complex_polar [simp]: + "cmod (complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = + abs r" +by (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult + right_distrib [symmetric] power_mult_distrib mult_ac + simp del: realpow_Suc) lemma complex_mod_rcis: "cmod(rcis r a) = abs r" by (unfold rcis_def cis_def, auto) @@ -1728,9 +1609,6 @@ val complex_divide_zero = thm"complex_divide_zero"; val complex_minus_mult_eq1 = thm"complex_minus_mult_eq1"; val complex_minus_mult_eq2 = thm"complex_minus_mult_eq2"; -val complex_mult_minus_one = thm"complex_mult_minus_one"; -val complex_mult_minus_one_right = thm"complex_mult_minus_one_right"; -val complex_minus_mult_cancel = thm"complex_minus_mult_cancel"; val complex_minus_mult_commute = thm"complex_minus_mult_commute"; val complex_add_mult_distrib = thm"complex_add_mult_distrib"; val complex_add_mult_distrib2 = thm"complex_add_mult_distrib2"; @@ -1740,21 +1618,6 @@ val COMPLEX_DIVISION_BY_ZERO = thm"COMPLEX_DIVISION_BY_ZERO"; val complex_mult_inv_left = thm"complex_mult_inv_left"; val complex_mult_inv_right = thm"complex_mult_inv_right"; -val complex_mult_left_cancel = thm"complex_mult_left_cancel"; -val complex_mult_right_cancel = thm"complex_mult_right_cancel"; -val complex_inverse_not_zero = thm"complex_inverse_not_zero"; -val complex_mult_not_zero = thm"complex_mult_not_zero"; -val complex_inverse_inverse = thm"complex_inverse_inverse"; -val complex_inverse_one = thm"complex_inverse_one"; -val complex_minus_inverse = thm"complex_minus_inverse"; -val complex_inverse_distrib = thm"complex_inverse_distrib"; -val complex_times_divide1_eq = thm"complex_times_divide1_eq"; -val complex_times_divide2_eq = thm"complex_times_divide2_eq"; -val complex_divide_divide1_eq = thm"complex_divide_divide1_eq"; -val complex_divide_divide2_eq = thm"complex_divide_divide2_eq"; -val complex_minus_divide_eq = thm"complex_minus_divide_eq"; -val complex_divide_minus_eq = thm"complex_divide_minus_eq"; -val complex_add_divide_distrib = thm"complex_add_divide_distrib"; val inj_complex_of_real = thm"inj_complex_of_real"; val complex_of_real_one = thm"complex_of_real_one"; val complex_of_real_zero = thm"complex_of_real_zero"; @@ -1790,7 +1653,6 @@ val complex_cnj_zero = thm"complex_cnj_zero"; val complex_cnj_zero_iff = thm"complex_cnj_zero_iff"; val complex_mult_cnj = thm"complex_mult_cnj"; -val complex_mult_zero_iff = thm"complex_mult_zero_iff"; val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero"; val complex_diff_mult_distrib = thm"complex_diff_mult_distrib"; val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2"; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Complex/ComplexArith0.ML --- a/src/HOL/Complex/ComplexArith0.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Complex/ComplexArith0.ML Fri Jan 09 10:46:18 2004 +0100 @@ -168,7 +168,7 @@ Addsimps [complex_divide_minus1]; Goal "-1/(x::complex) = - (1/x)"; -by (simp_tac (simpset() addsimps [complex_divide_def, complex_minus_inverse]) 1); +by (simp_tac (simpset() addsimps [complex_divide_def, inverse_minus_eq]) 1); qed "complex_minus1_divide"; Addsimps [complex_minus1_divide]; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/HTranscendental.ML --- a/src/HOL/Hyperreal/HTranscendental.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/HTranscendental.ML Fri Jan 09 10:46:18 2004 +0100 @@ -4,6 +4,8 @@ Description : Nonstandard extensions of transcendental functions *) +val hpowr_Suc= thm"hpowr_Suc"; + (*-------------------------------------------------------------------------*) (* NS extension of square root function *) (*-------------------------------------------------------------------------*) @@ -44,8 +46,7 @@ qed "hypreal_sqrt_not_zero"; Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"; -by (forward_tac [hypreal_sqrt_not_zero] 1); -by (dres_inst_tac [("n1","2"),("r1","( *f* sqrt) x")] (hrealpow_inverse RS sym) 1); +by (cut_inst_tac [("n1","2"),("a1","( *f* sqrt) x")] (power_inverse RS sym) 1); by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset())); qed "hypreal_inverse_sqrt_pow2"; @@ -81,14 +82,14 @@ Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"; by (rtac hypreal_sqrt_approx_zero2 1); by (REPEAT(rtac hypreal_le_add_order 1)); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "hypreal_sqrt_sum_squares"; Addsimps [hypreal_sqrt_sum_squares]; Goal "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"; by (rtac hypreal_sqrt_approx_zero2 1); by (rtac hypreal_le_add_order 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "hypreal_sqrt_sum_squares2"; Addsimps [hypreal_sqrt_sum_squares2]; @@ -126,15 +127,15 @@ Addsimps [hypreal_sqrt_hyperpow_hrabs]; Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"; -by (res_inst_tac [("n","1")] hrealpow_Suc_cancel_eq 1); +by (res_inst_tac [("n","1")] power_inject_base 1); by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset())); -by (rtac (st_mult RS subst) 2); -by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 4); -by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 6); +by (rtac (st_mult RS subst) 1); +by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 3); +by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 5); by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le])); by (ALLGOALS(rtac (HFinite_square_iff RS iffD1))); -by (auto_tac (claset(),simpset() addsimps - [hypreal_sqrt_mult_distrib2 RS sym] +by (auto_tac (claset(), + simpset() addsimps [hypreal_sqrt_mult_distrib2 RS sym] delsimps [HFinite_square_iff])); qed "st_hypreal_sqrt"; @@ -169,7 +170,7 @@ Goal "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)"; by (rtac HFinite_hypreal_sqrt_iff 1); by (rtac hypreal_le_add_order 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "HFinite_sqrt_sum_squares"; Addsimps [HFinite_sqrt_sum_squares]; @@ -197,7 +198,7 @@ Goal "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)"; by (rtac Infinitesimal_hypreal_sqrt_iff 1); by (rtac hypreal_le_add_order 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "Infinitesimal_sqrt_sum_squares"; Addsimps [Infinitesimal_sqrt_sum_squares]; @@ -225,7 +226,7 @@ Goal "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)"; by (rtac HInfinite_hypreal_sqrt_iff 1); by (rtac hypreal_le_add_order 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [zero_le_square])); qed "HInfinite_sqrt_sum_squares"; Addsimps [HInfinite_sqrt_sum_squares]; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Fri Jan 09 10:46:18 2004 +0100 @@ -697,8 +697,12 @@ instance hypreal :: ordered_field proof fix x y z :: hypreal - show "x \ y ==> z + x \ z + y" by (rule hypreal_add_left_le_mono1) - show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2) + show "0 < (1::hypreal)" + by (unfold hypreal_one_def hypreal_zero_def hypreal_less_def, force) + show "x \ y ==> z + x \ z + y" + by (rule hypreal_add_left_le_mono1) + show "x < y ==> 0 < z ==> z * x < z * y" + by (simp add: hypreal_mult_less_mono2) show "\x\ = (if x < 0 then -x else x)" by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le) qed diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Fri Jan 09 01:28:24 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,547 +0,0 @@ -(* Title : HyperPow.ML - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Natural Powers of hyperreals theory - -Exponentials on the hyperreals -*) - -Goal "(0::hypreal) ^ (Suc n) = 0"; -by Auto_tac; -qed "hrealpow_zero"; -Addsimps [hrealpow_zero]; - -Goal "r ~= (0::hypreal) --> r ^ n ~= 0"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "hrealpow_not_zero"; - -Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n"; -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "hrealpow_inverse"; - -Goal "abs (r::hypreal) ^ n = abs (r ^ n)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "hrealpow_hrabs"; - -Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps mult_ac)); -qed "hrealpow_add"; - -Goal "(r::hypreal) ^ Suc 0 = r"; -by (Simp_tac 1); -qed "hrealpow_one"; -Addsimps [hrealpow_one]; - -Goal "(r::hypreal) ^ Suc (Suc 0) = r * r"; -by (Simp_tac 1); -qed "hrealpow_two"; - -Goal "(0::hypreal) <= r --> 0 <= r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff])); -qed_spec_mp "hrealpow_ge_zero"; - -Goal "(0::hypreal) < r --> 0 < r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff])); -qed_spec_mp "hrealpow_gt_zero"; - -Goal "x <= y & (0::hypreal) < x --> x ^ n <= y ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addSIs [mult_mono], simpset())); -by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1); -qed_spec_mp "hrealpow_le"; - -Goal "x < y & (0::hypreal) < x & 0 < n --> x ^ n < y ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I], - simpset() addsimps [hrealpow_gt_zero])); -qed "hrealpow_less"; - -Goal "1 ^ n = (1::hypreal)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "hrealpow_eq_one"; -Addsimps [hrealpow_eq_one]; - -Goal "abs(-(1 ^ n)) = (1::hypreal)"; -by Auto_tac; -qed "hrabs_minus_hrealpow_one"; -Addsimps [hrabs_minus_hrealpow_one]; - -Goal "abs(-1 ^ n) = (1::hypreal)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "hrabs_hrealpow_minus_one"; -Addsimps [hrabs_hrealpow_minus_one]; - -Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps mult_ac)); -qed "hrealpow_mult"; - -Goal "(0::hypreal) <= r ^ Suc (Suc 0)"; -by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff])); -qed "hrealpow_two_le"; -Addsimps [hrealpow_two_le]; - -Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"; -by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1); -qed "hrealpow_two_le_add_order"; -Addsimps [hrealpow_two_le_add_order]; - -Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"; -by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1); -qed "hrealpow_two_le_add_order2"; -Addsimps [hrealpow_two_le_add_order2]; - -Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"; -by (auto_tac (claset() addIs [order_antisym], simpset())); -qed "hypreal_add_nonneg_eq_0_iff"; - -Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; -by (simp_tac (HOL_ss addsimps [zero_le_square, hypreal_le_add_order, - hypreal_add_nonneg_eq_0_iff]) 1); -by Auto_tac; -qed "hypreal_three_squares_add_zero_iff"; - -Goal "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = (x = 0 & y = 0 & z = 0)"; -by (simp_tac (HOL_ss addsimps - [hypreal_three_squares_add_zero_iff, hrealpow_two]) 1); -qed "hrealpow_three_squares_add_zero_iff"; -Addsimps [hrealpow_three_squares_add_zero_iff]; - -Goal "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"; -by (auto_tac (claset(), - simpset() addsimps [hrabs_def, zero_le_mult_iff])); -qed "hrabs_hrealpow_two"; -Addsimps [hrabs_hrealpow_two]; - -Goal "abs(x) ^ Suc (Suc 0) = (x::hypreal) ^ Suc (Suc 0)"; -by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1] - delsimps [hpowr_Suc]) 1); -qed "hrealpow_two_hrabs"; -Addsimps [hrealpow_two_hrabs]; - -Goal "(1::hypreal) < r ==> 1 < r ^ Suc (Suc 0)"; -by (auto_tac (claset(), simpset() addsimps [hrealpow_two])); -by (res_inst_tac [("y","1*1")] order_le_less_trans 1); -by (rtac hypreal_mult_less_mono 2); -by Auto_tac; -qed "hrealpow_two_gt_one"; - -Goal "(1::hypreal) <= r ==> 1 <= r ^ Suc (Suc 0)"; -by (etac (order_le_imp_less_or_eq RS disjE) 1); -by (etac (hrealpow_two_gt_one RS order_less_imp_le) 1); -by Auto_tac; -qed "hrealpow_two_ge_one"; - -Goal "(1::hypreal) <= 2 ^ n"; -by (res_inst_tac [("y","1 ^ n")] order_trans 1); -by (rtac hrealpow_le 2); -by Auto_tac; -qed "two_hrealpow_ge_one"; - -Goal "hypreal_of_nat n < 2 ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_of_nat_Suc, left_distrib])); -by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1); -by (arith_tac 1); -qed "two_hrealpow_gt"; -Addsimps [two_hrealpow_gt,two_hrealpow_ge_one]; - -Goal "-1 ^ (2*n) = (1::hypreal)"; -by (induct_tac "n" 1); -by Auto_tac; -qed "hrealpow_minus_one"; - -Goal "n+n = (2*n::nat)"; -by Auto_tac; -qed "double_lemma"; - -(*ugh: need to get rid fo the n+n*) -Goal "-1 ^ (n + n) = (1::hypreal)"; -by (auto_tac (claset(), - simpset() addsimps [double_lemma, hrealpow_minus_one])); -qed "hrealpow_minus_one2"; -Addsimps [hrealpow_minus_one2]; - -Goal "(-(x::hypreal)) ^ Suc (Suc 0) = x ^ Suc (Suc 0)"; -by Auto_tac; -qed "hrealpow_minus_two"; -Addsimps [hrealpow_minus_two]; - -Goal "(0::hypreal) < r & r < 1 --> r ^ Suc n < r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_mult_less_mono2])); -qed_spec_mp "hrealpow_Suc_less"; - -Goal "(0::hypreal) <= r & r < 1 --> r ^ Suc n <= r ^ n"; -by (induct_tac "n" 1); -by (auto_tac (claset() addIs [order_less_imp_le] - addSDs [order_le_imp_less_or_eq,hrealpow_Suc_less], - simpset() addsimps [hypreal_mult_less_mono2])); -qed_spec_mp "hrealpow_Suc_le"; - -Goal "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"; -by (induct_tac "m" 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_one_def, hypreal_mult])); -qed "hrealpow"; - -Goal "(x + (y::hypreal)) ^ Suc (Suc 0) = \ -\ x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"; -by (simp_tac (simpset() addsimps - [right_distrib, left_distrib, - hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1); -qed "hrealpow_sum_square_expand"; - - -(*** Literal arithmetic involving powers, type hypreal ***) - -Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"; -by (induct_tac "n" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib]))); -qed "hypreal_of_real_power"; -Addsimps [hypreal_of_real_power]; - -Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"; -by (simp_tac (HOL_ss addsimps [hypreal_number_of_def, - hypreal_of_real_power]) 1); -qed "power_hypreal_of_real_number_of"; - -Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of]; - -(*--------------------------------------------------------------- - we'll prove the following theorem by going down to the - level of the ultrafilter and relying on the analogous - property for the real rather than prove it directly - using induction: proof is much simpler this way! - ---------------------------------------------------------------*) -Goal "[|(0::hypreal) <= x; 0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y"; -by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hrealpow,hypreal_le,hypreal_mult])); -by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1); -qed "hrealpow_increasing"; - -(*By antisymmetry with the above we conclude x=y, replacing the deleted - theorem hrealpow_Suc_cancel_eq*) - -Goal "x : HFinite --> x ^ n : HFinite"; -by (induct_tac "n" 1); -by (auto_tac (claset() addIs [HFinite_mult], simpset())); -qed_spec_mp "hrealpow_HFinite"; - -(*--------------------------------------------------------------- - Hypernaturals Powers - --------------------------------------------------------------*) -Goalw [congruent_def] - "congruent hyprel \ -\ (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"; -by (auto_tac (claset() addSIs [ext], simpset())); -by (ALLGOALS(Fuf_tac)); -qed "hyperpow_congruent"; - -Goalw [hyperpow_def] - "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = \ -\ Abs_hypreal(hyprel``{%n. X n ^ Y n})"; -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI], - simpset() addsimps [hyprel_in_hypreal RS - Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent])); -by (Fuf_tac 1); -qed "hyperpow"; - -Goalw [hypnat_one_def] "(0::hypreal) pow (n + (1::hypnat)) = 0"; -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add])); -qed "hyperpow_zero"; -Addsimps [hyperpow_zero]; - -Goal "r ~= (0::hypreal) --> r pow n ~= 0"; -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hyperpow])); -by (dtac FreeUltrafilterNat_Compl_mem 1); -by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE], - simpset()) 1); -qed_spec_mp "hyperpow_not_zero"; - -Goal "r ~= (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"; -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem], - simpset() addsimps [hypreal_inverse,hyperpow])); -by (rtac FreeUltrafilterNat_subset 1); -by (auto_tac (claset() addDs [realpow_not_zero] - addIs [realpow_inverse], - simpset())); -qed "hyperpow_inverse"; - -Goal "abs r pow n = abs (r pow n)"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs RS sym])); -qed "hyperpow_hrabs"; - -Goal "r pow (n + m) = (r pow n) * (r pow m)"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add])); -qed "hyperpow_add"; - -Goalw [hypnat_one_def] "r pow (1::hypnat) = r"; -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hyperpow])); -qed "hyperpow_one"; -Addsimps [hyperpow_one]; - -Goalw [hypnat_one_def] - "r pow ((1::hypnat) + (1::hypnat)) = r * r"; -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hyperpow,hypnat_add, hypreal_mult])); -qed "hyperpow_two"; - -Goal "(0::hypreal) < r --> 0 < r pow n"; -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero], - simpset() addsimps [hyperpow,hypreal_less, hypreal_le])); -qed_spec_mp "hyperpow_gt_zero"; - -Goal "(0::hypreal) <= r --> 0 <= r pow n"; -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero], - simpset() addsimps [hyperpow,hypreal_le])); -qed "hyperpow_ge_zero"; - -Goal "(0::hypreal) < x & x <= y --> x pow n <= y pow n"; -by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hyperpow,hypreal_le,hypreal_less])); -by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1 - THEN assume_tac 1); -by (auto_tac (claset() addIs [realpow_le], simpset())); -qed_spec_mp "hyperpow_le"; - -Goal "1 pow n = (1::hypreal)"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_one_def, hyperpow])); -qed "hyperpow_eq_one"; -Addsimps [hyperpow_eq_one]; - -Goal "abs(-(1 pow n)) = (1::hypreal)"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (auto_tac (claset(), - simpset() addsimps [hyperpow, hypreal_hrabs, hypreal_one_def])); -qed "hrabs_minus_hyperpow_one"; -Addsimps [hrabs_minus_hyperpow_one]; - -Goal "abs(-1 pow n) = (1::hypreal)"; -by (subgoal_tac "abs((- (1::hypreal)) pow n) = (1::hypreal)" 1); -by (Asm_full_simp_tac 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_one_def, hyperpow,hypreal_minus, - hypreal_hrabs])); -qed "hrabs_hyperpow_minus_one"; -Addsimps [hrabs_hyperpow_minus_one]; - -Goal "(r * s) pow n = (r pow n) * (s pow n)"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","s")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hyperpow, hypreal_mult,realpow_mult])); -qed "hyperpow_mult"; - -Goal "(0::hypreal) <= r pow ((1::hypnat) + (1::hypnat))"; -by (auto_tac (claset(), - simpset() addsimps [hyperpow_two, zero_le_mult_iff])); -qed "hyperpow_two_le"; -Addsimps [hyperpow_two_le]; - -Goal "abs(x pow ((1::hypnat) + (1::hypnat))) = x pow ((1::hypnat) + (1::hypnat))"; -by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1); -qed "hrabs_hyperpow_two"; -Addsimps [hrabs_hyperpow_two]; - -Goal "abs(x) pow ((1::hypnat) + (1::hypnat)) = x pow ((1::hypnat) + (1::hypnat))"; -by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1); -qed "hyperpow_two_hrabs"; -Addsimps [hyperpow_two_hrabs]; - -(*? very similar to hrealpow_two_gt_one *) -Goal "(1::hypreal) < r ==> 1 < r pow ((1::hypnat) + (1::hypnat))"; -by (auto_tac (claset(), simpset() addsimps [hyperpow_two])); -by (res_inst_tac [("y","1*1")] order_le_less_trans 1); -by (rtac hypreal_mult_less_mono 2); -by Auto_tac; -qed "hyperpow_two_gt_one"; - -Goal "(1::hypreal) <= r ==> 1 <= r pow ((1::hypnat) + (1::hypnat))"; -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] - addIs [hyperpow_two_gt_one,order_less_imp_le], - simpset())); -qed "hyperpow_two_ge_one"; - -Goal "(1::hypreal) <= 2 pow n"; -by (res_inst_tac [("y","1 pow n")] order_trans 1); -by (rtac hyperpow_le 2); -by Auto_tac; -qed "two_hyperpow_ge_one"; -Addsimps [two_hyperpow_ge_one]; - -Addsimps [simplify (simpset()) realpow_minus_one]; - -Goal "-1 pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)"; -by (subgoal_tac "(-((1::hypreal))) pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)" 1); -by (Asm_full_simp_tac 1); -by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1); -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (auto_tac (claset(), - simpset() addsimps [double_lemma, hyperpow, hypnat_add, - hypreal_minus])); -qed "hyperpow_minus_one2"; -Addsimps [hyperpow_minus_one2]; - -Goalw [hypnat_one_def] - "(0::hypreal) < r & r < 1 --> r pow (n + (1::hypnat)) < r pow n"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less] - addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset], - simpset() addsimps [hypreal_zero_def, hypreal_one_def, - hyperpow, hypreal_less, hypnat_add])); -qed_spec_mp "hyperpow_Suc_less"; - -Goalw [hypnat_one_def] - "0 <= r & r < (1::hypreal) --> r pow (n + (1::hypnat)) <= r pow n"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] - addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset], - simpset() addsimps [hypreal_zero_def, hypreal_one_def, hyperpow, - hypreal_le,hypnat_add, hypreal_less])); -qed_spec_mp "hyperpow_Suc_le"; - -Goalw [hypnat_one_def] - "(0::hypreal) <= r & r < 1 & n < N --> r pow N <= r pow n"; -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hyperpow, hypreal_le,hypreal_less, - hypnat_less, hypreal_zero_def, hypreal_one_def])); -by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); -by (etac FreeUltrafilterNat_Int 1); -by (auto_tac (claset() addSDs [conjI RS realpow_less_le], simpset())); -qed_spec_mp "hyperpow_less_le"; - -Goal "[| (0::hypreal) <= r; r < 1 |] \ -\ ==> ALL N n. n < N --> r pow N <= r pow n"; -by (blast_tac (claset() addSIs [hyperpow_less_le]) 1); -qed "hyperpow_less_le2"; - -Goal "[| 0 <= r; r < (1::hypreal); N : HNatInfinite |] \ -\ ==> ALL n: Nats. r pow N <= r pow n"; -by (auto_tac (claset() addSIs [hyperpow_less_le], - simpset() addsimps [HNatInfinite_iff])); -qed "hyperpow_SHNat_le"; - -Goalw [hypreal_of_real_def,hypnat_of_nat_def] - "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"; -by (auto_tac (claset(), simpset() addsimps [hyperpow])); -qed "hyperpow_realpow"; - -Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals"; -by (simp_tac (simpset() delsimps [hypreal_of_real_power] - addsimps [hyperpow_realpow]) 1); -qed "hyperpow_SReal"; -Addsimps [hyperpow_SReal]; - -Goal "N : HNatInfinite ==> (0::hypreal) pow N = 0"; -by (dtac HNatInfinite_is_Suc 1); -by Auto_tac; -qed "hyperpow_zero_HNatInfinite"; -Addsimps [hyperpow_zero_HNatInfinite]; - -Goal "[| (0::hypreal) <= r; r < 1; n <= N |] ==> r pow N <= r pow n"; -by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1); -by (auto_tac (claset() addIs [hyperpow_less_le], simpset())); -qed "hyperpow_le_le"; - -Goal "[| (0::hypreal) < r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r"; -by (dres_inst_tac [("n","(1::hypnat)")] (order_less_imp_le RS hyperpow_le_le) 1); -by Auto_tac; -qed "hyperpow_Suc_le_self"; - -Goal "[| (0::hypreal) <= r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r"; -by (dres_inst_tac [("n","(1::hypnat)")] hyperpow_le_le 1); -by Auto_tac; -qed "hyperpow_Suc_le_self2"; - -Goalw [Infinitesimal_def] - "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x"; -by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2], - simpset() addsimps [hyperpow_hrabs RS sym, - hypnat_gt_zero_iff2, abs_ge_zero])); -qed "lemma_Infinitesimal_hyperpow"; - -Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal"; -by (rtac hrabs_le_Infinitesimal 1); -by (rtac lemma_Infinitesimal_hyperpow 2); -by Auto_tac; -qed "Infinitesimal_hyperpow"; - -Goalw [hypnat_of_nat_def] - "(x ^ n : Infinitesimal) = (x pow (hypnat_of_nat n) : Infinitesimal)"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow])); -qed "hrealpow_hyperpow_Infinitesimal_iff"; - -Goal "[| x : Infinitesimal; 0 < n |] ==> x ^ n : Infinitesimal"; -by (auto_tac (claset() addSIs [Infinitesimal_hyperpow], - simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff, - hypnat_of_nat_less_iff,hypnat_of_nat_zero] - delsimps [hypnat_of_nat_less_iff RS sym])); -qed "Infinitesimal_hrealpow"; - -(* MOVE UP *) -Goal "(0::hypreal) <= x * x"; -by (auto_tac (claset(),simpset() addsimps - [zero_le_mult_iff])); -qed "hypreal_mult_self_ge_zero"; -Addsimps [hypreal_mult_self_ge_zero]; - -Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps - [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num])); -by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq], - simpset()) 1); -qed "hrealpow_Suc_cancel_eq"; - diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/HyperPow.thy Fri Jan 09 10:46:18 2004 +0100 @@ -4,33 +4,459 @@ Description : Powers theory for hyperreals *) -HyperPow = HRealAbs + HyperNat + RealPow + +header{*Exponentials on the Hyperreals*} + +theory HyperPow = HRealAbs + HyperNat + RealPow: -(** First: hypnat is linearly ordered **) +instance hypnat :: order + by (intro_classes, + (assumption | + rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+) -instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym, - hypnat_less_le) -instance hypnat :: linorder (hypnat_le_linear) + +text{*Type @{typ hypnat} is linearly ordered*} +instance hypnat :: linorder + by (intro_classes, rule hypnat_le_linear) -instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc, - hypnat_add_zero_left) +instance hypnat :: plus_ac0 + by (intro_classes, + (assumption | + rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+) -instance hypreal :: {power} +instance hypreal :: power .. consts hpowr :: "[hypreal,nat] => hypreal" primrec - hpowr_0 "r ^ 0 = (1::hypreal)" - hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)" + hpowr_0: "r ^ 0 = (1::hypreal)" + hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" + + +instance hypreal :: ringpower +proof + fix z :: hypreal + fix n :: nat + show "z^0 = 1" by simp + show "z^(Suc n) = z * (z^n)" by simp +qed + consts - "pow" :: [hypreal,hypnat] => hypreal (infixr 80) + "pow" :: "[hypreal,hypnat] => hypreal" (infixr 80) defs (* hypernatural powers of hyperreals *) - hyperpow_def - "(R::hypreal) pow (N::hypnat) - == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N). - hyprel``{%n::nat. (X n) ^ (Y n)})" + hyperpow_def: + "(R::hypreal) pow (N::hypnat) == + Abs_hypreal(\X \ Rep_hypreal(R). \Y \ Rep_hypnat(N). + hyprel``{%n::nat. (X n) ^ (Y n)})" + +lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" +apply (simp (no_asm)) +done + +lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)" +apply (simp add: power_abs); +done + +lemma hrealpow_two_le: "(0::hypreal) \ r ^ Suc (Suc 0)" +apply (auto simp add: zero_le_mult_iff) +done +declare hrealpow_two_le [simp] + +lemma hrealpow_two_le_add_order: + "(0::hypreal) \ u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" +apply (simp only: hrealpow_two_le hypreal_le_add_order) +done +declare hrealpow_two_le_add_order [simp] + +lemma hrealpow_two_le_add_order2: + "(0::hypreal) \ u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" +apply (simp only: hrealpow_two_le hypreal_le_add_order) +done +declare hrealpow_two_le_add_order2 [simp] + +lemma hypreal_add_nonneg_eq_0_iff: + "[| 0 \ x; 0 \ y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" +apply arith +done + +text{*FIXME: DELETE THESE*} +lemma hypreal_three_squares_add_zero_iff: + "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))" +apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff) +apply auto +done + +lemma hrealpow_three_squares_add_zero_iff [simp]: + "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = + (x = 0 & y = 0 & z = 0)" +by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two) + + +lemma hrabs_hrealpow_two [simp]: + "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)" +by (simp add: abs_mult) + +lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \ 2 ^ n" +by (insert power_increasing [of 0 n "2::hypreal"], simp) + +lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n" +apply (induct_tac "n") +apply (auto simp add: hypreal_of_nat_Suc left_distrib) +apply (cut_tac n = "n" in two_hrealpow_ge_one) +apply arith +done +declare two_hrealpow_gt [simp] + +lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)" +apply (induct_tac "n") +apply auto +done + +lemma double_lemma: "n+n = (2*n::nat)" +apply auto +done + +(*ugh: need to get rid fo the n+n*) +lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)" +apply (auto simp add: double_lemma hrealpow_minus_one) +done +declare hrealpow_minus_one2 [simp] + +lemma hrealpow: + "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})" +apply (induct_tac "m") +apply (auto simp add: hypreal_one_def hypreal_mult) +done + +lemma hrealpow_sum_square_expand: + "(x + (y::hypreal)) ^ Suc (Suc 0) = + x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" +by (simp add: right_distrib left_distrib hypreal_of_nat_Suc) + + +subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*} + +lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n" +apply (induct_tac "n") +apply (simp_all add: nat_mult_distrib) +done +declare hypreal_of_real_power [simp] + +lemma power_hypreal_of_real_number_of: + "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" +by (simp only: hypreal_number_of_def hypreal_of_real_power) + +declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp] + +lemma hrealpow_HFinite: "x \ HFinite ==> x ^ n \ HFinite" +apply (induct_tac "n") +apply (auto intro: HFinite_mult) +done + + +subsection{*Powers with Hypernatural Exponents*} + +lemma hyperpow_congruent: + "congruent hyprel + (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})" +apply (unfold congruent_def) +apply (auto intro!: ext) +apply fuf+ +done + +lemma hyperpow: + "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = + Abs_hypreal(hyprel``{%n. X n ^ Y n})" +apply (unfold hyperpow_def) +apply (rule_tac f = "Abs_hypreal" in arg_cong) +apply (auto intro!: lemma_hyprel_refl bexI + simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel + hyperpow_congruent) +apply fuf +done + +lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0" +apply (unfold hypnat_one_def) +apply (simp (no_asm) add: hypreal_zero_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (auto simp add: hyperpow hypnat_add) +done +declare hyperpow_zero [simp] + +lemma hyperpow_not_zero [rule_format (no_asm)]: + "r \ (0::hypreal) --> r pow n \ 0" +apply (simp (no_asm) add: hypreal_zero_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto simp add: hyperpow) +apply (drule FreeUltrafilterNat_Compl_mem) +apply ultra +done + +lemma hyperpow_inverse: + "r \ (0::hypreal) --> inverse(r pow n) = (inverse r) pow n" +apply (simp (no_asm) add: hypreal_zero_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow) +apply (rule FreeUltrafilterNat_subset) +apply (auto dest: realpow_not_zero intro: power_inverse) +done + +lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)" +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric]) +done + +lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)" +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "m" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add) +done + +lemma hyperpow_one: "r pow (1::hypnat) = r" +apply (unfold hypnat_one_def) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto simp add: hyperpow) +done +declare hyperpow_one [simp] + +lemma hyperpow_two: + "r pow ((1::hypnat) + (1::hypnat)) = r * r" +apply (unfold hypnat_one_def) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto simp add: hyperpow hypnat_add hypreal_mult) +done + +lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n" +apply (simp add: hypreal_zero_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto elim!: FreeUltrafilterNat_subset zero_less_power + simp add: hyperpow hypreal_less hypreal_le) +done + +lemma hyperpow_ge_zero: "(0::hypreal) \ r ==> 0 \ r pow n" +apply (simp add: hypreal_zero_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto elim!: FreeUltrafilterNat_subset zero_le_power + simp add: hyperpow hypreal_le) +done + +lemma hyperpow_le: "[|(0::hypreal) < x; x \ y|] ==> x pow n \ y pow n" +apply (simp add: hypreal_zero_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (auto simp add: hyperpow hypreal_le hypreal_less) +apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption) +apply (auto intro: power_mono) +done + +lemma hyperpow_eq_one: "1 pow n = (1::hypreal)" +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (auto simp add: hypreal_one_def hyperpow) +done +declare hyperpow_eq_one [simp] + +lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)" +apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ") +apply simp +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs) +done +declare hrabs_hyperpow_minus_one [simp] + +lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)" +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (rule_tac z = "s" in eq_Abs_hypreal) +apply (auto simp add: hyperpow hypreal_mult power_mult_distrib) +done + +lemma hyperpow_two_le: "(0::hypreal) \ r pow ((1::hypnat) + (1::hypnat))" +apply (auto simp add: hyperpow_two zero_le_mult_iff) +done +declare hyperpow_two_le [simp] + +lemma hrabs_hyperpow_two: + "abs(x pow (1 + 1)) = x pow (1 + 1)" +apply (simp (no_asm) add: hrabs_eqI1) +done +declare hrabs_hyperpow_two [simp] + +lemma hyperpow_two_hrabs: + "abs(x) pow (1 + 1) = x pow (1 + 1)" +apply (simp add: hyperpow_hrabs) +done +declare hyperpow_two_hrabs [simp] + +lemma hyperpow_two_gt_one: + "(1::hypreal) < r ==> 1 < r pow (1 + 1)" +apply (auto simp add: hyperpow_two) +apply (rule_tac y = "1*1" in order_le_less_trans) +apply (rule_tac [2] hypreal_mult_less_mono) +apply auto +done + +lemma hyperpow_two_ge_one: + "(1::hypreal) \ r ==> 1 \ r pow (1 + 1)" +apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le) +done + +lemma two_hyperpow_ge_one: "(1::hypreal) \ 2 pow n" +apply (rule_tac y = "1 pow n" in order_trans) +apply (rule_tac [2] hyperpow_le) +apply auto +done +declare two_hyperpow_ge_one [simp] + +lemma hyperpow_minus_one2: + "-1 pow ((1 + 1)*n) = (1::hypreal)" +apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ") +apply simp +apply (simp only: hypreal_one_def) +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus) +done +declare hyperpow_minus_one2 [simp] + +lemma hyperpow_less_le: + "[|(0::hypreal) \ r; r \ 1; n < N|] ==> r pow N \ r pow n" +apply (rule_tac z = "n" in eq_Abs_hypnat) +apply (rule_tac z = "N" in eq_Abs_hypnat) +apply (rule_tac z = "r" in eq_Abs_hypreal) +apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less + hypreal_zero_def hypreal_one_def) +apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset]) +apply (erule FreeUltrafilterNat_Int) +apply assumption; +apply (auto intro: power_decreasing) +done + +lemma hyperpow_SHNat_le: + "[| 0 \ r; r \ (1::hypreal); N \ HNatInfinite |] + ==> ALL n: Nats. r pow N \ r pow n" +by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff) + +lemma hyperpow_realpow: + "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" +apply (unfold hypreal_of_real_def hypnat_of_nat_def) +apply (auto simp add: hyperpow) +done + +lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \ Reals" +apply (unfold SReal_def) +apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow) +done +declare hyperpow_SReal [simp] + +lemma hyperpow_zero_HNatInfinite: "N \ HNatInfinite ==> (0::hypreal) pow N = 0" +apply (drule HNatInfinite_is_Suc) +apply auto +done +declare hyperpow_zero_HNatInfinite [simp] + +lemma hyperpow_le_le: + "[| (0::hypreal) \ r; r \ 1; n \ N |] ==> r pow N \ r pow n" +apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq) +apply (auto intro: hyperpow_less_le) +done + +lemma hyperpow_Suc_le_self2: + "[| (0::hypreal) \ r; r < 1 |] ==> r pow (n + (1::hypnat)) \ r" +apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le) +apply auto +done + +lemma lemma_Infinitesimal_hyperpow: + "[| x \ Infinitesimal; 0 < N |] ==> abs (x pow N) \ abs x" +apply (unfold Infinitesimal_def) +apply (auto intro!: hyperpow_Suc_le_self2 + simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero) +done + +lemma Infinitesimal_hyperpow: + "[| x \ Infinitesimal; 0 < N |] ==> x pow N \ Infinitesimal" +apply (rule hrabs_le_Infinitesimal) +apply (rule_tac [2] lemma_Infinitesimal_hyperpow) +apply auto +done + +lemma hrealpow_hyperpow_Infinitesimal_iff: + "(x ^ n \ Infinitesimal) = (x pow (hypnat_of_nat n) \ Infinitesimal)" +apply (unfold hypnat_of_nat_def) +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (auto simp add: hrealpow hyperpow) +done + +lemma Infinitesimal_hrealpow: + "[| x \ Infinitesimal; 0 < n |] ==> x ^ n \ Infinitesimal" +by (force intro!: Infinitesimal_hyperpow + simp add: hrealpow_hyperpow_Infinitesimal_iff + hypnat_of_nat_less_iff hypnat_of_nat_zero + simp del: hypnat_of_nat_less_iff [symmetric]) + +ML +{* +val hrealpow_two = thm "hrealpow_two"; +val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one"; +val hrealpow_two_le = thm "hrealpow_two_le"; +val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order"; +val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2"; +val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff"; +val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff"; +val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff"; +val hrabs_hrealpow_two = thm "hrabs_hrealpow_two"; +val two_hrealpow_ge_one = thm "two_hrealpow_ge_one"; +val two_hrealpow_gt = thm "two_hrealpow_gt"; +val hrealpow_minus_one = thm "hrealpow_minus_one"; +val double_lemma = thm "double_lemma"; +val hrealpow_minus_one2 = thm "hrealpow_minus_one2"; +val hrealpow = thm "hrealpow"; +val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand"; +val hypreal_of_real_power = thm "hypreal_of_real_power"; +val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of"; +val hrealpow_HFinite = thm "hrealpow_HFinite"; +val hyperpow_congruent = thm "hyperpow_congruent"; +val hyperpow = thm "hyperpow"; +val hyperpow_zero = thm "hyperpow_zero"; +val hyperpow_not_zero = thm "hyperpow_not_zero"; +val hyperpow_inverse = thm "hyperpow_inverse"; +val hyperpow_hrabs = thm "hyperpow_hrabs"; +val hyperpow_add = thm "hyperpow_add"; +val hyperpow_one = thm "hyperpow_one"; +val hyperpow_two = thm "hyperpow_two"; +val hyperpow_gt_zero = thm "hyperpow_gt_zero"; +val hyperpow_ge_zero = thm "hyperpow_ge_zero"; +val hyperpow_le = thm "hyperpow_le"; +val hyperpow_eq_one = thm "hyperpow_eq_one"; +val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one"; +val hyperpow_mult = thm "hyperpow_mult"; +val hyperpow_two_le = thm "hyperpow_two_le"; +val hrabs_hyperpow_two = thm "hrabs_hyperpow_two"; +val hyperpow_two_hrabs = thm "hyperpow_two_hrabs"; +val hyperpow_two_gt_one = thm "hyperpow_two_gt_one"; +val hyperpow_two_ge_one = thm "hyperpow_two_ge_one"; +val two_hyperpow_ge_one = thm "two_hyperpow_ge_one"; +val hyperpow_minus_one2 = thm "hyperpow_minus_one2"; +val hyperpow_less_le = thm "hyperpow_less_le"; +val hyperpow_SHNat_le = thm "hyperpow_SHNat_le"; +val hyperpow_realpow = thm "hyperpow_realpow"; +val hyperpow_SReal = thm "hyperpow_SReal"; +val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite"; +val hyperpow_le_le = thm "hyperpow_le_le"; +val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2"; +val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow"; +val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow"; +val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff"; +val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow"; +*} + end diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Fri Jan 09 10:46:18 2004 +0100 @@ -1348,7 +1348,7 @@ Goal "[| DERIV f x :> d; f(x) \\ 0 |] \ \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; by (rtac (real_mult_commute RS subst) 1); -by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, realpow_inverse]) 1); +by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, power_inverse]) 1); by (fold_goals_tac [o_def]); by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1); qed "DERIV_inverse_fun"; @@ -1369,7 +1369,7 @@ by (REPEAT(assume_tac 1)); by (asm_full_simp_tac (simpset() addsimps [real_divide_def, right_distrib, - realpow_inverse,minus_mult_left] @ mult_ac + power_inverse,minus_mult_left] @ mult_ac delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); qed "DERIV_quotient"; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/MacLaurin.ML --- a/src/HOL/Hyperreal/MacLaurin.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/MacLaurin.ML Fri Jan 09 10:46:18 2004 +0100 @@ -65,8 +65,8 @@ delsimps [realpow_Suc]) 2); by (stac real_mult_inv_left 2); by (stac real_mult_inv_left 3); -by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2); -by (assume_tac 2); +by (rtac (real_not_refl2 RS not_sym) 2); +by (etac zero_less_power 2); by (rtac real_of_nat_fact_not_zero 2); by (Simp_tac 2); by (etac exE 1); @@ -281,7 +281,7 @@ by (Asm_full_simp_tac 1); by (auto_tac (claset(),simpset() addsimps [real_divide_def, CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))", - realpow_mult RS sym])); + power_mult_distrib RS sym])); qed "Maclaurin_minus"; Goal "(h < 0 & 0 < n & diff 0 = f & \ @@ -490,7 +490,7 @@ by (dtac lemma_odd_mod_4_div_2 1); by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1); by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono], - simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS + simpset() addsimps [real_divide_def,abs_mult,abs_inverse,power_abs RS sym])); qed "Maclaurin_sin_bound"; @@ -520,7 +520,7 @@ by (cut_inst_tac [("f","sin"),("n","n"),("x","x"), ("diff","%n x. sin(x + 1/2*real (n)*pi)")] Maclaurin_all_lt_objl 1); -by (Step_tac 1); +by (Safe_tac); by (Simp_tac 1); by (Simp_tac 1); by (case_tac "n" 1); diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/NthRoot.thy Fri Jan 09 10:46:18 2004 +0100 @@ -20,9 +20,14 @@ apply (rule_tac x = "1" in exI) apply (drule_tac [2] linorder_not_le [THEN iffD1]) apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc]) -apply (auto intro!: realpow_Suc_le_self simp add: zero_less_one) +apply (simp add: ); +apply (force intro!: realpow_Suc_le_self simp del: realpow_Suc) done +text{*Used only just below*} +lemma realpow_ge_self2: "[| (1::real) \ r; 0 < n |] ==> r \ r ^ n" +by (insert power_increasing [of 1 n r], simp) + lemma lemma_nth_realpow_isUb_ex: "[| (0::real) < a; 0 < n |] ==> \u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u" @@ -129,10 +134,10 @@ apply (rule_tac n = "k" in real_mult_less_self) apply (blast intro: lemma_nth_realpow_isLub_gt_zero) apply (safe) -apply (drule_tac n = "k" in lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero]) -apply (drule_tac [3] conjI [THEN realpow_le2]) -apply (rule_tac [3] order_less_imp_le) -apply (auto intro: order_trans) +apply (drule_tac n = "k" in + lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero]) +apply assumption+ +apply (blast intro: order_trans order_less_imp_le power_mono) done text{*Second result we want*} @@ -141,11 +146,12 @@ isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a" apply (frule lemma_nth_realpow_isLub_le , safe) -apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2]) +apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult + [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2]) apply (auto simp add: real_of_nat_def) done -(*----------- The theorem at last! -----------*) +text{*The theorem at last!*} lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> \r. r ^ n = a" apply (frule nth_realpow_isLub_ex , auto) apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym) diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/Poly.ML --- a/src/HOL/Hyperreal/Poly.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/Poly.ML Fri Jan 09 10:46:18 2004 +0100 @@ -1002,7 +1002,7 @@ by (dtac (poly_mult_left_cancel RS iffD1) 1); by (Asm_full_simp_tac 1); by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult, - poly_minus] delsimps [pmult_Cons, thm"mult_cancel_left"]) 1); + poly_minus] delsimps [pmult_Cons, mult_cancel_left, field_mult_cancel_left]) 1); by (Step_tac 1); by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel RS iffD1) 1); diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Fri Jan 09 10:46:18 2004 +0100 @@ -1216,22 +1216,25 @@ qed "LIMSEQ_pow"; (*---------------------------------------------------------------- - 0 <= x < 1 ==> (x ^ n ----> 0) + 0 <= x <= 1 ==> (x ^ n ----> 0) Proof will use (NS) Cauchy equivalence for convergence and also fact that bounded and monotonic sequence converges. ---------------------------------------------------------------*) -Goalw [Bseq_def] "[| 0 <= x; x < 1 |] ==> Bseq (%n. x ^ n)"; +Goalw [Bseq_def] "[| 0 <= x; x <= 1 |] ==> Bseq (%n. x ^ n)"; by (res_inst_tac [("x","1")] exI 1); -by (auto_tac (claset() addDs [conjI RS realpow_le] +by (asm_full_simp_tac (simpset() addsimps [power_abs]) 1); +by (auto_tac (claset() addDs [power_mono] addIs [order_less_imp_le], - simpset() addsimps [abs_eqI1, realpow_abs] )); + simpset() addsimps [abs_if] )); qed "Bseq_realpow"; -Goal "[| 0 <= x; x < 1 |] ==> monoseq (%n. x ^ n)"; -by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1); +Goal "[| 0 <= x; x <= 1 |] ==> monoseq (%n. x ^ n)"; +by (clarify_tac (claset() addSIs [mono_SucI2]) 1); +by (cut_inst_tac [("n","n"),("N","Suc n"),("a","x")] power_decreasing 1); +by Auto_tac; qed "monoseq_realpow"; -Goal "[| 0 <= x; x < 1 |] ==> convergent (%n. x ^ n)"; +Goal "[| 0 <= x; x <= 1 |] ==> convergent (%n. x ^ n)"; by (blast_tac (claset() addSIs [Bseq_monoseq_convergent, Bseq_realpow,monoseq_realpow]) 1); qed "convergent_realpow"; @@ -1269,7 +1272,7 @@ by (cut_inst_tac [("a","a"),("x1","inverse x")] ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1); by (auto_tac (claset(), - simpset() addsimps [real_divide_def, realpow_inverse])); + simpset() addsimps [real_divide_def, power_inverse])); by (asm_simp_tac (simpset() addsimps [inverse_eq_divide, pos_divide_less_eq]) 1); qed "LIMSEQ_divide_realpow_zero"; @@ -1289,7 +1292,7 @@ Goal "abs(c) < 1 ==> (%n. c ^ n) ----> 0"; by (rtac (LIMSEQ_rabs_zero RS iffD1) 1); by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero], - simpset() addsimps [realpow_abs])); + simpset() addsimps [power_abs])); qed "LIMSEQ_rabs_realpow_zero2"; Goal "abs(c) < 1 ==> (%n. c ^ n) ----NS> 0"; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/Series.ML --- a/src/HOL/Hyperreal/Series.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/Series.ML Fri Jan 09 10:46:18 2004 +0100 @@ -575,7 +575,7 @@ summable_comparison_test 1); by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1); by (dtac (le_Suc_ex_iff RS iffD1) 1); -by (auto_tac (claset(),simpset() addsimps [realpow_add, realpow_not_zero])); +by (auto_tac (claset(),simpset() addsimps [power_add, realpow_not_zero])); by (induct_tac "na" 1 THEN Auto_tac); by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1); by (auto_tac (claset() addIs [mult_right_mono], diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Fri Jan 09 10:46:18 2004 +0100 @@ -15,7 +15,7 @@ val mult_less_cancel_left = thm"mult_less_cancel_left"; Goalw [root_def] "root (Suc n) 0 = 0"; -by (safe_tac (claset() addSIs [some_equality,realpow_zero] +by (safe_tac (claset() addSIs [some_equality,power_0_Suc] addSEs [realpow_zero_zero])); qed "real_root_zero"; Addsimps [real_root_zero]; @@ -34,7 +34,7 @@ Goalw [root_def] "0 < x ==> root(Suc n) (x ^ (Suc n)) = x"; by (rtac some_equality 1); -by (forw_inst_tac [("n","n")] realpow_gt_zero 2); +by (forw_inst_tac [("n","n")] zero_less_power 2); by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff])); by (res_inst_tac [("R1.0","u"),("R2.0","x")] real_linear_less2 1); by (dres_inst_tac [("n1","n"),("x","u")] (zero_less_Suc RSN (3, realpow_less)) 1); @@ -52,7 +52,7 @@ by (dres_inst_tac [("n","n")] realpow_pos_nth2 1); by (Safe_tac THEN rtac someI2 1); by (auto_tac (claset() addSIs [order_less_imp_le] - addDs [realpow_gt_zero],simpset() addsimps [zero_less_mult_iff])); + addDs [zero_less_power],simpset() addsimps [zero_less_mult_iff])); qed "real_root_pos_pos"; Goal "0 <= x ==> 0 <= root(Suc n) x"; @@ -66,7 +66,7 @@ by (rtac ccontr 1); by (res_inst_tac [("R1.0","u"),("R2.0","1")] real_linear_less2 1); by (dres_inst_tac [("n","n")] realpow_Suc_less_one 1); -by (dres_inst_tac [("n","n")] realpow_Suc_gt_one 4); +by (dres_inst_tac [("n","n")] power_gt1_lemma 4); by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); qed "real_root_one"; Addsimps [real_root_one]; @@ -171,8 +171,8 @@ by (Asm_full_simp_tac 1 THEN Asm_full_simp_tac 1); by (res_inst_tac [("a","xa * x")] someI2 1); by (auto_tac (claset() addEs [real_less_asym], - simpset() addsimps mult_ac@[realpow_mult RS sym,realpow_two_disj, - realpow_gt_zero, real_mult_order] delsimps [realpow_Suc])); + simpset() addsimps mult_ac@[power_mult_distrib RS sym,realpow_two_disj, + zero_less_power, real_mult_order] delsimps [realpow_Suc])); qed "real_sqrt_mult_distrib"; Goal "[|0<=x; 0<=y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)"; @@ -240,8 +240,7 @@ qed "real_sqrt_not_eq_zero"; Goal "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"; -by (ftac real_sqrt_not_eq_zero 1); -by (cut_inst_tac [("n1","2"),("r1","sqrt x")] (realpow_inverse RS sym) 1); +by (cut_inst_tac [("n1","2"),("a1","sqrt x")] (power_inverse RS sym) 1); by (auto_tac (claset() addDs [real_sqrt_gt_zero_pow2],simpset())); qed "real_inv_sqrt_pow2"; @@ -320,7 +319,7 @@ summable_comparison_test 1); by (rtac summable_exp 2); by (res_inst_tac [("x","0")] exI 1); -by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym, +by (auto_tac (claset(), simpset() addsimps [power_abs RS sym, abs_mult,zero_le_mult_iff])); by (auto_tac (claset() addIs [mult_right_mono], simpset() addsimps [positive_imp_inverse_positive,abs_eqI2])); @@ -334,7 +333,7 @@ summable_comparison_test 1); by (rtac summable_exp 2); by (res_inst_tac [("x","0")] exI 1); -by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,abs_mult, +by (auto_tac (claset(), simpset() addsimps [power_abs RS sym,abs_mult, zero_le_mult_iff])); by (auto_tac (claset() addSIs [mult_right_mono], simpset() addsimps [positive_imp_inverse_positive,abs_eqI2])); @@ -426,7 +425,7 @@ \ sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"; by (case_tac "x = y" 1); by (auto_tac (claset(),simpset() addsimps [real_mult_commute, - realpow_add RS sym] delsimps [sumr_Suc])); + power_add RS sym] delsimps [sumr_Suc])); by (res_inst_tac [("c1","x - y")] (real_mult_left_cancel RS iffD1) 1); by (rtac (minus_minus RS subst) 2); by (stac minus_mult_left 2); @@ -454,26 +453,26 @@ by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP "[| (0::real) x<=y" [mult_le_cancel_left]) 1); by (auto_tac (claset(), - simpset() addsimps [mult_assoc,realpow_abs])); + simpset() addsimps [mult_assoc,power_abs])); by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2); -by (auto_tac (claset(),simpset() addsimps [abs_mult,realpow_abs] @ mult_ac)); +by (auto_tac (claset(),simpset() addsimps [abs_mult,power_abs] @ mult_ac)); by (res_inst_tac [("a2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq RS disjE) 1 THEN dtac sym 2); by (auto_tac (claset() addSIs [mult_right_mono], - simpset() addsimps [mult_assoc RS sym, realpow_abs,summable_def])); + simpset() addsimps [mult_assoc RS sym, power_abs,summable_def, power_0_left])); by (res_inst_tac [("x","K * inverse(1 - (abs(z) * inverse(abs x)))")] exI 1); by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [mult_assoc])); by (subgoal_tac "abs(z ^ n) * inverse(abs x ^ n) = (abs(z) * inverse(abs x)) ^ n" 1); -by (auto_tac (claset(),simpset() addsimps [realpow_abs RS sym])); +by (auto_tac (claset(),simpset() addsimps [power_abs RS sym])); by (subgoal_tac "x ~= 0" 1); by (subgoal_tac "x ~= 0" 3); by (auto_tac (claset(), simpset() delsimps [abs_inverse, abs_mult] addsimps [abs_inverse RS sym, realpow_not_zero, abs_mult RS sym, - realpow_inverse, realpow_mult RS sym])); + power_inverse, power_mult_distrib RS sym])); by (auto_tac (claset() addSIs [geometric_sums], - simpset() addsimps [realpow_abs, inverse_eq_divide])); + simpset() addsimps [power_abs, inverse_eq_divide])); by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP "[|(0::real) x summable (%n. f(n) * (z ^ n))"; by (dres_inst_tac [("z","abs z")] powser_insidea 1); by (auto_tac (claset() addIs [summable_rabs_cancel], - simpset() addsimps [realpow_abs RS sym])); + simpset() addsimps [power_abs RS sym])); qed "powser_inside"; (* ------------------------------------------------------------------------ *) @@ -538,7 +537,7 @@ \ (((z + h) ^ (m - p)) - (z ^ (m - p))))"; by (rtac sumr_subst 1); by (auto_tac (claset(),simpset() addsimps [right_distrib, - real_diff_def,realpow_add RS sym] + real_diff_def,power_add RS sym] @ mult_ac)); qed "lemma_termdiff1"; @@ -588,23 +587,23 @@ by (auto_tac (claset() addSIs [sumr_bound2],simpset() addsimps [abs_mult])); by (case_tac "n" 1 THEN Auto_tac); by (dtac less_add_one 1); -by (auto_tac (claset(),simpset() addsimps [realpow_add,real_add_assoc RS sym, +by (auto_tac (claset(),simpset() addsimps [power_add,real_add_assoc RS sym, CLAIM_SIMP "(a * b) * c = a * (c * (b::real))" mult_ac] delsimps [sumr_Suc])); by (auto_tac (claset() addSIs [mult_mono],simpset()delsimps [sumr_Suc])); -by (auto_tac (claset() addSIs [realpow_le2],simpset() addsimps - [realpow_abs] delsimps [sumr_Suc] )); +by (auto_tac (claset() addSIs [power_mono], + simpset() addsimps [power_abs] delsimps [sumr_Suc] )); by (res_inst_tac [("j","real (Suc d) * (K ^ d)")] real_le_trans 1); by (subgoal_tac "0 <= K" 2); by (arith_tac 3); -by (dres_inst_tac [("n","d")] realpow_ge_zero2 2); +by (dres_inst_tac [("n","d")] zero_le_power 2); by (auto_tac (claset(),simpset() delsimps [sumr_Suc] )); by (rtac (sumr_rabs RS real_le_trans) 1); by (rtac sumr_bound2 1 THEN auto_tac (claset() addSDs [less_add_one] - addSIs [mult_mono], simpset() addsimps [abs_mult, realpow_add])); -by (auto_tac (claset() addSIs [realpow_le2,realpow_ge_zero],simpset() addsimps - [realpow_abs])); + addSIs [mult_mono], simpset() addsimps [abs_mult, power_add])); +by (auto_tac (claset() addSIs [power_mono,zero_le_power], + simpset() addsimps [power_abs])); by (ALLGOALS(arith_tac)); qed "lemma_termdiff3"; @@ -956,8 +955,8 @@ by (rtac real_le_trans 1); by (res_inst_tac [("n","2"),("f","(%n. inverse (real (fact n)) * x ^ n)")] series_pos_le 2); -by (auto_tac (claset() addIs [summable_exp],simpset() - addsimps [numeral_2_eq_2,realpow_ge_zero,zero_le_mult_iff])); +by (auto_tac (claset() addIs [summable_exp],simpset() + addsimps [numeral_2_eq_2,zero_le_power,zero_le_mult_iff])); qed "exp_ge_add_one_self"; Addsimps [exp_ge_add_one_self]; @@ -1233,8 +1232,8 @@ (* ------------------------------------------------------------------------ *) Goalw [sin_def] "sin 0 = 0"; -by (auto_tac (claset() addSIs [(sums_unique RS sym), - LIMSEQ_const],simpset() addsimps [sums_def])); +by (auto_tac (claset() addSIs [sums_unique RS sym, LIMSEQ_const], + simpset() addsimps [sums_def] delsimps [power_0_left])); qed "sin_zero"; Addsimps [sin_zero]; @@ -1361,7 +1360,7 @@ Goalw [real_le_def] "abs(sin x) <= 1"; by (rtac notI 1); -by (dtac realpow_two_gt_one 1); +by (dres_inst_tac [("n","Suc 0")] power_gt1 1); by (auto_tac (claset(),simpset() delsimps [realpow_Suc])); by (dres_inst_tac [("r1","cos x")] (realpow_two_le RSN (2, real_gt_one_ge_zero_add_less)) 1); @@ -1389,7 +1388,7 @@ Goalw [real_le_def] "abs(cos x) <= 1"; by (rtac notI 1); -by (dtac realpow_two_gt_one 1); +by (dres_inst_tac [("n","Suc 0")] power_gt1 1); by (auto_tac (claset(),simpset() delsimps [realpow_Suc])); by (dres_inst_tac [("r1","sin x")] (realpow_two_le RSN (2, real_gt_one_ge_zero_add_less)) 1); @@ -1606,7 +1605,7 @@ CLAIM "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"] delsimps [fact_Suc])); by (subgoal_tac "0 < x ^ (4 * m)" 1); -by (asm_simp_tac (simpset() addsimps [realpow_gt_zero]) 2); +by (asm_simp_tac (simpset() addsimps [zero_less_power]) 2); by (asm_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1); by (rtac real_mult_less_mono 1); (*mult_strict_mono would be stronger*) by (ALLGOALS(Asm_simp_tac)); @@ -1624,7 +1623,7 @@ by (auto_tac (claset(), simpset() addsimps [cos_squared_eq, minus_add_distrib RS sym, neg_less_0_iff_less,sin_gt_zero1, - real_add_order,realpow_gt_zero,cos_double] + real_add_order,zero_less_power,cos_double] delsimps [realpow_Suc,minus_add_distrib])); qed "cos_double_less_one"; @@ -1635,7 +1634,7 @@ by (auto_tac (claset(),simpset() addsimps mult_ac@[cos_def])); qed "cos_paired"; -Addsimps [realpow_gt_zero]; +Addsimps [zero_less_power]; Goal "cos (2) < 0"; by (cut_inst_tac [("x","2")] cos_paired 1); @@ -2376,11 +2375,11 @@ Addsimps [cos_arctan_not_zero]; Goal "cos x ~= 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"; -by (rtac (realpow_inverse RS subst) 1); +by (rtac (power_inverse RS subst) 1); by (res_inst_tac [("c1","cos(x) ^ 2")] (real_mult_right_cancel RS iffD1) 1); by (auto_tac (claset() addDs [realpow_not_zero], simpset() addsimps - [realpow_mult,left_distrib,realpow_divide, - tan_def,real_mult_assoc,realpow_inverse RS sym] + [power_mult_distrib,left_distrib,realpow_divide, + tan_def,real_mult_assoc,power_inverse RS sym] delsimps [realpow_Suc])); qed "tan_sec"; @@ -2430,7 +2429,7 @@ Goal "cos (2 * real (n::nat) * pi) = 1"; by (auto_tac (claset(),simpset() addsimps [cos_double, - real_mult_assoc,realpow_add RS sym,numeral_2_eq_2])); + real_mult_assoc,power_add RS sym,numeral_2_eq_2])); (*FIXME: just needs x^n for literals!*) qed "cos_2npi"; Addsimps [cos_2npi]; @@ -2584,14 +2583,14 @@ \ ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"; by (rtac real_root_pos_unique 1); by (auto_tac (claset() addSIs [real_root_pos_pos_le],simpset() - addsimps [realpow_mult,zero_le_mult_iff, + addsimps [power_mult_distrib,zero_le_mult_iff, real_root_pow_pos2] delsimps [realpow_Suc])); qed "real_root_mult"; Goal "0 <= x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"; by (rtac real_root_pos_unique 1); by (auto_tac (claset() addIs [real_root_pos_pos_le],simpset() - addsimps [realpow_inverse RS sym,real_root_pow_pos2] + addsimps [power_inverse RS sym,real_root_pow_pos2] delsimps [realpow_Suc])); qed "real_root_inverse"; @@ -3035,8 +3034,8 @@ by (rtac add_mono 1); by (auto_tac (claset(),simpset() delsimps [realpow_Suc])); by (ALLGOALS(rtac ((CLAIM "(2::real) ^ 2 = 4") RS subst))); -by (ALLGOALS(rtac (realpow_mult RS subst))); -by (ALLGOALS(rtac realpow_le)); +by (ALLGOALS(rtac (power_mult_distrib RS subst))); +by (ALLGOALS(rtac power_mono)); by Auto_tac; qed "lemma_sqrt_hcomplex_capprox"; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Integ/Int.thy --- a/src/HOL/Integ/Int.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Integ/Int.thy Fri Jan 09 10:46:18 2004 +0100 @@ -148,6 +148,7 @@ instance int :: ordered_ring proof fix i j k :: int + show "0 < (1::int)" by (rule int_0_less_1) show "i \ j ==> k + i \ k + j" by simp show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Integ/IntDef.thy Fri Jan 09 10:46:18 2004 +0100 @@ -344,7 +344,8 @@ show "i * j = j * i" by (rule zmult_commute) show "1 * i = i" by simp show "(i + j) * k = i * k + j * k" by (simp add: int_distrib) - show "0 \ (1::int)" by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq) + show "0 \ (1::int)" + by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq) assume eq: "k+i = k+j" hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc) thus "i = j" by simp diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Integ/IntPower.thy --- a/src/HOL/Integ/IntPower.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Integ/IntPower.thy Fri Jan 09 10:46:18 2004 +0100 @@ -15,6 +15,15 @@ power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)" +instance int :: ringpower +proof + fix z :: int + fix n :: nat + show "z^0 = 1" by simp + show "z^(Suc n) = z * (z^n)" by simp +qed + + lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" apply (induct_tac "y", auto) apply (rule zmod_zmult1_eq [THEN trans]) @@ -22,27 +31,11 @@ apply (rule zmod_zmult_distrib [symmetric]) done -lemma zpower_1 [simp]: "1^y = (1::int)" -by (induct_tac "y", auto) - -lemma zpower_zmult_distrib: "(x*z)^y = ((x^y)*(z^y)::int)" -by (induct_tac "y", auto) - lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)" -by (induct_tac "y", auto) + by (rule Power.power_add) lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)" -apply (induct_tac "y", auto) -apply (subst zpower_zmult_distrib) -apply (subst zpower_zadd_distrib) -apply (simp (no_asm_simp)) -done - - -(*** Logical equivalences for inequalities ***) - -lemma zpower_eq_0_iff [simp]: "(x^n = 0) = (x = (0::int) & 0 (0::int) | n=0)" @@ -58,11 +51,8 @@ ML {* val zpower_zmod = thm "zpower_zmod"; -val zpower_1 = thm "zpower_1"; -val zpower_zmult_distrib = thm "zpower_zmult_distrib"; val zpower_zadd_distrib = thm "zpower_zadd_distrib"; val zpower_zpower = thm "zpower_zpower"; -val zpower_eq_0_iff = thm "zpower_eq_0_iff"; val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff"; val zero_le_zpower_abs = thm "zero_le_zpower_abs"; *} diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/IsaMakefile Fri Jan 09 10:46:18 2004 +0100 @@ -93,7 +93,7 @@ Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \ Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \ Nat.thy NatArith.ML NatArith.thy Numeral.thy \ - Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \ + Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \ Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \ Relation_Power.thy Ring_and_Field.thy\ Set.ML Set.thy SetInterval.ML SetInterval.thy \ @@ -152,8 +152,7 @@ Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\ Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \ Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\ - Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\ - Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\ + Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\ Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.ML Hyperreal/Log.thy\ Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\ Hyperreal/NatStar.ML Hyperreal/NatStar.thy\ diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Library/Rational_Numbers.thy --- a/src/HOL/Library/Rational_Numbers.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Library/Rational_Numbers.thy Fri Jan 09 10:46:18 2004 +0100 @@ -514,8 +514,7 @@ by (induct q, induct r) (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat) show "0 \ (1::rat)" - by (simp add: zero_rat_def one_rat_def rat_of_equality - zero_fraction_def one_fraction_def) + by (simp add: zero_rat one_rat eq_rat) assume eq: "s+q = s+r" hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc) thus "q = r" by (simp add: rat_left_minus rat_add_0) @@ -592,6 +591,8 @@ instance rat :: ordered_field proof fix q r s :: rat + show "0 < (1::rat)" + by (simp add: zero_rat one_rat less_rat) show "q \ r ==> s + q \ s + r" proof (induct q, induct r, induct s) fix a b c d e f :: int diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Nat.thy Fri Jan 09 10:46:18 2004 +0100 @@ -771,6 +771,7 @@ instance nat :: ordered_semiring proof fix i j k :: nat + show "0 < (1::nat)" by simp show "i \ j ==> k + i \ k + j" by simp show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) qed diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/NumberTheory/EvenOdd.thy --- a/src/HOL/NumberTheory/EvenOdd.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/NumberTheory/EvenOdd.thy Fri Jan 09 10:46:18 2004 +0100 @@ -173,7 +173,7 @@ also have "(-1::int)^2 = 1"; by auto finally; show ?thesis; - by (auto simp add: zpower_1) + by auto qed; qed; @@ -199,7 +199,7 @@ also have "(-1::int)^2 = 1"; by auto finally; show ?thesis; - by (auto simp add: zpower_1) + by auto qed; qed; diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Power.ML --- a/src/HOL/Power.ML Fri Jan 09 01:28:24 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,191 +0,0 @@ -(* Title: HOL/Power.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat -Also binomial coefficents -*) - -(*** Simple laws about Power ***) - -Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)"; -by (induct_tac "k" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac))); -qed "power_add"; - -Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k"; -by (induct_tac "k" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add]))); -qed "power_mult"; - -Goal "!!i::nat. 0 < i ==> 0 < i^n"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "zero_less_power"; -Addsimps [zero_less_power]; - -Goal "i^n = 0 ==> i = (0::nat)"; -by (etac contrapos_pp 1); -by Auto_tac; -qed "power_eq_0D"; - -Goal "!!i::nat. 1 <= i ==> Suc 0 <= i^n"; -by (induct_tac "n" 1); -by Auto_tac; -qed "one_le_power"; -Addsimps [one_le_power]; - -Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)"; -by (induct_tac "n" 1); -by Auto_tac; -by (ALLGOALS (case_tac "m")); -by (Simp_tac 1); -by Auto_tac; -qed_spec_mp "power_inject"; -Addsimps [power_inject]; - -Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n"; -by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); -by (asm_simp_tac (simpset() addsimps [power_add]) 1); -qed "le_imp_power_dvd"; - -Goal "(1::nat) < i ==> \\n. i ^ m <= i ^ n --> m <= n"; -by (induct_tac "m" 1); -by Auto_tac; -by (case_tac "na" 1); -by Auto_tac; -by (subgoal_tac "Suc 1 * 1 <= i * i^n" 1); -by (Asm_full_simp_tac 1); -by (rtac mult_le_mono 1); -by Auto_tac; -qed_spec_mp "power_le_imp_le"; - -Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"; -by (rtac ccontr 1); -by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1); -by (etac zero_less_power 1); -by (contr_tac 1); -qed "power_less_imp_less"; - -Goal "k^j dvd n --> i<=j --> k^i dvd (n::nat)"; -by (induct_tac "j" 1); -by (ALLGOALS (simp_tac (simpset() addsimps [le_Suc_eq]))); -by (blast_tac (claset() addSDs [dvd_mult_right]) 1); -qed_spec_mp "power_le_dvd"; - -Goal "[|i^m dvd i^n; (1::nat) < i|] ==> m <= n"; -by (rtac power_le_imp_le 1); -by (assume_tac 1); -by (etac dvd_imp_le 1); -by (Asm_full_simp_tac 1); -qed "power_dvd_imp_le"; - - -(*** Logical equivalences for inequalities ***) - -Goal "(x^n = 0) = (x = (0::nat) & 0 (n choose k) = 0"; -by (induct_tac "n" 1); -by Auto_tac; -by (etac allE 1); -by (etac mp 1); -by (arith_tac 1); -qed_spec_mp "binomial_eq_0"; - -Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc]; -Delsimps [binomial_0, binomial_Suc]; - -Goal "(n choose n) = 1"; -by (induct_tac "n" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0]))); -qed "binomial_n_n"; -Addsimps [binomial_n_n]; - -Goal "(Suc n choose n) = Suc n"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "binomial_Suc_n"; -Addsimps [binomial_Suc_n]; - -Goal "(n choose Suc 0) = n"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "binomial_1"; -Addsimps [binomial_1]; - -Goal "k <= n --> 0 < (n choose k)"; -by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "zero_less_binomial"; - -Goal "(n choose k = 0) = (n Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"; -by (induct_tac "n" 1); -by (simp_tac (simpset() addsimps [binomial_0]) 1); -by (Clarify_tac 1); -by (case_tac "k" 1); -by (auto_tac (claset(), - simpset() addsimps [add_mult_distrib, add_mult_distrib2, - le_Suc_eq, binomial_eq_0])); -qed_spec_mp "Suc_times_binomial_eq"; - -(*This is the well-known version, but it's harder to use because of the - need to reason about division.*) -Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; -by (asm_simp_tac (simpset() - addsimps [Suc_times_binomial_eq, div_mult_self_is_m, zero_less_Suc] - delsimps [mult_Suc, mult_Suc_right]) 1); -qed "binomial_Suc_Suc_eq_times"; - -(*Another version, with -1 instead of Suc.*) -Goal "[|k <= n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))"; -by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1); -by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); -by Auto_tac; -qed "times_binomial_minus1_eq"; - diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Power.thy Fri Jan 09 10:46:18 2004 +0100 @@ -3,23 +3,451 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge -The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat -Also binomial coefficents *) -Power = Divides + -consts - binomial :: "[nat,nat] => nat" (infixl "choose" 65) +header{*Exponentiation and Binomial Coefficients*} + +theory Power = Divides: + +subsection{*Powers for Arbitrary (Semi)Rings*} + +axclass ringpower \ semiring, power + power_0 [simp]: "a ^ 0 = 1" + power_Suc: "a ^ (Suc n) = a * (a ^ n)" + +lemma power_0_Suc [simp]: "(0::'a::ringpower) ^ (Suc n) = 0" +by (simp add: power_Suc) + +text{*It looks plausible as a simprule, but its effect can be strange.*} +lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::ringpower))" +by (induct_tac "n", auto) + +lemma power_one [simp]: "1^n = (1::'a::ringpower)" +apply (induct_tac "n") +apply (auto simp add: power_Suc) +done + +lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a" +by (simp add: power_Suc) + +lemma power_add: "(a::'a::ringpower) ^ (m+n) = (a^m) * (a^n)" +apply (induct_tac "n") +apply (simp_all add: power_Suc mult_ac) +done + +lemma power_mult: "(a::'a::ringpower) ^ (m*n) = (a^m) ^ n" +apply (induct_tac "n") +apply (simp_all add: power_Suc power_add) +done + +lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)" +apply (induct_tac "n") +apply (auto simp add: power_Suc mult_ac) +done + +lemma zero_less_power: + "0 < (a::'a::{ordered_semiring,ringpower}) ==> 0 < a^n" +apply (induct_tac "n") +apply (simp_all add: power_Suc zero_less_one mult_pos) +done + +lemma zero_le_power: + "0 \ (a::'a::{ordered_semiring,ringpower}) ==> 0 \ a^n" +apply (simp add: order_le_less) +apply (erule disjE) +apply (simp_all add: zero_less_power zero_less_one power_0_left) +done + +lemma one_le_power: + "1 \ (a::'a::{ordered_semiring,ringpower}) ==> 1 \ a^n" +apply (induct_tac "n") +apply (simp_all add: power_Suc) +apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) +apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) +done + +lemma gt1_imp_ge0: "1 < a ==> 0 \ (a::'a::ordered_semiring)" + by (simp add: order_trans [OF zero_le_one order_less_imp_le]) + +lemma power_gt1_lemma: + assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})" + shows "1 < a * a^n" +proof - + have "1*1 < a * a^n" + proof (rule order_less_le_trans) + show "1*1 < a*1" by (simp add: gt1) + show "a*1 \ a * a^n" + by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le + zero_le_one order_refl) + qed + thus ?thesis by simp +qed + +lemma power_gt1: + "1 < (a::'a::{ordered_semiring,ringpower}) ==> 1 < a ^ (Suc n)" +by (simp add: power_gt1_lemma power_Suc) + +lemma power_le_imp_le_exp: + assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a" + shows "!!n. a^m \ a^n ==> m \ n" +proof (induct "m") + case 0 + show ?case by simp +next + case (Suc m) + show ?case + proof (cases n) + case 0 + from prems have "a * a^m \ 1" by (simp add: power_Suc) + with gt1 show ?thesis + by (force simp only: power_gt1_lemma + linorder_not_less [symmetric]) + next + case (Suc n) + from prems show ?thesis + by (force dest: mult_left_le_imp_le + simp add: power_Suc order_less_trans [OF zero_less_one gt1]) + qed +qed + +text{*Surely we can strengthen this? It holds for 0 (a^m = a^n) = (m=n)" + by (force simp add: order_antisym power_le_imp_le_exp) + +text{*Can relax the first premise to @{term "0 m < n" +by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] + power_le_imp_le_exp) + + +lemma power_mono: + "[|a \ b; (0::'a::{ringpower,ordered_semiring}) \ a|] ==> a^n \ b^n" +apply (induct_tac "n") +apply (simp_all add: power_Suc) +apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b]) +done + +lemma power_strict_mono [rule_format]: + "[|a < b; (0::'a::{ringpower,ordered_semiring}) \ a|] + ==> 0 < n --> a^n < b^n" +apply (induct_tac "n") +apply (auto simp add: mult_strict_mono zero_le_power power_Suc + order_le_less_trans [of 0 a b]) +done + +lemma power_eq_0_iff [simp]: + "(a^n = 0) = (a = (0::'a::{ordered_ring,ringpower}) & 0 (0::'a::{field,ringpower}) ==> a^n \ 0" +by force + +text{*Perhaps these should be simprules.*} +lemma power_inverse: + "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n" +apply (induct_tac "n") +apply (auto simp add: power_Suc inverse_mult_distrib) +done + +lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n" +apply (induct_tac "n") +apply (auto simp add: power_Suc abs_mult) +done + +lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n" +proof - + have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) + thus ?thesis by (simp only: power_mult_distrib) +qed + +text{*Lemma for @{text power_strict_decreasing}*} +lemma power_Suc_less: + "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|] + ==> a * a^n < a^n" +apply (induct_tac n) +apply (auto simp add: power_Suc mult_strict_left_mono) +done + +lemma power_strict_decreasing: + "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|] + ==> a^N < a^n" +apply (erule rev_mp) +apply (induct_tac "N") +apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) +apply (rename_tac m) +apply (subgoal_tac "a * a^m < 1 * a^n", simp) +apply (rule mult_strict_mono) +apply (auto simp add: zero_le_power zero_less_one order_less_imp_le) +done + +text{*Proof resembles that of @{text power_strict_decreasing}*} +lemma power_decreasing: + "[|n \ N; 0 \ a; a \ (1::'a::{ordered_semiring,ringpower})|] + ==> a^N \ a^n" +apply (erule rev_mp) +apply (induct_tac "N") +apply (auto simp add: power_Suc le_Suc_eq) +apply (rename_tac m) +apply (subgoal_tac "a * a^m \ 1 * a^n", simp) +apply (rule mult_mono) +apply (auto simp add: zero_le_power zero_le_one) +done + +lemma power_Suc_less_one: + "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1" +apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) +done + +text{*Proof again resembles that of @{text power_strict_decreasing}*} +lemma power_increasing: + "[|n \ N; (1::'a::{ordered_semiring,ringpower}) \ a|] ==> a^n \ a^N" +apply (erule rev_mp) +apply (induct_tac "N") +apply (auto simp add: power_Suc le_Suc_eq) +apply (rename_tac m) +apply (subgoal_tac "1 * a^n \ a * a^m", simp) +apply (rule mult_mono) +apply (auto simp add: order_trans [OF zero_le_one] zero_le_power) +done + +text{*Lemma for @{text power_strict_increasing}*} +lemma power_less_power_Suc: + "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n" +apply (induct_tac n) +apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) +done + +lemma power_strict_increasing: + "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N" +apply (erule rev_mp) +apply (induct_tac "N") +apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) +apply (rename_tac m) +apply (subgoal_tac "1 * a^n < a * a^m", simp) +apply (rule mult_strict_mono) +apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power + order_less_imp_le) +done + +lemma power_le_imp_le_base: + assumes le: "a ^ Suc n \ b ^ Suc n" + and xnonneg: "(0::'a::{ordered_semiring,ringpower}) \ a" + and ynonneg: "0 \ b" + shows "a \ b" + proof (rule ccontr) + assume "~ a \ b" + then have "b < a" by (simp only: linorder_not_le) + then have "b ^ Suc n < a ^ Suc n" + by (simp only: prems power_strict_mono) + from le and this show "False" + by (simp add: linorder_not_less [symmetric]) + qed + +lemma power_inject_base: + "[| a ^ Suc n = b ^ Suc n; 0 \ a; 0 \ b |] + ==> a = (b::'a::{ordered_semiring,ringpower})" +by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) + + +subsection{*Exponentiation for the Natural Numbers*} primrec (power) "p ^ 0 = 1" "p ^ (Suc n) = (p::nat) * (p ^ n)" +instance nat :: ringpower +proof + fix z :: nat + fix n :: nat + show "z^0 = 1" by simp + show "z^(Suc n) = z * (z^n)" by simp +qed + +lemma nat_one_le_power [simp]: "1 \ i ==> Suc 0 \ i^n" +by (insert one_le_power [of i n], simp) + +lemma le_imp_power_dvd: "!!i::nat. m \ n ==> i^m dvd i^n" +apply (unfold dvd_def) +apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst]) +apply (simp add: power_add) +done + +text{*Valid for the naturals, but what if @{text"0 m < n" +apply (rule ccontr) +apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD]) +apply (erule zero_less_power, auto) +done + +lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \ (0::nat) | n=0)" +by (induct_tac "n", auto) + +lemma power_le_dvd [rule_format]: "k^j dvd n --> i\j --> k^i dvd (n::nat)" +apply (induct_tac "j") +apply (simp_all add: le_Suc_eq) +apply (blast dest!: dvd_mult_right) +done + +lemma power_dvd_imp_le: "[|i^m dvd i^n; (1::nat) < i|] ==> m \ n" +apply (rule power_le_imp_le_exp, assumption) +apply (erule dvd_imp_le, simp) +done + + +subsection{*Binomial Coefficients*} + +text{*This development is based on the work of Andy Gordon and +Florian Kammueller*} + +consts + binomial :: "[nat,nat] => nat" (infixl "choose" 65) + primrec - binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)" + binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" + + binomial_Suc: "(Suc n choose k) = + (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" + +lemma binomial_n_0 [simp]: "(n choose 0) = 1" +by (case_tac "n", simp_all) + +lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" +by simp + +lemma binomial_Suc_Suc [simp]: + "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" +by simp + +lemma binomial_eq_0 [rule_format]: "\k. n < k --> (n choose k) = 0" +apply (induct_tac "n", auto) +apply (erule allE) +apply (erule mp, arith) +done + +declare binomial_0 [simp del] binomial_Suc [simp del] + +lemma binomial_n_n [simp]: "(n choose n) = 1" +apply (induct_tac "n") +apply (simp_all add: binomial_eq_0) +done + +lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" +by (induct_tac "n", simp_all) + +lemma binomial_1 [simp]: "(n choose Suc 0) = n" +by (induct_tac "n", simp_all) + +lemma zero_less_binomial [rule_format]: "k \ n --> 0 < (n choose k)" +by (rule_tac m = n and n = k in diff_induct, simp_all) - binomial_Suc "(Suc n choose k) = - (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" +lemma binomial_eq_0_iff: "(n choose k = 0) = (nn)" +by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) + +(*Might be more useful if re-oriented*) +lemma Suc_times_binomial_eq [rule_format]: + "\k. k \ n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" +apply (induct_tac "n") +apply (simp add: binomial_0, clarify) +apply (case_tac "k") +apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq + binomial_eq_0) +done + +text{*This is the well-known version, but it's harder to use because of the + need to reason about division.*} +lemma binomial_Suc_Suc_eq_times: + "k \ n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" +by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc + del: mult_Suc mult_Suc_right) + +text{*Another version, with -1 instead of Suc.*} +lemma times_binomial_minus1_eq: + "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" +apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) +apply (simp split add: nat_diff_split, auto) +done + +text{*ML bindings for the general exponentiation theorems*} +ML +{* +val power_0 = thm"power_0"; +val power_Suc = thm"power_Suc"; +val power_0_Suc = thm"power_0_Suc"; +val power_0_left = thm"power_0_left"; +val power_one = thm"power_one"; +val power_one_right = thm"power_one_right"; +val power_add = thm"power_add"; +val power_mult = thm"power_mult"; +val power_mult_distrib = thm"power_mult_distrib"; +val zero_less_power = thm"zero_less_power"; +val zero_le_power = thm"zero_le_power"; +val one_le_power = thm"one_le_power"; +val gt1_imp_ge0 = thm"gt1_imp_ge0"; +val power_gt1_lemma = thm"power_gt1_lemma"; +val power_gt1 = thm"power_gt1"; +val power_le_imp_le_exp = thm"power_le_imp_le_exp"; +val power_inject_exp = thm"power_inject_exp"; +val power_less_imp_less_exp = thm"power_less_imp_less_exp"; +val power_mono = thm"power_mono"; +val power_strict_mono = thm"power_strict_mono"; +val power_eq_0_iff = thm"power_eq_0_iff"; +val field_power_eq_0_iff = thm"field_power_eq_0_iff"; +val field_power_not_zero = thm"field_power_not_zero"; +val power_inverse = thm"power_inverse"; +val power_abs = thm"power_abs"; +val power_minus = thm"power_minus"; +val power_Suc_less = thm"power_Suc_less"; +val power_strict_decreasing = thm"power_strict_decreasing"; +val power_decreasing = thm"power_decreasing"; +val power_Suc_less_one = thm"power_Suc_less_one"; +val power_increasing = thm"power_increasing"; +val power_strict_increasing = thm"power_strict_increasing"; +val power_le_imp_le_base = thm"power_le_imp_le_base"; +val power_inject_base = thm"power_inject_base"; +*} + +text{*ML bindings for the remaining theorems*} +ML +{* +val nat_one_le_power = thm"nat_one_le_power"; +val le_imp_power_dvd = thm"le_imp_power_dvd"; +val nat_power_less_imp_less = thm"nat_power_less_imp_less"; +val nat_zero_less_power_iff = thm"nat_zero_less_power_iff"; +val power_le_dvd = thm"power_le_dvd"; +val power_dvd_imp_le = thm"power_dvd_imp_le"; +val binomial_n_0 = thm"binomial_n_0"; +val binomial_0_Suc = thm"binomial_0_Suc"; +val binomial_Suc_Suc = thm"binomial_Suc_Suc"; +val binomial_eq_0 = thm"binomial_eq_0"; +val binomial_n_n = thm"binomial_n_n"; +val binomial_Suc_n = thm"binomial_Suc_n"; +val binomial_1 = thm"binomial_1"; +val zero_less_binomial = thm"zero_less_binomial"; +val binomial_eq_0_iff = thm"binomial_eq_0_iff"; +val zero_less_binomial_iff = thm"zero_less_binomial_iff"; +val Suc_times_binomial_eq = thm"Suc_times_binomial_eq"; +val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times"; +val times_binomial_minus1_eq = thm"times_binomial_minus1_eq"; +*} end diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Real/RealDef.thy Fri Jan 09 10:46:18 2004 +0100 @@ -825,6 +825,9 @@ instance real :: ordered_field proof fix x y z :: real + show "0 < (1::real)" + by (force intro: real_gt_zero_preal_Ex [THEN iffD2] + simp add: real_one_def real_of_preal_def) show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) show "\x\ = (if x < 0 then -x else x)" diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Real/RealPow.thy Fri Jan 09 10:46:18 2004 +0100 @@ -8,6 +8,8 @@ theory RealPow = RealArith: +declare abs_mult_self [simp] + instance real :: power .. primrec (realpow) @@ -15,118 +17,45 @@ realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)" -lemma realpow_zero [simp]: "(0::real) ^ (Suc n) = 0" -by auto +instance real :: ringpower +proof + fix z :: real + fix n :: nat + show "z^0 = 1" by simp + show "z^(Suc n) = z * (z^n)" by simp +qed -lemma realpow_not_zero [rule_format]: "r \ (0::real) --> r ^ n \ 0" -by (induct_tac "n", auto) + +lemma realpow_not_zero: "r \ (0::real) ==> r ^ n \ 0" + by (rule field_power_not_zero) lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0" -apply (rule ccontr) -apply (auto dest: realpow_not_zero) -done - -lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n" -apply (induct_tac "n") -apply (auto simp add: inverse_mult_distrib) -done - -lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n" -apply (induct_tac "n") -apply (auto simp add: abs_mult) -done - -lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)" -apply (induct_tac "n") -apply (auto simp add: mult_ac) -done - -lemma realpow_one [simp]: "(r::real) ^ 1 = r" by simp lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r" by simp -lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n" -apply (induct_tac "n") -apply (auto intro: real_mult_order simp add: zero_less_one) -done - -lemma realpow_ge_zero [rule_format]: "(0::real) \ r --> 0 \ r ^ n" -apply (induct_tac "n") -apply (auto simp add: zero_le_mult_iff) -done - -lemma realpow_le [rule_format]: "(0::real) \ x & x \ y --> x ^ n \ y ^ n" -apply (induct_tac "n") -apply (auto intro!: mult_mono) -apply (simp (no_asm_simp) add: realpow_ge_zero) -done - -lemma realpow_0_left [rule_format, simp]: - "0 < n --> 0 ^ n = (0::real)" -apply (induct_tac "n", auto) +text{*Legacy: weaker version of the theorem @{text power_strict_mono}, +used 6 times in NthRoot and Transcendental*} +lemma realpow_less: + "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n" +apply (rule power_strict_mono, auto) done -lemma realpow_less' [rule_format]: - "[|(0::real) \ x; x < y |] ==> 0 < n --> x ^ n < y ^ n" -apply (induct n) -apply (auto simp add: real_mult_less_mono' realpow_ge_zero) -done - -text{*Legacy: weaker version of the theorem above*} -lemma realpow_less: - "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n" -apply (rule realpow_less', auto) -done - -lemma realpow_eq_one [simp]: "1 ^ n = (1::real)" -by (induct_tac "n", auto) - lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)" -apply (induct_tac "n") -apply (auto simp add: abs_mult) -done - -lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)" -apply (induct_tac "n") -apply (auto simp add: mult_ac) -done +by (simp add: power_abs) lemma realpow_two_le [simp]: "(0::real) \ r^ Suc (Suc 0)" by (simp add: real_le_square) lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)" -by (simp add: abs_eqI1 real_le_square) +by (simp add: abs_mult) lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)" -by (simp add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc) - -lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))" -apply auto -apply (cut_tac real_zero_less_one) -apply (frule_tac x = 0 in order_less_trans, assumption) -apply (frule_tac c = r and a = 1 in mult_strict_right_mono) -apply assumption; -apply (simp add: ); -done - -lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \ r ^ n" -apply (induct_tac "n", auto) -apply (subgoal_tac "1*1 \ r * r^n") -apply (rule_tac [2] mult_mono, auto) -done - -lemma realpow_ge_one2: "(1::real) \ r ==> 1 \ r ^ n" -apply (drule order_le_imp_less_or_eq) -apply (auto dest: realpow_ge_one) -done +by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc) lemma two_realpow_ge_one [simp]: "(1::real) \ 2 ^ n" -apply (rule_tac y = "1 ^ n" in order_trans) -apply (rule_tac [2] realpow_le) -apply (auto intro: order_less_imp_le) -done +by (insert power_increasing [of 0 n "2::real"], simp) lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" apply (induct_tac "n") @@ -145,111 +74,38 @@ lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)" by auto -lemma realpow_Suc_less [rule_format]: - "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n" - by (induct_tac "n", auto simp add: mult_less_cancel_left) - -lemma realpow_Suc_le [rule_format]: - "0 \ r & r < (1::real) --> r ^ Suc n \ r ^ n" -apply (induct_tac "n") -apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq) -done - -lemma realpow_zero_le [simp]: "(0::real) \ 0 ^ n" -by (case_tac "n", auto) - -lemma realpow_Suc_le2 [rule_format]: "0 < r & r < (1::real) --> r ^ Suc n \ r ^ n" -by (blast intro!: order_less_imp_le realpow_Suc_less) +lemma realpow_Suc_le_self: "[| 0 \ r; r \ (1::real) |] ==> r ^ Suc n \ r" +by (insert power_decreasing [of 1 "Suc n" r], simp) -lemma realpow_Suc_le3: "[| 0 \ r; r < (1::real) |] ==> r ^ Suc n \ r ^ n" -apply (erule order_le_imp_less_or_eq [THEN disjE]) -apply (rule realpow_Suc_le2, auto) -done +text{*Used ONCE in Transcendental*} +lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1" +by (insert power_strict_decreasing [of 0 "Suc n" r], simp) -lemma realpow_less_le [rule_format]: "0 \ r & r < (1::real) & n < N --> r ^ N \ r ^ n" -apply (induct_tac "N") -apply (simp_all (no_asm_simp)) -apply clarify -apply (subgoal_tac "r * r ^ na \ 1 * r ^ n", simp) -apply (rule mult_mono) -apply (auto simp add: realpow_ge_zero less_Suc_eq) -done - -lemma realpow_le_le: "[| 0 \ r; r < (1::real); n \ N |] ==> r ^ N \ r ^ n" -apply (drule_tac n = N in le_imp_less_or_eq) -apply (auto intro: realpow_less_le) +text{*Used ONCE in Lim.ML*} +lemma realpow_minus_mult [rule_format]: + "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" +apply (simp split add: nat_diff_split) done -lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \ r" -by (drule_tac n = 1 and N = "Suc n" in order_less_imp_le [THEN realpow_le_le], auto) - -lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1" -by (blast intro: realpow_Suc_le_self order_le_less_trans) - -lemma realpow_le_Suc [rule_format]: "(1::real) \ r --> r ^ n \ r ^ Suc n" -by (induct_tac "n", auto) - -lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n" -by (induct_tac "n", auto simp add: mult_less_cancel_left) - -lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \ r ^ Suc n" -by (blast intro!: order_less_imp_le realpow_less_Suc) - -(*One use in RealPow.thy*) -lemma real_mult_self_le2: "[| (1::real) \ r; (1::real) \ x |] ==> x \ r * x" -apply (subgoal_tac "1 * x \ r * x", simp) -apply (rule mult_right_mono, auto) -done - -lemma realpow_gt_ge2 [rule_format]: "(1::real) \ r & n < N --> r ^ n \ r ^ N" -apply (induct_tac "N", auto) -apply (frule_tac [!] n = na in realpow_ge_one2) -apply (drule_tac [!] real_mult_self_le2, assumption) -prefer 2 apply assumption -apply (auto intro: order_trans simp add: less_Suc_eq) -done - -lemma realpow_ge_ge2: "[| (1::real) \ r; n \ N |] ==> r ^ n \ r ^ N" -apply (drule_tac n = N in le_imp_less_or_eq) -apply (auto intro: realpow_gt_ge2) -done - -lemma realpow_Suc_ge_self2: "(1::real) \ r ==> r \ r ^ Suc n" -by (drule_tac n = 1 and N = "Suc n" in realpow_ge_ge2, auto) - -(*Used ONCE in Hyperreal/NthRoot.ML*) -lemma realpow_ge_self2: "[| (1::real) \ r; 0 < n |] ==> r \ r ^ n" -apply (drule less_not_refl2 [THEN not0_implies_Suc]) -apply (auto intro!: realpow_Suc_ge_self2) -done - -lemma realpow_minus_mult [rule_format, simp]: - "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" -apply (induct_tac "n") -apply (auto simp add: real_mult_commute) -done - -lemma realpow_two_mult_inverse [simp]: "r \ 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" +lemma realpow_two_mult_inverse [simp]: + "r \ 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" by (simp add: realpow_two real_mult_assoc [symmetric]) -(* 05/00 *) lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)" by simp -lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" +lemma realpow_two_diff: + "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" apply (unfold real_diff_def) apply (simp add: right_distrib left_distrib mult_ac) done -lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" +lemma realpow_two_disj: + "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" apply (cut_tac x = x and y = y in realpow_two_diff) apply (auto simp del: realpow_Suc) done -(* used in Transc *) -lemma realpow_diff: "[|(x::real) \ 0; m \ n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)" -by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac) - lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)" apply (induct_tac "n") apply (auto simp add: real_of_nat_one real_of_nat_mult) @@ -261,29 +117,12 @@ done lemma realpow_increasing: - assumes xnonneg: "(0::real) \ x" - and ynonneg: "0 \ y" - and le: "x ^ Suc n \ y ^ Suc n" - shows "x \ y" - proof (rule ccontr) - assume "~ x \ y" - then have "y x; 0 \ y; x ^ Suc n = y ^ Suc n |] ==> x = y" -by (blast intro: realpow_increasing order_antisym order_eq_refl sym) + "[|(0::real) \ x; 0 \ y; x ^ Suc n \ y ^ Suc n|] ==> x \ y" + by (rule power_le_imp_le_base) -(*** Logical equivalences for inequalities ***) - -lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0 (0::real) | n=0)" +lemma zero_less_realpow_abs_iff [simp]: + "(0 < (abs x)^n) = (x \ (0::real) | n=0)" apply (induct_tac "n") apply (auto simp add: zero_less_mult_iff) done @@ -294,7 +133,7 @@ done -(*** Literal arithmetic involving powers, type real ***) +subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*} lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" apply (induct_tac "n") @@ -302,7 +141,8 @@ done declare real_of_int_power [symmetric, simp] -lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" +lemma power_real_number_of: + "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" by (simp only: real_number_of_def real_of_int_power) declare power_real_number_of [of _ "number_of w", standard, simp] @@ -311,20 +151,6 @@ lemma real_power_two: "(r::real)\ = r * r" by (simp add: numeral_2_eq_2) -lemma real_sqr_ge_zero [iff]: "0 \ (r::real)\" - by (simp add: real_power_two) - -lemma real_sqr_gt_zero: "(r::real) \ 0 ==> 0 < r\" -proof - - assume "r \ 0" - hence "0 \ r\" by simp - also have "0 \ r\" by (simp add: real_sqr_ge_zero) - finally show ?thesis . -qed - -lemma real_sqr_not_zero: "r \ 0 ==> (r::real)\ \ 0" - by simp - subsection{*Various Other Theorems*} @@ -333,25 +159,19 @@ by (auto intro: real_sum_squares_cancel) lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" -apply (auto simp add: left_distrib right_distrib real_diff_def) -done +by (auto simp add: left_distrib right_distrib real_diff_def) -lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)" +lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)" apply auto apply (drule right_minus_eq [THEN iffD2]) apply (auto simp add: real_squared_diff_one_factored) done -declare real_mult_is_one [iff] lemma real_le_add_half_cancel: "(x + y/2 \ (y::real)) = (x \ y /2)" -apply auto -done -declare real_le_add_half_cancel [simp] +by auto -lemma real_minus_half_eq: "(x::real) - x/2 = x/2" -apply auto -done -declare real_minus_half_eq [simp] +lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2" +by auto lemma real_mult_inverse_cancel: "[|(0::real) < x; 0 < x1; x1 * y < x * u |] @@ -364,34 +184,22 @@ done text{*Used once: in Hyperreal/Transcendental.ML*} -lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" +lemma real_mult_inverse_cancel2: + "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) done -lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))" -apply auto -done -declare inverse_real_of_nat_gt_zero [simp] +lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))" +by auto -lemma inverse_real_of_nat_ge_zero: "0 \ inverse (real (Suc n))" -apply auto -done -declare inverse_real_of_nat_ge_zero [simp] +lemma inverse_real_of_nat_ge_zero [simp]: "0 \ inverse (real (Suc n))" +by auto lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)" -apply (blast dest!: real_sum_squares_cancel) -done +by (blast dest!: real_sum_squares_cancel) lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)" -apply (blast dest!: real_sum_squares_cancel2) -done - -(* nice theorem *) -lemma abs_mult_abs: "abs x * abs x = x * (x::real)" -apply (insert linorder_less_linear [of x 0]) -apply (auto simp add: abs_eqI2 abs_minus_eqI2) -done -declare abs_mult_abs [simp] +by (blast dest!: real_sum_squares_cancel2) subsection {*Various Other Theorems*} @@ -399,50 +207,29 @@ lemma realpow_divide: "(x/y) ^ n = ((x::real) ^ n/ y ^ n)" apply (unfold real_divide_def) -apply (auto simp add: realpow_mult realpow_inverse) -done - -lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \ r --> 0 \ r ^ n" -apply (induct_tac "n") -apply (auto simp add: zero_le_mult_iff) +apply (auto simp add: power_mult_distrib power_inverse) done -lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \ x & x \ y --> x ^ n \ y ^ n" -apply (induct_tac "n") -apply (auto intro!: mult_mono simp add: realpow_ge_zero2) -done - -lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)" -apply (frule_tac n = "n" in realpow_ge_one) -apply (drule real_le_imp_less_or_eq, safe) -apply (frule zero_less_one [THEN real_less_trans]) -apply (drule_tac y = "r ^ n" in real_mult_less_mono2) -apply assumption -apply (auto dest: real_less_trans) +lemma realpow_two_sum_zero_iff [simp]: + "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 + simp add: real_power_two) done -lemma realpow_two_sum_zero_iff: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: numeral_2_eq_2) -done -declare realpow_two_sum_zero_iff [simp] - -lemma realpow_two_le_add_order: "(0::real) \ u ^ 2 + v ^ 2" +lemma realpow_two_le_add_order [simp]: "(0::real) \ u ^ 2 + v ^ 2" apply (rule real_le_add_order) -apply (auto simp add: numeral_2_eq_2) +apply (auto simp add: real_power_two) done -declare realpow_two_le_add_order [simp] -lemma realpow_two_le_add_order2: "(0::real) \ u ^ 2 + v ^ 2 + w ^ 2" +lemma realpow_two_le_add_order2 [simp]: "(0::real) \ u ^ 2 + v ^ 2 + w ^ 2" apply (rule real_le_add_order)+ -apply (auto simp add: numeral_2_eq_2) +apply (auto simp add: real_power_two) done -declare realpow_two_le_add_order2 [simp] lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y" -apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero) +apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero) apply (drule real_le_imp_less_or_eq) -apply (drule_tac y = "y" in real_sum_squares_not_zero) -apply auto +apply (drule_tac y = y in real_sum_squares_not_zero, auto) done lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y" @@ -450,48 +237,29 @@ apply (erule real_sum_square_gt_zero) done -lemma real_minus_mult_self_le: "-(u * u) \ (x * (x::real))" -apply (rule_tac j = "0" in real_le_trans) -apply auto -done -declare real_minus_mult_self_le [simp] +lemma real_minus_mult_self_le [simp]: "-(u * u) \ (x * (x::real))" +by (rule_tac j = 0 in real_le_trans, auto) -lemma realpow_square_minus_le: "-(u ^ 2) \ (x::real) ^ 2" -apply (auto simp add: numeral_2_eq_2) -done -declare realpow_square_minus_le [simp] +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \ (x::real) ^ 2" +by (auto simp add: real_power_two) lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))" -apply (case_tac "n") -apply auto -done +by (case_tac "n", auto) -lemma real_num_zero_less_two_pow: "0 < (2::real) ^ (4*d)" +lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)" apply (induct_tac "d") apply (auto simp add: realpow_num_eq_if) done -declare real_num_zero_less_two_pow [simp] -lemma lemma_realpow_num_two_mono: "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)" +lemma lemma_realpow_num_two_mono: + "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)" apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ") apply (simp (no_asm_simp) add: real_mult_assoc [symmetric]) apply (auto simp add: realpow_num_eq_if) done -lemma lemma_realpow_4: "2 ^ 2 = (4::real)" -apply (simp (no_asm) add: realpow_num_eq_if) -done -declare lemma_realpow_4 [simp] - -lemma lemma_realpow_16: "2 ^ 4 = (16::real)" -apply (simp (no_asm) add: realpow_num_eq_if) -done -declare lemma_realpow_16 [simp] - -lemma zero_le_x_squared: "(0::real) \ x^2" -apply (simp add: numeral_2_eq_2) -done -declare zero_le_x_squared [simp] +lemma zero_le_x_squared [simp]: "(0::real) \ x^2" +by (simp add: real_power_two) @@ -500,67 +268,33 @@ val realpow_0 = thm "realpow_0"; val realpow_Suc = thm "realpow_Suc"; -val realpow_zero = thm "realpow_zero"; val realpow_not_zero = thm "realpow_not_zero"; val realpow_zero_zero = thm "realpow_zero_zero"; -val realpow_inverse = thm "realpow_inverse"; -val realpow_abs = thm "realpow_abs"; -val realpow_add = thm "realpow_add"; -val realpow_one = thm "realpow_one"; val realpow_two = thm "realpow_two"; -val realpow_gt_zero = thm "realpow_gt_zero"; -val realpow_ge_zero = thm "realpow_ge_zero"; -val realpow_le = thm "realpow_le"; -val realpow_0_left = thm "realpow_0_left"; val realpow_less = thm "realpow_less"; -val realpow_eq_one = thm "realpow_eq_one"; val abs_realpow_minus_one = thm "abs_realpow_minus_one"; -val realpow_mult = thm "realpow_mult"; val realpow_two_le = thm "realpow_two_le"; val abs_realpow_two = thm "abs_realpow_two"; val realpow_two_abs = thm "realpow_two_abs"; -val realpow_two_gt_one = thm "realpow_two_gt_one"; -val realpow_ge_one = thm "realpow_ge_one"; -val realpow_ge_one2 = thm "realpow_ge_one2"; val two_realpow_ge_one = thm "two_realpow_ge_one"; val two_realpow_gt = thm "two_realpow_gt"; val realpow_minus_one = thm "realpow_minus_one"; val realpow_minus_one_odd = thm "realpow_minus_one_odd"; val realpow_minus_one_even = thm "realpow_minus_one_even"; -val realpow_Suc_less = thm "realpow_Suc_less"; -val realpow_Suc_le = thm "realpow_Suc_le"; -val realpow_zero_le = thm "realpow_zero_le"; -val realpow_Suc_le2 = thm "realpow_Suc_le2"; -val realpow_Suc_le3 = thm "realpow_Suc_le3"; -val realpow_less_le = thm "realpow_less_le"; -val realpow_le_le = thm "realpow_le_le"; val realpow_Suc_le_self = thm "realpow_Suc_le_self"; val realpow_Suc_less_one = thm "realpow_Suc_less_one"; -val realpow_le_Suc = thm "realpow_le_Suc"; -val realpow_less_Suc = thm "realpow_less_Suc"; -val realpow_le_Suc2 = thm "realpow_le_Suc2"; -val realpow_gt_ge2 = thm "realpow_gt_ge2"; -val realpow_ge_ge2 = thm "realpow_ge_ge2"; -val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2"; -val realpow_ge_self2 = thm "realpow_ge_self2"; val realpow_minus_mult = thm "realpow_minus_mult"; val realpow_two_mult_inverse = thm "realpow_two_mult_inverse"; val realpow_two_minus = thm "realpow_two_minus"; val realpow_two_disj = thm "realpow_two_disj"; -val realpow_diff = thm "realpow_diff"; val realpow_real_of_nat = thm "realpow_real_of_nat"; val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos"; val realpow_increasing = thm "realpow_increasing"; -val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq"; -val realpow_eq_0_iff = thm "realpow_eq_0_iff"; val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff"; val zero_le_realpow_abs = thm "zero_le_realpow_abs"; val real_of_int_power = thm "real_of_int_power"; val power_real_number_of = thm "power_real_number_of"; val real_power_two = thm "real_power_two"; -val real_sqr_ge_zero = thm "real_sqr_ge_zero"; -val real_sqr_gt_zero = thm "real_sqr_gt_zero"; -val real_sqr_not_zero = thm "real_sqr_not_zero"; val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a"; val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2"; val real_squared_diff_one_factored = thm "real_squared_diff_one_factored"; @@ -573,12 +307,8 @@ val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero"; val real_sum_squares_not_zero = thm "real_sum_squares_not_zero"; val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2"; -val abs_mult_abs = thm "abs_mult_abs"; val realpow_divide = thm "realpow_divide"; -val realpow_ge_zero2 = thm "realpow_ge_zero2"; -val realpow_le2 = thm "realpow_le2"; -val realpow_Suc_gt_one = thm "realpow_Suc_gt_one"; val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff"; val realpow_two_le_add_order = thm "realpow_two_le_add_order"; val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2"; @@ -589,8 +319,6 @@ val realpow_num_eq_if = thm "realpow_num_eq_if"; val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow"; val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono"; -val lemma_realpow_4 = thm "lemma_realpow_4"; -val lemma_realpow_16 = thm "lemma_realpow_16"; val zero_le_x_squared = thm "zero_le_x_squared"; *} diff -r 1fff56703e29 -r 744c868ee0b7 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/Ring_and_Field.thy Fri Jan 09 10:46:18 2004 +0100 @@ -38,6 +38,7 @@ diff_minus: "a - b = a + (-b)" axclass ordered_semiring \ semiring, linorder + zero_less_one: "0 < 1" --{*This axiom too is needed for semirings only.*} add_left_mono: "a \ b ==> c + a \ c + b" mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b" @@ -484,6 +485,22 @@ "[|a \ b; 0 \ c|] ==> a*c \ b * (c::'a::ordered_semiring)" by (simp add: mult_left_mono mult_commute [of _ c]) +lemma mult_left_le_imp_le: + "[|c*a \ c*b; 0 < c|] ==> a \ (b::'a::ordered_semiring)" + by (force simp add: mult_strict_left_mono linorder_not_less [symmetric]) + +lemma mult_right_le_imp_le: + "[|a*c \ b*c; 0 < c|] ==> a \ (b::'a::ordered_semiring)" + by (force simp add: mult_strict_right_mono linorder_not_less [symmetric]) + +lemma mult_left_less_imp_less: + "[|c*a < c*b; 0 \ c|] ==> a < (b::'a::ordered_semiring)" + by (force simp add: mult_left_mono linorder_not_le [symmetric]) + +lemma mult_right_less_imp_less: + "[|a*c < b*c; 0 \ c|] ==> a < (b::'a::ordered_semiring)" + by (force simp add: mult_right_mono linorder_not_le [symmetric]) + lemma mult_strict_left_mono_neg: "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)" apply (drule mult_strict_left_mono [of _ _ "-c"]) @@ -552,12 +569,7 @@ lemma zero_le_square: "(0::'a::ordered_ring) \ a*a" by (simp add: zero_le_mult_iff linorder_linear) -lemma zero_less_one: "(0::'a::ordered_ring) < 1" -apply (insert zero_le_square [of 1]) -apply (simp add: order_less_le) -done - -lemma zero_le_one: "(0::'a::ordered_ring) \ 1" +lemma zero_le_one: "(0::'a::ordered_semiring) \ 1" by (rule zero_less_one [THEN order_less_imp_le]) @@ -708,7 +720,7 @@ text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement of an ordering.*} -lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)" +lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)" proof cases assume "a=0" thus ?thesis by simp next @@ -733,7 +745,7 @@ by (simp add: mult_assoc cnz) qed -lemma field_mult_cancel_right: +lemma field_mult_cancel_right [simp]: "(a*c = b*c) = (c = (0::'a::field) | a=b)" proof cases assume "c=0" thus ?thesis by simp @@ -742,7 +754,7 @@ thus ?thesis by (force dest: field_mult_cancel_right_lemma) qed -lemma field_mult_cancel_left: +lemma field_mult_cancel_left [simp]: "(c*a = c*b) = (c = (0::'a::field) | a=b)" by (simp add: mult_commute [of c] field_mult_cancel_right) @@ -1401,6 +1413,10 @@ minus_mult_left [symmetric] minus_mult_right [symmetric]) done + +lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)" +by (simp add: abs_if) + lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))" by (simp add: abs_if) @@ -1617,6 +1633,10 @@ val mult_strict_right_mono = thm"mult_strict_right_mono"; val mult_left_mono = thm"mult_left_mono"; val mult_right_mono = thm"mult_right_mono"; +val mult_left_le_imp_le = thm"mult_left_le_imp_le"; +val mult_right_le_imp_le = thm"mult_right_le_imp_le"; +val mult_left_less_imp_less = thm"mult_left_less_imp_less"; +val mult_right_less_imp_less = thm"mult_right_less_imp_less"; val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg"; val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg"; val mult_pos = thm"mult_pos"; @@ -1744,6 +1764,7 @@ val abs_zero = thm"abs_zero"; val abs_one = thm"abs_one"; val abs_mult = thm"abs_mult"; +val abs_mult_self = thm"abs_mult_self"; val abs_eq_0 = thm"abs_eq_0"; val zero_less_abs_iff = thm"zero_less_abs_iff"; val abs_not_less_zero = thm"abs_not_less_zero";