Library/pocklington.ml

   1 (* ========================================================================= *)
   2 (* HOL primality proving via Pocklington-optimized  Pratt certificates.      *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/iter.ml";;
   6 needs "Library/prime.ml";;
   7
   8 prioritize_num();;
   9
  10 let num_0 = Int 0;;
  11 let num_1 = Int 1;;
  12 let num_2 = Int 2;;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (* Mostly for compatibility. Should eliminate this eventually.               *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let nat_mod_lemma = prove
  19  (`!x y n:num. (x == y) (mod n) /\ y <= x ==> ?q. x = y + n * q`,
  20   REPEAT GEN_TAC THEN REWRITE_TAC[num_congruent] THEN
  21   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
  22   ONCE_REWRITE_TAC
  23    [INTEGER_RULE `(x == y) (mod &n) <=> &n divides (x - y)`] THEN
  24   ASM_SIMP_TAC[INT_OF_NUM_SUB;
  25                ARITH_RULE `x <= y ==> (y:num = x + d <=> y - x = d)`] THEN
  26   REWRITE_TAC[GSYM num_divides; divides]);;
  27
  28 let nat_mod = prove
  29  (`!x y n:num. (mod n) x y <=> ?q1 q2. x + n * q1 = y + n * q2`,
  30   REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM cong] THEN
  31   EQ_TAC THENL [ALL_TAC; NUMBER_TAC] THEN
  32   MP_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THEN
  33   REWRITE_TAC[TAUT `a \/ b ==> c ==> d <=> (c /\ b) \/ (c /\ a) ==> d`] THEN
  34   DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
  35    [ALL_TAC;
  36     ONCE_REWRITE_TAC[NUMBER_RULE
  37       `(x:num == y) (mod n) <=> (y == x) (mod n)`]] THEN
  38   MESON_TAC[nat_mod_lemma; ARITH_RULE `x + y * 0 = x`]);;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* Lemmas about previously defined terms.                                    *)
  42 (* ------------------------------------------------------------------------- *)
  43
  44 let PRIME = prove
  45  (`!p. prime p <=> ~(p = 0) /\ ~(p = 1) /\ !m. 0 < m /\ m < p ==> coprime(p,m)`,
  46   GEN_TAC THEN ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
  47   ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[PRIME_1] THEN
  48   EQ_TAC THENL
  49    [DISCH_THEN(MP_TAC o MATCH_MP PRIME_COPRIME) THEN
  50     DISCH_TAC THEN X_GEN_TAC `m:num` THEN STRIP_TAC THEN
  51     FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
  52     STRIP_TAC THEN ASM_REWRITE_TAC[COPRIME_1] THEN
  53     ASM_MESON_TAC[NOT_LT; LT_REFL; DIVIDES_LE]; ALL_TAC] THEN
  54   FIRST_ASSUM(X_CHOOSE_THEN `q:num` MP_TAC o MATCH_MP PRIME_FACTOR) THEN
  55   REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `q:num`) THEN
  56   SUBGOAL_THEN `~(coprime(p,q))` (fun th -> REWRITE_TAC[th]) THENL
  57    [REWRITE_TAC[coprime; NOT_FORALL_THM] THEN
  58     EXISTS_TAC `q:num` THEN ASM_REWRITE_TAC[DIVIDES_REFL] THEN
  59     ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
  60   FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
  61   ASM_REWRITE_TAC[LT_LE; LE_0] THEN
  62   ASM_CASES_TAC `p:num = q` THEN ASM_REWRITE_TAC[] THEN
  63   SIMP_TAC[] THEN DISCH_TAC THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
  64   ASM_MESON_TAC[DIVIDES_ZERO]);;
  65
  66 let FINITE_NUMBER_SEGMENT = prove
  67  (`!n. { m | 0 < m /\ m < n } HAS_SIZE (n - 1)`,
  68   INDUCT_TAC THENL
  69    [SUBGOAL_THEN `{m | 0 < m /\ m < 0} = EMPTY` SUBST1_TAC THENL
  70      [REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY; LT]; ALL_TAC] THEN
  71     REWRITE_TAC[HAS_SIZE; FINITE_RULES; CARD_CLAUSES] THEN
  72     CONV_TAC NUM_REDUCE_CONV;
  73     ASM_CASES_TAC `n = 0` THENL
  74      [SUBGOAL_THEN `{m | 0 < m /\ m < SUC n} = EMPTY` SUBST1_TAC THENL
  75        [ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
  76         ARITH_TAC; ALL_TAC] THEN
  77       ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN
  78       REWRITE_TAC[HAS_SIZE_0];
  79       SUBGOAL_THEN `{m | 0 < m /\ m < SUC n} = n INSERT {m | 0 < m /\ m < n}`
  80       SUBST1_TAC THENL
  81        [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT] THEN
  82         UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  83       UNDISCH_TAC `~(n = 0)` THEN
  84       POP_ASSUM MP_TAC THEN
  85       SIMP_TAC[FINITE_RULES; HAS_SIZE; CARD_CLAUSES] THEN
  86       DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM; LT_REFL] THEN
  87       ARITH_TAC]]);;
  88
  89 let COPRIME_MOD = prove
  90  (`!a n. ~(n = 0) ==> (coprime(a MOD n,n) <=> coprime(a,n))`,
  91   REPEAT STRIP_TAC THEN
  92   FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV)
  93    [MATCH_MP DIVISION th]) THEN REWRITE_TAC[coprime] THEN
  94   AP_TERM_TAC THEN ABS_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  95   MESON_TAC[DIVIDES_ADD; DIVIDES_ADD_REVR; DIVIDES_ADD_REVL;
  96             DIVIDES_LMUL; DIVIDES_RMUL]);;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* Congruences.                                                              *)
 100 (* ------------------------------------------------------------------------- *)
 101
 102 let CONG = prove
 103  (`!x y n. ~(n = 0) ==> ((x == y) (mod n) <=> (x MOD n = y MOD n))`,
 104   REWRITE_TAC[cong; nat_mod] THEN
 105   REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL
 106    [ASM_CASES_TAC `x <= y` THENL
 107      [CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `q1 - q2`;
 108       MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `q2 - q1`] THEN
 109     REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN
 110     POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN ARITH_TAC;
 111     MAP_EVERY EXISTS_TAC [`y DIV n`; `x DIV n`] THEN
 112     UNDISCH_TAC `x MOD n = y MOD n` THEN
 113     MATCH_MP_TAC(ARITH_RULE
 114      `(y = dy + my) /\ (x = dx + mx) ==> (mx = my) ==> (x + dy = y + dx)`) THEN
 115     ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_SIMP_TAC[DIVISION]]);;
 116
 117 let CONG_MOD_0 = prove
 118  (`!x y. (x == y) (mod 0) <=> (x = y)`,
 119   NUMBER_TAC);;
 120
 121 let CONG_MOD_1 = prove
 122  (`!x y. (x == y) (mod 1)`,
 123   NUMBER_TAC);;
 124
 125 let CONG_0 = prove
 126  (`!x n. ((x == 0) (mod n) <=> n divides x)`,
 127   NUMBER_TAC);;
 128
 129 let CONG_SUB_CASES = prove
 130  (`!x y n. (x == y) (mod n) <=>
 131            if x <= y then (y - x == 0) (mod n)
 132            else (x - y == 0) (mod n)`,
 133   REPEAT GEN_TAC THEN REWRITE_TAC[cong; nat_mod] THEN
 134   COND_CASES_TAC THENL
 135    [GEN_REWRITE_TAC LAND_CONV [SWAP_EXISTS_THM]; ALL_TAC] THEN
 136   REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
 137   POP_ASSUM MP_TAC THEN ARITH_TAC);;
 138
 139 let CONG_CASES = prove
 140  (`!x y n. (x == y) (mod n) <=> (?q. x = q * n + y) \/ (?q. y = q * n + x)`,
 141   REPEAT GEN_TAC THEN EQ_TAC THENL
 142    [ALL_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUMBER_TAC] THEN
 143   REWRITE_TAC[cong; nat_mod; LEFT_IMP_EXISTS_THM] THEN
 144   MAP_EVERY X_GEN_TAC [`q1:num`; `q2:num`] THEN
 145   DISCH_THEN(MP_TAC o MATCH_MP(ARITH_RULE
 146    `x + a = y + b ==> x = (b - a) + y \/ y = (a - b) + x`)) THEN
 147   REWRITE_TAC[GSYM LEFT_SUB_DISTRIB] THEN MESON_TAC[MULT_SYM]);;
 148
 149 let CONG_MULT_LCANCEL = prove
 150  (`!a n x y. coprime(a,n) /\ (a * x == a * y) (mod n) ==> (x == y) (mod n)`,
 151   NUMBER_TAC);;
 152
 153 let CONG_MULT_RCANCEL = prove
 154  (`!a n x y. coprime(a,n) /\ (x * a == y * a) (mod n) ==> (x == y) (mod n)`,
 155   NUMBER_TAC);;
 156
 157 let CONG_REFL = prove
 158  (`!x n. (x == x) (mod n)`,
 159   NUMBER_TAC);;
 160
 161 let EQ_IMP_CONG = prove
 162  (`!a b n. a = b ==> (a == b) (mod n)`,
 163   SIMP_TAC[CONG_REFL]);;
 164
 165 let CONG_SYM = prove
 166  (`!x y n. (x == y) (mod n) <=> (y == x) (mod n)`,
 167   NUMBER_TAC);;
 168
 169 let CONG_TRANS = prove
 170  (`!x y z n. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`,
 171   NUMBER_TAC);;
 172
 173 let CONG_ADD = prove
 174  (`!x x' y y'.
 175      (x == x') (mod n) /\ (y == y') (mod n) ==> (x + y == x' + y') (mod n)`,
 176   NUMBER_TAC);;
 177
 178 let CONG_MULT = prove
 179  (`!x x' y y'.
 180      (x == x') (mod n) /\ (y == y') (mod n) ==> (x * y == x' * y') (mod n)`,
 181   NUMBER_TAC);;
 182
 183 let CONG_EXP = prove
 184  (`!n k x y. (x == y) (mod n) ==> (x EXP k == y EXP k) (mod n)`,
 185   GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[CONG_MULT; EXP; CONG_REFL]);;
 186
 187 let CONG_SUB = prove
 188  (`!x x' y y'.
 189      (x == x') (mod n) /\ (y == y') (mod n) /\ y <= x /\ y' <= x'
 190      ==> (x - y == x' - y') (mod n)`,
 191   REPEAT GEN_TAC THEN REWRITE_TAC[cong; nat_mod] THEN
 192   REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
 193   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN REPEAT GEN_TAC THEN
 194   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
 195    `(x + a = x' + a') /\ (y + b = y' + b') /\ y <= x /\ y' <= x'
 196     ==> ((x - y) + (a + b') = (x' - y') + (a' + b))`)) THEN
 197   REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN MESON_TAC[]);;
 198
 199 let CONG_MULT_LCANCEL_EQ = prove
 200  (`!a n x y. coprime(a,n) ==> ((a * x == a * y) (mod n) <=> (x == y) (mod n))`,
 201   NUMBER_TAC);;
 202
 203 let CONG_MULT_RCANCEL_EQ = prove
 204  (`!a n x y. coprime(a,n) ==> ((x * a == y * a) (mod n) <=> (x == y) (mod n))`,
 205   NUMBER_TAC);;
 206
 207 let CONG_ADD_LCANCEL_EQ = prove
 208  (`!a n x y. (a + x == a + y) (mod n) <=> (x == y) (mod n)`,
 209   NUMBER_TAC);;
 210
 211 let CONG_ADD_RCANCEL_EQ = prove
 212  (`!a n x y. (x + a == y + a) (mod n) <=> (x == y) (mod n)`,
 213   NUMBER_TAC);;
 214
 215 let CONG_ADD_RCANCEL = prove
 216  (`!a n x y. (x + a == y + a) (mod n) ==> (x == y) (mod n)`,
 217   NUMBER_TAC);;
 218
 219 let CONG_ADD_LCANCEL = prove
 220  (`!a n x y. (a + x == a + y) (mod n) ==> (x == y) (mod n)`,
 221   NUMBER_TAC);;
 222
 223 let CONG_ADD_LCANCEL_EQ_0 = prove
 224  (`!a n x y. (a + x == a) (mod n) <=> (x == 0) (mod n)`,
 225   NUMBER_TAC);;
 226
 227 let CONG_ADD_RCANCEL_EQ_0 = prove
 228  (`!a n x y. (x + a == a) (mod n) <=> (x == 0) (mod n)`,
 229   NUMBER_TAC);;
 230
 231 let CONG_IMP_EQ = prove
 232  (`!x y n. x < n /\ y < n /\ (x == y) (mod n) ==> x = y`,
 233   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[LT] THEN
 234   ASM_MESON_TAC[CONG; MOD_LT]);;
 235
 236 let CONG_DIVIDES_MODULUS = prove
 237  (`!x y m n. (x == y) (mod m) /\ n divides m ==> (x == y) (mod n)`,
 238   NUMBER_TAC);;
 239
 240 let CONG_0_DIVIDES = prove
 241  (`!n x. (x == 0) (mod n) <=> n divides x`,
 242   NUMBER_TAC);;
 243
 244 let CONG_1_DIVIDES = prove
 245  (`!n x. (x == 1) (mod n) ==> n divides (x - 1)`,
 246   REPEAT GEN_TAC THEN REWRITE_TAC[divides; cong; nat_mod] THEN
 247   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN REPEAT GEN_TAC THEN
 248   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
 249    `(x + q1 = 1 + q2) ==> ~(x = 0) ==> (x - 1 = q2 - q1)`)) THEN
 250   ASM_CASES_TAC `x = 0` THEN
 251   ASM_REWRITE_TAC[ARITH; GSYM LEFT_SUB_DISTRIB] THEN
 252   ASM_MESON_TAC[MULT_CLAUSES]);;
 253
 254 let CONG_DIVIDES = prove
 255  (`!x y n. (x == y) (mod n) ==> (n divides x <=> n divides y)`,
 256   NUMBER_TAC);;
 257
 258 let CONG_COPRIME = prove
 259  (`!x y n. (x == y) (mod n) ==> (coprime(n,x) <=> coprime(n,y))`,
 260   NUMBER_TAC);;
 261
 262 let CONG_MOD = prove
 263  (`!a n. ~(n = 0) ==> (a MOD n == a) (mod n)`,
 264   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN
 265   DISCH_THEN(MP_TAC o SPEC `a:num`) THEN
 266   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 267   DISCH_THEN(fun th -> GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV) [th]) THEN
 268   REWRITE_TAC[cong; nat_mod] THEN
 269   MAP_EVERY EXISTS_TAC [`a DIV n`; `0`] THEN
 270   REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; ADD_AC; MULT_AC]);;
 271
 272 let MOD_MULT_CONG = prove
 273  (`!a b x y. ~(a = 0) /\ ~(b = 0)
 274              ==> ((x MOD (a * b) == y) (mod a) <=> (x == y) (mod a))`,
 275   REPEAT STRIP_TAC THEN SUBGOAL_THEN `(x MOD (a * b) == x) (mod a)`
 276    (fun th -> MESON_TAC[th; CONG_TRANS; CONG_SYM]) THEN
 277   MATCH_MP_TAC CONG_DIVIDES_MODULUS THEN EXISTS_TAC `a * b` THEN
 278   ASM_SIMP_TAC[CONG_MOD; MULT_EQ_0; DIVIDES_RMUL; DIVIDES_REFL]);;
 279
 280 let CONG_MOD_MULT = prove
 281  (`!x y m n. (x == y) (mod n) /\ m divides n ==> (x == y) (mod m)`,
 282   NUMBER_TAC);;
 283
 284 let CONG_LMOD = prove
 285  (`!x y n. ~(n = 0) ==> ((x MOD n == y) (mod n) <=> (x == y) (mod n))`,
 286   MESON_TAC[CONG_MOD; CONG_TRANS; CONG_SYM]);;
 287
 288 let CONG_RMOD = prove
 289  (`!x y n. ~(n = 0) ==> ((x == y MOD n) (mod n) <=> (x == y) (mod n))`,
 290   MESON_TAC[CONG_MOD; CONG_TRANS; CONG_SYM]);;
 291
 292 let CONG_MOD_LT = prove
 293  (`!y. y < n ==> (x MOD n = y <=> (x == y) (mod n))`,
 294   MESON_TAC[MOD_LT; CONG; LT]);;
 295
 296 (* ------------------------------------------------------------------------- *)
 297 (* Some things when we know more about the order.                            *)
 298 (* ------------------------------------------------------------------------- *)
 299
 300 let CONG_LT = prove
 301  (`!x y n. y < n ==> ((x == y) (mod n) <=> ?d. x = d * n + y)`,
 302   REWRITE_TAC[GSYM INT_OF_NUM_EQ; GSYM INT_OF_NUM_LT;
 303               GSYM INT_OF_NUM_ADD; GSYM INT_OF_NUM_MUL] THEN
 304   REWRITE_TAC[num_congruent; int_congruent] THEN
 305   REWRITE_TAC[INT_ARITH `x = m * n + y <=> x - y:int = n * m`] THEN
 306   REPEAT STRIP_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 307   DISCH_THEN(X_CHOOSE_TAC `d:int`) THEN
 308   DISJ_CASES_TAC(SPEC `d:int` INT_IMAGE) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 309   FIRST_X_ASSUM(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
 310   FIRST_X_ASSUM(SUBST_ALL_TAC o MATCH_MP (INT_ARITH
 311    `x - y:int = n * --m ==> y = x + n * m`)) THEN
 312   POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(ARITH_RULE `m = 0 \/ 1 <= m`) THEN
 313   ASM_REWRITE_TAC[INT_MUL_RZERO; INT_ARITH `x - (x + a):int = --a`] THENL
 314    [STRIP_TAC THEN EXISTS_TAC `0` THEN INT_ARITH_TAC;
 315     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 316     DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST1_TAC) THEN
 317     REWRITE_TAC[INT_OF_NUM_ADD; INT_OF_NUM_MUL; INT_OF_NUM_LT] THEN
 318     ARITH_TAC]);;
 319
 320 let CONG_LE = prove
 321  (`!x y n. y <= x ==> ((x == y) (mod n) <=> ?q. x = q * n + y)`,
 322   ONCE_REWRITE_TAC[CONG_SYM] THEN ONCE_REWRITE_TAC[CONG_SUB_CASES] THEN
 323   SIMP_TAC[ARITH_RULE `y <= x ==> (x = a + y <=> x - y = a)`] THEN
 324   REWRITE_TAC[CONG_0; divides] THEN MESON_TAC[MULT_SYM]);;
 325
 326 let CONG_TO_1 = prove
 327  (`!a n. (a == 1) (mod n) <=> a = 0 /\ n = 1 \/ ?m. a = 1 + m * n`,
 328   REPEAT STRIP_TAC THEN
 329   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[CONG_MOD_1] THENL
 330    [MESON_TAC[ARITH_RULE `n = 0 \/ n = 1 + (n - 1) * 1`]; ALL_TAC] THEN
 331   DISJ_CASES_TAC(ARITH_RULE `a = 0 \/ ~(a = 0) /\ 1 <= a`) THEN
 332   ASM_SIMP_TAC[CONG_LE] THENL [ALL_TAC; MESON_TAC[ADD_SYM; MULT_SYM]] THEN
 333   ASM_MESON_TAC[CONG_SYM; CONG_0; DIVIDES_ONE; ARITH_RULE `~(0 = 1 + a)`]);;
 334
 335 (* ------------------------------------------------------------------------- *)
 336 (* In particular two common cases.                                           *)
 337 (* ------------------------------------------------------------------------- *)
 338
 339 let EVEN_MOD_2 = prove
 340  (`EVEN n <=> (n == 0) (mod 2)`,
 341   SIMP_TAC[EVEN_EXISTS; CONG_LT; ARITH; ADD_CLAUSES; MULT_AC]);;
 342
 343 let ODD_MOD_2 = prove
 344  (`ODD n <=> (n == 1) (mod 2)`,
 345   SIMP_TAC[ODD_EXISTS; CONG_LT; ARITH; ADD_CLAUSES; ADD1; MULT_AC]);;
 346
 347 (* ------------------------------------------------------------------------- *)
 348 (* Conversion to evaluate congruences.                                       *)
 349 (* ------------------------------------------------------------------------- *)
 350
 351 let CONG_CONV =
 352   let pth = prove
 353    (`(x == y) (mod n) <=>
 354      if x <= y then n divides (y - x) else n divides (x - y)`,
 355     ONCE_REWRITE_TAC[CONG_SUB_CASES] THEN REWRITE_TAC[CONG_0_DIVIDES]) in
 356   GEN_REWRITE_CONV I [pth] THENC
 357   RATOR_CONV(LAND_CONV NUM_LE_CONV) THENC
 358   GEN_REWRITE_CONV I [COND_CLAUSES] THENC
 359   RAND_CONV NUM_SUB_CONV THENC
 360   DIVIDES_CONV;;
 361
 362 (* ------------------------------------------------------------------------- *)
 363 (* Some basic theorems about solving congruences.                            *)
 364 (* ------------------------------------------------------------------------- *)
 365
 366 let CONG_SOLVE = prove
 367  (`!a b n. coprime(a,n) ==> ?x. (a * x == b) (mod n)`,
 368   REPEAT STRIP_TAC THEN
 369   MP_TAC(SPECL [`a:num`; `n:num`] BEZOUT_ADD_STRONG) THEN
 370   ASM_CASES_TAC `a = 0` THENL
 371    [ASM_MESON_TAC[COPRIME_0; COPRIME_SYM; CONG_MOD_1]; ALL_TAC] THEN
 372   ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC LAND_CONV [SWAP_EXISTS_THM] THEN
 373   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 374   MAP_EVERY X_GEN_TAC [`x:num`; `d:num`; `y:num`] THEN
 375   ASM_CASES_TAC `d = 1` THEN ASM_REWRITE_TAC[] THENL
 376    [ALL_TAC; ASM_MESON_TAC[COPRIME]] THEN
 377   STRIP_TAC THEN EXISTS_TAC `x * b:num` THEN ASM_REWRITE_TAC[MULT_ASSOC] THEN
 378   REWRITE_TAC[RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
 379   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `b = 0 + b`] THEN
 380   MATCH_MP_TAC CONG_ADD THEN REWRITE_TAC[CONG_REFL] THEN
 381   REWRITE_TAC[CONG_0; GSYM MULT_ASSOC] THEN MESON_TAC[divides]);;
 382
 383 let CONG_SOLVE_UNIQUE = prove
 384  (`!a b n. coprime(a,n) /\ ~(n = 0) ==> ?!x. x < n /\ (a * x == b) (mod n)`,
 385   REPEAT STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
 386   MP_TAC(SPECL [`a:num`; `b:num`; `n:num`] CONG_SOLVE) THEN
 387   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `x:num`) THEN
 388   EXISTS_TAC `x MOD n` THEN
 389   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
 390    [ASM_SIMP_TAC[DIVISION] THEN MATCH_MP_TAC CONG_TRANS THEN
 391     EXISTS_TAC `a * x:num` THEN ASM_REWRITE_TAC[] THEN
 392     MATCH_MP_TAC CONG_MULT THEN REWRITE_TAC[CONG_REFL] THEN
 393     ASM_SIMP_TAC[CONG; MOD_MOD_REFL];
 394     ALL_TAC] THEN
 395   STRIP_TAC THEN X_GEN_TAC `y:num` THEN STRIP_TAC THEN
 396   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `y MOD n` THEN CONJ_TAC THENL
 397    [ASM_SIMP_TAC[MOD_LT]; ALL_TAC] THEN
 398   ASM_SIMP_TAC[GSYM CONG] THEN MATCH_MP_TAC CONG_MULT_LCANCEL THEN
 399   EXISTS_TAC `a:num` THEN ASM_MESON_TAC[CONG_TRANS; CONG_SYM]);;
 400
 401 let CONG_SOLVE_UNIQUE_NONTRIVIAL = prove
 402  (`!a p x. prime p /\ coprime(p,a) /\ 0 < x /\ x < p
 403            ==> ?!y. 0 < y /\ y < p /\ (x * y == a) (mod p)`,
 404   REPEAT GEN_TAC THEN ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
 405   REPEAT STRIP_TAC THEN SUBGOAL_THEN `1 < p` ASSUME_TAC THENL
 406    [REWRITE_TAC[ARITH_RULE `1 < p <=> ~(p = 0) /\ ~(p = 1)`] THEN
 407     ASM_MESON_TAC[PRIME_1];
 408     ALL_TAC] THEN
 409   MP_TAC(SPECL [`x:num`; `a:num`; `p:num`] CONG_SOLVE_UNIQUE) THEN
 410   ANTS_TAC THENL
 411    [CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[PRIME_0]] THEN
 412     ONCE_REWRITE_TAC[COPRIME_SYM] THEN
 413     MP_TAC(SPECL [`x:num`; `p:num`] PRIME_COPRIME) THEN
 414     ASM_CASES_TAC `x = 1` THEN ASM_REWRITE_TAC[COPRIME_1] THEN
 415     ASM_MESON_TAC[COPRIME_SYM; NOT_LT; DIVIDES_LE; LT_REFL];
 416     ALL_TAC] THEN
 417   MATCH_MP_TAC EQ_IMP THEN
 418   AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 419   X_GEN_TAC `r:num` THEN REWRITE_TAC[] THEN
 420   REWRITE_TAC[ARITH_RULE `0 < r <=> ~(r = 0)`] THEN
 421   ASM_CASES_TAC `r = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
 422   ASM_SIMP_TAC[ARITH_RULE `~(p = 0) ==> 0 < p`] THEN
 423   ONCE_REWRITE_TAC[CONG_SYM] THEN REWRITE_TAC[CONG_0] THEN
 424   ASM_MESON_TAC[DIVIDES_REFL; PRIME_1; coprime]);;
 425
 426 let CONG_UNIQUE_INVERSE_PRIME = prove
 427  (`!p x. prime p /\ 0 < x /\ x < p
 428          ==> ?!y. 0 < y /\ y < p /\ (x * y == 1) (mod p)`,
 429   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_SOLVE_UNIQUE_NONTRIVIAL THEN
 430   ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[COPRIME_1; COPRIME_SYM]);;
 431
 432 (* ------------------------------------------------------------------------- *)
 433 (* Forms of the Chinese remainder theorem.                                   *)
 434 (* ------------------------------------------------------------------------- *)
 435
 436 let CONG_CHINESE = prove
 437  (`coprime(a,b) /\ (x == y) (mod a) /\ (x == y) (mod b)
 438    ==> (x == y) (mod (a * b))`,
 439   ONCE_REWRITE_TAC[CONG_SUB_CASES] THEN MESON_TAC[CONG_0; DIVIDES_MUL]);;
 440
 441 let CHINESE_REMAINDER_UNIQUE = prove
 442  (`!a b m n.
 443         coprime(a,b) /\ ~(a = 0) /\ ~(b = 0)
 444         ==> ?!x. x < a * b /\ (x == m) (mod a) /\ (x == n) (mod b)`,
 445   REPEAT STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL
 446    [MP_TAC(SPECL [`a:num`; `b:num`; `m:num`; `n:num`] CHINESE_REMAINDER) THEN
 447     ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 448     MAP_EVERY X_GEN_TAC [`x:num`; `q1:num`; `q2:num`] THEN
 449     DISCH_TAC THEN EXISTS_TAC `x MOD (a * b)` THEN
 450     CONJ_TAC THENL [ASM_MESON_TAC[DIVISION; MULT_EQ_0]; ALL_TAC] THEN
 451     GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 452     CONJ_TAC THENL
 453      [FIRST_X_ASSUM(SUBST1_TAC o CONJUNCT1);
 454       FIRST_X_ASSUM(SUBST1_TAC o CONJUNCT2)] THEN
 455     ASM_SIMP_TAC[MOD_MULT_CONG] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
 456     REWRITE_TAC[cong; nat_mod; GSYM ADD_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 457     MESON_TAC[];
 458     REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_IMP_EQ THEN
 459     EXISTS_TAC `a * b` THEN ASM_REWRITE_TAC[] THEN
 460     ASM_MESON_TAC[CONG_CHINESE; CONG_SYM; CONG_TRANS]]);;
 461
 462 let CHINESE_REMAINDER_COPRIME_UNIQUE = prove
 463  (`!a b m n.
 464         coprime(a,b) /\ ~(a = 0) /\ ~(b = 0) /\ coprime(m,a) /\ coprime(n,b)
 465         ==> ?!x. coprime(x,a * b) /\ x < a * b /\
 466                  (x == m) (mod a) /\ (x == n) (mod b)`,
 467   REPEAT STRIP_TAC THEN MP_TAC
 468    (SPECL [`a:num`; `b:num`; `m:num`; `n:num`] CHINESE_REMAINDER_UNIQUE) THEN
 469   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(MESON[]
 470    `(!x. P(x) ==> Q(x)) ==> (?!x. P x) ==> ?!x. Q(x) /\ P(x)`) THEN
 471   ASM_SIMP_TAC[CHINESE_REMAINDER_UNIQUE] THEN
 472   ASM_MESON_TAC[CONG_COPRIME; COPRIME_SYM; COPRIME_MUL]);;
 473
 474 let CONG_CHINESE_EQ = prove
 475  (`!a b x y.
 476      coprime(a,b)
 477      ==> ((x == y) (mod (a * b)) <=> (x == y) (mod a) /\ (x == y) (mod b))`,
 478   NUMBER_TAC);;
 479
 480 (* ------------------------------------------------------------------------- *)
 481 (* Euler totient function.                                                   *)
 482 (* ------------------------------------------------------------------------- *)
 483
 484 let phi = new_definition
 485   `phi(n) = CARD { m | 0 < m /\ m <= n /\ coprime(m,n) }`;;
 486
 487 let PHI_ALT = prove
 488  (`phi(n) = CARD { m | coprime(m,n) /\ m < n}`,
 489   REWRITE_TAC[phi] THEN
 490   ASM_CASES_TAC `n = 0` THENL
 491    [AP_TERM_TAC THEN
 492     ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 493     MESON_TAC[LT; NOT_LT];
 494     ALL_TAC] THEN
 495   ASM_CASES_TAC `n = 1` THENL
 496    [SUBGOAL_THEN
 497      `({m | 0 < m /\ m <= n /\ coprime (m,n)} = {1}) /\
 498       ({m | coprime (m,n) /\ m < n} = {0})`
 499      (CONJUNCTS_THEN SUBST1_TAC)
 500     THENL [ALL_TAC; SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY]] THEN
 501     ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN
 502     REWRITE_TAC[COPRIME_1] THEN REPEAT STRIP_TAC THEN ARITH_TAC;
 503     ALL_TAC] THEN
 504   AP_TERM_TAC THEN ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 505   X_GEN_TAC `m:num` THEN ASM_CASES_TAC `m = 0` THEN
 506   ASM_REWRITE_TAC[LT] THENL
 507    [ASM_MESON_TAC[COPRIME_0; COPRIME_SYM];
 508     ASM_MESON_TAC[LE_LT; COPRIME_REFL; LT_NZ]]);;
 509
 510 let PHI_FINITE_LEMMA = prove
 511  (`!P n. FINITE {m | coprime(m,n) /\ m < n}`,
 512   REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
 513   REWRITE_TAC[FINITE_NUMSEG; SUBSET; IN_NUMSEG; IN_ELIM_THM] THEN ARITH_TAC);;
 514
 515 let PHI_ANOTHER = prove
 516  (`!n. ~(n = 1) ==> (phi(n) = CARD {m | 0 < m /\ m < n /\ coprime(m,n)})`,
 517   REPEAT STRIP_TAC THEN REWRITE_TAC[phi] THEN
 518   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 519   ASM_MESON_TAC[LE_LT; COPRIME_REFL; COPRIME_1; LT_NZ]);;
 520
 521 let PHI_LIMIT = prove
 522  (`!n. phi(n) <= n`,
 523   GEN_TAC THEN REWRITE_TAC[PHI_ALT] THEN
 524   GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_LT] THEN
 525   MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[FINITE_NUMSEG_LT] THEN
 526   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 527
 528 let PHI_LIMIT_STRONG = prove
 529  (`!n. ~(n = 1) ==> phi(n) <= n - 1`,
 530   REPEAT STRIP_TAC THEN
 531   MP_TAC(SPEC `n:num` FINITE_NUMBER_SEGMENT) THEN
 532   ASM_SIMP_TAC[PHI_ANOTHER; HAS_SIZE] THEN
 533   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN
 534   MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[] THEN
 535   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 536
 537 let PHI_0 = prove
 538  (`phi 0 = 0`,
 539   MP_TAC(SPEC `0` PHI_LIMIT) THEN REWRITE_TAC[ARITH] THEN ARITH_TAC);;
 540
 541 let PHI_1 = prove
 542  (`phi 1 = 1`,
 543   REWRITE_TAC[PHI_ALT; COPRIME_1; CARD_NUMSEG_LT]);;
 544
 545 let PHI_LOWERBOUND_1_STRONG = prove
 546  (`!n. 1 <= n ==> 1 <= phi(n)`,
 547   REPEAT STRIP_TAC THEN
 548   SUBGOAL_THEN `1 = CARD {1}` SUBST1_TAC THENL
 549    [SIMP_TAC[CARD_CLAUSES; NOT_IN_EMPTY; FINITE_RULES; ARITH]; ALL_TAC] THEN
 550   REWRITE_TAC[phi] THEN MATCH_MP_TAC CARD_SUBSET THEN CONJ_TAC THENL
 551    [SIMP_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN
 552     REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_1] THEN
 553     GEN_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 554     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{b | b <= n}` THEN
 555     REWRITE_TAC[CARD_NUMSEG_LE; FINITE_NUMSEG_LE] THEN
 556     SIMP_TAC[SUBSET; IN_ELIM_THM]]);;
 557
 558 let PHI_LOWERBOUND_1 = prove
 559  (`!n. 2 <= n ==> 1 <= phi(n)`,
 560   MESON_TAC[PHI_LOWERBOUND_1_STRONG; LE_TRANS; ARITH_RULE `1 <= 2`]);;
 561
 562 let PHI_LOWERBOUND_2 = prove
 563  (`!n. 3 <= n ==> 2 <= phi(n)`,
 564   REPEAT STRIP_TAC THEN
 565   SUBGOAL_THEN `2 = CARD {1,(n-1)}` SUBST1_TAC THENL
 566    [SIMP_TAC[CARD_CLAUSES; IN_INSERT; NOT_IN_EMPTY; FINITE_RULES; ARITH] THEN
 567     ASM_SIMP_TAC[ARITH_RULE `3 <= n ==> ~(1 = n - 1)`]; ALL_TAC] THEN
 568   REWRITE_TAC[phi] THEN MATCH_MP_TAC CARD_SUBSET THEN CONJ_TAC THENL
 569    [SIMP_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN
 570     GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 571     REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_1] THEN
 572     ASM_SIMP_TAC[ARITH;
 573                ARITH_RULE `3 <= n ==> 0 < n - 1 /\ n - 1 <= n /\ 1 <= n`] THEN
 574     REWRITE_TAC[coprime] THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
 575     MP_TAC(SPEC `n:num` COPRIME_1) THEN REWRITE_TAC[coprime] THEN
 576     DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 577     SUBGOAL_THEN `1 = n - (n - 1)` SUBST1_TAC THENL
 578      [UNDISCH_TAC `3 <= n` THEN ARITH_TAC;
 579       ASM_SIMP_TAC[DIVIDES_SUB]];
 580     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{b | b <= n}` THEN
 581     REWRITE_TAC[CARD_NUMSEG_LE; FINITE_NUMSEG_LE] THEN
 582     SIMP_TAC[SUBSET; IN_ELIM_THM]]);;
 583
 584 let PHI_EQ_0 = prove
 585  (`!n. phi n = 0 <=> n = 0`,
 586   GEN_TAC THEN EQ_TAC THEN SIMP_TAC[PHI_0] THEN
 587   MP_TAC(SPEC `n:num` PHI_LOWERBOUND_1_STRONG) THEN ARITH_TAC);;
 588
 589 (* ------------------------------------------------------------------------- *)
 590 (* Value on primes and prime powers.                                         *)
 591 (* ------------------------------------------------------------------------- *)
 592
 593 let PHI_PRIME_EQ = prove
 594  (`!n. (phi n = n - 1) /\ ~(n = 0) /\ ~(n = 1) <=> prime n`,
 595   GEN_TAC THEN REWRITE_TAC[PRIME] THEN
 596   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
 597   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[PHI_1; ARITH] THEN
 598   MP_TAC(SPEC `n:num` FINITE_NUMBER_SEGMENT) THEN
 599   ASM_SIMP_TAC[PHI_ANOTHER; HAS_SIZE] THEN
 600   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN
 601   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 602    `{m | 0 < m /\ m < n /\ coprime (m,n)} = {m | 0 < m /\ m < n}` THEN
 603   CONJ_TAC THENL
 604    [ALL_TAC;
 605     REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 606     AP_TERM_TAC THEN ABS_TAC THEN
 607     REWRITE_TAC[COPRIME_SYM] THEN CONV_TAC TAUT] THEN
 608   EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
 609   MATCH_MP_TAC CARD_SUBSET_EQ THEN ASM_REWRITE_TAC[] THEN
 610   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 611
 612 let PHI_PRIME = prove
 613  (`!p. prime p ==> phi p = p - 1`,
 614   MESON_TAC[PHI_PRIME_EQ]);;
 615
 616 let PHI_PRIMEPOW_SUC = prove
 617  (`!p k. prime(p) ==> phi(p EXP (k + 1)) = p EXP (k + 1) - p EXP k`,
 618   REPEAT STRIP_TAC THEN
 619   ASM_SIMP_TAC[PHI_ALT;  COPRIME_PRIMEPOW; ADD_EQ_0; ARITH] THEN
 620   REWRITE_TAC[SET_RULE
 621    `{n | ~(P n) /\ Q n} = {n | Q n} DIFF {n | P n /\ Q n}`] THEN
 622   SIMP_TAC[FINITE_NUMSEG_LT; SUBSET; IN_ELIM_THM; CARD_DIFF] THEN
 623   REWRITE_TAC[CARD_NUMSEG_LT] THEN AP_TERM_TAC THEN
 624   SUBGOAL_THEN `{m | p divides m /\ m < p EXP (k + 1)} =
 625                 IMAGE (\x. p * x) {m | m < p EXP k}`
 626    (fun th -> ASM_SIMP_TAC[th; CARD_IMAGE_INJ; EQ_MULT_LCANCEL; PRIME_IMP_NZ;
 627                            FINITE_NUMSEG_LT; CARD_NUMSEG_LT]) THEN
 628   REWRITE_TAC[EXTENSION; TAUT `(a <=> b) <=> (a ==> b) /\ (b ==> a)`;
 629               FORALL_AND_THM; FORALL_IN_IMAGE] THEN
 630   ASM_SIMP_TAC[IN_ELIM_THM; GSYM ADD1; EXP; LT_MULT_LCANCEL; PRIME_IMP_NZ] THEN
 631   CONJ_TAC THENL [ALL_TAC; NUMBER_TAC] THEN
 632   X_GEN_TAC `x:num` THEN REWRITE_TAC[divides] THEN
 633   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 634   DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST_ALL_TAC) THEN
 635   REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN EXISTS_TAC `n:num` THEN
 636   UNDISCH_TAC `p * n < p * p EXP k` THEN
 637   ASM_SIMP_TAC[LT_MULT_LCANCEL; PRIME_IMP_NZ]);;
 638
 639 let PHI_PRIMEPOW = prove
 640  (`!p k. prime p
 641          ==> phi(p EXP k) = if k = 0 then 1 else p EXP k - p EXP (k - 1)`,
 642   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
 643   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; CONJUNCT1 EXP; PHI_1] THEN
 644   ASM_SIMP_TAC[ADD1; PHI_PRIMEPOW_SUC; ADD_SUB]);;
 645
 646 let PHI_2 = prove
 647  (`phi 2 = 1`,
 648   SIMP_TAC[PHI_PRIME; PRIME_2] THEN CONV_TAC NUM_REDUCE_CONV);;
 649
 650 (* ------------------------------------------------------------------------- *)
 651 (* Multiplicativity property.                                                *)
 652 (* ------------------------------------------------------------------------- *)
 653
 654 let PHI_MULTIPLICATIVE = prove
 655  (`!a b. coprime(a,b) ==> phi(a * b) = phi(a) * phi(b)`,
 656   REPEAT STRIP_TAC THEN
 657   MAP_EVERY ASM_CASES_TAC [`a = 0`; `b = 0`] THEN
 658   ASM_REWRITE_TAC[PHI_0; MULT_CLAUSES] THEN
 659   SIMP_TAC[PHI_ALT; GSYM CARD_PRODUCT; PHI_FINITE_LEMMA] THEN
 660   CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN
 661   EXISTS_TAC `\p. p MOD a,p MOD b` THEN
 662   REWRITE_TAC[PHI_FINITE_LEMMA; IN_ELIM_PAIR_THM] THEN
 663   ASM_SIMP_TAC[IN_ELIM_THM; COPRIME_MOD; DIVISION] THEN CONJ_TAC THENL
 664    [MESON_TAC[COPRIME_LMUL2; COPRIME_RMUL2]; ALL_TAC] THEN
 665   X_GEN_TAC `pp:num#num` THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 666   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
 667   ASM_REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC] THEN MP_TAC(SPECL
 668    [`a:num`; `b:num`; `m:num`; `n:num`] CHINESE_REMAINDER_COPRIME_UNIQUE) THEN
 669   ASM_SIMP_TAC[CONG; MOD_LT]);;
 670
 671 (* ------------------------------------------------------------------------- *)
 672 (* Even-ness of phi for most arguments.                                      *)
 673 (* ------------------------------------------------------------------------- *)
 674
 675 let EVEN_PHI = prove
 676  (`!n. 3 <= n ==> EVEN(phi n)`,
 677   REWRITE_TAC[ARITH_RULE `3 <= n <=> 1 < n /\ ~(n = 2)`; IMP_CONJ] THEN
 678   MATCH_MP_TAC INDUCT_COPRIME_STRONG THEN
 679   SIMP_TAC[PHI_PRIMEPOW; PHI_MULTIPLICATIVE; EVEN_MULT; EVEN_SUB] THEN
 680   CONJ_TAC THENL [MESON_TAC[COPRIME_REFL; ARITH_RULE `~(2 = 1)`]; ALL_TAC] THEN
 681   REWRITE_TAC[EVEN_EXP] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 682   FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP PRIME_ODD) THEN ASM_REWRITE_TAC[] THENL
 683    [ASM_CASES_TAC `k = 1` THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
 684     ASM_REWRITE_TAC[GSYM NOT_ODD]]);;
 685
 686 let EVEN_PHI_EQ = prove
 687  (`!n. EVEN(phi n) <=> n = 0 \/ 3 <= n`,
 688   GEN_TAC THEN EQ_TAC THENL
 689    [ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 690     REWRITE_TAC[ARITH_RULE `~(n = 0 \/ 3 <= n) <=> n = 1 \/ n = 2`] THEN
 691     STRIP_TAC THEN ASM_REWRITE_TAC[PHI_1; PHI_2] THEN CONV_TAC NUM_REDUCE_CONV;
 692     STRIP_TAC THEN ASM_SIMP_TAC[PHI_0; EVEN_PHI; EVEN]]);;
 693
 694 let ODD_PHI_EQ = prove
 695  (`!n. ODD(phi n) <=> n = 1 \/ n = 2`,
 696   REWRITE_TAC[GSYM NOT_EVEN; EVEN_PHI_EQ] THEN ARITH_TAC);;
 697
 698 (* ------------------------------------------------------------------------- *)
 699 (* Some iteration theorems.                                                  *)
 700 (* ------------------------------------------------------------------------- *)
 701
 702 let NPRODUCT_MOD = prove
 703  (`!s a:A->num n.
 704         FINITE s /\ ~(n = 0)
 705         ==> (iterate (*) s (\m. a(m) MOD n) == iterate (*) s a) (mod n)`,
 706   REPEAT STRIP_TAC THEN MP_TAC(SPEC `\x y. (x == y) (mod n)`
 707    (MATCH_MP ITERATE_RELATED MONOIDAL_MUL)) THEN
 708   SIMP_TAC[NEUTRAL_MUL; CONG_MULT; CONG_REFL] THEN DISCH_THEN MATCH_MP_TAC THEN
 709   ASM_SIMP_TAC[CONG_MOD]);;
 710
 711 let NPRODUCT_CMUL = prove
 712  (`!s a c n.
 713         FINITE s
 714         ==> iterate (*) s (\m. c * a(m)) = c EXP (CARD s) * iterate (*) s a`,
 715   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
 716   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 717   ASM_SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_MUL; NEUTRAL_MUL; CARD_CLAUSES;
 718                EXP; MULT_CLAUSES] THEN
 719   REWRITE_TAC[MULT_AC]);;
 720
 721 let COPRIME_NPRODUCT = prove
 722  (`!s n. FINITE s /\ (!x. x IN s ==> coprime(n,a(x)))
 723          ==> coprime(n,iterate (*) s a)`,
 724   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 725   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 726   SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_MUL; NEUTRAL_MUL;
 727            IN_INSERT; COPRIME_MUL; COPRIME_1]);;
 728
 729 let ITERATE_OVER_COPRIME = prove
 730  (`!op f n k.
 731         monoidal(op) /\ coprime(k,n) /\
 732         (!x y. (x == y) (mod n) ==> f x = f y)
 733         ==> iterate op {d | coprime(d,n) /\ d < n} (\m. f(k * m)) =
 734             iterate op {d | coprime(d,n) /\ d < n} f`,
 735   let lemma = prove
 736    (`~(n = 0) ==> ((a * x MOD n == b) (mod n) <=> (a * x == b) (mod n))`,
 737     MESON_TAC[CONG_REFL; CONG_SYM; CONG_TRANS; CONG_MULT; CONG_MOD]) in
 738   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 739    [ASM_SIMP_TAC[LT; SET_RULE `{x | F} = {}`; ITERATE_CLAUSES]; ALL_TAC] THEN
 740   STRIP_TAC THEN SUBGOAL_THEN `?m. (k * m == 1) (mod n)` CHOOSE_TAC THENL
 741    [ASM_MESON_TAC[CONG_SOLVE; MULT_SYM; CONG_SYM]; ALL_TAC] THEN
 742   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_EQ_GENERAL_INVERSES) THEN
 743   MAP_EVERY EXISTS_TAC [`\x. (k * x) MOD n`; `\x. (m * x) MOD n`] THEN
 744   REWRITE_TAC[IN_ELIM_THM] THEN
 745   ASM_SIMP_TAC[COPRIME_MOD; CONG_MOD_LT; CONG_LMOD; DIVISION; lemma;
 746                COPRIME_LMUL] THEN
 747   REPEAT STRIP_TAC THEN
 748   TRY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[CONG_LMOD]) THEN
 749   UNDISCH_TAC `(k * m == 1) (mod n)` THEN CONV_TAC NUMBER_RULE);;
 750
 751 let ITERATE_ITERATE_DIVISORS = prove
 752  (`!op:A->A->A f x.
 753         monoidal op
 754         ==> iterate op (1..x) (\n. iterate op {d | d divides n} (f n)) =
 755             iterate op (1..x)
 756                        (\n. iterate op (1..(x DIV n)) (\k. f (k * n) n))`,
 757   REPEAT STRIP_TAC THEN
 758   ASM_SIMP_TAC[ITERATE_ITERATE_PRODUCT; FINITE_NUMSEG; FINITE_DIVISORS;
 759                IN_NUMSEG; LE_1] THEN
 760   MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]
 761       ITERATE_EQ_GENERAL_INVERSES) THEN
 762   MAP_EVERY EXISTS_TAC [`\(n,d). d,n DIV d`; `\(n:num,k). n * k,n`] THEN
 763   ASM_SIMP_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; PAIR_EQ] THEN CONJ_TAC THEN
 764   REWRITE_TAC[IN_ELIM_THM] THEN X_GEN_TAC `n:num` THENL
 765    [X_GEN_TAC `k:num` THEN SIMP_TAC[DIV_MULT; LE_1; GSYM LE_RDIV_EQ] THEN
 766     SIMP_TAC[MULT_EQ_0; ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
 767     DISCH_THEN(K ALL_TAC) THEN NUMBER_TAC;
 768     X_GEN_TAC `d:num` THEN ASM_CASES_TAC `d = 0` THEN
 769     ASM_REWRITE_TAC[DIVIDES_ZERO] THENL [ARITH_TAC; ALL_TAC] THEN
 770     STRIP_TAC THEN ASM_SIMP_TAC[DIV_MONO] THEN CONJ_TAC THENL
 771      [ALL_TAC; ASM_MESON_TAC[DIVIDES_DIV_MULT; MULT_SYM]] THEN
 772     FIRST_X_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 773     ASM_SIMP_TAC[DIV_EQ_0; ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
 774     ASM_ARITH_TAC]);;
 775
 776 (* ------------------------------------------------------------------------- *)
 777 (* Fermat's Little theorem / Fermat-Euler theorem.                           *)
 778 (* ------------------------------------------------------------------------- *)
 779
 780 let FERMAT_LITTLE = prove
 781  (`!a n. coprime(a,n) ==> (a EXP (phi n) == 1) (mod n)`,
 782   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
 783   ASM_SIMP_TAC[COPRIME_0; PHI_0; CONG_MOD_0] THEN CONV_TAC NUM_REDUCE_CONV THEN
 784   DISCH_TAC THEN MATCH_MP_TAC CONG_MULT_LCANCEL THEN
 785   EXISTS_TAC `iterate (*) {m | coprime (m,n) /\ m < n} (\m. m)` THEN
 786   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[PHI_ALT; MULT_CLAUSES] THEN
 787   SIMP_TAC[IN_ELIM_THM; ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_NPRODUCT;
 788            PHI_FINITE_LEMMA; GSYM NPRODUCT_CMUL] THEN
 789   ONCE_REWRITE_TAC[CONG_SYM] THEN MATCH_MP_TAC CONG_TRANS THEN
 790   EXISTS_TAC `iterate (*) {m | coprime(m,n) /\ m < n} (\m. (a * m) MOD n)` THEN
 791   ASM_SIMP_TAC[NPRODUCT_MOD; PHI_FINITE_LEMMA] THEN
 792   MP_TAC(ISPECL [`( * ):num->num->num`; `\x. x MOD n`; `n:num`; `a:num`]
 793                 ITERATE_OVER_COPRIME) THEN
 794   ASM_SIMP_TAC[MONOIDAL_MUL; GSYM CONG] THEN
 795   DISCH_TAC THEN ONCE_REWRITE_TAC[CONG_SYM] THEN
 796   MATCH_MP_TAC NPRODUCT_MOD THEN ASM_SIMP_TAC[PHI_FINITE_LEMMA]);;
 797
 798 let FERMAT_LITTLE_PRIME = prove
 799  (`!a p. prime p /\ coprime(a,p) ==> (a EXP (p - 1) == 1) (mod p)`,
 800   MESON_TAC[FERMAT_LITTLE; PHI_PRIME_EQ]);;
 801
 802 (* ------------------------------------------------------------------------- *)
 803 (* Lucas's theorem.                                                          *)
 804 (* ------------------------------------------------------------------------- *)
 805
 806 let LUCAS_COPRIME_LEMMA = prove
 807  (`!m n a. ~(m = 0) /\ (a EXP m == 1) (mod n) ==> coprime(a,n)`,
 808   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 809    [ASM_REWRITE_TAC[CONG_MOD_0; EXP_EQ_1] THEN
 810     ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[] THEN
 811     ONCE_REWRITE_TAC[COPRIME_SYM] THEN SIMP_TAC[COPRIME_1];
 812     ALL_TAC] THEN
 813   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[COPRIME_1] THEN
 814   REPEAT STRIP_TAC THEN
 815   REWRITE_TAC[coprime] THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
 816   UNDISCH_TAC `(a EXP m == 1) (mod n)` THEN
 817   ASM_SIMP_TAC[CONG] THEN
 818   SUBGOAL_THEN `1 MOD n = 1` SUBST1_TAC THENL
 819    [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `0` THEN
 820     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 821     MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
 822     ALL_TAC] THEN
 823   DISCH_TAC THEN
 824   SUBGOAL_THEN `d divides (a EXP m) MOD n` MP_TAC THENL
 825    [ALL_TAC; ASM_SIMP_TAC[DIVIDES_ONE]] THEN
 826   MATCH_MP_TAC DIVIDES_ADD_REVR THEN
 827   EXISTS_TAC `a EXP m DIV n * n` THEN
 828   ASM_SIMP_TAC[GSYM DIVISION; DIVIDES_LMUL] THEN
 829   SUBGOAL_THEN `m = SUC(m - 1)` SUBST1_TAC THENL
 830    [UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC;
 831     ASM_SIMP_TAC[EXP; DIVIDES_RMUL]]);;
 832
 833 let LUCAS_WEAK = prove
 834  (`!a n. 2 <= n /\
 835          (a EXP (n - 1) == 1) (mod n) /\
 836          (!m. 0 < m /\ m < n - 1 ==> ~(a EXP m == 1) (mod n))
 837          ==> prime(n)`,
 838   REPEAT STRIP_TAC THEN
 839   ASM_SIMP_TAC[GSYM PHI_PRIME_EQ; PHI_LIMIT_STRONG; GSYM LE_ANTISYM;
 840                ARITH_RULE `2 <= n ==> ~(n = 0) /\ ~(n = 1)`] THEN
 841   FIRST_X_ASSUM(MP_TAC o SPEC `phi n`) THEN
 842   SUBGOAL_THEN `coprime(a,n)` (fun th -> SIMP_TAC[FERMAT_LITTLE; th]) THENL
 843    [MATCH_MP_TAC LUCAS_COPRIME_LEMMA THEN EXISTS_TAC `n - 1` THEN
 844     ASM_SIMP_TAC [ARITH_RULE `2 <= n ==> ~(n - 1 = 0)`]; ALL_TAC] THEN
 845   REWRITE_TAC[GSYM NOT_LT] THEN
 846   MATCH_MP_TAC(TAUT `a ==> ~(a /\ b) ==> ~b`) THEN
 847   ASM_SIMP_TAC[PHI_LOWERBOUND_1; ARITH_RULE `1 <= n ==> 0 < n`]);;
 848
 849 let LUCAS = prove
 850  (`!a n. 2 <= n /\
 851          (a EXP (n - 1) == 1) (mod n) /\
 852          (!p. prime(p) /\ p divides (n - 1)
 853               ==> ~(a EXP ((n - 1) DIV p) == 1) (mod n))
 854          ==> prime(n)`,
 855   REPEAT STRIP_TAC THEN
 856   FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `2 <= n ==> ~(n = 0)`)) THEN
 857   MATCH_MP_TAC LUCAS_WEAK THEN EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[] THEN
 858   REWRITE_TAC[TAUT `a ==> ~b <=> ~(a /\ b)`; GSYM NOT_EXISTS_THM] THEN
 859   ONCE_REWRITE_TAC[num_WOP] THEN
 860   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
 861   FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `0 < n ==> ~(n = 0)`)) THEN
 862   SUBGOAL_THEN `m divides (n - 1)` MP_TAC THENL
 863    [REWRITE_TAC[divides] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
 864     ASM_SIMP_TAC[GSYM MOD_EQ_0] THEN
 865     MATCH_MP_TAC(ARITH_RULE `~(0 < n) ==> (n = 0)`) THEN DISCH_TAC THEN
 866     FIRST_X_ASSUM(MP_TAC o SPEC `(n - 1) MOD m`) THEN
 867     ASM_SIMP_TAC[DIVISION] THEN CONJ_TAC THENL
 868      [MATCH_MP_TAC LT_TRANS THEN EXISTS_TAC `m:num` THEN
 869       ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 870     MATCH_MP_TAC CONG_MULT_LCANCEL THEN
 871     EXISTS_TAC `a EXP ((n - 1) DIV m * m)` THEN CONJ_TAC THENL
 872      [ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_EXP THEN
 873       ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC LUCAS_COPRIME_LEMMA THEN
 874       EXISTS_TAC `m:num` THEN ASM_SIMP_TAC[]; ALL_TAC] THEN
 875     REWRITE_TAC[GSYM EXP_ADD] THEN
 876     ASM_SIMP_TAC[GSYM DIVISION] THEN REWRITE_TAC[MULT_CLAUSES] THEN
 877     ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[GSYM EXP_EXP] THEN
 878     UNDISCH_TAC `(a EXP (n - 1) == 1) (mod n)` THEN
 879     UNDISCH_TAC `(a EXP m == 1) (mod n)` THEN
 880     ASM_SIMP_TAC[CONG] THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 881     EXISTS_TAC `((a EXP m) MOD n) EXP ((n - 1) DIV m) MOD n` THEN
 882     CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[MOD_EXP_MOD]] THEN
 883     ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[MOD_EXP_MOD] THEN
 884     REWRITE_TAC[EXP_ONE]; ALL_TAC] THEN
 885   REWRITE_TAC[divides] THEN
 886   DISCH_THEN(X_CHOOSE_THEN `r:num` SUBST_ALL_TAC) THEN
 887   SUBGOAL_THEN `~(r = 1)` MP_TAC THENL
 888    [UNDISCH_TAC `m < m * r` THEN CONV_TAC CONTRAPOS_CONV THEN
 889     SIMP_TAC[MULT_CLAUSES; LT_REFL]; ALL_TAC] THEN
 890   DISCH_THEN(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
 891   DISCH_THEN(X_CHOOSE_THEN `p:num` MP_TAC) THEN STRIP_TAC THEN
 892   UNDISCH_TAC `!p. prime p /\ p divides m * r
 893                    ==> ~(a EXP ((m * r) DIV p) == 1) (mod n)` THEN
 894   DISCH_THEN(MP_TAC o SPEC `p:num`) THEN ASM_SIMP_TAC[DIVIDES_LMUL] THEN
 895   SUBGOAL_THEN `(m * r) DIV p = m * (r DIV p)` SUBST1_TAC THENL
 896    [MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
 897     UNDISCH_TAC `prime p` THEN
 898     ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
 899     ASM_SIMP_TAC[ARITH_RULE `~(p = 0) ==> 0 < p`] THEN
 900     DISCH_TAC THEN REWRITE_TAC[ADD_CLAUSES; GSYM MULT_ASSOC] THEN
 901     AP_TERM_TAC THEN UNDISCH_TAC `p divides r` THEN
 902     REWRITE_TAC[divides] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 903     ASM_SIMP_TAC[DIV_MULT] THEN REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
 904   UNDISCH_TAC `(a EXP m == 1) (mod n)` THEN
 905   ASM_SIMP_TAC[CONG] THEN
 906   DISCH_THEN(MP_TAC o C AP_THM `r DIV p` o AP_TERM `(EXP)`) THEN
 907   DISCH_THEN(MP_TAC o C AP_THM `n:num` o AP_TERM `(MOD)`) THEN
 908   ASM_SIMP_TAC[MOD_EXP_MOD] THEN
 909   REWRITE_TAC[EXP_EXP; EXP_ONE]);;
 910
 911 (* ------------------------------------------------------------------------- *)
 912 (* Definition of the order of a number mod n (always 0 in non-coprime case). *)
 913 (* ------------------------------------------------------------------------- *)
 914
 915 let order = new_definition
 916  `order n a = @d. !k. (a EXP k == 1) (mod n) <=> d divides k`;;
 917
 918 let EXP_ITER = prove
 919  (`!x n. x EXP n = ITER n (\y. x * y) (1)`,
 920   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER; EXP]);;
 921
 922 let ORDER_DIVIDES = prove
 923  (`!n a d. (a EXP d == 1) (mod n) <=> order(n) a divides d`,
 924   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[order] THEN CONV_TAC SELECT_CONV THEN
 925   MP_TAC(ISPECL [`\x y:num. (x == y) (mod n)`; `\x:num. a * x`; `1`]
 926         ORDER_EXISTENCE_ITER) THEN
 927   REWRITE_TAC[GSYM EXP_ITER] THEN DISCH_THEN MATCH_MP_TAC THEN
 928   NUMBER_TAC);;
 929
 930 let ORDER = prove
 931  (`!n a. (a EXP (order(n) a) == 1) (mod n)`,
 932   REWRITE_TAC[ORDER_DIVIDES; DIVIDES_REFL]);;
 933
 934 let ORDER_MINIMAL = prove
 935  (`!n a m. 0 < m /\ m < order(n) a ==> ~((a EXP m == 1) (mod n))`,
 936   REWRITE_TAC[ORDER_DIVIDES] THEN REPEAT STRIP_TAC THEN
 937   FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN ASM_ARITH_TAC);;
 938
 939 let ORDER_WORKS = prove
 940  (`!n a. (a EXP (order(n) a) == 1) (mod n) /\
 941          !m. 0 < m /\ m < order(n) a ==> ~((a EXP m == 1) (mod n))`,
 942   MESON_TAC[ORDER; ORDER_MINIMAL]);;
 943
 944 let ORDER_1 = prove
 945  (`!n. order n 1 = 1`,
 946   REWRITE_TAC[GSYM DIVIDES_ONE; GSYM ORDER_DIVIDES; EXP_1; CONG_REFL]);;
 947
 948 let ORDER_EQ_0 = prove
 949  (`!n a. order(n) a = 0 <=> ~coprime(n,a)`,
 950   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 951    [ONCE_REWRITE_TAC[COPRIME_SYM] THEN DISCH_TAC THEN
 952     FIRST_ASSUM(MP_TAC o MATCH_MP FERMAT_LITTLE) THEN
 953     ASM_REWRITE_TAC[ORDER_DIVIDES; DIVIDES_ZERO; PHI_EQ_0] THEN
 954     ASM_MESON_TAC[COPRIME_0; ORDER_1; ARITH_RULE `~(1 = 0)`];
 955     MP_TAC(SPECL [`n:num`; `a:num`] ORDER) THEN
 956     SPEC_TAC(`order n a`,`m:num`) THEN INDUCT_TAC THEN REWRITE_TAC[] THEN
 957     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (TAUT
 958      `~p ==> (q ==> p) ==> q ==> r`)) THEN
 959     REWRITE_TAC[EXP] THEN CONV_TAC NUMBER_RULE]);;
 960
 961 let ORDER_CONG = prove
 962  (`!n a b. (a == b) (mod n) ==> order n a = order n b`,
 963   REPEAT STRIP_TAC THEN REWRITE_TAC[order] THEN
 964   AP_TERM_TAC THEN ABS_TAC THEN
 965   ASM_MESON_TAC[CONG_EXP; CONG_REFL; CONG_SYM; CONG_TRANS]);;
 966
 967 let COPRIME_ORDER = prove
 968  (`!n a. coprime(n,a)
 969          ==> order(n) a > 0 /\
 970             (a EXP (order(n) a) == 1) (mod n) /\
 971             !m. 0 < m /\ m < order(n) a ==> ~((a EXP m == 1) (mod n))`,
 972   SIMP_TAC[ARITH_RULE `n > 0 <=> ~(n = 0)`; ORDER_EQ_0] THEN
 973   MESON_TAC[ORDER; ORDER_MINIMAL]);;
 974
 975 let ORDER_DIVIDES_PHI = prove
 976  (`!a n. coprime(n,a) ==> (order n a) divides (phi n)`,
 977   MESON_TAC[ORDER_DIVIDES; FERMAT_LITTLE; COPRIME_SYM]);;
 978
 979 let ORDER_DIVIDES_EXPDIFF = prove
 980  (`!a n d e. coprime(n,a)
 981              ==> ((a EXP d == a EXP e) (mod n) <=> (d == e) (mod (order n a)))`,
 982   SUBGOAL_THEN
 983    `!a n d e. coprime(n,a) /\ e <= d
 984               ==> ((a EXP d == a EXP e) (mod n) <=> (d == e) (mod (order n a)))`
 985    (fun th -> MESON_TAC[th; LE_CASES; CONG_SYM]) THEN
 986   REPEAT STRIP_TAC THEN
 987   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 988   DISCH_THEN(X_CHOOSE_THEN `c:num` SUBST1_TAC) THEN
 989   SUBST1_TAC(ARITH_RULE `e = e + 0`) THEN
 990   REWRITE_TAC[ARITH_RULE `(e + 0) + c = e + c`] THEN
 991   REWRITE_TAC[EXP_ADD] THEN
 992   ASM_SIMP_TAC[CONG_ADD_LCANCEL_EQ; COPRIME_EXP;
 993     ONCE_REWRITE_RULE[COPRIME_SYM] CONG_MULT_LCANCEL_EQ] THEN
 994   REWRITE_TAC[EXP; CONG_0_DIVIDES; ORDER_DIVIDES]);;
 995
 996 let ORDER_UNIQUE = prove
 997  (`!n a k. 0 < k /\
 998            (a EXP k == 1) (mod n) /\
 999            (!m. 0 < m /\ m < k ==> ~(a EXP m == 1) (mod n))
1000            ==> order n a = k`,
1001   REPEAT STRIP_TAC THEN
1002   FIRST_X_ASSUM(MP_TAC o SPEC `order n a`) THEN
1003   MP_TAC(ISPECL [`n:num`; `a:num`] ORDER_WORKS) THEN
1004   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `k:num`)) THEN
1005   ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `order n a = 0` THEN
1006   ASM_REWRITE_TAC[] THENL [ALL_TAC; ASM_ARITH_TAC] THEN
1007   FIRST_X_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [ORDER_EQ_0]) THEN
1008   MP_TAC(ISPECL [`n:num`; `a:num`; `k:num`] COPRIME_REXP) THEN
1009   ASM_SIMP_TAC[LE_1; LT] THEN
1010   UNDISCH_TAC `(a EXP k == 1) (mod n)` THEN CONV_TAC NUMBER_RULE);;
1011
1012 (* ------------------------------------------------------------------------- *)
1013 (* Another trivial primality characterization.                               *)
1014 (* ------------------------------------------------------------------------- *)
1015
1016 let PRIME_PRIME_FACTOR = prove
1017  (`!n. prime n <=> ~(n = 1) /\ !p. prime p /\ p divides n ==> (p = n)`,
1018   GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [prime] THEN
1019   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[] THEN EQ_TAC THENL
1020    [MESON_TAC[PRIME_1]; ALL_TAC] THEN
1021   STRIP_TAC THEN X_GEN_TAC `d:num` THEN
1022   ASM_CASES_TAC `d = 1` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1023   FIRST_ASSUM(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC o
1024     MATCH_MP PRIME_FACTOR) THEN
1025   ASM_MESON_TAC[DIVIDES_TRANS; DIVIDES_ANTISYM]);;
1026
1027 let PRIME_DIVISOR_SQRT = prove
1028  (`!n. prime(n) <=> ~(n = 1) /\ !d. d divides n /\ d EXP 2 <= n ==> (d = 1)`,
1029   GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [prime] THEN
1030   ASM_CASES_TAC `n = 1` THEN ASM_SIMP_TAC[DIVIDES_ONE] THEN
1031   ASM_CASES_TAC `n = 0` THENL
1032    [ASM_REWRITE_TAC[DIVIDES_0; LE; EXP_EQ_0; ARITH_EQ] THEN
1033     MATCH_MP_TAC(TAUT `~a /\ ~b ==> (a <=> b)`) THEN CONJ_TAC THENL
1034      [DISCH_THEN(MP_TAC o SPEC `2`) THEN REWRITE_TAC[ARITH];
1035       DISCH_THEN(MP_TAC o SPEC `0`) THEN REWRITE_TAC[ARITH]];
1036     ALL_TAC] THEN
1037   EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `d:num` THEN STRIP_TAC THENL
1038    [ASM_CASES_TAC `d = n:num` THENL
1039      [ALL_TAC; ASM_MESON_TAC[]] THEN
1040     UNDISCH_TAC `d EXP 2 <= n` THEN ASM_REWRITE_TAC[] THEN
1041     REWRITE_TAC[EXP_2; ARITH_RULE `~(n * n <= n) <=> n * 1 < n * n`] THEN
1042     ASM_REWRITE_TAC[LT_MULT_LCANCEL] THEN
1043     MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
1044     ALL_TAC] THEN
1045   UNDISCH_TAC `d divides n` THEN REWRITE_TAC[divides] THEN
1046   DISCH_THEN(X_CHOOSE_THEN `e:num` SUBST_ALL_TAC) THEN
1047   SUBGOAL_THEN `d EXP 2 <= d * e \/ e EXP 2 <= d * e` MP_TAC THENL
1048    [REWRITE_TAC[EXP_2; LE_MULT_LCANCEL; LE_MULT_RCANCEL] THEN ARITH_TAC;
1049     ALL_TAC] THEN
1050   DISCH_THEN DISJ_CASES_TAC THENL
1051    [FIRST_X_ASSUM(MP_TAC o SPEC `d:num`);
1052     FIRST_X_ASSUM(MP_TAC o SPEC `e:num`)] THEN
1053   ASM_SIMP_TAC[DIVIDES_RMUL; DIVIDES_LMUL; DIVIDES_REFL; MULT_CLAUSES]);;
1054
1055 let PRIME_PRIME_FACTOR_SQRT = prove
1056  (`!n. prime n <=>
1057        ~(n = 0) /\ ~(n = 1) /\ ~(?p. prime p /\ p divides n /\ p EXP 2 <= n)`,
1058   GEN_TAC THEN ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[PRIME_1] THEN
1059   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
1060   GEN_REWRITE_TAC LAND_CONV [PRIME_DIVISOR_SQRT] THEN
1061   EQ_TAC THENL [MESON_TAC[PRIME_1]; ALL_TAC] THEN
1062   REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC THEN
1063   ASM_REWRITE_TAC[] THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
1064   ASM_CASES_TAC `d = 1` THEN ASM_REWRITE_TAC[] THEN
1065   FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
1066   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
1067   FIRST_X_ASSUM(MP_TAC o SPEC `p:num`) THEN ASM_REWRITE_TAC[] THEN
1068   CONJ_TAC THENL [ASM_MESON_TAC[DIVIDES_TRANS]; ALL_TAC] THEN
1069   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `d EXP 2` THEN ASM_REWRITE_TAC[] THEN
1070   REWRITE_TAC[num_CONV `2`; EXP_MONO_LE_SUC] THEN
1071   ASM_MESON_TAC[DIVIDES_LE; DIVIDES_ZERO]);;
1072
1073 (* ------------------------------------------------------------------------- *)
1074 (* Pocklington theorem.                                                      *)
1075 (* ------------------------------------------------------------------------- *)
1076
1077 let POCKLINGTON_LEMMA = prove
1078  (`!a n q r.
1079         2 <= n /\ (n - 1 = q * r) /\
1080         (a EXP (n - 1) == 1) (mod n) /\
1081         (!p. prime(p) /\ p divides q
1082              ==> coprime(a EXP ((n - 1) DIV p) - 1,n))
1083         ==> !p. prime p /\ p divides n ==> (p == 1) (mod q)`,
1084   REPEAT STRIP_TAC THEN
1085   SUBGOAL_THEN `order p (a EXP r) = q` ASSUME_TAC THENL
1086    [ALL_TAC;
1087     SUBGOAL_THEN `coprime(a EXP r,p)` (MP_TAC o MATCH_MP FERMAT_LITTLE) THENL
1088      [ALL_TAC;
1089       ASM_REWRITE_TAC[ORDER_DIVIDES] THEN
1090       SUBGOAL_THEN `phi p = p - 1` SUBST1_TAC THENL
1091        [ASM_MESON_TAC[PHI_PRIME_EQ]; ALL_TAC] THEN
1092       REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN
1093       DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1094        `(p - 1 = q * d) ==> ~(p = 0) ==> (p + q * 0 = 1 + q * d)`)) THEN
1095       REWRITE_TAC[nat_mod; cong] THEN ASM_MESON_TAC[PRIME_0]] THEN
1096     ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_EXP THEN
1097     UNDISCH_TAC `(a EXP (n - 1) == 1) (mod n)` THEN
1098     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1099     REWRITE_TAC[coprime; NOT_FORALL_THM; NOT_IMP] THEN
1100     DISCH_THEN(X_CHOOSE_THEN `d:num` STRIP_ASSUME_TAC) THEN
1101     SUBGOAL_THEN `d = p:num` SUBST_ALL_TAC THENL
1102      [ASM_MESON_TAC[prime]; ALL_TAC] THEN
1103     SUBGOAL_THEN `p divides (a EXP (n - 1))` ASSUME_TAC THENL
1104      [FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
1105        `2 <= n ==> (n - 1 = SUC(n - 2))`)) THEN
1106       REWRITE_TAC[EXP] THEN ASM_SIMP_TAC[DIVIDES_RMUL];
1107       ALL_TAC] THEN
1108     REWRITE_TAC[cong; nat_mod] THEN
1109     SUBGOAL_THEN `~(p divides 1)` MP_TAC THENL
1110      [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
1111     ASM_MESON_TAC[DIVIDES_RMUL; DIVIDES_ADD; DIVIDES_ADD_REVL]] THEN
1112   SUBGOAL_THEN `(order p (a EXP r)) divides q` MP_TAC THENL
1113    [REWRITE_TAC[GSYM ORDER_DIVIDES; EXP_EXP] THEN
1114     ONCE_REWRITE_TAC[MULT_SYM] THEN
1115     UNDISCH_TAC `(a EXP (n - 1) == 1) (mod n)` THEN
1116     ASM_REWRITE_TAC[] THEN
1117     UNDISCH_TAC `p divides n` THEN REWRITE_TAC[divides] THEN
1118     DISCH_THEN(X_CHOOSE_THEN `b:num` SUBST_ALL_TAC) THEN
1119     REWRITE_TAC[cong; nat_mod] THEN MESON_TAC[MULT_AC];
1120     ALL_TAC] THEN
1121   REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN
1122   ASM_CASES_TAC `d = 1` THEN ASM_SIMP_TAC[MULT_CLAUSES] THEN
1123   DISCH_THEN(ASSUME_TAC o SYM) THEN
1124   FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
1125   DISCH_THEN(X_CHOOSE_THEN `P:num` STRIP_ASSUME_TAC) THEN
1126   SUBGOAL_THEN `P divides q` ASSUME_TAC THENL
1127    [ASM_MESON_TAC[DIVIDES_LMUL]; ALL_TAC] THEN
1128   FIRST_X_ASSUM(MP_TAC o SPEC `P:num`) THEN ASM_REWRITE_TAC[] THEN
1129   MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1130   UNDISCH_TAC `P divides q` THEN REWRITE_TAC[divides] THEN
1131   DISCH_THEN(X_CHOOSE_THEN `s:num` SUBST_ALL_TAC) THEN
1132   REWRITE_TAC[GSYM MULT_ASSOC] THEN
1133   SUBGOAL_THEN `~(P = 0)` ASSUME_TAC THENL
1134    [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
1135   ASM_SIMP_TAC[DIV_MULT] THEN
1136   UNDISCH_TAC `P divides d` THEN REWRITE_TAC[divides] THEN
1137   DISCH_THEN(X_CHOOSE_THEN `t:num` SUBST_ALL_TAC) THEN
1138   UNDISCH_TAC `order p (a EXP r) * P * t = P * s` THEN
1139   ONCE_REWRITE_TAC[ARITH_RULE
1140    `(a * p * b = p * c) <=> (p * a * b = p * c)`] THEN
1141   REWRITE_TAC[EQ_MULT_LCANCEL] THEN ASM_REWRITE_TAC[] THEN
1142   DISCH_THEN(SUBST_ALL_TAC o SYM) THEN REWRITE_TAC[coprime] THEN
1143   DISCH_THEN(MP_TAC o SPEC `p:num`) THEN REWRITE_TAC[NOT_IMP] THEN
1144   CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[PRIME_1]] THEN
1145   ASM_REWRITE_TAC[] THEN
1146   ONCE_REWRITE_TAC[AC MULT_AC `(d * t) * r = r * d * t`] THEN
1147   REWRITE_TAC[EXP_MULT] THEN
1148   MATCH_MP_TAC CONG_1_DIVIDES THEN
1149   MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC `1 EXP t` THEN
1150   SIMP_TAC[CONG_EXP; ORDER] THEN REWRITE_TAC[EXP_ONE; CONG_REFL]);;
1151
1152 let POCKLINGTON = prove
1153  (`!a n q r.
1154         2 <= n /\ (n - 1 = q * r) /\ n <= q EXP 2 /\
1155         (a EXP (n - 1) == 1) (mod n) /\
1156         (!p. prime(p) /\ p divides q
1157              ==> coprime(a EXP ((n - 1) DIV p) - 1,n))
1158         ==> prime(n)`,
1159   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[PRIME_PRIME_FACTOR_SQRT] THEN
1160   ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> ~(n = 0) /\ ~(n = 1)`] THEN
1161   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
1162   MP_TAC(SPECL [`a:num`; `n:num`; `q:num`; `r:num`] POCKLINGTON_LEMMA) THEN
1163   ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `p:num`) THEN
1164   ASM_REWRITE_TAC[] THEN
1165   SUBGOAL_THEN `p EXP 2 <= q EXP 2` MP_TAC THENL
1166    [ASM_MESON_TAC[LE_TRANS]; ALL_TAC] THEN
1167   REWRITE_TAC[num_CONV `2`; EXP_MONO_LE_SUC] THEN
1168   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[] THEN
1169   DISCH_THEN(MP_TAC o MATCH_MP CONG_1_DIVIDES) THEN
1170   DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
1171   FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN ARITH_TAC);;
1172
1173 (* ------------------------------------------------------------------------- *)
1174 (* Variant for application, to separate the exponentiation.                  *)
1175 (* ------------------------------------------------------------------------- *)
1176
1177 let POCKLINGTON_ALT = prove
1178  (`!a n q r.
1179         2 <= n /\ (n - 1 = q * r) /\ n <= q EXP 2 /\
1180         (a EXP (n - 1) == 1) (mod n) /\
1181         (!p. prime(p) /\ p divides q
1182              ==> ?b. (a EXP ((n - 1) DIV p) == b) (mod n) /\
1183                      coprime(b - 1,n))
1184         ==> prime(n)`,
1185   REPEAT STRIP_TAC THEN MATCH_MP_TAC POCKLINGTON THEN
1186   MAP_EVERY EXISTS_TAC [`a:num`; `q:num`; `r:num`] THEN
1187   ASM_REWRITE_TAC[] THEN
1188   X_GEN_TAC `p:num` THEN STRIP_TAC THEN
1189   FIRST_X_ASSUM(MP_TAC o SPEC `p:num`) THEN ASM_REWRITE_TAC[] THEN
1190   DISCH_THEN(X_CHOOSE_THEN `b:num` STRIP_ASSUME_TAC) THEN
1191   SUBGOAL_THEN `(a EXP ((q * r) DIV p) - 1 == b - 1) (mod n)`
1192    (fun th -> ASM_MESON_TAC[CONG_COPRIME; COPRIME_SYM; th]) THEN
1193   MATCH_MP_TAC CONG_SUB THEN ASM_REWRITE_TAC[CONG_REFL] THEN
1194   REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`; EXP_EQ_0] THEN
1195   SUBGOAL_THEN `~(a = 0)` ASSUME_TAC THENL
1196    [DISCH_TAC THEN UNDISCH_TAC `(a EXP (n - 1) == 1) (mod n)` THEN
1197     SIMP_TAC[ARITH_RULE `2 <= n ==> (n - 1 = SUC(n - 2))`;
1198              ASSUME `a = 0`; ASSUME `2 <= n`] THEN
1199     REWRITE_TAC[MULT_CLAUSES; EXP] THEN
1200     ONCE_REWRITE_TAC[CONG_SYM] THEN
1201     REWRITE_TAC[CONG_0_DIVIDES; DIVIDES_ONE] THEN
1202     UNDISCH_TAC `2 <= n` THEN ARITH_TAC;
1203     ALL_TAC] THEN
1204   ASM_REWRITE_TAC[] THEN
1205   UNDISCH_TAC `(a EXP ((q * r) DIV p) == b) (mod n)` THEN
1206   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[] THEN
1207   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[CONG_0_DIVIDES] THEN
1208   SUBGOAL_THEN `~(n divides (a EXP (n - 1)))` MP_TAC THENL
1209    [ASM_MESON_TAC[CONG_DIVIDES; DIVIDES_ONE; ARITH_RULE `~(2 <= 1)`];
1210     ALL_TAC] THEN
1211   ASM_REWRITE_TAC[CONTRAPOS_THM] THEN UNDISCH_TAC `p divides q` THEN
1212   GEN_REWRITE_TAC LAND_CONV [divides] THEN
1213   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
1214   REWRITE_TAC[GSYM MULT_ASSOC] THEN
1215   SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
1216    [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
1217   ASM_SIMP_TAC[DIV_MULT] THEN
1218   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
1219   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [EXP_MULT] THEN
1220   SUBGOAL_THEN `p = SUC(p - 1)` SUBST1_TAC THENL
1221    [UNDISCH_TAC `~(p = 0)` THEN ARITH_TAC; ALL_TAC] THEN
1222   REWRITE_TAC[EXP; DIVIDES_RMUL]);;
1223
1224 (* ------------------------------------------------------------------------- *)
1225 (* Prime factorizations.                                                     *)
1226 (* ------------------------------------------------------------------------- *)
1227
1228 let primefact = new_definition
1229   `primefact ps n <=> (ITLIST (*) ps 1 = n) /\ !p. MEM p ps ==> prime(p)`;;
1230
1231 let PRIMEFACT = prove
1232  (`!n. ~(n = 0) ==> ?ps. primefact ps n`,
1233   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
1234   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[] THENL
1235    [REPEAT DISCH_TAC THEN EXISTS_TAC `[]:num list` THEN
1236     REWRITE_TAC[primefact; ITLIST; MEM]; ALL_TAC] THEN
1237   DISCH_TAC THEN DISCH_TAC THEN
1238   FIRST_ASSUM(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC o
1239     MATCH_MP PRIME_FACTOR) THEN
1240   UNDISCH_TAC `p divides n` THEN REWRITE_TAC[divides] THEN
1241   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
1242   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
1243   UNDISCH_TAC `~(p * m = 0)` THEN
1244   ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN DISCH_TAC THEN
1245   GEN_REWRITE_TAC (funpow 3 LAND_CONV) [ARITH_RULE `n = 1 * n`] THEN
1246   ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
1247   SUBGOAL_THEN `1 < p` (fun th -> REWRITE_TAC[th]) THENL
1248    [MATCH_MP_TAC(ARITH_RULE `~(p = 0) /\ ~(p = 1) ==> 1 < p`) THEN
1249     REPEAT STRIP_TAC THEN UNDISCH_TAC `prime p` THEN
1250     ASM_REWRITE_TAC[PRIME_0; PRIME_1]; ALL_TAC] THEN
1251   REWRITE_TAC[primefact] THEN
1252   DISCH_THEN(X_CHOOSE_THEN `ps:num list` ASSUME_TAC) THEN
1253   EXISTS_TAC `CONS (p:num) ps` THEN
1254   ASM_REWRITE_TAC[MEM; ITLIST] THEN ASM_MESON_TAC[]);;
1255
1256 let PRIMAFACT_CONTAINS = prove
1257  (`!ps n. primefact ps n ==> !p. prime p /\ p divides n ==> MEM p ps`,
1258   REPEAT GEN_TAC THEN REWRITE_TAC[primefact] THEN
1259   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1260   POP_ASSUM(SUBST1_TAC o SYM) THEN
1261   SPEC_TAC(`ps:num list`,`ps:num list`) THEN LIST_INDUCT_TAC THEN
1262   REWRITE_TAC[ITLIST; MEM] THENL
1263    [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
1264   STRIP_TAC THEN GEN_TAC THEN
1265   DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN
1266   DISCH_THEN(DISJ_CASES_TAC o MATCH_MP PRIME_DIVPROD) THEN
1267   ASM_MESON_TAC[prime; PRIME_1]);;
1268
1269 let PRIMEFACT_VARIANT = prove
1270  (`!ps n. primefact ps n <=> (ITLIST (*) ps 1 = n) /\ ALL prime ps`,
1271   REPEAT GEN_TAC THEN REWRITE_TAC[primefact] THEN AP_TERM_TAC THEN
1272   SPEC_TAC(`ps:num list`,`ps:num list`) THEN LIST_INDUCT_TAC THEN
1273   ASM_REWRITE_TAC[MEM; ALL] THEN ASM_MESON_TAC[]);;
1274
1275 (* ------------------------------------------------------------------------- *)
1276 (* Variant of Lucas theorem.                                                 *)
1277 (* ------------------------------------------------------------------------- *)
1278
1279 let LUCAS_PRIMEFACT = prove
1280  (`2 <= n /\
1281    (a EXP (n - 1) == 1) (mod n) /\
1282    (ITLIST (*) ps 1 = n - 1) /\
1283    ALL (\p. prime p /\ ~(a EXP ((n - 1) DIV p) == 1) (mod n)) ps
1284    ==> prime n`,
1285   REPEAT STRIP_TAC THEN MATCH_MP_TAC LUCAS THEN
1286   EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[] THEN
1287   SUBGOAL_THEN `primefact ps (n - 1)` MP_TAC THENL
1288    [ASM_REWRITE_TAC[PRIMEFACT_VARIANT] THEN MATCH_MP_TAC ALL_IMP THEN
1289     EXISTS_TAC `\p. prime p /\ ~(a EXP ((n - 1) DIV p) == 1) (mod n)` THEN
1290     ASM_SIMP_TAC[]; ALL_TAC] THEN
1291   DISCH_THEN(ASSUME_TAC o MATCH_MP PRIMAFACT_CONTAINS) THEN
1292   X_GEN_TAC `p:num` THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN UNDISCH_TAC
1293    `ALL (\p. prime p /\ ~(a EXP ((n - 1) DIV p) == 1) (mod n)) ps` THEN
1294   SPEC_TAC(`ps:num list`,`ps:num list`) THEN LIST_INDUCT_TAC THEN
1295   SIMP_TAC[ALL; MEM] THEN ASM_MESON_TAC[]);;
1296
1297 (* ------------------------------------------------------------------------- *)
1298 (* Variant of Pocklington theorem.                                           *)
1299 (* ------------------------------------------------------------------------- *)
1300
1301 let POCKLINGTON_PRIMEFACT = prove
1302  (`2 <= n /\ (q * r = n - 1) /\ n <= q * q
1303    ==> ((a EXP r) MOD n = b)
1304        ==> (ITLIST (*) ps 1 = q)
1305            ==> ((b EXP q) MOD n = 1)
1306                ==> ALL (\p. prime p /\
1307                             coprime((b EXP (q DIV p)) MOD n - 1,n)) ps
1308                    ==> prime n`,
1309   DISCH_THEN(fun th -> DISCH_THEN(SUBST1_TAC o SYM) THEN MP_TAC th) THEN
1310   SIMP_TAC[MOD_EXP_MOD; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1311   SIMP_TAC[ONCE_REWRITE_RULE[MULT_SYM] EXP_EXP] THEN
1312   REPEAT STRIP_TAC THEN MATCH_MP_TAC POCKLINGTON THEN
1313   MAP_EVERY EXISTS_TAC [`a:num`; `q:num`; `r:num`] THEN
1314   ASM_REWRITE_TAC[EXP_2] THEN CONJ_TAC THENL
1315    [MP_TAC(SPECL [`a EXP (n - 1)`; `n:num`] DIVISION) THEN
1316     ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1317     STRIP_TAC THEN ABBREV_TAC `Q = a EXP (n - 1) DIV n` THEN
1318     ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[cong; nat_mod] THEN
1319     MAP_EVERY EXISTS_TAC [`0`; `Q:num`] THEN ARITH_TAC;
1320     ALL_TAC] THEN
1321   SUBGOAL_THEN `primefact ps q` MP_TAC THENL
1322    [ASM_REWRITE_TAC[PRIMEFACT_VARIANT] THEN MATCH_MP_TAC ALL_IMP THEN
1323     EXISTS_TAC `\p. prime p /\ coprime(a EXP (q DIV p * r) MOD n - 1,n)` THEN
1324     ASM_SIMP_TAC[]; ALL_TAC] THEN
1325   DISCH_THEN(ASSUME_TAC o MATCH_MP PRIMAFACT_CONTAINS) THEN
1326   X_GEN_TAC `p:num` THEN
1327   DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN MP_TAC th) THEN
1328   DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1329   RULE_ASSUM_TAC(REWRITE_RULE[GSYM ALL_MEM]) THEN
1330   DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1331   MATCH_MP_TAC(TAUT `(a ==> (b <=> c)) ==> a /\ b ==> c`) THEN
1332   DISCH_TAC THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
1333   SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
1334    [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
1335   SUBGOAL_THEN `q DIV p * r = (n - 1) DIV p` SUBST1_TAC THENL
1336    [UNDISCH_TAC `p divides q` THEN REWRITE_TAC[divides] THEN
1337     DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC) THEN
1338     UNDISCH_THEN `(p * d) * r = n - 1` (SUBST1_TAC o SYM) THEN
1339     ASM_SIMP_TAC[DIV_MULT; GSYM MULT_ASSOC];
1340     ALL_TAC] THEN
1341   MATCH_MP_TAC CONG_COPRIME THEN MATCH_MP_TAC CONG_SUB THEN
1342   ASM_SIMP_TAC[CONG_MOD; ARITH_RULE `2 <= n ==> ~(n = 0)`; CONG_REFL] THEN
1343   MATCH_MP_TAC(ARITH_RULE `a <= b /\ ~(a = 0) ==> 1 <= a /\ 1 <= b`) THEN
1344   ASM_SIMP_TAC[MOD_LE; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1345   ASM_SIMP_TAC[MOD_EQ_0; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1346   DISCH_THEN(X_CHOOSE_THEN `s:num` MP_TAC) THEN
1347   DISCH_THEN(MP_TAC o C AP_THM `p:num` o AP_TERM `(EXP)`) THEN
1348   REWRITE_TAC[EXP_EXP] THEN
1349   SUBGOAL_THEN `(n - 1) DIV p * p = n - 1` SUBST1_TAC THENL
1350    [SUBST1_TAC(SYM(ASSUME `q * r = n - 1`)) THEN
1351     UNDISCH_TAC `p divides q` THEN REWRITE_TAC[divides] THEN
1352     DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
1353     REWRITE_TAC[GSYM MULT_ASSOC] THEN
1354     ASM_MESON_TAC[DIV_MULT; MULT_AC; PRIME_0];
1355     ALL_TAC] THEN
1356   DISCH_THEN(MP_TAC o C AP_THM `n:num` o AP_TERM `(MOD)`) THEN
1357   ASM_REWRITE_TAC[] THEN
1358   FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
1359    `~(p = 0) ==> (p = SUC(p - 1))`)) THEN
1360   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[EXP; GSYM MULT_ASSOC] THEN
1361   ASM_SIMP_TAC[MOD_MULT; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
1362   REWRITE_TAC[ARITH_EQ]);;
1363
1364 (* ------------------------------------------------------------------------- *)
1365 (* Utility functions.                                                        *)
1366 (* ------------------------------------------------------------------------- *)
1367
1368 let even_num n =
1369   mod_num n num_2 =/ num_0;;
1370
1371 let odd_num = not o even_num;;
1372
1373 (* ------------------------------------------------------------------------- *)
1374 (* Least p >= 0 with x <= 2^p.                                               *)
1375 (* ------------------------------------------------------------------------- *)
1376
1377 let log2 =
1378   let rec log2 x y =
1379     if x </ num_1 then y
1380     else log2 (quo_num x num_2) (y +/ num_1) in
1381   fun x -> log2 (x -/ num_1) num_0;;
1382
1383 (* ------------------------------------------------------------------------- *)
1384 (* Raise number to power (x^m) modulo n.                                     *)
1385 (* ------------------------------------------------------------------------- *)
1386
1387 let rec powermod x m n =
1388   if m =/ num_0 then num_1 else
1389   let y = powermod x (quo_num m num_2) n in
1390   let z = mod_num (y */ y) n in
1391   if even_num m then z else
1392   mod_num (x */ z) n;;
1393
1394 (* ------------------------------------------------------------------------- *)
1395 (* Make a call to PARI/GP to factor a number into (probable) primes.         *)
1396 (* ------------------------------------------------------------------------- *)
1397
1398 let factor =
1399   let suck_file s = let data = string_of_file s in Sys.remove s; data in
1400   let extract_output s =
1401     let l0 = explode s in
1402     let l0' = rev l0 in
1403     let l1 = snd(chop_list(index "]" l0') l0') in
1404     let l2 = "["::rev(fst(chop_list(index "[" l1) l1)) in
1405     let tm = parse_term (implode l2) in
1406     map ((dest_numeral F_F dest_numeral) o dest_pair) (dest_list tm) in
1407   fun n ->
1408     if n =/ num_1 then [] else
1409     let filename = Filename.temp_file "pocklington" ".out" in
1410     let s = "echo 'print(factorint(" ^
1411             (string_of_num n) ^
1412             "))  \n quit' | gp >" ^ filename ^ " 2>/dev/null" in
1413     if Sys.command s = 0 then
1414       let output = suck_file filename in
1415       extract_output output
1416     else
1417        failwith "factor: Call to GP/PARI failed";;
1418
1419 (* ------------------------------------------------------------------------- *)
1420 (* Alternative giving multiset instead of set plus indices.                  *)
1421 (* Also just use a stupid algorithm for small enough numbers or if PARI/GP   *)
1422 (* is not installed. I should really write a better factoring algorithm.     *)
1423 (* ------------------------------------------------------------------------- *)
1424
1425 let PARI_THRESHOLD = pow2 25;;
1426
1427 let multifactor =
1428   let rec findfactor m n =
1429     if mod_num n m =/ num_0 then m
1430     else if m */ m >/ n then n
1431     else findfactor (m +/ num_1) n in
1432   let rec stupidfactor n =
1433     let p = findfactor num_2 n in
1434     if p =/ n then [n] else p::(stupidfactor(quo_num n p)) in
1435   let rec multilist l =
1436     if l = [] then [] else
1437     let (x,n) = hd l in
1438     replicate x (Num.int_of_num n) @ multilist (tl l) in
1439   fun n -> try if n </ PARI_THRESHOLD then failwith ""
1440                else multilist (factor n)
1441            with Failure _ -> sort (</) (stupidfactor n);;
1442
1443 (* ------------------------------------------------------------------------- *)
1444 (* Recursive creation of Pratt primality certificates.                       *)
1445 (* ------------------------------------------------------------------------- *)
1446
1447 type certificate =
1448     Prime_2
1449   | Primroot_and_factors of
1450       ((num * num list) * num * (num * certificate) list);;
1451
1452 let find_primitive_root =
1453   let rec find_primitive_root a m ms n =
1454     if gcd_num a n =/ num_1 &
1455        powermod a m n =/ num_1 &
1456        forall (fun k -> powermod a k n <>/ num_1) ms
1457     then a
1458     else find_primitive_root (a +/ num_1) m ms n in
1459   let find_primitive_root_from_2 = find_primitive_root num_2 in
1460   fun m ms n ->
1461     if n </ num_2 then failwith "find_primitive_root: input too small"
1462     else find_primitive_root_from_2 m ms n;;
1463
1464 let uniq_num =
1465   let rec uniq x l =
1466     match l with
1467       [] -> raise Unchanged
1468     | (h::t) -> if x =/ h then
1469                   try uniq x t
1470                   with Unchanged -> l
1471                 else x::(uniq h t) in
1472   fun l -> if l = [] then [] else uniq (hd l) (tl l);;
1473
1474 let setify_num s =
1475   let s' = sort (<=/) s in
1476   try uniq_num s' with Unchanged -> s';;
1477
1478 let certify_prime =
1479   let rec cert_prime n =
1480     if n <=/ num_2 then
1481        if n =/ num_2 then Prime_2
1482        else failwith "certify_prime: not a prime!"
1483     else
1484       let m = n -/ num_1 in
1485       let pfact = multifactor m in
1486       let primes = setify_num pfact in
1487       let ms = map (fun d -> div_num m d) primes in
1488       let a = find_primitive_root m ms n in
1489       Primroot_and_factors((n,pfact),a,map (fun n -> n,cert_prime n) primes) in
1490   fun n -> if length(multifactor n) = 1 then cert_prime n
1491            else failwith "certify_prime: input is not a prime";;
1492
1493 (* ------------------------------------------------------------------------- *)
1494 (* Relatively efficient evaluation of "(a EXP k) MOD n".                     *)
1495 (* ------------------------------------------------------------------------- *)
1496
1497 let EXP_MOD_CONV =
1498   let pth = prove
1499    (`~(n = 0)
1500      ==> ((a EXP 0) MOD n = 1 MOD n) /\
1501          ((a EXP (NUMERAL (BIT0 m))) MOD n =
1502                 let b = (a EXP (NUMERAL m)) MOD n in
1503                 (b * b) MOD n) /\
1504          ((a EXP (NUMERAL (BIT1 m))) MOD n =
1505                 let b = (a EXP (NUMERAL m)) MOD n in
1506                 (a * ((b * b) MOD n)) MOD n)`,
1507     DISCH_TAC THEN REWRITE_TAC[EXP] THEN
1508     REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN
1509     REWRITE_TAC[EXP; EXP_ADD] THEN
1510     CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
1511     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD] THEN
1512     REWRITE_TAC[MULT_ASSOC] THEN
1513     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD] THEN
1514     ONCE_REWRITE_TAC[MULT_SYM] THEN
1515     REWRITE_TAC[MULT_ASSOC] THEN
1516     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD])
1517   and pth_cong = SPEC_ALL CONG
1518   and n_tm = `n:num` in
1519   fun tm ->
1520     let ntm = rand tm in
1521     let th1 = INST [ntm,n_tm] pth in
1522     let th2 = EQF_ELIM(NUM_EQ_CONV(rand(lhand(concl th1)))) in
1523     let th_base,th_steps = CONJ_PAIR(MP th1 th2) in
1524     let conv_base = GEN_REWRITE_CONV I [th_base]
1525     and conv_step = GEN_REWRITE_CONV I [th_steps] in
1526     let rec conv tm =
1527       try conv_base tm with Failure _ ->
1528       (conv_step THENC
1529        RAND_CONV conv THENC
1530        let_CONV THENC
1531        NUM_REDUCE_CONV) tm in
1532     conv tm;;
1533
1534 (* ------------------------------------------------------------------------- *)
1535 (* HOL checking of primality certificate, using Pocklington shortcut.        *)
1536 (* ------------------------------------------------------------------------- *)
1537
1538 let prime_theorem_cache = ref [];;
1539
1540 let rec lookup_under_num n l =
1541   if l = [] then failwith "lookup_under_num" else
1542   let h = hd l in
1543   if fst h =/ n then snd h
1544   else lookup_under_num n (tl l);;
1545
1546 let rec split_factors q qs ps n =
1547   if q */ q >=/ n then rev qs,ps
1548   else split_factors (q */ hd ps) (hd ps :: qs) (tl ps) n;;
1549
1550 let check_certificate =
1551   let n_tm = `n:num`
1552   and a_tm = `a:num`
1553   and q_tm = `q:num`
1554   and r_tm = `r:num`
1555   and b_tm = `b:num`
1556   and ps_tm = `ps:num list`
1557   and conv_itlist =
1558    GEN_REWRITE_CONV TOP_DEPTH_CONV [ITLIST] THENC NUM_REDUCE_CONV
1559   and conv_all =
1560    GEN_REWRITE_CONV TOP_DEPTH_CONV
1561     [ALL; BETA_THM; TAUT `a /\ T <=> a`] THENC
1562    GEN_REWRITE_CONV DEPTH_CONV
1563     [TAUT `(a /\ a /\ b <=> a /\ b) /\ (a /\ a <=> a)`]
1564   and subarith_conv =
1565     let gconv_net = itlist (uncurry net_of_conv)
1566       [`a - b`,NUM_SUB_CONV;
1567        `a DIV b`,NUM_DIV_CONV;
1568        `(a EXP b) MOD c`,EXP_MOD_CONV;
1569        `coprime(a,b)`,COPRIME_CONV;
1570        `p /\ T`,REWR_CONV(TAUT `p /\ T <=> p`);
1571        `T /\ p`,REWR_CONV(TAUT `T /\ p <=> p`)]
1572       empty_net  in
1573     DEPTH_CONV(REWRITES_CONV gconv_net) in
1574   let rec check_certificate cert =
1575     match cert with
1576       Prime_2 ->
1577           PRIME_2
1578     | Primroot_and_factors((n,ps),a,ncerts) ->
1579           try lookup_under_num n (!prime_theorem_cache) with Failure _ ->
1580           let qs,rs = split_factors num_1 [] (rev ps) n in
1581           let q = itlist ( */ ) qs num_1
1582           and r = itlist ( */ ) rs num_1 in
1583           let th1 = INST [mk_numeral n,n_tm;
1584                           mk_flist (map mk_numeral qs),ps_tm;
1585                           mk_numeral q,q_tm;
1586                           mk_numeral r,r_tm;
1587                           mk_numeral a,a_tm]
1588                          POCKLINGTON_PRIMEFACT in
1589           let th2 = MP th1 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th1)))) in
1590           let tha = EXP_MOD_CONV(lhand(lhand(concl th2))) in
1591           let thb = MP (INST [rand(concl tha),b_tm] th2) tha in
1592           let th3 = MP thb (EQT_ELIM(conv_itlist (lhand(concl thb)))) in
1593           let th4 = MP th3 (EXP_MOD_CONV (lhand(lhand(concl th3)))) in
1594           let th5 = conv_all(lhand(concl th4)) in
1595           let th6 = TRANS th5 (subarith_conv(rand(concl th5))) in
1596           let th7 = IMP_TRANS (snd(EQ_IMP_RULE th6)) th4 in
1597           let ants = conjuncts(lhand(concl th7)) in
1598           let certs =
1599             map (fun t -> lookup_under_num (dest_numeral(rand t)) ncerts)
1600                 ants in
1601           let ths = map check_certificate certs in
1602           let fth = MP th7 (end_itlist CONJ ths) in
1603           prime_theorem_cache := (n,fth)::(!prime_theorem_cache); fth in
1604   check_certificate;;
1605
1606 (* ------------------------------------------------------------------------- *)
1607 (* Hence a primality-proving rule.                                           *)
1608 (* ------------------------------------------------------------------------- *)
1609
1610 let PROVE_PRIME = check_certificate o certify_prime;;
1611
1612 (* ------------------------------------------------------------------------- *)
1613 (* Rule to generate prime factorization theorems.                            *)
1614 (* ------------------------------------------------------------------------- *)
1615
1616 let PROVE_PRIMEFACT =
1617   let pth = SPEC_ALL PRIMEFACT_VARIANT
1618   and start_CONV = PURE_REWRITE_CONV[ITLIST; ALL] THENC NUM_REDUCE_CONV
1619   and ps_tm = `ps:num list`
1620   and n_tm = `n:num` in
1621   fun n ->
1622      let pfact = multifactor n in
1623      let th1 = INST [mk_flist(map mk_numeral pfact),ps_tm;
1624                      mk_numeral n,n_tm] pth in
1625      let th2 = TRANS th1 (start_CONV(rand(concl th1))) in
1626      let ths = map PROVE_PRIME pfact in
1627      EQ_MP (SYM th2) (end_itlist CONJ ths);;
1628
1629 (* ------------------------------------------------------------------------- *)
1630 (* Conversion for truth or falsity of primality assertion.                   *)
1631 (* ------------------------------------------------------------------------- *)
1632
1633 let PRIME_TEST =
1634   let NOT_PRIME_THM = prove
1635    (`((m = 1) <=> F) ==> ((m = p) <=> F) ==> (m * n = p) ==> (prime(p) <=> F)`,
1636     MESON_TAC[prime; divides])
1637   and m_tm = `m:num` and n_tm = `n:num` and p_tm = `p:num` in
1638   fun tm ->
1639     let p = dest_numeral tm in
1640     if p =/ num_0 then EQF_INTRO PRIME_0
1641     else if p =/ num_1 then EQF_INTRO PRIME_1 else
1642     let pfact = multifactor p in
1643     if length pfact = 1 then
1644      (remark ("proving that " ^ string_of_num p ^ " is prime");
1645       EQT_INTRO(PROVE_PRIME p))
1646     else
1647      (remark ("proving that " ^ string_of_num p ^ " is composite");
1648       let m = hd pfact and n = end_itlist ( */ ) (tl pfact) in
1649       let th0 = INST [mk_numeral m,m_tm; mk_numeral n,n_tm; mk_numeral p,p_tm]
1650                      NOT_PRIME_THM in
1651       let th1 = MP th0 (NUM_EQ_CONV (lhand(lhand(concl th0)))) in
1652       let th2 = MP th1 (NUM_EQ_CONV (lhand(lhand(concl th1)))) in
1653       MP th2 (NUM_MULT_CONV(lhand(lhand(concl th2)))));;
1654
1655 let PRIME_CONV =
1656   let prime_tm = `prime` in
1657   fun tm0 ->
1658     let ptm,tm = dest_comb tm0 in
1659     if ptm <> prime_tm then failwith "expected term of form prime(n)"
1660     else PRIME_TEST tm;;
1661
1662 (* ------------------------------------------------------------------------- *)
1663 (* Another lemma.                                                            *)
1664 (* ------------------------------------------------------------------------- *)
1665
1666 let PRIME_POWER_EXISTS = prove
1667  (`!q. prime q
1668        ==> ((?i. n = q EXP i) <=>
1669             (!p. prime p /\ p divides n ==> p = q))`,
1670   REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THEN
1671   ASM_SIMP_TAC[IMP_CONJ; PRIME_DIVEXP_EQ; DIVIDES_PRIME_PRIME] THEN
1672   ASM_CASES_TAC `n = 0` THENL
1673    [FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `2` th) THEN MP_TAC(SPEC `3` th)) THEN
1674     ASM_REWRITE_TAC[PRIME_2; PRIME_CONV `prime 3`; DIVIDES_0] THEN ARITH_TAC;
1675     ALL_TAC] THEN
1676   ASM_CASES_TAC `n = 1` THENL
1677    [EXISTS_TAC `0` THEN ASM_REWRITE_TAC[EXP]; ALL_TAC] THEN
1678   MP_TAC(ISPEC `n:num` PRIMEPOW_FACTOR) THEN
1679   ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1680   DISCH_THEN(X_CHOOSE_THEN `p:num` MP_TAC) THEN
1681   ASM_CASES_TAC `p:num = q` THENL
1682    [FIRST_X_ASSUM(SUBST_ALL_TAC o SYM);
1683     ASM_MESON_TAC[DIVIDES_REXP; LE_1; DIVIDES_RMUL; DIVIDES_REFL]] THEN
1684   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `i:num` THEN
1685   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
1686   FIRST_X_ASSUM SUBST_ALL_TAC THEN
1687   MATCH_MP_TAC(NUM_RING `m = 1 ==> x * m = x`) THEN
1688   MATCH_MP_TAC(ARITH_RULE `~(m = 0) /\ ~(2 <= m) ==> m = 1`) THEN
1689   CONJ_TAC THENL [ASM_MESON_TAC[COPRIME_0; PRIME_1]; ALL_TAC] THEN
1690   DISCH_THEN(MP_TAC o MATCH_MP PRIMEPOW_FACTOR) THEN
1691   DISCH_THEN(X_CHOOSE_THEN `r:num` STRIP_ASSUME_TAC) THEN
1692   FIRST_X_ASSUM(MP_TAC o SPEC `r:num`) THEN
1693   REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
1694    [ASM_MESON_TAC[DIVIDES_LMUL; DIVIDES_RMUL; DIVIDES_REXP; LE_1; DIVIDES_REFL];
1695     DISCH_THEN SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
1696     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COPRIME_RMUL]) THEN
1697     ASM_SIMP_TAC[COPRIME_REXP; LE_1; COPRIME_REFL] THEN
1698     ASM_MESON_TAC[PRIME_1]]);;
1699
1700 (* ------------------------------------------------------------------------- *)
1701 (* Example.                                                                  *)
1702 (* ------------------------------------------------------------------------- *)
1703
1704 map (time PRIME_TEST o mk_small_numeral) (0--50);;
1705
1706 time PRIME_TEST `65535`;;
1707
1708 time PRIME_TEST `65536`;;
1709
1710 time PRIME_TEST `65537`;;
1711
1712 time PROVE_PRIMEFACT (Int 222);;
1713
1714 time PROVE_PRIMEFACT (Int 151);;
1715
1716 (* ------------------------------------------------------------------------- *)
1717 (* The "Landau trick" in Erdos's proof of Chebyshev-Bertrand theorem.        *)
1718 (* ------------------------------------------------------------------------- *)
1719
1720 map (time PRIME_TEST o mk_small_numeral)
1721   [3; 5; 7; 13; 23; 43; 83; 163; 317; 631; 1259; 2503; 4001];;