# HG changeset patch
# User hoelzl
# Date 1363945303 -3600
# Node ID ef949192e5d63e5a9d315667c23b87bdd0d89a8d
# Parent  3793c3a1137838120329243d7a504feabc2a879c
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)

diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -831,16 +831,7 @@
 
 lemma lemma_MVT:
      "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
-proof cases
-  assume "a=b" thus ?thesis by simp
-next
-  assume "a\<noteq>b"
-  hence ba: "b-a \<noteq> 0" by arith
-  show ?thesis
-    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
-        simp add: right_diff_distrib,
-        simp add: left_diff_distrib)
-qed
+  by (cases "a = b") (simp_all add: field_simps)
 
 theorem MVT:
   assumes lt:  "a < b"
@@ -1090,152 +1081,47 @@
     by simp
 qed
 
-subsection {* Continuous injective functions *}
-
-text{*Dull lemma: an continuous injection on an interval must have a
-strict maximum at an end point, not in the middle.*}
-
-lemma lemma_isCont_inj:
-  fixes f :: "real \<Rightarrow> real"
-  assumes d: "0 < d"
-      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
-      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
-  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
-proof (rule ccontr)
-  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
-  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
-  show False
-  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
-    case le
-    from d cont all [of "x+d"]
-    have flef: "f(x+d) \<le> f x"
-     and xlex: "x - d \<le> x"
-     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
-       by (auto simp add: abs_if)
-    from IVT [OF le flef xlex cont']
-    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
-    moreover
-    hence "g(f x') = g (f(x+d))" by simp
-    ultimately show False using d inj [of x'] inj [of "x+d"]
-      by (simp add: abs_le_iff)
-  next
-    case ge
-    from d cont all [of "x-d"]
-    have flef: "f(x-d) \<le> f x"
-     and xlex: "x \<le> x+d"
-     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
-       by (auto simp add: abs_if)
-    from IVT2 [OF ge flef xlex cont']
-    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
-    moreover
-    hence "g(f x') = g (f(x-d))" by simp
-    ultimately show False using d inj [of x'] inj [of "x-d"]
-      by (simp add: abs_le_iff)
-  qed
-qed
-
-
-text{*Similar version for lower bound.*}
-
-lemma lemma_isCont_inj2:
-  fixes f g :: "real \<Rightarrow> real"
-  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
-        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
-      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
-apply (insert lemma_isCont_inj
-          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
-apply (simp add: linorder_not_le)
-done
-
-text{*Show there's an interval surrounding @{term "f(x)"} in
-@{text "f[[x - d, x + d]]"} .*}
-
-lemma isCont_inj_range:
-  fixes f :: "real \<Rightarrow> real"
-  assumes d: "0 < d"
-      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
-      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
-  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
-proof -
-  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
-    by (auto simp add: abs_le_iff)
-  from isCont_Lb_Ub [OF this]
-  obtain L M
-  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"
-    and all2 [rule_format]:
-           "\<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)"
-    by auto
-  with d have "L \<le> f x & f x \<le> M" by simp
-  moreover have "L \<noteq> f x"
-  proof -
-    from lemma_isCont_inj2 [OF d inj cont]
-    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
-    thus ?thesis using all1 [of u] by arith
-  qed
-  moreover have "f x \<noteq> M"
-  proof -
-    from lemma_isCont_inj [OF d inj cont]
-    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
-    thus ?thesis using all1 [of u] by arith
-  qed
-  ultimately have "L < f x & f x < M" by arith
-  hence "0 < f x - L" "0 < M - f x" by arith+
-  from real_lbound_gt_zero [OF this]
-  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
-  thus ?thesis
-  proof (intro exI conjI)
-    show "0<e" using e(1) .
-    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
-    proof (intro strip)
-      fix y::real
-      assume "\<bar>y - f x\<bar> \<le> e"
-      with e have "L \<le> y \<and> y \<le> M" by arith
-      from all2 [OF this]
-      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
-      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y" 
-        by (force simp add: abs_le_iff)
-    qed
-  qed
-qed
-
-
 text{*Continuity of inverse function*}
 
 lemma isCont_inverse_function:
   fixes f g :: "real \<Rightarrow> real"
   assumes d: "0 < d"
-      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
-      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
+      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
+      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
   shows "isCont g (f x)"
-proof (simp add: isCont_iff LIM_eq)
-  show "\<forall>r. 0 < r \<longrightarrow>
-         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
-  proof (intro strip)
-    fix r::real
-    assume r: "0<r"
-    from real_lbound_gt_zero [OF r d]
-    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
-    with inj cont
-    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
-                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
-    from isCont_inj_range [OF e this]
-    obtain e' where e': "0 < e'"
-        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
-          by blast
-    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"
-    proof (intro exI conjI)
-      show "0<e'" using e' .
-      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
-      proof (intro strip)
-        fix z::real
-        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
-        with e e_lt e_simps all [rule_format, of "f x + z"]
-        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
-      qed
-    qed
-  qed
+proof -
+  let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
+
+  have f: "continuous_on ?D f"
+    using cont by (intro continuous_at_imp_continuous_on ballI) auto
+  then have g: "continuous_on (f`?D) g"
+    using inj by (intro continuous_on_inv) auto
+
+  from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
+    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
+  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
+    by (rule continuous_on_subset)
+  moreover
+  have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
+    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
+  then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
+    by auto
+  ultimately
+  show ?thesis
+    by (simp add: continuous_on_eq_continuous_at)
 qed
 
+lemma isCont_inverse_function2:
+  fixes f g :: "real \<Rightarrow> real" shows
+  "\<lbrakk>a < x; x < b;
+    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
+    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
+   \<Longrightarrow> isCont g (f x)"
+apply (rule isCont_inverse_function
+       [where f=f and d="min (x - a) (b - x)"])
+apply (simp_all add: abs_le_iff)
+done
+
 text {* Derivative of inverse function *}
 
 lemma DERIV_inverse_function:
@@ -1285,7 +1171,6 @@
     using neq by (rule tendsto_inverse)
 qed
 
-
 subsection {* Generalized Mean Value Theorem *}
 
 theorem GMVT:
@@ -1355,21 +1240,6 @@
       ==> isCont g (f x)"
 by (rule isCont_inverse_function)
 
-lemma isCont_inv_fun_inv:
-  fixes f g :: "real \<Rightarrow> real"
-  shows "[| 0 < d;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
-       ==> \<exists>e. 0 < e &  
-             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
-apply (drule isCont_inj_range)
-prefer 2 apply (assumption, assumption, auto)
-apply (rule_tac x = e in exI, auto)
-apply (rotate_tac 2)
-apply (drule_tac x = y in spec, auto)
-done
-
-
 text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
 lemma LIM_fun_gt_zero:
      "[| f -- c --> (l::real); 0 < l |]  
diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -470,7 +470,7 @@
   fixes f :: "'a::t2_space => real"
   fixes A assumes "open A"
   shows "continuous_on A f <-> continuous_on A (ereal o f)"
-  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
+  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
 
 
 lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -8,14 +8,6 @@
 imports Convex_Euclidean_Space
 begin
 
-lemma continuous_on_cong: (* MOVE to Topological_Spaces *)
-  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
-  unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto
-
-lemma continuous_on_compose2:
-  shows "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
-  using continuous_on_compose[of s f g] by (simp add: comp_def)
-
 subsection {* Paths. *}
 
 definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
@@ -126,7 +118,8 @@
   have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
     using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
   show "continuous_on {0..1} g1" "continuous_on {0..1} g2"
-    unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont])
+    unfolding g1 g2
+    by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
 next
   assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
   have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
@@ -689,8 +682,8 @@
     unfolding xy
     apply (rule_tac x="f \<circ> g" in exI)
     unfolding path_defs
-    using assms(1)
-    apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"])
+    apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)])
+    apply auto
     done
 qed
 
diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -34,6 +34,24 @@
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
 
+lemma Lim_within_open:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
+  by (fact tendsto_within_open)
+
+lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+  by (fact tendsto_within_subset)
+
+lemma continuous_on_union:
+  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+  by (fact continuous_on_closed_Un)
+
+lemma continuous_on_cases:
+  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
+    \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
+    continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
+  by (rule continuous_on_If) auto
+
 subsection {* Topological Basis *}
 
 context topological_space
@@ -1301,10 +1319,6 @@
 lemma Lim_within_empty: "(f ---> l) (net within {})"
   unfolding tendsto_def Limits.eventually_within by simp
 
-lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
-  unfolding tendsto_def Topological_Spaces.eventually_within
-  by (auto elim!: eventually_elim1)
-
 lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
   shows "(f ---> l) (net within (S \<union> T))"
   using assms unfolding tendsto_def Limits.eventually_within
@@ -1352,16 +1366,6 @@
   "x \<in> interior S \<Longrightarrow> at x within S = at x"
   by (simp add: filter_eq_iff eventually_within_interior)
 
-lemma at_within_open:
-  "\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x"
-  by (simp only: at_within_interior interior_open)
-
-lemma Lim_within_open:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes"a \<in> S" "open S"
-  shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
-  using assms by (simp only: at_within_open)
-
 lemma Lim_within_LIMSEQ:
   fixes a :: "'a::metric_space"
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
@@ -2552,35 +2556,6 @@
   thus ?thesis unfolding closed_sequential_limits by fast
 qed
 
