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