Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proposal to replace "binomial_ring" in /HOL/Bi...

Email Gateway (Aug 22 2022 at 21:15):

From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Hello,

I propose to replace the theorem "binomial_ring"

theorem binomial_ring: "(a + b :: 'a::{comm_ring_1,power})^n =
(∑k≤n. (of_nat (n choose k)) * a^k * b^(n-k))"

in "/HOL/Binomial.thy" by the slightly more general

theorem binomial_semiring: "(a + b :: 'a::{comm_semiring_1})^n =
(∑k≤n. (of_nat (n choose k)) * a^k * b^(n-k))"

The proof I use is largely identical. I only replace the part

also have "… = a^(n + 1) + b^(n + 1) +
(∑k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) +
(∑k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))"
by (simp add: atMost_atLeast0 decomp2)

by

also have "… = b^(n + 1) +
(∑k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + (a^(n +
1) +
(∑k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)))"
using sum.nat_ivl_Suc' [of 1 n "λk. of_nat (n choose (k-1)) * a ^
k * b ^ (n + 1 - k)"]
by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0
sum.nat_ivl_Suc')

Is this mailing list the appropriate place to discuss work on the
standard library of Isabelle?

Thanks,
Christian

Email Gateway (Aug 23 2022 at 08:13):

From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
There is one sum.nat_ivl_Suc' too much. The last line should be

by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0)

Email Gateway (Aug 23 2022 at 08:15):

From: Tobias Nipkow <nipkow@in.tum.de>
Dear Christian Weinz,

Thanks for the generalization, I have incorporated it.

Tobias
smime.p7s

Last updated: Apr 26 2024 at 16:20 UTC