author | wenzelm |
Fri, 19 Jun 2015 23:40:46 +0200 | |
changeset 60527 | eb431a5651fe |
parent 60526 | fad653acf58f |
child 60688 | 01488b559910 |
permissions | -rw-r--r-- |
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 _ "n-m"]) |
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. (n-j) 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. (n-k) 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 |