src/HOL/Transcendental.thy
changeset 44756 efcd71fbaeec
parent 44755 257ac9da021f
child 45308 2e84e5f0463b
     1.1 --- a/src/HOL/Transcendental.thy	Tue Sep 06 09:56:09 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Sep 06 10:30:00 2011 -0700
     1.3 @@ -1922,21 +1922,9 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma tan_half: fixes x :: real assumes "- (pi / 2) < x" and "x < pi / 2"
     1.8 -  shows "tan x = sin (2 * x) / (cos (2 * x) + 1)"
     1.9 -proof -
    1.10 -  from cos_gt_zero_pi[OF `- (pi / 2) < x` `x < pi / 2`]
    1.11 -  have "cos x \<noteq> 0" by auto
    1.12 -
    1.13 -  have minus_cos_2x: "\<And>X. X - cos (2*x) = X - (cos x) ^ 2 + (sin x) ^ 2" unfolding cos_double by algebra
    1.14 -
    1.15 -  have "tan x = (tan x + tan x) / 2" by auto
    1.16 -  also have "\<dots> = sin (x + x) / (cos x * cos x) / 2" unfolding add_tan_eq[OF `cos x \<noteq> 0` `cos x \<noteq> 0`] ..
    1.17 -  also have "\<dots> = sin (2 * x) / ((cos x) ^ 2 + (cos x) ^ 2 + cos (2*x) - cos (2*x))" unfolding divide_divide_eq_left numeral_2_eq_2 by auto
    1.18 -  also have "\<dots> = sin (2 * x) / ((cos x) ^ 2 + cos (2*x) + (sin x)^2)" unfolding minus_cos_2x by auto
    1.19 -  also have "\<dots> = sin (2 * x) / (cos (2*x) + 1)" by auto
    1.20 -  finally show ?thesis .
    1.21 -qed
    1.22 +lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
    1.23 +  unfolding tan_def sin_double cos_double sin_squared_eq
    1.24 +  by (simp add: power2_eq_square)
    1.25  
    1.26  lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<twosuperior>)"
    1.27    unfolding tan_def
    1.28 @@ -2803,7 +2791,7 @@
    1.29  
    1.30    have "arctan x = y" using arctan_tan low high y_eq by auto
    1.31    also have "\<dots> = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto
    1.32 -  also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half[OF low2 high2] by auto
    1.33 +  also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half by auto
    1.34    finally show ?thesis unfolding eq `tan y = x` .
    1.35  qed
    1.36