src/HOL/Number_Theory/Fib.thy
 changeset 41541 1fa4725c4656 parent 36350 bc7982c54e37 child 41959 b460124855b8
equal inserted replaced
41540:414a68d72279 41541:1fa4725c4656
`     1 (*  Title:      Fib.thy`
`     1 (*  Title:      Fib.thy`
`     2     Authors:    Lawrence C. Paulson, Jeremy Avigad`
`     2     Authors:    Lawrence C. Paulson, Jeremy Avigad`
`     4 `
`     3 `
`     5 Defines the fibonacci function.`
`     4 Defines the fibonacci function.`
`     6 `
`     5 `
`     7 The original "Fib" is due to Lawrence C. Paulson, and was adapted by`
`     6 The original "Fib" is due to Lawrence C. Paulson, and was adapted by`
`     8 Jeremy Avigad.`
`     7 Jeremy Avigad.`
`     9 *)`
`     8 *)`
`    11 `
`     9 `
`    12 header {* Fib *}`
`    10 header {* Fib *}`
`    13 `
`    11 `
`    14 theory Fib`
`    12 theory Fib`
`    15 imports Binomial`
`    13 imports Binomial`
`   282 qed`
`   280 qed`
`   283 `
`   281 `
`   284 lemma gcd_fib_mod_int: `
`   282 lemma gcd_fib_mod_int: `
`   285   assumes "0 < (m::int)" and "0 <= n"`
`   283   assumes "0 < (m::int)" and "0 <= n"`
`   286   shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"`
`   284   shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"`
`   288   apply (rule gcd_fib_mod_nat [transferred])`
`   285   apply (rule gcd_fib_mod_nat [transferred])`
`   289   using prems apply auto`
`   286   using assms apply auto`
`   290 done`
`   287   done`
`   291 `
`   288 `
`   292 lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  `
`   289 lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  `
`   293     -- {* Law 6.111 *}`
`   290     -- {* Law 6.111 *}`
`   294   apply (induct m n rule: gcd_nat_induct)`
`   291   apply (induct m n rule: gcd_nat_induct)`
`   295   apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)`
`   292   apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)`
`   296 done`
`   293   done`
`   297 `
`   294 `
`   298 lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>`
`   295 lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>`
`   299     fib (gcd (m::int) n) = gcd (fib m) (fib n)"`
`   296     fib (gcd (m::int) n) = gcd (fib m) (fib n)"`
`   300   by (erule fib_gcd_nat [transferred])`
`   297   by (erule fib_gcd_nat [transferred])`
`   301 `
`   298 `
`   304 `
`   301 `
`   305 theorem fib_mult_eq_setsum_nat:`
`   302 theorem fib_mult_eq_setsum_nat:`
`   306     "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"`
`   303     "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"`
`   307   apply (induct n)`
`   304   apply (induct n)`
`   308   apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)`
`   305   apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)`
`   309 done`
`   306   done`
`   310 `
`   307 `
`   311 theorem fib_mult_eq_setsum'_nat:`
`   308 theorem fib_mult_eq_setsum'_nat:`
`   312     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"`
`   309     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"`
`   313   using fib_mult_eq_setsum_nat by (simp add: One_nat_def)`
`   310   using fib_mult_eq_setsum_nat by (simp add: One_nat_def)`
`   314 `
`   311 `