src/HOL/Real/RealPow.thy
changeset 23292 1c39f1bd1f53
parent 23291 9179346e1208
child 23293 77577fc2f141
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu Jun 07 11:25:27 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jun 07 14:26:05 2007 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
     1.8 +(*lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
     1.9  by simp
    1.10  
    1.11  lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
    1.12 @@ -37,20 +37,25 @@
    1.13  text{*Legacy: weaker version of the theorem @{text power_strict_mono}*}
    1.14  lemma realpow_less:
    1.15       "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
    1.16 +thm power_strict_mono
    1.17  apply (rule power_strict_mono, auto) 
    1.18 -done
    1.19 +done *)
    1.20 +
    1.21 +(* declare [simp del]: zero_le_power
    1.22  
    1.23  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
    1.24  by (simp)
    1.25  
    1.26 +
    1.27  lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
    1.28 -by (simp add: abs_mult)
    1.29 +by (simp)
    1.30  
    1.31  lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
    1.32 -by (simp add: power_abs [symmetric] del: realpow_Suc)
    1.33 +by (simp)
    1.34  
    1.35 +*)
    1.36  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
    1.37 -by (insert power_increasing [of 0 n "2::real"], simp)
    1.38 +by (rule power_increasing[of 0 n "2::real", simplified])
    1.39  
    1.40  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
    1.41  apply (induct "n")
    1.42 @@ -70,7 +75,7 @@
    1.43  
    1.44  lemma realpow_two_mult_inverse [simp]:
    1.45       "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
    1.46 -by (simp add: realpow_two real_mult_assoc [symmetric])
    1.47 +by (simp add:  real_mult_assoc [symmetric])
    1.48  
    1.49  lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
    1.50  by simp