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

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

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

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

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

On 8/27/2017 6:11 PM, Lawrence Paulson wrote: In the AFP, grep picks up these: ~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r . ./Coinductive/Examples/CCPO_Topology.thy ./Concurrent_Ref_Alg/Refinement_Lattice.thy ./DataRefinementIBP/Diagram.thy ./DataRefinementIBP/Hoare.thy

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

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

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

In the AFP, grep picks up these: ~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r . ./Coinductive/Examples/CCPO_Topology.thy ./Concurrent_Ref_Alg/Refinement_Lattice.thy ./DataRefinementIBP/Diagram.thy ./DataRefinementIBP/Hoare.thy ./DataRefinementIBP/Statements.thy

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

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

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

> 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

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

I have investigated the possibility of replacing the existing complete_distrib_lattice with the stronger version. Here are the problems: 1. The new class needs Hilbert choice in few places: proving the dual of the distributivity property, proving the set and fun instantiations, and proving