1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
(* Fibonacci.thy taken from Isabelle distribution
Gertrud Bauer / Larry Paulson *)
theory Fibonacci = Primes:
subsection {* Fibonacci numbers *}
consts fib :: "nat => nat"
recdef fib less_than
"fib 0 = 0"
"fib (Suc 0) = 1"
"fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "0 < fib (Suc n)"
by (induct n rule: fib.induct) (simp+)
text {* Alternative induction rule. *}
theorem fib_induct:
"\<lbrakk>P 0; P 1; \<And>n. \<lbrakk>P (n + 1); P n\<rbrakk> \<Longrightarrow> P (n + 2)\<rbrakk> \<Longrightarrow> P (n::nat)"
by (induct rule: fib.induct, simp+)
subsection {* Fib and gcd commute *}
text {* A few laws taken from \cite{Concrete-Math}. *}
lemma fib_add:
"fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
(is "?P n")
-- {* see \cite[page 280]{Concrete-Math} *}
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
fix n
have "fib (n + 2 + k + 1)
= fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
also assume "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
(is " _ = ?R1")
also assume "fib (n + 1 + k + 1)
= fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
(is " _ = ?R2")
also have "?R1 + ?R2
= fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
by (simp add: add_mult_distrib2)
finally show "?P (n + 2)" .
qed
lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
fix n
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
by simp
also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
by (simp only: gcd_add2')
also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
by (simp add: gcd_commute)
also assume "... = 1"
finally show "?P (n + 2)" .
qed
lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
proof -
assume "0 < n"
hence "gcd (n * k + m, n) = gcd (n, m mod n)"
by (simp add: gcd_non_0 add_commute)
also have "... = gcd (m, n)" by (simp! add: gcd_non_0)
finally show ?thesis .
qed
lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
proof (cases m)
assume "m = 0"
thus ?thesis by simp
next
fix k assume "m = Suc k"
hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
by (simp add: gcd_commute)
also have "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
by (simp add: gcd_mult_add)
also have "... = gcd (fib n, fib (k + 1))"
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
also have "... = gcd (fib m, fib n)"
by (simp! add: gcd_commute)
finally show ?thesis .
qed
lemma gcd_fib_diff:
"m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
proof -
assume "m <= n"
have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
by (simp add: gcd_fib_add)
also have "n - m + m = n" by (simp!)
finally show ?thesis .
qed
lemma gcd_fib_mod:
"0 < m \<Longrightarrow> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
proof -
assume m: "0 < m"
show ?thesis
proof (induct n rule: nat_less_induct)
fix n
assume hyp: "ALL ma. ma < n
--> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
proof -
have "n mod m = (if n < m then n else (n - m) mod m)"
by (rule mod_if)
also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
proof cases
assume "n < m" thus ?thesis by simp
next
assume not_lt: "~ n < m" hence le: "m <= n" by simp
have "n - m < n" by (simp! add: diff_less)
with hyp have "gcd (fib m, fib ((n - m) mod m))
= gcd (fib m, fib (n - m))" by simp
also from le have "... = gcd (fib m, fib n)"
by (rule gcd_fib_diff)
finally have "gcd (fib m, fib ((n - m) mod m)) =
gcd (fib m, fib n)" .
with not_lt show ?thesis by simp
qed
finally show ?thesis .
qed
qed
qed
theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
proof (induct m n rule: gcd_induct)
fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
fix n :: nat assume n: "0 < n"
hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
qed
end
|
