src/HOL/Number_Theory/Fib.thy
 changeset 32479 521cc9bf2958 parent 31952 40501bb2d57c child 35644 d20cf282342e
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Tue Sep 01 15:39:33 2009 +0200
1.3 @@ -0,0 +1,319 @@
1.4 +(*  Title:      Fib.thy
1.5 +    Authors:    Lawrence C. Paulson, Jeremy Avigad
1.6 +
1.7 +
1.8 +Defines the fibonacci function.
1.9 +
1.10 +The original "Fib" is due to Lawrence C. Paulson, and was adapted by
1.12 +*)
1.13 +
1.14 +
1.16 +
1.17 +theory Fib
1.18 +imports Binomial
1.19 +begin
1.20 +
1.21 +
1.22 +subsection {* Main definitions *}
1.23 +
1.24 +class fib =
1.25 +
1.26 +fixes
1.27 +  fib :: "'a \<Rightarrow> 'a"
1.28 +
1.29 +
1.30 +(* definition for the natural numbers *)
1.31 +
1.32 +instantiation nat :: fib
1.33 +
1.34 +begin
1.35 +
1.36 +fun
1.37 +  fib_nat :: "nat \<Rightarrow> nat"
1.38 +where
1.39 +  "fib_nat n =
1.40 +   (if n = 0 then 0 else
1.41 +   (if n = 1 then 1 else
1.42 +     fib (n - 1) + fib (n - 2)))"
1.43 +
1.44 +instance proof qed
1.45 +
1.46 +end
1.47 +
1.48 +(* definition for the integers *)
1.49 +
1.50 +instantiation int :: fib
1.51 +
1.52 +begin
1.53 +
1.54 +definition
1.55 +  fib_int :: "int \<Rightarrow> int"
1.56 +where
1.57 +  "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
1.58 +
1.59 +instance proof qed
1.60 +
1.61 +end
1.62 +
1.63 +
1.64 +subsection {* Set up Transfer *}
1.65 +
1.66 +
1.67 +lemma transfer_nat_int_fib:
1.68 +  "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
1.69 +  unfolding fib_int_def by auto
1.70 +
1.71 +lemma transfer_nat_int_fib_closure:
1.72 +  "n >= (0::int) \<Longrightarrow> fib n >= 0"
1.73 +  by (auto simp add: fib_int_def)
1.74 +
1.76 +    transfer_nat_int_fib transfer_nat_int_fib_closure]
1.77 +
1.78 +lemma transfer_int_nat_fib:
1.79 +  "fib (int n) = int (fib n)"
1.80 +  unfolding fib_int_def by auto
1.81 +
1.82 +lemma transfer_int_nat_fib_closure:
1.83 +  "is_nat n \<Longrightarrow> fib n >= 0"
1.84 +  unfolding fib_int_def by auto
1.85 +
1.87 +    transfer_int_nat_fib transfer_int_nat_fib_closure]
1.88 +
1.89 +
1.90 +subsection {* Fibonacci numbers *}
1.91 +
1.92 +lemma fib_0_nat [simp]: "fib (0::nat) = 0"
1.93 +  by simp
1.94 +
1.95 +lemma fib_0_int [simp]: "fib (0::int) = 0"
1.96 +  unfolding fib_int_def by simp
1.97 +
1.98 +lemma fib_1_nat [simp]: "fib (1::nat) = 1"
1.99 +  by simp
1.100 +
1.101 +lemma fib_Suc_0_nat [simp]: "fib (Suc 0) = Suc 0"
1.102 +  by simp
1.103 +
1.104 +lemma fib_1_int [simp]: "fib (1::int) = 1"
1.105 +  unfolding fib_int_def by simp
1.106 +
1.107 +lemma fib_reduce_nat: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
1.108 +  by simp
1.109 +
1.110 +declare fib_nat.simps [simp del]
1.111 +
1.112 +lemma fib_reduce_int: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
1.113 +  unfolding fib_int_def
1.114 +  by (auto simp add: fib_reduce_nat nat_diff_distrib)
1.115 +
1.116 +lemma fib_neg_int [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
1.117 +  unfolding fib_int_def by auto
1.118 +
1.119 +lemma fib_2_nat [simp]: "fib (2::nat) = 1"
1.120 +  by (subst fib_reduce_nat, auto)
1.121 +
1.122 +lemma fib_2_int [simp]: "fib (2::int) = 1"
1.123 +  by (subst fib_reduce_int, auto)
1.124 +
1.125 +lemma fib_plus_2_nat: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
1.126 +  by (subst fib_reduce_nat, auto simp add: One_nat_def)
1.127 +(* the need for One_nat_def is due to the natdiff_cancel_numerals
1.128 +   procedure *)
1.129 +
1.130 +lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
1.131 +    (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
1.132 +  apply (atomize, induct n rule: nat_less_induct)
1.133 +  apply auto
1.134 +  apply (case_tac "n = 0", force)
1.135 +  apply (case_tac "n = 1", force)
1.136 +  apply (subgoal_tac "n >= 2")
1.137 +  apply (frule_tac x = "n - 1" in spec)
1.138 +  apply (drule_tac x = "n - 2" in spec)
1.139 +  apply (drule_tac x = "n - 2" in spec)
1.140 +  apply auto
1.141 +  apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
1.142 +done
1.143 +
1.144 +lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
1.145 +    fib k * fib n"
1.146 +  apply (induct n rule: fib_induct_nat)
1.147 +  apply auto
1.148 +  apply (subst fib_reduce_nat)
1.149 +  apply (auto simp add: ring_simps)
1.150 +  apply (subst (1 3 5) fib_reduce_nat)
1.151 +  apply (auto simp add: ring_simps Suc_eq_plus1)
1.152 +(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
1.153 +  apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
1.154 +  apply (erule ssubst) back back
1.155 +  apply (erule ssubst) back
1.156 +  apply auto
1.157 +done
1.158 +
1.159 +lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
1.160 +    fib k * fib n"
1.162 +
1.163 +
1.164 +(* transfer from nats to ints *)
1.165 +lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
1.166 +    fib (n + k + 1) = fib (k + 1) * fib (n + 1) +
1.167 +    fib k * fib n "
1.168 +
1.169 +  by (rule fib_add_nat [transferred])
1.170 +
1.171 +lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
1.172 +  apply (induct n rule: fib_induct_nat)
1.173 +  apply (auto simp add: fib_plus_2_nat)
1.174 +done
1.175 +
1.176 +lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
1.177 +  by (frule fib_neq_0_nat, simp)
1.178 +
1.179 +lemma fib_gr_0_int: "(n::int) > 0 \<Longrightarrow> fib n > 0"
1.180 +  unfolding fib_int_def by (simp add: fib_gr_0_nat)
1.181 +
1.182 +text {*
1.183 +  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
1.184 +  much easier using integers, not natural numbers!
1.185 +*}
1.186 +
1.187 +lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
1.188 +    (fib (int n + 1))^2 = (-1)^(n + 1)"
1.189 +  apply (induct n)
1.190 +  apply (auto simp add: ring_simps power2_eq_square fib_reduce_int
1.192 +done
1.193 +
1.194 +lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
1.195 +    (fib (n + 1))^2 = (-1)^(nat n + 1)"
1.196 +  by (insert fib_Cassini_aux_int [of "nat n"], auto)
1.197 +
1.198 +(*
1.199 +lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
1.200 +    (fib (n + 1))^2 + (-1)^(nat n + 1)"
1.201 +  by (frule fib_Cassini_int, simp)
1.202 +*)
1.203 +
1.204 +lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
1.205 +  (if even n then tsub ((fib (n + 1))^2) 1
1.206 +   else (fib (n + 1))^2 + 1)"
1.207 +  apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
1.208 +  apply (subst tsub_eq)
1.209 +  apply (insert fib_gr_0_int [of "n + 1"], force)
1.210 +  apply auto
1.211 +done
1.212 +
1.213 +lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
1.214 +  (if even n then (fib (n + 1))^2 - 1
1.215 +   else (fib (n + 1))^2 + 1)"
1.216 +
1.217 +  by (rule fib_Cassini'_int [transferred, of n], auto)
1.218 +
1.219 +
1.221 +
1.222 +lemma coprime_fib_plus_1_nat: "coprime (fib (n::nat)) (fib (n + 1))"
1.223 +  apply (induct n rule: fib_induct_nat)
1.224 +  apply auto
1.225 +  apply (subst (2) fib_reduce_nat)
1.226 +  apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
1.227 +  apply (subst add_commute, auto)
1.228 +  apply (subst gcd_commute_nat, auto simp add: ring_simps)
1.229 +done
1.230 +
1.231 +lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
1.232 +  using coprime_fib_plus_1_nat by (simp add: One_nat_def)
1.233 +
1.234 +lemma coprime_fib_plus_1_int:
1.235 +    "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
1.236 +  by (erule coprime_fib_plus_1_nat [transferred])
1.237 +
1.238 +lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
1.239 +  apply (simp add: gcd_commute_nat [of "fib m"])
1.240 +  apply (rule cases_nat [of _ m])
1.241 +  apply simp
1.242 +  apply (subst add_assoc [symmetric])
1.244 +  apply (subst gcd_commute_nat)
1.245 +  apply (subst mult_commute)
1.247 +  apply (subst gcd_commute_nat)
1.248 +  apply (rule gcd_mult_cancel_nat)
1.249 +  apply (rule coprime_fib_plus_1_nat)
1.250 +done
1.251 +
1.252 +lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
1.253 +    gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
1.254 +  by (erule gcd_fib_add_nat [transferred])
1.255 +
1.256 +lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
1.257 +    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
1.259 +
1.260 +lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
1.261 +    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
1.263 +
1.264 +lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
1.265 +    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.266 +proof (induct n rule: less_induct)
1.267 +  case (less n)
1.268 +  from less.prems have pos_m: "0 < m" .
1.269 +  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.270 +  proof (cases "m < n")
1.271 +    case True note m_n = True
1.272 +    then have m_n': "m \<le> n" by auto
1.273 +    with pos_m have pos_n: "0 < n" by auto
1.274 +    with pos_m m_n have diff: "n - m < n" by auto
1.275 +    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
1.276 +    by (simp add: mod_if [of n]) (insert m_n, auto)
1.277 +    also have "\<dots> = gcd (fib m)  (fib (n - m))"
1.278 +      by (simp add: less.hyps diff pos_m)
1.279 +    also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
1.280 +    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
1.281 +  next
1.282 +    case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.283 +    by (cases "m = n") auto
1.284 +  qed
1.285 +qed
1.286 +
1.287 +lemma gcd_fib_mod_int:
1.288 +  assumes "0 < (m::int)" and "0 <= n"
1.289 +  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
1.290 +
1.291 +  apply (rule gcd_fib_mod_nat [transferred])
1.292 +  using prems apply auto
1.293 +done
1.294 +
1.295 +lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
1.296 +    -- {* Law 6.111 *}
1.297 +  apply (induct m n rule: gcd_nat_induct)
1.298 +  apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
1.299 +done
1.300 +
1.301 +lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
1.302 +    fib (gcd (m::int) n) = gcd (fib m) (fib n)"
1.303 +  by (erule fib_gcd_nat [transferred])
1.304 +
1.305 +lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
1.306 +  by auto
1.307 +
1.308 +theorem fib_mult_eq_setsum_nat:
1.309 +    "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.310 +  apply (induct n)
1.311 +  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps)
1.312 +done
1.313 +
1.314 +theorem fib_mult_eq_setsum'_nat:
1.315 +    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
1.316 +  using fib_mult_eq_setsum_nat by (simp add: One_nat_def)
1.317 +
1.318 +theorem fib_mult_eq_setsum_int [rule_format]:
1.319 +    "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
1.320 +  by (erule fib_mult_eq_setsum_nat [transferred])
1.321 +
1.322 +end
```