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.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.16 @@ -533,15 +527,6 @@
1.17  lemma real_sqrt_ge_one: "1 \<le> x ==> 1 \<le> sqrt x"
1.18  by simp
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.34  subsection {* Square Root of Sum of Squares *}
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.44  declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
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.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.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)