src/HOL/Number_Theory/Fib.thy
 changeset 64267 b9a1486e79be parent 63167 0909deb8059b child 64317 029e6247210e
```     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Sun Oct 16 22:43:51 2016 +0200
1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Mon Oct 17 11:46:22 2016 +0200
1.3 @@ -100,18 +100,18 @@
1.4      \<comment> \<open>Law 6.111\<close>
1.5    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
1.6
1.7 -theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.8 +theorem fib_mult_eq_sum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.9    by (induct n rule: nat.induct) (auto simp add:  field_simps)
1.10
1.11
1.12  subsection \<open>Fibonacci and Binomial Coefficients\<close>
1.13
1.14 -lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
1.15 +lemma sum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
1.16    by (induct n) auto
1.17
1.18 -lemma setsum_choose_drop_zero:
1.19 +lemma sum_choose_drop_zero:
1.20      "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
1.21 -  by (rule trans [OF setsum.cong setsum_drop_zero]) auto
1.22 +  by (rule trans [OF sum.cong sum_drop_zero]) auto
1.23
1.24  lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
1.25  proof (induct n rule: fib.induct)
1.26 @@ -124,13 +124,13 @@
1.27    case (3 n)
1.28    have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
1.29          (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
1.30 -    by (rule setsum.cong) (simp_all add: choose_reduce_nat)
1.31 +    by (rule sum.cong) (simp_all add: choose_reduce_nat)
1.32    also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
1.33                     (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
1.34 -    by (simp add: setsum.distrib)
1.35 +    by (simp add: sum.distrib)
1.36    also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
1.37                     (\<Sum>j = 0..n. n - j choose j)"
1.38 -    by (metis setsum_choose_drop_zero)
1.39 +    by (metis sum_choose_drop_zero)
1.40    finally show ?case using 3
1.41      by simp
1.42  qed
```