27 |
27 |
28 text {* Note that the type constraints above are necessary, because the |
28 text {* Note that the type constraints above are necessary, because the |
29 definition command cannot specialise the types. *} |
29 definition command cannot specialise the types. *} |
30 |
30 |
31 definition (in order_syntax) |
31 definition (in order_syntax) |
32 less (infixl "\<sqsubset>" 50) "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" |
32 less (infixl "\<sqsubset>" 50) where "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" |
33 |
33 |
34 text {* Upper and lower bounds of a set. *} |
34 text {* Upper and lower bounds of a set. *} |
35 |
35 |
36 definition (in order_syntax) |
36 definition (in order_syntax) |
37 Upper where |
37 Upper where |
38 "Upper A == {u. (ALL x. x \<in> A \<inter> L --> x \<sqsubseteq> u)} \<inter> L" |
38 "Upper A == {u. (ALL x. x \<in> A \<inter> L --> x \<sqsubseteq> u)} \<inter> L" |
39 |
39 |
40 definition (in order_syntax) |
40 definition (in order_syntax) |
41 Lower :: "'a set => 'a set" |
41 Lower :: "'a set => 'a set" where |
42 "Lower A == {l. (ALL x. x \<in> A \<inter> L --> l \<sqsubseteq> x)} \<inter> L" |
42 "Lower A == {l. (ALL x. x \<in> A \<inter> L --> l \<sqsubseteq> x)} \<inter> L" |
43 |
43 |
44 text {* Least and greatest, as predicate. *} |
44 text {* Least and greatest, as predicate. *} |
45 |
45 |
46 definition (in order_syntax) |
46 definition (in order_syntax) |
47 least :: "['a, 'a set] => bool" |
47 least :: "['a, 'a set] => bool" where |
48 "least l A == A \<subseteq> L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" |
48 "least l A == A \<subseteq> L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" |
49 |
49 |
50 definition (in order_syntax) |
50 definition (in order_syntax) |
51 greatest :: "['a, 'a set] => bool" |
51 greatest :: "['a, 'a set] => bool" where |
52 "greatest g A == A \<subseteq> L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" |
52 "greatest g A == A \<subseteq> L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" |
53 |
53 |
54 text {* Supremum and infimum *} |
54 text {* Supremum and infimum *} |
55 |
55 |
56 definition (in order_syntax) |
56 definition (in order_syntax) |
57 sup :: "'a set => 'a" ("\<Squnion>_" [90] 90) |
57 sup :: "'a set => 'a" ("\<Squnion>_" [90] 90) where |
58 "\<Squnion>A == THE x. least x (Upper A)" |
58 "\<Squnion>A == THE x. least x (Upper A)" |
59 |
59 |
60 definition (in order_syntax) |
60 definition (in order_syntax) |
61 inf :: "'a set => 'a" ("\<Sqinter>_" [90] 90) |
61 inf :: "'a set => 'a" ("\<Sqinter>_" [90] 90) where |
62 "\<Sqinter>A == THE x. greatest x (Lower A)" |
62 "\<Sqinter>A == THE x. greatest x (Lower A)" |
63 |
63 |
64 definition (in order_syntax) |
64 definition (in order_syntax) |
65 join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65) |
65 join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65) where |
66 "x \<squnion> y == sup {x, y}" |
66 "x \<squnion> y == sup {x, y}" |
67 |
67 |
68 definition (in order_syntax) |
68 definition (in order_syntax) |
69 meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70) |
69 meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70) where |
70 "x \<sqinter> y == inf {x, y}" |
70 "x \<sqinter> y == inf {x, y}" |
71 |
71 |
72 locale partial_order = order_syntax + |
72 locale partial_order = order_syntax + |
73 assumes refl [intro, simp]: |
73 assumes refl [intro, simp]: |
74 "x \<in> L ==> x \<sqsubseteq> x" |
74 "x \<in> L ==> x \<sqsubseteq> x" |
77 and trans [trans]: |
77 and trans [trans]: |
78 "[| x \<sqsubseteq> y; y \<sqsubseteq> z; |
78 "[| x \<sqsubseteq> y; y \<sqsubseteq> z; |
79 x \<in> L; y \<in> L; z \<in> L |] ==> x \<sqsubseteq> z" |
79 x \<in> L; y \<in> L; z \<in> L |] ==> x \<sqsubseteq> z" |
80 |
80 |
81 abbreviation (in partial_order) |
81 abbreviation (in partial_order) |
82 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
82 less (infixl "\<sqsubset>" 50) where "less == order_syntax.less le" |
83 abbreviation (in partial_order) |
83 abbreviation (in partial_order) |
84 Upper where "Upper == order_syntax.Upper L le" |
84 Upper where "Upper == order_syntax.Upper L le" |
85 abbreviation (in partial_order) |
85 abbreviation (in partial_order) |
86 Lower where "Lower == order_syntax.Lower L le" |
86 Lower where "Lower == order_syntax.Lower L le" |
87 abbreviation (in partial_order) |
87 abbreviation (in partial_order) |
88 least where "least == order_syntax.least L le" |
88 least where "least == order_syntax.least L le" |
89 abbreviation (in partial_order) |
89 abbreviation (in partial_order) |
90 greatest where "greatest == order_syntax.greatest L le" |
90 greatest where "greatest == order_syntax.greatest L le" |
91 abbreviation (in partial_order) |
91 abbreviation (in partial_order) |
92 sup ("\<Squnion>_" [90] 90) "sup == order_syntax.sup L le" |
92 sup ("\<Squnion>_" [90] 90) where "sup == order_syntax.sup L le" |
93 abbreviation (in partial_order) |
93 abbreviation (in partial_order) |
94 inf ("\<Sqinter>_" [90] 90) "inf == order_syntax.inf L le" |
94 inf ("\<Sqinter>_" [90] 90) where "inf == order_syntax.inf L le" |
95 abbreviation (in partial_order) |
95 abbreviation (in partial_order) |
96 join (infixl "\<squnion>" 65) "join == order_syntax.join L le" |
96 join (infixl "\<squnion>" 65) where "join == order_syntax.join L le" |
97 abbreviation (in partial_order) |
97 abbreviation (in partial_order) |
98 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet L le" |
98 meet (infixl "\<sqinter>" 70) where "meet == order_syntax.meet L le" |
99 |
99 |
100 |
100 |
101 subsubsection {* Upper *} |
101 subsubsection {* Upper *} |
102 |
102 |
103 lemma (in order_syntax) Upper_closed [intro, simp]: |
103 lemma (in order_syntax) Upper_closed [intro, simp]: |
205 "[| x \<in> L; y \<in> L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le {x, y})" |
205 "[| x \<in> L; y \<in> L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le {x, y})" |
206 and inf_of_two_exists: |
206 and inf_of_two_exists: |
207 "[| x \<in> L; y \<in> L |] ==> EX s. order_syntax.greatest L le s (order_syntax.Lower L le {x, y})" |
207 "[| x \<in> L; y \<in> L |] ==> EX s. order_syntax.greatest L le s (order_syntax.Lower L le {x, y})" |
208 |
208 |
209 abbreviation (in lattice) |
209 abbreviation (in lattice) |
210 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
210 less (infixl "\<sqsubset>" 50) where "less == order_syntax.less le" |
211 abbreviation (in lattice) |
211 abbreviation (in lattice) |
212 Upper where "Upper == order_syntax.Upper L le" |
212 Upper where "Upper == order_syntax.Upper L le" |
213 abbreviation (in lattice) |
213 abbreviation (in lattice) |
214 Lower where "Lower == order_syntax.Lower L le" |
214 Lower where "Lower == order_syntax.Lower L le" |
215 abbreviation (in lattice) |
215 abbreviation (in lattice) |
216 least where "least == order_syntax.least L le" |
216 least where "least == order_syntax.least L le" |
217 abbreviation (in lattice) |
217 abbreviation (in lattice) |
218 greatest where "greatest == order_syntax.greatest L le" |
218 greatest where "greatest == order_syntax.greatest L le" |
219 abbreviation (in lattice) |
219 abbreviation (in lattice) |
220 sup ("\<Squnion>_" [90] 90) "sup == order_syntax.sup L le" |
220 sup ("\<Squnion>_" [90] 90) where "sup == order_syntax.sup L le" |
221 abbreviation (in lattice) |
221 abbreviation (in lattice) |
222 inf ("\<Sqinter>_" [90] 90) "inf == order_syntax.inf L le" |
222 inf ("\<Sqinter>_" [90] 90) where "inf == order_syntax.inf L le" |
223 abbreviation (in lattice) |
223 abbreviation (in lattice) |
224 join (infixl "\<squnion>" 65) "join == order_syntax.join L le" |
224 join (infixl "\<squnion>" 65) where "join == order_syntax.join L le" |
225 abbreviation (in lattice) |
225 abbreviation (in lattice) |
226 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet L le" |
226 meet (infixl "\<sqinter>" 70) where "meet == order_syntax.meet L le" |
227 |
227 |
228 lemma (in order_syntax) least_Upper_above: |
228 lemma (in order_syntax) least_Upper_above: |
229 "[| least s (Upper A); x \<in> A; A \<subseteq> L |] ==> x \<sqsubseteq> s" |
229 "[| least s (Upper A); x \<in> A; A \<subseteq> L |] ==> x \<sqsubseteq> s" |
230 by (unfold least_def) blast |
230 by (unfold least_def) blast |
231 |
231 |
688 |
688 |
689 locale total_order = lattice + |
689 locale total_order = lattice + |
690 assumes total: "[| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
690 assumes total: "[| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
691 |
691 |
692 abbreviation (in total_order) |
692 abbreviation (in total_order) |
693 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
693 less (infixl "\<sqsubset>" 50) where "less == order_syntax.less le" |
694 abbreviation (in total_order) |
694 abbreviation (in total_order) |
695 Upper where "Upper == order_syntax.Upper L le" |
695 Upper where "Upper == order_syntax.Upper L le" |
696 abbreviation (in total_order) |
696 abbreviation (in total_order) |
697 Lower where "Lower == order_syntax.Lower L le" |
697 Lower where "Lower == order_syntax.Lower L le" |
698 abbreviation (in total_order) |
698 abbreviation (in total_order) |
699 least where "least == order_syntax.least L le" |
699 least where "least == order_syntax.least L le" |
700 abbreviation (in total_order) |
700 abbreviation (in total_order) |
701 greatest where "greatest == order_syntax.greatest L le" |
701 greatest where "greatest == order_syntax.greatest L le" |
702 abbreviation (in total_order) |
702 abbreviation (in total_order) |
703 sup ("\<Squnion>_" [90] 90) "sup == order_syntax.sup L le" |
703 sup ("\<Squnion>_" [90] 90) where "sup == order_syntax.sup L le" |
704 abbreviation (in total_order) |
704 abbreviation (in total_order) |
705 inf ("\<Sqinter>_" [90] 90) "inf == order_syntax.inf L le" |
705 inf ("\<Sqinter>_" [90] 90) where "inf == order_syntax.inf L le" |
706 abbreviation (in total_order) |
706 abbreviation (in total_order) |
707 join (infixl "\<squnion>" 65) "join == order_syntax.join L le" |
707 join (infixl "\<squnion>" 65) where "join == order_syntax.join L le" |
708 abbreviation (in total_order) |
708 abbreviation (in total_order) |
709 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet L le" |
709 meet (infixl "\<sqinter>" 70) where "meet == order_syntax.meet L le" |
710 |
710 |
711 text {* Introduction rule: the usual definition of total order *} |
711 text {* Introduction rule: the usual definition of total order *} |
712 |
712 |
713 lemma (in partial_order) total_orderI: |
713 lemma (in partial_order) total_orderI: |
714 assumes total: "!!x y. [| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
714 assumes total: "!!x y. [| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
766 "[| A \<subseteq> L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le A)" |
766 "[| A \<subseteq> L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le A)" |
767 and inf_exists: |
767 and inf_exists: |
768 "[| A \<subseteq> L |] ==> EX i. order_syntax.greatest L le i (order_syntax.Lower L le A)" |
768 "[| A \<subseteq> L |] ==> EX i. order_syntax.greatest L le i (order_syntax.Lower L le A)" |
769 |
769 |
770 abbreviation (in complete_lattice) |
770 abbreviation (in complete_lattice) |
771 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
771 less (infixl "\<sqsubset>" 50) where "less == order_syntax.less le" |
772 abbreviation (in complete_lattice) |
772 abbreviation (in complete_lattice) |
773 Upper where "Upper == order_syntax.Upper L le" |
773 Upper where "Upper == order_syntax.Upper L le" |
774 abbreviation (in complete_lattice) |
774 abbreviation (in complete_lattice) |
775 Lower where "Lower == order_syntax.Lower L le" |
775 Lower where "Lower == order_syntax.Lower L le" |
776 abbreviation (in complete_lattice) |
776 abbreviation (in complete_lattice) |
777 least where "least == order_syntax.least L le" |
777 least where "least == order_syntax.least L le" |
778 abbreviation (in complete_lattice) |
778 abbreviation (in complete_lattice) |
779 greatest where "greatest == order_syntax.greatest L le" |
779 greatest where "greatest == order_syntax.greatest L le" |
780 abbreviation (in complete_lattice) |
780 abbreviation (in complete_lattice) |
781 sup ("\<Squnion>_" [90] 90) "sup == order_syntax.sup L le" |
781 sup ("\<Squnion>_" [90] 90) where "sup == order_syntax.sup L le" |
782 abbreviation (in complete_lattice) |
782 abbreviation (in complete_lattice) |
783 inf ("\<Sqinter>_" [90] 90) "inf == order_syntax.inf L le" |
783 inf ("\<Sqinter>_" [90] 90) where "inf == order_syntax.inf L le" |
784 abbreviation (in complete_lattice) |
784 abbreviation (in complete_lattice) |
785 join (infixl "\<squnion>" 65) "join == order_syntax.join L le" |
785 join (infixl "\<squnion>" 65) where "join == order_syntax.join L le" |
786 abbreviation (in complete_lattice) |
786 abbreviation (in complete_lattice) |
787 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet L le" |
787 meet (infixl "\<sqinter>" 70) where "meet == order_syntax.meet L le" |
788 |
788 |
789 text {* Introduction rule: the usual definition of complete lattice *} |
789 text {* Introduction rule: the usual definition of complete lattice *} |
790 |
790 |
791 lemma (in partial_order) complete_latticeI: |
791 lemma (in partial_order) complete_latticeI: |
792 assumes sup_exists: |
792 assumes sup_exists: |
798 show "lattice_axioms L le" |
798 show "lattice_axioms L le" |
799 by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
799 by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
800 qed (assumption | rule complete_lattice_axioms.intro)+ |
800 qed (assumption | rule complete_lattice_axioms.intro)+ |
801 |
801 |
802 definition (in order_syntax) |
802 definition (in order_syntax) |
803 top ("\<top>") |
803 top ("\<top>") where |
804 "\<top> == sup L" |
804 "\<top> == sup L" |
805 |
805 |
806 definition (in order_syntax) |
806 definition (in order_syntax) |
807 bottom ("\<bottom>") |
807 bottom ("\<bottom>") where |
808 "\<bottom> == inf L" |
808 "\<bottom> == inf L" |
809 |
809 |
810 abbreviation (in partial_order) |
810 abbreviation (in partial_order) |
811 top ("\<top>") "top == order_syntax.top L le" |
811 top ("\<top>") where "top == order_syntax.top L le" |
812 abbreviation (in partial_order) |
812 abbreviation (in partial_order) |
813 bottom ("\<bottom>") "bottom == order_syntax.bottom L le" |
813 bottom ("\<bottom>") where "bottom == order_syntax.bottom L le" |
814 abbreviation (in lattice) |
814 abbreviation (in lattice) |
815 top ("\<top>") "top == order_syntax.top L le" |
815 top ("\<top>") where "top == order_syntax.top L le" |
816 abbreviation (in lattice) |
816 abbreviation (in lattice) |
817 bottom ("\<bottom>") "bottom == order_syntax.bottom L le" |
817 bottom ("\<bottom>") where "bottom == order_syntax.bottom L le" |
818 abbreviation (in total_order) |
818 abbreviation (in total_order) |
819 top ("\<top>") "top == order_syntax.top L le" |
819 top ("\<top>") where "top == order_syntax.top L le" |
820 abbreviation (in total_order) |
820 abbreviation (in total_order) |
821 bottom ("\<bottom>") "bottom == order_syntax.bottom L le" |
821 bottom ("\<bottom>") where "bottom == order_syntax.bottom L le" |
822 abbreviation (in complete_lattice) |
822 abbreviation (in complete_lattice) |
823 top ("\<top>") "top == order_syntax.top L le" |
823 top ("\<top>") where "top == order_syntax.top L le" |
824 abbreviation (in complete_lattice) |
824 abbreviation (in complete_lattice) |
825 bottom ("\<bottom>") "bottom == order_syntax.bottom L le" |
825 bottom ("\<bottom>") where "bottom == order_syntax.bottom L le" |
826 |
826 |
827 |
827 |
828 lemma (in complete_lattice) supI: |
828 lemma (in complete_lattice) supI: |
829 "[| !!l. least l (Upper A) ==> P l; A \<subseteq> L |] |
829 "[| !!l. least l (Upper A) ==> P l; A \<subseteq> L |] |
830 ==> P (\<Squnion>A)" |
830 ==> P (\<Squnion>A)" |