src/HOL/Algebra/Lattice.thy
 author wenzelm Thu Mar 26 20:08:55 2009 +0100 (2009-03-26) changeset 30729 461ee3e49ad3 parent 30363 9b8d9b6ef803 child 32960 69916a850301 permissions -rw-r--r--
interpretation/interpret: prefixes are mandatory by default;
1 (*
2   Title:     HOL/Algebra/Lattice.thy
3   Author:    Clemens Ballarin, started 7 November 2003
4   Copyright: Clemens Ballarin
6 Most congruence rules by Stephan Hohe.
7 *)
9 theory Lattice imports Congruence begin
11 section {* Orders and Lattices *}
13 subsection {* Partial Orders *}
15 record 'a gorder = "'a eq_object" +
16   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
18 locale weak_partial_order = equivalence L for L (structure) +
19   assumes le_refl [intro, simp]:
20       "x \<in> carrier L ==> x \<sqsubseteq> x"
21     and weak_le_anti_sym [intro]:
22       "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
23     and le_trans [trans]:
24       "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
25     and le_cong:
26       "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
28 constdefs (structure L)
29   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
30   "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
33 subsubsection {* The order relation *}
35 context weak_partial_order begin
37 lemma le_cong_l [intro, trans]:
38   "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
39   by (auto intro: le_cong [THEN iffD2])
41 lemma le_cong_r [intro, trans]:
42   "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
43   by (auto intro: le_cong [THEN iffD1])
45 lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
46   by (simp add: le_cong_l)
48 end
50 lemma weak_llessI:
51   fixes R (structure)
52   assumes "x \<sqsubseteq> y" and "~(x .= y)"
53   shows "x \<sqsubset> y"
54   using assms unfolding lless_def by simp
56 lemma lless_imp_le:
57   fixes R (structure)
58   assumes "x \<sqsubset> y"
59   shows "x \<sqsubseteq> y"
60   using assms unfolding lless_def by simp
62 lemma weak_lless_imp_not_eq:
63   fixes R (structure)
64   assumes "x \<sqsubset> y"
65   shows "\<not> (x .= y)"
66   using assms unfolding lless_def by simp
68 lemma weak_llessE:
69   fixes R (structure)
70   assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
71   shows "P"
72   using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
74 lemma (in weak_partial_order) lless_cong_l [trans]:
75   assumes xx': "x .= x'"
76     and xy: "x' \<sqsubset> y"
77     and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
78   shows "x \<sqsubset> y"
79   using assms unfolding lless_def by (auto intro: trans sym)
81 lemma (in weak_partial_order) lless_cong_r [trans]:
82   assumes xy: "x \<sqsubset> y"
83     and  yy': "y .= y'"
84     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
85   shows "x \<sqsubset> y'"
86   using assms unfolding lless_def by (auto intro: trans sym)
89 lemma (in weak_partial_order) lless_antisym:
90   assumes "a \<in> carrier L" "b \<in> carrier L"
91     and "a \<sqsubset> b" "b \<sqsubset> a"
92   shows "P"
93   using assms
94   by (elim weak_llessE) auto
96 lemma (in weak_partial_order) lless_trans [trans]:
97   assumes "a \<sqsubset> b" "b \<sqsubset> c"
98     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
99   shows "a \<sqsubset> c"
100   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
103 subsubsection {* Upper and lower bounds of a set *}
105 constdefs (structure L)
106   Upper :: "[_, 'a set] => 'a set"
107   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
109   Lower :: "[_, 'a set] => 'a set"
110   "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
112 lemma Upper_closed [intro!, simp]:
113   "Upper L A \<subseteq> carrier L"
114   by (unfold Upper_def) clarify
116 lemma Upper_memD [dest]:
117   fixes L (structure)
118   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
119   by (unfold Upper_def) blast
121 lemma (in weak_partial_order) Upper_elemD [dest]:
122   "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
123   unfolding Upper_def elem_def
124   by (blast dest: sym)
126 lemma Upper_memI:
127   fixes L (structure)
128   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
129   by (unfold Upper_def) blast
131 lemma (in weak_partial_order) Upper_elemI:
132   "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
133   unfolding Upper_def by blast
135 lemma Upper_antimono:
136   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
137   by (unfold Upper_def) blast
139 lemma (in weak_partial_order) Upper_is_closed [simp]:
140   "A \<subseteq> carrier L ==> is_closed (Upper L A)"
141   by (rule is_closedI) (blast intro: Upper_memI)+
143 lemma (in weak_partial_order) Upper_mem_cong:
144   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
145     and aa': "a .= a'"
146     and aelem: "a \<in> Upper L A"
147   shows "a' \<in> Upper L A"
148 proof (rule Upper_memI[OF _ a'carr])
149   fix y
150   assume yA: "y \<in> A"
151   hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
152   also note aa'
153   finally
154       show "y \<sqsubseteq> a'"
155       by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
156 qed
158 lemma (in weak_partial_order) Upper_cong:
159   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
160     and AA': "A {.=} A'"
161   shows "Upper L A = Upper L A'"
162 unfolding Upper_def
163 apply rule
164  apply (rule, clarsimp) defer 1
165  apply (rule, clarsimp) defer 1
166 proof -
167   fix x a'
168   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
169     and a'A': "a' \<in> A'"
170   assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
172   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
173   from this obtain a
174       where aA: "a \<in> A"
175       and a'a: "a' .= a"
176       by auto
177   note [simp] = subsetD[OF Acarr aA] carr
179   note a'a
180   also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
181   finally show "a' \<sqsubseteq> x" by simp
182 next
183   fix x a
184   assume carr: "x \<in> carrier L" "a \<in> carrier L"
185     and aA: "a \<in> A"
186   assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
188   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
189   from this obtain a'
190       where a'A': "a' \<in> A'"
191       and aa': "a .= a'"
192       by auto
193   note [simp] = subsetD[OF A'carr a'A'] carr
195   note aa'
196   also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
197   finally show "a \<sqsubseteq> x" by simp
198 qed
200 lemma Lower_closed [intro!, simp]:
201   "Lower L A \<subseteq> carrier L"
202   by (unfold Lower_def) clarify
204 lemma Lower_memD [dest]:
205   fixes L (structure)
206   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
207   by (unfold Lower_def) blast
209 lemma Lower_memI:
210   fixes L (structure)
211   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
212   by (unfold Lower_def) blast
214 lemma Lower_antimono:
215   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
216   by (unfold Lower_def) blast
218 lemma (in weak_partial_order) Lower_is_closed [simp]:
219   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
220   by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
222 lemma (in weak_partial_order) Lower_mem_cong:
223   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
224     and aa': "a .= a'"
225     and aelem: "a \<in> Lower L A"
226   shows "a' \<in> Lower L A"
227 using assms Lower_closed[of L A]
228 by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
230 lemma (in weak_partial_order) Lower_cong:
231   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
232     and AA': "A {.=} A'"
233   shows "Lower L A = Lower L A'"
234 using Lower_memD[of y]
235 unfolding Lower_def
236 apply safe
237  apply clarsimp defer 1
238  apply clarsimp defer 1
239 proof -
240   fix x a'
241   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
242     and a'A': "a' \<in> A'"
243   assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
244   hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
246   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
247   from this obtain a
248       where aA: "a \<in> A"
249       and a'a: "a' .= a"
250       by auto
252   from aA and subsetD[OF Acarr aA]
253       have "x \<sqsubseteq> a" by (rule aLxCond)
254   also note a'a[symmetric]
255   finally
256       show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
257 next
258   fix x a
259   assume carr: "x \<in> carrier L" "a \<in> carrier L"
260     and aA: "a \<in> A"
261   assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
262   hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
264   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
265   from this obtain a'
266       where a'A': "a' \<in> A'"
267       and aa': "a .= a'"
268       by auto
269   from a'A' and subsetD[OF A'carr a'A']
270       have "x \<sqsubseteq> a'" by (rule a'LxCond)
271   also note aa'[symmetric]
272   finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
273 qed
276 subsubsection {* Least and greatest, as predicate *}
278 constdefs (structure L)
279   least :: "[_, 'a, 'a set] => bool"
280   "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
282   greatest :: "[_, 'a, 'a set] => bool"
283   "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
285 text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
286   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
288 lemma least_closed [intro, simp]:
289   "least L l A ==> l \<in> carrier L"
290   by (unfold least_def) fast
292 lemma least_mem:
293   "least L l A ==> l \<in> A"
294   by (unfold least_def) fast
296 lemma (in weak_partial_order) weak_least_unique:
297   "[| least L x A; least L y A |] ==> x .= y"
298   by (unfold least_def) blast
300 lemma least_le:
301   fixes L (structure)
302   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
303   by (unfold least_def) fast
305 lemma (in weak_partial_order) least_cong:
306   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
307   by (unfold least_def) (auto dest: sym)
309 text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for
310   @{term "A {.=} A'"} *}
312 lemma (in weak_partial_order) least_Upper_cong_l:
313   assumes "x .= x'"
314     and "x \<in> carrier L" "x' \<in> carrier L"
315     and "A \<subseteq> carrier L"
316   shows "least L x (Upper L A) = least L x' (Upper L A)"
317   apply (rule least_cong) using assms by auto
319 lemma (in weak_partial_order) least_Upper_cong_r:
320   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
321     and AA': "A {.=} A'"
322   shows "least L x (Upper L A) = least L x (Upper L A')"
323 apply (subgoal_tac "Upper L A = Upper L A'", simp)
324 by (rule Upper_cong) fact+
326 lemma least_UpperI:
327   fixes L (structure)
328   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
329     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
330     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
331   shows "least L s (Upper L A)"
332 proof -
333   have "Upper L A \<subseteq> carrier L" by simp
334   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
335   moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
336   ultimately show ?thesis by (simp add: least_def)
337 qed
339 lemma least_Upper_above:
340   fixes L (structure)
341   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
342   by (unfold least_def) blast
344 lemma greatest_closed [intro, simp]:
345   "greatest L l A ==> l \<in> carrier L"
346   by (unfold greatest_def) fast
348 lemma greatest_mem:
349   "greatest L l A ==> l \<in> A"
350   by (unfold greatest_def) fast
352 lemma (in weak_partial_order) weak_greatest_unique:
353   "[| greatest L x A; greatest L y A |] ==> x .= y"
354   by (unfold greatest_def) blast
356 lemma greatest_le:
357   fixes L (structure)
358   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
359   by (unfold greatest_def) fast
361 lemma (in weak_partial_order) greatest_cong:
362   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
363   greatest L x A = greatest L x' A"
364   by (unfold greatest_def) (auto dest: sym)
366 text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for
367   @{term "A {.=} A'"} *}
369 lemma (in weak_partial_order) greatest_Lower_cong_l:
370   assumes "x .= x'"
371     and "x \<in> carrier L" "x' \<in> carrier L"
372     and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
373   shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
374   apply (rule greatest_cong) using assms by auto
376 lemma (in weak_partial_order) greatest_Lower_cong_r:
377   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
378     and AA': "A {.=} A'"
379   shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
380 apply (subgoal_tac "Lower L A = Lower L A'", simp)
381 by (rule Lower_cong) fact+
383 lemma greatest_LowerI:
384   fixes L (structure)
385   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
386     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
387     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
388   shows "greatest L i (Lower L A)"
389 proof -
390   have "Lower L A \<subseteq> carrier L" by simp
391   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
392   moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
393   ultimately show ?thesis by (simp add: greatest_def)
394 qed
396 lemma greatest_Lower_below:
397   fixes L (structure)
398   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
399   by (unfold greatest_def) blast
401 text {* Supremum and infimum *}
403 constdefs (structure L)
404   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_"  90)
405   "\<Squnion>A == SOME x. least L x (Upper L A)"
407   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_"  90)
408   "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
410   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
411   "x \<squnion> y == \<Squnion> {x, y}"
413   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
414   "x \<sqinter> y == \<Sqinter> {x, y}"
417 subsection {* Lattices *}
419 locale weak_upper_semilattice = weak_partial_order +
420   assumes sup_of_two_exists:
421     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
423 locale weak_lower_semilattice = weak_partial_order +
424   assumes inf_of_two_exists:
425     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
427 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
430 subsubsection {* Supremum *}
432 lemma (in weak_upper_semilattice) joinI:
433   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
434   ==> P (x \<squnion> y)"
435 proof (unfold join_def sup_def)
436   assume L: "x \<in> carrier L"  "y \<in> carrier L"
437     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
438   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
439   with L show "P (SOME l. least L l (Upper L {x, y}))"
440     by (fast intro: someI2 P)
441 qed
443 lemma (in weak_upper_semilattice) join_closed [simp]:
444   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
445   by (rule joinI) (rule least_closed)
447 lemma (in weak_upper_semilattice) join_cong_l:
448   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
449     and xx': "x .= x'"
450   shows "x \<squnion> y .= x' \<squnion> y"
451 proof (rule joinI, rule joinI)
452   fix a b
453   from xx' carr
454       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
456   assume leasta: "least L a (Upper L {x, y})"
457   assume "least L b (Upper L {x', y})"
458   with carr
459       have leastb: "least L b (Upper L {x, y})"
460       by (simp add: least_Upper_cong_r[OF _ _ seq])
462   from leasta leastb
463       show "a .= b" by (rule weak_least_unique)
464 qed (rule carr)+
466 lemma (in weak_upper_semilattice) join_cong_r:
467   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
468     and yy': "y .= y'"
469   shows "x \<squnion> y .= x \<squnion> y'"
470 proof (rule joinI, rule joinI)
471   fix a b
472   have "{x, y} = {y, x}" by fast
473   also from carr yy'
474       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
475   also have "{y', x} = {x, y'}" by fast
476   finally
477       have seq: "{x, y} {.=} {x, y'}" .
479   assume leasta: "least L a (Upper L {x, y})"
480   assume "least L b (Upper L {x, y'})"
481   with carr
482       have leastb: "least L b (Upper L {x, y})"
483       by (simp add: least_Upper_cong_r[OF _ _ seq])
485   from leasta leastb
486       show "a .= b" by (rule weak_least_unique)
487 qed (rule carr)+
489 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
490   "x \<in> carrier L ==> least L x (Upper L {x})"
491   by (rule least_UpperI) auto
493 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
494   "x \<in> carrier L ==> \<Squnion>{x} .= x"
495   unfolding sup_def
496   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
498 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
499   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
500   unfolding sup_def
501   by (rule someI2) (auto intro: sup_of_singletonI)
503 text {* Condition on @{text A}: supremum exists. *}
505 lemma (in weak_upper_semilattice) sup_insertI:
506   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
507   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
508   ==> P (\<Squnion>(insert x A))"
509 proof (unfold sup_def)
510   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
511     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
512     and least_a: "least L a (Upper L A)"
513   from L least_a have La: "a \<in> carrier L" by simp
514   from L sup_of_two_exists least_a
515   obtain s where least_s: "least L s (Upper L {a, x})" by blast
516   show "P (SOME l. least L l (Upper L (insert x A)))"
517   proof (rule someI2)
518     show "least L s (Upper L (insert x A))"
519     proof (rule least_UpperI)
520       fix z
521       assume "z \<in> insert x A"
522       then show "z \<sqsubseteq> s"
523       proof
524         assume "z = x" then show ?thesis
525           by (simp add: least_Upper_above [OF least_s] L La)
526       next
527         assume "z \<in> A"
528         with L least_s least_a show ?thesis
529           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
530       qed
531     next
532       fix y
533       assume y: "y \<in> Upper L (insert x A)"
534       show "s \<sqsubseteq> y"
535       proof (rule least_le [OF least_s], rule Upper_memI)
536 	fix z
537 	assume z: "z \<in> {a, x}"
538 	then show "z \<sqsubseteq> y"
539 	proof
540           have y': "y \<in> Upper L A"
541             apply (rule subsetD [where A = "Upper L (insert x A)"])
542              apply (rule Upper_antimono)
543 	     apply blast
544 	    apply (rule y)
545             done
546           assume "z = a"
547           with y' least_a show ?thesis by (fast dest: least_le)
548 	next
549 	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
550           with y L show ?thesis by blast
551 	qed
552       qed (rule Upper_closed [THEN subsetD, OF y])
553     next
554       from L show "insert x A \<subseteq> carrier L" by simp
555       from least_s show "s \<in> carrier L" by simp
556     qed
557   qed (rule P)
558 qed
560 lemma (in weak_upper_semilattice) finite_sup_least:
561   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
562 proof (induct set: finite)
563   case empty
564   then show ?case by simp
565 next
566   case (insert x A)
567   show ?case
568   proof (cases "A = {}")
569     case True
570     with insert show ?thesis
571       by simp (simp add: least_cong [OF weak_sup_of_singleton]
572 	sup_of_singleton_closed sup_of_singletonI)
573 	(* The above step is hairy; least_cong can make simp loop.
574 	Would want special version of simp to apply least_cong. *)
575   next
576     case False
577     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
578     with _ show ?thesis
579       by (rule sup_insertI) (simp_all add: insert [simplified])
580   qed
581 qed
583 lemma (in weak_upper_semilattice) finite_sup_insertI:
584   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
585     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
586   shows "P (\<Squnion> (insert x A))"
587 proof (cases "A = {}")
588   case True with P and xA show ?thesis
589     by (simp add: finite_sup_least)
590 next
591   case False with P and xA show ?thesis
592     by (simp add: sup_insertI finite_sup_least)
593 qed
595 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
596   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
597 proof (induct set: finite)
598   case empty then show ?case by simp
599 next
600   case insert then show ?case
601     by - (rule finite_sup_insertI, simp_all)
602 qed
604 lemma (in weak_upper_semilattice) join_left:
605   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
606   by (rule joinI [folded join_def]) (blast dest: least_mem)
608 lemma (in weak_upper_semilattice) join_right:
609   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
610   by (rule joinI [folded join_def]) (blast dest: least_mem)
612 lemma (in weak_upper_semilattice) sup_of_two_least:
613   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
614 proof (unfold sup_def)
615   assume L: "x \<in> carrier L"  "y \<in> carrier L"
616   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
617   with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
618   by (fast intro: someI2 weak_least_unique)  (* blast fails *)
619 qed
621 lemma (in weak_upper_semilattice) join_le:
622   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
623     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
624   shows "x \<squnion> y \<sqsubseteq> z"
625 proof (rule joinI [OF _ x y])
626   fix s
627   assume "least L s (Upper L {x, y})"
628   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
629 qed
631 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
632   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
633   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
634 proof (rule finite_sup_insertI)
635   -- {* The textbook argument in Jacobson I, p 457 *}
636   fix s
637   assume sup: "least L s (Upper L {x, y, z})"
638   show "x \<squnion> (y \<squnion> z) .= s"
639   proof (rule weak_le_anti_sym)
640     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
641       by (fastsimp intro!: join_le elim: least_Upper_above)
642   next
643     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
644     by (erule_tac least_le)
645       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
646   qed (simp_all add: L least_closed [OF sup])
647 qed (simp_all add: L)
649 text {* Commutativity holds for @{text "="}. *}
651 lemma join_comm:
652   fixes L (structure)
653   shows "x \<squnion> y = y \<squnion> x"
654   by (unfold join_def) (simp add: insert_commute)
656 lemma (in weak_upper_semilattice) weak_join_assoc:
657   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
658   shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
659 proof -
660   (* FIXME: could be simplified by improved simp: uniform use of .=,
661      omit [symmetric] in last step. *)
662   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
663   also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
664   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
665   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
666   finally show ?thesis by (simp add: L)
667 qed
670 subsubsection {* Infimum *}
672 lemma (in weak_lower_semilattice) meetI:
673   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
674   x \<in> carrier L; y \<in> carrier L |]
675   ==> P (x \<sqinter> y)"
676 proof (unfold meet_def inf_def)
677   assume L: "x \<in> carrier L"  "y \<in> carrier L"
678     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
679   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
680   with L show "P (SOME g. greatest L g (Lower L {x, y}))"
681   by (fast intro: someI2 weak_greatest_unique P)
682 qed
684 lemma (in weak_lower_semilattice) meet_closed [simp]:
685   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
686   by (rule meetI) (rule greatest_closed)
688 lemma (in weak_lower_semilattice) meet_cong_l:
689   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
690     and xx': "x .= x'"
691   shows "x \<sqinter> y .= x' \<sqinter> y"
692 proof (rule meetI, rule meetI)
693   fix a b
694   from xx' carr
695       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
697   assume greatesta: "greatest L a (Lower L {x, y})"
698   assume "greatest L b (Lower L {x', y})"
699   with carr
700       have greatestb: "greatest L b (Lower L {x, y})"
701       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
703   from greatesta greatestb
704       show "a .= b" by (rule weak_greatest_unique)
705 qed (rule carr)+
707 lemma (in weak_lower_semilattice) meet_cong_r:
708   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
709     and yy': "y .= y'"
710   shows "x \<sqinter> y .= x \<sqinter> y'"
711 proof (rule meetI, rule meetI)
712   fix a b
713   have "{x, y} = {y, x}" by fast
714   also from carr yy'
715       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
716   also have "{y', x} = {x, y'}" by fast
717   finally
718       have seq: "{x, y} {.=} {x, y'}" .
720   assume greatesta: "greatest L a (Lower L {x, y})"
721   assume "greatest L b (Lower L {x, y'})"
722   with carr
723       have greatestb: "greatest L b (Lower L {x, y})"
724       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
726   from greatesta greatestb
727       show "a .= b" by (rule weak_greatest_unique)
728 qed (rule carr)+
730 lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
731   "x \<in> carrier L ==> greatest L x (Lower L {x})"
732   by (rule greatest_LowerI) auto
734 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
735   "x \<in> carrier L ==> \<Sqinter>{x} .= x"
736   unfolding inf_def
737   by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
739 lemma (in weak_partial_order) inf_of_singleton_closed:
740   "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
741   unfolding inf_def
742   by (rule someI2) (auto intro: inf_of_singletonI)
744 text {* Condition on @{text A}: infimum exists. *}
746 lemma (in weak_lower_semilattice) inf_insertI:
747   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
748   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
749   ==> P (\<Sqinter>(insert x A))"
750 proof (unfold inf_def)
751   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
752     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
753     and greatest_a: "greatest L a (Lower L A)"
754   from L greatest_a have La: "a \<in> carrier L" by simp
755   from L inf_of_two_exists greatest_a
756   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
757   show "P (SOME g. greatest L g (Lower L (insert x A)))"
758   proof (rule someI2)
759     show "greatest L i (Lower L (insert x A))"
760     proof (rule greatest_LowerI)
761       fix z
762       assume "z \<in> insert x A"
763       then show "i \<sqsubseteq> z"
764       proof
765         assume "z = x" then show ?thesis
766           by (simp add: greatest_Lower_below [OF greatest_i] L La)
767       next
768         assume "z \<in> A"
769         with L greatest_i greatest_a show ?thesis
770           by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
771       qed
772     next
773       fix y
774       assume y: "y \<in> Lower L (insert x A)"
775       show "y \<sqsubseteq> i"
776       proof (rule greatest_le [OF greatest_i], rule Lower_memI)
777 	fix z
778 	assume z: "z \<in> {a, x}"
779 	then show "y \<sqsubseteq> z"
780 	proof
781           have y': "y \<in> Lower L A"
782             apply (rule subsetD [where A = "Lower L (insert x A)"])
783             apply (rule Lower_antimono)
784 	     apply blast
785 	    apply (rule y)
786             done
787           assume "z = a"
788           with y' greatest_a show ?thesis by (fast dest: greatest_le)
789 	next
790           assume "z \<in> {x}"
791           with y L show ?thesis by blast
792 	qed
793       qed (rule Lower_closed [THEN subsetD, OF y])
794     next
795       from L show "insert x A \<subseteq> carrier L" by simp
796       from greatest_i show "i \<in> carrier L" by simp
797     qed
798   qed (rule P)
799 qed
801 lemma (in weak_lower_semilattice) finite_inf_greatest:
802   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
803 proof (induct set: finite)
804   case empty then show ?case by simp
805 next
806   case (insert x A)
807   show ?case
808   proof (cases "A = {}")
809     case True
810     with insert show ?thesis
811       by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
812 	inf_of_singleton_closed inf_of_singletonI)
813   next
814     case False
815     from insert show ?thesis
816     proof (rule_tac inf_insertI)
817       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
818     qed simp_all
819   qed
820 qed
822 lemma (in weak_lower_semilattice) finite_inf_insertI:
823   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
824     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
825   shows "P (\<Sqinter> (insert x A))"
826 proof (cases "A = {}")
827   case True with P and xA show ?thesis
828     by (simp add: finite_inf_greatest)
829 next
830   case False with P and xA show ?thesis
831     by (simp add: inf_insertI finite_inf_greatest)
832 qed
834 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
835   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
836 proof (induct set: finite)
837   case empty then show ?case by simp
838 next
839   case insert then show ?case
840     by (rule_tac finite_inf_insertI) (simp_all)
841 qed
843 lemma (in weak_lower_semilattice) meet_left:
844   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
845   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
847 lemma (in weak_lower_semilattice) meet_right:
848   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
849   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
851 lemma (in weak_lower_semilattice) inf_of_two_greatest:
852   "[| x \<in> carrier L; y \<in> carrier L |] ==>
853   greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
854 proof (unfold inf_def)
855   assume L: "x \<in> carrier L"  "y \<in> carrier L"
856   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
857   with L
858   show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
859   by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
860 qed
862 lemma (in weak_lower_semilattice) meet_le:
863   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
864     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
865   shows "z \<sqsubseteq> x \<sqinter> y"
866 proof (rule meetI [OF _ x y])
867   fix i
868   assume "greatest L i (Lower L {x, y})"
869   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
870 qed
872 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
873   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
874   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
875 proof (rule finite_inf_insertI)
876   txt {* The textbook argument in Jacobson I, p 457 *}
877   fix i
878   assume inf: "greatest L i (Lower L {x, y, z})"
879   show "x \<sqinter> (y \<sqinter> z) .= i"
880   proof (rule weak_le_anti_sym)
881     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
882       by (fastsimp intro!: meet_le elim: greatest_Lower_below)
883   next
884     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
885     by (erule_tac greatest_le)
886       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
887   qed (simp_all add: L greatest_closed [OF inf])
888 qed (simp_all add: L)
890 lemma meet_comm:
891   fixes L (structure)
892   shows "x \<sqinter> y = y \<sqinter> x"
893   by (unfold meet_def) (simp add: insert_commute)
895 lemma (in weak_lower_semilattice) weak_meet_assoc:
896   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
897   shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
898 proof -
899   (* FIXME: improved simp, see weak_join_assoc above *)
900   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
901   also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
902   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
903   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
904   finally show ?thesis by (simp add: L)
905 qed
908 subsection {* Total Orders *}
910 locale weak_total_order = weak_partial_order +
911   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
913 text {* Introduction rule: the usual definition of total order *}
915 lemma (in weak_partial_order) weak_total_orderI:
916   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
917   shows "weak_total_order L"
918   proof qed (rule total)
920 text {* Total orders are lattices. *}
922 sublocale weak_total_order < weak: weak_lattice
923 proof
924   fix x y
925   assume L: "x \<in> carrier L"  "y \<in> carrier L"
926   show "EX s. least L s (Upper L {x, y})"
927   proof -
928     note total L
929     moreover
930     {
931       assume "x \<sqsubseteq> y"
932       with L have "least L y (Upper L {x, y})"
933         by (rule_tac least_UpperI) auto
934     }
935     moreover
936     {
937       assume "y \<sqsubseteq> x"
938       with L have "least L x (Upper L {x, y})"
939         by (rule_tac least_UpperI) auto
940     }
941     ultimately show ?thesis by blast
942   qed
943 next
944   fix x y
945   assume L: "x \<in> carrier L"  "y \<in> carrier L"
946   show "EX i. greatest L i (Lower L {x, y})"
947   proof -
948     note total L
949     moreover
950     {
951       assume "y \<sqsubseteq> x"
952       with L have "greatest L y (Lower L {x, y})"
953         by (rule_tac greatest_LowerI) auto
954     }
955     moreover
956     {
957       assume "x \<sqsubseteq> y"
958       with L have "greatest L x (Lower L {x, y})"
959         by (rule_tac greatest_LowerI) auto
960     }
961     ultimately show ?thesis by blast
962   qed
963 qed
966 subsection {* Complete Lattices *}
968 locale weak_complete_lattice = weak_lattice +
969   assumes sup_exists:
970     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
971     and inf_exists:
972     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
974 text {* Introduction rule: the usual definition of complete lattice *}
976 lemma (in weak_partial_order) weak_complete_latticeI:
977   assumes sup_exists:
978     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
979     and inf_exists:
980     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
981   shows "weak_complete_lattice L"
982   proof qed (auto intro: sup_exists inf_exists)
984 constdefs (structure L)
985   top :: "_ => 'a" ("\<top>\<index>")
986   "\<top> == sup L (carrier L)"
988   bottom :: "_ => 'a" ("\<bottom>\<index>")
989   "\<bottom> == inf L (carrier L)"
992 lemma (in weak_complete_lattice) supI:
993   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
994   ==> P (\<Squnion>A)"
995 proof (unfold sup_def)
996   assume L: "A \<subseteq> carrier L"
997     and P: "!!l. least L l (Upper L A) ==> P l"
998   with sup_exists obtain s where "least L s (Upper L A)" by blast
999   with L show "P (SOME l. least L l (Upper L A))"
1000   by (fast intro: someI2 weak_least_unique P)
1001 qed
1003 lemma (in weak_complete_lattice) sup_closed [simp]:
1004   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
1005   by (rule supI) simp_all
1007 lemma (in weak_complete_lattice) top_closed [simp, intro]:
1008   "\<top> \<in> carrier L"
1009   by (unfold top_def) simp
1011 lemma (in weak_complete_lattice) infI:
1012   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
1013   ==> P (\<Sqinter>A)"
1014 proof (unfold inf_def)
1015   assume L: "A \<subseteq> carrier L"
1016     and P: "!!l. greatest L l (Lower L A) ==> P l"
1017   with inf_exists obtain s where "greatest L s (Lower L A)" by blast
1018   with L show "P (SOME l. greatest L l (Lower L A))"
1019   by (fast intro: someI2 weak_greatest_unique P)
1020 qed
1022 lemma (in weak_complete_lattice) inf_closed [simp]:
1023   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
1024   by (rule infI) simp_all
1026 lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
1027   "\<bottom> \<in> carrier L"
1028   by (unfold bottom_def) simp
1030 text {* Jacobson: Theorem 8.1 *}
1032 lemma Lower_empty [simp]:
1033   "Lower L {} = carrier L"
1034   by (unfold Lower_def) simp
1036 lemma Upper_empty [simp]:
1037   "Upper L {} = carrier L"
1038   by (unfold Upper_def) simp
1040 theorem (in weak_partial_order) weak_complete_lattice_criterion1:
1041   assumes top_exists: "EX g. greatest L g (carrier L)"
1042     and inf_exists:
1043       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
1044   shows "weak_complete_lattice L"
1045 proof (rule weak_complete_latticeI)
1046   from top_exists obtain top where top: "greatest L top (carrier L)" ..
1047   fix A
1048   assume L: "A \<subseteq> carrier L"
1049   let ?B = "Upper L A"
1050   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
1051   then have B_non_empty: "?B ~= {}" by fast
1052   have B_L: "?B \<subseteq> carrier L" by simp
1053   from inf_exists [OF B_L B_non_empty]
1054   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
1055   have "least L b (Upper L A)"
1056 apply (rule least_UpperI)
1057    apply (rule greatest_le [where A = "Lower L ?B"])
1058     apply (rule b_inf_B)
1059    apply (rule Lower_memI)
1060     apply (erule Upper_memD [THEN conjunct1])
1061      apply assumption
1062     apply (rule L)
1063    apply (fast intro: L [THEN subsetD])
1064   apply (erule greatest_Lower_below [OF b_inf_B])
1065   apply simp
1066  apply (rule L)
1067 apply (rule greatest_closed [OF b_inf_B])
1068 done
1069   then show "EX s. least L s (Upper L A)" ..
1070 next
1071   fix A
1072   assume L: "A \<subseteq> carrier L"
1073   show "EX i. greatest L i (Lower L A)"
1074   proof (cases "A = {}")
1075     case True then show ?thesis
1076       by (simp add: top_exists)
1077   next
1078     case False with L show ?thesis
1079       by (rule inf_exists)
1080   qed
1081 qed
1083 (* TODO: prove dual version *)
1086 subsection {* Orders and Lattices where @{text eq} is the Equality *}
1088 locale partial_order = weak_partial_order +
1089   assumes eq_is_equal: "op .= = op ="
1090 begin
1092 declare weak_le_anti_sym [rule del]
1094 lemma le_anti_sym [intro]:
1095   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
1096   using weak_le_anti_sym unfolding eq_is_equal .
1098 lemma lless_eq:
1099   "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
1100   unfolding lless_def by (simp add: eq_is_equal)
1102 lemma lless_asym:
1103   assumes "a \<in> carrier L" "b \<in> carrier L"
1104     and "a \<sqsubset> b" "b \<sqsubset> a"
1105   shows "P"
1106   using assms unfolding lless_eq by auto
1108 end
1111 text {* Least and greatest, as predicate *}
1113 lemma (in partial_order) least_unique:
1114   "[| least L x A; least L y A |] ==> x = y"
1115   using weak_least_unique unfolding eq_is_equal .
1117 lemma (in partial_order) greatest_unique:
1118   "[| greatest L x A; greatest L y A |] ==> x = y"
1119   using weak_greatest_unique unfolding eq_is_equal .
1122 text {* Lattices *}
1124 locale upper_semilattice = partial_order +
1125   assumes sup_of_two_exists:
1126     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
1128 sublocale upper_semilattice < weak: weak_upper_semilattice
1129   proof qed (rule sup_of_two_exists)
1131 locale lower_semilattice = partial_order +
1132   assumes inf_of_two_exists:
1133     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
1135 sublocale lower_semilattice < weak: weak_lower_semilattice
1136   proof qed (rule inf_of_two_exists)
1138 locale lattice = upper_semilattice + lower_semilattice
1141 text {* Supremum *}
1143 declare (in partial_order) weak_sup_of_singleton [simp del]
1145 lemma (in partial_order) sup_of_singleton [simp]:
1146   "x \<in> carrier L ==> \<Squnion>{x} = x"
1147   using weak_sup_of_singleton unfolding eq_is_equal .
1149 lemma (in upper_semilattice) join_assoc_lemma:
1150   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
1151   shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
1152   using weak_join_assoc_lemma L unfolding eq_is_equal .
1154 lemma (in upper_semilattice) join_assoc:
1155   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
1156   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
1157   using weak_join_assoc L unfolding eq_is_equal .
1160 text {* Infimum *}
1162 declare (in partial_order) weak_inf_of_singleton [simp del]
1164 lemma (in partial_order) inf_of_singleton [simp]:
1165   "x \<in> carrier L ==> \<Sqinter>{x} = x"
1166   using weak_inf_of_singleton unfolding eq_is_equal .
1168 text {* Condition on @{text A}: infimum exists. *}
1170 lemma (in lower_semilattice) meet_assoc_lemma:
1171   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
1172   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
1173   using weak_meet_assoc_lemma L unfolding eq_is_equal .
1175 lemma (in lower_semilattice) meet_assoc:
1176   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
1177   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
1178   using weak_meet_assoc L unfolding eq_is_equal .
1181 text {* Total Orders *}
1183 locale total_order = partial_order +
1184   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
1186 sublocale total_order < weak: weak_total_order
1187   proof qed (rule total_order_total)
1189 text {* Introduction rule: the usual definition of total order *}
1191 lemma (in partial_order) total_orderI:
1192   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
1193   shows "total_order L"
1194   proof qed (rule total)
1196 text {* Total orders are lattices. *}
1198 sublocale total_order < weak: lattice
1199   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
1202 text {* Complete lattices *}
1204 locale complete_lattice = lattice +
1205   assumes sup_exists:
1206     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
1207     and inf_exists:
1208     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
1210 sublocale complete_lattice < weak: weak_complete_lattice
1211   proof qed (auto intro: sup_exists inf_exists)
1213 text {* Introduction rule: the usual definition of complete lattice *}
1215 lemma (in partial_order) complete_latticeI:
1216   assumes sup_exists:
1217     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
1218     and inf_exists:
1219     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
1220   shows "complete_lattice L"
1221   proof qed (auto intro: sup_exists inf_exists)
1223 theorem (in partial_order) complete_lattice_criterion1:
1224   assumes top_exists: "EX g. greatest L g (carrier L)"
1225     and inf_exists:
1226       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
1227   shows "complete_lattice L"
1228 proof (rule complete_latticeI)
1229   from top_exists obtain top where top: "greatest L top (carrier L)" ..
1230   fix A
1231   assume L: "A \<subseteq> carrier L"
1232   let ?B = "Upper L A"
1233   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
1234   then have B_non_empty: "?B ~= {}" by fast
1235   have B_L: "?B \<subseteq> carrier L" by simp
1236   from inf_exists [OF B_L B_non_empty]
1237   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
1238   have "least L b (Upper L A)"
1239 apply (rule least_UpperI)
1240    apply (rule greatest_le [where A = "Lower L ?B"])
1241     apply (rule b_inf_B)
1242    apply (rule Lower_memI)
1243     apply (erule Upper_memD [THEN conjunct1])
1244      apply assumption
1245     apply (rule L)
1246    apply (fast intro: L [THEN subsetD])
1247   apply (erule greatest_Lower_below [OF b_inf_B])
1248   apply simp
1249  apply (rule L)
1250 apply (rule greatest_closed [OF b_inf_B])
1251 done
1252   then show "EX s. least L s (Upper L A)" ..
1253 next
1254   fix A
1255   assume L: "A \<subseteq> carrier L"
1256   show "EX i. greatest L i (Lower L A)"
1257   proof (cases "A = {}")
1258     case True then show ?thesis
1259       by (simp add: top_exists)
1260   next
1261     case False with L show ?thesis
1262       by (rule inf_exists)
1263   qed
1264 qed
1266 (* TODO: prove dual version *)
1269 subsection {* Examples *}
1271 subsubsection {* The Powerset of a Set is a Complete Lattice *}
1273 theorem powerset_is_complete_lattice:
1274   "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
1275   (is "complete_lattice ?L")
1276 proof (rule partial_order.complete_latticeI)
1277   show "partial_order ?L"
1278     proof qed auto
1279 next
1280   fix B
1281   assume B: "B \<subseteq> carrier ?L"
1282   show "EX s. least ?L s (Upper ?L B)"
1283   proof
1284     from B show "least ?L (\<Union> B) (Upper ?L B)"
1285       by (fastsimp intro!: least_UpperI simp: Upper_def)
1286   qed
1287 next
1288   fix B
1289   assume B: "B \<subseteq> carrier ?L"
1290   show "EX i. greatest ?L i (Lower ?L B)"
1291   proof
1292     from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
1293       txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
1294 	@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
1295       by (fastsimp intro!: greatest_LowerI simp: Lower_def)
1296   qed
1297 qed
1299 text {* An other example, that of the lattice of subgroups of a group,
1300   can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
1302 end