author | wenzelm |
Tue, 24 Jul 2007 19:44:33 +0200 | |
changeset 23962 | e0358fac0541 |
parent 23688 | 7cd68def72b2 |
child 24549 | c8cee92b06bc |
permissions | -rw-r--r-- |
15628 | 1 |
(* ID: $Id$ |
9944 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1997 University of Cambridge |
|
4 |
*) |
|
5 |
||
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
6 |
header {* The Fibonacci function *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
7 |
|
16417 | 8 |
theory Fib imports Primes begin |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
9 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
10 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
11 |
Fibonacci numbers: proofs of laws taken from: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
12 |
R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
13 |
(Addison-Wesley, 1989) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
14 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
15 |
\bigskip |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
16 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
17 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
18 |
consts fib :: "nat => nat" |
15628 | 19 |
recdef fib "measure (\<lambda>x. x)" |
20 |
zero: "fib 0 = 0" |
|
21 |
one: "fib (Suc 0) = Suc 0" |
|
22 |
Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
23 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
24 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
25 |
\medskip The difficulty in these proofs is to ensure that the |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
26 |
induction hypotheses are applied before the definition of @{term |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
27 |
fib}. Towards this end, the @{term fib} equations are not declared |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
28 |
to the Simplifier and are applied very selectively at first. |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
29 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
30 |
|
15628 | 31 |
text{*We disable @{text fib.Suc_Suc} for simplification ...*} |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
32 |
declare fib.Suc_Suc [simp del] |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
33 |
|
15628 | 34 |
text{*...then prove a version that has a more restrictive pattern.*} |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
35 |
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))" |
15628 | 36 |
by (rule fib.Suc_Suc) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
37 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
38 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
39 |
text {* \medskip Concrete Mathematics, page 280 *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
40 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
41 |
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
42 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
43 |
prefer 3 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
44 |
txt {* simplify the LHS just enough to apply the induction hypotheses *} |
15628 | 45 |
apply (simp add: fib_Suc3) |
46 |
apply (simp_all add: fib.Suc_Suc add_mult_distrib2) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
47 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
48 |
|
15628 | 49 |
lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
50 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
51 |
apply (simp_all add: fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
52 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
53 |
|
15628 | 54 |
lemma fib_Suc_gr_0: "0 < fib (Suc n)" |
55 |
by (insert fib_Suc_neq_0 [of n], simp) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
56 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
57 |
lemma fib_gr_0: "0 < n ==> 0 < fib n" |
15628 | 58 |
by (case_tac n, auto simp add: fib_Suc_gr_0) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
59 |
|
9944 | 60 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
61 |
text {* |
15628 | 62 |
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is |
63 |
much easier using integers, not natural numbers! |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
64 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
65 |
|
15628 | 66 |
lemma fib_Cassini_int: |
15003 | 67 |
"int (fib (Suc (Suc n)) * fib n) = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11786
diff
changeset
|
68 |
(if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1 |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11786
diff
changeset
|
69 |
else int (fib (Suc n) * fib (Suc n)) + 1)" |
23315 | 70 |
proof(induct n rule: fib.induct) |
71 |
case 1 thus ?case by (simp add: fib.Suc_Suc) |
|
72 |
next |
|
73 |
case 2 thus ?case by (simp add: fib.Suc_Suc mod_Suc) |
|
74 |
next |
|
75 |
case (3 x) |
|
76 |
have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger |
|
77 |
with prems show ?case by (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2 |
|
15628 | 78 |
mod_Suc zmult_int [symmetric]) |
23315 | 79 |
qed |
15628 | 80 |
|
81 |
text{*We now obtain a version for the natural numbers via the coercion |
|
82 |
function @{term int}.*} |
|
83 |
theorem fib_Cassini: |
|
84 |
"fib (Suc (Suc n)) * fib n = |
|
85 |
(if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 |
|
86 |
else fib (Suc n) * fib (Suc n) + 1)" |
|
87 |
apply (rule int_int_eq [THEN iffD1]) |
|
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23365
diff
changeset
|
88 |
apply (simp add: fib_Cassini_int) |
15628 | 89 |
apply (subst zdiff_int [symmetric]) |
90 |
apply (insert fib_Suc_gr_0 [of n], simp_all) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
91 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
92 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
93 |
|
15628 | 94 |
text {* \medskip Toward Law 6.111 of Concrete Mathematics *} |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
95 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
96 |
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
97 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
98 |
prefer 3 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
99 |
apply (simp add: gcd_commute fib_Suc3) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
100 |
apply (simp_all add: fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
101 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
102 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
103 |
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" |
15628 | 104 |
apply (simp add: gcd_commute [of "fib m"]) |
105 |
apply (case_tac m) |
|
106 |
apply simp |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
107 |
apply (simp add: fib_add) |
15628 | 108 |
apply (simp add: add_commute gcd_non_0 [OF fib_Suc_gr_0]) |
109 |
apply (simp add: gcd_non_0 [OF fib_Suc_gr_0, symmetric]) |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
110 |
apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
111 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
112 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
113 |
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" |
15628 | 114 |
by (simp add: gcd_fib_add [symmetric, of _ "n-m"]) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
115 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
116 |
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
23688 | 117 |
proof (induct n rule: less_induct) |
118 |
case (less n) |
|
119 |
from less.prems have pos_m: "0 < m" . |
|
120 |
show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
|
121 |
proof (cases "m < n") |
|
122 |
case True note m_n = True |
|
123 |
then have m_n': "m \<le> n" by auto |
|
124 |
with pos_m have pos_n: "0 < n" by auto |
|
125 |
with pos_m m_n have diff: "n - m < n" by auto |
|
126 |
have "gcd (fib m, fib (n mod m)) = gcd (fib m, fib ((n - m) mod m))" |
|
127 |
by (simp add: mod_if [of n]) (insert m_n, auto) |
|
128 |
also have "\<dots> = gcd (fib m, fib (n - m))" by (simp add: less.hyps diff pos_m) |
|
129 |
also have "\<dots> = gcd (fib m, fib n)" by (simp add: gcd_fib_diff m_n') |
|
130 |
finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" . |
|
131 |
next |
|
132 |
case False then show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
|
133 |
by (cases "m = n") auto |
|
134 |
qed |
|
135 |
qed |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
136 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
137 |
lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" -- {* Law 6.111 *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
138 |
apply (induct m n rule: gcd_induct) |
15628 | 139 |
apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
140 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
141 |
|
15628 | 142 |
theorem fib_mult_eq_setsum: |
11786 | 143 |
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
144 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
145 |
apply (auto simp add: atMost_Suc fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
146 |
apply (simp add: add_mult_distrib add_mult_distrib2) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
147 |
done |
9944 | 148 |
|
149 |
end |