1 (* Title: Fib.thy |
|
2 Authors: Lawrence C. Paulson, Jeremy Avigad |
|
3 |
|
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 |
|
11 |
|
12 header {* Fib *} |
|
13 |
|
14 theory Fib |
|
15 imports Binomial |
|
16 begin |
|
17 |
|
18 |
|
19 subsection {* Main definitions *} |
|
20 |
|
21 class fib = |
|
22 |
|
23 fixes |
|
24 fib :: "'a \<Rightarrow> 'a" |
|
25 |
|
26 |
|
27 (* definition for the natural numbers *) |
|
28 |
|
29 instantiation nat :: fib |
|
30 |
|
31 begin |
|
32 |
|
33 fun |
|
34 fib_nat :: "nat \<Rightarrow> nat" |
|
35 where |
|
36 "fib_nat n = |
|
37 (if n = 0 then 0 else |
|
38 (if n = 1 then 1 else |
|
39 fib (n - 1) + fib (n - 2)))" |
|
40 |
|
41 instance proof qed |
|
42 |
|
43 end |
|
44 |
|
45 (* definition for the integers *) |
|
46 |
|
47 instantiation int :: fib |
|
48 |
|
49 begin |
|
50 |
|
51 definition |
|
52 fib_int :: "int \<Rightarrow> int" |
|
53 where |
|
54 "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)" |
|
55 |
|
56 instance proof qed |
|
57 |
|
58 end |
|
59 |
|
60 |
|
61 subsection {* Set up Transfer *} |
|
62 |
|
63 |
|
64 lemma transfer_nat_int_fib: |
|
65 "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)" |
|
66 unfolding fib_int_def by auto |
|
67 |
|
68 lemma transfer_nat_int_fib_closure: |
|
69 "n >= (0::int) \<Longrightarrow> fib n >= 0" |
|
70 by (auto simp add: fib_int_def) |
|
71 |
|
72 declare TransferMorphism_nat_int[transfer add return: |
|
73 transfer_nat_int_fib transfer_nat_int_fib_closure] |
|
74 |
|
75 lemma transfer_int_nat_fib: |
|
76 "fib (int n) = int (fib n)" |
|
77 unfolding fib_int_def by auto |
|
78 |
|
79 lemma transfer_int_nat_fib_closure: |
|
80 "is_nat n \<Longrightarrow> fib n >= 0" |
|
81 unfolding fib_int_def by auto |
|
82 |
|
83 declare TransferMorphism_int_nat[transfer add return: |
|
84 transfer_int_nat_fib transfer_int_nat_fib_closure] |
|
85 |
|
86 |
|
87 subsection {* Fibonacci numbers *} |
|
88 |
|
89 lemma fib_0_nat [simp]: "fib (0::nat) = 0" |
|
90 by simp |
|
91 |
|
92 lemma fib_0_int [simp]: "fib (0::int) = 0" |
|
93 unfolding fib_int_def by simp |
|
94 |
|
95 lemma fib_1_nat [simp]: "fib (1::nat) = 1" |
|
96 by simp |
|
97 |
|
98 lemma fib_Suc_0_nat [simp]: "fib (Suc 0) = Suc 0" |
|
99 by simp |
|
100 |
|
101 lemma fib_1_int [simp]: "fib (1::int) = 1" |
|
102 unfolding fib_int_def by simp |
|
103 |
|
104 lemma fib_reduce_nat: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)" |
|
105 by simp |
|
106 |
|
107 declare fib_nat.simps [simp del] |
|
108 |
|
109 lemma fib_reduce_int: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)" |
|
110 unfolding fib_int_def |
|
111 by (auto simp add: fib_reduce_nat nat_diff_distrib) |
|
112 |
|
113 lemma fib_neg_int [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0" |
|
114 unfolding fib_int_def by auto |
|
115 |
|
116 lemma fib_2_nat [simp]: "fib (2::nat) = 1" |
|
117 by (subst fib_reduce_nat, auto) |
|
118 |
|
119 lemma fib_2_int [simp]: "fib (2::int) = 1" |
|
120 by (subst fib_reduce_int, auto) |
|
121 |
|
122 lemma fib_plus_2_nat: "fib ((n::nat) + 2) = fib (n + 1) + fib n" |
|
123 by (subst fib_reduce_nat, auto simp add: One_nat_def) |
|
124 (* the need for One_nat_def is due to the natdiff_cancel_numerals |
|
125 procedure *) |
|
126 |
|
127 lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow> |
|
128 (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n" |
|
129 apply (atomize, induct n rule: nat_less_induct) |
|
130 apply auto |
|
131 apply (case_tac "n = 0", force) |
|
132 apply (case_tac "n = 1", force) |
|
133 apply (subgoal_tac "n >= 2") |
|
134 apply (frule_tac x = "n - 1" in spec) |
|
135 apply (drule_tac x = "n - 2" in spec) |
|
136 apply (drule_tac x = "n - 2" in spec) |
|
137 apply auto |
|
138 apply (auto simp add: One_nat_def) (* again, natdiff_cancel *) |
|
139 done |
|
140 |
|
141 lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) + |
|
142 fib k * fib n" |
|
143 apply (induct n rule: fib_induct_nat) |
|
144 apply auto |
|
145 apply (subst fib_reduce_nat) |
|
146 apply (auto simp add: ring_simps) |
|
147 apply (subst (1 3 5) fib_reduce_nat) |
|
148 apply (auto simp add: ring_simps Suc_eq_plus1) |
|
149 (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *) |
|
150 apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))") |
|
151 apply (erule ssubst) back back |
|
152 apply (erule ssubst) back |
|
153 apply auto |
|
154 done |
|
155 |
|
156 lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) + |
|
157 fib k * fib n" |
|
158 using fib_add_nat by (auto simp add: One_nat_def) |
|
159 |
|
160 |
|
161 (* transfer from nats to ints *) |
|
162 lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> |
|
163 fib (n + k + 1) = fib (k + 1) * fib (n + 1) + |
|
164 fib k * fib n " |
|
165 |
|
166 by (rule fib_add_nat [transferred]) |
|
167 |
|
168 lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0" |
|
169 apply (induct n rule: fib_induct_nat) |
|
170 apply (auto simp add: fib_plus_2_nat) |
|
171 done |
|
172 |
|
173 lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0" |
|
174 by (frule fib_neq_0_nat, simp) |
|
175 |
|
176 lemma fib_gr_0_int: "(n::int) > 0 \<Longrightarrow> fib n > 0" |
|
177 unfolding fib_int_def by (simp add: fib_gr_0_nat) |
|
178 |
|
179 text {* |
|
180 \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is |
|
181 much easier using integers, not natural numbers! |
|
182 *} |
|
183 |
|
184 lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) - |
|
185 (fib (int n + 1))^2 = (-1)^(n + 1)" |
|
186 apply (induct n) |
|
187 apply (auto simp add: ring_simps power2_eq_square fib_reduce_int |
|
188 power_add) |
|
189 done |
|
190 |
|
191 lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n - |
|
192 (fib (n + 1))^2 = (-1)^(nat n + 1)" |
|
193 by (insert fib_Cassini_aux_int [of "nat n"], auto) |
|
194 |
|
195 (* |
|
196 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n = |
|
197 (fib (n + 1))^2 + (-1)^(nat n + 1)" |
|
198 by (frule fib_Cassini_int, simp) |
|
199 *) |
|
200 |
|
201 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n = |
|
202 (if even n then tsub ((fib (n + 1))^2) 1 |
|
203 else (fib (n + 1))^2 + 1)" |
|
204 apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even) |
|
205 apply (subst tsub_eq) |
|
206 apply (insert fib_gr_0_int [of "n + 1"], force) |
|
207 apply auto |
|
208 done |
|
209 |
|
210 lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n = |
|
211 (if even n then (fib (n + 1))^2 - 1 |
|
212 else (fib (n + 1))^2 + 1)" |
|
213 |
|
214 by (rule fib_Cassini'_int [transferred, of n], auto) |
|
215 |
|
216 |
|
217 text {* \medskip Toward Law 6.111 of Concrete Mathematics *} |
|
218 |
|
219 lemma coprime_fib_plus_1_nat: "coprime (fib (n::nat)) (fib (n + 1))" |
|
220 apply (induct n rule: fib_induct_nat) |
|
221 apply auto |
|
222 apply (subst (2) fib_reduce_nat) |
|
223 apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *) |
|
224 apply (subst add_commute, auto) |
|
225 apply (subst gcd_commute_nat, auto simp add: ring_simps) |
|
226 done |
|
227 |
|
228 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))" |
|
229 using coprime_fib_plus_1_nat by (simp add: One_nat_def) |
|
230 |
|
231 lemma coprime_fib_plus_1_int: |
|
232 "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))" |
|
233 by (erule coprime_fib_plus_1_nat [transferred]) |
|
234 |
|
235 lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)" |
|
236 apply (simp add: gcd_commute_nat [of "fib m"]) |
|
237 apply (rule cases_nat [of _ m]) |
|
238 apply simp |
|
239 apply (subst add_assoc [symmetric]) |
|
240 apply (simp add: fib_add_nat) |
|
241 apply (subst gcd_commute_nat) |
|
242 apply (subst mult_commute) |
|
243 apply (subst gcd_add_mult_nat) |
|
244 apply (subst gcd_commute_nat) |
|
245 apply (rule gcd_mult_cancel_nat) |
|
246 apply (rule coprime_fib_plus_1_nat) |
|
247 done |
|
248 |
|
249 lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> |
|
250 gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)" |
|
251 by (erule gcd_fib_add_nat [transferred]) |
|
252 |
|
253 lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow> |
|
254 gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
|
255 by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"]) |
|
256 |
|
257 lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow> |
|
258 gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
|
259 by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"]) |
|
260 |
|
261 lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow> |
|
262 gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
|
263 proof (induct n rule: less_induct) |
|
264 case (less n) |
|
265 from less.prems have pos_m: "0 < m" . |
|
266 show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
|
267 proof (cases "m < n") |
|
268 case True note m_n = True |
|
269 then have m_n': "m \<le> n" by auto |
|
270 with pos_m have pos_n: "0 < n" by auto |
|
271 with pos_m m_n have diff: "n - m < n" by auto |
|
272 have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))" |
|
273 by (simp add: mod_if [of n]) (insert m_n, auto) |
|
274 also have "\<dots> = gcd (fib m) (fib (n - m))" |
|
275 by (simp add: less.hyps diff pos_m) |
|
276 also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n') |
|
277 finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" . |
|
278 next |
|
279 case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
|
280 by (cases "m = n") auto |
|
281 qed |
|
282 qed |
|
283 |
|
284 lemma gcd_fib_mod_int: |
|
285 assumes "0 < (m::int)" and "0 <= n" |
|
286 shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
|
287 |
|
288 apply (rule gcd_fib_mod_nat [transferred]) |
|
289 using prems apply auto |
|
290 done |
|
291 |
|
292 lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)" |
|
293 -- {* Law 6.111 *} |
|
294 apply (induct m n rule: gcd_nat_induct) |
|
295 apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat) |
|
296 done |
|
297 |
|
298 lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> |
|
299 fib (gcd (m::int) n) = gcd (fib m) (fib n)" |
|
300 by (erule fib_gcd_nat [transferred]) |
|
301 |
|
302 lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}" |
|
303 by auto |
|
304 |
|
305 theorem fib_mult_eq_setsum_nat: |
|
306 "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
|
307 apply (induct n) |
|
308 apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps) |
|
309 done |
|
310 |
|
311 theorem fib_mult_eq_setsum'_nat: |
|
312 "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
|
313 using fib_mult_eq_setsum_nat by (simp add: One_nat_def) |
|
314 |
|
315 theorem fib_mult_eq_setsum_int [rule_format]: |
|
316 "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)" |
|
317 by (erule fib_mult_eq_setsum_nat [transferred]) |
|
318 |
|
319 end |
|