src/HOL/Isar_Examples/Fibonacci.thy
author haftmann
Sat Nov 11 18:41:08 2017 +0000 (19 months ago)
changeset 67051 e7e54a0b9197
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
dedicated definition for coprimality
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@58882
    15
section \<open>Fib and Gcd commute\<close>
wenzelm@8051
    16
haftmann@27366
    17
theory Fibonacci
wenzelm@66453
    18
  imports "HOL-Computational_Algebra.Primes"
haftmann@27366
    19
begin
wenzelm@8051
    20
wenzelm@61932
    21
text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
wenzelm@61932
    22
  Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
wenzelm@8051
    23
wenzelm@58614
    24
subsection \<open>Fibonacci numbers\<close>
wenzelm@8051
    25
wenzelm@63095
    26
fun fib :: "nat \<Rightarrow> nat"
wenzelm@63585
    27
  where
wenzelm@63585
    28
    "fib 0 = 0"
wenzelm@63585
    29
  | "fib (Suc 0) = 1"
wenzelm@63585
    30
  | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
wenzelm@8051
    31
wenzelm@37672
    32
lemma [simp]: "fib (Suc n) > 0"
wenzelm@18153
    33
  by (induct n rule: fib.induct) simp_all
wenzelm@8051
    34
wenzelm@8051
    35
wenzelm@58614
    36
text \<open>Alternative induction rule.\<close>
wenzelm@8051
    37
wenzelm@63095
    38
theorem fib_induct: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
wenzelm@63095
    39
  for n :: nat
wenzelm@18153
    40
  by (induct rule: fib.induct) simp_all
wenzelm@8051
    41
wenzelm@8051
    42
wenzelm@58614
    43
subsection \<open>Fib and gcd commute\<close>
wenzelm@8051
    44
wenzelm@58614
    45
text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
wenzelm@8051
    46
wenzelm@63095
    47
lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@9659
    48
  (is "?P n")
wenzelm@61799
    49
  \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
wenzelm@11809
    50
proof (induct n rule: fib_induct)
wenzelm@10007
    51
  show "?P 0" by simp
wenzelm@10007
    52
  show "?P 1" by simp
wenzelm@10007
    53
  fix n
wenzelm@11704
    54
  have "fib (n + 2 + k + 1)
wenzelm@10007
    55
    = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
wenzelm@63095
    56
  also assume "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" (is " _ = ?R1")
wenzelm@63095
    57
  also assume "fib (n + 1 + k + 1) = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
wenzelm@63095
    58
    (is " _ = ?R2")
wenzelm@63095
    59
  also have "?R1 + ?R2 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
wenzelm@10007
    60
    by (simp add: add_mult_distrib2)
wenzelm@11704
    61
  finally show "?P (n + 2)" .
wenzelm@10007
    62
qed
wenzelm@8051
    63
haftmann@67051
    64
lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
wenzelm@63095
    65
  (is "?P n")
wenzelm@11809
    66
proof (induct n rule: fib_induct)
wenzelm@10007
    67
  show "?P 0" by simp
wenzelm@10007
    68
  show "?P 1" by simp
wenzelm@10007
    69
  fix n
haftmann@67051
    70
  assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
wenzelm@11704
    71
  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
wenzelm@10007
    72
    by simp
wenzelm@55640
    73
  also have "\<dots> = fib (n + 2) + fib (n + 1)"
wenzelm@55640
    74
    by simp
wenzelm@55640
    75
  also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
eberlm@62429
    76
    by (rule gcd_add2)
wenzelm@55640
    77
  also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
haftmann@62348
    78
    by (simp add: gcd.commute)
haftmann@67051
    79
  also have "\<dots> = 1"
haftmann@67051
    80
    using P by simp
haftmann@67051
    81
  finally show "?P (n + 2)"
haftmann@67051
    82
    by (simp add: coprime_iff_gcd_eq_1)
wenzelm@10007
    83
qed
wenzelm@8051
    84
wenzelm@55640
    85
lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
wenzelm@10007
    86
proof -
wenzelm@10007
    87
  assume "0 < n"
haftmann@27556
    88
  then have "gcd (n * k + m) n = gcd n (m mod n)"
haftmann@57512
    89
    by (simp add: gcd_non_0_nat add.commute)
wenzelm@58614
    90
  also from \<open>0 < n\<close> have "\<dots> = gcd m n"
wenzelm@55640
    91
    by (simp add: gcd_non_0_nat)
wenzelm@10007
    92
  finally show ?thesis .
