`I managed to integrate the new complete distributive lattice into HOL`

`library.`

The changes are these:

## Advertising

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