src/HOL/Isar_examples/Fibonacci.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 18241 afdba6b3e383
child 27366 d0cda1ea705e
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
wenzelm@8051
     1
(*  Title:      HOL/Isar_examples/Fibonacci.thy
wenzelm@8051
     2
    ID:         $Id$
wenzelm@8051
     3
    Author:     Gertrud Bauer
wenzelm@8051
     4
    Copyright   1999 Technische Universitaet Muenchen
wenzelm@8051
     5
wenzelm@8051
     6
The Fibonacci function.  Demonstrates the use of recdef.  Original
wenzelm@8051
     7
tactic script by Lawrence C Paulson.
wenzelm@8051
     8
wenzelm@8051
     9
Fibonacci numbers: proofs of laws taken from
wenzelm@8051
    10
wenzelm@8051
    11
  R. L. Graham, D. E. Knuth, O. Patashnik.
wenzelm@8051
    12
  Concrete Mathematics.
wenzelm@8051
    13
  (Addison-Wesley, 1989)
wenzelm@8051
    14
*)
wenzelm@8051
    15
wenzelm@10007
    16
header {* Fib and Gcd commute *}
wenzelm@8051
    17
haftmann@16417
    18
theory Fibonacci imports Primes begin
wenzelm@8051
    19
wenzelm@8051
    20
text_raw {*
wenzelm@8051
    21
 \footnote{Isar version by Gertrud Bauer.  Original tactic script by
wenzelm@8052
    22
 Larry Paulson.  A few proofs of laws taken from
wenzelm@8051
    23
 \cite{Concrete-Math}.}
wenzelm@10007
    24
*}
wenzelm@8051
    25
wenzelm@8051
    26
wenzelm@10007
    27
subsection {* Fibonacci numbers *}
wenzelm@8051
    28
wenzelm@10007
    29
consts fib :: "nat => nat"
wenzelm@8051
    30
recdef fib less_than
wenzelm@18153
    31
  "fib 0 = 0"
wenzelm@18153
    32
  "fib (Suc 0) = 1"
wenzelm@18153
    33
  "fib (Suc (Suc x)) = fib x + fib (Suc x)"
wenzelm@8051
    34
wenzelm@10007
    35
lemma [simp]: "0 < fib (Suc n)"
wenzelm@18153
    36
  by (induct n rule: fib.induct) simp_all
wenzelm@8051
    37
wenzelm@8051
    38
wenzelm@10007
    39
text {* Alternative induction rule. *}
wenzelm@8051
    40
wenzelm@8304
    41
theorem fib_induct:
wenzelm@11704
    42
    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
wenzelm@18153
    43
  by (induct rule: fib.induct) simp_all
wenzelm@8051
    44
wenzelm@8051
    45
wenzelm@10007
    46
subsection {* Fib and gcd commute *}
wenzelm@8051
    47
wenzelm@10007
    48
text {* A few laws taken from \cite{Concrete-Math}. *}
wenzelm@8051
    49
wenzelm@9659
    50
lemma fib_add:
wenzelm@8051
    51
  "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@9659
    52
  (is "?P n")
wenzelm@10007
    53
  -- {* see \cite[page 280]{Concrete-Math} *}
wenzelm@11809
    54
proof (induct n rule: fib_induct)
wenzelm@10007
    55
  show "?P 0" by simp
wenzelm@10007
    56
  show "?P 1" by simp
wenzelm@10007
    57
  fix n
wenzelm@11704
    58
  have "fib (n + 2 + k + 1)
wenzelm@10007
    59
    = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
wenzelm@10007
    60
  also assume "fib (n + k + 1)
wenzelm@8051
    61
    = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
    62
      (is " _ = ?R1")
wenzelm@10007
    63
  also assume "fib (n + 1 + k + 1)
wenzelm@8051
    64
    = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
wenzelm@10007
    65
      (is " _ = ?R2")
wenzelm@10007
    66
  also have "?R1 + ?R2
wenzelm@11704
    67
    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
wenzelm@10007
    68
    by (simp add: add_mult_distrib2)
wenzelm@11704
    69
  finally show "?P (n + 2)" .
wenzelm@10007
    70
qed
wenzelm@8051
    71
wenzelm@10007
    72
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
wenzelm@11809
    73
proof (induct n rule: fib_induct)
wenzelm@10007
    74
  show "?P 0" by simp
wenzelm@10007
    75
  show "?P 1" by simp
wenzelm@10007
    76
  fix n
wenzelm@11704
    77
  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
wenzelm@10007
    78
    by simp
wenzelm@11704
    79
  also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
