31719
|
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 nat_fib_0 [simp]: "fib (0::nat) = 0"
|
|
90 |
by simp
|
|
91 |
|
|
92 |
lemma int_fib_0 [simp]: "fib (0::int) = 0"
|
|
93 |
unfolding fib_int_def by simp
|
|
94 |
|
|
95 |
lemma nat_fib_1 [simp]: "fib (1::nat) = 1"
|
|
96 |
by simp
|
|
97 |
|
|
98 |
lemma nat_fib_Suc_0 [simp]: "fib (Suc 0) = Suc 0"
|
|
99 |
by simp
|
|
100 |
|
|
101 |
lemma int_fib_1 [simp]: "fib (1::int) = 1"
|
|
102 |
unfolding fib_int_def by simp
|
|
103 |
|
|
104 |
lemma nat_fib_reduce: "(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 int_fib_reduce: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
|
|
110 |
unfolding fib_int_def
|
|
111 |
by (auto simp add: nat_fib_reduce nat_diff_distrib)
|
|
112 |
|
|
113 |
lemma int_fib_neg [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
|
|
114 |
unfolding fib_int_def by auto
|
|
115 |
|
|
116 |
lemma nat_fib_2 [simp]: "fib (2::nat) = 1"
|
|
117 |
by (subst nat_fib_reduce, auto)
|
|
118 |
|
|
119 |
lemma int_fib_2 [simp]: "fib (2::int) = 1"
|
|
120 |
by (subst int_fib_reduce, auto)
|
|
121 |
|
|
122 |
lemma nat_fib_plus_2: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
|
|
123 |
by (subst nat_fib_reduce, 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 nat_fib_induct: "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 nat_fib_add: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
|
|
142 |
fib k * fib n"
|
|
143 |
apply (induct n rule: nat_fib_induct)
|
|
144 |
apply auto
|
|
145 |
apply (subst nat_fib_reduce)
|
|
146 |
apply (auto simp add: ring_simps)
|
|
147 |
apply (subst (1 3 5) nat_fib_reduce)
|
|
148 |
apply (auto simp add: ring_simps Suc_remove)
|
|
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 nat_fib_add': "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
|
|
157 |
fib k * fib n"
|
|
158 |
using nat_fib_add by (auto simp add: One_nat_def)
|
|
159 |
|
|
160 |
|
|
161 |
(* transfer from nats to ints *)
|
|
162 |
lemma int_fib_add [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 nat_fib_add [transferred])
|
|
167 |
|
|
168 |
lemma nat_fib_neq_0: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
|
|
169 |
apply (induct n rule: nat_fib_induct)
|
|
170 |
apply (auto simp add: nat_fib_plus_2)
|
|
171 |
done
|
|
172 |
|
|
173 |
lemma nat_fib_gr_0: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
|
|
174 |
by (frule nat_fib_neq_0, simp)
|
|
175 |
|
|
176 |
lemma int_fib_gr_0: "(n::int) > 0 \<Longrightarrow> fib n > 0"
|
|
177 |
unfolding fib_int_def by (simp add: nat_fib_gr_0)
|
|
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 int_fib_Cassini_aux: "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 int_fib_reduce
|
|
188 |
power_add)
|
|
189 |
done
|
|
190 |
|
|
191 |
lemma int_fib_Cassini: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
|
|
192 |
(fib (n + 1))^2 = (-1)^(nat n + 1)"
|
|
193 |
by (insert int_fib_Cassini_aux [of "nat n"], auto)
|
|
194 |
|
|
195 |
(*
|
|
196 |
lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
|
|
197 |
(fib (n + 1))^2 + (-1)^(nat n + 1)"
|
|
198 |
by (frule int_fib_Cassini, simp)
|
|
199 |
*)
|
|
200 |
|
|
201 |
lemma int_fib_Cassini': "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 int_fib_Cassini, auto simp add: pos_int_even_equiv_nat_even)
|
|
205 |
apply (subst tsub_eq)
|
|
206 |
apply (insert int_fib_gr_0 [of "n + 1"], force)
|
|
207 |
apply auto
|
|
208 |
done
|
|
209 |
|
|
210 |
lemma nat_fib_Cassini: "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 int_fib_Cassini' [transferred, of n], auto)
|
|
215 |
|
|
216 |
|
|
217 |
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
|
|
218 |
|
|
219 |
lemma nat_coprime_fib_plus_1: "coprime (fib (n::nat)) (fib (n + 1))"
|
|
220 |
apply (induct n rule: nat_fib_induct)
|
|
221 |
apply auto
|
|
222 |
apply (subst (2) nat_fib_reduce)
|
|
223 |
apply (auto simp add: Suc_remove) (* again, natdiff_cancel *)
|
|
224 |
apply (subst add_commute, auto)
|
|
225 |
apply (subst nat_gcd_commute, auto simp add: ring_simps)
|
|
226 |
done
|
|
227 |
|
|
228 |
lemma nat_coprime_fib_Suc: "coprime (fib n) (fib (Suc n))"
|
|
229 |
using nat_coprime_fib_plus_1 by (simp add: One_nat_def)
|
|
230 |
|
|
231 |
lemma int_coprime_fib_plus_1:
|
|
232 |
"n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
|
|
233 |
by (erule nat_coprime_fib_plus_1 [transferred])
|
|
234 |
|
|
235 |
lemma nat_gcd_fib_add: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
|
|
236 |
apply (simp add: nat_gcd_commute [of "fib m"])
|
|
237 |
apply (rule nat_cases [of _ m])
|
|
238 |
apply simp
|
|
239 |
apply (subst add_assoc [symmetric])
|
|
240 |
apply (simp add: nat_fib_add)
|
|
241 |
apply (subst nat_gcd_commute)
|
|
242 |
apply (subst mult_commute)
|
|
243 |
apply (subst nat_gcd_add_mult)
|
|
244 |
apply (subst nat_gcd_commute)
|
|
245 |
apply (rule nat_gcd_mult_cancel)
|
|
246 |
apply (rule nat_coprime_fib_plus_1)
|
|
247 |
done
|
|
248 |
|
|
249 |
lemma int_gcd_fib_add [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
|
|
250 |
gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
|
|
251 |
by (erule nat_gcd_fib_add [transferred])
|
|
252 |
|
|
253 |
lemma nat_gcd_fib_diff: "(m::nat) \<le> n \<Longrightarrow>
|
|
254 |
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
|
|
255 |
by (simp add: nat_gcd_fib_add [symmetric, of _ "n-m"])
|
|
256 |
|
|
257 |
lemma int_gcd_fib_diff: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
|
|
258 |
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
|
|
259 |
by (simp add: int_gcd_fib_add [symmetric, of _ "n-m"])
|
|
260 |
|
|
261 |
lemma nat_gcd_fib_mod: "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: nat_gcd_fib_diff 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 int_gcd_fib_mod:
|
|
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 nat_gcd_fib_mod [transferred])
|
|
289 |
using prems apply auto
|
|
290 |
done
|
|
291 |
|
|
292 |
lemma nat_fib_gcd: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
|
|
293 |
-- {* Law 6.111 *}
|
|
294 |
apply (induct m n rule: nat_gcd_induct)
|
|
295 |
apply (simp_all add: nat_gcd_non_0 nat_gcd_commute nat_gcd_fib_mod)
|
|
296 |
done
|
|
297 |
|
|
298 |
lemma int_fib_gcd: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
|
|
299 |
fib (gcd (m::int) n) = gcd (fib m) (fib n)"
|
|
300 |
by (erule nat_fib_gcd [transferred])
|
|
301 |
|
|
302 |
lemma nat_atMost_plus_one: "{..(k::nat) + 1} = insert (k + 1) {..k}"
|
|
303 |
by auto
|
|
304 |
|
|
305 |
theorem nat_fib_mult_eq_setsum:
|
|
306 |
"fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
|
|
307 |
apply (induct n)
|
|
308 |
apply (auto simp add: nat_atMost_plus_one nat_fib_plus_2 ring_simps)
|
|
309 |
done
|
|
310 |
|
|
311 |
theorem nat_fib_mult_eq_setsum':
|
|
312 |
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
|
|
313 |
using nat_fib_mult_eq_setsum by (simp add: One_nat_def)
|
|
314 |
|
|
315 |
theorem int_fib_mult_eq_setsum [rule_format]:
|
|
316 |
"n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
|
|
317 |
by (erule nat_fib_mult_eq_setsum [transferred])
|
|
318 |
|
|
319 |
end
|