96 |
96 |
97 subsection \<open>Lattices\<close> |
97 subsection \<open>Lattices\<close> |
98 |
98 |
99 locale weak_upper_semilattice = weak_partial_order + |
99 locale weak_upper_semilattice = weak_partial_order + |
100 assumes sup_of_two_exists: |
100 assumes sup_of_two_exists: |
101 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
101 "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})" |
102 |
102 |
103 locale weak_lower_semilattice = weak_partial_order + |
103 locale weak_lower_semilattice = weak_partial_order + |
104 assumes inf_of_two_exists: |
104 assumes inf_of_two_exists: |
105 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
105 "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})" |
106 |
106 |
107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice |
107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice |
108 |
108 |
109 lemma (in weak_lattice) dual_weak_lattice: |
109 lemma (in weak_lattice) dual_weak_lattice: |
110 "weak_lattice (inv_gorder L)" |
110 "weak_lattice (inv_gorder L)" |
282 case False with P and xA show ?thesis |
282 case False with P and xA show ?thesis |
283 by (simp add: sup_insertI finite_sup_least) |
283 by (simp add: sup_insertI finite_sup_least) |
284 qed |
284 qed |
285 |
285 |
286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]: |
286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]: |
287 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" |
287 "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Squnion>A \<in> carrier L" |
288 proof (induct set: finite) |
288 proof (induct set: finite) |
289 case empty then show ?case by simp |
289 case empty then show ?case by simp |
290 next |
290 next |
291 case insert then show ?case |
291 case insert then show ?case |
292 by - (rule finite_sup_insertI, simp_all) |
292 by - (rule finite_sup_insertI, simp_all) |
526 case False with P and xA show ?thesis |
526 case False with P and xA show ?thesis |
527 by (simp add: inf_insertI finite_inf_greatest) |
527 by (simp add: inf_insertI finite_inf_greatest) |
528 qed |
528 qed |
529 |
529 |
530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]: |
530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]: |
531 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" |
531 "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Sqinter>A \<in> carrier L" |
532 proof (induct set: finite) |
532 proof (induct set: finite) |
533 case empty then show ?case by simp |
533 case empty then show ?case by simp |
534 next |
534 next |
535 case insert then show ?case |
535 case insert then show ?case |
536 by (rule_tac finite_inf_insertI) (simp_all) |
536 by (rule_tac finite_inf_insertI) (simp_all) |
685 |
685 |
686 subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close> |
686 subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close> |
687 |
687 |
688 locale upper_semilattice = partial_order + |
688 locale upper_semilattice = partial_order + |
689 assumes sup_of_two_exists: |
689 assumes sup_of_two_exists: |
690 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
690 "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})" |
691 |
691 |
692 sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice |
692 sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice |
693 by unfold_locales (rule sup_of_two_exists) |
693 by unfold_locales (rule sup_of_two_exists) |
694 |
694 |
695 locale lower_semilattice = partial_order + |
695 locale lower_semilattice = partial_order + |
696 assumes inf_of_two_exists: |
696 assumes inf_of_two_exists: |
697 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
697 "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})" |
698 |
698 |
699 sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice |
699 sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice |
700 by unfold_locales (rule inf_of_two_exists) |
700 by unfold_locales (rule inf_of_two_exists) |
701 |
701 |
702 locale lattice = upper_semilattice + lower_semilattice |
702 locale lattice = upper_semilattice + lower_semilattice |