# HG changeset patch
# User hoelzl
# Date 1364296852 -3600
# Node ID 6a56b7088a6ab16b3bce2b00b33e32ba198666a7
# Parent  7957d26c3334269feb9d3912918ee42d1a0a6118
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef

diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Complex_Main.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -4,7 +4,6 @@
 imports
   Main
   Real
-  SupInf
   Complex
   Log
   Ln
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/Conditional_Complete_Lattices.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Conditional_Complete_Lattices.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -0,0 +1,295 @@
+(*  Title:      HOL/Conditional_Complete_Lattices.thy
+    Author:     Amine Chaieb and L C Paulson, University of Cambridge
+    Author:     Johanens Hölzl, TU München
+*)
+
+header {* Conditional Complete Lattices *}
+
+theory Conditional_Complete_Lattices
+imports Main Lubs
+begin
+
+lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
+  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
+
+lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
+  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
+
+text {*
+
+To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
+@{const Inf} in theorem names with c.
+
+*}
+
+class conditional_complete_lattice = lattice + Sup + Inf +
+  assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
+    and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
+  assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
+    and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
+begin
+
+lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
+  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
+  by (blast intro: antisym cSup_upper cSup_least)
+
+lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
+  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
+  by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
+
+lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
+  by (metis order_trans cSup_upper cSup_least)
+
+lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
+  by (metis order_trans cInf_lower cInf_greatest)
+
+lemma cSup_singleton [simp]: "Sup {x} = x"
+  by (intro cSup_eq_maximum) auto
+
+lemma cInf_singleton [simp]: "Inf {x} = x"
+  by (intro cInf_eq_minimum) auto
+
+lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
+  "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
+  by (metis cSup_upper order_trans)
+ 
+lemma cInf_lower2:
+  "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
+  by (metis cInf_lower order_trans)
+
+lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
+  by (blast intro: cSup_upper)
+
+lemma cInf_lower_EX:  "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
+  by (blast intro: cInf_lower)
+
+lemma cSup_eq_non_empty:
+  assumes 1: "X \<noteq> {}"
+  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
+  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
+  shows "Sup X = a"
+  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
+
+lemma cInf_eq_non_empty:
+  assumes 1: "X \<noteq> {}"
+  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
+  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
+  shows "Inf X = a"
+  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
+
+lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}"
+  by (rule cInf_eq_non_empty) (auto intro: cSup_upper cSup_least)
+
+lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}"
+  by (rule cSup_eq_non_empty) (auto intro: cInf_lower cInf_greatest)
+
+lemma cSup_insert: 
+  assumes x: "X \<noteq> {}"
+      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+  shows "Sup (insert a X) = sup a (Sup X)"
+proof (intro cSup_eq_non_empty)
+  fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least)
+qed (auto intro: le_supI2 z cSup_upper)
+
+lemma cInf_insert: 
+  assumes x: "X \<noteq> {}"
+      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+  shows "Inf (insert a X) = inf a (Inf X)"
+proof (intro cInf_eq_non_empty)
+  fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest)
+qed (auto intro: le_infI2 z cInf_lower)
+
+lemma cSup_insert_If: 
+  "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
+  using cSup_insert[of X z] by simp
+
+lemma cInf_insert_if: 
+  "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
+  using cInf_insert[of X z] by simp
+
+lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
+proof (induct X arbitrary: x rule: finite_induct)
+  case (insert x X y) then show ?case
+    apply (cases "X = {}")
+    apply simp
+    apply (subst cSup_insert[of _ "Sup X"])
+    apply (auto intro: le_supI2)
+    done
+qed simp
+
+lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
+proof (induct X arbitrary: x rule: finite_induct)
+  case (insert x X y) then show ?case
+    apply (cases "X = {}")
+    apply simp
+    apply (subst cInf_insert[of _ "Inf X"])
+    apply (auto intro: le_infI2)
+    done
+qed simp
+
+lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
+proof (induct X rule: finite_ne_induct)
+  case (insert x X) then show ?case
+    using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
+qed simp
+
+lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
+proof (induct X rule: finite_ne_induct)
+  case (insert x X) then show ?case
+    using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
+qed simp
+
+lemma cSup_atMost[simp]: "Sup {..x} = x"
+  by (auto intro!: cSup_eq_maximum)
+
+lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
+  by (auto intro!: cSup_eq_maximum)
+
+lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
+  by (auto intro!: cSup_eq_maximum)
+
+lemma cInf_atLeast[simp]: "Inf {x..} = x"
+  by (auto intro!: cInf_eq_minimum)
+
+lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
+  by (auto intro!: cInf_eq_minimum)
+
+lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
+  by (auto intro!: cInf_eq_minimum)
+
+end
+
+instance complete_lattice \<subseteq> conditional_complete_lattice
+  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
+
+lemma isLub_cSup: 
+  "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
+  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
+            intro!: setgeI intro: cSup_upper cSup_least)
+
+lemma cSup_eq:
+  fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
+  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
+  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
+  shows "Sup X = a"
+proof cases
+  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
+qed (intro cSup_eq_non_empty assms)
+
+lemma cInf_eq:
+  fixes a :: "'a :: {conditional_complete_lattice, no_top}"
+  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
+  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
+  shows "Inf X = a"
+proof cases
+  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
+qed (intro cInf_eq_non_empty assms)
+
+lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+  by (metis cSup_least setle_def)
+
+lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+  by (metis cInf_greatest setge_def)
+
+class conditional_complete_linorder = conditional_complete_lattice + linorder
+begin
+
+lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
+  "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
+  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
+
+lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
+  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
+
+lemma less_cSupE:
+  assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
+  by (metis cSup_least assms not_le that)
+
+lemma less_cSupD:
+  "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
+  by (metis less_cSup_iff not_leE)
+
+lemma cInf_lessD:
+  "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
+  by (metis cInf_less_iff not_leE)
+
+lemma complete_interval:
+  assumes "a < b" and "P a" and "\<not> P b"
+  shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
+             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
+proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
+  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+    by (rule cSup_upper [where z=b], auto)
+       (metis `a < b` `\<not> P b` linear less_le)
+next
+  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
+    apply (rule cSup_least) 
+    apply auto
+    apply (metis less_le_not_le)
+    apply (metis `a<b` `~ P b` linear less_le)
+    done
+next
+  fix x
+  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+  show "P x"
+    apply (rule less_cSupE [OF lt], auto)
+    apply (metis less_le_not_le)
+    apply (metis x) 
+    done
+next
+  fix d
+    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
+    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+      by (rule_tac z="b" in cSup_upper, auto) 
+         (metis `a<b` `~ P b` linear less_le)
+qed
+
+end
+
+lemma cSup_bounds:
+  fixes S :: "'a :: conditional_complete_lattice set"
+  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
+  shows "a \<le> Sup S \<and> Sup S \<le> b"
+proof-
+  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
+  hence b: "Sup S \<le> b" using u 
+    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
+  from Se obtain y where y: "y \<in> S" by blast
+  from lub l have "a \<le> Sup S"
+    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+       (metis le_iff_sup le_sup_iff y)
+  with b show ?thesis by blast
+qed
+
+
+lemma cSup_unique: "(S::'a :: {conditional_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
+  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
+
+lemma cInf_unique: "b <=* (S::'a :: {conditional_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
+  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
+
+lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
+  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
+
+lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
+  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
+
+lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+  by (auto intro!: cSup_eq_non_empty intro: dense_le)
+
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+  by (auto intro!: cSup_eq intro: dense_le_bounded)
+
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
+  by (auto intro!: cSup_eq intro: dense_le_bounded)
+
+lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
+  by (auto intro!: cInf_eq intro: dense_ge)
+
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
+  by (auto intro!: cInf_eq intro: dense_ge_bounded)
+
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
+  by (auto intro!: cInf_eq intro: dense_ge_bounded)
+
+end
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -8,17 +8,56 @@
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
-lemma cSup_finite_ge_iff: 
+lemma cSup_abs_le: (* TODO: is this really needed? *)
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
+
+lemma cInf_abs_ge: (* TODO: is this really needed? *)
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
+by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
+
+lemma cSup_asclose: (* TODO: is this really needed? *)
   fixes S :: "real set"
