author  paulson <lp15@cam.ac.uk> 
Tue, 21 Apr 2015 17:19:00 +0100  
changeset 60141  833adf7db7d8 
parent 59667  651ea265d568 
child 60526  fad653acf58f 
permissions  rwrr 
41959  1 
(* Title: HOL/Number_Theory/Fib.thy 
2 
Author: Lawrence C. Paulson 

3 
Author: Jeremy Avigad 

31719  4 

5 
Defines the fibonacci function. 

6 

7 
The original "Fib" is due to Lawrence C. Paulson, and was adapted by 

8 
Jeremy Avigad. 

9 
*) 

10 

58889  11 
section {* Fib *} 
31719  12 

13 
theory Fib 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

14 
imports Main "../GCD" "../Binomial" 
31719  15 
begin 
16 

17 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

18 
subsection {* Fibonacci numbers *} 
31719  19 

54713  20 
fun fib :: "nat \<Rightarrow> nat" 
31719  21 
where 
54713  22 
fib0: "fib 0 = 0" 
23 
 fib1: "fib (Suc 0) = 1" 

24 
 fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n" 

31719  25 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

26 
subsection {* Basic Properties *} 
31719  27 

54713  28 
lemma fib_1 [simp]: "fib (1::nat) = 1" 
29 
by (metis One_nat_def fib1) 

31719  30 

54713  31 
lemma fib_2 [simp]: "fib (2::nat) = 1" 
32 
using fib.simps(3) [of 0] 

33 
by (simp add: numeral_2_eq_2) 

31719  34 

54713  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)) 

31719  37 

54713  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) 

31719  40 

54713  41 
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0" 
42 
by (induct n rule: fib.induct) (auto simp add: ) 

31719  43 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

44 
subsection {* A Few Elementary Results *} 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

45 

31719  46 
text {* 
47 
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is 

48 
much easier using integers, not natural numbers! 

49 
*} 

50 

54713  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) 

31719  53 

54713  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 

31719  58 

59 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

60 
subsection {* Law 6.111 of Concrete Mathematics *} 
31719  61 

54713  62 
lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))" 
63 
apply (induct n rule: fib.induct) 

31719  64 
apply auto 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
54713
diff
changeset

65 
apply (metis gcd_add1_nat add.commute) 
44872  66 
done 
31719  67 

54713  68 
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

69 
apply (simp add: gcd_commute_nat [of "fib m"]) 
54713  70 
apply (cases m) 
71 
apply (auto simp add: fib_add) 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

72 
apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute) 
44872  73 
done 
31719  74 

54713  75 
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> 
31719  76 
gcd (fib m) (fib (n  m)) = gcd (fib m) (fib n)" 
54713  77 
by (simp add: gcd_fib_add [symmetric, of _ "nm"]) 
31719  78 

54713  79 
lemma gcd_fib_mod: "0 < m \<Longrightarrow> 
31719  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") 

44872  86 
case True 
87 
then have "m \<le> n" by auto 

31719  88 
with pos_m have pos_n: "0 < n" by auto 
44872  89 
with pos_m `m < n` have diff: "n  m < n" by auto 
31719  90 
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n  m) mod m))" 
44872  91 
by (simp add: mod_if [of n]) (insert `m < n`, auto) 
92 
also have "\<dots> = gcd (fib m) (fib (n  m))" 

31719  93 
by (simp add: less.hyps diff pos_m) 
44872  94 
also have "\<dots> = gcd (fib m) (fib n)" 
54713  95 
by (simp add: gcd_fib_diff `m \<le> n`) 
31719  96 
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" . 
97 
next 

44872  98 
case False 
99 
then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" 

100 
by (cases "m = n") auto 

31719  101 
qed 
102 
qed 

103 

54713  104 
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" 
31719  105 
 {* Law 6.111 *} 
54713  106 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod) 
31719  107 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

108 
theorem fib_mult_eq_setsum_nat: 
31719  109 
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" 
54713  110 
by (induct n rule: nat.induct) (auto simp add: field_simps) 
31719  111 

60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

112 
subsection {* Fibonacci and Binomial Coefficients *} 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

113 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

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)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

115 
by (induct n) auto 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

116 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

117 
lemma setsum_choose_drop_zero: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

118 
"(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n  k) choose (k  1)) = (\<Sum>j = 0..n. (nj) choose j)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

119 
by (rule trans [OF setsum.cong setsum_drop_zero]) auto 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

120 

833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

121 
lemma ne_diagonal_fib: 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

122 
"(\<Sum>k = 0..n. (nk) choose k) = fib (Suc n)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

123 
proof (induct n rule: fib.induct) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

124 
case 1 show ?case by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

125 
next 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

126 
case 2 show ?case by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

127 
next 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

128 
case (3 n) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

129 
have "(\<Sum>k = 0..Suc n. Suc (Suc n)  k choose k) = 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

130 
(\<Sum>k = 0..Suc n. (Suc n  k choose k) + (if k=0 then 0 else (Suc n  k choose (k  1))))" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

131 
by (rule setsum.cong) (simp_all add: choose_reduce_nat) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

132 
also have "... = (\<Sum>k = 0..Suc n. Suc n  k choose k) + 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

133 
(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n  k choose (k  1)))" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

134 
by (simp add: setsum.distrib) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

135 
also have "... = (\<Sum>k = 0..Suc n. Suc n  k choose k) + 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

136 
(\<Sum>j = 0..n. n  j choose j)" 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

137 
by (metis setsum_choose_drop_zero) 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

138 
finally show ?case using 3 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

139 
by simp 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

140 
qed 
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

141 

31719  142 
end 
54713  143 