author | wenzelm |
Tue, 07 Nov 2006 19:40:13 +0100 | |
changeset 21233 | 5a5c8ea5f66a |
parent 20432 | 07ec57376051 |
child 23315 | df3a7e9ebadb |
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)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
70 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
71 |
apply (simp add: fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
72 |
apply (simp add: fib.Suc_Suc mod_Suc) |
15628 | 73 |
apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2 |
74 |
mod_Suc zmult_int [symmetric]) |
|
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20272
diff
changeset
|
75 |
apply (presburger (no_abs)) |
15628 | 76 |
done |
77 |
||
78 |
text{*We now obtain a version for the natural numbers via the coercion |
|
79 |
function @{term int}.*} |
|
80 |
theorem fib_Cassini: |
|
81 |
"fib (Suc (Suc n)) * fib n = |
|
82 |
(if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1 |
|
83 |
else fib (Suc n) * fib (Suc n) + 1)" |
|
84 |
apply (rule int_int_eq [THEN iffD1]) |
|
85 |
apply (simp add: fib_Cassini_int) |
|
86 |
apply (subst zdiff_int [symmetric]) |
|
87 |
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
|
88 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
89 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
90 |
|
15628 | 91 |
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
|
92 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
93 |
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
|
94 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
95 |
prefer 3 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
96 |
apply (simp add: gcd_commute fib_Suc3) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
97 |
apply (simp_all add: fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
98 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
99 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
100 |
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" |
15628 | 101 |
apply (simp add: gcd_commute [of "fib m"]) |
102 |
apply (case_tac m) |
|
103 |
apply simp |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
104 |
apply (simp add: fib_add) |
15628 | 105 |
apply (simp add: add_commute gcd_non_0 [OF fib_Suc_gr_0]) |
106 |
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
|
107 |
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
|
108 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
109 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
110 |
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" |
15628 | 111 |
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
|
112 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
113 |
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
114 |
apply (induct n rule: nat_less_induct) |
15628 | 115 |
apply (simp add: mod_if gcd_fib_diff mod_geq) |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
116 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
117 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
118 |
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
|
119 |
apply (induct m n rule: gcd_induct) |
15628 | 120 |
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
|
121 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
122 |
|
15628 | 123 |
theorem fib_mult_eq_setsum: |
11786 | 124 |
"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
|
125 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
126 |
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
|
127 |
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
|
128 |
done |
9944 | 129 |
|
130 |
end |