[isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev