move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51478270b21f3ae0a
parent 51477 2990382dc066
child 51479 33db4b7189af
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
src/HOL/Library/Product_Vector.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/Log.thy
src/HOL/Metric_Spaces.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NthRoot.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -117,15 +117,6 @@
     1.4      by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
     1.5  qed
     1.6  
     1.7 -lemma openI: (* TODO: move *)
     1.8 -  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
     1.9 -  shows "open S"
    1.10 -proof -
    1.11 -  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
    1.12 -  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
    1.13 -  ultimately show "open S" by simp
    1.14 -qed
    1.15 -
    1.16  lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
    1.17    unfolding image_def subset_eq by force
    1.18  
    1.19 @@ -202,15 +193,23 @@
    1.20         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
    1.21  qed
    1.22  
    1.23 +lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
    1.24 +  unfolding continuous_def by (rule tendsto_fst)
    1.25 +
    1.26 +lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
    1.27 +  unfolding continuous_def by (rule tendsto_snd)
    1.28 +
    1.29 +lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
    1.30 +  unfolding continuous_def by (rule tendsto_Pair)
    1.31 +
    1.32  lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
    1.33 -  unfolding isCont_def by (rule tendsto_fst)
    1.34 +  by (fact continuous_fst)
    1.35  
    1.36  lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
    1.37 -  unfolding isCont_def by (rule tendsto_snd)
    1.38 +  by (fact continuous_snd)
    1.39  
    1.40 -lemma isCont_Pair [simp]:
    1.41 -  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
    1.42 -  unfolding isCont_def by (rule tendsto_Pair)
    1.43 +lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
    1.44 +  by (fact continuous_Pair)
    1.45  
    1.46  subsubsection {* Separation axioms *}
    1.47  
     2.1 --- a/src/HOL/Lim.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/Lim.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -118,46 +118,6 @@
     2.4    shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
     2.5  by (simp add: isCont_def LIM_isCont_iff)
     2.6  
     2.7 -lemma isCont_norm [simp]:
     2.8 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
     2.9 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
    2.10 -  unfolding isCont_def by (rule tendsto_norm)
    2.11 -
    2.12 -lemma isCont_rabs [simp]:
    2.13 -  fixes f :: "'a::topological_space \<Rightarrow> real"
    2.14 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
    2.15 -  unfolding isCont_def by (rule tendsto_rabs)
    2.16 -
    2.17 -lemma isCont_add [simp]:
    2.18 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    2.19 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
    2.20 -  unfolding isCont_def by (rule tendsto_add)
    2.21 -
    2.22 -lemma isCont_minus [simp]:
    2.23 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    2.24 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
    2.25 -  unfolding isCont_def by (rule tendsto_minus)
    2.26 -
    2.27 -lemma isCont_diff [simp]:
    2.28 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    2.29 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
    2.30 -  unfolding isCont_def by (rule tendsto_diff)
    2.31 -
    2.32 -lemma isCont_mult [simp]:
    2.33 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
    2.34 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
    2.35 -  unfolding isCont_def by (rule tendsto_mult)
    2.36 -
    2.37 -lemma isCont_inverse [simp]:
    2.38 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
    2.39 -  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
    2.40 -  unfolding isCont_def by (rule tendsto_inverse)
    2.41 -
    2.42 -lemma isCont_divide [simp]:
    2.43 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
    2.44 -  shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
    2.45 -  unfolding isCont_def by (rule tendsto_divide)
    2.46 -
    2.47  lemma isCont_LIM_compose2:
    2.48    fixes a :: "'a::real_normed_vector"
    2.49    assumes f [unfolded isCont_def]: "isCont f a"
    2.50 @@ -166,35 +126,60 @@
    2.51    shows "(\<lambda>x. g (f x)) -- a --> l"
    2.52  by (rule LIM_compose2 [OF f g inj])
    2.53  
    2.54 +
    2.55 +lemma isCont_norm [simp]:
    2.56 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    2.57 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
    2.58 +  by (fact continuous_norm)
    2.59 +
    2.60 +lemma isCont_rabs [simp]:
    2.61 +  fixes f :: "'a::t2_space \<Rightarrow> real"
    2.62 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
    2.63 +  by (fact continuous_rabs)
    2.64 +
    2.65 +lemma isCont_add [simp]:
    2.66 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    2.67 +  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
    2.68 +  by (fact continuous_add)
    2.69 +
    2.70 +lemma isCont_minus [simp]:
    2.71 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    2.72 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
    2.73 +  by (fact continuous_minus)
    2.74 +
    2.75 +lemma isCont_diff [simp]:
    2.76 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    2.77 +  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
    2.78 +  by (fact continuous_diff)
    2.79 +
    2.80 +lemma isCont_mult [simp]:
    2.81 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
    2.82 +  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
    2.83 +  by (fact continuous_mult)
    2.84 +
    2.85  lemma (in bounded_linear) isCont:
    2.86    "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
    2.87 -  unfolding isCont_def by (rule tendsto)
    2.88 +  by (fact continuous)
    2.89  
    2.90  lemma (in bounded_bilinear) isCont:
    2.91    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
    2.92 -  unfolding isCont_def by (rule tendsto)
    2.93 +  by (fact continuous)
    2.94  
    2.95 -lemmas isCont_scaleR [simp] =
    2.96 +lemmas isCont_scaleR [simp] = 
    2.97    bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
    2.98  
    2.99  lemmas isCont_of_real [simp] =
   2.100    bounded_linear.isCont [OF bounded_linear_of_real]
   2.101  
   2.102  lemma isCont_power [simp]:
   2.103 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   2.104 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   2.105    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   2.106 -  unfolding isCont_def by (rule tendsto_power)
   2.107 -
   2.108 -lemma isCont_sgn [simp]:
   2.109 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   2.110 -  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   2.111 -  unfolding isCont_def by (rule tendsto_sgn)
   2.112 +  by (fact continuous_power)
   2.113  
   2.114  lemma isCont_setsum [simp]:
   2.115 -  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   2.116 -  fixes A :: "'a set"
   2.117 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
   2.118    shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   2.119 -  unfolding isCont_def by (simp add: tendsto_setsum)
   2.120 +  by (auto intro: continuous_setsum)
   2.121  
   2.122  lemmas isCont_intros =
   2.123    isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
     3.1 --- a/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     3.2 +++ b/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -236,6 +236,14 @@
     3.4    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
     3.5    unfolding norm_conv_dist by (intro tendsto_intros)
     3.6  
     3.7 +lemma continuous_norm [continuous_intros]:
     3.8 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
     3.9 +  unfolding continuous_def by (rule tendsto_norm)
    3.10 +
    3.11 +lemma continuous_on_norm [continuous_on_intros]:
    3.12 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
    3.13 +  unfolding continuous_on_def by (auto intro: tendsto_norm)
    3.14 +
    3.15  lemma tendsto_norm_zero:
    3.16    "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) F"
    3.17    by (drule tendsto_norm, simp)
    3.18 @@ -252,6 +260,14 @@
    3.19    "(f ---> (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) F"
    3.20    by (fold real_norm_def, rule tendsto_norm)
    3.21  
    3.22 +lemma continuous_rabs [continuous_intros]:
    3.23 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)"
    3.24 +  unfolding real_norm_def[symmetric] by (rule continuous_norm)
    3.25 +
    3.26 +lemma continuous_on_rabs [continuous_on_intros]:
    3.27 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)"
    3.28 +  unfolding real_norm_def[symmetric] by (rule continuous_on_norm)
    3.29 +
    3.30  lemma tendsto_rabs_zero:
    3.31    "(f ---> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) F"
    3.32    by (fold real_norm_def, rule tendsto_norm_zero)
    3.33 @@ -271,8 +287,18 @@
    3.34    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) F"
    3.35    by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
    3.36  
    3.37 +lemma continuous_add [continuous_intros]:
    3.38 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    3.39 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
    3.40 +  unfolding continuous_def by (rule tendsto_add)
    3.41 +
    3.42 +lemma continuous_on_add [continuous_on_intros]:
    3.43 +  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    3.44 +  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
    3.45 +  unfolding continuous_on_def by (auto intro: tendsto_add)
    3.46 +
    3.47  lemma tendsto_add_zero:
    3.48 -  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
    3.49 +  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
    3.50    shows "\<lbrakk>(f ---> 0) F; (g ---> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) F"
    3.51    by (drule (1) tendsto_add, simp)
    3.52  
    3.53 @@ -281,6 +307,16 @@
    3.54    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) F"
    3.55    by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
    3.56  
    3.57 +lemma continuous_minus [continuous_intros]:
    3.58 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    3.59 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
    3.60 +  unfolding continuous_def by (rule tendsto_minus)
    3.61 +
    3.62 +lemma continuous_on_minus [continuous_on_intros]:
    3.63 +  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
    3.64 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
    3.65 +  unfolding continuous_on_def by (auto intro: tendsto_minus)
    3.66 +
    3.67  lemma tendsto_minus_cancel:
    3.68    fixes a :: "'a::real_normed_vector"
    3.69    shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
    3.70 @@ -296,6 +332,16 @@
    3.71    shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
    3.72    by (simp add: diff_minus tendsto_add tendsto_minus)
    3.73  
    3.74 +lemma continuous_diff [continuous_intros]:
    3.75 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    3.76 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
    3.77 +  unfolding continuous_def by (rule tendsto_diff)
    3.78 +
    3.79 +lemma continuous_on_diff [continuous_on_intros]:
    3.80 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    3.81 +  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
    3.82 +  unfolding continuous_on_def by (auto intro: tendsto_diff)
    3.83 +
    3.84  lemma tendsto_setsum [tendsto_intros]:
    3.85    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
    3.86    assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) F"
    3.87 @@ -308,6 +354,16 @@
    3.88      by (simp add: tendsto_const)
    3.89  qed
    3.90  
    3.91 +lemma continuous_setsum [continuous_intros]:
    3.92 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
    3.93 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
    3.94 +  unfolding continuous_def by (rule tendsto_setsum)
    3.95 +
    3.96 +lemma continuous_on_setsum [continuous_intros]:
    3.97 +  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
    3.98 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
    3.99 +  unfolding continuous_on_def by (auto intro: tendsto_setsum)
   3.100 +
   3.101  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
   3.102  
   3.103  subsubsection {* Linear operators and multiplication *}
   3.104 @@ -316,6 +372,14 @@
   3.105    "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
   3.106    by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
   3.107  
   3.108 +lemma (in bounded_linear) continuous:
   3.109 +  "continuous F g \<Longrightarrow> continuous F (\<lambda>x. f (g x))"
   3.110 +  using tendsto[of g _ F] by (auto simp: continuous_def)
   3.111 +
   3.112 +lemma (in bounded_linear) continuous_on:
   3.113 +  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
   3.114 +  using tendsto[of g] by (auto simp: continuous_on_def)
   3.115 +
   3.116  lemma (in bounded_linear) tendsto_zero:
   3.117    "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
   3.118    by (drule tendsto, simp only: zero)
   3.119 @@ -325,6 +389,14 @@
   3.120    by (simp only: tendsto_Zfun_iff prod_diff_prod
   3.121                   Zfun_add Zfun Zfun_left Zfun_right)
   3.122  
   3.123 +lemma (in bounded_bilinear) continuous:
   3.124 +  "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ** g x)"
   3.125 +  using tendsto[of f _ F g] by (auto simp: continuous_def)
   3.126 +
   3.127 +lemma (in bounded_bilinear) continuous_on:
   3.128 +  "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
   3.129 +  using tendsto[of f _ _ g] by (auto simp: continuous_on_def)
   3.130 +
   3.131  lemma (in bounded_bilinear) tendsto_zero:
   3.132    assumes f: "(f ---> 0) F"
   3.133    assumes g: "(g ---> 0) F"
   3.134 @@ -348,6 +420,24 @@
   3.135  lemmas tendsto_mult [tendsto_intros] =
   3.136    bounded_bilinear.tendsto [OF bounded_bilinear_mult]
   3.137  
   3.138 +lemmas continuous_of_real [continuous_intros] =
   3.139 +  bounded_linear.continuous [OF bounded_linear_of_real]
   3.140 +
   3.141 +lemmas continuous_scaleR [continuous_intros] =
   3.142 +  bounded_bilinear.continuous [OF bounded_bilinear_scaleR]
   3.143 +
   3.144 +lemmas continuous_mult [continuous_intros] =
   3.145 +  bounded_bilinear.continuous [OF bounded_bilinear_mult]
   3.146 +
   3.147 +lemmas continuous_on_of_real [continuous_on_intros] =
   3.148 +  bounded_linear.continuous_on [OF bounded_linear_of_real]
   3.149 +
   3.150 +lemmas continuous_on_scaleR [continuous_on_intros] =
   3.151 +  bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]
   3.152 +
   3.153 +lemmas continuous_on_mult [continuous_on_intros] =
   3.154 +  bounded_bilinear.continuous_on [OF bounded_bilinear_mult]
   3.155 +
   3.156  lemmas tendsto_mult_zero =
   3.157    bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]
   3.158  
   3.159 @@ -362,6 +452,16 @@
   3.160    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
   3.161    by (induct n) (simp_all add: tendsto_const tendsto_mult)
   3.162  
   3.163 +lemma continuous_power [continuous_intros]:
   3.164 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   3.165 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
   3.166 +  unfolding continuous_def by (rule tendsto_power)
   3.167 +
   3.168 +lemma continuous_on_power [continuous_on_intros]:
   3.169 +  fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
   3.170 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
   3.171 +  unfolding continuous_on_def by (auto intro: tendsto_power)
   3.172 +
   3.173  lemma tendsto_setprod [tendsto_intros]:
   3.174    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   3.175    assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) F"
   3.176 @@ -374,6 +474,16 @@
   3.177      by (simp add: tendsto_const)
   3.178  qed
   3.179  
   3.180 +lemma continuous_setprod [continuous_intros]:
   3.181 +  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   3.182 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
   3.183 +  unfolding continuous_def by (rule tendsto_setprod)
   3.184 +
   3.185 +lemma continuous_on_setprod [continuous_intros]:
   3.186 +  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   3.187 +  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
   3.188 +  unfolding continuous_on_def by (auto intro: tendsto_setprod)
   3.189 +
   3.190  subsubsection {* Inverse and division *}
   3.191  
   3.192  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   3.193 @@ -483,17 +593,89 @@
   3.194      unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
   3.195  qed
   3.196  
   3.197 +lemma continuous_inverse:
   3.198 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   3.199 +  assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
   3.200 +  shows "continuous F (\<lambda>x. inverse (f x))"
   3.201 +  using assms unfolding continuous_def by (rule tendsto_inverse)
   3.202 +
   3.203 +lemma continuous_at_within_inverse[continuous_intros]:
   3.204 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   3.205 +  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
   3.206 +  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
   3.207 +  using assms unfolding continuous_within by (rule tendsto_inverse)
   3.208 +
   3.209 +lemma isCont_inverse[continuous_intros, simp]:
   3.210 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   3.211 +  assumes "isCont f a" and "f a \<noteq> 0"
   3.212 +  shows "isCont (\<lambda>x. inverse (f x)) a"
   3.213 +  using assms unfolding continuous_at by (rule tendsto_inverse)
   3.214 +
   3.215 +lemma continuous_on_inverse[continuous_on_intros]:
   3.216 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   3.217 +  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   3.218 +  shows "continuous_on s (\<lambda>x. inverse (f x))"
   3.219 +  using assms unfolding continuous_on_def by (fast intro: tendsto_inverse)
   3.220 +
   3.221  lemma tendsto_divide [tendsto_intros]:
   3.222    fixes a b :: "'a::real_normed_field"
   3.223    shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
   3.224      \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
   3.225    by (simp add: tendsto_mult tendsto_inverse divide_inverse)
   3.226  
   3.227 +lemma continuous_divide:
   3.228 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
   3.229 +  assumes "continuous F f" and "continuous F g" and "g (Lim F (\<lambda>x. x)) \<noteq> 0"
   3.230 +  shows "continuous F (\<lambda>x. (f x) / (g x))"
   3.231 +  using assms unfolding continuous_def by (rule tendsto_divide)
   3.232 +
   3.233 +lemma continuous_at_within_divide[continuous_intros]:
   3.234 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
   3.235 +  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \<noteq> 0"
   3.236 +  shows "continuous (at a within s) (\<lambda>x. (f x) / (g x))"
   3.237 +  using assms unfolding continuous_within by (rule tendsto_divide)
   3.238 +
   3.239 +lemma isCont_divide[continuous_intros, simp]:
   3.240 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
   3.241 +  assumes "isCont f a" "isCont g a" "g a \<noteq> 0"
   3.242 +  shows "isCont (\<lambda>x. (f x) / g x) a"
   3.243 +  using assms unfolding continuous_at by (rule tendsto_divide)
   3.244 +
   3.245 +lemma continuous_on_divide[continuous_on_intros]:
   3.246 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
   3.247 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
   3.248 +  shows "continuous_on s (\<lambda>x. (f x) / (g x))"
   3.249 +  using assms unfolding continuous_on_def by (fast intro: tendsto_divide)
   3.250 +
   3.251  lemma tendsto_sgn [tendsto_intros]:
   3.252    fixes l :: "'a::real_normed_vector"
   3.253    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
   3.254    unfolding sgn_div_norm by (simp add: tendsto_intros)
   3.255  
   3.256 +lemma continuous_sgn:
   3.257 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.258 +  assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
   3.259 +  shows "continuous F (\<lambda>x. sgn (f x))"
   3.260 +  using assms unfolding continuous_def by (rule tendsto_sgn)
   3.261 +
   3.262 +lemma continuous_at_within_sgn[continuous_intros]:
   3.263 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.264 +  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
   3.265 +  shows "continuous (at a within s) (\<lambda>x. sgn (f x))"
   3.266 +  using assms unfolding continuous_within by (rule tendsto_sgn)
   3.267 +
   3.268 +lemma isCont_sgn[continuous_intros]:
   3.269 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   3.270 +  assumes "isCont f a" and "f a \<noteq> 0"
   3.271 +  shows "isCont (\<lambda>x. sgn (f x)) a"
   3.272 +  using assms unfolding continuous_at by (rule tendsto_sgn)
   3.273 +
   3.274 +lemma continuous_on_sgn[continuous_on_intros]:
   3.275 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   3.276 +  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   3.277 +  shows "continuous_on s (\<lambda>x. sgn (f x))"
   3.278 +  using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
   3.279 +
   3.280  lemma filterlim_at_infinity:
   3.281    fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
   3.282    assumes "0 \<le> c"
     4.1 --- a/src/HOL/Log.thy	Fri Mar 22 10:41:43 2013 +0100
     4.2 +++ b/src/HOL/Log.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -21,6 +21,29 @@
     4.4    "log a x = ln x / ln a"
     4.5  
     4.6  
     4.7 +lemma tendsto_log [tendsto_intros]:
     4.8 +  "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a; a \<noteq> 1; 0 < b\<rbrakk> \<Longrightarrow> ((\<lambda>x. log (f x) (g x)) ---> log a b) F"
     4.9 +  unfolding log_def by (intro tendsto_intros) auto
    4.10 +
    4.11 +lemma continuous_log:
    4.12 +  assumes "continuous F f" and "continuous F g" and "0 < f (Lim F (\<lambda>x. x))" and "f (Lim F (\<lambda>x. x)) \<noteq> 1" and "0 < g (Lim F (\<lambda>x. x))"
    4.13 +  shows "continuous F (\<lambda>x. log (f x) (g x))"
    4.14 +  using assms unfolding continuous_def by (rule tendsto_log)
    4.15 +
    4.16 +lemma continuous_at_within_log[continuous_intros]:
    4.17 +  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "0 < f a" and "f a \<noteq> 1" and "0 < g a"
    4.18 +  shows "continuous (at a within s) (\<lambda>x. log (f x) (g x))"
    4.19 +  using assms unfolding continuous_within by (rule tendsto_log)
    4.20 +
    4.21 +lemma isCont_log[continuous_intros, simp]:
    4.22 +  assumes "isCont f a" "isCont g a" "0 < f a" "f a \<noteq> 1" "0 < g a"
    4.23 +  shows "isCont (\<lambda>x. log (f x) (g x)) a"
    4.24 +  using assms unfolding continuous_at by (rule tendsto_log)
    4.25 +
    4.26 +lemma continuous_on_log[continuous_on_intros]:
    4.27 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x" "\<forall>x\<in>s. f x \<noteq> 1" "\<forall>x\<in>s. 0 < g x"
    4.28 +  shows "continuous_on s (\<lambda>x. log (f x) (g x))"
    4.29 +  using assms unfolding continuous_on_def by (fast intro: tendsto_log)
    4.30  
    4.31  lemma powr_one_eq_one [simp]: "1 powr a = 1"
    4.32  by (simp add: powr_def)
    4.33 @@ -338,6 +361,26 @@
    4.34    "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
    4.35    unfolding powr_def by (intro tendsto_intros)
    4.36  
    4.37 +lemma continuous_powr:
    4.38 +  assumes "continuous F f" and "continuous F g" and "0 < f (Lim F (\<lambda>x. x))"
    4.39 +  shows "continuous F (\<lambda>x. (f x) powr (g x))"
    4.40 +  using assms unfolding continuous_def by (rule tendsto_powr)
    4.41 +
    4.42 +lemma continuous_at_within_powr[continuous_intros]:
    4.43 +  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "0 < f a"
    4.44 +  shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
    4.45 +  using assms unfolding continuous_within by (rule tendsto_powr)
    4.46 +
    4.47 +lemma isCont_powr[continuous_intros, simp]:
    4.48 +  assumes "isCont f a" "isCont g a" "0 < f a"
    4.49 +  shows "isCont (\<lambda>x. (f x) powr g x) a"
    4.50 +  using assms unfolding continuous_at by (rule tendsto_powr)
    4.51 +
    4.52 +lemma continuous_on_powr[continuous_on_intros]:
    4.53 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. 0 < f x"
    4.54 +  shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
    4.55 +  using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
    4.56 +
    4.57  (* FIXME: generalize by replacing d by with g x and g ---> d? *)
    4.58  lemma tendsto_zero_powrI:
    4.59    assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
     5.1 --- a/src/HOL/Metric_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     5.2 +++ b/src/HOL/Metric_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     5.3 @@ -582,6 +582,16 @@
     5.4    qed
     5.5  qed
     5.6  
     5.7 +lemma continuous_dist[continuous_intros]:
     5.8 +  fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
     5.9 +  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))"
    5.10 +  unfolding continuous_def by (rule tendsto_dist)
    5.11 +
    5.12 +lemma continuous_on_dist[continuous_on_intros]:
    5.13 +  fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
    5.14 +  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
    5.15 +  unfolding continuous_on_def by (auto intro: tendsto_dist)
    5.16 +
    5.17  lemma tendsto_at_topI_sequentially:
    5.18    fixes f :: "real \<Rightarrow> real"
    5.19    assumes mono: "mono f"
     6.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 10:41:43 2013 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 10:41:43 2013 +0100
     6.3 @@ -26,14 +26,6 @@
     6.4  lemma divide_nonneg_nonneg:assumes "a \<ge> 0" "b \<ge> 0" shows "0 \<le> a / (b::real)"
     6.5    apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto
     6.6  
     6.7 -lemma continuous_setsum:
     6.8 -  fixes f :: "'i \<Rightarrow> 'a::t2_space \<Rightarrow> 'b::real_normed_vector"
     6.9 -  assumes f: "\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)" shows "continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)"
    6.10 -proof cases
    6.11 -  assume "finite I" from this f show ?thesis
    6.12 -    by (induct I) (auto intro!: continuous_intros)
    6.13 -qed (auto intro!: continuous_intros)
    6.14 -
    6.15  lemma brouwer_compactness_lemma:
    6.16    fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
    6.17    assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = 0))"
     7.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 22 10:41:43 2013 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 22 10:41:43 2013 +0100
     7.3 @@ -576,10 +576,6 @@
     7.4    unfolding FDERIV_conv_has_derivative [symmetric]
     7.5    by (rule FDERIV_unique)
     7.6  
     7.7 -lemma continuous_isCont: "isCont f x = continuous (at x) f"
     7.8 -  unfolding isCont_def LIM_def
     7.9 -  unfolding continuous_at Lim_at unfolding dist_nz by auto
    7.10 -
    7.11  lemma frechet_derivative_unique_within_closed_interval:
    7.12    fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
    7.13    assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "x \<in> {a..b}" (is "x\<in>?I")
    7.14 @@ -783,15 +779,12 @@
    7.15    shows "\<exists>x\<in>{a<..<b}. (f b - f a = (f' x) (b - a))"
    7.16  proof-
    7.17    have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
    7.18 -    apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
    7.19 -    defer
    7.20 -    apply(rule continuous_on_intros assms(2))+
    7.21 -  proof
    7.22 +  proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
    7.23      fix x assume x:"x \<in> {a<..<b}"
    7.24      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
    7.25        by (intro has_derivative_intros assms(3)[rule_format,OF x]
    7.26          mult_right_has_derivative)
    7.27 -  qed(insert assms(1), auto simp add:field_simps)
    7.28 +  qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
    7.29    then guess x ..
    7.30    thus ?thesis apply(rule_tac x=x in bexI)
    7.31      apply(drule fun_cong[of _ _ "b - a"]) by auto
     8.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Mar 22 10:41:43 2013 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Mar 22 10:41:43 2013 +0100
     8.3 @@ -22,7 +22,7 @@
     8.4  qed
     8.5  
     8.6  lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
     8.7 -  using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x]
     8.8 +  using isCont_power[OF isCont_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
     8.9    apply (auto simp add: power2_eq_square)
    8.10    apply (rule_tac x="s" in exI)
    8.11    apply auto
     9.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
     9.3 @@ -8,6 +8,14 @@
     9.4  imports Convex_Euclidean_Space
     9.5  begin
     9.6  
     9.7 +lemma continuous_on_cong: (* MOVE to Topological_Spaces *)
     9.8 +  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
     9.9 +  unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto
    9.10 +
    9.11 +lemma continuous_on_compose2:
    9.12 +  shows "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
    9.13 +  using continuous_on_compose[of s f g] by (simp add: comp_def)
    9.14 +
    9.15  subsection {* Paths. *}
    9.16  
    9.17  definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
    9.18 @@ -111,106 +119,32 @@
    9.19    assumes "pathfinish g1 = pathstart g2"
    9.20    shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2"
    9.21    unfolding path_def pathfinish_def pathstart_def
    9.22 -  apply rule defer
    9.23 -  apply(erule conjE)
    9.24 -proof -
    9.25 -  assume as: "continuous_on {0..1} (g1 +++ g2)"
    9.26 -  have *: "g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)"
    9.27 -      "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))"
    9.28 -    unfolding o_def by (auto simp add: add_divide_distrib)
    9.29 -  have "op *\<^sub>R (1 / 2) ` {0::real..1} \<subseteq> {0..1}"
    9.30 -    "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \<subseteq> {0..1}"
    9.31 +proof safe
    9.32 +  assume cont: "continuous_on {0..1} (g1 +++ g2)"
    9.33 +  have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))"
    9.34 +    by (intro continuous_on_cong refl) (auto simp: joinpaths_def)
    9.35 +  have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
    9.36 +    using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
    9.37 +  show "continuous_on {0..1} g1" "continuous_on {0..1} g2"
    9.38 +    unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont])
    9.39 +next
    9.40 +  assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
    9.41 +  have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
    9.42      by auto
    9.43 -  then show "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2"
    9.44 -    apply -
    9.45 -    apply rule
    9.46 -    apply (subst *) defer
    9.47 -    apply (subst *)
    9.48 -    apply (rule_tac[!] continuous_on_compose)
    9.49 -    apply (intro continuous_on_intros) defer
    9.50 -    apply (intro continuous_on_intros)
    9.51 -    apply (rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
    9.52 -    apply (rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"])
    9.53 -    apply (rule as, assumption, rule as, assumption)
    9.54 -    apply rule defer
    9.55 -    apply rule
    9.56 -  proof -
    9.57 -    fix x
    9.58 -    assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
    9.59 -    then have "x \<le> 1 / 2" unfolding image_iff by auto
    9.60 -    then show "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto
    9.61 -  next
    9.62 -    fix x
    9.63 -    assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}"
    9.64 -    then have "x \<ge> 1 / 2" unfolding image_iff by auto
    9.65 -    then show "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)"
    9.66 -    proof (cases "x = 1 / 2")
    9.67 -      case True
    9.68 -      then have "x = (1/2) *\<^sub>R 1" by auto
    9.69 -      then show ?thesis
    9.70 -        unfolding joinpaths_def
    9.71 -        using assms[unfolded pathstart_def pathfinish_def]
    9.72 -        by (auto simp add: mult_ac)
    9.73 -    qed (auto simp add:le_less joinpaths_def)
    9.74 -  qed
    9.75 -next
    9.76 -  assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2"
    9.77 -  have *: "{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by auto
    9.78 -  have **: "op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}"
    9.79 -    apply (rule set_eqI, rule)
    9.80 -    unfolding image_iff
    9.81 -    defer
    9.82 -    apply (rule_tac x="(1/2)*\<^sub>R x" in bexI)
    9.83 -    apply auto
    9.84 -    done
    9.85 -  have ***: "(\<lambda>x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}"
    9.86 -    apply (auto simp add: image_def)
    9.87 -    apply (rule_tac x="(x + 1) / 2" in bexI)
    9.88 -    apply (auto simp add: add_divide_distrib)
    9.89 -    done
    9.90 +  { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}"
    9.91 +      by (intro image_eqI[where x="x/2"]) auto }
    9.92 +  note 1 = this
    9.93 +  { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2 - 1) ` {1 / 2..1}"
    9.94 +      by (intro image_eqI[where x="x/2 + 1/2"]) auto }
    9.95 +  note 2 = this
    9.96    show "continuous_on {0..1} (g1 +++ g2)"
    9.97 -    unfolding *
    9.98 -    apply (rule continuous_on_union)
    9.99 -    apply (rule closed_real_atLeastAtMost)+
   9.100 -  proof -
   9.101 -    show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)"
   9.102 -      apply (rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
   9.103 -      unfolding o_def[THEN sym]
   9.104 -      apply (rule continuous_on_compose)
   9.105 -      apply (intro continuous_on_intros)
   9.106 -      unfolding **
   9.107 -      apply (rule as(1))
   9.108 -      unfolding joinpaths_def
   9.109 -      apply auto
   9.110 -      done
   9.111 -  next
   9.112 -    show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)"
   9.113 -      apply (rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
   9.114 -      apply (rule continuous_on_compose)
   9.115 -      apply (intro continuous_on_intros)
   9.116 -      unfolding *** o_def joinpaths_def
   9.117 -      apply (rule as(2))
   9.118 -      using assms[unfolded pathstart_def pathfinish_def]
   9.119 -      apply (auto simp add: mult_ac)  
   9.120 -      done
   9.121 -  qed
   9.122 +    using assms unfolding joinpaths_def 01
   9.123 +    by (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros)
   9.124 +       (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2)
   9.125  qed
   9.126  
   9.127  lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)"
   9.128 -proof
   9.129 -  fix x
   9.130 -  assume "x \<in> path_image (g1 +++ g2)"
   9.131 -  then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))"
   9.132 -    unfolding path_image_def image_iff joinpaths_def by auto
   9.133 -  then show "x \<in> path_image g1 \<union> path_image g2"
   9.134 -    apply (cases "y \<le> 1/2")
   9.135 -    apply (rule_tac UnI1) defer
   9.136 -    apply (rule_tac UnI2)
   9.137 -    unfolding y(2) path_image_def
   9.138 -    using y(1)
   9.139 -    apply (auto intro!: imageI)
   9.140 -    done
   9.141 -qed
   9.142 +  unfolding path_image_def joinpaths_def by auto
   9.143  
   9.144  lemma subset_path_image_join:
   9.145    assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s"
   9.146 @@ -218,7 +152,7 @@
   9.147    using path_image_join_subset[of g1 g2] and assms by auto
   9.148  
   9.149  lemma path_image_join:
   9.150 -  assumes "path g1" "path g2" "pathfinish g1 = pathstart g2"
   9.151 +  assumes "pathfinish g1 = pathstart g2"
   9.152    shows "path_image(g1 +++ g2) = (path_image g1) \<union> (path_image g2)"
   9.153    apply (rule, rule path_image_join_subset, rule)
   9.154    unfolding Un_iff
   9.155 @@ -240,7 +174,7 @@
   9.156    then show "x \<in> path_image (g1 +++ g2)"
   9.157      unfolding joinpaths_def path_image_def image_iff
   9.158      apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI)
   9.159 -    using assms(3)[unfolded pathfinish_def pathstart_def]
   9.160 +    using assms(1)[unfolded pathfinish_def pathstart_def]
   9.161      apply (auto simp add: add_divide_distrib) 
   9.162      done
   9.163  qed
    10.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
    10.3 @@ -1273,18 +1273,6 @@
    10.4  
    10.5  subsection {* Limits *}
    10.6  
    10.7 -text{* Notation Lim to avoid collition with lim defined in analysis *}
    10.8 -
    10.9 -definition Lim :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b"
   10.10 -  where "Lim A f = (THE l. (f ---> l) A)"
   10.11 -
   10.12 -text{* Uniqueness of the limit, when nontrivial. *}
   10.13 -
   10.14 -lemma tendsto_Lim:
   10.15 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
   10.16 -  shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
   10.17 -  unfolding Lim_def using tendsto_unique[of net f] by auto
   10.18 -
   10.19  lemma Lim:
   10.20   "(f ---> l) net \<longleftrightarrow>
   10.21          trivial_limit net \<or>
   10.22 @@ -3769,35 +3757,6 @@
   10.23  
   10.24  subsection {* Continuity *}
   10.25  
   10.26 -text {* Define continuity over a net to take in restrictions of the set. *}
   10.27 -
   10.28 -definition
   10.29 -  continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
   10.30 -  where "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
   10.31 -
   10.32 -lemma continuous_trivial_limit:
   10.33 - "trivial_limit net ==> continuous net f"
   10.34 -  unfolding continuous_def tendsto_def trivial_limit_eq by auto
   10.35 -
   10.36 -lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
   10.37 -  unfolding continuous_def
   10.38 -  unfolding tendsto_def
   10.39 -  using netlimit_within[of x s]
   10.40 -  by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
   10.41 -
   10.42 -lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
   10.43 -  using continuous_within [of x UNIV f] by simp
   10.44 -
   10.45 -lemma continuous_isCont: "isCont f x = continuous (at x) f"
   10.46 -  unfolding isCont_def LIM_def
   10.47 -  unfolding continuous_at Lim_at unfolding dist_nz by auto
   10.48 -
   10.49 -lemma continuous_at_within:
   10.50 -  assumes "continuous (at x) f"  shows "continuous (at x within s) f"
   10.51 -  using assms unfolding continuous_at continuous_within
   10.52 -  by (rule Lim_at_within)
   10.53 -
   10.54 -
   10.55  text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
   10.56  
   10.57  lemma continuous_within_eps_delta:
   10.58 @@ -3843,20 +3802,6 @@
   10.59  
   10.60  text{* Define setwise continuity in terms of limits within the set. *}
   10.61  
   10.62 -definition
   10.63 -  continuous_on ::
   10.64 -    "'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
   10.65 -where
   10.66 -  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
   10.67 -
   10.68 -lemma continuous_on_topological:
   10.69 -  "continuous_on s f \<longleftrightarrow>
   10.70 -    (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
   10.71 -      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
   10.72 -unfolding continuous_on_def tendsto_def
   10.73 -unfolding Limits.eventually_within eventually_at_topological
   10.74 -by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
   10.75 -
   10.76  lemma continuous_on_iff:
   10.77    "continuous_on s f \<longleftrightarrow>
   10.78      (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
   10.79 @@ -3884,38 +3829,7 @@
   10.80    unfolding continuous_within continuous_at using Lim_at_within by auto
   10.81  
   10.82  lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
   10.83 -unfolding tendsto_def by (simp add: trivial_limit_eq)
   10.84 -
   10.85 -lemma continuous_at_imp_continuous_on:
   10.86 -  assumes "\<forall>x\<in>s. continuous (at x) f"
   10.87 -  shows "continuous_on s f"
   10.88 -unfolding continuous_on_def
   10.89 -proof
   10.90 -  fix x assume "x \<in> s"
   10.91 -  with assms have *: "(f ---> f (netlimit (at x))) (at x)"
   10.92 -    unfolding continuous_def by simp
   10.93 -  have "(f ---> f x) (at x)"
   10.94 -  proof (cases "trivial_limit (at x)")
   10.95 -    case True thus ?thesis
   10.96 -      by (rule Lim_trivial_limit)
   10.97 -  next
   10.98 -    case False
   10.99 -    hence 1: "netlimit (at x) = x"
  10.100 -      using netlimit_within [of x UNIV] by simp
  10.101 -    with * show ?thesis by simp
  10.102 -  qed
  10.103 -  thus "(f ---> f x) (at x within s)"
  10.104 -    by (rule Lim_at_within)
  10.105 -qed
  10.106 -
  10.107 -lemma continuous_on_eq_continuous_within:
  10.108 -  "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
  10.109 -unfolding continuous_on_def continuous_def
  10.110 -apply (rule ball_cong [OF refl])
  10.111 -apply (case_tac "trivial_limit (at x within s)")
  10.112 -apply (simp add: Lim_trivial_limit)
  10.113 -apply (simp add: netlimit_within)
  10.114 -done
  10.115 +  by simp
  10.116  
  10.117  lemmas continuous_on = continuous_on_def -- "legacy theorem name"
  10.118  
  10.119 @@ -4056,169 +3970,32 @@
  10.120  
  10.121  subsubsection {* Structural rules for pointwise continuity *}
  10.122  
  10.123 -ML {*
  10.124 -
  10.125 -structure Continuous_Intros = Named_Thms
  10.126 -(
  10.127 -  val name = @{binding continuous_intros}
  10.128 -  val description = "Structural introduction rules for pointwise continuity"
  10.129 -)
  10.130 -
  10.131 -*}
  10.132 -
  10.133 -setup Continuous_Intros.setup
  10.134 -
  10.135 -lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\<lambda>x. x)"
  10.136 -  unfolding continuous_within by (rule tendsto_ident_at_within)
  10.137 -
  10.138 -lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)"
  10.139 -  unfolding continuous_at by (rule tendsto_ident_at)
  10.140 -
  10.141 -lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)"
  10.142 -  unfolding continuous_def by (rule tendsto_const)
  10.143 -
  10.144 -lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
  10.145 -  unfolding continuous_def by (rule tendsto_fst)
  10.146 -
  10.147 -lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
  10.148 -  unfolding continuous_def by (rule tendsto_snd)
  10.149 -
  10.150 -lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
  10.151 -  unfolding continuous_def by (rule tendsto_Pair)
  10.152 -
  10.153 -lemma continuous_dist[continuous_intros]:
  10.154 -  assumes "continuous F f" and "continuous F g"
  10.155 -  shows "continuous F (\<lambda>x. dist (f x) (g x))"
  10.156 -  using assms unfolding continuous_def by (rule tendsto_dist)
  10.157 +lemmas continuous_within_id = continuous_ident
  10.158 +
  10.159 +lemmas continuous_at_id = isCont_ident
  10.160  
  10.161  lemma continuous_infdist[continuous_intros]:
  10.162    assumes "continuous F f"
  10.163    shows "continuous F (\<lambda>x. infdist (f x) A)"
  10.164    using assms unfolding continuous_def by (rule tendsto_infdist)
  10.165  
  10.166 -lemma continuous_norm[continuous_intros]:
  10.167 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
  10.168 -  unfolding continuous_def by (rule tendsto_norm)
  10.169 -
  10.170  lemma continuous_infnorm[continuous_intros]:
  10.171    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
  10.172    unfolding continuous_def by (rule tendsto_infnorm)
  10.173  
  10.174 -lemma continuous_add[continuous_intros]:
  10.175 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
  10.176 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
  10.177 -  unfolding continuous_def by (rule tendsto_add)
  10.178 -
  10.179 -lemma continuous_minus[continuous_intros]:
  10.180 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
  10.181 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
  10.182 -  unfolding continuous_def by (rule tendsto_minus)
  10.183 -
  10.184 -lemma continuous_diff[continuous_intros]:
  10.185 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
  10.186 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
  10.187 -  unfolding continuous_def by (rule tendsto_diff)
  10.188 -
  10.189 -lemma continuous_scaleR[continuous_intros]:
  10.190 -  fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
  10.191 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)"
  10.192 -  unfolding continuous_def by (rule tendsto_scaleR)
  10.193 -
  10.194 -lemma continuous_mult[continuous_intros]:
  10.195 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
  10.196 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
  10.197 -  unfolding continuous_def by (rule tendsto_mult)
  10.198 -
  10.199  lemma continuous_inner[continuous_intros]:
  10.200    assumes "continuous F f" and "continuous F g"
  10.201    shows "continuous F (\<lambda>x. inner (f x) (g x))"
  10.202    using assms unfolding continuous_def by (rule tendsto_inner)
  10.203  
  10.204 -lemma continuous_inverse[continuous_intros]:
  10.205 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
  10.206 -  assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
  10.207 -  shows "continuous F (\<lambda>x. inverse (f x))"
  10.208 -  using assms unfolding continuous_def by (rule tendsto_inverse)
  10.209 -
  10.210 -lemma continuous_at_within_inverse[continuous_intros]:
  10.211 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
  10.212 -  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
  10.213 -  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
  10.214 -  using assms unfolding continuous_within by (rule tendsto_inverse)
  10.215 -
  10.216 -lemma continuous_at_inverse[continuous_intros]:
  10.217 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
  10.218 -  assumes "continuous (at a) f" and "f a \<noteq> 0"
  10.219 -  shows "continuous (at a) (\<lambda>x. inverse (f x))"
  10.220 -  using assms unfolding continuous_at by (rule tendsto_inverse)
  10.221 +lemmas continuous_at_inverse = isCont_inverse
  10.222  
  10.223  subsubsection {* Structural rules for setwise continuity *}
  10.224  
  10.225 -ML {*
  10.226 -
  10.227 -structure Continuous_On_Intros = Named_Thms
  10.228 -(
  10.229 -  val name = @{binding continuous_on_intros}
  10.230 -  val description = "Structural introduction rules for setwise continuity"
  10.231 -)
  10.232 -
  10.233 -*}
  10.234 -
  10.235 -setup Continuous_On_Intros.setup
  10.236 -
  10.237 -lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
  10.238 -  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
  10.239 -
  10.240 -lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
  10.241 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
  10.242 -
  10.243 -lemma continuous_on_norm[continuous_on_intros]:
  10.244 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
  10.245 -  unfolding continuous_on_def by (fast intro: tendsto_norm)
  10.246 -
  10.247  lemma continuous_on_infnorm[continuous_on_intros]:
  10.248    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
  10.249    unfolding continuous_on by (fast intro: tendsto_infnorm)
  10.250  
  10.251 -lemma continuous_on_minus[continuous_on_intros]:
  10.252 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
  10.253 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
  10.254 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
  10.255 -
  10.256 -lemma continuous_on_add[continuous_on_intros]:
  10.257 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
  10.258 -  shows "continuous_on s f \<Longrightarrow> continuous_on s g
  10.259 -           \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
  10.260 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
  10.261 -
  10.262 -lemma continuous_on_diff[continuous_on_intros]:
  10.263 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
  10.264 -  shows "continuous_on s f \<Longrightarrow> continuous_on s g
  10.265 -           \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
  10.266 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
  10.267 -
  10.268 -lemma (in bounded_linear) continuous_on[continuous_on_intros]:
  10.269 -  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
  10.270 -  unfolding continuous_on_def by (fast intro: tendsto)
  10.271 -
  10.272 -lemma (in bounded_bilinear) continuous_on[continuous_on_intros]:
  10.273 -  "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
  10.274 -  unfolding continuous_on_def by (fast intro: tendsto)
  10.275 -
  10.276 -lemma continuous_on_scaleR[continuous_on_intros]:
  10.277 -  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
  10.278 -  assumes "continuous_on s f" and "continuous_on s g"
  10.279 -  shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
  10.280 -  using bounded_bilinear_scaleR assms
  10.281 -  by (rule bounded_bilinear.continuous_on)
  10.282 -
  10.283 -lemma continuous_on_mult[continuous_on_intros]:
  10.284 -  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
  10.285 -  assumes "continuous_on s f" and "continuous_on s g"
  10.286 -  shows "continuous_on s (\<lambda>x. f x * g x)"
  10.287 -  using bounded_bilinear_mult assms
  10.288 -  by (rule bounded_bilinear.continuous_on)
  10.289 -
  10.290  lemma continuous_on_inner[continuous_on_intros]:
  10.291    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
  10.292    assumes "continuous_on s f" and "continuous_on s g"
  10.293 @@ -4226,12 +4003,6 @@
  10.294    using bounded_bilinear_inner assms
  10.295    by (rule bounded_bilinear.continuous_on)
  10.296  
  10.297 -lemma continuous_on_inverse[continuous_on_intros]:
  10.298 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
  10.299 -  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
  10.300 -  shows "continuous_on s (\<lambda>x. inverse (f x))"
  10.301 -  using assms unfolding continuous_on by (fast intro: tendsto_inverse)
  10.302 -
  10.303  subsubsection {* Structural rules for uniform continuity *}
  10.304  
  10.305  lemma uniformly_continuous_on_id[continuous_on_intros]:
  10.306 @@ -4312,33 +4083,7 @@
  10.307  
  10.308  text{* Continuity of all kinds is preserved under composition. *}
  10.309  
  10.310 -lemma continuous_within_topological:
  10.311 -  "continuous (at x within s) f \<longleftrightarrow>
  10.312 -    (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
  10.313 -      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
  10.314 -unfolding continuous_within
  10.315 -unfolding tendsto_def Limits.eventually_within eventually_at_topological
  10.316 -by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
  10.317 -
  10.318 -lemma continuous_within_compose[continuous_intros]:
  10.319 -  assumes "continuous (at x within s) f"
  10.320 -  assumes "continuous (at (f x) within f ` s) g"
  10.321 -  shows "continuous (at x within s) (g o f)"
  10.322 -using assms unfolding continuous_within_topological by simp metis
  10.323 -
  10.324 -lemma continuous_at_compose[continuous_intros]:
  10.325 -  assumes "continuous (at x) f" and "continuous (at (f x)) g"
  10.326 -  shows "continuous (at x) (g o f)"
  10.327 -proof-
  10.328 -  have "continuous (at (f x) within range f) g" using assms(2)
  10.329 -    using continuous_within_subset[of "f x" UNIV g "range f"] by simp
  10.330 -  thus ?thesis using assms(1)
  10.331 -    using continuous_within_compose[of x UNIV f g] by simp
  10.332 -qed
  10.333 -
  10.334 -lemma continuous_on_compose[continuous_on_intros]:
  10.335 -  "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
  10.336 -  unfolding continuous_on_topological by simp metis
  10.337 +lemmas continuous_at_compose = isCont_o
  10.338  
  10.339  lemma uniformly_continuous_on_compose[continuous_on_intros]:
  10.340    assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
  10.341 @@ -5182,8 +4927,7 @@
  10.342    have "compact (s \<times> s)" using `compact s` by (intro compact_Times)
  10.343    moreover have "s \<times> s \<noteq> {}" using `s \<noteq> {}` by auto
  10.344    moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"
  10.345 -    by (intro continuous_at_imp_continuous_on ballI continuous_dist
  10.346 -      continuous_isCont[THEN iffD1] isCont_fst isCont_snd isCont_ident)
  10.347 +    by (intro continuous_at_imp_continuous_on ballI continuous_intros)
  10.348    ultimately show ?thesis
  10.349      using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
  10.350  qed
  10.351 @@ -5873,7 +5617,7 @@
  10.352    by (rule isCont_open_vimage)
  10.353  
  10.354  lemma open_Collect_less:
  10.355 -  fixes f g :: "'a::topological_space \<Rightarrow> real"
  10.356 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
  10.357    assumes f: "\<And>x. isCont f x"
  10.358    assumes g: "\<And>x. isCont g x"
  10.359    shows "open {x. f x < g x}"
  10.360 @@ -5887,7 +5631,7 @@
  10.361  qed
  10.362  
  10.363  lemma closed_Collect_le:
  10.364 -  fixes f g :: "'a::topological_space \<Rightarrow> real"
  10.365 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
  10.366    assumes f: "\<And>x. isCont f x"
  10.367    assumes g: "\<And>x. isCont g x"
  10.368    shows "closed {x. f x \<le> g x}"
  10.369 @@ -5901,7 +5645,7 @@
  10.370  qed
  10.371  
  10.372  lemma closed_Collect_eq:
  10.373 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
  10.374 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
  10.375    assumes f: "\<And>x. isCont f x"
  10.376    assumes g: "\<And>x. isCont g x"
  10.377    shows "closed {x. f x = g x}"
    11.1 --- a/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
    11.2 +++ b/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
    11.3 @@ -338,6 +338,18 @@
    11.4  apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero)
    11.5  done
    11.6  
    11.7 +lemma tendsto_real_root[tendsto_intros]:
    11.8 +  "(f ---> x) F \<Longrightarrow> 0 < n \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
    11.9 +  using isCont_tendsto_compose[OF isCont_real_root, of n f x F] .
   11.10 +
   11.11 +lemma continuous_real_root[continuous_intros]:
   11.12 +  "continuous F f \<Longrightarrow> 0 < n \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
   11.13 +  unfolding continuous_def by (rule tendsto_real_root)
   11.14 +  
   11.15 +lemma continuous_on_real_root[continuous_on_intros]:
   11.16 +  "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
   11.17 +  unfolding continuous_on_def by (auto intro: tendsto_real_root)
   11.18 +
   11.19  lemma DERIV_real_root:
   11.20    assumes n: "0 < n"
   11.21    assumes x: "0 < x"
   11.22 @@ -491,6 +503,18 @@
   11.23  lemma isCont_real_sqrt: "isCont sqrt x"
   11.24  unfolding sqrt_def by (rule isCont_real_root [OF pos2])
   11.25  
   11.26 +lemma tendsto_real_sqrt[tendsto_intros]:
   11.27 +  "(f ---> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
   11.28 +  unfolding sqrt_def by (rule tendsto_real_root [OF _ pos2])
   11.29 +
   11.30 +lemma continuous_real_sqrt[continuous_intros]:
   11.31 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
   11.32 +  unfolding sqrt_def by (rule continuous_real_root [OF _ pos2])
   11.33 +  
   11.34 +lemma continuous_on_real_sqrt[continuous_on_intros]:
   11.35 +  "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
   11.36 +  unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2])
   11.37 +
   11.38  lemma DERIV_real_sqrt_generic:
   11.39    assumes "x \<noteq> 0"
   11.40    assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
    12.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Mar 22 10:41:43 2013 +0100
    12.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Mar 22 10:41:43 2013 +0100
    12.3 @@ -675,11 +675,6 @@
    12.4    by (rule borel_measurable_continuous_Pair)
    12.5       (auto intro: continuous_on_fst continuous_on_snd continuous_on_mult)
    12.6  
    12.7 -lemma continuous_on_dist:
    12.8 -  fixes f :: "'a :: t2_space \<Rightarrow> 'b :: metric_space"
    12.9 -  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   12.10 -  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
   12.11 -
   12.12  lemma borel_measurable_dist[measurable (raw)]:
   12.13    fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   12.14    assumes f: "f \<in> borel_measurable M"
   12.15 @@ -794,8 +789,7 @@
   12.16    have "(\<lambda>x. if f x \<in> {0<..} then ln (f x) else ln 0) \<in> borel_measurable M"
   12.17    proof (rule borel_measurable_continuous_on_open[OF _ _ f])
   12.18      show "continuous_on {0<..} ln"
   12.19 -      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont
   12.20 -               simp: continuous_isCont[symmetric])
   12.21 +      by (auto intro!: continuous_at_imp_continuous_on DERIV_ln DERIV_isCont)
   12.22      show "open ({0<..}::real set)" by auto
   12.23    qed
   12.24    also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
   12.25 @@ -808,8 +802,7 @@
   12.26    unfolding log_def by auto
   12.27  
   12.28  lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel"
   12.29 -  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI
   12.30 -            continuous_isCont[THEN iffD1] isCont_exp)
   12.31 +  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)
   12.32  
   12.33  lemma measurable_count_space_eq2_countable:
   12.34    fixes f :: "'a => 'c::countable"
    13.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Mar 22 10:41:43 2013 +0100
    13.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Mar 22 10:41:43 2013 +0100
    13.3 @@ -1049,7 +1049,7 @@
    13.4  
    13.5      let ?g = "\<lambda>x. if x = a then f a else if x = b then f b else if x \<in> {a <..< b} then f x else 0"
    13.6      from f have "continuous_on {a <..< b} f"
    13.7 -      by (subst continuous_on_eq_continuous_at) (auto simp add: continuous_isCont)
    13.8 +      by (subst continuous_on_eq_continuous_at) auto
    13.9      then have "?g \<in> borel_measurable borel"
   13.10        using borel_measurable_continuous_on_open[of "{a <..< b }" f "\<lambda>x. x" borel 0]
   13.11        by (auto intro!: measurable_If[where P="\<lambda>x. x = a"] measurable_If[where P="\<lambda>x. x = b"])
    14.1 --- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
    14.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
    14.3 @@ -39,6 +39,15 @@
    14.4  lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
    14.5    unfolding INF_def by (rule open_Inter) auto
    14.6  
    14.7 +lemma openI:
    14.8 +  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
    14.9 +  shows "open S"
   14.10 +proof -
   14.11 +  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
   14.12 +  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
   14.13 +  ultimately show "open S" by simp
   14.14 +qed
   14.15 +
   14.16  lemma closed_empty [intro, simp]:  "closed {}"
   14.17    unfolding closed_def by simp
   14.18  
   14.19 @@ -835,6 +844,9 @@
   14.20    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   14.21    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
   14.22  
   14.23 +definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where
   14.24 +  "Lim A f = (THE l. (f ---> l) A)"
   14.25 +
   14.26  lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
   14.27    by simp
   14.28  
   14.29 @@ -919,11 +931,10 @@
   14.30    "((\<lambda>x. x) ---> a) (at a within S)"
   14.31    unfolding tendsto_def eventually_within eventually_at_topological by auto
   14.32  
   14.33 -lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
   14.34 +lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
   14.35    by (simp add: tendsto_def)
   14.36  
   14.37 -lemma tendsto_unique:
   14.38 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
   14.39 +lemma (in t2_space) tendsto_unique:
   14.40    assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
   14.41    shows "a = b"
   14.42  proof (rule ccontr)
   14.43 @@ -946,9 +957,8 @@
   14.44      by (simp add: trivial_limit_def)
   14.45  qed
   14.46  
   14.47 -lemma tendsto_const_iff:
   14.48 -  fixes a b :: "'a::t2_space"
   14.49 -  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
   14.50 +lemma (in t2_space) tendsto_const_iff:
   14.51 +  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
   14.52    by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
   14.53  
   14.54  lemma increasing_tendsto:
   14.55 @@ -1003,6 +1013,18 @@
   14.56    shows "a \<le> x"
   14.57    using F x tendsto_const a by (rule tendsto_le)
   14.58  
   14.59 +subsubsection {* Rules about @{const Lim} *}
   14.60 +
   14.61 +lemma (in t2_space) tendsto_Lim:
   14.62 +  "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
   14.63 +  unfolding Lim_def using tendsto_unique[of net f] by auto
   14.64 +
   14.65 +lemma Lim_ident_at: "\<not> trivial_limit (at x) \<Longrightarrow> Lim (at x) (\<lambda>x. x) = x"
   14.66 +  by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
   14.67 +
   14.68 +lemma Lim_ident_at_within: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   14.69 +  by (rule tendsto_Lim[OF _ tendsto_ident_at_within]) auto
   14.70 +
   14.71  subsection {* Limits to @{const at_top} and @{const at_bot} *}
   14.72  
   14.73  lemma filterlim_at_top:
   14.74 @@ -1132,14 +1154,15 @@
   14.75      ("((_)/ ----> (_))" [60, 60] 60) where
   14.76    "X ----> L \<equiv> (X ---> L) sequentially"
   14.77  
   14.78 -definition
   14.79 -  lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
   14.80 -    --{*Standard definition of limit using choice operator*}
   14.81 -  "lim X = (THE L. X ----> L)"
   14.82 +abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
   14.83 +  "lim X \<equiv> Lim sequentially X"
   14.84  
   14.85  definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   14.86    "convergent X = (\<exists>L. X ----> L)"
   14.87  
   14.88 +lemma lim_def: "lim X = (THE L. X ----> L)"
   14.89 +  unfolding Lim_def ..
   14.90 +
   14.91  subsubsection {* Monotone sequences and subsequences *}
   14.92  
   14.93  definition
   14.94 @@ -1608,23 +1631,154 @@
   14.95  
   14.96  subsection {* Continuity *}
   14.97  
   14.98 -definition isCont :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
   14.99 -  "isCont f a \<longleftrightarrow> f -- a --> f a"
  14.100 +subsubsection {* Continuity on a set *}
  14.101 +
  14.102 +definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
  14.103 +  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
  14.104 +
  14.105 +lemma continuous_on_topological:
  14.106 +  "continuous_on s f \<longleftrightarrow>
  14.107 +    (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
  14.108 +  unfolding continuous_on_def tendsto_def eventually_within eventually_at_topological by metis
  14.109 +
  14.110 +lemma continuous_on_open_invariant:
  14.111 +  "continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s))"
  14.112 +proof safe
  14.113 +  fix B :: "'b set" assume "continuous_on s f" "open B"
  14.114 +  then have "\<forall>x\<in>f -` B \<inter> s. (\<exists>A. open A \<and> x \<in> A \<and> s \<inter> A \<subseteq> f -` B)"
  14.115 +    by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL)
  14.116 +  then guess A unfolding bchoice_iff ..
  14.117 +  then show "\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s"
  14.118 +    by (intro exI[of _ "\<Union>x\<in>f -` B \<inter> s. A x"]) auto
  14.119 +next
  14.120 +  assume B: "\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s)"
  14.121 +  show "continuous_on s f"
  14.122 +    unfolding continuous_on_topological
  14.123 +  proof safe
  14.124 +    fix x B assume "x \<in> s" "open B" "f x \<in> B"
  14.125 +    with B obtain A where A: "open A" "A \<inter> s = f -` B \<inter> s" by auto
  14.126 +    with `x \<in> s` `f x \<in> B` show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
  14.127 +      by (intro exI[of _ A]) auto
  14.128 +  qed
  14.129 +qed
  14.130 +
  14.131 +lemma continuous_on_closed_invariant:
  14.132 +  "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
  14.133 +proof -
  14.134 +  have *: "\<And>P Q::'b set\<Rightarrow>bool. (\<And>A. P A \<longleftrightarrow> Q (- A)) \<Longrightarrow> (\<forall>A. P A) \<longleftrightarrow> (\<forall>A. Q A)"
  14.135 +    by (metis double_compl)
  14.136 +  show ?thesis
  14.137 +    unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric])
  14.138 +qed
  14.139 +
  14.140 +ML {*
  14.141 +
  14.142 +structure Continuous_On_Intros = Named_Thms
  14.143 +(
  14.144 +  val name = @{binding continuous_on_intros}
  14.145 +  val description = "Structural introduction rules for setwise continuity"
  14.146 +)
  14.147 +
  14.148 +*}
  14.149 +
  14.150 +setup Continuous_On_Intros.setup
  14.151 +
  14.152 +lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
  14.153 +  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
  14.154 +
  14.155 +lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
  14.156 +  unfolding continuous_on_def by (auto intro: tendsto_const)
  14.157 +
  14.158 +lemma continuous_on_compose[continuous_on_intros]:
  14.159 +  "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
  14.160 +  unfolding continuous_on_topological by simp metis
  14.161 +
  14.162 +subsubsection {* Continuity at a point *}
  14.163 +
  14.164 +definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
  14.165 +  "continuous F f \<longleftrightarrow> (f ---> f (Lim F (\<lambda>x. x))) F"
  14.166 +
  14.167 +ML {*
  14.168  
  14.169 -lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
  14.170 -  unfolding isCont_def by (rule tendsto_ident_at)
  14.171 +structure Continuous_Intros = Named_Thms
  14.172 +(
  14.173 +  val name = @{binding continuous_intros}
  14.174 +  val description = "Structural introduction rules for pointwise continuity"
  14.175 +)
  14.176 +
  14.177 +*}
  14.178 +
  14.179 +setup Continuous_Intros.setup
  14.180 +
  14.181 +lemma continuous_bot[continuous_intros, simp]: "continuous bot f"
  14.182 +  unfolding continuous_def by auto
  14.183 +
  14.184 +lemma continuous_trivial_limit: "trivial_limit net \<Longrightarrow> continuous net f"
  14.185 +  by simp
  14.186 +
  14.187 +lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f x) (at x within s)"
  14.188 +  by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at_within continuous_def)
  14.189 +
  14.190 +lemma continuous_within_topological:
  14.191 +  "continuous (at x within s) f \<longleftrightarrow>
  14.192 +    (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
  14.193 +  unfolding continuous_within tendsto_def eventually_within eventually_at_topological by metis
  14.194 +
  14.195 +lemma continuous_within_compose[continuous_intros]:
  14.196 +  "continuous (at x within s) f \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
  14.197 +  continuous (at x within s) (g o f)"
  14.198 +  by (simp add: continuous_within_topological) metis
  14.199 +
  14.200 +lemma continuous_within_compose2:
  14.201 +  "continuous (at x within s) f \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
  14.202 +  continuous (at x within s) (\<lambda>x. g (f x))"
  14.203 +  using continuous_within_compose[of x s f g] by (simp add: comp_def)
  14.204  
  14.205 -lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
  14.206 -  unfolding isCont_def by (rule tendsto_const)
  14.207 +lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f -- x --> f x"
  14.208 +  using continuous_within[of x UNIV f] by simp
  14.209 +
  14.210 +lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
  14.211 +  unfolding continuous_within by (rule tendsto_ident_at_within)
  14.212 +
  14.213 +lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
  14.214 +  unfolding continuous_def by (rule tendsto_const)
  14.215 +
  14.216 +lemma continuous_on_eq_continuous_within:
  14.217 +  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. continuous (at x within s) f)"
  14.218 +  unfolding continuous_on_def continuous_within ..
  14.219 +
  14.220 +abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
  14.221 +  "isCont f a \<equiv> continuous (at a) f"
  14.222 +
  14.223 +lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
  14.224 +  by (rule continuous_at)
  14.225 +
  14.226 +lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
  14.227 +  by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
  14.228 +
  14.229 +lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
  14.230 +  by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
  14.231 +
  14.232 +lemma isContI_continuous: "continuous (at x within UNIV) f \<Longrightarrow> isCont f x"
  14.233 +  by simp
  14.234 +
  14.235 +lemma isCont_ident[continuous_intros, simp]: "isCont (\<lambda>x. x) a"
  14.236 +  using continuous_ident by (rule isContI_continuous)
  14.237 +
  14.238 +lemmas isCont_const = continuous_const
  14.239 +
  14.240 +lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
  14.241 +  unfolding isCont_def by (rule tendsto_compose)
  14.242 +
  14.243 +lemma isCont_o[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a"
  14.244 +  unfolding o_def by (rule isCont_o2)
  14.245  
  14.246  lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
  14.247    unfolding isCont_def by (rule tendsto_compose)
  14.248  
  14.249 -lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
  14.250 -  unfolding isCont_def by (rule tendsto_compose)
  14.251 -
  14.252 -lemma isCont_o: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g o f) a"
  14.253 -  unfolding o_def by (rule isCont_o2)
  14.254 +lemma continuous_within_compose3:
  14.255 +  "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
  14.256 +  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
  14.257  
  14.258  end
  14.259  
    15.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
    15.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
    15.3 @@ -881,6 +881,12 @@
    15.4    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
    15.5    by (rule isCont_tendsto_compose [OF isCont_exp])
    15.6  
    15.7 +lemma continuous_exp [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
    15.8 +  unfolding continuous_def by (rule tendsto_exp)
    15.9 +
   15.10 +lemma continuous_on_exp [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
   15.11 +  unfolding continuous_on_def by (auto intro: tendsto_exp)
   15.12 +
   15.13  subsubsection {* Properties of the Exponential Function *}
   15.14  
   15.15  lemma powser_zero:
   15.16 @@ -1169,6 +1175,22 @@
   15.17    "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   15.18    by (rule isCont_tendsto_compose [OF isCont_ln])
   15.19  
   15.20 +lemma continuous_ln:
   15.21 +  "continuous F f \<Longrightarrow> 0 < f (Lim F (\<lambda>x. x)) \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
   15.22 +  unfolding continuous_def by (rule tendsto_ln)
   15.23 +
   15.24 +lemma isCont_ln' [continuous_intros]:
   15.25 +  "continuous (at x) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
   15.26 +  unfolding continuous_at by (rule tendsto_ln)
   15.27 +
   15.28 +lemma continuous_within_ln [continuous_intros]:
   15.29 +  "continuous (at x within s) f \<Longrightarrow> 0 < f x \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
   15.30 +  unfolding continuous_within by (rule tendsto_ln)
   15.31 +
   15.32 +lemma continuous_on_ln [continuous_on_intros]:
   15.33 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. 0 < f x) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
   15.34 +  unfolding continuous_on_def by (auto intro: tendsto_ln)
   15.35 +
   15.36  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
   15.37    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
   15.38    apply (erule DERIV_cong [OF DERIV_exp exp_ln])
   15.39 @@ -1449,6 +1471,22 @@
   15.40    "(f ---> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) ---> cos a) F"
   15.41    by (rule isCont_tendsto_compose [OF isCont_cos])
   15.42  
   15.43 +lemma continuous_sin [continuous_intros]:
   15.44 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
   15.45 +  unfolding continuous_def by (rule tendsto_sin)
   15.46 +
   15.47 +lemma continuous_on_sin [continuous_on_intros]:
   15.48 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
   15.49 +  unfolding continuous_on_def by (auto intro: tendsto_sin)
   15.50 +
   15.51 +lemma continuous_cos [continuous_intros]:
   15.52 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
   15.53 +  unfolding continuous_def by (rule tendsto_cos)
   15.54 +
   15.55 +lemma continuous_on_cos [continuous_on_intros]:
   15.56 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
   15.57 +  unfolding continuous_on_def by (auto intro: tendsto_cos)
   15.58 +
   15.59  declare
   15.60    DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   15.61    DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
   15.62 @@ -2076,6 +2114,22 @@
   15.63    "\<lbrakk>(f ---> a) F; cos a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. tan (f x)) ---> tan a) F"
   15.64    by (rule isCont_tendsto_compose [OF isCont_tan])
   15.65  
   15.66 +lemma continuous_tan:
   15.67 +  "continuous F f \<Longrightarrow> cos (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. tan (f x))"
   15.68 +  unfolding continuous_def by (rule tendsto_tan)
   15.69 +
   15.70 +lemma isCont_tan'' [continuous_intros]:
   15.71 +  "continuous (at x) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. tan (f x))"
   15.72 +  unfolding continuous_at by (rule tendsto_tan)
   15.73 +
   15.74 +lemma continuous_within_tan [continuous_intros]:
   15.75 +  "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
   15.76 +  unfolding continuous_within by (rule tendsto_tan)
   15.77 +
   15.78 +lemma continuous_on_tan [continuous_on_intros]:
   15.79 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. cos (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. tan (f x))"
   15.80 +  unfolding continuous_on_def by (auto intro: tendsto_tan)
   15.81 +
   15.82  lemma LIM_cos_div_sin: "(%x. cos(x)/sin(x)) -- pi/2 --> 0"
   15.83    by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
   15.84  
   15.85 @@ -2403,7 +2457,7 @@
   15.86  lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
   15.87    using arctan_eq_iff [of x 0] by simp
   15.88  
   15.89 -lemma isCont_inverse_function2:
   15.90 +lemma isCont_inverse_function2: (* generalize with continuous_on *)
   15.91    fixes f g :: "real \<Rightarrow> real" shows
   15.92    "\<lbrakk>a < x; x < b;
   15.93      \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
   15.94 @@ -2414,7 +2468,7 @@
   15.95  apply (simp_all add: abs_le_iff)
   15.96  done
   15.97  
   15.98 -lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x"
   15.99 +lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
  15.100  apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
  15.101  apply (rule isCont_inverse_function2 [where f=sin])
  15.102  apply (erule (1) arcsin_lt_bounded [THEN conjunct1])
  15.103 @@ -2422,7 +2476,7 @@
  15.104  apply (fast intro: arcsin_sin, simp)
  15.105  done
  15.106  
  15.107 -lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x"
  15.108 +lemma isCont_arccos: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arccos x" (* generalize with continuous_on {-1 .. 1} *)
  15.109  apply (subgoal_tac "isCont arccos (cos (arccos x))", simp)
  15.110  apply (rule isCont_inverse_function2 [where f=cos])
  15.111  apply (erule (1) arccos_lt_bounded [THEN conjunct1])
  15.112 @@ -2439,6 +2493,15 @@
  15.113  apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
  15.114  done
  15.115  
  15.116 +lemma tendsto_arctan [tendsto_intros]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) ---> arctan x) F"
  15.117 +  by (rule isCont_tendsto_compose [OF isCont_arctan])
  15.118 +
  15.119 +lemma continuous_arctan [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. arctan (f x))"
  15.120 +  unfolding continuous_def by (rule tendsto_arctan)
  15.121 +
  15.122 +lemma continuous_on_arctan [continuous_on_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
  15.123 +  unfolding continuous_on_def by (auto intro: tendsto_arctan)
  15.124 +  
  15.125  lemma DERIV_arcsin:
  15.126    "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
  15.127  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])