author huffman Fri May 25 00:36:54 2007 +0200 (2007-05-25) changeset 23097 f4779adcd1a2 parent 23096 423ad2fe9f76 child 23098 11e1a67fbfe8
simplify some proofs
```     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])
```