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