1 (* Title: HOL/Isar_examples/Fibonacci.thy |
|
2 Author: Gertrud Bauer |
|
3 Copyright 1999 Technische Universitaet Muenchen |
|
4 |
|
5 The Fibonacci function. Demonstrates the use of recdef. Original |
|
6 tactic script by Lawrence C Paulson. |
|
7 |
|
8 Fibonacci numbers: proofs of laws taken from |
|
9 |
|
10 R. L. Graham, D. E. Knuth, O. Patashnik. |
|
11 Concrete Mathematics. |
|
12 (Addison-Wesley, 1989) |
|
13 *) |
|
14 |
|
15 header {* Fib and Gcd commute *} |
|
16 |
|
17 theory Fibonacci |
|
18 imports Primes |
|
19 begin |
|
20 |
|
21 text_raw {* |
|
22 \footnote{Isar version by Gertrud Bauer. Original tactic script by |
|
23 Larry Paulson. A few proofs of laws taken from |
|
24 \cite{Concrete-Math}.} |
|
25 *} |
|
26 |
|
27 |
|
28 subsection {* Fibonacci numbers *} |
|
29 |
|
30 fun fib :: "nat \<Rightarrow> nat" where |
|
31 "fib 0 = 0" |
|
32 | "fib (Suc 0) = 1" |
|
33 | "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
|
34 |
|
35 lemma [simp]: "0 < fib (Suc n)" |
|
36 by (induct n rule: fib.induct) simp_all |
|
37 |
|
38 |
|
39 text {* Alternative induction rule. *} |
|
40 |
|
41 theorem fib_induct: |
|
42 "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)" |
|
43 by (induct rule: fib.induct) simp_all |
|
44 |
|
45 |
|
46 subsection {* Fib and gcd commute *} |
|
47 |
|
48 text {* A few laws taken from \cite{Concrete-Math}. *} |
|
49 |
|
50 lemma fib_add: |
|
51 "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" |
|
52 (is "?P n") |
|
53 -- {* see \cite[page 280]{Concrete-Math} *} |
|
54 proof (induct n rule: fib_induct) |
|
55 show "?P 0" by simp |
|
56 show "?P 1" by simp |
|
57 fix n |
|
58 have "fib (n + 2 + k + 1) |
|
59 = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp |
|
60 also assume "fib (n + k + 1) |
|
61 = fib (k + 1) * fib (n + 1) + fib k * fib n" |
|
62 (is " _ = ?R1") |
|
63 also assume "fib (n + 1 + k + 1) |
|
64 = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)" |
|
65 (is " _ = ?R2") |
|
66 also have "?R1 + ?R2 |
|
67 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" |
|
68 by (simp add: add_mult_distrib2) |
|
69 finally show "?P (n + 2)" . |
|
70 qed |
|
71 |
|
72 lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n") |
|
73 proof (induct n rule: fib_induct) |
|
74 show "?P 0" by simp |
|
75 show "?P 1" by simp |
|
76 fix n |
|
77 have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" |
|
78 by simp |
|
79 also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))" |
|
80 by (simp only: gcd_add2') |
|
81 also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))" |
|
82 by (simp add: gcd_commute) |
|
83 also assume "... = 1" |
|
84 finally show "?P (n + 2)" . |
|
85 qed |
|
86 |
|
87 lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n" |
|
88 proof - |
|
89 assume "0 < n" |
|
90 then have "gcd (n * k + m) n = gcd n (m mod n)" |
|
91 by (simp add: gcd_non_0 add_commute) |
|
92 also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0) |
|
93 finally show ?thesis . |
|
94 qed |
|
95 |
|
96 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" |
|
97 proof (cases m) |
|
98 case 0 |
|
99 then show ?thesis by simp |
|
100 next |
|
101 case (Suc k) |
|
102 then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" |
|
103 by (simp add: gcd_commute) |
|
104 also have "fib (n + k + 1) |
|
105 = fib (k + 1) * fib (n + 1) + fib k * fib n" |
|
106 by (rule fib_add) |
|
107 also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" |
|
108 by (simp add: gcd_mult_add) |
|
109 also have "... = gcd (fib n) (fib (k + 1))" |
|
110 by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
|
111 also have "... = gcd (fib m) (fib n)" |
|
112 using Suc by (simp add: gcd_commute) |
|
113 finally show ?thesis . |
|
114 qed |
|
115 |
|
116 lemma gcd_fib_diff: |
|
117 assumes "m <= n" |
|
118 shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" |
|
119 proof - |
|
120 have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))" |
|
121 by (simp add: gcd_fib_add) |
|
122 also from `m <= n` have "n - m + m = n" by simp |
|
123 finally show ?thesis . |
|
124 qed |
|
125 |
|
126 lemma gcd_fib_mod: |
|
127 assumes "0 < m" |
|
128 shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" |
|
129 proof (induct n rule: nat_less_induct) |
|
130 case (1 n) note hyp = this |
|
131 show ?case |
|
132 proof - |
|
133 have "n mod m = (if n < m then n else (n - m) mod m)" |
|
134 by (rule mod_if) |
|
135 also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)" |
|
136 proof (cases "n < m") |
|
137 case True then show ?thesis by simp |
|
138 next |
|
139 case False then have "m <= n" by simp |
|
140 from `0 < m` and False have "n - m < n" by simp |
|
141 with hyp have "gcd (fib m) (fib ((n - m) mod m)) |
|
142 = gcd (fib m) (fib (n - m))" by simp |
|
143 also have "... = gcd (fib m) (fib n)" |
|
144 using `m <= n` by (rule gcd_fib_diff) |
|
145 finally have "gcd (fib m) (fib ((n - m) mod m)) = |
|
146 gcd (fib m) (fib n)" . |
|
147 with False show ?thesis by simp |
|
148 qed |
|
149 finally show ?thesis . |
|
150 qed |
|
151 qed |
|
152 |
|
153 |
|
154 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n") |
|
155 proof (induct m n rule: gcd_induct) |
|
156 fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp |
|
157 fix n :: nat assume n: "0 < n" |
|
158 then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0) |
|
159 also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))" |
|
160 also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod) |
|
161 also have "... = gcd (fib m) (fib n)" by (rule gcd_commute) |
|
162 finally show "fib (gcd m n) = gcd (fib m) (fib n)" . |
|
163 qed |
|
164 |
|
165 end |
|