1 (* Title: HOL/Old_Number_Theory/Fib.thy |
1 (* Title: HOL/Old_Number_Theory/Fib.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1997 University of Cambridge |
3 Copyright 1997 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* The Fibonacci function *} |
6 section \<open>The Fibonacci function\<close> |
7 |
7 |
8 theory Fib |
8 theory Fib |
9 imports Primes |
9 imports Primes |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text \<open> |
13 Fibonacci numbers: proofs of laws taken from: |
13 Fibonacci numbers: proofs of laws taken from: |
14 R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. |
14 R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. |
15 (Addison-Wesley, 1989) |
15 (Addison-Wesley, 1989) |
16 |
16 |
17 \bigskip |
17 \bigskip |
18 *} |
18 \<close> |
19 |
19 |
20 fun fib :: "nat \<Rightarrow> nat" |
20 fun fib :: "nat \<Rightarrow> nat" |
21 where |
21 where |
22 "fib 0 = 0" |
22 "fib 0 = 0" |
23 | "fib (Suc 0) = 1" |
23 | "fib (Suc 0) = 1" |
24 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
24 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
25 |
25 |
26 text {* |
26 text \<open> |
27 \medskip The difficulty in these proofs is to ensure that the |
27 \medskip The difficulty in these proofs is to ensure that the |
28 induction hypotheses are applied before the definition of @{term |
28 induction hypotheses are applied before the definition of @{term |
29 fib}. Towards this end, the @{term fib} equations are not declared |
29 fib}. Towards this end, the @{term fib} equations are not declared |
30 to the Simplifier and are applied very selectively at first. |
30 to the Simplifier and are applied very selectively at first. |
31 *} |
31 \<close> |
32 |
32 |
33 text{*We disable @{text fib.fib_2fib_2} for simplification ...*} |
33 text\<open>We disable @{text fib.fib_2fib_2} for simplification ...\<close> |
34 declare fib_2 [simp del] |
34 declare fib_2 [simp del] |
35 |
35 |
36 text{*...then prove a version that has a more restrictive pattern.*} |
36 text\<open>...then prove a version that has a more restrictive pattern.\<close> |
37 lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))" |
37 lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))" |
38 by (rule fib_2) |
38 by (rule fib_2) |
39 |
39 |
40 text {* \medskip Concrete Mathematics, page 280 *} |
40 text \<open>\medskip Concrete Mathematics, page 280\<close> |
41 |
41 |
42 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
42 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
43 proof (induct n rule: fib.induct) |
43 proof (induct n rule: fib.induct) |
44 case 1 show ?case by simp |
44 case 1 show ?case by simp |
45 next |
45 next |
58 |
58 |
59 lemma fib_gr_0: "0 < n ==> 0 < fib n" |
59 lemma fib_gr_0: "0 < n ==> 0 < fib n" |
60 by (case_tac n, auto simp add: fib_Suc_gr_0) |
60 by (case_tac n, auto simp add: fib_Suc_gr_0) |
61 |
61 |
62 |
62 |
63 text {* |
63 text \<open> |
64 \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is |
64 \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is |
65 much easier using integers, not natural numbers! |
65 much easier using integers, not natural numbers! |
66 *} |
66 \<close> |
67 |
67 |
68 lemma fib_Cassini_int: |
68 lemma fib_Cassini_int: |
69 "int (fib (Suc (Suc n)) * fib n) = |
69 "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)) - 1 |
71 else int (fib (Suc n) * fib (Suc n)) + 1)" |
71 else int (fib (Suc n) * fib (Suc n)) + 1)" |
77 case (3 x) |
77 case (3 x) |
78 have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
78 have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
79 with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2) |
79 with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2) |
80 qed |
80 qed |
81 |
81 |
82 text{*We now obtain a version for the natural numbers via the coercion |
82 text\<open>We now obtain a version for the natural numbers via the coercion |
83 function @{term int}.*} |
83 function @{term int}.\<close> |
84 theorem fib_Cassini: |
84 theorem fib_Cassini: |
85 "fib (Suc (Suc n)) * fib n = |
85 "fib (Suc (Suc n)) * fib n = |
86 (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 |
86 (if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 |
87 else fib (Suc n) * fib (Suc n) + 1)" |
87 else fib (Suc n) * fib (Suc n) + 1)" |
88 apply (rule int_int_eq [THEN iffD1]) |
88 apply (rule int_int_eq [THEN iffD1]) |
90 apply (subst of_nat_diff) |
90 apply (subst of_nat_diff) |
91 apply (insert fib_Suc_gr_0 [of n], simp_all) |
91 apply (insert fib_Suc_gr_0 [of n], simp_all) |
92 done |
92 done |
93 |
93 |
94 |
94 |
95 text {* \medskip Toward Law 6.111 of Concrete Mathematics *} |
95 text \<open>\medskip Toward Law 6.111 of Concrete Mathematics\<close> |
96 |
96 |
97 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0" |
97 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0" |
98 apply (induct n rule: fib.induct) |
98 apply (induct n rule: fib.induct) |
99 prefer 3 |
99 prefer 3 |
100 apply (simp add: gcd_commute fib_Suc3) |
100 apply (simp add: gcd_commute fib_Suc3) |
133 case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
133 case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
134 by (cases "m = n") auto |
134 by (cases "m = n") auto |
135 qed |
135 qed |
136 qed |
136 qed |
137 |
137 |
138 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" -- {* Law 6.111 *} |
138 lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" -- \<open>Law 6.111\<close> |
139 apply (induct m n rule: gcd_induct) |
139 apply (induct m n rule: gcd_induct) |
140 apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod) |
140 apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod) |
141 done |
141 done |
142 |
142 |
143 theorem fib_mult_eq_setsum: |
143 theorem fib_mult_eq_setsum: |