[isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

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.preoteasa at aalto.fi
>> <mailto:viorel.preoteasa at 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-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170824/fdd83d11/attachment.sig>