wenzelm@10007
    80
    by (simp only: gcd_add2')
wenzelm@10007
    81
  also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
wenzelm@10007
    82
    by (simp add: gcd_commute)
wenzelm@10007
    83
  also assume "... = 1"
wenzelm@11704
    84
  finally show "?P (n + 2)" .
wenzelm@10007
    85
qed
wenzelm@8051
    86
wenzelm@10007
    87
lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
wenzelm@10007
    88
proof -
wenzelm@10007
    89
  assume "0 < n"
wenzelm@18153
    90
  then have "gcd (n * k + m, n) = gcd (n, m mod n)"
wenzelm@10007
    91
    by (simp add: gcd_non_0 add_commute)
wenzelm@18153
    92
  also from `0 < n` have "... = gcd (m, n)" by (simp add: gcd_non_0)
wenzelm@10007
    93
  finally show ?thesis .
wenzelm@10007
    94
qed
wenzelm@8051
    95
wenzelm@10007
    96
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
wenzelm@10007
    97
proof (cases m)
wenzelm@18153
    98
  case 0
wenzelm@18153
    99
  then show ?thesis by simp
wenzelm@10007
   100
next
wenzelm@18153
   101
  case (Suc k)
wenzelm@18153
   102
  then have "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
wenzelm@10007
   103
    by (simp add: gcd_commute)
wenzelm@10007
   104
  also have "fib (n + k + 1)
wenzelm@10007
   105
    = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
   106
    by (rule fib_add)
wenzelm@10007
   107
  also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
wenzelm@10007
   108
    by (simp add: gcd_mult_add)
wenzelm@10007
   109
  also have "... = gcd (fib n, fib (k + 1))"
wenzelm@10007
   110
    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
wenzelm@10007
   111
  also have "... = gcd (fib m, fib n)"
wenzelm@18153
   112
    using Suc by (simp add: gcd_commute)
wenzelm@10007
   113
  finally show ?thesis .
wenzelm@10007
   114
qed
wenzelm@8051
   115
wenzelm@9659
   116
lemma gcd_fib_diff:
wenzelm@18153
   117
  assumes "m <= n"
wenzelm@18153
   118
  shows "gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
wenzelm@10007
   119
proof -
wenzelm@10007
   120
  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
wenzelm@10007
   121
    by (simp add: gcd_fib_add)
wenzelm@18153
   122
  also from `m <= n` have "n - m + m = n" by simp
wenzelm@10007
   123
  finally show ?thesis .
wenzelm@10007
   124
qed
wenzelm@8051
   125
wenzelm@9659
   126
lemma gcd_fib_mod:
wenzelm@18241
   127
  assumes "0 < m"
wenzelm@18153
   128
  shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
wenzelm@18153
   129
proof (induct n rule: nat_less_induct)
wenzelm@18153
   130
  case (1 n) note hyp = this
wenzelm@18153
   131
  show ?case
wenzelm@18153
   132
  proof -
wenzelm@18153
   133
    have "n mod m = (if n < m then n else (n - m) mod m)"
wenzelm@18153
   134
      by (rule mod_if)
wenzelm@18153
   135
    also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
wenzelm@18153
   136
    proof (cases "n < m")
wenzelm@18153
   137
      case True then show ?thesis by simp
wenzelm@18153
   138
    next
wenzelm@18153
   139
      case False then have "m <= n" by simp
wenzelm@18241
   140
      from `0 < m` and False have "n - m < n" by simp
wenzelm@18153
   141
      with hyp have "gcd (fib m, fib ((n - m) mod m))
wenzelm@18153
   142
        = gcd (fib m, fib (n - m))" by simp
wenzelm@18153
   143
      also have "... = gcd (fib m, fib n)"
wenzelm@18153
   144
        using `m <= n` by (rule gcd_fib_diff)
wenzelm@18153
   145
      finally have "gcd (fib m, fib ((n - m) mod m)) =
wenzelm@18153
   146
        gcd (fib m, fib n)" .
wenzelm@18153
   147
      with False show ?thesis by simp
wenzelm@10408
   148
    qed
wenzelm@18153
   149
    finally show ?thesis .
wenzelm@10007
   150
  qed
wenzelm@10007
   151
qed
wenzelm@8051
   152
wenzelm@8051
   153
wenzelm@10007
   154
theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
wenzelm@11809
   155
proof (induct m n rule: gcd_induct)
wenzelm@10007
   156
  fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
wenzelm@10007
   157
  fix n :: nat assume n: "0 < n"
wenzelm@18153
   158
  then have "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
wenzelm@10007
   159
  also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
wenzelm@10007
   160
  also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
wenzelm@10007
   161
  also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
wenzelm@10007
   162
  finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
wenzelm@10007
   163
qed
wenzelm@8051
   164
wenzelm@10007
   165
end