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