src/HOL/Real/RealPow.thy
changeset 22970 b5910e3dec4c
parent 22967 0651b224528a
child 23096 423ad2fe9f76
     1.1 --- a/src/HOL/Real/RealPow.thy	Mon May 14 18:04:52 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Mon May 14 18:48:24 2007 +0200
     1.3 @@ -187,15 +187,26 @@
     1.4  unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
     1.5  
     1.6  
     1.7 -subsection{*Various Other Theorems*}
     1.8 +subsection{* Squares of Reals *}
     1.9 +
    1.10 +lemma real_two_squares_add_zero_iff [simp]:
    1.11 +  "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
    1.12 +by (rule sum_squares_eq_zero_iff)
    1.13 +
    1.14 +lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
    1.15 +by simp
    1.16 +
    1.17 +lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
    1.18 +by simp
    1.19 +
    1.20 +lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
    1.21 +by (rule sum_squares_ge_zero)
    1.22  
    1.23  lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
    1.24 -  apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
    1.25 -  apply (auto dest: real_sum_squares_cancel simp add: add_commute)
    1.26 -  done
    1.27 +by (simp add: real_add_eq_0_iff [symmetric])
    1.28  
    1.29  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
    1.30 -by (auto simp add: left_distrib right_distrib real_diff_def)
    1.31 +by (simp add: left_distrib right_diff_distrib)
    1.32  
    1.33  lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
    1.34  apply auto
    1.35 @@ -203,6 +214,49 @@
    1.36  apply (auto simp add: real_squared_diff_one_factored)
    1.37  done
    1.38  
    1.39 +lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
    1.40 +by simp
    1.41 +
    1.42 +lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
    1.43 +by simp
    1.44 +
    1.45 +lemma realpow_two_sum_zero_iff [simp]:
    1.46 +     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
    1.47 +by (rule sum_power2_eq_zero_iff)
    1.48 +
    1.49 +lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
    1.50 +by (rule sum_power2_ge_zero)
    1.51 +
    1.52 +lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
    1.53 +by (intro add_nonneg_nonneg zero_le_power2)
    1.54 +
    1.55 +lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
    1.56 +by (simp add: sum_squares_gt_zero_iff)
    1.57 +
    1.58 +lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
    1.59 +by (simp add: sum_squares_gt_zero_iff)
    1.60 +
    1.61 +lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
    1.62 +by (rule_tac j = 0 in real_le_trans, auto)
    1.63 +
    1.64 +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    1.65 +by (auto simp add: power2_eq_square)
    1.66 +
    1.67 +(* The following theorem is by Benjamin Porter *)
    1.68 +lemma real_sq_order:
    1.69 +  fixes x::real
    1.70 +  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
    1.71 +  shows "x \<le> y"
    1.72 +proof -
    1.73 +  from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
    1.74 +    by (simp only: numeral_2_eq_2)
    1.75 +  thus "x \<le> y" using ygt0
    1.76 +    by (rule power_le_imp_le_base)
    1.77 +qed
    1.78 +
    1.79 +
    1.80 +subsection {*Various Other Theorems*}
    1.81 +
    1.82  lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
    1.83  by auto
    1.84  
    1.85 @@ -230,60 +284,6 @@
    1.86  lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
    1.87  by simp
    1.88  
    1.89 -lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
    1.90 -by (blast dest!: real_sum_squares_cancel)
    1.91 -
    1.92 -lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
    1.93 -by (blast dest!: real_sum_squares_cancel2)
    1.94 -
    1.95 -
    1.96 -subsection {*Various Other Theorems*}
    1.97 -
    1.98 -lemma realpow_two_sum_zero_iff [simp]:
    1.99 -     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
   1.100 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
   1.101 -                   simp add: power2_eq_square)
   1.102 -done
   1.103 -
   1.104 -lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
   1.105 -apply (rule real_le_add_order)
   1.106 -apply (auto simp add: power2_eq_square)
   1.107 -done
   1.108 -
   1.109 -lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
   1.110 -apply (rule real_le_add_order)+
   1.111 -apply (auto simp add: power2_eq_square)
   1.112 -done
   1.113 -
   1.114 -lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
   1.115 -apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero)
   1.116 -apply (drule real_le_imp_less_or_eq)
   1.117 -apply (drule_tac y = y in real_sum_squares_not_zero, auto)
   1.118 -done
   1.119 -
   1.120 -lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
   1.121 -apply (rule real_add_commute [THEN subst])
   1.122 -apply (erule real_sum_square_gt_zero)
   1.123 -done
   1.124 -
   1.125 -lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
   1.126 -by (rule_tac j = 0 in real_le_trans, auto)
   1.127 -
   1.128 -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
   1.129 -by (auto simp add: power2_eq_square)
   1.130 -
   1.131 -(* The following theorem is by Benjamin Porter *)
   1.132 -lemma real_sq_order:
   1.133 -  fixes x::real
   1.134 -  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
   1.135 -  shows "x \<le> y"
   1.136 -proof -
   1.137 -  from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
   1.138 -    by (simp only: numeral_2_eq_2)
   1.139 -  thus "x \<le> y" using ygt0
   1.140 -    by (rule power_le_imp_le_base)
   1.141 -qed
   1.142 -
   1.143  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
   1.144  by (case_tac "n", auto)
   1.145