# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1444736528 -3600
# Node ID d53db136e8fda950c9a359336639bd452bf45952
# Parent  fb95d06fb21f9849c01ae9742febcfcb2a5593aa
new material on path_component_sets, inside, outside, etc. And more default simprules

diff -r fb95d06fb21f -r d53db136e8fd NEWS
--- a/NEWS	Tue Oct 13 09:21:21 2015 +0200
+++ b/NEWS	Tue Oct 13 12:42:08 2015 +0100
@@ -344,7 +344,7 @@
   - Always generate "case_transfer" theorem.
 
 * Transfer:
-  - new methods for interactive debugging of 'transfer' and 
+  - new methods for interactive debugging of 'transfer' and
     'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
     'transfer_prover_start' and 'transfer_prover_end'.
 
@@ -408,8 +408,11 @@
     less_eq_multiset_def
     INCOMPATIBILITY
 
-* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem,
-    ported from HOL Light
+* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's
+integral theorem, ported from HOL Light
+
+* Multivariate_Analysis: Added topological concepts such as connected components
+and the inside or outside of a set.
 
 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
 command. Minor INCOMPATIBILITY, use 'function' instead.
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Library/Convex.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -43,7 +43,7 @@
     unfolding convex_def by auto
 qed (auto simp: convex_def)
 
-lemma mem_convex:
+lemma convexD_alt:
   assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
   using assms unfolding convex_alt by auto
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -1259,7 +1259,7 @@
     shows "midpoint x y \<in> convex hull s"
 proof -
   have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \<in> convex hull s"
-    apply (rule mem_convex)
+    apply (rule convexD_alt)
     using assms
     apply (auto simp: convex_convex_hull)
     done
@@ -1649,7 +1649,7 @@
     apply (simp add: segment_convex_hull)
     apply (rule convex_hull_subset)
     using assms
-    apply (auto simp: hull_inc c' Convex.mem_convex)
+    apply (auto simp: hull_inc c' Convex.convexD_alt)
     done
 qed
 
@@ -1666,7 +1666,7 @@
     apply (simp_all add: segment_convex_hull)
     apply (rule_tac [!] convex_hull_subset)
     using assms
-    apply (auto simp: hull_inc c' Convex.mem_convex)
+    apply (auto simp: hull_inc c' Convex.convexD_alt)
     done
   show ?thesis
     apply (rule path_integral_unique)
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -522,9 +522,6 @@
   proof (rule complex_taylor [of "closed_segment 0 z" n 
                                  "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" 
                                  "exp\<bar>Im z\<bar>" 0 z,  simplified])
-  show "convex (closed_segment 0 z)"
-    by (rule convex_segment [of 0 z])
-  next
     fix k x
     show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
             (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
@@ -537,13 +534,6 @@
     assume "x \<in> closed_segment 0 z"
     then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
-  next
-    show "0 \<in> closed_segment 0 z"
-      by (auto simp: closed_segment_def)
-  next
-    show "z \<in> closed_segment 0 z"
-      apply (simp add: closed_segment_def scaleR_conv_of_real)
-      using of_real_1 zero_le_one by blast
   qed
   have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
             = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
@@ -565,9 +555,6 @@
            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
 simplified])
-  show "convex (closed_segment 0 z)"
-    by (rule convex_segment [of 0 z])
-  next
     fix k x
     assume "x \<in> closed_segment 0 z" "k \<le> n"
     show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
@@ -581,13 +568,6 @@
     assume "x \<in> closed_segment 0 z"
     then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
-  next
-    show "0 \<in> closed_segment 0 z"
-      by (auto simp: closed_segment_def)
-  next
-    show "z \<in> closed_segment 0 z"
-      apply (simp add: closed_segment_def scaleR_conv_of_real)
-      using of_real_1 zero_le_one by blast
   qed
   have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
             = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -1305,7 +1305,7 @@
 
 lemma connectedD:
   "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
-  by (metis connected_def)
+  by (rule Topological_Spaces.topological_space_class.connectedD)
 
 lemma convex_connected:
   fixes s :: "'a::real_normed_vector set"
@@ -1332,10 +1332,8 @@
   ultimately show False by auto
 qed
 
-text \<open>One rather trivial consequence.\<close>
-
-lemma connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
-  by(simp add: convex_connected convex_UNIV)
+corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
+  by(simp add: convex_connected)
 
 text \<open>Balls, being convex, are connected.\<close>
 
@@ -3318,7 +3316,7 @@
   moreover have c: "c \<in> S"
     using assms rel_interior_subset by auto
   moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
-    using mem_convex[of S x c e]
+    using convexD_alt[of S x c e]
     apply (simp add: algebra_simps)
     using assms
     apply auto
@@ -3920,7 +3918,7 @@
           "0 \<le> c \<and> c \<le> 1" "u \<in> s" "finite t" "t \<subseteq> s" "card t \<le> n"  "v \<in> convex hull t"
           by auto
         moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u t"
-          apply (rule mem_convex)
+          apply (rule convexD_alt)
           using obt(2) and convex_convex_hull and hull_subset[of "insert u t" convex]
           using obt(7) and hull_mono[of t "insert u t"]
           apply auto
@@ -4263,7 +4261,7 @@
     using closer_point_lemma[of a x y] by auto
   let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y"
   have "?z \<in> s"
-    using mem_convex[OF assms(1,3,4), of u] using u by auto
+    using convexD_alt[OF assms(1,3,4), of u] using u by auto
   then show False
     using assms(5)[THEN bspec[where x="?z"]] and u(3)
     by (auto simp add: dist_commute algebra_simps)
@@ -5486,7 +5484,7 @@
       by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
     with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
     with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
-      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule mem_convex)
+      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
     then show "y \<in> s" using \<open>u < 1\<close>
       by simp
   qed
@@ -6345,10 +6343,15 @@
     done
 qed
 
-lemma convex_segment: "convex (closed_segment a b)"
+lemma convex_segment [iff]: "convex (closed_segment a b)"
   unfolding segment_convex_hull by(rule convex_convex_hull)
 
-lemma ends_in_segment: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
+lemma connected_segment [iff]:
+  fixes x :: "'a :: real_normed_vector"
+  shows "connected (closed_segment x y)"
+  by (simp add: convex_connected)
+
+lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
   unfolding segment_convex_hull
   apply (rule_tac[!] hull_subset[unfolded subset_eq, rule_format])
   apply auto
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -942,6 +942,9 @@
 definition "path_component s x y \<longleftrightarrow>
   (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
 
+abbreviation
+   "path_component_set s x \<equiv> Collect (path_component s x)"
+
 lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def
 
 lemma path_component_mem:
@@ -972,8 +975,7 @@
   done
 
 lemma path_component_trans:
-  assumes "path_component s x y"
-    and "path_component s y z"
+  assumes "path_component s x y" and "path_component s y z"
   shows "path_component s x z"
   using assms
   unfolding path_component_def
@@ -985,23 +987,36 @@
 lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
   unfolding path_component_def by auto
 
+lemma path_connected_linepath:
+    fixes s :: "'a::real_normed_vector set"
+    shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
+  apply (simp add: path_component_def)
+  apply (rule_tac x="linepath a b" in exI, auto)
+  done
+
 
 text \<open>Can also consider it as a set, as the name suggests.\<close>
 
 lemma path_component_set:
-  "{y. path_component s x y} =
+  "path_component_set s x =
     {y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)}"
-  unfolding mem_Collect_eq path_component_def
-  apply auto
-  done
+  by (auto simp: path_component_def)
 
-lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
+lemma path_component_subset: "path_component_set s x \<subseteq> s"
   by (auto simp add: path_component_mem(2))
 
-lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s"
+lemma path_component_eq_empty: "path_component_set s x = {} \<longleftrightarrow> x \<notin> s"
   using path_component_mem path_component_refl_eq
     by fastforce
 
+lemma path_component_mono:
+     "s \<subseteq> t \<Longrightarrow> (path_component_set s x) \<subseteq> (path_component_set t x)"
+  by (simp add: Collect_mono path_component_of_subset)
+
+lemma path_component_eq:
+   "y \<in> path_component_set s x \<Longrightarrow> path_component_set s y = path_component_set s x"
+by (metis (no_types, lifting) Collect_cong mem_Collect_eq path_component_sym path_component_trans)
+
 subsection \<open>Path connectedness of a space\<close>
 
 definition "path_connected s \<longleftrightarrow>
@@ -1010,10 +1025,13 @@
 lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
   unfolding path_connected_def path_component_def by auto
 
-lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)"
-  unfolding path_connected_component path_component_subset
-  apply auto
-  using path_component_mem(2) by blast
+lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. path_component_set s x = s)"
+  unfolding path_connected_component path_component_subset 
+  using path_component_mem by blast
+
+lemma path_component_maximal:
+     "\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
+  by (metis path_component_mono path_connected_component_set)
 
 subsection \<open>Some useful lemmas about path-connectedness\<close>
 
