793 |
793 |
794 subclass complete_lattice |
794 subclass complete_lattice |
795 proof |
795 proof |
796 fix x A |
796 fix x A |
797 show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x" |
797 show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x" |
798 by (cut_tac A = A and a = x in Inf_finite_insert, simp add: insert_absorb inf.absorb_iff2) |
798 by (metis Set.set_insert abel_semigroup.commute local.Inf_finite_insert local.inf.abel_semigroup_axioms local.inf.left_idem local.inf.orderI) |
799 show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A" |
799 show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A" |
800 by (cut_tac A = A and a = x in Sup_finite_insert, simp add: insert_absorb sup.absorb_iff2) |
800 by (metis Set.set_insert insert_absorb2 local.Sup_finite_insert local.sup.absorb_iff2) |
801 next |
801 next |
802 fix A z |
802 fix A z |
803 show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A" |
803 have "\<Squnion> UNIV = z \<squnion> \<Squnion>UNIV" |
804 apply (cut_tac F = A and P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A" in finite_induct, simp_all add: Inf_finite_empty Inf_finite_insert) |
804 by (subst Sup_finite_insert [symmetric], simp add: insert_UNIV) |
805 by(cut_tac A = UNIV and a = z in Sup_finite_insert, simp add: insert_UNIV local.sup.absorb_iff2) |
805 from this have [simp]: "z \<le> \<Squnion>UNIV" |
806 |
806 using local.le_iff_sup by auto |
807 show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z" |
807 have "(\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A" |
808 apply (cut_tac F = A and P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" in finite_induct, simp_all add: Sup_finite_empty Sup_finite_insert) |
808 apply (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"]) |
809 by(cut_tac A = UNIV and a = z in Inf_finite_insert, simp add: insert_UNIV local.inf.absorb_iff2) |
809 by (simp_all add: Inf_finite_empty Inf_finite_insert) |
|
810 from this show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A" |
|
811 by simp |
|
812 |
|
813 have "\<Sqinter> UNIV = z \<sqinter> \<Sqinter>UNIV" |
|
814 by (subst Inf_finite_insert [symmetric], simp add: insert_UNIV) |
|
815 from this have [simp]: "\<Sqinter>UNIV \<le> z" |
|
816 by (simp add: local.inf.absorb_iff2) |
|
817 have "(\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" |
|
818 by (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" ], simp_all add: Sup_finite_empty Sup_finite_insert) |
|
819 from this show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z" |
|
820 by blast |
810 next |
821 next |
811 show "\<Sqinter>{} = \<top>" |
822 show "\<Sqinter>{} = \<top>" |
812 by (simp add: Inf_finite_empty top_finite_def) |
823 by (simp add: Inf_finite_empty top_finite_def) |
813 show " \<Squnion>{} = \<bottom>" |
824 show " \<Squnion>{} = \<bottom>" |
814 by (simp add: Sup_finite_empty bot_finite_def) |
825 by (simp add: Sup_finite_empty bot_finite_def) |
816 end |
827 end |
817 |
828 |
818 class finite_distrib_lattice = finite_lattice + distrib_lattice |
829 class finite_distrib_lattice = finite_lattice + distrib_lattice |
819 begin |
830 begin |
820 lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}" |
831 lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}" |
821 proof (cut_tac F = A and P = "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}" in finite_induct, simp_all) |
832 proof (rule finite_induct [of A "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"], simp_all) |
822 fix x::"'a" |
833 fix x::"'a" |
823 fix F |
834 fix F |
824 assume "x \<notin> F" |
835 assume "x \<notin> F" |
825 assume A: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}" |
836 assume [simp]: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}" |
826 |
|
827 have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}" |
837 have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}" |
828 by auto |
838 by blast |
829 |
|
830 have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F" |
839 have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F" |
831 by (simp add: inf_sup_distrib1) |
840 by (simp add: inf_sup_distrib1) |
832 also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}" |
841 also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}" |
833 by (simp add: A) |
842 by simp |
834 also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}" |
843 also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}" |
835 by (unfold Sup_insert[THEN sym], simp) |
844 by (unfold Sup_insert[THEN sym], simp) |
836 |
|
837 finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}" |
845 finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}" |
838 by simp |
846 by simp |
839 qed |
847 qed |
840 |
848 |
841 lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" |
849 lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" |
842 proof (cut_tac F = A and P = "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" in finite_induct, simp_all add: finite_UnionD) |
850 proof (rule finite_induct [of A "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"], simp_all add: finite_UnionD) |
843 fix x::"'a set" |
851 fix x::"'a set" |
844 fix F |
852 fix F |
845 assume "x \<notin> F" |
853 assume "x \<notin> F" |
846 have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f . (\<forall>Y\<in>F. f Y \<in> Y)}" |
854 have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f . (\<forall>Y\<in>F. f Y \<in> Y)}" |
847 by auto |
855 by auto |
848 have [simp]:" \<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> \<exists>fa. insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa x) (fa ` F) \<and> fa x \<in> x \<and> (\<forall>Y\<in>F. fa Y \<in> Y)" |
856 define fa where "fa = (\<lambda> (b::'a) f Y . (if Y = x then b else f Y))" |
849 apply (rule_tac x = "(\<lambda> Y . (if Y = x then b else f Y))" in exI) |
857 have "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa b f x) (fa b f ` F) \<and> fa b f x \<in> x \<and> (\<forall>Y\<in>F. fa b f Y \<in> Y)" |
850 by auto |
858 by (auto simp add: fa_def) |
851 have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> (\<Sqinter>x\<in>F. f x) \<sqinter> b \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf" |
859 from this have B: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> fa b f ` ({x} \<union> F) \<in> {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)}" |
852 apply (rule_tac i = "(\<lambda> Y . (if Y = x then b else f Y)) ` ({x} \<union> F)" in SUP_upper2, simp) |
860 by blast |
853 apply (subst inf_commute) |
861 have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x) \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf" |
854 by (simp add: INF_greatest Inf_lower inf.coboundedI2) |
862 using B apply (rule SUP_upper2, simp_all) |
|
863 by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def) |
855 |
864 |
856 assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf" |
865 assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf" |
857 |
866 |
858 from this have "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> \<Squnion>x \<sqinter> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf" |
867 from this have "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> \<Squnion>x \<sqinter> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf" |
859 apply simp |
868 apply simp |
864 also have "... = Sup {Sup {Inf (f ` F) \<sqinter> b | b . b \<in> x} |f . (\<forall>Y\<in>F. f Y \<in> Y)}" |
873 also have "... = Sup {Sup {Inf (f ` F) \<sqinter> b | b . b \<in> x} |f . (\<forall>Y\<in>F. f Y \<in> Y)}" |
865 apply (subst inf_commute) |
874 apply (subst inf_commute) |
866 by (simp add: finite_inf_Sup) |
875 by (simp add: finite_inf_Sup) |
867 |
876 |
868 also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf" |
877 also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf" |
869 by (rule Sup_least, clarsimp, rule Sup_least, clarsimp) |
878 apply (rule Sup_least, clarsimp)+ |
|
879 by (subst inf_commute, simp) |
870 |
880 |
871 finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf" |
881 finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf" |
872 by simp |
882 by simp |
873 qed |
883 qed |
874 |
884 |