Hi Viorel, it's probably easiest to send a patch containing your changes to this mailing list. (Alternatively, a copy of all the files you changed.) Some Isabelle committer can then push this to the testboard which will run the whole AFP.
Cheers Lars On 27 August 2017 16:59:44 CEST, Viorel Preoteasa <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>> 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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
