src/HOL/Number_Theory/Fib.thy
author wenzelm
Sun Aug 18 19:59:19 2013 +0200 (2013-08-18)
changeset 53077 a1b3784f8129
parent 44872 a98ef45122f3
child 54713 6666fc0b9ebc
permissions -rw-r--r--
more symbols;
     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 class fib =
    21   fixes fib :: "'a \<Rightarrow> 'a"
    22 
    23 
    24 (* definition for the natural numbers *)
    25 
    26 instantiation nat :: fib
    27 begin
    28 
    29 fun fib_nat :: "nat \<Rightarrow> nat"
    30 where
    31   "fib_nat n =
    32    (if n = 0 then 0 else
    33    (if n = 1 then 1 else
    34      fib (n - 1) + fib (n - 2)))"
    35 
    36 instance ..
    37 
    38 end
    39 
    40 (* definition for the integers *)
    41 
    42 instantiation int :: fib
    43 begin
    44 
    45 definition fib_int :: "int \<Rightarrow> int"
    46   where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
    47 
    48 instance ..
    49 
    50 end
    51 
    52 
    53 subsection {* Set up Transfer *}
    54 
    55 lemma transfer_nat_int_fib:
    56   "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
    57   unfolding fib_int_def by auto
    58 
    59 lemma transfer_nat_int_fib_closure:
    60   "n >= (0::int) \<Longrightarrow> fib n >= 0"
    61   by (auto simp add: fib_int_def)
    62 
    63 declare transfer_morphism_nat_int[transfer add return:
    64     transfer_nat_int_fib transfer_nat_int_fib_closure]
    65 
    66 lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
    67   unfolding fib_int_def by auto
    68 
    69 lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
    70   unfolding fib_int_def by auto
    71 
    72 declare transfer_morphism_int_nat[transfer add return:
    73     transfer_int_nat_fib transfer_int_nat_fib_closure]
    74 
    75 
    76 subsection {* Fibonacci numbers *}
    77 
    78 lemma fib_0_nat [simp]: "fib (0::nat) = 0"
    79   by simp
    80 
    81 lemma fib_0_int [simp]: "fib (0::int) = 0"
    82   unfolding fib_int_def by simp
    83 
    84 lemma fib_1_nat [simp]: "fib (1::nat) = 1"
    85   by simp
    86 
    87 lemma fib_Suc_0_nat [simp]: "fib (Suc 0) = Suc 0"
    88   by simp
    89 
    90 lemma fib_1_int [simp]: "fib (1::int) = 1"
    91   unfolding fib_int_def by simp
    92 
    93 lemma fib_reduce_nat: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
    94   by simp
    95 
    96 declare fib_nat.simps [simp del]
    97 
    98 lemma fib_reduce_int: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
    99   unfolding fib_int_def
   100   by (auto simp add: fib_reduce_nat nat_diff_distrib)
   101 
   102 lemma fib_neg_int [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
   103   unfolding fib_int_def by auto
   104 
   105 lemma fib_2_nat [simp]: "fib (2::nat) = 1"
   106   by (subst fib_reduce_nat, auto)
   107 
   108 lemma fib_2_int [simp]: "fib (2::int) = 1"
   109   by (subst fib_reduce_int, auto)
   110 
   111 lemma fib_plus_2_nat: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
   112   by (subst fib_reduce_nat, auto simp add: One_nat_def)
   113 (* the need for One_nat_def is due to the natdiff_cancel_numerals
   114    procedure *)
   115 
   116 lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
   117     (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
   118   apply (atomize, induct n rule: nat_less_induct)
   119   apply auto
   120   apply (case_tac "n = 0", force)
   121   apply (case_tac "n = 1", force)
   122   apply (subgoal_tac "n >= 2")
   123   apply (frule_tac x = "n - 1" in spec)
   124   apply (drule_tac x = "n - 2" in spec)
   125   apply (drule_tac x = "n - 2" in spec)
   126   apply auto
   127   apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
   128 done
   129 
   130 lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
   131     fib k * fib n"
   132   apply (induct n rule: fib_induct_nat)
   133   apply auto
   134   apply (subst fib_reduce_nat)
   135   apply (auto simp add: field_simps)
   136   apply (subst (1 3 5) fib_reduce_nat)
   137   apply (auto simp add: field_simps Suc_eq_plus1)
   138 (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   139   apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   140   apply (erule ssubst) back back
   141   apply (erule ssubst) back
   142   apply auto
   143 done
   144 
   145 lemma fib_add'_nat: "fib (n + Suc k) =
   146     fib (Suc k) * fib (Suc n) + fib k * fib n"
   147   using fib_add_nat by (auto simp add: One_nat_def)
   148 
   149 
   150 (* transfer from nats to ints *)
   151 lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
   152     fib (n + k + 1) = fib (k + 1) * fib (n + 1) +  fib k * fib n "
   153   by (rule fib_add_nat [transferred])
   154 
   155 lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
   156   apply (induct n rule: fib_induct_nat)
   157   apply (auto simp add: fib_plus_2_nat)
   158   done
   159 
   160 lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
   161   by (frule fib_neq_0_nat, simp)
   162 
   163 lemma fib_gr_0_int: "(n::int) > 0 \<Longrightarrow> fib n > 0"
   164   unfolding fib_int_def by (simp add: fib_gr_0_nat)
   165 
   166 text {*
   167   \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
   168   much easier using integers, not natural numbers!
   169 *}
   170 
   171 lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
   172     (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
   173   apply (induct n)
   174   apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
   175   done
   176 
   177 lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
   178     (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
   179   by (insert fib_Cassini_aux_int [of "nat n"], auto)
   180 
   181 (*
   182 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
   183     (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
   184   by (frule fib_Cassini_int, simp)
   185 *)
   186 
   187 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
   188   (if even n then tsub ((fib (n + 1))\<^sup>2) 1
   189    else (fib (n + 1))\<^sup>2 + 1)"
   190   apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
   191   apply (subst tsub_eq)
   192   apply (insert fib_gr_0_int [of "n + 1"], force)
   193   apply auto
   194   done
   195 
   196 lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
   197     (if even n then (fib (n + 1))\<^sup>2 - 1
   198      else (fib (n + 1))\<^sup>2 + 1)"
   199   by (rule fib_Cassini'_int [transferred, of n], auto)
   200 
   201 
   202 text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
   203 
   204 lemma coprime_fib_plus_1_nat: "coprime (fib (n::nat)) (fib (n + 1))"
   205   apply (induct n rule: fib_induct_nat)
   206   apply auto
   207   apply (subst (2) fib_reduce_nat)
   208   apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
   209   apply (subst add_commute, auto)
   210   apply (subst gcd_commute_nat, auto simp add: field_simps)
   211   done
   212 
   213 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   214   using coprime_fib_plus_1_nat by (simp add: One_nat_def)
   215 
   216 lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
   217   by (erule coprime_fib_plus_1_nat [transferred])
   218 
   219 lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
   220   apply (simp add: gcd_commute_nat [of "fib m"])
   221   apply (rule cases_nat [of _ m])
   222   apply simp
   223   apply (subst add_assoc [symmetric])
   224   apply (simp add: fib_add_nat)
   225   apply (subst gcd_commute_nat)
   226   apply (subst mult_commute)
   227   apply (subst gcd_add_mult_nat)
   228   apply (subst gcd_commute_nat)
   229   apply (rule gcd_mult_cancel_nat)
   230   apply (rule coprime_fib_plus_1_nat)
   231   done
   232 
   233 lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   234     gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
   235   by (erule gcd_fib_add_nat [transferred])
   236 
   237 lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
   238     gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   239   by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
   240 
   241 lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
   242     gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   243   by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
   244 
   245 lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
   246     gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   247 proof (induct n rule: less_induct)
   248   case (less n)
   249   from less.prems have pos_m: "0 < m" .
   250   show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   251   proof (cases "m < n")
   252     case True
   253     then have "m \<le> n" by auto
   254     with pos_m have pos_n: "0 < n" by auto
   255     with pos_m `m < n` have diff: "n - m < n" by auto
   256     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
   257       by (simp add: mod_if [of n]) (insert `m < n`, auto)
   258     also have "\<dots> = gcd (fib m)  (fib (n - m))"
   259       by (simp add: less.hyps diff pos_m)
   260     also have "\<dots> = gcd (fib m) (fib n)"
   261       by (simp add: gcd_fib_diff_nat `m \<le> n`)
   262     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   263   next
   264     case False
   265     then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   266       by (cases "m = n") auto
   267   qed
   268 qed
   269 
   270 lemma gcd_fib_mod_int:
   271   assumes "0 < (m::int)" and "0 <= n"
   272   shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   273   apply (rule gcd_fib_mod_nat [transferred])
   274   using assms apply auto
   275   done
   276 
   277 lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
   278     -- {* Law 6.111 *}
   279   apply (induct m n rule: gcd_nat_induct)
   280   apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
   281   done
   282 
   283 lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   284     fib (gcd (m::int) n) = gcd (fib m) (fib n)"
   285   by (erule fib_gcd_nat [transferred])
   286 
   287 lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
   288   by auto
   289 
   290 theorem fib_mult_eq_setsum_nat:
   291     "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   292   apply (induct n)
   293   apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
   294   done
   295 
   296 theorem fib_mult_eq_setsum'_nat:
   297     "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   298   using fib_mult_eq_setsum_nat by (simp add: One_nat_def)
   299 
   300 theorem fib_mult_eq_setsum_int [rule_format]:
   301     "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
   302   by (erule fib_mult_eq_setsum_nat [transferred])
   303 
   304 end