--- a/src/HOL/NumberTheory/Fib.thy Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Mon Jun 11 11:06:04 2007 +0200
@@ -67,13 +67,16 @@
"int (fib (Suc (Suc n)) * fib n) =
(if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1
else int (fib (Suc n) * fib (Suc n)) + 1)"
- apply (induct n rule: fib.induct)
- apply (simp add: fib.Suc_Suc)
- apply (simp add: fib.Suc_Suc mod_Suc)
- apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
+proof(induct n rule: fib.induct)
+ case 1 thus ?case by (simp add: fib.Suc_Suc)
+next
+ case 2 thus ?case by (simp add: fib.Suc_Suc mod_Suc)
+next
+ case (3 x)
+ have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
+ with prems show ?case by (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
mod_Suc zmult_int [symmetric])
- apply (presburger (no_abs))
- done
+qed
text{*We now obtain a version for the natural numbers via the coercion
function @{term int}.*}