12 |
12 |
13 |
13 |
14 subsection \<open>Fibonacci numbers\<close> |
14 subsection \<open>Fibonacci numbers\<close> |
15 |
15 |
16 fun fib :: "nat \<Rightarrow> nat" |
16 fun fib :: "nat \<Rightarrow> nat" |
17 where |
17 where |
18 fib0: "fib 0 = 0" |
18 fib0: "fib 0 = 0" |
19 | fib1: "fib (Suc 0) = 1" |
19 | fib1: "fib (Suc 0) = 1" |
20 | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n" |
20 | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n" |
21 |
21 |
22 |
22 |
23 subsection \<open>Basic Properties\<close> |
23 subsection \<open>Basic Properties\<close> |
24 |
24 |
25 lemma fib_1 [simp]: "fib (1::nat) = 1" |
25 lemma fib_1 [simp]: "fib 1 = 1" |
26 by (metis One_nat_def fib1) |
26 by (metis One_nat_def fib1) |
27 |
27 |
28 lemma fib_2 [simp]: "fib (2::nat) = 1" |
28 lemma fib_2 [simp]: "fib 2 = 1" |
29 using fib.simps(3) [of 0] |
29 using fib.simps(3) [of 0] by (simp add: numeral_2_eq_2) |
30 by (simp add: numeral_2_eq_2) |
|
31 |
30 |
32 lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n" |
31 lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n" |
33 by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3)) |
32 by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3)) |
34 |
33 |
35 lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
34 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
36 by (induct n rule: fib.induct) (auto simp add: field_simps) |
35 by (induct n rule: fib.induct) (auto simp add: field_simps) |
37 |
36 |
38 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0" |
37 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0" |
39 by (induct n rule: fib.induct) (auto simp add: ) |
38 by (induct n rule: fib.induct) auto |
40 |
39 |
41 |
40 |
42 subsection \<open>More efficient code\<close> |
41 subsection \<open>More efficient code\<close> |
43 |
42 |
44 text \<open> |
43 text \<open> |
45 The naive approach is very inefficient since the branching recursion leads to many |
44 The naive approach is very inefficient since the branching recursion leads to many |
46 values of @{term fib} being computed multiple times. We can avoid this by ``remembering'' |
45 values of @{term fib} being computed multiple times. We can avoid this by ``remembering'' |
47 the last two values in the sequence, yielding a tail-recursive version. |
46 the last two values in the sequence, yielding a tail-recursive version. |
48 This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the |
47 This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the |
49 time required to multiply two $n$-bit integers), but much better than the naive version, |
48 time required to multiply two $n$-bit integers), but much better than the naive version, |
50 which is exponential. |
49 which is exponential. |
51 \<close> |
50 \<close> |
52 |
51 |
53 fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where |
52 fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
54 "gen_fib a b 0 = a" |
53 where |
55 | "gen_fib a b (Suc 0) = b" |
54 "gen_fib a b 0 = a" |
56 | "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)" |
55 | "gen_fib a b (Suc 0) = b" |
|
56 | "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)" |
57 |
57 |
58 lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)" |
58 lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)" |
59 by (induction a b n rule: gen_fib.induct) simp_all |
59 by (induct a b n rule: gen_fib.induct) simp_all |
60 |
60 |
61 lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)" |
61 lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)" |
62 by (induction m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence) |
62 by (induct m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence) |
63 |
63 |
64 lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n" |
64 lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n" |
65 using gen_fib_fib[of 0 n] by simp |
65 using gen_fib_fib[of 0 n] by simp |
66 |
66 |
67 declare fib_conv_gen_fib [code] |
67 declare fib_conv_gen_fib [code] |
68 |
68 |
69 |
69 |
70 subsection \<open>A Few Elementary Results\<close> |
70 subsection \<open>A Few Elementary Results\<close> |
71 |
71 |
72 text \<open> |
72 text \<open> |
73 \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is |
73 \<^medskip> Concrete Mathematics, page 278: Cassini's identity. The proof is |
74 much easier using integers, not natural numbers! |
74 much easier using integers, not natural numbers! |
75 \<close> |
75 \<close> |
76 |
76 |
77 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)" |
77 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)" |
78 by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add) |
78 by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add) |
79 |
79 |
80 lemma fib_Cassini_nat: |
80 lemma fib_Cassini_nat: |
81 "fib (Suc (Suc n)) * fib n = |
81 "fib (Suc (Suc n)) * fib n = |
82 (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)" |
82 (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)" |
83 using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power) |
83 using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power) |
84 |
84 |
85 |
85 |
86 subsection \<open>Law 6.111 of Concrete Mathematics\<close> |
86 subsection \<open>Law 6.111 of Concrete Mathematics\<close> |
87 |
87 |
88 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))" |
88 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))" |
89 apply (induct n rule: fib.induct) |
89 apply (induct n rule: fib.induct) |
90 apply auto |
90 apply auto |
91 apply (metis gcd_add1 add.commute) |
91 apply (metis gcd_add1 add.commute) |
92 done |
92 done |
93 |
93 |
107 case (less n) |
107 case (less n) |
108 show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
108 show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
109 proof (cases "m < n") |
109 proof (cases "m < n") |
110 case True |
110 case True |
111 then have "m \<le> n" by auto |
111 then have "m \<le> n" by auto |
112 with \<open>0 < m\<close> have pos_n: "0 < n" by auto |
112 with \<open>0 < m\<close> have "0 < n" by auto |
113 with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto |
113 with \<open>0 < m\<close> \<open>m < n\<close> have *: "n - m < n" by auto |
114 have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))" |
114 have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))" |
115 by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto) |
115 by (simp add: mod_if [of n]) (use \<open>m < n\<close> in auto) |
116 also have "\<dots> = gcd (fib m) (fib (n - m))" |
116 also have "\<dots> = gcd (fib m) (fib (n - m))" |
117 by (simp add: less.hyps diff \<open>0 < m\<close>) |
117 by (simp add: less.hyps * \<open>0 < m\<close>) |
118 also have "\<dots> = gcd (fib m) (fib n)" |
118 also have "\<dots> = gcd (fib m) (fib n)" |
119 by (simp add: gcd_fib_diff \<open>m \<le> n\<close>) |
119 by (simp add: gcd_fib_diff \<open>m \<le> n\<close>) |
120 finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" . |
120 finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" . |
121 next |
121 next |
122 case False |
122 case False |
123 then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
123 then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
124 by (cases "m = n") auto |
124 by (cases "m = n") auto |
125 qed |
125 qed |
126 qed |
126 qed |
127 |
127 |
128 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" |
128 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" \<comment> \<open>Law 6.111\<close> |
129 \<comment> \<open>Law 6.111\<close> |
|
130 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod) |
129 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod) |
131 |
130 |
132 theorem fib_mult_eq_sum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
131 theorem fib_mult_eq_sum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
133 by (induct n rule: nat.induct) (auto simp add: field_simps) |
132 by (induct n rule: nat.induct) (auto simp add: field_simps) |
134 |
133 |
135 |
134 |
136 subsection \<open>Closed form\<close> |
135 subsection \<open>Closed form\<close> |
137 |
136 |
138 lemma fib_closed_form: |
137 lemma fib_closed_form: |
139 defines "\<phi> \<equiv> (1 + sqrt 5) / (2::real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2::real)" |
138 fixes \<phi> \<psi> :: real |
140 shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5" |
139 defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
141 proof (induction n rule: fib.induct) |
140 and "\<psi> \<equiv> (1 - sqrt 5) / 2" |
|
141 shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5" |
|
142 proof (induct n rule: fib.induct) |
142 fix n :: nat |
143 fix n :: nat |
143 assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5" |
144 assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5" |
144 assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5" |
145 assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5" |
145 have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp |
146 have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp |
146 also have "... = (\<phi>^n*(\<phi> + 1) - \<psi>^n*(\<psi> + 1)) / sqrt 5" |
147 also have "\<dots> = (\<phi>^n * (\<phi> + 1) - \<psi>^n * (\<psi> + 1)) / sqrt 5" |
147 by (simp add: IH1 IH2 field_simps) |
148 by (simp add: IH1 IH2 field_simps) |
148 also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square) |
149 also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square) |
149 also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square) |
150 also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square) |
150 also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)" |
151 also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)" |
151 by (simp add: power2_eq_square) |
152 by (simp add: power2_eq_square) |
152 finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" . |
153 finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" . |
153 qed (simp_all add: \<phi>_def \<psi>_def field_simps) |
154 qed (simp_all add: \<phi>_def \<psi>_def field_simps) |
154 |
155 |
155 lemma fib_closed_form': |
156 lemma fib_closed_form': |
156 defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)" |
157 fixes \<phi> \<psi> :: real |
|
158 defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
159 and "\<psi> \<equiv> (1 - sqrt 5) / 2" |
157 assumes "n > 0" |
160 assumes "n > 0" |
158 shows "fib n = round (\<phi> ^ n / sqrt 5)" |
161 shows "fib n = round (\<phi> ^ n / sqrt 5)" |
159 proof (rule sym, rule round_unique') |
162 proof (rule sym, rule round_unique') |
160 have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5" |
163 have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5" |
161 by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs) |
164 by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs) |
162 also { |
165 also { |
163 from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1" |
166 from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1" |
164 by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt) |
167 by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt) |
165 also have "... < sqrt 5 / 2" by (simp add: \<psi>_def field_simps) |
168 also have "\<dots> < sqrt 5 / 2" by (simp add: \<psi>_def field_simps) |
166 finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps) |
169 finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps) |
167 } |
170 } |
168 finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" . |
171 finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" . |
169 qed |
172 qed |
170 |
173 |
171 lemma fib_asymptotics: |
174 lemma fib_asymptotics: |
172 defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" |
175 fixes \<phi> :: real |
173 shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1" |
176 defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
177 shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1" |
174 proof - |
178 proof - |
175 define \<psi> where "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)" |
179 define \<psi> :: real where "\<psi> \<equiv> (1 - sqrt 5) / 2" |
176 have "\<phi> > 1" by (simp add: \<phi>_def) |
180 have "\<phi> > 1" by (simp add: \<phi>_def) |
177 hence A: "\<phi> \<noteq> 0" by auto |
181 then have *: "\<phi> \<noteq> 0" by auto |
178 have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0" |
182 have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0" |
179 by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos) |
183 by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos) |
180 hence "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0" by (intro tendsto_diff tendsto_const) |
184 then have "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0" |
181 with A show ?thesis |
185 by (intro tendsto_diff tendsto_const) |
|
186 with * show ?thesis |
182 by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def]) |
187 by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def]) |
183 qed |
188 qed |
184 |
189 |
185 |
190 |
186 subsection \<open>Divide-and-Conquer recurrence\<close> |
191 subsection \<open>Divide-and-Conquer recurrence\<close> |
187 |
192 |
188 text \<open> |
193 text \<open> |
189 The following divide-and-conquer recurrence allows for a more efficient computation |
194 The following divide-and-conquer recurrence allows for a more efficient computation |
190 of Fibonacci numbers; however, it requires memoisation of values to be reasonably |
195 of Fibonacci numbers; however, it requires memoisation of values to be reasonably |
191 efficient, cutting the number of values to be computed to logarithmically many instead of |
196 efficient, cutting the number of values to be computed to logarithmically many instead of |
192 linearly many. The vast majority of the computation time is then actually spent on the |
197 linearly many. The vast majority of the computation time is then actually spent on the |
193 multiplication, since the output number is exponential in the input number. |
198 multiplication, since the output number is exponential in the input number. |
194 \<close> |
199 \<close> |
195 |
200 |
196 lemma fib_rec_odd: |
201 lemma fib_rec_odd: |
197 defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)" |
202 fixes \<phi> \<psi> :: real |
198 shows "fib (Suc (2*n)) = fib n^2 + fib (Suc n)^2" |
203 defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
204 and "\<psi> \<equiv> (1 - sqrt 5) / 2" |
|
205 shows "fib (Suc (2 * n)) = fib n^2 + fib (Suc n)^2" |
199 proof - |
206 proof - |
200 have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5" |
207 have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5" |
201 by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square) |
208 by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square) |
202 also have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = |
209 also |
203 \<phi>^(2*n) + \<psi>^(2*n) - 2*(\<phi>*\<psi>)^n + \<phi>^(2*n+2) + \<psi>^(2*n+2) - 2*(\<phi>*\<psi>)^(n+1)" (is "_ = ?A") |
210 let ?A = "\<phi>^(2 * n) + \<psi>^(2 * n) - 2*(\<phi> * \<psi>)^n + \<phi>^(2 * n + 2) + \<psi>^(2 * n + 2) - 2*(\<phi> * \<psi>)^(n + 1)" |
204 by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib) |
211 have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = ?A" |
205 also have "\<phi> * \<psi> = -1" by (simp add: \<phi>_def \<psi>_def field_simps) |
212 by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib) |
206 hence "?A = \<phi>^(2*n+1) * (\<phi> + inverse \<phi>) + \<psi>^(2*n+1) * (\<psi> + inverse \<psi>)" |
213 also have "\<phi> * \<psi> = -1" |
|
214 by (simp add: \<phi>_def \<psi>_def field_simps) |
|
215 then have "?A = \<phi>^(2 * n + 1) * (\<phi> + inverse \<phi>) + \<psi>^(2 * n + 1) * (\<psi> + inverse \<psi>)" |
207 by (auto simp: field_simps power2_eq_square) |
216 by (auto simp: field_simps power2_eq_square) |
208 also have "1 + sqrt 5 > 0" by (auto intro: add_pos_pos) |
217 also have "1 + sqrt 5 > 0" |
209 hence "\<phi> + inverse \<phi> = sqrt 5" by (simp add: \<phi>_def field_simps) |
218 by (auto intro: add_pos_pos) |
210 also have "\<psi> + inverse \<psi> = -sqrt 5" by (simp add: \<psi>_def field_simps) |
219 then have "\<phi> + inverse \<phi> = sqrt 5" |
211 also have "(\<phi> ^ (2*n+1) * sqrt 5 + \<psi> ^ (2*n+1)* - sqrt 5) / 5 = |
220 by (simp add: \<phi>_def field_simps) |
212 (\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * (sqrt 5 / 5)" by (simp add: field_simps) |
221 also have "\<psi> + inverse \<psi> = -sqrt 5" |
213 also have "sqrt 5 / 5 = inverse (sqrt 5)" by (simp add: field_simps) |
222 by (simp add: \<psi>_def field_simps) |
214 also have "(\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * ... = of_nat (fib (Suc (2*n)))" |
223 also have "(\<phi> ^ (2 * n + 1) * sqrt 5 + \<psi> ^ (2 * n + 1) * - sqrt 5) / 5 = |
|
224 (\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * (sqrt 5 / 5)" |
|
225 by (simp add: field_simps) |
|
226 also have "sqrt 5 / 5 = inverse (sqrt 5)" |
|
227 by (simp add: field_simps) |
|
228 also have "(\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * \<dots> = of_nat (fib (Suc (2 * n)))" |
215 by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse) |
229 by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse) |
216 finally show ?thesis by (simp only: of_nat_eq_iff) |
230 finally show ?thesis |
217 qed |
231 by (simp only: of_nat_eq_iff) |
218 |
232 qed |
219 lemma fib_rec_even: "fib (2*n) = (fib (n - 1) + fib (n + 1)) * fib n" |
233 |
220 proof (induction n) |
234 lemma fib_rec_even: "fib (2 * n) = (fib (n - 1) + fib (n + 1)) * fib n" |
|
235 proof (induct n) |
|
236 case 0 |
|
237 then show ?case by simp |
|
238 next |
221 case (Suc n) |
239 case (Suc n) |
222 let ?rfib = "\<lambda>x. real (fib x)" |
240 let ?rfib = "\<lambda>x. real (fib x)" |
223 have "2 * (Suc n) = Suc (Suc (2*n))" by simp |
241 have "2 * (Suc n) = Suc (Suc (2 * n))" by simp |
224 also have "real (fib ...) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n" |
242 also have "real (fib \<dots>) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n" |
225 by (simp add: fib_rec_odd Suc) |
243 by (simp add: fib_rec_odd Suc) |
226 also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n" |
244 also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n" |
227 by (cases n) simp_all |
245 by (cases n) simp_all |
228 also have "?rfib n^2 + ?rfib (Suc n)^2 + ... = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)" |
246 also have "?rfib n^2 + ?rfib (Suc n)^2 + \<dots> = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)" |
229 by (simp add: algebra_simps power2_eq_square) |
247 by (simp add: algebra_simps power2_eq_square) |
230 also have "... = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp |
248 also have "\<dots> = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp |
231 finally show ?case by (simp only: of_nat_eq_iff) |
249 finally show ?case by (simp only: of_nat_eq_iff) |
232 qed simp |
250 qed |
233 |
251 |
234 lemma fib_rec_even': "fib (2*n) = (2*fib (n - 1) + fib n) * fib n" |
252 lemma fib_rec_even': "fib (2 * n) = (2 * fib (n - 1) + fib n) * fib n" |
235 by (subst fib_rec_even, cases n) simp_all |
253 by (subst fib_rec_even, cases n) simp_all |
236 |
254 |
237 lemma fib_rec: |
255 lemma fib_rec: |
238 "fib n = (if n = 0 then 0 else if n = 1 then 1 else |
256 "fib n = |
239 if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn |
257 (if n = 0 then 0 else if n = 1 then 1 |
240 else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)" |
258 else if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn |
|
259 else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)" |
241 by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def) |
260 by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def) |
242 |
261 |
243 |
262 |
244 subsection \<open>Fibonacci and Binomial Coefficients\<close> |
263 subsection \<open>Fibonacci and Binomial Coefficients\<close> |
245 |
264 |
246 lemma sum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)" |
265 lemma sum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)" |
247 by (induct n) auto |
266 by (induct n) auto |
248 |
267 |
249 lemma sum_choose_drop_zero: |
268 lemma sum_choose_drop_zero: |
250 "(\<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)" |
269 "(\<Sum>k = 0..Suc n. if k = 0 then 0 else (Suc n - k) choose (k - 1)) = |
|
270 (\<Sum>j = 0..n. (n-j) choose j)" |
251 by (rule trans [OF sum.cong sum_drop_zero]) auto |
271 by (rule trans [OF sum.cong sum_drop_zero]) auto |
252 |
272 |
253 lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)" |
273 lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)" |
254 proof (induct n rule: fib.induct) |
274 proof (induct n rule: fib.induct) |
255 case 1 |
275 case 1 |