remove redundant lemmas
authorhuffman
Mon May 14 09:16:47 2007 +0200 (2007-05-14)
changeset 22960114cf1906681
parent 22959 07a7c2900877
child 22961 e499ded5d0fc
remove redundant lemmas
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 09:11:30 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 09:16:47 2007 +0200
     1.3 @@ -1817,7 +1817,7 @@
     1.4  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"
     1.5  apply (rule power_inverse [THEN subst])
     1.6  apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
     1.7 -apply (auto dest: realpow_not_zero 
     1.8 +apply (auto dest: field_power_not_zero
     1.9          simp add: power_mult_distrib left_distrib power_divide tan_def 
    1.10                    mult_assoc power_inverse [symmetric] 
    1.11          simp del: realpow_Suc)
    1.12 @@ -1927,7 +1927,7 @@
    1.13  qed
    1.14  
    1.15  lemma lemma_real_divide_sqrt_ge_minus_one:
    1.16 -     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))" 
    1.17 +     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))"
    1.18  by (simp add: divide_const_simps linorder_not_le [symmetric]
    1.19           del: real_sqrt_le_0_iff real_sqrt_ge_0_iff)
    1.20  
    1.21 @@ -2159,14 +2159,10 @@
    1.22  done
    1.23  
    1.24  lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.25 -apply (rule_tac n = 1 in realpow_increasing)
    1.26 -apply (auto simp add: numeral_2_eq_2 [symmetric] power2_abs)
    1.27 -done
    1.28 +by (rule power2_le_imp_le, simp_all)
    1.29  
    1.30  lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.31 -apply (rule real_add_commute [THEN subst])
    1.32 -apply (rule real_sqrt_ge_abs1)
    1.33 -done
    1.34 +by (rule power2_le_imp_le, simp_all)
    1.35  
    1.36  lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2"
    1.37  by simp
    1.38 @@ -2192,9 +2188,8 @@
    1.39       "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
    1.40  apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
    1.41  apply (erule_tac [2] lemma_real_divide_sqrt_less)
    1.42 -apply (rule_tac n = 1 in realpow_increasing)
    1.43 -apply (auto simp add: real_0_le_divide_iff power_divide numeral_2_eq_2 [symmetric] 
    1.44 -        simp del: realpow_Suc)
    1.45 +apply (rule power2_le_imp_le)
    1.46 +apply (auto simp add: real_0_le_divide_iff power_divide)
    1.47  apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
    1.48  apply (rule add_mono)
    1.49  apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)