author | hoelzl |
Tue, 05 Nov 2013 09:45:02 +0100 | |
changeset 55715 | c4159fe6fa46 |
parent 52479 | src/HOL/Library/Glbs.thy@763c6872bd10 |
permissions | -rw-r--r-- |
hoelzl@55715 | 1 |
(* Title: HOL/Library/Lubs_Glbs.thy |
hoelzl@55715 | 2 |
Author: Jacques D. Fleuriot, University of Cambridge |
hoelzl@55715 | 3 |
Author: Amine Chaieb, University of Cambridge *) |
chaieb@29775 | 4 |
|
hoelzl@55715 | 5 |
header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *} |
chaieb@29775 | 6 |
|
hoelzl@55715 | 7 |
theory Lubs_Glbs |
hoelzl@55715 | 8 |
imports Complex_Main |
chaieb@29775 | 9 |
begin |
chaieb@29775 | 10 |
|
hoelzl@55715 | 11 |
text {* Thanks to suggestions by James Margetson *} |
hoelzl@55715 | 12 |
|
hoelzl@55715 | 13 |
definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70) |
hoelzl@55715 | 14 |
where "S *<= x = (ALL y: S. y \<le> x)" |
hoelzl@55715 | 15 |
|
hoelzl@55715 | 16 |
definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70) |
hoelzl@55715 | 17 |
where "x <=* S = (ALL y: S. x \<le> y)" |
hoelzl@55715 | 18 |
|
hoelzl@55715 | 19 |
|
hoelzl@55715 | 20 |
subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *} |
hoelzl@55715 | 21 |
|
hoelzl@55715 | 22 |
lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x" |
hoelzl@55715 | 23 |
by (simp add: setle_def) |
hoelzl@55715 | 24 |
|
hoelzl@55715 | 25 |
lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x" |
hoelzl@55715 | 26 |
by (simp add: setle_def) |
hoelzl@55715 | 27 |
|
hoelzl@55715 | 28 |
lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S" |
hoelzl@55715 | 29 |
by (simp add: setge_def) |
hoelzl@55715 | 30 |
|
hoelzl@55715 | 31 |
lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y" |
hoelzl@55715 | 32 |
by (simp add: setge_def) |
hoelzl@55715 | 33 |
|
hoelzl@55715 | 34 |
|
hoelzl@55715 | 35 |
definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
hoelzl@55715 | 36 |
where "leastP P x = (P x \<and> x <=* Collect P)" |
hoelzl@55715 | 37 |
|
hoelzl@55715 | 38 |
definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
hoelzl@55715 | 39 |
where "isUb R S x = (S *<= x \<and> x: R)" |
hoelzl@55715 | 40 |
|
hoelzl@55715 | 41 |
definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
hoelzl@55715 | 42 |
where "isLub R S x = leastP (isUb R S) x" |
hoelzl@55715 | 43 |
|
hoelzl@55715 | 44 |
definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
hoelzl@55715 | 45 |
where "ubs R S = Collect (isUb R S)" |
hoelzl@55715 | 46 |
|
hoelzl@55715 | 47 |
|
hoelzl@55715 | 48 |
subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *} |
hoelzl@55715 | 49 |
|
hoelzl@55715 | 50 |
lemma leastPD1: "leastP P x \<Longrightarrow> P x" |
hoelzl@55715 | 51 |
by (simp add: leastP_def) |
hoelzl@55715 | 52 |
|
hoelzl@55715 | 53 |
lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P" |
hoelzl@55715 | 54 |
by (simp add: leastP_def) |
hoelzl@55715 | 55 |
|
hoelzl@55715 | 56 |
lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y" |
hoelzl@55715 | 57 |
by (blast dest!: leastPD2 setgeD) |
hoelzl@55715 | 58 |
|
hoelzl@55715 | 59 |
lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x" |
hoelzl@55715 | 60 |
by (simp add: isLub_def isUb_def leastP_def) |
hoelzl@55715 | 61 |
|
hoelzl@55715 | 62 |
lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R" |
hoelzl@55715 | 63 |
by (simp add: isLub_def isUb_def leastP_def) |
hoelzl@55715 | 64 |
|
hoelzl@55715 | 65 |
lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x" |
hoelzl@55715 | 66 |
unfolding isUb_def by (blast dest: isLubD1 isLubD1a) |
hoelzl@55715 | 67 |
|
hoelzl@55715 | 68 |
lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" |
hoelzl@55715 | 69 |
by (blast dest!: isLubD1 setleD) |
hoelzl@55715 | 70 |
|
hoelzl@55715 | 71 |
lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x" |
hoelzl@55715 | 72 |
by (simp add: isLub_def) |
hoelzl@55715 | 73 |
|
hoelzl@55715 | 74 |
lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x" |
hoelzl@55715 | 75 |
by (simp add: isLub_def) |
hoelzl@55715 | 76 |
|
hoelzl@55715 | 77 |
lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x" |
hoelzl@55715 | 78 |
by (simp add: isLub_def leastP_def) |
hoelzl@55715 | 79 |
|
hoelzl@55715 | 80 |
lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" |
hoelzl@55715 | 81 |
by (simp add: isUb_def setle_def) |
hoelzl@55715 | 82 |
|
hoelzl@55715 | 83 |
lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x" |
hoelzl@55715 | 84 |
by (simp add: isUb_def) |
hoelzl@55715 | 85 |
|
hoelzl@55715 | 86 |
lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R" |
hoelzl@55715 | 87 |
by (simp add: isUb_def) |
hoelzl@55715 | 88 |
|
hoelzl@55715 | 89 |
lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x" |
hoelzl@55715 | 90 |
by (simp add: isUb_def) |
hoelzl@55715 | 91 |
|
hoelzl@55715 | 92 |
lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y" |
hoelzl@55715 | 93 |
unfolding isLub_def by (blast intro!: leastPD3) |
hoelzl@55715 | 94 |
|
hoelzl@55715 | 95 |
lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S" |
hoelzl@55715 | 96 |
unfolding ubs_def isLub_def by (rule leastPD2) |
hoelzl@55715 | 97 |
|
hoelzl@55715 | 98 |
lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)" |
hoelzl@55715 | 99 |
apply (frule isLub_isUb) |
hoelzl@55715 | 100 |
apply (frule_tac x = y in isLub_isUb) |
hoelzl@55715 | 101 |
apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
hoelzl@55715 | 102 |
done |
hoelzl@55715 | 103 |
|
hoelzl@55715 | 104 |
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" |
hoelzl@55715 | 105 |
by (simp add: isUbI setleI) |
hoelzl@55715 | 106 |
|
hoelzl@55715 | 107 |
|
wenzelm@47380 | 108 |
definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" |
wenzelm@47380 | 109 |
where "greatestP P x = (P x \<and> Collect P *<= x)" |
chaieb@29775 | 110 |
|
wenzelm@47380 | 111 |
definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
wenzelm@47380 | 112 |
where "isLb R S x = (x <=* S \<and> x: R)" |
chaieb@29775 | 113 |
|
wenzelm@47380 | 114 |
definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" |
wenzelm@47380 | 115 |
where "isGlb R S x = greatestP (isLb R S) x" |
chaieb@29775 | 116 |
|
wenzelm@47380 | 117 |
definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" |
wenzelm@47380 | 118 |
where "lbs R S = Collect (isLb R S)" |
chaieb@29775 | 119 |
|
chaieb@29775 | 120 |
|
hoelzl@55715 | 121 |
subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *} |
chaieb@29775 | 122 |
|
hoelzl@55715 | 123 |
lemma greatestPD1: "greatestP P x \<Longrightarrow> P x" |
wenzelm@47380 | 124 |
by (simp add: greatestP_def) |
chaieb@29775 | 125 |
|
wenzelm@47380 | 126 |
lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x" |
wenzelm@47380 | 127 |
by (simp add: greatestP_def) |
chaieb@29775 | 128 |
|
wenzelm@47380 | 129 |
lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y" |
wenzelm@47380 | 130 |
by (blast dest!: greatestPD2 setleD) |
chaieb@29775 | 131 |
|
wenzelm@47380 | 132 |
lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S" |
wenzelm@47380 | 133 |
by (simp add: isGlb_def isLb_def greatestP_def) |
chaieb@29775 | 134 |
|
wenzelm@47380 | 135 |
lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R" |
wenzelm@47380 | 136 |
by (simp add: isGlb_def isLb_def greatestP_def) |
chaieb@29775 | 137 |
|
wenzelm@47380 | 138 |
lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x" |
wenzelm@47380 | 139 |
unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a) |
chaieb@29775 | 140 |
|
wenzelm@47380 | 141 |
lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x" |
wenzelm@47380 | 142 |
by (blast dest!: isGlbD1 setgeD) |
chaieb@29775 | 143 |
|
wenzelm@47380 | 144 |
lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x" |
wenzelm@47380 | 145 |
by (simp add: isGlb_def) |
chaieb@29775 | 146 |
|
wenzelm@47380 | 147 |
lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x" |
wenzelm@47380 | 148 |
by (simp add: isGlb_def) |
chaieb@29775 | 149 |
|
wenzelm@47380 | 150 |
lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x" |
wenzelm@47380 | 151 |
by (simp add: isGlb_def greatestP_def) |
chaieb@29775 | 152 |
|
wenzelm@47380 | 153 |
lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x" |
wenzelm@47380 | 154 |
by (simp add: isLb_def setge_def) |
chaieb@29775 | 155 |
|
wenzelm@47380 | 156 |
lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S " |
wenzelm@47380 | 157 |
by (simp add: isLb_def) |
chaieb@29775 | 158 |
|
wenzelm@47380 | 159 |
lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R" |
wenzelm@47380 | 160 |
by (simp add: isLb_def) |
chaieb@29775 | 161 |
|
wenzelm@47380 | 162 |
lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x" |
wenzelm@47380 | 163 |
by (simp add: isLb_def) |
chaieb@29775 | 164 |
|
wenzelm@47380 | 165 |
lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y" |
wenzelm@47380 | 166 |
unfolding isGlb_def by (blast intro!: greatestPD3) |
wenzelm@47380 | 167 |
|
wenzelm@47380 | 168 |
lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x" |
wenzelm@47380 | 169 |
unfolding lbs_def isGlb_def by (rule greatestPD2) |
chaieb@29775 | 170 |
|
hoelzl@52479 | 171 |
lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)" |
hoelzl@52479 | 172 |
apply (frule isGlb_isLb) |
hoelzl@52479 | 173 |
apply (frule_tac x = y in isGlb_isLb) |
hoelzl@52479 | 174 |
apply (blast intro!: order_antisym dest!: isGlb_le_isLb) |
hoelzl@52479 | 175 |
done |
hoelzl@52479 | 176 |
|
hoelzl@55715 | 177 |
lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)" |
hoelzl@55715 | 178 |
by (auto simp: bdd_above_def setle_def) |
hoelzl@55715 | 179 |
|
hoelzl@55715 | 180 |
lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)" |
hoelzl@55715 | 181 |
by (auto simp: bdd_below_def setge_def) |
hoelzl@55715 | 182 |
|
hoelzl@55715 | 183 |
lemma isLub_cSup: |
hoelzl@55715 | 184 |
"(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)" |
hoelzl@55715 | 185 |
by (auto simp add: isLub_def setle_def leastP_def isUb_def |
hoelzl@55715 | 186 |
intro!: setgeI cSup_upper cSup_least) |
hoelzl@55715 | 187 |
|
hoelzl@55715 | 188 |
lemma isGlb_cInf: |
hoelzl@55715 | 189 |
"(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)" |
hoelzl@55715 | 190 |
by (auto simp add: isGlb_def setge_def greatestP_def isLb_def |
hoelzl@55715 | 191 |
intro!: setleI cInf_lower cInf_greatest) |
hoelzl@55715 | 192 |
|
hoelzl@55715 | 193 |
lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b" |
hoelzl@55715 | 194 |
by (metis cSup_least setle_def) |
hoelzl@55715 | 195 |
|
hoelzl@55715 | 196 |
lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b" |
hoelzl@55715 | 197 |
by (metis cInf_greatest setge_def) |
hoelzl@55715 | 198 |
|
hoelzl@55715 | 199 |
lemma cSup_bounds: |
hoelzl@55715 | 200 |
fixes S :: "'a :: conditionally_complete_lattice set" |
hoelzl@55715 | 201 |
shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b" |
hoelzl@55715 | 202 |
using cSup_least[of S b] cSup_upper2[of _ S a] |
hoelzl@55715 | 203 |
by (auto simp: bdd_above_setle setge_def setle_def) |
hoelzl@55715 | 204 |
|
hoelzl@55715 | 205 |
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" |
hoelzl@55715 | 206 |
by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) |
hoelzl@55715 | 207 |
|
hoelzl@55715 | 208 |
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" |
hoelzl@55715 | 209 |
by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) |
hoelzl@55715 | 210 |
|
hoelzl@55715 | 211 |
text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*} |
hoelzl@55715 | 212 |
|
hoelzl@55715 | 213 |
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" |
hoelzl@55715 | 214 |
by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper) |
hoelzl@55715 | 215 |
|
hoelzl@55715 | 216 |
lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" |
hoelzl@55715 | 217 |
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) |
hoelzl@55715 | 218 |
|
hoelzl@55715 | 219 |
lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" |
hoelzl@55715 | 220 |
by (blast intro: reals_complete Bseq_isUb) |
hoelzl@55715 | 221 |
|
hoelzl@55715 | 222 |
lemma isLub_mono_imp_LIMSEQ: |
hoelzl@55715 | 223 |
fixes X :: "nat \<Rightarrow> real" |
hoelzl@55715 | 224 |
assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *) |
hoelzl@55715 | 225 |
assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" |
hoelzl@55715 | 226 |
shows "X ----> u" |
hoelzl@55715 | 227 |
proof - |
hoelzl@55715 | 228 |
have "X ----> (SUP i. X i)" |
hoelzl@55715 | 229 |
using u[THEN isLubD1] X |
hoelzl@55715 | 230 |
by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle) |
hoelzl@55715 | 231 |
also have "(SUP i. X i) = u" |
hoelzl@55715 | 232 |
using isLub_cSup[of "range X"] u[THEN isLubD1] |
hoelzl@55715 | 233 |
by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute) |
hoelzl@55715 | 234 |
finally show ?thesis . |
hoelzl@55715 | 235 |
qed |
hoelzl@55715 | 236 |
|
hoelzl@55715 | 237 |
lemmas real_isGlb_unique = isGlb_unique[where 'a=real] |
hoelzl@55715 | 238 |
|
hoelzl@55715 | 239 |
lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)" |
hoelzl@55715 | 240 |
by (rule cInf_superset_mono) (auto simp: bdd_below_setge) |
hoelzl@55715 | 241 |
|
hoelzl@55715 | 242 |
lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)" |
hoelzl@55715 | 243 |
by (rule cSup_subset_mono) (auto simp: bdd_above_setle) |
hoelzl@55715 | 244 |
|
chaieb@29775 | 245 |
end |