src/HOL/Isar_Examples/Fibonacci.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 37672 645eb9fec794
child 54892 64c2d4f8d981
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 31758
diff changeset
     1
(*  Title:      HOL/Isar_Examples/Fibonacci.thy
8051
wenzelm
parents:
diff changeset
     2
    Author:     Gertrud Bauer
wenzelm
parents:
diff changeset
     3
    Copyright   1999 Technische Universitaet Muenchen
wenzelm
parents:
diff changeset
     4
wenzelm
parents:
diff changeset
     5
The Fibonacci function.  Demonstrates the use of recdef.  Original
wenzelm
parents:
diff changeset
     6
tactic script by Lawrence C Paulson.
wenzelm
parents:
diff changeset
     7
wenzelm
parents:
diff changeset
     8
Fibonacci numbers: proofs of laws taken from
wenzelm
parents:
diff changeset
     9
wenzelm
parents:
diff changeset
    10
  R. L. Graham, D. E. Knuth, O. Patashnik.
wenzelm
parents:
diff changeset
    11
  Concrete Mathematics.
wenzelm
parents:
diff changeset
    12
  (Addison-Wesley, 1989)
wenzelm
parents:
diff changeset
    13
*)
wenzelm
parents:
diff changeset
    14
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    15
header {* Fib and Gcd commute *}
8051
wenzelm
parents:
diff changeset
    16
27366
d0cda1ea705e dropped recdef
haftmann
parents: 18241
diff changeset
    17
theory Fibonacci
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    18
imports "../Number_Theory/Primes"
27366
d0cda1ea705e dropped recdef
haftmann
parents: 18241
diff changeset
    19
begin
8051
wenzelm
parents:
diff changeset
    20
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    21
text_raw {* \footnote{Isar version by Gertrud Bauer.  Original tactic
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    22
  script by Larry Paulson.  A few proofs of laws taken from
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    23
  \cite{Concrete-Math}.} *}
8051
wenzelm
parents:
diff changeset
    24
wenzelm
parents:
diff changeset
    25
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    26
declare One_nat_def [simp]
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    27
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    28
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    29
subsection {* Fibonacci numbers *}
8051
wenzelm
parents:
diff changeset
    30
27366
d0cda1ea705e dropped recdef
haftmann
parents: 18241
diff changeset
    31
fun fib :: "nat \<Rightarrow> nat" where
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
    32
  "fib 0 = 0"
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    33
| "fib (Suc 0) = 1"
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    34
| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
8051
wenzelm
parents:
diff changeset
    35
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    36
lemma [simp]: "fib (Suc n) > 0"
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
    37
  by (induct n rule: fib.induct) simp_all
8051
wenzelm
parents:
diff changeset
    38
wenzelm
parents:
diff changeset
    39
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    40
text {* Alternative induction rule. *}
8051
wenzelm
parents:
diff changeset
    41
8304
e132d147374b even better induct setup;
wenzelm
parents: 8281
diff changeset
    42
theorem fib_induct:
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    43
    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
    44
  by (induct rule: fib.induct) simp_all
8051
wenzelm
parents:
diff changeset
    45
wenzelm
parents:
diff changeset
    46
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    47
subsection {* Fib and gcd commute *}
8051
wenzelm
parents:
diff changeset
    48
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    49
text {* A few laws taken from \cite{Concrete-Math}. *}
8051
wenzelm
parents:
diff changeset
    50
9659
wenzelm
parents: 8935
diff changeset
    51
lemma fib_add:
8051
wenzelm
parents:
diff changeset
    52
  "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
9659
wenzelm
parents: 8935
diff changeset
    53
  (is "?P n")
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    54
  -- {* see \cite[page 280]{Concrete-Math} *}
11809
c9ffdd63dd93 tuned induction proofs;
wenzelm
parents: 11704
diff changeset
    55
proof (induct n rule: fib_induct)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    56
  show "?P 0" by simp
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    57
  show "?P 1" by simp
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    58
  fix n
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    59
  have "fib (n + 2 + k + 1)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    60
    = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    61
  also assume "fib (n + k + 1)
8051
wenzelm
parents:
diff changeset
    62
    = fib (k + 1) * fib (n + 1) + fib k * fib n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    63
      (is " _ = ?R1")
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    64
  also assume "fib (n + 1 + k + 1)