-  assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
-by (metis Max_ge Se cSup_eq_Max Max_in fS linorder_not_le less_le_trans)
+  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
+proof-
+  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
+  thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
+    by  (auto simp add: setge_def setle_def)
+qed
+
+lemma cInf_asclose: (* TODO: is this really needed? *)
+  fixes S :: "real set"
+  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
+    by auto
+  also have "... \<le> e" 
+    apply (rule cSup_asclose) 
+    apply (auto simp add: S)
+    apply (metis abs_minus_add_cancel b add_commute diff_minus)
+    done
+  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
+  thus ?thesis
+    by (simp add: Inf_real_def)
+qed
+
+lemma cSup_finite_ge_iff: 
+  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
+  by (metis cSup_eq_Max Max_ge_iff)
 
 lemma cSup_finite_le_iff: 
-  fixes S :: "real set"
-  assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se cSup_eq_Max Max_in fS order_trans)
+  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
+  by (metis cSup_eq_Max Max_le_iff)
+
+lemma cInf_finite_ge_iff: 
+  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
+  by (metis cInf_eq_Min Min_ge_iff)
+
+lemma cInf_finite_le_iff: 
+  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
+  by (metis cInf_eq_Min Min_le_iff)
 
 lemma Inf: (* rename *)
   fixes S :: "real set"
