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