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