equal
deleted
inserted
replaced
13 (Addison-Wesley, 1989) |
13 (Addison-Wesley, 1989) |
14 *) |
14 *) |
15 |
15 |
16 header {* Fib and Gcd commute *} |
16 header {* Fib and Gcd commute *} |
17 |
17 |
18 theory Fibonacci imports Primes begin |
18 theory Fibonacci |
|
19 imports Primes |
|
20 begin |
19 |
21 |
20 text_raw {* |
22 text_raw {* |
21 \footnote{Isar version by Gertrud Bauer. Original tactic script by |
23 \footnote{Isar version by Gertrud Bauer. Original tactic script by |
22 Larry Paulson. A few proofs of laws taken from |
24 Larry Paulson. A few proofs of laws taken from |
23 \cite{Concrete-Math}.} |
25 \cite{Concrete-Math}.} |
24 *} |
26 *} |
25 |
27 |
26 |
28 |
27 subsection {* Fibonacci numbers *} |
29 subsection {* Fibonacci numbers *} |
28 |
30 |
29 consts fib :: "nat => nat" |
31 fun fib :: "nat \<Rightarrow> nat" where |
30 recdef fib less_than |
|
31 "fib 0 = 0" |
32 "fib 0 = 0" |
32 "fib (Suc 0) = 1" |
33 | "fib (Suc 0) = 1" |
33 "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
34 | "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
34 |
35 |
35 lemma [simp]: "0 < fib (Suc n)" |
36 lemma [simp]: "0 < fib (Suc n)" |
36 by (induct n rule: fib.induct) simp_all |
37 by (induct n rule: fib.induct) simp_all |
37 |
38 |
38 |
39 |