Library/integer.ml

   1 (* ========================================================================= *)
   2 (* Basic divisibility notions over the integers.                             *)
   3 (*                                                                           *)
   4 (* This is similar to stuff in Library/prime.ml etc. for natural numbers.    *)
   5 (* ========================================================================= *)
   6
   7 prioritize_int();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Basic properties of divisibility.                                         *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let INT_DIVIDES_REFL = INTEGER_RULE
  14   `!d. d divides d`;;
  15
  16 let INT_DIVIDES_TRANS = INTEGER_RULE
  17   `!x y z. x divides y /\ y divides z ==> x divides z`;;
  18
  19 let INT_DIVIDES_ADD = INTEGER_RULE
  20   `!d a b. d divides a /\ d divides b ==> d divides (a + b)`;;
  21
  22 let INT_DIVIDES_SUB = INTEGER_RULE
  23   `!d a b. d divides a /\ d divides b ==> d divides (a - b)`;;
  24
  25 let INT_DIVIDES_0 = INTEGER_RULE
  26   `!d. d divides &0`;;
  27
  28 let INT_DIVIDES_ZERO = INTEGER_RULE
  29   `!x. &0 divides x <=> x = &0`;;
  30
  31 let INT_DIVIDES_LNEG = INTEGER_RULE
  32   `!d x. (--d) divides x <=> d divides x`;;
  33
  34 let INT_DIVIDES_RNEG = INTEGER_RULE
  35   `!d x. d divides (--x) <=> d divides x`;;
  36
  37 let INT_DIVIDES_RMUL = INTEGER_RULE
  38   `!d x y. d divides x ==> d divides (x * y)`;;
  39
  40 let INT_DIVIDES_LMUL = INTEGER_RULE
  41   `!d x y. d divides y ==> d divides (x * y)`;;
  42
  43 let INT_DIVIDES_1 = INTEGER_RULE
  44   `!x. &1 divides x`;;
  45
  46 let INT_DIVIDES_ADD_REVR = INTEGER_RULE
  47   `!d a b. d divides a /\ d divides (a + b) ==> d divides b`;;
  48
  49 let INT_DIVIDES_ADD_REVL = INTEGER_RULE
  50   `!d a b. d divides b /\ d divides (a + b) ==> d divides a`;;
  51
  52 let INT_DIVIDES_MUL_L = INTEGER_RULE
  53   `!a b c. a divides b ==> (c * a) divides (c * b)`;;
  54
  55 let INT_DIVIDES_MUL_R = INTEGER_RULE
  56   `!a b c. a divides b ==> (a * c) divides (b * c)`;;
  57
  58 let INT_DIVIDES_LMUL2 = INTEGER_RULE
  59   `!d a x. (x * d) divides a ==> d divides a`;;
  60
  61 let INT_DIVIDES_RMUL2 = INTEGER_RULE
  62   `!d a x. (d * x) divides a ==> d divides a`;;
  63
  64 let INT_DIVIDES_CMUL2 = INTEGER_RULE
  65   `!a b c. (c * a) divides (c * b) /\ ~(c = &0) ==> a divides b`;;
  66
  67 let INT_DIVIDES_LMUL2_EQ = INTEGER_RULE
  68   `!a b c. ~(c = &0) ==> ((c * a) divides (c * b) <=> a divides b)`;;
  69
  70 let INT_DIVIDES_RMUL2_EQ = INTEGER_RULE
  71   `!a b c. ~(c = &0) ==> ((a * c) divides (b * c) <=> a divides b)`;;
  72
  73 let INT_DIVIDES_MUL2 = INTEGER_RULE
  74   `!a b c d. a divides b /\ c divides d ==> (a * c) divides (b * d)`;;
  75
  76 let INT_DIVIDES_LABS = prove
  77  (`!d n. abs(d) divides n <=> d divides n`,
  78   REPEAT GEN_TAC THEN SIMP_TAC[INT_ABS] THEN COND_CASES_TAC THEN INTEGER_TAC);;
  79
  80 let INT_DIVIDES_RABS = prove
  81  (`!d n. d divides (abs n) <=> d divides n`,
  82   REPEAT GEN_TAC THEN SIMP_TAC[INT_ABS] THEN COND_CASES_TAC THEN INTEGER_TAC);;
  83
  84 let INT_DIVIDES_ABS = prove
  85  (`(!d n. abs(d) divides n <=> d divides n) /\
  86    (!d n. d divides (abs n) <=> d divides n)`,
  87   REWRITE_TAC[INT_DIVIDES_LABS; INT_DIVIDES_RABS]);;
  88
  89 let INT_DIVIDES_POW = prove
  90  (`!x y n. x divides y ==> (x pow n) divides (y pow n)`,
  91   REWRITE_TAC[int_divides] THEN MESON_TAC[INT_POW_MUL]);;
  92
  93 let INT_DIVIDES_POW2 = prove
  94  (`!n x y. ~(n = 0) /\ (x pow n) divides y ==> x divides y`,
  95   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; INT_POW] THEN INTEGER_TAC);;
  96
  97 let INT_DIVIDES_RPOW = prove
  98  (`!x y n. x divides y /\ ~(n = 0) ==> x divides (y pow n)`,
  99   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 100   SIMP_TAC[INT_DIVIDES_RMUL; INT_POW]);;
 101
 102 let INT_DIVIDES_RPOW_SUC = prove
 103  (`!x y n. x divides y ==> x divides (y pow (SUC n))`,
 104   SIMP_TAC[INT_DIVIDES_RPOW; NOT_SUC]);;
 105
 106 let INT_DIVIDES_ANTISYM_DIVISORS = prove
 107  (`!a b:int. a divides b /\ b divides a <=> !d. d divides a <=> d divides b`,
 108   MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);;
 109
 110 (* ------------------------------------------------------------------------- *)
 111 (* Now carefully distinguish signs.                                          *)
 112 (* ------------------------------------------------------------------------- *)
 113
 114 let INT_DIVIDES_ONE_POS = prove
 115  (`!x. &0 <= x ==> (x divides &1 <=> x = &1)`,
 116   REPEAT STRIP_TAC THEN EQ_TAC THENL
 117    [REWRITE_TAC[int_divides]; INTEGER_TAC] THEN
 118   DISCH_THEN(CHOOSE_THEN(MP_TAC o AP_TERM `abs` o SYM)) THEN
 119   SIMP_TAC[INT_ABS_NUM; INT_ABS_MUL_1] THEN ASM_SIMP_TAC[INT_ABS]);;
 120
 121 let INT_DIVIDES_ONE_ABS = prove
 122  (`!d. d divides &1 <=> abs(d) = &1`,
 123   MESON_TAC[INT_DIVIDES_LABS; INT_DIVIDES_ONE_POS; INT_ABS_POS]);;
 124
 125 let INT_DIVIDES_ONE = prove
 126  (`!d. d divides &1 <=> d = &1 \/ d = -- &1`,
 127   REWRITE_TAC[INT_DIVIDES_ONE_ABS] THEN INT_ARITH_TAC);;
 128
 129 let INT_DIVIDES_ANTISYM_ASSOCIATED = prove
 130  (`!x y. x divides y /\ y divides x <=> ?u. u divides &1 /\ x = y * u`,
 131   REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; INTEGER_TAC] THEN
 132   ASM_CASES_TAC `x = &0` THEN ASM_SIMP_TAC[INT_DIVIDES_ZERO; INT_MUL_LZERO] THEN
 133   ASM_MESON_TAC[int_divides; INT_DIVIDES_REFL;
 134     INTEGER_RULE `y = x * d /\ x = y * e /\ ~(y = &0) ==> d divides &1`]);;
 135
 136 let INT_DIVIDES_ANTISYM = prove
 137  (`!x y. x divides y /\ y divides x <=> x = y \/ x = --y`,
 138   REWRITE_TAC[INT_DIVIDES_ANTISYM_ASSOCIATED; INT_DIVIDES_ONE] THEN
 139   REWRITE_TAC[RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2] THEN
 140   INT_ARITH_TAC);;
 141
 142 let INT_DIVIDES_ANTISYM_ABS = prove
 143  (`!x y. x divides y /\ y divides x <=> abs(x) = abs(y)`,
 144   REWRITE_TAC[INT_DIVIDES_ANTISYM] THEN INT_ARITH_TAC);;
 145
 146 let INT_DIVIDES_ANTISYM_POS = prove
 147  (`!x y. &0 <= x /\ &0 <= y ==> (x divides y /\ y divides x <=> x = y)`,
 148   REWRITE_TAC[INT_DIVIDES_ANTISYM_ABS] THEN INT_ARITH_TAC);;
 149
 150 (* ------------------------------------------------------------------------- *)
 151 (* Lemmas about GCDs.                                                        *)
 152 (* ------------------------------------------------------------------------- *)
 153
 154 let INT_GCD_POS = prove
 155  (`!a b. &0 <= gcd(a,b)`,
 156   REWRITE_TAC[int_gcd]);;
 157
 158 let INT_GCD_DIVIDES = prove
 159  (`!a b. gcd(a,b) divides a /\ gcd(a,b) divides b`,
 160   INTEGER_TAC);;
 161
 162 let INT_GCD_BEZOUT = prove
 163  (`!a b. ?x y. gcd(a,b) = a * x + b * y`,
 164   INTEGER_TAC);;
 165
 166 let INT_DIVIDES_GCD = prove
 167  (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`,
 168   INTEGER_TAC);;
 169
 170 let INT_DIVIDES_GCD = prove
 171  (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`,
 172   INTEGER_TAC);;
 173
 174 let INT_GCD = INTEGER_RULE
 175   `!a b. (gcd(a,b) divides a /\ gcd(a,b) divides b) /\
 176          (!e. e divides a /\ e divides b ==> e divides gcd(a,b))`;;
 177
 178 let INT_GCD_UNIQUE = prove
 179  (`!a b d. gcd(a,b) = d <=> &0 <= d /\ d divides a /\ d divides b /\
 180                             !e. e divides a /\ e divides b ==> e divides d`,
 181   REPEAT GEN_TAC THEN EQ_TAC THENL
 182    [MESON_TAC[INT_GCD; INT_GCD_POS]; ALL_TAC] THEN
 183   ASM_SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS; INT_DIVIDES_GCD] THEN
 184   REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN INTEGER_TAC);;
 185
 186 let INT_GCD_UNIQUE_ABS = prove
 187  (`!a b d. gcd(a,b) = abs(d) <=>
 188            d divides a /\ d divides b /\
 189            !e. e divides a /\ e divides b ==> e divides d`,
 190   REWRITE_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS]);;
 191
 192 let INT_GCD_REFL = prove
 193  (`!a. gcd(a,a) = abs(a)`,
 194   REWRITE_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);;
 195
 196 let INT_GCD_SYM = prove
 197  (`!a b. gcd(a,b) = gcd(b,a)`,
 198   SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN INTEGER_TAC);;
 199
 200 let INT_GCD_ASSOC = prove
 201  (`!a b c. gcd(a,gcd(b,c)) = gcd(gcd(a,b),c)`,
 202   SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN INTEGER_TAC);;
 203
 204 let INT_GCD_1 = prove
 205  (`!a. gcd(a,&1) = &1 /\ gcd(&1,a) = &1`,
 206   SIMP_TAC[INT_GCD_UNIQUE; INT_POS; INT_DIVIDES_1]);;
 207
 208 let INT_GCD_0 = prove
 209  (`!a. gcd(a,&0) = abs(a) /\ gcd(&0,a) = abs(a)`,
 210   SIMP_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);;
 211
 212 let INT_GCD_ABS = prove
 213  (`!a b. gcd(abs(a),b) = gcd(a,b) /\ gcd(a,abs(b)) = gcd(a,b)`,
 214   REWRITE_TAC[INT_GCD_UNIQUE; INT_DIVIDES_ABS; INT_GCD_POS; INT_GCD]);;
 215
 216 let INT_GCD_MULTIPLE =
 217  (`!a b. gcd(a,a * b) = abs(a) /\ gcd(b,a * b) = abs(b)`,
 218   REWRITE_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);;
 219
 220 let INT_GCD_ADD = prove
 221  (`(!a b. gcd(a + b,b) = gcd(a,b)) /\
 222    (!a b. gcd(b + a,b) = gcd(a,b)) /\
 223    (!a b. gcd(a,a + b) = gcd(a,b)) /\
 224    (!a b. gcd(a,b + a) = gcd(a,b))`,
 225   SIMP_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);;
 226
 227 let INT_GCD_SUB = prove
 228  (`(!a b. gcd(a - b,b) = gcd(a,b)) /\
 229    (!a b. gcd(b - a,b) = gcd(a,b)) /\
 230    (!a b. gcd(a,a - b) = gcd(a,b)) /\
 231    (!a b. gcd(a,b - a) = gcd(a,b))`,
 232   SIMP_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);;
 233
 234 let INT_DIVIDES_GCD_LEFT = prove
 235  (`!m n:int. m divides n <=> gcd(m,n) = abs m`,
 236   SIMP_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS; INT_DIVIDES_REFL] THEN
 237   MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);;
 238
 239 let INT_DIVIDES_GCD_RIGHT = prove
 240  (`!m n:int. n divides m <=> gcd(m,n) = abs n`,
 241   SIMP_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS; INT_DIVIDES_REFL] THEN
 242   MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);;
 243
 244 (* ------------------------------------------------------------------------- *)
 245 (* More lemmas about coprimality.                                            *)
 246 (* ------------------------------------------------------------------------- *)
 247
 248 let INT_COPRIME_GCD = prove
 249  (`!a b. coprime(a,b) <=> gcd(a,b) = &1`,
 250   SIMP_TAC[GSYM INT_DIVIDES_ONE_POS; INT_GCD_POS] THEN INTEGER_TAC);;
 251
 252 let int_coprime = prove
 253  (`!a b. coprime(a,b) <=> !d. d divides a /\ d divides b ==> d divides &1`,
 254   REWRITE_TAC[INT_COPRIME_GCD; INT_GCD_UNIQUE; INT_POS; INT_DIVIDES_1]);;
 255
 256 let COPRIME = prove
 257  (`!a b. coprime(a,b) <=> !d. d divides a /\ d divides b <=> d divides &1`,
 258   MESON_TAC[INT_DIVIDES_1; INT_DIVIDES_TRANS; int_coprime]);;
 259
 260 let INT_COPRIME_SYM = prove
 261  (`!a b. coprime(a,b) <=> coprime(b,a)`,
 262   INTEGER_TAC);;
 263
 264 let INT_COPRIME_DIVPROD = prove
 265  (`!d a b. d divides (a * b) /\ coprime(d,a) ==> d divides b`,
 266   INTEGER_TAC);;
 267
 268 let INT_COPRIME_1 = prove
 269  (`!a. coprime(a,&1) /\ coprime(&1,a)`,
 270   INTEGER_TAC);;
 271
 272 let INT_GCD_COPRIME = prove
 273  (`!a b a' b'. ~(gcd(a,b) = &0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
 274                ==> coprime(a',b')`,
 275   INTEGER_TAC);;
 276
 277 let INT_GCD_COPRIME_EXISTS = prove
 278  (`!a b. ~(gcd(a,b) = &0) ==>
 279         ?a' b'. (a = a' * gcd(a,b)) /\
 280                 (b = b' * gcd(a,b)) /\
 281                 coprime(a',b')`,
 282   INTEGER_TAC);;
 283
 284 let INT_COPRIME_0 = prove
 285  (`(!a. coprime(a,&0) <=> a divides &1) /\
 286    (!a. coprime(&0,a) <=> a divides &1)`,
 287   INTEGER_TAC);;
 288
 289 let INT_COPRIME_MUL = prove
 290  (`!d a b. coprime(d,a) /\ coprime(d,b) ==> coprime(d,a * b)`,
 291   INTEGER_TAC);;
 292
 293 let INT_COPRIME_LMUL2 = prove
 294  (`!d a b. coprime(d,a * b) ==> coprime(d,b)`,
 295   INTEGER_TAC);;
 296
 297 let INT_COPRIME_RMUL2 = prove
 298  (`!d a b.  coprime(d,a * b) ==> coprime(d,a)`,
 299   INTEGER_TAC);;
 300
 301 let INT_COPRIME_LMUL = prove
 302  (`!d a b. coprime(a * b,d) <=> coprime(a,d) /\ coprime(b,d)`,
 303   INTEGER_TAC);;
 304
 305 let INT_COPRIME_RMUL = prove
 306  (`!d a b. coprime(d,a * b) <=> coprime(d,a) /\ coprime(d,b)`,
 307   INTEGER_TAC);;
 308
 309 let INT_COPRIME_REFL = prove
 310  (`!n. coprime(n,n) <=> n divides &1`,
 311   INTEGER_TAC);;
 312
 313 let INT_COPRIME_PLUS1 = prove
 314  (`!n. coprime(n + &1,n) /\ coprime(n,n + &1)`,
 315   INTEGER_TAC);;
 316
 317 let INT_COPRIME_MINUS1 = prove
 318  (`!n. coprime(n - &1,n) /\ coprime(n,n - &1)`,
 319   INTEGER_TAC);;
 320
 321 let INT_COPRIME_RPOW = prove
 322  (`!m n k. coprime(m,n pow k) <=> coprime(m,n) \/ k = 0`,
 323   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 324   ASM_SIMP_TAC[INT_POW; INT_COPRIME_1; INT_COPRIME_RMUL; NOT_SUC] THEN
 325   CONV_TAC TAUT);;
 326
 327 let INT_COPRIME_LPOW = prove
 328  (`!m n k. coprime(m pow k,n) <=> coprime(m,n) \/ k = 0`,
 329   ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN REWRITE_TAC[INT_COPRIME_RPOW]);;
 330
 331 let INT_COPRIME_POW2 = prove
 332  (`!m n k. coprime(m pow k,n pow k) <=> coprime(m,n) \/ k = 0`,
 333   REWRITE_TAC[INT_COPRIME_RPOW; INT_COPRIME_LPOW; DISJ_ACI]);;
 334
 335 let INT_COPRIME_POW = prove
 336  (`!n a d. coprime(d,a) ==> coprime(d,a pow n)`,
 337   SIMP_TAC[INT_COPRIME_RPOW]);;
 338
 339 let INT_COPRIME_POW_IMP = prove
 340  (`!n a b. coprime(a,b) ==> coprime(a pow n,b pow n)`,
 341   MESON_TAC[INT_COPRIME_POW; INT_COPRIME_SYM]);;
 342
 343 let INT_GCD_EQ_0 = prove
 344  (`!a b. gcd(a,b) = &0 <=> a = &0 /\ b = &0`,
 345   INTEGER_TAC);;
 346
 347 let INT_DIVISION_DECOMP = prove
 348  (`!a b c. a divides (b * c)
 349            ==> ?b' c'. (a = b' * c') /\ b' divides b /\ c' divides c`,
 350   REPEAT STRIP_TAC THEN EXISTS_TAC `gcd(a,b)` THEN
 351   ASM_CASES_TAC `gcd(a,b) = &0` THEN REPEAT(POP_ASSUM MP_TAC) THENL
 352    [SIMP_TAC[INT_GCD_EQ_0; INT_GCD_0; INT_ABS_NUM]; INTEGER_TAC] THEN
 353   REWRITE_TAC[INT_MUL_LZERO] THEN MESON_TAC[INT_DIVIDES_REFL]);;
 354
 355 let INT_DIVIDES_MUL = prove
 356  (`!m n r. m divides r /\ n divides r /\ coprime(m,n) ==> (m * n) divides r`,
 357   INTEGER_TAC);;
 358
 359 let INT_CHINESE_REMAINDER = prove
 360  (`!a b u v. coprime(a,b) /\ ~(a = &0) /\ ~(b = &0)
 361              ==> ?x q1 q2. (x = u + q1 * a) /\ (x = v + q2 * b)`,
 362   INTEGER_TAC);;
 363
 364 let INT_CHINESE_REMAINDER_USUAL = prove
 365  (`!a b u v. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`,
 366   INTEGER_TAC);;
 367
 368 let INT_COPRIME_DIVISORS = prove
 369  (`!a b d e. d divides a /\ e divides b /\ coprime(a,b) ==> coprime(d,e)`,
 370   INTEGER_TAC);;
 371
 372 let INT_COPRIME_LNEG = prove
 373  (`!a b. coprime(--a,b) <=> coprime(a,b)`,
 374   INTEGER_TAC);;
 375
 376 let INT_COPRIME_RNEG = prove
 377  (`!a b. coprime(a,--b) <=> coprime(a,b)`,
 378   INTEGER_TAC);;
 379
 380 let INT_COPRIME_NEG = prove
 381  (`(!a b. coprime(--a,b) <=> coprime(a,b)) /\
 382    (!a b. coprime(a,--b) <=> coprime(a,b))`,
 383   INTEGER_TAC);;
 384
 385 let INT_COPRIME_LABS = prove
 386  (`!a b. coprime(abs a,b) <=> coprime(a,b)`,
 387   REWRITE_TAC[INT_ABS] THEN MESON_TAC[INT_COPRIME_LNEG]);;
 388
 389 let INT_COPRIME_RABS = prove
 390  (`!a b. coprime(a,abs b) <=> coprime(a,b)`,
 391   REWRITE_TAC[INT_ABS] THEN MESON_TAC[INT_COPRIME_RNEG]);;
 392
 393 let INT_COPRIME_ABS = prove
 394  (`(!a b. coprime(abs a,b) <=> coprime(a,b)) /\
 395    (!a b. coprime(a,abs b) <=> coprime(a,b))`,
 396   REWRITE_TAC[INT_COPRIME_LABS; INT_COPRIME_RABS]);;
 397
 398 (* ------------------------------------------------------------------------- *)
 399 (* More lemmas about congruences.                                            *)
 400 (* ------------------------------------------------------------------------- *)
 401
 402 let INT_CONG_MOD_0 = prove
 403  (`!x y. (x == y) (mod &0) <=> (x = y)`,
 404   INTEGER_TAC);;
 405
 406 let INT_CONG_MOD_1 = prove
 407  (`!x y. (x == y) (mod &1)`,
 408   INTEGER_TAC);;
 409
 410 let INT_CONG_0 = prove
 411  (`!x n. ((x == &0) (mod n) <=> n divides x)`,
 412   INTEGER_TAC);;
 413
 414 let INT_CONG = prove
 415  (`!x y n. (x == y) (mod n) <=> n divides (x - y)`,
 416   INTEGER_TAC);;
 417
 418 let INT_CONG_MUL_LCANCEL = prove
 419  (`!a n x y. coprime(a,n) /\ (a * x == a * y) (mod n) ==> (x == y) (mod n)`,
 420   INTEGER_TAC);;
 421
 422 let INT_CONG_MUL_RCANCEL = prove
 423  (`!a n x y. coprime(a,n) /\ (x * a == y * a) (mod n) ==> (x == y) (mod n)`,
 424   INTEGER_TAC);;
 425
 426 let INT_CONG_REFL = prove
 427  (`!x n. (x == x) (mod n)`,
 428   INTEGER_TAC);;
 429
 430 let INT_EQ_IMP_CONG = prove
 431  (`!a b n. a = b ==> (a == b) (mod n)`,
 432   INTEGER_TAC);;
 433
 434 let INT_CONG_SYM = prove
 435  (`!x y n. (x == y) (mod n) <=> (y == x) (mod n)`,
 436   INTEGER_TAC);;
 437
 438 let INT_CONG_TRANS = prove
 439  (`!x y z n. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`,
 440   INTEGER_TAC);;
 441
 442 let INT_CONG_ADD = prove
 443  (`!x x' y y'.
 444      (x == x') (mod n) /\ (y == y') (mod n) ==> (x + y == x' + y') (mod n)`,
 445   INTEGER_TAC);;
 446
 447 let INT_CONG_SUB = prove
 448  (`!x x' y y'.
 449      (x == x') (mod n) /\ (y == y') (mod n) ==> (x - y == x' - y') (mod n)`,
 450   INTEGER_TAC);;
 451
 452 let INT_CONG_MUL = prove
 453  (`!x x' y y'.
 454      (x == x') (mod n) /\ (y == y') (mod n) ==> (x * y == x' * y') (mod n)`,
 455   INTEGER_TAC);;
 456
 457 let INT_CONG_POW = prove
 458  (`!n k x y. (x == y) (mod n) ==> (x pow k == y pow k) (mod n)`,
 459   GEN_TAC THEN INDUCT_TAC THEN
 460   ASM_SIMP_TAC[INT_CONG_MUL; INT_POW; INT_CONG_REFL]);;
 461
 462 let INT_CONG_MUL_LCANCEL_EQ = prove
 463  (`!a n x y. coprime(a,n) ==> ((a * x == a * y) (mod n) <=> (x == y) (mod n))`,
 464   INTEGER_TAC);;
 465
 466 let INT_CONG_MUL_RCANCEL_EQ = prove
 467  (`!a n x y. coprime(a,n) ==> ((x * a == y * a) (mod n) <=> (x == y) (mod n))`,
 468   INTEGER_TAC);;
 469
 470 let INT_CONG_ADD_LCANCEL_EQ = prove
 471  (`!a n x y. (a + x == a + y) (mod n) <=> (x == y) (mod n)`,
 472   INTEGER_TAC);;
 473
 474 let INT_CONG_ADD_RCANCEL_EQ = prove
 475  (`!a n x y. (x + a == y + a) (mod n) <=> (x == y) (mod n)`,
 476   INTEGER_TAC);;
 477
 478 let INT_CONG_ADD_RCANCEL = prove
 479  (`!a n x y. (x + a == y + a) (mod n) ==> (x == y) (mod n)`,
 480   INTEGER_TAC);;
 481
 482 let INT_CONG_ADD_LCANCEL = prove
 483  (`!a n x y. (a + x == a + y) (mod n) ==> (x == y) (mod n)`,
 484   INTEGER_TAC);;
 485
 486 let INT_CONG_ADD_LCANCEL_EQ_0 = prove
 487  (`!a n x y. (a + x == a) (mod n) <=> (x == &0) (mod n)`,
 488   INTEGER_TAC);;
 489
 490 let INT_CONG_ADD_RCANCEL_EQ_0 = prove
 491  (`!a n x y. (x + a == a) (mod n) <=> (x == &0) (mod n)`,
 492   INTEGER_TAC);;
 493
 494 let INT_CONG_INT_DIVIDES_MODULUS = prove
 495  (`!x y m n. (x == y) (mod m) /\ n divides m ==> (x == y) (mod n)`,
 496   INTEGER_TAC);;
 497
 498 let INT_CONG_0_DIVIDES = prove
 499  (`!n x. (x == &0) (mod n) <=> n divides x`,
 500   INTEGER_TAC);;
 501
 502 let INT_CONG_1_DIVIDES = prove
 503  (`!n x. (x == &1) (mod n) ==> n divides (x - &1)`,
 504   INTEGER_TAC);;
 505
 506 let INT_CONG_DIVIDES = prove
 507  (`!x y n. (x == y) (mod n) ==> (n divides x <=> n divides y)`,
 508   INTEGER_TAC);;
 509
 510 let INT_CONG_COPRIME = prove
 511  (`!x y n. (x == y) (mod n) ==> (coprime(n,x) <=> coprime(n,y))`,
 512   INTEGER_TAC);;
 513
 514 let INT_CONG_MOD_MULT = prove
 515  (`!x y m n. (x == y) (mod n) /\ m divides n ==> (x == y) (mod m)`,
 516   INTEGER_TAC);;
 517
 518 let INT_CONG_TO_1 = prove
 519  (`!a n. (a == &1) (mod n) <=> ?m. a = &1 + m * n`,
 520   INTEGER_TAC);;
 521
 522 let INT_CONG_SOLVE = prove
 523  (`!a b n. coprime(a,n) ==> ?x. (a * x == b) (mod n)`,
 524   INTEGER_TAC);;
 525
 526 let INT_CONG_SOLVE_UNIQUE = prove
 527  (`!a b n. coprime(a,n)
 528            ==> !x y. (a * x == b) (mod n) /\ (a * y == b) (mod n)
 529                      ==> (x == y) (mod n)`,
 530   INTEGER_TAC);;
 531
 532 let INT_CONG_CHINESE = prove
 533  (`coprime(a,b) /\ (x == y) (mod a) /\ (x == y) (mod b)
 534    ==> (x == y) (mod (a * b))`,
 535   INTEGER_TAC);;
 536
 537 let INT_CHINESE_REMAINDER_COPRIME = prove
 538  (`!a b m n.
 539         coprime(a,b) /\ ~(a = &0) /\ ~(b = &0) /\ coprime(m,a) /\ coprime(n,b)
 540         ==> ?x. coprime(x,a * b) /\
 541                 (x == m) (mod a) /\ (x == n) (mod b)`,
 542   INTEGER_TAC);;
 543
 544 let INT_CHINESE_REMAINDER_COPRIME_UNIQUE = prove
 545  (`!a b m n x y.
 546         coprime(a,b) /\
 547         (x == m) (mod a) /\ (x == n) (mod b) /\
 548         (y == m) (mod a) /\ (y == n) (mod b)
 549         ==> (x == y) (mod (a * b))`,
 550   INTEGER_TAC);;
 551
 552 let SOLVABLE_GCD = prove
 553  (`!a b n. gcd(a,n) divides b ==> ?x. (a * x == b) (mod n)`,
 554   INTEGER_TAC);;
 555
 556 let INT_LINEAR_CONG_POS = prove
 557  (`!n a x:int. ~(n = &0) ==> ?y. &0 <= y /\ (a * x == a * y) (mod n)`,
 558   REPEAT STRIP_TAC THEN EXISTS_TAC `x + abs(x * n):int` THEN CONJ_TAC THENL
 559    [MATCH_MP_TAC(INT_ARITH `abs(x:int) * &1 <= y ==> &0 <= x + y`) THEN
 560     REWRITE_TAC[INT_ABS_MUL] THEN MATCH_MP_TAC INT_LE_LMUL THEN
 561     ASM_INT_ARITH_TAC;
 562     MATCH_MP_TAC(INTEGER_RULE
 563      `n divides y ==> (a * x:int == a * (x + y)) (mod n)`) THEN
 564     REWRITE_TAC[INT_DIVIDES_RABS] THEN INTEGER_TAC]);;
 565
 566 let INT_CONG_SOLVE_POS = prove
 567  (`!a b n:int.
 568         coprime(a,n) /\ ~(n = &0 /\ abs a = &1)
 569         ==> ?x. &0 <= x /\ (a * x == b) (mod n)`,
 570   REPEAT GEN_TAC THEN ASM_CASES_TAC `n:int = &0` THEN
 571   ASM_REWRITE_TAC[INT_COPRIME_0; INT_DIVIDES_ONE] THENL
 572    [INT_ARITH_TAC;
 573     ASM_MESON_TAC[INT_LINEAR_CONG_POS; INT_CONG_SOLVE; INT_CONG_TRANS;
 574                   INT_CONG_SYM]]);;
 575
 576 let INT_CONG_IMP_EQ = prove
 577  (`!x y n:int. abs(x - y) < n /\ (x == y) (mod n) ==> x = y`,
 578   REPEAT GEN_TAC THEN
 579   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 580   ONCE_REWRITE_TAC[int_congruent; GSYM INT_SUB_0] THEN
 581   DISCH_THEN(X_CHOOSE_THEN `q:int` SUBST_ALL_TAC) THEN
 582   FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
 583    `abs(n * q) < n ==> abs(n * q) < abs n * &1`)) THEN
 584   REWRITE_TAC[INT_ABS_MUL; INT_ENTIRE] THEN
 585   REWRITE_TAC[INT_ARITH
 586    `abs n * (q:int) < abs n * &1 <=> ~(&0 <= abs n * (q - &1))`] THEN
 587   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
 588   STRIP_TAC THEN MATCH_MP_TAC INT_LE_MUL THEN ASM_INT_ARITH_TAC);;
 589
 590 (* ------------------------------------------------------------------------- *)
 591 (* A stronger form of the CRT.                                               *)
 592 (* ------------------------------------------------------------------------- *)
 593
 594 let INT_CRT_STRONG = prove
 595  (`!a1 a2 n1 n2:int.
 596         (a1 == a2) (mod (gcd(n1,n2)))
 597         ==> ?x. (x == a1) (mod n1) /\ (x == a2) (mod n2)`,
 598   INTEGER_TAC);;
 599
 600 let INT_CRT_STRONG_IFF = prove
 601  (`!a1 a2 n1 n2:int.
 602         (?x. (x == a1) (mod n1) /\ (x == a2) (mod n2)) <=>
 603         (a1 == a2) (mod (gcd(n1,n2)))`,
 604   INTEGER_TAC);;
 605
 606 (* ------------------------------------------------------------------------- *)
 607 (* Other miscellaneous lemmas.                                               *)
 608 (* ------------------------------------------------------------------------- *)
 609
 610 let EVEN_SQUARE_MOD4 = prove
 611  (`((&2 * n) pow 2 == &0) (mod &4)`,
 612   INTEGER_TAC);;
 613
 614 let ODD_SQUARE_MOD4 = prove
 615  (`((&2 * n + &1) pow 2 == &1) (mod &4)`,
 616   INTEGER_TAC);;
 617
 618 let INT_DIVIDES_LE = prove
 619  (`!x y. x divides y ==> abs(x) <= abs(y) \/ y = &0`,
 620   REWRITE_TAC[int_divides; LEFT_IMP_EXISTS_THM] THEN
 621   MAP_EVERY X_GEN_TAC [`x:int`; `y:int`; `z:int`] THEN
 622   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_ABS_MUL; INT_ENTIRE] THEN
 623   REWRITE_TAC[INT_ARITH `x <= x * z <=> &0 <= x * (z - &1)`] THEN
 624   ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
 625   ASM_CASES_TAC `z = &0` THEN ASM_REWRITE_TAC[] THEN
 626   MATCH_MP_TAC INT_LE_MUL THEN ASM_INT_ARITH_TAC);;
 627
 628 let INT_DIVIDES_POW_LE = prove
 629  (`!p m n. &2 <= abs p ==> ((p pow m) divides (p pow n) <=> m <= n)`,
 630   REPEAT STRIP_TAC THEN EQ_TAC THENL
 631    [DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN
 632     ASM_SIMP_TAC[INT_POW_EQ_0; INT_ARITH `&2 <= abs p ==> ~(p = &0)`] THEN
 633     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 634     REWRITE_TAC[INT_NOT_LE; NOT_LE; INT_ABS_POW] THEN
 635     ASM_MESON_TAC[INT_POW_MONO_LT; ARITH_RULE `&2 <= x ==> &1 < x`];
 636     SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; INT_POW_ADD] THEN INTEGER_TAC]);;
 637
 638 (* ------------------------------------------------------------------------- *)
 639 (* Integer primality / irreducibility.                                       *)
 640 (* ------------------------------------------------------------------------- *)
 641
 642 let int_prime = new_definition
 643  `int_prime p <=> abs(p) > &1 /\
 644                   !x. x divides p ==> abs(x) = &1 \/ abs(x) = abs(p)`;;
 645
 646 let INT_PRIME_NEG = prove
 647  (`!p. int_prime(--p) <=> int_prime p`,
 648   REWRITE_TAC[int_prime; INT_DIVIDES_RNEG; INT_ABS_NEG]);;
 649
 650 let INT_PRIME_ABS = prove
 651  (`!p. int_prime(abs p) <=> int_prime p`,
 652   GEN_TAC THEN REWRITE_TAC[INT_ABS] THEN
 653   COND_CASES_TAC THEN ASM_REWRITE_TAC[INT_PRIME_NEG]);;
 654
 655 let INT_PRIME_GE_2 = prove
 656  (`!p. int_prime p ==> &2 <= abs(p)`,
 657   REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);;
 658
 659 let INT_PRIME_0 = prove
 660  (`~(int_prime(&0))`,
 661   REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);;
 662
 663 let INT_PRIME_1 = prove
 664  (`~(int_prime(&1))`,
 665   REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);;
 666
 667 let INT_PRIME_2 = prove
 668  (`int_prime(&2)`,
 669   REWRITE_TAC[int_prime] THEN CONV_TAC INT_REDUCE_CONV THEN
 670   X_GEN_TAC `x:int` THEN
 671   ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[INT_DIVIDES_ZERO] THEN
 672   CONV_TAC INT_REDUCE_CONV THEN
 673   DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC);;
 674
 675 let INT_PRIME_FACTOR = prove
 676  (`!x. ~(abs x = &1) ==> ?p. int_prime p /\ p divides x`,
 677   MATCH_MP_TAC WF_INT_MEASURE THEN EXISTS_TAC `abs` THEN
 678   REWRITE_TAC[INT_ABS_POS] THEN X_GEN_TAC `x:int` THEN
 679   REPEAT STRIP_TAC THEN ASM_CASES_TAC `int_prime x` THENL
 680    [EXISTS_TAC `x:int` THEN ASM_REWRITE_TAC[] THEN
 681     REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC;
 682     ALL_TAC] THEN
 683   ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THENL
 684    [EXISTS_TAC `&2` THEN ASM_REWRITE_TAC[INT_PRIME_2; INT_DIVIDES_0];
 685     ALL_TAC] THEN
 686   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [int_prime]) THEN
 687   ASM_SIMP_TAC[INT_ARITH `~(x = &0) /\ ~(abs x = &1) ==> abs x > &1`] THEN
 688   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; DE_MORGAN_THM] THEN
 689   DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC) THEN
 690   FIRST_X_ASSUM(MP_TAC o SPEC `y:int`) THEN ASM_REWRITE_TAC[] THEN
 691   ANTS_TAC THENL
 692    [FIRST_X_ASSUM(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC;
 693     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN
 694     UNDISCH_TAC `y divides x` THEN INTEGER_TAC]);;
 695
 696 let INT_PRIME_FACTOR_LT = prove
 697  (`!n m p. int_prime(p) /\ ~(n = &0) /\ n = p * m ==> abs m < abs n`,
 698   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[INT_ABS_MUL] THEN
 699   MATCH_MP_TAC(INT_ARITH `&0 < m * (p - &1) ==> m < p * m`) THEN
 700   MATCH_MP_TAC INT_LT_MUL THEN
 701   UNDISCH_TAC `~(n = &0)` THEN ASM_CASES_TAC `m = &0` THEN
 702   ASM_REWRITE_TAC[INT_MUL_RZERO] THEN DISCH_THEN(K ALL_TAC) THEN
 703   CONJ_TAC THENL [ASM_INT_ARITH_TAC; ALL_TAC] THEN
 704   FIRST_ASSUM(MP_TAC o MATCH_MP INT_PRIME_GE_2) THEN INT_ARITH_TAC);;
 705
 706 let INT_PRIME_FACTOR_INDUCT = prove
 707  (`!P. P(&0) /\ P(&1) /\ P(-- &1) /\
 708        (!p n. int_prime p /\ ~(n = &0) /\ P n ==> P(p * n))
 709        ==> !n. P n`,
 710   GEN_TAC THEN STRIP_TAC THEN
 711   MATCH_MP_TAC WF_INT_MEASURE THEN EXISTS_TAC `abs` THEN
 712   REWRITE_TAC[INT_ABS_POS] THEN X_GEN_TAC `n:int` THEN DISCH_TAC THEN
 713   ASM_CASES_TAC `n = &0` THEN ASM_REWRITE_TAC[] THEN
 714   ASM_CASES_TAC `abs n = &1` THENL
 715    [ASM_MESON_TAC[INT_ARITH `abs x = &a <=> x = &a \/ x = -- &a`];
 716     ALL_TAC] THEN
 717   FIRST_ASSUM(X_CHOOSE_THEN `p:int`
 718     STRIP_ASSUME_TAC o MATCH_MP INT_PRIME_FACTOR) THEN
 719   FIRST_X_ASSUM(X_CHOOSE_THEN `d:int` SUBST_ALL_TAC o
 720     GEN_REWRITE_RULE I [int_divides]) THEN
 721   FIRST_X_ASSUM(MP_TAC o SPECL [`p:int`; `d:int`]) THEN
 722   RULE_ASSUM_TAC(REWRITE_RULE[INT_ENTIRE; DE_MORGAN_THM]) THEN
 723   DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 724   FIRST_X_ASSUM MATCH_MP_TAC THEN
 725   ASM_MESON_TAC[INT_PRIME_FACTOR_LT; INT_ENTIRE]);;
 726
 727 (* ------------------------------------------------------------------------- *)
 728 (* Infinitude.                                                               *)
 729 (* ------------------------------------------------------------------------- *)
 730
 731 let INT_DIVIDES_FACT = prove
 732  (`!n x. &1 <= abs(x) /\ abs(x) <= &n ==> x divides &(FACT n)`,
 733   INDUCT_TAC THENL [INT_ARITH_TAC; ALL_TAC] THEN
 734   REWRITE_TAC[FACT; INT_ARITH `x <= &n <=> x = &n \/ x < &n`] THEN
 735   REWRITE_TAC[GSYM INT_OF_NUM_SUC; INT_ARITH `x < &m + &1 <=> x <= &m`] THEN
 736   REWRITE_TAC[INT_OF_NUM_SUC; GSYM INT_OF_NUM_MUL] THEN REPEAT STRIP_TAC THEN
 737   ASM_SIMP_TAC[INT_DIVIDES_LMUL] THEN
 738   MATCH_MP_TAC INT_DIVIDES_RMUL THEN
 739   ASM_MESON_TAC[INT_DIVIDES_LABS; INT_DIVIDES_REFL]);;
 740
 741 let INT_EUCLID_BOUND = prove
 742  (`!n. ?p. int_prime(p) /\ &n < p /\ p <= &(FACT n) + &1`,
 743   GEN_TAC THEN MP_TAC(SPEC `&(FACT n) + &1` INT_PRIME_FACTOR) THEN
 744   REWRITE_TAC[INT_OF_NUM_ADD; INT_ABS_NUM; INT_OF_NUM_EQ] THEN
 745   REWRITE_TAC[EQ_ADD_RCANCEL_0; FACT_NZ; GSYM INT_OF_NUM_ADD] THEN
 746   DISCH_THEN(X_CHOOSE_THEN `p:int` STRIP_ASSUME_TAC) THEN
 747   EXISTS_TAC `abs p` THEN ASM_REWRITE_TAC[INT_PRIME_ABS] THEN CONJ_TAC THENL
 748    [ALL_TAC;
 749     FIRST_ASSUM(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN
 750     REWRITE_TAC[GSYM INT_OF_NUM_ADD; GSYM INT_OF_NUM_SUC] THEN
 751     INT_ARITH_TAC] THEN
 752   REWRITE_TAC[GSYM INT_NOT_LE] THEN DISCH_TAC THEN
 753   MP_TAC(SPECL [`n:num`; `p:int`] INT_DIVIDES_FACT) THEN
 754   ASM_SIMP_TAC[INT_PRIME_GE_2; INT_ARITH `&2 <= p ==> &1 <= p`] THEN
 755   DISCH_TAC THEN SUBGOAL_THEN `p divides &1` MP_TAC THENL
 756    [REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC;
 757     REWRITE_TAC[INT_DIVIDES_ONE] THEN
 758     ASM_MESON_TAC[INT_PRIME_NEG; INT_PRIME_1]]);;
 759
 760 let INT_EUCLID = prove
 761  (`!n. ?p. int_prime(p) /\ p > n`,
 762   MP_TAC INT_IMAGE THEN MATCH_MP_TAC MONO_FORALL THEN
 763   X_GEN_TAC `n:int` THEN REWRITE_TAC[INT_GT] THEN
 764   ASM_REWRITE_TAC[OR_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 765   MP_TAC INT_EUCLID_BOUND THEN MATCH_MP_TAC MONO_FORALL THEN
 766   X_GEN_TAC `m:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 767   MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN
 768   FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN INT_ARITH_TAC);;
 769
 770 let INT_PRIMES_INFINITE = prove
 771  (`INFINITE {p | int_prime p}`,
 772   SUBGOAL_THEN `INFINITE {n | int_prime(&n)}` MP_TAC THEN
 773   REWRITE_TAC[INFINITE; CONTRAPOS_THM] THENL
 774    [REWRITE_TAC[num_FINITE; IN_ELIM_THM] THEN
 775     REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM; NOT_IMP; NOT_LE] THEN
 776     REWRITE_TAC[GSYM INT_OF_NUM_LT; INT_EXISTS_POS] THEN
 777     MP_TAC INT_EUCLID_BOUND THEN
 778     MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
 779     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
 780     SIMP_TAC[] THEN INT_ARITH_TAC;
 781     MP_TAC(ISPECL [`&`; `{p | int_prime p}`] FINITE_IMAGE_INJ) THEN
 782     REWRITE_TAC[INT_OF_NUM_EQ; IN_ELIM_THM]]);;
 783
 784 let INT_COPRIME_PRIME = prove
 785  (`!p a b. coprime(a,b) ==> ~(int_prime(p) /\ p divides a /\ p divides b)`,
 786   REWRITE_TAC[int_coprime] THEN
 787   MESON_TAC[INT_DIVIDES_ONE; INT_PRIME_NEG; INT_PRIME_1]);;
 788
 789 let INT_COPRIME_PRIME_EQ = prove
 790  (`!a b. coprime(a,b) <=> !p. ~(int_prime(p) /\ p divides a /\ p divides b)`,
 791   REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[INT_COPRIME_PRIME]; ALL_TAC] THEN
 792   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 793   REWRITE_TAC[int_coprime; INT_DIVIDES_ONE_ABS] THEN
 794   ONCE_REWRITE_TAC[NOT_FORALL_THM] THEN REWRITE_TAC[NOT_IMP] THEN
 795   DISCH_THEN(X_CHOOSE_THEN `d:int` STRIP_ASSUME_TAC) THEN
 796   FIRST_ASSUM(X_CHOOSE_TAC `p:int` o MATCH_MP INT_PRIME_FACTOR) THEN
 797   EXISTS_TAC `p:int` THEN ASM_MESON_TAC[INT_DIVIDES_TRANS]);;
 798
 799 let INT_PRIME_COPRIME = prove
 800  (`!x p. int_prime(p) ==> p divides x \/ coprime(p,x)`,
 801   REPEAT STRIP_TAC THEN REWRITE_TAC[int_coprime] THEN
 802   MATCH_MP_TAC(TAUT `(~b ==> a) ==> a \/ b`) THEN
 803   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; INT_DIVIDES_ONE_ABS] THEN
 804   DISCH_THEN(X_CHOOSE_THEN `d:int` STRIP_ASSUME_TAC) THEN
 805   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [int_prime]) THEN
 806   DISCH_THEN(MP_TAC o SPEC `d:int` o CONJUNCT2) THEN ASM_REWRITE_TAC[] THEN
 807   ASM_MESON_TAC[INT_DIVIDES_TRANS; INT_DIVIDES_LABS; INT_DIVIDES_RABS]);;
 808
 809 let INT_PRIME_COPRIME_EQ = prove
 810  (`!p n. int_prime p ==> (coprime(p,n) <=> ~(p divides n))`,
 811   REPEAT STRIP_TAC THEN
 812   MATCH_MP_TAC(TAUT `(b \/ a) /\ ~(a /\ b) ==> (a <=> ~b)`) THEN
 813   ASM_SIMP_TAC[INT_PRIME_COPRIME; int_coprime; INT_DIVIDES_ONE_ABS] THEN
 814   ASM_MESON_TAC[INT_DIVIDES_REFL; INT_PRIME_1; INT_PRIME_ABS]);;
 815
 816 let INT_COPRIME_PRIMEPOW = prove
 817  (`!p k m. int_prime p /\ ~(k = 0)
 818            ==> (coprime(m,p pow k) <=> ~(p divides m))`,
 819   SIMP_TAC[INT_COPRIME_RPOW] THEN ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN
 820   SIMP_TAC[INT_PRIME_COPRIME_EQ]);;
 821
 822 let INT_COPRIME_BEZOUT = prove
 823  (`!a b. coprime(a,b) <=> ?x y. a * x + b * y = &1`,
 824   INTEGER_TAC);;
 825
 826 let INT_COPRIME_BEZOUT_ALT = prove
 827  (`!a b. coprime(a,b) ==> ?x y. a * x = b * y + &1`,
 828   INTEGER_TAC);;
 829
 830 let INT_BEZOUT_PRIME = prove
 831  (`!a p. int_prime p /\ ~(p divides a) ==> ?x y. a * x = p * y + &1`,
 832   MESON_TAC[INT_COPRIME_BEZOUT_ALT; INT_COPRIME_SYM; INT_PRIME_COPRIME_EQ]);;
 833
 834 let INT_PRIME_DIVPROD = prove
 835  (`!p a b. int_prime(p) /\ p divides (a * b) ==> p divides a \/ p divides b`,
 836   ONCE_REWRITE_TAC[TAUT `a /\ b ==> c \/ d <=> a ==> (~c /\ ~d ==> ~b)`] THEN
 837   SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ] THEN INTEGER_TAC);;
 838
 839 let INT_PRIME_DIVPROD_EQ = prove
 840  (`!p a b. int_prime(p)
 841            ==> (p divides (a * b) <=> p divides a \/ p divides b)`,
 842   MESON_TAC[INT_PRIME_DIVPROD; INT_DIVIDES_LMUL; INT_DIVIDES_RMUL]);;
 843
 844 let INT_PRIME_DIVPOW = prove
 845  (`!n p x. int_prime(p) /\ p divides (x pow n) ==> p divides x`,
 846   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 847   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 848   ASM_SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ; INT_COPRIME_POW]);;
 849
 850 let INT_PRIME_DIVPOW_N = prove
 851  (`!n p x. int_prime p /\ p divides (x pow n) ==> (p pow n) divides (x pow n)`,
 852   MESON_TAC[INT_PRIME_DIVPOW; INT_DIVIDES_POW]);;
 853
 854 let INT_COPRIME_SOS = prove
 855  (`!x y. coprime(x,y) ==> coprime(x * y,x pow 2 + y pow 2)`,
 856   INTEGER_TAC);;
 857
 858 let INT_PRIME_IMP_NZ = prove
 859  (`!p. int_prime p ==> ~(p = &0)`,
 860   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_PRIME_GE_2) THEN
 861   INT_ARITH_TAC);;
 862
 863 let INT_DISTINCT_PRIME_COPRIME = prove
 864  (`!p q. int_prime p /\ int_prime q /\ ~(abs p = abs q) ==> coprime(p,q)`,
 865   REWRITE_TAC[GSYM INT_DIVIDES_ANTISYM_ABS] THEN
 866   MESON_TAC[INT_COPRIME_SYM; INT_PRIME_COPRIME_EQ]);;
 867
 868 let INT_PRIME_COPRIME_LT = prove
 869  (`!x p. int_prime p /\ &0 < abs x /\ abs x < abs p ==> coprime(x,p)`,
 870   ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN SIMP_TAC[INT_PRIME_COPRIME_EQ] THEN
 871   REPEAT GEN_TAC THEN STRIP_TAC THEN
 872   DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC);;
 873
 874 let INT_DIVIDES_PRIME_PRIME = prove
 875  (`!p q. int_prime p /\ int_prime q  ==> (p divides q <=> abs p = abs q)`,
 876   REPEAT STRIP_TAC THEN EQ_TAC THENL
 877    [ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 878     ASM_SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ; INT_DISTINCT_PRIME_COPRIME];
 879     SIMP_TAC[GSYM INT_DIVIDES_ANTISYM_ABS]]);;
 880
 881 let INT_COPRIME_POW_DIVPROD = prove
 882  (`!d a b. (d pow n) divides (a * b) /\ coprime(d,a) ==> (d pow n) divides b`,
 883   MESON_TAC[INT_COPRIME_DIVPROD; INT_COPRIME_POW; INT_COPRIME_SYM]);;
 884
 885 let INT_PRIME_COPRIME_CASES = prove
 886  (`!p a b. int_prime p /\ coprime(a,b) ==> coprime(p,a) \/ coprime(p,b)`,
 887   MESON_TAC[INT_COPRIME_PRIME; INT_PRIME_COPRIME_EQ]);;
 888
 889 let INT_PRIME_DIVPROD_POW = prove
 890  (`!n p a b. int_prime(p) /\ coprime(a,b) /\ (p pow n) divides (a * b)
 891              ==> (p pow n) divides a \/ (p pow n) divides b`,
 892   MESON_TAC[INT_COPRIME_POW_DIVPROD; INT_PRIME_COPRIME_CASES; INT_MUL_SYM]);;
 893
 894 let INT_DIVIDES_POW2_REV = prove
 895  (`!n a b. (a pow n) divides (b pow n) /\ ~(n = 0) ==> a divides b`,
 896   REPEAT GEN_TAC THEN ASM_CASES_TAC `gcd(a,b) = &0` THENL
 897    [ASM_MESON_TAC[INT_GCD_EQ_0; INT_DIVIDES_REFL]; ALL_TAC] THEN
 898   FIRST_ASSUM(MP_TAC o MATCH_MP INT_GCD_COPRIME_EXISTS) THEN
 899   STRIP_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 900   ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[INT_POW_MUL] THEN
 901   ASM_SIMP_TAC[INT_POW_EQ_0; INT_DIVIDES_RMUL2_EQ] THEN
 902   DISCH_THEN(MP_TAC o MATCH_MP (INTEGER_RULE
 903    `a divides b ==> coprime(a,b) ==> a divides &1`)) THEN
 904   ASM_SIMP_TAC[INT_COPRIME_POW2] THEN
 905   ASM_MESON_TAC[INT_DIVIDES_POW2; INT_DIVIDES_TRANS; INT_DIVIDES_1]);;
 906
 907 let INT_DIVIDES_POW2_EQ = prove
 908  (`!n a b. ~(n = 0) ==> ((a pow n) divides (b pow n) <=> a divides b)`,
 909   MESON_TAC[INT_DIVIDES_POW2_REV; INT_DIVIDES_POW]);;
 910
 911 let INT_POW_MUL_EXISTS = prove
 912  (`!m n p k. ~(m = &0) /\ m pow k * n = p pow k ==> ?q. n = q pow k`,
 913   REPEAT GEN_TAC THEN ASM_CASES_TAC `k = 0` THEN
 914   ASM_SIMP_TAC[INT_POW; INT_MUL_LID] THEN STRIP_TAC THEN
 915   MP_TAC(SPECL [`k:num`; `m:int`; `p:int`] INT_DIVIDES_POW2_REV) THEN
 916   ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
 917    [ASM_MESON_TAC[int_divides; INT_MUL_SYM]; ALL_TAC] THEN
 918   REWRITE_TAC[int_divides] THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN
 919   FIRST_X_ASSUM(MP_TAC o SYM) THEN
 920   ASM_SIMP_TAC[INT_POW_MUL; INT_EQ_MUL_LCANCEL; INT_POW_EQ_0] THEN
 921   MESON_TAC[]);;
 922
 923 let INT_COPRIME_POW_ABS = prove
 924  (`!n a b c. coprime(a,b) /\ a * b = c pow n
 925              ==> ?r s. abs a = r pow n /\ abs b = s pow n`,
 926   GEN_TAC THEN GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN
 927   GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN ASM_CASES_TAC `n = 0` THENL
 928    [ASM_REWRITE_TAC[INT_POW] THEN MESON_TAC[INT_ABS_MUL_1; INT_ABS_NUM];
 929     ALL_TAC] THEN
 930   MATCH_MP_TAC INT_PRIME_FACTOR_INDUCT THEN REPEAT CONJ_TAC THENL
 931    [REPEAT GEN_TAC THEN ASM_REWRITE_TAC[INT_POW_ZERO; INT_ENTIRE] THEN
 932     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC DISJ_CASES_TAC) THEN
 933     ASM_SIMP_TAC[INT_COPRIME_0; INT_DIVIDES_ONE_ABS; INT_ABS_NUM] THEN
 934     ASM_MESON_TAC[INT_POW_ONE; INT_POW_ZERO];
 935     REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `abs:int->int`) THEN
 936     SIMP_TAC[INT_POW_ONE; INT_ABS_NUM; INT_ABS_MUL_1] THEN
 937     MESON_TAC[INT_POW_ONE];
 938     REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `abs:int->int`) THEN
 939     SIMP_TAC[INT_POW_ONE; INT_ABS_POW; INT_ABS_NEG; INT_ABS_NUM;
 940              INT_ABS_MUL_1] THEN MESON_TAC[INT_POW_ONE];
 941     REWRITE_TAC[INT_POW_MUL] THEN REPEAT STRIP_TAC THEN
 942     SUBGOAL_THEN `p pow n divides a \/ p pow n divides b` MP_TAC THENL
 943      [ASM_MESON_TAC[INT_PRIME_DIVPROD_POW; int_divides]; ALL_TAC] THEN
 944     REWRITE_TAC[int_divides] THEN
 945     DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `d:int` SUBST_ALL_TAC)) THEN
 946     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INT_COPRIME_SYM]) THEN
 947     ASM_SIMP_TAC[INT_COPRIME_RMUL; INT_COPRIME_LMUL;
 948                  INT_COPRIME_LPOW; INT_COPRIME_RPOW] THEN
 949     STRIP_TAC THENL
 950      [FIRST_X_ASSUM(MP_TAC o SPECL [`b:int`; `d:int`]);
 951       FIRST_X_ASSUM(MP_TAC o SPECL [`d:int`; `a:int`])] THEN
 952     ASM_REWRITE_TAC[] THEN
 953     (ANTS_TAC THENL
 954       [MATCH_MP_TAC(INT_RING `!p. ~(p = &0) /\ a * p = b * p ==> a = b`) THEN
 955        EXISTS_TAC `p pow n` THEN
 956        ASM_SIMP_TAC[INT_POW_EQ_0; INT_PRIME_IMP_NZ] THEN
 957        FIRST_X_ASSUM(MP_TAC o SYM) THEN CONV_TAC INT_RING;
 958        STRIP_TAC THEN
 959        ASM_REWRITE_TAC[INT_ABS_POW; GSYM INT_POW_MUL; INT_ABS_MUL] THEN
 960        MESON_TAC[]])]);;
 961
 962 let INT_COPRIME_POW_ODD = prove
 963  (`!n a b c. ODD n /\ coprime(a,b) /\ a * b = c pow n
 964              ==> ?r s. a = r pow n /\ b = s pow n`,
 965   REPEAT STRIP_TAC THEN
 966   MP_TAC(SPECL [`n:num`; `a:int`; `b:int`; `c:int`] INT_COPRIME_POW_ABS) THEN
 967   ASM_REWRITE_TAC[INT_ABS] THEN
 968   REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN
 969   MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[INT_ABS] THEN
 970   ASM_MESON_TAC[INT_POW_NEG; INT_NEG_NEG; NOT_ODD]);;
 971
 972 let INT_DIVIDES_PRIME_POW_LE = prove
 973  (`!p q m n. int_prime p /\ int_prime q
 974              ==> ((p pow m) divides (q pow n) <=>
 975                   m = 0 \/ abs p = abs q /\ m <= n)`,
 976   REPEAT STRIP_TAC THEN ASM_CASES_TAC `m = 0` THEN
 977   ASM_REWRITE_TAC[INT_POW; INT_DIVIDES_1] THEN
 978   GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_LABS] THEN
 979   GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_RABS] THEN
 980   REWRITE_TAC[INT_ABS_POW] THEN EQ_TAC THENL
 981    [DISCH_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`);
 982     ALL_TAC] THEN
 983   ASM_MESON_TAC[INT_DIVIDES_POW_LE; INT_PRIME_GE_2; INT_PRIME_DIVPOW;
 984       INT_ABS_ABS; INT_PRIME_ABS; INT_DIVIDES_POW2; INT_DIVIDES_PRIME_PRIME]);;
 985
 986 let INT_EQ_PRIME_POW_ABS = prove
 987  (`!p q m n. int_prime p /\ int_prime q
 988              ==> (abs p pow m = abs q pow n <=>
 989                   m = 0 /\ n = 0 \/ abs p = abs q /\ m = n)`,
 990   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INT_ABS_POW] THEN
 991   GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_ANTISYM_ABS] THEN
 992   ASM_SIMP_TAC[INT_DIVIDES_PRIME_POW_LE; INT_PRIME_ABS] THEN
 993   ASM_CASES_TAC `abs p = abs q` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);;
 994
 995 let INT_EQ_PRIME_POW_POS = prove
 996  (`!p q m n. int_prime p /\ int_prime q /\ &0 <= p /\ &0 <= q
 997              ==> (p pow m = q pow n <=>
 998                   m = 0 /\ n = 0 \/ p = q /\ m = n)`,
 999   REPEAT STRIP_TAC THEN
1000   MP_TAC(SPECL [`p:int`; `q:int`; `m:num`; `n:num`] INT_EQ_PRIME_POW_ABS) THEN
1001   ASM_SIMP_TAC[INT_ABS]);;
1002
1003 let INT_DIVIDES_FACT_PRIME = prove
1004  (`!p. int_prime p ==> !n. p divides &(FACT n) <=> abs p <= &n`,
1005   GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT] THENL
1006    [REWRITE_TAC[INT_ARITH `abs x <= &0 <=> x = &0`] THEN
1007     ASM_MESON_TAC[INT_DIVIDES_ONE; INT_PRIME_NEG; INT_PRIME_0; INT_PRIME_1];
1008     ASM_SIMP_TAC[INT_PRIME_DIVPROD_EQ; GSYM INT_OF_NUM_MUL] THEN
1009     REWRITE_TAC[GSYM INT_OF_NUM_SUC] THEN
1010     ASM_MESON_TAC[INT_DIVIDES_LE; INT_ARITH `x <= n ==> x <= n + &1`;
1011                   INT_DIVIDES_REFL; INT_DIVIDES_LABS;
1012                   INT_ARITH `p <= n + &1 ==> p <= n \/ p = n + &1`;
1013                   INT_ARITH `~(&n + &1 = &0)`;
1014                   INT_ARITH `abs(&n + &1) = &n + &1`]]);;