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