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

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

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

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

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-exLarry

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

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@in.tum.de

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

Last updated: Mar 04 2024 at 12:30 UTC