I managed to integrate the new complete distributive lattice into HOL library.

The changes are these:

 - replaced the complete_distrib_lattice with the new stronger version.
- moved some proofs about complete_distrib_lattice and some instantiations to Hilbert_Choice

 - added all results complete_distrib_lattice, including instantiations
of set, fun that uses uses Hilbert choice.

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

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


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 partly historical, but it’s worth noting how much of HOL can be developed without it.

isabelle-dev mailing list

Reply via email to