[isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

On 2017-08-24 23:25, Manuel Eberl wrote:
> Purely out of interest: Does this also hold for filters?
>
> Manuel

Do filters form a complete lattice? It seems that a filter of a lattice 
should be nonempty.
I think that this condition would prevent the set of filters to be a 
lattice.

If empty set is accepted as a filter, then one could have a complete lattice
of filters (filter will be closed to arbitrary intersections). But I 
don't know
if this complete lattice is distributive.

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