author nipkow Tue, 07 Jan 2020 07:03:18 +0100 changeset 71351 b3a93a91803b parent 71350 cd0b0717c4e4 child 71352 41f3ca717da5
generalized thm (as suggested by Christian Weinz)
 src/HOL/Binomial.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Binomial.thy	Tue Jan 07 06:43:09 2020 +0100
+++ b/src/HOL/Binomial.thy	Tue Jan 07 07:03:18 2020 +0100
@@ -155,7 +155,7 @@
subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>

text \<open>Avigad's version, generalized to any commutative ring\<close>
-theorem binomial_ring: "(a + b :: 'a::{comm_ring_1,power})^n =
+theorem binomial_ring: "(a + b :: 'a::comm_semiring_1)^n =
(\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
proof (induct n)
case 0
@@ -177,10 +177,11 @@
also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
(\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))"
by (simp add: atMost_atLeast0 sum.shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum.cl_ivl_Suc)
-  also have "\<dots> = a^(n + 1) + b^(n + 1) +
-      (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) +
-      (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))"
-    by (simp add: atMost_atLeast0 decomp2)
+  also have "\<dots> = b^(n + 1) +
+      (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k)) + (a^(n + 1) +
+      (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)))"
+      using sum.nat_ivl_Suc' [of 1 n "\<lambda>k. of_nat (n choose (k-1)) * a ^ k * b ^ (n + 1 - k)"]
+    by (simp add: sum.atLeast_Suc_atMost atMost_atLeast0)
also have "\<dots> = a^(n + 1) + b^(n + 1) +
(\<Sum>k=1..n. of_nat (n + 1 choose k) * a^k * b^(n + 1 - k))"
by (auto simp add: field_simps sum.distrib [symmetric] choose_reduce_nat)```