-lemma compact_imp_closed:
-  fixes s :: "'a::t2_space set"
-  assumes "compact s" shows "closed s"
-unfolding closed_def
-proof (rule openI)
-  fix y assume "y \<in> - s"
-  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
-  note `compact s`
-  moreover have "\<forall>u\<in>?C. open u" by simp
-  moreover have "s \<subseteq> \<Union>?C"
-  proof
-    fix x assume "x \<in> s"
-    with `y \<in> - s` have "x \<noteq> y" by clarsimp
-    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
-      by (rule hausdorff)
-    with `x \<in> s` show "x \<in> \<Union>?C"
-      unfolding eventually_nhds by auto
-  qed
-  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
-    by (rule compactE)
-  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
-  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
-    by (simp add: eventually_Ball_finite)
-  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
-    by (auto elim!: eventually_mono [rotated])
-  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
-    by (simp add: eventually_nhds subset_eq)
-qed
-
 lemma compact_imp_bounded:
   assumes "compact U" shows "bounded U"
 proof -
@@ -2614,20 +2589,6 @@
   "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
   unfolding SUP_def by (rule compact_Union) auto
 
-lemma compact_inter_closed [intro]:
-  assumes "compact s" and "closed t"
-  shows "compact (s \<inter> t)"
-proof (rule compactI)
-  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
-  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
-  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
-  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
-    using `compact s` unfolding compact_eq_heine_borel by auto
-  then guess D ..
-  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
-    by (intro exI[of _ "D - {-t}"]) auto
-qed
-
 lemma closed_inter_compact [intro]:
   assumes "closed s" and "compact t"
   shows "compact (s \<inter> t)"
@@ -3802,19 +3763,11 @@
 
 lemmas continuous_on = continuous_on_def -- "legacy theorem name"
 
-lemma continuous_on_eq_continuous_at:
-  shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
-  by (auto simp add: continuous_on continuous_at Lim_within_open)
-
 lemma continuous_within_subset:
  "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
              ==> continuous (at x within t) f"
   unfolding continuous_within by(metis Lim_within_subset)
 
