src/HOL/Transcendental.thy
changeset 44318 425c1f8f9487
parent 44317 b7e9fa025f15
child 44319 806e0390de53
equal deleted inserted replaced
44317:b7e9fa025f15 44318:425c1f8f9487
  2399 unfolding tan_def by (simp add: sin_45 cos_45)
  2399 unfolding tan_def by (simp add: sin_45 cos_45)
  2400 
  2400 
  2401 lemma tan_60: "tan (pi / 3) = sqrt 3"
  2401 lemma tan_60: "tan (pi / 3) = sqrt 3"
  2402 unfolding tan_def by (simp add: sin_60 cos_60)
  2402 unfolding tan_def by (simp add: sin_60 cos_60)
  2403 
  2403 
  2404 lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
       
  2405   by (auto intro!: DERIV_intros) (* TODO: delete *)
       
  2406 
       
  2407 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  2404 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
  2408 proof -
  2405 proof -
  2409   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  2406   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
  2410     by (auto simp add: algebra_simps sin_add)
  2407     by (auto simp add: algebra_simps sin_add)
  2411   thus ?thesis
  2408   thus ?thesis