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.9 +    apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
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.17 -  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
1.19 -  done
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>