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
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
