src/HOL/Number_Theory/Fib.thy
changeset 41541 1fa4725c4656
parent 36350 bc7982c54e37
child 41959 b460124855b8
equal deleted 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
     3 
       
     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 *)
    10 
       
    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)"
   287 
       
   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