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