author | paulson <lp15@cam.ac.uk> |
Tue, 21 Apr 2015 17:19:00 +0100 | |
changeset 60141 | 833adf7db7d8 |
parent 59667 | 651ea265d568 |
child 60526 | fad653acf58f |
permissions | -rw-r--r-- |
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 _ "n-m"]) |
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. (n-j) 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. (n-k) 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 |