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 anythought of a new release.LarryOn 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preote...@aalto.fi<mailto:viorel.preote...@aalto.fi>> wrote:I managed to integrate the new complete distributive lattice into HOLlibrary.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 someinstantiations to Hilbert_ChoiceHilbert_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 ofcomplete_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.preote...@aalto.fi <mailto:viorel.preote...@aalto.fi><mailto:viorel.preote...@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 partlyhistorical, but it’s worth noting how much of HOL can be developedwithout it.Larry

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev