--- a/src/HOL/Isar_Examples/Fibonacci.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Thu Jul 01 18:31:46 2010 +0200
@@ -15,22 +15,20 @@
header {* Fib and Gcd commute *}
theory Fibonacci
-imports Primes
+imports "../Old_Number_Theory/Primes"
begin
-text_raw {*
- \footnote{Isar version by Gertrud Bauer. Original tactic script by
- Larry Paulson. A few proofs of laws taken from
- \cite{Concrete-Math}.}
-*}
+text_raw {* \footnote{Isar version by Gertrud Bauer. Original tactic
+ script by Larry Paulson. A few proofs of laws taken from
+ \cite{Concrete-Math}.} *}
subsection {* Fibonacci numbers *}
fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0"
- | "fib (Suc 0) = 1"
- | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "0 < fib (Suc n)"
by (induct n rule: fib.induct) simp_all
@@ -102,7 +100,7 @@
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
by (simp add: gcd_commute)
also have "fib (n + k + 1)
- = fib (k + 1) * fib (n + 1) + fib k * fib n"
+ = fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
by (simp add: gcd_mult_add)
@@ -139,18 +137,17 @@
case False then have "m <= n" by simp
from `0 < m` and False have "n - m < n" by simp
with hyp have "gcd (fib m) (fib ((n - m) mod m))
- = gcd (fib m) (fib (n - m))" by simp
+ = gcd (fib m) (fib (n - m))" by simp
also have "... = gcd (fib m) (fib n)"
using `m <= n` by (rule gcd_fib_diff)
finally have "gcd (fib m) (fib ((n - m) mod m)) =
- gcd (fib m) (fib n)" .
+ gcd (fib m) (fib n)" .
with False show ?thesis by simp
qed
finally show ?thesis .
qed
qed
-
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
proof (induct m n rule: gcd_induct)
fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp