I have now a file with the new class, and all necessary proofs (both distributivity equalities, bool, set, fun interpretations, proofs of the old distributivity properties).

## Advertising

I have also the proof that complete linear order is subclass of the new complete distributive lattice class. Are there any other subclasses of the current complete distributive lattice class? This would be something that could cause problems. Otherwise, the existing complete distrib lattice is subclass of the one that I implemented, so it should not cause any problems. All existing results in the current class can be reused without modification. My theory works now in Isabelle 2016-1, but I can try it in Isabelle2017-RC0 also. I can try to integrate it, but I don't know how to test it to see if there are any problems with something else. For reference, I attach the theory file with the new class of complete distributive lattice. Best regards, Viorel On 8/24/2017 6:40 PM, Florian Haftmann wrote:

As far as I remember, I introduced the complete_distrib_lattice class after realizing the a complete lattice whose binary operations are distributive is not necessarily a distributive complete lattice. Hence the specification of that type class has been contrieved without consulting literature. Hence that change should be fine if someone is willing to undertake it before the RC stabilization phase. Cheers, Florian Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:Sounds good to me. Can anybody think of an objection? LarryOn 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preote...@aalto.fi <mailto:viorel.preote...@aalto.fi>> wrote: Hello, I am not sure if this is the right place to post this message, but it is related to the upcoming release as I am prosing adding something to the Isabelle library. While working with complete distributive lattices, I noticed that the Isabelle class complete_distrib_lattice is weaker compared to what it seems to be regarded as a complete distributive lattice. As I needed the more general concept, I have developed it, and if Isabelle community finds it useful to be in the library, then I could provide the proofs or integrate it myself in the Complete_Lattice.thy The only axiom needed for complete distributive lattices is: Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})" and from this, the equality and its dual can be proved, as well as the existing axioms of complete_distrib_lattice and the instantiation to bool, set and fun. Best regards, Viorel On 2017-08-21 21:24, Makarius wrote:Dear Isabelle contributors, we are now definitely heading towards the Isabelle2017 release. The first official release candidate Isabelle2017-RC1 is anticipated for 2/3-Sep-2017, that is a bit less than 2 weeks from now. That is also the deadline for any significant additions. I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE in Isabelle/5c0a3f63057d, but it seems that many potential entries are still missing. Please provide entries in NEWS and CONTRIBUTORS for all relevant things you have done since the last release. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

