--- 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))
--- 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. *}
--- 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>
--- 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
--- 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
+
--- 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*}