Purely out of interest: Does this also hold for filters? Manuel
On 2017-08-24 20:54, Viorel Preoteasa wrote: > 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). > > 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? >>> Larry >>> >>>> On 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 > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev