author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 44310 ba3d031b5dbb child 44312 471ff02a8574
new isCont theorems;
simplify some proofs.
```     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.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.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.128 +  by (simp add: tan_def)
1.129
1.130  lemma tan_pi [simp]: "tan pi = 0"
1.132 +  by (simp add: tan_def)
1.133
1.134  lemma tan_npi [simp]: "tan (real (n::nat) * pi) = 0"
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.144 +  by (simp add: tan_def)
1.145
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.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.158
1.160 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
1.161 -       ==> tan x + tan y = sin(x + y)/(cos x * cos y)"
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.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.169
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.175 -done
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.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)
```