author | wenzelm |
Sat, 06 Oct 2001 00:02:46 +0200 | |
changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 11809 | c9ffdd63dd93 |
permissions | -rw-r--r-- |
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 |
||
10007 | 16 |
header {* Fib and Gcd commute *} |
8051 | 17 |
|
10007 | 18 |
theory Fibonacci = Primes: |
8051 | 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}.} |
10007 | 24 |
*} |
8051 | 25 |
|
26 |
||
10007 | 27 |
subsection {* Fibonacci numbers *} |
8051 | 28 |
|
10007 | 29 |
consts fib :: "nat => nat" |
8051 | 30 |
recdef fib less_than |
31 |
"fib 0 = 0" |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
32 |
"fib (Suc 0) = 1" |
10007 | 33 |
"fib (Suc (Suc x)) = fib x + fib (Suc x)" |
8051 | 34 |
|
10007 | 35 |
lemma [simp]: "0 < fib (Suc n)" |
36 |
by (induct n rule: fib.induct) (simp+) |
|
8051 | 37 |
|
38 |
||
10007 | 39 |
text {* Alternative induction rule. *} |
8051 | 40 |
|
8304 | 41 |
theorem fib_induct: |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
42 |
"P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)" |
10007 | 43 |
by (induct rule: fib.induct, simp+) |
8051 | 44 |
|
45 |
||
46 |
||
10007 | 47 |
subsection {* Fib and gcd commute *} |
8051 | 48 |
|
10007 | 49 |
text {* A few laws taken from \cite{Concrete-Math}. *} |
8051 | 50 |
|
9659 | 51 |
lemma fib_add: |
8051 | 52 |
"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" |
9659 | 53 |
(is "?P n") |
10007 | 54 |
-- {* see \cite[page 280]{Concrete-Math} *} |
55 |
proof (induct ?P n rule: fib_induct) |
|
56 |
show "?P 0" by simp |
|
57 |
show "?P 1" by simp |
|
58 |
fix n |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
59 |
have "fib (n + 2 + k + 1) |
10007 | 60 |
= fib (n + k + 1) + fib (n + 1 + k + 1)" by simp |
61 |
also assume "fib (n + k + 1) |
|
8051 | 62 |
= fib (k + 1) * fib (n + 1) + fib k * fib n" |
10007 | 63 |
(is " _ = ?R1") |
64 |
also assume "fib (n + 1 + k + 1) |
|
8051 | 65 |
= fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)" |
10007 | 66 |
(is " _ = ?R2") |
67 |
also have "?R1 + ?R2 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
68 |
= fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" |
10007 | 69 |
by (simp add: add_mult_distrib2) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
70 |
finally show "?P (n + 2)" . |
10007 | 71 |
qed |
8051 | 72 |
|
10007 | 73 |
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n") |
74 |
proof (induct ?P n rule: fib_induct) |
|
75 |
show "?P 0" by simp |
|
76 |
show "?P 1" by simp |
|
77 |
fix n |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
78 |
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" |
10007 | 79 |
by simp |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
80 |
also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))" |
10007 | 81 |
by (simp only: gcd_add2') |
82 |
also have "... = gcd (fib (n + 1), fib (n + 1 + 1))" |
|
83 |
by (simp add: gcd_commute) |
|
84 |
also assume "... = 1" |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
85 |
finally show "?P (n + 2)" . |
10007 | 86 |
qed |
8051 | 87 |
|
10007 | 88 |
lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)" |
89 |
proof - |
|
90 |
assume "0 < n" |
|
91 |
hence "gcd (n * k + m, n) = gcd (n, m mod n)" |
|
92 |
by (simp add: gcd_non_0 add_commute) |
|
93 |
also have "... = gcd (m, n)" by (simp! add: gcd_non_0) |
|
94 |
finally show ?thesis . |
|
95 |
qed |
|
8051 | 96 |
|
10007 | 97 |
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" |
98 |
proof (cases m) |
|
99 |
assume "m = 0" |
|
100 |
thus ?thesis by simp |
|
101 |
next |
|
102 |
fix k assume "m = Suc k" |
|
103 |
hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))" |
|
104 |
by (simp add: gcd_commute) |
|
105 |
also have "fib (n + k + 1) |
|
106 |
= fib (k + 1) * fib (n + 1) + fib k * fib n" |
|
107 |
by (rule fib_add) |
|
108 |
also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))" |
|
109 |
by (simp add: gcd_mult_add) |
|
110 |
also have "... = gcd (fib n, fib (k + 1))" |
|
111 |
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
|
112 |
also have "... = gcd (fib m, fib n)" |
|
113 |
by (simp! add: gcd_commute) |
|
114 |
finally show ?thesis . |
|
115 |
qed |
|
8051 | 116 |
|
9659 | 117 |
lemma gcd_fib_diff: |
10007 | 118 |
"m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" |
119 |
proof - |
|
120 |
assume "m <= n" |
|
121 |
have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))" |
|
122 |
by (simp add: gcd_fib_add) |
|
123 |
also have "n - m + m = n" by (simp!) |
|
124 |
finally show ?thesis . |
|
125 |
qed |
|
8051 | 126 |
|
9659 | 127 |
lemma gcd_fib_mod: |
10007 | 128 |
"0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
10408 | 129 |
proof - |
8051 | 130 |
assume m: "0 < m" |
10408 | 131 |
show ?thesis |
132 |
proof (induct n rule: nat_less_induct) |
|
133 |
fix n |
|
134 |
assume hyp: "ALL ma. ma < n |
|
135 |
--> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)" |
|
136 |
show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
|
137 |
proof - |
|
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 cases |
|
142 |
assume "n < m" thus ?thesis by simp |
|
143 |
next |
|
144 |
assume not_lt: "~ n < m" hence le: "m <= n" by simp |
|
145 |
have "n - m < n" by (simp! add: diff_less) |
|
146 |
with hyp have "gcd (fib m, fib ((n - m) mod m)) |
|
147 |
= gcd (fib m, fib (n - m))" by simp |
|
148 |
also from le have "... = gcd (fib m, fib n)" |
|
149 |
by (rule gcd_fib_diff) |
|
150 |
finally have "gcd (fib m, fib ((n - m) mod m)) = |
|
151 |
gcd (fib m, fib n)" . |
|
152 |
with not_lt show ?thesis by simp |
|
153 |
qed |
|
154 |
finally show ?thesis . |
|
155 |
qed |
|
10007 | 156 |
qed |
157 |
qed |
|
8051 | 158 |
|
159 |
||
10007 | 160 |
theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n") |
161 |
proof (induct ?P m n rule: gcd_induct) |
|
162 |
fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp |
|
163 |
fix n :: nat assume n: "0 < n" |
|
164 |
hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0) |
|
165 |
also assume hyp: "fib ... = gcd (fib n, fib (m mod n))" |
|
166 |
also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod) |
|
167 |
also have "... = gcd (fib m, fib n)" by (rule gcd_commute) |
|
168 |
finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" . |
|
169 |
qed |
|
8051 | 170 |
|
10007 | 171 |
end |