Theory Fibonacci
section ‹Fib and Gcd commute›
theory Fibonacci
imports "HOL-Computational_Algebra.Primes"
begin
text_raw ‹⁋‹Isar version by Gertrud Bauer. Original tactic script by Larry
Paulson. A few proofs of laws taken from \<^cite>‹"Concrete-Math"›.››
subsection ‹Fibonacci numbers›
fun fib :: "nat ⇒ nat"
where
"fib 0 = 0"
| "fib (Suc 0) = 1"
| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "fib (Suc n) > 0"
by (induct n rule: fib.induct) simp_all
text ‹Alternative induction rule.›
theorem fib_induct: "P 0 ⟹ P 1 ⟹ (⋀n. P (n + 1) ⟹ P n ⟹ P (n + 2)) ⟹ P n"
for n :: nat
by (induct rule: fib.induct) simp_all
subsection ‹Fib and gcd commute›
text ‹A few laws taken from \<^cite>‹"Concrete-Math"›.›
lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
(is "?P n")
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
fix n
have "fib (n + 2 + k + 1)
= fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
also assume "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" (is " _ = ?R1")
also assume "fib (n + 1 + k + 1) = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
(is " _ = ?R2")
also have "?R1 + ?R2 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
by (simp add: add_mult_distrib2)
finally show "?P (n + 2)" .
qed
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)"
by simp
also have "gcd (fib (n + 2)) … = gcd (fib (n + 2)) (fib (n + 1))"
by (rule gcd_add2)
also have "… = gcd (fib (n + 1)) (fib (n + 1 + 1))"
by (simp add: gcd.commute)
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"
proof -
assume "0 < n"
then have "gcd (n * k + m) n = gcd n (m mod n)"
by (simp add: gcd_non_0_nat add.commute)
also from ‹0 < n› have "… = gcd m n"
by (simp add: gcd_non_0_nat)
finally show ?thesis .
qed
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
proof (cases m)
case 0
then show ?thesis by simp
next
case (Suc k)
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
by (simp add: gcd.commute)
also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
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))"
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 .
qed
lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m ≤ n"
proof -
have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
by (simp add: gcd_fib_add)
also from ‹m ≤ n› have "n - m + m = n"
by simp
finally show ?thesis .
qed
lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"
proof (induct n rule: nat_less_induct)
case hyp: (1 n)
show ?case
proof -
have "n mod m = (if n < m then n else (n - m) mod m)"
by (rule mod_if)
also have "gcd (fib m) (fib …) = gcd (fib m) (fib n)"
proof (cases "n < m")
case True
then show ?thesis by simp
next
case False
then have "m ≤ n" by simp
from ‹0 < m› and False have "n - m < n"
by simp
with hyp have "gcd (fib m) (fib ((n - m) mod m))
= gcd (fib m) (fib (n - m))" by simp
also have "… = gcd (fib m) (fib n)"
using ‹m ≤ n› by (rule gcd_fib_diff)
finally have "gcd (fib m) (fib ((n - m) mod m)) =
gcd (fib m) (fib n)" .
with False show ?thesis by simp
qed
finally show ?thesis .
qed
qed
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
(is "?P m n")
proof (induct m n rule: gcd_nat_induct)
fix m n :: nat
show "fib (gcd m 0) = gcd (fib m) (fib 0)"
by simp
assume n: "0 < n"
then have "gcd m n = gcd n (m mod n)"
by (simp add: gcd_non_0_nat)
also assume hyp: "fib … = gcd (fib n) (fib (m mod n))"
also from n have "… = gcd (fib n) (fib m)"
by (rule gcd_fib_mod)
also have "… = gcd (fib m) (fib n)"
by (rule gcd.commute)
finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
qed
end