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

[Viorel Preoteasa]

I have been very busy, but I will find time to work on it.

Viorel


On 11/23/2017 6:46 PM, Lawrence Paulson wrote:
> Whatever happened with this? The new release has been out for a while, 
> and it would make sense to integrate your work now, well before any 
> thought of a new release.
> Larry
>
>> On 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preoteasa at aalto.fi 
>> <mailto:viorel.preoteasa at aalto.fi>> wrote:
>>
>> I managed to integrate the new complete distributive lattice into HOL 
>> library.
>>
>> The changes are these:
>>
>> Complete_Lattice.thy
>> - replaced the complete_distrib_lattice with the new stronger version.
>> - moved some proofs about complete_distrib_lattice and some 
>> instantiations to Hilbert_Choice
>>
>> Hilbert_Choice.thy
>> - added all results complete_distrib_lattice, including instantiations
>> of set, fun that uses uses Hilbert choice.
>>
>> Enum.thy
>> - new proofs that finite_3 and finite_4 are complete_distrib_lattice.
>> - I added here the classes finite_lattice and finite_distrib_lattice
>> and proved that they are complete. This simplified quite much the proofs
>> that finite_3 and finite_4 are complete_distrib_lattice.
>>
>> Predicate.thy
>> - new proof that predicates are complete_distrib_lattice.
>>
>> I compiled HOL in Isabelle2017-RC0 using
>>
>> isabelle build -v -c HOL
>>
>> and I got:
>>
>> Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 
>> 43.344s GC time, factor 1.83)
>> Finished HOL (0:04:26 elapsed time)
>>
>> Finished at Sun Aug 27 17:41:30 GMT+3 2017
>> 0:04:37 elapsed time
>>
>> But I don't now how to go from here to have these changes into Isabelle.
>>
>> There is also AFP. If there are instantiations of 
>> complete_distrib_lattice, then most probably they will fail.
>>
>> One simple solution in this case could be to keep also the
>> old complete_distrib_lattice as complete_pseudo_distrib_lattice.
>>
>> Viorel
>>
>>
>> On 8/26/2017 3:06 PM, Lawrence Paulson wrote:
>>>> On 25 Aug 2017, at 20:14, Viorel Preoteasa 
>>>> <viorel.preoteasa at aalto.fi <mailto:viorel.preoteasa at aalto.fi> 
>>>> <mailto:viorel.preoteasa at aalto.fi>> wrote:
>>>>
>>>> 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.
>>>>
>>>> On the other hand, it seems inconvenient to have the Hilbert Choice
>>>> to depend on so many other theories.
>>> I’d prefer this provided the instantiations aren’t needed earlier.
>>> The delay in the introduction of the Axiom of Choice is partly 
>>> historical, but it’s worth noting how much of HOL can be developed 
>>> without it.
>>> Larry
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171124/ccde4618/attachment-0002.html>