src/HOL/Real/RealPow.thy
changeset 14304 cc0b4bbfbc43
parent 14288 d149e3cbdb39
child 14334 6137d24eef79
     1.1 --- a/src/HOL/Real/RealPow.thy	Fri Dec 19 10:38:39 2003 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Fri Dec 19 10:38:48 2003 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4  done
     1.5  declare real_mult_is_one [iff]
     1.6  
     1.7 -lemma real_le_add_half_cancel: "(x + y/2 <= (y::real)) = (x <= y /2)"
     1.8 +lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
     1.9  apply auto
    1.10  done
    1.11  declare real_le_add_half_cancel [simp]
    1.12 @@ -372,7 +372,7 @@
    1.13  done
    1.14  declare inverse_real_of_nat_gt_zero [simp]
    1.15  
    1.16 -lemma inverse_real_of_nat_ge_zero: "0 <= inverse (real (Suc n))"
    1.17 +lemma inverse_real_of_nat_ge_zero: "0 \<le> inverse (real (Suc n))"
    1.18  apply auto
    1.19  done
    1.20  declare inverse_real_of_nat_ge_zero [simp]
    1.21 @@ -401,12 +401,12 @@
    1.22  apply (auto simp add: realpow_mult realpow_inverse)
    1.23  done
    1.24  
    1.25 -lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) <= r --> 0 <= r ^ n"
    1.26 +lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
    1.27  apply (induct_tac "n")
    1.28  apply (auto simp add: real_0_le_mult_iff)
    1.29  done
    1.30  
    1.31 -lemma realpow_le2 [rule_format (no_asm)]: "(0::real) <= x & x <= y --> x ^ n <= y ^ n"
    1.32 +lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
    1.33  apply (induct_tac "n")
    1.34  apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2)
    1.35  done
    1.36 @@ -425,25 +425,18 @@
    1.37  done
    1.38  declare realpow_two_sum_zero_iff [simp]
    1.39  
    1.40 -lemma realpow_two_le_add_order: "(0::real) <= u ^ 2 + v ^ 2"
    1.41 +lemma realpow_two_le_add_order: "(0::real) \<le> u ^ 2 + v ^ 2"
    1.42  apply (rule real_le_add_order)
    1.43  apply (auto simp add: numeral_2_eq_2)
    1.44  done
    1.45  declare realpow_two_le_add_order [simp]
    1.46  
    1.47 -lemma realpow_two_le_add_order2: "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2"
    1.48 +lemma realpow_two_le_add_order2: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
    1.49  apply (rule real_le_add_order)+
    1.50  apply (auto simp add: numeral_2_eq_2)
    1.51  done
    1.52  declare realpow_two_le_add_order2 [simp]
    1.53  
    1.54 -lemma real_mult_self_sum_ge_zero: "(0::real) <= x*x + y*y"
    1.55 -apply (cut_tac u = "x" and v = "y" in realpow_two_le_add_order)
    1.56 -apply (auto simp add: numeral_2_eq_2)
    1.57 -done
    1.58 -declare real_mult_self_sum_ge_zero [simp]
    1.59 -declare real_mult_self_sum_ge_zero [THEN abs_eqI1, simp]
    1.60 -
    1.61  lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
    1.62  apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
    1.63  apply (drule real_le_imp_less_or_eq)
    1.64 @@ -456,13 +449,13 @@
    1.65  apply (erule real_sum_square_gt_zero)
    1.66  done
    1.67  
    1.68 -lemma real_minus_mult_self_le: "-(u * u) <= (x * (x::real))"
    1.69 +lemma real_minus_mult_self_le: "-(u * u) \<le> (x * (x::real))"
    1.70  apply (rule_tac j = "0" in real_le_trans)
    1.71  apply auto
    1.72  done
    1.73  declare real_minus_mult_self_le [simp]
    1.74  
    1.75 -lemma realpow_square_minus_le: "-(u ^ 2) <= (x::real) ^ 2"
    1.76 +lemma realpow_square_minus_le: "-(u ^ 2) \<le> (x::real) ^ 2"
    1.77  apply (auto simp add: numeral_2_eq_2)
    1.78  done
    1.79  declare realpow_square_minus_le [simp]
    1.80 @@ -494,7 +487,7 @@
    1.81  done
    1.82  declare lemma_realpow_16 [simp]
    1.83  
    1.84 -lemma zero_le_x_squared: "(0::real) <= x^2"
    1.85 +lemma zero_le_x_squared: "(0::real) \<le> x^2"
    1.86  apply (simp add: numeral_2_eq_2)
    1.87  done
    1.88  declare zero_le_x_squared [simp]
    1.89 @@ -588,7 +581,6 @@
    1.90  val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
    1.91  val realpow_two_le_add_order = thm "realpow_two_le_add_order";
    1.92  val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
    1.93 -val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
    1.94  val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
    1.95  val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
    1.96  val real_minus_mult_self_le = thm "real_minus_mult_self_le";