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 .