remove redundant lemmas
authorhuffman
Mon May 14 09:27:24 2007 +0200 (2007-05-14)
changeset 22961e499ded5d0fc
parent 22960 114cf1906681
child 22962 4bb05ba38939
remove redundant lemmas
src/HOL/Hyperreal/NthRoot.thy
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 09:16:47 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 09:27:24 2007 +0200
     1.3 @@ -474,14 +474,11 @@
     1.4  
     1.5  subsection {* Square Root of Sum of Squares *}
     1.6  
     1.7 -lemma "(sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior> = x\<twosuperior> + y\<twosuperior>"
     1.8 -by simp
     1.9 -
    1.10  lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
    1.11 -by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero]) 
    1.12 +by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero])
    1.13  
    1.14  lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.15 -by (auto intro!: real_sqrt_ge_zero)
    1.16 +by simp
    1.17  
    1.18  lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
    1.19       "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
    1.20 @@ -497,12 +494,6 @@
    1.21  lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
    1.22  by (rule power2_le_imp_le, simp_all)
    1.23  
    1.24 -lemma real_sqrt_sos_less_one_iff: "(sqrt (x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
    1.25 -by (rule real_sqrt_lt_1_iff)
    1.26 -
    1.27 -lemma real_sqrt_sos_eq_one_iff: "(sqrt (x\<twosuperior> + y\<twosuperior>) = 1) = (x\<twosuperior> + y\<twosuperior> = 1)"
    1.28 -by (rule real_sqrt_eq_1_iff)
    1.29 -
    1.30  lemma power2_sum:
    1.31    fixes x y :: "'a::{number_ring,recpower}"
    1.32    shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"