author | berghofe |
Mon, 24 Jan 2005 18:16:57 +0100 | |
changeset 15463 | 95cb3eb74307 |
parent 15328 | 35951e6a7855 |
child 16325 | a6431098a929 |
permissions | -rw-r--r-- |
14551 | 1 |
(* |
14706 | 2 |
Title: HOL/Algebra/Lattice.thy |
14551 | 3 |
Id: $Id$ |
4 |
Author: Clemens Ballarin, started 7 November 2003 |
|
5 |
Copyright: Clemens Ballarin |
|
6 |
*) |
|
7 |
||
14706 | 8 |
header {* Orders and Lattices *} |
14551 | 9 |
|
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
10 |
theory Lattice = Main: |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
11 |
|
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
12 |
text {* Object with a carrier set. *} |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
13 |
|
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
14 |
record 'a partial_object = |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
15 |
carrier :: "'a set" |
14551 | 16 |
|
17 |
subsection {* Partial Orders *} |
|
18 |
||
19 |
record 'a order = "'a partial_object" + |
|
20 |
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) |
|
21 |
||
14693 | 22 |
locale partial_order = struct L + |
14551 | 23 |
assumes refl [intro, simp]: |
24 |
"x \<in> carrier L ==> x \<sqsubseteq> x" |
|
25 |
and anti_sym [intro]: |
|
26 |
"[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y" |
|
27 |
and trans [trans]: |
|
28 |
"[| x \<sqsubseteq> y; y \<sqsubseteq> z; |
|
29 |
x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" |
|
30 |
||
14651 | 31 |
constdefs (structure L) |
32 |
less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) |
|
33 |
"x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" |
|
14551 | 34 |
|
14651 | 35 |
-- {* Upper and lower bounds of a set. *} |
36 |
Upper :: "[_, 'a set] => 'a set" |
|
14693 | 37 |
"Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> |
14551 | 38 |
carrier L" |
39 |
||
14651 | 40 |
Lower :: "[_, 'a set] => 'a set" |
14693 | 41 |
"Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> |
14551 | 42 |
carrier L" |
43 |
||
14651 | 44 |
-- {* Least and greatest, as predicate. *} |
45 |
least :: "[_, 'a, 'a set] => bool" |
|
14693 | 46 |
"least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" |
14551 | 47 |
|
14651 | 48 |
greatest :: "[_, 'a, 'a set] => bool" |
14693 | 49 |
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" |
14551 | 50 |
|
14651 | 51 |
-- {* Supremum and infimum *} |
52 |
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) |
|
53 |
"\<Squnion>A == THE x. least L x (Upper L A)" |
|
14551 | 54 |
|
14651 | 55 |
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) |
56 |
"\<Sqinter>A == THE x. greatest L x (Lower L A)" |
|
14551 | 57 |
|
14651 | 58 |
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) |
59 |
"x \<squnion> y == sup L {x, y}" |
|
14551 | 60 |
|
14651 | 61 |
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65) |
62 |
"x \<sqinter> y == inf L {x, y}" |
|
14551 | 63 |
|
14651 | 64 |
|
65 |
subsubsection {* Upper *} |
|
14551 | 66 |
|
67 |
lemma Upper_closed [intro, simp]: |
|
68 |
"Upper L A \<subseteq> carrier L" |
|
69 |
by (unfold Upper_def) clarify |
|
70 |
||
71 |
lemma UpperD [dest]: |
|
14693 | 72 |
includes struct L |
14551 | 73 |
shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" |
14693 | 74 |
by (unfold Upper_def) blast |
14551 | 75 |
|
76 |
lemma Upper_memI: |
|
14693 | 77 |
includes struct L |
14551 | 78 |
shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A" |
14693 | 79 |
by (unfold Upper_def) blast |
14551 | 80 |
|
81 |
lemma Upper_antimono: |
|
82 |
"A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" |
|
83 |
by (unfold Upper_def) blast |
|
84 |
||
14651 | 85 |
|
86 |
subsubsection {* Lower *} |
|
14551 | 87 |
|
88 |
lemma Lower_closed [intro, simp]: |
|
89 |
"Lower L A \<subseteq> carrier L" |
|
90 |
by (unfold Lower_def) clarify |
|
91 |
||
92 |
lemma LowerD [dest]: |
|
14693 | 93 |
includes struct L |
14551 | 94 |
shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x" |
14693 | 95 |
by (unfold Lower_def) blast |
14551 | 96 |
|
97 |
lemma Lower_memI: |
|
14693 | 98 |
includes struct L |
14551 | 99 |
shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A" |
14693 | 100 |
by (unfold Lower_def) blast |
14551 | 101 |
|
102 |
lemma Lower_antimono: |
|
103 |
"A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" |
|
104 |
by (unfold Lower_def) blast |
|
105 |
||
14651 | 106 |
|
107 |
subsubsection {* least *} |
|
14551 | 108 |
|
109 |
lemma least_carrier [intro, simp]: |
|
110 |
shows "least L l A ==> l \<in> carrier L" |
|
111 |
by (unfold least_def) fast |
|
112 |
||
113 |
lemma least_mem: |
|
114 |
"least L l A ==> l \<in> A" |
|
115 |
by (unfold least_def) fast |
|
116 |
||
117 |
lemma (in partial_order) least_unique: |
|
118 |
"[| least L x A; least L y A |] ==> x = y" |
|
119 |
by (unfold least_def) blast |
|
120 |
||
121 |
lemma least_le: |
|
14693 | 122 |
includes struct L |
14551 | 123 |
shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a" |
124 |
by (unfold least_def) fast |
|
125 |
||
126 |
lemma least_UpperI: |
|
14693 | 127 |
includes struct L |
14551 | 128 |
assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" |
129 |
and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" |
|
14693 | 130 |
and L: "A \<subseteq> carrier L" "s \<in> carrier L" |
14551 | 131 |
shows "least L s (Upper L A)" |
14693 | 132 |
proof - |
133 |
have "Upper L A \<subseteq> carrier L" by simp |
|
134 |
moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def) |
|
135 |
moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast |
|
136 |
ultimately show ?thesis by (simp add: least_def) |
|
14551 | 137 |
qed |
138 |
||
14651 | 139 |
|
140 |
subsubsection {* greatest *} |
|
14551 | 141 |
|
142 |
lemma greatest_carrier [intro, simp]: |
|
143 |
shows "greatest L l A ==> l \<in> carrier L" |
|
144 |
by (unfold greatest_def) fast |
|
145 |
||
146 |
lemma greatest_mem: |
|
147 |
"greatest L l A ==> l \<in> A" |
|
148 |
by (unfold greatest_def) fast |
|
149 |
||
150 |
lemma (in partial_order) greatest_unique: |
|
151 |
"[| greatest L x A; greatest L y A |] ==> x = y" |
|
152 |
by (unfold greatest_def) blast |
|
153 |
||
154 |
lemma greatest_le: |
|
14693 | 155 |
includes struct L |
14551 | 156 |
shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" |
157 |
by (unfold greatest_def) fast |
|
158 |
||
159 |
lemma greatest_LowerI: |
|
14693 | 160 |
includes struct L |
14551 | 161 |
assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" |
162 |
and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" |
|
14693 | 163 |
and L: "A \<subseteq> carrier L" "i \<in> carrier L" |
14551 | 164 |
shows "greatest L i (Lower L A)" |
14693 | 165 |
proof - |
166 |
have "Lower L A \<subseteq> carrier L" by simp |
|
167 |
moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) |
|
168 |
moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast |
|
169 |
ultimately show ?thesis by (simp add: greatest_def) |
|
14551 | 170 |
qed |
171 |
||
14693 | 172 |
|
14551 | 173 |
subsection {* Lattices *} |
174 |
||
175 |
locale lattice = partial_order + |
|
176 |
assumes sup_of_two_exists: |
|
177 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
|
178 |
and inf_of_two_exists: |
|
179 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
|
180 |
||
181 |
lemma least_Upper_above: |
|
14693 | 182 |
includes struct L |
14551 | 183 |
shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" |
184 |
by (unfold least_def) blast |
|
185 |
||
186 |
lemma greatest_Lower_above: |
|
14693 | 187 |
includes struct L |
14551 | 188 |
shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" |
189 |
by (unfold greatest_def) blast |
|
190 |
||
14666 | 191 |
|
14551 | 192 |
subsubsection {* Supremum *} |
193 |
||
194 |
lemma (in lattice) joinI: |
|
195 |
"[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] |
|
196 |
==> P (x \<squnion> y)" |
|
197 |
proof (unfold join_def sup_def) |
|
14693 | 198 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
14551 | 199 |
and P: "!!l. least L l (Upper L {x, y}) ==> P l" |
200 |
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
|
201 |
with L show "P (THE l. least L l (Upper L {x, y}))" |
|
14693 | 202 |
by (fast intro: theI2 least_unique P) |
14551 | 203 |
qed |
204 |
||
205 |
lemma (in lattice) join_closed [simp]: |
|
206 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" |
|
207 |
by (rule joinI) (rule least_carrier) |
|
208 |
||
14651 | 209 |
lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
14551 | 210 |
"x \<in> carrier L ==> least L x (Upper L {x})" |
211 |
by (rule least_UpperI) fast+ |
|
212 |
||
213 |
lemma (in partial_order) sup_of_singleton [simp]: |
|
14693 | 214 |
includes struct L |
215 |
shows "x \<in> carrier L ==> \<Squnion>{x} = x" |
|
14551 | 216 |
by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) |
217 |
||
14666 | 218 |
|
219 |
text {* Condition on @{text A}: supremum exists. *} |
|
14551 | 220 |
|
221 |
lemma (in lattice) sup_insertI: |
|
222 |
"[| !!s. least L s (Upper L (insert x A)) ==> P s; |
|
223 |
least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] |
|
14693 | 224 |
==> P (\<Squnion>(insert x A))" |
14551 | 225 |
proof (unfold sup_def) |
14693 | 226 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 227 |
and P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
228 |
and least_a: "least L a (Upper L A)" |
|
229 |
from L least_a have La: "a \<in> carrier L" by simp |
|
230 |
from L sup_of_two_exists least_a |
|
231 |
obtain s where least_s: "least L s (Upper L {a, x})" by blast |
|
232 |
show "P (THE l. least L l (Upper L (insert x A)))" |
|
14693 | 233 |
proof (rule theI2) |
14551 | 234 |
show "least L s (Upper L (insert x A))" |
235 |
proof (rule least_UpperI) |
|
236 |
fix z |
|
14693 | 237 |
assume "z \<in> insert x A" |
238 |
then show "z \<sqsubseteq> s" |
|
239 |
proof |
|
240 |
assume "z = x" then show ?thesis |
|
241 |
by (simp add: least_Upper_above [OF least_s] L La) |
|
242 |
next |
|
243 |
assume "z \<in> A" |
|
244 |
with L least_s least_a show ?thesis |
|
245 |
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
|
246 |
qed |
|
247 |
next |
|
248 |
fix y |
|
249 |
assume y: "y \<in> Upper L (insert x A)" |
|
250 |
show "s \<sqsubseteq> y" |
|
251 |
proof (rule least_le [OF least_s], rule Upper_memI) |
|
252 |
fix z |
|
253 |
assume z: "z \<in> {a, x}" |
|
254 |
then show "z \<sqsubseteq> y" |
|
255 |
proof |
|
256 |
have y': "y \<in> Upper L A" |
|
257 |
apply (rule subsetD [where A = "Upper L (insert x A)"]) |
|
258 |
apply (rule Upper_antimono) apply clarify apply assumption |
|
259 |
done |
|
260 |
assume "z = a" |
|
261 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
262 |
next |
|
263 |
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) |
|
264 |
with y L show ?thesis by blast |
|
265 |
qed |
|
266 |
qed (rule Upper_closed [THEN subsetD]) |
|
267 |
next |
|
268 |
from L show "insert x A \<subseteq> carrier L" by simp |
|
269 |
from least_s show "s \<in> carrier L" by simp |
|
14551 | 270 |
qed |
271 |
next |
|
272 |
fix l |
|
273 |
assume least_l: "least L l (Upper L (insert x A))" |
|
274 |
show "l = s" |
|
275 |
proof (rule least_unique) |
|
276 |
show "least L s (Upper L (insert x A))" |
|
277 |
proof (rule least_UpperI) |
|
14693 | 278 |
fix z |
279 |
assume "z \<in> insert x A" |
|
280 |
then show "z \<sqsubseteq> s" |
|
281 |
proof |
|
282 |
assume "z = x" then show ?thesis |
|
283 |
by (simp add: least_Upper_above [OF least_s] L La) |
|
284 |
next |
|
285 |
assume "z \<in> A" |
|
286 |
with L least_s least_a show ?thesis |
|
287 |
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
|
14551 | 288 |
qed |
289 |
next |
|
14693 | 290 |
fix y |
291 |
assume y: "y \<in> Upper L (insert x A)" |
|
292 |
show "s \<sqsubseteq> y" |
|
293 |
proof (rule least_le [OF least_s], rule Upper_memI) |
|
294 |
fix z |
|
295 |
assume z: "z \<in> {a, x}" |
|
296 |
then show "z \<sqsubseteq> y" |
|
297 |
proof |
|
298 |
have y': "y \<in> Upper L A" |
|
299 |
apply (rule subsetD [where A = "Upper L (insert x A)"]) |
|
300 |
apply (rule Upper_antimono) apply clarify apply assumption |
|
301 |
done |
|
302 |
assume "z = a" |
|
303 |
with y' least_a show ?thesis by (fast dest: least_le) |
|
304 |
next |
|
305 |
assume "z \<in> {x}" |
|
306 |
with y L show ?thesis by blast |
|
307 |
qed |
|
308 |
qed (rule Upper_closed [THEN subsetD]) |
|
14551 | 309 |
next |
14693 | 310 |
from L show "insert x A \<subseteq> carrier L" by simp |
311 |
from least_s show "s \<in> carrier L" by simp |
|
14551 | 312 |
qed |
313 |
qed |
|
314 |
qed |
|
315 |
qed |
|
316 |
||
317 |
lemma (in lattice) finite_sup_least: |
|
14693 | 318 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)" |
14551 | 319 |
proof (induct set: Finites) |
14693 | 320 |
case empty |
321 |
then show ?case by simp |
|
14551 | 322 |
next |
15328 | 323 |
case (insert x A) |
14551 | 324 |
show ?case |
325 |
proof (cases "A = {}") |
|
326 |
case True |
|
327 |
with insert show ?thesis by (simp add: sup_of_singletonI) |
|
328 |
next |
|
329 |
case False |
|
14693 | 330 |
with insert have "least L (\<Squnion>A) (Upper L A)" by simp |
331 |
with _ show ?thesis |
|
332 |
by (rule sup_insertI) (simp_all add: insert [simplified]) |
|
14551 | 333 |
qed |
334 |
qed |
|
335 |
||
336 |
lemma (in lattice) finite_sup_insertI: |
|
337 |
assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
|
14693 | 338 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 339 |
shows "P (\<Squnion> (insert x A))" |
340 |
proof (cases "A = {}") |
|
341 |
case True with P and xA show ?thesis |
|
342 |
by (simp add: sup_of_singletonI) |
|
343 |
next |
|
344 |
case False with P and xA show ?thesis |
|
345 |
by (simp add: sup_insertI finite_sup_least) |
|
346 |
qed |
|
347 |
||
348 |
lemma (in lattice) finite_sup_closed: |
|
14693 | 349 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" |
14551 | 350 |
proof (induct set: Finites) |
351 |
case empty then show ?case by simp |
|
352 |
next |
|
15328 | 353 |
case insert then show ?case |
14693 | 354 |
by - (rule finite_sup_insertI, simp_all) |
14551 | 355 |
qed |
356 |
||
357 |
lemma (in lattice) join_left: |
|
358 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
|
14693 | 359 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 360 |
|
361 |
lemma (in lattice) join_right: |
|
362 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
|
14693 | 363 |
by (rule joinI [folded join_def]) (blast dest: least_mem) |
14551 | 364 |
|
365 |
lemma (in lattice) sup_of_two_least: |
|
14693 | 366 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" |
14551 | 367 |
proof (unfold sup_def) |
14693 | 368 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
14551 | 369 |
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
370 |
with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" |
|
371 |
by (fast intro: theI2 least_unique) (* blast fails *) |
|
372 |
qed |
|
373 |
||
374 |
lemma (in lattice) join_le: |
|
14693 | 375 |
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
376 |
and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
|
14551 | 377 |
shows "x \<squnion> y \<sqsubseteq> z" |
378 |
proof (rule joinI) |
|
379 |
fix s |
|
380 |
assume "least L s (Upper L {x, y})" |
|
381 |
with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
|
382 |
qed |
|
14693 | 383 |
|
14551 | 384 |
lemma (in lattice) join_assoc_lemma: |
14693 | 385 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
386 |
shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" |
|
14551 | 387 |
proof (rule finite_sup_insertI) |
14651 | 388 |
-- {* The textbook argument in Jacobson I, p 457 *} |
14551 | 389 |
fix s |
390 |
assume sup: "least L s (Upper L {x, y, z})" |
|
391 |
show "x \<squnion> (y \<squnion> z) = s" |
|
392 |
proof (rule anti_sym) |
|
393 |
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" |
|
394 |
by (fastsimp intro!: join_le elim: least_Upper_above) |
|
395 |
next |
|
396 |
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
397 |
by (erule_tac least_le) |
|
398 |
(blast intro!: Upper_memI intro: trans join_left join_right join_closed) |
|
399 |
qed (simp_all add: L least_carrier [OF sup]) |
|
400 |
qed (simp_all add: L) |
|
401 |
||
402 |
lemma join_comm: |
|
14693 | 403 |
includes struct L |
14551 | 404 |
shows "x \<squnion> y = y \<squnion> x" |
405 |
by (unfold join_def) (simp add: insert_commute) |
|
406 |
||
407 |
lemma (in lattice) join_assoc: |
|
14693 | 408 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 409 |
shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
410 |
proof - |
|
411 |
have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) |
|
14693 | 412 |
also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma) |
413 |
also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) |
|
14551 | 414 |
also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) |
415 |
finally show ?thesis . |
|
416 |
qed |
|
417 |
||
14693 | 418 |
|
14551 | 419 |
subsubsection {* Infimum *} |
420 |
||
421 |
lemma (in lattice) meetI: |
|
422 |
"[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
|
423 |
x \<in> carrier L; y \<in> carrier L |] |
|
424 |
==> P (x \<sqinter> y)" |
|
425 |
proof (unfold meet_def inf_def) |
|
14693 | 426 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
14551 | 427 |
and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
428 |
with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast |
|
429 |
with L show "P (THE g. greatest L g (Lower L {x, y}))" |
|
430 |
by (fast intro: theI2 greatest_unique P) |
|
431 |
qed |
|
432 |
||
433 |
lemma (in lattice) meet_closed [simp]: |
|
434 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" |
|
435 |
by (rule meetI) (rule greatest_carrier) |
|
436 |
||
14651 | 437 |
lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
14551 | 438 |
"x \<in> carrier L ==> greatest L x (Lower L {x})" |
439 |
by (rule greatest_LowerI) fast+ |
|
440 |
||
441 |
lemma (in partial_order) inf_of_singleton [simp]: |
|
14693 | 442 |
includes struct L |
14551 | 443 |
shows "x \<in> carrier L ==> \<Sqinter> {x} = x" |
444 |
by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
|
445 |
||
446 |
text {* Condition on A: infimum exists. *} |
|
447 |
||
448 |
lemma (in lattice) inf_insertI: |
|
449 |
"[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
|
450 |
greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
|
14693 | 451 |
==> P (\<Sqinter>(insert x A))" |
14551 | 452 |
proof (unfold inf_def) |
14693 | 453 |
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 454 |
and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" |
455 |
and greatest_a: "greatest L a (Lower L A)" |
|
456 |
from L greatest_a have La: "a \<in> carrier L" by simp |
|
457 |
from L inf_of_two_exists greatest_a |
|
458 |
obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast |
|
459 |
show "P (THE g. greatest L g (Lower L (insert x A)))" |
|
14693 | 460 |
proof (rule theI2) |
14551 | 461 |
show "greatest L i (Lower L (insert x A))" |
462 |
proof (rule greatest_LowerI) |
|
463 |
fix z |
|
14693 | 464 |
assume "z \<in> insert x A" |
465 |
then show "i \<sqsubseteq> z" |
|
466 |
proof |
|
467 |
assume "z = x" then show ?thesis |
|
468 |
by (simp add: greatest_Lower_above [OF greatest_i] L La) |
|
469 |
next |
|
470 |
assume "z \<in> A" |
|
471 |
with L greatest_i greatest_a show ?thesis |
|
472 |
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
473 |
qed |
|
474 |
next |
|
475 |
fix y |
|
476 |
assume y: "y \<in> Lower L (insert x A)" |
|
477 |
show "y \<sqsubseteq> i" |
|
478 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
479 |
fix z |
|
480 |
assume z: "z \<in> {a, x}" |
|
481 |
then show "y \<sqsubseteq> z" |
|
482 |
proof |
|
483 |
have y': "y \<in> Lower L A" |
|
484 |
apply (rule subsetD [where A = "Lower L (insert x A)"]) |
|
485 |
apply (rule Lower_antimono) apply clarify apply assumption |
|
486 |
done |
|
487 |
assume "z = a" |
|
488 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
489 |
next |
|
490 |
assume "z \<in> {x}" |
|
491 |
with y L show ?thesis by blast |
|
492 |
qed |
|
493 |
qed (rule Lower_closed [THEN subsetD]) |
|
494 |
next |
|
495 |
from L show "insert x A \<subseteq> carrier L" by simp |
|
496 |
from greatest_i show "i \<in> carrier L" by simp |
|
14551 | 497 |
qed |
498 |
next |
|
499 |
fix g |
|
500 |
assume greatest_g: "greatest L g (Lower L (insert x A))" |
|
501 |
show "g = i" |
|
502 |
proof (rule greatest_unique) |
|
503 |
show "greatest L i (Lower L (insert x A))" |
|
504 |
proof (rule greatest_LowerI) |
|
14693 | 505 |
fix z |
506 |
assume "z \<in> insert x A" |
|
507 |
then show "i \<sqsubseteq> z" |
|
508 |
proof |
|
509 |
assume "z = x" then show ?thesis |
|
510 |
by (simp add: greatest_Lower_above [OF greatest_i] L La) |
|
511 |
next |
|
512 |
assume "z \<in> A" |
|
513 |
with L greatest_i greatest_a show ?thesis |
|
514 |
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
515 |
qed |
|
14551 | 516 |
next |
14693 | 517 |
fix y |
518 |
assume y: "y \<in> Lower L (insert x A)" |
|
519 |
show "y \<sqsubseteq> i" |
|
520 |
proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
521 |
fix z |
|
522 |
assume z: "z \<in> {a, x}" |
|
523 |
then show "y \<sqsubseteq> z" |
|
524 |
proof |
|
525 |
have y': "y \<in> Lower L A" |
|
526 |
apply (rule subsetD [where A = "Lower L (insert x A)"]) |
|
527 |
apply (rule Lower_antimono) apply clarify apply assumption |
|
528 |
done |
|
529 |
assume "z = a" |
|
530 |
with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
531 |
next |
|
532 |
assume "z \<in> {x}" |
|
533 |
with y L show ?thesis by blast |
|
14551 | 534 |
qed |
14693 | 535 |
qed (rule Lower_closed [THEN subsetD]) |
14551 | 536 |
next |
14693 | 537 |
from L show "insert x A \<subseteq> carrier L" by simp |
538 |
from greatest_i show "i \<in> carrier L" by simp |
|
14551 | 539 |
qed |
540 |
qed |
|
541 |
qed |
|
542 |
qed |
|
543 |
||
544 |
lemma (in lattice) finite_inf_greatest: |
|
14693 | 545 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)" |
14551 | 546 |
proof (induct set: Finites) |
547 |
case empty then show ?case by simp |
|
548 |
next |
|
15328 | 549 |
case (insert x A) |
14551 | 550 |
show ?case |
551 |
proof (cases "A = {}") |
|
552 |
case True |
|
553 |
with insert show ?thesis by (simp add: inf_of_singletonI) |
|
554 |
next |
|
555 |
case False |
|
556 |
from insert show ?thesis |
|
557 |
proof (rule_tac inf_insertI) |
|
14693 | 558 |
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp |
14551 | 559 |
qed simp_all |
560 |
qed |
|
561 |
qed |
|
562 |
||
563 |
lemma (in lattice) finite_inf_insertI: |
|
564 |
assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" |
|
14693 | 565 |
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
14551 | 566 |
shows "P (\<Sqinter> (insert x A))" |
567 |
proof (cases "A = {}") |
|
568 |
case True with P and xA show ?thesis |
|
569 |
by (simp add: inf_of_singletonI) |
|
570 |
next |
|
571 |
case False with P and xA show ?thesis |
|
572 |
by (simp add: inf_insertI finite_inf_greatest) |
|
573 |
qed |
|
574 |
||
575 |
lemma (in lattice) finite_inf_closed: |
|
14693 | 576 |
"[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" |
14551 | 577 |
proof (induct set: Finites) |
578 |
case empty then show ?case by simp |
|
579 |
next |
|
15328 | 580 |
case insert then show ?case |
14551 | 581 |
by (rule_tac finite_inf_insertI) (simp_all) |
582 |
qed |
|
583 |
||
584 |
lemma (in lattice) meet_left: |
|
585 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
|
14693 | 586 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 587 |
|
588 |
lemma (in lattice) meet_right: |
|
589 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
|
14693 | 590 |
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
14551 | 591 |
|
592 |
lemma (in lattice) inf_of_two_greatest: |
|
593 |
"[| x \<in> carrier L; y \<in> carrier L |] ==> |
|
594 |
greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" |
|
595 |
proof (unfold inf_def) |
|
14693 | 596 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
14551 | 597 |
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
598 |
with L |
|
599 |
show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" |
|
600 |
by (fast intro: theI2 greatest_unique) (* blast fails *) |
|
601 |
qed |
|
602 |
||
603 |
lemma (in lattice) meet_le: |
|
14693 | 604 |
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
605 |
and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
|
14551 | 606 |
shows "z \<sqsubseteq> x \<sqinter> y" |
607 |
proof (rule meetI) |
|
608 |
fix i |
|
609 |
assume "greatest L i (Lower L {x, y})" |
|
610 |
with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
|
611 |
qed |
|
14693 | 612 |
|
14551 | 613 |
lemma (in lattice) meet_assoc_lemma: |
14693 | 614 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
615 |
shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" |
|
14551 | 616 |
proof (rule finite_inf_insertI) |
617 |
txt {* The textbook argument in Jacobson I, p 457 *} |
|
618 |
fix i |
|
619 |
assume inf: "greatest L i (Lower L {x, y, z})" |
|
620 |
show "x \<sqinter> (y \<sqinter> z) = i" |
|
621 |
proof (rule anti_sym) |
|
622 |
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
|
623 |
by (fastsimp intro!: meet_le elim: greatest_Lower_above) |
|
624 |
next |
|
625 |
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" |
|
626 |
by (erule_tac greatest_le) |
|
627 |
(blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) |
|
628 |
qed (simp_all add: L greatest_carrier [OF inf]) |
|
629 |
qed (simp_all add: L) |
|
630 |
||
631 |
lemma meet_comm: |
|
14693 | 632 |
includes struct L |
14551 | 633 |
shows "x \<sqinter> y = y \<sqinter> x" |
634 |
by (unfold meet_def) (simp add: insert_commute) |
|
635 |
||
636 |
lemma (in lattice) meet_assoc: |
|
14693 | 637 |
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
14551 | 638 |
shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
639 |
proof - |
|
640 |
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) |
|
641 |
also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma) |
|
642 |
also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) |
|
643 |
also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma) |
|
644 |
finally show ?thesis . |
|
645 |
qed |
|
646 |
||
14693 | 647 |
|
14551 | 648 |
subsection {* Total Orders *} |
649 |
||
650 |
locale total_order = lattice + |
|
651 |
assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
|
652 |
||
653 |
text {* Introduction rule: the usual definition of total order *} |
|
654 |
||
655 |
lemma (in partial_order) total_orderI: |
|
656 |
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
|
657 |
shows "total_order L" |
|
658 |
proof (rule total_order.intro) |
|
659 |
show "lattice_axioms L" |
|
660 |
proof (rule lattice_axioms.intro) |
|
661 |
fix x y |
|
14693 | 662 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
14551 | 663 |
show "EX s. least L s (Upper L {x, y})" |
664 |
proof - |
|
665 |
note total L |
|
666 |
moreover |
|
667 |
{ |
|
14693 | 668 |
assume "x \<sqsubseteq> y" |
14551 | 669 |
with L have "least L y (Upper L {x, y})" |
14693 | 670 |
by (rule_tac least_UpperI) auto |
14551 | 671 |
} |
672 |
moreover |
|
673 |
{ |
|
14693 | 674 |
assume "y \<sqsubseteq> x" |
14551 | 675 |
with L have "least L x (Upper L {x, y})" |
14693 | 676 |
by (rule_tac least_UpperI) auto |
14551 | 677 |
} |
678 |
ultimately show ?thesis by blast |
|
679 |
qed |
|
680 |
next |
|
681 |
fix x y |
|
14693 | 682 |
assume L: "x \<in> carrier L" "y \<in> carrier L" |
14551 | 683 |
show "EX i. greatest L i (Lower L {x, y})" |
684 |
proof - |
|
685 |
note total L |
|
686 |
moreover |
|
687 |
{ |
|
14693 | 688 |
assume "y \<sqsubseteq> x" |
14551 | 689 |
with L have "greatest L y (Lower L {x, y})" |
14693 | 690 |
by (rule_tac greatest_LowerI) auto |
14551 | 691 |
} |
692 |
moreover |
|
693 |
{ |
|
14693 | 694 |
assume "x \<sqsubseteq> y" |
14551 | 695 |
with L have "greatest L x (Lower L {x, y})" |
14693 | 696 |
by (rule_tac greatest_LowerI) auto |
14551 | 697 |
} |
698 |
ultimately show ?thesis by blast |
|
699 |
qed |
|
700 |
qed |
|
701 |
qed (assumption | rule total_order_axioms.intro)+ |
|
702 |
||
14693 | 703 |
|
14551 | 704 |
subsection {* Complete lattices *} |
705 |
||
706 |
locale complete_lattice = lattice + |
|
707 |
assumes sup_exists: |
|
708 |
"[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
|
709 |
and inf_exists: |
|
710 |
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" |
|
711 |
||
712 |
text {* Introduction rule: the usual definition of complete lattice *} |
|
713 |
||
714 |
lemma (in partial_order) complete_latticeI: |
|
715 |
assumes sup_exists: |
|
716 |
"!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
|
717 |
and inf_exists: |
|
718 |
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" |
|
719 |
shows "complete_lattice L" |
|
720 |
proof (rule complete_lattice.intro) |
|
721 |
show "lattice_axioms L" |
|
14693 | 722 |
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
14551 | 723 |
qed (assumption | rule complete_lattice_axioms.intro)+ |
724 |
||
14651 | 725 |
constdefs (structure L) |
726 |
top :: "_ => 'a" ("\<top>\<index>") |
|
727 |
"\<top> == sup L (carrier L)" |
|
14551 | 728 |
|
14651 | 729 |
bottom :: "_ => 'a" ("\<bottom>\<index>") |
730 |
"\<bottom> == inf L (carrier L)" |
|
14551 | 731 |
|
732 |
||
733 |
lemma (in complete_lattice) supI: |
|
734 |
"[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |] |
|
14651 | 735 |
==> P (\<Squnion>A)" |
14551 | 736 |
proof (unfold sup_def) |
737 |
assume L: "A \<subseteq> carrier L" |
|
738 |
and P: "!!l. least L l (Upper L A) ==> P l" |
|
739 |
with sup_exists obtain s where "least L s (Upper L A)" by blast |
|
740 |
with L show "P (THE l. least L l (Upper L A))" |
|
741 |
by (fast intro: theI2 least_unique P) |
|
742 |
qed |
|
743 |
||
744 |
lemma (in complete_lattice) sup_closed [simp]: |
|
14693 | 745 |
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" |
14551 | 746 |
by (rule supI) simp_all |
747 |
||
748 |
lemma (in complete_lattice) top_closed [simp, intro]: |
|
749 |
"\<top> \<in> carrier L" |
|
750 |
by (unfold top_def) simp |
|
751 |
||
752 |
lemma (in complete_lattice) infI: |
|
753 |
"[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] |
|
14693 | 754 |
==> P (\<Sqinter>A)" |
14551 | 755 |
proof (unfold inf_def) |
756 |
assume L: "A \<subseteq> carrier L" |
|
757 |
and P: "!!l. greatest L l (Lower L A) ==> P l" |
|
758 |
with inf_exists obtain s where "greatest L s (Lower L A)" by blast |
|
759 |
with L show "P (THE l. greatest L l (Lower L A))" |
|
760 |
by (fast intro: theI2 greatest_unique P) |
|
761 |
qed |
|
762 |
||
763 |
lemma (in complete_lattice) inf_closed [simp]: |
|
14693 | 764 |
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" |
14551 | 765 |
by (rule infI) simp_all |
766 |
||
767 |
lemma (in complete_lattice) bottom_closed [simp, intro]: |
|
768 |
"\<bottom> \<in> carrier L" |
|
769 |
by (unfold bottom_def) simp |
|
770 |
||
771 |
text {* Jacobson: Theorem 8.1 *} |
|
772 |
||
773 |
lemma Lower_empty [simp]: |
|
774 |
"Lower L {} = carrier L" |
|
775 |
by (unfold Lower_def) simp |
|
776 |
||
777 |
lemma Upper_empty [simp]: |
|
778 |
"Upper L {} = carrier L" |
|
779 |
by (unfold Upper_def) simp |
|
780 |
||
781 |
theorem (in partial_order) complete_lattice_criterion1: |
|
782 |
assumes top_exists: "EX g. greatest L g (carrier L)" |
|
783 |
and inf_exists: |
|
784 |
"!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" |
|
785 |
shows "complete_lattice L" |
|
786 |
proof (rule complete_latticeI) |
|
787 |
from top_exists obtain top where top: "greatest L top (carrier L)" .. |
|
788 |
fix A |
|
789 |
assume L: "A \<subseteq> carrier L" |
|
790 |
let ?B = "Upper L A" |
|
791 |
from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) |
|
792 |
then have B_non_empty: "?B ~= {}" by fast |
|
793 |
have B_L: "?B \<subseteq> carrier L" by simp |
|
794 |
from inf_exists [OF B_L B_non_empty] |
|
795 |
obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. |
|
796 |
have "least L b (Upper L A)" |
|
797 |
apply (rule least_UpperI) |
|
14693 | 798 |
apply (rule greatest_le [where A = "Lower L ?B"]) |
14551 | 799 |
apply (rule b_inf_B) |
800 |
apply (rule Lower_memI) |
|
801 |
apply (erule UpperD) |
|
802 |
apply assumption |
|
803 |
apply (rule L) |
|
804 |
apply (fast intro: L [THEN subsetD]) |
|
805 |
apply (erule greatest_Lower_above [OF b_inf_B]) |
|
806 |
apply simp |
|
807 |
apply (rule L) |
|
808 |
apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) |
|
809 |
done |
|
810 |
then show "EX s. least L s (Upper L A)" .. |
|
811 |
next |
|
812 |
fix A |
|
813 |
assume L: "A \<subseteq> carrier L" |
|
814 |
show "EX i. greatest L i (Lower L A)" |
|
815 |
proof (cases "A = {}") |
|
816 |
case True then show ?thesis |
|
817 |
by (simp add: top_exists) |
|
818 |
next |
|
819 |
case False with L show ?thesis |
|
820 |
by (rule inf_exists) |
|
821 |
qed |
|
822 |
qed |
|
823 |
||
824 |
(* TODO: prove dual version *) |
|
825 |
||
826 |
subsection {* Examples *} |
|
827 |
||
828 |
subsubsection {* Powerset of a set is a complete lattice *} |
|
829 |
||
830 |
theorem powerset_is_complete_lattice: |
|
831 |
"complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" |
|
832 |
(is "complete_lattice ?L") |
|
833 |
proof (rule partial_order.complete_latticeI) |
|
834 |
show "partial_order ?L" |
|
835 |
by (rule partial_order.intro) auto |
|
836 |
next |
|
837 |
fix B |
|
838 |
assume "B \<subseteq> carrier ?L" |
|
839 |
then have "least ?L (\<Union> B) (Upper ?L B)" |
|
840 |
by (fastsimp intro!: least_UpperI simp: Upper_def) |
|
841 |
then show "EX s. least ?L s (Upper ?L B)" .. |
|
842 |
next |
|
843 |
fix B |
|
844 |
assume "B \<subseteq> carrier ?L" |
|
845 |
then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" |
|
846 |
txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: |
|
847 |
@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} |
|
848 |
by (fastsimp intro!: greatest_LowerI simp: Lower_def) |
|
849 |
then show "EX i. greatest ?L i (Lower ?L B)" .. |
|
850 |
qed |
|
851 |
||
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
852 |
text {* An other example, that of the lattice of subgroups of a group, |
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset
|
853 |
can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} |
14551 | 854 |
|
14693 | 855 |
end |