src/HOL/Isar_Examples/Fibonacci.thy
 changeset 67051 e7e54a0b9197 parent 66453 cc19f7ca2ed6
```     1.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -21,10 +21,6 @@
1.4  text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
1.5    Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
1.6
1.7 -
1.8 -declare One_nat_def [simp]
1.9 -
1.10 -
1.11  subsection \<open>Fibonacci numbers\<close>
1.12
1.13  fun fib :: "nat \<Rightarrow> nat"
1.14 @@ -65,12 +61,13 @@
1.15    finally show "?P (n + 2)" .
1.16  qed
1.17
1.18 -lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1"
1.19 +lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
1.20    (is "?P n")
1.21  proof (induct n rule: fib_induct)
1.22    show "?P 0" by simp
1.23    show "?P 1" by simp
1.24    fix n
1.25 +  assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
1.26    have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
1.27      by simp
1.28    also have "\<dots> = fib (n + 2) + fib (n + 1)"
1.29 @@ -79,8 +76,10 @@
1.30      by (rule gcd_add2)
1.31    also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
1.32      by (simp add: gcd.commute)
1.33 -  also assume "\<dots> = 1"
1.34 -  finally show "?P (n + 2)" .
1.35 +  also have "\<dots> = 1"
1.36 +    using P by simp
1.37 +  finally show "?P (n + 2)"
1.38 +    by (simp add: coprime_iff_gcd_eq_1)
1.39  qed
1.40
1.41  lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
1.42 @@ -106,7 +105,8 @@
1.43    also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
1.44      by (simp add: gcd_mult_add)
1.45    also have "\<dots> = gcd (fib n) (fib (k + 1))"
1.46 -    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
1.47 +    using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
1.48 +    by (simp add: ac_simps)
1.49    also have "\<dots> = gcd (fib m) (fib n)"
1.50      using Suc by (simp add: gcd.commute)
1.51    finally show ?thesis .
```