1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 11:49:53 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 14:17:28 2011 -0700
     1.3 @@ -871,8 +871,15 @@
     1.4  apply (simp del: of_real_add)
     1.5  done
     1.6  
     1.7 -lemma isCont_exp [simp]: "isCont exp x"
     1.8 -by (rule DERIV_exp [THEN DERIV_isCont])
     1.9 +lemma isCont_exp: "isCont exp x"
    1.10 +  by (rule DERIV_exp [THEN DERIV_isCont])
    1.11 +
    1.12 +lemma isCont_exp' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
    1.13 +  by (rule isCont_o2 [OF _ isCont_exp])
    1.14 +
    1.15 +lemma tendsto_exp [tendsto_intros]:
    1.16 +  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
    1.17 +  by (rule isCont_tendsto_compose [OF isCont_exp])
    1.18  
    1.19  
    1.20  subsubsection {* Properties of the Exponential Function *}
    1.21 @@ -1271,12 +1278,25 @@
    1.22  apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
    1.23  done
    1.24  
    1.25 -lemma isCont_sin [simp]: "isCont sin x"
    1.26 -by (rule DERIV_sin [THEN DERIV_isCont])
    1.27 -
    1.28 -lemma isCont_cos [simp]: "isCont cos x"
    1.29 -by (rule DERIV_cos [THEN DERIV_isCont])
    1.30 -
    1.31 +lemma isCont_sin: "isCont sin x"
    1.32 +  by (rule DERIV_sin [THEN DERIV_isCont])
    1.33 +
    1.34 +lemma isCont_cos: "isCont cos x"
    1.35 +  by (rule DERIV_cos [THEN DERIV_isCont])
    1.36 +
    1.37 +lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
    1.38 +  by (rule isCont_o2 [OF _ isCont_sin])
    1.39 +
    1.40 +lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
    1.41 +  by (rule isCont_o2 [OF _ isCont_cos])
    1.42 +
    1.43 +lemma tendsto_sin [tendsto_intros]:
    1.44 +  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) ---> sin a) F"
    1.45 +  by (rule isCont_tendsto_compose [OF isCont_sin])
    1.46 +
    1.47 +lemma tendsto_cos [tendsto_intros]:
    1.48 +  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
    1.49 +  by (rule isCont_tendsto_compose [OF isCont_cos])
    1.50  
    1.51  declare
    1.52    DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    1.53 @@ -1287,10 +1307,10 @@
    1.54  subsection {* Properties of Sine and Cosine *}
    1.55  
    1.56  lemma sin_zero [simp]: "sin 0 = 0"
    1.57 -unfolding sin_def sin_coeff_def by (simp add: powser_zero)
    1.58 +  unfolding sin_def sin_coeff_def by (simp add: powser_zero)
    1.59  
    1.60  lemma cos_zero [simp]: "cos 0 = 1"
    1.61 -unfolding cos_def cos_coeff_def by (simp add: powser_zero)
    1.62 +  unfolding cos_def cos_coeff_def by (simp add: powser_zero)
    1.63  
    1.64  lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    1.65    by (rule DERIV_cong) (* TODO: delete *)
    1.66 @@ -1336,32 +1356,19 @@
    1.67  
    1.68  lemma DERIV_fun_pow: "DERIV g x :> m ==>
    1.69        DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
    1.70 -unfolding One_nat_def
    1.71 -apply (rule DERIV_cong)
    1.72 -apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
    1.73 -apply (rule DERIV_pow, auto)
    1.74 -done
    1.75 +  by (auto intro!: DERIV_intros)
    1.76  
    1.77  lemma DERIV_fun_exp:
    1.78       "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
    1.79 -apply (rule DERIV_cong)
    1.80 -apply (rule_tac f = exp in DERIV_chain2)
    1.81 -apply (rule DERIV_exp, auto)
    1.82 -done
    1.83 +  by (auto intro!: DERIV_intros)
    1.84  
    1.85  lemma DERIV_fun_sin:
    1.86       "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
    1.87 -apply (rule DERIV_cong)
    1.88 -apply (rule_tac f = sin in DERIV_chain2)
    1.89 -apply (rule DERIV_sin, auto)
    1.90 -done
    1.91 +  by (auto intro!: DERIV_intros)
    1.92  
    1.93  lemma DERIV_fun_cos:
    1.94       "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
    1.95 -apply (rule DERIV_cong)
    1.96 -apply (rule_tac f = cos in DERIV_chain2)
    1.97 -apply (rule DERIV_cos, auto)
    1.98 -done
    1.99 +  by (auto intro!: DERIV_intros)
   1.100  
   1.101  lemma sin_cos_add_lemma:
   1.102       "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
   1.103 @@ -1485,10 +1492,10 @@
   1.104  done
   1.105  
   1.106  lemma sin_gt_zero1: "[|0 < x; x < 2 |] ==> 0 < sin x"
   1.107 -by (auto intro: sin_gt_zero)
   1.108 +  by (rule sin_gt_zero)
   1.109  
   1.110  lemma cos_double_less_one: "[| 0 < x; x < 2 |] ==> cos (2 * x) < 1"
   1.111 -apply (cut_tac x = x in sin_gt_zero1)
   1.112 +apply (cut_tac x = x in sin_gt_zero)
   1.113  apply (auto simp add: cos_squared_eq cos_double)
   1.114  done
   1.115  
   1.116 @@ -1888,59 +1895,41 @@
   1.117  
   1.118  subsection {* Tangent *}
   1.119  
   1.120 -definition
   1.121 -  tan :: "real => real" where
   1.122 -  "tan x = (sin x)/(cos x)"
   1.123 +definition tan :: "real \<Rightarrow> real" where
   1.124 +  "tan = (\<lambda>x. sin x / cos x)"
   1.125  
   1.126  lemma tan_zero [simp]: "tan 0 = 0"
   1.127 -by (simp add: tan_def)
   1.128 +  by (simp add: tan_def)
   1.129  
   1.130  lemma tan_pi [simp]: "tan pi = 0"
   1.131 -by (simp add: tan_def)
   1.132 +  by (simp add: tan_def)
   1.133  
   1.134  lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
   1.135 -by (simp add: tan_def)
   1.136 +  by (simp add: tan_def)
   1.137  
   1.138  lemma tan_minus [simp]: "tan (-x) = - tan x"
   1.139 -by (simp add: tan_def minus_mult_left)
   1.140 +  by (simp add: tan_def)
   1.141  
   1.142  lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
   1.143 -by (simp add: tan_def)
   1.144 +  by (simp add: tan_def)
   1.145  
   1.146  lemma lemma_tan_add1:
   1.147 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
   1.148 -        ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"
   1.149 -apply (simp add: tan_def divide_inverse)
   1.150 -apply (auto simp del: inverse_mult_distrib
   1.151 -            simp add: inverse_mult_distrib [symmetric] mult_ac)
   1.152 -apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
   1.153 -apply (auto simp del: inverse_mult_distrib
   1.154 -            simp add: mult_assoc left_diff_distrib cos_add)
   1.155 -done
   1.156 +  "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> 1 - tan x * tan y = cos (x + y)/(cos x * cos y)"
   1.157 +  by (simp add: tan_def cos_add field_simps)
   1.158  
   1.159  lemma add_tan_eq:
   1.160 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
   1.161 -       ==> tan x + tan y = sin(x + y)/(cos x * cos y)"
   1.162 -apply (simp add: tan_def)
   1.163 -apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
   1.164 -apply (auto simp add: mult_assoc left_distrib)
   1.165 -apply (simp add: sin_add)
   1.166 -done
   1.167 +  "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0\<rbrakk> \<Longrightarrow> tan x + tan y = sin(x + y)/(cos x * cos y)"
   1.168 +  by (simp add: tan_def sin_add field_simps)
   1.169  
   1.170  lemma tan_add:
   1.171       "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
   1.172        ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
   1.173 -apply (simp (no_asm_simp) add: add_tan_eq lemma_tan_add1)
   1.174 -apply (simp add: tan_def)
   1.175 -done
   1.176 +  by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def)
   1.177  
   1.178  lemma tan_double:
   1.179       "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
   1.180        ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))"
   1.181 -apply (insert tan_add [of x x])
   1.182 -apply (simp add: mult_2 [symmetric])
   1.183 -apply (auto simp add: numeral_2_eq_2)
   1.184 -done
   1.185 +  using tan_add [of x x] by (simp add: power2_eq_square)
   1.186  
   1.187  lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
   1.188  by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
   1.189 @@ -1968,26 +1957,23 @@
   1.190    finally show ?thesis .
   1.191  qed
   1.192  
   1.193 -lemma lemma_DERIV_tan:
   1.194 -     "cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
   1.195 -  by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
   1.196 -
   1.197 -lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
   1.198 -by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
   1.199 -
   1.200 -lemma isCont_tan [simp]: "cos x \<noteq> 0 ==> isCont tan x"
   1.201 -by (rule DERIV_tan [THEN DERIV_isCont])
   1.202 -
   1.203 -lemma LIM_cos_div_sin [simp]: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
   1.204 -apply (subgoal_tac "(\<lambda>x. cos x * inverse (sin x)) -- pi * inverse 2 --> 0*1")
   1.205 -apply (simp add: divide_inverse [symmetric])
   1.206 -apply (rule LIM_mult)
   1.207 -apply (rule_tac [2] inverse_1 [THEN subst])
   1.208 -apply (rule_tac [2] LIM_inverse)
   1.209 -apply (simp_all add: divide_inverse [symmetric])
   1.210 -apply (simp_all only: isCont_def [symmetric] cos_pi_half [symmetric] sin_pi_half [symmetric])
   1.211 -apply (blast intro!: DERIV_isCont DERIV_sin DERIV_cos)+
   1.212 -done
   1.213 +lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<twosuperior>)"
   1.214 +  unfolding tan_def
   1.215 +  by (auto intro!: DERIV_intros, simp add: divide_inverse power2_eq_square)
   1.216 +
   1.217 +lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
   1.218 +  by (rule DERIV_tan [THEN DERIV_isCont])
   1.219 +
   1.220 +lemma isCont_tan' [simp]:
   1.221 +  "\<lbrakk>isCont f a; cos (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. tan (f x)) a"
   1.222 +  by (rule isCont_o2 [OF _ isCont_tan])
   1.223 +
   1.224 +lemma tendsto_tan [tendsto_intros]:
   1.225 +  "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
   1.226 +  by (rule isCont_tendsto_compose [OF isCont_tan])
   1.227 +
   1.228 +lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
   1.229 +  by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
   1.230  
   1.231  lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
   1.232  apply (cut_tac LIM_cos_div_sin)