author  wenzelm 
Thu, 13 Jan 2011 23:50:16 +0100  
changeset 41541  1fa4725c4656 
parent 36350  bc7982c54e37 
child 41959  b460124855b8 
permissions  rwrr 
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 _ "nm"]) 
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 _ "nm"]) 
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 