src/HOL/Number_Theory/Fib.thy
changeset 67051 e7e54a0b9197
parent 65393 079a6f850c02
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -87,17 +87,34 @@
     1.4  
     1.5  lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
     1.6    apply (induct n rule: fib.induct)
     1.7 -  apply auto
     1.8 -  apply (metis gcd_add1 add.commute)
     1.9 +    apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
    1.10 +  apply (simp add: add.assoc [symmetric])
    1.11    done
    1.12  
    1.13 -lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
    1.14 -  apply (simp add: gcd.commute [of "fib m"])
    1.15 -  apply (cases m)
    1.16 -  apply (auto simp add: fib_add)
    1.17 -  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
    1.18 -    gcd_add_mult gcd_mult_cancel gcd.commute)
    1.19 -  done
    1.20 +lemma gcd_fib_add:
    1.21 +  "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
    1.22 +proof (cases m)
    1.23 +  case 0
    1.24 +  then show ?thesis
    1.25 +    by simp
    1.26 +next
    1.27 +  case (Suc q)
    1.28 +  from coprime_fib_Suc_nat [of q]
    1.29 +  have "coprime (fib (Suc q)) (fib q)"
    1.30 +    by (simp add: ac_simps)
    1.31 +  have "gcd (fib q) (fib (Suc q)) = Suc 0"
    1.32 +    using coprime_fib_Suc_nat [of q] by simp
    1.33 +  then have *: "gcd (fib n * fib q) (fib n * fib (Suc q)) = fib n"
    1.34 +    by (simp add: gcd_mult_distrib_nat [symmetric])
    1.35 +  moreover have "gcd (fib (Suc q)) (fib n * fib q + fib (Suc n) * fib (Suc q)) =
    1.36 +    gcd (fib (Suc q)) (fib n * fib q)"
    1.37 +    using gcd_add_mult [of "fib (Suc q)"] by (simp add: ac_simps)
    1.38 +  moreover have "gcd (fib (Suc q)) (fib n * fib (Suc q)) = fib (Suc q)"
    1.39 +    by simp
    1.40 +  ultimately show ?thesis
    1.41 +    using Suc \<open>coprime (fib (Suc q)) (fib q)\<close>
    1.42 +    by (auto simp add: fib_add algebra_simps gcd_mult_right_right_cancel)
    1.43 +qed
    1.44  
    1.45  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
    1.46    by (simp add: gcd_fib_add [symmetric, of _ "n-m"])