--- a/src/HOL/Number_Theory/Fib.thy Fri Jun 19 21:41:33 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Fri Jun 19 23:40:46 2015 +0200
@@ -1,17 +1,12 @@
(* Title: HOL/Number_Theory/Fib.thy
Author: Lawrence C. Paulson
Author: Jeremy Avigad
-
-Defines the fibonacci function.
-
-The original "Fib" is due to Lawrence C. Paulson, and was adapted by
-Jeremy Avigad.
*)
-section \<open>Fib\<close>
+section \<open>The fibonacci function\<close>
theory Fib
-imports Main "../GCD" "../Binomial"
+imports Main GCD Binomial
begin
@@ -19,9 +14,10 @@
fun fib :: "nat \<Rightarrow> nat"
where
- fib0: "fib 0 = 0"
- | fib1: "fib (Suc 0) = 1"
- | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+ fib0: "fib 0 = 0"
+| fib1: "fib (Suc 0) = 1"
+| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+
subsection \<open>Basic Properties\<close>
@@ -41,6 +37,7 @@
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
by (induct n rule: fib.induct) (auto simp add: )
+
subsection \<open>A Few Elementary Results\<close>
text \<open>
@@ -49,12 +46,12 @@
\<close>
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
- by (induction n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
+ by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
lemma fib_Cassini_nat:
- "fib (Suc (Suc n)) * fib n =
- (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
-using fib_Cassini_int [of n] by auto
+ "fib (Suc (Suc n)) * fib n =
+ (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
+ using fib_Cassini_int [of n] by auto
subsection \<open>Law 6.111 of Concrete Mathematics\<close>
@@ -69,28 +66,26 @@
apply (simp add: gcd_commute_nat [of "fib m"])
apply (cases m)
apply (auto simp add: fib_add)
- apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
+ apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
+ gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
done
-lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
- gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
+lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
-lemma gcd_fib_mod: "0 < m \<Longrightarrow>
- gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+lemma gcd_fib_mod: "0 < m \<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
then have "m \<le> n" by auto
- with pos_m have pos_n: "0 < n" by auto
- with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
+ with \<open>0 < m\<close> have pos_n: "0 < n" by auto
+ with \<open>0 < m\<close> \<open>m < n\<close> 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 \<open>m < n\<close>, auto)
also have "\<dots> = gcd (fib m) (fib (n - m))"
- by (simp add: less.hyps diff pos_m)
+ by (simp add: less.hyps diff \<open>0 < m\<close>)
also have "\<dots> = gcd (fib m) (fib n)"
by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
@@ -105,10 +100,10 @@
-- \<open>Law 6.111\<close>
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
-theorem fib_mult_eq_setsum_nat:
- "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
+theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
by (induct n rule: nat.induct) (auto simp add: field_simps)
+
subsection \<open>Fibonacci and Binomial Coefficients\<close>
lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
@@ -118,21 +113,22 @@
"(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
by (rule trans [OF setsum.cong setsum_drop_zero]) auto
-lemma ne_diagonal_fib:
- "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
+lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
proof (induct n rule: fib.induct)
- case 1 show ?case by simp
+ case 1
+ show ?case by simp
next
- case 2 show ?case by simp
+ case 2
+ show ?case by simp
next
case (3 n)
have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
(\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
by (rule setsum.cong) (simp_all add: choose_reduce_nat)
- also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+ also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
by (simp add: setsum.distrib)
- also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+ also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
(\<Sum>j = 0..n. n - j choose j)"
by (metis setsum_choose_drop_zero)
finally show ?case using 3