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 A
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 H
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
./D
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 Pre
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
./LatticePropertie
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
Hil
> 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
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 that