# Theory Fibonacci

Up to index of Isabelle/HOL/Isar_examples

theory Fibonacci
imports Primes
begin

    (*  Title:      HOL/Isar_examples/Fibonacci.thy
        ID:         $Id: Fibonacci.thy,v 1.18 2005/06/17 14:13:07 haftmann Exp $
        Author:     Gertrud Bauer
        Copyright   1999 Technische Universitaet Muenchen

    The Fibonacci function.  Demonstrates the use of recdef.  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)
    *)

    header {* Fib and Gcd commute *}

    theory Fibonacci imports Primes begin

    text_raw {*
     \footnote{Isar version by Gertrud Bauer.  Original tactic script by
     Larry Paulson.  A few proofs of laws taken from
     \cite{Concrete-Math}.}
    *}

    subsection {* Fibonacci numbers *}

    consts fib :: "nat => nat"
    recdef fib less_than
     "fib 0 = 0"
     "fib (Suc 0) = 1"
     "fib (Suc (Suc x)) = fib x + fib (Suc x)"

    lemma [simp]: "0 < fib (Suc n)"
      by (induct n rule: fib.induct) (simp+)

    text {* Alternative induction rule. *}

    theorem fib_induct:
        "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
      by (induct rule: fib.induct, simp+)

    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")
      -- {* see \cite[page 280]{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 gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (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 + 1) = fib (n + 1) + fib (n + 2)"
        by simp
      also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
        by (simp only: 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)" .
    qed

    lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
    proof -
      assume "0 < n"
      hence "gcd (n * k + m, n) = gcd (n, m mod n)"
        by (simp add: gcd_non_0 add_commute)
      also have "... = gcd (m, n)" by (simp! add: gcd_non_0)
      finally show ?thesis .
    qed

    lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
    proof (cases m)
      assume "m = 0"
      thus ?thesis by simp
    next
      fix k assume "m = Suc k"
      hence "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))"
        by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
      also have "... = gcd (fib m, fib n)"
        by (simp! add: gcd_commute)
      finally show ?thesis .
    qed

    lemma gcd_fib_diff:
      "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
    proof -
      assume "m <= n"
      have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
        by (simp add: gcd_fib_add)
      also have "n - m + m = n" by (simp!)
      finally show ?thesis .
    qed

    lemma gcd_fib_mod:
      "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
    proof -
      assume m: "0 < m"
      show ?thesis
      proof (induct n rule: nat_less_induct)
        fix n
        assume hyp: "ALL ma. ma < n
          --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
        show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
        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
            assume "n < m" thus ?thesis by simp
          next
            assume not_lt: "~ n < m" hence le: "m <= n" by simp
            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 from le have "... = gcd (fib m, fib n)"
              by (rule gcd_fib_diff)
            finally have "gcd (fib m, fib ((n - m) mod m)) =
              gcd (fib m, fib n)" .
            with not_lt show ?thesis by simp
          qed
          finally show ?thesis .
        qed
      qed
    qed

    theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
    proof (induct m n rule: gcd_induct)
      fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
      fix n :: nat assume n: "0 < n"
      hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
      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

### Fibonacci numbers

lemma

      0 < fib (Suc n)

theorem fib_induct:

      [| P 0; P 1; !!n. [| P (n + 1); P n |] ==> P (n + 2) |] ==> P n

### Fib and gcd commute

lemma fib_add:

      fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n

lemma gcd_fib_Suc_eq_1:

      gcd (fib n, fib (n + 1)) = 1

lemma gcd_mult_add:

      0 < n ==> gcd (n * k + m, n) = gcd (m, n)

lemma gcd_fib_add:

      gcd (fib m, fib (n + m)) = gcd (fib m, fib n)

lemma gcd_fib_diff:

      m ≤ n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)

lemma gcd_fib_mod:

      0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)

theorem fib_gcd:

      fib (gcd (m, n)) = gcd (fib m, fib n)