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

[Viorel Preoteasa]

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 > 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] Towards the Isabelle2017 release - Complete Distributive Lattice

[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] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

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
./DataRefinementIBP/Statements.thy
./LatticeProperties/Conj_Disj.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy
./PSemigroupsConvolution/Quantales.thy

But why would they fail? The new version is surely stronger, so any 
changes should be pretty straightforward, right?




They will fail only if there are instantiations of the new class, since 
it is stronger. I will check these files. I discovered some files also

src/HOL/Library that need to be updated.

Some of the AFP files from this list are from my submissions.

Viorel


Larry

On 27 Aug 2017, at 15:59, Viorel Preoteasa > wrote:


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.




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

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

[Lars Hupel]

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  
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

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
./LatticeProperties/Conj_Disj.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy
./PSemigroupsConvolution/Quantales.thy

But why would they fail? The new version is surely stronger, so any changes 
should be pretty straightforward, right? 

Larry

> On 27 Aug 2017, at 15:59, Viorel Preoteasa  wrote:
> 
> 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.
> 

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

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

[Viorel Preoteasa]

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] Towards the Isabelle2017 release - Complete Distributive Lattice

[Lawrence Paulson]

> 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] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

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 complete_linearord is subclass of the new class. I
think that the Hilbert choice cannot be avoided, as for example
Wikipedia page states that no nontrivial instance of this could exists
without the axiom of choice.

2. Hilbert_Choice comes very late in the library, and depends on the
Complete_Lattice.thy

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.

Another possibility is to move everything related to complete
distributive lattice in a new theory that imports Hilbert_Choice,
but I don't know if the current distributivity properties are used
before Hilbert_Choice.

On the other hand, it seems inconvenient to have the Hilbert Choice
to depend on so many other theories.

Viorel

On 8/24/2017 6:40 PM, Florian Haftmann wrote:

As far as I remember, I introduced the complete_distrib_lattice class
after realizing the a complete lattice whose binary operations are
distributive is not necessarily a distributive complete lattice.  Hence
the specification of that type class has been contrieved without
consulting literature.

Hence that change should be fine if someone is willing to undertake it
before the RC stabilization phase.

Cheers,
Florian

Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:

Sounds good to me. Can anybody think of an objection?
Larry


On 23 Aug 2017, at 15:17, Viorel Preoteasa > wrote:

Hello,

I am not sure if this is the right place to post this message, but it is
related to  the upcoming release as I am prosing adding something
to the Isabelle library.

While working with complete distributive lattices, I noticed that
the Isabelle class complete_distrib_lattice is weaker compared to
what it seems to be regarded as a complete distributive lattice.

As I needed the more general concept, I have developed it,
and if Isabelle community finds it useful to be in the library,
then I could provide the proofs or integrate it myself in the
Complete_Lattice.thy

The only axiom needed for complete distributive lattices is:

Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈
Y)})"

and from this, the equality and its dual can be proved, as well as
the existing axioms of complete_distrib_lattice and the instantiation
to bool, set and fun.

Best regards,

Viorel


On 2017-08-21 21:24, Makarius wrote:

Dear Isabelle contributors,

we are now definitely heading towards the Isabelle2017 release.

The first official release candidate Isabelle2017-RC1 is anticipated for
2/3-Sep-2017, that is a bit less than 2 weeks from now.

That is also the deadline for any significant additions.


I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
in Isabelle/5c0a3f63057d, but it seems that many potential entries are
still missing.

Please provide entries in NEWS and CONTRIBUTORS for all relevant things
you have done since the last release.


Makarius
___
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




___
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