16 carrier :: "'a set" |
16 carrier :: "'a set" |
17 |
17 |
18 |
18 |
19 subsection {* Partial Orders *} |
19 subsection {* Partial Orders *} |
20 |
20 |
|
21 (* |
21 record 'a order = "'a partial_object" + |
22 record 'a order = "'a partial_object" + |
22 le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) |
23 le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) |
23 |
24 *) |
24 locale partial_order = |
25 |
25 fixes L (structure) |
26 text {* Locale @{text order_syntax} is required since we want to refer |
|
27 to definitions (and their derived theorems) outside of @{text partial_order}. |
|
28 *} |
|
29 |
|
30 locale order_syntax = |
|
31 fixes carrier :: "'a set" and le :: "['a, 'a] => bool" (infix "\<sqsubseteq>" 50) |
|
32 |
|
33 text {* Note that the type constraints above are necessary, because the |
|
34 definition command cannot specialise the types. *} |
|
35 |
|
36 definition (in order_syntax) |
|
37 less (infixl "\<sqsubset>" 50) "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" |
|
38 |
|
39 text {* Upper and lower bounds of a set. *} |
|
40 |
|
41 definition (in order_syntax) |
|
42 Upper where |
|
43 "Upper A == {u. (ALL x. x \<in> A \<inter> carrier --> x \<sqsubseteq> u)} \<inter> |
|
44 carrier" |
|
45 |
|
46 definition (in order_syntax) |
|
47 Lower :: "'a set => 'a set" |
|
48 "Lower A == {l. (ALL x. x \<in> A \<inter> carrier --> l \<sqsubseteq> x)} \<inter> |
|
49 carrier" |
|
50 |
|
51 text {* Least and greatest, as predicate. *} |
|
52 |
|
53 definition (in order_syntax) |
|
54 least :: "['a, 'a set] => bool" |
|
55 "least l A == A \<subseteq> carrier & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" |
|
56 |
|
57 definition (in order_syntax) |
|
58 greatest :: "['a, 'a set] => bool" |
|
59 "greatest g A == A \<subseteq> carrier & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" |
|
60 |
|
61 text {* Supremum and infimum *} |
|
62 |
|
63 definition (in order_syntax) |
|
64 sup :: "'a set => 'a" ("\<Squnion>") (* FIXME precedence [90] 90 *) |
|
65 "\<Squnion>A == THE x. least x (Upper A)" |
|
66 |
|
67 definition (in order_syntax) |
|
68 inf :: "'a set => 'a" ("\<Sqinter>") (* FIXME precedence *) |
|
69 "\<Sqinter>A == THE x. greatest x (Lower A)" |
|
70 |
|
71 definition (in order_syntax) |
|
72 join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65) |
|
73 "x \<squnion> y == sup {x, y}" |
|
74 |
|
75 definition (in order_syntax) |
|
76 meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70) |
|
77 "x \<sqinter> y == inf {x, y}" |
|
78 |
|
79 locale partial_order = order_syntax + |
26 assumes refl [intro, simp]: |
80 assumes refl [intro, simp]: |
27 "x \<in> carrier L ==> x \<sqsubseteq> x" |
81 "x \<in> carrier ==> x \<sqsubseteq> x" |
28 and anti_sym [intro]: |
82 and anti_sym [intro]: |
29 "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y" |
83 "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier; y \<in> carrier |] ==> x = y" |
30 and trans [trans]: |
84 and trans [trans]: |
31 "[| x \<sqsubseteq> y; y \<sqsubseteq> z; |
85 "[| x \<sqsubseteq> y; y \<sqsubseteq> z; |
32 x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" |
86 x \<in> carrier; y \<in> carrier; z \<in> carrier |] ==> x \<sqsubseteq> z" |
33 |
87 |
34 constdefs (structure L) |
88 abbreviation (in partial_order) |
35 lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) |
89 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
36 "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" |
90 abbreviation (in partial_order) |
37 |
91 Upper where "Upper == order_syntax.Upper carrier le" |
38 -- {* Upper and lower bounds of a set. *} |
92 abbreviation (in partial_order) |
39 Upper :: "[_, 'a set] => 'a set" |
93 Lower where "Lower == order_syntax.Lower carrier le" |
40 "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> |
94 abbreviation (in partial_order) |
41 carrier L" |
95 least where "least == order_syntax.least carrier le" |
42 |
96 abbreviation (in partial_order) |
43 Lower :: "[_, 'a set] => 'a set" |
97 greatest where "greatest == order_syntax.greatest carrier le" |
44 "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> |
98 abbreviation (in partial_order) |
45 carrier L" |
99 sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le" |
46 |
100 abbreviation (in partial_order) |
47 -- {* Least and greatest, as predicate. *} |
101 inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le" |
48 least :: "[_, 'a, 'a set] => bool" |
102 abbreviation (in partial_order) |
49 "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" |
103 join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le" |
50 |
104 abbreviation (in partial_order) |
51 greatest :: "[_, 'a, 'a set] => bool" |
105 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le" |
52 "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" |
|
53 |
|
54 -- {* Supremum and infimum *} |
|
55 sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) |
|
56 "\<Squnion>A == THE x. least L x (Upper L A)" |
|
57 |
|
58 inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) |
|
59 "\<Sqinter>A == THE x. greatest L x (Lower L A)" |
|
60 |
|
61 join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) |
|
62 "x \<squnion> y == sup L {x, y}" |
|
63 |
|
64 meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) |
|
65 "x \<sqinter> y == inf L {x, y}" |
|
66 |
106 |
67 |
107 |
68 subsubsection {* Upper *} |
108 subsubsection {* Upper *} |
69 |
109 |
70 lemma Upper_closed [intro, simp]: |
110 lemma (in order_syntax) Upper_closed [intro, simp]: |
71 "Upper L A \<subseteq> carrier L" |
111 "Upper A \<subseteq> carrier" |
72 by (unfold Upper_def) clarify |
112 by (unfold Upper_def) clarify |
73 |
113 |
74 lemma UpperD [dest]: |
114 lemma (in order_syntax) UpperD [dest]: |
75 fixes L (structure) |
115 fixes L (structure) |
76 shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" |
116 shows "[| u \<in> Upper A; x \<in> A; A \<subseteq> carrier |] ==> x \<sqsubseteq> u" |
77 by (unfold Upper_def) blast |
117 by (unfold Upper_def) blast |
78 |
118 |
79 lemma Upper_memI: |
119 lemma (in order_syntax) Upper_memI: |
80 fixes L (structure) |
120 fixes L (structure) |
81 shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A" |
121 shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier |] ==> x \<in> Upper A" |
82 by (unfold Upper_def) blast |
122 by (unfold Upper_def) blast |
83 |
123 |
84 lemma Upper_antimono: |
124 lemma (in order_syntax) Upper_antimono: |
85 "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" |
125 "A \<subseteq> B ==> Upper B \<subseteq> Upper A" |
86 by (unfold Upper_def) blast |
126 by (unfold Upper_def) blast |
87 |
127 |
88 |
128 |
89 subsubsection {* Lower *} |
129 subsubsection {* Lower *} |
90 |
130 |
91 lemma Lower_closed [intro, simp]: |
131 lemma (in order_syntax) Lower_closed [intro, simp]: |
92 "Lower L A \<subseteq> carrier L" |
132 "Lower A \<subseteq> carrier" |
93 by (unfold Lower_def) clarify |
133 by (unfold Lower_def) clarify |
94 |
134 |
95 lemma LowerD [dest]: |
135 lemma (in order_syntax) LowerD [dest]: |
96 fixes L (structure) |
136 "[| l \<in> Lower A; x \<in> A; A \<subseteq> carrier |] ==> l \<sqsubseteq> x" |
97 shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x" |
|
98 by (unfold Lower_def) blast |
137 by (unfold Lower_def) blast |
99 |
138 |
100 lemma Lower_memI: |
139 lemma (in order_syntax) Lower_memI: |
101 fixes L (structure) |
140 "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier |] ==> x \<in> Lower A" |
102 shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A" |
|
103 by (unfold Lower_def) blast |
141 by (unfold Lower_def) blast |
104 |
142 |
105 lemma Lower_antimono: |
143 lemma (in order_syntax) Lower_antimono: |
106 "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" |
144 "A \<subseteq> B ==> Lower B \<subseteq> Lower A" |
107 by (unfold Lower_def) blast |
145 by (unfold Lower_def) blast |
108 |
146 |
109 |
147 |
110 subsubsection {* least *} |
148 subsubsection {* least *} |
111 |
149 |
112 lemma least_carrier [intro, simp]: |
150 lemma (in order_syntax) least_carrier [intro, simp]: |
113 shows "least L l A ==> l \<in> carrier L" |
151 "least l A ==> l \<in> carrier" |
114 by (unfold least_def) fast |
152 by (unfold least_def) fast |
115 |
153 |
116 lemma least_mem: |
154 lemma (in order_syntax) least_mem: |
117 "least L l A ==> l \<in> A" |
155 "least l A ==> l \<in> A" |
118 by (unfold least_def) fast |
156 by (unfold least_def) fast |
119 |
157 |
120 lemma (in partial_order) least_unique: |
158 lemma (in partial_order) least_unique: |
121 "[| least L x A; least L y A |] ==> x = y" |
159 "[| least x A; least y A |] ==> x = y" |
122 by (unfold least_def) blast |
160 by (unfold least_def) blast |
123 |
161 |
124 lemma least_le: |
162 lemma (in order_syntax) least_le: |
125 fixes L (structure) |
163 "[| least x A; a \<in> A |] ==> x \<sqsubseteq> a" |
126 shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a" |
|
127 by (unfold least_def) fast |
164 by (unfold least_def) fast |
128 |
165 |
129 lemma least_UpperI: |
166 lemma (in order_syntax) least_UpperI: |
130 fixes L (structure) |
|
131 assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" |
167 assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" |
132 and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" |
168 and below: "!! y. y \<in> Upper A ==> s \<sqsubseteq> y" |
133 and L: "A \<subseteq> carrier L" "s \<in> carrier L" |
169 and L: "A \<subseteq> carrier" "s \<in> carrier" |
134 shows "least L s (Upper L A)" |
170 shows "least s (Upper A)" |
135 proof - |
171 proof - |
136 have "Upper L A \<subseteq> carrier L" by simp |
172 have "Upper A \<subseteq> carrier" by simp |
137 moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def) |
173 moreover from above L have "s \<in> Upper A" by (simp add: Upper_def) |
138 moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast |
174 moreover from below have "ALL x : Upper A. s \<sqsubseteq> x" by fast |
139 ultimately show ?thesis by (simp add: least_def) |
175 ultimately show ?thesis by (simp add: least_def) |
140 qed |
176 qed |
141 |
177 |
142 |
178 |
143 subsubsection {* greatest *} |
179 subsubsection {* greatest *} |
144 |
180 |
145 lemma greatest_carrier [intro, simp]: |
181 lemma (in order_syntax) greatest_carrier [intro, simp]: |
146 shows "greatest L l A ==> l \<in> carrier L" |
182 "greatest l A ==> l \<in> carrier" |
147 by (unfold greatest_def) fast |
183 by (unfold greatest_def) fast |
148 |
184 |
149 lemma greatest_mem: |
185 lemma (in order_syntax) greatest_mem: |
150 "greatest L l A ==> l \<in> A" |
186 "greatest l A ==> l \<in> A" |
151 by (unfold greatest_def) fast |
187 by (unfold greatest_def) fast |
152 |
188 |
153 lemma (in partial_order) greatest_unique: |
189 lemma (in partial_order) greatest_unique: |
154 "[| greatest L x A; greatest L y A |] ==> x = y" |
190 "[| greatest x A; greatest y A |] ==> x = y" |
155 by (unfold greatest_def) blast |
191 by (unfold greatest_def) blast |
156 |
192 |
157 lemma greatest_le: |
193 lemma (in order_syntax) greatest_le: |
158 fixes L (structure) |
194 "[| greatest x A; a \<in> A |] ==> a \<sqsubseteq> x" |
159 shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" |
|
160 by (unfold greatest_def) fast |
195 by (unfold greatest_def) fast |
161 |
196 |
162 lemma greatest_LowerI: |
197 lemma (in order_syntax) greatest_LowerI: |
163 fixes L (structure) |
|
164 assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" |
198 assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" |
165 and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" |
199 and above: "!! y. y \<in> Lower A ==> y \<sqsubseteq> i" |
166 and L: "A \<subseteq> carrier L" "i \<in> carrier L" |
200 and L: "A \<subseteq> carrier" "i \<in> carrier" |
167 shows "greatest L i (Lower L A)" |
201 shows "greatest i (Lower A)" |
168 proof - |
202 proof - |
169 have "Lower L A \<subseteq> carrier L" by simp |
203 have "Lower A \<subseteq> carrier" by simp |
170 moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) |
204 moreover from below L have "i \<in> Lower A" by (simp add: Lower_def) |
171 moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast |
205 moreover from above have "ALL x : Lower A. x \<sqsubseteq> i" by fast |
172 ultimately show ?thesis by (simp add: greatest_def) |
206 ultimately show ?thesis by (simp add: greatest_def) |
173 qed |
207 qed |
174 |
208 |
175 |
209 |
176 subsection {* Lattices *} |
210 subsection {* Lattices *} |
177 |
211 |
178 locale lattice = partial_order + |
212 locale lattice = partial_order + |
179 assumes sup_of_two_exists: |
213 assumes sup_of_two_exists: |
180 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
214 "[| x \<in> carrier; y \<in> carrier |] ==> EX s. order_syntax.least carrier le s (order_syntax.Upper carrier le {x, y})" |
181 and inf_of_two_exists: |
215 and inf_of_two_exists: |
182 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
216 "[| x \<in> carrier; y \<in> carrier |] ==> EX s. order_syntax.greatest carrier le s (order_syntax.Lower carrier le {x, y})" |
183 |
217 |
184 lemma least_Upper_above: |
218 abbreviation (in lattice) |
185 fixes L (structure) |
219 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
186 shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" |
220 abbreviation (in lattice) |
|
221 Upper where "Upper == order_syntax.Upper carrier le" |
|
222 abbreviation (in lattice) |
|
223 Lower where "Lower == order_syntax.Lower carrier le" |
|
224 abbreviation (in lattice) |
|
225 least where "least == order_syntax.least carrier le" |
|
226 abbreviation (in lattice) |
|
227 greatest where "greatest == order_syntax.greatest carrier le" |
|
228 abbreviation (in lattice) |
|
229 sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le" |
|
230 abbreviation (in lattice) |
|
231 inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le" |
|
232 abbreviation (in lattice) |
|
233 join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le" |
|
234 abbreviation (in lattice) |
|
235 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le" |
|
236 |
|
237 lemma (in order_syntax) least_Upper_above: |
|
238 "[| least s (Upper A); x \<in> A; A \<subseteq> carrier |] ==> x \<sqsubseteq> s" |
187 by (unfold least_def) blast |
239 by (unfold least_def) blast |
188 |
240 |
189 lemma greatest_Lower_above: |
241 lemma (in order_syntax) greatest_Lower_above: |
190 fixes L (structure) |
242 "[| greatest i (Lower A); x \<in> A; A \<subseteq> carrier |] ==> i \<sqsubseteq> x" |
191 shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" |
|
192 by (unfold greatest_def) blast |
243 by (unfold greatest_def) blast |
193 |
244 |
194 |
245 |
195 subsubsection {* Supremum *} |
246 subsubsection {* Supremum *} |
196 |
247 |
197 lemma (in lattice) joinI: |
248 lemma (in lattice) joinI: |
198 "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] |
249 "[| !!l. least l (Upper {x, y}) ==> P l; x \<in> carrier; y \<in> carrier |] |
199 ==> P (x \<squnion> y)" |
250 ==> P (x \<squnion> y)" |
200 proof (unfold join_def sup_def) |
251 proof (unfold join_def sup_def) |
201 assume L: "x \<in> carrier L" "y \<in> carrier L" |
252 assume L: "x \<in> carrier" "y \<in> carrier" |
202 and P: "!!l. least L l (Upper L {x, y}) ==> P l" |
253 and P: "!!l. least l (Upper {x, y}) ==> P l" |
203 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
254 with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast |
204 with L show "P (THE l. least L l (Upper L {x, y}))" |
255 with L show "P (THE l. least l (Upper {x, y}))" |
205 by (fast intro: theI2 least_unique P) |
256 by (fast intro: theI2 least_unique P) |
206 qed |
257 qed |
207 |
258 |
208 lemma (in lattice) join_closed [simp]: |
259 lemma (in lattice) join_closed [simp]: |
209 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" |
260 "[| x \<in> carrier; y \<in> carrier |] ==> x \<squnion> y \<in> carrier" |
210 by (rule joinI) (rule least_carrier) |
261 by (rule joinI) (rule least_carrier) |
211 |
262 |
212 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
263 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
213 "x \<in> carrier L ==> least L x (Upper L {x})" |
264 "x \<in> carrier ==> least x (Upper {x})" |
214 by (rule least_UpperI) fast+ |
265 by (rule least_UpperI) fast+ |
215 |
266 |
216 lemma (in partial_order) sup_of_singleton [simp]: |
267 lemma (in partial_order) sup_of_singleton [simp]: |
217 "x \<in> carrier L ==> \<Squnion>{x} = x" |
268 "x \<in> carrier ==> \<Squnion>{x} = x" |
218 by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) |
269 by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) |
219 |
270 |
220 |
271 |
221 text {* Condition on @{text A}: supremum exists. *} |
272 text {* Condition on @{text A}: supremum exists. *} |
222 |
273 |
223 lemma (in lattice) sup_insertI: |
274 lemma (in lattice) sup_insertI: |
224 "[| !!s. least L s (Upper L (insert x A)) ==> P s; |
275 "[| !!s. least s (Upper (insert x A)) ==> P s; |
225 least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] |
276 least a (Upper A); x \<in> carrier; A \<subseteq> carrier |] |
226 ==> P (\<Squnion>(insert x A))" |
277 ==> P (\<Squnion>(insert x A))" |
227 proof (unfold sup_def) |
278 proof (unfold sup_def) |
228 assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
279 assume L: "x \<in> carrier" "A \<subseteq> carrier" |
229 and P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
280 and P: "!!l. least l (Upper (insert x A)) ==> P l" |
230 and least_a: "least L a (Upper L A)" |
281 and least_a: "least a (Upper A)" |
231 from L least_a have La: "a \<in> carrier L" by simp |
282 from least_a have La: "a \<in> carrier" by simp |
232 from L sup_of_two_exists least_a |
283 from L sup_of_two_exists least_a |
233 obtain s where least_s: "least L s (Upper L {a, x})" by blast |
284 obtain s where least_s: "least s (Upper {a, x})" by blast |
234 show "P (THE l. least L l (Upper L (insert x A)))" |
285 show "P (THE l. least l (Upper (insert x A)))" |
235 proof (rule theI2) |
286 proof (rule theI2) |
236 show "least L s (Upper L (insert x A))" |
287 show "least s (Upper (insert x A))" |
237 proof (rule least_UpperI) |
288 proof (rule least_UpperI) |
238 fix z |
289 fix z |
239 assume "z \<in> insert x A" |
290 assume "z \<in> insert x A" |
240 then show "z \<sqsubseteq> s" |
291 then show "z \<sqsubseteq> s" |
241 proof |
292 proof |
327 proof (cases "A = {}") |
378 proof (cases "A = {}") |
328 case True |
379 case True |
329 with insert show ?thesis by (simp add: sup_of_singletonI) |
380 with insert show ?thesis by (simp add: sup_of_singletonI) |
330 next |
381 next |
331 case False |
382 case False |
332 with insert have "least L (\<Squnion>A) (Upper L A)" by simp |
383 with insert have "least (\<Squnion>A) (Upper A)" by simp |
333 with _ show ?thesis |
384 with _ show ?thesis |
334 by (rule sup_insertI) (simp_all add: insert [simplified]) |
385 by (rule sup_insertI) (simp_all add: insert [simplified]) |
335 qed |
386 qed |
336 qed |
387 qed |
337 |
388 |
338 lemma (in lattice) finite_sup_insertI: |
389 lemma (in lattice) finite_sup_insertI: |
339 assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
390 assumes P: "!!l. least l (Upper (insert x A)) ==> P l" |
340 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
391 and xA: "finite A" "x \<in> carrier" "A \<subseteq> carrier" |
341 shows "P (\<Squnion> (insert x A))" |
392 shows "P (\<Squnion> (insert x A))" |
342 proof (cases "A = {}") |
393 proof (cases "A = {}") |
343 case True with P and xA show ?thesis |
394 case True with P and xA show ?thesis |
344 by (simp add: sup_of_singletonI) |
395 by (simp add: sup_of_singletonI) |
345 next |
396 next |
346 case False with P and xA show ?thesis |
397 case False with P and xA show ?thesis |
347 by (simp add: sup_insertI finite_sup_least) |
398 by (simp add: sup_insertI finite_sup_least) |
348 qed |
399 qed |
349 |
400 |
350 lemma (in lattice) finite_sup_closed: |
401 lemma (in lattice) finite_sup_closed: |
351 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" |
402 "[| finite A; A \<subseteq> carrier; A ~= {} |] ==> \<Squnion>A \<in> carrier" |
352 proof (induct set: Finites) |
403 proof (induct set: Finites) |
353 case empty then show ?case by simp |
404 case empty then show ?case by simp |
354 next |
405 next |
355 case insert then show ?case |
406 case insert then show ?case |
356 by - (rule finite_sup_insertI, simp_all) |
407 by - (rule finite_sup_insertI, simp_all) |
357 qed |
408 qed |
358 |
409 |
359 lemma (in lattice) join_left: |
410 lemma (in lattice) join_left: |
360 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
411 "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqsubseteq> x \<squnion> y" |
361 by (rule joinI [folded join_def]) (blast dest: least_mem) |
412 by (rule joinI [folded join_def]) (blast dest: least_mem) |
362 |
413 |
363 lemma (in lattice) join_right: |
414 lemma (in lattice) join_right: |
364 "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
415 "[| x \<in> carrier; y \<in> carrier |] ==> y \<sqsubseteq> x \<squnion> y" |
365 by (rule joinI [folded join_def]) (blast dest: least_mem) |
416 by (rule joinI [folded join_def]) (blast dest: least_mem) |
366 |
417 |
367 lemma (in lattice) sup_of_two_least: |
418 lemma (in lattice) sup_of_two_least: |
368 "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" |
419 "[| x \<in> carrier; y \<in> carrier |] ==> least (\<Squnion>{x, y}) (Upper {x, y})" |
369 proof (unfold sup_def) |
420 proof (unfold sup_def) |
370 assume L: "x \<in> carrier L" "y \<in> carrier L" |
421 assume L: "x \<in> carrier" "y \<in> carrier" |
371 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
422 with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast |
372 with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" |
423 with L show "least (THE xa. least xa (Upper {x, y})) (Upper {x, y})" |
373 by (fast intro: theI2 least_unique) (* blast fails *) |
424 by (fast intro: theI2 least_unique) (* blast fails *) |
374 qed |
425 qed |
375 |
426 |
376 lemma (in lattice) join_le: |
427 lemma (in lattice) join_le: |
377 assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
428 assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
378 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
429 and L: "x \<in> carrier" "y \<in> carrier" "z \<in> carrier" |
379 shows "x \<squnion> y \<sqsubseteq> z" |
430 shows "x \<squnion> y \<sqsubseteq> z" |
380 proof (rule joinI) |
431 proof (rule joinI) |
381 fix s |
432 fix s |
382 assume "least L s (Upper L {x, y})" |
433 assume "least s (Upper {x, y})" |
383 with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
434 with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
384 qed |
435 qed |
385 |
436 |
386 lemma (in lattice) join_assoc_lemma: |
437 lemma (in lattice) join_assoc_lemma: |
387 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
438 assumes L: "x \<in> carrier" "y \<in> carrier" "z \<in> carrier" |
388 shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" |
439 shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" |
389 proof (rule finite_sup_insertI) |
440 proof (rule finite_sup_insertI) |
390 -- {* The textbook argument in Jacobson I, p 457 *} |
441 -- {* The textbook argument in Jacobson I, p 457 *} |
391 fix s |
442 fix s |
392 assume sup: "least L s (Upper L {x, y, z})" |
443 assume sup: "least s (Upper {x, y, z})" |
393 show "x \<squnion> (y \<squnion> z) = s" |
444 show "x \<squnion> (y \<squnion> z) = s" |
394 proof (rule anti_sym) |
445 proof (rule anti_sym) |
395 from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" |
446 from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" |
396 by (fastsimp intro!: join_le elim: least_Upper_above) |
447 by (fastsimp intro!: join_le elim: least_Upper_above) |
397 next |
448 next |
419 |
469 |
420 |
470 |
421 subsubsection {* Infimum *} |
471 subsubsection {* Infimum *} |
422 |
472 |
423 lemma (in lattice) meetI: |
473 lemma (in lattice) meetI: |
424 "[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
474 "[| !!i. greatest i (Lower {x, y}) ==> P i; |
425 x \<in> carrier L; y \<in> carrier L |] |
475 x \<in> carrier; y \<in> carrier |] |
426 ==> P (x \<sqinter> y)" |
476 ==> P (x \<sqinter> y)" |
427 proof (unfold meet_def inf_def) |
477 proof (unfold meet_def inf_def) |
428 assume L: "x \<in> carrier L" "y \<in> carrier L" |
478 assume L: "x \<in> carrier" "y \<in> carrier" |
429 and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
479 and P: "!!g. greatest g (Lower {x, y}) ==> P g" |
430 with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast |
480 with inf_of_two_exists obtain i where "greatest i (Lower {x, y})" by fast |
431 with L show "P (THE g. greatest L g (Lower L {x, y}))" |
481 with L show "P (THE g. greatest g (Lower {x, y}))" |
432 by (fast intro: theI2 greatest_unique P) |
482 by (fast intro: theI2 greatest_unique P) |
433 qed |
483 qed |
434 |
484 |
435 lemma (in lattice) meet_closed [simp]: |
485 lemma (in lattice) meet_closed [simp]: |
436 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" |
486 "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqinter> y \<in> carrier" |
437 by (rule meetI) (rule greatest_carrier) |
487 by (rule meetI) (rule greatest_carrier) |
438 |
488 |
439 lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
489 lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
440 "x \<in> carrier L ==> greatest L x (Lower L {x})" |
490 "x \<in> carrier ==> greatest x (Lower {x})" |
441 by (rule greatest_LowerI) fast+ |
491 by (rule greatest_LowerI) fast+ |
442 |
492 |
443 lemma (in partial_order) inf_of_singleton [simp]: |
493 lemma (in partial_order) inf_of_singleton [simp]: |
444 "x \<in> carrier L ==> \<Sqinter> {x} = x" |
494 "x \<in> carrier ==> \<Sqinter> {x} = x" |
445 by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
495 by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
446 |
496 |
447 text {* Condition on A: infimum exists. *} |
497 text {* Condition on A: infimum exists. *} |
448 |
498 |
449 lemma (in lattice) inf_insertI: |
499 lemma (in lattice) inf_insertI: |
450 "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
500 "[| !!i. greatest i (Lower (insert x A)) ==> P i; |
451 greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
501 greatest a (Lower A); x \<in> carrier; A \<subseteq> carrier |] |
452 ==> P (\<Sqinter>(insert x A))" |
502 ==> P (\<Sqinter>(insert x A))" |
453 proof (unfold inf_def) |
503 proof (unfold inf_def) |
454 assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
504 assume L: "x \<in> carrier" "A \<subseteq> carrier" |
455 and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" |
505 and P: "!!g. greatest g (Lower (insert x A)) ==> P g" |
456 and greatest_a: "greatest L a (Lower L A)" |
506 and greatest_a: "greatest a (Lower A)" |
457 from L greatest_a have La: "a \<in> carrier L" by simp |
507 from greatest_a have La: "a \<in> carrier" by simp |
458 from L inf_of_two_exists greatest_a |
508 from L inf_of_two_exists greatest_a |
459 obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast |
509 obtain i where greatest_i: "greatest i (Lower {a, x})" by blast |
460 show "P (THE g. greatest L g (Lower L (insert x A)))" |
510 show "P (THE g. greatest g (Lower (insert x A)))" |
461 proof (rule theI2) |
511 proof (rule theI2) |
462 show "greatest L i (Lower L (insert x A))" |
512 show "greatest i (Lower (insert x A))" |
463 proof (rule greatest_LowerI) |
513 proof (rule greatest_LowerI) |
464 fix z |
514 fix z |
465 assume "z \<in> insert x A" |
515 assume "z \<in> insert x A" |
466 then show "i \<sqsubseteq> z" |
516 then show "i \<sqsubseteq> z" |
467 proof |
517 proof |
554 with insert show ?thesis by (simp add: inf_of_singletonI) |
604 with insert show ?thesis by (simp add: inf_of_singletonI) |
555 next |
605 next |
556 case False |
606 case False |
557 from insert show ?thesis |
607 from insert show ?thesis |
558 proof (rule_tac inf_insertI) |
608 proof (rule_tac inf_insertI) |
559 from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp |
609 from False insert show "greatest (\<Sqinter>A) (Lower A)" by simp |
560 qed simp_all |
610 qed simp_all |
561 qed |
611 qed |
562 qed |
612 qed |
563 |
613 |
564 lemma (in lattice) finite_inf_insertI: |
614 lemma (in lattice) finite_inf_insertI: |
565 assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" |
615 assumes P: "!!i. greatest i (Lower (insert x A)) ==> P i" |
566 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
616 and xA: "finite A" "x \<in> carrier" "A \<subseteq> carrier" |
567 shows "P (\<Sqinter> (insert x A))" |
617 shows "P (\<Sqinter> (insert x A))" |
568 proof (cases "A = {}") |
618 proof (cases "A = {}") |
569 case True with P and xA show ?thesis |
619 case True with P and xA show ?thesis |
570 by (simp add: inf_of_singletonI) |
620 by (simp add: inf_of_singletonI) |
571 next |
621 next |
572 case False with P and xA show ?thesis |
622 case False with P and xA show ?thesis |
573 by (simp add: inf_insertI finite_inf_greatest) |
623 by (simp add: inf_insertI finite_inf_greatest) |
574 qed |
624 qed |
575 |
625 |
576 lemma (in lattice) finite_inf_closed: |
626 lemma (in lattice) finite_inf_closed: |
577 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" |
627 "[| finite A; A \<subseteq> carrier; A ~= {} |] ==> \<Sqinter>A \<in> carrier" |
578 proof (induct set: Finites) |
628 proof (induct set: Finites) |
579 case empty then show ?case by simp |
629 case empty then show ?case by simp |
580 next |
630 next |
581 case insert then show ?case |
631 case insert then show ?case |
582 by (rule_tac finite_inf_insertI) (simp_all) |
632 by (rule_tac finite_inf_insertI) (simp_all) |
583 qed |
633 qed |
584 |
634 |
585 lemma (in lattice) meet_left: |
635 lemma (in lattice) meet_left: |
586 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
636 "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqinter> y \<sqsubseteq> x" |
587 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
637 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
588 |
638 |
589 lemma (in lattice) meet_right: |
639 lemma (in lattice) meet_right: |
590 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
640 "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqinter> y \<sqsubseteq> y" |
591 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
641 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
592 |
642 |
593 lemma (in lattice) inf_of_two_greatest: |
643 lemma (in lattice) inf_of_two_greatest: |
594 "[| x \<in> carrier L; y \<in> carrier L |] ==> |
644 "[| x \<in> carrier; y \<in> carrier |] ==> |
595 greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" |
645 greatest (\<Sqinter> {x, y}) (Lower {x, y})" |
596 proof (unfold inf_def) |
646 proof (unfold inf_def) |
597 assume L: "x \<in> carrier L" "y \<in> carrier L" |
647 assume L: "x \<in> carrier" "y \<in> carrier" |
598 with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
648 with inf_of_two_exists obtain s where "greatest s (Lower {x, y})" by fast |
599 with L |
649 with L |
600 show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" |
650 show "greatest (THE xa. greatest xa (Lower {x, y})) (Lower {x, y})" |
601 by (fast intro: theI2 greatest_unique) (* blast fails *) |
651 by (fast intro: theI2 greatest_unique) (* blast fails *) |
602 qed |
652 qed |
603 |
653 |
604 lemma (in lattice) meet_le: |
654 lemma (in lattice) meet_le: |
605 assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
655 assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
606 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
656 and L: "x \<in> carrier" "y \<in> carrier" "z \<in> carrier" |
607 shows "z \<sqsubseteq> x \<sqinter> y" |
657 shows "z \<sqsubseteq> x \<sqinter> y" |
608 proof (rule meetI) |
658 proof (rule meetI) |
609 fix i |
659 fix i |
610 assume "greatest L i (Lower L {x, y})" |
660 assume "greatest i (Lower {x, y})" |
611 with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
661 with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
612 qed |
662 qed |
613 |
663 |
614 lemma (in lattice) meet_assoc_lemma: |
664 lemma (in lattice) meet_assoc_lemma: |
615 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
665 assumes L: "x \<in> carrier" "y \<in> carrier" "z \<in> carrier" |
616 shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" |
666 shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" |
617 proof (rule finite_inf_insertI) |
667 proof (rule finite_inf_insertI) |
618 txt {* The textbook argument in Jacobson I, p 457 *} |
668 txt {* The textbook argument in Jacobson I, p 457 *} |
619 fix i |
669 fix i |
620 assume inf: "greatest L i (Lower L {x, y, z})" |
670 assume inf: "greatest i (Lower {x, y, z})" |
621 show "x \<sqinter> (y \<sqinter> z) = i" |
671 show "x \<sqinter> (y \<sqinter> z) = i" |
622 proof (rule anti_sym) |
672 proof (rule anti_sym) |
623 from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
673 from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
624 by (fastsimp intro!: meet_le elim: greatest_Lower_above) |
674 by (fastsimp intro!: meet_le elim: greatest_Lower_above) |
625 next |
675 next |
647 |
696 |
648 |
697 |
649 subsection {* Total Orders *} |
698 subsection {* Total Orders *} |
650 |
699 |
651 locale total_order = lattice + |
700 locale total_order = lattice + |
652 assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
701 assumes total: "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
|
702 |
|
703 abbreviation (in total_order) |
|
704 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
|
705 abbreviation (in total_order) |
|
706 Upper where "Upper == order_syntax.Upper carrier le" |
|
707 abbreviation (in total_order) |
|
708 Lower where "Lower == order_syntax.Lower carrier le" |
|
709 abbreviation (in total_order) |
|
710 least where "least == order_syntax.least carrier le" |
|
711 abbreviation (in total_order) |
|
712 greatest where "greatest == order_syntax.greatest carrier le" |
|
713 abbreviation (in total_order) |
|
714 sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le" |
|
715 abbreviation (in total_order) |
|
716 inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le" |
|
717 abbreviation (in total_order) |
|
718 join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le" |
|
719 abbreviation (in total_order) |
|
720 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le" |
653 |
721 |
654 text {* Introduction rule: the usual definition of total order *} |
722 text {* Introduction rule: the usual definition of total order *} |
655 |
723 |
656 lemma (in partial_order) total_orderI: |
724 lemma (in partial_order) total_orderI: |
657 assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
725 assumes total: "!!x y. [| x \<in> carrier; y \<in> carrier |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" |
658 shows "total_order L" |
726 shows "total_order carrier le" |
659 proof intro_locales |
727 proof intro_locales |
660 show "lattice_axioms L" |
728 show "lattice_axioms carrier le" |
661 proof (rule lattice_axioms.intro) |
729 proof (rule lattice_axioms.intro) |
662 fix x y |
730 fix x y |
663 assume L: "x \<in> carrier L" "y \<in> carrier L" |
731 assume L: "x \<in> carrier" "y \<in> carrier" |
664 show "EX s. least L s (Upper L {x, y})" |
732 show "EX s. least s (Upper {x, y})" |
665 proof - |
733 proof - |
666 note total L |
734 note total L |
667 moreover |
735 moreover |
668 { |
736 { |
669 assume "x \<sqsubseteq> y" |
737 assume "x \<sqsubseteq> y" |
670 with L have "least L y (Upper L {x, y})" |
738 with L have "least y (Upper {x, y})" |
671 by (rule_tac least_UpperI) auto |
739 by (rule_tac least_UpperI) auto |
672 } |
740 } |
673 moreover |
741 moreover |
674 { |
742 { |
675 assume "y \<sqsubseteq> x" |
743 assume "y \<sqsubseteq> x" |
676 with L have "least L x (Upper L {x, y})" |
744 with L have "least x (Upper {x, y})" |
677 by (rule_tac least_UpperI) auto |
745 by (rule_tac least_UpperI) auto |
678 } |
746 } |
679 ultimately show ?thesis by blast |
747 ultimately show ?thesis by blast |
680 qed |
748 qed |
681 next |
749 next |
682 fix x y |
750 fix x y |
683 assume L: "x \<in> carrier L" "y \<in> carrier L" |
751 assume L: "x \<in> carrier" "y \<in> carrier" |
684 show "EX i. greatest L i (Lower L {x, y})" |
752 show "EX i. greatest i (Lower {x, y})" |
685 proof - |
753 proof - |
686 note total L |
754 note total L |
687 moreover |
755 moreover |
688 { |
756 { |
689 assume "y \<sqsubseteq> x" |
757 assume "y \<sqsubseteq> x" |
690 with L have "greatest L y (Lower L {x, y})" |
758 with L have "greatest y (Lower {x, y})" |
691 by (rule_tac greatest_LowerI) auto |
759 by (rule_tac greatest_LowerI) auto |
692 } |
760 } |
693 moreover |
761 moreover |
694 { |
762 { |
695 assume "x \<sqsubseteq> y" |
763 assume "x \<sqsubseteq> y" |
696 with L have "greatest L x (Lower L {x, y})" |
764 with L have "greatest x (Lower {x, y})" |
697 by (rule_tac greatest_LowerI) auto |
765 by (rule_tac greatest_LowerI) auto |
698 } |
766 } |
699 ultimately show ?thesis by blast |
767 ultimately show ?thesis by blast |
700 qed |
768 qed |
701 qed |
769 qed |
704 |
772 |
705 subsection {* Complete lattices *} |
773 subsection {* Complete lattices *} |
706 |
774 |
707 locale complete_lattice = lattice + |
775 locale complete_lattice = lattice + |
708 assumes sup_exists: |
776 assumes sup_exists: |
709 "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
777 "[| A \<subseteq> carrier |] ==> EX s. order_syntax.least carrier le s (order_syntax.Upper carrier le A)" |
710 and inf_exists: |
778 and inf_exists: |
711 "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" |
779 "[| A \<subseteq> carrier |] ==> EX i. order_syntax.greatest carrier le i (order_syntax.Lower carrier le A)" |
|
780 |
|
781 abbreviation (in complete_lattice) |
|
782 less (infixl "\<sqsubset>" 50) "less == order_syntax.less le" |
|
783 abbreviation (in complete_lattice) |
|
784 Upper where "Upper == order_syntax.Upper carrier le" |
|
785 abbreviation (in complete_lattice) |
|
786 Lower where "Lower == order_syntax.Lower carrier le" |
|
787 abbreviation (in complete_lattice) |
|
788 least where "least == order_syntax.least carrier le" |
|
789 abbreviation (in complete_lattice) |
|
790 greatest where "greatest == order_syntax.greatest carrier le" |
|
791 abbreviation (in complete_lattice) |
|
792 sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le" |
|
793 abbreviation (in complete_lattice) |
|
794 inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le" |
|
795 abbreviation (in complete_lattice) |
|
796 join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le" |
|
797 abbreviation (in complete_lattice) |
|
798 meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le" |
712 |
799 |
713 text {* Introduction rule: the usual definition of complete lattice *} |
800 text {* Introduction rule: the usual definition of complete lattice *} |
714 |
801 |
715 lemma (in partial_order) complete_latticeI: |
802 lemma (in partial_order) complete_latticeI: |
716 assumes sup_exists: |
803 assumes sup_exists: |
717 "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" |
804 "!!A. [| A \<subseteq> carrier |] ==> EX s. least s (Upper A)" |
718 and inf_exists: |
805 and inf_exists: |
719 "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" |
806 "!!A. [| A \<subseteq> carrier |] ==> EX i. greatest i (Lower A)" |
720 shows "complete_lattice L" |
807 shows "complete_lattice carrier le" |
721 proof intro_locales |
808 proof intro_locales |
722 show "lattice_axioms L" |
809 show "lattice_axioms carrier le" |
723 by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
810 by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ |
724 qed (assumption | rule complete_lattice_axioms.intro)+ |
811 qed (assumption | rule complete_lattice_axioms.intro)+ |
725 |
812 |
726 constdefs (structure L) |
813 definition (in order_syntax) |
727 top :: "_ => 'a" ("\<top>\<index>") |
814 top ("\<top>") |
728 "\<top> == sup L (carrier L)" |
815 "\<top> == sup carrier" |
729 |
816 |
730 bottom :: "_ => 'a" ("\<bottom>\<index>") |
817 definition (in order_syntax) |
731 "\<bottom> == inf L (carrier L)" |
818 bottom ("\<bottom>") |
|
819 "\<bottom> == inf carrier" |
|
820 |
|
821 abbreviation (in partial_order) |
|
822 top ("\<top>") "top == order_syntax.top carrier le" |
|
823 abbreviation (in partial_order) |
|
824 bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le" |
|
825 abbreviation (in lattice) |
|
826 top ("\<top>") "top == order_syntax.top carrier le" |
|
827 abbreviation (in lattice) |
|
828 bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le" |
|
829 abbreviation (in total_order) |
|
830 top ("\<top>") "top == order_syntax.top carrier le" |
|
831 abbreviation (in total_order) |
|
832 bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le" |
|
833 abbreviation (in complete_lattice) |
|
834 top ("\<top>") "top == order_syntax.top carrier le" |
|
835 abbreviation (in complete_lattice) |
|
836 bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le" |
732 |
837 |
733 |
838 |
734 lemma (in complete_lattice) supI: |
839 lemma (in complete_lattice) supI: |
735 "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |] |
840 "[| !!l. least l (Upper A) ==> P l; A \<subseteq> carrier |] |
736 ==> P (\<Squnion>A)" |
841 ==> P (\<Squnion>A)" |
737 proof (unfold sup_def) |
842 proof (unfold sup_def) |
738 assume L: "A \<subseteq> carrier L" |
843 assume L: "A \<subseteq> carrier" |
739 and P: "!!l. least L l (Upper L A) ==> P l" |
844 and P: "!!l. least l (Upper A) ==> P l" |
740 with sup_exists obtain s where "least L s (Upper L A)" by blast |
845 with sup_exists obtain s where "least s (Upper A)" by blast |
741 with L show "P (THE l. least L l (Upper L A))" |
846 with L show "P (THE l. least l (Upper A))" |
742 by (fast intro: theI2 least_unique P) |
847 by (fast intro: theI2 least_unique P) |
743 qed |
848 qed |
744 |
849 |
745 lemma (in complete_lattice) sup_closed [simp]: |
850 lemma (in complete_lattice) sup_closed [simp]: |
746 "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" |
851 "A \<subseteq> carrier ==> \<Squnion>A \<in> carrier" |
747 by (rule supI) simp_all |
852 by (rule supI) simp_all |
748 |
853 |
749 lemma (in complete_lattice) top_closed [simp, intro]: |
854 lemma (in complete_lattice) top_closed [simp, intro]: |
750 "\<top> \<in> carrier L" |
855 "\<top> \<in> carrier" |
751 by (unfold top_def) simp |
856 by (unfold top_def) simp |
752 |
857 |
753 lemma (in complete_lattice) infI: |
858 lemma (in complete_lattice) infI: |
754 "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] |
859 "[| !!i. greatest i (Lower A) ==> P i; A \<subseteq> carrier |] |
755 ==> P (\<Sqinter>A)" |
860 ==> P (\<Sqinter>A)" |
756 proof (unfold inf_def) |
861 proof (unfold inf_def) |
757 assume L: "A \<subseteq> carrier L" |
862 assume L: "A \<subseteq> carrier" |
758 and P: "!!l. greatest L l (Lower L A) ==> P l" |
863 and P: "!!l. greatest l (Lower A) ==> P l" |
759 with inf_exists obtain s where "greatest L s (Lower L A)" by blast |
864 with inf_exists obtain s where "greatest s (Lower A)" by blast |
760 with L show "P (THE l. greatest L l (Lower L A))" |
865 with L show "P (THE l. greatest l (Lower A))" |
761 by (fast intro: theI2 greatest_unique P) |
866 by (fast intro: theI2 greatest_unique P) |
762 qed |
867 qed |
763 |
868 |
764 lemma (in complete_lattice) inf_closed [simp]: |
869 lemma (in complete_lattice) inf_closed [simp]: |
765 "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" |
870 "A \<subseteq> carrier ==> \<Sqinter>A \<in> carrier" |
766 by (rule infI) simp_all |
871 by (rule infI) simp_all |
767 |
872 |
768 lemma (in complete_lattice) bottom_closed [simp, intro]: |
873 lemma (in complete_lattice) bottom_closed [simp, intro]: |
769 "\<bottom> \<in> carrier L" |
874 "\<bottom> \<in> carrier" |
770 by (unfold bottom_def) simp |
875 by (unfold bottom_def) simp |
771 |
876 |
772 text {* Jacobson: Theorem 8.1 *} |
877 text {* Jacobson: Theorem 8.1 *} |
773 |
878 |
774 lemma Lower_empty [simp]: |
879 lemma (in order_syntax) Lower_empty [simp]: |
775 "Lower L {} = carrier L" |
880 "Lower {} = carrier" |
776 by (unfold Lower_def) simp |
881 by (unfold Lower_def) simp |
777 |
882 |
778 lemma Upper_empty [simp]: |
883 lemma (in order_syntax) Upper_empty [simp]: |
779 "Upper L {} = carrier L" |
884 "Upper {} = carrier" |
780 by (unfold Upper_def) simp |
885 by (unfold Upper_def) simp |
781 |
886 |
782 theorem (in partial_order) complete_lattice_criterion1: |
887 theorem (in partial_order) complete_lattice_criterion1: |
783 assumes top_exists: "EX g. greatest L g (carrier L)" |
888 assumes top_exists: "EX g. greatest g (carrier)" |
784 and inf_exists: |
889 and inf_exists: |
785 "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" |
890 "!!A. [| A \<subseteq> carrier; A ~= {} |] ==> EX i. greatest i (Lower A)" |
786 shows "complete_lattice L" |
891 shows "complete_lattice carrier le" |
787 proof (rule complete_latticeI) |
892 proof (rule complete_latticeI) |
788 from top_exists obtain top where top: "greatest L top (carrier L)" .. |
893 from top_exists obtain top where top: "greatest top (carrier)" .. |
789 fix A |
894 fix A |
790 assume L: "A \<subseteq> carrier L" |
895 assume L: "A \<subseteq> carrier" |
791 let ?B = "Upper L A" |
896 let ?B = "Upper A" |
792 from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) |
897 from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) |
793 then have B_non_empty: "?B ~= {}" by fast |
898 then have B_non_empty: "?B ~= {}" by fast |
794 have B_L: "?B \<subseteq> carrier L" by simp |
899 have B_L: "?B \<subseteq> carrier" by simp |
795 from inf_exists [OF B_L B_non_empty] |
900 from inf_exists [OF B_L B_non_empty] |
796 obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. |
901 obtain b where b_inf_B: "greatest b (Lower ?B)" .. |
797 have "least L b (Upper L A)" |
902 have "least b (Upper A)" |
798 apply (rule least_UpperI) |
903 apply (rule least_UpperI) |
799 apply (rule greatest_le [where A = "Lower L ?B"]) |
904 apply (rule greatest_le [where A = "Lower ?B"]) |
800 apply (rule b_inf_B) |
905 apply (rule b_inf_B) |
801 apply (rule Lower_memI) |
906 apply (rule Lower_memI) |
802 apply (erule UpperD) |
907 apply (erule UpperD) |
803 apply assumption |
908 apply assumption |
804 apply (rule L) |
909 apply (rule L) |