src/HOL/Number_Theory/Fib.thy
author haftmann
Fri Jul 04 20:18:47 2014 +0200 (2014-07-04)
changeset 57512 cc97b347b301
parent 54713 6666fc0b9ebc
child 58889 5b7a9633cfa8
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
wenzelm@41959
     1
(*  Title:      HOL/Number_Theory/Fib.thy
wenzelm@41959
     2
    Author:     Lawrence C. Paulson
wenzelm@41959
     3
    Author:     Jeremy Avigad
nipkow@31719
     4
nipkow@31719
     5
Defines the fibonacci function.
nipkow@31719
     6
nipkow@31719
     7
The original "Fib" is due to Lawrence C. Paulson, and was adapted by
nipkow@31719
     8
Jeremy Avigad.
nipkow@31719
     9
*)
nipkow@31719
    10
nipkow@31719
    11
header {* Fib *}
nipkow@31719
    12
nipkow@31719
    13
theory Fib
nipkow@31719
    14
imports Binomial
nipkow@31719
    15
begin
nipkow@31719
    16
nipkow@31719
    17
nipkow@31719
    18
subsection {* Main definitions *}
nipkow@31719
    19
paulson@54713
    20
fun fib :: "nat \<Rightarrow> nat"
nipkow@31719
    21
where
paulson@54713
    22
    fib0: "fib 0 = 0"
paulson@54713
    23
  | fib1: "fib (Suc 0) = 1"
paulson@54713
    24
  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
nipkow@31719
    25
nipkow@31719
    26
subsection {* Fibonacci numbers *}
nipkow@31719
    27
paulson@54713
    28
lemma fib_1 [simp]: "fib (1::nat) = 1"
paulson@54713
    29
  by (metis One_nat_def fib1)
nipkow@31719
    30
paulson@54713
    31
lemma fib_2 [simp]: "fib (2::nat) = 1"
paulson@54713
    32
  using fib.simps(3) [of 0]
paulson@54713
    33
  by (simp add: numeral_2_eq_2)
nipkow@31719
    34
paulson@54713
    35
lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
paulson@54713
    36
  by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
nipkow@31719
    37
paulson@54713
    38
lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
paulson@54713
    39
  by (induct n rule: fib.induct) (auto simp add: field_simps)
nipkow@31719
    40
paulson@54713
    41
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
paulson@54713
    42
  by (induct n rule: fib.induct) (auto simp add: )
nipkow@31719
    43
nipkow@31719
    44
text {*
nipkow@31719
    45
  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
nipkow@31719
    46
  much easier using integers, not natural numbers!
nipkow@31719
    47
*}
nipkow@31719
    48
paulson@54713
    49
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
paulson@54713
    50
  by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
nipkow@31719
    51
paulson@54713
    52
lemma fib_Cassini_nat:
paulson@54713
    53
    "fib (Suc (Suc n)) * fib n =
paulson@54713
    54
       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
paulson@54713
    55
using fib_Cassini_int [of n] by auto
nipkow@31719
    56
nipkow@31719
    57
nipkow@31719
    58
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
nipkow@31719
    59
paulson@54713
    60
lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
paulson@54713
    61
  apply (induct n rule: fib.induct)
nipkow@31719
    62
  apply auto
haftmann@57512
    63
  apply (metis gcd_add1_nat add.commute)
wenzelm@44872
    64
  done
nipkow@31719
    65
paulson@54713
    66
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
nipkow@31952
    67
  apply (simp add: gcd_commute_nat [of "fib m"])
paulson@54713
    68
  apply (cases m)
paulson@54713
    69
  apply (auto simp add: fib_add)
nipkow@31952
    70
  apply (subst gcd_commute_nat)
haftmann@57512
    71
  apply (subst mult.commute)
paulson@54713
    72
  apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
wenzelm@44872
    73
  done
nipkow@31719
    74
paulson@54713
    75
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
nipkow@31719
    76
    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
paulson@54713
    77
  by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
nipkow@31719
    78
paulson@54713
    79
lemma gcd_fib_mod: "0 < m \<Longrightarrow>
nipkow@31719
    80
    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
nipkow@31719
    81
proof (induct n rule: less_induct)
nipkow@31719
    82
  case (less n)
nipkow@31719
    83
  from less.prems have pos_m: "0 < m" .
nipkow@31719
    84
  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
nipkow@31719
    85
  proof (cases "m < n")
wenzelm@44872
    86
    case True
wenzelm@44872
    87
    then have "m \<le> n" by auto
nipkow@31719
    88
    with pos_m have pos_n: "0 < n" by auto
wenzelm@44872
    89
    with pos_m `m < n` have diff: "n - m < n" by auto
nipkow@31719
    90
    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
wenzelm@44872
    91
      by (simp add: mod_if [of n]) (insert `m < n`, auto)
wenzelm@44872
    92
    also have "\<dots> = gcd (fib m)  (fib (n - m))"
nipkow@31719
    93
      by (simp add: less.hyps diff pos_m)
wenzelm@44872
    94
    also have "\<dots> = gcd (fib m) (fib n)"
paulson@54713
    95
      by (simp add: gcd_fib_diff `m \<le> n`)
nipkow@31719
    96
    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
nipkow@31719
    97
  next
wenzelm@44872
    98
    case False
wenzelm@44872
    99
    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
wenzelm@44872
   100
      by (cases "m = n") auto
nipkow@31719
   101
  qed
nipkow@31719
   102
qed
nipkow@31719
   103
paulson@54713
   104
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
nipkow@31719
   105
    -- {* Law 6.111 *}
paulson@54713
   106
  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
nipkow@31719
   107
nipkow@31952
   108
theorem fib_mult_eq_setsum_nat:
nipkow@31719
   109
    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
paulson@54713
   110
  by (induct n rule: nat.induct) (auto simp add:  field_simps)
nipkow@31719
   111
nipkow@31719
   112
end
paulson@54713
   113