@@ -1069,11 +1087,11 @@
 lemma open_path_component:
   fixes s :: "'a::real_normed_vector set"
   assumes "open s"
-  shows "open {y. path_component s x y}"
+  shows "open (path_component_set s x)"
   unfolding open_contains_ball
 proof
   fix y
-  assume as: "y \<in> {y. path_component s x y}"
+  assume as: "y \<in> path_component_set s x"
   then have "y \<in> s"
     apply -
     apply (rule path_component_mem(2))
@@ -1083,7 +1101,7 @@
   then obtain e where e: "e > 0" "ball y e \<subseteq> s"
     using assms[unfolded open_contains_ball]
     by auto
-  show "\<exists>e > 0. ball y e \<subseteq> {y. path_component s x y}"
+  show "\<exists>e > 0. ball y e \<subseteq> path_component_set s x"
     apply (rule_tac x=e in exI)
     apply (rule,rule \<open>e>0\<close>)
     apply rule
@@ -1105,15 +1123,15 @@
 lemma open_non_path_component:
   fixes s :: "'a::real_normed_vector set"
   assumes "open s"
-  shows "open (s - {y. path_component s x y})"
+  shows "open (s - path_component_set s x)"
   unfolding open_contains_ball
 proof
   fix y
-  assume as: "y \<in> s - {y. path_component s x y}"
+  assume as: "y \<in> s - path_component_set s x"
   then obtain e where e: "e > 0" "ball y e \<subseteq> s"
     using assms [unfolded open_contains_ball]
     by auto
-  show "\<exists>e>0. ball y e \<subseteq> s - {y. path_component s x y}"
+  show "\<exists>e>0. ball y e \<subseteq> s - path_component_set s x"
     apply (rule_tac x=e in exI)
     apply rule
     apply (rule \<open>e>0\<close>)
@@ -1122,8 +1140,8 @@
     defer
   proof (rule ccontr)
     fix z
-    assume "z \<in> ball y e" "\<not> z \<notin> {y. path_component s x y}"
-    then have "y \<in> {y. path_component s x y}"
+    assume "z \<in> ball y e" "\<not> z \<notin> path_component_set s x"
+    then have "y \<in> path_component_set s x"
       unfolding not_not mem_Collect_eq using \<open>e>0\<close>
       apply -
       apply (rule path_component_trans, assumption)
@@ -1145,17 +1163,17 @@
 proof (rule, rule, rule path_component_subset, rule)
   fix x y
   assume "x \<in> s" and "y \<in> s"
-  show "y \<in> {y. path_component s x y}"
+  show "y \<in> path_component_set s x"
   proof (rule ccontr)
     assume "\<not> ?thesis"
-    moreover have "{y. path_component s x y} \<inter> s \<noteq> {}"
+    moreover have "path_component_set s x \<inter> s \<noteq> {}"
       using \<open>x \<in> s\<close> path_component_eq_empty path_component_subset[of s x]
       by auto
     ultimately
     show False
       using \<open>y \<in> s\<close> open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
       using assms(2)[unfolded connected_def not_ex, rule_format,
-        of"{y. path_component s x y}" "s - {y. path_component s x y}"]
+        of "path_component_set s x" "s - path_component_set s x"]
       by auto
   qed
 qed
