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

[Makarius]

This is a brief summary of the current situation:

* The current RC version is
http://isabelle.in.tum.de/website-Isabelle2017-RC3 and
http://isabelle.in.tum.de/website-Isabelle2017 is an alias for that.

* http://isabelle.in.tum.de/repos/isabelle/rev/ebb97a834338 is a
preliminary merge of the isabelle-release repository. I am myself
mentally back to isabelle-dev.

* The situation of afp-devel is still somewhat unclear to me. When will
the fork to afp-2017 happen?


Makarius

___
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

[Lars Hupel]

> My plan would be to fork the AFP 2017 release branch tomorrow (around 
> midnight CET from Mon to Tue).
> 
> There still seems to be quite a bit of ongoing activity - if there is 
> anything that needs to go into the afp-2017 release, please let me know.

One more thing that is of interest to users: the statistics page for
devel AFP is currently broken. I'm trying to fix this for the upcoming
2017 release.

Cheers
Lars
___
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

[Gerwin.Klein]

My plan would be to fork the AFP 2017 release branch tomorrow (around midnight 
CET from Mon to Tue).

There still seems to be quite a bit of ongoing activity - if there is anything 
that needs to go into the afp-2017 release, please let me know.

Cheers,
Gerwin



> On 9 Sep 2017, at 04:30, Makarius  wrote:
> 
> We are now past the fork point for the Isabelle2017 release.
> 
> Here is a summary of the status of the Isabelle development process:
> 
>* https://bitbucket.org/isabelle_project/isabelle-release/ is where
>  the final release preparations happen before roll-out in a few
>  weeks.
> 
>  The starting point is
> https://bitbucket.org/isabelle_project/isabelle-release/commits/bcea02893d17
> 
>* http://isabelle.in.tum.de/repos/isabelle is back in post-release
>  mode right now (changeset 435cb8d69e27).  Anything pushed there
>  is for the next release after Isabelle2017.
> 
>* AFP (presently at dfb6f8bc70e3) needs to be understood wrt.
>  isabelle-release at the moment. Gerwin will explain when and how
>  the fork of afp-devel vs. afp-2017 happens.
> 
>* http://isabelle.in.tum.de/devel with the automated testing and
>  snapshot service follows the isabelle-dev repository; I've
>  refrained from forking that as well to keep the long term test
>  results in a linear form.
> 
>* isabelle-users is the place to discuss Isabelle2017-RC versions.
> 
>* isabelle-dev is the place to discuss ongoing post-release
>  development.
> 
> 
> The isabelle-release repository has no public push access. Any changes
> that are relevant for the release need to be sent to me via email
> (produced by "hg export" or "hg bundle"). Changesets need to be
> prepared from a current state of isabelle-release, not the ongoing
> post-release development, and applied to only one of the two repository
> branches.
> 
> Changes to the actual code base should be limited to really important
> things.
> 
> During the forked state of the two repositories, big upheaveals on the
> isabelle-dev repository should be avoided, so that the isabelle-release
> branch can be merged back cleanly after some weeks; but it is
> better to publish changes now than to stockpile them for a long time.
> 
> 
>   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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Makarius]

We are now past the fork point for the Isabelle2017 release.

Here is a summary of the status of the Isabelle development process:

* https://bitbucket.org/isabelle_project/isabelle-release/ is where
  the final release preparations happen before roll-out in a few
  weeks.

  The starting point is
https://bitbucket.org/isabelle_project/isabelle-release/commits/bcea02893d17

* http://isabelle.in.tum.de/repos/isabelle is back in post-release
  mode right now (changeset 435cb8d69e27).  Anything pushed there
  is for the next release after Isabelle2017.

* AFP (presently at dfb6f8bc70e3) needs to be understood wrt.
  isabelle-release at the moment. Gerwin will explain when and how
  the fork of afp-devel vs. afp-2017 happens.

* http://isabelle.in.tum.de/devel with the automated testing and
  snapshot service follows the isabelle-dev repository; I've
  refrained from forking that as well to keep the long term test
  results in a linear form.

* isabelle-users is the place to discuss Isabelle2017-RC versions.

* isabelle-dev is the place to discuss ongoing post-release
  development.


The isabelle-release repository has no public push access. Any changes
that are relevant for the release need to be sent to me via email
(produced by "hg export" or "hg bundle"). Changesets need to be
prepared from a current state of isabelle-release, not the ongoing
post-release development, and applied to only one of the two repository
branches.

Changes to the actual code base should be limited to really important
things.

During the forked state of the two repositories, big upheaveals on the
isabelle-dev repository should be avoided, so that the isabelle-release
branch can be merged back cleanly after some weeks; but it is
better to publish changes now than to stockpile them for a long time.


Makarius

___
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

[Makarius]

On 08/09/17 11:13, Makarius wrote:

> The all-important release fork will happen today in the evening.

That is now!

Within the next hour there should not be any pushes to
http://isabelle.in.tum.de/repos/isabelle in order to avoid confusion
about the two branches.

I will come back a bit later with clear identification of both branches,
as well as an official Isabelle2017-RC2.


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

[Makarius]

On 03/09/17 12:06, Makarius wrote:
> 
> The isabelle-dev repository remains open for 3 more days. Afterwards it
> forks to https://bitbucket.org/isabelle_project/isabelle-release and
> further changes (really important ones!) need to be sent to me via email.

There were some delays, but we are now ready. The all-important release
fork will happen today in the evening.

This is the last chance for small amendments directly on the repository.
Afterwards any further changes (important ones) need to be sent to me
via email.


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

[Thiemann, Rene]

Dear Florian,

thanks for the explanation and the hint on style.

The below pattern works perfectly in our formalization.

Cheers,
René

> Am 31.08.2017 um 14:03 schrieb Florian Haftmann 
> :
> 
> Note that the pattern above is avoided nowadays by an interpretation
> with mixin definitions:
> 
> locale foo = fixes f :: "nat => nat"
>  assumes ...
> begin
> 
> fun bar :: "nat => nat” where ...
> 
> end
> 
> global_interpretation foo id
>  defines com = bar
>  by standard simp

___
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

[Makarius]

On 21/08/17 20:24, Makarius wrote:
> 
> 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.

That is today. I will publish Isabelle2017-RC1 within a few hours.

The isabelle-dev repository remains open for 3 more days. Afterwards it
forks to https://bitbucket.org/isabelle_project/isabelle-release and
further changes (really important ones!) need to be sent to me via email.


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

[Florian Haftmann]

Hi Rene,

> =
> locale foo = fixes f :: "nat => nat"
>   assumes f_mono[termination_simp]: "f x <= x"
> begin
> 
> fun bar :: "nat => nat" where
>   "bar 0 = 0"
> | "bar (Suc x) = Suc (bar (f x))"
> 
> end
> 
> definition com where
>   [code del]: "com = foo.bar id"
> 
> interpretation foo id
>   rewrites "foo.bar id = com"
>   unfolding com_def by (unfold_locales, auto)
> 
> lemma "com 5 = 5" by eval
> export_code com in Haskell
> =
> 
> 
> This works perfectly fine in Isabelle 2016-1, and especially
> the [code del] is required to make the final export_code and eval succeed.
> 
> In contrast, in a recent development version, the [code del] still is 
> accepted,
> but the export_code will deliver “com _ = error …” and the “eval” will fail.
> 
> The solution is easy: remove the previously required [code del].

this is due to subtle changes in the semantics of [code del] which now
merely removes a single equation from a list of concrete function
equations; strict removal of a function declaration is now done using
[[code drop: …]].

Note that the pattern above is avoided nowadays by an interpretation
with mixin definitions:

theory Bar
  imports Main
begin

locale foo = fixes f :: "nat => nat"
  assumes f_mono [termination_simp]: "f x ≤ x"
begin

fun bar :: "nat => nat" where
  "bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"

end

global_interpretation foo id
  defines com = bar
  by standard simp

lemma "com 5 = 5" by eval
export_code com in Haskell

end

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Makarius]

On 24/08/17 09:38, Thiemann, Rene wrote:
> 
> - Most changes have been caused by integrating session-qualified theory 
> imports.
>   This will also require a reform of the splitting of sessions, which 
> previously
>   was structured towards a fast build-process, but now should be structured 
> more 
>   towards logical structure (which is currently reflected in the 
> directory-structure).

Some notes on this.

 (1) Isabelle2017-RC0 does not yet have full qualification of all
library theories etc. but I have changed that shortly afterwards, so it
is already in newer snapshots from
http://isabelle.in.tum.de/devel/release_snapshot -- or you just wait a
few days for Isabelle2017-RC1.

 (2) Logical structure is indeed defined primarily by the overall
session layout, i.e. a theory T loaded into session S will get a name
S.T that remains valid once and for all. The theory file may reside in a
subdirectory of the session itself, but that does not contribute to its
official name.

 (3) It possible to refer to theories from other sessions without
creating a new name (actually the prefereed way), using a ROOT
specification like this:

  sessions "S"
  theories "S.T"

As a corollary it should be quite easy to assemble auxiliary session
images from already existing sessions (without using parent images).

 (4) Despite the important reform of session-qualified imports now, it
is still possible to use unqualified imports from parent images. That is
a concession to easy upgrades of existing project sources, although it
is up to the old name confusions. The "isabelle imports -U" tool
eliminates such unqualified imports already, and right after the
Isabelle2017 release the unqualified option will just disappear:
everything *must* be imported as qualified afterwards.


Makarius



___
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

[Makarius]

On 24/08/17 17:40, Florian Haftmann wrote:
> 
> Hence that change should be fine if someone is willing to undertake it
> before the RC stabilization phase.

We are already in stabilization phase for some weeks. There are a few
days left until Isabelle2017-RC1 (presumably on 03-Sep-2017) to make
small additions and do some fine tuning.

After the Isabelle2017-RC1 there will be the usual 4-6 weeks to sort out
genuine problems only, notably ones that have been newly introduced
since the last release.


Makarius



signature.asc
Description: OpenPGP digital signature
___
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

[Thiemann, Rene]

Dear Florian,

>> - There have been some changes w.r.t. code-generation which now lead
>>  to runtime exception in the generated code. For instance, now
>>  I get code like
>>  “f x = Code.abort …”
>>  whereas in 2016-1 there was a proper code like
>>  “f x = some ordinary right-hand side”
>>  We did not yet isolate the problem and will report later.
> 
> OK, I will dig into this after you have isolated it.  Might be well that
> this only occurs on certain theory merges.

The problem seems to be a change wrt. locale interpretations.

Consider the following code:

=
locale foo = fixes f :: "nat => nat"
  assumes f_mono[termination_simp]: "f x <= x"
begin

fun bar :: "nat => nat" where
  "bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"

end

definition com where
  [code del]: "com = foo.bar id"

interpretation foo id
  rewrites "foo.bar id = com"
  unfolding com_def by (unfold_locales, auto)

lemma "com 5 = 5" by eval
export_code com in Haskell
=


This works perfectly fine in Isabelle 2016-1, and especially
the [code del] is required to make the final export_code and eval succeed.

In contrast, in a recent development version, the [code del] still is accepted,
but the export_code will deliver “com _ = error …” and the “eval” will fail.

The solution is easy: remove the previously required [code del].

Cheers,
René


signature.asc
Description: Message signed with OpenPGP
___
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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

On 2017-08-24 23:25, Manuel Eberl wrote:

Purely out of interest: Does this also hold for filters?

Manuel


Do filters form a complete lattice? It seems that a filter of a lattice 
should be nonempty.
I think that this condition would prevent the set of filters to be a 
lattice.


If empty set is accepted as a filter, then one could have a complete lattice
of filters (filter will be closed to arbitrary intersections). But I 
don't know

if this complete lattice is distributive.

Viorel



On 2017-08-24 20:54, Viorel Preoteasa wrote:

I have now a file with the new class, and all necessary proofs
(both distributivity equalities, bool, set, fun interpretations,
proofs of the old distributivity properties).

I have also the proof that complete linear order is subclass of
the new complete distributive lattice class.

Are there any other subclasses of the current complete distributive
lattice class? This would be something that could cause problems.

Otherwise, the existing complete distrib lattice is subclass
of the one that I implemented, so it should not cause any problems.
All existing results in the current class can be reused without
modification.

My theory works now in Isabelle 2016-1, but I can try it in
Isabelle2017-RC0 also.

I can try to integrate it, but I don't know how to test it
to see if there are any problems with something else.

For reference, I attach the theory file with the new
class of complete distributive lattice.

Best regards,

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


___
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

[Florian Haftmann]

Am 24.08.2017 um 22:39 schrieb Manuel Eberl:
> On 2017-08-24 17:34, Florian Haftmann wrote:
>> I would still appreciate if someone would take the comment »Deviates
>> from the definition given in the library in number theory« as a starting
>> point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.
> 
> Oh actually I fixed that a few months ago. I even wrote on the mailing
> list back then, I think. Those definitions should now be equivalent.

This sound good.

> I didn't know there was a totient function in HOL-Algebra, otherwise I
> would have removed the duplicate back then.

I had a look at it; I think to reconcile it we would have to move
Totient.thy to Library/, otherwise there would be a dependency cycle.

Looks like something to be done not before the next release.

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

For the final record:

> \phi is the result of a simple typo accident
see http://isabelle.in.tum.de/repos/isabelle/rev/ba94aeb02fbc

> Concerning \mu and \nu, I am currently investigating whether an import
> swap could re-establish the situation known from Isabelle2016-1

see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Manuel Eberl]

On 2017-08-24 17:34, Florian Haftmann wrote:
> I would still appreciate if someone would take the comment »Deviates
> from the definition given in the library in number theory« as a starting
> point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.

Oh actually I fixed that a few months ago. I even wrote on the mailing
list back then, I think. Those definitions should now be equivalent.

I didn't know there was a totient function in HOL-Algebra, otherwise I
would have removed the duplicate back then.

(By the way, I have lots of additional material on the totient function
and related functions that will come to an AFP near you very soon)

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

[Manuel Eberl]

Purely out of interest: Does this also hold for filters?

Manuel


On 2017-08-24 20:54, Viorel Preoteasa wrote:
> I have now a file with the new class, and all necessary proofs
> (both distributivity equalities, bool, set, fun interpretations,
> proofs of the old distributivity properties).
> 
> I have also the proof that complete linear order is subclass of
> the new complete distributive lattice class.
> 
> Are there any other subclasses of the current complete distributive
> lattice class? This would be something that could cause problems.
> 
> Otherwise, the existing complete distrib lattice is subclass
> of the one that I implemented, so it should not cause any problems.
> All existing results in the current class can be reused without
> modification.
> 
> My theory works now in Isabelle 2016-1, but I can try it in
> Isabelle2017-RC0 also.
> 
> I can try to integrate it, but I don't know how to test it
> to see if there are any problems with something else.
> 
> For reference, I attach the theory file with the new
> class of complete distributive lattice.
> 
> Best regards,
> 
> 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
> 
___
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

[Florian Haftmann]

Hi Rene,

> - In the NEWS I read about freeing short constant names like the
>   “Renamed ii to imaginary_unit in order to free up ii as a variable”.
>   I definitely support this kind of change, but at the same time found
>   quite the opposite in HOL-Algebra:
>   If one imports HOL-Algebra.Multiplicative_Group (which we actually do
>   via some transitive import), then \mu (LFP), \nu (GFP) and 
>   \phi (Euler’s totient function) become constants.
>   This was a bit annoying.

thanks for pointing that out.

\phi is the result of a simple typo accident (cf.
http://isabelle.in.tum.de/repos/testboard/rev/6c818fc0c817).

I would still appreciate if someone would take the comment »Deviates
from the definition given in the library in number theory« as a starting
point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.

Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1
(http://isabelle.in.tum.de/repos/testboard/rev/0ad153ee9ece).

> - There have been some changes w.r.t. code-generation which now lead
>   to runtime exception in the generated code. For instance, now
>   I get code like
>   “f x = Code.abort …” 
>   whereas in 2016-1 there was a proper code like
>   “f x = some ordinary right-hand side” 
>   We did not yet isolate the problem and will report later.

OK, I will dig into this after you have isolated it.  Might be well that
this only occurs on certain theory merges.

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear all,

let me share my opinions after porting IsaFoR to yesterdays development version:

- In total the transition from our 2016-1 source went quite smooth 
  (~ 14 hours for whole of IsaFoR)

- Most changes have been caused by integrating session-qualified theory imports.
  This will also require a reform of the splitting of sessions, which previously
  was structured towards a fast build-process, but now should be structured 
more 
  towards logical structure (which is currently reflected in the 
directory-structure).

- In the NEWS I read about freeing short constant names like the
  “Renamed ii to imaginary_unit in order to free up ii as a variable”.
  I definitely support this kind of change, but at the same time found
  quite the opposite in HOL-Algebra:
  If one imports HOL-Algebra.Multiplicative_Group (which we actually do
  via some transitive import), then \mu (LFP), \nu (GFP) and 
  \phi (Euler’s totient function) become constants.
  This was a bit annoying.

- There have been some changes w.r.t. code-generation which now lead
  to runtime exception in the generated code. For instance, now
  I get code like
  “f x = Code.abort …” 
  whereas in 2016-1 there was a proper code like
  “f x = some ordinary right-hand side” 
  We did not yet isolate the problem and will report later.

Cheers,
René  


> Am 21.08.2017 um 20:24 schrieb Makarius :
> 
> 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

Re: [isabelle-dev] Towards the Isabelle2017 release

[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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

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