412 apply (fact dual_complete_lattice) |
412 apply (fact dual_complete_lattice) |
413 apply (rule class.complete_distrib_lattice_axioms.intro) |
413 apply (rule class.complete_distrib_lattice_axioms.intro) |
414 apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf) |
414 apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf) |
415 done |
415 done |
416 |
416 |
417 subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice} |
417 subclass distrib_lattice proof |
418 and prove @{text inf_Sup} and @{text sup_Inf} from that? *} |
|
419 fix a b c |
418 fix a b c |
420 from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" . |
419 from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" . |
421 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert) |
420 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert) |
422 qed |
421 qed |
423 |
422 |
554 |
553 |
555 instantiation bool :: complete_lattice |
554 instantiation bool :: complete_lattice |
556 begin |
555 begin |
557 |
556 |
558 definition |
557 definition |
559 "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)" |
558 [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A" |
560 |
559 |
561 definition |
560 definition |
562 "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)" |
561 [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A" |
563 |
562 |
564 instance proof |
563 instance proof |
565 qed (auto simp add: Inf_bool_def Sup_bool_def) |
564 qed (auto intro: bool_induct) |
566 |
565 |
567 end |
566 end |
568 |
567 |
569 lemma INF_bool_eq [simp]: |
568 lemma INF_bool_eq [simp]: |
570 "INFI = Ball" |
569 "INFI = Ball" |
571 proof (rule ext)+ |
570 proof (rule ext)+ |
572 fix A :: "'a set" |
571 fix A :: "'a set" |
573 fix P :: "'a \<Rightarrow> bool" |
572 fix P :: "'a \<Rightarrow> bool" |
574 show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)" |
573 show "(\<Sqinter>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)" |
575 by (auto simp add: Ball_def INF_def Inf_bool_def) |
574 by (auto simp add: INF_def) |
576 qed |
575 qed |
577 |
576 |
578 lemma SUP_bool_eq [simp]: |
577 lemma SUP_bool_eq [simp]: |
579 "SUPR = Bex" |
578 "SUPR = Bex" |
580 proof (rule ext)+ |
579 proof (rule ext)+ |
581 fix A :: "'a set" |
580 fix A :: "'a set" |
582 fix P :: "'a \<Rightarrow> bool" |
581 fix P :: "'a \<Rightarrow> bool" |
583 show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)" |
582 show "(\<Squnion>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P x)" |
584 by (auto simp add: Bex_def SUP_def Sup_bool_def) |
583 by (auto simp add: SUP_def) |
585 qed |
584 qed |
586 |
585 |
587 instance bool :: complete_boolean_algebra proof |
586 instance bool :: complete_boolean_algebra proof |
588 qed (auto simp add: Inf_bool_def Sup_bool_def) |
587 qed (auto intro: bool_induct) |
589 |
588 |
590 instantiation "fun" :: (type, complete_lattice) complete_lattice |
589 instantiation "fun" :: (type, complete_lattice) complete_lattice |
591 begin |
590 begin |
592 |
591 |
593 definition |
592 definition |
636 proof (rule set_eqI) |
635 proof (rule set_eqI) |
637 fix x |
636 fix x |
638 have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)" |
637 have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)" |
639 by auto |
638 by auto |
640 then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}" |
639 then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}" |
641 by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def) |
640 by (simp add: Inf_fun_def) (simp add: mem_def) |
642 qed |
641 qed |
643 |
642 |
644 lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)" |
643 lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)" |
645 by (unfold Inter_eq) blast |
644 by (unfold Inter_eq) blast |
646 |
645 |
819 proof (rule set_eqI) |
818 proof (rule set_eqI) |
820 fix x |
819 fix x |
821 have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)" |
820 have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)" |
822 by auto |
821 by auto |
823 then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}" |
822 then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}" |
824 by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def) |
823 by (simp add: Sup_fun_def) (simp add: mem_def) |
825 qed |
824 qed |
826 |
825 |
827 lemma Union_iff [simp, no_atp]: |
826 lemma Union_iff [simp, no_atp]: |
828 "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)" |
827 "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)" |
829 by (unfold Union_eq) blast |
828 by (unfold Union_eq) blast |