@@ -6282,7 +6321,8 @@
       unfolding real_norm_def abs_le_iff
       apply auto
       done
-    show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially"
+
+    show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
     proof (rule LIMSEQ_I)
       case goal1
       hence "0<r/2" by auto
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -1374,34 +1374,33 @@
   by (simp add: sequentially_imp_eventually_within)
 
 lemma Lim_right_bound:
-  fixes f :: "real \<Rightarrow> real"
+  fixes f :: "'a :: {linorder_topology, conditional_complete_linorder, no_top} \<Rightarrow>
+    'b::{linorder_topology, conditional_complete_linorder}"
   assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
   assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
   shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
 proof cases
   assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
 next
-  assume [simp]: "{x<..} \<inter> I \<noteq> {}"
+  assume e: "{x<..} \<inter> I \<noteq> {}"
   show ?thesis
-  proof (rule Lim_within_LIMSEQ, safe)
-    fix S assume S: "\<forall>n. S n \<noteq> x \<and> S n \<in> {x <..} \<inter> I" "S ----> x"
-    
-    show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
-    proof (rule LIMSEQ_I, rule ccontr)
-      fix r :: real assume "0 < r"
-      with cInf_close[of "f ` ({x<..} \<inter> I)" r]
-      obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
-      from `x < y` have "0 < y - x" by auto
-      from S(2)[THEN LIMSEQ_D, OF this]
-      obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>S n - x\<bar> < y - x" by auto
-      
-      assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
-      moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
-        using S bnd by (intro cInf_lower[where z=K]) auto
-      ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
-        by (auto simp: not_less field_simps)
-      with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
-      show False by auto
+  proof (rule order_tendstoI)
+    fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))"
+    { fix y assume "y \<in> {x<..} \<inter> I"
+      with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
+        by (auto intro: cInf_lower)
+      with a have "a < f y" by (blast intro: less_le_trans) }
+    then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
+      by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
+  next
+    fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
+    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
+    show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
+      unfolding within_within_eq[symmetric]
+        Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
+    proof (safe intro!: exI[of _ y] y)
+      fix z assume "x < z" "z \<in> I" "z < y"
+      with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
     qed
   qed
 qed
@@ -1718,12 +1717,11 @@
     using cInf_lower_EX[of _ S] assms by metis
 
   fix e :: real assume "0 < e"
