# HG changeset patch
# User hoelzl
# Date 1363945303 -3600
# Node ID 3793c3a1137838120329243d7a504feabc2a879c
# Parent  33db4b7189af09131c208eb48db236660cbcbac3
move connected to HOL image; used to show intermediate value theorem

diff -r 33db4b7189af -r 3793c3a11378 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
@@ -495,63 +495,6 @@
   qed
 qed
 
-lemma lemma_BOLZANO:
-     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
-         \<forall>x. \<exists>d::real. 0 < d &
-                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
-         a \<le> b |]
-      ==> P(a,b)"
-  using Bolzano[of a b "\<lambda>a b. P (a, b)"] by metis
-
-lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) --> P(a,c)) &
-       (\<forall>x. \<exists>d::real. 0 < d &
-                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b))))
-      --> (\<forall>a b. a \<le> b --> P(a,b))"
-apply clarify
-apply (blast intro: lemma_BOLZANO)
-done
-
-
-subsection {* Intermediate Value Theorem *}
-
-text {*Prove Contrapositive by Bisection*}
-
-lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b);
-         a \<le> b;
-         (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
-      ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
-apply (rule contrapos_pp, assumption)
-apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2)
-apply safe
-apply simp_all
-apply (simp add: isCont_iff LIM_eq)
-apply (rule ccontr)
-apply (subgoal_tac "a \<le> x & x \<le> b")
- prefer 2
- apply simp
- apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
-apply (drule_tac x = x in spec)+
-apply simp
-apply (drule_tac P = "%r. ?P r --> (\<exists>s>0. ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
-apply safe
-apply simp
-apply (drule_tac x = s in spec, clarify)
-apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe)
-apply (drule_tac x = "ba-x" in spec)
-apply (simp_all add: abs_if)
-apply (drule_tac x = "aa-x" in spec)
-apply (case_tac "x \<le> aa", simp_all)
-done
-
-lemma IVT2: "[| f(b::real) \<le> (y::real); y \<le> f(a);
-         a \<le> b;
-         (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
-      |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
-apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
-apply (drule IVT [where f = "%x. - f x"], assumption)
-apply simp_all
-done
-
 (*HOL style here: object-level formulations*)
 lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b &
       (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
diff -r 33db4b7189af -r 3793c3a11378 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -1155,119 +1155,32 @@
 
 subsection {* Connectedness of convex sets *}
 
-lemma connected_real_lemma:
-  fixes f :: "real \<Rightarrow> 'a::metric_space"
-  assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
-    and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
-    and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
-    and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
-    and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
-  shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
-proof -
-  let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
-  have Se: " \<exists>x. x \<in> ?S"
-    apply (rule exI[where x=a])
-    apply (auto simp add: fa)
-    done
-  have Sub: "\<exists>y. isUb UNIV ?S y"
-    apply (rule exI[where x= b])
-    using ab fb e12 apply (auto simp add: isUb_def setle_def)
-    done
-  from reals_complete[OF Se Sub] obtain l where
-    l: "isLub UNIV ?S l"by blast
-  have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
-    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-    apply (metis linorder_linear)
-    done
-  have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
-    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-    apply (metis linorder_linear not_le)
-    done
-  have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
-  have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
-  have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
-  then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
-  { assume le2: "f l \<in> e2"
-    from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
-    then have lap: "l - a > 0" using alb by arith
-    from e2[rule_format, OF le2] obtain e where
-      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
-    from dst[OF alb e(1)] obtain d where
-      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-    let ?d' = "min (d/2) ((l - a)/2)"
-    have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
-      by (simp add: min_max.less_infI2)
-    then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
-    then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
-    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
-    from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
-    moreover
-    have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
-    ultimately have False using e12 alb d' by auto }
-  moreover
-  { assume le1: "f l \<in> e1"
-    from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
-    then have blp: "b - l > 0" using alb by arith
-    from e1[rule_format, OF le1] obtain e where
-      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
-    from dst[OF alb e(1)] obtain d where
-      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-    have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
-    then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
-    then obtain d' where d': "d' > 0" "d' < d" by metis
-    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
-    then have "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
-    with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
-    with l d' have False
-      by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
-  ultimately show ?thesis using alb by metis
-qed
+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)
 
 lemma convex_connected:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s" shows "connected s"
-proof -
-  { fix e1 e2
-    assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
-    assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
-    then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
-    then have n: "norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
-
-    { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"
-      { fix y
-        have *: "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"
-          by (simp add: algebra_simps)
-        assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
-        hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
-          unfolding * and scaleR_right_diff_distrib[symmetric]
-          unfolding less_divide_eq using n by auto
-      }
-      then have "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
-        apply (rule_tac x="e / norm (x1 - x2)" in exI)
-        using as
-        apply auto
-        unfolding zero_less_divide_iff
-        using n apply simp
-        done
-    } note * = this
-
-    have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
-      apply (rule connected_real_lemma)
-      apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
-      using * apply (simp add: dist_norm)
-      using as(1,2)[unfolded open_dist] apply simp
-      using as(1,2)[unfolded open_dist] apply simp
-      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
-      using as(3) apply auto
-      done
-    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
-      by auto
-    then have False
-      using as(4)
-      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
-      using x1(2) x2(2) by auto
-    }
-  then show ?thesis unfolding connected_def by auto
+proof (rule connectedI)
+  fix A B
+  assume "open A" "open B" "A \<inter> B \<inter> s = {}" "s \<subseteq> A \<union> B"
+  moreover
+  assume "A \<inter> s \<noteq> {}" "B \<inter> s \<noteq> {}"
+  then obtain a b where a: "a \<in> A" "a \<in> s" and b: "b \<in> B" "b \<in> s" by auto
+  def f \<equiv> "\<lambda>u. u *\<^sub>R a + (1 - u) *\<^sub>R b"
+  then have "continuous_on {0 .. 1} f"
+    by (auto intro!: continuous_on_intros)
+  then have "connected (f ` {0 .. 1})"
+    by (auto intro!: connected_continuous_image)
+  note connectedD[OF this, of A B]
+  moreover have "a \<in> A \<inter> f ` {0 .. 1}"
+    using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def)
+  moreover have "b \<in> B \<inter> f ` {0 .. 1}"
+    using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def)
+  moreover have "f ` {0 .. 1} \<subseteq> s"
+    using `convex s` a b unfolding convex_def f_def by auto
+  ultimately show False by auto
 qed
 
 text {* One rather trivial consequence. *}
diff -r 33db4b7189af -r 3793c3a11378 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
@@ -769,10 +769,6 @@
 
 subsection{* Connectedness *}
 
-definition "connected S \<longleftrightarrow>
-  ~(\<exists>e1 e2. open e1 \<and> open e2 \<and> S \<subseteq> (e1 \<union> e2) \<and> (e1 \<inter> e2 \<inter> S = {})
-  \<and> ~(e1 \<inter> S = {}) \<and> ~(e2 \<inter> S = {}))"
-
 lemma connected_local:
  "connected S \<longleftrightarrow> ~(\<exists>e1 e2.
                  openin (subtopology euclidean S) e1 \<and>
diff -r 33db4b7189af -r 3793c3a11378 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
@@ -5,7 +5,7 @@
 header {* Vector Spaces and Algebras over the Reals *}
 
 theory RealVector
-imports RComplete Metric_Spaces
+imports RComplete Metric_Spaces SupInf
 begin
 
 subsection {* Locale for additive functions *}
@@ -917,4 +917,157 @@
     by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
 qed
 
+section {* Connectedness *}
+
+class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
+begin
+
+lemma Inf_notin_open:
+  assumes A: "open A" and bnd: "\<forall>a\<in>A. x < a"
+  shows "Inf A \<notin> A"
+proof
+  assume "Inf A \<in> A"
+  then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A"
+    using open_left[of A "Inf A" x] assms by auto
+  with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
+    by (auto simp: subset_eq)
+  then show False
+    using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
+qed
+
+lemma Sup_notin_open:
+  assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x"
+  shows "Sup A \<notin> A"
+proof
+  assume "Sup A \<in> A"
+  then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A"
+    using open_right[of A "Sup A" x] assms by auto
+  with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
+    by (auto simp: subset_eq)
+  then show False
+    using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
+qed
+
 end
+
+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"
+  shows "connected U"
+proof (rule connectedI)
+  { fix A B assume "open A" "open B" "A \<inter> B \<inter> U = {}" "U \<subseteq> A \<union> B"
+    fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U"
+
+    let ?z = "Inf (B \<inter> {x <..})"
+
+    have "x \<le> ?z" "?z \<le> y"
+      using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
+    with `x \<in> U` `y \<in> U` have "?z \<in> U"
+      by (rule *)
+    moreover have "?z \<notin> B \<inter> {x <..}"
+      using `open B` by (intro Inf_notin_open) auto
+    ultimately have "?z \<in> A"
+      using `x \<le> ?z` `A \<inter> B \<inter> U = {}` `x \<in> A` `U \<subseteq> A \<union> B` by auto
+
+    { assume "?z < y"
+      obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
+        using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
+      moreover obtain b where "b \<in> B" "x < b" "b < min a y"
+        using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
+        by (auto intro: less_imp_le)
+      moreover then have "?z \<le> b"
+        by (intro cInf_lower[where z=x]) auto
+      moreover have "b \<in> U"
+        using `x \<le> ?z` `?z \<le> b` `b < min a y`
+        by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)
+      ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U"
+        by (intro bexI[of _ b]) auto }
+    then have False
+      using `?z \<le> y` `?z \<in> A` `y \<in> B` `y \<in> U` `A \<inter> B \<inter> U = {}` unfolding le_less by blast }
+  note not_disjoint = this
+
+  fix A B assume AB: "open A" "open B" "U \<subseteq> A \<union> B" "A \<inter> B \<inter> U = {}"
+  moreover assume "A \<inter> U \<noteq> {}" then obtain x where x: "x \<in> U" "x \<in> A" by auto
+  moreover assume "B \<inter> U \<noteq> {}" then obtain y where y: "y \<in> U" "y \<in> B" by auto
+  moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
+  ultimately show False by (cases x y rule: linorder_cases) auto
+qed
+
+lemma connected_iff_interval:
+  fixes U :: "'a :: linear_continuum_topology set"
+  shows "connected U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>y\<in>U. \<forall>z. x \<le> z \<longrightarrow> z \<le> y \<longrightarrow> z \<in> U)"
+  by (auto intro: connectedI_interval dest: connectedD_interval)
+
+lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
+  unfolding connected_iff_interval by auto
+
+lemma connected_contains_Ioo: 
+  fixes A :: "'a :: linorder_topology set"
+  assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
+  using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
+
+subsection {* Intermediate Value Theorem *}
+
+lemma IVT':
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
+  assumes *: "continuous_on {a .. b} f"
+  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
+proof -
+  have "connected {a..b}"
+    unfolding connected_iff_interval by auto
+  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
+  show ?thesis
+    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
+qed
+
+lemma IVT2':
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
+  assumes *: "continuous_on {a .. b} f"
+  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
+proof -
+  have "connected {a..b}"
+    unfolding connected_iff_interval by auto
+  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
+  show ?thesis
+    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
+qed
+
+lemma IVT:
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  shows "f a \<le> y \<Longrightarrow> y \<le> f b \<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 IVT') (auto intro: continuous_at_imp_continuous_on)
+
+lemma IVT2:
+  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  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 ..
+
+end
diff -r 33db4b7189af -r 3793c3a11378 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
@@ -236,35 +236,27 @@
     by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
 qed
 
