simplify some proofs
authorhuffman
Fri May 25 00:36:54 2007 +0200 (2007-05-25)
changeset 23097f4779adcd1a2
parent 23096 423ad2fe9f76
child 23098 11e1a67fbfe8
simplify some proofs
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 24 22:55:53 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Fri May 25 00:36:54 2007 +0200
     1.3 @@ -1027,12 +1027,7 @@
     1.4  by arith
     1.5  
     1.6  lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
     1.7 -apply (auto simp add: linorder_not_less [symmetric])
     1.8 -apply (drule_tac n = "Suc 0" in power_gt1)
     1.9 -apply (auto simp del: realpow_Suc)
    1.10 -apply (drule_tac r1 = "cos x" in realpow_two_le [THEN [2] real_gt_one_ge_zero_add_less])
    1.11 -apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
    1.12 -done
    1.13 +by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
    1.14  
    1.15  lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
    1.16  apply (insert abs_sin_le_one [of x]) 
    1.17 @@ -1045,12 +1040,7 @@
    1.18  done
    1.19  
    1.20  lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
    1.21 -apply (auto simp add: linorder_not_less [symmetric])
    1.22 -apply (drule_tac n = "Suc 0" in power_gt1)
    1.23 -apply (auto simp del: realpow_Suc)
    1.24 -apply (drule_tac r1 = "sin x" in realpow_two_le [THEN [2] real_gt_one_ge_zero_add_less])
    1.25 -apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
    1.26 -done
    1.27 +by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
    1.28  
    1.29  lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
    1.30  apply (insert abs_cos_le_one [of x])