1 (* ========================================================================= *)
2 (* Perfect number theorems. *)
3 (* ========================================================================= *)
5 needs "Library/prime.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* The sum-of-divisors function. *)
11 (* ------------------------------------------------------------------------- *)
13 let sigma = new_definition
14 `sigma(n) = if n = 0 then 0 else nsum {d | d divides n} (\i. i)`;;
16 (* ------------------------------------------------------------------------- *)
17 (* Definition of perfection. *)
18 (* ------------------------------------------------------------------------- *)
20 let perfect = new_definition
21 `perfect n <=> ~(n = 0) /\ sigma(n) = 2 * n`;;
23 (* ------------------------------------------------------------------------- *)
24 (* Various number-theoretic lemmas. *)
25 (* ------------------------------------------------------------------------- *)
27 let ODD_POW2_MINUS1 = prove
28 (`!k. ~(k = 0) ==> ODD(2 EXP k - 1)`,
30 SUBGOAL_THEN `EVEN(2 EXP k) <=> EVEN((2 EXP k - 1) + 1)` MP_TAC THENL
31 [AP_TERM_TAC THEN REWRITE_TAC[ARITH_RULE `k = k - 1 + 1 <=> ~(k = 0)`] THEN
32 REWRITE_TAC[EXP_EQ_0; ARITH];
33 ASM_REWRITE_TAC[GSYM NOT_EVEN; EVEN_ADD; EVEN_EXP; ARITH]]);;
35 let EVEN_ODD_DECOMP = prove
36 (`!n. ~(n = 0) ==> ?r s. ODD s /\ n = 2 EXP r * s`,
37 MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
38 MP_TAC(SPEC `n:num` EVEN_OR_ODD) THEN
39 REWRITE_TAC[EVEN_EXISTS; ODD_EXISTS] THEN
40 DISCH_THEN(DISJ_CASES_THEN (X_CHOOSE_THEN `m:num` SUBST_ALL_TAC)) THENL
41 [DISCH_THEN(MP_TAC o SPEC `m:num`) THEN
42 REWRITE_TAC[MULT_EQ_0; ARITH; ARITH_RULE `m < 2 * m <=> ~(m = 0)`] THEN
43 ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[] THEN
44 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
45 X_GEN_TAC `s:num` THEN DISCH_THEN(X_CHOOSE_TAC `r:num`) THEN
46 EXISTS_TAC `SUC r` THEN ASM_REWRITE_TAC[EXP; GSYM MULT_ASSOC];
47 REPEAT(DISCH_THEN(K ALL_TAC)) THEN EXISTS_TAC `0` THEN
48 REWRITE_TAC[EXP; MULT_CLAUSES] THEN MESON_TAC[]]);;
50 let FINITE_DIVISORS = prove
51 (`!n. ~(n = 0) ==> FINITE {d | d divides n}`,
52 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
53 EXISTS_TAC `{d | d <= n}` THEN REWRITE_TAC[FINITE_NUMSEG_LE] THEN
54 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[DIVIDES_LE]);;
56 let MULT_EQ_COPRIME = prove
57 (`!a b x y. a * b = x * y /\ coprime(a,x)
58 ==> ?d. y = a * d /\ b = x * d`,
60 MP_TAC(SPECL [`a:num`; `x:num`; `y:num`] COPRIME_DIVPROD) THEN
61 MP_TAC(SPECL [`x:num`; `a:num`; `b:num`] COPRIME_DIVPROD) THEN
63 [ASM_MESON_TAC[DIVIDES_REFL; DIVIDES_RMUL; COPRIME_SYM];
64 REWRITE_TAC[divides] THEN STRIP_TAC]) THEN
65 UNDISCH_TAC `a * b = x * y` THEN ASM_REWRITE_TAC[] THEN
66 REWRITE_TAC[ARITH_RULE
67 `(a * x * u = x * a * v) <=> (a * x) * u = (a * x) * v`] THEN
68 REWRITE_TAC[EQ_MULT_LCANCEL; MULT_EQ_0] THEN ASM_MESON_TAC[]);;
70 let COPRIME_ODD_POW2 = prove
71 (`!k n. ODD(n) ==> coprime(2 EXP k,n)`,
72 SIMP_TAC[coprime; PRIME_2; DIVIDES_PRIMEPOW] THEN REWRITE_TAC[divides] THEN
73 REPEAT STRIP_TAC THEN UNDISCH_TAC `ODD n` THEN ASM_REWRITE_TAC[] THEN
74 SIMP_TAC[ODD_MULT; ODD_EXP; ARITH]);;
77 (`!s t. FINITE s /\ FINITE t
78 ==> nsum s f * nsum t g =
79 nsum {(x:A,y:B) | x IN s /\ y IN t} (\(x,y). f(x) * g(y))`,
80 SIMP_TAC[GSYM NSUM_NSUM_PRODUCT; NSUM_LMUL; NSUM_RMUL]);;
82 (* ------------------------------------------------------------------------- *)
83 (* Some elementary properties of the sigma function. *)
84 (* ------------------------------------------------------------------------- *)
92 REWRITE_TAC[sigma; DIVIDES_ONE; SET_RULE `{d | d = 1} = {1}`] THEN
93 REWRITE_TAC[ARITH; NSUM_SING]);;
95 let SIGMA_LBOUND = prove
96 (`!n. 1 < n ==> n + 1 <= sigma(n)`,
98 FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `1 < n ==> ~(n = 0)`)) THEN
99 ASM_REWRITE_TAC[sigma] THEN MATCH_MP_TAC LE_TRANS THEN
100 EXISTS_TAC `nsum {1,n} (\i. i)` THEN CONJ_TAC THENL
101 [SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; IN_SING; NOT_IN_EMPTY] THEN
103 MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN ASM_SIMP_TAC[FINITE_DIVISORS] THEN
104 REWRITE_TAC[SUBSET; IN_ELIM_THM; NOT_IN_EMPTY; IN_INSERT] THEN
105 MESON_TAC[DIVIDES_1; DIVIDES_REFL]]);;
107 let SIGMA_MULT = prove
108 (`!a b. 1 < a /\ 1 < b ==> 1 + b + a * b <= sigma(a * b)`,
109 REPEAT STRIP_TAC THEN
110 EVERY_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `1 < n ==> ~(n = 0)`)) THEN
111 ASM_REWRITE_TAC[sigma] THEN MATCH_MP_TAC LE_TRANS THEN
112 EXISTS_TAC `nsum {1,b,a*b} (\i. i)` THEN CONJ_TAC THENL
113 [SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; IN_INSERT; NOT_IN_EMPTY] THEN
114 ONCE_REWRITE_TAC[ARITH_RULE `x = a * b <=> a * b = 1 * x`] THEN
115 ASM_REWRITE_TAC[EQ_MULT_RCANCEL] THEN
116 REWRITE_TAC[MULT_CLAUSES; MULT_EQ_1] THEN
118 ASM_REWRITE_TAC[MULT_EQ_0] THEN
119 MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN
120 ASM_SIMP_TAC[FINITE_DIVISORS; MULT_EQ_0] THEN
121 REWRITE_TAC[SUBSET; IN_ELIM_THM; NOT_IN_EMPTY; IN_INSERT] THEN
122 MESON_TAC[DIVIDES_1; DIVIDES_REFL; DIVIDES_LMUL]]);;
124 let SIGMA_PRIME = prove
125 (`!p. prime(p) ==> sigma(p) = p + 1`,
127 ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0; SIGMA_0; ARITH] THEN
128 ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[PRIME_1; SIGMA_1; ARITH] THEN
129 DISCH_TAC THEN ASM_REWRITE_TAC[sigma] THEN
130 MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `nsum {1,p} (\i. i)` THEN
132 [AP_THM_TAC THEN AP_TERM_TAC THEN
133 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
134 ASM_MESON_TAC[prime; DIVIDES_1; DIVIDES_REFL];
135 ASM_SIMP_TAC[NSUM_CLAUSES; IN_SING; FINITE_RULES; NOT_IN_EMPTY] THEN
138 let SIGMA_PRIME_EQ = prove
139 (`!p. prime(p) <=> sigma(p) = p + 1`,
140 GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[SIGMA_PRIME] THEN
141 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
142 REWRITE_TAC[prime; DE_MORGAN_THM] THEN
143 ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[SIGMA_1; ARITH] THEN
144 REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; divides; DE_MORGAN_THM] THEN
145 DISCH_THEN(X_CHOOSE_THEN `a:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
146 DISCH_THEN(X_CHOOSE_THEN `b:num` SUBST_ALL_TAC) THEN
147 MP_TAC(SPECL [`a:num`; `b:num`] SIGMA_MULT) THEN
148 ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; SIGMA_0; ARITH] THEN
149 ASM_CASES_TAC `b = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; SIGMA_0; ARITH] THEN
150 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[MULT_EQ_1] THEN
151 ONCE_REWRITE_TAC[ARITH_RULE `a = a * b <=> a * b = a * 1`] THEN
152 REWRITE_TAC[EQ_MULT_LCANCEL] THEN ARITH_TAC);;
154 let SIGMA_POW2 = prove
155 (`!k. sigma(2 EXP k) = 2 EXP (k + 1) - 1`,
156 GEN_TAC THEN REWRITE_TAC[sigma; EXP_EQ_0; ARITH] THEN
157 MATCH_MP_TAC EQ_TRANS THEN
158 EXISTS_TAC `nsum {2 EXP i | i <= k} (\i. i)` THEN CONJ_TAC THENL
159 [AP_THM_TAC THEN AP_TERM_TAC THEN
160 SIMP_TAC[DIVIDES_PRIMEPOW; PRIME_2; EXTENSION; IN_ELIM_THM];
162 MATCH_MP_TAC(ARITH_RULE `x + 1 = y ==> x = y - 1`) THEN
163 SPEC_TAC(`k:num`,`k:num`) THEN INDUCT_TAC THEN REWRITE_TAC[LE] THENL
164 [REWRITE_TAC[SET_RULE `{2 EXP i | i = 0} = {2 EXP 0}`] THEN
165 REWRITE_TAC[ARITH; NSUM_SING];
168 `{2 EXP i | i = SUC k \/ i <= k} =
169 (2 EXP (SUC k)) INSERT {2 EXP i | i <= k}`] THEN
170 POP_ASSUM MP_TAC THEN
172 `{2 EXP i | i <= k} = IMAGE (\i. 2 EXP i) {i | i <= k}`] THEN
173 SIMP_TAC[NSUM_CLAUSES; FINITE_IMAGE; FINITE_NUMSEG_LE] THEN
174 REWRITE_TAC[IN_IMAGE; GSYM LE_ANTISYM; LE_EXP; ARITH] THEN
175 REWRITE_TAC[LE_ANTISYM; IN_ELIM_THM; UNWIND_THM1] THEN
176 REWRITE_TAC[ARITH_RULE `~(SUC k <= k)`] THEN
177 DISCH_TAC THEN ASM_REWRITE_TAC[GSYM ADD_ASSOC] THEN
178 REWRITE_TAC[EXP; EXP_ADD; ARITH] THEN ARITH_TAC);;
180 (* ------------------------------------------------------------------------- *)
181 (* Multiplicativity of sigma, the most interesting property. *)
182 (* ------------------------------------------------------------------------- *)
184 let SIGMA_MULTIPLICATIVE = prove
185 (`!a b. coprime(a,b) ==> sigma(a * b) = sigma(a) * sigma(b)`,
187 ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[SIGMA_0; MULT_CLAUSES] THEN
188 ASM_CASES_TAC `b = 0` THEN ASM_REWRITE_TAC[SIGMA_0; MULT_CLAUSES] THEN
189 DISCH_TAC THEN ASM_REWRITE_TAC[sigma; MULT_EQ_0] THEN
190 ASM_SIMP_TAC[FINITE_DIVISORS; MULT_NSUM] THEN
191 REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC EQ_TRANS THEN
193 `nsum (IMAGE (\(x,y). x * y)
194 {x,y | x divides a /\ y divides b}) (\i. i)` THEN
196 [AP_THM_TAC THEN AP_TERM_TAC THEN
197 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM; EXISTS_PAIR_THM] THEN
198 REWRITE_TAC[PAIR_EQ] THEN
199 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> c /\ a /\ b`] THEN
200 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
201 X_GEN_TAC `n:num` THEN EQ_TAC THEN REWRITE_TAC[DIVISION_DECOMP] THEN
202 REWRITE_TAC[divides] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
205 W(fun (asl,w) -> MP_TAC(PART_MATCH (lhs o rand) NSUM_IMAGE (lhand w))) THEN
206 REWRITE_TAC[o_DEF; ETA_AX] THEN DISCH_THEN MATCH_MP_TAC THEN
207 REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
208 MAP_EVERY X_GEN_TAC [`w:num`; `x:num`; `y:num`; `z:num`] THEN
209 REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC THEN
210 REPEAT(FIRST_X_ASSUM(SUBST_ALL_TAC o SYM o
211 check (is_var o rand o concl))) THEN
212 REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN
213 ASM_MESON_TAC[COPRIME_DIVISORS; COPRIME_SYM; COPRIME_DIVPROD;
214 DIVIDES_RMUL; DIVIDES_REFL; MULT_SYM]);;
216 (* ------------------------------------------------------------------------- *)
217 (* Hence the main theorems. *)
218 (* ------------------------------------------------------------------------- *)
220 let PERFECT_EUCLID = prove
221 (`!k. prime(2 EXP k - 1) ==> perfect(2 EXP (k - 1) * (2 EXP k - 1))`,
222 GEN_TAC THEN ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[ARITH; PRIME_0] THEN
224 SUBGOAL_THEN `coprime(2 EXP (k - 1),2 EXP k - 1)` ASSUME_TAC THENL
225 [MATCH_MP_TAC COPRIME_ODD_POW2 THEN ASM_SIMP_TAC[ODD_POW2_MINUS1];
227 ASM_SIMP_TAC[perfect; SIGMA_MULTIPLICATIVE; SIGMA_PRIME; SIGMA_POW2] THEN
228 ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> k - 1 + 1 = k`; EXP_EQ_0;
229 MULT_EQ_0; ARITH] THEN
230 CONJ_TAC THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
231 REWRITE_TAC[MULT_ASSOC] THEN GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
232 AP_TERM_TAC THEN REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
233 AP_TERM_TAC THEN UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC);;
235 let PERFECT_EULER = prove
236 (`!n. EVEN(n) /\ perfect(n)
237 ==> ?k. prime(2 EXP k - 1) /\ n = 2 EXP (k - 1) * (2 EXP k - 1)`,
238 GEN_TAC THEN MP_TAC(SPEC `n:num` EVEN_ODD_DECOMP) THEN
239 ASM_CASES_TAC `n = 0` THENL
240 [ASM_REWRITE_TAC[perfect]; ASM_REWRITE_TAC[]] THEN
241 REWRITE_TAC[LEFT_IMP_EXISTS_THM; GSYM NOT_EVEN] THEN
242 MAP_EVERY X_GEN_TAC [`r:num`; `s:num`] THEN
243 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
244 ASM_REWRITE_TAC[EVEN_EXP; EVEN_MULT; ARITH] THEN
245 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
246 REWRITE_TAC[perfect] THEN
247 ASM_SIMP_TAC[SIGMA_MULTIPLICATIVE; SIGMA_POW2;
248 COPRIME_ODD_POW2; GSYM NOT_EVEN] THEN
249 DISCH_TAC THEN EXISTS_TAC `r + 1` THEN
250 REWRITE_TAC[ADD_SUB; EQ_MULT_LCANCEL] THEN REWRITE_TAC[EXP_EQ_0; ARITH] THEN
251 FIRST_X_ASSUM(MP_TAC o check(is_eq o concl)) THEN
252 REWRITE_TAC[MULT_ASSOC; GSYM(CONJUNCT2 EXP); ADD1] THEN
253 DISCH_THEN(MP_TAC o MATCH_MP
254 (REWRITE_RULE[IMP_CONJ] MULT_EQ_COPRIME)) THEN
256 [ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_ODD_POW2 THEN
257 SIMP_TAC[ODD_POW2_MINUS1; ADD_EQ_0; ARITH_EQ];
259 DISCH_THEN(X_CHOOSE_THEN `d:num` MP_TAC) THEN
260 ASM_CASES_TAC `d = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THENL
261 [ASM_MESON_TAC[EVEN]; ALL_TAC] THEN
262 ASM_CASES_TAC `d = 1` THENL
263 [ASM_REWRITE_TAC[MULT_CLAUSES; SIGMA_PRIME_EQ] THEN
264 DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC) THEN
265 ASM_REWRITE_TAC[] THEN EXPAND_TAC "s" THEN
266 MATCH_MP_TAC(GSYM SUB_ADD) THEN
267 REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`; EXP_EQ_0; ARITH];
269 DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) ASSUME_TAC) THEN
270 MP_TAC(SPECL [`2 EXP (r + 1) - 1`; `d:num`] SIGMA_MULT) THEN
271 ASM_REWRITE_TAC[] THEN
272 MATCH_MP_TAC(TAUT `a /\ ~b ==> (a ==> b) ==> c`) THEN
273 REPEAT CONJ_TAC THENL
274 [MATCH_MP_TAC(ARITH_RULE `2 EXP 1 < a ==> 1 < a - 1`) THEN
275 REWRITE_TAC[LT_EXP; ARITH] THEN
276 UNDISCH_TAC `~(r = 0)` THEN ARITH_TAC;
277 MAP_EVERY UNDISCH_TAC [`~(d = 0)`; `~(d = 1)`] THEN ARITH_TAC;
278 REWRITE_TAC[NOT_LE] THEN EXPAND_TAC "s" THEN
279 REWRITE_TAC[RIGHT_SUB_DISTRIB; MULT_CLAUSES] THEN
280 MATCH_MP_TAC(ARITH_RULE `1 * d < x * d ==> x * d < 1 + d + x * d - d`) THEN
281 ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
282 MATCH_MP_TAC(ARITH_RULE `2 EXP 0 < a ==> 1 < a`) THEN
283 REWRITE_TAC[LT_EXP] THEN UNDISCH_TAC `~(r = 0)` THEN ARITH_TAC]);;