author | wenzelm |
Sat, 06 Oct 2001 00:02:46 +0200 | |
changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 11786 | 51ce34ef5113 |
permissions | -rw-r--r-- |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
1 |
(* Title: HOL/NumberTheory/Fib.thy |
9944 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
5 |
*) |
|
6 |
||
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
7 |
header {* The Fibonacci function *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
8 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
9 |
theory Fib = Primes: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
10 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
11 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
12 |
Fibonacci numbers: proofs of laws taken from: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
13 |
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
|
14 |
(Addison-Wesley, 1989) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
15 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
16 |
\bigskip |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
19 |
consts fib :: "nat => nat" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
20 |
recdef fib less_than |
11468 | 21 |
zero: "fib 0 = 0" |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
22 |
one: "fib (Suc 0) = Suc 0" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
23 |
Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
24 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
25 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
26 |
\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
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
31 |
|
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
34 |
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
35 |
apply (rule fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
36 |
done |
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 *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
45 |
apply (simp add: fib.Suc_Suc [of "Suc (m + n)", standard]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
46 |
apply (simp_all (no_asm_simp) add: fib.Suc_Suc add_mult_distrib add_mult_distrib2) |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
49 |
lemma fib_Suc_neq_0 [simp]: "fib (Suc n) \<noteq> 0" |
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 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
54 |
lemma [simp]: "0 < fib (Suc n)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
55 |
apply (simp add: neq0_conv [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
56 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
57 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
58 |
lemma fib_gr_0: "0 < n ==> 0 < fib n" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
59 |
apply (rule not0_implies_Suc [THEN exE]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
60 |
apply auto |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
61 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
62 |
|
9944 | 63 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
64 |
text {* |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
65 |
\medskip Concrete Mathematics, page 278: Cassini's identity. It is |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
66 |
much easier to prove using integers! |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
67 |
*} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
68 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
69 |
lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
70 |
(if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1 |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
71 |
else int (fib (Suc n) * fib (Suc n)) + Numeral1)" |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
72 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
73 |
apply (simp add: fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
74 |
apply (simp add: fib.Suc_Suc mod_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
75 |
apply (simp add: fib.Suc_Suc |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
76 |
add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac) |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
77 |
apply (subgoal_tac "x mod 2 < 2", arith) |
11377
0f16ad464c62
Simprocs for type "nat" no longer introduce numerals unless they are already
paulson
parents:
11049
diff
changeset
|
78 |
apply simp |
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
79 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
80 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
81 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
82 |
text {* \medskip Towards Law 6.111 of Concrete Mathematics *} |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
83 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
84 |
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
|
85 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
86 |
prefer 3 |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
87 |
apply (simp add: gcd_commute fib_Suc3) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
88 |
apply (simp_all add: fib.Suc_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
89 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
90 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
91 |
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
92 |
apply (simp (no_asm) add: gcd_commute [of "fib m"]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
93 |
apply (case_tac "m = 0") |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
94 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
95 |
apply (clarify dest!: not0_implies_Suc) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
96 |
apply (simp add: fib_add) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
97 |
apply (simp add: add_commute gcd_non_0) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
98 |
apply (simp add: gcd_non_0 [symmetric]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
99 |
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
|
100 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
101 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
102 |
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
103 |
apply (rule gcd_fib_add [symmetric, THEN trans]) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
104 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
105 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
106 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
107 |
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
|
108 |
apply (induct n rule: nat_less_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
109 |
apply (subst mod_if) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
110 |
apply (simp add: gcd_fib_diff mod_geq not_less_iff_le diff_less) |
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 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
|
114 |
apply (induct m n rule: gcd_induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
115 |
apply simp |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
116 |
apply (simp add: gcd_non_0) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
117 |
apply (simp add: gcd_commute gcd_fib_mod) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
118 |
done |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
119 |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
120 |
lemma fib_mult_eq_setsum: |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
121 |
"fib (Suc n) * fib n = setsum (\<lambda>k. fib k * fib k) (atMost n)" |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
122 |
apply (induct n rule: fib.induct) |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
10147
diff
changeset
|
123 |
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
|
124 |
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
|
125 |
done |
9944 | 126 |
|
127 |
end |