src/HOL/Number_Theory/Fib.thy
 author haftmann Fri Jul 04 20:18:47 2014 +0200 (2014-07-04) changeset 57512 cc97b347b301 parent 54713 6666fc0b9ebc child 58889 5b7a9633cfa8 permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
```     1 (*  Title:      HOL/Number_Theory/Fib.thy
```
```     2     Author:     Lawrence C. Paulson
```
```     3     Author:     Jeremy Avigad
```
```     4
```
```     5 Defines the fibonacci function.
```
```     6
```
```     7 The original "Fib" is due to Lawrence C. Paulson, and was adapted by
```
```     8 Jeremy Avigad.
```
```     9 *)
```
```    10
```
```    11 header {* Fib *}
```
```    12
```
```    13 theory Fib
```
```    14 imports Binomial
```
```    15 begin
```
```    16
```
```    17
```
```    18 subsection {* Main definitions *}
```
```    19
```
```    20 fun fib :: "nat \<Rightarrow> nat"
```
```    21 where
```
```    22     fib0: "fib 0 = 0"
```
```    23   | fib1: "fib (Suc 0) = 1"
```
```    24   | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
```
```    25
```
```    26 subsection {* Fibonacci numbers *}
```
```    27
```
```    28 lemma fib_1 [simp]: "fib (1::nat) = 1"
```
```    29   by (metis One_nat_def fib1)
```
```    30
```
```    31 lemma fib_2 [simp]: "fib (2::nat) = 1"
```
```    32   using fib.simps(3) [of 0]
```
```    33   by (simp add: numeral_2_eq_2)
```
```    34
```
```    35 lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
```
```    36   by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
```
```    37
```
```    38 lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
```
```    39   by (induct n rule: fib.induct) (auto simp add: field_simps)
```
```    40
```
```    41 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
```
```    42   by (induct n rule: fib.induct) (auto simp add: )
```
```    43
```
```    44 text {*
```
```    45   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
```
```    46   much easier using integers, not natural numbers!
```
```    47 *}
```
```    48
```
```    49 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
```
```    50   by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
```
```    51
```
```    52 lemma fib_Cassini_nat:
```
```    53     "fib (Suc (Suc n)) * fib n =
```
```    54        (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
```
```    55 using fib_Cassini_int [of n] by auto
```
```    56
```
```    57
```
```    58 text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
```
```    59
```
```    60 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
```
```    61   apply (induct n rule: fib.induct)
```
```    62   apply auto
```
```    63   apply (metis gcd_add1_nat add.commute)
```
```    64   done
```
```    65
```
```    66 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
```
```    67   apply (simp add: gcd_commute_nat [of "fib m"])
```
```    68   apply (cases m)
```
```    69   apply (auto simp add: fib_add)
```
```    70   apply (subst gcd_commute_nat)
```
```    71   apply (subst mult.commute)
```
```    72   apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
```
```    73   done
```
```    74
```
```    75 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
```
```    76     gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
```
```    77   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
```
```    78
```
```    79 lemma gcd_fib_mod: "0 < m \<Longrightarrow>
```
```    80     gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
```
```    81 proof (induct n rule: less_induct)
```
```    82   case (less n)
```
```    83   from less.prems have pos_m: "0 < m" .
```
```    84   show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
```
```    85   proof (cases "m < n")
```
```    86     case True
```
```    87     then have "m \<le> n" by auto
```
```    88     with pos_m have pos_n: "0 < n" by auto
```
```    89     with pos_m `m < n` have diff: "n - m < n" by auto
```
```    90     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
```
```    91       by (simp add: mod_if [of n]) (insert `m < n`, auto)
```
```    92     also have "\<dots> = gcd (fib m)  (fib (n - m))"
```
```    93       by (simp add: less.hyps diff pos_m)
```
```    94     also have "\<dots> = gcd (fib m) (fib n)"
```
```    95       by (simp add: gcd_fib_diff `m \<le> n`)
```
```    96     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
```
```    97   next
```
```    98     case False
```
```    99     then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
```
```   100       by (cases "m = n") auto
```
```   101   qed
```
```   102 qed
```
```   103
```
```   104 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
```
```   105     -- {* Law 6.111 *}
```
```   106   by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
```
```   107
```
```   108 theorem fib_mult_eq_setsum_nat:
```
```   109     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
```
```   110   by (induct n rule: nat.induct) (auto simp add:  field_simps)
```
```   111
```
```   112 end
```
```   113
```