wenzelm@10007
    93
qed
wenzelm@8051
    94
haftmann@27556
    95
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
wenzelm@10007
    96
proof (cases m)
wenzelm@18153
    97
  case 0
wenzelm@18153
    98
  then show ?thesis by simp
wenzelm@10007
    99
next
wenzelm@18153
   100
  case (Suc k)
haftmann@27556
   101
  then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
haftmann@62348
   102
    by (simp add: gcd.commute)
wenzelm@63095
   103
  also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
wenzelm@10007
   104
    by (rule fib_add)
wenzelm@55640
   105
  also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
wenzelm@10007
   106
    by (simp add: gcd_mult_add)
wenzelm@55640
   107
  also have "\<dots> = gcd (fib n) (fib (k + 1))"
haftmann@67051
   108
    using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
haftmann@67051
   109
    by (simp add: ac_simps)
wenzelm@55640
   110
  also have "\<dots> = gcd (fib m) (fib n)"
haftmann@62348
   111
    using Suc by (simp add: gcd.commute)
wenzelm@10007
   112
  finally show ?thesis .
wenzelm@10007
   113
qed
wenzelm@8051
   114
wenzelm@63095
   115
lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m \<le> n"
wenzelm@10007
   116
proof -
haftmann@27556
   117
  have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
wenzelm@10007
   118
    by (simp add: gcd_fib_add)
wenzelm@58614
   119
  also from \<open>m \<le> n\<close> have "n - m + m = n"
wenzelm@55640
   120
    by simp
wenzelm@10007
   121
  finally show ?thesis .
wenzelm@10007
   122
qed
wenzelm@8051
   123
wenzelm@63095
   124
lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"
wenzelm@18153
   125
proof (induct n rule: nat_less_induct)
wenzelm@63095
   126
  case hyp: (1 n)
wenzelm@18153
   127
  show ?case
wenzelm@18153
   128
  proof -
wenzelm@18153
   129
    have "n mod m = (if n < m then n else (n - m) mod m)"
wenzelm@18153
   130
      by (rule mod_if)
wenzelm@55640
   131
    also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
wenzelm@18153
   132
    proof (cases "n < m")
wenzelm@55640
   133
      case True
wenzelm@55640
   134
      then show ?thesis by simp
wenzelm@18153
   135
    next
wenzelm@55640
   136
      case False
wenzelm@55640
   137
      then have "m \<le> n" by simp
wenzelm@58614
   138
      from \<open>0 < m\<close> and False have "n - m < n"
wenzelm@55640
   139
        by simp
haftmann@27556
   140
      with hyp have "gcd (fib m) (fib ((n - m) mod m))
wenzelm@37671
   141
          = gcd (fib m) (fib (n - m))" by simp
wenzelm@55640
   142
      also have "\<dots> = gcd (fib m) (fib n)"
wenzelm@58614
   143
        using \<open>m \<le> n\<close> by (rule gcd_fib_diff)
haftmann@27556
   144
      finally have "gcd (fib m) (fib ((n - m) mod m)) =
wenzelm@37671
   145
          gcd (fib m) (fib n)" .
wenzelm@18153
   146
      with False show ?thesis by simp
wenzelm@10408
   147
    qed
wenzelm@18153
   148
    finally show ?thesis .
wenzelm@10007
   149
  qed
wenzelm@10007
   150
qed
wenzelm@8051
   151
wenzelm@63095
   152
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
wenzelm@63095
   153
  (is "?P m n")
wenzelm@37672
   154
proof (induct m n rule: gcd_nat_induct)
wenzelm@63095
   155
  fix m n :: nat
wenzelm@55640
   156
  show "fib (gcd m 0) = gcd (fib m) (fib 0)"
wenzelm@55640
   157
    by simp
wenzelm@55640
   158
  assume n: "0 < n"
wenzelm@55640
   159
  then have "gcd m n = gcd n (m mod n)"
wenzelm@55640
   160
    by (simp add: gcd_non_0_nat)
wenzelm@55640
   161
  also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
wenzelm@55640
   162
  also from n have "\<dots> = gcd (fib n) (fib m)"
wenzelm@55640
   163
    by (rule gcd_fib_mod)
wenzelm@55640
   164
  also have "\<dots> = gcd (fib m) (fib n)"
haftmann@62348
   165
    by (rule gcd.commute)
haftmann@27556
   166
  finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
wenzelm@10007
   167
qed
wenzelm@8051
   168
wenzelm@10007
   169
end