148 lemma (in partial_order) greatest_unique: |
145 lemma (in partial_order) greatest_unique: |
149 "[| greatest L x A; greatest L y A |] ==> x = y" |
146 "[| greatest L x A; greatest L y A |] ==> x = y" |
150 by (unfold greatest_def) blast |
147 by (unfold greatest_def) blast |
151 |
148 |
152 lemma greatest_le: |
149 lemma greatest_le: |
153 includes order_syntax |
150 includes struct L |
154 shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" |
151 shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" |
155 by (unfold greatest_def) fast |
152 by (unfold greatest_def) fast |
156 |
153 |
157 lemma greatest_LowerI: |
154 lemma greatest_LowerI: |
158 includes order_syntax |
155 includes struct L |
159 assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" |
156 assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" |
160 and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" |
157 and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" |
161 and L: "A \<subseteq> carrier L" "i \<in> carrier L" |
158 and L: "A \<subseteq> carrier L" "i \<in> carrier L" |
162 shows "greatest L i (Lower L A)" |
159 shows "greatest L i (Lower L A)" |
163 proof (unfold greatest_def, intro conjI) |
160 proof - |
164 show "Lower L A \<subseteq> carrier L" by simp |
161 have "Lower L A \<subseteq> carrier L" by simp |
165 next |
162 moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) |
166 from below L show "i \<in> Lower L A" by (simp add: Lower_def) |
163 moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast |
167 next |
164 ultimately show ?thesis by (simp add: greatest_def) |
168 from above show "ALL x : Lower L A. x \<sqsubseteq> i" by fast |
165 qed |
169 qed |
166 |
170 |
167 |
171 subsection {* Lattices *} |
168 subsection {* Lattices *} |
172 |
169 |
173 locale lattice = partial_order + |
170 locale lattice = partial_order + |
174 assumes sup_of_two_exists: |
171 assumes sup_of_two_exists: |
175 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
172 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" |
176 and inf_of_two_exists: |
173 and inf_of_two_exists: |
177 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
174 "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" |
178 |
175 |
179 lemma least_Upper_above: |
176 lemma least_Upper_above: |
180 includes order_syntax |
177 includes struct L |
181 shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" |
178 shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" |
182 by (unfold least_def) blast |
179 by (unfold least_def) blast |
183 |
180 |
184 lemma greatest_Lower_above: |
181 lemma greatest_Lower_above: |
185 includes order_syntax |
182 includes struct L |
186 shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" |
183 shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" |
187 by (unfold greatest_def) blast |
184 by (unfold greatest_def) blast |
188 |
185 |
189 |
186 |
190 subsubsection {* Supremum *} |
187 subsubsection {* Supremum *} |
191 |
188 |
192 lemma (in lattice) joinI: |
189 lemma (in lattice) joinI: |
193 "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] |
190 "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] |
194 ==> P (x \<squnion> y)" |
191 ==> P (x \<squnion> y)" |
195 proof (unfold join_def sup_def) |
192 proof (unfold join_def sup_def) |
196 assume L: "x \<in> carrier L" "y \<in> carrier L" |
193 assume L: "x \<in> carrier L" "y \<in> carrier L" |
197 and P: "!!l. least L l (Upper L {x, y}) ==> P l" |
194 and P: "!!l. least L l (Upper L {x, y}) ==> P l" |
198 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
195 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
199 with L show "P (THE l. least L l (Upper L {x, y}))" |
196 with L show "P (THE l. least L l (Upper L {x, y}))" |
200 by (fast intro: theI2 least_unique P) |
197 by (fast intro: theI2 least_unique P) |
201 qed |
198 qed |
202 |
199 |
203 lemma (in lattice) join_closed [simp]: |
200 lemma (in lattice) join_closed [simp]: |
204 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" |
201 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" |
205 by (rule joinI) (rule least_carrier) |
202 by (rule joinI) (rule least_carrier) |
207 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
204 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) |
208 "x \<in> carrier L ==> least L x (Upper L {x})" |
205 "x \<in> carrier L ==> least L x (Upper L {x})" |
209 by (rule least_UpperI) fast+ |
206 by (rule least_UpperI) fast+ |
210 |
207 |
211 lemma (in partial_order) sup_of_singleton [simp]: |
208 lemma (in partial_order) sup_of_singleton [simp]: |
212 includes order_syntax |
209 includes struct L |
213 shows "x \<in> carrier L ==> \<Squnion> {x} = x" |
210 shows "x \<in> carrier L ==> \<Squnion>{x} = x" |
214 by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) |
211 by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) |
215 |
212 |
216 |
213 |
217 text {* Condition on @{text A}: supremum exists. *} |
214 text {* Condition on @{text A}: supremum exists. *} |
218 |
215 |
219 lemma (in lattice) sup_insertI: |
216 lemma (in lattice) sup_insertI: |
220 "[| !!s. least L s (Upper L (insert x A)) ==> P s; |
217 "[| !!s. least L s (Upper L (insert x A)) ==> P s; |
221 least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] |
218 least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] |
222 ==> P (\<Squnion> (insert x A))" |
219 ==> P (\<Squnion>(insert x A))" |
223 proof (unfold sup_def) |
220 proof (unfold sup_def) |
224 assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
221 assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
225 and P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
222 and P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
226 and least_a: "least L a (Upper L A)" |
223 and least_a: "least L a (Upper L A)" |
227 from L least_a have La: "a \<in> carrier L" by simp |
224 from L least_a have La: "a \<in> carrier L" by simp |
228 from L sup_of_two_exists least_a |
225 from L sup_of_two_exists least_a |
229 obtain s where least_s: "least L s (Upper L {a, x})" by blast |
226 obtain s where least_s: "least L s (Upper L {a, x})" by blast |
230 show "P (THE l. least L l (Upper L (insert x A)))" |
227 show "P (THE l. least L l (Upper L (insert x A)))" |
231 proof (rule theI2 [where a = s]) |
228 proof (rule theI2) |
232 show "least L s (Upper L (insert x A))" |
229 show "least L s (Upper L (insert x A))" |
233 proof (rule least_UpperI) |
230 proof (rule least_UpperI) |
234 fix z |
231 fix z |
235 assume xA: "z \<in> insert x A" |
232 assume "z \<in> insert x A" |
236 show "z \<sqsubseteq> s" |
233 then show "z \<sqsubseteq> s" |
237 proof - |
234 proof |
238 { |
235 assume "z = x" then show ?thesis |
239 assume "z = x" then have ?thesis |
236 by (simp add: least_Upper_above [OF least_s] L La) |
240 by (simp add: least_Upper_above [OF least_s] L La) |
237 next |
241 } |
238 assume "z \<in> A" |
242 moreover |
239 with L least_s least_a show ?thesis |
243 { |
240 by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
244 assume "z \<in> A" |
241 qed |
245 with L least_s least_a have ?thesis |
242 next |
246 by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
243 fix y |
247 } |
244 assume y: "y \<in> Upper L (insert x A)" |
248 moreover note xA |
245 show "s \<sqsubseteq> y" |
249 ultimately show ?thesis by blast |
246 proof (rule least_le [OF least_s], rule Upper_memI) |
|
247 fix z |
|
248 assume z: "z \<in> {a, x}" |
|
249 then show "z \<sqsubseteq> y" |
|
250 proof |
|
251 have y': "y \<in> Upper L A" |
|
252 apply (rule subsetD [where A = "Upper L (insert x A)"]) |
|
253 apply (rule Upper_antimono) apply clarify apply assumption |
|
254 done |
|
255 assume "z = a" |
|
256 with y' least_a show ?thesis by (fast dest: least_le) |
|
257 next |
|
258 assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) |
|
259 with y L show ?thesis by blast |
|
260 qed |
|
261 qed (rule Upper_closed [THEN subsetD]) |
|
262 next |
|
263 from L show "insert x A \<subseteq> carrier L" by simp |
|
264 from least_s show "s \<in> carrier L" by simp |
250 qed |
265 qed |
251 next |
266 next |
252 fix y |
|
253 assume y: "y \<in> Upper L (insert x A)" |
|
254 show "s \<sqsubseteq> y" |
|
255 proof (rule least_le [OF least_s], rule Upper_memI) |
|
256 fix z |
|
257 assume z: "z \<in> {a, x}" |
|
258 show "z \<sqsubseteq> y" |
|
259 proof - |
|
260 { |
|
261 have y': "y \<in> Upper L A" |
|
262 apply (rule subsetD [where A = "Upper L (insert x A)"]) |
|
263 apply (rule Upper_antimono) apply clarify apply assumption |
|
264 done |
|
265 assume "z = a" |
|
266 with y' least_a have ?thesis by (fast dest: least_le) |
|
267 } |
|
268 moreover |
|
269 { |
|
270 assume "z = x" |
|
271 with y L have ?thesis by blast |
|
272 } |
|
273 moreover note z |
|
274 ultimately show ?thesis by blast |
|
275 qed |
|
276 qed (rule Upper_closed [THEN subsetD]) |
|
277 next |
|
278 from L show "insert x A \<subseteq> carrier L" by simp |
|
279 next |
|
280 from least_s show "s \<in> carrier L" by simp |
|
281 qed |
|
282 next |
|
283 fix l |
267 fix l |
284 assume least_l: "least L l (Upper L (insert x A))" |
268 assume least_l: "least L l (Upper L (insert x A))" |
285 show "l = s" |
269 show "l = s" |
286 proof (rule least_unique) |
270 proof (rule least_unique) |
287 show "least L s (Upper L (insert x A))" |
271 show "least L s (Upper L (insert x A))" |
288 proof (rule least_UpperI) |
272 proof (rule least_UpperI) |
289 fix z |
273 fix z |
290 assume xA: "z \<in> insert x A" |
274 assume "z \<in> insert x A" |
291 show "z \<sqsubseteq> s" |
275 then show "z \<sqsubseteq> s" |
292 proof - |
276 proof |
293 { |
277 assume "z = x" then show ?thesis |
294 assume "z = x" then have ?thesis |
278 by (simp add: least_Upper_above [OF least_s] L La) |
295 by (simp add: least_Upper_above [OF least_s] L La) |
279 next |
296 } |
280 assume "z \<in> A" |
297 moreover |
281 with L least_s least_a show ?thesis |
298 { |
282 by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
299 assume "z \<in> A" |
|
300 with L least_s least_a have ?thesis |
|
301 by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) |
|
302 } |
|
303 moreover note xA |
|
304 ultimately show ?thesis by blast |
|
305 qed |
283 qed |
306 next |
284 next |
307 fix y |
285 fix y |
308 assume y: "y \<in> Upper L (insert x A)" |
286 assume y: "y \<in> Upper L (insert x A)" |
309 show "s \<sqsubseteq> y" |
287 show "s \<sqsubseteq> y" |
310 proof (rule least_le [OF least_s], rule Upper_memI) |
288 proof (rule least_le [OF least_s], rule Upper_memI) |
311 fix z |
289 fix z |
312 assume z: "z \<in> {a, x}" |
290 assume z: "z \<in> {a, x}" |
313 show "z \<sqsubseteq> y" |
291 then show "z \<sqsubseteq> y" |
314 proof - |
292 proof |
315 { |
293 have y': "y \<in> Upper L A" |
316 have y': "y \<in> Upper L A" |
294 apply (rule subsetD [where A = "Upper L (insert x A)"]) |
317 apply (rule subsetD [where A = "Upper L (insert x A)"]) |
295 apply (rule Upper_antimono) apply clarify apply assumption |
318 apply (rule Upper_antimono) apply clarify apply assumption |
296 done |
319 done |
297 assume "z = a" |
320 assume "z = a" |
298 with y' least_a show ?thesis by (fast dest: least_le) |
321 with y' least_a have ?thesis by (fast dest: least_le) |
299 next |
322 } |
300 assume "z \<in> {x}" |
323 moreover |
301 with y L show ?thesis by blast |
324 { |
302 qed |
325 assume "z = x" |
303 qed (rule Upper_closed [THEN subsetD]) |
326 with y L have ?thesis by blast |
|
327 } |
|
328 moreover note z |
|
329 ultimately show ?thesis by blast |
|
330 qed |
|
331 qed (rule Upper_closed [THEN subsetD]) |
|
332 next |
304 next |
333 from L show "insert x A \<subseteq> carrier L" by simp |
305 from L show "insert x A \<subseteq> carrier L" by simp |
334 next |
306 from least_s show "s \<in> carrier L" by simp |
335 from least_s show "s \<in> carrier L" by simp |
|
336 qed |
307 qed |
337 qed |
308 qed |
338 qed |
309 qed |
339 qed |
310 qed |
340 |
311 |
341 lemma (in lattice) finite_sup_least: |
312 lemma (in lattice) finite_sup_least: |
342 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion> A) (Upper L A)" |
313 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)" |
343 proof (induct set: Finites) |
314 proof (induct set: Finites) |
344 case empty then show ?case by simp |
315 case empty |
|
316 then show ?case by simp |
345 next |
317 next |
346 case (insert A x) |
318 case (insert A x) |
347 show ?case |
319 show ?case |
348 proof (cases "A = {}") |
320 proof (cases "A = {}") |
349 case True |
321 case True |
350 with insert show ?thesis by (simp add: sup_of_singletonI) |
322 with insert show ?thesis by (simp add: sup_of_singletonI) |
351 next |
323 next |
352 case False |
324 case False |
353 from insert show ?thesis |
325 with insert have "least L (\<Squnion>A) (Upper L A)" by simp |
354 proof (rule_tac sup_insertI) |
326 with _ show ?thesis |
355 from False insert show "least L (\<Squnion> A) (Upper L A)" by simp |
327 by (rule sup_insertI) (simp_all add: insert [simplified]) |
356 qed simp_all |
|
357 qed |
328 qed |
358 qed |
329 qed |
359 |
330 |
360 lemma (in lattice) finite_sup_insertI: |
331 lemma (in lattice) finite_sup_insertI: |
361 assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
332 assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" |
362 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
333 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
363 shows "P (\<Squnion> (insert x A))" |
334 shows "P (\<Squnion> (insert x A))" |
364 proof (cases "A = {}") |
335 proof (cases "A = {}") |
365 case True with P and xA show ?thesis |
336 case True with P and xA show ?thesis |
366 by (simp add: sup_of_singletonI) |
337 by (simp add: sup_of_singletonI) |
367 next |
338 next |
368 case False with P and xA show ?thesis |
339 case False with P and xA show ?thesis |
369 by (simp add: sup_insertI finite_sup_least) |
340 by (simp add: sup_insertI finite_sup_least) |
370 qed |
341 qed |
371 |
342 |
372 lemma (in lattice) finite_sup_closed: |
343 lemma (in lattice) finite_sup_closed: |
373 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion> A \<in> carrier L" |
344 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" |
374 proof (induct set: Finites) |
345 proof (induct set: Finites) |
375 case empty then show ?case by simp |
346 case empty then show ?case by simp |
376 next |
347 next |
377 case (insert A x) then show ?case |
348 case (insert A x) then show ?case |
378 by (rule_tac finite_sup_insertI) (simp_all) |
349 by - (rule finite_sup_insertI, simp_all) |
379 qed |
350 qed |
380 |
351 |
381 lemma (in lattice) join_left: |
352 lemma (in lattice) join_left: |
382 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
353 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" |
383 by (rule joinI [folded join_def]) (blast dest: least_mem ) |
354 by (rule joinI [folded join_def]) (blast dest: least_mem) |
384 |
355 |
385 lemma (in lattice) join_right: |
356 lemma (in lattice) join_right: |
386 "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
357 "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" |
387 by (rule joinI [folded join_def]) (blast dest: least_mem ) |
358 by (rule joinI [folded join_def]) (blast dest: least_mem) |
388 |
359 |
389 lemma (in lattice) sup_of_two_least: |
360 lemma (in lattice) sup_of_two_least: |
390 "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion> {x, y}) (Upper L {x, y})" |
361 "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" |
391 proof (unfold sup_def) |
362 proof (unfold sup_def) |
392 assume L: "x \<in> carrier L" "y \<in> carrier L" |
363 assume L: "x \<in> carrier L" "y \<in> carrier L" |
393 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
364 with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast |
394 with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" |
365 with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" |
395 by (fast intro: theI2 least_unique) (* blast fails *) |
366 by (fast intro: theI2 least_unique) (* blast fails *) |
396 qed |
367 qed |
397 |
368 |
398 lemma (in lattice) join_le: |
369 lemma (in lattice) join_le: |
399 assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
370 assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" |
400 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
371 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
401 shows "x \<squnion> y \<sqsubseteq> z" |
372 shows "x \<squnion> y \<sqsubseteq> z" |
402 proof (rule joinI) |
373 proof (rule joinI) |
403 fix s |
374 fix s |
404 assume "least L s (Upper L {x, y})" |
375 assume "least L s (Upper L {x, y})" |
405 with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
376 with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) |
406 qed |
377 qed |
407 |
378 |
408 lemma (in lattice) join_assoc_lemma: |
379 lemma (in lattice) join_assoc_lemma: |
409 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
380 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
410 shows "x \<squnion> (y \<squnion> z) = \<Squnion> {x, y, z}" |
381 shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" |
411 proof (rule finite_sup_insertI) |
382 proof (rule finite_sup_insertI) |
412 -- {* The textbook argument in Jacobson I, p 457 *} |
383 -- {* The textbook argument in Jacobson I, p 457 *} |
413 fix s |
384 fix s |
414 assume sup: "least L s (Upper L {x, y, z})" |
385 assume sup: "least L s (Upper L {x, y, z})" |
415 show "x \<squnion> (y \<squnion> z) = s" |
386 show "x \<squnion> (y \<squnion> z) = s" |
422 (blast intro!: Upper_memI intro: trans join_left join_right join_closed) |
393 (blast intro!: Upper_memI intro: trans join_left join_right join_closed) |
423 qed (simp_all add: L least_carrier [OF sup]) |
394 qed (simp_all add: L least_carrier [OF sup]) |
424 qed (simp_all add: L) |
395 qed (simp_all add: L) |
425 |
396 |
426 lemma join_comm: |
397 lemma join_comm: |
427 includes order_syntax |
398 includes struct L |
428 shows "x \<squnion> y = y \<squnion> x" |
399 shows "x \<squnion> y = y \<squnion> x" |
429 by (unfold join_def) (simp add: insert_commute) |
400 by (unfold join_def) (simp add: insert_commute) |
430 |
401 |
431 lemma (in lattice) join_assoc: |
402 lemma (in lattice) join_assoc: |
432 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
403 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
433 shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
404 shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
434 proof - |
405 proof - |
435 have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) |
406 have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) |
436 also from L have "... = \<Squnion> {z, x, y}" by (simp add: join_assoc_lemma) |
407 also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma) |
437 also from L have "... = \<Squnion> {x, y, z}" by (simp add: insert_commute) |
408 also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) |
438 also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) |
409 also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) |
439 finally show ?thesis . |
410 finally show ?thesis . |
440 qed |
411 qed |
|
412 |
441 |
413 |
442 subsubsection {* Infimum *} |
414 subsubsection {* Infimum *} |
443 |
415 |
444 lemma (in lattice) meetI: |
416 lemma (in lattice) meetI: |
445 "[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
417 "[| !!i. greatest L i (Lower L {x, y}) ==> P i; |
446 x \<in> carrier L; y \<in> carrier L |] |
418 x \<in> carrier L; y \<in> carrier L |] |
447 ==> P (x \<sqinter> y)" |
419 ==> P (x \<sqinter> y)" |
448 proof (unfold meet_def inf_def) |
420 proof (unfold meet_def inf_def) |
449 assume L: "x \<in> carrier L" "y \<in> carrier L" |
421 assume L: "x \<in> carrier L" "y \<in> carrier L" |
450 and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
422 and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" |
451 with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast |
423 with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast |
452 with L show "P (THE g. greatest L g (Lower L {x, y}))" |
424 with L show "P (THE g. greatest L g (Lower L {x, y}))" |
453 by (fast intro: theI2 greatest_unique P) |
425 by (fast intro: theI2 greatest_unique P) |
454 qed |
426 qed |
460 lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
432 lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) |
461 "x \<in> carrier L ==> greatest L x (Lower L {x})" |
433 "x \<in> carrier L ==> greatest L x (Lower L {x})" |
462 by (rule greatest_LowerI) fast+ |
434 by (rule greatest_LowerI) fast+ |
463 |
435 |
464 lemma (in partial_order) inf_of_singleton [simp]: |
436 lemma (in partial_order) inf_of_singleton [simp]: |
465 includes order_syntax |
437 includes struct L |
466 shows "x \<in> carrier L ==> \<Sqinter> {x} = x" |
438 shows "x \<in> carrier L ==> \<Sqinter> {x} = x" |
467 by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
439 by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) |
468 |
440 |
469 text {* Condition on A: infimum exists. *} |
441 text {* Condition on A: infimum exists. *} |
470 |
442 |
471 lemma (in lattice) inf_insertI: |
443 lemma (in lattice) inf_insertI: |
472 "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
444 "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; |
473 greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
445 greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] |
474 ==> P (\<Sqinter> (insert x A))" |
446 ==> P (\<Sqinter>(insert x A))" |
475 proof (unfold inf_def) |
447 proof (unfold inf_def) |
476 assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
448 assume L: "x \<in> carrier L" "A \<subseteq> carrier L" |
477 and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" |
449 and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" |
478 and greatest_a: "greatest L a (Lower L A)" |
450 and greatest_a: "greatest L a (Lower L A)" |
479 from L greatest_a have La: "a \<in> carrier L" by simp |
451 from L greatest_a have La: "a \<in> carrier L" by simp |
480 from L inf_of_two_exists greatest_a |
452 from L inf_of_two_exists greatest_a |
481 obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast |
453 obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast |
482 show "P (THE g. greatest L g (Lower L (insert x A)))" |
454 show "P (THE g. greatest L g (Lower L (insert x A)))" |
483 proof (rule theI2 [where a = i]) |
455 proof (rule theI2) |
484 show "greatest L i (Lower L (insert x A))" |
456 show "greatest L i (Lower L (insert x A))" |
485 proof (rule greatest_LowerI) |
457 proof (rule greatest_LowerI) |
486 fix z |
458 fix z |
487 assume xA: "z \<in> insert x A" |
459 assume "z \<in> insert x A" |
488 show "i \<sqsubseteq> z" |
460 then show "i \<sqsubseteq> z" |
489 proof - |
461 proof |
490 { |
462 assume "z = x" then show ?thesis |
491 assume "z = x" then have ?thesis |
463 by (simp add: greatest_Lower_above [OF greatest_i] L La) |
492 by (simp add: greatest_Lower_above [OF greatest_i] L La) |
464 next |
493 } |
465 assume "z \<in> A" |
494 moreover |
466 with L greatest_i greatest_a show ?thesis |
495 { |
467 by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
496 assume "z \<in> A" |
468 qed |
497 with L greatest_i greatest_a have ?thesis |
469 next |
498 by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
470 fix y |
499 } |
471 assume y: "y \<in> Lower L (insert x A)" |
500 moreover note xA |
472 show "y \<sqsubseteq> i" |
501 ultimately show ?thesis by blast |
473 proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
474 fix z |
|
475 assume z: "z \<in> {a, x}" |
|
476 then show "y \<sqsubseteq> z" |
|
477 proof |
|
478 have y': "y \<in> Lower L A" |
|
479 apply (rule subsetD [where A = "Lower L (insert x A)"]) |
|
480 apply (rule Lower_antimono) apply clarify apply assumption |
|
481 done |
|
482 assume "z = a" |
|
483 with y' greatest_a show ?thesis by (fast dest: greatest_le) |
|
484 next |
|
485 assume "z \<in> {x}" |
|
486 with y L show ?thesis by blast |
|
487 qed |
|
488 qed (rule Lower_closed [THEN subsetD]) |
|
489 next |
|
490 from L show "insert x A \<subseteq> carrier L" by simp |
|
491 from greatest_i show "i \<in> carrier L" by simp |
502 qed |
492 qed |
503 next |
493 next |
504 fix y |
|
505 assume y: "y \<in> Lower L (insert x A)" |
|
506 show "y \<sqsubseteq> i" |
|
507 proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
|
508 fix z |
|
509 assume z: "z \<in> {a, x}" |
|
510 show "y \<sqsubseteq> z" |
|
511 proof - |
|
512 { |
|
513 have y': "y \<in> Lower L A" |
|
514 apply (rule subsetD [where A = "Lower L (insert x A)"]) |
|
515 apply (rule Lower_antimono) apply clarify apply assumption |
|
516 done |
|
517 assume "z = a" |
|
518 with y' greatest_a have ?thesis by (fast dest: greatest_le) |
|
519 } |
|
520 moreover |
|
521 { |
|
522 assume "z = x" |
|
523 with y L have ?thesis by blast |
|
524 } |
|
525 moreover note z |
|
526 ultimately show ?thesis by blast |
|
527 qed |
|
528 qed (rule Lower_closed [THEN subsetD]) |
|
529 next |
|
530 from L show "insert x A \<subseteq> carrier L" by simp |
|
531 next |
|
532 from greatest_i show "i \<in> carrier L" by simp |
|
533 qed |
|
534 next |
|
535 fix g |
494 fix g |
536 assume greatest_g: "greatest L g (Lower L (insert x A))" |
495 assume greatest_g: "greatest L g (Lower L (insert x A))" |
537 show "g = i" |
496 show "g = i" |
538 proof (rule greatest_unique) |
497 proof (rule greatest_unique) |
539 show "greatest L i (Lower L (insert x A))" |
498 show "greatest L i (Lower L (insert x A))" |
540 proof (rule greatest_LowerI) |
499 proof (rule greatest_LowerI) |
541 fix z |
500 fix z |
542 assume xA: "z \<in> insert x A" |
501 assume "z \<in> insert x A" |
543 show "i \<sqsubseteq> z" |
502 then show "i \<sqsubseteq> z" |
544 proof - |
503 proof |
545 { |
504 assume "z = x" then show ?thesis |
546 assume "z = x" then have ?thesis |
505 by (simp add: greatest_Lower_above [OF greatest_i] L La) |
547 by (simp add: greatest_Lower_above [OF greatest_i] L La) |
506 next |
548 } |
507 assume "z \<in> A" |
549 moreover |
508 with L greatest_i greatest_a show ?thesis |
550 { |
509 by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
551 assume "z \<in> A" |
510 qed |
552 with L greatest_i greatest_a have ?thesis |
|
553 by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) |
|
554 } |
|
555 moreover note xA |
|
556 ultimately show ?thesis by blast |
|
557 qed |
|
558 next |
511 next |
559 fix y |
512 fix y |
560 assume y: "y \<in> Lower L (insert x A)" |
513 assume y: "y \<in> Lower L (insert x A)" |
561 show "y \<sqsubseteq> i" |
514 show "y \<sqsubseteq> i" |
562 proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
515 proof (rule greatest_le [OF greatest_i], rule Lower_memI) |
563 fix z |
516 fix z |
564 assume z: "z \<in> {a, x}" |
517 assume z: "z \<in> {a, x}" |
565 show "y \<sqsubseteq> z" |
518 then show "y \<sqsubseteq> z" |
566 proof - |
519 proof |
567 { |
520 have y': "y \<in> Lower L A" |
568 have y': "y \<in> Lower L A" |
521 apply (rule subsetD [where A = "Lower L (insert x A)"]) |
569 apply (rule subsetD [where A = "Lower L (insert x A)"]) |
522 apply (rule Lower_antimono) apply clarify apply assumption |
570 apply (rule Lower_antimono) apply clarify apply assumption |
523 done |
571 done |
524 assume "z = a" |
572 assume "z = a" |
525 with y' greatest_a show ?thesis by (fast dest: greatest_le) |
573 with y' greatest_a have ?thesis by (fast dest: greatest_le) |
526 next |
574 } |
527 assume "z \<in> {x}" |
575 moreover |
528 with y L show ?thesis by blast |
576 { |
|
577 assume "z = x" |
|
578 with y L have ?thesis by blast |
|
579 } |
|
580 moreover note z |
|
581 ultimately show ?thesis by blast |
|
582 qed |
529 qed |
583 qed (rule Lower_closed [THEN subsetD]) |
530 qed (rule Lower_closed [THEN subsetD]) |
584 next |
531 next |
585 from L show "insert x A \<subseteq> carrier L" by simp |
532 from L show "insert x A \<subseteq> carrier L" by simp |
586 next |
533 from greatest_i show "i \<in> carrier L" by simp |
587 from greatest_i show "i \<in> carrier L" by simp |
|
588 qed |
534 qed |
589 qed |
535 qed |
590 qed |
536 qed |
591 qed |
537 qed |
592 |
538 |
593 lemma (in lattice) finite_inf_greatest: |
539 lemma (in lattice) finite_inf_greatest: |
594 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter> A) (Lower L A)" |
540 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)" |
595 proof (induct set: Finites) |
541 proof (induct set: Finites) |
596 case empty then show ?case by simp |
542 case empty then show ?case by simp |
597 next |
543 next |
598 case (insert A x) |
544 case (insert A x) |
599 show ?case |
545 show ?case |
602 with insert show ?thesis by (simp add: inf_of_singletonI) |
548 with insert show ?thesis by (simp add: inf_of_singletonI) |
603 next |
549 next |
604 case False |
550 case False |
605 from insert show ?thesis |
551 from insert show ?thesis |
606 proof (rule_tac inf_insertI) |
552 proof (rule_tac inf_insertI) |
607 from False insert show "greatest L (\<Sqinter> A) (Lower L A)" by simp |
553 from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp |
608 qed simp_all |
554 qed simp_all |
609 qed |
555 qed |
610 qed |
556 qed |
611 |
557 |
612 lemma (in lattice) finite_inf_insertI: |
558 lemma (in lattice) finite_inf_insertI: |
613 assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" |
559 assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" |
614 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
560 and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" |
615 shows "P (\<Sqinter> (insert x A))" |
561 shows "P (\<Sqinter> (insert x A))" |
616 proof (cases "A = {}") |
562 proof (cases "A = {}") |
617 case True with P and xA show ?thesis |
563 case True with P and xA show ?thesis |
618 by (simp add: inf_of_singletonI) |
564 by (simp add: inf_of_singletonI) |
619 next |
565 next |
620 case False with P and xA show ?thesis |
566 case False with P and xA show ?thesis |
621 by (simp add: inf_insertI finite_inf_greatest) |
567 by (simp add: inf_insertI finite_inf_greatest) |
622 qed |
568 qed |
623 |
569 |
624 lemma (in lattice) finite_inf_closed: |
570 lemma (in lattice) finite_inf_closed: |
625 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter> A \<in> carrier L" |
571 "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" |
626 proof (induct set: Finites) |
572 proof (induct set: Finites) |
627 case empty then show ?case by simp |
573 case empty then show ?case by simp |
628 next |
574 next |
629 case (insert A x) then show ?case |
575 case (insert A x) then show ?case |
630 by (rule_tac finite_inf_insertI) (simp_all) |
576 by (rule_tac finite_inf_insertI) (simp_all) |
631 qed |
577 qed |
632 |
578 |
633 lemma (in lattice) meet_left: |
579 lemma (in lattice) meet_left: |
634 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
580 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" |
635 by (rule meetI [folded meet_def]) (blast dest: greatest_mem ) |
581 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
636 |
582 |
637 lemma (in lattice) meet_right: |
583 lemma (in lattice) meet_right: |
638 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
584 "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" |
639 by (rule meetI [folded meet_def]) (blast dest: greatest_mem ) |
585 by (rule meetI [folded meet_def]) (blast dest: greatest_mem) |
640 |
586 |
641 lemma (in lattice) inf_of_two_greatest: |
587 lemma (in lattice) inf_of_two_greatest: |
642 "[| x \<in> carrier L; y \<in> carrier L |] ==> |
588 "[| x \<in> carrier L; y \<in> carrier L |] ==> |
643 greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" |
589 greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" |
644 proof (unfold inf_def) |
590 proof (unfold inf_def) |
645 assume L: "x \<in> carrier L" "y \<in> carrier L" |
591 assume L: "x \<in> carrier L" "y \<in> carrier L" |
646 with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
592 with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast |
647 with L |
593 with L |
648 show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" |
594 show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" |
649 by (fast intro: theI2 greatest_unique) (* blast fails *) |
595 by (fast intro: theI2 greatest_unique) (* blast fails *) |
650 qed |
596 qed |
651 |
597 |
652 lemma (in lattice) meet_le: |
598 lemma (in lattice) meet_le: |
653 assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
599 assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" |
654 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
600 and L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
655 shows "z \<sqsubseteq> x \<sqinter> y" |
601 shows "z \<sqsubseteq> x \<sqinter> y" |
656 proof (rule meetI) |
602 proof (rule meetI) |
657 fix i |
603 fix i |
658 assume "greatest L i (Lower L {x, y})" |
604 assume "greatest L i (Lower L {x, y})" |
659 with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
605 with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) |
660 qed |
606 qed |
661 |
607 |
662 lemma (in lattice) meet_assoc_lemma: |
608 lemma (in lattice) meet_assoc_lemma: |
663 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
609 assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" |
664 shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter> {x, y, z}" |
610 shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" |
665 proof (rule finite_inf_insertI) |
611 proof (rule finite_inf_insertI) |
666 txt {* The textbook argument in Jacobson I, p 457 *} |
612 txt {* The textbook argument in Jacobson I, p 457 *} |
667 fix i |
613 fix i |
668 assume inf: "greatest L i (Lower L {x, y, z})" |
614 assume inf: "greatest L i (Lower L {x, y, z})" |
669 show "x \<sqinter> (y \<sqinter> z) = i" |
615 show "x \<sqinter> (y \<sqinter> z) = i" |
705 shows "total_order L" |
652 shows "total_order L" |
706 proof (rule total_order.intro) |
653 proof (rule total_order.intro) |
707 show "lattice_axioms L" |
654 show "lattice_axioms L" |
708 proof (rule lattice_axioms.intro) |
655 proof (rule lattice_axioms.intro) |
709 fix x y |
656 fix x y |
710 assume L: "x \<in> carrier L" "y \<in> carrier L" |
657 assume L: "x \<in> carrier L" "y \<in> carrier L" |
711 show "EX s. least L s (Upper L {x, y})" |
658 show "EX s. least L s (Upper L {x, y})" |
712 proof - |
659 proof - |
713 note total L |
660 note total L |
714 moreover |
661 moreover |
715 { |
662 { |
716 assume "x \<sqsubseteq> y" |
663 assume "x \<sqsubseteq> y" |
717 with L have "least L y (Upper L {x, y})" |
664 with L have "least L y (Upper L {x, y})" |
718 by (rule_tac least_UpperI) auto |
665 by (rule_tac least_UpperI) auto |
719 } |
666 } |
720 moreover |
667 moreover |
721 { |
668 { |
722 assume "y \<sqsubseteq> x" |
669 assume "y \<sqsubseteq> x" |
723 with L have "least L x (Upper L {x, y})" |
670 with L have "least L x (Upper L {x, y})" |
724 by (rule_tac least_UpperI) auto |
671 by (rule_tac least_UpperI) auto |
725 } |
672 } |
726 ultimately show ?thesis by blast |
673 ultimately show ?thesis by blast |
727 qed |
674 qed |
728 next |
675 next |
729 fix x y |
676 fix x y |
730 assume L: "x \<in> carrier L" "y \<in> carrier L" |
677 assume L: "x \<in> carrier L" "y \<in> carrier L" |
731 show "EX i. greatest L i (Lower L {x, y})" |
678 show "EX i. greatest L i (Lower L {x, y})" |
732 proof - |
679 proof - |
733 note total L |
680 note total L |
734 moreover |
681 moreover |
735 { |
682 { |
736 assume "y \<sqsubseteq> x" |
683 assume "y \<sqsubseteq> x" |
737 with L have "greatest L y (Lower L {x, y})" |
684 with L have "greatest L y (Lower L {x, y})" |
738 by (rule_tac greatest_LowerI) auto |
685 by (rule_tac greatest_LowerI) auto |
739 } |
686 } |
740 moreover |
687 moreover |
741 { |
688 { |
742 assume "x \<sqsubseteq> y" |
689 assume "x \<sqsubseteq> y" |
743 with L have "greatest L x (Lower L {x, y})" |
690 with L have "greatest L x (Lower L {x, y})" |
744 by (rule_tac greatest_LowerI) auto |
691 by (rule_tac greatest_LowerI) auto |
745 } |
692 } |
746 ultimately show ?thesis by blast |
693 ultimately show ?thesis by blast |
747 qed |
694 qed |
748 qed |
695 qed |
749 qed (assumption | rule total_order_axioms.intro)+ |
696 qed (assumption | rule total_order_axioms.intro)+ |
|
697 |
750 |
698 |
751 subsection {* Complete lattices *} |
699 subsection {* Complete lattices *} |
752 |
700 |
753 locale complete_lattice = lattice + |
701 locale complete_lattice = lattice + |
754 assumes sup_exists: |
702 assumes sup_exists: |