move connected to HOL image; used to show intermediate value theorem
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 514803793c3a11378
parent 51479 33db4b7189af
child 51481 ef949192e5d6
move connected to HOL image; used to show intermediate value theorem
src/HOL/Deriv.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/RealVector.thy
src/HOL/Topological_Spaces.thy
src/HOL/ex/Gauge_Integration.thy
     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -495,63 +495,6 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma lemma_BOLZANO:
     1.8 -     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
     1.9 -         \<forall>x. \<exists>d::real. 0 < d &
    1.10 -                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
    1.11 -         a \<le> b |]
    1.12 -      ==> P(a,b)"
    1.13 -  using Bolzano[of a b "\<lambda>a b. P (a, b)"] by metis
    1.14 -
    1.15 -lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) --> P(a,c)) &
    1.16 -       (\<forall>x. \<exists>d::real. 0 < d &
    1.17 -                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b))))
    1.18 -      --> (\<forall>a b. a \<le> b --> P(a,b))"
    1.19 -apply clarify
    1.20 -apply (blast intro: lemma_BOLZANO)
    1.21 -done
    1.22 -
    1.23 -
    1.24 -subsection {* Intermediate Value Theorem *}
    1.25 -
    1.26 -text {*Prove Contrapositive by Bisection*}
    1.27 -
    1.28 -lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b);
    1.29 -         a \<le> b;
    1.30 -         (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
    1.31 -      ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
    1.32 -apply (rule contrapos_pp, assumption)
    1.33 -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)
    1.34 -apply safe
    1.35 -apply simp_all
    1.36 -apply (simp add: isCont_iff LIM_eq)
    1.37 -apply (rule ccontr)
    1.38 -apply (subgoal_tac "a \<le> x & x \<le> b")
    1.39 - prefer 2
    1.40 - apply simp
    1.41 - apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
    1.42 -apply (drule_tac x = x in spec)+
    1.43 -apply simp
    1.44 -apply (drule_tac P = "%r. ?P r --> (\<exists>s>0. ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
    1.45 -apply safe
    1.46 -apply simp
    1.47 -apply (drule_tac x = s in spec, clarify)
    1.48 -apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe)
    1.49 -apply (drule_tac x = "ba-x" in spec)
    1.50 -apply (simp_all add: abs_if)
    1.51 -apply (drule_tac x = "aa-x" in spec)
    1.52 -apply (case_tac "x \<le> aa", simp_all)
    1.53 -done
    1.54 -
    1.55 -lemma IVT2: "[| f(b::real) \<le> (y::real); y \<le> f(a);
    1.56 -         a \<le> b;
    1.57 -         (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
    1.58 -      |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
    1.59 -apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
    1.60 -apply (drule IVT [where f = "%x. - f x"], assumption)
    1.61 -apply simp_all
    1.62 -done
    1.63 -
    1.64  (*HOL style here: object-level formulations*)
    1.65  lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b &
    1.66        (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -1155,119 +1155,32 @@
     2.4  
     2.5  subsection {* Connectedness of convex sets *}
     2.6  
     2.7 -lemma connected_real_lemma:
     2.8 -  fixes f :: "real \<Rightarrow> 'a::metric_space"
     2.9 -  assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
    2.10 -    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"
    2.11 -    and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
    2.12 -    and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
    2.13 -    and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
    2.14 -  shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
    2.15 -proof -
    2.16 -  let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
    2.17 -  have Se: " \<exists>x. x \<in> ?S"
    2.18 -    apply (rule exI[where x=a])
    2.19 -    apply (auto simp add: fa)
    2.20 -    done
    2.21 -  have Sub: "\<exists>y. isUb UNIV ?S y"
    2.22 -    apply (rule exI[where x= b])
    2.23 -    using ab fb e12 apply (auto simp add: isUb_def setle_def)
    2.24 -    done
    2.25 -  from reals_complete[OF Se Sub] obtain l where
    2.26 -    l: "isLub UNIV ?S l"by blast
    2.27 -  have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
    2.28 -    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    2.29 -    apply (metis linorder_linear)
    2.30 -    done
    2.31 -  have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
    2.32 -    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    2.33 -    apply (metis linorder_linear not_le)
    2.34 -    done
    2.35 -  have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
    2.36 -  have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
    2.37 -  have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
    2.38 -  then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
    2.39 -  { assume le2: "f l \<in> e2"
    2.40 -    from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
    2.41 -    then have lap: "l - a > 0" using alb by arith
    2.42 -    from e2[rule_format, OF le2] obtain e where
    2.43 -      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
    2.44 -    from dst[OF alb e(1)] obtain d where
    2.45 -      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
    2.46 -    let ?d' = "min (d/2) ((l - a)/2)"
    2.47 -    have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
    2.48 -      by (simp add: min_max.less_infI2)
    2.49 -    then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
    2.50 -    then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
    2.51 -    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
    2.52 -    from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
    2.53 -    moreover
    2.54 -    have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
    2.55 -    ultimately have False using e12 alb d' by auto }
    2.56 -  moreover
    2.57 -  { assume le1: "f l \<in> e1"
    2.58 -    from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
    2.59 -    then have blp: "b - l > 0" using alb by arith
    2.60 -    from e1[rule_format, OF le1] obtain e where
    2.61 -      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
    2.62 -    from dst[OF alb e(1)] obtain d where
    2.63 -      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
    2.64 -    have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
    2.65 -    then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
    2.66 -    then obtain d' where d': "d' > 0" "d' < d" by metis
    2.67 -    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
    2.68 -    then have "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
    2.69 -    with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
    2.70 -    with l d' have False
    2.71 -      by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
    2.72 -  ultimately show ?thesis using alb by metis
    2.73 -qed
    2.74 +lemma connectedD:
    2.75 +  "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 = {}"
    2.76 +  by (metis connected_def)
    2.77  
    2.78  lemma convex_connected:
    2.79    fixes s :: "'a::real_normed_vector set"
    2.80    assumes "convex s" shows "connected s"
    2.81 -proof -
    2.82 -  { fix e1 e2
    2.83 -    assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
    2.84 -    assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
    2.85 -    then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
    2.86 -    then have n: "norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
    2.87 -
    2.88 -    { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"
    2.89 -      { fix y
    2.90 -        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"
    2.91 -          by (simp add: algebra_simps)
    2.92 -        assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
    2.93 -        hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
    2.94 -          unfolding * and scaleR_right_diff_distrib[symmetric]
    2.95 -          unfolding less_divide_eq using n by auto
    2.96 -      }
    2.97 -      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"
    2.98 -        apply (rule_tac x="e / norm (x1 - x2)" in exI)
    2.99 -        using as
   2.100 -        apply auto
   2.101 -        unfolding zero_less_divide_iff
   2.102 -        using n apply simp
   2.103 -        done
   2.104 -    } note * = this
   2.105 -
   2.106 -    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"
   2.107 -      apply (rule connected_real_lemma)
   2.108 -      apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
   2.109 -      using * apply (simp add: dist_norm)
   2.110 -      using as(1,2)[unfolded open_dist] apply simp
   2.111 -      using as(1,2)[unfolded open_dist] apply simp
   2.112 -      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
   2.113 -      using as(3) apply auto
   2.114 -      done
   2.115 -    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"
   2.116 -      by auto
   2.117 -    then have False
   2.118 -      using as(4)
   2.119 -      using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
   2.120 -      using x1(2) x2(2) by auto
   2.121 -    }
   2.122 -  then show ?thesis unfolding connected_def by auto
   2.123 +proof (rule connectedI)
   2.124 +  fix A B
   2.125 +  assume "open A" "open B" "A \<inter> B \<inter> s = {}" "s \<subseteq> A \<union> B"
   2.126 +  moreover
   2.127 +  assume "A \<inter> s \<noteq> {}" "B \<inter> s \<noteq> {}"
   2.128 +  then obtain a b where a: "a \<in> A" "a \<in> s" and b: "b \<in> B" "b \<in> s" by auto
   2.129 +  def f \<equiv> "\<lambda>u. u *\<^sub>R a + (1 - u) *\<^sub>R b"
   2.130 +  then have "continuous_on {0 .. 1} f"
   2.131 +    by (auto intro!: continuous_on_intros)
   2.132 +  then have "connected (f ` {0 .. 1})"
   2.133 +    by (auto intro!: connected_continuous_image)
   2.134 +  note connectedD[OF this, of A B]
   2.135 +  moreover have "a \<in> A \<inter> f ` {0 .. 1}"
   2.136 +    using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def)
   2.137 +  moreover have "b \<in> B \<inter> f ` {0 .. 1}"
   2.138 +    using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def)
   2.139 +  moreover have "f ` {0 .. 1} \<subseteq> s"
   2.140 +    using `convex s` a b unfolding convex_def f_def by auto
   2.141 +  ultimately show False by auto
   2.142  qed
   2.143  
   2.144  text {* One rather trivial consequence. *}
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -769,10 +769,6 @@
     3.4  
     3.5  subsection{* Connectedness *}
     3.6  
     3.7 -definition "connected S \<longleftrightarrow>
     3.8 -  ~(\<exists>e1 e2. open e1 \<and> open e2 \<and> S \<subseteq> (e1 \<union> e2) \<and> (e1 \<inter> e2 \<inter> S = {})
     3.9 -  \<and> ~(e1 \<inter> S = {}) \<and> ~(e2 \<inter> S = {}))"
    3.10 -
    3.11  lemma connected_local:
    3.12   "connected S \<longleftrightarrow> ~(\<exists>e1 e2.
    3.13                   openin (subtopology euclidean S) e1 \<and>
     4.1 --- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     4.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Vector Spaces and Algebras over the Reals *}
     4.5  
     4.6  theory RealVector
     4.7 -imports RComplete Metric_Spaces
     4.8 +imports RComplete Metric_Spaces SupInf
     4.9  begin
    4.10  
    4.11  subsection {* Locale for additive functions *}
    4.12 @@ -917,4 +917,157 @@
    4.13      by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
    4.14  qed
    4.15  
    4.16 +section {* Connectedness *}
    4.17 +
    4.18 +class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
    4.19 +begin
    4.20 +
    4.21 +lemma Inf_notin_open:
    4.22 +  assumes A: "open A" and bnd: "\<forall>a\<in>A. x < a"
    4.23 +  shows "Inf A \<notin> A"
    4.24 +proof
    4.25 +  assume "Inf A \<in> A"
    4.26 +  then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A"
    4.27 +    using open_left[of A "Inf A" x] assms by auto
    4.28 +  with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
    4.29 +    by (auto simp: subset_eq)
    4.30 +  then show False
    4.31 +    using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    4.32 +qed
    4.33 +
    4.34 +lemma Sup_notin_open:
    4.35 +  assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x"
    4.36 +  shows "Sup A \<notin> A"
    4.37 +proof
    4.38 +  assume "Sup A \<in> A"
    4.39 +  then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A"
    4.40 +    using open_right[of A "Sup A" x] assms by auto
    4.41 +  with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
    4.42 +    by (auto simp: subset_eq)
    4.43 +  then show False
    4.44 +    using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    4.45 +qed
    4.46 +
    4.47  end
    4.48 +
    4.49 +lemma connectedI_interval:
    4.50 +  fixes U :: "'a :: linear_continuum_topology set"
    4.51 +  assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    4.52 +  shows "connected U"
    4.53 +proof (rule connectedI)
    4.54 +  { fix A B assume "open A" "open B" "A \<inter> B \<inter> U = {}" "U \<subseteq> A \<union> B"
    4.55 +    fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U"
    4.56 +
    4.57 +    let ?z = "Inf (B \<inter> {x <..})"
    4.58 +
    4.59 +    have "x \<le> ?z" "?z \<le> y"
    4.60 +      using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
    4.61 +    with `x \<in> U` `y \<in> U` have "?z \<in> U"
    4.62 +      by (rule *)
    4.63 +    moreover have "?z \<notin> B \<inter> {x <..}"
    4.64 +      using `open B` by (intro Inf_notin_open) auto
    4.65 +    ultimately have "?z \<in> A"
    4.66 +      using `x \<le> ?z` `A \<inter> B \<inter> U = {}` `x \<in> A` `U \<subseteq> A \<union> B` by auto
    4.67 +
    4.68 +    { assume "?z < y"
    4.69 +      obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
    4.70 +        using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
    4.71 +      moreover obtain b where "b \<in> B" "x < b" "b < min a y"
    4.72 +        using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
    4.73 +        by (auto intro: less_imp_le)
    4.74 +      moreover then have "?z \<le> b"
    4.75 +        by (intro cInf_lower[where z=x]) auto
    4.76 +      moreover have "b \<in> U"
    4.77 +        using `x \<le> ?z` `?z \<le> b` `b < min a y`
    4.78 +        by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)
    4.79 +      ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U"
    4.80 +        by (intro bexI[of _ b]) auto }
    4.81 +    then have False
    4.82 +      using `?z \<le> y` `?z \<in> A` `y \<in> B` `y \<in> U` `A \<inter> B \<inter> U = {}` unfolding le_less by blast }
    4.83 +  note not_disjoint = this
    4.84 +
    4.85 +  fix A B assume AB: "open A" "open B" "U \<subseteq> A \<union> B" "A \<inter> B \<inter> U = {}"
    4.86 +  moreover assume "A \<inter> U \<noteq> {}" then obtain x where x: "x \<in> U" "x \<in> A" by auto
    4.87 +  moreover assume "B \<inter> U \<noteq> {}" then obtain y where y: "y \<in> U" "y \<in> B" by auto
    4.88 +  moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
    4.89 +  ultimately show False by (cases x y rule: linorder_cases) auto
    4.90 +qed
    4.91 +
    4.92 +lemma connected_iff_interval:
    4.93 +  fixes U :: "'a :: linear_continuum_topology set"
    4.94 +  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)"
    4.95 +  by (auto intro: connectedI_interval dest: connectedD_interval)
    4.96 +
    4.97 +lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
    4.98 +  unfolding connected_iff_interval by auto
    4.99 +
   4.100 +lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
   4.101 +  unfolding connected_iff_interval by auto
   4.102 +
   4.103 +lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
   4.104 +  unfolding connected_iff_interval by auto
   4.105 +
   4.106 +lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
   4.107 +  unfolding connected_iff_interval by auto
   4.108 +
   4.109 +lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
   4.110 +  unfolding connected_iff_interval by auto
   4.111 +
   4.112 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
   4.113 +  unfolding connected_iff_interval by auto
   4.114 +
   4.115 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
   4.116 +  unfolding connected_iff_interval by auto
   4.117 +
   4.118 +lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
   4.119 +  unfolding connected_iff_interval by auto
   4.120 +
   4.121 +lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
   4.122 +  unfolding connected_iff_interval by auto
   4.123 +
   4.124 +lemma connected_contains_Ioo: 
   4.125 +  fixes A :: "'a :: linorder_topology set"
   4.126 +  assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
   4.127 +  using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
   4.128 +
   4.129 +subsection {* Intermediate Value Theorem *}
   4.130 +
   4.131 +lemma IVT':
   4.132 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   4.133 +  assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
   4.134 +  assumes *: "continuous_on {a .. b} f"
   4.135 +  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   4.136 +proof -
   4.137 +  have "connected {a..b}"
   4.138 +    unfolding connected_iff_interval by auto
   4.139 +  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
   4.140 +  show ?thesis
   4.141 +    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
   4.142 +qed
   4.143 +
   4.144 +lemma IVT2':
   4.145 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   4.146 +  assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
   4.147 +  assumes *: "continuous_on {a .. b} f"
   4.148 +  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   4.149 +proof -
   4.150 +  have "connected {a..b}"
   4.151 +    unfolding connected_iff_interval by auto
   4.152 +  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
   4.153 +  show ?thesis
   4.154 +    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
   4.155 +qed
   4.156 +
   4.157 +lemma IVT:
   4.158 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   4.159 +  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"
   4.160 +  by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
   4.161 +
   4.162 +lemma IVT2:
   4.163 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   4.164 +  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"
   4.165 +  by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
   4.166 +
   4.167 +instance real :: linear_continuum_topology ..
   4.168 +
   4.169 +end
     5.1 --- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     5.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     5.3 @@ -236,35 +236,27 @@
     5.4      by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
     5.5  qed
     5.6  
     5.7 -lemma open_right:
     5.8 -  fixes S :: "'a :: {no_top, linorder_topology} set"
     5.9 -  assumes "open S" "x \<in> S" shows "\<exists>b>x. {x ..< b} \<subseteq> S"
    5.10 +lemma (in linorder_topology) open_right:
    5.11 +  assumes "open S" "x \<in> S" and gt_ex: "x < y" shows "\<exists>b>x. {x ..< b} \<subseteq> S"
    5.12    using assms unfolding open_generated_order
    5.13  proof induction
    5.14    case (Int A B)
    5.15    then obtain a b where "a > x" "{x ..< a} \<subseteq> A"  "b > x" "{x ..< b} \<subseteq> B" by auto
    5.16    then show ?case by (auto intro!: exI[of _ "min a b"])
    5.17  next
    5.18 -  case (Basis S)
    5.19 -  moreover from gt_ex[of x] guess b ..
    5.20 -  ultimately show ?case by (fastforce intro: exI[of _ b])
    5.21 -qed (fastforce intro: gt_ex)+
    5.22 +  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] gt_ex)
    5.23 +qed blast+
    5.24  
    5.25 -lemma open_left:
    5.26 -  fixes S :: "'a :: {no_bot, linorder_topology} set"
    5.27 -  assumes "open S" "x \<in> S" shows "\<exists>b<x. {b <.. x} \<subseteq> S"
    5.28 +lemma (in linorder_topology) open_left:
    5.29 +  assumes "open S" "x \<in> S" and lt_ex: "y < x" shows "\<exists>b<x. {b <.. x} \<subseteq> S"
    5.30    using assms unfolding open_generated_order
    5.31  proof induction
    5.32    case (Int A B)
    5.33    then obtain a b where "a < x" "{a <.. x} \<subseteq> A"  "b < x" "{b <.. x} \<subseteq> B" by auto
    5.34    then show ?case by (auto intro!: exI[of _ "max a b"])
    5.35  next
    5.36 -  case (Basis S)
    5.37 -  moreover from lt_ex[of x] guess b ..
    5.38 -  ultimately show ?case by (fastforce intro: exI[of _ b])
    5.39 -next
    5.40 -  case UN then show ?case by blast
    5.41 -qed (fastforce intro: lt_ex)
    5.42 +  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex)
    5.43 +qed blast+
    5.44  
    5.45  subsection {* Filters *}
    5.46  
    5.47 @@ -744,8 +736,9 @@
    5.48    shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
    5.49    unfolding eventually_nhds eventually_within at_def
    5.50  proof safe
    5.51 -  fix S assume "open S" "x \<in> S"
    5.52 -  note open_right[OF this]
    5.53 +  from gt_ex[of x] guess y ..
    5.54 +  moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
    5.55 +  moreover note gt_ex[of x]
    5.56    moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
    5.57    ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
    5.58      by (auto simp: subset_eq Ball_def)
    5.59 @@ -760,8 +753,8 @@
    5.60    shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
    5.61    unfolding eventually_nhds eventually_within at_def
    5.62  proof safe
    5.63 -  fix S assume "open S" "x \<in> S"
    5.64 -  note open_left[OF this]
    5.65 +  from lt_ex[of x] guess y ..
    5.66 +  moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
    5.67    moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
    5.68    ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
    5.69      by (auto simp: subset_eq Ball_def)
    5.70 @@ -1482,7 +1475,7 @@
    5.71        (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
    5.72    proof (safe intro!: exI[of _ F])
    5.73      fix i
    5.74 -    show "open (F i)" using nhds(1) by (auto simp: F_def intro!: open_INT)
    5.75 +    show "open (F i)" using nhds(1) by (auto simp: F_def)
    5.76      show "x \<in> F i" using nhds(2) by (auto simp: F_def)
    5.77    next
    5.78      fix S assume "open S" "x \<in> S"
    5.79 @@ -1873,5 +1866,65 @@
    5.80    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)"
    5.81    using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
    5.82  
    5.83 +
    5.84 +subsection {* Connectedness *}
    5.85 +
    5.86 +context topological_space
    5.87 +begin
    5.88 +
    5.89 +definition "connected S \<longleftrightarrow>
    5.90 +  \<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> {})"
    5.91 +
    5.92 +lemma connectedI:
    5.93 +  "(\<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)
    5.94 +  \<Longrightarrow> connected U"
    5.95 +  by (auto simp: connected_def)
    5.96 +
    5.97 +lemma connected_empty[simp]: "connected {}"
    5.98 +  by (auto intro!: connectedI)
    5.99 +
   5.100  end
   5.101  
   5.102 +lemma (in linorder_topology) connectedD_interval:
   5.103 +  assumes "connected U" and xy: "x \<in> U" "y \<in> U" and "x \<le> z" "z \<le> y"
   5.104 +  shows "z \<in> U"
   5.105 +proof -
   5.106 +  have eq: "{..<z} \<union> {z<..} = - {z}"
   5.107 +    by auto
   5.108 +  { assume "z \<notin> U" "x < z" "z < y"
   5.109 +    with xy have "\<not> connected U"
   5.110 +      unfolding connected_def simp_thms
   5.111 +      apply (rule_tac exI[of _ "{..< z}"])
   5.112 +      apply (rule_tac exI[of _ "{z <..}"])
   5.113 +      apply (auto simp add: eq)
   5.114 +      done }
   5.115 +  with assms show "z \<in> U"
   5.116 +    by (metis less_le)
   5.117 +qed
   5.118 +
   5.119 +lemma connected_continuous_image:
   5.120 +  assumes *: "continuous_on s f"
   5.121 +  assumes "connected s"
   5.122 +  shows "connected (f ` s)"
   5.123 +proof (rule connectedI)
   5.124 +  fix A B assume A: "open A" "A \<inter> f ` s \<noteq> {}" and B: "open B" "B \<inter> f ` s \<noteq> {}" and
   5.125 +    AB: "A \<inter> B \<inter> f ` s = {}" "f ` s \<subseteq> A \<union> B"
   5.126 +  obtain A' where A': "open A'" "f -` A \<inter> s = A' \<inter> s"
   5.127 +    using * `open A` unfolding continuous_on_open_invariant by metis
   5.128 +  obtain B' where B': "open B'" "f -` B \<inter> s = B' \<inter> s"
   5.129 +    using * `open B` unfolding continuous_on_open_invariant by metis
   5.130 +
   5.131 +  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> {}"
   5.132 +  proof (rule exI[of _ A'], rule exI[of _ B'], intro conjI)
   5.133 +    have "s \<subseteq> (f -` A \<inter> s) \<union> (f -` B \<inter> s)" using AB by auto
   5.134 +    then show "s \<subseteq> A' \<union> B'" using A' B' by auto
   5.135 +  next
   5.136 +    have "(f -` A \<inter> s) \<inter> (f -` B \<inter> s) = {}" using AB by auto
   5.137 +    then show "A' \<inter> B' \<inter> s = {}" using A' B' by auto
   5.138 +  qed (insert A' B' A B, auto)
   5.139 +  with `connected s` show False
   5.140 +    unfolding connected_def by blast
   5.141 +qed
   5.142 +
   5.143 +end
   5.144 +
     6.1 --- a/src/HOL/ex/Gauge_Integration.thy	Fri Mar 22 10:41:43 2013 +0100
     6.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Fri Mar 22 10:41:43 2013 +0100
     6.3 @@ -97,11 +97,7 @@
     6.4    assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
     6.5    assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
     6.6    shows "P a b"
     6.7 -apply (subgoal_tac "split P (a,b)", simp)
     6.8 -apply (rule lemma_BOLZANO [OF _ _ 1])
     6.9 -apply (clarify, erule (3) 2)
    6.10 -apply (clarify, rule 3)
    6.11 -done
    6.12 +  using 1 2 3 by (rule Bolzano)
    6.13  
    6.14  text{*We can always find a division that is fine wrt any gauge*}
    6.15