equal
deleted
inserted
replaced
50 text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close> |
50 text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close> |
51 |
51 |
52 lemma fib_add: |
52 lemma fib_add: |
53 "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" |
53 "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" |
54 (is "?P n") |
54 (is "?P n") |
55 -- \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close> |
55 \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close> |
56 proof (induct n rule: fib_induct) |
56 proof (induct n rule: fib_induct) |
57 show "?P 0" by simp |
57 show "?P 0" by simp |
58 show "?P 1" by simp |
58 show "?P 1" by simp |
59 fix n |
59 fix n |
60 have "fib (n + 2 + k + 1) |
60 have "fib (n + 2 + k + 1) |