Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Sum_of_powers

Email Gateway (Aug 15 2022 at 13:32):

From: Lawrence Paulson <lp15@cam.ac.uk>
I think that HOL/ex/Sum_of_Powers.thy should be moved to the AFP.

It is a significant result: that the sum of the K-th powers of the first N positive integers is a polynomial in N. Using Bernoulli numbers and Bernoulli polynomials. This should not be hidden away in HOL-ex

Larry

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Aug 15 2022 at 13:53):

From: Manuel Eberl <manuel@pruvisto.org>
It already is in the AFP:
https://www.isa-afp.org/theories/bernoulli/#Bernoulli

If I recall correctly, I took Lukas's theory from HOL-ex, added a lot of
my own stuff, and put it in the AFP (with his permission and with him as
a co-author).

As for why I did not delete the version in HOL-ex, I cannot remember –
perhaps because it still is a small and self-contained derivation of
that result.

Manuel

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Aug 15 2022 at 14:41):

From: Lawrence Paulson <lp15@cam.ac.uk>
I think it should be deleted. It’s confusing to have two copies of the same material, and I even wasted time trying to move the preliminaries out of there; perhaps they should be deleted as well.

Larry

Email Gateway (Aug 15 2022 at 14:51):

From: Manuel Eberl <manuel@pruvisto.org>
No objections in principle, but as always, deleting it may break
existing citations. We could leave it in and replace its content with
just a link to the AFP entry. Or just delete it and not care about
external references. I don't have any strong feelings about this –
perhaps Lukas will comment on this as well.

Manuel

Email Gateway (Aug 15 2022 at 16:04):

From: Tobias Nipkow <nipkow@in.tum.de>
On 15/08/2022 15:53, Manuel Eberl wrote:

It already is in the AFP: https://www.isa-afp.org/theories/bernoulli/#Bernoulli

If I recall correctly, I took Lukas's theory from HOL-ex, added a lot of my own
stuff, and put it in the AFP (with his permission and with him as a co-author).

As for why I did not delete the version in HOL-ex, I cannot remember – perhaps
because it still is a small and self-contained derivation of that result.

It doesn't look much more self-contained than
https://www.isa-afp.org/theories/bernoulli/#Bernoulli
Thus I am also in favour of deletiom. The NEWS entry can point to the AFP entry.

Tobias

Manuel

On 15/08/2022 15:31, Lawrence Paulson wrote:

I think that HOL/ex/Sum_of_Powers.thy should be moved to the AFP.

It is a significant result: that the sum of the K-th powers of the first N
positive integers is a polynomial in N. Using Bernoulli numbers and Bernoulli
polynomials. This should not be hidden away in HOL-ex

Larry

---

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

---

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s

Email Gateway (Aug 16 2022 at 06:29):

From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Manuel, Larry, please simply delete the duplicate version. I assume
Manuel kept it because the Top 100 theorems list might refer to that
statement in that theory, but if that reference breaks, we can and
should just fix that and not keep this duplicate.

Lukas

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Apr 25 2024 at 08:20 UTC