1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Lubs_Glbs.thy Tue Nov 05 09:45:02 2013 +0100
1.3 @@ -0,0 +1,245 @@
1.4 +(* Title: HOL/Library/Lubs_Glbs.thy
1.5 + Author: Jacques D. Fleuriot, University of Cambridge
1.6 + Author: Amine Chaieb, University of Cambridge *)
1.7 +
1.8 +header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
1.9 +
1.10 +theory Lubs_Glbs
1.11 +imports Complex_Main
1.12 +begin
1.13 +
1.14 +text {* Thanks to suggestions by James Margetson *}
1.15 +
1.16 +definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70)
1.17 + where "S *<= x = (ALL y: S. y \<le> x)"
1.18 +
1.19 +definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70)
1.20 + where "x <=* S = (ALL y: S. x \<le> y)"
1.21 +
1.22 +
1.23 +subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
1.24 +
1.25 +lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
1.26 + by (simp add: setle_def)
1.27 +
1.28 +lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
1.29 + by (simp add: setle_def)
1.30 +
1.31 +lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
1.32 + by (simp add: setge_def)
1.33 +
1.34 +lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
1.35 + by (simp add: setge_def)
1.36 +
1.37 +
1.38 +definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.39 + where "leastP P x = (P x \<and> x <=* Collect P)"
1.40 +
1.41 +definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.42 + where "isUb R S x = (S *<= x \<and> x: R)"
1.43 +
1.44 +definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.45 + where "isLub R S x = leastP (isUb R S) x"
1.46 +
1.47 +definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
1.48 + where "ubs R S = Collect (isUb R S)"
1.49 +
1.50 +
1.51 +subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
1.52 +
1.53 +lemma leastPD1: "leastP P x \<Longrightarrow> P x"
1.54 + by (simp add: leastP_def)
1.55 +
1.56 +lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
1.57 + by (simp add: leastP_def)
1.58 +
1.59 +lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
1.60 + by (blast dest!: leastPD2 setgeD)
1.61 +
1.62 +lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
1.63 + by (simp add: isLub_def isUb_def leastP_def)
1.64 +
1.65 +lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
1.66 + by (simp add: isLub_def isUb_def leastP_def)
1.67 +
1.68 +lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
1.69 + unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
1.70 +
1.71 +lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
1.72 + by (blast dest!: isLubD1 setleD)
1.73 +
1.74 +lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
1.75 + by (simp add: isLub_def)
1.76 +
1.77 +lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
1.78 + by (simp add: isLub_def)
1.79 +
1.80 +lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
1.81 + by (simp add: isLub_def leastP_def)
1.82 +
1.83 +lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
1.84 + by (simp add: isUb_def setle_def)
1.85 +
1.86 +lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
1.87 + by (simp add: isUb_def)
1.88 +
1.89 +lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
1.90 + by (simp add: isUb_def)
1.91 +
1.92 +lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
1.93 + by (simp add: isUb_def)
1.94 +
1.95 +lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
1.96 + unfolding isLub_def by (blast intro!: leastPD3)
1.97 +
1.98 +lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
1.99 + unfolding ubs_def isLub_def by (rule leastPD2)
1.100 +
1.101 +lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
1.102 + apply (frule isLub_isUb)
1.103 + apply (frule_tac x = y in isLub_isUb)
1.104 + apply (blast intro!: order_antisym dest!: isLub_le_isUb)
1.105 + done
1.106 +
1.107 +lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
1.108 + by (simp add: isUbI setleI)
1.109 +
1.110 +
1.111 +definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.112 + where "greatestP P x = (P x \<and> Collect P *<= x)"
1.113 +
1.114 +definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.115 + where "isLb R S x = (x <=* S \<and> x: R)"
1.116 +
1.117 +definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.118 + where "isGlb R S x = greatestP (isLb R S) x"
1.119 +
1.120 +definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
1.121 + where "lbs R S = Collect (isLb R S)"
1.122 +
1.123 +
1.124 +subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *}
1.125 +
1.126 +lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
1.127 + by (simp add: greatestP_def)
1.128 +
1.129 +lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
1.130 + by (simp add: greatestP_def)
1.131 +
1.132 +lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
1.133 + by (blast dest!: greatestPD2 setleD)
1.134 +
1.135 +lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
1.136 + by (simp add: isGlb_def isLb_def greatestP_def)
1.137 +
1.138 +lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
1.139 + by (simp add: isGlb_def isLb_def greatestP_def)
1.140 +
1.141 +lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
1.142 + unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
1.143 +
1.144 +lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
1.145 + by (blast dest!: isGlbD1 setgeD)
1.146 +
1.147 +lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
1.148 + by (simp add: isGlb_def)
1.149 +
1.150 +lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
1.151 + by (simp add: isGlb_def)
1.152 +
1.153 +lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
1.154 + by (simp add: isGlb_def greatestP_def)
1.155 +
1.156 +lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
1.157 + by (simp add: isLb_def setge_def)
1.158 +
1.159 +lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
1.160 + by (simp add: isLb_def)
1.161 +
1.162 +lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
1.163 + by (simp add: isLb_def)
1.164 +
1.165 +lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
1.166 + by (simp add: isLb_def)
1.167 +
1.168 +lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
1.169 + unfolding isGlb_def by (blast intro!: greatestPD3)
1.170 +
1.171 +lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
1.172 + unfolding lbs_def isGlb_def by (rule greatestPD2)
1.173 +
1.174 +lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
1.175 + apply (frule isGlb_isLb)
1.176 + apply (frule_tac x = y in isGlb_isLb)
1.177 + apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
1.178 + done
1.179 +
1.180 +lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)"
1.181 + by (auto simp: bdd_above_def setle_def)
1.182 +
1.183 +lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)"
1.184 + by (auto simp: bdd_below_def setge_def)
1.185 +
1.186 +lemma isLub_cSup:
1.187 + "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
1.188 + by (auto simp add: isLub_def setle_def leastP_def isUb_def
1.189 + intro!: setgeI cSup_upper cSup_least)
1.190 +
1.191 +lemma isGlb_cInf:
1.192 + "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
1.193 + by (auto simp add: isGlb_def setge_def greatestP_def isLb_def
1.194 + intro!: setleI cInf_lower cInf_greatest)
1.195 +
1.196 +lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
1.197 + by (metis cSup_least setle_def)
1.198 +
1.199 +lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
1.200 + by (metis cInf_greatest setge_def)
1.201 +
1.202 +lemma cSup_bounds:
1.203 + fixes S :: "'a :: conditionally_complete_lattice set"
1.204 + shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b"
1.205 + using cSup_least[of S b] cSup_upper2[of _ S a]
1.206 + by (auto simp: bdd_above_setle setge_def setle_def)
1.207 +
1.208 +lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
1.209 + by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
1.210 +
1.211 +lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
1.212 + by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
1.213 +
1.214 +text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*}
1.215 +
1.216 +lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
1.217 + by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
1.218 +
1.219 +lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
1.220 + by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
1.221 +
1.222 +lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
1.223 + by (blast intro: reals_complete Bseq_isUb)
1.224 +
1.225 +lemma isLub_mono_imp_LIMSEQ:
1.226 + fixes X :: "nat \<Rightarrow> real"
1.227 + assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
1.228 + assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
1.229 + shows "X ----> u"
1.230 +proof -
1.231 + have "X ----> (SUP i. X i)"
1.232 + using u[THEN isLubD1] X
1.233 + by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
1.234 + also have "(SUP i. X i) = u"
1.235 + using isLub_cSup[of "range X"] u[THEN isLubD1]
1.236 + by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
1.237 + finally show ?thesis .
1.238 +qed
1.239 +
1.240 +lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
1.241 +
1.242 +lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)"
1.243 + by (rule cInf_superset_mono) (auto simp: bdd_below_setge)
1.244 +
1.245 +lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)"
1.246 + by (rule cSup_subset_mono) (auto simp: bdd_above_setle)
1.247 +
1.248 +end