src/HOL/Isar_Examples/Fibonacci.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 57512 cc97b347b301
child 58614 7338eb25226c
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
wenzelm@33026
     1
(*  Title:      HOL/Isar_Examples/Fibonacci.thy
wenzelm@8051
     2
    Author:     Gertrud Bauer
wenzelm@8051
     3
    Copyright   1999 Technische Universitaet Muenchen
wenzelm@8051
     4
haftmann@54892
     5
The Fibonacci function.  Original
wenzelm@8051
     6
tactic script by Lawrence C Paulson.
wenzelm@8051
     7
wenzelm@8051
     8
Fibonacci numbers: proofs of laws taken from
wenzelm@8051
     9
wenzelm@8051
    10
  R. L. Graham, D. E. Knuth, O. Patashnik.
wenzelm@8051
    11
  Concrete Mathematics.
wenzelm@8051
    12
  (Addison-Wesley, 1989)
wenzelm@8051
    13
*)
wenzelm@8051
    14
wenzelm@10007
    15
header {* Fib and Gcd commute *}
wenzelm@8051
    16
haftmann@27366
    17
theory Fibonacci
wenzelm@37672
    18
imports "../Number_Theory/Primes"
haftmann@27366
    19
begin
wenzelm@8051
    20
wenzelm@37671
    21
text_raw {* \footnote{Isar version by Gertrud Bauer.  Original tactic
wenzelm@37671
    22
  script by Larry Paulson.  A few proofs of laws taken from
wenzelm@37671
    23
  \cite{Concrete-Math}.} *}
wenzelm@8051
    24
wenzelm@8051
    25
wenzelm@37672
    26
declare One_nat_def [simp]
wenzelm@37672
    27
wenzelm@37672
    28
wenzelm@10007
    29
subsection {* Fibonacci numbers *}
wenzelm@8051
    30
haftmann@27366
    31
fun fib :: "nat \<Rightarrow> nat" where
wenzelm@18153
    32
  "fib 0 = 0"
wenzelm@37671
    33
| "fib (Suc 0) = 1"
wenzelm@37671
    34
| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
wenzelm@8051
    35
wenzelm@37672
    36
lemma [simp]: "fib (Suc n) > 0"
wenzelm@18153
    37
  by (induct n rule: fib.induct) simp_all
wenzelm@8051
    38
wenzelm@8051
    39
wenzelm@10007
    40
text {* Alternative induction rule. *}
wenzelm@8051
    41
wenzelm@8304
    42
theorem fib_induct:
wenzelm@55640
    43
  fixes n :: nat
wenzelm@55640
    44
  shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
wenzelm@18153
    45
  by (induct rule: fib.induct) simp_all
wenzelm@8051
    46
wenzelm@8051
    47
wenzelm@10007
    48
subsection {* Fib and gcd commute *}
wenzelm@8051
    49
wenzelm@10007
    50
text {* A few laws taken from \cite{Concrete-Math}. *}
wenzelm@8051
    51
wenzelm@9659
    52
lemma fib_add:
wenzelm@8051
    53
  "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@9659
    54
  (is "?P n")
wenzelm@10007
    55
  -- {* see \cite[page 280]{Concrete-Math} *}
wenzelm@11809
    56
proof (induct n rule: fib_induct)
wenzelm@10007
    57
  show "?P 0" by simp
wenzelm@10007
    58
  show "?P 1" by simp
wenzelm@10007
    59
  fix n
wenzelm@11704
    60
  have "fib (n + 2 + k + 1)
wenzelm@10007
    61
    = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
wenzelm@10007
    62
  also assume "fib (n + k + 1)
wenzelm@8051
    63
    = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
    64
      (is " _ = ?R1")
wenzelm@10007
    65
  also assume "fib (n + 1 + k + 1)
wenzelm@8051
    66
    = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
wenzelm@10007
    67
      (is " _ = ?R2")
wenzelm@10007
    68
  also have "?R1 + ?R2
wenzelm@11704
    69
    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
wenzelm@10007
    70
    by (simp add: add_mult_distrib2)
wenzelm@11704
    71
  finally show "?P (n + 2)" .
wenzelm@10007
    72
qed
wenzelm@8051
    73
haftmann@27556
    74
lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
wenzelm@11809
    75
proof (induct n rule: fib_induct)
wenzelm@10007
    76
  show "?P 0" by simp
wenzelm@10007
    77
  show "?P 1" by simp
wenzelm@10007
    78
  fix n
wenzelm@11704
    79
  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
wenzelm@10007
    80
    by simp
wenzelm@55640
    81
  also have "\<dots> = fib (n + 2) + fib (n + 1)"
wenzelm@55640
    82
    by simp
wenzelm@55640
    83
  also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
wenzelm@37672
    84
    by (rule gcd_add2_nat)
wenzelm@55640
    85
  also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
wenzelm@37672
    86
    by (simp add: gcd_commute_nat)
wenzelm@55640
    87
  also assume "\<dots> = 1"
wenzelm@11704
    88
  finally show "?P (n + 2)" .
wenzelm@10007
    89
qed
wenzelm@8051
    90
wenzelm@55640
    91
lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
wenzelm@10007
    92
proof -
wenzelm@10007
    93
  assume "0 < n"
haftmann@27556
    94
  then have "gcd (n * k + m) n = gcd n (m mod n)"
haftmann@57512
    95
    by (simp add: gcd_non_0_nat add.commute)
wenzelm@55640
    96
  also from `0 < n` have "\<dots> = gcd m n"
wenzelm@55640
    97
    by (simp add: gcd_non_0_nat)
wenzelm@10007
    98
  finally show ?thesis .
wenzelm@10007
    99
qed
wenzelm@8051
   100
haftmann@27556
   101
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
wenzelm@10007
   102
proof (cases m)
wenzelm@18153
   103
  case 0
wenzelm@18153
   104
  then show ?thesis by simp
wenzelm@10007
   105
next
wenzelm@18153
   106
  case (Suc k)
haftmann@27556
   107
  then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
wenzelm@37672
   108
    by (simp add: gcd_commute_nat)
wenzelm@10007
   109
  also have "fib (n + k + 1)
wenzelm@37671
   110
      = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
   111
    by (rule fib_add)
wenzelm@55640
   112
  also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
wenzelm@10007
   113
    by (simp add: gcd_mult_add)
wenzelm@55640
   114
  also have "\<dots> = gcd (fib n) (fib (k + 1))"
wenzelm@37672
   115
    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
wenzelm@55640
   116
  also have "\<dots> = gcd (fib m) (fib n)"
wenzelm@37672
   117
    using Suc by (simp add: gcd_commute_nat)
wenzelm@10007
   118
  finally show ?thesis .
wenzelm@10007
   119
qed
wenzelm@8051
   120
wenzelm@9659
   121
lemma gcd_fib_diff:
wenzelm@55640
   122
  assumes "m \<le> n"
haftmann@27556
   123
  shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
wenzelm@10007
   124
proof -
haftmann@27556
   125
  have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
wenzelm@10007
   126
    by (simp add: gcd_fib_add)
wenzelm@55640
   127
  also from `m \<le> n` have "n - m + m = n"
wenzelm@55640
   128
    by simp
wenzelm@10007
   129
  finally show ?thesis .
wenzelm@10007
   130
qed
wenzelm@8051
   131
wenzelm@9659
   132
lemma gcd_fib_mod:
wenzelm@18241
   133
  assumes "0 < m"
haftmann@27556
   134
  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
wenzelm@18153
   135
proof (induct n rule: nat_less_induct)
wenzelm@18153
   136
  case (1 n) note hyp = this
wenzelm@18153
   137
  show ?case
wenzelm@18153
   138
  proof -
wenzelm@18153
   139
    have "n mod m = (if n < m then n else (n - m) mod m)"
wenzelm@18153
   140
      by (rule mod_if)
wenzelm@55640
   141
    also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
wenzelm@18153
   142
    proof (cases "n < m")
wenzelm@55640
   143
      case True
wenzelm@55640
   144
      then show ?thesis by simp
wenzelm@18153
   145
    next
wenzelm@55640
   146
      case False
wenzelm@55640
   147
      then have "m \<le> n" by simp
wenzelm@55640
   148
      from `0 < m` and False have "n - m < n"
wenzelm@55640
   149
        by simp
haftmann@27556
   150
      with hyp have "gcd (fib m) (fib ((n - m) mod m))
wenzelm@37671
   151
          = gcd (fib m) (fib (n - m))" by simp
wenzelm@55640
   152
      also have "\<dots> = gcd (fib m) (fib n)"
wenzelm@55656
   153
        using `m \<le> n` by (rule gcd_fib_diff)
haftmann@27556
   154
      finally have "gcd (fib m) (fib ((n - m) mod m)) =
wenzelm@37671
   155
          gcd (fib m) (fib n)" .
wenzelm@18153
   156
      with False show ?thesis by simp
wenzelm@10408
   157
    qed
wenzelm@18153
   158
    finally show ?thesis .
wenzelm@10007
   159
  qed
wenzelm@10007
   160
qed
wenzelm@8051
   161
haftmann@27556
   162
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
wenzelm@37672
   163
proof (induct m n rule: gcd_nat_induct)
wenzelm@55640
   164
  fix m
wenzelm@55640
   165
  show "fib (gcd m 0) = gcd (fib m) (fib 0)"
wenzelm@55640
   166
    by simp
wenzelm@55640
   167
  fix n :: nat
wenzelm@55640
   168
  assume n: "0 < n"
wenzelm@55640
   169
  then have "gcd m n = gcd n (m mod n)"
wenzelm@55640
   170
    by (simp add: gcd_non_0_nat)
wenzelm@55640
   171
  also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
wenzelm@55640
   172
  also from n have "\<dots> = gcd (fib n) (fib m)"
wenzelm@55640
   173
    by (rule gcd_fib_mod)
wenzelm@55640
   174
  also have "\<dots> = gcd (fib m) (fib n)"
wenzelm@55640
   175
    by (rule gcd_commute_nat)
haftmann@27556
   176
  finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
wenzelm@10007
   177
qed
wenzelm@8051
   178
wenzelm@10007
   179
end