src/HOL/Number_Theory/Fib.thy
 author haftmann Tue Sep 01 15:39:33 2009 +0200 (2009-09-01) changeset 32479 521cc9bf2958 parent 31952 src/HOL/NewNumberTheory/Fib.thy@40501bb2d57c child 35644 d20cf282342e permissions -rw-r--r--
some reorganization of number theory
```     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 TransferMorphism_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 TransferMorphism_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
```