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