src/HOL/Transcendental.thy
changeset 51478 270b21f3ae0a
parent 51477 2990382dc066
child 51481 ef949192e5d6
--- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -881,6 +881,12 @@
   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
   by (rule isCont_tendsto_compose [OF isCont_exp])
 
+lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
+  unfolding continuous_def by (rule tendsto_exp)
+
+lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_exp)
+
 subsubsection {* Properties of the Exponential Function *}
 
 lemma powser_zero:
@@ -1169,6 +1175,22 @@
   "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   by (rule isCont_tendsto_compose [OF isCont_ln])
 
+lemma continuous_ln:
+  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
+  unfolding continuous_def by (rule tendsto_ln)
+
+lemma isCont_ln' [continuous_intros]:
+  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
+  unfolding continuous_at by (rule tendsto_ln)
+
+lemma continuous_within_ln [continuous_intros]:
+  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
+  unfolding continuous_within by (rule tendsto_ln)
+
+lemma continuous_on_ln [continuous_on_intros]:
+  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_ln)
+
 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
   apply (erule DERIV_cong [OF DERIV_exp exp_ln])
@@ -1449,6 +1471,22 @@
   "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
   by (rule isCont_tendsto_compose [OF isCont_cos])
 
+lemma continuous_sin [continuous_intros]:
+  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
+  unfolding continuous_def by (rule tendsto_sin)
+
+lemma continuous_on_sin [continuous_on_intros]:
+  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_sin)
+
+lemma continuous_cos [continuous_intros]:
+  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
+  unfolding continuous_def by (rule tendsto_cos)
+
+lemma continuous_on_cos [continuous_on_intros]:
+  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_cos)
+
 declare
   DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
@@ -2076,6 +2114,22 @@
   "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
   by (rule isCont_tendsto_compose [OF isCont_tan])
 
+lemma continuous_tan:
+  "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
+  unfolding continuous_def by (rule tendsto_tan)
+
+lemma isCont_tan'' [continuous_intros]:
+  "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
+  unfolding continuous_at by (rule tendsto_tan)
+
+lemma continuous_within_tan [continuous_intros]:
+  "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
+  unfolding continuous_within by (rule tendsto_tan)
+
+lemma continuous_on_tan [continuous_on_intros]:
+  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_tan)
+
 lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
 
@@ -2403,7 +2457,7 @@
 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
   using arctan_eq_iff [of x 0] by simp
 
-lemma isCont_inverse_function2:
+lemma isCont_inverse_function2: (* generalize with continuous_on *)
   fixes f g :: "real \<Rightarrow> real" shows
   "\<lbrakk>a < x; x < b;
     \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
@@ -2414,7 +2468,7 @@
 apply (simp_all add: abs_le_iff)
 done
 
-lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x"
+lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
 apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
 apply (rule isCont_inverse_function2 [where f=sin])
 apply (erule (1) arcsin_lt_bounded [THEN conjunct1])
@@ -2422,7 +2476,7 @@
 apply (fast intro: arcsin_sin, simp)
 done
 
-lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x"
+lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x" (* generalize with continuous_on {-1 .. 1} *)
 apply (subgoal_tac "isCont arccos (cos (arccos x))", simp)
 apply (rule isCont_inverse_function2 [where f=cos])
 apply (erule (1) arccos_lt_bounded [THEN conjunct1])
@@ -2439,6 +2493,15 @@
 apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
 done
 
+lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
+  by (rule isCont_tendsto_compose [OF isCont_arctan])
+
+lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
+  unfolding continuous_def by (rule tendsto_arctan)
+
+lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_arctan)
+  
 lemma DERIV_arcsin:
   "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
 apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])