src/HOL/Number_Theory/Fib.thy
changeset 44872 a98ef45122f3
parent 41959 b460124855b8
child 53077 a1b3784f8129
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Sat Sep 10 22:11:55 2011 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sat Sep 10 23:27:32 2011 +0200
     1.3 @@ -18,48 +18,40 @@
     1.4  subsection {* Main definitions *}
     1.5  
     1.6  class fib =
     1.7 -
     1.8 -fixes 
     1.9 -  fib :: "'a \<Rightarrow> 'a"
    1.10 +  fixes fib :: "'a \<Rightarrow> 'a"
    1.11  
    1.12  
    1.13  (* definition for the natural numbers *)
    1.14  
    1.15  instantiation nat :: fib
    1.16 -
    1.17 -begin 
    1.18 +begin
    1.19  
    1.20 -fun 
    1.21 -  fib_nat :: "nat \<Rightarrow> nat"
    1.22 +fun fib_nat :: "nat \<Rightarrow> nat"
    1.23  where
    1.24    "fib_nat n =
    1.25     (if n = 0 then 0 else
    1.26     (if n = 1 then 1 else
    1.27       fib (n - 1) + fib (n - 2)))"
    1.28  
    1.29 -instance proof qed
    1.30 +instance ..
    1.31  
    1.32  end
    1.33  
    1.34  (* definition for the integers *)
    1.35  
    1.36  instantiation int :: fib
    1.37 -
    1.38 -begin 
    1.39 +begin
    1.40  
    1.41 -definition
    1.42 -  fib_int :: "int \<Rightarrow> int"
    1.43 -where  
    1.44 -  "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
    1.45 +definition fib_int :: "int \<Rightarrow> int"
    1.46 +  where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
    1.47  
    1.48 -instance proof qed
    1.49 +instance ..
    1.50  
    1.51  end
    1.52  
    1.53  
    1.54  subsection {* Set up Transfer *}
    1.55  
    1.56 -
    1.57  lemma transfer_nat_int_fib:
    1.58    "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
    1.59    unfolding fib_int_def by auto
    1.60 @@ -68,18 +60,16 @@
    1.61    "n >= (0::int) \<Longrightarrow> fib n >= 0"
    1.62    by (auto simp add: fib_int_def)
    1.63  
    1.64 -declare transfer_morphism_nat_int[transfer add return: 
    1.65 +declare transfer_morphism_nat_int[transfer add return:
    1.66      transfer_nat_int_fib transfer_nat_int_fib_closure]
    1.67  
    1.68 -lemma transfer_int_nat_fib:
    1.69 -  "fib (int n) = int (fib n)"
    1.70 +lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
    1.71    unfolding fib_int_def by auto
    1.72  
    1.73 -lemma transfer_int_nat_fib_closure:
    1.74 -  "is_nat n \<Longrightarrow> fib n >= 0"
    1.75 +lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
    1.76    unfolding fib_int_def by auto
    1.77  
    1.78 -declare transfer_morphism_int_nat[transfer add return: 
    1.79 +declare transfer_morphism_int_nat[transfer add return:
    1.80      transfer_int_nat_fib transfer_int_nat_fib_closure]
    1.81  
    1.82  
    1.83 @@ -123,7 +113,7 @@
    1.84  (* the need for One_nat_def is due to the natdiff_cancel_numerals
    1.85     procedure *)
    1.86  
    1.87 -lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow> 
    1.88 +lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
    1.89      (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
    1.90    apply (atomize, induct n rule: nat_less_induct)
    1.91    apply auto
    1.92 @@ -137,7 +127,7 @@
    1.93    apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
    1.94  done
    1.95  
    1.96 -lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) + 
    1.97 +lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
    1.98      fib k * fib n"
    1.99    apply (induct n rule: fib_induct_nat)
   1.100    apply auto
   1.101 @@ -148,26 +138,24 @@
   1.102  (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   1.103    apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   1.104    apply (erule ssubst) back back
   1.105 -  apply (erule ssubst) back 
   1.106 +  apply (erule ssubst) back
   1.107    apply auto
   1.108  done
   1.109  
   1.110 -lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) + 
   1.111 -    fib k * fib n"
   1.112 +lemma fib_add'_nat: "fib (n + Suc k) =
   1.113 +    fib (Suc k) * fib (Suc n) + fib k * fib n"
   1.114    using fib_add_nat by (auto simp add: One_nat_def)
   1.115  
   1.116  
   1.117  (* transfer from nats to ints *)
   1.118 -lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
   1.119 -    fib (n + k + 1) = fib (k + 1) * fib (n + 1) + 
   1.120 -    fib k * fib n "
   1.121 -
   1.122 +lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
   1.123 +    fib (n + k + 1) = fib (k + 1) * fib (n + 1) +  fib k * fib n "
   1.124    by (rule fib_add_nat [transferred])
   1.125  
   1.126  lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
   1.127    apply (induct n rule: fib_induct_nat)
   1.128    apply (auto simp add: fib_plus_2_nat)
   1.129 -done
   1.130 +  done
   1.131  
   1.132  lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
   1.133    by (frule fib_neq_0_nat, simp)
   1.134 @@ -180,21 +168,20 @@
   1.135    much easier using integers, not natural numbers!
   1.136  *}
   1.137  
   1.138 -lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) - 
   1.139 +lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
   1.140      (fib (int n + 1))^2 = (-1)^(n + 1)"
   1.141    apply (induct n)
   1.142 -  apply (auto simp add: field_simps power2_eq_square fib_reduce_int
   1.143 -      power_add)
   1.144 -done
   1.145 +  apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
   1.146 +  done
   1.147  
   1.148 -lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n - 
   1.149 +lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
   1.150      (fib (n + 1))^2 = (-1)^(nat n + 1)"
   1.151    by (insert fib_Cassini_aux_int [of "nat n"], auto)
   1.152  
   1.153  (*
   1.154 -lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n = 
   1.155 +lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
   1.156      (fib (n + 1))^2 + (-1)^(nat n + 1)"
   1.157 -  by (frule fib_Cassini_int, simp) 
   1.158 +  by (frule fib_Cassini_int, simp)
   1.159  *)
   1.160  
   1.161  lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
   1.162 @@ -204,12 +191,11 @@
   1.163    apply (subst tsub_eq)
   1.164    apply (insert fib_gr_0_int [of "n + 1"], force)
   1.165    apply auto
   1.166 -done
   1.167 +  done
   1.168  
   1.169  lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
   1.170 -  (if even n then (fib (n + 1))^2 - 1
   1.171 -   else (fib (n + 1))^2 + 1)"
   1.172 -
   1.173 +    (if even n then (fib (n + 1))^2 - 1
   1.174 +     else (fib (n + 1))^2 + 1)"
   1.175    by (rule fib_Cassini'_int [transferred, of n], auto)
   1.176  
   1.177  
   1.178 @@ -222,13 +208,12 @@
   1.179    apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
   1.180    apply (subst add_commute, auto)
   1.181    apply (subst gcd_commute_nat, auto simp add: field_simps)
   1.182 -done
   1.183 +  done
   1.184  
   1.185  lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   1.186    using coprime_fib_plus_1_nat by (simp add: One_nat_def)
   1.187  
   1.188 -lemma coprime_fib_plus_1_int: 
   1.189 -    "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
   1.190 +lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
   1.191    by (erule coprime_fib_plus_1_nat [transferred])
   1.192  
   1.193  lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
   1.194 @@ -243,51 +228,53 @@
   1.195    apply (subst gcd_commute_nat)
   1.196    apply (rule gcd_mult_cancel_nat)
   1.197    apply (rule coprime_fib_plus_1_nat)
   1.198 -done
   1.199 +  done
   1.200  
   1.201 -lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 
   1.202 +lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   1.203      gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
   1.204    by (erule gcd_fib_add_nat [transferred])
   1.205  
   1.206 -lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow> 
   1.207 +lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
   1.208      gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   1.209    by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
   1.210  
   1.211 -lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow> 
   1.212 +lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
   1.213      gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   1.214    by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
   1.215  
   1.216 -lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow> 
   1.217 +lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
   1.218      gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   1.219  proof (induct n rule: less_induct)
   1.220    case (less n)
   1.221    from less.prems have pos_m: "0 < m" .
   1.222    show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   1.223    proof (cases "m < n")
   1.224 -    case True note m_n = True
   1.225 -    then have m_n': "m \<le> n" by auto
   1.226 +    case True
   1.227 +    then have "m \<le> n" by auto
   1.228      with pos_m have pos_n: "0 < n" by auto
   1.229 -    with pos_m m_n have diff: "n - m < n" by auto
   1.230 +    with pos_m `m < n` have diff: "n - m < n" by auto
   1.231      have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
   1.232 -    by (simp add: mod_if [of n]) (insert m_n, auto)
   1.233 -    also have "\<dots> = gcd (fib m)  (fib (n - m))" 
   1.234 +      by (simp add: mod_if [of n]) (insert `m < n`, auto)
   1.235 +    also have "\<dots> = gcd (fib m)  (fib (n - m))"
   1.236        by (simp add: less.hyps diff pos_m)
   1.237 -    also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
   1.238 +    also have "\<dots> = gcd (fib m) (fib n)"
   1.239 +      by (simp add: gcd_fib_diff_nat `m \<le> n`)
   1.240      finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   1.241    next
   1.242 -    case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   1.243 -    by (cases "m = n") auto
   1.244 +    case False
   1.245 +    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   1.246 +      by (cases "m = n") auto
   1.247    qed
   1.248  qed
   1.249  
   1.250 -lemma gcd_fib_mod_int: 
   1.251 +lemma gcd_fib_mod_int:
   1.252    assumes "0 < (m::int)" and "0 <= n"
   1.253    shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   1.254    apply (rule gcd_fib_mod_nat [transferred])
   1.255    using assms apply auto
   1.256    done
   1.257  
   1.258 -lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  
   1.259 +lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
   1.260      -- {* Law 6.111 *}
   1.261    apply (induct m n rule: gcd_nat_induct)
   1.262    apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
   1.263 @@ -297,7 +284,7 @@
   1.264      fib (gcd (m::int) n) = gcd (fib m) (fib n)"
   1.265    by (erule fib_gcd_nat [transferred])
   1.266  
   1.267 -lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}" 
   1.268 +lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
   1.269    by auto
   1.270  
   1.271  theorem fib_mult_eq_setsum_nat: