src/HOL/Number_Theory/Fib.thy
 author wenzelm Thu May 26 17:51:22 2016 +0200 (2016-05-26) changeset 63167 0909deb8059b parent 62429 25271ff79171 child 64267 b9a1486e79be permissions -rw-r--r--
isabelle update_cartouches -c -t;
```     1 (*  Title:      HOL/Number_Theory/Fib.thy
```
```     2     Author:     Lawrence C. Paulson
```
```     3     Author:     Jeremy Avigad
```
```     4 *)
```
```     5
```
```     6 section \<open>The fibonacci function\<close>
```
```     7
```
```     8 theory Fib
```
```     9 imports Main GCD Binomial
```
```    10 begin
```
```    11
```
```    12
```
```    13 subsection \<open>Fibonacci numbers\<close>
```
```    14
```
```    15 fun fib :: "nat \<Rightarrow> nat"
```
```    16 where
```
```    17   fib0: "fib 0 = 0"
```
```    18 | fib1: "fib (Suc 0) = 1"
```
```    19 | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
```
```    20
```
```    21
```
```    22 subsection \<open>Basic Properties\<close>
```
```    23
```
```    24 lemma fib_1 [simp]: "fib (1::nat) = 1"
```
```    25   by (metis One_nat_def fib1)
```
```    26
```
```    27 lemma fib_2 [simp]: "fib (2::nat) = 1"
```
```    28   using fib.simps(3) [of 0]
```
```    29   by (simp add: numeral_2_eq_2)
```
```    30
```
```    31 lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
```
```    32   by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
```
```    33
```
```    34 lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
```
```    35   by (induct n rule: fib.induct) (auto simp add: field_simps)
```
```    36
```
```    37 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
```
```    38   by (induct n rule: fib.induct) (auto simp add: )
```
```    39
```
```    40
```
```    41 subsection \<open>A Few Elementary Results\<close>
```
```    42
```
```    43 text \<open>
```
```    44   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
```
```    45   much easier using integers, not natural numbers!
```
```    46 \<close>
```
```    47
```
```    48 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
```
```    49   by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
```
```    50
```
```    51 lemma fib_Cassini_nat:
```
```    52   "fib (Suc (Suc n)) * fib n =
```
```    53      (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
```
```    54   using fib_Cassini_int [of n]  by (auto simp del: of_nat_mult of_nat_power)
```
```    55
```
```    56
```
```    57 subsection \<open>Law 6.111 of Concrete Mathematics\<close>
```
```    58
```
```    59 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
```
```    60   apply (induct n rule: fib.induct)
```
```    61   apply auto
```
```    62   apply (metis gcd_add1 add.commute)
```
```    63   done
```
```    64
```
```    65 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
```
```    66   apply (simp add: gcd.commute [of "fib m"])
```
```    67   apply (cases m)
```
```    68   apply (auto simp add: fib_add)
```
```    69   apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
```
```    70     gcd_add_mult gcd_mult_cancel gcd.commute)
```
```    71   done
```
```    72
```
```    73 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
```
```    74   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
```
```    75
```
```    76 lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
```
```    77 proof (induct n rule: less_induct)
```
```    78   case (less n)
```
```    79   show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
```
```    80   proof (cases "m < n")
```
```    81     case True
```
```    82     then have "m \<le> n" by auto
```
```    83     with \<open>0 < m\<close> have pos_n: "0 < n" by auto
```
```    84     with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
```
```    85     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
```
```    86       by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
```
```    87     also have "\<dots> = gcd (fib m)  (fib (n - m))"
```
```    88       by (simp add: less.hyps diff \<open>0 < m\<close>)
```
```    89     also have "\<dots> = gcd (fib m) (fib n)"
```
```    90       by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
```
```    91     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
```
```    92   next
```
```    93     case False
```
```    94     then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
```
```    95       by (cases "m = n") auto
```
```    96   qed
```
```    97 qed
```
```    98
```
```    99 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
```
```   100     \<comment> \<open>Law 6.111\<close>
```
```   101   by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
```
```   102
```
```   103 theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
```
```   104   by (induct n rule: nat.induct) (auto simp add:  field_simps)
```
```   105
```
```   106
```
```   107 subsection \<open>Fibonacci and Binomial Coefficients\<close>
```
```   108
```
```   109 lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
```
```   110   by (induct n) auto
```
```   111
```
```   112 lemma setsum_choose_drop_zero:
```
```   113     "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
```
```   114   by (rule trans [OF setsum.cong setsum_drop_zero]) auto
```
```   115
```
```   116 lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
```
```   117 proof (induct n rule: fib.induct)
```
```   118   case 1
```
```   119   show ?case by simp
```
```   120 next
```
```   121   case 2
```
```   122   show ?case by simp
```
```   123 next
```
```   124   case (3 n)
```
```   125   have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
```
```   126         (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
```
```   127     by (rule setsum.cong) (simp_all add: choose_reduce_nat)
```
```   128   also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
```
```   129                    (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
```
```   130     by (simp add: setsum.distrib)
```
```   131   also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
```
```   132                    (\<Sum>j = 0..n. n - j choose j)"
```
```   133     by (metis setsum_choose_drop_zero)
```
```   134   finally show ?case using 3
```
```   135     by simp
```
```   136 qed
```
```   137
```
```   138 end
```
```   139
```