src/HOL/Number_Theory/Fib.thy
changeset 60141 833adf7db7d8
parent 59667 651ea265d568
child 60526 fad653acf58f
     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.39 -text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
    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.47    apply (auto simp add: fib_add)
    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