[isabelle-dev] Towards the Isabelle2017 release

[Manuel Eberl]

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