diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Isar_Examples/Fibonacci.thy --- a/src/HOL/Isar_Examples/Fibonacci.thy Sat Nov 11 18:33:35 2017 +0000 +++ b/src/HOL/Isar_Examples/Fibonacci.thy Sat Nov 11 18:41:08 2017 +0000 @@ -21,10 +21,6 @@ text_raw \\<^footnote>\Isar version by Gertrud Bauer. Original tactic script by Larry Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\\ - -declare One_nat_def [simp] - - subsection \Fibonacci numbers\ fun fib :: "nat \ nat" @@ -65,12 +61,13 @@ finally show "?P (n + 2)" . qed -lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" +lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))" (is "?P n") proof (induct n rule: fib_induct) show "?P 0" by simp show "?P 1" by simp fix n + assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))" have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" by simp also have "\ = fib (n + 2) + fib (n + 1)" @@ -79,8 +76,10 @@ by (rule gcd_add2) also have "\ = gcd (fib (n + 1)) (fib (n + 1 + 1))" by (simp add: gcd.commute) - also assume "\ = 1" - finally show "?P (n + 2)" . + also have "\ = 1" + using P by simp + finally show "?P (n + 2)" + by (simp add: coprime_iff_gcd_eq_1) qed lemma gcd_mult_add: "(0::nat) < n \ gcd (n * k + m) n = gcd m n" @@ -106,7 +105,8 @@ also have "gcd \ (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" by (simp add: gcd_mult_add) also have "\ = gcd (fib n) (fib (k + 1))" - by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) + using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"] + by (simp add: ac_simps) also have "\ = gcd (fib m) (fib n)" using Suc by (simp add: gcd.commute) finally show ?thesis .