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

[Lars Hupel]

Hi Viorel,

it's probably easiest to send a patch containing your changes to this mailing list. (Alternatively, a copy of all the files you changed.) Some Isabelle committer can then push this to the testboard which will run the whole AFP.

Cheers
Lars

On 27 August 2017 16:59:44 CEST, Viorel Preoteasa <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>> 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
>_______________________________________________
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170827/952918e1/attachment-0002.html>