src/HOL/NthRoot.thy
changeset 44320 33439faadd67
parent 44289 d81d09cdab9c
child 44349 f057535311c5
     1.1 --- a/src/HOL/NthRoot.thy	Fri Aug 19 18:42:41 2011 -0700
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Aug 19 19:01:00 2011 -0700
     1.3 @@ -518,12 +518,6 @@
     1.4  apply (rule real_sqrt_abs)
     1.5  done
     1.6  
     1.7 -lemma real_sqrt_pow2_gt_zero: "0 < x ==> 0 < (sqrt x)\<twosuperior>"
     1.8 -by simp (* TODO: delete *)
     1.9 -
    1.10 -lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 0"
    1.11 -by simp (* TODO: delete *)
    1.12 -
    1.13  lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
    1.14  by (simp add: power_inverse [symmetric])
    1.15  
    1.16 @@ -533,15 +527,6 @@
    1.17  lemma real_sqrt_ge_one: "1 \<le> x ==> 1 \<le> sqrt x"
    1.18  by simp
    1.19  
    1.20 -lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2"
    1.21 -by simp
    1.22 -
    1.23 -lemma real_sqrt_two_ge_zero [simp]: "0 \<le> sqrt 2"
    1.24 -by simp
    1.25 -
    1.26 -lemma real_sqrt_two_gt_one [simp]: "1 < sqrt 2"
    1.27 -by simp
    1.28 -
    1.29  lemma sqrt_divide_self_eq:
    1.30    assumes nneg: "0 \<le> x"
    1.31    shows "sqrt x / x = inverse (sqrt x)"
    1.32 @@ -575,21 +560,18 @@
    1.33  
    1.34  subsection {* Square Root of Sum of Squares *}
    1.35  
    1.36 -lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
    1.37 -by (rule real_sqrt_ge_zero [OF sum_squares_ge_zero])
    1.38 -
    1.39 -lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.40 -by simp
    1.41 +lemma real_sqrt_sum_squares_ge_zero: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.42 +  by simp (* TODO: delete *)
    1.43  
    1.44  declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
    1.45  
    1.46  lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
    1.47       "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
    1.48 -by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
    1.49 +  by (simp add: zero_le_mult_iff)
    1.50  
    1.51  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
    1.52       "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
    1.53 -by (auto simp add: zero_le_mult_iff)
    1.54 +  by (simp add: zero_le_mult_iff)
    1.55  
    1.56  lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<twosuperior> + y\<twosuperior>) = x \<Longrightarrow> y = 0"
    1.57  by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)