theory Distributive imports Main begin section{*Complete Distributive Lattice*} notation bot ("\<bottom>") and top ("\<top>") and inf (infixl "\<sqinter>" 70) and sup (infixl "\<squnion>" 65) context complete_lattice begin lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)}) \<le> Inf (Sup ` A)" by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2 Sup_upper) end class complete_distributive_lattice = complete_lattice + assumes Inf_Sup_le: "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})" begin lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})" by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le) lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})" proof (rule antisym) show "SUPREMUM A Inf \<le> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup" apply (rule Sup_least, rule INF_greatest) using Inf_lower2 Sup_upper by auto next show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf" proof (simp add: Inf_Sup, rule_tac SUP_least, simp, safe) fix f assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y" from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z" by auto show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> SUPREMUM A Inf" proof (cases "\<exists> Z \<in> A . INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z") case True from this obtain Z where [simp]: "Z \<in> A" and A: "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z" by blast have B: "... \<le> SUPREMUM A Inf" by (simp add: SUP_upper) from A and B show ?thesis by (drule_tac order_trans, simp_all) next case False from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x" using Inf_greatest by blast define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x)" have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y" using X by (simp add: F_def, rule someI2_ex, auto) have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Y" using X by (simp add: F_def, rule someI2_ex, auto) from C and B obtain Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z" by blast from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z" by simp from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)" by (rule_tac INF_lower, blast) from this and W and Y show ?thesis by simp qed qed qed lemma dual_complete_distributive_lattice: "class.complete_distributive_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" apply (rule class.complete_distributive_lattice.intro) apply (fact dual_complete_lattice) by (simp add: class.complete_distributive_lattice_axioms_def Sup_Inf) lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)" proof (rule antisym) show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)" using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce) next have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Sup" by (rule INF_greatest, auto simp add: INF_lower) also have "... = a \<squnion> Inf B" by (cut_tac A = "{{a}, B}" in Sup_Inf, simp) finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B" by simp qed lemma inf_Sup: "a \<sqinter> Sup B = (SUP b:B. a \<sqinter> b)" proof (rule antisym) show " (SUP b:B. a \<sqinter> b) \<le> a \<sqinter> Sup B" by (metis SUP_least Sup_upper inf.orderI inf_idem inf_mono) next have "a \<sqinter> Sup B = SUPREMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Inf" by (cut_tac A = "{{a}, B}" in Inf_Sup, simp) also have "... \<le> (SUP b:B. a \<sqinter> b)" by (rule SUP_least, auto simp add: SUP_upper) finally show "a \<sqinter> Sup B \<le> (SUP b:B. a \<sqinter> b)" by simp qed subclass complete_distrib_lattice by (standard, rule sup_Inf, rule inf_Sup) end instantiation bool :: complete_distributive_lattice begin instance proof fix A :: "(bool set) set" show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" by (clarsimp, fastforce) qed end instantiation "set" :: (type) complete_distributive_lattice begin instance proof (standard, clarsimp) fix A :: "(('a set) set) set" fix x::'a define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y \<and> x \<in> X)))" assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X" have B: " (\<forall>xa \<in> F ` A. x \<in> xa)" by (safe, metis (no_types, lifting) A F_def someI_ex) have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))" by (rule_tac x = "F" in exI, metis (no_types, lifting) A F_def someI_ex) from B and this show "\<exists>xa. (\<exists>f. xa = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>xa. x \<in> xa)" by auto qed end context complete_distributive_lattice begin lemma INF_SUP: "(INF y. SUP x. ((P x y)::'a)) = (SUP x. INF y. P (x y) y)" proof (rule antisym) show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)" by (meson UNIV_I image_eqI INF_lower2 Sup_upper INF_greatest SUP_least) next have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B") proof (rule_tac INF_greatest, clarsimp) fix y have "?A \<le> (SUP x. P x y)" by (rule INF_lower, simp) also have "... \<le> Sup {uu. \<exists>x. uu = P x y}" by (simp add: full_SetCompr_eq) finally show "?A \<le> Sup {uu. \<exists>x. uu = P x y}" by simp qed also have "... \<le> (SUP x. INF y. P (x y) y)" proof (subst Inf_Sup, rule_tac SUP_least, clarsimp) fix f assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y" have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> (INF y. P ((\<lambda> y. SOME x . f ({P x y | x. True}) = P x y) y) y)" proof (rule INF_greatest, clarsimp) fix y have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}" by (rule_tac INF_lower, blast) also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y" using A by (rule_tac someI2_ex, auto) finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y" by simp qed also have "... \<le> (SUP x. INF y. P (x y) y)" by (rule SUP_upper, simp) finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> (SUP x. INF y. P (x y) y)" by simp qed finally show "(INF y. SUP x. P x y) \<le> (SUP x. INF y. P (x y) y)" by simp qed end instantiation "fun" :: (type, complete_distributive_lattice) complete_distributive_lattice begin instance proof (standard, simp add: le_fun_def, clarify) fix A::"('a \<Rightarrow> 'b) set set" fix x have "\<And> X . X \<in> A \<Longrightarrow> (INF xa:A. SUP f:xa. f x) \<le> (SUP f:X. f x)" by (rule_tac INF_lower, simp) also have "\<And> X . X \<in> A \<Longrightarrow> (SUP f:X. f x) \<le> Sup {f x |f. f \<in> X}" by (metis (mono_tags, lifting) SUP_least Sup_upper mem_Collect_eq) finally have "(INF xa:A. SUP f:xa. f x) \<le> Inf (Sup ` { {f x | f . f \<in> X} | X . X \<in> A})" by (rule_tac INF_greatest, blast) also have "... \<le> (SUP xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF f:xa. f x)" proof (unfold Inf_Sup, rule SUP_least, clarsimp) fix f assume A: "\<forall>Y. (\<exists>X. Y = {f x |f. f \<in> X} \<and> X \<in> A) \<longrightarrow> f Y \<in> Y" from this have [simp]: "\<And> xa . xa \<in> A \<Longrightarrow> (SOME g. g \<in> xa \<and> g x = f {h x |h. h \<in> xa}) x = f {h x |h. h \<in> xa}" apply (rule_tac Q = "\<lambda> F . F x = f {h x |h. h \<in> xa}" in someI2_ex) by (drule_tac x = "{g x | g . g \<in> xa}" in spec, auto) from A have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> (SOME g. g \<in> Y \<and> g x = f {h x |h. h \<in> Y}) \<in> Y" apply (rule_tac Q = "\<lambda> F . F \<in> Y" in someI2_ex) by (drule_tac x = "{g x | g . g \<in> Y}" in spec, auto) have "(INF x:{{f x |f. f \<in> X} |X. X \<in> A}. f x) \<le> (INF g:((\<lambda> Y . SOME g . g \<in> Y \<and> g x = f({h x | h . h \<in> Y})) `A). g x)" by (rule INF_greatest, clarsimp, rule INF_lower, blast) also have "... \<le> (SUP xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF f:xa. f x)" by (rule SUP_upper, clarsimp, rule_tac x = "((\<lambda> Y . SOME g . g \<in> Y \<and> g x = f({h x | h . h \<in> Y})))" in exI, simp) finally show "(INF x:{{f x |f. f \<in> X} |X. X \<in> A}. f x) \<le> (SUP xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF f:xa. f x)" by simp qed finally show "(INF xa:A. SUP f:xa. f x) \<le> (SUP xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF f:xa. f x)" by simp qed end context complete_linorder begin subclass complete_distributive_lattice proof (standard, rule ccontr) fix A assume "\<not> INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" using local.not_le by blast show "False" proof (cases "\<exists> z . INFIMUM A Sup > z \<and> z > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf") case True from this obtain z where A: "z < INFIMUM A Sup" and X: "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < z" by blast from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y" by (meson local.less_INF_D) from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . z < k" using local.less_Sup_iff by blast define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)" have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y" by (metis (no_types, lifting) F_def B someI_ex) have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y" apply (simp add: F_def) by (metis (mono_tags, lifting) B someI_ex) have "z \<le> Inf (F ` A)" by (simp add: D local.INF_greatest local.order.strict_implies_order) also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" apply (rule SUP_upper, safe) using E by blast finally have "z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" by simp from X and this show ?thesis using local.not_less by blast next case False from this have A: "\<And> z . INFIMUM A Sup \<le> z \<or> z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" using local.le_less_linear by blast from C have "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < Sup Y" by (meson local.less_INF_D) from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k" using local.less_Sup_iff by blast define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)" have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y" by (metis (no_types, lifting) F_def B someI_ex) have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y" apply (simp add: F_def) by (metis (mono_tags, lifting) B someI_ex) have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y" using D False local.leI by blast from this have "INFIMUM A Sup \<le> Inf (F ` A)" by (simp add: local.INF_greatest) also have "Inf (F ` A) \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" apply (rule SUP_upper, safe) using E by blast finally have "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" by simp from C and this show ?thesis using local.not_less by blast qed qed end end

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev