author huffman Sun Oct 30 09:42:13 2011 +0100 (2011-10-30) changeset 45309 5885ec8eb6b0 parent 45308 2e84e5f0463b child 45310 adaf2184b79d
removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]
```     1.1 --- a/src/HOL/Transcendental.thy	Sun Oct 30 09:07:02 2011 +0100
1.2 +++ b/src/HOL/Transcendental.thy	Sun Oct 30 09:42:13 2011 +0100
1.3 @@ -1604,16 +1604,13 @@
1.4  by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
1.5
1.6  lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
1.8 -declare sin_cos_eq [symmetric, simp]
1.10
1.11  lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
1.13 -declare minus_sin_cos_eq [symmetric, simp]
1.14
1.15  lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
1.17 -declare cos_sin_eq [symmetric, simp]
1.19
1.20  lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
1.22 @@ -1694,12 +1691,7 @@
1.23  done
1.24
1.25  lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
1.26 -apply (subst sin_cos_eq)
1.27 -apply (rotate_tac 1)
1.28 -apply (drule real_sum_of_halves [THEN ssubst])
1.29 -apply (auto intro!: cos_gt_zero_pi simp del: sin_cos_eq [symmetric])
1.30 -done
1.31 -
1.32 +by (simp add: sin_cos_eq cos_gt_zero_pi)
1.33
1.34  lemma pi_ge_two: "2 \<le> pi"
1.35  proof (rule ccontr)
1.36 @@ -1750,13 +1742,13 @@
1.37  apply (rule ccontr)
1.38  apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
1.39  apply (erule contrapos_np)
1.40 -apply (simp del: minus_sin_cos_eq [symmetric])
1.41 +apply simp
1.42  apply (cut_tac y="-y" in cos_total, simp) apply simp
1.43  apply (erule ex1E)
1.44  apply (rule_tac a = "x - (pi/2)" in ex1I)
1.46  apply (rotate_tac 3)
1.47 -apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all)
1.48 +apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all add: cos_add)
1.49  done
1.50
1.51  lemma reals_Archimedean4:
1.52 @@ -1797,7 +1789,7 @@
1.53   apply (clarify, rule_tac x = "n - 1" in exI)
1.54   apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
1.55  apply (rule cos_zero_lemma)
1.58  done
1.59
1.60
1.61 @@ -1949,7 +1941,7 @@
1.62  apply (rule_tac x = "(pi/2) - e" in exI)
1.63  apply (simp (no_asm_simp))
1.64  apply (drule_tac x = "(pi/2) - e" in spec)
1.65 -apply (auto simp add: tan_def)
1.66 +apply (auto simp add: tan_def sin_diff cos_diff)
1.67  apply (rule inverse_less_iff_less [THEN iffD1])
1.68  apply (auto simp add: divide_inverse)
1.69  apply (rule mult_pos_pos)
1.70 @@ -2380,20 +2372,10 @@
1.71  qed
1.72
1.73  lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
1.74 -proof -
1.75 -  have "sin (pi / 4) = cos (pi / 2 - pi / 4)" by (rule sin_cos_eq)
1.76 -  also have "pi / 2 - pi / 4 = pi / 4" by simp
1.77 -  also have "cos (pi / 4) = sqrt 2 / 2" by (rule cos_45)
1.78 -  finally show ?thesis .
1.79 -qed
1.80 +by (simp add: sin_cos_eq cos_45)
1.81
1.82  lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
1.83 -proof -
1.84 -  have "sin (pi / 3) = cos (pi / 2 - pi / 3)" by (rule sin_cos_eq)
1.85 -  also have "pi / 2 - pi / 3 = pi / 6" by simp
1.86 -  also have "cos (pi / 6) = sqrt 3 / 2" by (rule cos_30)
1.87 -  finally show ?thesis .
1.88 -qed
1.89 +by (simp add: sin_cos_eq cos_30)
1.90
1.91  lemma cos_60: "cos (pi / 3) = 1 / 2"
1.92  apply (rule power2_eq_imp_eq)
1.93 @@ -2402,12 +2384,7 @@
1.94  done
1.95
1.96  lemma sin_30: "sin (pi / 6) = 1 / 2"
1.97 -proof -
1.98 -  have "sin (pi / 6) = cos (pi / 2 - pi / 6)" by (rule sin_cos_eq)
1.99 -  also have "pi / 2 - pi / 6 = pi / 3" by simp
1.100 -  also have "cos (pi / 3) = 1 / 2" by (rule cos_60)
1.101 -  finally show ?thesis .
1.102 -qed
1.103 +by (simp add: sin_cos_eq cos_60)
1.104
1.105  lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
1.106  unfolding tan_def by (simp add: sin_30 cos_30)
```