@@ -1239,12 +1257,91 @@
     by (rule path_component_trans)
 qed
 
+lemma path_component_path_image_pathstart:
+  assumes p: "path p" and x: "x \<in> path_image p"
+  shows "path_component (path_image p) (pathstart p) x"
+using x
+proof (clarsimp simp add: path_image_def)
+  fix y
+  assume "x = p y" and y: "0 \<le> y" "y \<le> 1"
+  show "path_component (p ` {0..1}) (pathstart p) (p y)"
+  proof (cases "y=0")
+    case True then show ?thesis
+      by (simp add: path_component_refl_eq pathstart_def)
+  next
+    case False have "continuous_on {0..1} (p o (op*y))"
+      apply (rule continuous_intros)+
+      using p [unfolded path_def] y
+      apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
+      done
+    then have "path (\<lambda>u. p (y * u))"
+      by (simp add: path_def)
+    then show ?thesis
+      apply (simp add: path_component_def)
+      apply (rule_tac x = "\<lambda>u. p (y * u)" in exI)
+      apply (intro conjI)
+      using y False
+      apply (auto simp: mult_le_one pathstart_def pathfinish_def path_image_def)
+      done
+  qed
+qed
+
+lemma path_connected_path_image: "path p \<Longrightarrow> path_connected(path_image p)"
+  unfolding path_connected_component
+  by (meson path_component_path_image_pathstart path_component_sym path_component_trans)
+
+lemma path_connected_path_component:
+   "path_connected (path_component_set s x)"
+proof -
+  { fix y z
+    assume pa: "path_component s x y" "path_component s x z"
+    then have pae: "path_component_set s x = path_component_set s y"
+      using path_component_eq by auto
+    have yz: "path_component s y z"
+      using pa path_component_sym path_component_trans by blast
+    then have "\<exists>g. path g \<and> path_image g \<subseteq> path_component_set s x \<and> pathstart g = y \<and> pathfinish g = z"
+      apply (simp add: path_component_def, clarify)
+      apply (rule_tac x=g in exI)
+      by (simp add: pae path_component_maximal path_connected_path_image pathstart_in_path_image)
+  }
+  then show ?thesis
+    by (simp add: path_connected_def)
+qed
+
+lemma path_component: "path_component s x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t)"
+  apply (intro iffI)
+  apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
+  using path_component_of_subset path_connected_component by blast
+
+lemma path_component_path_component [simp]:
+   "path_component_set (path_component_set s x) x = path_component_set s x"
+proof (cases "x \<in> s")
+  case True show ?thesis
+    apply (rule subset_antisym)
+    apply (simp add: path_component_subset)
+    by (simp add: True path_component_maximal path_component_refl path_connected_path_component)
+next
+  case False then show ?thesis
+    by (metis False empty_iff path_component_eq_empty)
+qed
+
+lemma path_component_subset_connected_component:
+   "(path_component_set s x) \<subseteq> (connected_component_set s x)"
+proof (cases "x \<in> s")
+  case True show ?thesis
+    apply (rule connected_component_maximal)
+    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
+    done
+next
+  case False then show ?thesis
+    using path_component_eq_empty by auto
+qed
 
 subsection \<open>Sphere is path-connected\<close>
 
 lemma path_connected_punctured_universe:
   assumes "2 \<le> DIM('a::euclidean_space)"
-  shows "path_connected ((UNIV::'a set) - {a})"
+  shows "path_connected (- {a::'a})"
 proof -
   let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}"
   let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}"
@@ -1287,7 +1384,7 @@
   also have "\<dots> = {x. x \<noteq> a}"
     unfolding euclidean_eq_iff [where 'a='a]
     by (simp add: Bex_def)
-  also have "\<dots> = UNIV - {a}"
+  also have "\<dots> = - {a}"
     by auto
   finally show ?thesis .
 qed
@@ -1316,7 +1413,7 @@
     using r
     apply (auto simp add: scaleR_right_diff_distrib)
     done
-  have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})"
+  have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (- {0})"
     apply (rule set_eqI)
     apply rule
     unfolding image_iff
@@ -1324,7 +1421,7 @@
     unfolding mem_Collect_eq
     apply (auto split: split_if_asm)
     done
-  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
+  have "continuous_on (- {0}) (\<lambda>x::'a. 1 / norm x)"
     by (auto intro!: continuous_intros)
   then show ?thesis
     unfolding * **
@@ -1332,8 +1429,630 @@
     by (auto intro!: path_connected_continuous_image continuous_intros)
 qed
 
-lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}"
+corollary connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x - a) = r}"
   using path_connected_sphere path_connected_imp_connected
   by auto
 
