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