`I have investigated the possibility of replacing the existing`

`complete_distrib_lattice with the stronger version.`

Here are the problems:

## Advertising

1. The new class needs Hilbert choice in few places: proving the dual of the distributivity property, proving the set and fun instantiations, and proving that complete_linearord is subclass of the new class. I think that the Hilbert choice cannot be avoided, as for example Wikipedia page states that no nontrivial instance of this could exists without the axiom of choice. 2. Hilbert_Choice comes very late in the library, and depends on the Complete_Lattice.thy One possible solution: Add the new class in Complete_Lattice.thy, replacing the existing class Prove the instantiations and the complete_linearord subclass later in Hilbert_Choice. Another possibility is to move everything related to complete distributive lattice in a new theory that imports Hilbert_Choice, but I don't know if the current distributivity properties are used before Hilbert_Choice. On the other hand, it seems inconvenient to have the Hilbert Choice to depend on so many other theories. 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

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