src/HOL/Real/RealDef.thy
changeset 22958 b3a5569a81e5
parent 22456 6070e48ecb78
child 22962 4bb05ba38939
     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