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

[Viorel Preoteasa]

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