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