wenzelm@11049
|
1 |
(* Title: HOL/NumberTheory/Fib.thy
|
paulson@9944
|
2 |
ID: $Id$
|
paulson@9944
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@9944
|
4 |
Copyright 1997 University of Cambridge
|
paulson@9944
|
5 |
*)
|
paulson@9944
|
6 |
|
wenzelm@11049
|
7 |
header {* The Fibonacci function *}
|
paulson@9944
|
8 |
|
wenzelm@11049
|
9 |
theory Fib = Primes:
|
wenzelm@11049
|
10 |
|
wenzelm@11049
|
11 |
text {*
|
wenzelm@11049
|
12 |
Fibonacci numbers: proofs of laws taken from:
|
wenzelm@11049
|
13 |
R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics.
|
wenzelm@11049
|
14 |
(Addison-Wesley, 1989)
|
wenzelm@11049
|
15 |
|
wenzelm@11049
|
16 |
\bigskip
|
wenzelm@11049
|
17 |
*}
|
wenzelm@11049
|
18 |
|
wenzelm@11049
|
19 |
consts fib :: "nat => nat"
|
wenzelm@11049
|
20 |
recdef fib less_than
|
paulson@11468
|
21 |
zero: "fib 0 = 0"
|
wenzelm@11701
|
22 |
one: "fib (Suc 0) = Suc 0"
|
wenzelm@11049
|
23 |
Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
|
wenzelm@11049
|
24 |
|
wenzelm@11049
|
25 |
text {*
|
wenzelm@11049
|
26 |
\medskip The difficulty in these proofs is to ensure that the
|
wenzelm@11049
|
27 |
induction hypotheses are applied before the definition of @{term
|
wenzelm@11049
|
28 |
fib}. Towards this end, the @{term fib} equations are not declared
|
wenzelm@11049
|
29 |
to the Simplifier and are applied very selectively at first.
|
wenzelm@11049
|
30 |
*}
|
wenzelm@11049
|
31 |
|
wenzelm@11049
|
32 |
declare fib.Suc_Suc [simp del]
|
wenzelm@11049
|
33 |
|
wenzelm@11049
|
34 |
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
|
wenzelm@11049
|
35 |
apply (rule fib.Suc_Suc)
|
wenzelm@11049
|
36 |
done
|
wenzelm@11049
|
37 |
|
wenzelm@11049
|
38 |
|
wenzelm@11049
|
39 |
text {* \medskip Concrete Mathematics, page 280 *}
|
wenzelm@11049
|
40 |
|
wenzelm@11049
|
41 |
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
|
wenzelm@11049
|
42 |
apply (induct n rule: fib.induct)
|
wenzelm@11049
|
43 |
prefer 3
|
wenzelm@11049
|
44 |
txt {* simplify the LHS just enough to apply the induction hypotheses *}
|
wenzelm@11049
|
45 |
apply (simp add: fib.Suc_Suc [of "Suc (m + n)", standard])
|
wenzelm@11049
|
46 |
apply (simp_all (no_asm_simp) add: fib.Suc_Suc add_mult_distrib add_mult_distrib2)
|
wenzelm@11049
|
47 |
done
|
wenzelm@11049
|
48 |
|
wenzelm@11049
|
49 |
lemma fib_Suc_neq_0 [simp]: "fib (Suc n) \<noteq> 0"
|
wenzelm@11049
|
50 |
apply (induct n rule: fib.induct)
|
wenzelm@11049
|
51 |
apply (simp_all add: fib.Suc_Suc)
|
wenzelm@11049
|
52 |
done
|
wenzelm@11049
|
53 |
|
wenzelm@11049
|
54 |
lemma [simp]: "0 < fib (Suc n)"
|
wenzelm@11049
|
55 |
apply (simp add: neq0_conv [symmetric])
|
wenzelm@11049
|
56 |
done
|
wenzelm@11049
|
57 |
|
wenzelm@11049
|
58 |
lemma fib_gr_0: "0 < n ==> 0 < fib n"
|
wenzelm@11049
|
59 |
apply (rule not0_implies_Suc [THEN exE])
|
wenzelm@11049
|
60 |
apply auto
|
wenzelm@11049
|
61 |
done
|
wenzelm@11049
|
62 |
|
wenzelm@11049
|
63 |
|
wenzelm@11049
|
64 |
text {*
|
wenzelm@11049
|
65 |
\medskip Concrete Mathematics, page 278: Cassini's identity. It is
|
wenzelm@11049
|
66 |
much easier to prove using integers!
|
wenzelm@11049
|
67 |
*}
|
wenzelm@11049
|
68 |
|
wenzelm@11049
|
69 |
lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
|
wenzelm@11704
|
70 |
(if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1
|
wenzelm@11701
|
71 |
else int (fib (Suc n) * fib (Suc n)) + Numeral1)"
|
wenzelm@11049
|
72 |
apply (induct n rule: fib.induct)
|
wenzelm@11049
|
73 |
apply (simp add: fib.Suc_Suc)
|
wenzelm@11049
|
74 |
apply (simp add: fib.Suc_Suc mod_Suc)
|
wenzelm@11049
|
75 |
apply (simp add: fib.Suc_Suc
|
wenzelm@11049
|
76 |
add_mult_distrib add_mult_distrib2 mod_Suc zmult_int [symmetric] zmult_ac)
|
wenzelm@11704
|
77 |
apply (subgoal_tac "x mod 2 < 2", arith)
|
paulson@11377
|
78 |
apply simp
|
wenzelm@11049
|
79 |
done
|
wenzelm@11049
|
80 |
|
wenzelm@11049
|
81 |
|
wenzelm@11049
|
82 |
text {* \medskip Towards Law 6.111 of Concrete Mathematics *}
|
wenzelm@11049
|
83 |
|
wenzelm@11701
|
84 |
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0"
|
wenzelm@11049
|
85 |
apply (induct n rule: fib.induct)
|
wenzelm@11049
|
86 |
prefer 3
|
wenzelm@11049
|
87 |
apply (simp add: gcd_commute fib_Suc3)
|
wenzelm@11049
|
88 |
apply (simp_all add: fib.Suc_Suc)
|
wenzelm@11049
|
89 |
done
|
wenzelm@11049
|
90 |
|
wenzelm@11049
|
91 |
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
|
wenzelm@11049
|
92 |
apply (simp (no_asm) add: gcd_commute [of "fib m"])
|
wenzelm@11049
|
93 |
apply (case_tac "m = 0")
|
wenzelm@11049
|
94 |
apply simp
|
wenzelm@11049
|
95 |
apply (clarify dest!: not0_implies_Suc)
|
wenzelm@11049
|
96 |
apply (simp add: fib_add)
|
wenzelm@11049
|
97 |
apply (simp add: add_commute gcd_non_0)
|
wenzelm@11049
|
98 |
apply (simp add: gcd_non_0 [symmetric])
|
wenzelm@11049
|
99 |
apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel)
|
wenzelm@11049
|
100 |
done
|
wenzelm@11049
|
101 |
|
wenzelm@11049
|
102 |
lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
|
wenzelm@11049
|
103 |
apply (rule gcd_fib_add [symmetric, THEN trans])
|
wenzelm@11049
|
104 |
apply simp
|
wenzelm@11049
|
105 |
done
|
wenzelm@11049
|
106 |
|
wenzelm@11049
|
107 |
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
|
wenzelm@11049
|
108 |
apply (induct n rule: nat_less_induct)
|
wenzelm@11049
|
109 |
apply (subst mod_if)
|
wenzelm@11049
|
110 |
apply (simp add: gcd_fib_diff mod_geq not_less_iff_le diff_less)
|
wenzelm@11049
|
111 |
done
|
wenzelm@11049
|
112 |
|
wenzelm@11049
|
113 |
lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" -- {* Law 6.111 *}
|
wenzelm@11049
|
114 |
apply (induct m n rule: gcd_induct)
|
wenzelm@11049
|
115 |
apply simp
|
wenzelm@11049
|
116 |
apply (simp add: gcd_non_0)
|
wenzelm@11049
|
117 |
apply (simp add: gcd_commute gcd_fib_mod)
|
wenzelm@11049
|
118 |
done
|
wenzelm@11049
|
119 |
|
wenzelm@11049
|
120 |
lemma fib_mult_eq_setsum:
|
wenzelm@11049
|
121 |
"fib (Suc n) * fib n = setsum (\<lambda>k. fib k * fib k) (atMost n)"
|
wenzelm@11049
|
122 |
apply (induct n rule: fib.induct)
|
wenzelm@11049
|
123 |
apply (auto simp add: atMost_Suc fib.Suc_Suc)
|
wenzelm@11049
|
124 |
apply (simp add: add_mult_distrib add_mult_distrib2)
|
wenzelm@11049
|
125 |
done
|
paulson@9944
|
126 |
|
paulson@9944
|
127 |
end
|