Library/prime.ml

   1 (* ========================================================================= *)
   2 (* Basic theory of divisibility, gcd, coprimality and primality (over N).    *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* HOL88 compatibility (since all this is a port of old HOL88 stuff).        *)
   9 (* ------------------------------------------------------------------------- *)
  10
  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]);;
  14
  15 let LESS_ADD_1 = prove
  16  (`!m n. n < m ==> (?p. m = n + (p + 1))`,
  17   REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);;
  18
  19 let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;;
  20
  21 let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
  22
  23 let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;;
  24
  25 let LESS_EQ_0 = prove
  26  (`!n. n <= 0 <=> (n = 0)`,
  27   REWRITE_TAC[LE]);;
  28
  29 let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;;
  30
  31 let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;;
  32
  33 let NOT_EXP_0 = prove
  34  (`!m n. ~((SUC n) EXP m = 0)`,
  35   REWRITE_TAC[EXP_EQ_0; NOT_SUC]);;
  36
  37 let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;;
  38
  39 let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;;
  40
  41 let ZERO_LESS_EXP = prove
  42  (`!m n. 0 < ((SUC n) EXP m)`,
  43   REWRITE_TAC[LT_NZ; NOT_EXP_0]);;
  44
  45 (* ------------------------------------------------------------------------- *)
  46 (* General arithmetic lemmas.                                                *)
  47 (* ------------------------------------------------------------------------- *)
  48
  49 let MULT_FIX = prove(
  50   `!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`,
  51   REPEAT GEN_TAC THEN
  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);;
  58
  59 let LESS_EQ_MULT = prove(
  60   `!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`,
  61   REPEAT GEN_TAC THEN
  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]);;
  65
  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);;
  74
  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]);;
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* Properties of the exponential function.                                   *)
  82 (* ------------------------------------------------------------------------- *)
  83
  84 let EXP_0 = prove
  85  (`!n. 0 EXP (SUC n) = 0`,
  86   REWRITE_TAC[EXP; MULT_CLAUSES]);;
  87
  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]);;
  91
  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]);;
  95
  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]);;
  99
 100 let EXP_EXP = prove
 101  (`!x m n. (x EXP m) EXP n = x EXP (m * n)`,
 102   REWRITE_TAC[EXP_MULT]);;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere.            *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let DIFF_LEMMA = prove(
 109   `!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`,
 110   REPEAT GEN_TAC THEN
 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);;
 117
 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]);;
 122
 123 let CANCEL_TIMES2 = prove(
 124   `!x y. (2 * x = 2 * y) <=> (x = y)`,
 125   REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);;
 126
 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]);;
 134
 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]);;
 146
 147 let DIFF_SQUARE = prove(
 148   `!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`,
 149   REPEAT GEN_TAC THEN
 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]);;
 161
 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]);;
 166
 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]);;
 176
 177 let EXP_4 = prove(
 178   `!n. n EXP 4 = (n EXP 2) EXP 2`,
 179   GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN
 180   REWRITE_TAC[ARITH]);;
 181
 182 (* ------------------------------------------------------------------------- *)
 183 (* Elementary theory of divisibility                                         *)
 184 (* ------------------------------------------------------------------------- *)
 185
 186 let DIVIDES_0 = prove
 187  (`!x. x divides 0`,
 188   NUMBER_TAC);;
 189
 190 let DIVIDES_ZERO = prove
 191  (`!x. 0 divides x <=> (x = 0)`,
 192   NUMBER_TAC);;
 193
 194 let DIVIDES_1 = prove
 195  (`!x. 1 divides x`,
 196   NUMBER_TAC);;
 197
 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);;
 204
 205 let DIVIDES_REFL = prove
 206  (`!x. x divides x`,
 207   NUMBER_TAC);;
 208
 209 let DIVIDES_TRANS = prove
 210  (`!a b c. a divides b /\ b divides c ==> a divides c`,
 211   NUMBER_TAC);;
 212
 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]]);;
 223
 224 let DIVIDES_ADD = prove
 225  (`!d a b. d divides a /\ d divides b ==> d divides (a + b)`,
 226   NUMBER_TAC);;
 227
 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
 234   REFL_TAC);;
 235
 236 let DIVIDES_LMUL = prove
 237  (`!d a x. d divides a ==> d divides (x * a)`,
 238   NUMBER_TAC);;
 239
 240 let DIVIDES_RMUL = prove
 241  (`!d a x. d divides a ==> d divides (a * x)`,
 242   NUMBER_TAC);;
 243
 244 let DIVIDES_ADD_REVR = prove
 245  (`!d a b. d divides a /\ d divides (a + b) ==> d divides b`,
 246   NUMBER_TAC);;
 247
 248 let DIVIDES_ADD_REVL = prove
 249  (`!d a b. d divides b /\ d divides (a + b) ==> d divides a`,
 250   NUMBER_TAC);;
 251
 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);;
 260
 261 let DIVIDES_MUL_L = prove
 262  (`!a b c. a divides b ==> (c * a) divides (c * b)`,
 263   NUMBER_TAC);;
 264
 265 let DIVIDES_MUL_R = prove
 266  (`!a b c. a divides b ==> (a * c) divides (b * c)`,
 267   NUMBER_TAC);;
 268
 269 let DIVIDES_LMUL2 = prove
 270  (`!d a x. (x * d) divides a ==> d divides a`,
 271   NUMBER_TAC);;
 272
 273 let DIVIDES_RMUL2 = prove
 274  (`!d a x. (d * x) divides a ==> d divides a`,
 275   NUMBER_TAC);;
 276
 277 let DIVIDES_CMUL2 = prove
 278  (`!a b c. (c * a) divides (c * b) /\ ~(c = 0) ==> a divides b`,
 279   NUMBER_TAC);;
 280
 281 let DIVIDES_LMUL2_EQ = prove
 282  (`!a b c. ~(c = 0) ==> ((c * a) divides (c * b) <=> a divides b)`,
 283   NUMBER_TAC);;
 284
 285 let DIVIDES_RMUL2_EQ = prove
 286  (`!a b c. ~(c = 0) ==> ((a * c) divides (b * c) <=> a divides b)`,
 287   NUMBER_TAC);;
 288
 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);;
 294
 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);;
 301
 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]);;
 311
 312 let DIVIDES_MUL2 = prove
 313  (`!a b c d. a divides b /\ c divides d ==> (a * c) divides (b * d)`,
 314   NUMBER_TAC);;
 315
 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);;
 321
 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);;
 325
 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]);;
 332
 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]);;
 340
 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]]);;
 356
 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]]);;
 361
 362 let DIVIDES_2 = prove(
 363   `!n. 2 divides n <=> EVEN(n)`,
 364   REWRITE_TAC[divides; EVEN_EXISTS]);;
 365
 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]);;
 369
 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]);;
 373
 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]);;
 380
 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]]);;
 390
 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]);;
 396
 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
 401   SET_TAC[]);;
 402
 403 let DIVIDES_DIVIDES_DIV = prove
 404  (`!n d. 1 <= n /\ d divides n
 405          ==> (e divides (n DIV d) <=> (d * e) divides n)`,
 406   REPEAT GEN_TAC THEN
 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]]);;
 413
 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]);;
 418
 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]);;
 423
 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]);;
 430
 431 (* ------------------------------------------------------------------------- *)
 432 (* The Bezout theorem is a bit ugly for N; it'd be easier for Z              *)
 433 (* ------------------------------------------------------------------------- *)
 434
 435 let IND_EUCLID = prove(
 436   `!P. (!a b. P a b <=> P b a) /\
 437        (!a. P a 0) /\
 438        (!a b. P a b ==> P a (a + b)) ==>
 439          !a b. P a b`,
 440   REPEAT STRIP_TAC THEN
 441   W(fun (asl,w) -> SUBGOAL_THEN `!n a b. (a + b = n) ==> P a b`
 442                    MATCH_MP_TAC) THENL
 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
 469   REWRITE_TAC[]);;
 470
 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]);;
 486
 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]);;
 503
 504 let BEZOUT = prove(
 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]);;
 513
 514 (* ------------------------------------------------------------------------- *)
 515 (* We can get a stronger version with a nonzeroness assumption.              *)
 516 (* ------------------------------------------------------------------------- *)
 517
 518 let BEZOUT_ADD_STRONG = prove
 519  (`!a b. ~(a = 0)
 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
 535    [ALL_TAC;
 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
 552   ANTS_TAC THENL
 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;
 558     ALL_TAC] THEN
 559   DISCH_THEN(fun th ->
 560     MAP_EVERY EXISTS_TAC [`d:num`; `y * (b - 1)`; `(b - 1) * x - d`] THEN
 561     MP_TAC th) 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]);;
 565
 566 (* ------------------------------------------------------------------------- *)
 567 (* Greatest common divisor.                                                  *)
 568 (* ------------------------------------------------------------------------- *)
 569
 570 let GCD = prove
 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))`,
 573   NUMBER_TAC);;
 574
 575 let DIVIDES_GCD = prove
 576  (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`,
 577   NUMBER_TAC);;
 578
 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) <=>
 582            (d = gcd(a,b))`,
 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]);;
 587
 588 let GCD_EQ = prove
 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]);;
 592
 593 let GCD_SYM = prove
 594  (`!a b. gcd(a,b) = gcd(b,a)`,
 595   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM GCD_UNIQUE] THEN NUMBER_TAC);;
 596
 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]);;
 603
 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))`,
 607   REPEAT GEN_TAC THEN
 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[]]);;
 617
 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]);;
 630
 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[]);;
 642
 643 let GCD_RMUL = prove(
 644   `!a b c. gcd(a * c, b * c) = c * gcd(a,b)`,
 645   REPEAT GEN_TAC THEN
 646   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 647   MATCH_ACCEPT_TAC GCD_LMUL);;
 648
 649 let GCD_BEZOUT = prove(
 650   `!a b d. (?x y. ((a * x) - (b * y) = d) \/ ((b * x) - (a * y) = d)) <=>
 651            gcd(a,b) divides 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[]]);;
 661
 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]);;
 667
 668 let GCD_0 = prove
 669   (`(!a. gcd(0,a) = a) /\ (!a. gcd(a,0) = a)`,
 670   MESON_TAC[GCD_UNIQUE; DIVIDES_0; DIVIDES_REFL]);;
 671
 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[]);;
 679
 680 let GCD_REFL = prove(
 681   `!a. gcd(a,a) = a`,
 682   GEN_TAC THEN CONV_TAC SYM_CONV THEN
 683   ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
 684   REWRITE_TAC[DIVIDES_REFL]);;
 685
 686 let GCD_1 = prove
 687   (`(!a. gcd(1,a) = 1) /\ (!a. gcd(a,1) = 1)`,
 688   MESON_TAC[GCD_UNIQUE; DIVIDES_1]);;
 689
 690 let GCD_MULTIPLE = prove(
 691   `!a b. gcd(b,a * b) = b`,
 692   REPEAT GEN_TAC THEN
 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]);;
 697
 698 let GCD_ADD = prove
 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);;
 704
 705 let GCD_SUB = prove
 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]);;
 709
 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]);;
 714
 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]);;
 719
 720 (* ------------------------------------------------------------------------- *)
 721 (* Coprimality                                                               *)
 722 (* ------------------------------------------------------------------------- *)
 723
 724 let coprime = prove
 725  (`coprime(a,b) <=> !d. d divides a /\ d divides b ==> (d = 1)`,
 726   EQ_TAC THENL
 727    [REWRITE_TAC[GSYM DIVIDES_ONE];
 728     DISCH_THEN(MP_TAC o SPEC `gcd(a,b)`) THEN REWRITE_TAC[GCD]] THEN
 729   NUMBER_TAC);;
 730
 731 let COPRIME = prove(
 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
 737   ASM_REWRITE_TAC[]);;
 738
 739 let COPRIME_GCD = prove
 740  (`!a b. coprime(a,b) <=> (gcd(a,b) = 1)`,
 741   REWRITE_TAC[GSYM DIVIDES_ONE] THEN NUMBER_TAC);;
 742
 743 let COPRIME_SYM = prove
 744  (`!a b. coprime(a,b) <=> coprime(b,a)`,
 745   NUMBER_TAC);;
 746
 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]);;
 751
 752 let COPRIME_DIVPROD = prove
 753  (`!d a b. d divides (a * b) /\ coprime(d,a) ==> d divides b`,
 754   NUMBER_TAC);;
 755
 756 let COPRIME_1 = prove
 757  (`!a. coprime(a,1)`,
 758   NUMBER_TAC);;
 759
 760 let GCD_COPRIME = prove
 761  (`!a b a' b'. ~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
 762                ==> coprime(a',b')`,
 763   NUMBER_TAC);;
 764
 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)) /\
 769                 coprime(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[]);;
 779
 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);;
 784
 785 let COPRIME_MUL = prove
 786  (`!d a b. coprime(d,a) /\ coprime(d,b) ==> coprime(d,a * b)`,
 787   NUMBER_TAC);;
 788
 789 let COPRIME_LMUL2 = prove
 790  (`!d a b. coprime(d,a * b) ==> coprime(d,b)`,
 791   NUMBER_TAC);;
 792
 793 let COPRIME_RMUL2 = prove
 794  (`!d a b.  coprime(d,a * b) ==> coprime(d,a)`,
 795   NUMBER_TAC);;
 796
 797 let COPRIME_LMUL = prove
 798  (`!d a b. coprime(a * b,d) <=> coprime(a,d) /\ coprime(b,d)`,
 799   NUMBER_TAC);;
 800
 801 let COPRIME_RMUL = prove
 802  (`!d a b. coprime(d,a * b) <=> coprime(d,a) /\ coprime(d,b)`,
 803   NUMBER_TAC);;
 804
 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[]);;
 811
 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[]);;
 818
 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);;
 825
 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]);;
 829
 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]);;
 833
 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]);;
 837
 838 let COPRIME_REFL = prove
 839  (`!n. coprime(n,n) <=> (n = 1)`,
 840   REWRITE_TAC[COPRIME_GCD; GCD_REFL]);;
 841
 842 let COPRIME_PLUS1 = prove
 843  (`!n. coprime(n + 1,n)`,
 844   NUMBER_TAC);;
 845
 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]);;
 851
 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[]]);;
 880
 881 let GCD_EXP = prove(
 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[]]);;
 893
 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]);;
 918
 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]);;
 930
 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]);;
 934
 935 let DIVIDES_MUL = prove
 936  (`!m n r. m divides r /\ n divides r /\ coprime(m,n) ==> (m * n) divides r`,
 937   NUMBER_TAC);;
 938
 939 (* ------------------------------------------------------------------------- *)
 940 (* A binary form of the Chinese Remainder Theorem.                           *)
 941 (* ------------------------------------------------------------------------- *)
 942
 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)`,
 946   let lemma = prove
 947    (`(?d x y. (d = 1) /\ P x y d) <=> (?x y. P x y 1)`,
 948     MESON_TAC[]) in
 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])
 955   THENL
 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]);;
 968
 969 (* ------------------------------------------------------------------------- *)
 970 (* Primality                                                                 *)
 971 (* ------------------------------------------------------------------------- *)
 972
 973 let prime = new_definition
 974   `prime(p) <=> ~(p = 1) /\ !x. x divides p ==> (x = 1) \/ (x = p)`;;
 975
 976 (* ------------------------------------------------------------------------- *)
 977 (* A few useful theorems about primes                                        *)
 978 (* ------------------------------------------------------------------------- *)
 979
 980 let PRIME_0 = prove(
 981   `~prime(0)`,
 982   REWRITE_TAC[prime] THEN
 983   DISCH_THEN(MP_TAC o SPEC `2` o CONJUNCT2) THEN
 984   REWRITE_TAC[DIVIDES_0; ARITH]);;
 985
 986 let PRIME_1 = prove(
 987   `~prime(1)`,
 988   REWRITE_TAC[prime]);;
 989
 990 let PRIME_2 = prove(
 991   `prime(2)`,
 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[]);;
1000
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]);;
1007
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
1025       ASM_REWRITE_TAC[];
1026       DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `2` THEN
1027       REWRITE_TAC[PRIME_2; DIVIDES_0]]]);;
1028
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]);;
1039
1040 let PRIME_FACTOR_INDUCT = prove
1041  (`!P. P 0 /\ P 1 /\
1042        (!p n. prime p /\ ~(n = 0) /\ P n ==> P(p * n))
1043        ==> !n. 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]);;
1055
1056 (* ------------------------------------------------------------------------- *)
1057 (* Infinitude of primes.                                                     *)
1058 (* ------------------------------------------------------------------------- *)
1059
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)`]]);;
1068
1069 let EUCLID = prove
1070  (`!n. ?p. prime(p) /\ p > n`,
1071   REWRITE_TAC[GT] THEN MESON_TAC[EUCLID_BOUND]);;
1072
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]);;
1077
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]]);;
1084
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[]]);;
1096
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[]);;
1105
1106 let PRIME_COPRIME_STRONG = prove
1107  (`!n p. prime(p) ==> p divides n \/ coprime(p,n)`,
1108   MESON_TAC[PRIME_COPRIME; COPRIME_1]);;
1109
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)`]);;
1117
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]);;
1122
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]);;
1129
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]);;
1136
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]);;
1141
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[]]);;
1152
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]);;
1156
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[]]);;
1165
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);;
1170
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]);;
1176
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]);;
1183
1184 let COPRIME_SOS = prove
1185  (`!x y. coprime(x,y) ==> coprime(x * y,(x EXP 2) + (y EXP 2))`,
1186   NUMBER_TAC);;
1187
1188 let PRIME_IMP_NZ = prove
1189  (`!p. prime(p) ==> ~(p = 0)`,
1190   MESON_TAC[PRIME_0]);;
1191
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]);;
1195
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]);;
1200
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]);;
1204
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]);;
1214
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);;
1220
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[]);;
1226
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`]]);;
1233
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]);;
1238
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]);;
1243
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);;
1252
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]);;
1264
1265 (* ------------------------------------------------------------------------- *)
1266 (* One property of coprimality is easier to prove via prime factors.         *)
1267 (* ------------------------------------------------------------------------- *)
1268
1269 let COPRIME_EXP_DIVPROD = prove
1270  (`!d n a b.
1271       (d EXP n) divides (a * b) /\ coprime(d,a) ==> (d EXP n) divides b`,
1272   MESON_TAC[COPRIME_DIVPROD; COPRIME_EXP; COPRIME_SYM]);;
1273
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]);;
1277
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]);;
1282
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
1293   MESON_TAC[]);;
1294
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
1312     STRIP_TAC THENL
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
1316     (ANTS_TAC THENL
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[]])]);;
1321
1322 (* ------------------------------------------------------------------------- *)
1323 (* More useful lemmas.                                                       *)
1324 (* ------------------------------------------------------------------------- *)
1325
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);;
1344
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]);;
1365
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]);;
1372
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
1377     DISCH_TAC 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
1385     MESON_TAC[LE_ADD];
1386     REWRITE_TAC[LE_EXISTS] THEN STRIP_TAC THEN
1387     ASM_REWRITE_TAC[EXP_ADD] THEN MESON_TAC[DIVIDES_RMUL; DIVIDES_REFL]]);;
1388
1389 let PRIMEPOW_DIVIDES_PROD = prove
1390  (`!p k m n.
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]);;
1397
1398 let COPRIME_DIVISORS = prove
1399  (`!a b d e. d divides a /\ e divides b /\ coprime(a,b) ==> coprime(d,e)`,
1400   NUMBER_TAC);;
1401
1402 let PRIMEPOW_FACTOR = prove
1403  (`!n. 2 <= n
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]);;
1420
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];
1435     ALL_TAC] THEN
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
1443     ASSUME_TAC th) 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]]);;
1466
1467 let PRIMEPOW_DIVISORS_EQ = prove
1468  (`!m n. m = n <=>
1469          !p k. prime p ==> (p EXP k divides m <=> p EXP k divides n)`,
1470   MESON_TAC[DIVIDES_ANTISYM; PRIMEPOW_DIVISORS_DIVIDES]);;
1471
1472 (* ------------------------------------------------------------------------- *)
1473 (* Index of a (usually prime) divisor of a number.                           *)
1474 (* ------------------------------------------------------------------------- *)
1475
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]);;
1484
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]);;
1491
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}`;;
1495
1496 let INDEX_0 = prove
1497  (`!p. index p 0 = 0`,
1498   REWRITE_TAC[index_def]);;
1499
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]]);;
1518
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]);;
1526
1527 let INDEX_1 = prove
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]);;
1534
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
1541   CONJ_TAC THENL
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]]);;
1548
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
1555   INDUCT_TAC THEN
1556   ASM_SIMP_TAC[INDEX_MUL; EXP_EQ_0; EXP; INDEX_1; MULT_CLAUSES] THEN
1557   ARITH_TAC);;
1558
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);;
1564
1565 let INDEX_FACT_ALT = prove
1566  (`!p n. prime p
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
1574   TRANS_TAC EQ_TRANS
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
1577   CONJ_TAC THENL
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)`]]);;
1598
1599 let INDEX_FACT_UNBOUNDED = prove
1600  (`!p n. prime p
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]);;
1606
1607 let PRIMEPOW_DIVIDES_FACT = prove
1608  (`!p n k. prime p
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]);;
1613
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]);;
1621
1622 let INDEX_EQ_0 = prove
1623  (`!p n. index p n = 0 <=> n = 0 \/ p = 1 \/ ~(p divides n)`,
1624   REPEAT GEN_TAC THEN
1625   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 0 <=> ~(1 <= n)`] THEN
1626   REWRITE_TAC[LE_INDEX; EXP_1; ARITH] THEN MESON_TAC[]);;
1627
1628 let INDEX_TRIVIAL_BOUND = prove
1629  (`!n p. index p n <= n`,
1630   REPEAT GEN_TAC THEN
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);;
1642
1643 let INDEX_DECOMPOSITION = prove
1644  (`!n p. ?m. p EXP (index p n) * m = n /\ (n = 0 \/ p = 1 \/ ~(p divides m))`,
1645   REPEAT GEN_TAC THEN
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
1657   NUMBER_TAC);;
1658
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]);;
1667
1668 (* ------------------------------------------------------------------------- *)
1669 (* Least common multiples.                                                   *)
1670 (* ------------------------------------------------------------------------- *)
1671
1672 let lcm = new_definition
1673  `lcm(m,n) = if m * n = 0 then 0 else (m * n) DIV gcd(m,n)`;;
1674
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
1687     CONJ_TAC THENL
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]];
1693     ALL_TAC] THEN
1694    REPEAT(POP_ASSUM MP_TAC) THEN NUMBER_TAC);;
1695
1696 let LCM = prove
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);;
1712
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]);;
1719
1720 let LCM_0 = prove
1721  (`(!n. lcm(0,n) = 0) /\ (!n. lcm(n,0) = 0)`,
1722   REWRITE_TAC[lcm; MULT_CLAUSES] THEN ARITH_TAC);;
1723
1724 let LCM_1 = prove
1725  (`(!n. lcm(1,n) = n) /\ (!n. lcm(n,1) = n)`,
1726   SIMP_TAC[lcm; MULT_CLAUSES; GCD_1; DIV_1] THEN MESON_TAC[]);;
1727
1728 let LCM_SYM = prove
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`]);;
1731
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);;
1741
1742 let PRIMEPOW_DIVIDES_LCM = prove
1743  (`!m n p k.
1744         prime p
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
1759   SUBGOAL_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)`
1762   SUBST1_TAC THENL
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
1767   DISCH_THEN(MP_TAC o
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
1773   ANTS_TAC THENL
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
1783     MESON_TAC[MULT_AC];
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]]);;
1789
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]);;
1797
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);;
1803
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[]);;
1808
1809 let LCM_MULTIPLE = prove
1810  (`!a b. lcm(b,a * b) = a * b`,
1811   REWRITE_TAC[MULTIPLES_EQ; LCM_DIVIDES] THEN NUMBER_TAC);;
1812
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);;
1817
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);;
1822
1823 let LCM_UNIQUE = prove
1824  (`!d m n.
1825        m divides d /\ n divides d /\
1826        (!e. m divides e /\ n divides e ==> d divides e) <=>
1827        d = lcm(m,n)`,
1828   REWRITE_TAC[MULTIPLES_EQ; LCM_DIVIDES] THEN
1829   MESON_TAC[DIVIDES_REFL; DIVIDES_TRANS]);;
1830
1831 let LCM_EQ = prove
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]);;
1835
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);;
1850
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]);;
1854
1855 let LCM_EXP = prove
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);;
1870
1871 (* ------------------------------------------------------------------------- *)
1872 (* Induction principle for multiplicative functions etc.                     *)
1873 (* ------------------------------------------------------------------------- *)
1874
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
1891   MATCH_MP_TAC(TAUT
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];
1900     ALL_TAC] THEN
1901   CONJ_TAC THENL
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
1906     ASM_ARITH_TAC;
1907     ALL_TAC] THEN
1908   CONJ_TAC THENL
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]]);;
1917
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
1925    [ASM_MESON_TAC[];
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[]]);;
1928
1929 (* ------------------------------------------------------------------------- *)
1930 (* A conversion for divisibility.                                            *)
1931 (* ------------------------------------------------------------------------- *)
1932
1933 let DIVIDES_CONV =
1934   let pth_0 = SPEC `b:num` DIVIDES_ZERO
1935   and pth_1 = prove
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
1940   fun tm ->
1941      let a,b = dest_divides tm in
1942      if a = zero_tm then
1943        CONV_RULE (RAND_CONV NUM_EQ_CONV) (INST [b,b_tm] pth_0)
1944      else
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;;
1948
1949 (* ------------------------------------------------------------------------- *)
1950 (* A conversion for coprimality.                                             *)
1951 (* ------------------------------------------------------------------------- *)
1952
1953 let COPRIME_CONV =
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])
1960   and pth_no = prove
1961    (`(m = x * d) /\ (n = y * d) /\ ~(d = 1) ==> (coprime(m,n) <=> F)`,
1962     REWRITE_TAC[coprime; divides] THEN MESON_TAC[MULT_AC])
1963   and pth_oo = prove
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
1974       (x -/ q */ y,y)
1975     else let (x,y) = bezout(n,m) in (y,x) in
1976   fun tm ->
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
1984    let th =
1985      if d =/ Int 1 then
1986        if x >/ Int 0 then
1987           INST [l,m_tm; r,n_tm; mk_numeral x,x_tm;
1988                 mk_numeral(minus_num y),y_tm] pth_yes_l
1989        else
1990           INST [r,m_tm; l,n_tm; mk_numeral(minus_num x),y_tm;
1991                 mk_numeral y,x_tm] pth_yes_r
1992      else
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))));;
1996
1997 (* ------------------------------------------------------------------------- *)
1998 (* More general (slightly less efficiently coded) GCD_CONV, and LCM_CONV.    *)
1999 (* ------------------------------------------------------------------------- *)
2000
2001 let GCD_CONV =
2002   let pth0 = prove(`gcd(0,0) = 0`,REWRITE_TAC[GCD_0]) in
2003   let pth1 = prove
2004    (`!m n x y d m' n'.
2005       (m * x = n * y + d) /\ (m = m' * d) /\ (n = n' * d) ==> (gcd(m,n) = d)`,
2006     REPEAT GEN_TAC THEN
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
2011   let pth2 = prove
2012    (`!m n x y d m' n'.
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
2021       (x -/ q */ y,y)
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))));;
2038
2039 let LCM_CONV =
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));;