author  wenzelm 
Fri, 19 Jun 2015 23:40:46 +0200  
changeset 60527  eb431a5651fe 
parent 60526  fad653acf58f 
child 60688  01488b559910 
permissions  rwrr 
41959  1 
(* Title: HOL/Number_Theory/Fib.thy 
2 
Author: Lawrence C. Paulson 

3 
Author: Jeremy Avigad 

31719  4 
*) 
5 

60527  6 
section \<open>The fibonacci function\<close> 
31719  7 

8 
theory Fib 

60527  9 
imports Main GCD Binomial 
31719  10 
begin 
11 

12 

60526  13 
subsection \<open>Fibonacci numbers\<close> 
31719  14 

54713  15 
fun fib :: "nat \<Rightarrow> nat" 
31719  16 
where 
60527  17 
fib0: "fib 0 = 0" 
18 
 fib1: "fib (Suc 0) = 1" 

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

20 

31719  21 

60526  22 
subsection \<open>Basic Properties\<close> 
31719  23 

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

31719  26 

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

29 
by (simp add: numeral_2_eq_2) 

31719  30 

54713  31 
lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n" 
32 
by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3)) 

31719  33 

54713  34 
lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" 
35 
by (induct n rule: fib.induct) (auto simp add: field_simps) 

31719  36 

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

31719  39 

60527  40 

60526  41 
subsection \<open>A Few Elementary Results\<close> 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

42 

60526  43 
text \<open> 
31719  44 
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is 
45 
much easier using integers, not natural numbers! 

60526  46 
\<close> 
31719  47 

54713  48 
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n)  int((fib (Suc n))\<^sup>2) =  ((1)^n)" 
60527  49 
by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add) 
31719  50 

54713  51 
lemma fib_Cassini_nat: 
60527  52 
"fib (Suc (Suc n)) * fib n = 
53 
(if even n then (fib (Suc n))\<^sup>2  1 else (fib (Suc n))\<^sup>2 + 1)" 

54 
using fib_Cassini_int [of n] by auto 

31719  55 

56 

60526  57 
subsection \<open>Law 6.111 of Concrete Mathematics\<close> 
31719  58 

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

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

62 
apply (metis gcd_add1_nat add.commute) 
44872  63 
done 
31719  64 

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

66 
apply (simp add: gcd_commute_nat [of "fib m"]) 
54713  67 
apply (cases m) 
68 
apply (auto simp add: fib_add) 

60527  69 
apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat 
70 
gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute) 

44872  71 
done 
31719  72 

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

60527  76 
lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" 
31719  77 
proof (induct n rule: less_induct) 
78 
case (less n) 

79 
show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" 

80 
proof (cases "m < n") 

44872  81 
case True 
82 
then have "m \<le> n" by auto 

60527  83 
with \<open>0 < m\<close> have pos_n: "0 < n" by auto 
84 
with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n  m < n" by auto 

31719  85 
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n  m) mod m))" 
60526  86 
by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto) 
44872  87 
also have "\<dots> = gcd (fib m) (fib (n  m))" 
60527  88 
by (simp add: less.hyps diff \<open>0 < m\<close>) 
44872  89 
also have "\<dots> = gcd (fib m) (fib n)" 
60526  90 
by (simp add: gcd_fib_diff \<open>m \<le> n\<close>) 
31719  91 
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" . 
92 
next 

44872  93 
case False 
94 
then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" 

95 
by (cases "m = n") auto 

31719  96 
qed 
97 
qed 

98 

54713  99 
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" 
60526  100 
 \<open>Law 6.111\<close> 
54713  101 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod) 
31719  102 

60527  103 
theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" 
54713  104 
by (induct n rule: nat.induct) (auto simp add: field_simps) 
31719  105 

60527  106 

60526  107 
subsection \<open>Fibonacci and Binomial Coefficients\<close> 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

108 

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

109 
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

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

111 

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

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

113 
"(\<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

114 
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

115 

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

117 
proof (induct n rule: fib.induct) 
60527  118 
case 1 
119 
show ?case by simp 

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

120 
next 
60527  121 
case 2 
122 
show ?case by simp 

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

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

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

125 
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

126 
(\<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

127 
by (rule setsum.cong) (simp_all add: choose_reduce_nat) 
60527  128 
also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n  k choose k) + 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

129 
(\<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

130 
by (simp add: setsum.distrib) 
60527  131 
also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n  k choose k) + 
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

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

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

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

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

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

137 

31719  138 
end 
54713  139 