[isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

I have investigated the possibility of replacing the existing 
complete_distrib_lattice with the stronger version.

Here are the problems:

1. The new class needs Hilbert choice in few places: proving the dual
of the distributivity property, proving the set and fun instantiations,
and proving that complete_linearord is subclass of the new class. I
think that the Hilbert choice cannot be avoided, as for example
Wikipedia page states that no nontrivial instance of this could exists
without the axiom of choice.

2. Hilbert_Choice comes very late in the library, and depends on the
Complete_Lattice.thy

One possible solution:

Add the new class in Complete_Lattice.thy, replacing the existing class

Prove the instantiations and the complete_linearord subclass later
in Hilbert_Choice.

Another possibility is to move everything related to complete
distributive lattice in a new theory that imports Hilbert_Choice,
but I don't know if the current distributivity properties are used
before Hilbert_Choice.

On the other hand, it seems inconvenient to have the Hilbert Choice
to depend on so many other theories.

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