-lemma open_right:
-  fixes S :: "'a :: {no_top, linorder_topology} set"
-  assumes "open S" "x \<in> S" shows "\<exists>b>x. {x ..< b} \<subseteq> S"
+lemma (in linorder_topology) open_right:
+  assumes "open S" "x \<in> S" and gt_ex: "x < y" shows "\<exists>b>x. {x ..< b} \<subseteq> S"
   using assms unfolding open_generated_order
 proof induction
   case (Int A B)
   then obtain a b where "a > x" "{x ..< a} \<subseteq> A"  "b > x" "{x ..< b} \<subseteq> B" by auto
   then show ?case by (auto intro!: exI[of _ "min a b"])
 next
-  case (Basis S)
-  moreover from gt_ex[of x] guess b ..
-  ultimately show ?case by (fastforce intro: exI[of _ b])
-qed (fastforce intro: gt_ex)+
+  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] gt_ex)
+qed blast+
 
-lemma open_left:
-  fixes S :: "'a :: {no_bot, linorder_topology} set"
-  assumes "open S" "x \<in> S" shows "\<exists>b<x. {b <.. x} \<subseteq> S"
+lemma (in linorder_topology) open_left:
+  assumes "open S" "x \<in> S" and lt_ex: "y < x" shows "\<exists>b<x. {b <.. x} \<subseteq> S"
   using assms unfolding open_generated_order
 proof induction
   case (Int A B)
   then obtain a b where "a < x" "{a <.. x} \<subseteq> A"  "b < x" "{b <.. x} \<subseteq> B" by auto
   then show ?case by (auto intro!: exI[of _ "max a b"])
 next
