cleaned up
authorhuffman
Mon May 14 08:15:13 2007 +0200 (2007-05-14)
changeset 22958b3a5569a81e5
parent 22957 82a799ae7579
child 22959 07a7c2900877
cleaned up
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon May 14 08:12:38 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Mon May 14 08:15:13 2007 +0200
     1.3 @@ -112,13 +112,7 @@
     1.4  lemma realrel_in_real [simp]: "realrel``{(x,y)}: Real"
     1.5  by (simp add: Real_def realrel_def quotient_def, blast)
     1.6  
     1.7 -
     1.8 -lemma inj_on_Abs_Real: "inj_on Abs_Real Real"
     1.9 -apply (rule inj_on_inverseI)
    1.10 -apply (erule Abs_Real_inverse)
    1.11 -done
    1.12 -
    1.13 -declare inj_on_Abs_Real [THEN inj_on_iff, simp]
    1.14 +declare Abs_Real_inject [simp]
    1.15  declare Abs_Real_inverse [simp]
    1.16  
    1.17  
    1.18 @@ -299,11 +293,6 @@
    1.19    show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
    1.20  qed
    1.21  
    1.22 -
    1.23 -(*Pull negations out*)
    1.24 -declare minus_mult_right [symmetric, simp] 
    1.25 -        minus_mult_left [symmetric, simp]
    1.26 -
    1.27  lemma real_mult_1_right: "z * (1::real) = z"
    1.28    by (rule OrderedGroup.mult_1_right)
    1.29  
    1.30 @@ -602,26 +591,19 @@
    1.31  done
    1.32  
    1.33  lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
    1.34 -by (drule add_strict_mono [of concl: 0 0], assumption, simp)
    1.35 +by (rule add_pos_pos)
    1.36  
    1.37  lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
    1.38 -apply (drule order_le_imp_less_or_eq)+
    1.39 -apply (auto intro: real_add_order order_less_imp_le)
    1.40 -done
    1.41 +by (rule add_nonneg_nonneg)
    1.42  
    1.43  lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
    1.44 -apply (case_tac "x \<noteq> 0")
    1.45 -apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto)
    1.46 -done
    1.47 +by (rule inverse_unique [symmetric])
    1.48  
    1.49  lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
    1.50 -by (auto dest: less_imp_inverse_less)
    1.51 +by (simp add: one_less_inverse_iff)
    1.52  
    1.53  lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
    1.54 -proof -
    1.55 -  have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square)
    1.56 -  thus ?thesis by simp
    1.57 -qed
    1.58 +by (intro add_nonneg_nonneg zero_le_square)
    1.59  
    1.60  
    1.61  subsection{*Embedding the Integers into the Reals*}
    1.62 @@ -1017,7 +999,7 @@
    1.63  by (simp add: abs_if)
    1.64  
    1.65  lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
    1.66 -by (simp add: real_of_nat_ge_zero)
    1.67 +by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
    1.68  
    1.69  lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
    1.70  by simp
     2.1 --- a/src/HOL/Real/RealPow.thy	Mon May 14 08:12:38 2007 +0200
     2.2 +++ b/src/HOL/Real/RealPow.thy	Mon May 14 08:15:13 2007 +0200
     2.3 @@ -67,7 +67,7 @@
     2.4  by (insert power_decreasing [of 1 "Suc n" r], simp)
     2.5  
     2.6  lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
     2.7 -by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
     2.8 +by (rule power_Suc_less_one)
     2.9  
    2.10  lemma realpow_minus_mult [rule_format]:
    2.11       "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
    2.12 @@ -115,9 +115,7 @@
    2.13  done
    2.14  
    2.15  lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
    2.16 -apply (induct "n")
    2.17 -apply (auto simp add: zero_le_mult_iff)
    2.18 -done
    2.19 +by (rule zero_le_power_abs)
    2.20  
    2.21  
    2.22  subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}