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

2017-11-23 Thread Lawrence Paulson
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  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 >> > 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


Re: [isabelle-dev] Slow builds due to excessive heap images

2017-11-23 Thread Florian Haftmann
> They are just identifiers and I don't think they are computed with.
> However, I don't intend to change formalization beyond a global
> implementation of int by some fixed size integers, if that can be done
> easily. Otherwise we live with the increase in runtime from 7:20 to 8:20.

Hence a suitable theory would follow Code_Numeral and provide
code_printing declarations to map integer to a fixed-width
overflow-guarding implementation.

But I am also not sure whether this is worth the effort.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev