equal
deleted
inserted
replaced
27 subsection {* Fibonacci numbers *} |
27 subsection {* Fibonacci numbers *} |
28 |
28 |
29 consts fib :: "nat => nat" |
29 consts fib :: "nat => nat" |
30 recdef fib less_than |
30 recdef fib less_than |
31 "fib 0 = 0" |
31 "fib 0 = 0" |
32 "fib 1 = 1" |
32 "fib 1' = 1" |
33 "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
33 "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
34 |
34 |
35 lemma [simp]: "0 < fib (Suc n)" |
35 lemma [simp]: "0 < fib (Suc n)" |
36 by (induct n rule: fib.induct) (simp+) |
36 by (induct n rule: fib.induct) (simp+) |
37 |
37 |