352 |
352 |
353 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" |
353 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" |
354 unfolding Inf_Sup by auto |
354 unfolding Inf_Sup by auto |
355 |
355 |
356 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
356 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
357 apply (rule antisym) |
357 by (auto intro: antisym Inf_greatest Inf_lower) |
358 apply (rule le_infI) |
|
359 apply (rule Inf_lower) |
|
360 apply simp |
|
361 apply (rule Inf_greatest) |
|
362 apply (rule Inf_lower) |
|
363 apply simp |
|
364 apply (rule Inf_greatest) |
|
365 apply (erule insertE) |
|
366 apply (rule le_infI1) |
|
367 apply simp |
|
368 apply (rule le_infI2) |
|
369 apply (erule Inf_lower) |
|
370 done |
|
371 |
358 |
372 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" |
359 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" |
373 apply (rule antisym) |
360 by (auto intro: antisym Sup_least Sup_upper) |
374 apply (rule Sup_least) |
|
375 apply (erule insertE) |
|
376 apply (rule le_supI1) |
|
377 apply simp |
|
378 apply (rule le_supI2) |
|
379 apply (erule Sup_upper) |
|
380 apply (rule le_supI) |
|
381 apply (rule Sup_upper) |
|
382 apply simp |
|
383 apply (rule Sup_least) |
|
384 apply (rule Sup_upper) |
|
385 apply simp |
|
386 done |
|
387 |
361 |
388 lemma Inf_singleton [simp]: |
362 lemma Inf_singleton [simp]: |
389 "\<Sqinter>{a} = a" |
363 "\<Sqinter>{a} = a" |
390 by (auto intro: antisym Inf_lower Inf_greatest) |
364 by (auto intro: antisym Inf_lower Inf_greatest) |
391 |
365 |