author huffman Tue, 06 Sep 2011 10:30:00 -0700 changeset 44756 efcd71fbaeec parent 44755 257ac9da021f child 44757 8aae88168599
simplify proof of tan_half, removing unused assumptions
```--- a/src/HOL/Transcendental.thy	Tue Sep 06 09:56:09 2011 -0700
+++ b/src/HOL/Transcendental.thy	Tue Sep 06 10:30:00 2011 -0700
@@ -1922,21 +1922,9 @@
thus ?thesis by simp
qed

-lemma tan_half: fixes x :: real assumes "- (pi / 2) < x" and "x < pi / 2"
-  shows "tan x = sin (2 * x) / (cos (2 * x) + 1)"
-proof -
-  from cos_gt_zero_pi[OF `- (pi / 2) < x` `x < pi / 2`]
-  have "cos x \<noteq> 0" by auto
-
-  have minus_cos_2x: "\<And>X. X - cos (2*x) = X - (cos x) ^ 2 + (sin x) ^ 2" unfolding cos_double by algebra
-
-  have "tan x = (tan x + tan x) / 2" by auto
-  also have "\<dots> = sin (x + x) / (cos x * cos x) / 2" unfolding add_tan_eq[OF `cos x \<noteq> 0` `cos x \<noteq> 0`] ..
-  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
-  also have "\<dots> = sin (2 * x) / ((cos x) ^ 2 + cos (2*x) + (sin x)^2)" unfolding minus_cos_2x by auto
-  also have "\<dots> = sin (2 * x) / (cos (2*x) + 1)" by auto
-  finally show ?thesis .
-qed
+lemma tan_half: "tan x = sin (2 * x) / (cos (2 * x) + 1)"
+  unfolding tan_def sin_double cos_double sin_squared_eq