src/HOL/Number_Theory/Fib.thy
```     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 20 13:46:36 2015 +0100
1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Tue Apr 21 17:19:00 2015 +0100
1.3 @@ -11,11 +11,11 @@
1.4  section {* Fib *}
1.5
1.6  theory Fib
1.7 -imports Main "../GCD"
1.8 +imports Main "../GCD" "../Binomial"
1.9  begin
1.10
1.11
1.12 -subsection {* Main definitions *}
1.13 +subsection {* Fibonacci numbers *}
1.14
1.15  fun fib :: "nat \<Rightarrow> nat"
1.16  where
1.17 @@ -23,7 +23,7 @@
1.18    | fib1: "fib (Suc 0) = 1"
1.19    | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
1.20
1.21 -subsection {* Fibonacci numbers *}
1.22 +subsection {* Basic Properties *}
1.23
1.24  lemma fib_1 [simp]: "fib (1::nat) = 1"
1.25    by (metis One_nat_def fib1)
1.26 @@ -41,6 +41,8 @@
1.27  lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
1.28    by (induct n rule: fib.induct) (auto simp add: )
1.29
1.30 +subsection {* A Few Elementary Results *}
1.31 +
1.32  text {*
1.33    \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
1.34    much easier using integers, not natural numbers!
1.35 @@ -55,7 +57,7 @@
1.36  using fib_Cassini_int [of n] by auto
1.37
1.38
1.40 +subsection {* Law 6.111 of Concrete Mathematics *}
1.41
1.42  lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
1.43    apply (induct n rule: fib.induct)
1.44 @@ -67,9 +69,7 @@
1.45    apply (simp add: gcd_commute_nat [of "fib m"])
1.46    apply (cases m)
1.48 -  apply (subst gcd_commute_nat)
1.49 -  apply (subst mult.commute)
1.50 -  apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
1.51 +  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
1.52    done
1.53
1.54  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
1.55 @@ -109,5 +109,35 @@
1.56      "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.57    by (induct n rule: nat.induct) (auto simp add:  field_simps)
1.58
1.59 +subsection {* Fibonacci and Binomial Coefficients *}
1.60 +
1.61 +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.62 +  by (induct n) auto
1.63 +
1.64 +lemma setsum_choose_drop_zero:
1.65 +    "(\<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.66 +  by (rule trans [OF setsum.cong setsum_drop_zero]) auto
1.67 +
1.68 +lemma ne_diagonal_fib:
1.69 +   "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
1.70 +proof (induct n rule: fib.induct)
1.71 +  case 1 show ?case by simp
1.72 +next
1.73 +  case 2 show ?case by simp
1.74 +next
1.75 +  case (3 n)
1.76 +  have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
1.77 +        (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
1.78 +    by (rule setsum.cong) (simp_all add: choose_reduce_nat)
1.79 +  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
1.80 +                   (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
1.81 +    by (simp add: setsum.distrib)
1.82 +  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
1.83 +                   (\<Sum>j = 0..n. n - j choose j)"
1.84 +    by (metis setsum_choose_drop_zero)
1.85 +  finally show ?case using 3
1.86 +    by simp
1.87 +qed
1.88 +
1.89  end
1.90
```