src/HOL/NumberTheory/Fib.thy
 changeset 24573 5bbdc9b60648 parent 24549 c8cee92b06bc child 25222 78943ac46f6d
```     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Fri Sep 14 13:32:07 2007 +0200
1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Fri Sep 14 15:27:12 2007 +0200
1.3 @@ -17,8 +17,8 @@
1.4
1.5  fun fib :: "nat \<Rightarrow> nat"
1.6  where
1.7 -     "fib 0 = 0"
1.8 -|    "fib (Suc 0) = 1"
1.9 +         "fib 0 = 0"
1.10 +|        "fib (Suc 0) = 1"
1.11  | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
1.12
1.13  text {*
1.14 @@ -38,12 +38,13 @@
1.15  text {* \medskip Concrete Mathematics, page 280 *}
1.16
1.17  lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
1.18 -  apply (induct n rule: fib.induct)
1.19 -    prefer 3
1.20 -    txt {* simplify the LHS just enough to apply the induction hypotheses *}
1.21 -    apply (simp add: fib_Suc3)
1.23 -    done
1.24 +proof (induct n rule: fib.induct)
1.25 +  case 1 show ?case by simp
1.26 +next
1.27 +  case 2 show ?case  by (simp add: fib_2)
1.28 +next
1.30 +qed
1.31
1.32  lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
1.33    apply (induct n rule: fib.induct)
1.34 @@ -72,9 +73,8 @@
1.35    case 2 thus ?case by (simp add: fib_2 mod_Suc)
1.36  next
1.37    case (3 x)
1.38 -  have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger