Quelle  Fibonacci.thy

(*  Title:      HOL/Isar_Examples/Fibonacci.thy
  Author: Gertrud Bauer
  Copyright 1999 Technische Universitaet Muenchen
 
 The Fibonacci function. Original
 tactic script by Lawrence C Paulson.
 
 Fibonacci numbers: proofs of laws taken from
 
  R. L. Graham, D. E. Knuth, O. Patashnik.
  Concrete Mathematics.
  (Addison-Wesley, 1989)
*)

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 🍋‹"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 🍋‹"Concrete-Math"›.›
 
 lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
  (is "?P n")
  🍋 ‹see 🍋‹‹page 280› in "Concrete-Math"›\›
 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) 🚫 ==> gcd (n * k + m) n = gcd m n"
 proof -
  assume "0 🚫"
  then have "gcd (n * k + m) n = gcd n (m mod n)"
  by (simp add: gcd_non_0_nat add.commute)
  also from ‹0 🚫› 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 🚫"
 proof (induct n rule: nat_less_induct)
  case hyp: (1 n)
  show ?case
  proof -
  have "n mod m = (if n 🚫 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 🚫")
  case True
  then show ?thesis by simp
  next
  case False
  then have "m ≤ n" by simp
  from ‹0 🚫› and False have "n - m 🚫"
  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 🚫"
  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