src/HOL/Number_Theory/Fib.thy
author wenzelm
Thu May 26 17:51:22 2016 +0200 (2016-05-26)
changeset 63167 0909deb8059b
parent 62429 25271ff79171
child 64267 b9a1486e79be
permissions -rw-r--r--
isabelle update_cartouches -c -t;
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
wenzelm@60527
     6
section \<open>The fibonacci function\<close>
nipkow@31719
     7
nipkow@31719
     8
theory Fib
wenzelm@60527
     9
imports Main GCD Binomial
nipkow@31719
    10
begin
nipkow@31719
    11
nipkow@31719
    12
wenzelm@60526
    13
subsection \<open>Fibonacci numbers\<close>
nipkow@31719
    14
paulson@54713
    15
fun fib :: "nat \<Rightarrow> nat"
nipkow@31719
    16
where
wenzelm@60527
    17
  fib0: "fib 0 = 0"
wenzelm@60527
    18
| fib1: "fib (Suc 0) = 1"
wenzelm@60527
    19
| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
wenzelm@60527
    20
nipkow@31719
    21
wenzelm@60526
    22
subsection \<open>Basic Properties\<close>
nipkow@31719
    23
paulson@54713
    24
lemma fib_1 [simp]: "fib (1::nat) = 1"
paulson@54713
    25
  by (metis One_nat_def fib1)
nipkow@31719
    26
paulson@54713
    27
lemma fib_2 [simp]: "fib (2::nat) = 1"
paulson@54713
    28
  using fib.simps(3) [of 0]
paulson@54713
    29
  by (simp add: numeral_2_eq_2)
nipkow@31719
    30
paulson@54713
    31
lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
paulson@54713
    32
  by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
nipkow@31719
    33
paulson@54713
    34
lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
paulson@54713
    35
  by (induct n rule: fib.induct) (auto simp add: field_simps)
nipkow@31719
    36
paulson@54713
    37
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
paulson@54713
    38
  by (induct n rule: fib.induct) (auto simp add: )
nipkow@31719
    39
wenzelm@60527
    40
wenzelm@60526
    41
subsection \<open>A Few Elementary Results\<close>
lp15@60141
    42
wenzelm@60526
    43
text \<open>
nipkow@31719
    44
  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
nipkow@31719
    45
  much easier using integers, not natural numbers!
wenzelm@60526
    46
\<close>
nipkow@31719
    47
paulson@54713
    48
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
wenzelm@60527
    49
  by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
nipkow@31719
    50
paulson@54713
    51
lemma fib_Cassini_nat:
wenzelm@60527
    52
  "fib (Suc (Suc n)) * fib n =
wenzelm@60527
    53
     (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
lp15@61649
    54
  using fib_Cassini_int [of n]  by (auto simp del: of_nat_mult of_nat_power)
nipkow@31719
    55
nipkow@31719
    56
wenzelm@60526
    57
subsection \<open>Law 6.111 of Concrete Mathematics\<close>
nipkow@31719
    58
paulson@54713
    59
lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
paulson@54713
    60
  apply (induct n rule: fib.induct)
nipkow@31719
    61
  apply auto
eberlm@62429
    62
  apply (metis gcd_add1 add.commute)
wenzelm@44872
    63
  done
nipkow@31719
    64
paulson@54713
    65
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
haftmann@62348
    66
  apply (simp add: gcd.commute [of "fib m"])
paulson@54713
    67
  apply (cases m)
paulson@54713
    68
  apply (auto simp add: fib_add)
haftmann@62348
    69
  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
eberlm@62429
    70
    gcd_add_mult gcd_mult_cancel gcd.commute)
wenzelm@44872
    71
  done
nipkow@31719
    72
wenzelm@60527
    73
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
paulson@54713
    74
  by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
nipkow@31719
    75
wenzelm@60527
    76
lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
nipkow@31719
    77
proof (induct n rule: less_induct)
nipkow@31719
    78
  case (less n)
nipkow@31719
    79
  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
nipkow@31719
    80
  proof (cases "m < n")
wenzelm@44872
    81
    case True
wenzelm@44872
    82
    then have "m \<le> n" by auto
wenzelm@60527
    83
    with \<open>0 < m\<close> have pos_n: "0 < n" by auto
wenzelm@60527
    84
    with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
nipkow@31719
    85
    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
wenzelm@60526
    86
      by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
wenzelm@44872
    87
    also have "\<dots> = gcd (fib m)  (fib (n - m))"
wenzelm@60527
    88
      by (simp add: less.hyps diff \<open>0 < m\<close>)
wenzelm@44872
    89
    also have "\<dots> = gcd (fib m) (fib n)"
wenzelm@60526
    90
      by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
nipkow@31719
    91
    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
nipkow@31719
    92
  next
wenzelm@44872
    93
    case False
wenzelm@44872
    94
    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
wenzelm@44872
    95
      by (cases "m = n") auto
nipkow@31719
    96
  qed
nipkow@31719
    97
qed
nipkow@31719
    98
paulson@54713
    99
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
wenzelm@63167
   100
    \<comment> \<open>Law 6.111\<close>
haftmann@62348
   101
  by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
nipkow@31719
   102
wenzelm@60527
   103
theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
paulson@54713
   104
  by (induct n rule: nat.induct) (auto simp add:  field_simps)
nipkow@31719
   105
wenzelm@60527
   106
wenzelm@60526
   107
subsection \<open>Fibonacci and Binomial Coefficients\<close>
lp15@60141
   108
lp15@60141
   109
lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
lp15@60141
   110
  by (induct n) auto
lp15@60141
   111
lp15@60141
   112
lemma setsum_choose_drop_zero:
lp15@60141
   113
    "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
lp15@60141
   114
  by (rule trans [OF setsum.cong setsum_drop_zero]) auto
lp15@60141
   115
wenzelm@60527
   116
lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
lp15@60141
   117
proof (induct n rule: fib.induct)
wenzelm@60527
   118
  case 1
wenzelm@60527
   119
  show ?case by simp
lp15@60141
   120
next
wenzelm@60527
   121
  case 2
wenzelm@60527
   122
  show ?case by simp
lp15@60141
   123
next
lp15@60141
   124
  case (3 n)
lp15@60141
   125
  have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
lp15@60141
   126
        (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
lp15@60141
   127
    by (rule setsum.cong) (simp_all add: choose_reduce_nat)
wenzelm@60527
   128
  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
lp15@60141
   129
                   (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
lp15@60141
   130
    by (simp add: setsum.distrib)
wenzelm@60527
   131
  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
lp15@60141
   132
                   (\<Sum>j = 0..n. n - j choose j)"
lp15@60141
   133
    by (metis setsum_choose_drop_zero)
lp15@60141
   134
  finally show ?case using 3
lp15@60141
   135
    by simp
lp15@60141
   136
qed
lp15@60141
   137
nipkow@31719
   138
end
paulson@54713
   139