separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
authorhoelzl
Tue Mar 26 12:20:52 2013 +0100 (2013-03-26)
changeset 515186a56b7088a6a
parent 51517 7957d26c3334
child 51519 2831ce75ec49
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
src/HOL/Complex_Main.thy
src/HOL/Conditional_Complete_Lattices.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/RComplete.thy
src/HOL/RealDef.thy
src/HOL/RealVector.thy
src/HOL/SupInf.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Mon Mar 25 20:00:27 2013 +0100
     1.2 +++ b/src/HOL/Complex_Main.thy	Tue Mar 26 12:20:52 2013 +0100
     1.3 @@ -4,7 +4,6 @@
     1.4  imports
     1.5    Main
     1.6    Real
     1.7 -  SupInf
     1.8    Complex
     1.9    Log
    1.10    Ln
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Conditional_Complete_Lattices.thy	Tue Mar 26 12:20:52 2013 +0100
     2.3 @@ -0,0 +1,295 @@
     2.4 +(*  Title:      HOL/Conditional_Complete_Lattices.thy
     2.5 +    Author:     Amine Chaieb and L C Paulson, University of Cambridge
     2.6 +    Author:     Johanens Hölzl, TU München
     2.7 +*)
     2.8 +
     2.9 +header {* Conditional Complete Lattices *}
    2.10 +
    2.11 +theory Conditional_Complete_Lattices
    2.12 +imports Main Lubs
    2.13 +begin
    2.14 +
    2.15 +lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
    2.16 +  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
    2.17 +
    2.18 +lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
    2.19 +  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
    2.20 +
    2.21 +text {*
    2.22 +
    2.23 +To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
    2.24 +@{const Inf} in theorem names with c.
    2.25 +
    2.26 +*}
    2.27 +
    2.28 +class conditional_complete_lattice = lattice + Sup + Inf +
    2.29 +  assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
    2.30 +    and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
    2.31 +  assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
    2.32 +    and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
    2.33 +begin
    2.34 +
    2.35 +lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
    2.36 +  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
    2.37 +  by (blast intro: antisym cSup_upper cSup_least)
    2.38 +
    2.39 +lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
    2.40 +  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
    2.41 +  by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
    2.42 +
    2.43 +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)"
    2.44 +  by (metis order_trans cSup_upper cSup_least)
    2.45 +
    2.46 +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)"
    2.47 +  by (metis order_trans cInf_lower cInf_greatest)
    2.48 +
    2.49 +lemma cSup_singleton [simp]: "Sup {x} = x"
    2.50 +  by (intro cSup_eq_maximum) auto
    2.51 +
    2.52 +lemma cInf_singleton [simp]: "Inf {x} = x"
    2.53 +  by (intro cInf_eq_minimum) auto
    2.54 +
    2.55 +lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
    2.56 +  "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
    2.57 +  by (metis cSup_upper order_trans)
    2.58 + 
    2.59 +lemma cInf_lower2:
    2.60 +  "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
    2.61 +  by (metis cInf_lower order_trans)
    2.62 +
    2.63 +lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
    2.64 +  by (blast intro: cSup_upper)
    2.65 +
    2.66 +lemma cInf_lower_EX:  "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
    2.67 +  by (blast intro: cInf_lower)
    2.68 +
    2.69 +lemma cSup_eq_non_empty:
    2.70 +  assumes 1: "X \<noteq> {}"
    2.71 +  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
    2.72 +  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
    2.73 +  shows "Sup X = a"
    2.74 +  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
    2.75 +
    2.76 +lemma cInf_eq_non_empty:
    2.77 +  assumes 1: "X \<noteq> {}"
    2.78 +  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
    2.79 +  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
    2.80 +  shows "Inf X = a"
    2.81 +  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
    2.82 +
    2.83 +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}"
    2.84 +  by (rule cInf_eq_non_empty) (auto intro: cSup_upper cSup_least)
    2.85 +
    2.86 +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}"
    2.87 +  by (rule cSup_eq_non_empty) (auto intro: cInf_lower cInf_greatest)
    2.88 +
    2.89 +lemma cSup_insert: 
    2.90 +  assumes x: "X \<noteq> {}"
    2.91 +      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    2.92 +  shows "Sup (insert a X) = sup a (Sup X)"
    2.93 +proof (intro cSup_eq_non_empty)
    2.94 +  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)
    2.95 +qed (auto intro: le_supI2 z cSup_upper)
    2.96 +
    2.97 +lemma cInf_insert: 
    2.98 +  assumes x: "X \<noteq> {}"
    2.99 +      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   2.100 +  shows "Inf (insert a X) = inf a (Inf X)"
   2.101 +proof (intro cInf_eq_non_empty)
   2.102 +  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)
   2.103 +qed (auto intro: le_infI2 z cInf_lower)
   2.104 +
   2.105 +lemma cSup_insert_If: 
   2.106 +  "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
   2.107 +  using cSup_insert[of X z] by simp
   2.108 +
   2.109 +lemma cInf_insert_if: 
   2.110 +  "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
   2.111 +  using cInf_insert[of X z] by simp
   2.112 +
   2.113 +lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
   2.114 +proof (induct X arbitrary: x rule: finite_induct)
   2.115 +  case (insert x X y) then show ?case
   2.116 +    apply (cases "X = {}")
   2.117 +    apply simp
   2.118 +    apply (subst cSup_insert[of _ "Sup X"])
   2.119 +    apply (auto intro: le_supI2)
   2.120 +    done
   2.121 +qed simp
   2.122 +
   2.123 +lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
   2.124 +proof (induct X arbitrary: x rule: finite_induct)
   2.125 +  case (insert x X y) then show ?case
   2.126 +    apply (cases "X = {}")
   2.127 +    apply simp
   2.128 +    apply (subst cInf_insert[of _ "Inf X"])
   2.129 +    apply (auto intro: le_infI2)
   2.130 +    done
   2.131 +qed simp
   2.132 +
   2.133 +lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
   2.134 +proof (induct X rule: finite_ne_induct)
   2.135 +  case (insert x X) then show ?case
   2.136 +    using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
   2.137 +qed simp
   2.138 +
   2.139 +lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
   2.140 +proof (induct X rule: finite_ne_induct)
   2.141 +  case (insert x X) then show ?case
   2.142 +    using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
   2.143 +qed simp
   2.144 +
   2.145 +lemma cSup_atMost[simp]: "Sup {..x} = x"
   2.146 +  by (auto intro!: cSup_eq_maximum)
   2.147 +
   2.148 +lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
   2.149 +  by (auto intro!: cSup_eq_maximum)
   2.150 +
   2.151 +lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
   2.152 +  by (auto intro!: cSup_eq_maximum)
   2.153 +
   2.154 +lemma cInf_atLeast[simp]: "Inf {x..} = x"
   2.155 +  by (auto intro!: cInf_eq_minimum)
   2.156 +
   2.157 +lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
   2.158 +  by (auto intro!: cInf_eq_minimum)
   2.159 +
   2.160 +lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
   2.161 +  by (auto intro!: cInf_eq_minimum)
   2.162 +
   2.163 +end
   2.164 +
   2.165 +instance complete_lattice \<subseteq> conditional_complete_lattice
   2.166 +  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
   2.167 +
   2.168 +lemma isLub_cSup: 
   2.169 +  "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   2.170 +  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
   2.171 +            intro!: setgeI intro: cSup_upper cSup_least)
   2.172 +
   2.173 +lemma cSup_eq:
   2.174 +  fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
   2.175 +  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
   2.176 +  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
   2.177 +  shows "Sup X = a"
   2.178 +proof cases
   2.179 +  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
   2.180 +qed (intro cSup_eq_non_empty assms)
   2.181 +
   2.182 +lemma cInf_eq:
   2.183 +  fixes a :: "'a :: {conditional_complete_lattice, no_top}"
   2.184 +  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
   2.185 +  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
   2.186 +  shows "Inf X = a"
   2.187 +proof cases
   2.188 +  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
   2.189 +qed (intro cInf_eq_non_empty assms)
   2.190 +
   2.191 +lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   2.192 +  by (metis cSup_least setle_def)
   2.193 +
   2.194 +lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   2.195 +  by (metis cInf_greatest setge_def)
   2.196 +
   2.197 +class conditional_complete_linorder = conditional_complete_lattice + linorder
   2.198 +begin
   2.199 +
   2.200 +lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
   2.201 +  "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
   2.202 +  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
   2.203 +
   2.204 +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)"
   2.205 +  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
   2.206 +
   2.207 +lemma less_cSupE:
   2.208 +  assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
   2.209 +  by (metis cSup_least assms not_le that)
   2.210 +
   2.211 +lemma less_cSupD:
   2.212 +  "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
   2.213 +  by (metis less_cSup_iff not_leE)
   2.214 +
   2.215 +lemma cInf_lessD:
   2.216 +  "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
   2.217 +  by (metis cInf_less_iff not_leE)
   2.218 +
   2.219 +lemma complete_interval:
   2.220 +  assumes "a < b" and "P a" and "\<not> P b"
   2.221 +  shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
   2.222 +             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
   2.223 +proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   2.224 +  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   2.225 +    by (rule cSup_upper [where z=b], auto)
   2.226 +       (metis `a < b` `\<not> P b` linear less_le)
   2.227 +next
   2.228 +  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   2.229 +    apply (rule cSup_least) 
   2.230 +    apply auto
   2.231 +    apply (metis less_le_not_le)
   2.232 +    apply (metis `a<b` `~ P b` linear less_le)
   2.233 +    done
   2.234 +next
   2.235 +  fix x
   2.236 +  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   2.237 +  show "P x"
   2.238 +    apply (rule less_cSupE [OF lt], auto)
   2.239 +    apply (metis less_le_not_le)
   2.240 +    apply (metis x) 
   2.241 +    done
   2.242 +next
   2.243 +  fix d
   2.244 +    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
   2.245 +    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   2.246 +      by (rule_tac z="b" in cSup_upper, auto) 
   2.247 +         (metis `a<b` `~ P b` linear less_le)
   2.248 +qed
   2.249 +
   2.250 +end
   2.251 +
   2.252 +lemma cSup_bounds:
   2.253 +  fixes S :: "'a :: conditional_complete_lattice set"
   2.254 +  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   2.255 +  shows "a \<le> Sup S \<and> Sup S \<le> b"
   2.256 +proof-
   2.257 +  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
   2.258 +  hence b: "Sup S \<le> b" using u 
   2.259 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
   2.260 +  from Se obtain y where y: "y \<in> S" by blast
   2.261 +  from lub l have "a \<le> Sup S"
   2.262 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   2.263 +       (metis le_iff_sup le_sup_iff y)
   2.264 +  with b show ?thesis by blast
   2.265 +qed
   2.266 +
   2.267 +
   2.268 +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"
   2.269 +  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
   2.270 +
   2.271 +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"
   2.272 +  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
   2.273 +
   2.274 +lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
   2.275 +  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
   2.276 +
   2.277 +lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
   2.278 +  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
   2.279 +
   2.280 +lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   2.281 +  by (auto intro!: cSup_eq_non_empty intro: dense_le)
   2.282 +
   2.283 +lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   2.284 +  by (auto intro!: cSup_eq intro: dense_le_bounded)
   2.285 +
   2.286 +lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   2.287 +  by (auto intro!: cSup_eq intro: dense_le_bounded)
   2.288 +
   2.289 +lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
   2.290 +  by (auto intro!: cInf_eq intro: dense_ge)
   2.291 +
   2.292 +lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
   2.293 +  by (auto intro!: cInf_eq intro: dense_ge_bounded)
   2.294 +
   2.295 +lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
   2.296 +  by (auto intro!: cInf_eq intro: dense_ge_bounded)
   2.297 +
   2.298 +end
     3.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 25 20:00:27 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 26 12:20:52 2013 +0100
     3.3 @@ -8,17 +8,56 @@
     3.4    "~~/src/HOL/Library/Indicator_Function"
     3.5  begin
     3.6  
     3.7 -lemma cSup_finite_ge_iff: 
     3.8 +lemma cSup_abs_le: (* TODO: is this really needed? *)
     3.9 +  fixes S :: "real set"
    3.10 +  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
    3.11 +by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
    3.12 +
    3.13 +lemma cInf_abs_ge: (* TODO: is this really needed? *)
    3.14 +  fixes S :: "real set"
    3.15 +  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
    3.16 +by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
    3.17 +
    3.18 +lemma cSup_asclose: (* TODO: is this really needed? *)
    3.19    fixes S :: "real set"
    3.20 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
    3.21 -  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
    3.22 -by (metis Max_ge Se cSup_eq_Max Max_in fS linorder_not_le less_le_trans)
    3.23 +  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
    3.24 +proof-
    3.25 +  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
    3.26 +  thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
    3.27 +    by  (auto simp add: setge_def setle_def)
    3.28 +qed
    3.29 +
    3.30 +lemma cInf_asclose: (* TODO: is this really needed? *)
    3.31 +  fixes S :: "real set"
    3.32 +  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
    3.33 +proof -
    3.34 +  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
    3.35 +    by auto
    3.36 +  also have "... \<le> e" 
    3.37 +    apply (rule cSup_asclose) 
    3.38 +    apply (auto simp add: S)
    3.39 +    apply (metis abs_minus_add_cancel b add_commute diff_minus)
    3.40 +    done
    3.41 +  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
    3.42 +  thus ?thesis
    3.43 +    by (simp add: Inf_real_def)
    3.44 +qed
    3.45 +
    3.46 +lemma cSup_finite_ge_iff: 
    3.47 +  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
    3.48 +  by (metis cSup_eq_Max Max_ge_iff)
    3.49  
    3.50  lemma cSup_finite_le_iff: 
    3.51 -  fixes S :: "real set"
    3.52 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
    3.53 -  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    3.54 -by (metis Max_ge Se cSup_eq_Max Max_in fS order_trans)
    3.55 +  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
    3.56 +  by (metis cSup_eq_Max Max_le_iff)
    3.57 +
    3.58 +lemma cInf_finite_ge_iff: 
    3.59 +  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
    3.60 +  by (metis cInf_eq_Min Min_ge_iff)
    3.61 +
    3.62 +lemma cInf_finite_le_iff: 
    3.63 +  fixes S :: "real set" shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
    3.64 +  by (metis cInf_eq_Min Min_le_iff)
    3.65  
    3.66  lemma Inf: (* rename *)
    3.67    fixes S :: "real set"
    3.68 @@ -6282,7 +6321,8 @@
    3.69        unfolding real_norm_def abs_le_iff
    3.70        apply auto
    3.71        done
    3.72 -    show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially"
    3.73 +
    3.74 +    show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
    3.75      proof (rule LIMSEQ_I)
    3.76        case goal1
    3.77        hence "0<r/2" by auto
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 25 20:00:27 2013 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 26 12:20:52 2013 +0100
     4.3 @@ -1374,34 +1374,33 @@
     4.4    by (simp add: sequentially_imp_eventually_within)
     4.5  
     4.6  lemma Lim_right_bound:
     4.7 -  fixes f :: "real \<Rightarrow> real"
     4.8 +  fixes f :: "'a :: {linorder_topology, conditional_complete_linorder, no_top} \<Rightarrow>
     4.9 +    'b::{linorder_topology, conditional_complete_linorder}"
    4.10    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"
    4.11    assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
    4.12    shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
    4.13  proof cases
    4.14    assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
    4.15  next
    4.16 -  assume [simp]: "{x<..} \<inter> I \<noteq> {}"
    4.17 +  assume e: "{x<..} \<inter> I \<noteq> {}"
    4.18    show ?thesis
    4.19 -  proof (rule Lim_within_LIMSEQ, safe)
    4.20 -    fix S assume S: "\<forall>n. S n \<noteq> x \<and> S n \<in> {x <..} \<inter> I" "S ----> x"
    4.21 -    
    4.22 -    show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
    4.23 -    proof (rule LIMSEQ_I, rule ccontr)
    4.24 -      fix r :: real assume "0 < r"
    4.25 -      with cInf_close[of "f ` ({x<..} \<inter> I)" r]
    4.26 -      obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
    4.27 -      from `x < y` have "0 < y - x" by auto
    4.28 -      from S(2)[THEN LIMSEQ_D, OF this]
    4.29 -      obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>S n - x\<bar> < y - x" by auto
    4.30 -      
    4.31 -      assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
    4.32 -      moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
    4.33 -        using S bnd by (intro cInf_lower[where z=K]) auto
    4.34 -      ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
    4.35 -        by (auto simp: not_less field_simps)
    4.36 -      with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
    4.37 -      show False by auto
    4.38 +  proof (rule order_tendstoI)
    4.39 +    fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))"
    4.40 +    { fix y assume "y \<in> {x<..} \<inter> I"
    4.41 +      with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
    4.42 +        by (auto intro: cInf_lower)
    4.43 +      with a have "a < f y" by (blast intro: less_le_trans) }
    4.44 +    then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
    4.45 +      by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
    4.46 +  next
    4.47 +    fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
    4.48 +    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
    4.49 +    show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
    4.50 +      unfolding within_within_eq[symmetric]
    4.51 +        Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
    4.52 +    proof (safe intro!: exI[of _ y] y)
    4.53 +      fix z assume "x < z" "z \<in> I" "z < y"
    4.54 +      with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
    4.55      qed
    4.56    qed
    4.57  qed
    4.58 @@ -1718,12 +1717,11 @@
    4.59      using cInf_lower_EX[of _ S] assms by metis
    4.60  
    4.61    fix e :: real assume "0 < e"
    4.62 -  then obtain x where x: "x \<in> S" "x < Inf S + e"
    4.63 -    using cInf_close `S \<noteq> {}` by auto
    4.64 -  moreover then have "x > Inf S - e" using * by auto
    4.65 -  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
    4.66 -  then show "\<exists>x\<in>S. dist x (Inf S) < e"
    4.67 -    using x by (auto simp: dist_norm)
    4.68 +  then have "Inf S < Inf S + e" by simp
    4.69 +  with assms obtain x where "x \<in> S" "x < Inf S + e"
    4.70 +    by (subst (asm) cInf_less_iff[of _ B]) auto
    4.71 +  with * show "\<exists>x\<in>S. dist x (Inf S) < e"
    4.72 +    by (intro bexI[of _ x]) (auto simp add: dist_real_def)
    4.73  qed
    4.74  
    4.75  lemma closed_contains_Inf:
     5.1 --- a/src/HOL/RComplete.thy	Mon Mar 25 20:00:27 2013 +0100
     5.2 +++ b/src/HOL/RComplete.thy	Tue Mar 26 12:20:52 2013 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  header {* Completeness of the Reals; Floor and Ceiling Functions *}
     5.5  
     5.6  theory RComplete
     5.7 -imports Lubs RealDef
     5.8 +imports Conditional_Complete_Lattices RealDef
     5.9  begin
    5.10  
    5.11  lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
     6.1 --- a/src/HOL/RealDef.thy	Mon Mar 25 20:00:27 2013 +0100
     6.2 +++ b/src/HOL/RealDef.thy	Tue Mar 26 12:20:52 2013 +0100
     6.3 @@ -8,7 +8,7 @@
     6.4  header {* Development of the Reals using Cauchy Sequences *}
     6.5  
     6.6  theory RealDef
     6.7 -imports Rat
     6.8 +imports Rat Conditional_Complete_Lattices
     6.9  begin
    6.10  
    6.11  text {*
    6.12 @@ -922,6 +922,56 @@
    6.13      using 1 2 3 by (rule_tac x="Real B" in exI, simp)
    6.14  qed
    6.15  
    6.16 +
    6.17 +instantiation real :: conditional_complete_linorder
    6.18 +begin
    6.19 +
    6.20 +subsection{*Supremum of a set of reals*}
    6.21 +
    6.22 +definition
    6.23 +  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
    6.24 +
    6.25 +definition
    6.26 +  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
    6.27 +
    6.28 +instance
    6.29 +proof
    6.30 +  { fix z x :: real and X :: "real set"
    6.31 +    assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    6.32 +    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"
    6.33 +      using complete_real[of X] by blast
    6.34 +    then show "x \<le> Sup X"
    6.35 +      unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) }
    6.36 +  note Sup_upper = this
    6.37 +
    6.38 +  { fix z :: real and X :: "real set"
    6.39 +    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    6.40 +    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"
    6.41 +      using complete_real[of X] by blast
    6.42 +    then have "Sup X = s"
    6.43 +      unfolding Sup_real_def by (best intro: Least_equality)  
    6.44 +    also with s z have "... \<le> z"
    6.45 +      by blast
    6.46 +    finally show "Sup X \<le> z" . }
    6.47 +  note Sup_least = this
    6.48 +
    6.49 +  { fix x z :: real and X :: "real set"
    6.50 +    assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    6.51 +    have "-x \<le> Sup (uminus ` X)"
    6.52 +      by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
    6.53 +    then show "Inf X \<le> x" 
    6.54 +      by (auto simp add: Inf_real_def) }
    6.55 +
    6.56 +  { fix z :: real and X :: "real set"
    6.57 +    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    6.58 +    have "Sup (uminus ` X) \<le> -z"
    6.59 +      using x z by (force intro: Sup_least)
    6.60 +    then show "z \<le> Inf X" 
    6.61 +        by (auto simp add: Inf_real_def) }
    6.62 +qed
    6.63 +end
    6.64 +
    6.65 +
    6.66  subsection {* Hiding implementation details *}
    6.67  
    6.68  hide_const (open) vanishes cauchy positive Real
    6.69 @@ -1525,7 +1575,6 @@
    6.70  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
    6.71  by simp
    6.72  
    6.73 -
    6.74  subsection {* Implementation of rational real numbers *}
    6.75  
    6.76  text {* Formal constructor *}
     7.1 --- a/src/HOL/RealVector.thy	Mon Mar 25 20:00:27 2013 +0100
     7.2 +++ b/src/HOL/RealVector.thy	Tue Mar 26 12:20:52 2013 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Vector Spaces and Algebras over the Reals *}
     7.5  
     7.6  theory RealVector
     7.7 -imports RComplete Metric_Spaces SupInf
     7.8 +imports Metric_Spaces
     7.9  begin
    7.10  
    7.11  subsection {* Locale for additive functions *}
    7.12 @@ -685,6 +685,8 @@
    7.13  
    7.14  end
    7.15  
    7.16 +instance real :: linear_continuum_topology ..
    7.17 +
    7.18  subsection {* Extra type constraints *}
    7.19  
    7.20  text {* Only allow @{term "open"} in class @{text topological_space}. *}
    7.21 @@ -917,180 +919,4 @@
    7.22      by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
    7.23  qed
    7.24  
    7.25 -section {* Connectedness *}
    7.26 -
    7.27 -class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
    7.28 -begin
    7.29 -
    7.30 -lemma Inf_notin_open:
    7.31 -  assumes A: "open A" and bnd: "\<forall>a\<in>A. x < a"
    7.32 -  shows "Inf A \<notin> A"
    7.33 -proof
    7.34 -  assume "Inf A \<in> A"
    7.35 -  then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A"
    7.36 -    using open_left[of A "Inf A" x] assms by auto
    7.37 -  with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
    7.38 -    by (auto simp: subset_eq)
    7.39 -  then show False
    7.40 -    using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    7.41 -qed
    7.42 -
    7.43 -lemma Sup_notin_open:
    7.44 -  assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x"
    7.45 -  shows "Sup A \<notin> A"
    7.46 -proof
    7.47 -  assume "Sup A \<in> A"
    7.48 -  then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A"
    7.49 -    using open_right[of A "Sup A" x] assms by auto
    7.50 -  with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
    7.51 -    by (auto simp: subset_eq)
    7.52 -  then show False
    7.53 -    using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    7.54 -qed
    7.55 -
    7.56  end
    7.57 -
    7.58 -instance real :: linear_continuum_topology ..
    7.59 -
    7.60 -lemma connectedI_interval:
    7.61 -  fixes U :: "'a :: linear_continuum_topology set"
    7.62 -  assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    7.63 -  shows "connected U"
    7.64 -proof (rule connectedI)
    7.65 -  { fix A B assume "open A" "open B" "A \<inter> B \<inter> U = {}" "U \<subseteq> A \<union> B"
    7.66 -    fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U"
    7.67 -
    7.68 -    let ?z = "Inf (B \<inter> {x <..})"
    7.69 -
    7.70 -    have "x \<le> ?z" "?z \<le> y"
    7.71 -      using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
    7.72 -    with `x \<in> U` `y \<in> U` have "?z \<in> U"
    7.73 -      by (rule *)
    7.74 -    moreover have "?z \<notin> B \<inter> {x <..}"
    7.75 -      using `open B` by (intro Inf_notin_open) auto
    7.76 -    ultimately have "?z \<in> A"
    7.77 -      using `x \<le> ?z` `A \<inter> B \<inter> U = {}` `x \<in> A` `U \<subseteq> A \<union> B` by auto
    7.78 -
    7.79 -    { assume "?z < y"
    7.80 -      obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
    7.81 -        using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
    7.82 -      moreover obtain b where "b \<in> B" "x < b" "b < min a y"
    7.83 -        using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
    7.84 -        by (auto intro: less_imp_le)
    7.85 -      moreover then have "?z \<le> b"
    7.86 -        by (intro cInf_lower[where z=x]) auto
    7.87 -      moreover have "b \<in> U"
    7.88 -        using `x \<le> ?z` `?z \<le> b` `b < min a y`
    7.89 -        by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)
    7.90 -      ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U"
    7.91 -        by (intro bexI[of _ b]) auto }
    7.92 -    then have False
    7.93 -      using `?z \<le> y` `?z \<in> A` `y \<in> B` `y \<in> U` `A \<inter> B \<inter> U = {}` unfolding le_less by blast }
    7.94 -  note not_disjoint = this
    7.95 -
    7.96 -  fix A B assume AB: "open A" "open B" "U \<subseteq> A \<union> B" "A \<inter> B \<inter> U = {}"
    7.97 -  moreover assume "A \<inter> U \<noteq> {}" then obtain x where x: "x \<in> U" "x \<in> A" by auto
    7.98 -  moreover assume "B \<inter> U \<noteq> {}" then obtain y where y: "y \<in> U" "y \<in> B" by auto
    7.99 -  moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
   7.100 -  ultimately show False by (cases x y rule: linorder_cases) auto
   7.101 -qed
   7.102 -
   7.103 -lemma connected_iff_interval:
   7.104 -  fixes U :: "'a :: linear_continuum_topology set"
   7.105 -  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)"
   7.106 -  by (auto intro: connectedI_interval dest: connectedD_interval)
   7.107 -
   7.108 -lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
   7.109 -  unfolding connected_iff_interval by auto
   7.110 -
   7.111 -lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
   7.112 -  unfolding connected_iff_interval by auto
   7.113 -
   7.114 -lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
   7.115 -  unfolding connected_iff_interval by auto
   7.116 -
   7.117 -lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
   7.118 -  unfolding connected_iff_interval by auto
   7.119 -
   7.120 -lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
   7.121 -  unfolding connected_iff_interval by auto
   7.122 -
   7.123 -lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
   7.124 -  unfolding connected_iff_interval by auto
   7.125 -
   7.126 -lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
   7.127 -  unfolding connected_iff_interval by auto
   7.128 -
   7.129 -lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
   7.130 -  unfolding connected_iff_interval by auto
   7.131 -
   7.132 -lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
   7.133 -  unfolding connected_iff_interval by auto
   7.134 -
   7.135 -lemma connected_contains_Ioo: 
   7.136 -  fixes A :: "'a :: linorder_topology set"
   7.137 -  assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
   7.138 -  using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
   7.139 -
   7.140 -subsection {* Intermediate Value Theorem *}
   7.141 -
   7.142 -lemma IVT':
   7.143 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   7.144 -  assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
   7.145 -  assumes *: "continuous_on {a .. b} f"
   7.146 -  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   7.147 -proof -
   7.148 -  have "connected {a..b}"
   7.149 -    unfolding connected_iff_interval by auto
   7.150 -  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
   7.151 -  show ?thesis
   7.152 -    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
   7.153 -qed
   7.154 -
   7.155 -lemma IVT2':
   7.156 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   7.157 -  assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
   7.158 -  assumes *: "continuous_on {a .. b} f"
   7.159 -  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   7.160 -proof -
   7.161 -  have "connected {a..b}"
   7.162 -    unfolding connected_iff_interval by auto
   7.163 -  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
   7.164 -  show ?thesis
   7.165 -    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
   7.166 -qed
   7.167 -
   7.168 -lemma IVT:
   7.169 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   7.170 -  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"
   7.171 -  by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
   7.172 -
   7.173 -lemma IVT2:
   7.174 -  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   7.175 -  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"
   7.176 -  by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
   7.177 -
   7.178 -lemma continuous_inj_imp_mono:
   7.179 -  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   7.180 -  assumes x: "a < x" "x < b"
   7.181 -  assumes cont: "continuous_on {a..b} f"
   7.182 -  assumes inj: "inj_on f {a..b}"
   7.183 -  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
   7.184 -proof -
   7.185 -  note I = inj_on_iff[OF inj]
   7.186 -  { assume "f x < f a" "f x < f b"
   7.187 -    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"
   7.188 -      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
   7.189 -      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
   7.190 -    with x I have False by auto }
   7.191 -  moreover
   7.192 -  { assume "f a < f x" "f b < f x"
   7.193 -    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"
   7.194 -      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
   7.195 -      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
   7.196 -    with x I have False by auto }
   7.197 -  ultimately show ?thesis
   7.198 -    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)
   7.199 -qed
   7.200 -
   7.201 -end
     8.1 --- a/src/HOL/SupInf.thy	Mon Mar 25 20:00:27 2013 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,433 +0,0 @@
     8.4 -(*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
     8.5 -
     8.6 -header {*Sup and Inf Operators on Sets of Reals.*}
     8.7 -
     8.8 -theory SupInf
     8.9 -imports RComplete
    8.10 -begin
    8.11 -
    8.12 -lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
    8.13 -  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
    8.14 -
    8.15 -lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
    8.16 -  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
    8.17 -
    8.18 -text {*
    8.19 -
    8.20 -To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
    8.21 -@{const Inf} in theorem names with c.
    8.22 -
    8.23 -*}
    8.24 -
    8.25 -class conditional_complete_lattice = lattice + Sup + Inf +
    8.26 -  assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
    8.27 -    and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
    8.28 -  assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
    8.29 -    and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
    8.30 -begin
    8.31 -
    8.32 -lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
    8.33 -  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
    8.34 -  by (blast intro: antisym cSup_upper cSup_least)
    8.35 -
    8.36 -lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
    8.37 -  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
    8.38 -  by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
    8.39 -
    8.40 -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)"
    8.41 -  by (metis order_trans cSup_upper cSup_least)
    8.42 -
    8.43 -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)"
    8.44 -  by (metis order_trans cInf_lower cInf_greatest)
    8.45 -
    8.46 -lemma cSup_singleton [simp]: "Sup {x} = x"
    8.47 -  by (intro cSup_eq_maximum) auto
    8.48 -
    8.49 -lemma cInf_singleton [simp]: "Inf {x} = x"
    8.50 -  by (intro cInf_eq_minimum) auto
    8.51 -
    8.52 -lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
    8.53 -  "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
    8.54 -  by (metis cSup_upper order_trans)
    8.55 - 
    8.56 -lemma cInf_lower2:
    8.57 -  "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
    8.58 -  by (metis cInf_lower order_trans)
    8.59 -
    8.60 -lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
    8.61 -  by (blast intro: cSup_upper)
    8.62 -
    8.63 -lemma cInf_lower_EX:  "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
    8.64 -  by (blast intro: cInf_lower)
    8.65 -
    8.66 -lemma cSup_eq_non_empty:
    8.67 -  assumes 1: "X \<noteq> {}"
    8.68 -  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
    8.69 -  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
    8.70 -  shows "Sup X = a"
    8.71 -  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
    8.72 -
    8.73 -lemma cInf_eq_non_empty:
    8.74 -  assumes 1: "X \<noteq> {}"
    8.75 -  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
    8.76 -  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
    8.77 -  shows "Inf X = a"
    8.78 -  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
    8.79 -
    8.80 -lemma cSup_insert: 
    8.81 -  assumes x: "X \<noteq> {}"
    8.82 -      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    8.83 -  shows "Sup (insert a X) = sup a (Sup X)"
    8.84 -proof (intro cSup_eq_non_empty)
    8.85 -  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)
    8.86 -qed (auto intro: le_supI2 z cSup_upper)
    8.87 -
    8.88 -lemma cInf_insert: 
    8.89 -  assumes x: "X \<noteq> {}"
    8.90 -      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    8.91 -  shows "Inf (insert a X) = inf a (Inf X)"
    8.92 -proof (intro cInf_eq_non_empty)
    8.93 -  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)
    8.94 -qed (auto intro: le_infI2 z cInf_lower)
    8.95 -
    8.96 -lemma cSup_insert_If: 
    8.97 -  "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
    8.98 -  using cSup_insert[of X z] by simp
    8.99 -
   8.100 -lemma cInf_insert_if: 
   8.101 -  "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
   8.102 -  using cInf_insert[of X z] by simp
   8.103 -
   8.104 -lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
   8.105 -proof (induct X arbitrary: x rule: finite_induct)
   8.106 -  case (insert x X y) then show ?case
   8.107 -    apply (cases "X = {}")
   8.108 -    apply simp
   8.109 -    apply (subst cSup_insert[of _ "Sup X"])
   8.110 -    apply (auto intro: le_supI2)
   8.111 -    done
   8.112 -qed simp
   8.113 -
   8.114 -lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
   8.115 -proof (induct X arbitrary: x rule: finite_induct)
   8.116 -  case (insert x X y) then show ?case
   8.117 -    apply (cases "X = {}")
   8.118 -    apply simp
   8.119 -    apply (subst cInf_insert[of _ "Inf X"])
   8.120 -    apply (auto intro: le_infI2)
   8.121 -    done
   8.122 -qed simp
   8.123 -
   8.124 -lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
   8.125 -proof (induct X rule: finite_ne_induct)
   8.126 -  case (insert x X) then show ?case
   8.127 -    using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
   8.128 -qed simp
   8.129 -
   8.130 -lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
   8.131 -proof (induct X rule: finite_ne_induct)
   8.132 -  case (insert x X) then show ?case
   8.133 -    using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
   8.134 -qed simp
   8.135 -
   8.136 -lemma cSup_atMost[simp]: "Sup {..x} = x"
   8.137 -  by (auto intro!: cSup_eq_maximum)
   8.138 -
   8.139 -lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
   8.140 -  by (auto intro!: cSup_eq_maximum)
   8.141 -
   8.142 -lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
   8.143 -  by (auto intro!: cSup_eq_maximum)
   8.144 -
   8.145 -lemma cInf_atLeast[simp]: "Inf {x..} = x"
   8.146 -  by (auto intro!: cInf_eq_minimum)
   8.147 -
   8.148 -lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
   8.149 -  by (auto intro!: cInf_eq_minimum)
   8.150 -
   8.151 -lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
   8.152 -  by (auto intro!: cInf_eq_minimum)
   8.153 -
   8.154 -end
   8.155 -
   8.156 -instance complete_lattice \<subseteq> conditional_complete_lattice
   8.157 -  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
   8.158 -
   8.159 -lemma isLub_cSup: 
   8.160 -  "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   8.161 -  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
   8.162 -            intro!: setgeI intro: cSup_upper cSup_least)
   8.163 -
   8.164 -lemma cSup_eq:
   8.165 -  fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
   8.166 -  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
   8.167 -  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
   8.168 -  shows "Sup X = a"
   8.169 -proof cases
   8.170 -  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
   8.171 -qed (intro cSup_eq_non_empty assms)
   8.172 -
   8.173 -lemma cInf_eq:
   8.174 -  fixes a :: "'a :: {conditional_complete_lattice, no_top}"
   8.175 -  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
   8.176 -  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
   8.177 -  shows "Inf X = a"
   8.178 -proof cases
   8.179 -  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
   8.180 -qed (intro cInf_eq_non_empty assms)
   8.181 -
   8.182 -lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   8.183 -  by (metis cSup_least setle_def)
   8.184 -
   8.185 -lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   8.186 -  by (metis cInf_greatest setge_def)
   8.187 -
   8.188 -class conditional_complete_linorder = conditional_complete_lattice + linorder
   8.189 -begin
   8.190 -
   8.191 -lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
   8.192 -  "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
   8.193 -  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
   8.194 -
   8.195 -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)"
   8.196 -  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
   8.197 -
   8.198 -lemma less_cSupE:
   8.199 -  assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
   8.200 -  by (metis cSup_least assms not_le that)
   8.201 -
   8.202 -lemma complete_interval:
   8.203 -  assumes "a < b" and "P a" and "\<not> P b"
   8.204 -  shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
   8.205 -             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
   8.206 -proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   8.207 -  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   8.208 -    by (rule cSup_upper [where z=b], auto)
   8.209 -       (metis `a < b` `\<not> P b` linear less_le)
   8.210 -next
   8.211 -  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   8.212 -    apply (rule cSup_least) 
   8.213 -    apply auto
   8.214 -    apply (metis less_le_not_le)
   8.215 -    apply (metis `a<b` `~ P b` linear less_le)
   8.216 -    done
   8.217 -next
   8.218 -  fix x
   8.219 -  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   8.220 -  show "P x"
   8.221 -    apply (rule less_cSupE [OF lt], auto)
   8.222 -    apply (metis less_le_not_le)
   8.223 -    apply (metis x) 
   8.224 -    done
   8.225 -next
   8.226 -  fix d
   8.227 -    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
   8.228 -    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   8.229 -      by (rule_tac z="b" in cSup_upper, auto) 
   8.230 -         (metis `a<b` `~ P b` linear less_le)
   8.231 -qed
   8.232 -
   8.233 -end
   8.234 -
   8.235 -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"
   8.236 -  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
   8.237 -
   8.238 -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"
   8.239 -  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
   8.240 -
   8.241 -lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
   8.242 -  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
   8.243 -
   8.244 -lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
   8.245 -  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
   8.246 -
   8.247 -lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   8.248 -  by (auto intro!: cSup_eq_non_empty intro: dense_le)
   8.249 -
   8.250 -lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   8.251 -  by (auto intro!: cSup_eq intro: dense_le_bounded)
   8.252 -
   8.253 -lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   8.254 -  by (auto intro!: cSup_eq intro: dense_le_bounded)
   8.255 -
   8.256 -lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
   8.257 -  by (auto intro!: cInf_eq intro: dense_ge)
   8.258 -
   8.259 -lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
   8.260 -  by (auto intro!: cInf_eq intro: dense_ge_bounded)
   8.261 -
   8.262 -lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
   8.263 -  by (auto intro!: cInf_eq intro: dense_ge_bounded)
   8.264 -
   8.265 -instantiation real :: conditional_complete_linorder
   8.266 -begin
   8.267 -
   8.268 -subsection{*Supremum of a set of reals*}
   8.269 -
   8.270 -definition
   8.271 -  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
   8.272 -
   8.273 -definition
   8.274 -  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
   8.275 -
   8.276 -instance
   8.277 -proof
   8.278 -  { fix z x :: real and X :: "real set"
   8.279 -    assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   8.280 -    show "x \<le> Sup X"
   8.281 -    proof (auto simp add: Sup_real_def) 
   8.282 -      from complete_real[of X]
   8.283 -      obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   8.284 -        by (blast intro: x z)
   8.285 -      hence "x \<le> s"
   8.286 -        by (blast intro: x z)
   8.287 -      also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
   8.288 -        by (fast intro: Least_equality [symmetric])  
   8.289 -      finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
   8.290 -    qed }
   8.291 -  note Sup_upper = this
   8.292 -
   8.293 -  { fix z :: real and X :: "real set"
   8.294 -    assume x: "X \<noteq> {}"
   8.295 -        and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   8.296 -    show "Sup X \<le> z"
   8.297 -    proof (auto simp add: Sup_real_def) 
   8.298 -      from complete_real x
   8.299 -      obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   8.300 -        by (blast intro: z)
   8.301 -      hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
   8.302 -        by (best intro: Least_equality)  
   8.303 -      also with s z have "... \<le> z"
   8.304 -        by blast
   8.305 -      finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
   8.306 -    qed }
   8.307 -  note Sup_least = this
   8.308 -
   8.309 -  { fix x z :: real and X :: "real set"
   8.310 -    assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   8.311 -    show "Inf X \<le> x"
   8.312 -    proof -
   8.313 -      have "-x \<le> Sup (uminus ` X)"
   8.314 -        by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
   8.315 -      thus ?thesis 
   8.316 -        by (auto simp add: Inf_real_def)
   8.317 -    qed }
   8.318 -
   8.319 -  { fix z :: real and X :: "real set"
   8.320 -    assume x: "X \<noteq> {}"
   8.321 -      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   8.322 -    show "z \<le> Inf X"
   8.323 -    proof -
   8.324 -      have "Sup (uminus ` X) \<le> -z"
   8.325 -        using x z by (force intro: Sup_least)
   8.326 -      hence "z \<le> - Sup (uminus ` X)"
   8.327 -        by simp
   8.328 -      thus ?thesis 
   8.329 -        by (auto simp add: Inf_real_def)
   8.330 -    qed }
   8.331 -qed
   8.332 -end
   8.333 -
   8.334 -subsection{*Supremum of a set of reals*}
   8.335 -
   8.336 -lemma cSup_abs_le:
   8.337 -  fixes S :: "real set"
   8.338 -  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
   8.339 -by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
   8.340 -
   8.341 -lemma cSup_bounds:
   8.342 -  fixes S :: "real set"
   8.343 -  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   8.344 -  shows "a \<le> Sup S \<and> Sup S \<le> b"
   8.345 -proof-
   8.346 -  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
   8.347 -  hence b: "Sup S \<le> b" using u 
   8.348 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
   8.349 -  from Se obtain y where y: "y \<in> S" by blast
   8.350 -  from lub l have "a \<le> Sup S"
   8.351 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   8.352 -       (metis le_iff_sup le_sup_iff y)
   8.353 -  with b show ?thesis by blast
   8.354 -qed
   8.355 -
   8.356 -lemma cSup_asclose: 
   8.357 -  fixes S :: "real set"
   8.358 -  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
   8.359 -proof-
   8.360 -  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
   8.361 -  thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
   8.362 -    by  (auto simp add: setge_def setle_def)
   8.363 -qed
   8.364 -
   8.365 -subsection{*Infimum of a set of reals*}
   8.366 -
   8.367 -lemma cInf_greater:
   8.368 -  fixes z :: real
   8.369 -  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
   8.370 -  by (metis cInf_less_iff not_leE)
   8.371 -
   8.372 -lemma cInf_close:
   8.373 -  fixes e :: real
   8.374 -  shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
   8.375 -  by (metis add_strict_increasing add_commute cInf_greater linorder_not_le pos_add_strict)
   8.376 -
   8.377 -lemma cInf_finite_in: 
   8.378 -  fixes S :: "real set"
   8.379 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   8.380 -  shows "Inf S \<in> S"
   8.381 -  using cInf_eq_Min[OF fS Se] Min_in[OF fS Se] by metis
   8.382 -
   8.383 -lemma cInf_finite_ge_iff: 
   8.384 -  fixes S :: "real set"
   8.385 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   8.386 -by (metis cInf_eq_Min cInf_finite_in Min_le order_trans)
   8.387 -
   8.388 -lemma cInf_finite_le_iff:
   8.389 -  fixes S :: "real set"
   8.390 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   8.391 -by (metis cInf_eq_Min cInf_finite_ge_iff cInf_finite_in Min_le order_antisym linear)
   8.392 -
   8.393 -lemma cInf_finite_gt_iff: 
   8.394 -  fixes S :: "real set"
   8.395 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   8.396 -by (metis cInf_finite_le_iff linorder_not_less)
   8.397 -
   8.398 -lemma cInf_finite_lt_iff: 
   8.399 -  fixes S :: "real set"
   8.400 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   8.401 -by (metis cInf_finite_ge_iff linorder_not_less)
   8.402 -
   8.403 -lemma cInf_abs_ge:
   8.404 -  fixes S :: "real set"
   8.405 -  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
   8.406 -by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
   8.407 -
   8.408 -lemma cInf_asclose:
   8.409 -  fixes S :: "real set"
   8.410 -  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
   8.411 -proof -
   8.412 -  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
   8.413 -    by auto
   8.414 -  also have "... \<le> e" 
   8.415 -    apply (rule cSup_asclose) 
   8.416 -    apply (auto simp add: S)
   8.417 -    apply (metis abs_minus_add_cancel b add_commute diff_minus)
   8.418 -    done
   8.419 -  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   8.420 -  thus ?thesis
   8.421 -    by (simp add: Inf_real_def)
   8.422 -qed
   8.423 -
   8.424 -subsection{*Relate max and min to Sup and Inf.*}
   8.425 -
   8.426 -lemma real_max_cSup:
   8.427 -  fixes x :: real
   8.428 -  shows "max x y = Sup {x,y}"
   8.429 -  by (subst cSup_insert[of _ y]) (simp_all add: sup_max)
   8.430 -
   8.431 -lemma real_min_cInf: 
   8.432 -  fixes x :: real
   8.433 -  shows "min x y = Inf {x,y}"
   8.434 -  by (subst cInf_insert[of _ y]) (simp_all add: inf_min)
   8.435 -
   8.436 -end
     9.1 --- a/src/HOL/Topological_Spaces.thy	Mon Mar 25 20:00:27 2013 +0100
     9.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Mar 26 12:20:52 2013 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Topological Spaces *}
     9.5  
     9.6  theory Topological_Spaces
     9.7 -imports Main
     9.8 +imports Main Conditional_Complete_Lattices
     9.9  begin
    9.10  
    9.11  subsection {* Topological space *}
    9.12 @@ -2062,5 +2062,180 @@
    9.13      unfolding connected_def by blast
    9.14  qed
    9.15  
    9.16 +
    9.17 +section {* Connectedness *}
    9.18 +
    9.19 +class linear_continuum_topology = linorder_topology + conditional_complete_linorder + inner_dense_linorder
    9.20 +begin
    9.21 +
    9.22 +lemma Inf_notin_open:
    9.23 +  assumes A: "open A" and bnd: "\<forall>a\<in>A. x < a"
    9.24 +  shows "Inf A \<notin> A"
    9.25 +proof
    9.26 +  assume "Inf A \<in> A"
    9.27 +  then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A"
    9.28 +    using open_left[of A "Inf A" x] assms by auto
    9.29 +  with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A"
    9.30 +    by (auto simp: subset_eq)
    9.31 +  then show False
    9.32 +    using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    9.33 +qed
    9.34 +
    9.35 +lemma Sup_notin_open:
    9.36 +  assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x"
    9.37 +  shows "Sup A \<notin> A"
    9.38 +proof
    9.39 +  assume "Sup A \<in> A"
    9.40 +  then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A"
    9.41 +    using open_right[of A "Sup A" x] assms by auto
    9.42 +  with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A"
    9.43 +    by (auto simp: subset_eq)
    9.44 +  then show False
    9.45 +    using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le)
    9.46 +qed
    9.47 +
    9.48  end
    9.49  
    9.50 +lemma connectedI_interval:
    9.51 +  fixes U :: "'a :: linear_continuum_topology set"
    9.52 +  assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    9.53 +  shows "connected U"
    9.54 +proof (rule connectedI)
    9.55 +  { fix A B assume "open A" "open B" "A \<inter> B \<inter> U = {}" "U \<subseteq> A \<union> B"
    9.56 +    fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U"
    9.57 +
    9.58 +    let ?z = "Inf (B \<inter> {x <..})"
    9.59 +
    9.60 +    have "x \<le> ?z" "?z \<le> y"
    9.61 +      using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest)
    9.62 +    with `x \<in> U` `y \<in> U` have "?z \<in> U"
    9.63 +      by (rule *)
    9.64 +    moreover have "?z \<notin> B \<inter> {x <..}"
    9.65 +      using `open B` by (intro Inf_notin_open) auto
    9.66 +    ultimately have "?z \<in> A"
    9.67 +      using `x \<le> ?z` `A \<inter> B \<inter> U = {}` `x \<in> A` `U \<subseteq> A \<union> B` by auto
    9.68 +
    9.69 +    { assume "?z < y"
    9.70 +      obtain a where "?z < a" "{?z ..< a} \<subseteq> A"
    9.71 +        using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto
    9.72 +      moreover obtain b where "b \<in> B" "x < b" "b < min a y"
    9.73 +        using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
    9.74 +        by (auto intro: less_imp_le)
    9.75 +      moreover then have "?z \<le> b"
    9.76 +        by (intro cInf_lower[where z=x]) auto
    9.77 +      moreover have "b \<in> U"
    9.78 +        using `x \<le> ?z` `?z \<le> b` `b < min a y`
    9.79 +        by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le)
    9.80 +      ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U"
    9.81 +        by (intro bexI[of _ b]) auto }
    9.82 +    then have False
    9.83 +      using `?z \<le> y` `?z \<in> A` `y \<in> B` `y \<in> U` `A \<inter> B \<inter> U = {}` unfolding le_less by blast }
    9.84 +  note not_disjoint = this
    9.85 +
    9.86 +  fix A B assume AB: "open A" "open B" "U \<subseteq> A \<union> B" "A \<inter> B \<inter> U = {}"
    9.87 +  moreover assume "A \<inter> U \<noteq> {}" then obtain x where x: "x \<in> U" "x \<in> A" by auto
    9.88 +  moreover assume "B \<inter> U \<noteq> {}" then obtain y where y: "y \<in> U" "y \<in> B" by auto
    9.89 +  moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
    9.90 +  ultimately show False by (cases x y rule: linorder_cases) auto
    9.91 +qed
    9.92 +
    9.93 +lemma connected_iff_interval:
    9.94 +  fixes U :: "'a :: linear_continuum_topology set"
    9.95 +  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)"
    9.96 +  by (auto intro: connectedI_interval dest: connectedD_interval)
    9.97 +
    9.98 +lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
    9.99 +  unfolding connected_iff_interval by auto
   9.100 +
   9.101 +lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
   9.102 +  unfolding connected_iff_interval by auto
   9.103 +
   9.104 +lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
   9.105 +  unfolding connected_iff_interval by auto
   9.106 +
   9.107 +lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
   9.108 +  unfolding connected_iff_interval by auto
   9.109 +
   9.110 +lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
   9.111 +  unfolding connected_iff_interval by auto
   9.112 +
   9.113 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
   9.114 +  unfolding connected_iff_interval by auto
   9.115 +
   9.116 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
   9.117 +  unfolding connected_iff_interval by auto
   9.118 +
   9.119 +lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
   9.120 +  unfolding connected_iff_interval by auto
   9.121 +
   9.122 +lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
   9.123 +  unfolding connected_iff_interval by auto
   9.124 +
   9.125 +lemma connected_contains_Ioo: 
   9.126 +  fixes A :: "'a :: linorder_topology set"
   9.127 +  assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
   9.128 +  using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
   9.129 +
   9.130 +subsection {* Intermediate Value Theorem *}
   9.131 +
   9.132 +lemma IVT':
   9.133 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   9.134 +  assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
   9.135 +  assumes *: "continuous_on {a .. b} f"
   9.136 +  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   9.137 +proof -
   9.138 +  have "connected {a..b}"
   9.139 +    unfolding connected_iff_interval by auto
   9.140 +  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
   9.141 +  show ?thesis
   9.142 +    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
   9.143 +qed
   9.144 +
   9.145 +lemma IVT2':
   9.146 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   9.147 +  assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
   9.148 +  assumes *: "continuous_on {a .. b} f"
   9.149 +  shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   9.150 +proof -
   9.151 +  have "connected {a..b}"
   9.152 +    unfolding connected_iff_interval by auto
   9.153 +  from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
   9.154 +  show ?thesis
   9.155 +    by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
   9.156 +qed
   9.157 +
   9.158 +lemma IVT:
   9.159 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   9.160 +  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"
   9.161 +  by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
   9.162 +
   9.163 +lemma IVT2:
   9.164 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   9.165 +  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"
   9.166 +  by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
   9.167 +
   9.168 +lemma continuous_inj_imp_mono:
   9.169 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   9.170 +  assumes x: "a < x" "x < b"
   9.171 +  assumes cont: "continuous_on {a..b} f"
   9.172 +  assumes inj: "inj_on f {a..b}"
   9.173 +  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
   9.174 +proof -
   9.175 +  note I = inj_on_iff[OF inj]
   9.176 +  { assume "f x < f a" "f x < f b"
   9.177 +    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"
   9.178 +      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
   9.179 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
   9.180 +    with x I have False by auto }
   9.181 +  moreover
   9.182 +  { assume "f a < f x" "f b < f x"
   9.183 +    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"
   9.184 +      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
   9.185 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
   9.186 +    with x I have False by auto }
   9.187 +  ultimately show ?thesis
   9.188 +    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)
   9.189 +qed
   9.190 +
   9.191 +end
   9.192 +