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