src/HOL/Number_Theory/Fib.thy
 author paulson Tue Apr 21 17:19:00 2015 +0100 (2015-04-21) changeset 60141 833adf7db7d8 parent 59667 651ea265d568 child 60526 fad653acf58f permissions -rw-r--r--
New material, mostly about limits. Consolidation.
1 (*  Title:      HOL/Number_Theory/Fib.thy
2     Author:     Lawrence C. Paulson
5 Defines the fibonacci function.
7 The original "Fib" is due to Lawrence C. Paulson, and was adapted by
9 *)
11 section {* Fib *}
13 theory Fib
14 imports Main "../GCD" "../Binomial"
15 begin
18 subsection {* Fibonacci numbers *}
20 fun fib :: "nat \<Rightarrow> nat"
21 where
22     fib0: "fib 0 = 0"
23   | fib1: "fib (Suc 0) = 1"
24   | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
26 subsection {* Basic Properties *}
28 lemma fib_1 [simp]: "fib (1::nat) = 1"
29   by (metis One_nat_def fib1)
31 lemma fib_2 [simp]: "fib (2::nat) = 1"
32   using fib.simps(3) [of 0]
35 lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
36   by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
38 lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
39   by (induct n rule: fib.induct) (auto simp add: field_simps)
41 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
42   by (induct n rule: fib.induct) (auto simp add: )
44 subsection {* A Few Elementary Results *}
46 text {*
47   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
48   much easier using integers, not natural numbers!
49 *}
51 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
52   by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
54 lemma fib_Cassini_nat:
55     "fib (Suc (Suc n)) * fib n =
56        (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
57 using fib_Cassini_int [of n] by auto
60 subsection {* Law 6.111 of Concrete Mathematics *}
62 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
63   apply (induct n rule: fib.induct)
64   apply auto
66   done
68 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
69   apply (simp add: gcd_commute_nat [of "fib m"])
70   apply (cases m)
72   apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
73   done
75 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
76     gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
79 lemma gcd_fib_mod: "0 < m \<Longrightarrow>
80     gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
81 proof (induct n rule: less_induct)
82   case (less n)
83   from less.prems have pos_m: "0 < m" .
84   show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
85   proof (cases "m < n")
86     case True
87     then have "m \<le> n" by auto
88     with pos_m have pos_n: "0 < n" by auto
89     with pos_m `m < n` have diff: "n - m < n" by auto
90     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
91       by (simp add: mod_if [of n]) (insert `m < n`, auto)
92     also have "\<dots> = gcd (fib m)  (fib (n - m))"
93       by (simp add: less.hyps diff pos_m)
94     also have "\<dots> = gcd (fib m) (fib n)"
95       by (simp add: gcd_fib_diff `m \<le> n`)
96     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
97   next
98     case False
99     then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
100       by (cases "m = n") auto
101   qed
102 qed
104 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
105     -- {* Law 6.111 *}
106   by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
108 theorem fib_mult_eq_setsum_nat:
109     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
110   by (induct n rule: nat.induct) (auto simp add:  field_simps)
112 subsection {* Fibonacci and Binomial Coefficients *}
114 lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
115   by (induct n) auto
117 lemma setsum_choose_drop_zero:
118     "(\<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)"
119   by (rule trans [OF setsum.cong setsum_drop_zero]) auto
121 lemma ne_diagonal_fib:
122    "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
123 proof (induct n rule: fib.induct)
124   case 1 show ?case by simp
125 next
126   case 2 show ?case by simp
127 next
128   case (3 n)
129   have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
130         (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
131     by (rule setsum.cong) (simp_all add: choose_reduce_nat)
132   also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
133                    (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"