src/HOL/Isar_examples/Fibonacci.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 18153 a084aa91f701
permissions -rw-r--r--
Constant "If" is now local
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@8051
    31
 "fib 0 = 0"
wenzelm@11701
    32
 "fib (Suc 0) = 1"
wenzelm@10007
    33
 "fib (Suc (Suc x)) = fib x + fib (Suc x)"
wenzelm@8051
    34
wenzelm@10007
    35
lemma [simp]: "0 < fib (Suc n)"
wenzelm@10007
    36
  by (induct n rule: fib.induct) (simp+)
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@10007
    43
  by (induct rule: fib.induct, simp+)
wenzelm@8051
    44
wenzelm@8051
    45
wenzelm@8051
    46
wenzelm@10007
    47
subsection {* Fib and gcd commute *}
wenzelm@8051
    48
wenzelm@10007
    49
text {* A few laws taken from \cite{Concrete-Math}. *}
wenzelm@8051
    50
wenzelm@9659
    51
lemma fib_add:
wenzelm@8051
    52
  "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@9659
    53
  (is "?P n")
wenzelm@10007
    54
  -- {* see \cite[page 280]{Concrete-Math} *}
wenzelm@11809
    55
proof (induct n rule: fib_induct)
wenzelm@10007
    56
  show "?P 0" by simp
wenzelm@10007
    57
  show "?P 1" by simp
wenzelm@10007
    58
  fix n
wenzelm@11704
    59
  have "fib (n + 2 + k + 1)
wenzelm@10007
    60
    = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
wenzelm@10007
    61
  also assume "fib (n + k + 1)
wenzelm@8051
    62
    = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
    63
      (is " _ = ?R1")
wenzelm@10007
    64
  also assume "fib (n + 1 + k + 1)
wenzelm@8051
    65
    = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
wenzelm@10007
    66
      (is " _ = ?R2")
wenzelm@10007
    67
  also have "?R1 + ?R2
wenzelm@11704
    68
    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
wenzelm@10007
    69
    by (simp add: add_mult_distrib2)
wenzelm@11704
    70
  finally show "?P (n + 2)" .
wenzelm@10007
    71
qed
wenzelm@8051
    72
wenzelm@10007
    73
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
wenzelm@11809
    74
proof (induct n rule: fib_induct)
wenzelm@10007
    75
  show "?P 0" by simp
wenzelm@10007
    76
  show "?P 1" by simp
wenzelm@10007
    77
  fix n
wenzelm@11704
    78
  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
wenzelm@10007
    79
    by simp
wenzelm@11704
    80
  also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
wenzelm@10007
    81
    by (simp only: gcd_add2')
wenzelm@10007
    82
  also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
wenzelm@10007
    83
    by (simp add: gcd_commute)
wenzelm@10007
    84
  also assume "... = 1"
wenzelm@11704
    85
  finally show "?P (n + 2)" .
wenzelm@10007
    86
qed
wenzelm@8051
    87
wenzelm@10007
    88
lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
wenzelm@10007
    89
proof -
wenzelm@10007
    90
  assume "0 < n"
wenzelm@10007
    91
  hence "gcd (n * k + m, n) = gcd (n, m mod n)"
wenzelm@10007
    92
    by (simp add: gcd_non_0 add_commute)
wenzelm@10007
    93
  also have "... = gcd (m, n)" by (simp! add: gcd_non_0)
wenzelm@10007
    94
  finally show ?thesis .
wenzelm@10007
    95
qed
wenzelm@8051
    96
wenzelm@10007
    97
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
wenzelm@10007
    98
proof (cases m)
wenzelm@10007
    99
  assume "m = 0"
wenzelm@10007
   100
  thus ?thesis by simp
wenzelm@10007
   101
next
wenzelm@10007
   102
  fix k assume "m = Suc k"
wenzelm@10007
   103
  hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
wenzelm@10007
   104
    by (simp add: gcd_commute)
wenzelm@10007
   105
  also have "fib (n + k + 1)
wenzelm@10007
   106
    = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
   107
    by (rule fib_add)
wenzelm@10007
   108
  also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
wenzelm@10007
   109
    by (simp add: gcd_mult_add)
wenzelm@10007
   110
  also have "... = gcd (fib n, fib (k + 1))"
wenzelm@10007
   111
    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
wenzelm@10007
   112
  also have "... = gcd (fib m, fib n)"
wenzelm@10007
   113
    by (simp! add: gcd_commute)
wenzelm@10007
   114
  finally show ?thesis .
wenzelm@10007
   115
qed
wenzelm@8051
   116
wenzelm@9659
   117
lemma gcd_fib_diff:
wenzelm@10007
   118
  "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
wenzelm@10007
   119
proof -
wenzelm@10007
   120
  assume "m <= n"
wenzelm@10007
   121
  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
wenzelm@10007
   122
    by (simp add: gcd_fib_add)
wenzelm@10007
   123
  also have "n - m + m = n" by (simp!)
wenzelm@10007
   124
  finally show ?thesis .
wenzelm@10007
   125
qed
wenzelm@8051
   126
wenzelm@9659
   127
lemma gcd_fib_mod:
wenzelm@10007
   128
  "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
wenzelm@10408
   129
proof -
wenzelm@8051
   130
  assume m: "0 < m"
wenzelm@10408
   131
  show ?thesis
wenzelm@10408
   132
  proof (induct n rule: nat_less_induct)
wenzelm@10408
   133
    fix n
wenzelm@10408
   134
    assume hyp: "ALL ma. ma < n
wenzelm@10408
   135
      --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
wenzelm@10408
   136
    show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
wenzelm@10408
   137
    proof -
wenzelm@10408
   138
      have "n mod m = (if n < m then n else (n - m) mod m)"
wenzelm@10408
   139
	by (rule mod_if)
wenzelm@10408
   140
      also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
wenzelm@10408
   141
      proof cases
wenzelm@10408
   142
	assume "n < m" thus ?thesis by simp
wenzelm@10408
   143
      next
wenzelm@10408
   144
	assume not_lt: "~ n < m" hence le: "m <= n" by simp
nipkow@15439
   145
	have "n - m < n" by (simp!)
wenzelm@10408
   146
	with hyp have "gcd (fib m, fib ((n - m) mod m))
wenzelm@10408
   147
	  = gcd (fib m, fib (n - m))" by simp
wenzelm@10408
   148
	also from le have "... = gcd (fib m, fib n)"
wenzelm@10408
   149
	  by (rule gcd_fib_diff)
wenzelm@10408
   150
	finally have "gcd (fib m, fib ((n - m) mod m)) =
wenzelm@10408
   151
	  gcd (fib m, fib n)" .
wenzelm@10408
   152
	with not_lt show ?thesis by simp
wenzelm@10408
   153
      qed
wenzelm@10408
   154
      finally show ?thesis .
wenzelm@10408
   155
    qed
wenzelm@10007
   156
  qed
wenzelm@10007
   157
qed
wenzelm@8051
   158
wenzelm@8051
   159
wenzelm@10007
   160
theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
wenzelm@11809
   161
proof (induct m n rule: gcd_induct)
wenzelm@10007
   162
  fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
wenzelm@10007
   163
  fix n :: nat assume n: "0 < n"
wenzelm@10007
   164
  hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
wenzelm@10007
   165
  also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
wenzelm@10007
   166
  also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
wenzelm@10007
   167
  also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
wenzelm@10007
   168
  finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
wenzelm@10007
   169
qed
wenzelm@8051
   170
wenzelm@10007
   171
end