src/HOL/Transcendental.thy
changeset 45309 5885ec8eb6b0
parent 45308 2e84e5f0463b
child 45915 0e5a87b772f9
     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.7 -by (simp add: diff_minus cos_add)
     1.8 -declare sin_cos_eq [symmetric, simp]
     1.9 +by (simp add: cos_diff)
    1.10  
    1.11  lemma minus_sin_cos_eq: "-sin x = cos (x + pi/2)"
    1.12  by (simp add: cos_add)
    1.13 -declare minus_sin_cos_eq [symmetric, simp]
    1.14  
    1.15  lemma cos_sin_eq: "cos x = sin (pi/2 - x)"
    1.16 -by (simp add: diff_minus sin_add)
    1.17 -declare cos_sin_eq [symmetric, simp]
    1.18 +by (simp add: sin_diff)
    1.19  
    1.20  lemma sin_periodic_pi [simp]: "sin (x + pi) = - sin x"
    1.21  by (simp add: sin_add)
    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.45  apply (simp (no_asm) add: add_assoc)
    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.56 -apply (simp_all add: add_increasing)
    1.57 +apply (simp_all add: cos_add)
    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)