src/HOL/Algebra/Lattice.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 19286 83404ccd270a permissions -rw-r--r--
Constant "If" is now local
1 (*
2   Title:     HOL/Algebra/Lattice.thy
3   Id:        $Id$
4   Author:    Clemens Ballarin, started 7 November 2003
5   Copyright: Clemens Ballarin
6 *)
8 header {* Orders and Lattices *}
10 theory Lattice imports Main begin
12 text {* Object with a carrier set. *}
14 record 'a partial_object =
15   carrier :: "'a set"
17 subsection {* Partial Orders *}
19 record 'a order = "'a partial_object" +
20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
22 locale partial_order = struct L +
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"
31 constdefs (structure L)
32   less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
33   "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
35   -- {* Upper and lower bounds of a set. *}
36   Upper :: "[_, 'a set] => 'a set"
37   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
38                 carrier L"
40   Lower :: "[_, 'a set] => 'a set"
41   "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
42                 carrier L"
44   -- {* Least and greatest, as predicate. *}
45   least :: "[_, 'a, 'a set] => bool"
46   "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
48   greatest :: "[_, 'a, 'a set] => bool"
49   "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
51   -- {* Supremum and infimum *}
52   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_"  90)
53   "\<Squnion>A == THE x. least L x (Upper L A)"
55   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_"  90)
56   "\<Sqinter>A == THE x. greatest L x (Lower L A)"
58   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
59   "x \<squnion> y == sup L {x, y}"
61   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
62   "x \<sqinter> y == inf L {x, y}"
65 subsubsection {* Upper *}
67 lemma Upper_closed [intro, simp]:
68   "Upper L A \<subseteq> carrier L"
69   by (unfold Upper_def) clarify
71 lemma UpperD [dest]:
72   includes struct L
73   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
74   by (unfold Upper_def) blast
76 lemma Upper_memI:
77   includes struct L
78   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
79   by (unfold Upper_def) blast
81 lemma Upper_antimono:
82   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
83   by (unfold Upper_def) blast
86 subsubsection {* Lower *}
88 lemma Lower_closed [intro, simp]:
89   "Lower L A \<subseteq> carrier L"
90   by (unfold Lower_def) clarify
92 lemma LowerD [dest]:
93   includes struct L
94   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
95   by (unfold Lower_def) blast
97 lemma Lower_memI:
98   includes struct L
99   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
100   by (unfold Lower_def) blast
102 lemma Lower_antimono:
103   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
104   by (unfold Lower_def) blast
107 subsubsection {* least *}
109 lemma least_carrier [intro, simp]:
110   shows "least L l A ==> l \<in> carrier L"
111   by (unfold least_def) fast
113 lemma least_mem:
114   "least L l A ==> l \<in> A"
115   by (unfold least_def) fast
117 lemma (in partial_order) least_unique:
118   "[| least L x A; least L y A |] ==> x = y"
119   by (unfold least_def) blast
121 lemma least_le:
122   includes struct L
123   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
124   by (unfold least_def) fast
126 lemma least_UpperI:
127   includes struct L
128   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
129     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
130     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
131   shows "least L s (Upper L A)"
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)
137 qed
140 subsubsection {* greatest *}
142 lemma greatest_carrier [intro, simp]:
143   shows "greatest L l A ==> l \<in> carrier L"
144   by (unfold greatest_def) fast
146 lemma greatest_mem:
147   "greatest L l A ==> l \<in> A"
148   by (unfold greatest_def) fast
150 lemma (in partial_order) greatest_unique:
151   "[| greatest L x A; greatest L y A |] ==> x = y"
152   by (unfold greatest_def) blast
154 lemma greatest_le:
155   includes struct L
156   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
157   by (unfold greatest_def) fast
159 lemma greatest_LowerI:
160   includes struct L
161   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
162     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
163     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
164   shows "greatest L i (Lower L A)"
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)
170 qed
173 subsection {* Lattices *}
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})"
181 lemma least_Upper_above:
182   includes struct L
183   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
184   by (unfold least_def) blast
186 lemma greatest_Lower_above:
187   includes struct L
188   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
189   by (unfold greatest_def) blast
192 subsubsection {* Supremum *}
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)
198   assume L: "x \<in> carrier L"  "y \<in> carrier L"
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}))"
202     by (fast intro: theI2 least_unique P)
203 qed
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)
209 lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
210   "x \<in> carrier L ==> least L x (Upper L {x})"
211   by (rule least_UpperI) fast+
213 lemma (in partial_order) sup_of_singleton [simp]:
214   includes struct L
215   shows "x \<in> carrier L ==> \<Squnion>{x} = x"
216   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
219 text {* Condition on @{text A}: supremum exists. *}
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 |]
224   ==> P (\<Squnion>(insert x A))"
225 proof (unfold sup_def)
226   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
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)))"
233   proof (rule theI2)
234     show "least L s (Upper L (insert x A))"
235     proof (rule least_UpperI)
236       fix z
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
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)
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)
288 	qed
289       next
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])
309       next
310         from L show "insert x A \<subseteq> carrier L" by simp
311         from least_s show "s \<in> carrier L" by simp
312       qed
313     qed
314   qed
315 qed
317 lemma (in lattice) finite_sup_least:
318   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
319 proof (induct set: Finites)
320   case empty
321   then show ?case by simp
322 next
323   case (insert x A)
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
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])
333   qed
334 qed
336 lemma (in lattice) finite_sup_insertI:
337   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
338     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
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
348 lemma (in lattice) finite_sup_closed:
349   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
350 proof (induct set: Finites)
351   case empty then show ?case by simp
352 next
353   case insert then show ?case
354     by - (rule finite_sup_insertI, simp_all)
355 qed
357 lemma (in lattice) join_left:
358   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
359   by (rule joinI [folded join_def]) (blast dest: least_mem)
361 lemma (in lattice) join_right:
362   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
363   by (rule joinI [folded join_def]) (blast dest: least_mem)
365 lemma (in lattice) sup_of_two_least:
366   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
367 proof (unfold sup_def)
368   assume L: "x \<in> carrier L"  "y \<in> carrier L"
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
374 lemma (in lattice) join_le:
375   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
376     and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
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
384 lemma (in lattice) join_assoc_lemma:
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}"
387 proof (rule finite_sup_insertI)
388   -- {* The textbook argument in Jacobson I, p 457 *}
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)
402 lemma join_comm:
403   includes struct L
404   shows "x \<squnion> y = y \<squnion> x"
405   by (unfold join_def) (simp add: insert_commute)
407 lemma (in lattice) join_assoc:
408   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
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)
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)
414   also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)
415   finally show ?thesis .
416 qed
419 subsubsection {* Infimum *}
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)
426   assume L: "x \<in> carrier L"  "y \<in> carrier L"
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
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)
437 lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
438   "x \<in> carrier L ==> greatest L x (Lower L {x})"
439   by (rule greatest_LowerI) fast+
441 lemma (in partial_order) inf_of_singleton [simp]:
442   includes struct L
443   shows "x \<in> carrier L ==> \<Sqinter> {x} = x"
444   by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
446 text {* Condition on A: infimum exists. *}
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 |]
451   ==> P (\<Sqinter>(insert x A))"
452 proof (unfold inf_def)
453   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
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)))"
460   proof (rule theI2)
461     show "greatest L i (Lower L (insert x A))"
462     proof (rule greatest_LowerI)
463       fix z
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
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)
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
516       next
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
534 	  qed
535         qed (rule Lower_closed [THEN subsetD])
536       next
537         from L show "insert x A \<subseteq> carrier L" by simp
538         from greatest_i show "i \<in> carrier L" by simp
539       qed
540     qed
541   qed
542 qed
544 lemma (in lattice) finite_inf_greatest:
545   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
546 proof (induct set: Finites)
547   case empty then show ?case by simp
548 next
549   case (insert x A)
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)
558       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
559     qed simp_all
560   qed
561 qed
563 lemma (in lattice) finite_inf_insertI:
564   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
565     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
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
575 lemma (in lattice) finite_inf_closed:
576   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
577 proof (induct set: Finites)
578   case empty then show ?case by simp
579 next
580   case insert then show ?case
581     by (rule_tac finite_inf_insertI) (simp_all)
582 qed
584 lemma (in lattice) meet_left:
585   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
586   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
588 lemma (in lattice) meet_right:
589   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
590   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
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)
596   assume L: "x \<in> carrier L"  "y \<in> carrier L"
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
603 lemma (in lattice) meet_le:
604   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
605     and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
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
613 lemma (in lattice) meet_assoc_lemma:
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}"
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)
631 lemma meet_comm:
632   includes struct L
633   shows "x \<sqinter> y = y \<sqinter> x"
634   by (unfold meet_def) (simp add: insert_commute)
636 lemma (in lattice) meet_assoc:
637   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
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
648 subsection {* Total Orders *}
650 locale total_order = lattice +
651   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
653 text {* Introduction rule: the usual definition of total order *}
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
662     assume L: "x \<in> carrier L"  "y \<in> carrier L"
663     show "EX s. least L s (Upper L {x, y})"
664     proof -
665       note total L
666       moreover
667       {
668         assume "x \<sqsubseteq> y"
669         with L have "least L y (Upper L {x, y})"
670           by (rule_tac least_UpperI) auto
671       }
672       moreover
673       {
674         assume "y \<sqsubseteq> x"
675         with L have "least L x (Upper L {x, y})"
676           by (rule_tac least_UpperI) auto
677       }
678       ultimately show ?thesis by blast
679     qed
680   next
681     fix x y
682     assume L: "x \<in> carrier L"  "y \<in> carrier L"
683     show "EX i. greatest L i (Lower L {x, y})"
684     proof -
685       note total L
686       moreover
687       {
688         assume "y \<sqsubseteq> x"
689         with L have "greatest L y (Lower L {x, y})"
690           by (rule_tac greatest_LowerI) auto
691       }
692       moreover
693       {
694         assume "x \<sqsubseteq> y"
695         with L have "greatest L x (Lower L {x, y})"
696           by (rule_tac greatest_LowerI) auto
697       }
698       ultimately show ?thesis by blast
699     qed
700   qed
701 qed (assumption | rule total_order_axioms.intro)+
704 subsection {* Complete lattices *}
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)"
712 text {* Introduction rule: the usual definition of complete lattice *}
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"
722     by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
723 qed (assumption | rule complete_lattice_axioms.intro)+
725 constdefs (structure L)
726   top :: "_ => 'a" ("\<top>\<index>")
727   "\<top> == sup L (carrier L)"
729   bottom :: "_ => 'a" ("\<bottom>\<index>")
730   "\<bottom> == inf L (carrier L)"
733 lemma (in complete_lattice) supI:
734   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
735   ==> P (\<Squnion>A)"
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
744 lemma (in complete_lattice) sup_closed [simp]:
745   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
746   by (rule supI) simp_all
748 lemma (in complete_lattice) top_closed [simp, intro]:
749   "\<top> \<in> carrier L"
750   by (unfold top_def) simp
752 lemma (in complete_lattice) infI:
753   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
754   ==> P (\<Sqinter>A)"
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
763 lemma (in complete_lattice) inf_closed [simp]:
764   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
765   by (rule infI) simp_all
767 lemma (in complete_lattice) bottom_closed [simp, intro]:
768   "\<bottom> \<in> carrier L"
769   by (unfold bottom_def) simp
771 text {* Jacobson: Theorem 8.1 *}
773 lemma Lower_empty [simp]:
774   "Lower L {} = carrier L"
775   by (unfold Lower_def) simp
777 lemma Upper_empty [simp]:
778   "Upper L {} = carrier L"
779   by (unfold Upper_def) simp
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)
798    apply (rule greatest_le [where A = "Lower L ?B"])
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
824 (* TODO: prove dual version *)
826 subsection {* Examples *}
828 subsubsection {* Powerset of a set is a complete lattice *}
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
852 text {* An other example, that of the lattice of subgroups of a group,
853   can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
855 end