325 |
325 |
326 subsection {* Complete lattices *} |
326 subsection {* Complete lattices *} |
327 |
327 |
328 class complete_lattice = lattice + |
328 class complete_lattice = lattice + |
329 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) |
329 fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900) |
|
330 and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
330 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" |
331 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x" |
331 assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" |
332 and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A" |
332 begin |
333 assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" |
333 |
334 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" |
334 definition |
335 begin |
335 Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900) |
|
336 where |
|
337 "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}" |
|
338 |
336 |
339 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}" |
337 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}" |
340 unfolding Sup_def by (auto intro: Inf_greatest Inf_lower) |
338 by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least) |
341 |
339 |
342 lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A" |
340 lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}" |
343 by (auto simp: Sup_def intro: Inf_greatest) |
341 by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least) |
344 |
|
345 lemma Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<^loc>\<le> z) \<Longrightarrow> \<Squnion>A \<^loc>\<le> z" |
|
346 by (auto simp: Sup_def intro: Inf_lower) |
|
347 |
342 |
348 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" |
343 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}" |
349 unfolding Sup_def by auto |
344 unfolding Sup_Inf by auto |
350 |
345 |
351 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" |
346 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}" |
352 unfolding Inf_Sup by auto |
347 unfolding Inf_Sup by auto |
353 |
348 |
354 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
349 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A" |
365 apply simp |
360 apply simp |
366 apply (rule le_infI2) |
361 apply (rule le_infI2) |
367 apply (erule Inf_lower) |
362 apply (erule Inf_lower) |
368 done |
363 done |
369 |
364 |
370 lemma Sup_insert [code func]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" |
365 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A" |
371 apply (rule antisym) |
366 apply (rule antisym) |
372 apply (rule Sup_least) |
367 apply (rule Sup_least) |
373 apply (erule insertE) |
368 apply (erule insertE) |
374 apply (rule le_supI1) |
369 apply (rule le_supI1) |
375 apply simp |
370 apply simp |
385 |
380 |
386 lemma Inf_singleton [simp]: |
381 lemma Inf_singleton [simp]: |
387 "\<Sqinter>{a} = a" |
382 "\<Sqinter>{a} = a" |
388 by (auto intro: antisym Inf_lower Inf_greatest) |
383 by (auto intro: antisym Inf_lower Inf_greatest) |
389 |
384 |
390 lemma Sup_singleton [simp, code func]: |
385 lemma Sup_singleton [simp]: |
391 "\<Squnion>{a} = a" |
386 "\<Squnion>{a} = a" |
392 by (auto intro: antisym Sup_upper Sup_least) |
387 by (auto intro: antisym Sup_upper Sup_least) |
393 |
388 |
394 lemma Inf_insert_simp: |
389 lemma Inf_insert_simp: |
395 "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" |
390 "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)" |
489 sup_bool_eq: "sup P Q \<equiv> P \<or> Q" |
484 sup_bool_eq: "sup P Q \<equiv> P \<or> Q" |
490 by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) |
485 by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) |
491 |
486 |
492 instance bool :: complete_lattice |
487 instance bool :: complete_lattice |
493 Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x" |
488 Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x" |
494 apply intro_classes |
489 Sup_bool_def: "Sup A \<equiv> \<exists>x\<in>A. x" |
495 apply (unfold Inf_bool_def) |
490 by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def) |
496 apply (iprover intro!: le_boolI elim: ballE) |
|
497 apply (iprover intro!: ballI le_boolI elim: ballE le_boolE) |
|
498 done |
|
499 |
|
500 theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)" |
|
501 apply (rule order_antisym) |
|
502 apply (rule Sup_least) |
|
503 apply (rule le_boolI) |
|
504 apply (erule bexI, assumption) |
|
505 apply (rule le_boolI) |
|
506 apply (erule bexE) |
|
507 apply (rule le_boolE) |
|
508 apply (rule Sup_upper) |
|
509 apply assumption+ |
|
510 done |
|
511 |
491 |
512 lemma Inf_empty_bool [simp]: |
492 lemma Inf_empty_bool [simp]: |
513 "Inf {}" |
493 "Inf {}" |
514 unfolding Inf_bool_def by auto |
494 unfolding Inf_bool_def by auto |
515 |
495 |
516 lemma not_Sup_empty_bool [simp]: |
496 lemma not_Sup_empty_bool [simp]: |
517 "\<not> Sup {}" |
497 "\<not> Sup {}" |
518 unfolding Sup_def Inf_bool_def by auto |
498 unfolding Sup_bool_def by auto |
519 |
499 |
520 lemma top_bool_eq: "top = True" |
500 lemma top_bool_eq: "top = True" |
521 by (iprover intro!: order_antisym le_boolI top_greatest) |
501 by (iprover intro!: order_antisym le_boolI top_greatest) |
522 |
502 |
523 lemma bot_bool_eq: "bot = False" |
503 lemma bot_bool_eq: "bot = False" |
539 lemmas mono_Un = mono_sup |
519 lemmas mono_Un = mono_sup |
540 [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq] |
520 [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq] |
541 |
521 |
542 instance set :: (type) complete_lattice |
522 instance set :: (type) complete_lattice |
543 Inf_set_def: "Inf S \<equiv> \<Inter>S" |
523 Inf_set_def: "Inf S \<equiv> \<Inter>S" |
544 by intro_classes (auto simp add: Inf_set_def) |
524 Sup_set_def: "Sup S \<equiv> \<Union>S" |
545 |
525 by intro_classes (auto simp add: Inf_set_def Sup_set_def) |
546 lemmas [code func del] = Inf_set_def |
526 |
547 |
527 lemmas [code func del] = Inf_set_def Sup_set_def |
548 theorem Sup_set_eq: "Sup S = \<Union>S" |
|
549 apply (rule subset_antisym) |
|
550 apply (rule Sup_least) |
|
551 apply (erule Union_upper) |
|
552 apply (rule Union_least) |
|
553 apply (erule Sup_upper) |
|
554 done |
|
555 |
528 |
556 lemma top_set_eq: "top = UNIV" |
529 lemma top_set_eq: "top = UNIV" |
557 by (iprover intro!: subset_antisym subset_UNIV top_greatest) |
530 by (iprover intro!: subset_antisym subset_UNIV top_greatest) |
558 |
531 |
559 lemma bot_set_eq: "bot = {}" |
532 lemma bot_set_eq: "bot = {}" |
579 instance "fun" :: (type, distrib_lattice) distrib_lattice |
552 instance "fun" :: (type, distrib_lattice) distrib_lattice |
580 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
553 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
581 |
554 |
582 instance "fun" :: (type, complete_lattice) complete_lattice |
555 instance "fun" :: (type, complete_lattice) complete_lattice |
583 Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})" |
556 Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})" |
584 apply intro_classes |
557 Sup_fun_def: "Sup A \<equiv> (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})" |
585 apply (unfold Inf_fun_def) |
558 by intro_classes |
586 apply (rule le_funI) |
559 (auto simp add: Inf_fun_def Sup_fun_def le_fun_def |
587 apply (rule Inf_lower) |
560 intro: Inf_lower Sup_upper Inf_greatest Sup_least) |
588 apply (rule CollectI) |
561 |
589 apply (rule bexI) |
562 lemmas [code func del] = Inf_fun_def Sup_fun_def |
590 apply (rule refl) |
|
591 apply assumption |
|
592 apply (rule le_funI) |
|
593 apply (rule Inf_greatest) |
|
594 apply (erule CollectE) |
|
595 apply (erule bexE) |
|
596 apply (iprover elim: le_funE) |
|
597 done |
|
598 |
|
599 lemmas [code func del] = Inf_fun_def |
|
600 |
|
601 theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})" |
|
602 apply (rule order_antisym) |
|
603 apply (rule Sup_least) |
|
604 apply (rule le_funI) |
|
605 apply (rule Sup_upper) |
|
606 apply fast |
|
607 apply (rule le_funI) |
|
608 apply (rule Sup_least) |
|
609 apply (erule CollectE) |
|
610 apply (erule bexE) |
|
611 apply (drule le_funD [OF Sup_upper]) |
|
612 apply simp |
|
613 done |
|
614 |
563 |
615 lemma Inf_empty_fun: |
564 lemma Inf_empty_fun: |
616 "Inf {} = (\<lambda>_. Inf {})" |
565 "Inf {} = (\<lambda>_. Inf {})" |
617 by rule (auto simp add: Inf_fun_def) |
566 by rule (auto simp add: Inf_fun_def) |
618 |
567 |
619 lemma Sup_empty_fun: |
568 lemma Sup_empty_fun: |
620 "Sup {} = (\<lambda>_. Sup {})" |
569 "Sup {} = (\<lambda>_. Sup {})" |
621 proof - |
570 by rule (auto simp add: Sup_fun_def) |
622 have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto |
|
623 show ?thesis |
|
624 by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux) |
|
625 qed |
|
626 |
571 |
627 lemma top_fun_eq: "top = (\<lambda>x. top)" |
572 lemma top_fun_eq: "top = (\<lambda>x. top)" |
628 by (iprover intro!: order_antisym le_funI top_greatest) |
573 by (iprover intro!: order_antisym le_funI top_greatest) |
629 |
574 |
630 lemma bot_fun_eq: "bot = (\<lambda>x. bot)" |
575 lemma bot_fun_eq: "bot = (\<lambda>x. bot)" |