17 *} |
17 *} |
18 |
18 |
19 consts fib :: "nat => nat" |
19 consts fib :: "nat => nat" |
20 recdef fib less_than |
20 recdef fib less_than |
21 zero: "fib 0 = 0" |
21 zero: "fib 0 = 0" |
22 one: "fib 1' = 1'" |
22 one: "fib (Suc 0) = Suc 0" |
23 Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
23 Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
24 |
24 |
25 text {* |
25 text {* |
26 \medskip The difficulty in these proofs is to ensure that the |
26 \medskip The difficulty in these proofs is to ensure that the |
27 induction hypotheses are applied before the definition of @{term |
27 induction hypotheses are applied before the definition of @{term |
65 \medskip Concrete Mathematics, page 278: Cassini's identity. It is |
65 \medskip Concrete Mathematics, page 278: Cassini's identity. It is |
66 much easier to prove using integers! |
66 much easier to prove using integers! |
67 *} |
67 *} |
68 |
68 |
69 lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = |
69 lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = |
70 (if n mod #2 = 0 then int (fib (Suc n) * fib (Suc n)) - #1 |
70 (if n mod # 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1 |
71 else int (fib (Suc n) * fib (Suc n)) + #1)" |
71 else int (fib (Suc n) * fib (Suc n)) + Numeral1)" |
72 apply (induct n rule: fib.induct) |
72 apply (induct n rule: fib.induct) |
73 apply (simp add: fib.Suc_Suc) |
73 apply (simp add: fib.Suc_Suc) |
74 apply (simp add: fib.Suc_Suc mod_Suc) |
74 apply (simp add: fib.Suc_Suc mod_Suc) |
75 apply (simp add: fib.Suc_Suc |
75 apply (simp add: fib.Suc_Suc |
76 add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac) |
76 add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac) |
77 apply (subgoal_tac "x mod #2 < #2", arith) |
77 apply (subgoal_tac "x mod # 2 < # 2", arith) |
78 apply simp |
78 apply simp |
79 done |
79 done |
80 |
80 |
81 |
81 |
82 text {* \medskip Towards Law 6.111 of Concrete Mathematics *} |
82 text {* \medskip Towards Law 6.111 of Concrete Mathematics *} |
83 |
83 |
84 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1'" |
84 lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0" |
85 apply (induct n rule: fib.induct) |
85 apply (induct n rule: fib.induct) |
86 prefer 3 |
86 prefer 3 |
87 apply (simp add: gcd_commute fib_Suc3) |
87 apply (simp add: gcd_commute fib_Suc3) |
88 apply (simp_all add: fib.Suc_Suc) |
88 apply (simp_all add: fib.Suc_Suc) |
89 done |
89 done |