-lemma continuous_on_subset:
-  shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
-  unfolding continuous_on by (metis subset_eq Lim_within_subset)
-
 lemma continuous_on_interior:
   shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
   by (erule interiorE, drule (1) continuous_on_subset,
@@ -4087,70 +4040,18 @@
 qed
 
 lemma continuous_on_open:
-  shows "continuous_on s f \<longleftrightarrow>
+  "continuous_on s f \<longleftrightarrow>
         (\<forall>t. openin (subtopology euclidean (f ` s)) t
             --> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof (safe)
-  fix t :: "'b set"
-  assume 1: "continuous_on s f"
-  assume 2: "openin (subtopology euclidean (f ` s)) t"
-  from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
-    unfolding openin_open by auto
-  def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
-  have "open U" unfolding U_def by (simp add: open_Union)
-  moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
-  proof (intro ballI iffI)
-    fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
-      unfolding U_def t by auto
-  next
-    fix x assume "x \<in> s" and "f x \<in> t"
-    hence "x \<in> s" and "f x \<in> B"
-      unfolding t by auto
-    with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
-      unfolding t continuous_on_topological by metis
-    then show "x \<in> U"
-      unfolding U_def by auto
-  qed
-  ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
-  then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
-    unfolding openin_open by fast
-next
-  assume "?rhs" show "continuous_on s f"
-  unfolding continuous_on_topological
-  proof (clarify)
-    fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
-    have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
-      unfolding openin_open using `open B` by auto
-    then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
-      using `?rhs` by fast
-    then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
-      unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
-  qed
-qed
+  unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
+  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
 text {* Similarly in terms of closed sets. *}
 
 lemma continuous_on_closed:
   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")
-proof
-  assume ?lhs
-  { fix t
-    have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
-    have **:"f ` s - (f ` s - (f ` s - t)) = f ` s - t" by auto
-    assume as:"closedin (subtopology euclidean (f ` s)) t"
-    hence "closedin (subtopology euclidean (f ` s)) (f ` s - (f ` s - t))" unfolding closedin_def topspace_euclidean_subtopology unfolding ** by auto
-    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"]]
-      unfolding openin_closedin_eq topspace_euclidean_subtopology unfolding * by auto  }
-  thus ?rhs by auto
-next
-  assume ?rhs
-  { fix t
-    have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
-    assume as:"openin (subtopology euclidean (f ` s)) t"
-    hence "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?rhs`[THEN spec[where x="(f ` s) - t"]]
-      unfolding openin_closedin_eq topspace_euclidean_subtopology *[THEN sym] closedin_subtopology by auto }
-  thus ?lhs unfolding continuous_on_open by auto
-qed
+  unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
+  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
 text {* Half-global and completely global cases. *}
 
@@ -4544,38 +4445,6 @@
   qed (insert D, auto)
 qed auto
 
-text{* Continuity of inverse function on compact domain. *}
-
-lemma continuous_on_inv:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
-  assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
-  shows "continuous_on (f ` s) g"
-unfolding continuous_on_topological
-proof (clarsimp simp add: assms(3))
-  fix x :: 'a and B :: "'a set"
-  assume "x \<in> s" and "open B" and "x \<in> B"
-  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
-    using assms(3) by (auto, metis)
-  have "continuous_on (s - B) f"
-    using `continuous_on s f` Diff_subset
-    by (rule continuous_on_subset)
-  moreover have "compact (s - B)"
-    using `open B` and `compact s`
-    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
-  ultimately have "compact (f ` (s - B))"
-    by (rule compact_continuous_image)
-  hence "closed (f ` (s - B))"
-    by (rule compact_imp_closed)
-  hence "open (- f ` (s - B))"
-    by (rule open_Compl)
-  moreover have "f x \<in> - f ` (s - B)"
-    using `x \<in> s` and `x \<in> B` by (simp add: 1)
-  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
-    by (simp add: 1)
-  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
-    by fast
-qed
-
 text {* A uniformly convergent limit of continuous functions is continuous. *}
 
 lemma continuous_uniform_limit:
@@ -5664,27 +5533,6 @@
         (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
   unfolding tendsto_def trivial_limit_eq by auto
 
-lemma continuous_on_union:
-  assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
-  shows "continuous_on (s \<union> t) f"
-  using assms unfolding continuous_on Lim_within_union
-  unfolding Lim_topological trivial_limit_within closed_limpt by auto
-
-lemma continuous_on_cases:
-  assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
-          "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
-  shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
-proof-
-  let ?h = "(\<lambda>x. if P x then f x else g x)"
-  have "\<forall>x\<in>s. f x = (if P x then f x else g x)" using assms(5) by auto
-  hence "continuous_on s ?h" using continuous_on_eq[of s f ?h] using assms(3) by auto
-  moreover
-  have "\<forall>x\<in>t. g x = (if P x then f x else g x)" using assms(5) by auto
-  hence "continuous_on t ?h" using continuous_on_eq[of t g ?h] using assms(4) by auto
-  ultimately show ?thesis using continuous_on_union[OF assms(1,2), of ?h] by auto
-qed
-
-
 text{* Some more convenient intermediate-value theorem formulations.             *}
 
 lemma connected_ivt_hyperplane:
diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -950,6 +950,8 @@
 
 end
 
+instance real :: linear_continuum_topology ..
+
 lemma connectedI_interval:
   fixes U :: "'a :: linear_continuum_topology set"
   assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
@@ -1068,6 +1070,27 @@
   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"
   by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
 
-instance real :: linear_continuum_topology ..
+lemma continuous_inj_imp_mono:
+  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  assumes x: "a < x" "x < b"
+  assumes cont: "continuous_on {a..b} f"
+  assumes inj: "inj_on f {a..b}"
+  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
+proof -
+  note I = inj_on_iff[OF inj]
+  { assume "f x < f a" "f x < f b"
+    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"
+      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
+      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+    with x I have False by auto }
+  moreover
+  { assume "f a < f x" "f b < f x"
+    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"
+      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
+      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+    with x I have False by auto }
+  ultimately show ?thesis
+    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)
+qed
 
 end
diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -724,6 +724,9 @@
   "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
 unfolding at_def eventually_within eventually_nhds by simp
 
+lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
+  unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
+
 lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   unfolding trivial_limit_def eventually_at_topological
   by (safe, case_tac "S = {a}", simp, fast, fast)
@@ -869,6 +872,9 @@
     by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
 qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
 
+lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+  by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
+
 lemma filterlim_at:
   "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
   by (simp add: at_def filterlim_within)
@@ -1540,6 +1546,9 @@
         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
   "f -- a --> L \<equiv> (f ---> L) (at a)"
 
+lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
+  unfolding tendsto_def by (simp add: at_within_open)
+
 lemma LIM_const_not_eq[tendsto_intros]:
   fixes a :: "'a::perfect_space"
   fixes k L :: "'b::t2_space"
@@ -1629,6 +1638,10 @@
 definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
   "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
 
+lemma continuous_on_cong [cong]:
+  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
+  unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
+
 lemma continuous_on_topological:
   "continuous_on s f \<longleftrightarrow>
     (\<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)))"
@@ -1655,6 +1668,11 @@
   qed
 qed
 
+lemma continuous_on_open_vimage:
+  "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))"
+  unfolding continuous_on_open_invariant
+  by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+
 lemma continuous_on_closed_invariant:
   "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
 proof -
@@ -1664,6 +1682,36 @@
     unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric])
 qed
 
