src/HOL/Number_Theory/Fib.thy
 author haftmann Fri, 04 Jul 2014 20:18:47 +0200 changeset 57512 cc97b347b301 parent 54713 6666fc0b9ebc child 58889 5b7a9633cfa8 permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
```
(*  Title:      HOL/Number_Theory/Fib.thy
Author:     Lawrence C. Paulson

Defines the fibonacci function.

The original "Fib" is due to Lawrence C. Paulson, and was adapted by
*)

theory Fib
imports Binomial
begin

subsection {* Main definitions *}

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"

subsection {* Fibonacci numbers *}

lemma fib_1 [simp]: "fib (1::nat) = 1"
by (metis One_nat_def fib1)

lemma fib_2 [simp]: "fib (2::nat) = 1"
using fib.simps(3) [of 0]

lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"

lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
by (induct n rule: fib.induct) (auto simp add: field_simps)

lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
by (induct n rule: fib.induct) (auto simp add: )

text {*
\medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
much easier using integers, not natural numbers!
*}

lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"

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

lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
apply (induct n rule: fib.induct)
apply auto
done

lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
apply (simp add: gcd_commute_nat [of "fib m"])
apply (cases m)
apply (subst gcd_commute_nat)
apply (subst mult.commute)
apply (metis 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_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 `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: less.hyps diff pos_m)
also have "\<dots> = gcd (fib m) (fib n)"
by (simp add: gcd_fib_diff `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
qed
qed

lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
-- {* Law 6.111 *}
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)"
by (induct n rule: nat.induct) (auto simp add:  field_simps)

end

```