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

2017-08-25 Thread 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

2017-08-25 Thread 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] some results about "lex"

2017-08-25 Thread Tobias Nipkow 

Dear Christian,

They are useful, I have added them (and slightly modified the names): 
http://isabelle.in.tum.de/repos/isabelle/rev/5df7a346f07b


Thanks
Tobias

On 25/08/2017 06:55, Christian Sternagel wrote:

Dear list,

maybe the following results about "lex" are worthwhile to add to the
library?

lemma lex_append_right:
   "(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r"
   by (force simp: lex_def lexn_conv)

lemma lex_append_left:
   "(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex r"
   by (induct xs) auto

lemma lex_take_index:
   assumes "(xs, ys) ∈ lex r"
   obtains i where "i < length xs" and "i < length ys" and "take i xs =
take i ys"
 and "(xs ! i, ys ! i) ∈ r"
proof -
   obtain n us x xs' y ys' where "(xs, ys) ∈ lexn r n" and "length xs =
n" and "length ys = n"
 and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) ∈ r"
 using assms by (fastforce simp: lex_def lexn_conv)
   then show ?thesis by (intro that [of "length us"]) auto
qed

cheers

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

2017-08-25 Thread Clemens Ballarin 

Dear Florian,


For the final record:


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


I had overlooked that \mu and \nu are global constants when importing 
this material, which I had received from Simon Foster.  This needs to be 
addressed properly.


Your workaround merely helps users of Group, not of Complete_Lattice.  
Moreover, it doesn't make sense that Complete_Lattice imports Group, and 
that the structure theorem about subgroups is now in lattice theory.


I request you revert this patch.

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

2017-08-25 Thread 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