src/HOL/Transcendental.thy
 changeset 51478 270b21f3ae0a parent 51477 2990382dc066 child 51481 ef949192e5d6
```     1.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -881,6 +881,12 @@
1.4    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
1.5    by (rule isCont_tendsto_compose [OF isCont_exp])
1.6
1.7 +lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
1.8 +  unfolding continuous_def by (rule tendsto_exp)
1.9 +
1.10 +lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
1.11 +  unfolding continuous_on_def by (auto intro: tendsto_exp)
1.12 +
1.13  subsubsection {* Properties of the Exponential Function *}
1.14
1.15  lemma powser_zero:
1.16 @@ -1169,6 +1175,22 @@
1.17    "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
1.18    by (rule isCont_tendsto_compose [OF isCont_ln])
1.19
1.20 +lemma continuous_ln:
1.21 +  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
1.22 +  unfolding continuous_def by (rule tendsto_ln)
1.23 +
1.24 +lemma isCont_ln' [continuous_intros]:
1.25 +  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
1.26 +  unfolding continuous_at by (rule tendsto_ln)
1.27 +
1.28 +lemma continuous_within_ln [continuous_intros]:
1.29 +  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
1.30 +  unfolding continuous_within by (rule tendsto_ln)
1.31 +
1.32 +lemma continuous_on_ln [continuous_on_intros]:
1.33 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
1.34 +  unfolding continuous_on_def by (auto intro: tendsto_ln)
1.35 +
1.36  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
1.37    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
1.38    apply (erule DERIV_cong [OF DERIV_exp exp_ln])
1.39 @@ -1449,6 +1471,22 @@
1.40    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
1.41    by (rule isCont_tendsto_compose [OF isCont_cos])
1.42
1.43 +lemma continuous_sin [continuous_intros]:
1.44 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
1.45 +  unfolding continuous_def by (rule tendsto_sin)
1.46 +
1.47 +lemma continuous_on_sin [continuous_on_intros]:
1.48 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
1.49 +  unfolding continuous_on_def by (auto intro: tendsto_sin)
1.50 +
1.51 +lemma continuous_cos [continuous_intros]:
1.52 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
1.53 +  unfolding continuous_def by (rule tendsto_cos)
1.54 +
1.55 +lemma continuous_on_cos [continuous_on_intros]:
1.56 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
1.57 +  unfolding continuous_on_def by (auto intro: tendsto_cos)
1.58 +
1.59  declare
1.60    DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.61    DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.62 @@ -2076,6 +2114,22 @@
1.63    "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
1.64    by (rule isCont_tendsto_compose [OF isCont_tan])
1.65
1.66 +lemma continuous_tan:
1.67 +  "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
1.68 +  unfolding continuous_def by (rule tendsto_tan)
1.69 +
1.70 +lemma isCont_tan'' [continuous_intros]:
1.71 +  "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
1.72 +  unfolding continuous_at by (rule tendsto_tan)
1.73 +
1.74 +lemma continuous_within_tan [continuous_intros]:
1.75 +  "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
1.76 +  unfolding continuous_within by (rule tendsto_tan)
1.77 +
1.78 +lemma continuous_on_tan [continuous_on_intros]:
1.79 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
1.80 +  unfolding continuous_on_def by (auto intro: tendsto_tan)
1.81 +
1.82  lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
1.83    by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
1.84
1.85 @@ -2403,7 +2457,7 @@
1.86  lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
1.87    using arctan_eq_iff [of x 0] by simp
1.88
1.89 -lemma isCont_inverse_function2:
1.90 +lemma isCont_inverse_function2: (* generalize with continuous_on *)
1.91    fixes f g :: "real \<Rightarrow> real" shows
1.92    "\<lbrakk>a < x; x < b;
1.93      \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
1.94 @@ -2414,7 +2468,7 @@
1.96  done
1.97
1.98 -lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x"
1.99 +lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
1.100  apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
1.101  apply (rule isCont_inverse_function2 [where f=sin])
1.102  apply (erule (1) arcsin_lt_bounded [THEN conjunct1])
1.103 @@ -2422,7 +2476,7 @@
1.104  apply (fast intro: arcsin_sin, simp)
1.105  done
1.106
1.107 -lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x"
1.108 +lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x" (* generalize with continuous_on {-1 .. 1} *)
1.109  apply (subgoal_tac "isCont arccos (cos (arccos x))", simp)
1.110  apply (rule isCont_inverse_function2 [where f=cos])
1.111  apply (erule (1) arccos_lt_bounded [THEN conjunct1])
1.112 @@ -2439,6 +2493,15 @@
1.113  apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
1.114  done
1.115
1.116 +lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
1.117 +  by (rule isCont_tendsto_compose [OF isCont_arctan])
1.118 +
1.119 +lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
1.120 +  unfolding continuous_def by (rule tendsto_arctan)
1.121 +
1.122 +lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
1.123 +  unfolding continuous_on_def by (auto intro: tendsto_arctan)
1.124 +
1.125  lemma DERIV_arcsin:
1.126    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
1.127  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
```