1 (* ========================================================================= *)
2 (* Basic theory of divisibility, gcd, coprimality and primality (over N). *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* HOL88 compatibility (since all this is a port of old HOL88 stuff). *)
9 (* ------------------------------------------------------------------------- *)
11 let MULT_MONO_EQ = prove
12 (`!m i n. ((SUC n) * m = (SUC n) * i) <=> (m = i)`,
13 REWRITE_TAC[EQ_MULT_LCANCEL; NOT_SUC]);;
15 let LESS_ADD_1 = prove
16 (`!m n. n < m ==> (?p. m = n + (p + 1))`,
17 REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);;
19 let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;;
21 let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
23 let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;;
26 (`!n. n <= 0 <=> (n = 0)`,
29 let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;;
31 let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;;
34 (`!m n. ~((SUC n) EXP m = 0)`,
35 REWRITE_TAC[EXP_EQ_0; NOT_SUC]);;
37 let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;;
39 let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;;
41 let ZERO_LESS_EXP = prove
42 (`!m n. 0 < ((SUC n) EXP m)`,
43 REWRITE_TAC[LT_NZ; NOT_EXP_0]);;
45 (* ------------------------------------------------------------------------- *)
46 (* General arithmetic lemmas. *)
47 (* ------------------------------------------------------------------------- *)
50 `!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`,
52 STRUCT_CASES_TAC(SPEC `x:num` num_CASES) THEN
53 REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN
54 REWRITE_TAC[GSYM(el 4 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN
55 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
56 [GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
57 MATCH_ACCEPT_TAC MULT_MONO_EQ);;
59 let LESS_EQ_MULT = prove(
60 `!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`,
62 DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LE_EXISTS]) THEN
63 ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB;
64 GSYM ADD_ASSOC; LE_ADD]);;
66 let LESS_MULT = prove(
67 `!m n p q. m < n /\ p < q ==> (m * p) < (n * q)`,
68 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN
69 ((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN
70 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
71 REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN
72 ONCE_REWRITE_TAC[GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN
73 MATCH_ACCEPT_TAC LESS_ADD_SUC);;
75 let MULT_LCANCEL = prove(
76 `!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)`,
77 REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC `a:num` num_CASES) THEN
78 REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);;
80 (* ------------------------------------------------------------------------- *)
81 (* Properties of the exponential function. *)
82 (* ------------------------------------------------------------------------- *)
85 (`!n. 0 EXP (SUC n) = 0`,
86 REWRITE_TAC[EXP; MULT_CLAUSES]);;
88 let EXP_MONO_LT_SUC = prove
89 (`!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) <=> (x < y)`,
90 REWRITE_TAC[EXP_MONO_LT; NOT_SUC]);;
92 let EXP_MONO_LE_SUC = prove
93 (`!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) <=> x <= y`,
94 REWRITE_TAC[EXP_MONO_LE; NOT_SUC]);;
96 let EXP_MONO_EQ_SUC = prove
97 (`!x y n. (x EXP (SUC n) = y EXP (SUC n)) <=> (x = y)`,
98 REWRITE_TAC[EXP_MONO_EQ; NOT_SUC]);;
101 (`!x m n. (x EXP m) EXP n = x EXP (m * n)`,
102 REWRITE_TAC[EXP_MULT]);;
104 (* ------------------------------------------------------------------------- *)
105 (* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere. *)
106 (* ------------------------------------------------------------------------- *)
108 let DIFF_LEMMA = prove(
109 `!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`,
111 DISJ_CASES_TAC(SPEC `a:num` LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN
112 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN
113 DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
114 GEN_REWRITE_TAC LAND_CONV [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN
115 REWRITE_TAC[ADD_ASSOC] THEN
116 REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);;
118 let NOT_EVEN_EQ_ODD = prove(
119 `!m n. ~(2 * m = SUC(2 * n))`,
120 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
121 REWRITE_TAC[EVEN; EVEN_MULT; ARITH]);;
123 let CANCEL_TIMES2 = prove(
124 `!x y. (2 * x = 2 * y) <=> (x = y)`,
125 REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);;
127 let EVEN_SQUARE = prove(
128 `!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x`,
129 GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN
130 DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
131 EXISTS_TAC `m * m` THEN REWRITE_TAC[EXP_2] THEN
132 REWRITE_TAC[SYM(REWRITE_CONV[ARITH] `2 * 2`)] THEN
133 REWRITE_TAC[MULT_AC]);;
135 let ODD_SQUARE = prove(
136 `!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1`,
137 GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
138 DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
139 ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
140 REWRITE_TAC[GSYM ADD1; SUC_INJ] THEN
141 EXISTS_TAC `(m * m) + m` THEN
142 REWRITE_TAC(map num_CONV [`4`; `3`; `2`; `1`]) THEN
143 REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
144 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
145 REWRITE_TAC[ADD_AC]);;
147 let DIFF_SQUARE = prove(
148 `!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`,
150 DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THENL
151 [SUBGOAL_THEN `(x * x) <= (y * y)` MP_TAC THENL
152 [MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[];
153 POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN
154 REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]];
155 POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
156 REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
157 REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
158 REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
159 AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN
160 AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);;
162 let ADD_IMP_SUB = prove(
163 `!x y z. (x + y = z) ==> (x = z - y)`,
164 REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
165 REWRITE_TAC[ADD_SUB]);;
167 let ADD_SUM_DIFF = prove(
168 `!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\
169 ((w + v) + (w - v) = 2 * w)`,
170 REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
171 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
172 REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
173 REWRITE_TAC[MULT_2; GSYM ADD_ASSOC] THEN
174 ONCE_REWRITE_TAC[ADD_SYM] THEN
175 REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);;
178 `!n. n EXP 4 = (n EXP 2) EXP 2`,
179 GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN
180 REWRITE_TAC[ARITH]);;
182 (* ------------------------------------------------------------------------- *)
183 (* Elementary theory of divisibility *)
184 (* ------------------------------------------------------------------------- *)
186 let DIVIDES_0 = prove
190 let DIVIDES_ZERO = prove
191 (`!x. 0 divides x <=> (x = 0)`,
194 let DIVIDES_1 = prove
198 let DIVIDES_ONE = prove(
199 `!x. (x divides 1) <=> (x = 1)`,
200 GEN_TAC THEN REWRITE_TAC[divides] THEN
201 CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
202 REWRITE_TAC[MULT_EQ_1] THEN EQ_TAC THEN STRIP_TAC THEN
203 ASM_REWRITE_TAC[] THEN EXISTS_TAC `1` THEN REFL_TAC);;
205 let DIVIDES_REFL = prove
209 let DIVIDES_TRANS = prove
210 (`!a b c. a divides b /\ b divides c ==> a divides c`,
213 let DIVIDES_ANTISYM = prove
214 (`!x y. x divides y /\ y divides x <=> (x = y)`,
215 REPEAT GEN_TAC THEN EQ_TAC THENL
216 [REWRITE_TAC[divides] THEN
217 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (CHOOSE_THEN SUBST1_TAC)) THEN
218 DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
219 CONV_TAC(LAND_CONV SYM_CONV) THEN
220 REWRITE_TAC[GSYM MULT_ASSOC; MULT_FIX; MULT_EQ_1] THEN
221 STRIP_TAC THEN ASM_REWRITE_TAC[];
222 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[DIVIDES_REFL]]);;
224 let DIVIDES_ADD = prove
225 (`!d a b. d divides a /\ d divides b ==> d divides (a + b)`,
228 let DIVIDES_SUB = prove
229 (`!d a b. d divides a /\ d divides b ==> d divides (a - b)`,
230 REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
231 DISCH_THEN(CONJUNCTS_THEN (CHOOSE_THEN SUBST1_TAC)) THEN
232 REWRITE_TAC[GSYM LEFT_SUB_DISTRIB] THEN
233 W(EXISTS_TAC o rand o lhs o snd o dest_exists o snd) THEN
236 let DIVIDES_LMUL = prove
237 (`!d a x. d divides a ==> d divides (x * a)`,
240 let DIVIDES_RMUL = prove
241 (`!d a x. d divides a ==> d divides (a * x)`,
244 let DIVIDES_ADD_REVR = prove
245 (`!d a b. d divides a /\ d divides (a + b) ==> d divides b`,
248 let DIVIDES_ADD_REVL = prove
249 (`!d a b. d divides b /\ d divides (a + b) ==> d divides a`,
252 let DIVIDES_DIV = prove
253 (`!n x. 0 < n /\ (x MOD n = 0) ==> n divides x`,
254 REPEAT STRIP_TAC THEN
255 FIRST_ASSUM(MP_TAC o SPEC `x:num` o MATCH_MP DIVISION o
256 MATCH_MP (ARITH_RULE `0 < n ==> ~(n = 0)`)) THEN
257 ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN
258 REWRITE_TAC[divides] THEN EXISTS_TAC `x DIV n` THEN
259 ONCE_REWRITE_TAC[MULT_SYM] THEN FIRST_ASSUM MATCH_ACCEPT_TAC);;
261 let DIVIDES_MUL_L = prove
262 (`!a b c. a divides b ==> (c * a) divides (c * b)`,
265 let DIVIDES_MUL_R = prove
266 (`!a b c. a divides b ==> (a * c) divides (b * c)`,
269 let DIVIDES_LMUL2 = prove
270 (`!d a x. (x * d) divides a ==> d divides a`,
273 let DIVIDES_RMUL2 = prove
274 (`!d a x. (d * x) divides a ==> d divides a`,
277 let DIVIDES_CMUL2 = prove
278 (`!a b c. (c * a) divides (c * b) /\ ~(c = 0) ==> a divides b`,
281 let DIVIDES_LMUL2_EQ = prove
282 (`!a b c. ~(c = 0) ==> ((c * a) divides (c * b) <=> a divides b)`,
285 let DIVIDES_RMUL2_EQ = prove
286 (`!a b c. ~(c = 0) ==> ((a * c) divides (b * c) <=> a divides b)`,
289 let DIVIDES_CASES = prove
290 (`!m n. n divides m ==> m = 0 \/ m = n \/ 2 * n <= m`,
291 SIMP_TAC[ARITH_RULE `m = n \/ 2 * n <= m <=> m = n * 1 \/ n * 2 <= m`] THEN
292 SIMP_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
293 REWRITE_TAC[MULT_EQ_0; EQ_MULT_LCANCEL; LE_MULT_LCANCEL] THEN ARITH_TAC);;
295 let DIVIDES_LE_STRONG = prove
296 (`!m n. m divides n ==> 1 <= m /\ m <= n \/ n = 0`,
297 REPEAT GEN_TAC THEN ASM_CASES_TAC `m = 0` THEN
298 ASM_REWRITE_TAC[DIVIDES_ZERO; ARITH] THEN
299 DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
300 POP_ASSUM MP_TAC THEN ARITH_TAC);;
302 let DIVIDES_DIV_NOT = prove(
303 `!n x q r. (x = (q * n) + r) /\ 0 < r /\ r < n ==> ~(n divides x)`,
304 REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
305 MP_TAC(SPEC `n:num` DIVIDES_REFL) THEN
306 DISCH_THEN(MP_TAC o SPEC `q:num` o MATCH_MP DIVIDES_LMUL) THEN
307 PURE_REWRITE_TAC[TAUT `a ==> ~b <=> a /\ b ==> F`] THEN
308 DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_ADD_REVR) THEN
309 DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
310 ASM_REWRITE_TAC[DE_MORGAN_THM; NOT_LE; GSYM LESS_EQ_0]);;
312 let DIVIDES_MUL2 = prove
313 (`!a b c d. a divides b /\ c divides d ==> (a * c) divides (b * d)`,
316 let DIVIDES_EXP = prove(
317 `!x y n. x divides y ==> (x EXP n) divides (y EXP n)`,
318 REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
319 DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
320 EXISTS_TAC `d EXP n` THEN MATCH_ACCEPT_TAC MULT_EXP);;
322 let DIVIDES_EXP2 = prove(
323 `!n x y. ~(n = 0) /\ (x EXP n) divides y ==> x divides y`,
324 INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; EXP] THEN NUMBER_TAC);;
326 let DIVIDES_EXP_LE = prove
327 (`!p m n. 2 <= p ==> ((p EXP m) divides (p EXP n) <=> m <= n)`,
328 REPEAT STRIP_TAC THEN EQ_TAC THENL
329 [DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
330 ASM_REWRITE_TAC[LE_EXP; EXP_EQ_0] THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
331 SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; EXP_ADD] THEN NUMBER_TAC]);;
333 let DIVIDES_TRIVIAL_UPPERBOUND = prove
334 (`!p n. ~(n = 0) /\ 2 <= p ==> ~((p EXP n) divides n)`,
335 REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
336 ASM_REWRITE_TAC[NOT_LE] THEN MATCH_MP_TAC LTE_TRANS THEN
337 EXISTS_TAC `2 EXP n` THEN REWRITE_TAC[LT_POW2_REFL] THEN
338 UNDISCH_TAC `~(n = 0)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
339 INDUCT_TAC THEN ASM_REWRITE_TAC[EXP_MONO_LE_SUC]);;
341 let FACTORIZATION_INDEX = prove
342 (`!n p. ~(n = 0) /\ 2 <= p
343 ==> ?k. (p EXP k) divides n /\
344 !l. k < l ==> ~((p EXP l) divides n)`,
345 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM NOT_LE; CONTRAPOS_THM] THEN
346 REWRITE_TAC[GSYM num_MAX] THEN CONJ_TAC THENL
347 [EXISTS_TAC `0` THEN REWRITE_TAC[EXP; DIVIDES_1];
348 EXISTS_TAC `n:num` THEN
349 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
350 ASM_REWRITE_TAC[] THEN
351 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LE_TRANS) THEN
352 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP l` THEN
353 SIMP_TAC[LT_POW2_REFL; LT_IMP_LE] THEN
354 SPEC_TAC(`l:num`,`l:num`) THEN INDUCT_TAC THEN
355 ASM_REWRITE_TAC[ARITH; CONJUNCT1 EXP; EXP_MONO_LE_SUC]]);;
357 let DIVIDES_FACT = prove
358 (`!n p. 1 <= p /\ p <= n ==> p divides (FACT n)`,
359 INDUCT_TAC THEN REWRITE_TAC[FACT; LE] THENL
360 [ARITH_TAC; ASM_MESON_TAC[DIVIDES_LMUL; DIVIDES_RMUL; DIVIDES_REFL]]);;
362 let DIVIDES_2 = prove(
363 `!n. 2 divides n <=> EVEN(n)`,
364 REWRITE_TAC[divides; EVEN_EXISTS]);;
366 let DIVIDES_REXP_SUC = prove
367 (`!x y n. x divides y ==> x divides (y EXP (SUC n))`,
368 REWRITE_TAC[EXP; DIVIDES_RMUL]);;
370 let DIVIDES_REXP = prove
371 (`!x y n. x divides y /\ ~(n = 0) ==> x divides (y EXP n)`,
372 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN SIMP_TAC[DIVIDES_REXP_SUC]);;
374 let DIVIDES_MOD = prove
375 (`!m n. ~(m = 0) ==> (m divides n <=> (n MOD m = 0))`,
376 REWRITE_TAC[divides] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL
377 [ASM_MESON_TAC[MOD_MULT]; DISCH_TAC] THEN
378 FIRST_X_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP DIVISION) THEN
379 ASM_REWRITE_TAC[ADD_CLAUSES] THEN MESON_TAC[MULT_AC]);;
381 let DIVIDES_DIV_MULT = prove
382 (`!m n. m divides n <=> ((n DIV m) * m = n)`,
383 REPEAT GEN_TAC THEN ASM_CASES_TAC `m = 0` THENL
384 [ASM_REWRITE_TAC[DIVIDES_ZERO; MULT_CLAUSES; EQ_SYM_EQ]; ALL_TAC] THEN
385 EQ_TAC THENL [ALL_TAC; MESON_TAC[DIVIDES_LMUL; DIVIDES_REFL]] THEN
386 DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
387 EXISTS_TAC `n DIV m * m + n MOD m` THEN CONJ_TAC THENL
388 [ASM_MESON_TAC[DIVIDES_MOD; ADD_CLAUSES];
389 ASM_MESON_TAC[DIVISION]]);;
391 let FINITE_DIVISORS = prove
392 (`!n. ~(n = 0) ==> FINITE {d | d divides n}`,
393 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
394 EXISTS_TAC `{d:num | d <= n}` THEN REWRITE_TAC[FINITE_NUMSEG_LE] THEN
395 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[DIVIDES_LE]);;
397 let FINITE_SPECIAL_DIVISORS = prove
398 (`!n. ~(n = 0) ==> FINITE {d | P d /\ d divides n}`,
399 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
400 EXISTS_TAC `{d | d divides n}` THEN ASM_SIMP_TAC[FINITE_DIVISORS] THEN
403 let DIVIDES_DIVIDES_DIV = prove
404 (`!n d. 1 <= n /\ d divides n
405 ==> (e divides (n DIV d) <=> (d * e) divides n)`,
407 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [DIVIDES_DIV_MULT] THEN
408 ABBREV_TAC `q = n DIV d` THEN
409 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
410 ASM_CASES_TAC `d = 0` THENL
411 [ASM_SIMP_TAC[MULT_CLAUSES; LE_1];
412 ASM_MESON_TAC[DIVIDES_LMUL2_EQ; MULT_SYM]]);;
414 let DIVISORS_EQ = prove
415 (`!m n. m = n <=> !d. d divides m <=> d divides n`,
416 REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN
417 MESON_TAC[DIVIDES_REFL; DIVIDES_TRANS]);;
419 let MULTIPLES_EQ = prove
420 (`!m n. m = n <=> !d. m divides d <=> n divides d`,
421 REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN
422 MESON_TAC[DIVIDES_REFL; DIVIDES_TRANS]);;
424 let DIVIDES_NSUM = prove
425 (`!n f s. FINITE s /\ (!i. i IN s ==> n divides (f i))
426 ==> n divides nsum s f`,
427 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
428 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
429 ASM_SIMP_TAC[DIVIDES_0; NSUM_CLAUSES; FORALL_IN_INSERT; DIVIDES_ADD]);;
431 (* ------------------------------------------------------------------------- *)
432 (* The Bezout theorem is a bit ugly for N; it'd be easier for Z *)
433 (* ------------------------------------------------------------------------- *)
435 let IND_EUCLID = prove(
436 `!P. (!a b. P a b <=> P b a) /\
438 (!a b. P a b ==> P a (a + b)) ==>
440 REPEAT STRIP_TAC THEN
441 W(fun (asl,w) -> SUBGOAL_THEN `!n a b. (a + b = n) ==> P a b`
443 [ALL_TAC; EXISTS_TAC `a + b` THEN REFL_TAC] THEN
444 MATCH_MP_TAC num_WF THEN
445 REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN MP_TAC
446 (SPECL [`a:num`; `b:num`] LESS_LESS_CASES) THENL
447 [DISCH_THEN SUBST1_TAC THEN
448 GEN_REWRITE_TAC RAND_CONV [GSYM ADD_0] THEN
449 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
450 ALL_TAC; ALL_TAC] THEN
451 DISCH_THEN(fun th -> SUBST1_TAC(SYM(MATCH_MP SUB_ADD
452 (MATCH_MP LT_IMP_LE th))) THEN
453 DISJ_CASES_THEN MP_TAC (MATCH_MP DIFF_LEMMA th)) THENL
454 [DISCH_THEN SUBST1_TAC THEN
455 FIRST_ASSUM (CONV_TAC o REWR_CONV) THEN
456 FIRST_ASSUM MATCH_ACCEPT_TAC;
457 REWRITE_TAC[ASSUME `a + b = n`] THEN
458 DISCH_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
459 FIRST_ASSUM MATCH_MP_TAC THEN
460 UNDISCH_TAC `a + b - a < n` THEN
461 DISCH_THEN(ANTE_RES_THEN MATCH_MP_TAC);
462 DISCH_THEN SUBST1_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
463 REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] (ASSUME `a + b = n`)] THEN
464 DISCH_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
465 FIRST_ASSUM (CONV_TAC o REWR_CONV) THEN
466 FIRST_ASSUM MATCH_MP_TAC THEN
467 UNDISCH_TAC `b + a - b < n` THEN
468 DISCH_THEN(ANTE_RES_THEN MATCH_MP_TAC)] THEN
471 let BEZOUT_LEMMA = prove(
472 `!a b. (?d x y. (d divides a /\ d divides b) /\
473 ((a * x = (b * y) + d) \/
474 (b * x = (a * y) + d)))
475 ==> (?d x y. (d divides a /\ d divides (a + b)) /\
476 ((a * x = ((a + b) * y) + d) \/
477 ((a + b) * x = (a * y) + d)))`,
478 REPEAT STRIP_TAC THEN EXISTS_TAC `d:num` THENL
479 [MAP_EVERY EXISTS_TAC [`x + y`; `y:num`];
480 MAP_EVERY EXISTS_TAC [`x:num`; `x + y`]] THEN
481 ASM_REWRITE_TAC[] THEN
482 (CONJ_TAC THENL [MATCH_MP_TAC DIVIDES_ADD; ALL_TAC]) THEN
483 ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
484 REWRITE_TAC[ADD_ASSOC] THEN DISJ1_TAC THEN
485 REWRITE_TAC[ADD_AC]);;
487 let BEZOUT_ADD = prove(
488 `!a b. ?d x y. (d divides a /\ d divides b) /\
489 ((a * x = (b * y) + d) \/
490 (b * x = (a * y) + d))`,
491 W(fun (asl,w) -> MP_TAC(SPEC (list_mk_abs([`a:num`; `b:num`],
492 snd(strip_forall w)))
493 IND_EUCLID)) THEN BETA_TAC THEN DISCH_THEN MATCH_MP_TAC THEN
494 REPEAT CONJ_TAC THENL
495 [REPEAT GEN_TAC THEN REPEAT
496 (AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
497 GEN_TAC THEN BETA_TAC) THEN
498 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [DISJ_SYM] THEN
499 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [CONJ_SYM] THEN REFL_TAC;
500 GEN_TAC THEN MAP_EVERY EXISTS_TAC [`a:num`; `1`; `0`] THEN
501 REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; DIVIDES_0; DIVIDES_REFL];
502 MATCH_ACCEPT_TAC BEZOUT_LEMMA]);;
505 `!a b. ?d x y. (d divides a /\ d divides b) /\
506 (((a * x) - (b * y) = d) \/
507 ((b * x) - (a * y) = d))`,
508 REPEAT GEN_TAC THEN REPEAT_TCL STRIP_THM_THEN ASSUME_TAC
509 (SPECL [`a:num`; `b:num`] BEZOUT_ADD) THEN
510 REPEAT(W(EXISTS_TAC o fst o dest_exists o snd)) THEN
511 ASM_REWRITE_TAC[] THEN
512 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB]);;
514 (* ------------------------------------------------------------------------- *)
515 (* We can get a stronger version with a nonzeroness assumption. *)
516 (* ------------------------------------------------------------------------- *)
518 let BEZOUT_ADD_STRONG = prove
520 ==> ?d x y. d divides a /\ d divides b /\ (a * x = b * y + d)`,
521 REPEAT STRIP_TAC THEN
522 MP_TAC(SPECL [`a:num`; `b:num`] BEZOUT_ADD) THEN
523 REWRITE_TAC[TAUT `a /\ (b \/ c) <=> a /\ b \/ a /\ c`] THEN
524 REWRITE_TAC[EXISTS_OR_THM; GSYM CONJ_ASSOC] THEN
525 MATCH_MP_TAC(TAUT `(b ==> a) ==> a \/ b ==> a`) THEN
526 DISCH_THEN(X_CHOOSE_THEN `d:num` (X_CHOOSE_THEN `x:num`
527 (X_CHOOSE_THEN `y:num` STRIP_ASSUME_TAC))) THEN
528 FIRST_X_ASSUM(MP_TAC o SYM) THEN
529 ASM_CASES_TAC `b = 0` THENL
530 [ASM_SIMP_TAC[MULT_CLAUSES; ADD_EQ_0; MULT_EQ_0; ADD_CLAUSES] THEN
531 STRIP_TAC THEN UNDISCH_TAC `d divides a` THEN
532 ASM_REWRITE_TAC[DIVIDES_ZERO]; ALL_TAC] THEN
533 MP_TAC(SPECL [`d:num`; `b:num`] DIVIDES_LE) THEN ASM_REWRITE_TAC[] THEN
534 REWRITE_TAC[LE_LT] THEN STRIP_TAC THENL
536 DISCH_TAC THEN EXISTS_TAC `b:num` THEN EXISTS_TAC `b:num` THEN
537 EXISTS_TAC `a - 1` THEN
538 UNDISCH_TAC `d divides a` THEN ASM_SIMP_TAC[DIVIDES_REFL] THEN
539 REWRITE_TAC[ARITH_RULE `b * x + b = (x + 1) * b`] THEN
540 ASM_SIMP_TAC[ARITH_RULE `~(a = 0) ==> ((a - 1) + 1 = a)`]] THEN
541 ASM_CASES_TAC `x = 0` THENL
542 [ASM_SIMP_TAC[MULT_CLAUSES; ADD_EQ_0; MULT_EQ_0] THEN STRIP_TAC THEN
543 UNDISCH_TAC `d divides a` THEN ASM_REWRITE_TAC[DIVIDES_ZERO]; ALL_TAC] THEN
544 DISCH_THEN(MP_TAC o AP_TERM `( * ) (b - 1)`) THEN
545 DISCH_THEN(MP_TAC o AP_TERM `(+) (d:num)`) THEN
546 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV)
547 [LEFT_ADD_DISTRIB] THEN
548 REWRITE_TAC[ARITH_RULE `d + bay + b1 * d = (1 + b1) * d + bay`] THEN
549 ASM_SIMP_TAC[ARITH_RULE `~(b = 0) ==> (1 + (b - 1) = b)`] THEN
550 DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
551 `(a + b = c + d) ==> a <= d ==> (b = (d - a) + c:num)`)) THEN
553 [ONCE_REWRITE_TAC[AC MULT_AC `(b - 1) * b * x = b * (b - 1) * x`] THEN
554 REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
555 GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `d = d * 1`] THEN
556 MATCH_MP_TAC LE_MULT2 THEN
557 MAP_EVERY UNDISCH_TAC [`d < b:num`; `~(x = 0)`] THEN ARITH_TAC;
560 MAP_EVERY EXISTS_TAC [`d:num`; `y * (b - 1)`; `(b - 1) * x - d`] THEN
562 ASM_REWRITE_TAC[] THEN
563 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV) [LEFT_SUB_DISTRIB] THEN
564 REWRITE_TAC[MULT_AC]);;
566 (* ------------------------------------------------------------------------- *)
567 (* Greatest common divisor. *)
568 (* ------------------------------------------------------------------------- *)
571 (`!a b. (gcd(a,b) divides a /\ gcd(a,b) divides b) /\
572 (!e. e divides a /\ e divides b ==> e divides gcd(a,b))`,
575 let DIVIDES_GCD = prove
576 (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`,
579 let GCD_UNIQUE = prove(
580 `!d a b. (d divides a /\ d divides b) /\
581 (!e. e divides a /\ e divides b ==> e divides d) <=>
583 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[GCD] THEN
584 ONCE_REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN
585 ASM_REWRITE_TAC[DIVIDES_GCD] THEN
586 FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[GCD]);;
589 (`(!d. d divides x /\ d divides y <=> d divides u /\ d divides v)
590 ==> gcd(x,y) = gcd(u,v)`,
591 REWRITE_TAC[DIVIDES_GCD; GSYM DIVIDES_ANTISYM] THEN MESON_TAC[GCD]);;
594 (`!a b. gcd(a,b) = gcd(b,a)`,
595 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM GCD_UNIQUE] THEN NUMBER_TAC);;
597 let GCD_ASSOC = prove(
598 `!a b c. gcd(a,gcd(b,c)) = gcd(gcd(a,b),c)`,
599 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
600 REWRITE_TAC[DIVIDES_GCD; CONJ_ASSOC; GCD] THEN
601 CONJ_TAC THEN MATCH_MP_TAC DIVIDES_TRANS THEN
602 EXISTS_TAC `gcd(b,c)` THEN ASM_REWRITE_TAC[GCD]);;
604 let BEZOUT_GCD = prove(
605 `!a b. ?x y. ((a * x) - (b * y) = gcd(a,b)) \/
606 ((b * x) - (a * y) = gcd(a,b))`,
608 MP_TAC(SPECL [`a:num`; `b:num`] BEZOUT) THEN
609 DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN [`d:num`; `x:num`; `y:num`])
610 (CONJUNCTS_THEN ASSUME_TAC)) THEN
611 SUBGOAL_THEN `d divides gcd(a,b)` MP_TAC THENL
612 [MATCH_MP_TAC(last(CONJUNCTS(SPEC_ALL GCD))) THEN ASM_REWRITE_TAC[];
613 DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST1_TAC o REWRITE_RULE[divides]) THEN
614 MAP_EVERY EXISTS_TAC [`x * k`; `y * k`] THEN
615 ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB; MULT_ASSOC] THEN
616 FIRST_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN REWRITE_TAC[]]);;
618 let BEZOUT_GCD_STRONG = prove
619 (`!a b. ~(a = 0) ==> ?x y. a * x = b * y + gcd(a,b)`,
620 REPEAT STRIP_TAC THEN
621 FIRST_ASSUM(MP_TAC o SPEC `b:num` o MATCH_MP BEZOUT_ADD_STRONG) THEN
622 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
623 MAP_EVERY X_GEN_TAC [`d:num`; `x:num`; `y:num`] THEN
624 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
625 SUBGOAL_THEN `d divides gcd(a,b)` MP_TAC THENL
626 [ASM_MESON_TAC[GCD]; ALL_TAC] THEN
627 DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST1_TAC o REWRITE_RULE[divides]) THEN
628 MAP_EVERY EXISTS_TAC [`x * k`; `y * k`] THEN
629 ASM_REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB; MULT_ASSOC]);;
631 let GCD_LMUL = prove(
632 `!a b c. gcd(c * a, c * b) = c * gcd(a,b)`,
633 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
634 ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
635 REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC DIVIDES_MUL_L) THEN
636 REWRITE_TAC[GCD] THEN REPEAT STRIP_TAC THEN
637 REPEAT_TCL STRIP_THM_THEN (SUBST1_TAC o SYM)
638 (SPECL [`a:num`; `b:num`] BEZOUT_GCD) THEN
639 REWRITE_TAC[LEFT_SUB_DISTRIB; MULT_ASSOC] THEN
640 MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
641 MATCH_MP_TAC DIVIDES_RMUL THEN ASM_REWRITE_TAC[]);;
643 let GCD_RMUL = prove(
644 `!a b c. gcd(a * c, b * c) = c * gcd(a,b)`,
646 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
647 MATCH_ACCEPT_TAC GCD_LMUL);;
649 let GCD_BEZOUT = prove(
650 `!a b d. (?x y. ((a * x) - (b * y) = d) \/ ((b * x) - (a * y) = d)) <=>
652 REPEAT GEN_TAC THEN EQ_TAC THENL
653 [STRIP_TAC THEN POP_ASSUM(SUBST1_TAC o SYM) THEN
654 MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
655 MATCH_MP_TAC DIVIDES_RMUL THEN REWRITE_TAC[GCD];
656 DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST1_TAC o REWRITE_RULE[divides]) THEN
657 STRIP_ASSUME_TAC(SPECL [`a:num`; `b:num`] BEZOUT_GCD) THEN
658 MAP_EVERY EXISTS_TAC [`x * k`; `y * k`] THEN
659 ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB; MULT_ASSOC] THEN
660 FIRST_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN REWRITE_TAC[]]);;
662 let GCD_BEZOUT_SUM = prove(
663 `!a b d x y. ((a * x) + (b * y) = d) ==> gcd(a,b) divides d`,
664 REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
665 MATCH_MP_TAC DIVIDES_ADD THEN CONJ_TAC THEN
666 MATCH_MP_TAC DIVIDES_RMUL THEN REWRITE_TAC[GCD]);;
669 (`(!a. gcd(0,a) = a) /\ (!a. gcd(a,0) = a)`,
670 MESON_TAC[GCD_UNIQUE; DIVIDES_0; DIVIDES_REFL]);;
672 let GCD_ZERO = prove(
673 `!a b. (gcd(a,b) = 0) <=> (a = 0) /\ (b = 0)`,
674 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
675 ASM_REWRITE_TAC[GCD_0] THEN
676 MP_TAC(SPECL [`a:num`; `b:num`] GCD) THEN
677 ASM_REWRITE_TAC[DIVIDES_ZERO] THEN
678 STRIP_TAC THEN ASM_REWRITE_TAC[]);;
680 let GCD_REFL = prove(
682 GEN_TAC THEN CONV_TAC SYM_CONV THEN
683 ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
684 REWRITE_TAC[DIVIDES_REFL]);;
687 (`(!a. gcd(1,a) = 1) /\ (!a. gcd(a,1) = 1)`,
688 MESON_TAC[GCD_UNIQUE; DIVIDES_1]);;
690 let GCD_MULTIPLE = prove(
691 `!a b. gcd(b,a * b) = b`,
693 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV)
694 [GSYM(el 2 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
695 REWRITE_TAC[GCD_RMUL; GCD_1] THEN
696 REWRITE_TAC[MULT_CLAUSES]);;
699 (`(!a b. gcd(a + b,b) = gcd(a,b)) /\
700 (!a b. gcd(b + a,b) = gcd(a,b)) /\
701 (!a b. gcd(a,a + b) = gcd(a,b)) /\
702 (!a b. gcd(a,b + a) = gcd(a,b))`,
703 REWRITE_TAC[GSYM GCD_UNIQUE] THEN NUMBER_TAC);;
706 (`(!a b. b <= a ==> gcd(a - b,b) = gcd(a,b)) /\
707 (!a b. a <= b ==> gcd(a,b - a) = gcd(a,b))`,
708 MESON_TAC[SUB_ADD; GCD_ADD]);;
710 let DIVIDES_GCD_LEFT = prove
711 (`!m n:num. m divides n <=> gcd(m,n) = m`,
712 REWRITE_TAC[DIVISORS_EQ; DIVIDES_GCD] THEN
713 MESON_TAC[DIVIDES_REFL; DIVIDES_TRANS]);;
715 let DIVIDES_GCD_RIGHT = prove
716 (`!m n:num. n divides m <=> gcd(m,n) = n`,
717 REWRITE_TAC[DIVISORS_EQ; DIVIDES_GCD] THEN
718 MESON_TAC[DIVIDES_REFL; DIVIDES_TRANS]);;
720 (* ------------------------------------------------------------------------- *)
722 (* ------------------------------------------------------------------------- *)
725 (`coprime(a,b) <=> !d. d divides a /\ d divides b ==> (d = 1)`,
727 [REWRITE_TAC[GSYM DIVIDES_ONE];
728 DISCH_THEN(MP_TAC o SPEC `gcd(a,b)`) THEN REWRITE_TAC[GCD]] THEN
732 `!a b. coprime(a,b) <=> !d. d divides a /\ d divides b <=> (d = 1)`,
733 REPEAT GEN_TAC THEN REWRITE_TAC[coprime] THEN
734 REPEAT(EQ_TAC ORELSE STRIP_TAC) THEN ASM_REWRITE_TAC[DIVIDES_1] THENL
735 [FIRST_ASSUM MATCH_MP_TAC;
736 FIRST_ASSUM(CONV_TAC o REWR_CONV o GSYM) THEN CONJ_TAC] THEN
739 let COPRIME_GCD = prove
740 (`!a b. coprime(a,b) <=> (gcd(a,b) = 1)`,
741 REWRITE_TAC[GSYM DIVIDES_ONE] THEN NUMBER_TAC);;
743 let COPRIME_SYM = prove
744 (`!a b. coprime(a,b) <=> coprime(b,a)`,
747 let COPRIME_BEZOUT = prove(
748 `!a b. coprime(a,b) <=> ?x y. ((a * x) - (b * y) = 1) \/
749 ((b * x) - (a * y) = 1)`,
750 REWRITE_TAC[GCD_BEZOUT; DIVIDES_ONE; COPRIME_GCD]);;
752 let COPRIME_DIVPROD = prove
753 (`!d a b. d divides (a * b) /\ coprime(d,a) ==> d divides b`,
756 let COPRIME_1 = prove
760 let GCD_COPRIME = prove
761 (`!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
765 let GCD_COPRIME_EXISTS = prove(
766 `!a b. ~(gcd(a,b) = 0) ==>
767 ?a' b'. (a = a' * gcd(a,b)) /\
768 (b = b' * gcd(a,b)) /\
770 REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPECL [`a:num`; `b:num`] GCD) THEN
771 DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[divides] THEN
772 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a':num` o GSYM)
773 (X_CHOOSE_TAC `b':num` o GSYM)) THEN
774 MAP_EVERY EXISTS_TAC [`a':num`; `b':num`] THEN
775 ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[] THEN
776 MATCH_MP_TAC GCD_COPRIME THEN
777 MAP_EVERY EXISTS_TAC [`a:num`; `b:num`] THEN
778 ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[]);;
780 let COPRIME_0 = prove
781 (`(!d. coprime(d,0) <=> d = 1) /\
782 (!d. coprime(0,d) <=> d = 1)`,
783 REWRITE_TAC[GSYM DIVIDES_ONE] THEN NUMBER_TAC);;
785 let COPRIME_MUL = prove
786 (`!d a b. coprime(d,a) /\ coprime(d,b) ==> coprime(d,a * b)`,
789 let COPRIME_LMUL2 = prove
790 (`!d a b. coprime(d,a * b) ==> coprime(d,b)`,
793 let COPRIME_RMUL2 = prove
794 (`!d a b. coprime(d,a * b) ==> coprime(d,a)`,
797 let COPRIME_LMUL = prove
798 (`!d a b. coprime(a * b,d) <=> coprime(a,d) /\ coprime(b,d)`,
801 let COPRIME_RMUL = prove
802 (`!d a b. coprime(d,a * b) <=> coprime(d,a) /\ coprime(d,b)`,
805 let COPRIME_EXP = prove
806 (`!n a d. coprime(d,a) ==> coprime(d,a EXP n)`,
807 INDUCT_TAC THEN REWRITE_TAC[EXP; COPRIME_1] THEN
808 REPEAT GEN_TAC THEN DISCH_TAC THEN
809 MATCH_MP_TAC COPRIME_MUL THEN ASM_REWRITE_TAC[] THEN
810 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
812 let COPRIME_EXP_IMP = prove
813 (`!n a b. coprime(a,b) ==> coprime(a EXP n,b EXP n)`,
814 REPEAT GEN_TAC THEN DISCH_TAC THEN
815 MATCH_MP_TAC COPRIME_EXP THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
816 MATCH_MP_TAC COPRIME_EXP THEN
817 ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[]);;
819 let COPRIME_REXP = prove
820 (`!m n k. coprime(m,n EXP k) <=> coprime(m,n) \/ k = 0`,
821 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
822 REWRITE_TAC[CONJUNCT1 EXP; COPRIME_1] THEN
823 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[COPRIME_EXP; NOT_SUC] THEN
824 REWRITE_TAC[EXP] THEN CONV_TAC NUMBER_RULE);;
826 let COPRIME_LEXP = prove
827 (`!m n k. coprime(m EXP k,n) <=> coprime(m,n) \/ k = 0`,
828 ONCE_REWRITE_TAC[COPRIME_SYM] THEN REWRITE_TAC[COPRIME_REXP]);;
830 let COPRIME_EXP2 = prove
831 (`!m n k. coprime(m EXP k,n EXP k) <=> coprime(m,n) \/ k = 0`,
832 REWRITE_TAC[COPRIME_REXP; COPRIME_LEXP; DISJ_ACI]);;
834 let COPRIME_EXP2_SUC = prove
835 (`!n a b. coprime(a EXP (SUC n),b EXP (SUC n)) <=> coprime(a,b)`,
836 REWRITE_TAC[COPRIME_EXP2; NOT_SUC]);;
838 let COPRIME_REFL = prove
839 (`!n. coprime(n,n) <=> (n = 1)`,
840 REWRITE_TAC[COPRIME_GCD; GCD_REFL]);;
842 let COPRIME_PLUS1 = prove
843 (`!n. coprime(n + 1,n)`,
846 let COPRIME_MINUS1 = prove
847 (`!n. ~(n = 0) ==> coprime(n - 1,n)`,
848 REPEAT STRIP_TAC THEN SIMP_TAC[coprime] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
849 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_SUB) THEN
850 ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - (n - 1) = 1`; DIVIDES_ONE]);;
852 let BEZOUT_GCD_POW = prove(
853 `!n a b. ?x y. (((a EXP n) * x) - ((b EXP n) * y) = gcd(a,b) EXP n) \/
854 (((b EXP n) * x) - ((a EXP n) * y) = gcd(a,b) EXP n)`,
855 REPEAT GEN_TAC THEN ASM_CASES_TAC `gcd(a,b) = 0` THENL
856 [STRUCT_CASES_TAC(SPEC `n:num` num_CASES) THEN
857 ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THENL
858 [MAP_EVERY EXISTS_TAC [`1`; `0`] THEN REWRITE_TAC[SUB_0];
859 REPEAT(EXISTS_TAC `0`) THEN REWRITE_TAC[MULT_CLAUSES; SUB_0]];
860 MP_TAC(SPECL [`a:num`; `b:num`] GCD) THEN
861 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
862 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[divides] THEN
863 DISCH_THEN(X_CHOOSE_THEN `b':num` ASSUME_TAC) THEN
864 DISCH_THEN(X_CHOOSE_THEN `a':num` ASSUME_TAC) THEN
865 MP_TAC(SPECL [`a:num`; `b:num`; `a':num`; `b':num`] GCD_COPRIME) THEN
866 RULE_ASSUM_TAC GSYM THEN RULE_ASSUM_TAC(ONCE_REWRITE_RULE[MULT_SYM]) THEN
867 ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o GSYM) THEN
868 ASM_REWRITE_TAC[] THEN
869 DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP COPRIME_EXP_IMP) THEN
870 REWRITE_TAC[COPRIME_BEZOUT] THEN
871 DISCH_THEN(X_CHOOSE_THEN `x:num` (X_CHOOSE_THEN `y:num` MP_TAC)) THEN
872 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THEN
873 DISCH_THEN (MP_TAC o AP_TERM `(*) (gcd(a,b) EXP n)`) THEN
874 REWRITE_TAC[MULT_CLAUSES; LEFT_SUB_DISTRIB] THEN
875 DISCH_THEN(SUBST1_TAC o SYM) THEN
876 MAP_EVERY EXISTS_TAC [`x:num`; `y:num`] THEN
877 REWRITE_TAC[MULT_ASSOC; GSYM MULT_EXP] THEN
878 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[MULT_SYM]) THEN
879 ASM_REWRITE_TAC[]]);;
882 `!n a b. gcd(a EXP n,b EXP n) = gcd(a,b) EXP n`,
883 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
884 ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN REPEAT CONJ_TAC THENL
885 [MATCH_MP_TAC DIVIDES_EXP THEN REWRITE_TAC[GCD];
886 MATCH_MP_TAC DIVIDES_EXP THEN REWRITE_TAC[GCD];
887 X_GEN_TAC `d:num` THEN STRIP_TAC THEN
888 MP_TAC(SPECL [`n:num`; `a:num`; `b:num`] BEZOUT_GCD_POW) THEN
889 DISCH_THEN(REPEAT_TCL CHOOSE_THEN (DISJ_CASES_THEN
890 (SUBST1_TAC o SYM))) THEN
891 MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
892 MATCH_MP_TAC DIVIDES_RMUL THEN ASM_REWRITE_TAC[]]);;
894 let DIVISION_DECOMP = prove(
895 `!a b c. a divides (b * c) ==>
896 ?b' c'. (a = b' * c') /\ b' divides b /\ c' divides c`,
897 REPEAT GEN_TAC THEN DISCH_TAC THEN
898 EXISTS_TAC `gcd(a,b)` THEN REWRITE_TAC[GCD] THEN
899 MP_TAC(SPECL [`a:num`; `b:num`] GCD_COPRIME_EXISTS) THEN
900 ASM_CASES_TAC `gcd(a,b) = 0` THENL
901 [ASM_REWRITE_TAC[] THEN EXISTS_TAC `1` THEN
902 RULE_ASSUM_TAC(REWRITE_RULE[GCD_ZERO]) THEN
903 ASM_REWRITE_TAC[MULT_CLAUSES; DIVIDES_1];
904 ASM_REWRITE_TAC[] THEN
905 DISCH_THEN(X_CHOOSE_THEN `a':num` (X_CHOOSE_THEN `b':num`
906 (STRIP_ASSUME_TAC o GSYM o ONCE_REWRITE_RULE[MULT_SYM]))) THEN
907 EXISTS_TAC `a':num` THEN ASM_REWRITE_TAC[] THEN
908 UNDISCH_TAC `a divides (b * c)` THEN
909 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC
910 (LAND_CONV o LAND_CONV) [GSYM th]) THEN
911 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV)
912 [GSYM th]) THEN REWRITE_TAC[MULT_ASSOC] THEN
913 DISCH_TAC THEN MATCH_MP_TAC COPRIME_DIVPROD THEN
914 EXISTS_TAC `b':num` THEN ASM_REWRITE_TAC[] THEN
915 MATCH_MP_TAC DIVIDES_CMUL2 THEN EXISTS_TAC `gcd(a,b)` THEN
916 REWRITE_TAC[MULT_ASSOC] THEN CONJ_TAC THEN
917 FIRST_ASSUM MATCH_ACCEPT_TAC]);;
919 let DIVIDES_EXP2_REV = prove
920 (`!n a b. (a EXP n) divides (b EXP n) /\ ~(n = 0) ==> a divides b`,
921 REPEAT GEN_TAC THEN ASM_CASES_TAC `gcd(a,b) = 0` THENL
922 [ASM_MESON_TAC[GCD_ZERO; DIVIDES_REFL]; ALL_TAC] THEN
923 FIRST_ASSUM(MP_TAC o MATCH_MP GCD_COPRIME_EXISTS) THEN
924 STRIP_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
925 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[MULT_EXP] THEN
926 ASM_SIMP_TAC[EXP_EQ_0; DIVIDES_RMUL2_EQ] THEN
927 DISCH_THEN(MP_TAC o MATCH_MP (NUMBER_RULE
928 `a divides b ==> coprime(a,b) ==> a divides 1`)) THEN
929 ASM_SIMP_TAC[COPRIME_EXP2; DIVIDES_ONE; DIVIDES_1; EXP_EQ_1]);;
931 let DIVIDES_EXP2_EQ = prove
932 (`!n a b. ~(n = 0) ==> ((a EXP n) divides (b EXP n) <=> a divides b)`,
933 MESON_TAC[DIVIDES_EXP2_REV; DIVIDES_EXP]);;
935 let DIVIDES_MUL = prove
936 (`!m n r. m divides r /\ n divides r /\ coprime(m,n) ==> (m * n) divides r`,
939 (* ------------------------------------------------------------------------- *)
940 (* A binary form of the Chinese Remainder Theorem. *)
941 (* ------------------------------------------------------------------------- *)
943 let CHINESE_REMAINDER = prove
944 (`!a b u v. coprime(a,b) /\ ~(a = 0) /\ ~(b = 0)
945 ==> ?x q1 q2. (x = u + q1 * a) /\ (x = v + q2 * b)`,
947 (`(?d x y. (d = 1) /\ P x y d) <=> (?x y. P x y 1)`,
949 REPEAT STRIP_TAC THEN
950 MP_TAC(SPECL [`b:num`; `a:num`] BEZOUT_ADD_STRONG) THEN
951 MP_TAC(SPECL [`a:num`; `b:num`] BEZOUT_ADD_STRONG) THEN
952 ASM_REWRITE_TAC[CONJ_ASSOC] THEN
953 SUBGOAL_THEN `!d. d divides a /\ d divides b <=> (d = 1)`
954 (fun th -> REWRITE_TAC[th; ONCE_REWRITE_RULE[CONJ_SYM] th])
956 [UNDISCH_TAC `coprime(a,b)` THEN
957 SIMP_TAC[GSYM DIVIDES_GCD; COPRIME_GCD; DIVIDES_ONE]; ALL_TAC] THEN
958 REWRITE_TAC[lemma] THEN
959 DISCH_THEN(X_CHOOSE_THEN `x1:num` (X_CHOOSE_TAC `y1:num`)) THEN
960 DISCH_THEN(X_CHOOSE_THEN `x2:num` (X_CHOOSE_TAC `y2:num`)) THEN
961 EXISTS_TAC `v * a * x1 + u * b * x2:num` THEN
962 EXISTS_TAC `v * x1 + u * y2:num` THEN
963 EXISTS_TAC `v * y1 + u * x2:num` THEN CONJ_TAC THENL
964 [SUBST1_TAC(ASSUME `b * x2 = a * y2 + 1`);
965 SUBST1_TAC(ASSUME `a * x1 = b * y1 + 1`)] THEN
966 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
967 REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC]);;
969 (* ------------------------------------------------------------------------- *)
971 (* ------------------------------------------------------------------------- *)
973 let prime = new_definition
974 `prime(p) <=> ~(p = 1) /\ !x. x divides p ==> (x = 1) \/ (x = p)`;;
976 (* ------------------------------------------------------------------------- *)
977 (* A few useful theorems about primes *)
978 (* ------------------------------------------------------------------------- *)
982 REWRITE_TAC[prime] THEN
983 DISCH_THEN(MP_TAC o SPEC `2` o CONJUNCT2) THEN
984 REWRITE_TAC[DIVIDES_0; ARITH]);;
988 REWRITE_TAC[prime]);;
992 REWRITE_TAC[prime; ARITH] THEN
993 REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
994 FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
995 REWRITE_TAC[ARITH] THEN REWRITE_TAC[LE_LT] THEN
996 REWRITE_TAC[num_CONV `2`; num_CONV `1`; LESS_THM; NOT_LESS_0] THEN
997 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC) THEN
998 REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[DIVIDES_ZERO] THEN
999 REWRITE_TAC[ARITH] THEN REWRITE_TAC[]);;
1001 let PRIME_GE_2 = prove(
1002 `!p. prime(p) ==> 2 <= p`,
1003 GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LE] THEN
1004 REWRITE_TAC[num_CONV `2`; num_CONV `1`; LESS_THM; NOT_LESS_0] THEN
1005 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
1006 REWRITE_TAC[SYM(num_CONV `1`); PRIME_0; PRIME_1]);;
1008 let PRIME_FACTOR = prove(
1009 `!n. ~(n = 1) ==> ?p. prime(p) /\ p divides n`,
1010 MATCH_MP_TAC num_WF THEN
1011 X_GEN_TAC `n:num` THEN REPEAT STRIP_TAC THEN
1012 ASM_CASES_TAC `prime(n)` THENL
1013 [EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[DIVIDES_REFL];
1014 UNDISCH_TAC `~prime(n)` THEN
1015 DISCH_THEN(MP_TAC o REWRITE_RULE[prime]) THEN
1016 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[NOT_FORALL_THM] THEN
1017 DISCH_THEN(X_CHOOSE_THEN `m:num` MP_TAC) THEN
1018 REWRITE_TAC[NOT_IMP; DE_MORGAN_THM] THEN STRIP_TAC THEN
1019 FIRST_ASSUM(DISJ_CASES_THEN MP_TAC o MATCH_MP DIVIDES_LE) THENL
1020 [ASM_REWRITE_TAC[LE_LT] THEN
1021 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[] THEN
1022 DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
1023 EXISTS_TAC `p:num` THEN ASM_REWRITE_TAC[] THEN
1024 MATCH_MP_TAC DIVIDES_TRANS THEN EXISTS_TAC `m:num` THEN
1026 DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `2` THEN
1027 REWRITE_TAC[PRIME_2; DIVIDES_0]]]);;
1029 let PRIME_FACTOR_LT = prove(
1030 `!n m p. prime(p) /\ ~(n = 0) /\ (n = p * m) ==> m < n`,
1031 REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN
1032 ASM_REWRITE_TAC[LE_EXISTS] THEN
1033 DISCH_THEN(X_CHOOSE_THEN `q:num` SUBST_ALL_TAC) THEN
1034 REWRITE_TAC[num_CONV `2`; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
1035 REWRITE_TAC[GSYM ADD_ASSOC] THEN MATCH_MP_TAC LESS_ADD_NONZERO THEN
1036 REWRITE_TAC[ADD_EQ_0] THEN DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
1037 FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN
1038 ASM_REWRITE_TAC[MULT_CLAUSES]);;
1040 let PRIME_FACTOR_INDUCT = prove
1042 (!p n. prime p /\ ~(n = 0) /\ P n ==> P(p * n))
1044 GEN_TAC THEN STRIP_TAC THEN
1045 MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
1046 DISCH_TAC THEN MAP_EVERY ASM_CASES_TAC [`n = 0`; `n = 1`] THEN
1047 ASM_REWRITE_TAC[] THEN FIRST_ASSUM(X_CHOOSE_THEN `p:num`
1048 STRIP_ASSUME_TAC o MATCH_MP PRIME_FACTOR) THEN
1049 FIRST_X_ASSUM(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC o
1050 GEN_REWRITE_RULE I [divides]) THEN
1051 FIRST_X_ASSUM(MP_TAC o SPECL [`p:num`; `d:num`]) THEN
1052 RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
1053 DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1054 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[PRIME_FACTOR_LT; MULT_EQ_0]);;
1056 (* ------------------------------------------------------------------------- *)
1057 (* Infinitude of primes. *)
1058 (* ------------------------------------------------------------------------- *)
1060 let EUCLID_BOUND = prove
1061 (`!n. ?p. prime(p) /\ n < p /\ p <= SUC(FACT n)`,
1062 GEN_TAC THEN MP_TAC(SPEC `FACT n + 1` PRIME_FACTOR) THEN
1063 SIMP_TAC[ARITH_RULE `0 < n ==> ~(n + 1 = 1)`; ADD1; FACT_LT] THEN
1064 MATCH_MP_TAC MONO_EXISTS THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
1065 [ASM_MESON_TAC[DIVIDES_ADD_REVR; DIVIDES_ONE; PRIME_1; NOT_LT; PRIME_0;
1066 ARITH_RULE `(p = 0) \/ 1 <= p`; DIVIDES_FACT];
1067 ASM_MESON_TAC[DIVIDES_LE; ARITH_RULE `~(x + 1 = 0)`]]);;
1070 (`!n. ?p. prime(p) /\ p > n`,
1071 REWRITE_TAC[GT] THEN MESON_TAC[EUCLID_BOUND]);;
1073 let PRIMES_INFINITE = prove
1074 (`INFINITE {p | prime p}`,
1075 REWRITE_TAC[INFINITE; num_FINITE; IN_ELIM_THM] THEN
1076 MESON_TAC[EUCLID; NOT_LE; GT]);;
1078 let COPRIME_PRIME = prove(
1079 `!p a b. coprime(a,b) ==> ~(prime(p) /\ p divides a /\ p divides b)`,
1080 REPEAT GEN_TAC THEN REWRITE_TAC[coprime] THEN REPEAT STRIP_TAC THEN
1081 SUBGOAL_THEN `p = 1` SUBST_ALL_TAC THENL
1082 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1083 UNDISCH_TAC `prime 1` THEN REWRITE_TAC[PRIME_1]]);;
1085 let COPRIME_PRIME_EQ = prove(
1086 `!a b. coprime(a,b) <=> !p. ~(prime(p) /\ p divides a /\ p divides b)`,
1087 REPEAT GEN_TAC THEN EQ_TAC THENL
1088 [DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP COPRIME_PRIME th]);
1089 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[coprime] THEN
1090 ONCE_REWRITE_TAC[NOT_FORALL_THM] THEN REWRITE_TAC[NOT_IMP] THEN
1091 DISCH_THEN(X_CHOOSE_THEN `d:num` STRIP_ASSUME_TAC) THEN
1092 FIRST_ASSUM(X_CHOOSE_TAC `p:num` o MATCH_MP PRIME_FACTOR) THEN
1093 EXISTS_TAC `p:num` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
1094 MATCH_MP_TAC DIVIDES_TRANS THEN EXISTS_TAC `d:num` THEN
1095 ASM_REWRITE_TAC[]]);;
1097 let PRIME_COPRIME = prove(
1098 `!n p. prime(p) ==> (n = 1) \/ p divides n \/ coprime(p,n)`,
1099 REPEAT GEN_TAC THEN REWRITE_TAC[prime; COPRIME_GCD] THEN
1100 STRIP_ASSUME_TAC(SPECL [`p:num`; `n:num`] GCD) THEN
1101 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1102 DISCH_THEN(MP_TAC o SPEC `gcd(p,n)`) THEN ASM_REWRITE_TAC[] THEN
1103 DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
1104 ASM_REWRITE_TAC[]);;
1106 let PRIME_COPRIME_STRONG = prove
1107 (`!n p. prime(p) ==> p divides n \/ coprime(p,n)`,
1108 MESON_TAC[PRIME_COPRIME; COPRIME_1]);;
1110 let PRIME_COPRIME_EQ = prove
1111 (`!p n. prime p ==> (coprime(p,n) <=> ~(p divides n))`,
1112 REPEAT STRIP_TAC THEN
1113 MATCH_MP_TAC(TAUT `(b \/ a) /\ ~(a /\ b) ==> (a <=> ~b)`) THEN
1114 ASM_SIMP_TAC[PRIME_COPRIME_STRONG] THEN
1115 ASM_MESON_TAC[COPRIME_REFL; PRIME_1; NUMBER_RULE
1116 `coprime(p,n) /\ p divides n ==> coprime(p,p)`]);;
1118 let COPRIME_PRIMEPOW = prove
1119 (`!p k m. prime p /\ ~(k = 0) ==> (coprime(m,p EXP k) <=> ~(p divides m))`,
1120 SIMP_TAC[COPRIME_REXP] THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
1121 SIMP_TAC[PRIME_COPRIME_EQ]);;
1123 let COPRIME_BEZOUT_STRONG = prove
1124 (`!a b. coprime(a,b) /\ ~(b = 1) ==> ?x y. a * x = b * y + 1`,
1125 REPEAT GEN_TAC THEN STRIP_TAC THEN
1126 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COPRIME_GCD]) THEN
1127 DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC BEZOUT_GCD_STRONG THEN
1128 ASM_MESON_TAC[COPRIME_0; COPRIME_SYM]);;
1130 let COPRIME_BEZOUT_ALT = prove
1131 (`!a b. coprime(a,b) /\ ~(a = 0) ==> ?x y. a * x = b * y + 1`,
1132 REPEAT GEN_TAC THEN STRIP_TAC THEN
1133 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COPRIME_GCD]) THEN
1134 DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC BEZOUT_GCD_STRONG THEN
1135 ASM_MESON_TAC[COPRIME_0; COPRIME_SYM]);;
1137 let BEZOUT_PRIME = prove
1138 (`!a p. prime p /\ ~(p divides a) ==> ?x y. a * x = p * y + 1`,
1139 MESON_TAC[PRIME_COPRIME_STRONG; COPRIME_SYM;
1140 COPRIME_BEZOUT_STRONG; PRIME_1]);;
1142 let PRIME_DIVPROD = prove(
1143 `!p a b. prime(p) /\ p divides (a * b) ==> p divides a \/ p divides b`,
1144 REPEAT GEN_TAC THEN STRIP_TAC THEN
1145 FIRST_ASSUM(MP_TAC o SPEC `a:num` o MATCH_MP PRIME_COPRIME) THEN
1146 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
1147 ASM_REWRITE_TAC[] THENL
1148 [DISJ2_TAC THEN UNDISCH_TAC `p divides (a * b)` THEN
1149 ASM_REWRITE_TAC[MULT_CLAUSES];
1150 DISJ2_TAC THEN MATCH_MP_TAC COPRIME_DIVPROD THEN
1151 EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[]]);;
1153 let PRIME_DIVPROD_EQ = prove
1154 (`!p a b. prime(p) ==> (p divides (a * b) <=> p divides a \/ p divides b)`,
1155 MESON_TAC[PRIME_DIVPROD; DIVIDES_LMUL; DIVIDES_RMUL]);;
1157 let PRIME_DIVEXP = prove(
1158 `!n p x. prime(p) /\ p divides (x EXP n) ==> p divides x`,
1159 INDUCT_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC[EXP; DIVIDES_ONE] THENL
1160 [DISCH_THEN(SUBST1_TAC o CONJUNCT2) THEN REWRITE_TAC[DIVIDES_1];
1161 DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN
1162 DISCH_THEN(DISJ_CASES_TAC o MATCH_MP PRIME_DIVPROD) THEN
1163 ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1164 ASM_REWRITE_TAC[]]);;
1166 let PRIME_DIVEXP_N = prove(
1167 `!n p x. prime(p) /\ p divides (x EXP n) ==> (p EXP n) divides (x EXP n)`,
1168 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP PRIME_DIVEXP) THEN
1169 MATCH_ACCEPT_TAC DIVIDES_EXP);;
1171 let PRIME_DIVEXP_EQ = prove
1172 (`!n p x. prime p ==> (p divides x EXP n <=> p divides x /\ ~(n = 0))`,
1173 REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THEN
1174 ASM_REWRITE_TAC[EXP; DIVIDES_ONE] THEN
1175 ASM_MESON_TAC[PRIME_DIVEXP; DIVIDES_REXP; PRIME_1]);;
1177 let PARITY_EXP = prove(
1178 `!n x. EVEN(x EXP (SUC n)) = EVEN(x)`,
1179 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM DIVIDES_2] THEN EQ_TAC THENL
1180 [DISCH_TAC THEN MATCH_MP_TAC PRIME_DIVEXP THEN
1181 EXISTS_TAC `SUC n` THEN ASM_REWRITE_TAC[PRIME_2];
1182 REWRITE_TAC[EXP] THEN MATCH_ACCEPT_TAC DIVIDES_RMUL]);;
1184 let COPRIME_SOS = prove
1185 (`!x y. coprime(x,y) ==> coprime(x * y,(x EXP 2) + (y EXP 2))`,
1188 let PRIME_IMP_NZ = prove
1189 (`!p. prime(p) ==> ~(p = 0)`,
1190 MESON_TAC[PRIME_0]);;
1192 let DISTINCT_PRIME_COPRIME = prove
1193 (`!p q. prime p /\ prime q /\ ~(p = q) ==> coprime(p,q)`,
1194 MESON_TAC[prime; coprime; PRIME_1]);;
1196 let PRIME_COPRIME_LT = prove
1197 (`!x p. prime p /\ 0 < x /\ x < p ==> coprime(x,p)`,
1198 REWRITE_TAC[coprime; prime] THEN
1199 MESON_TAC[LT_REFL; DIVIDES_LE; NOT_LT; PRIME_0]);;
1201 let DIVIDES_PRIME_PRIME = prove
1202 (`!p q. prime p /\ prime q ==> (p divides q <=> p = q)`,
1203 MESON_TAC[DIVIDES_REFL; DISTINCT_PRIME_COPRIME; PRIME_COPRIME_EQ]);;
1205 let DIVIDES_PRIME_EXP_LE = prove
1206 (`!p q m n. prime p /\ prime q
1207 ==> ((p EXP m) divides (q EXP n) <=> m = 0 \/ p = q /\ m <= n)`,
1208 GEN_TAC THEN GEN_TAC THEN REPEAT INDUCT_TAC THEN
1209 ASM_SIMP_TAC[EXP; DIVIDES_1; DIVIDES_ONE; MULT_EQ_1; NOT_SUC] THENL
1210 [MESON_TAC[PRIME_1; ARITH_RULE `~(SUC m <= 0)`]; ALL_TAC] THEN
1211 ASM_CASES_TAC `p:num = q` THEN
1212 ASM_SIMP_TAC[DIVIDES_EXP_LE; PRIME_GE_2; GSYM(CONJUNCT2 EXP)] THEN
1213 ASM_MESON_TAC[PRIME_DIVEXP; DIVIDES_PRIME_PRIME; EXP; DIVIDES_RMUL2]);;
1215 let EQ_PRIME_EXP = prove
1216 (`!p q m n. prime p /\ prime q
1217 ==> (p EXP m = q EXP n <=> m = 0 /\ n = 0 \/ p = q /\ m = n)`,
1218 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM DIVIDES_ANTISYM] THEN
1219 ASM_SIMP_TAC[DIVIDES_PRIME_EXP_LE] THEN ARITH_TAC);;
1221 let PRIME_ODD = prove
1222 (`!p. prime p ==> p = 2 \/ ODD p`,
1223 GEN_TAC THEN REWRITE_TAC[prime; GSYM NOT_EVEN; EVEN_EXISTS] THEN
1224 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `2`)) THEN
1225 REWRITE_TAC[divides; ARITH] THEN MESON_TAC[]);;
1227 let DIVIDES_FACT_PRIME = prove
1228 (`!p. prime p ==> !n. p divides (FACT n) <=> p <= n`,
1229 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT; LE] THENL
1230 [ASM_MESON_TAC[DIVIDES_ONE; PRIME_0; PRIME_1];
1231 ASM_MESON_TAC[PRIME_DIVPROD_EQ; DIVIDES_LE; NOT_SUC; DIVIDES_REFL;
1232 ARITH_RULE `~(p <= n) /\ p <= SUC n ==> p = SUC n`]]);;
1234 let EQ_PRIMEPOW = prove
1235 (`!p m n. prime p ==> (p EXP m = p EXP n <=> m = n)`,
1236 ONCE_REWRITE_TAC[GSYM LE_ANTISYM] THEN
1237 SIMP_TAC[LE_EXP; PRIME_IMP_NZ] THEN MESON_TAC[PRIME_1]);;
1239 let COPRIME_2 = prove
1240 (`(!n. coprime(2,n) <=> ODD n) /\ (!n. coprime(n,2) <=> ODD n)`,
1241 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [COPRIME_SYM] THEN
1242 SIMP_TAC[PRIME_COPRIME_EQ; PRIME_2; DIVIDES_2; NOT_EVEN]);;
1244 let DIVIDES_EXP_PLUS1 = prove
1245 (`!n k. ODD k ==> (n + 1) divides (n EXP k + 1)`,
1246 GEN_TAC THEN REWRITE_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1247 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[FORALL_UNWIND_THM2] THEN
1248 INDUCT_TAC THEN CONV_TAC NUM_REDUCE_CONV THEN
1249 REWRITE_TAC[EXP_1; DIVIDES_REFL] THEN
1250 REWRITE_TAC[ARITH_RULE `SUC(2 * SUC n) = SUC(2 * n) + 2`] THEN
1251 REWRITE_TAC[EXP_ADD; EXP_2] THEN POP_ASSUM MP_TAC THEN NUMBER_TAC);;
1253 let DIVIDES_EXP_MINUS1 = prove
1254 (`!k n. (n - 1) divides (n EXP k - 1)`,
1255 REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
1256 [STRUCT_CASES_TAC(SPEC `k:num` num_CASES) THEN
1257 ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THEN CONV_TAC NUM_REDUCE_CONV THEN
1258 REWRITE_TAC[DIVIDES_REFL];
1259 REWRITE_TAC[num_divides] THEN
1260 ASM_SIMP_TAC[GSYM INT_OF_NUM_SUB; LE_1; EXP_EQ_0; ARITH] THEN
1261 POP_ASSUM(K ALL_TAC) THEN REWRITE_TAC[GSYM INT_OF_NUM_POW] THEN
1262 SPEC_TAC(`k:num`,`k:num`) THEN INDUCT_TAC THEN REWRITE_TAC[INT_POW] THEN
1263 REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC]);;
1265 (* ------------------------------------------------------------------------- *)
1266 (* One property of coprimality is easier to prove via prime factors. *)
1267 (* ------------------------------------------------------------------------- *)
1269 let COPRIME_EXP_DIVPROD = prove
1271 (d EXP n) divides (a * b) /\ coprime(d,a) ==> (d EXP n) divides b`,
1272 MESON_TAC[COPRIME_DIVPROD; COPRIME_EXP; COPRIME_SYM]);;
1274 let PRIME_COPRIME_CASES = prove
1275 (`!p a b. prime p /\ coprime(a,b) ==> coprime(p,a) \/ coprime(p,b)`,
1276 MESON_TAC[COPRIME_PRIME; PRIME_COPRIME_EQ]);;
1278 let PRIME_DIVPROD_POW = prove
1279 (`!n p a b. prime(p) /\ coprime(a,b) /\ (p EXP n) divides (a * b)
1280 ==> (p EXP n) divides a \/ (p EXP n) divides b`,
1281 MESON_TAC[COPRIME_EXP_DIVPROD; PRIME_COPRIME_CASES; MULT_SYM]);;
1283 let EXP_MULT_EXISTS = prove
1284 (`!m n p k. ~(m = 0) /\ m EXP k * n = p EXP k ==> ?q. n = q EXP k`,
1285 REPEAT GEN_TAC THEN ASM_CASES_TAC `k = 0` THEN
1286 ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THEN STRIP_TAC THEN
1287 MP_TAC(SPECL [`k:num`; `m:num`; `p:num`] DIVIDES_EXP2_REV) THEN
1288 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
1289 [ASM_MESON_TAC[divides; MULT_SYM]; ALL_TAC] THEN
1290 REWRITE_TAC[divides] THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN
1291 FIRST_X_ASSUM(MP_TAC o SYM) THEN
1292 ASM_REWRITE_TAC[MULT_EXP; GSYM MULT_ASSOC; EQ_MULT_LCANCEL; EXP_EQ_0] THEN
1295 let COPRIME_POW = prove
1296 (`!n a b c. coprime(a,b) /\ a * b = c EXP n
1297 ==> ?r s. a = r EXP n /\ b = s EXP n`,
1298 GEN_TAC THEN GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN
1299 GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN ASM_CASES_TAC `n = 0` THEN
1300 ASM_SIMP_TAC[EXP; MULT_EQ_1] THEN MATCH_MP_TAC PRIME_FACTOR_INDUCT THEN
1301 REPEAT CONJ_TAC THENL
1302 [ASM_REWRITE_TAC[EXP_ZERO; MULT_EQ_0] THEN
1303 ASM_MESON_TAC[COPRIME_0; EXP_ZERO; COPRIME_0; EXP_ONE];
1304 SIMP_TAC[EXP_ONE; MULT_EQ_1] THEN MESON_TAC[EXP_ONE];
1305 REWRITE_TAC[MULT_EXP] THEN REPEAT STRIP_TAC THEN
1306 SUBGOAL_THEN `p EXP n divides a \/ p EXP n divides b` MP_TAC THENL
1307 [ASM_MESON_TAC[PRIME_DIVPROD_POW; divides]; ALL_TAC] THEN
1308 REWRITE_TAC[divides] THEN
1309 DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC)) THEN
1310 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COPRIME_SYM]) THEN
1311 ASM_SIMP_TAC[COPRIME_RMUL; COPRIME_LMUL; COPRIME_LEXP; COPRIME_REXP] THEN
1313 [FIRST_X_ASSUM(MP_TAC o SPECL [`b:num`; `d:num`]);
1314 FIRST_X_ASSUM(MP_TAC o SPECL [`d:num`; `a:num`])] THEN
1315 ASM_REWRITE_TAC[] THEN
1317 [MATCH_MP_TAC(NUM_RING `!p. ~(p = 0) /\ a * p = b * p ==> a = b`) THEN
1318 EXISTS_TAC `p EXP n` THEN ASM_SIMP_TAC[EXP_EQ_0; PRIME_IMP_NZ] THEN
1319 FIRST_X_ASSUM(MP_TAC o SYM) THEN CONV_TAC NUM_RING;
1320 STRIP_TAC THEN ASM_REWRITE_TAC[GSYM MULT_EXP] THEN MESON_TAC[]])]);;
1322 (* ------------------------------------------------------------------------- *)
1323 (* More useful lemmas. *)
1324 (* ------------------------------------------------------------------------- *)
1326 let PRIME_EXP = prove
1327 (`!p n. prime(p EXP n) <=> prime(p) /\ (n = 1)`,
1328 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[EXP; PRIME_1; ARITH_EQ] THEN
1329 POP_ASSUM_LIST(K ALL_TAC) THEN SPEC_TAC(`n:num`,`n:num`) THEN
1330 ASM_CASES_TAC `p = 0` THENL
1331 [ASM_REWRITE_TAC[PRIME_0; EXP; MULT_CLAUSES]; ALL_TAC] THEN
1332 INDUCT_TAC THEN REWRITE_TAC[ARITH; EXP_1; EXP; MULT_CLAUSES] THEN
1333 REWRITE_TAC[ARITH_RULE `~(SUC(SUC n) = 1)`] THEN
1334 REWRITE_TAC[prime; DE_MORGAN_THM] THEN
1335 ASM_REWRITE_TAC[MULT_EQ_1; EXP_EQ_1] THEN ASM_CASES_TAC `p = 1` THEN
1336 ASM_REWRITE_TAC[NOT_IMP; DE_MORGAN_THM] THEN
1337 DISCH_THEN(MP_TAC o SPEC `p:num`) THEN ASM_REWRITE_TAC[NOT_IMP] THEN
1338 CONJ_TAC THENL [MESON_TAC[EXP; divides]; ALL_TAC] THEN
1339 MATCH_MP_TAC(ARITH_RULE `p < pn:num ==> ~(p = pn)`) THEN
1340 GEN_REWRITE_TAC LAND_CONV [GSYM EXP_1] THEN
1341 REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
1342 ASM_REWRITE_TAC[LT_EXP; ARITH_EQ] THEN
1343 MAP_EVERY UNDISCH_TAC [`~(p = 0)`; `~(p = 1)`] THEN ARITH_TAC);;
1345 let PRIME_POWER_MULT = prove
1346 (`!k x y p. prime p /\ (x * y = p EXP k)
1347 ==> ?i j. (x = p EXP i) /\ (y = p EXP j)`,
1348 INDUCT_TAC THEN REWRITE_TAC[EXP; MULT_EQ_1] THENL
1349 [MESON_TAC[EXP]; ALL_TAC] THEN
1350 REPEAT STRIP_TAC THEN
1351 SUBGOAL_THEN `p divides x \/ p divides y` MP_TAC THENL
1352 [ASM_MESON_TAC[PRIME_DIVPROD; divides; MULT_AC]; ALL_TAC] THEN
1353 REWRITE_TAC[divides] THEN
1354 SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
1355 [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
1356 DISCH_THEN(DISJ_CASES_THEN (X_CHOOSE_THEN `d:num` SUBST_ALL_TAC)) THENL
1357 [UNDISCH_TAC `(p * d) * y = p * p EXP k`;
1358 UNDISCH_TAC `x * p * d = p * p EXP k` THEN
1359 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [MULT_SYM]] THEN
1360 REWRITE_TAC[GSYM MULT_ASSOC] THEN
1361 ASM_REWRITE_TAC[EQ_MULT_LCANCEL] THEN DISCH_TAC THENL
1362 [FIRST_X_ASSUM(MP_TAC o SPECL [`d:num`; `y:num`; `p:num`]);
1363 FIRST_X_ASSUM(MP_TAC o SPECL [`d:num`; `x:num`; `p:num`])] THEN
1364 ASM_REWRITE_TAC[] THEN MESON_TAC[EXP]);;
1366 let PRIME_POWER_EXP = prove
1367 (`!n x p k. prime p /\ ~(n = 0) /\ (x EXP n = p EXP k) ==> ?i. x = p EXP i`,
1368 INDUCT_TAC THEN REWRITE_TAC[EXP] THEN
1369 REPEAT GEN_TAC THEN REWRITE_TAC[NOT_SUC] THEN
1370 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[EXP] THEN
1371 ASM_MESON_TAC[PRIME_POWER_MULT]);;
1373 let DIVIDES_PRIMEPOW = prove
1374 (`!p. prime p ==> !d. d divides (p EXP k) <=> ?i. i <= k /\ d = p EXP i`,
1375 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL
1376 [REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:num` THEN
1378 MP_TAC(SPECL [`k:num`; `d:num`; `e:num`; `p:num`] PRIME_POWER_MULT) THEN
1379 ASM_REWRITE_TAC[] THEN
1380 DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN
1381 FIRST_X_ASSUM(MP_TAC o SYM) THEN REWRITE_TAC[GSYM EXP_ADD] THEN
1382 REWRITE_TAC[GSYM LE_ANTISYM; LE_EXP] THEN REWRITE_TAC[LE_ANTISYM] THEN
1383 POP_ASSUM MP_TAC THEN ASM_CASES_TAC `p = 0` THEN ASM_SIMP_TAC[PRIME_0] THEN
1384 ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[PRIME_1; LE_ANTISYM] THEN
1386 REWRITE_TAC[LE_EXISTS] THEN STRIP_TAC THEN
1387 ASM_REWRITE_TAC[EXP_ADD] THEN MESON_TAC[DIVIDES_RMUL; DIVIDES_REFL]]);;
1389 let PRIMEPOW_DIVIDES_PROD = prove
1391 prime p /\ (p EXP k) divides (m * n)
1392 ==> ?i j. (p EXP i) divides m /\ (p EXP j) divides n /\ k = i + j`,
1393 REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION_DECOMP) THEN
1394 REWRITE_TAC[NUMBER_RULE
1395 `a = b * c <=> b divides a /\ c divides a /\ b * c = a`] THEN
1396 ASM_MESON_TAC[EXP_ADD; EQ_PRIMEPOW; DIVIDES_PRIMEPOW]);;
1398 let COPRIME_DIVISORS = prove
1399 (`!a b d e. d divides a /\ e divides b /\ coprime(a,b) ==> coprime(d,e)`,
1402 let PRIMEPOW_FACTOR = prove
1404 ==> ?p k m. prime p /\ 1 <= k /\ coprime(p,m) /\ n = p EXP k * m`,
1405 REPEAT STRIP_TAC THEN MP_TAC(ISPEC `n:num` PRIME_FACTOR) THEN
1406 ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1407 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `p:num` THEN STRIP_TAC THEN
1408 MP_TAC(ISPECL [`n:num`; `p:num`] FACTORIZATION_INDEX) THEN
1409 ASM_SIMP_TAC[PRIME_GE_2; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1410 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
1411 REWRITE_TAC[divides; LEFT_AND_EXISTS_THM] THEN
1412 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
1413 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `k + 1`)) THEN
1414 ASM_REWRITE_TAC[ARITH_RULE `k < k + 1`; EXP_ADD; GSYM MULT_ASSOC] THEN
1415 ASM_SIMP_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; PRIME_IMP_NZ] THEN
1416 REWRITE_TAC[EXP_1; GSYM divides] THEN UNDISCH_TAC `(p:num) divides n` THEN
1417 ASM_REWRITE_TAC[] THEN
1418 ASM_CASES_TAC `k = 0` THEN ASM_SIMP_TAC[EXP; MULT_CLAUSES; LE_1] THEN
1419 ASM_MESON_TAC[PRIME_COPRIME_STRONG]);;
1421 let PRIMEPOW_DIVISORS_DIVIDES = prove
1422 (`!m n. m divides n <=>
1423 !p k. prime p /\ p EXP k divides m ==> p EXP k divides n`,
1424 REWRITE_TAC[TAUT `(p <=> q) <=> (p ==> q) /\ (q ==> p)`] THEN
1425 REWRITE_TAC[FORALL_AND_THM] THEN CONJ_TAC THENL
1426 [MESON_TAC[DIVIDES_TRANS]; ALL_TAC] THEN
1427 MATCH_MP_TAC num_WF THEN X_GEN_TAC `m:num` THEN
1428 DISCH_THEN(LABEL_TAC "*") THEN X_GEN_TAC `n:num` THEN
1429 ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THENL
1430 [MP_TAC(SPEC `n:num` EUCLID) THEN REWRITE_TAC[GT] THEN
1431 DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
1432 DISCH_THEN(MP_TAC o SPECL [`p:num`; `1`]) THEN ASM_REWRITE_TAC[EXP_1] THEN
1433 DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
1434 ASM_SIMP_TAC[GSYM NOT_LT; DIVIDES_REFL];
1436 ASM_CASES_TAC `m = 1` THEN ASM_REWRITE_TAC[DIVIDES_1] THEN
1437 MP_TAC(SPEC `m:num` PRIMEPOW_FACTOR) THEN
1438 ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
1439 MAP_EVERY X_GEN_TAC [`p:num`; `k:num`; `r:num`] THEN STRIP_TAC THEN
1440 DISCH_THEN(fun th ->
1441 MP_TAC(SPECL[`p:num`; `k:num`] th) THEN
1442 ASM_REWRITE_TAC[NUMBER_RULE `a divides (a * b)`] THEN
1444 REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
1445 X_GEN_TAC `s:num` THEN DISCH_TAC THEN ASM_REWRITE_TAC[GSYM divides] THEN
1446 MATCH_MP_TAC DIVIDES_MUL_L THEN REMOVE_THEN "*" (MP_TAC o SPEC `r:num`) THEN
1447 ASM_CASES_TAC `r = 0` THENL [ASM_MESON_TAC[MULT_CLAUSES]; ALL_TAC] THEN
1448 ASM_REWRITE_TAC[ARITH_RULE `q < p * q <=> 1 * q < p * q`] THEN
1449 ASM_SIMP_TAC[LT_MULT_RCANCEL; ARITH_RULE `1 < p <=> ~(p = 0 \/ p = 1)`] THEN
1450 REWRITE_TAC[EXP_EQ_0; EXP_EQ_1] THEN
1451 ANTS_TAC THENL [ASM_MESON_TAC[PRIME_0; PRIME_1; LE_1]; ALL_TAC] THEN
1452 DISCH_THEN MATCH_MP_TAC THEN MAP_EVERY X_GEN_TAC [`q:num`; `l:num`] THEN
1453 ASM_CASES_TAC `l = 0` THEN ASM_REWRITE_TAC[EXP; DIVIDES_1] THEN
1454 STRIP_TAC THEN ASM_CASES_TAC `q:num = p` THENL
1455 [UNDISCH_TAC `coprime(p,r)` THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
1456 REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `p:num`) THEN
1457 ASM_SIMP_TAC[DIVIDES_REFL; PRIME_GE_2; ARITH_RULE
1458 `2 <= p ==> ~(p = 1)`] THEN
1459 MATCH_MP_TAC(TAUT `p ==> ~p ==> q`) THEN
1460 TRANS_TAC DIVIDES_TRANS `p EXP l` THEN
1461 ASM_MESON_TAC[DIVIDES_REXP; DIVIDES_REFL];
1462 FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `l:num`]) THEN
1463 ASM_SIMP_TAC[DIVIDES_LMUL] THEN DISCH_THEN(MATCH_MP_TAC o MATCH_MP
1464 (REWRITE_RULE[IMP_CONJ] COPRIME_EXP_DIVPROD)) THEN
1465 MATCH_MP_TAC COPRIME_EXP THEN ASM_MESON_TAC[DISTINCT_PRIME_COPRIME]]);;
1467 let PRIMEPOW_DIVISORS_EQ = prove
1469 !p k. prime p ==> (p EXP k divides m <=> p EXP k divides n)`,
1470 MESON_TAC[DIVIDES_ANTISYM; PRIMEPOW_DIVISORS_DIVIDES]);;
1472 (* ------------------------------------------------------------------------- *)
1473 (* Index of a (usually prime) divisor of a number. *)
1474 (* ------------------------------------------------------------------------- *)
1476 let FINITE_EXP_LE = prove
1477 (`!P p n. 2 <= p ==> FINITE {j | P j /\ p EXP j <= n}`,
1478 REPEAT STRIP_TAC THEN
1479 MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
1480 SIMP_TAC[FINITE_NUMSEG; SUBSET; IN_ELIM_THM; LE_0; IN_NUMSEG] THEN
1481 X_GEN_TAC `i:num` THEN STRIP_TAC THEN TRANS_TAC LE_TRANS `p EXP i` THEN
1482 ASM_REWRITE_TAC[] THEN TRANS_TAC LE_TRANS `2 EXP i` THEN
1483 ASM_SIMP_TAC[EXP_MONO_LE_IMP; LT_POW2_REFL; LT_IMP_LE]);;
1485 let FINITE_INDICES = prove
1486 (`!P p n. 2 <= p /\ ~(n = 0) ==> FINITE {j | P j /\ p EXP j divides n}`,
1487 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
1488 EXISTS_TAC `{j | P j /\ p EXP j <= n}` THEN
1489 ASM_SIMP_TAC[FINITE_EXP_LE] THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
1490 ASM_MESON_TAC[DIVIDES_LE]);;
1492 let index_def = new_definition
1493 `index p n = if p <= 1 \/ n = 0 then 0
1494 else CARD {j | 1 <= j /\ p EXP j divides n}`;;
1497 (`!p. index p 0 = 0`,
1498 REWRITE_TAC[index_def]);;
1500 let PRIMEPOW_DIVIDES_INDEX = prove
1501 (`!n p k. p EXP k divides n <=> n = 0 \/ p = 1 \/ k <= index p n`,
1502 REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
1503 ASM_REWRITE_TAC[INDEX_0; DIVIDES_0; EXP_EQ_0] THEN
1504 ASM_CASES_TAC `p = 0` THEN
1505 ASM_REWRITE_TAC[EXP_ZERO; COND_RAND; COND_RATOR] THEN
1506 ASM_SIMP_TAC[LE_0; DIVIDES_1; ARITH; index_def; DIVIDES_ZERO] THEN
1507 SIMP_TAC[CONJUNCT1 LE; COND_ID] THEN
1508 ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[EXP_ONE; DIVIDES_1] THEN
1509 COND_CASES_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1510 SUBGOAL_THEN `2 <= p` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1511 MP_TAC(ISPECL [`n:num`; `p:num`] FACTORIZATION_INDEX) THEN
1512 ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `a:num` THEN STRIP_TAC THEN
1513 SUBGOAL_THEN `!k. p EXP k divides n <=> k <= a` ASSUME_TAC THENL
1514 [GEN_TAC THEN EQ_TAC THENL [ASM_MESON_TAC[NOT_LE]; ALL_TAC] THEN
1515 DISCH_TAC THEN TRANS_TAC DIVIDES_TRANS `p EXP a` THEN
1516 ASM_SIMP_TAC[DIVIDES_EXP_LE];
1517 ASM_REWRITE_TAC[GSYM numseg; CARD_NUMSEG_1]]);;
1519 let LE_INDEX = prove
1520 (`!n p k. k <= index p n <=> (n = 0 \/ p = 1 ==> k = 0) /\ p EXP k divides n`,
1521 REPEAT GEN_TAC THEN REWRITE_TAC[PRIMEPOW_DIVIDES_INDEX] THEN
1522 ASM_CASES_TAC `n = 0` THEN
1523 ASM_REWRITE_TAC[INDEX_0; CONJUNCT1 LE] THEN
1524 ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[] THEN
1525 REWRITE_TAC[index_def; ARITH; CONJUNCT1 LE]);;
1528 (`!p. index p 1 = 0`,
1529 GEN_TAC THEN REWRITE_TAC[index_def; ARITH] THEN COND_CASES_TAC THEN
1530 REWRITE_TAC[DIVIDES_ONE; EXP_EQ_1] THEN
1531 ASM_SIMP_TAC[ARITH_RULE `~(p <= 1) ==> ~(p = 1)`;
1532 ARITH_RULE `~(1 <= j /\ j = 0)`;
1533 EMPTY_GSPEC; CARD_CLAUSES]);;
1535 let INDEX_MUL = prove
1536 (`!m n. prime p /\ ~(m = 0) /\ ~(n = 0)
1537 ==> index p (m * n) = index p m + index p n`,
1538 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM LE_ANTISYM] THEN
1539 SUBGOAL_THEN `~(p = 1)` ASSUME_TAC THENL
1540 [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
1542 [MATCH_MP_TAC(MESON[LE_REFL]
1543 `(!k:num. k <= m ==> k <= n) ==> m <= n`) THEN
1544 MP_TAC(SPEC `p:num` PRIMEPOW_DIVIDES_PROD) THEN
1545 ASM_REWRITE_TAC[LE_INDEX; MULT_EQ_0] THEN ASM_MESON_TAC[LE_ADD2; LE_INDEX];
1546 ASM_REWRITE_TAC[LE_INDEX; MULT_EQ_0; EXP_ADD] THEN
1547 MATCH_MP_TAC DIVIDES_MUL2 THEN ASM_MESON_TAC[LE_INDEX; LE_REFL]]);;
1549 let INDEX_EXP = prove
1550 (`!p n k. prime p ==> index p (n EXP k) = k * index p n`,
1551 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
1552 GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
1553 ASM_REWRITE_TAC[EXP_ZERO; INDEX_0; COND_RAND; COND_RATOR; INDEX_1;
1554 MULT_CLAUSES; COND_ID] THEN
1556 ASM_SIMP_TAC[INDEX_MUL; EXP_EQ_0; EXP; INDEX_1; MULT_CLAUSES] THEN
1559 let INDEX_FACT = prove
1560 (`!p n. prime p ==> index p (FACT n) = nsum(1..n) (\m. index p m)`,
1561 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
1562 INDUCT_TAC THEN REWRITE_TAC[FACT; NSUM_CLAUSES_NUMSEG; INDEX_1; ARITH] THEN
1563 ASM_SIMP_TAC[INDEX_MUL; NOT_SUC; FACT_NZ] THEN ARITH_TAC);;
1565 let INDEX_FACT_ALT = prove
1567 ==> index p (FACT n) =
1568 nsum {j | 1 <= j /\ p EXP j <= n} (\j. n DIV (p EXP j))`,
1569 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[INDEX_FACT] THEN
1570 SUBGOAL_THEN `~(p = 0) /\ ~(p = 1) /\ 2 <= p /\ ~(p <= 1)`
1571 STRIP_ASSUME_TAC THENL
1572 [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC; ALL_TAC] THEN
1573 ASM_SIMP_TAC[index_def; LE_1] THEN
1575 `nsum(1..n) (\m. nsum {j | 1 <= j /\ p EXP j <= n}
1576 (\j. if p EXP j divides m then 1 else 0))` THEN
1578 [MATCH_MP_TAC NSUM_EQ_NUMSEG THEN X_GEN_TAC `m:num` THEN STRIP_TAC THEN
1579 ASM_REWRITE_TAC[GSYM NSUM_RESTRICT_SET; IN_ELIM_THM] THEN
1580 ASM_SIMP_TAC[NSUM_CONST; FINITE_INDICES; LE_1; MULT_CLAUSES] THEN
1581 AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
1582 ASM_MESON_TAC[DIVIDES_LE; LE_1; LE_TRANS];
1583 W(MP_TAC o PART_MATCH (lhs o rand) NSUM_SWAP o lhand o snd) THEN
1584 ASM_SIMP_TAC[FINITE_NUMSEG; FINITE_EXP_LE] THEN DISCH_THEN(K ALL_TAC) THEN
1585 MATCH_MP_TAC NSUM_EQ THEN X_GEN_TAC `j:num` THEN
1586 REWRITE_TAC[IN_ELIM_THM; GSYM NSUM_RESTRICT_SET] THEN STRIP_TAC THEN
1587 ASM_SIMP_TAC[NSUM_CONST; FINITE_NUMSEG; FINITE_RESTRICT; MULT_CLAUSES] THEN
1588 SUBGOAL_THEN `{m | m IN 1..n /\ p EXP j divides m} =
1589 IMAGE (\q. p EXP j * q) (1..(n DIV p EXP j))`
1590 (fun th -> ASM_SIMP_TAC[CARD_IMAGE_INJ; FINITE_NUMSEG; EQ_MULT_LCANCEL;
1591 th; EXP_EQ_0; PRIME_IMP_NZ; CARD_NUMSEG_1]) THEN
1592 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_NUMSEG; IN_ELIM_THM; divides] THEN
1593 X_GEN_TAC `d:num` THEN REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
1594 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `q:num` THEN
1595 ASM_CASES_TAC `d = p EXP j * q` THEN ASM_REWRITE_TAC[] THEN
1596 ASM_SIMP_TAC[LE_RDIV_EQ; EXP_EQ_0; PRIME_IMP_NZ; MULT_EQ_0;
1597 ARITH_RULE `1 <= x <=> ~(x = 0)`]]);;
1599 let INDEX_FACT_UNBOUNDED = prove
1601 ==> index p (FACT n) = nsum {j | 1 <= j} (\j. n DIV (p EXP j))`,
1602 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[INDEX_FACT_ALT] THEN
1603 CONV_TAC SYM_CONV THEN MATCH_MP_TAC NSUM_SUPERSET THEN
1604 ASM_SIMP_TAC[SUBSET; IN_ELIM_THM; IMP_CONJ; DIV_EQ_0; EXP_EQ_0;
1605 PRIME_IMP_NZ; NOT_LE]);;
1607 let PRIMEPOW_DIVIDES_FACT = prove
1609 ==> (p EXP k divides FACT n <=>
1610 k <= nsum {j | 1 <= j /\ p EXP j <= n} (\j. n DIV (p EXP j)))`,
1611 SIMP_TAC[PRIMEPOW_DIVIDES_INDEX; INDEX_FACT_ALT; FACT_NZ] THEN
1612 MESON_TAC[PRIME_1]);;
1614 let INDEX_REFL = prove
1615 (`!n. index n n = if n <= 1 then 0 else 1`,
1616 GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[index_def] THEN
1617 ASM_CASES_TAC `n = 0` THENL [ASM_ARITH_TAC; ASM_REWRITE_TAC[]] THEN
1618 ONCE_REWRITE_TAC[MESON[EXP_1] `a divides b <=> a divides b EXP 1`] THEN
1619 ASM_CASES_TAC `2 <= n` THENL [ALL_TAC; ASM_ARITH_TAC] THEN
1620 ASM_SIMP_TAC[DIVIDES_EXP_LE; GSYM numseg; CARD_NUMSEG_1]);;
1622 let INDEX_EQ_0 = prove
1623 (`!p n. index p n = 0 <=> n = 0 \/ p = 1 \/ ~(p divides n)`,
1625 GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 0 <=> ~(1 <= n)`] THEN
1626 REWRITE_TAC[LE_INDEX; EXP_1; ARITH] THEN MESON_TAC[]);;
1628 let INDEX_TRIVIAL_BOUND = prove
1629 (`!n p. index p n <= n`,
1631 MP_TAC(ISPECL [`n:num`; `p:num`; `n:num`] PRIMEPOW_DIVIDES_INDEX) THEN
1632 REWRITE_TAC[index_def] THEN COND_CASES_TAC THEN REWRITE_TAC[LE_0] THEN
1633 RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM; NOT_LE]) THEN
1634 ASM_SIMP_TAC[ARITH_RULE `1 < p ==> ~(p = 1)`] THEN
1635 DISCH_THEN(ASSUME_TAC o SYM) THEN
1636 MATCH_MP_TAC(ARITH_RULE `~(m:num <= n) ==> n <= m`) THEN
1637 ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
1638 ASM_REWRITE_TAC[NOT_LE] THEN
1639 MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `2 EXP n` THEN
1640 REWRITE_TAC[LT_POW2_REFL] THEN
1641 MATCH_MP_TAC EXP_MONO_LE_IMP THEN ASM_ARITH_TAC);;
1643 let INDEX_DECOMPOSITION = prove
1644 (`!n p. ?m. p EXP (index p n) * m = n /\ (n = 0 \/ p = 1 \/ ~(p divides m))`,
1646 MP_TAC(SPECL [`n:num`; `p:num`; `index p n`] LE_INDEX) THEN
1647 REWRITE_TAC[LE_REFL] THEN STRIP_TAC THEN
1648 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [divides]) THEN
1649 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
1650 DISCH_THEN(ASSUME_TAC o SYM) THEN ASM_REWRITE_TAC[] THEN
1651 MP_TAC(SPECL [`n:num`; `p:num`; `index p n + 1`] LE_INDEX) THEN
1652 REWRITE_TAC[ADD_EQ_0; ARITH_EQ; ARITH_RULE `~(n + 1 <= n)`] THEN
1653 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
1654 ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[] THEN
1655 REWRITE_TAC[EXP_ADD; EXP_1; CONTRAPOS_THM] THEN
1656 FIRST_X_ASSUM(MP_TAC o SYM) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1659 let INDEX_DECOMPOSITION_PRIME = prove
1660 (`!n p. prime p ==> ?m. p EXP (index p n) * m = n /\ (n = 0 \/ coprime(p,m))`,
1661 REPEAT STRIP_TAC THEN
1662 MP_TAC(SPECL [`n:num`; `p:num`] INDEX_DECOMPOSITION) THEN
1663 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
1664 ASM_CASES_TAC `p = 1` THENL [ASM_MESON_TAC[PRIME_1]; ASM_REWRITE_TAC[]] THEN
1665 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
1666 ASM_MESON_TAC[PRIME_COPRIME_STRONG]);;
1668 (* ------------------------------------------------------------------------- *)
1669 (* Least common multiples. *)
1670 (* ------------------------------------------------------------------------- *)
1672 let lcm = new_definition
1673 `lcm(m,n) = if m * n = 0 then 0 else (m * n) DIV gcd(m,n)`;;
1675 let LCM_DIVIDES = prove
1676 (`!m n d. lcm(m,n) divides d <=> m divides d /\ n divides d`,
1677 REPEAT GEN_TAC THEN REWRITE_TAC[lcm] THEN
1678 ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
1679 REWRITE_TAC[DIVIDES_ZERO] THENL [MESON_TAC[DIVIDES_0]; ALL_TAC] THEN
1680 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
1681 REWRITE_TAC[DIVIDES_ZERO] THENL [MESON_TAC[DIVIDES_0]; ALL_TAC] THEN
1682 ASM_REWRITE_TAC[MULT_EQ_0] THEN
1683 TRANS_TAC EQ_TRANS `(m * n) divides (gcd(m,n) * d)` THEN CONJ_TAC THENL
1684 [REWRITE_TAC[divides] THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
1685 X_GEN_TAC `r:num` THEN TRANS_TAC EQ_TRANS
1686 `gcd(m,n) * d = gcd(m,n) * ((m * n) DIV gcd (m,n) * r)` THEN
1688 [ASM_REWRITE_TAC[EQ_MULT_LCANCEL; GCD_ZERO];
1689 AP_TERM_TAC THEN REWRITE_TAC[MULT_ASSOC] THEN
1690 AP_THM_TAC THEN AP_TERM_TAC THEN
1691 GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
1692 REWRITE_TAC[GSYM DIVIDES_DIV_MULT]];
1694 REPEAT(POP_ASSUM MP_TAC) THEN NUMBER_TAC);;
1697 (`!m n. m divides lcm(m,n) /\
1698 n divides lcm(m,n) /\
1699 (!d. m divides d /\ n divides d ==> lcm(m,n) divides d)`,
1700 REPEAT GEN_TAC THEN SIMP_TAC[LCM_DIVIDES] THEN REWRITE_TAC[lcm] THEN
1701 MAP_EVERY ASM_CASES_TAC [`m = 0`; `n = 0`] THEN
1702 ASM_REWRITE_TAC[DIVIDES_0; MULT_CLAUSES] THEN
1703 ASM_REWRITE_TAC[DIVIDES_ZERO; DIVIDES_REFL; MULT_EQ_0] THEN
1704 CONJ_TAC THEN REWRITE_TAC[divides] THENL
1705 [EXISTS_TAC `n DIV gcd(m,n)`; EXISTS_TAC `m DIV gcd(m,n)`] THEN
1706 MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
1707 ASM_SIMP_TAC[GCD_ZERO; LE_1; ADD_CLAUSES] THEN CONV_TAC SYM_CONV THENL
1708 [ALL_TAC; GEN_REWRITE_TAC RAND_CONV [MULT_SYM]] THEN
1709 REWRITE_TAC[GSYM MULT_ASSOC] THEN AP_TERM_TAC THEN
1710 REWRITE_TAC[GSYM DIVIDES_DIV_MULT] THEN
1711 REPEAT(POP_ASSUM MP_TAC) THEN NUMBER_TAC);;
1713 let DIVIDES_LCM = prove
1714 (`!m n r. r divides m \/ r divides n
1715 ==> r divides lcm(m,n)`,
1716 REPEAT STRIP_TAC THEN FIRST_X_ASSUM
1717 (MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] DIVIDES_TRANS)) THEN
1718 ASM_MESON_TAC[LCM]);;
1721 (`(!n. lcm(0,n) = 0) /\ (!n. lcm(n,0) = 0)`,
1722 REWRITE_TAC[lcm; MULT_CLAUSES] THEN ARITH_TAC);;
1725 (`(!n. lcm(1,n) = n) /\ (!n. lcm(n,1) = n)`,
1726 SIMP_TAC[lcm; MULT_CLAUSES; GCD_1; DIV_1] THEN MESON_TAC[]);;
1729 (`!m n. lcm(m,n) = lcm(n,m)`,
1730 REWRITE_TAC[lcm; MULT_SYM; GCD_SYM; ARITH_RULE `MAX m n = MAX n m`]);;
1732 let DIVIDES_LCM_GCD = prove
1733 (`!m n d. d divides lcm(m,n) <=> d * gcd(m,n) divides m * n`,
1734 REPEAT GEN_TAC THEN REWRITE_TAC[lcm] THEN
1735 COND_CASES_TAC THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
1736 RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
1737 MP_TAC(NUMBER_RULE `gcd(m,n) divides m * n`) THEN
1738 SIMP_TAC[divides; LEFT_IMP_EXISTS_THM] THEN REWRITE_TAC[GSYM divides] THEN
1739 REPEAT STRIP_TAC THEN MP_TAC(SPECL [`m:num`; `n:num`] GCD_ZERO) THEN
1740 ASM_SIMP_TAC[DIV_MULT] THEN CONV_TAC NUMBER_RULE);;
1742 let PRIMEPOW_DIVIDES_LCM = prove
1745 ==> (p EXP k divides lcm(m,n) <=>
1746 p EXP k divides m \/ p EXP k divides n)`,
1747 REPEAT STRIP_TAC THEN EQ_TAC THENL [STRIP_TAC; MESON_TAC[DIVIDES_LCM]] THEN
1748 ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[LCM_0; DIVIDES_0] THEN
1749 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[LCM_0; DIVIDES_0] THEN
1750 MP_TAC(SPECL [`n:num`; `p:num`] FACTORIZATION_INDEX) THEN
1751 MP_TAC(SPECL [`m:num`; `p:num`] FACTORIZATION_INDEX) THEN
1752 ASM_SIMP_TAC[PRIME_GE_2; LEFT_IMP_EXISTS_THM; divides;
1753 LEFT_AND_EXISTS_THM] THEN
1754 MAP_EVERY X_GEN_TAC [`a:num`; `q:num`] THEN STRIP_TAC THEN
1755 MAP_EVERY X_GEN_TAC [`b:num`; `r:num`] THEN STRIP_TAC THEN
1756 REWRITE_TAC[GSYM divides] THEN
1757 UNDISCH_TAC `p EXP k divides lcm (m,n)` THEN
1758 ASM_REWRITE_TAC[DIVIDES_LCM_GCD] THEN
1760 `gcd(p EXP a * q,p EXP b * r) =
1761 p EXP (MIN a b) * gcd(p EXP (a - MIN a b) * q,p EXP (b - MIN a b) * r)`
1763 [REWRITE_TAC[GSYM GCD_LMUL; MULT_ASSOC; GSYM EXP_ADD] THEN
1764 AP_TERM_TAC THEN BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1765 AP_TERM_TAC THEN ARITH_TAC;
1766 REWRITE_TAC[MULT_ASSOC; GSYM EXP_ADD]] THEN
1768 MATCH_MP (NUMBER_RULE `a * b divides c ==> a divides c`)) THEN
1769 REWRITE_TAC[ARITH_RULE `((a * b) * c) * d:num = (a * c) * b * d`] THEN
1770 REWRITE_TAC[GSYM EXP_ADD] THEN
1771 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
1772 (ONCE_REWRITE_RULE[MULT_SYM] COPRIME_EXP_DIVPROD))) THEN
1774 [MATCH_MP_TAC COPRIME_MUL THEN CONJ_TAC THEN
1775 MATCH_MP_TAC(MESON[PRIME_COPRIME_STRONG]
1776 `prime p /\ ~(p divides n) ==> coprime(p,n)`) THEN
1777 ASM_REWRITE_TAC[divides] THEN STRIP_TAC THENL
1778 [UNDISCH_TAC `!l. a < l ==> ~(?x. m = p EXP l * x)` THEN
1779 DISCH_THEN(MP_TAC o SPEC `a + 1`);
1780 UNDISCH_TAC `!l. b < l ==> ~(?x. n = p EXP l * x)` THEN
1781 DISCH_THEN(MP_TAC o SPEC `b + 1`)] THEN
1782 ASM_REWRITE_TAC[ARITH_RULE `a < a + 1`; EXP_ADD; EXP_1] THEN
1784 ASM_SIMP_TAC[DIVIDES_EXP_LE; PRIME_GE_2] THEN
1785 DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1786 `k + MIN a b <= a + b ==> k <= a \/ k <= b`)) THEN
1787 MATCH_MP_TAC MONO_OR THEN REPEAT STRIP_TAC THEN
1788 MATCH_MP_TAC DIVIDES_RMUL THEN ASM_SIMP_TAC[DIVIDES_EXP_LE; PRIME_GE_2]]);;
1790 let LCM_ZERO = prove
1791 (`!m n. lcm(m,n) = 0 <=> m = 0 \/ n = 0`,
1792 REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [MULTIPLES_EQ] THEN
1793 REWRITE_TAC[LCM_DIVIDES; DIVIDES_ZERO] THEN
1794 MAP_EVERY ASM_CASES_TAC [`m = 0`; `n = 0`] THEN
1795 ASM_REWRITE_TAC[DIVIDES_ZERO] THEN
1796 ASM_MESON_TAC[DIVIDES_REFL; MULT_EQ_0; DIVIDES_LMUL; DIVIDES_RMUL]);;
1798 let LCM_ASSOC = prove
1799 (`!m n p. lcm(m,lcm(n,p)) = lcm(lcm(m,n),p)`,
1800 REPEAT GEN_TAC THEN REWRITE_TAC[MULTIPLES_EQ] THEN
1801 REWRITE_TAC[LCM_DIVIDES] THEN X_GEN_TAC `q:num` THEN
1802 REWRITE_TAC[LCM_ZERO] THEN CONV_TAC TAUT);;
1804 let LCM_REFL = prove
1805 (`!n. lcm(n,n) = n`,
1806 REWRITE_TAC[lcm; GCD_REFL; MULT_EQ_0; ARITH_RULE `MAX n n = n`] THEN
1807 SIMP_TAC[DIV_MULT] THEN MESON_TAC[]);;
1809 let LCM_MULTIPLE = prove
1810 (`!a b. lcm(b,a * b) = a * b`,
1811 REWRITE_TAC[MULTIPLES_EQ; LCM_DIVIDES] THEN NUMBER_TAC);;
1813 let LCM_GCD_DISTRIB = prove
1814 (`!a b c. lcm(a,gcd(b,c)) = gcd(lcm(a,b),lcm(a,c))`,
1815 REWRITE_TAC[PRIMEPOW_DIVISORS_EQ] THEN
1816 SIMP_TAC[PRIMEPOW_DIVIDES_LCM; DIVIDES_GCD] THEN CONV_TAC TAUT);;
1818 let GCD_LCM_DISTRIB = prove
1819 (`!a b c. gcd(a,lcm(b,c)) = lcm(gcd(a,b),gcd(a,c))`,
1820 REWRITE_TAC[PRIMEPOW_DIVISORS_EQ] THEN
1821 SIMP_TAC[PRIMEPOW_DIVIDES_LCM; DIVIDES_GCD] THEN CONV_TAC TAUT);;
1823 let LCM_UNIQUE = prove
1825 m divides d /\ n divides d /\
1826 (!e. m divides e /\ n divides e ==> d divides e) <=>
1828 REWRITE_TAC[MULTIPLES_EQ; LCM_DIVIDES] THEN
1829 MESON_TAC[DIVIDES_REFL; DIVIDES_TRANS]);;
1832 (`!x y u v. (!d. x divides d /\ y divides d <=> u divides d /\ v divides d)
1833 ==> lcm(x,y) = lcm(u,v)`,
1834 SIMP_TAC[MULTIPLES_EQ; LCM_DIVIDES]);;
1836 let LCM_LMUL = prove
1837 (`!a b c. lcm(c * a,c * b) = c * lcm(a,b)`,
1838 REPEAT GEN_TAC THEN ASM_CASES_TAC `c = 0` THEN
1839 ASM_REWRITE_TAC[MULT_CLAUSES; LCM_0] THEN
1840 ASM_REWRITE_TAC[lcm; GCD_LMUL; MULT_EQ_0; DISJ_ACI] THEN
1841 COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
1842 RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN
1843 ASM_SIMP_TAC[GSYM MULT_ASSOC; DIV_MULT2; MULT_EQ_0; GCD_ZERO] THEN
1844 MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
1845 ASM_SIMP_TAC[ADD_CLAUSES; LE_1; GCD_ZERO] THEN
1846 ONCE_REWRITE_TAC[ARITH_RULE
1847 `a * c * b:num = (c * d) * g <=> c * d * g = c * a * b`] THEN
1848 AP_TERM_TAC THEN REWRITE_TAC[GSYM DIVIDES_DIV_MULT] THEN
1849 CONV_TAC NUMBER_RULE);;
1851 let LCM_RMUL = prove
1852 (`!a b c. lcm(a * c,b * c) = c * lcm(a,b)`,
1853 MESON_TAC[LCM_LMUL; MULT_SYM]);;
1856 (`!n a b. lcm(a EXP n,b EXP n) = lcm(a,b) EXP n`,
1857 REPEAT GEN_TAC THEN REWRITE_TAC[lcm] THEN
1858 REWRITE_TAC[MULT_EQ_0; EXP_EQ_0] THEN
1859 ASM_CASES_TAC `n = 0` THEN
1860 ASM_REWRITE_TAC[EXP; GCD_REFL; DIV_1; MULT_CLAUSES] THEN
1861 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
1862 [ASM_MESON_TAC[num_CASES; EXP_0]; ALL_TAC] THEN
1863 RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN
1864 REWRITE_TAC[GCD_EXP; GSYM MULT_EXP] THEN
1865 MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
1866 ASM_SIMP_TAC[ADD_CLAUSES; LE_1; GCD_ZERO; EXP_EQ_0] THEN
1867 REWRITE_TAC[GSYM MULT_EXP] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1868 CONV_TAC SYM_CONV THEN REWRITE_TAC[GSYM DIVIDES_DIV_MULT] THEN
1869 CONV_TAC NUMBER_RULE);;
1871 (* ------------------------------------------------------------------------- *)
1872 (* Induction principle for multiplicative functions etc. *)
1873 (* ------------------------------------------------------------------------- *)
1875 let INDUCT_COPRIME = prove
1876 (`!P. (!a b. 1 < a /\ 1 < b /\ coprime(a,b) /\ P a /\ P b ==> P(a * b)) /\
1877 (!p k. prime p ==> P(p EXP k))
1878 ==> !n. 1 < n ==> P n`,
1879 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC num_WF THEN
1880 X_GEN_TAC `n:num` THEN REPEAT STRIP_TAC THEN
1881 FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `1 < n ==> ~(n = 1)`)) THEN
1882 DISCH_THEN(X_CHOOSE_TAC `p:num` o MATCH_MP PRIME_FACTOR) THEN
1883 MP_TAC(SPECL [`n:num`; `p:num`] FACTORIZATION_INDEX) THEN
1884 ASM_SIMP_TAC[PRIME_GE_2; ARITH_RULE `1 < n ==> ~(n = 0)`] THEN
1885 REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM; LEFT_AND_EXISTS_THM] THEN
1886 MAP_EVERY X_GEN_TAC [`k:num`; `m:num`] THEN STRIP_TAC THEN
1887 FIRST_X_ASSUM SUBST_ALL_TAC THEN
1888 ASM_CASES_TAC `m = 1` THEN ASM_SIMP_TAC[MULT_CLAUSES] THEN
1889 FIRST_X_ASSUM(CONJUNCTS_THEN2 MATCH_MP_TAC MP_TAC) THEN
1890 ASM_SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN
1892 `!p. (a /\ b /\ ~p) /\ c /\ (a /\ ~p ==> b ==> d)
1893 ==> a /\ b /\ c /\ d`) THEN
1894 EXISTS_TAC `m = 0` THEN
1895 SUBGOAL_THEN `~(k = 0)` ASSUME_TAC THENL
1896 [DISCH_THEN SUBST_ALL_TAC THEN
1897 FIRST_X_ASSUM(MP_TAC o C MATCH_MP (ARITH_RULE `0 < 1`)) THEN
1898 FIRST_X_ASSUM(MP_TAC o CONJUNCT2) THEN
1899 REWRITE_TAC[EXP; EXP_1; MULT_CLAUSES; divides];
1902 [UNDISCH_TAC `1 < p EXP k * m` THEN
1903 ASM_REWRITE_TAC[ARITH_RULE `1 < x <=> ~(x = 0) /\ ~(x = 1)`] THEN
1904 ASM_REWRITE_TAC[EXP_EQ_0; EXP_EQ_1; MULT_EQ_0; MULT_EQ_1] THEN
1905 FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2 o CONJUNCT1) THEN
1909 [FIRST_X_ASSUM(MP_TAC o C MATCH_MP (ARITH_RULE `k < k + 1`)) THEN
1910 REWRITE_TAC[EXP_ADD; EXP_1; GSYM MULT_ASSOC; EQ_MULT_LCANCEL] THEN
1911 ASM_SIMP_TAC[EXP_EQ_0; PRIME_IMP_NZ; GSYM divides] THEN DISCH_TAC THEN
1912 ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_EXP THEN
1913 ASM_MESON_TAC[PRIME_COPRIME; COPRIME_SYM];
1914 DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
1915 GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `m = 1 * m`] THEN
1916 ASM_REWRITE_TAC[LT_MULT_RCANCEL]]);;
1918 let INDUCT_COPRIME_STRONG = prove
1919 (`!P. (!a b. 1 < a /\ 1 < b /\ coprime(a,b) /\ P a /\ P b ==> P(a * b)) /\
1920 (!p k. prime p /\ ~(k = 0) ==> P(p EXP k))
1921 ==> !n. 1 < n ==> P n`,
1922 GEN_TAC THEN STRIP_TAC THEN
1923 ONCE_REWRITE_TAC[TAUT `a ==> b <=> a ==> a ==> b`] THEN
1924 MATCH_MP_TAC INDUCT_COPRIME THEN CONJ_TAC THENL
1926 MAP_EVERY X_GEN_TAC [`p:num`; `k:num`] THEN ASM_CASES_TAC `k = 0` THEN
1927 ASM_REWRITE_TAC[LT_REFL; EXP] THEN ASM_MESON_TAC[]]);;
1929 (* ------------------------------------------------------------------------- *)
1930 (* A conversion for divisibility. *)
1931 (* ------------------------------------------------------------------------- *)
1934 let pth_0 = SPEC `b:num` DIVIDES_ZERO
1936 (`~(a = 0) ==> (a divides b <=> (b MOD a = 0))`,
1937 REWRITE_TAC[DIVIDES_MOD])
1938 and a_tm = `a:num` and b_tm = `b:num` and zero_tm = `0`
1939 and dest_divides = dest_binop `(divides)` in
1941 let a,b = dest_divides tm in
1943 CONV_RULE (RAND_CONV NUM_EQ_CONV) (INST [b,b_tm] pth_0)
1945 let th1 = INST [a,a_tm; b,b_tm] pth_1 in
1946 let th2 = MP th1 (EQF_ELIM(NUM_EQ_CONV(rand(lhand(concl th1))))) in
1947 CONV_RULE (RAND_CONV (LAND_CONV NUM_MOD_CONV THENC NUM_EQ_CONV)) th2;;
1949 (* ------------------------------------------------------------------------- *)
1950 (* A conversion for coprimality. *)
1951 (* ------------------------------------------------------------------------- *)
1954 let pth_yes_l = prove
1955 (`(m * x = n * y + 1) ==> (coprime(m,n) <=> T)`,
1956 MESON_TAC[coprime; DIVIDES_RMUL; DIVIDES_ADD_REVR; DIVIDES_ONE])
1957 and pth_yes_r = prove
1958 (`(m * x = n * y + 1) ==> (coprime(n,m) <=> T)`,
1959 MESON_TAC[coprime; DIVIDES_RMUL; DIVIDES_ADD_REVR; DIVIDES_ONE])
1961 (`(m = x * d) /\ (n = y * d) /\ ~(d = 1) ==> (coprime(m,n) <=> F)`,
1962 REWRITE_TAC[coprime; divides] THEN MESON_TAC[MULT_AC])
1964 (`coprime(0,0) <=> F`,
1965 MESON_TAC[coprime; DIVIDES_REFL; NUM_REDUCE_CONV `1 = 0`])
1966 and m_tm = `m:num` and n_tm = `n:num`
1967 and x_tm = `x:num` and y_tm = `y:num`
1968 and d_tm = `d:num` and coprime_tm = `coprime` in
1969 let rec bezout (m,n) =
1970 if m =/ Int 0 then (Int 0,Int 1) else if n =/ Int 0 then (Int 1,Int 0)
1971 else if m <=/ n then
1972 let q = quo_num n m and r = mod_num n m in
1973 let (x,y) = bezout(m,r) in
1975 else let (x,y) = bezout(n,m) in (y,x) in
1977 let pop,ptm = dest_comb tm in
1978 if pop <> coprime_tm then failwith "COPRIME_CONV" else
1979 let l,r = dest_pair ptm in
1980 let m = dest_numeral l and n = dest_numeral r in
1981 if m =/ Int 0 & n =/ Int 0 then pth_oo else
1982 let (x,y) = bezout(m,n) in
1983 let d = x */ m +/ y */ n in
1987 INST [l,m_tm; r,n_tm; mk_numeral x,x_tm;
1988 mk_numeral(minus_num y),y_tm] pth_yes_l
1990 INST [r,m_tm; l,n_tm; mk_numeral(minus_num x),y_tm;
1991 mk_numeral y,x_tm] pth_yes_r
1993 INST [l,m_tm; r,n_tm; mk_numeral d,d_tm;
1994 mk_numeral(m // d),x_tm; mk_numeral(n // d),y_tm] pth_no in
1995 MP th (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th))));;
1997 (* ------------------------------------------------------------------------- *)
1998 (* More general (slightly less efficiently coded) GCD_CONV, and LCM_CONV. *)
1999 (* ------------------------------------------------------------------------- *)
2002 let pth0 = prove(`gcd(0,0) = 0`,REWRITE_TAC[GCD_0]) in
2005 (m * x = n * y + d) /\ (m = m' * d) /\ (n = n' * d) ==> (gcd(m,n) = d)`,
2007 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
2008 CONV_TAC(RAND_CONV SYM_CONV) THEN ASM_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
2009 ASM_MESON_TAC[DIVIDES_LMUL; DIVIDES_RMUL;
2010 DIVIDES_ADD_REVR; DIVIDES_REFL]) in
2013 (n * y = m * x + d) /\ (m = m' * d) /\ (n = n' * d) ==> (gcd(m,n) = d)`,
2014 MESON_TAC[pth1; GCD_SYM]) in
2015 let gcd_tm = `gcd` in
2016 let rec bezout (m,n) =
2017 if m =/ Int 0 then (Int 0,Int 1) else if n =/ Int 0 then (Int 1,Int 0)
2018 else if m <=/ n then
2019 let q = quo_num n m and r = mod_num n m in
2020 let (x,y) = bezout(m,r) in
2022 else let (x,y) = bezout(n,m) in (y,x) in
2023 fun tm -> let gt,lr = dest_comb tm in
2024 if gt <> gcd_tm then failwith "GCD_CONV" else
2025 let mtm,ntm = dest_pair lr in
2026 let m = dest_numeral mtm and n = dest_numeral ntm in
2027 if m =/ Int 0 & n =/ Int 0 then pth0 else
2028 let x0,y0 = bezout(m,n) in
2029 let x = abs_num x0 and y = abs_num y0 in
2030 let xtm = mk_numeral x and ytm = mk_numeral y in
2031 let d = abs_num(x */ m -/ y */ n) in
2032 let dtm = mk_numeral d in
2033 let m' = m // d and n' = n // d in
2034 let mtm' = mk_numeral m' and ntm' = mk_numeral n' in
2035 let th = SPECL [mtm;ntm;xtm;ytm;dtm;mtm';ntm']
2036 (if m */ x =/ n */ y +/ d then pth1 else pth2) in
2037 MP th (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th))));;
2040 GEN_REWRITE_CONV I [lcm] THENC
2041 RATOR_CONV(LAND_CONV(LAND_CONV NUM_MULT_CONV THENC NUM_EQ_CONV)) THENC
2042 (GEN_REWRITE_CONV I [CONJUNCT1(SPEC_ALL COND_CLAUSES)] ORELSEC
2043 (GEN_REWRITE_CONV I [CONJUNCT2(SPEC_ALL COND_CLAUSES)] THENC
2044 COMB2_CONV (RAND_CONV NUM_MULT_CONV) GCD_CONV THENC NUM_DIV_CONV));;