-  then obtain x where x: "x \<in> S" "x < Inf S + e"
-    using cInf_close `S \<noteq> {}` by auto
-  moreover then have "x > Inf S - e" using * by auto
-  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
-  then show "\<exists>x\<in>S. dist x (Inf S) < e"
-    using x by (auto simp: dist_norm)
+  then have "Inf S < Inf S + e" by simp
+  with assms obtain x where "x \<in> S" "x < Inf S + e"
+    by (subst (asm) cInf_less_iff[of _ B]) auto
+  with * show "\<exists>x\<in>S. dist x (Inf S) < e"
+    by (intro bexI[of _ x]) (auto simp add: dist_real_def)
 qed
 
 lemma closed_contains_Inf:
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/RComplete.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -8,7 +8,7 @@
 header {* Completeness of the Reals; Floor and Ceiling Functions *}
 
 theory RComplete
-imports Lubs RealDef
+imports Conditional_Complete_Lattices RealDef
 begin
 
 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/RealDef.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -8,7 +8,7 @@
 header {* Development of the Reals using Cauchy Sequences *}
 
 theory RealDef
-imports Rat
+imports Rat Conditional_Complete_Lattices
 begin
 
 text {*
@@ -922,6 +922,56 @@
     using 1 2 3 by (rule_tac x="Real B" in exI, simp)
 qed
 
+
+instantiation real :: conditional_complete_linorder
+begin
+
+subsection{*Supremum of a set of reals*}
+
+definition
+  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
+
+definition
+  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
+
+instance
+proof
+  { fix z x :: real and X :: "real set"
+    assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+    then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
+      using complete_real[of X] by blast
+    then show "x \<le> Sup X"
+      unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
+  note Sup_upper = this
+
+  { fix z :: real and X :: "real set"
+    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+    then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
+      using complete_real[of X] by blast
+    then have "Sup X = s"
+      unfolding Sup_real_def by (best intro: Least_equality)  
+    also with s z have "... \<le> z"
+      by blast
+    finally show "Sup X \<le> z" . }
+  note Sup_least = this
+
+  { fix x z :: real and X :: "real set"
+    assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+    have "-x \<le> Sup (uminus ` X)"
+      by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
+    then show "Inf X \<le> x" 
+      by (auto simp add: Inf_real_def) }
+
+  { fix z :: real and X :: "real set"
+    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+    have "Sup (uminus ` X) \<le> -z"
+      using x z by (force intro: Sup_least)
+    then show "z \<le> Inf X" 
+        by (auto simp add: Inf_real_def) }
+qed
+end
+
+
 subsection {* Hiding implementation details *}
 
 hide_const (open) vanishes cauchy positive Real
@@ -1525,7 +1575,6 @@
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 by simp
 
-
 subsection {* Implementation of rational real numbers *}
 
 text {* Formal constructor *}
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/RealVector.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -5,7 +5,7 @@
 header {* Vector Spaces and Algebras over the Reals *}
 
 theory RealVector
-imports RComplete Metric_Spaces SupInf
+imports Metric_Spaces
 begin
 
 subsection {* Locale for additive functions *}
@@ -685,6 +685,8 @@
 
 end
 
+instance real :: linear_continuum_topology ..
+
 subsection {* Extra type constraints *}
 
 text {* Only allow @{term "open"} in class @{text topological_space}. *}
@@ -917,180 +919,4 @@
     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
-
-instance real :: linear_continuum_topology ..
-
-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)
-
-lemma continuous_inj_imp_mono:
-  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
-  assumes x: "a < x" "x < b"
-  assumes cont: "continuous_on {a..b} f"
-  assumes inj: "inj_on f {a..b}"
-  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
-proof -
-  note I = inj_on_iff[OF inj]
-  { assume "f x < f a" "f x < f b"
-    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
-      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
-      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
-    with x I have False by auto }
-  moreover
-  { assume "f a < f x" "f b < f x"
-    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
-      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
-      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
-    with x I have False by auto }
-  ultimately show ?thesis
-    using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
-qed
-
-end
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Mon Mar 25 20:00:27 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,433 +0,0 @@
-(*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
-
-header {*Sup and Inf Operators on Sets of Reals.*}
-
-theory SupInf
-imports RComplete
-begin
-
-lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
-  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
-
-lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
-  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
-
-text {*
-
-To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
-@{const Inf} in theorem names with c.
-
-*}
-
-class conditional_complete_lattice = lattice + Sup + Inf +
-  assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
-    and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
-  assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
-    and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
-begin
-
-lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
-  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
-  by (blast intro: antisym cSup_upper cSup_least)
-
-lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
-  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
-  by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
-
-lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
-  by (metis order_trans cSup_upper cSup_least)
-
-lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
-  by (metis order_trans cInf_lower cInf_greatest)
-
-lemma cSup_singleton [simp]: "Sup {x} = x"
-  by (intro cSup_eq_maximum) auto
-
-lemma cInf_singleton [simp]: "Inf {x} = x"
-  by (intro cInf_eq_minimum) auto
-
-lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
-  "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
-  by (metis cSup_upper order_trans)
- 
-lemma cInf_lower2:
-  "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
-  by (metis cInf_lower order_trans)
-
-lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
-  by (blast intro: cSup_upper)
-
-lemma cInf_lower_EX:  "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
-  by (blast intro: cInf_lower)
-
-lemma cSup_eq_non_empty:
-  assumes 1: "X \<noteq> {}"
-  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
-  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
-  shows "Sup X = a"
-  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
-
-lemma cInf_eq_non_empty:
-  assumes 1: "X \<noteq> {}"
-  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
-  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
-  shows "Inf X = a"
-  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
-
-lemma cSup_insert: 
-  assumes x: "X \<noteq> {}"
-      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
-  shows "Sup (insert a X) = sup a (Sup X)"
-proof (intro cSup_eq_non_empty)
-  fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least)
-qed (auto intro: le_supI2 z cSup_upper)
-
-lemma cInf_insert: 
-  assumes x: "X \<noteq> {}"
-      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
-  shows "Inf (insert a X) = inf a (Inf X)"
-proof (intro cInf_eq_non_empty)
-  fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest)
-qed (auto intro: le_infI2 z cInf_lower)
-
-lemma cSup_insert_If: 
-  "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
-  using cSup_insert[of X z] by simp
-
-lemma cInf_insert_if: 
-  "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
-  using cInf_insert[of X z] by simp
-
-lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
-proof (induct X arbitrary: x rule: finite_induct)
-  case (insert x X y) then show ?case
-    apply (cases "X = {}")
-    apply simp
-    apply (subst cSup_insert[of _ "Sup X"])
-    apply (auto intro: le_supI2)
-    done
-qed simp
-
-lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
-proof (induct X arbitrary: x rule: finite_induct)
-  case (insert x X y) then show ?case
-    apply (cases "X = {}")
-    apply simp
-    apply (subst cInf_insert[of _ "Inf X"])
-    apply (auto intro: le_infI2)
-    done
-qed simp
-
-lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
-proof (induct X rule: finite_ne_induct)
-  case (insert x X) then show ?case
-    using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
-qed simp
-
-lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
-proof (induct X rule: finite_ne_induct)
-  case (insert x X) then show ?case
-    using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
-qed simp
-
-lemma cSup_atMost[simp]: "Sup {..x} = x"
-  by (auto intro!: cSup_eq_maximum)
-
-lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
-  by (auto intro!: cSup_eq_maximum)
-
-lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
-  by (auto intro!: cSup_eq_maximum)
-
-lemma cInf_atLeast[simp]: "Inf {x..} = x"
-  by (auto intro!: cInf_eq_minimum)
-
-lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
-  by (auto intro!: cInf_eq_minimum)
-
-lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
-  by (auto intro!: cInf_eq_minimum)
-
-end
-
-instance complete_lattice \<subseteq> conditional_complete_lattice
-  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
-
-lemma isLub_cSup: 
-  "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
-  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
-            intro!: setgeI intro: cSup_upper cSup_least)
-
-lemma cSup_eq:
-  fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
-  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
-  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
-  shows "Sup X = a"
-proof cases
-  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
-qed (intro cSup_eq_non_empty assms)
-
-lemma cInf_eq:
-  fixes a :: "'a :: {conditional_complete_lattice, no_top}"
-  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
-  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
-  shows "Inf X = a"
-proof cases
-  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
-qed (intro cInf_eq_non_empty assms)
-
-lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
-  by (metis cSup_least setle_def)
-
-lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
-  by (metis cInf_greatest setge_def)
-
-class conditional_complete_linorder = conditional_complete_lattice + linorder
-begin
-
-lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
-  "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
-  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
-
-lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
-  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
-
-lemma less_cSupE:
-  assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
-  by (metis cSup_least assms not_le that)
-
-lemma complete_interval:
-  assumes "a < b" and "P a" and "\<not> P b"
-  shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
-             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
-proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
-  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
-    by (rule cSup_upper [where z=b], auto)
-       (metis `a < b` `\<not> P b` linear less_le)
-next
-  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
-    apply (rule cSup_least) 
-    apply auto
-    apply (metis less_le_not_le)
-    apply (metis `a<b` `~ P b` linear less_le)
-    done
-next
-  fix x
-  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
-  show "P x"
-    apply (rule less_cSupE [OF lt], auto)
-    apply (metis less_le_not_le)
-    apply (metis x) 
-    done
-next
-  fix d
-    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
-    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
-      by (rule_tac z="b" in cSup_upper, auto) 
-         (metis `a<b` `~ P b` linear less_le)
-qed
-
-end
-
-lemma cSup_unique: "(S::'a :: {conditional_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
-  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
-
-lemma cInf_unique: "b <=* (S::'a :: {conditional_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
-  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
-
-lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
-  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
-
-lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
-  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
-
-lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
-  by (auto intro!: cSup_eq_non_empty intro: dense_le)
-
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
-  by (auto intro!: cSup_eq intro: dense_le_bounded)
-
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
-  by (auto intro!: cSup_eq intro: dense_le_bounded)
-
-lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
-  by (auto intro!: cInf_eq intro: dense_ge)
-
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
-  by (auto intro!: cInf_eq intro: dense_ge_bounded)
-
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
-  by (auto intro!: cInf_eq intro: dense_ge_bounded)
-
-instantiation real :: conditional_complete_linorder
-begin
-
-subsection{*Supremum of a set of reals*}
-
-definition
-  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
-
-definition
-  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
-
-instance
-proof
-  { fix z x :: real and X :: "real set"
-    assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
-    show "x \<le> Sup X"
-    proof (auto simp add: Sup_real_def) 
-      from complete_real[of X]
-      obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
-        by (blast intro: x z)
-      hence "x \<le> s"
-        by (blast intro: x z)
-      also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
-        by (fast intro: Least_equality [symmetric])  
-      finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
-    qed }
-  note Sup_upper = this
-
-  { fix z :: real and X :: "real set"
-    assume x: "X \<noteq> {}"
-        and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
-    show "Sup X \<le> z"
-    proof (auto simp add: Sup_real_def) 
-      from complete_real x
-      obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
-        by (blast intro: z)
-      hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
-        by (best intro: Least_equality)  
-      also with s z have "... \<le> z"
-        by blast
-      finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
-    qed }
-  note Sup_least = this
-
-  { fix x z :: real and X :: "real set"
-    assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
-    show "Inf X \<le> x"
-    proof -
-      have "-x \<le> Sup (uminus ` X)"
-        by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
-      thus ?thesis 
-        by (auto simp add: Inf_real_def)
-    qed }
-
-  { fix z :: real and X :: "real set"
-    assume x: "X \<noteq> {}"
-      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
-    show "z \<le> Inf X"
-    proof -
-      have "Sup (uminus ` X) \<le> -z"
-        using x z by (force intro: Sup_least)
-      hence "z \<le> - Sup (uminus ` X)"
-        by simp
-      thus ?thesis 
-        by (auto simp add: Inf_real_def)
-    qed }
-qed
-end
-
-subsection{*Supremum of a set of reals*}
-
-lemma cSup_abs_le:
-  fixes S :: "real set"
-  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
-by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
-
-lemma cSup_bounds:
-  fixes S :: "real set"
-  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
-  shows "a \<le> Sup S \<and> Sup S \<le> b"
-proof-
-  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
-  hence b: "Sup S \<le> b" using u 
-    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
-  from Se obtain y where y: "y \<in> S" by blast
-  from lub l have "a \<le> Sup S"
-    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
-       (metis le_iff_sup le_sup_iff y)
-  with b show ?thesis by blast
-qed
-
-lemma cSup_asclose: 
-  fixes S :: "real set"
-  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
-proof-
-  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
-  thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
-    by  (auto simp add: setge_def setle_def)
-qed
-
-subsection{*Infimum of a set of reals*}
-
-lemma cInf_greater:
-  fixes z :: real
-  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
-  by (metis cInf_less_iff not_leE)
-
-lemma cInf_close:
-  fixes e :: real
-  shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
-  by (metis add_strict_increasing add_commute cInf_greater linorder_not_le pos_add_strict)
-
-lemma cInf_finite_in: 
-  fixes S :: "real set"
-  assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "Inf S \<in> S"
-  using cInf_eq_Min[OF fS Se] Min_in[OF fS Se] by metis
-
-lemma cInf_finite_ge_iff: 
-  fixes S :: "real set"
-  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-by (metis cInf_eq_Min cInf_finite_in Min_le order_trans)
-
-lemma cInf_finite_le_iff:
-  fixes S :: "real set"
-  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
-by (metis cInf_eq_Min cInf_finite_ge_iff cInf_finite_in Min_le order_antisym linear)
-
-lemma cInf_finite_gt_iff: 
-  fixes S :: "real set"
-  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
-by (metis cInf_finite_le_iff linorder_not_less)
-
-lemma cInf_finite_lt_iff: 
-  fixes S :: "real set"
-  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
-by (metis cInf_finite_ge_iff linorder_not_less)
-
-lemma cInf_abs_ge:
-  fixes S :: "real set"
-  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
-by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
-
-lemma cInf_asclose:
-  fixes S :: "real set"
-  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
-proof -
-  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
-    by auto
-  also have "... \<le> e" 
-    apply (rule cSup_asclose) 
-    apply (auto simp add: S)
-    apply (metis abs_minus_add_cancel b add_commute diff_minus)
-    done
-  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
-  thus ?thesis
-    by (simp add: Inf_real_def)
-qed
-
-subsection{*Relate max and min to Sup and Inf.*}
-
-lemma real_max_cSup:
-  fixes x :: real
-  shows "max x y = Sup {x,y}"
-  by (subst cSup_insert[of _ y]) (simp_all add: sup_max)
-
-lemma real_min_cInf: 
-  fixes x :: real
-  shows "min x y = Inf {x,y}"
-  by (subst cInf_insert[of _ y]) (simp_all add: inf_min)
-
-end
diff -r 7957d26c3334 -r 6a56b7088a6a src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Mar 26 12:20:52 2013 +0100
@@ -6,7 +6,7 @@
 header {* Topological Spaces *}
 
 theory Topological_Spaces
-imports Main
+imports Main Conditional_Complete_Lattices
 begin
 
 subsection {* Topological space *}
@@ -2062,5 +2062,180 @@
     unfolding connected_def by blast
 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)
+
+lemma continuous_inj_imp_mono:
+  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+  assumes x: "a < x" "x < b"
+  assumes cont: "continuous_on {a..b} f"
+  assumes inj: "inj_on f {a..b}"
+  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
+proof -
+  note I = inj_on_iff[OF inj]
+  { assume "f x < f a" "f x < f b"
+    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
+      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
+      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+    with x I have False by auto }
+  moreover
+  { assume "f a < f x" "f b < f x"
+    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
+      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
+      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+    with x I have False by auto }
+  ultimately show ?thesis
+    using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
+qed
+
+end
+