move lemmas to RealPow.thy; tuned proofs
authorhuffman
Mon May 14 18:48:24 2007 +0200 (2007-05-14)
changeset 22970b5910e3dec4c
parent 22969 bf523cac9a05
child 22971 a6812b6a36a5
move lemmas to RealPow.thy; tuned proofs
src/HOL/Complex/NSComplex.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Real/real_arith.ML
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Mon May 14 18:04:52 2007 +0200
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon May 14 18:48:24 2007 +0200
     1.3 @@ -436,10 +436,6 @@
     1.4  lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
     1.5  by transfer (rule Im_sgn)
     1.6  
     1.7 -(*????move to RealDef????*)
     1.8 -lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
     1.9 -by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
    1.10 -
    1.11  lemma hcomplex_inverse_complex_split:
    1.12       "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
    1.13        hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
     2.1 --- a/src/HOL/Real/RealDef.thy	Mon May 14 18:04:52 2007 +0200
     2.2 +++ b/src/HOL/Real/RealDef.thy	Mon May 14 18:48:24 2007 +0200
     2.3 @@ -557,18 +557,6 @@
     2.4  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
     2.5  by(simp add:mult_commute)
     2.6  
     2.7 -text{*FIXME: delete or at least combine the next two lemmas*}
     2.8 -lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
     2.9 -apply (drule OrderedGroup.equals_zero_I [THEN sym])
    2.10 -apply (cut_tac x = y in real_le_square) 
    2.11 -apply (auto, drule order_antisym, auto)
    2.12 -done
    2.13 -
    2.14 -lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
    2.15 -apply (rule_tac y = x in real_sum_squares_cancel)
    2.16 -apply (simp add: add_commute)
    2.17 -done
    2.18 -
    2.19  lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
    2.20  by (rule add_pos_pos)
    2.21  
    2.22 @@ -581,9 +569,6 @@
    2.23  lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
    2.24  by (simp add: one_less_inverse_iff)
    2.25  
    2.26 -lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
    2.27 -by (intro add_nonneg_nonneg zero_le_square)
    2.28 -
    2.29  
    2.30  subsection{*Embedding the Integers into the Reals*}
    2.31  
     3.1 --- a/src/HOL/Real/RealPow.thy	Mon May 14 18:04:52 2007 +0200
     3.2 +++ b/src/HOL/Real/RealPow.thy	Mon May 14 18:48:24 2007 +0200
     3.3 @@ -187,15 +187,26 @@
     3.4  unfolding power2_eq_square by (rule sum_squares_gt_zero_iff)
     3.5  
     3.6  
     3.7 -subsection{*Various Other Theorems*}
     3.8 +subsection{* Squares of Reals *}
     3.9 +
    3.10 +lemma real_two_squares_add_zero_iff [simp]:
    3.11 +  "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
    3.12 +by (rule sum_squares_eq_zero_iff)
    3.13 +
    3.14 +lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
    3.15 +by simp
    3.16 +
    3.17 +lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
    3.18 +by simp
    3.19 +
    3.20 +lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
    3.21 +by (rule sum_squares_ge_zero)
    3.22  
    3.23  lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
    3.24 -  apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
    3.25 -  apply (auto dest: real_sum_squares_cancel simp add: add_commute)
    3.26 -  done
    3.27 +by (simp add: real_add_eq_0_iff [symmetric])
    3.28  
    3.29  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
    3.30 -by (auto simp add: left_distrib right_distrib real_diff_def)
    3.31 +by (simp add: left_distrib right_diff_distrib)
    3.32  
    3.33  lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
    3.34  apply auto
    3.35 @@ -203,6 +214,49 @@
    3.36  apply (auto simp add: real_squared_diff_one_factored)
    3.37  done
    3.38  
    3.39 +lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
    3.40 +by simp
    3.41 +
    3.42 +lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
    3.43 +by simp
    3.44 +
    3.45 +lemma realpow_two_sum_zero_iff [simp]:
    3.46 +     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
    3.47 +by (rule sum_power2_eq_zero_iff)
    3.48 +
    3.49 +lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
    3.50 +by (rule sum_power2_ge_zero)
    3.51 +
    3.52 +lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
    3.53 +by (intro add_nonneg_nonneg zero_le_power2)
    3.54 +
    3.55 +lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
    3.56 +by (simp add: sum_squares_gt_zero_iff)
    3.57 +
    3.58 +lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
    3.59 +by (simp add: sum_squares_gt_zero_iff)
    3.60 +
    3.61 +lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
    3.62 +by (rule_tac j = 0 in real_le_trans, auto)
    3.63 +
    3.64 +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    3.65 +by (auto simp add: power2_eq_square)
    3.66 +
    3.67 +(* The following theorem is by Benjamin Porter *)
    3.68 +lemma real_sq_order:
    3.69 +  fixes x::real
    3.70 +  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
    3.71 +  shows "x \<le> y"
    3.72 +proof -
    3.73 +  from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
    3.74 +    by (simp only: numeral_2_eq_2)
    3.75 +  thus "x \<le> y" using ygt0
    3.76 +    by (rule power_le_imp_le_base)
    3.77 +qed
    3.78 +
    3.79 +
    3.80 +subsection {*Various Other Theorems*}
    3.81 +
    3.82  lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
    3.83  by auto
    3.84  
    3.85 @@ -230,60 +284,6 @@
    3.86  lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
    3.87  by simp
    3.88  
    3.89 -lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
    3.90 -by (blast dest!: real_sum_squares_cancel)
    3.91 -
    3.92 -lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
    3.93 -by (blast dest!: real_sum_squares_cancel2)
    3.94 -
    3.95 -
    3.96 -subsection {*Various Other Theorems*}
    3.97 -
    3.98 -lemma realpow_two_sum_zero_iff [simp]:
    3.99 -     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
   3.100 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
   3.101 -                   simp add: power2_eq_square)
   3.102 -done
   3.103 -
   3.104 -lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
   3.105 -apply (rule real_le_add_order)
   3.106 -apply (auto simp add: power2_eq_square)
   3.107 -done
   3.108 -
   3.109 -lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
   3.110 -apply (rule real_le_add_order)+
   3.111 -apply (auto simp add: power2_eq_square)
   3.112 -done
   3.113 -
   3.114 -lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
   3.115 -apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero)
   3.116 -apply (drule real_le_imp_less_or_eq)
   3.117 -apply (drule_tac y = y in real_sum_squares_not_zero, auto)
   3.118 -done
   3.119 -
   3.120 -lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
   3.121 -apply (rule real_add_commute [THEN subst])
   3.122 -apply (erule real_sum_square_gt_zero)
   3.123 -done
   3.124 -
   3.125 -lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
   3.126 -by (rule_tac j = 0 in real_le_trans, auto)
   3.127 -
   3.128 -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
   3.129 -by (auto simp add: power2_eq_square)
   3.130 -
   3.131 -(* The following theorem is by Benjamin Porter *)
   3.132 -lemma real_sq_order:
   3.133 -  fixes x::real
   3.134 -  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
   3.135 -  shows "x \<le> y"
   3.136 -proof -
   3.137 -  from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
   3.138 -    by (simp only: numeral_2_eq_2)
   3.139 -  thus "x \<le> y" using ygt0
   3.140 -    by (rule power_le_imp_le_base)
   3.141 -qed
   3.142 -
   3.143  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
   3.144  by (case_tac "n", auto)
   3.145  
     4.1 --- a/src/HOL/Real/real_arith.ML	Mon May 14 18:04:52 2007 +0200
     4.2 +++ b/src/HOL/Real/real_arith.ML	Mon May 14 18:48:24 2007 +0200
     4.3 @@ -44,15 +44,12 @@
     4.4  val real_mult_order = thm "real_mult_order";
     4.5  val real_add_order = thm "real_add_order";
     4.6  val real_le_add_order = thm "real_le_add_order";
     4.7 -val real_le_square = thm "real_le_square";
     4.8  val real_mult_less_mono2 = thm "real_mult_less_mono2";
     4.9  
    4.10  val real_mult_less_iff1 = thm "real_mult_less_iff1";
    4.11  val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
    4.12  val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
    4.13  val real_mult_less_mono = thm "real_mult_less_mono";
    4.14 -val real_sum_squares_cancel = thm "real_sum_squares_cancel";
    4.15 -val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
    4.16  
    4.17  val real_mult_left_cancel = thm"real_mult_left_cancel";
    4.18  val real_mult_right_cancel = thm"real_mult_right_cancel";