--- a/src/HOL/Number_Theory/Fib.thy Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Sat Sep 10 23:27:32 2011 +0200
@@ -18,48 +18,40 @@
subsection {* Main definitions *}
class fib =
-
-fixes
- fib :: "'a \<Rightarrow> 'a"
+ fixes fib :: "'a \<Rightarrow> 'a"
(* definition for the natural numbers *)
instantiation nat :: fib
-
-begin
+begin
-fun
- fib_nat :: "nat \<Rightarrow> nat"
+fun fib_nat :: "nat \<Rightarrow> nat"
where
"fib_nat n =
(if n = 0 then 0 else
(if n = 1 then 1 else
fib (n - 1) + fib (n - 2)))"
-instance proof qed
+instance ..
end
(* definition for the integers *)
instantiation int :: fib
-
-begin
+begin
-definition
- fib_int :: "int \<Rightarrow> int"
-where
- "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
+definition fib_int :: "int \<Rightarrow> int"
+ where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
-instance proof qed
+instance ..
end
subsection {* Set up Transfer *}
-
lemma transfer_nat_int_fib:
"(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
unfolding fib_int_def by auto
@@ -68,18 +60,16 @@
"n >= (0::int) \<Longrightarrow> fib n >= 0"
by (auto simp add: fib_int_def)
-declare transfer_morphism_nat_int[transfer add return:
+declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_fib transfer_nat_int_fib_closure]
-lemma transfer_int_nat_fib:
- "fib (int n) = int (fib n)"
+lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
unfolding fib_int_def by auto
-lemma transfer_int_nat_fib_closure:
- "is_nat n \<Longrightarrow> fib n >= 0"
+lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
unfolding fib_int_def by auto
-declare transfer_morphism_int_nat[transfer add return:
+declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_fib transfer_int_nat_fib_closure]
@@ -123,7 +113,7 @@
(* the need for One_nat_def is due to the natdiff_cancel_numerals
procedure *)
-lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
+lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
(!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
apply (atomize, induct n rule: nat_less_induct)
apply auto
@@ -137,7 +127,7 @@
apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
done
-lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
+lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
fib k * fib n"
apply (induct n rule: fib_induct_nat)
apply auto
@@ -148,26 +138,24 @@
(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
apply (erule ssubst) back back
- apply (erule ssubst) back
+ apply (erule ssubst) back
apply auto
done
-lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
- fib k * fib n"
+lemma fib_add'_nat: "fib (n + Suc k) =
+ fib (Suc k) * fib (Suc n) + fib k * fib n"
using fib_add_nat by (auto simp add: One_nat_def)
(* transfer from nats to ints *)
-lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
- fib (n + k + 1) = fib (k + 1) * fib (n + 1) +
- fib k * fib n "
-
+lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
+ fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n "
by (rule fib_add_nat [transferred])
lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
apply (induct n rule: fib_induct_nat)
apply (auto simp add: fib_plus_2_nat)
-done
+ done
lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
by (frule fib_neq_0_nat, simp)
@@ -180,21 +168,20 @@
much easier using integers, not natural numbers!
*}
-lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
+lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
(fib (int n + 1))^2 = (-1)^(n + 1)"
apply (induct n)
- apply (auto simp add: field_simps power2_eq_square fib_reduce_int
- power_add)
-done
+ apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
+ done
-lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
+lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
(fib (n + 1))^2 = (-1)^(nat n + 1)"
by (insert fib_Cassini_aux_int [of "nat n"], auto)
(*
-lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
+lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
(fib (n + 1))^2 + (-1)^(nat n + 1)"
- by (frule fib_Cassini_int, simp)
+ by (frule fib_Cassini_int, simp)
*)
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
@@ -204,12 +191,11 @@
apply (subst tsub_eq)
apply (insert fib_gr_0_int [of "n + 1"], force)
apply auto
-done
+ done
lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
- (if even n then (fib (n + 1))^2 - 1
- else (fib (n + 1))^2 + 1)"
-
+ (if even n then (fib (n + 1))^2 - 1
+ else (fib (n + 1))^2 + 1)"
by (rule fib_Cassini'_int [transferred, of n], auto)
@@ -222,13 +208,12 @@
apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
apply (subst add_commute, auto)
apply (subst gcd_commute_nat, auto simp add: field_simps)
-done
+ done
lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
using coprime_fib_plus_1_nat by (simp add: One_nat_def)
-lemma coprime_fib_plus_1_int:
- "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
+lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
by (erule coprime_fib_plus_1_nat [transferred])
lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
@@ -243,51 +228,53 @@
apply (subst gcd_commute_nat)
apply (rule gcd_mult_cancel_nat)
apply (rule coprime_fib_plus_1_nat)
-done
+ done
-lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
by (erule gcd_fib_add_nat [transferred])
-lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
+lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
-lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
+lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
-lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
+lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (induct n rule: less_induct)
case (less n)
from less.prems have pos_m: "0 < m" .
show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (cases "m < n")
- case True note m_n = True
- then have m_n': "m \<le> n" by auto
+ case True
+ then have "m \<le> n" by auto
with pos_m have pos_n: "0 < n" by auto
- with pos_m m_n have diff: "n - m < n" by auto
+ with pos_m `m < n` have diff: "n - m < n" by auto
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
- by (simp add: mod_if [of n]) (insert m_n, auto)
- also have "\<dots> = gcd (fib m) (fib (n - m))"
+ by (simp add: mod_if [of n]) (insert `m < n`, auto)
+ also have "\<dots> = gcd (fib m) (fib (n - m))"
by (simp add: less.hyps diff pos_m)
- also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
+ also have "\<dots> = gcd (fib m) (fib n)"
+ by (simp add: gcd_fib_diff_nat `m \<le> n`)
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
next
- case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
- by (cases "m = n") auto
+ case False
+ then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+ by (cases "m = n") auto
qed
qed
-lemma gcd_fib_mod_int:
+lemma gcd_fib_mod_int:
assumes "0 < (m::int)" and "0 <= n"
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
apply (rule gcd_fib_mod_nat [transferred])
using assms apply auto
done
-lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
+lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
-- {* Law 6.111 *}
apply (induct m n rule: gcd_nat_induct)
apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
@@ -297,7 +284,7 @@
fib (gcd (m::int) n) = gcd (fib m) (fib n)"
by (erule fib_gcd_nat [transferred])
-lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
+lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
by auto
theorem fib_mult_eq_setsum_nat: