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