equal
deleted
inserted
replaced
15 \bigskip |
15 \bigskip |
16 *} |
16 *} |
17 |
17 |
18 fun fib :: "nat \<Rightarrow> nat" |
18 fun fib :: "nat \<Rightarrow> nat" |
19 where |
19 where |
20 "fib 0 = 0" |
20 "fib 0 = 0" |
21 | "fib (Suc 0) = 1" |
21 | "fib (Suc 0) = 1" |
22 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
22 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
23 |
23 |
24 text {* |
24 text {* |
25 \medskip The difficulty in these proofs is to ensure that the |
25 \medskip The difficulty in these proofs is to ensure that the |
26 induction hypotheses are applied before the definition of @{term |
26 induction hypotheses are applied before the definition of @{term |
36 by (rule fib_2) |
36 by (rule fib_2) |
37 |
37 |
38 text {* \medskip Concrete Mathematics, page 280 *} |
38 text {* \medskip Concrete Mathematics, page 280 *} |
39 |
39 |
40 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
40 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
41 apply (induct n rule: fib.induct) |
41 proof (induct n rule: fib.induct) |
42 prefer 3 |
42 case 1 show ?case by simp |
43 txt {* simplify the LHS just enough to apply the induction hypotheses *} |
43 next |
44 apply (simp add: fib_Suc3) |
44 case 2 show ?case by (simp add: fib_2) |
45 apply (simp_all add: fib_2 add_mult_distrib2) |
45 next |
46 done |
46 case 3 thus ?case by (simp add: fib_2 add_mult_distrib2) |
|
47 qed |
47 |
48 |
48 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0" |
49 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0" |
49 apply (induct n rule: fib.induct) |
50 apply (induct n rule: fib.induct) |
50 apply (simp_all add: fib_2) |
51 apply (simp_all add: fib_2) |
51 done |
52 done |
70 case 1 thus ?case by (simp add: fib_2) |
71 case 1 thus ?case by (simp add: fib_2) |
71 next |
72 next |
72 case 2 thus ?case by (simp add: fib_2 mod_Suc) |
73 case 2 thus ?case by (simp add: fib_2 mod_Suc) |
73 next |
74 next |
74 case (3 x) |
75 case (3 x) |
75 have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
76 have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
76 with prems show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2 |
77 with "3.hyps" show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2) |
77 mod_Suc zmult_int [symmetric]) |
|
78 qed |
78 qed |
79 |
79 |
80 text{*We now obtain a version for the natural numbers via the coercion |
80 text{*We now obtain a version for the natural numbers via the coercion |
81 function @{term int}.*} |
81 function @{term int}.*} |
82 theorem fib_Cassini: |
82 theorem fib_Cassini: |