+corollary path_connected_complement_bounded_convex:
+    fixes s :: "'a :: euclidean_space set"
+    assumes "bounded s" "convex s" and 2: "2 \<le> DIM('a)"
+    shows "path_connected (- s)"
+proof (cases "s={}")
+  case True then show ?thesis
+    using convex_imp_path_connected by auto
+next
+  case False
+  then obtain a where "a \<in> s" by auto
+  { fix x y assume "x \<notin> s" "y \<notin> s"
+    then have "x \<noteq> a" "y \<noteq> a" using `a \<in> s` by auto
+    then have bxy: "bounded(insert x (insert y s))"
+      by (simp add: `bounded s`)
+    then obtain B::real where B: "0 < B" and Bx: "norm (a - x) < B" and By: "norm (a - y) < B"
+                          and "s \<subseteq> ball a B"
+      using bounded_subset_ballD [OF bxy, of a] by (auto simp: dist_norm)
+    def C == "B / norm(x - a)"
+    { fix u
+      assume u: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + C *\<^sub>R (x - a)) \<in> s" and "0 \<le> u" "u \<le> 1"
+      have CC: "1 \<le> 1 + (C - 1) * u"
+        using `x \<noteq> a` `0 \<le> u`
+        apply (simp add: C_def divide_simps norm_minus_commute)
+        by (metis Bx diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
+      have *: "\<And>v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)"
+        by (simp add: algebra_simps)
+      have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) =
+            (1 + (u / (1 + C * u - u))) *\<^sub>R a + ((1 / (1 + C * u - u)) + (C * u / (1 + C * u - u))) *\<^sub>R x"
+        by (simp add: algebra_simps)
+      also have "... = (1 + (u / (1 + C * u - u))) *\<^sub>R a + (1 + (u / (1 + C * u - u))) *\<^sub>R x"
+        using CC by (simp add: field_simps)
+      also have "... = x + (1 + (u / (1 + C * u - u))) *\<^sub>R a + (u / (1 + C * u - u)) *\<^sub>R x"
+        by (simp add: algebra_simps)
+      also have "... = x + ((1 / (1 + C * u - u)) *\<^sub>R a +
+              ((u / (1 + C * u - u)) *\<^sub>R x + (C * u / (1 + C * u - u)) *\<^sub>R a))"
+        using CC by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
+      finally have xeq: "(1 - 1 / (1 + (C - 1) * u)) *\<^sub>R a + (1 / (1 + (C - 1) * u)) *\<^sub>R (a + (1 + (C - 1) * u) *\<^sub>R (x - a)) = x"
+        by (simp add: algebra_simps)
+      have False
+        using `convex s`
+        apply (simp add: convex_alt)
+        apply (drule_tac x=a in bspec)
+         apply (rule  `a \<in> s`)
+        apply (drule_tac x="a + (1 + (C - 1) * u) *\<^sub>R (x - a)" in bspec)
+         using u apply (simp add: *)
+        apply (drule_tac x="1 / (1 + (C - 1) * u)" in spec)
+        using `x \<noteq> a` `x \<notin> s` `0 \<le> u` CC
+        apply (auto simp: xeq)
+        done
+    }
+    then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))"
+      by (force simp: closed_segment_def intro!: path_connected_linepath)
+    def D == "B / norm(y - a)"  --{*massive duplication with the proof above*}
+    { fix u
+      assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \<in> s" and "0 \<le> u" "u \<le> 1"
+      have DD: "1 \<le> 1 + (D - 1) * u"
+        using `y \<noteq> a` `0 \<le> u`
+        apply (simp add: D_def divide_simps norm_minus_commute)
+        by (metis By diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
+      have *: "\<And>v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)"
+        by (simp add: algebra_simps)
+      have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) =
+            (1 + (u / (1 + D * u - u))) *\<^sub>R a + ((1 / (1 + D * u - u)) + (D * u / (1 + D * u - u))) *\<^sub>R y"
+        by (simp add: algebra_simps)
+      also have "... = (1 + (u / (1 + D * u - u))) *\<^sub>R a + (1 + (u / (1 + D * u - u))) *\<^sub>R y"
+        using DD by (simp add: field_simps)
+      also have "... = y + (1 + (u / (1 + D * u - u))) *\<^sub>R a + (u / (1 + D * u - u)) *\<^sub>R y"
+        by (simp add: algebra_simps)
+      also have "... = y + ((1 / (1 + D * u - u)) *\<^sub>R a +
+              ((u / (1 + D * u - u)) *\<^sub>R y + (D * u / (1 + D * u - u)) *\<^sub>R a))"
+        using DD by (simp add: field_simps) (simp add: add_divide_distrib scaleR_add_left)
+      finally have xeq: "(1 - 1 / (1 + (D - 1) * u)) *\<^sub>R a + (1 / (1 + (D - 1) * u)) *\<^sub>R (a + (1 + (D - 1) * u) *\<^sub>R (y - a)) = y"
+        by (simp add: algebra_simps)
+      have False
+        using `convex s`
+        apply (simp add: convex_alt)
+        apply (drule_tac x=a in bspec)
+         apply (rule  `a \<in> s`)
+        apply (drule_tac x="a + (1 + (D - 1) * u) *\<^sub>R (y - a)" in bspec)
+         using u apply (simp add: *)
+        apply (drule_tac x="1 / (1 + (D - 1) * u)" in spec)
+        using `y \<noteq> a` `y \<notin> s` `0 \<le> u` DD
+        apply (auto simp: xeq)
+        done
+    }
+    then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))"
+      by (force simp: closed_segment_def intro!: path_connected_linepath)
+    have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))"
+      apply (rule path_component_of_subset [of "{x. norm(x - a) = B}"])
+       using `s \<subseteq> ball a B`
+       apply (force simp: ball_def dist_norm norm_minus_commute)
+      apply (rule path_connected_sphere [OF 2, of a B, simplified path_connected_component, rule_format])
+      using `x \<noteq> a`  using `y \<noteq> a`  B apply (auto simp: C_def D_def)
+      done
+    have "path_component (- s) x y"
+      by (metis path_component_trans path_component_sym pcx pdy pyx)
+  }
+  then show ?thesis
+    by (auto simp: path_connected_component)
+qed
+
+
+lemma connected_complement_bounded_convex:
+    fixes s :: "'a :: euclidean_space set"
+    assumes "bounded s" "convex s" "2 \<le> DIM('a)"
+      shows  "connected (- s)"
+  using path_connected_complement_bounded_convex [OF assms] path_connected_imp_connected by blast
+
+lemma connected_diff_ball:
+    fixes s :: "'a :: euclidean_space set"
+    assumes "connected s" "cball a r \<subseteq> s" "2 \<le> DIM('a)"
+      shows "connected (s - ball a r)"
+  apply (rule connected_diff_open_from_closed [OF ball_subset_cball])
+  using assms connected_sphere
+  apply (auto simp: cball_diff_eq_sphere dist_norm)
+  done
+
+subsection\<open>Relations between components and path components\<close>
+
+lemma open_connected_component:
+  fixes s :: "'a::real_normed_vector set"
+  shows "open s \<Longrightarrow> open (connected_component_set s x)"
+    apply (simp add: open_contains_ball, clarify)
+    apply (rename_tac y)
+    apply (drule_tac x=y in bspec)
+     apply (simp add: connected_component_in, clarify)
+    apply (rule_tac x=e in exI)
+    by (metis mem_Collect_eq connected_component_eq connected_component_maximal centre_in_ball connected_ball)
+
+corollary open_components:
+    fixes s :: "'a::real_normed_vector set"
+    shows "\<lbrakk>open u; s \<in> components u\<rbrakk> \<Longrightarrow> open s"
+  by (simp add: components_iff) (metis open_connected_component)
+
+lemma in_closure_connected_component:
+  fixes s :: "'a::real_normed_vector set"
+  assumes x: "x \<in> s" and s: "open s"
+  shows "x \<in> closure (connected_component_set s y) \<longleftrightarrow>  x \<in> connected_component_set s y"
+proof -
+  { assume "x \<in> closure (connected_component_set s y)"
+    moreover have "x \<in> connected_component_set s x"
+      using x by simp
+    ultimately have "x \<in> connected_component_set s y"
+      using s by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component)
+  }
+  then show ?thesis
+    by (auto simp: closure_def)
+qed
+
+subsection\<open>Existence of unbounded components\<close>
+
+lemma cobounded_unbounded_component:
+    fixes s :: "'a :: euclidean_space set"
+    assumes "bounded (-s)"
+      shows "\<exists>x. x \<in> s \<and> ~ bounded (connected_component_set s x)"
+proof -
+  obtain i::'a where i: "i \<in> Basis"
+    using nonempty_Basis by blast
+  obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
+    using bounded_subset_ballD [OF assms, of 0] by auto
+  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
+    by (force simp add: ball_def dist_norm)
+  have unbounded_inner: "~ bounded {x. inner i x \<ge> B}"
+    apply (auto simp: bounded_def dist_norm)
+    apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
+    apply simp
+    using i
+    apply (auto simp: algebra_simps)
+    done
+  have **: "{x. B \<le> i \<bullet> x} \<subseteq> connected_component_set s (B *\<^sub>R i)"
+    apply (rule connected_component_maximal)
+    apply (auto simp: i intro: convex_connected convex_halfspace_ge [of B])
+    apply (rule *)
+    apply (rule order_trans [OF _ Basis_le_norm [OF i]])
+    by (simp add: inner_commute)
+  have "B *\<^sub>R i \<in> s"
+    by (rule *) (simp add: norm_Basis [OF i])
+  then show ?thesis
+    apply (rule_tac x="B *\<^sub>R i" in exI, clarify)
+    apply (frule bounded_subset [of _ "{x. B \<le> i \<bullet> x}", OF _ **])
+    using unbounded_inner apply blast
+    done
+qed
+
+lemma cobounded_unique_unbounded_component:
+    fixes s :: "'a :: euclidean_space set"
+    assumes bs: "bounded (-s)" and "2 \<le> DIM('a)"
+        and bo: "~ bounded(connected_component_set s x)"
+                "~ bounded(connected_component_set s y)"
+      shows "connected_component_set s x = connected_component_set s y"
+proof -
+  obtain i::'a where i: "i \<in> Basis"
+    using nonempty_Basis by blast
+  obtain B where B: "B>0" "-s \<subseteq> ball 0 B"
+    using bounded_subset_ballD [OF bs, of 0] by auto
+  then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
+    by (force simp add: ball_def dist_norm)
+  have ccb: "connected (- ball 0 B :: 'a set)"
+    using assms by (auto intro: connected_complement_bounded_convex)
+  obtain x' where x': "connected_component s x x'" "norm x' > B"
+    using bo [unfolded bounded_def dist_norm, simplified, rule_format]
+    by (metis diff_zero norm_minus_commute not_less)
+  obtain y' where y': "connected_component s y y'" "norm y' > B"
+    using bo [unfolded bounded_def dist_norm, simplified, rule_format]
+    by (metis diff_zero norm_minus_commute not_less)
+  have x'y': "connected_component s x' y'"
+    apply (simp add: connected_component_def)
+    apply (rule_tac x="- ball 0 B" in exI)
+    using x' y'
+    apply (auto simp: ccb dist_norm *)
+    done
+  show ?thesis
+    apply (rule connected_component_eq)
+    using x' y' x'y'
+    by (metis (no_types, lifting) connected_component_eq_empty connected_component_eq_eq connected_component_idemp connected_component_in)
+qed
+
+lemma cobounded_unbounded_components:
+    fixes s :: "'a :: euclidean_space set"
+    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> ~bounded c"
+  by (metis cobounded_unbounded_component components_def imageI)
+
+lemma cobounded_unique_unbounded_components:
+    fixes s :: "'a :: euclidean_space set"
+    shows  "\<lbrakk>bounded (- s); c \<in> components s; \<not> bounded c; c' \<in> components s; \<not> bounded c'; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> c' = c"
+  unfolding components_iff
+  by (metis cobounded_unique_unbounded_component)
+
+lemma cobounded_has_bounded_component:
+    fixes s :: "'a :: euclidean_space set"
+    shows "\<lbrakk>bounded (- s); ~connected s; 2 \<le> DIM('a)\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> bounded c"
+  by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq)
+
+
+subsection\<open>The "inside" and "outside" of a set\<close>
+
+text\<open>The inside comprises the points in a bounded connected component of the set's complement.
+  The outside comprises the points in unbounded connected component of the complement.\<close>
+
+definition inside where
+  "inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
+
+definition outside where
+  "outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
+
+lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
+  by (auto simp: outside_def) (metis Compl_iff bounded_empty connected_component_eq_empty)
+
+lemma inside_no_overlap [simp]: "inside s \<inter> s = {}"
+  by (auto simp: inside_def)
+
+lemma outside_no_overlap [simp]:
+   "outside s \<inter> s = {}"
+  by (auto simp: outside_def)
+
+lemma inside_inter_outside [simp]: "inside s \<inter> outside s = {}"
+  by (auto simp: inside_def outside_def)
+
+lemma inside_union_outside [simp]: "inside s \<union> outside s = (- s)"
+  by (auto simp: inside_def outside_def)
+
+lemma inside_eq_outside:
+   "inside s = outside s \<longleftrightarrow> s = UNIV"
+  by (auto simp: inside_def outside_def)
+
+lemma inside_outside: "inside s = (- (s \<union> outside s))"
+  by (force simp add: inside_def outside)
+
+lemma outside_inside: "outside s = (- (s \<union> inside s))"
+  by (auto simp: inside_outside) (metis IntI equals0D outside_no_overlap)
+
+lemma union_with_inside: "s \<union> inside s = - outside s"
+  by (auto simp: inside_outside) (simp add: outside_inside)
+
+lemma union_with_outside: "s \<union> outside s = - inside s"
+  by (simp add: inside_outside)
+
+lemma outside_mono: "s \<subseteq> t \<Longrightarrow> outside t \<subseteq> outside s"
+  by (auto simp: outside bounded_subset connected_component_mono)
+
+lemma inside_mono: "s \<subseteq> t \<Longrightarrow> inside s - t \<subseteq> inside t"
+  by (auto simp: inside_def bounded_subset connected_component_mono)
+
+lemma segment_bound_lemma:
+  fixes u::real
+  assumes "x \<ge> B" "y \<ge> B" "0 \<le> u" "u \<le> 1"
+  shows "(1 - u) * x + u * y \<ge> B"
+proof -
+  obtain dx dy where "dx \<ge> 0" "dy \<ge> 0" "x = B + dx" "y = B + dy"
+    using assms by auto (metis add.commute diff_add_cancel)
+  with `0 \<le> u` `u \<le> 1` show ?thesis
+    by (simp add: add_increasing2 mult_left_le field_simps)
+qed
+
+lemma cobounded_outside:
+  fixes s :: "'a :: real_normed_vector set"
+  assumes "bounded s" shows "bounded (- outside s)"
+proof -
+  obtain B where B: "B>0" "s \<subseteq> ball 0 B"
+    using bounded_subset_ballD [OF assms, of 0] by auto
+  { fix x::'a and C::real
+    assume Bno: "B \<le> norm x" and C: "0 < C"
+    have "\<exists>y. connected_component (- s) x y \<and> norm y > C"
+    proof (cases "x = 0")
+      case True with B Bno show ?thesis by force
+    next
+      case False with B C show ?thesis
+        apply (rule_tac x="((B+C)/norm x) *\<^sub>R x" in exI)
+        apply (simp add: connected_component_def)
+        apply (rule_tac x="closed_segment x (((B+C)/norm x) *\<^sub>R x)" in exI)
+        apply simp
+        apply (rule_tac y="- ball 0 B" in order_trans)
+         prefer 2 apply force
+        apply (simp add: closed_segment_def ball_def dist_norm, clarify)
+        apply (simp add: real_vector_class.scaleR_add_left [symmetric] divide_simps)
+        using segment_bound_lemma [of B "norm x" "B+C" ] Bno
+        by (meson le_add_same_cancel1 less_eq_real_def not_le)
+    qed
+  }
+  then show ?thesis
+    apply (simp add: outside_def assms)
+    apply (rule bounded_subset [OF bounded_ball [of 0 B]])
+    apply (force simp add: dist_norm not_less bounded_pos)
+    done
+qed
+
+lemma unbounded_outside:
+    fixes s :: "'a::{real_normed_vector, perfect_space} set"
+    shows "bounded s \<Longrightarrow> ~ bounded(outside s)"
+  using cobounded_imp_unbounded cobounded_outside by blast
+
+lemma bounded_inside:
+    fixes s :: "'a::{real_normed_vector, perfect_space} set"
+    shows "bounded s \<Longrightarrow> bounded(inside s)"
+  by (simp add: bounded_Int cobounded_outside inside_outside)
+
+lemma connected_outside:
+    fixes s :: "'a::euclidean_space set"
+    assumes "bounded s" "2 \<le> DIM('a)"
+      shows "connected(outside s)"
+  apply (simp add: connected_iff_connected_component, clarify)
+  apply (simp add: outside)
+  apply (rule_tac s="connected_component_set (- s) x" in connected_component_of_subset)
+  apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq)
+  apply clarify
+  apply (metis connected_component_eq_eq connected_component_in)
+  done
+
+lemma outside_connected_component_lt:
+    "outside s = {x. \<forall>B. \<exists>y. B < norm(y) \<and> connected_component (- s) x y}"
+apply (auto simp: outside bounded_def dist_norm)
+apply (metis diff_0 norm_minus_cancel not_less)
+by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6))
+
+lemma outside_connected_component_le:
+   "outside s =
+            {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and>
+                         connected_component (- s) x y}"
+apply (simp add: outside_connected_component_lt)
+apply (simp add: Set.set_eq_iff)
+by (meson gt_ex leD le_less_linear less_imp_le order.trans)
+
+lemma not_outside_connected_component_lt:
+    fixes s :: "'a::euclidean_space set"
+    assumes s: "bounded s" and "2 \<le> DIM('a)"
+      shows "- (outside s) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- s) x y)}"
+proof -
+  obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> s \<Longrightarrow> norm x \<le> B"
+    using s [simplified bounded_pos] by auto
+  { fix y::'a and z::'a
+    assume yz: "B < norm z" "B < norm y"
+    have "connected_component (- cball 0 B) y z"
+      apply (rule connected_componentI [OF _ subset_refl])
+      apply (rule connected_complement_bounded_convex)
+      using assms yz
+      by (auto simp: dist_norm)
+    then have "connected_component (- s) y z"
+      apply (rule connected_component_of_subset)
+      apply (metis Bno Compl_anti_mono mem_cball_0 subset_iff)
+      done
+  } note cyz = this
+  show ?thesis
+    apply (auto simp: outside)
+    apply (metis Compl_iff bounded_iff cobounded_imp_unbounded mem_Collect_eq not_le)
+    apply (simp add: bounded_pos)
+    by (metis B connected_component_trans cyz not_le)
+qed
+
+lemma not_outside_connected_component_le:
+    fixes s :: "'a::euclidean_space set"
+    assumes s: "bounded s"  "2 \<le> DIM('a)"
+      shows "- (outside s) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- s) x y)}"
+apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
+by (meson gt_ex less_le_trans)
+
+lemma inside_connected_component_lt:
+    fixes s :: "'a::euclidean_space set"
+    assumes s: "bounded s"  "2 \<le> DIM('a)"
+      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- s) x y))}"
+  by (auto simp: inside_outside not_outside_connected_component_lt [OF assms])
+
+lemma inside_connected_component_le:
+    fixes s :: "'a::euclidean_space set"
+    assumes s: "bounded s"  "2 \<le> DIM('a)"
+      shows "inside s = {x. (x \<notin> s) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- s) x y))}"
+  by (auto simp: inside_outside not_outside_connected_component_le [OF assms])
+
+lemma inside_subset:
+  assumes "connected u" and "~bounded u" and "t \<union> u = - s"
+  shows "inside s \<subseteq> t"
+apply (auto simp: inside_def)
+by (metis bounded_subset [of "connected_component_set (- s) _"] connected_component_maximal
+       Compl_iff Un_iff assms subsetI)
+
+lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
+  by (simp add: Int_commute frontier_def interior_closure)
+
+lemma connected_inter_frontier:
+     "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
+  apply (simp add: frontier_interiors connected_open_in, safe)
+  apply (drule_tac x="s \<inter> interior t" in spec, safe)
+   apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
+   apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
+  done
+
+lemma connected_component_UNIV:
+    fixes x :: "'a::real_normed_vector"
+    shows "connected_component_set UNIV x = UNIV"
+using connected_iff_eq_connected_component_set [of "UNIV::'a set"] connected_UNIV
+by auto
+
+lemma connected_component_eq_UNIV:
+    fixes x :: "'a::real_normed_vector"
+    shows "connected_component_set s x = UNIV \<longleftrightarrow> s = UNIV"
+  using connected_component_in connected_component_UNIV by blast
+
+lemma components_univ [simp]: "components UNIV = {UNIV :: 'a::real_normed_vector set}"
+  by (auto simp: components_eq_sing_iff)
+
+lemma interior_inside_frontier:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "bounded s"
+      shows "interior s \<subseteq> inside (frontier s)"
+proof -
+  { fix x y
+    assume x: "x \<in> interior s" and y: "y \<notin> s"
+       and cc: "connected_component (- frontier s) x y"
+    have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
+      apply (rule connected_inter_frontier, simp)
+      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x)
+      using  y cc
+      by blast
+    then have "bounded (connected_component_set (- frontier s) x)"
+      using connected_component_in by auto
+  }
+  then show ?thesis
+    apply (auto simp: inside_def frontier_def)
+    apply (rule classical)
+    apply (rule bounded_subset [OF assms], blast)
+    done
+qed
+
+lemma inside_empty [simp]: "inside {} = ({} :: 'a :: {real_normed_vector, perfect_space} set)"
+  by (simp add: inside_def connected_component_UNIV)
+
+lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
+using inside_empty inside_union_outside by blast
+
+lemma inside_same_component:
+   "\<lbrakk>connected_component (- s) x y; x \<in> inside s\<rbrakk> \<Longrightarrow> y \<in> inside s"
+  using connected_component_eq connected_component_in
+  by (fastforce simp add: inside_def)
+
+lemma outside_same_component:
+   "\<lbrakk>connected_component (- s) x y; x \<in> outside s\<rbrakk> \<Longrightarrow> y \<in> outside s"
+  using connected_component_eq connected_component_in
+  by (fastforce simp add: outside_def)
+
+lemma convex_in_outside:
+  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+  assumes s: "convex s" and z: "z \<notin> s"
+    shows "z \<in> outside s"
+proof (cases "s={}")
+  case True then show ?thesis by simp
+next
+  case False then obtain a where "a \<in> s" by blast
+  with z have zna: "z \<noteq> a" by auto
+  { assume "bounded (connected_component_set (- s) z)"
+    with bounded_pos_less obtain B where "B>0" and B: "\<And>x. connected_component (- s) z x \<Longrightarrow> norm x < B"
+      by (metis mem_Collect_eq)
+    def C \<equiv> "((B + 1 + norm z) / norm (z-a))"
+    have "C > 0"
+      using `0 < B` zna by (simp add: C_def divide_simps add_strict_increasing)
+    have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z"
+      by (metis add_diff_cancel norm_triangle_ineq3)
+    moreover have "norm (C *\<^sub>R (z-a)) > norm z + B"
+      using zna `B>0` by (simp add: C_def le_max_iff_disj field_simps)
+    ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith
+    { fix u::real
+      assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s"
+      then have Cpos: "1 + u * C > 0"
+        by (meson `0 < C` add_pos_nonneg less_eq_real_def zero_le_mult_iff zero_less_one)
+      then have *: "(1 / (1 + u * C)) *\<^sub>R z + (u * C / (1 + u * C)) *\<^sub>R z = z"
+        by (simp add: scaleR_add_left [symmetric] divide_simps)
+      then have False
+        using convexD_alt [OF s `a \<in> s` ins, of "1/(u*C + 1)"] `C>0` `z \<notin> s` Cpos u
+        by (simp add: * divide_simps algebra_simps)
+    } note contra = this
+    have "connected_component (- s) z (z + C *\<^sub>R (z-a))"
+      apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]])
+      apply (simp add: closed_segment_def)
+      using contra
+      apply auto
+      done
+    then have False
+      using zna B [of "z + C *\<^sub>R (z-a)"] C
+      by (auto simp: divide_simps max_mult_distrib_right)
+  }
+  then show ?thesis
+    by (auto simp: outside_def z)
+qed
+
+lemma outside_convex:
+  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+  assumes "convex s"
+    shows "outside s = - s"
+  by (metis ComplD assms convex_in_outside equalityI inside_union_outside subsetI sup.cobounded2)
+
+lemma inside_convex:
+  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+  shows "convex s \<Longrightarrow> inside s = {}"
+  by (simp add: inside_outside outside_convex)
+
+lemma outside_subset_convex:
+  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+  shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
+  using outside_convex outside_mono by blast
+
+lemma outside_frontier_misses_closure:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "bounded s"
+    shows  "outside(frontier s) \<subseteq> - closure s"
+  unfolding outside_inside Lattices.boolean_algebra_class.compl_le_compl_iff
+proof -
+  { assume "interior s \<subseteq> inside (frontier s)"
+    hence "interior s \<union> inside (frontier s) = inside (frontier s)"
+      by (simp add: subset_Un_eq)
+    then have "closure s \<subseteq> frontier s \<union> inside (frontier s)"
+      using frontier_def by auto
+  }
+  then show "closure s \<subseteq> frontier s \<union> inside (frontier s)"
+    using interior_inside_frontier [OF assms] by blast
+qed
+
+lemma outside_frontier_eq_complement_closure:
+  fixes s :: "'a :: {real_normed_vector, perfect_space} set"
+    assumes "bounded s" "convex s"
+      shows "outside(frontier s) = - closure s"
+by (metis Diff_subset assms convex_closure frontier_def outside_frontier_misses_closure
+          outside_subset_convex subset_antisym)
+
+lemma open_inside:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "closed s"
+      shows "open (inside s)"
+proof -
+  { fix x assume x: "x \<in> inside s"
+    have "open (connected_component_set (- s) x)"
+      using assms open_connected_component by blast
+    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
+      using dist_not_less_zero
+      apply (simp add: open_dist)
+      by (metis (no_types, lifting) Compl_iff connected_component_refl_eq inside_def mem_Collect_eq x)
+    then have "\<exists>e>0. ball x e \<subseteq> inside s"
+      by (metis e dist_commute inside_same_component mem_ball subsetI x)
+  }
+  then show ?thesis
+    by (simp add: open_contains_ball)
+qed
+
+lemma open_outside:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "closed s"
+      shows "open (outside s)"
+proof -
+  { fix x assume x: "x \<in> outside s"
+    have "open (connected_component_set (- s) x)"
+      using assms open_connected_component by blast
+    then obtain e where e: "e>0" and e: "\<And>y. dist y x < e \<longrightarrow> connected_component (- s) x y"
+      using dist_not_less_zero
+      apply (simp add: open_dist)
+      by (metis Int_iff outside_def connected_component_refl_eq  x)
+    then have "\<exists>e>0. ball x e \<subseteq> outside s"
+      by (metis e dist_commute outside_same_component mem_ball subsetI x)
+  }
+  then show ?thesis
+    by (simp add: open_contains_ball)
+qed
+
+lemma closure_inside_subset:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "closed s"
+      shows "closure(inside s) \<subseteq> s \<union> inside s"
+by (metis assms closure_minimal open_closed open_outside sup.cobounded2 union_with_inside)
+
+lemma frontier_inside_subset:
+    fixes s :: "'a::real_normed_vector set"
+    assumes "closed s"
+      shows "frontier(inside s) \<subseteq> s"
+proof -
+  have "closure (inside s) \<inter> - inside s = closure (inside s) - interior (inside s)"
+    by (metis (no_types) Diff_Compl assms closure_closed interior_closure open_closed open_inside)
+  moreover have "- inside s \<inter> - outside s = s"
+    by (metis (no_types) compl_sup double_compl inside_union_outside)
+  moreover have "closure (inside s) \<subseteq> - outside s"
+    by (metis (no_types) assms closure_inside_subset union_with_inside)
+  ultimately have "closure (inside s) - interior (inside s) \<subseteq> s"
+    by blast
+  then show ?thesis
+    by (simp add: frontier_def open_inside interior_open)
+qed
+
 end
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -836,6 +836,9 @@
 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
   by (simp add: set_eq_iff)
 
+lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
+  by (auto simp: cball_def ball_def dist_commute)
+
 lemma diff_less_iff:
   "(a::real) - b > 0 \<longleftrightarrow> a > b"
   "(a::real) - b < 0 \<longleftrightarrow> a < b"
@@ -1806,6 +1809,10 @@
 abbreviation
    "connected_component_set s x \<equiv> Collect (connected_component s x)"
 
+lemma connected_componentI:
+    "\<lbrakk>connected t; t \<subseteq> s; x \<in> t; y \<in> t\<rbrakk> \<Longrightarrow> connected_component s x y"
+  by (auto simp: connected_component_def)
+
 lemma connected_component_in: "connected_component s x y \<Longrightarrow> x \<in> s \<and> y \<in> s"
   by (auto simp: connected_component_def)
 
@@ -3086,8 +3093,21 @@
 definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
   where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
 
-lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
-  unfolding bounded_def subset_eq by auto
+lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
+  unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)
+
+lemma bounded_subset_ballD:
+  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
+proof -
+  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
+    using assms by (auto simp: bounded_subset_cball)
+  then show ?thesis
+    apply (rule_tac x="dist x y + e + 1" in exI)
+    apply (simp add: add.commute add_pos_nonneg)
+    apply (erule subset_trans)
+    apply (clarsimp simp add: cball_def)
+    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
+qed
 
 lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
   unfolding bounded_def
@@ -3207,6 +3227,11 @@
   then show "\<exists>x::'a. b < norm x" ..
 qed
 
+corollary cobounded_imp_unbounded:
+    fixes S :: "'a::{real_normed_vector, perfect_space} set"
+    shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
+  using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
+
 lemma bounded_linear_image:
   assumes "bounded S"
     and "bounded_linear f"
diff -r fb95d06fb21f -r d53db136e8fd src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Oct 13 09:21:21 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Oct 13 12:42:08 2015 +0100
@@ -1393,11 +1393,15 @@
   unfolding continuous_on_closed_invariant
   by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
 
+corollary closed_vimage_Int[continuous_intros]:
+  assumes "closed s" and "continuous_on t f" and t: "closed t"
+  shows "closed (f -` s \<inter> t)"
+  using assms unfolding continuous_on_closed_vimage [OF t]  by simp
+
 corollary closed_vimage[continuous_intros]:
   assumes "closed s" and "continuous_on UNIV f"
   shows "closed (f -` s)"
-  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
-  by simp
+  using closed_vimage_Int [OF assms] by simp
 
 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"