move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51481ef949192e5d6
parent 51480 3793c3a11378
child 51482 80efd8c49f52
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
src/HOL/Deriv.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/RealVector.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -831,16 +831,7 @@
     1.4  
     1.5  lemma lemma_MVT:
     1.6       "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
     1.7 -proof cases
     1.8 -  assume "a=b" thus ?thesis by simp
     1.9 -next
    1.10 -  assume "a\<noteq>b"
    1.11 -  hence ba: "b-a \<noteq> 0" by arith
    1.12 -  show ?thesis
    1.13 -    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
    1.14 -        simp add: right_diff_distrib,
    1.15 -        simp add: left_diff_distrib)
    1.16 -qed
    1.17 +  by (cases "a = b") (simp_all add: field_simps)
    1.18  
    1.19  theorem MVT:
    1.20    assumes lt:  "a < b"
    1.21 @@ -1090,152 +1081,47 @@
    1.22      by simp
    1.23  qed
    1.24  
    1.25 -subsection {* Continuous injective functions *}
    1.26 -
    1.27 -text{*Dull lemma: an continuous injection on an interval must have a
    1.28 -strict maximum at an end point, not in the middle.*}
    1.29 -
    1.30 -lemma lemma_isCont_inj:
    1.31 -  fixes f :: "real \<Rightarrow> real"
    1.32 -  assumes d: "0 < d"
    1.33 -      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
    1.34 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
    1.35 -  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
    1.36 -proof (rule ccontr)
    1.37 -  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
    1.38 -  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
    1.39 -  show False
    1.40 -  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
    1.41 -    case le
    1.42 -    from d cont all [of "x+d"]
    1.43 -    have flef: "f(x+d) \<le> f x"
    1.44 -     and xlex: "x - d \<le> x"
    1.45 -     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
    1.46 -       by (auto simp add: abs_if)
    1.47 -    from IVT [OF le flef xlex cont']
    1.48 -    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
    1.49 -    moreover
    1.50 -    hence "g(f x') = g (f(x+d))" by simp
    1.51 -    ultimately show False using d inj [of x'] inj [of "x+d"]
    1.52 -      by (simp add: abs_le_iff)
    1.53 -  next
    1.54 -    case ge
    1.55 -    from d cont all [of "x-d"]
    1.56 -    have flef: "f(x-d) \<le> f x"
    1.57 -     and xlex: "x \<le> x+d"
    1.58 -     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
    1.59 -       by (auto simp add: abs_if)
    1.60 -    from IVT2 [OF ge flef xlex cont']
    1.61 -    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
    1.62 -    moreover
    1.63 -    hence "g(f x') = g (f(x-d))" by simp
    1.64 -    ultimately show False using d inj [of x'] inj [of "x-d"]
    1.65 -      by (simp add: abs_le_iff)
    1.66 -  qed
    1.67 -qed
    1.68 -
    1.69 -
    1.70 -text{*Similar version for lower bound.*}
    1.71 -
    1.72 -lemma lemma_isCont_inj2:
    1.73 -  fixes f g :: "real \<Rightarrow> real"
    1.74 -  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
    1.75 -        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
    1.76 -      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
    1.77 -apply (insert lemma_isCont_inj
    1.78 -          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
    1.79 -apply (simp add: linorder_not_le)
    1.80 -done
    1.81 -
    1.82 -text{*Show there's an interval surrounding @{term "f(x)"} in
    1.83 -@{text "f[[x - d, x + d]]"} .*}
    1.84 -
    1.85 -lemma isCont_inj_range:
    1.86 -  fixes f :: "real \<Rightarrow> real"
    1.87 -  assumes d: "0 < d"
    1.88 -      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
    1.89 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
    1.90 -  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
    1.91 -proof -
    1.92 -  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
    1.93 -    by (auto simp add: abs_le_iff)
    1.94 -  from isCont_Lb_Ub [OF this]
    1.95 -  obtain L M
    1.96 -  where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
    1.97 -    and all2 [rule_format]:
    1.98 -           "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
    1.99 -    by auto
   1.100 -  with d have "L \<le> f x & f x \<le> M" by simp
   1.101 -  moreover have "L \<noteq> f x"
   1.102 -  proof -
   1.103 -    from lemma_isCont_inj2 [OF d inj cont]
   1.104 -    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
   1.105 -    thus ?thesis using all1 [of u] by arith
   1.106 -  qed
   1.107 -  moreover have "f x \<noteq> M"
   1.108 -  proof -
   1.109 -    from lemma_isCont_inj [OF d inj cont]
   1.110 -    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
   1.111 -    thus ?thesis using all1 [of u] by arith
   1.112 -  qed
   1.113 -  ultimately have "L < f x & f x < M" by arith
   1.114 -  hence "0 < f x - L" "0 < M - f x" by arith+
   1.115 -  from real_lbound_gt_zero [OF this]
   1.116 -  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
   1.117 -  thus ?thesis
   1.118 -  proof (intro exI conjI)
   1.119 -    show "0<e" using e(1) .
   1.120 -    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
   1.121 -    proof (intro strip)
   1.122 -      fix y::real
   1.123 -      assume "\<bar>y - f x\<bar> \<le> e"
   1.124 -      with e have "L \<le> y \<and> y \<le> M" by arith
   1.125 -      from all2 [OF this]
   1.126 -      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
   1.127 -      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y" 
   1.128 -        by (force simp add: abs_le_iff)
   1.129 -    qed
   1.130 -  qed
   1.131 -qed
   1.132 -
   1.133 -
   1.134  text{*Continuity of inverse function*}
   1.135  
   1.136  lemma isCont_inverse_function:
   1.137    fixes f g :: "real \<Rightarrow> real"
   1.138    assumes d: "0 < d"
   1.139 -      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
   1.140 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
   1.141 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
   1.142 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
   1.143    shows "isCont g (f x)"
   1.144 -proof (simp add: isCont_iff LIM_eq)
   1.145 -  show "\<forall>r. 0 < r \<longrightarrow>
   1.146 -         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
   1.147 -  proof (intro strip)
   1.148 -    fix r::real
   1.149 -    assume r: "0<r"
   1.150 -    from real_lbound_gt_zero [OF r d]
   1.151 -    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
   1.152 -    with inj cont
   1.153 -    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
   1.154 -                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
   1.155 -    from isCont_inj_range [OF e this]
   1.156 -    obtain e' where e': "0 < e'"
   1.157 -        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
   1.158 -          by blast
   1.159 -    show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
   1.160 -    proof (intro exI conjI)
   1.161 -      show "0<e'" using e' .
   1.162 -      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
   1.163 -      proof (intro strip)
   1.164 -        fix z::real
   1.165 -        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
   1.166 -        with e e_lt e_simps all [rule_format, of "f x + z"]
   1.167 -        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
   1.168 -      qed
   1.169 -    qed
   1.170 -  qed
   1.171 +proof -
   1.172 +  let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
   1.173 +
   1.174 +  have f: "continuous_on ?D f"
   1.175 +    using cont by (intro continuous_at_imp_continuous_on ballI) auto
   1.176 +  then have g: "continuous_on (f`?D) g"
   1.177 +    using inj by (intro continuous_on_inv) auto
   1.178 +
   1.179 +  from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
   1.180 +    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
   1.181 +  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
   1.182 +    by (rule continuous_on_subset)
   1.183 +  moreover
   1.184 +  have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
   1.185 +    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
   1.186 +  then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
   1.187 +    by auto
   1.188 +  ultimately
   1.189 +  show ?thesis
   1.190 +    by (simp add: continuous_on_eq_continuous_at)
   1.191  qed
   1.192  
   1.193 +lemma isCont_inverse_function2:
   1.194 +  fixes f g :: "real \<Rightarrow> real" shows
   1.195 +  "\<lbrakk>a < x; x < b;
   1.196 +    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
   1.197 +    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
   1.198 +   \<Longrightarrow> isCont g (f x)"
   1.199 +apply (rule isCont_inverse_function
   1.200 +       [where f=f and d="min (x - a) (b - x)"])
   1.201 +apply (simp_all add: abs_le_iff)
   1.202 +done
   1.203 +
   1.204  text {* Derivative of inverse function *}
   1.205  
   1.206  lemma DERIV_inverse_function:
   1.207 @@ -1285,7 +1171,6 @@
   1.208      using neq by (rule tendsto_inverse)
   1.209  qed
   1.210  
   1.211 -
   1.212  subsection {* Generalized Mean Value Theorem *}
   1.213  
   1.214  theorem GMVT:
   1.215 @@ -1355,21 +1240,6 @@
   1.216        ==> isCont g (f x)"
   1.217  by (rule isCont_inverse_function)
   1.218  
   1.219 -lemma isCont_inv_fun_inv:
   1.220 -  fixes f g :: "real \<Rightarrow> real"
   1.221 -  shows "[| 0 < d;  
   1.222 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   1.223 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   1.224 -       ==> \<exists>e. 0 < e &  
   1.225 -             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
   1.226 -apply (drule isCont_inj_range)
   1.227 -prefer 2 apply (assumption, assumption, auto)
   1.228 -apply (rule_tac x = e in exI, auto)
   1.229 -apply (rotate_tac 2)
   1.230 -apply (drule_tac x = y in spec, auto)
   1.231 -done
   1.232 -
   1.233 -
   1.234  text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
   1.235  lemma LIM_fun_gt_zero:
   1.236       "[| f -- c --> (l::real); 0 < l |]  
     2.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -470,7 +470,7 @@
     2.4    fixes f :: "'a::t2_space => real"
     2.5    fixes A assumes "open A"
     2.6    shows "continuous_on A f <-> continuous_on A (ereal o f)"
     2.7 -  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
     2.8 +  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
     2.9  
    2.10  
    2.11  lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
     3.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -8,14 +8,6 @@
     3.4  imports Convex_Euclidean_Space
     3.5  begin
     3.6  
     3.7 -lemma continuous_on_cong: (* MOVE to Topological_Spaces *)
     3.8 -  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
     3.9 -  unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto
    3.10 -
    3.11 -lemma continuous_on_compose2:
    3.12 -  shows "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
    3.13 -  using continuous_on_compose[of s f g] by (simp add: comp_def)
    3.14 -
    3.15  subsection {* Paths. *}
    3.16  
    3.17  definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
    3.18 @@ -126,7 +118,8 @@
    3.19    have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
    3.20      using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
    3.21    show "continuous_on {0..1} g1" "continuous_on {0..1} g2"
    3.22 -    unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont])
    3.23 +    unfolding g1 g2
    3.24 +    by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
    3.25  next
    3.26    assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
    3.27    have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
    3.28 @@ -689,8 +682,8 @@
    3.29      unfolding xy
    3.30      apply (rule_tac x="f \<circ> g" in exI)
    3.31      unfolding path_defs
    3.32 -    using assms(1)
    3.33 -    apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"])
    3.34 +    apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)])
    3.35 +    apply auto
    3.36      done
    3.37  qed
    3.38  
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -34,6 +34,24 @@
     4.4    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
     4.5    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
     4.6  
     4.7 +lemma Lim_within_open:
     4.8 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
     4.9 +  shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
    4.10 +  by (fact tendsto_within_open)
    4.11 +
    4.12 +lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
    4.13 +  by (fact tendsto_within_subset)
    4.14 +
    4.15 +lemma continuous_on_union:
    4.16 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    4.17 +  by (fact continuous_on_closed_Un)
    4.18 +
    4.19 +lemma continuous_on_cases:
    4.20 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
    4.21 +    \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
    4.22 +    continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
    4.23 +  by (rule continuous_on_If) auto
    4.24 +
    4.25  subsection {* Topological Basis *}
    4.26  
    4.27  context topological_space
    4.28 @@ -1301,10 +1319,6 @@
    4.29  lemma Lim_within_empty: "(f ---> l) (net within {})"
    4.30    unfolding tendsto_def Limits.eventually_within by simp
    4.31  
    4.32 -lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
    4.33 -  unfolding tendsto_def Topological_Spaces.eventually_within
    4.34 -  by (auto elim!: eventually_elim1)
    4.35 -
    4.36  lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
    4.37    shows "(f ---> l) (net within (S \<union> T))"
    4.38    using assms unfolding tendsto_def Limits.eventually_within
    4.39 @@ -1352,16 +1366,6 @@
    4.40    "x \<in> interior S \<Longrightarrow> at x within S = at x"
    4.41    by (simp add: filter_eq_iff eventually_within_interior)
    4.42  
    4.43 -lemma at_within_open:
    4.44 -  "\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x"
    4.45 -  by (simp only: at_within_interior interior_open)
    4.46 -
    4.47 -lemma Lim_within_open:
    4.48 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    4.49 -  assumes"a \<in> S" "open S"
    4.50 -  shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
    4.51 -  using assms by (simp only: at_within_open)
    4.52 -
    4.53  lemma Lim_within_LIMSEQ:
    4.54    fixes a :: "'a::metric_space"
    4.55    assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    4.56 @@ -2552,35 +2556,6 @@
    4.57    thus ?thesis unfolding closed_sequential_limits by fast
    4.58  qed
    4.59  
    4.60 -lemma compact_imp_closed:
    4.61 -  fixes s :: "'a::t2_space set"
    4.62 -  assumes "compact s" shows "closed s"
    4.63 -unfolding closed_def
    4.64 -proof (rule openI)
    4.65 -  fix y assume "y \<in> - s"
    4.66 -  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
    4.67 -  note `compact s`
    4.68 -  moreover have "\<forall>u\<in>?C. open u" by simp
    4.69 -  moreover have "s \<subseteq> \<Union>?C"
    4.70 -  proof
    4.71 -    fix x assume "x \<in> s"
    4.72 -    with `y \<in> - s` have "x \<noteq> y" by clarsimp
    4.73 -    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
    4.74 -      by (rule hausdorff)
    4.75 -    with `x \<in> s` show "x \<in> \<Union>?C"
    4.76 -      unfolding eventually_nhds by auto
    4.77 -  qed
    4.78 -  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
    4.79 -    by (rule compactE)
    4.80 -  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
    4.81 -  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
    4.82 -    by (simp add: eventually_Ball_finite)
    4.83 -  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
    4.84 -    by (auto elim!: eventually_mono [rotated])
    4.85 -  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
    4.86 -    by (simp add: eventually_nhds subset_eq)
    4.87 -qed
    4.88 -
    4.89  lemma compact_imp_bounded:
    4.90    assumes "compact U" shows "bounded U"
    4.91  proof -
    4.92 @@ -2614,20 +2589,6 @@
    4.93    "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
    4.94    unfolding SUP_def by (rule compact_Union) auto
    4.95  
    4.96 -lemma compact_inter_closed [intro]:
    4.97 -  assumes "compact s" and "closed t"
    4.98 -  shows "compact (s \<inter> t)"
    4.99 -proof (rule compactI)
   4.100 -  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
   4.101 -  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
   4.102 -  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
   4.103 -  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
   4.104 -    using `compact s` unfolding compact_eq_heine_borel by auto
   4.105 -  then guess D ..
   4.106 -  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
   4.107 -    by (intro exI[of _ "D - {-t}"]) auto
   4.108 -qed
   4.109 -
   4.110  lemma closed_inter_compact [intro]:
   4.111    assumes "closed s" and "compact t"
   4.112    shows "compact (s \<inter> t)"
   4.113 @@ -3802,19 +3763,11 @@
   4.114  
   4.115  lemmas continuous_on = continuous_on_def -- "legacy theorem name"
   4.116  
   4.117 -lemma continuous_on_eq_continuous_at:
   4.118 -  shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
   4.119 -  by (auto simp add: continuous_on continuous_at Lim_within_open)
   4.120 -
   4.121  lemma continuous_within_subset:
   4.122   "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
   4.123               ==> continuous (at x within t) f"
   4.124    unfolding continuous_within by(metis Lim_within_subset)
   4.125  
   4.126 -lemma continuous_on_subset:
   4.127 -  shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
   4.128 -  unfolding continuous_on by (metis subset_eq Lim_within_subset)
   4.129 -
   4.130  lemma continuous_on_interior:
   4.131    shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
   4.132    by (erule interiorE, drule (1) continuous_on_subset,
   4.133 @@ -4087,70 +4040,18 @@
   4.134  qed
   4.135  
   4.136  lemma continuous_on_open:
   4.137 -  shows "continuous_on s f \<longleftrightarrow>
   4.138 +  "continuous_on s f \<longleftrightarrow>
   4.139          (\<forall>t. openin (subtopology euclidean (f ` s)) t
   4.140              --> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
   4.141 -proof (safe)
   4.142 -  fix t :: "'b set"
   4.143 -  assume 1: "continuous_on s f"
   4.144 -  assume 2: "openin (subtopology euclidean (f ` s)) t"
   4.145 -  from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
   4.146 -    unfolding openin_open by auto
   4.147 -  def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
   4.148 -  have "open U" unfolding U_def by (simp add: open_Union)
   4.149 -  moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
   4.150 -  proof (intro ballI iffI)
   4.151 -    fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
   4.152 -      unfolding U_def t by auto
   4.153 -  next
   4.154 -    fix x assume "x \<in> s" and "f x \<in> t"
   4.155 -    hence "x \<in> s" and "f x \<in> B"
   4.156 -      unfolding t by auto
   4.157 -    with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
   4.158 -      unfolding t continuous_on_topological by metis
   4.159 -    then show "x \<in> U"
   4.160 -      unfolding U_def by auto
   4.161 -  qed
   4.162 -  ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
   4.163 -  then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
   4.164 -    unfolding openin_open by fast
   4.165 -next
   4.166 -  assume "?rhs" show "continuous_on s f"
   4.167 -  unfolding continuous_on_topological
   4.168 -  proof (clarify)
   4.169 -    fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
   4.170 -    have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
   4.171 -      unfolding openin_open using `open B` by auto
   4.172 -    then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
   4.173 -      using `?rhs` by fast
   4.174 -    then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
   4.175 -      unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
   4.176 -  qed
   4.177 -qed
   4.178 +  unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
   4.179 +  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
   4.180  
   4.181  text {* Similarly in terms of closed sets. *}
   4.182  
   4.183  lemma continuous_on_closed:
   4.184    shows "continuous_on s f \<longleftrightarrow>  (\<forall>t. closedin (subtopology euclidean (f ` s)) t  --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
   4.185 -proof
   4.186 -  assume ?lhs
   4.187 -  { fix t
   4.188 -    have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
   4.189 -    have **:"f ` s - (f ` s - (f ` s - t)) = f ` s - t" by auto
   4.190 -    assume as:"closedin (subtopology euclidean (f ` s)) t"
   4.191 -    hence "closedin (subtopology euclidean (f ` s)) (f ` s - (f ` s - t))" unfolding closedin_def topspace_euclidean_subtopology unfolding ** by auto
   4.192 -    hence "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?lhs`[unfolded continuous_on_open, THEN spec[where x="(f ` s) - t"]]
   4.193 -      unfolding openin_closedin_eq topspace_euclidean_subtopology unfolding * by auto  }
   4.194 -  thus ?rhs by auto
   4.195 -next
   4.196 -  assume ?rhs
   4.197 -  { fix t
   4.198 -    have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
   4.199 -    assume as:"openin (subtopology euclidean (f ` s)) t"
   4.200 -    hence "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?rhs`[THEN spec[where x="(f ` s) - t"]]
   4.201 -      unfolding openin_closedin_eq topspace_euclidean_subtopology *[THEN sym] closedin_subtopology by auto }
   4.202 -  thus ?lhs unfolding continuous_on_open by auto
   4.203 -qed
   4.204 +  unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
   4.205 +  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
   4.206  
   4.207  text {* Half-global and completely global cases. *}
   4.208  
   4.209 @@ -4544,38 +4445,6 @@
   4.210    qed (insert D, auto)
   4.211  qed auto
   4.212  
   4.213 -text{* Continuity of inverse function on compact domain. *}
   4.214 -
   4.215 -lemma continuous_on_inv:
   4.216 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
   4.217 -  assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
   4.218 -  shows "continuous_on (f ` s) g"
   4.219 -unfolding continuous_on_topological
   4.220 -proof (clarsimp simp add: assms(3))
   4.221 -  fix x :: 'a and B :: "'a set"
   4.222 -  assume "x \<in> s" and "open B" and "x \<in> B"
   4.223 -  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
   4.224 -    using assms(3) by (auto, metis)
   4.225 -  have "continuous_on (s - B) f"
   4.226 -    using `continuous_on s f` Diff_subset
   4.227 -    by (rule continuous_on_subset)
   4.228 -  moreover have "compact (s - B)"
   4.229 -    using `open B` and `compact s`
   4.230 -    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
   4.231 -  ultimately have "compact (f ` (s - B))"
   4.232 -    by (rule compact_continuous_image)
   4.233 -  hence "closed (f ` (s - B))"
   4.234 -    by (rule compact_imp_closed)
   4.235 -  hence "open (- f ` (s - B))"
   4.236 -    by (rule open_Compl)
   4.237 -  moreover have "f x \<in> - f ` (s - B)"
   4.238 -    using `x \<in> s` and `x \<in> B` by (simp add: 1)
   4.239 -  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
   4.240 -    by (simp add: 1)
   4.241 -  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
   4.242 -    by fast
   4.243 -qed
   4.244 -
   4.245  text {* A uniformly convergent limit of continuous functions is continuous. *}
   4.246  
   4.247  lemma continuous_uniform_limit:
   4.248 @@ -5664,27 +5533,6 @@
   4.249          (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
   4.250    unfolding tendsto_def trivial_limit_eq by auto
   4.251  
   4.252 -lemma continuous_on_union:
   4.253 -  assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
   4.254 -  shows "continuous_on (s \<union> t) f"
   4.255 -  using assms unfolding continuous_on Lim_within_union
   4.256 -  unfolding Lim_topological trivial_limit_within closed_limpt by auto
   4.257 -
   4.258 -lemma continuous_on_cases:
   4.259 -  assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
   4.260 -          "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
   4.261 -  shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
   4.262 -proof-
   4.263 -  let ?h = "(\<lambda>x. if P x then f x else g x)"
   4.264 -  have "\<forall>x\<in>s. f x = (if P x then f x else g x)" using assms(5) by auto
   4.265 -  hence "continuous_on s ?h" using continuous_on_eq[of s f ?h] using assms(3) by auto
   4.266 -  moreover
   4.267 -  have "\<forall>x\<in>t. g x = (if P x then f x else g x)" using assms(5) by auto
   4.268 -  hence "continuous_on t ?h" using continuous_on_eq[of t g ?h] using assms(4) by auto
   4.269 -  ultimately show ?thesis using continuous_on_union[OF assms(1,2), of ?h] by auto
   4.270 -qed
   4.271 -
   4.272 -
   4.273  text{* Some more convenient intermediate-value theorem formulations.             *}
   4.274  
   4.275  lemma connected_ivt_hyperplane:
     5.1 --- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     5.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     5.3 @@ -950,6 +950,8 @@
     5.4  
     5.5  end
     5.6  
     5.7 +instance real :: linear_continuum_topology ..
     5.8 +
     5.9  lemma connectedI_interval:
    5.10    fixes U :: "'a :: linear_continuum_topology set"
    5.11    assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    5.12 @@ -1068,6 +1070,27 @@
    5.13    shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    5.14    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
    5.15  
    5.16 -instance real :: linear_continuum_topology ..
    5.17 +lemma continuous_inj_imp_mono:
    5.18 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    5.19 +  assumes x: "a < x" "x < b"
    5.20 +  assumes cont: "continuous_on {a..b} f"
    5.21 +  assumes inj: "inj_on f {a..b}"
    5.22 +  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
    5.23 +proof -
    5.24 +  note I = inj_on_iff[OF inj]
    5.25 +  { assume "f x < f a" "f x < f b"
    5.26 +    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
    5.27 +      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
    5.28 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
    5.29 +    with x I have False by auto }
    5.30 +  moreover
    5.31 +  { assume "f a < f x" "f b < f x"
    5.32 +    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
    5.33 +      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
    5.34 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
    5.35 +    with x I have False by auto }
    5.36 +  ultimately show ?thesis
    5.37 +    using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
    5.38 +qed
    5.39  
    5.40  end
     6.1 --- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     6.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     6.3 @@ -724,6 +724,9 @@
     6.4    "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
     6.5  unfolding at_def eventually_within eventually_nhds by simp
     6.6  
     6.7 +lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
     6.8 +  unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
     6.9 +
    6.10  lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
    6.11    unfolding trivial_limit_def eventually_at_topological
    6.12    by (safe, case_tac "S = {a}", simp, fast, fast)
    6.13 @@ -869,6 +872,9 @@
    6.14      by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
    6.15  qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
    6.16  
    6.17 +lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
    6.18 +  by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
    6.19 +
    6.20  lemma filterlim_at:
    6.21    "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
    6.22    by (simp add: at_def filterlim_within)
    6.23 @@ -1540,6 +1546,9 @@
    6.24          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    6.25    "f -- a --> L \<equiv> (f ---> L) (at a)"
    6.26  
    6.27 +lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
    6.28 +  unfolding tendsto_def by (simp add: at_within_open)
    6.29 +
    6.30  lemma LIM_const_not_eq[tendsto_intros]:
    6.31    fixes a :: "'a::perfect_space"
    6.32    fixes k L :: "'b::t2_space"
    6.33 @@ -1629,6 +1638,10 @@
    6.34  definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
    6.35    "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
    6.36  
    6.37 +lemma continuous_on_cong [cong]:
    6.38 +  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
    6.39 +  unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
    6.40 +
    6.41  lemma continuous_on_topological:
    6.42    "continuous_on s f \<longleftrightarrow>
    6.43      (\<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)))"
    6.44 @@ -1655,6 +1668,11 @@
    6.45    qed
    6.46  qed
    6.47  
    6.48 +lemma continuous_on_open_vimage:
    6.49 +  "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))"
    6.50 +  unfolding continuous_on_open_invariant
    6.51 +  by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
    6.52 +
    6.53  lemma continuous_on_closed_invariant:
    6.54    "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
    6.55  proof -
    6.56 @@ -1664,6 +1682,36 @@
    6.57      unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric])
    6.58  qed
    6.59  
    6.60 +lemma continuous_on_closed_vimage:
    6.61 +  "closed s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> closed (f -` B \<inter> s))"
    6.62 +  unfolding continuous_on_closed_invariant
    6.63 +  by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
    6.64 +
    6.65 +lemma continuous_on_open_Union:
    6.66 +  "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
    6.67 +  unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
    6.68 +
    6.69 +lemma continuous_on_open_UN:
    6.70 +  "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
    6.71 +  unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
    6.72 +
    6.73 +lemma continuous_on_closed_Un:
    6.74 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    6.75 +  by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
    6.76 +
    6.77 +lemma continuous_on_If:
    6.78 +  assumes closed: "closed s" "closed t" and cont: "continuous_on s f" "continuous_on t g"
    6.79 +    and P: "\<And>x. x \<in> s \<Longrightarrow> \<not> P x \<Longrightarrow> f x = g x" "\<And>x. x \<in> t \<Longrightarrow> P x \<Longrightarrow> f x = g x"
    6.80 +  shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" (is "continuous_on _ ?h")
    6.81 +proof-
    6.82 +  from P have "\<forall>x\<in>s. f x = ?h x" "\<forall>x\<in>t. g x = ?h x"
    6.83 +    by auto
    6.84 +  with cont have "continuous_on s ?h" "continuous_on t ?h"
    6.85 +    by simp_all
    6.86 +  with closed show ?thesis
    6.87 +    by (rule continuous_on_closed_Un)
    6.88 +qed
    6.89 +
    6.90  ML {*
    6.91  
    6.92  structure Continuous_On_Intros = Named_Thms
    6.93 @@ -1686,6 +1734,10 @@
    6.94    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
    6.95    unfolding continuous_on_topological by simp metis
    6.96  
    6.97 +lemma continuous_on_compose2:
    6.98 +  "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
    6.99 +  using continuous_on_compose[of s f g] by (simp add: comp_def)
   6.100 +
   6.101  subsubsection {* Continuity at a point *}
   6.102  
   6.103  definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
   6.104 @@ -1749,6 +1801,12 @@
   6.105  lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
   6.106    by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
   6.107  
   6.108 +lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
   6.109 +  by (simp add: continuous_on_def continuous_at tendsto_within_open)
   6.110 +
   6.111 +lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
   6.112 +  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
   6.113 +
   6.114  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
   6.115    by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
   6.116  
   6.117 @@ -1801,8 +1859,101 @@
   6.118    using assms unfolding ball_simps[symmetric] SUP_def
   6.119    by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
   6.120  
   6.121 +lemma compact_inter_closed [intro]:
   6.122 +  assumes "compact s" and "closed t"
   6.123 +  shows "compact (s \<inter> t)"
   6.124 +proof (rule compactI)
   6.125 +  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
   6.126 +  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
   6.127 +  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
   6.128 +  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
   6.129 +    using `compact s` unfolding compact_eq_heine_borel by auto
   6.130 +  then guess D ..
   6.131 +  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
   6.132 +    by (intro exI[of _ "D - {-t}"]) auto
   6.133 +qed
   6.134 +
   6.135  end
   6.136  
   6.137 +lemma (in t2_space) compact_imp_closed:
   6.138 +  assumes "compact s" shows "closed s"
   6.139 +unfolding closed_def
   6.140 +proof (rule openI)
   6.141 +  fix y assume "y \<in> - s"
   6.142 +  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
   6.143 +  note `compact s`
   6.144 +  moreover have "\<forall>u\<in>?C. open u" by simp
   6.145 +  moreover have "s \<subseteq> \<Union>?C"
   6.146 +  proof
   6.147 +    fix x assume "x \<in> s"
   6.148 +    with `y \<in> - s` have "x \<noteq> y" by clarsimp
   6.149 +    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
   6.150 +      by (rule hausdorff)
   6.151 +    with `x \<in> s` show "x \<in> \<Union>?C"
   6.152 +      unfolding eventually_nhds by auto
   6.153 +  qed
   6.154 +  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
   6.155 +    by (rule compactE)
   6.156 +  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
   6.157 +  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
   6.158 +    by (simp add: eventually_Ball_finite)
   6.159 +  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
   6.160 +    by (auto elim!: eventually_mono [rotated])
   6.161 +  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
   6.162 +    by (simp add: eventually_nhds subset_eq)
   6.163 +qed
   6.164 +
   6.165 +lemma compact_continuous_image:
   6.166 +  assumes f: "continuous_on s f" and s: "compact s"
   6.167 +  shows "compact (f ` s)"
   6.168 +proof (rule compactI)
   6.169 +  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
   6.170 +  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
   6.171 +    unfolding continuous_on_open_invariant by blast
   6.172 +  then guess A unfolding bchoice_iff .. note A = this
   6.173 +  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
   6.174 +    by (fastforce simp add: subset_eq set_eq_iff)+
   6.175 +  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
   6.176 +  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
   6.177 +    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
   6.178 +qed
   6.179 +
   6.180 +lemma continuous_on_inv:
   6.181 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
   6.182 +  assumes "continuous_on s f"  "compact s"  "\<forall>x\<in>s. g (f x) = x"
   6.183 +  shows "continuous_on (f ` s) g"
   6.184 +unfolding continuous_on_topological
   6.185 +proof (clarsimp simp add: assms(3))
   6.186 +  fix x :: 'a and B :: "'a set"
   6.187 +  assume "x \<in> s" and "open B" and "x \<in> B"
   6.188 +  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
   6.189 +    using assms(3) by (auto, metis)
   6.190 +  have "continuous_on (s - B) f"
   6.191 +    using `continuous_on s f` Diff_subset
   6.192 +    by (rule continuous_on_subset)
   6.193 +  moreover have "compact (s - B)"
   6.194 +    using `open B` and `compact s`
   6.195 +    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
   6.196 +  ultimately have "compact (f ` (s - B))"
   6.197 +    by (rule compact_continuous_image)
   6.198 +  hence "closed (f ` (s - B))"
   6.199 +    by (rule compact_imp_closed)
   6.200 +  hence "open (- f ` (s - B))"
   6.201 +    by (rule open_Compl)
   6.202 +  moreover have "f x \<in> - f ` (s - B)"
   6.203 +    using `x \<in> s` and `x \<in> B` by (simp add: 1)
   6.204 +  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
   6.205 +    by (simp add: 1)
   6.206 +  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
   6.207 +    by fast
   6.208 +qed
   6.209 +
   6.210 +lemma continuous_on_inv_into:
   6.211 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
   6.212 +  assumes s: "continuous_on s f" "compact s" and f: "inj_on f s"
   6.213 +  shows "continuous_on (f ` s) (the_inv_into s f)"
   6.214 +  by (rule continuous_on_inv[OF s]) (auto simp: the_inv_into_f_f[OF f])
   6.215 +
   6.216  lemma (in linorder_topology) compact_attains_sup:
   6.217    assumes "compact S" "S \<noteq> {}"
   6.218    shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
   6.219 @@ -1841,21 +1992,6 @@
   6.220      by fastforce
   6.221  qed
   6.222  
   6.223 -lemma compact_continuous_image:
   6.224 -  assumes f: "continuous_on s f" and s: "compact s"
   6.225 -  shows "compact (f ` s)"
   6.226 -proof (rule compactI)
   6.227 -  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
   6.228 -  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
   6.229 -    unfolding continuous_on_open_invariant by blast
   6.230 -  then guess A unfolding bchoice_iff .. note A = this
   6.231 -  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
   6.232 -    by (fastforce simp add: subset_eq set_eq_iff)+
   6.233 -  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
   6.234 -  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
   6.235 -    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
   6.236 -qed
   6.237 -
   6.238  lemma continuous_attains_sup:
   6.239    fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
   6.240    shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
     7.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     7.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     7.3 @@ -2457,17 +2457,6 @@
     7.4  lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
     7.5    using arctan_eq_iff [of x 0] by simp
     7.6  
     7.7 -lemma isCont_inverse_function2: (* generalize with continuous_on *)
     7.8 -  fixes f g :: "real \<Rightarrow> real" shows
     7.9 -  "\<lbrakk>a < x; x < b;
    7.10 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
    7.11 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
    7.12 -   \<Longrightarrow> isCont g (f x)"
    7.13 -apply (rule isCont_inverse_function
    7.14 -       [where f=f and d="min (x - a) (b - x)"])
    7.15 -apply (simp_all add: abs_le_iff)
    7.16 -done
    7.17 -
    7.18  lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
    7.19  apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
    7.20  apply (rule isCont_inverse_function2 [where f=sin])