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 any
thought of a new release.
Larry
On 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 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.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 partly
historical, but it’s worth noting how much of HOL can be developed
without it.
Larry
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
