src/HOL/Number_Theory/Fib.thy
changeset 41541 1fa4725c4656
parent 36350 bc7982c54e37
child 41959 b460124855b8
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Thu Jan 13 21:50:13 2011 +0100
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Thu Jan 13 23:50:16 2011 +0100
     1.3 @@ -1,14 +1,12 @@
     1.4  (*  Title:      Fib.thy
     1.5      Authors:    Lawrence C. Paulson, Jeremy Avigad
     1.6  
     1.7 -
     1.8  Defines the fibonacci function.
     1.9  
    1.10  The original "Fib" is due to Lawrence C. Paulson, and was adapted by
    1.11  Jeremy Avigad.
    1.12  *)
    1.13  
    1.14 -
    1.15  header {* Fib *}
    1.16  
    1.17  theory Fib
    1.18 @@ -284,16 +282,15 @@
    1.19  lemma gcd_fib_mod_int: 
    1.20    assumes "0 < (m::int)" and "0 <= n"
    1.21    shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
    1.22 -
    1.23    apply (rule gcd_fib_mod_nat [transferred])
    1.24 -  using prems apply auto
    1.25 -done
    1.26 +  using assms apply auto
    1.27 +  done
    1.28  
    1.29  lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  
    1.30      -- {* Law 6.111 *}
    1.31    apply (induct m n rule: gcd_nat_induct)
    1.32    apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
    1.33 -done
    1.34 +  done
    1.35  
    1.36  lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
    1.37      fib (gcd (m::int) n) = gcd (fib m) (fib n)"
    1.38 @@ -306,7 +303,7 @@
    1.39      "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
    1.40    apply (induct n)
    1.41    apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
    1.42 -done
    1.43 +  done
    1.44  
    1.45  theorem fib_mult_eq_setsum'_nat:
    1.46      "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"