# 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: - "[| \a b c. P(a,b) & P(b,c) & a \ b & b \ c --> P(a,c); - \x. \d::real. 0 < d & - (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)); - a \ b |] - ==> P(a,b)" - using Bolzano[of a b "\a b. P (a, b)"] by metis - -lemma lemma_BOLZANO2: "((\a b c. (a \ b & b \ c & P(a,b) & P(b,c)) --> P(a,c)) & - (\x. \d::real. 0 < d & - (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)))) - --> (\a b. a \ 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) \ (y::real); y \ f(b); - a \ b; - (\x. a \ x & x \ b --> isCont f x) |] - ==> \x. a \ x & x \ b & f(x) = y" -apply (rule contrapos_pp, assumption) -apply (cut_tac P = "% (u,v) . a \ u & u \ v & v \ b --> ~ (f (u) \ y & y \ f (v))" in lemma_BOLZANO2) -apply safe -apply simp_all -apply (simp add: isCont_iff LIM_eq) -apply (rule ccontr) -apply (subgoal_tac "a \ x & x \ b") - prefer 2 - apply simp - apply (drule_tac P = "%d. 0 ?P d" and x = 1 in spec, arith) -apply (drule_tac x = x in spec)+ -apply simp -apply (drule_tac P = "%r. ?P r --> (\s>0. ?Q r s) " and x = "\y - f x\" 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 \ aa", simp_all) -done - -lemma IVT2: "[| f(b::real) \ (y::real); y \ f(a); - a \ b; - (\x. a \ x & x \ b --> isCont f x) - |] ==> \x. a \ x & x \ b & f(x) = y" -apply (subgoal_tac "- f a \ -y & -y \ - 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) \ (y::real) & y \ f(b) & a \ b & (\x. a \ x & x \ 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 \ 'a::metric_space" - assumes ab: "a \ b" and fa: "f a \ e1" and fb: "f b \ e2" - and dst: "\e x. a <= x \ x <= b \ 0 < e ==> \d > 0. \y. abs(y - x) < d \ dist(f y) (f x) < e" - and e1: "\y \ e1. \e > 0. \y'. dist y' y < e \ y' \ e1" - and e2: "\y \ e2. \e > 0. \y'. dist y' y < e \ y' \ e2" - and e12: "~(\x \ a. x <= b \ f x \ e1 \ f x \ e2)" - shows "\x \ a. x <= b \ f x \ e1 \ f x \ e2" (is "\ x. ?P x") -proof - - let ?S = "{c. \x \ a. x <= c \ f x \ e1}" - have Se: " \x. x \ ?S" - apply (rule exI[where x=a]) - apply (auto simp add: fa) - done - have Sub: "\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 \ l" "l \ 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: "\z \ a. z < l \ f z \ 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: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith - have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith - have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp - then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast - { assume le2: "f l \ e2" - from le2 fa fb e12 alb have la: "l \ 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" "\y. dist y (f l) < e \ y \ e2" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - let ?d' = "min (d/2) ((l - a)/2)" - have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) - by (simp add: min_max.less_infI2) - then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto - then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis - from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto - moreover - have "f (l - d') \ 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 \ e1" - from le1 fa fb e12 alb have lb: "l \ 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" "\y. dist y (f l) < e \ y \ e1" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp - then have "\d'. d' < d \ d' >0" using d(1) by blast - then obtain d' where d': "d' > 0" "d' < d" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto - then have "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto - with ale1 have "\y. a \ y \ y \ l + d' \ f y \ 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 \ open A \ open B \ S \ A \ B \ A \ B \ S = {} \ A \ S = {} \ B \ 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 \ e2 \ s = {}" "s \ e1 \ e2" - assume "e1 \ s \ {}" "e2 \ s \ {}" - then obtain x1 x2 where x1:"x1\e1" "x1\s" and x2:"x2\e2" "x2\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 \ x" "x \ 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 "\y - x\ < 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 "\d>0. \y. \y - x\ < d \ 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 "\x\0. x \ 1 \ (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1 \ (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" - apply (rule connected_real_lemma) - apply (simp add: `x1\e1` `x2\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\0" "x\1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ 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 \ B \ s = {}" "s \ A \ B" + moreover + assume "A \ s \ {}" "B \ s \ {}" + then obtain a b where a: "a \ A" "a \ s" and b: "b \ B" "b \ s" by auto + def f \ "\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 \ A \ f ` {0 .. 1}" + using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def) + moreover have "b \ B \ f ` {0 .. 1}" + using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def) + moreover have "f ` {0 .. 1} \ 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 \ - ~(\e1 e2. open e1 \ open e2 \ S \ (e1 \ e2) \ (e1 \ e2 \ S = {}) - \ ~(e1 \ S = {}) \ ~(e2 \ S = {}))" - lemma connected_local: "connected S \ ~(\e1 e2. openin (subtopology euclidean S) e1 \ 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: "\a\A. x < a" + shows "Inf A \ A" +proof + assume "Inf A \ A" + then obtain b where "b < Inf A" "{b <.. Inf A} \ 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 \ A" + by (auto simp: subset_eq) + then show False + using cInf_lower[OF `c \ A`, of x] bnd by (metis less_imp_le not_le) +qed + +lemma Sup_notin_open: + assumes A: "open A" and bnd: "\a\A. a < x" + shows "Sup A \ A" +proof + assume "Sup A \ A" + then obtain b where "Sup A < b" "{Sup A ..< b} \ 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 \ A" + by (auto simp: subset_eq) + then show False + using cSup_upper[OF `c \ A`, of x] bnd by (metis less_imp_le not_le) +qed + end + +lemma connectedI_interval: + fixes U :: "'a :: linear_continuum_topology set" + assumes *: "\x y z. x \ U \ y \ U \ x \ z \ z \ y \ z \ U" + shows "connected U" +proof (rule connectedI) + { fix A B assume "open A" "open B" "A \ B \ U = {}" "U \ A \ B" + fix x y assume "x < y" "x \ A" "y \ B" "x \ U" "y \ U" + + let ?z = "Inf (B \ {x <..})" + + have "x \ ?z" "?z \ y" + using `y \ B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest) + with `x \ U` `y \ U` have "?z \ U" + by (rule *) + moreover have "?z \ B \ {x <..}" + using `open B` by (intro Inf_notin_open) auto + ultimately have "?z \ A" + using `x \ ?z` `A \ B \ U = {}` `x \ A` `U \ A \ B` by auto + + { assume "?z < y" + obtain a where "?z < a" "{?z ..< a} \ A" + using open_right[OF `open A` `?z \ A` `?z < y`] by auto + moreover obtain b where "b \ B" "x < b" "b < min a y" + using cInf_less_iff[of "B \ {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \ B` + by (auto intro: less_imp_le) + moreover then have "?z \ b" + by (intro cInf_lower[where z=x]) auto + moreover have "b \ U" + using `x \ ?z` `?z \ b` `b < min a y` + by (intro *[OF `x \ U` `y \ U`]) (auto simp: less_imp_le) + ultimately have "\b\B. b \ A \ b \ U" + by (intro bexI[of _ b]) auto } + then have False + using `?z \ y` `?z \ A` `y \ B` `y \ U` `A \ B \ U = {}` unfolding le_less by blast } + note not_disjoint = this + + fix A B assume AB: "open A" "open B" "U \ A \ B" "A \ B \ U = {}" + moreover assume "A \ U \ {}" then obtain x where x: "x \ U" "x \ A" by auto + moreover assume "B \ U \ {}" then obtain y where y: "y \ U" "y \ 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 \ (\x\U. \y\U. \z. x \ z \ z \ y \ z \ 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 \ A" "b \ A" shows "{a <..< b} \ 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 \ 'b :: linorder_topology" + assumes y: "f a \ y" "y \ f b" "a \ b" + assumes *: "continuous_on {a .. b} f" + shows "\x. a \ x \ x \ b \ 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 \ 'b :: linorder_topology" + assumes y: "f b \ y" "y \ f a" "a \ b" + assumes *: "continuous_on {a .. b} f" + shows "\x. a \ x \ x \ b \ 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 \ 'b :: linorder_topology" + shows "f a \ y \ y \ f b \ a \ b \ (\x. a \ x \ x \ b \ isCont f x) \ \x. a \ x \ x \ b \ f x = y" + by (rule IVT') (auto intro: continuous_at_imp_continuous_on) + +lemma IVT2: + fixes f :: "'a :: linear_continuum_topology \ 'b :: linorder_topology" + shows "f b \ y \ y \ f a \ a \ b \ (\x. a \ x \ x \ b \ isCont f x) \ \x. a \ x \ x \ b \ 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 \ S" shows "\b>x. {x ..< b} \ S" +lemma (in linorder_topology) open_right: + assumes "open S" "x \ S" and gt_ex: "x < y" shows "\b>x. {x ..< b} \ S" using assms unfolding open_generated_order proof induction case (Int A B) then obtain a b where "a > x" "{x ..< a} \ A" "b > x" "{x ..< b} \ 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 \ S" shows "\b S" +lemma (in linorder_topology) open_left: + assumes "open S" "x \ S" and lt_ex: "y < x" shows "\b S" using assms unfolding open_generated_order proof induction case (Int A B) then obtain a b where "a < x" "{a <.. x} \ A" "b < x" "{b <.. x} \ 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) \ (\b. x < b \ (\z. x < z \ z < b \ P z))" unfolding eventually_nhds eventually_within at_def proof safe - fix S assume "open S" "x \ S" - note open_right[OF this] + from gt_ex[of x] guess y .. + moreover fix S assume "open S" "x \ S" note open_right[OF this, of y] + moreover note gt_ex[of x] moreover assume "\s\S. s \ - {x} \ s \ {x<..} \ P s" ultimately show "\b>x. \z. x < z \ z < b \ P z" by (auto simp: subset_eq Ball_def) @@ -760,8 +753,8 @@ shows "eventually P (at_left x) \ (\b. x > b \ (\z. b < z \ z < x \ P z))" unfolding eventually_nhds eventually_within at_def proof safe - fix S assume "open S" "x \ S" - note open_left[OF this] + from lt_ex[of x] guess y .. + moreover fix S assume "open S" "x \ S" note open_left[OF this, of y] moreover assume "\s\S. s \ - {x} \ s \ {.. P s" ultimately show "\bz. b < z \ z < x \ P z" by (auto simp: subset_eq Ball_def) @@ -1482,7 +1475,7 @@ (\S. open S \ x \ S \ eventually (\i. A i \ 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 \ F i" using nhds(2) by (auto simp: F_def) next fix S assume "open S" "x \ S" @@ -1873,5 +1866,65 @@ shows "compact s \ s \ {} \ continuous_on s f \ (\x\s. \y\s. f x \ 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 \ + \ (\A B. open A \ open B \ S \ A \ B \ A \ B \ S = {} \ A \ S \ {} \ B \ S \ {})" + +lemma connectedI: + "(\A B. open A \ open B \ A \ U \ {} \ B \ U \ {} \ A \ B \ U = {} \ U \ A \ B \ False) + \ 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 \ U" "y \ U" and "x \ z" "z \ y" + shows "z \ U" +proof - + have eq: "{.. {z<..} = - {z}" + by auto + { assume "z \ U" "x < z" "z < y" + with xy have "\ 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 \ 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 \ f ` s \ {}" and B: "open B" "B \ f ` s \ {}" and + AB: "A \ B \ f ` s = {}" "f ` s \ A \ B" + obtain A' where A': "open A'" "f -` A \ s = A' \ s" + using * `open A` unfolding continuous_on_open_invariant by metis + obtain B' where B': "open B'" "f -` B \ s = B' \ s" + using * `open B` unfolding continuous_on_open_invariant by metis + + have "\A B. open A \ open B \ s \ A \ B \ A \ B \ s = {} \ A \ s \ {} \ B \ s \ {}" + proof (rule exI[of _ A'], rule exI[of _ B'], intro conjI) + have "s \ (f -` A \ s) \ (f -` B \ s)" using AB by auto + then show "s \ A' \ B'" using A' B' by auto + next + have "(f -` A \ s) \ (f -` B \ s) = {}" using AB by auto + then show "A' \ B' \ 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: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" assumes 3: "\x. \d>0. \a b. a \ x & x \ b & (b-a) < d \ 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*}