author  haftmann 
Tue, 01 Sep 2009 15:39:33 +0200  
changeset 32479  521cc9bf2958 
parent 31952  src/HOL/NewNumberTheory/Fib.thy@40501bb2d57c 
child 35644  d20cf282342e 
permissions  rwrr 
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 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

89 
lemma fib_0_nat [simp]: "fib (0::nat) = 0" 
31719  90 
by simp 
91 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

92 
lemma fib_0_int [simp]: "fib (0::int) = 0" 
31719  93 
unfolding fib_int_def by simp 
94 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

95 
lemma fib_1_nat [simp]: "fib (1::nat) = 1" 
31719  96 
by simp 
97 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

98 
lemma fib_Suc_0_nat [simp]: "fib (Suc 0) = Suc 0" 
31719  99 
by simp 
100 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

101 
lemma fib_1_int [simp]: "fib (1::int) = 1" 
31719  102 
unfolding fib_int_def by simp 
103 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

104 
lemma fib_reduce_nat: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n  1) + fib (n  2)" 
31719  105 
by simp 
106 

107 
declare fib_nat.simps [simp del] 

108 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

109 
lemma fib_reduce_int: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n  1) + fib (n  2)" 
31719  110 
unfolding fib_int_def 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

111 
by (auto simp add: fib_reduce_nat nat_diff_distrib) 
31719  112 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

113 
lemma fib_neg_int [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0" 
31719  114 
unfolding fib_int_def by auto 
115 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

116 
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

117 
by (subst fib_reduce_nat, auto) 
31719  118 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

119 
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

120 
by (subst fib_reduce_int, auto) 
31719  121 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

122 
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

123 
by (subst fib_reduce_nat, auto simp add: One_nat_def) 
31719  124 
(* the need for One_nat_def is due to the natdiff_cancel_numerals 
125 
procedure *) 

126 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

127 
lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow> 
31719  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 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

141 
lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) + 
31719  142 
fib k * fib n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

143 
apply (induct n rule: fib_induct_nat) 
31719  144 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

145 
apply (subst fib_reduce_nat) 
31719  146 
apply (auto simp add: ring_simps) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

147 
apply (subst (1 3 5) fib_reduce_nat) 
31792  148 
apply (auto simp add: ring_simps Suc_eq_plus1) 
31719  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 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

156 
lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) + 
31719  157 
fib k * fib n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

158 
using fib_add_nat by (auto simp add: One_nat_def) 
31719  159 

160 

161 
(* transfer from nats to ints *) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

162 
lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> 
31719  163 
fib (n + k + 1) = fib (k + 1) * fib (n + 1) + 
164 
fib k * fib n " 

165 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

166 
by (rule fib_add_nat [transferred]) 
31719  167 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

168 
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

169 
apply (induct n rule: fib_induct_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

170 
apply (auto simp add: fib_plus_2_nat) 
31719  171 
done 
172 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

173 
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

174 
by (frule fib_neq_0_nat, simp) 
31719  175 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

176 
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

177 
unfolding fib_int_def by (simp add: fib_gr_0_nat) 
31719  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 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

184 
lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n)  
31719  185 
(fib (int n + 1))^2 = (1)^(n + 1)" 
186 
apply (induct n) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

187 
apply (auto simp add: ring_simps power2_eq_square fib_reduce_int 
31719  188 
power_add) 
189 
done 

190 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

191 
lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n  
31719  192 
(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

193 
by (insert fib_Cassini_aux_int [of "nat n"], auto) 
31719  194 

195 
(* 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

196 
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n = 
31719  197 
(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

198 
by (frule fib_Cassini_int, simp) 
31719  199 
*) 
200 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

201 
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n = 
31719  202 
(if even n then tsub ((fib (n + 1))^2) 1 
203 
else (fib (n + 1))^2 + 1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

204 
apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even) 
31719  205 
apply (subst tsub_eq) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

206 
apply (insert fib_gr_0_int [of "n + 1"], force) 
31719  207 
apply auto 
208 
done 

209 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

210 
lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n = 
31719  211 
(if even n then (fib (n + 1))^2  1 
212 
else (fib (n + 1))^2 + 1)" 

213 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

214 
by (rule fib_Cassini'_int [transferred, of n], auto) 
31719  215 

216 

217 
text {* \medskip Toward Law 6.111 of Concrete Mathematics *} 

218 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

219 
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

220 
apply (induct n rule: fib_induct_nat) 
31719  221 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

222 
apply (subst (2) fib_reduce_nat) 
31792  223 
apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *) 
31719  224 
apply (subst add_commute, auto) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

225 
apply (subst gcd_commute_nat, auto simp add: ring_simps) 
31719  226 
done 
227 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

228 
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

229 
using coprime_fib_plus_1_nat by (simp add: One_nat_def) 
31719  230 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

231 
lemma coprime_fib_plus_1_int: 
31719  232 
"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

233 
by (erule coprime_fib_plus_1_nat [transferred]) 
31719  234 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

235 
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

236 
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

237 
apply (rule cases_nat [of _ m]) 
31719  238 
apply simp 
239 
apply (subst add_assoc [symmetric]) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

240 
apply (simp add: fib_add_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

241 
apply (subst gcd_commute_nat) 
31719  242 
apply (subst mult_commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

243 
apply (subst gcd_add_mult_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

244 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

245 
apply (rule gcd_mult_cancel_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

246 
apply (rule coprime_fib_plus_1_nat) 
31719  247 
done 
248 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

249 
lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 
31719  250 
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

251 
by (erule gcd_fib_add_nat [transferred]) 
31719  252 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

253 
lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow> 
31719  254 
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

255 
by (simp add: gcd_fib_add_nat [symmetric, of _ "nm"]) 
31719  256 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

257 
lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow> 
31719  258 
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

259 
by (simp add: gcd_fib_add_int [symmetric, of _ "nm"]) 
31719  260 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

261 
lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow> 
31719  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) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

276 
also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n') 
31719  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 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

284 
lemma gcd_fib_mod_int: 
31719  285 
assumes "0 < (m::int)" and "0 <= n" 
286 
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" 

287 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

288 
apply (rule gcd_fib_mod_nat [transferred]) 
31719  289 
using prems apply auto 
290 
done 

291 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

292 
lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)" 
31719  293 
 {* Law 6.111 *} 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

294 
apply (induct m n rule: gcd_nat_induct) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

295 
apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat) 
31719  296 
done 
297 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

298 
lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 
31719  299 
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

300 
by (erule fib_gcd_nat [transferred]) 
31719  301 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

302 
lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}" 
31719  303 
by auto 
304 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

305 
theorem fib_mult_eq_setsum_nat: 
31719  306 
"fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" 
307 
apply (induct n) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

308 
apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps) 
31719  309 
done 
310 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

311 
theorem fib_mult_eq_setsum'_nat: 
31719  312 
"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

313 
using fib_mult_eq_setsum_nat by (simp add: One_nat_def) 
31719  314 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31792
diff
changeset

315 
theorem fib_mult_eq_setsum_int [rule_format]: 
31719  316 
"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

317 
by (erule fib_mult_eq_setsum_nat [transferred]) 
31719  318 

319 
end 