8051
wenzelm
parents:
diff changeset
    65
    = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    66
      (is " _ = ?R2")
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    67
  also have "?R1 + ?R2
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    68
    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    69
    by (simp add: add_mult_distrib2)
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    70
  finally show "?P (n + 2)" .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    71
qed
8051
wenzelm
parents:
diff changeset
    72
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
    73
lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
11809
c9ffdd63dd93 tuned induction proofs;
wenzelm
parents: 11704
diff changeset
    74
proof (induct n rule: fib_induct)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    75
  show "?P 0" by simp
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    76
  show "?P 1" by simp
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    77
  fix n
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    78
  have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    79
    by simp
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    80
  also have "... = fib (n + 2) + fib (n + 1)" by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
    81
  also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    82
    by (rule gcd_add2_nat)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
    83
  also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    84
    by (simp add: gcd_commute_nat)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    85
  also assume "... = 1"
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    86
  finally show "?P (n + 2)" .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    87
qed
8051
wenzelm
parents:
diff changeset
    88
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    89
lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    90
proof -
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    91
  assume "0 < n"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
    92
  then have "gcd (n * k + m) n = gcd n (m mod n)"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    93
    by (simp add: gcd_non_0_nat add_commute)
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
    94
  also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    95
  finally show ?thesis .
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    96
qed
8051
wenzelm
parents:
diff changeset
    97
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
    98
lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
    99
proof (cases m)
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   100
  case 0
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   101
  then show ?thesis by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   102
next
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   103
  case (Suc k)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   104
  then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
   105
    by (simp add: gcd_commute_nat)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   106
  also have "fib (n + k + 1)
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   107
      = fib (k + 1) * fib (n + 1) + fib k * fib n"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   108
    by (rule fib_add)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   109
  also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   110
    by (simp add: gcd_mult_add)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   111
  also have "... = gcd (fib n) (fib (k + 1))"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
   112
    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   113
  also have "... = gcd (fib m) (fib n)"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
   114
    using Suc by (simp add: gcd_commute_nat)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   115
  finally show ?thesis .
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   116
qed
8051
wenzelm
parents:
diff changeset
   117
9659
wenzelm
parents: 8935
diff changeset
   118
lemma gcd_fib_diff:
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   119
  assumes "m <= n"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   120
  shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   121
proof -
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   122
  have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   123
    by (simp add: gcd_fib_add)
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   124
  also from `m <= n` have "n - m + m = n" by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   125
  finally show ?thesis .
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   126
qed
8051
wenzelm
parents:
diff changeset
   127
9659
wenzelm
parents: 8935
diff changeset
   128
lemma gcd_fib_mod:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 18153
diff changeset
   129
  assumes "0 < m"
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   130
  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   131
proof (induct n rule: nat_less_induct)
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   132
  case (1 n) note hyp = this
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   133
  show ?case
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   134
  proof -
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   135
    have "n mod m = (if n < m then n else (n - m) mod m)"
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   136
      by (rule mod_if)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   137
    also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   138
    proof (cases "n < m")
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   139
      case True then show ?thesis by simp
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   140
    next
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   141
      case False then have "m <= n" by simp
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 18153
diff changeset
   142
      from `0 < m` and False have "n - m < n" by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   143
      with hyp have "gcd (fib m) (fib ((n - m) mod m))
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   144
          = gcd (fib m) (fib (n - m))" by simp
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   145
      also have "... = gcd (fib m) (fib n)"
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   146
        using `m <= n` by (rule gcd_fib_diff)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   147
      finally have "gcd (fib m) (fib ((n - m) mod m)) =
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   148
          gcd (fib m) (fib n)" .
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   149
      with False show ?thesis by simp
10408
d8b3613158b1 improved: 'induct' handle non-atomic goals;
wenzelm
parents: 10007
diff changeset
   150
    qed
18153
a084aa91f701 tuned proofs;
wenzelm
parents: 16417
diff changeset
   151
    finally show ?thesis .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   152
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   153
qed
8051
wenzelm
parents:
diff changeset
   154
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   155
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
   156
proof (induct m n rule: gcd_nat_induct)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   157
  fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   158
  fix n :: nat assume n: "0 < n"
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
   159
  then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   160
  also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   161
  also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37671
diff changeset
   162
  also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 27366
diff changeset
   163
  finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   164
qed
8051
wenzelm
parents:
diff changeset
   165
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9870
diff changeset
   166
end