-  case (Basis S)
-  moreover from lt_ex[of x] guess b ..
-  ultimately show ?case by (fastforce intro: exI[of _ b])
-next
-  case UN then show ?case by blast
-qed (fastforce intro: lt_ex)
+  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex)
+qed blast+
 
 subsection {* Filters *}
 
@@ -744,8 +736,9 @@
   shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
   unfolding eventually_nhds eventually_within at_def
 proof safe
-  fix S assume "open S" "x \<in> S"
-  note open_right[OF this]
+  from gt_ex[of x] guess y ..
+  moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
+  moreover note gt_ex[of x]
   moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
   ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
     by (auto simp: subset_eq Ball_def)
@@ -760,8 +753,8 @@
   shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
   unfolding eventually_nhds eventually_within at_def
 proof safe
-  fix S assume "open S" "x \<in> S"
-  note open_left[OF this]
+  from lt_ex[of x] guess y ..
+  moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
   moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
     by (auto simp: subset_eq Ball_def)
@@ -1482,7 +1475,7 @@
       (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
   proof (safe intro!: exI[of _ F])
     fix i
-    show "open (F i)" using nhds(1) by (auto simp: F_def intro!: open_INT)
+    show "open (F i)" using nhds(1) by (auto simp: F_def)
     show "x \<in> F i" using nhds(2) by (auto simp: F_def)
   next
     fix S assume "open S" "x \<in> S"
@@ -1873,5 +1866,65 @@
   shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
   using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
 
+
+subsection {* Connectedness *}
+
+context topological_space
+begin
+
+definition "connected S \<longleftrightarrow>
+  \<not> (\<exists>A B. open A \<and> open B \<and> S \<subseteq> A \<union> B \<and> A \<inter> B \<inter> S = {} \<and> A \<inter> S \<noteq> {} \<and> B \<inter> S \<noteq> {})"
+
+lemma connectedI:
+  "(\<And>A B. open A \<Longrightarrow> open B \<Longrightarrow> A \<inter> U \<noteq> {} \<Longrightarrow> B \<inter> U \<noteq> {} \<Longrightarrow> A \<inter> B \<inter> U = {} \<Longrightarrow> U \<subseteq> A \<union> B \<Longrightarrow> False)
+  \<Longrightarrow> connected U"
+  by (auto simp: connected_def)
+
+lemma connected_empty[simp]: "connected {}"
+  by (auto intro!: connectedI)
+
 end
 
+lemma (in linorder_topology) connectedD_interval:
+  assumes "connected U" and xy: "x \<in> U" "y \<in> U" and "x \<le> z" "z \<le> y"
+  shows "z \<in> U"
+proof -
+  have eq: "{..<z} \<union> {z<..} = - {z}"
+    by auto
+  { assume "z \<notin> U" "x < z" "z < y"
+    with xy have "\<not> connected U"
+      unfolding connected_def simp_thms
+      apply (rule_tac exI[of _ "{..< z}"])
+      apply (rule_tac exI[of _ "{z <..}"])
+      apply (auto simp add: eq)
+      done }
+  with assms show "z \<in> U"
+    by (metis less_le)
+qed
+
+lemma connected_continuous_image:
+  assumes *: "continuous_on s f"
+  assumes "connected s"
+  shows "connected (f ` s)"
+proof (rule connectedI)
+  fix A B assume A: "open A" "A \<inter> f ` s \<noteq> {}" and B: "open B" "B \<inter> f ` s \<noteq> {}" and
+    AB: "A \<inter> B \<inter> f ` s = {}" "f ` s \<subseteq> A \<union> B"
+  obtain A' where A': "open A'" "f -` A \<inter> s = A' \<inter> s"
+    using * `open A` unfolding continuous_on_open_invariant by metis
+  obtain B' where B': "open B'" "f -` B \<inter> s = B' \<inter> s"
+    using * `open B` unfolding continuous_on_open_invariant by metis
+
+  have "\<exists>A B. open A \<and> open B \<and> s \<subseteq> A \<union> B \<and> A \<inter> B \<inter> s = {} \<and> A \<inter> s \<noteq> {} \<and> B \<inter> s \<noteq> {}"
+  proof (rule exI[of _ A'], rule exI[of _ B'], intro conjI)
+    have "s \<subseteq> (f -` A \<inter> s) \<union> (f -` B \<inter> s)" using AB by auto
+    then show "s \<subseteq> A' \<union> B'" using A' B' by auto
+  next
+    have "(f -` A \<inter> s) \<inter> (f -` B \<inter> s) = {}" using AB by auto
+    then show "A' \<inter> B' \<inter> s = {}" using A' B' by auto
+  qed (insert A' B' A B, auto)
+  with `connected s` show False
+    unfolding connected_def by blast
+qed
+
+end
+
diff -r 33db4b7189af -r 3793c3a11378 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -97,11 +97,7 @@
   assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
   assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
   shows "P a b"
-apply (subgoal_tac "split P (a,b)", simp)
-apply (rule lemma_BOLZANO [OF _ _ 1])
-apply (clarify, erule (3) 2)
-apply (clarify, rule 3)
-done
+  using 1 2 3 by (rule Bolzano)
 
 text{*We can always find a division that is fine wrt any gauge*}