src/HOL/Transcendental.thy
changeset 36974 b877866b5b00
parent 36970 fb3fdb4b585e
child 37887 2ae085b07f2f
     1.1 --- a/src/HOL/Transcendental.thy	Mon May 17 12:00:10 2010 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon May 17 15:58:32 2010 -0700
     1.3 @@ -2580,18 +2580,6 @@
     1.4  lemma tan_60: "tan (pi / 3) = sqrt 3"
     1.5  unfolding tan_def by (simp add: sin_60 cos_60)
     1.6  
     1.7 -text{*NEEDED??*}
     1.8 -lemma [simp]:
     1.9 -     "sin (x + 1 / 2 * real (Suc m) * pi) =  
    1.10 -      cos (x + 1 / 2 * real  (m) * pi)"
    1.11 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
    1.12 -
    1.13 -text{*NEEDED??*}
    1.14 -lemma [simp]:
    1.15 -     "sin (x + real (Suc m) * pi / 2) =  
    1.16 -      cos (x + real (m) * pi / 2)"
    1.17 -by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
    1.18 -
    1.19  lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
    1.20    by (auto intro!: DERIV_intros)
    1.21  
    1.22 @@ -2620,16 +2608,6 @@
    1.23  apply (subst sin_add, simp)
    1.24  done
    1.25  
    1.26 -(*NEEDED??*)
    1.27 -lemma [simp]:
    1.28 -     "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
    1.29 -apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
    1.30 -done
    1.31 -
    1.32 -(*NEEDED??*)
    1.33 -lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
    1.34 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
    1.35 -
    1.36  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
    1.37  by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
    1.38