src/HOL/Number_Theory/Fib.thy
changeset 62348 9a5f43dac883
parent 61649 268d88ec9087
child 62429 25271ff79171
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -63,11 +63,11 @@
     1.4    done
     1.5  
     1.6  lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
     1.7 -  apply (simp add: gcd_commute_nat [of "fib m"])
     1.8 +  apply (simp add: gcd.commute [of "fib m"])
     1.9    apply (cases m)
    1.10    apply (auto simp add: fib_add)
    1.11 -  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
    1.12 -    gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
    1.13 +  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
    1.14 +    gcd_add_mult_nat gcd_mult_cancel gcd.commute)
    1.15    done
    1.16  
    1.17  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
    1.18 @@ -98,7 +98,7 @@
    1.19  
    1.20  lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
    1.21      -- \<open>Law 6.111\<close>
    1.22 -  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
    1.23 +  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
    1.24  
    1.25  theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
    1.26    by (induct n rule: nat.induct) (auto simp add:  field_simps)