+lemma continuous_on_closed_vimage:
+  "closed s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> closed (f -` B \<inter> s))"
+  unfolding continuous_on_closed_invariant
+  by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+
+lemma continuous_on_open_Union:
+  "(\<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"
+  unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
+
+lemma continuous_on_open_UN:
+  "(\<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"
+  unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
+
+lemma continuous_on_closed_Un:
+  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+  by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
+
+lemma continuous_on_If:
+  assumes closed: "closed s" "closed t" and cont: "continuous_on s f" "continuous_on t g"
+    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"
+  shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" (is "continuous_on _ ?h")
+proof-
+  from P have "\<forall>x\<in>s. f x = ?h x" "\<forall>x\<in>t. g x = ?h x"
+    by auto
+  with cont have "continuous_on s ?h" "continuous_on t ?h"
+    by simp_all
+  with closed show ?thesis
+    by (rule continuous_on_closed_Un)
+qed
+
 ML {*
 
 structure Continuous_On_Intros = Named_Thms
@@ -1686,6 +1734,10 @@
   "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
   unfolding continuous_on_topological by simp metis
 
+lemma continuous_on_compose2:
+  "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
+  using continuous_on_compose[of s f g] by (simp add: comp_def)
+
 subsubsection {* Continuity at a point *}
 
 definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
@@ -1749,6 +1801,12 @@
 lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
 
+lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
+  by (simp add: continuous_on_def continuous_at tendsto_within_open)
+
+lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
+  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
+
 lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
   by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
 
@@ -1801,8 +1859,101 @@
   using assms unfolding ball_simps[symmetric] SUP_def
   by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
 
+lemma compact_inter_closed [intro]:
+  assumes "compact s" and "closed t"
+  shows "compact (s \<inter> t)"
+proof (rule compactI)
+  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
+  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
+  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
+  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
+    using `compact s` unfolding compact_eq_heine_borel by auto
+  then guess D ..
+  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
+    by (intro exI[of _ "D - {-t}"]) auto
+qed
+
 end
 
+lemma (in t2_space) compact_imp_closed:
+  assumes "compact s" shows "closed s"
+unfolding closed_def
+proof (rule openI)
+  fix y assume "y \<in> - s"
+  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
+  note `compact s`
+  moreover have "\<forall>u\<in>?C. open u" by simp
+  moreover have "s \<subseteq> \<Union>?C"
+  proof
+    fix x assume "x \<in> s"
+    with `y \<in> - s` have "x \<noteq> y" by clarsimp
+    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
+      by (rule hausdorff)
+    with `x \<in> s` show "x \<in> \<Union>?C"
+      unfolding eventually_nhds by auto
+  qed
+  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
+    by (rule compactE)
+  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
+  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
+    by (simp add: eventually_Ball_finite)
+  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
+    by (auto elim!: eventually_mono [rotated])
+  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
+    by (simp add: eventually_nhds subset_eq)
+qed
+
+lemma compact_continuous_image:
+  assumes f: "continuous_on s f" and s: "compact s"
+  shows "compact (f ` s)"
+proof (rule compactI)
+  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
+  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
+    unfolding continuous_on_open_invariant by blast
+  then guess A unfolding bchoice_iff .. note A = this
+  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
+    by (fastforce simp add: subset_eq set_eq_iff)+
+  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
+  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
+    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
+qed
+
+lemma continuous_on_inv:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+  assumes "continuous_on s f"  "compact s"  "\<forall>x\<in>s. g (f x) = x"
+  shows "continuous_on (f ` s) g"
+unfolding continuous_on_topological
+proof (clarsimp simp add: assms(3))
+  fix x :: 'a and B :: "'a set"
+  assume "x \<in> s" and "open B" and "x \<in> B"
+  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
+    using assms(3) by (auto, metis)
+  have "continuous_on (s - B) f"
+    using `continuous_on s f` Diff_subset
+    by (rule continuous_on_subset)
+  moreover have "compact (s - B)"
+    using `open B` and `compact s`
+    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
+  ultimately have "compact (f ` (s - B))"
+    by (rule compact_continuous_image)
+  hence "closed (f ` (s - B))"
+    by (rule compact_imp_closed)
+  hence "open (- f ` (s - B))"
+    by (rule open_Compl)
+  moreover have "f x \<in> - f ` (s - B)"
+    using `x \<in> s` and `x \<in> B` by (simp add: 1)
+  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
+    by (simp add: 1)
+  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
+    by fast
+qed
+
+lemma continuous_on_inv_into:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+  assumes s: "continuous_on s f" "compact s" and f: "inj_on f s"
+  shows "continuous_on (f ` s) (the_inv_into s f)"
+  by (rule continuous_on_inv[OF s]) (auto simp: the_inv_into_f_f[OF f])
+
 lemma (in linorder_topology) compact_attains_sup:
   assumes "compact S" "S \<noteq> {}"
   shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
@@ -1841,21 +1992,6 @@
     by fastforce
 qed
 
-lemma compact_continuous_image:
-  assumes f: "continuous_on s f" and s: "compact s"
-  shows "compact (f ` s)"
-proof (rule compactI)
-  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
-  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
-    unfolding continuous_on_open_invariant by blast
-  then guess A unfolding bchoice_iff .. note A = this
-  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
-    by (fastforce simp add: subset_eq set_eq_iff)+
-  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
-  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
-    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
-qed
-
 lemma continuous_attains_sup:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
   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)"
diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -2457,17 +2457,6 @@
 lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
   using arctan_eq_iff [of x 0] by simp
 
-lemma isCont_inverse_function2: (* generalize with continuous_on *)
-  fixes f g :: "real \<Rightarrow> real" shows
-  "\<lbrakk>a < x; x < b;
-    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
-    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
-   \<Longrightarrow> isCont g (f x)"
-apply (rule isCont_inverse_function
-       [where f=f and d="min (x - a) (b - x)"])
-apply (simp_all add: abs_le_iff)
-done
-
 lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
 apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
 apply (rule isCont_inverse_function2 [where f=sin])