src/HOL/Algebra/Lattice.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66580 e5b1d4d55bf6 child 67091 1393c2340eec permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Algebra/Lattice.thy
2     Author:     Clemens Ballarin, started 7 November 2003
3     Copyright:  Clemens Ballarin
5 Most congruence rules by Stephan Hohe.
6 With additional contributions from Alasdair Armstrong and Simon Foster.
7 *)
9 theory Lattice
10 imports Order
11 begin
13 section \<open>Lattices\<close>
15 subsection \<open>Supremum and infimum\<close>
17 definition
18   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_"  90)
19   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
21 definition
22   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_"  90)
23   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
25 definition supr ::
26   "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
27   where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)"
29 definition infi ::
30   "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
31   where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
33 syntax
34   "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10)
35   "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10)
36   "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
37   "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
39 translations
40   "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
41   "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
42   "SSUP\<^bsub>L\<^esub> x. B"     == "CONST supr L CONST UNIV (%x. B)"
43   "SSUP\<^bsub>L\<^esub> x:A. B"   == "CONST supr L A (%x. B)"
45 definition
46   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
47   where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
49 definition
50   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
51   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
53 definition
54   LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
55   "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
57 definition
58   GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
59   "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
62 subsection \<open>Dual operators\<close>
64 lemma sup_dual [simp]:
65   "\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A"
66   by (simp add: sup_def inf_def)
68 lemma inf_dual [simp]:
69   "\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A"
70   by (simp add: sup_def inf_def)
72 lemma join_dual [simp]:
73   "p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q"
74   by (simp add:join_def meet_def)
76 lemma meet_dual [simp]:
77   "p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q"
78   by (simp add:join_def meet_def)
80 lemma top_dual [simp]:
81   "\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>"
82   by (simp add: top_def bottom_def)
84 lemma bottom_dual [simp]:
85   "\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>"
86   by (simp add: top_def bottom_def)
88 lemma LFP_dual [simp]:
89   "LEAST_FP (inv_gorder L) f = GREATEST_FP L f"
90   by (simp add:LEAST_FP_def GREATEST_FP_def)
92 lemma GFP_dual [simp]:
93   "GREATEST_FP (inv_gorder L) f = LEAST_FP L f"
94   by (simp add:LEAST_FP_def GREATEST_FP_def)
97 subsection \<open>Lattices\<close>
99 locale weak_upper_semilattice = weak_partial_order +
100   assumes sup_of_two_exists:
101     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
103 locale weak_lower_semilattice = weak_partial_order +
104   assumes inf_of_two_exists:
105     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
109 lemma (in weak_lattice) dual_weak_lattice:
110   "weak_lattice (inv_gorder L)"
111 proof -
112   interpret dual: weak_partial_order "inv_gorder L"
113     by (metis dual_weak_order)
115   show ?thesis
116     apply (unfold_locales)
117     apply (simp_all add: inf_of_two_exists sup_of_two_exists)
118   done
119 qed
122 subsubsection \<open>Supremum\<close>
124 lemma (in weak_upper_semilattice) joinI:
125   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
126   ==> P (x \<squnion> y)"
127 proof (unfold join_def sup_def)
128   assume L: "x \<in> carrier L"  "y \<in> carrier L"
129     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
130   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
131   with L show "P (SOME l. least L l (Upper L {x, y}))"
132     by (fast intro: someI2 P)
133 qed
135 lemma (in weak_upper_semilattice) join_closed [simp]:
136   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
137   by (rule joinI) (rule least_closed)
139 lemma (in weak_upper_semilattice) join_cong_l:
140   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
141     and xx': "x .= x'"
142   shows "x \<squnion> y .= x' \<squnion> y"
143 proof (rule joinI, rule joinI)
144   fix a b
145   from xx' carr
146       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
148   assume leasta: "least L a (Upper L {x, y})"
149   assume "least L b (Upper L {x', y})"
150   with carr
151       have leastb: "least L b (Upper L {x, y})"
152       by (simp add: least_Upper_cong_r[OF _ _ seq])
154   from leasta leastb
155       show "a .= b" by (rule weak_least_unique)
156 qed (rule carr)+
158 lemma (in weak_upper_semilattice) join_cong_r:
159   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
160     and yy': "y .= y'"
161   shows "x \<squnion> y .= x \<squnion> y'"
162 proof (rule joinI, rule joinI)
163   fix a b
164   have "{x, y} = {y, x}" by fast
165   also from carr yy'
166       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
167   also have "{y', x} = {x, y'}" by fast
168   finally
169       have seq: "{x, y} {.=} {x, y'}" .
171   assume leasta: "least L a (Upper L {x, y})"
172   assume "least L b (Upper L {x, y'})"
173   with carr
174       have leastb: "least L b (Upper L {x, y})"
175       by (simp add: least_Upper_cong_r[OF _ _ seq])
177   from leasta leastb
178       show "a .= b" by (rule weak_least_unique)
179 qed (rule carr)+
181 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
182   "x \<in> carrier L ==> least L x (Upper L {x})"
183   by (rule least_UpperI) auto
185 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
186   "x \<in> carrier L ==> \<Squnion>{x} .= x"
187   unfolding sup_def
188   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
190 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
191   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
192   unfolding sup_def
193   by (rule someI2) (auto intro: sup_of_singletonI)
195 text \<open>Condition on \<open>A\<close>: supremum exists.\<close>
197 lemma (in weak_upper_semilattice) sup_insertI:
198   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
199   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
200   ==> P (\<Squnion>(insert x A))"
201 proof (unfold sup_def)
202   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
203     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
204     and least_a: "least L a (Upper L A)"
205   from L least_a have La: "a \<in> carrier L" by simp
206   from L sup_of_two_exists least_a
207   obtain s where least_s: "least L s (Upper L {a, x})" by blast
208   show "P (SOME l. least L l (Upper L (insert x A)))"
209   proof (rule someI2)
210     show "least L s (Upper L (insert x A))"
211     proof (rule least_UpperI)
212       fix z
213       assume "z \<in> insert x A"
214       then show "z \<sqsubseteq> s"
215       proof
216         assume "z = x" then show ?thesis
217           by (simp add: least_Upper_above [OF least_s] L La)
218       next
219         assume "z \<in> A"
220         with L least_s least_a show ?thesis
221           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
222       qed
223     next
224       fix y
225       assume y: "y \<in> Upper L (insert x A)"
226       show "s \<sqsubseteq> y"
227       proof (rule least_le [OF least_s], rule Upper_memI)
228         fix z
229         assume z: "z \<in> {a, x}"
230         then show "z \<sqsubseteq> y"
231         proof
232           have y': "y \<in> Upper L A"
233             apply (rule subsetD [where A = "Upper L (insert x A)"])
234              apply (rule Upper_antimono)
235              apply blast
236             apply (rule y)
237             done
238           assume "z = a"
239           with y' least_a show ?thesis by (fast dest: least_le)
240         next
241           assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
242           with y L show ?thesis by blast
243         qed
244       qed (rule Upper_closed [THEN subsetD, OF y])
245     next
246       from L show "insert x A \<subseteq> carrier L" by simp
247       from least_s show "s \<in> carrier L" by simp
248     qed
249   qed (rule P)
250 qed
252 lemma (in weak_upper_semilattice) finite_sup_least:
253   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
254 proof (induct set: finite)
255   case empty
256   then show ?case by simp
257 next
258   case (insert x A)
259   show ?case
260   proof (cases "A = {}")
261     case True
262     with insert show ?thesis
263       by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
264         (* The above step is hairy; least_cong can make simp loop.
265         Would want special version of simp to apply least_cong. *)
266   next
267     case False
268     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
269     with _ show ?thesis
270       by (rule sup_insertI) (simp_all add: insert [simplified])
271   qed
272 qed
274 lemma (in weak_upper_semilattice) finite_sup_insertI:
275   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
276     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
277   shows "P (\<Squnion> (insert x A))"
278 proof (cases "A = {}")
279   case True with P and xA show ?thesis
280     by (simp add: finite_sup_least)
281 next
282   case False with P and xA show ?thesis
283     by (simp add: sup_insertI finite_sup_least)
284 qed
286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
287   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
288 proof (induct set: finite)
289   case empty then show ?case by simp
290 next
291   case insert then show ?case
292     by - (rule finite_sup_insertI, simp_all)
293 qed
295 lemma (in weak_upper_semilattice) join_left:
296   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
297   by (rule joinI [folded join_def]) (blast dest: least_mem)
299 lemma (in weak_upper_semilattice) join_right:
300   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
301   by (rule joinI [folded join_def]) (blast dest: least_mem)
303 lemma (in weak_upper_semilattice) sup_of_two_least:
304   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
305 proof (unfold sup_def)
306   assume L: "x \<in> carrier L"  "y \<in> carrier L"
307   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
308   with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
309   by (fast intro: someI2 weak_least_unique)  (* blast fails *)
310 qed
312 lemma (in weak_upper_semilattice) join_le:
313   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
314     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
315   shows "x \<squnion> y \<sqsubseteq> z"
316 proof (rule joinI [OF _ x y])
317   fix s
318   assume "least L s (Upper L {x, y})"
319   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
320 qed
322 lemma (in weak_lattice) weak_le_iff_meet:
323   assumes "x \<in> carrier L" "y \<in> carrier L"
324   shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y"
325   by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)
327 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
328   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
329   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
330 proof (rule finite_sup_insertI)
331   \<comment> \<open>The textbook argument in Jacobson I, p 457\<close>
332   fix s
333   assume sup: "least L s (Upper L {x, y, z})"
334   show "x \<squnion> (y \<squnion> z) .= s"
335   proof (rule weak_le_antisym)
336     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
337       by (fastforce intro!: join_le elim: least_Upper_above)
338   next
339     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
340     by (erule_tac least_le)
341       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
342   qed (simp_all add: L least_closed [OF sup])
343 qed (simp_all add: L)
345 text \<open>Commutativity holds for \<open>=\<close>.\<close>
347 lemma join_comm:
348   fixes L (structure)
349   shows "x \<squnion> y = y \<squnion> x"
350   by (unfold join_def) (simp add: insert_commute)
352 lemma (in weak_upper_semilattice) weak_join_assoc:
353   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
354   shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
355 proof -
356   (* FIXME: could be simplified by improved simp: uniform use of .=,
357      omit [symmetric] in last step. *)
358   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
359   also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
360   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
361   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
362   finally show ?thesis by (simp add: L)
363 qed
366 subsubsection \<open>Infimum\<close>
368 lemma (in weak_lower_semilattice) meetI:
369   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
370   x \<in> carrier L; y \<in> carrier L |]
371   ==> P (x \<sqinter> y)"
372 proof (unfold meet_def inf_def)
373   assume L: "x \<in> carrier L"  "y \<in> carrier L"
374     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
375   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
376   with L show "P (SOME g. greatest L g (Lower L {x, y}))"
377   by (fast intro: someI2 weak_greatest_unique P)
378 qed
380 lemma (in weak_lower_semilattice) meet_closed [simp]:
381   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
382   by (rule meetI) (rule greatest_closed)
384 lemma (in weak_lower_semilattice) meet_cong_l:
385   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
386     and xx': "x .= x'"
387   shows "x \<sqinter> y .= x' \<sqinter> y"
388 proof (rule meetI, rule meetI)
389   fix a b
390   from xx' carr
391       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
393   assume greatesta: "greatest L a (Lower L {x, y})"
394   assume "greatest L b (Lower L {x', y})"
395   with carr
396       have greatestb: "greatest L b (Lower L {x, y})"
397       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
399   from greatesta greatestb
400       show "a .= b" by (rule weak_greatest_unique)
401 qed (rule carr)+
403 lemma (in weak_lower_semilattice) meet_cong_r:
404   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
405     and yy': "y .= y'"
406   shows "x \<sqinter> y .= x \<sqinter> y'"
407 proof (rule meetI, rule meetI)
408   fix a b
409   have "{x, y} = {y, x}" by fast
410   also from carr yy'
411       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
412   also have "{y', x} = {x, y'}" by fast
413   finally
414       have seq: "{x, y} {.=} {x, y'}" .
416   assume greatesta: "greatest L a (Lower L {x, y})"
417   assume "greatest L b (Lower L {x, y'})"
418   with carr
419       have greatestb: "greatest L b (Lower L {x, y})"
420       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
422   from greatesta greatestb
423       show "a .= b" by (rule weak_greatest_unique)
424 qed (rule carr)+
426 lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
427   "x \<in> carrier L ==> greatest L x (Lower L {x})"
428   by (rule greatest_LowerI) auto
430 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
431   "x \<in> carrier L ==> \<Sqinter>{x} .= x"
432   unfolding inf_def
433   by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
435 lemma (in weak_partial_order) inf_of_singleton_closed:
436   "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
437   unfolding inf_def
438   by (rule someI2) (auto intro: inf_of_singletonI)
440 text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
442 lemma (in weak_lower_semilattice) inf_insertI:
443   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
444   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
445   ==> P (\<Sqinter>(insert x A))"
446 proof (unfold inf_def)
447   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
448     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
449     and greatest_a: "greatest L a (Lower L A)"
450   from L greatest_a have La: "a \<in> carrier L" by simp
451   from L inf_of_two_exists greatest_a
452   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
453   show "P (SOME g. greatest L g (Lower L (insert x A)))"
454   proof (rule someI2)
455     show "greatest L i (Lower L (insert x A))"
456     proof (rule greatest_LowerI)
457       fix z
458       assume "z \<in> insert x A"
459       then show "i \<sqsubseteq> z"
460       proof
461         assume "z = x" then show ?thesis
462           by (simp add: greatest_Lower_below [OF greatest_i] L La)
463       next
464         assume "z \<in> A"
465         with L greatest_i greatest_a show ?thesis
466           by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
467       qed
468     next
469       fix y
470       assume y: "y \<in> Lower L (insert x A)"
471       show "y \<sqsubseteq> i"
472       proof (rule greatest_le [OF greatest_i], rule Lower_memI)
473         fix z
474         assume z: "z \<in> {a, x}"
475         then show "y \<sqsubseteq> z"
476         proof
477           have y': "y \<in> Lower L A"
478             apply (rule subsetD [where A = "Lower L (insert x A)"])
479             apply (rule Lower_antimono)
480              apply blast
481             apply (rule y)
482             done
483           assume "z = a"
484           with y' greatest_a show ?thesis by (fast dest: greatest_le)
485         next
486           assume "z \<in> {x}"
487           with y L show ?thesis by blast
488         qed
489       qed (rule Lower_closed [THEN subsetD, OF y])
490     next
491       from L show "insert x A \<subseteq> carrier L" by simp
492       from greatest_i show "i \<in> carrier L" by simp
493     qed
494   qed (rule P)
495 qed
497 lemma (in weak_lower_semilattice) finite_inf_greatest:
498   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
499 proof (induct set: finite)
500   case empty then show ?case by simp
501 next
502   case (insert x A)
503   show ?case
504   proof (cases "A = {}")
505     case True
506     with insert show ?thesis
507       by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
508         inf_of_singleton_closed inf_of_singletonI)
509   next
510     case False
511     from insert show ?thesis
512     proof (rule_tac inf_insertI)
513       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
514     qed simp_all
515   qed
516 qed
518 lemma (in weak_lower_semilattice) finite_inf_insertI:
519   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
520     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
521   shows "P (\<Sqinter> (insert x A))"
522 proof (cases "A = {}")
523   case True with P and xA show ?thesis
524     by (simp add: finite_inf_greatest)
525 next
526   case False with P and xA show ?thesis
527     by (simp add: inf_insertI finite_inf_greatest)
528 qed
530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
531   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
532 proof (induct set: finite)
533   case empty then show ?case by simp
534 next
535   case insert then show ?case
536     by (rule_tac finite_inf_insertI) (simp_all)
537 qed
539 lemma (in weak_lower_semilattice) meet_left:
540   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
541   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
543 lemma (in weak_lower_semilattice) meet_right:
544   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
545   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
547 lemma (in weak_lower_semilattice) inf_of_two_greatest:
548   "[| x \<in> carrier L; y \<in> carrier L |] ==>
549   greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
550 proof (unfold inf_def)
551   assume L: "x \<in> carrier L"  "y \<in> carrier L"
552   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
553   with L
554   show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
555   by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
556 qed
558 lemma (in weak_lower_semilattice) meet_le:
559   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
560     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
561   shows "z \<sqsubseteq> x \<sqinter> y"
562 proof (rule meetI [OF _ x y])
563   fix i
564   assume "greatest L i (Lower L {x, y})"
565   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
566 qed
568 lemma (in weak_lattice) weak_le_iff_join:
569   assumes "x \<in> carrier L" "y \<in> carrier L"
570   shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)"
571   by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl)
573 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
574   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
575   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
576 proof (rule finite_inf_insertI)
577   txt \<open>The textbook argument in Jacobson I, p 457\<close>
578   fix i
579   assume inf: "greatest L i (Lower L {x, y, z})"
580   show "x \<sqinter> (y \<sqinter> z) .= i"
581   proof (rule weak_le_antisym)
582     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
583       by (fastforce intro!: meet_le elim: greatest_Lower_below)
584   next
585     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
586     by (erule_tac greatest_le)
587       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
588   qed (simp_all add: L greatest_closed [OF inf])
589 qed (simp_all add: L)
591 lemma meet_comm:
592   fixes L (structure)
593   shows "x \<sqinter> y = y \<sqinter> x"
594   by (unfold meet_def) (simp add: insert_commute)
596 lemma (in weak_lower_semilattice) weak_meet_assoc:
597   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
598   shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
599 proof -
600   (* FIXME: improved simp, see weak_join_assoc above *)
601   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
602   also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
603   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
604   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
605   finally show ?thesis by (simp add: L)
606 qed
608 text \<open>Total orders are lattices.\<close>
610 sublocale weak_total_order \<subseteq> weak?: weak_lattice
611 proof
612   fix x y
613   assume L: "x \<in> carrier L"  "y \<in> carrier L"
614   show "EX s. least L s (Upper L {x, y})"
615   proof -
616     note total L
617     moreover
618     {
619       assume "x \<sqsubseteq> y"
620       with L have "least L y (Upper L {x, y})"
621         by (rule_tac least_UpperI) auto
622     }
623     moreover
624     {
625       assume "y \<sqsubseteq> x"
626       with L have "least L x (Upper L {x, y})"
627         by (rule_tac least_UpperI) auto
628     }
629     ultimately show ?thesis by blast
630   qed
631 next
632   fix x y
633   assume L: "x \<in> carrier L"  "y \<in> carrier L"
634   show "EX i. greatest L i (Lower L {x, y})"
635   proof -
636     note total L
637     moreover
638     {
639       assume "y \<sqsubseteq> x"
640       with L have "greatest L y (Lower L {x, y})"
641         by (rule_tac greatest_LowerI) auto
642     }
643     moreover
644     {
645       assume "x \<sqsubseteq> y"
646       with L have "greatest L x (Lower L {x, y})"
647         by (rule_tac greatest_LowerI) auto
648     }
649     ultimately show ?thesis by blast
650   qed
651 qed
654 subsection \<open>Weak Bounded Lattices\<close>
656 locale weak_bounded_lattice =
657   weak_lattice +
658   weak_partial_order_bottom +
659   weak_partial_order_top
660 begin
662 lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>"
663   by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)
665 lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x"
666   by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)
668 lemma bottom_weak_eq:
669   "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>"
670   by (metis bottom_closed bottom_lower weak_le_antisym)
672 lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>"
673   by (metis join_closed join_left top_closed top_higher weak_le_antisym)
675 lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x"
676   by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)
678 lemma top_weak_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>"
679   by (metis top_closed top_higher weak_le_antisym)
681 end
683 sublocale weak_bounded_lattice \<subseteq> weak_partial_order ..
686 subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close>
688 locale upper_semilattice = partial_order +
689   assumes sup_of_two_exists:
690     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
692 sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice
693   by unfold_locales (rule sup_of_two_exists)
695 locale lower_semilattice = partial_order +
696   assumes inf_of_two_exists:
697     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
699 sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice
700   by unfold_locales (rule inf_of_two_exists)
702 locale lattice = upper_semilattice + lower_semilattice
704 sublocale lattice \<subseteq> weak_lattice ..
706 lemma (in lattice) dual_lattice:
707   "lattice (inv_gorder L)"
708 proof -
709   interpret dual: weak_lattice "inv_gorder L"
710     by (metis dual_weak_lattice)
712   show ?thesis
713     apply (unfold_locales)
714     apply (simp_all add: inf_of_two_exists sup_of_two_exists)
715     apply (simp add:eq_is_equal)
716   done
717 qed
719 lemma (in lattice) le_iff_join:
720   assumes "x \<in> carrier L" "y \<in> carrier L"
721   shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)"
722   by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)
724 lemma (in lattice) le_iff_meet:
725   assumes "x \<in> carrier L" "y \<in> carrier L"
726   shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y"
727   by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)
729 text \<open> Total orders are lattices. \<close>
731 sublocale total_order \<subseteq> weak?: lattice
732   by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)
734 text \<open>Functions that preserve joins and meets\<close>
736 definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
737 "join_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<squnion>\<^bsub>X\<^esub> y) = f x \<squnion>\<^bsub>Y\<^esub> f y)"
739 definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
740 "meet_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<sqinter>\<^bsub>X\<^esub> y) = f x \<sqinter>\<^bsub>Y\<^esub> f y)"
742 lemma join_pres_isotone:
743   assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f"
744   shows "isotone X Y f"
745   using assms
746   apply (rule_tac isotoneI)
747   apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)
748   using lattice_def partial_order_def upper_semilattice_def apply blast
749   using lattice_def partial_order_def upper_semilattice_def apply blast
750   apply fastforce
751 done
753 lemma meet_pres_isotone:
754   assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f"
755   shows "isotone X Y f"
756   using assms
757   apply (rule_tac isotoneI)
758   apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)
759   using lattice_def partial_order_def upper_semilattice_def apply blast
760   using lattice_def partial_order_def upper_semilattice_def apply blast
761   apply fastforce
762 done
765 subsection \<open>Bounded Lattices\<close>
767 locale bounded_lattice =
768   lattice +
769   weak_partial_order_bottom +
770   weak_partial_order_top
772 sublocale bounded_lattice \<subseteq> weak_bounded_lattice ..
774 context bounded_lattice
775 begin
777 lemma bottom_eq:
778   "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>"
779   by (metis bottom_closed bottom_lower le_antisym)
781 lemma top_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>"
782   by (metis le_antisym top_closed top_higher)
784 end
786 end