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