--- a/src/HOL/Transcendental.thy Tue Sep 06 18:13:36 2011 +0200
+++ b/src/HOL/Transcendental.thy Tue Sep 06 10:30:33 2011 -0700
@@ -1065,22 +1065,24 @@
using exp_inj_iff [where x=x and y=0] by simp
lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
-apply (rule IVT)
-apply (auto intro: isCont_exp simp add: le_diff_eq)
-apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)")
-apply simp
-apply (rule exp_ge_add_one_self_aux, simp)
-done
+proof (rule IVT)
+ assume "1 \<le> y"
+ hence "0 \<le> y - 1" by simp
+ hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
+ thus "y \<le> exp (y - 1)" by simp
+qed (simp_all add: le_diff_eq)
lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y"
-apply (rule_tac x = 1 and y = y in linorder_cases)
-apply (drule order_less_imp_le [THEN lemma_exp_total])
-apply (rule_tac [2] x = 0 in exI)
-apply (frule_tac [3] one_less_inverse)
-apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
-apply (rule_tac x = "-x" in exI)
-apply (simp add: exp_minus)
-done
+proof (rule linorder_le_cases [of 1 y])
+ assume "1 \<le> y" thus "\<exists>x. exp x = y"
+ by (fast dest: lemma_exp_total)
+next
+ assume "0 < y" and "y \<le> 1"
+ hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
+ then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
+ hence "exp (- x) = y" by (simp add: exp_minus)
+ thus "\<exists>x. exp x = y" ..
+qed
subsection {* Natural Logarithm *}
@@ -1920,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
+ by (simp add: power2_eq_square)
lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<twosuperior>)"
unfolding tan_def
@@ -2801,7 +2791,7 @@
have "arctan x = y" using arctan_tan low high y_eq by auto
also have "\<dots> = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto
- also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half[OF low2 high2] by auto
+ also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half by auto
finally show ?thesis unfolding eq `tan y = x` .
qed