Library/pratt.ml

   1 (* ========================================================================= *)
   2 (* HOL primality proving procedure, based on Pratt certificates.             *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6
   7 prioritize_num();;
   8
   9 let num_0 = Int 0;;
  10 let num_1 = Int 1;;
  11 let num_2 = Int 2;;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Mostly for compatibility. Should eliminate this eventually.               *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let nat_mod_lemma = prove
  18  (`!x y n:num. (x == y) (mod n) /\ y <= x ==> ?q. x = y + n * q`,
  19   REPEAT GEN_TAC THEN REWRITE_TAC[num_congruent] THEN
  20   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
  21   ONCE_REWRITE_TAC
  22    [INTEGER_RULE `(x == y) (mod &n) <=> &n divides (x - y)`] THEN
  23   ASM_SIMP_TAC[INT_OF_NUM_SUB;
  24                ARITH_RULE `x <= y ==> (y:num = x + d <=> y - x = d)`] THEN
  25   REWRITE_TAC[GSYM num_divides; divides]);;
  26
  27 let nat_mod = prove
  28  (`!x y n:num. (mod n) x y <=> ?q1 q2. x + n * q1 = y + n * q2`,
  29   REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM cong] THEN
  30   EQ_TAC THENL [ALL_TAC; NUMBER_TAC] THEN
  31   MP_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THEN
  32   REWRITE_TAC[TAUT `a \/ b ==> c ==> d <=> (c /\ b) \/ (c /\ a) ==> d`] THEN
  33   DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
  34    [ALL_TAC;
  35     ONCE_REWRITE_TAC[NUMBER_RULE
  36       `(x:num == y) (mod n) <=> (y == x) (mod n)`]] THEN
  37   MESON_TAC[nat_mod_lemma; ARITH_RULE `x + y * 0 = x`]);;
  38
  39 (* ------------------------------------------------------------------------- *)
  40 (* Lemmas about previously defined terms.                                    *)
  41 (* ------------------------------------------------------------------------- *)
  42
  43 let PRIME = prove
  44  (`!p. prime p <=>
  45        ~(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   REPEAT GEN_TAC THEN REWRITE_TAC[cong; nat_mod; MULT_CLAUSES; ADD_CLAUSES]);;
 120
 121 let CONG_MOD_1 = prove
 122  (`!x y. (x == y) (mod 1)`,
 123   REPEAT GEN_TAC THEN REWRITE_TAC[cong; nat_mod] THEN
 124   MAP_EVERY EXISTS_TAC [`y:num`; `x:num`] THEN
 125   REWRITE_TAC[MULT_CLAUSES; ADD_AC]);;
 126
 127 let CONG_0 = prove
 128  (`!x n. ((x == 0) (mod n) <=> n divides x)`,
 129   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN
 130   ASM_REWRITE_TAC[DIVIDES_ZERO; CONG_MOD_0] THEN
 131   ASM_SIMP_TAC[CONG; MOD_0; MOD_EQ_0] THEN
 132   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[divides]);;
 133
 134 let CONG_SUB_CASES = prove
 135  (`!x y n. (x == y) (mod n) <=>
 136            if x <= y then (y - x == 0) (mod n)
 137            else (x - y == 0) (mod n)`,
 138   REPEAT GEN_TAC THEN REWRITE_TAC[cong; nat_mod] THEN
 139   COND_CASES_TAC THENL
 140    [GEN_REWRITE_TAC LAND_CONV [SWAP_EXISTS_THM]; ALL_TAC] THEN
 141   REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
 142   POP_ASSUM MP_TAC THEN ARITH_TAC);;
 143
 144 let CONG_MULT_LCANCEL = prove
 145  (`!a n x y. coprime(a,n) /\ (a * x == a * y) (mod n) ==> (x == y) (mod n)`,
 146   REPEAT GEN_TAC THEN ASM_CASES_TAC `a = 0` THENL
 147    [ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[COPRIME_0] THEN
 148     SIMP_TAC[CONG_MOD_1]; ALL_TAC] THEN
 149   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 150   ONCE_REWRITE_TAC[CONG_SUB_CASES] THEN
 151   ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN
 152   REWRITE_TAC[GSYM LEFT_SUB_DISTRIB; CONG_0] THEN
 153   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 154   ASM_MESON_TAC[COPRIME_DIVPROD; COPRIME_SYM]);;
 155
 156 let CONG_REFL = prove
 157  (`!x n. (x == x) (mod n)`,
 158   MESON_TAC[cong; nat_mod; ADD_CLAUSES; MULT_CLAUSES]);;
 159
 160 let CONG_SYM = prove
 161  (`!x y n. (x == y) (mod n) <=> (y == x) (mod n)`,
 162   REWRITE_TAC[cong; nat_mod] THEN MESON_TAC[]);;
 163
 164 let CONG_TRANS = prove
 165  (`!x y z n. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`,
 166   REWRITE_TAC[cong; nat_mod] THEN
 167   MESON_TAC[ARITH_RULE
 168    `(x + n * q1 = y + n * q2) /\
 169     (y + n * q3 = z + n * q4)
 170     ==> (x + n * (q1 + q3) = z + n * (q2 + q4))`]);;
 171
 172 (* ------------------------------------------------------------------------- *)
 173 (* Euler totient function.                                                   *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let phi = new_definition
 177   `phi(n) = CARD { m | 0 < m /\ m <= n /\ coprime(m,n) }`;;
 178
 179 let PHI_ALT = prove
 180  (`phi(n) = CARD { m | coprime(m,n) /\ m < n}`,
 181   REWRITE_TAC[phi] THEN
 182   ASM_CASES_TAC `n = 0` THENL
 183    [AP_TERM_TAC THEN
 184     ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 185     MESON_TAC[LT; NOT_LT];
 186     ALL_TAC] THEN
 187   ASM_CASES_TAC `n = 1` THENL
 188    [SUBGOAL_THEN
 189      `({m | 0 < m /\ m <= n /\ coprime (m,n)} = {1}) /\
 190       ({m | coprime (m,n) /\ m < n} = {0})`
 191      (CONJUNCTS_THEN SUBST1_TAC)
 192     THENL [ALL_TAC; SIMP_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY]] THEN
 193     ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN
 194     REWRITE_TAC[COPRIME_1] THEN REPEAT STRIP_TAC THEN ARITH_TAC;
 195     ALL_TAC] THEN
 196   AP_TERM_TAC THEN ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 197   X_GEN_TAC `m:num` THEN ASM_CASES_TAC `m = 0` THEN
 198   ASM_REWRITE_TAC[LT] THENL
 199    [ASM_MESON_TAC[COPRIME_0; COPRIME_SYM];
 200     ASM_MESON_TAC[LE_LT; COPRIME_REFL; LT_NZ]]);;
 201
 202 let PHI_ANOTHER = prove
 203  (`!n. ~(n = 1) ==> (phi(n) = CARD {m | 0 < m /\ m < n /\ coprime(m,n)})`,
 204   REPEAT STRIP_TAC THEN REWRITE_TAC[phi] THEN
 205   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 206   ASM_MESON_TAC[LE_LT; COPRIME_REFL; COPRIME_1; LT_NZ]);;
 207
 208 let PHI_LIMIT = prove
 209  (`!n. phi(n) <= n`,
 210   GEN_TAC THEN REWRITE_TAC[PHI_ALT] THEN
 211   GEN_REWRITE_TAC RAND_CONV [GSYM CARD_NUMSEG_LT] THEN
 212   MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[FINITE_NUMSEG_LT] THEN
 213   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 214
 215 let PHI_LIMIT_STRONG = prove
 216  (`!n. ~(n = 1) ==> phi(n) <= n - 1`,
 217   REPEAT STRIP_TAC THEN
 218   MP_TAC(SPEC `n:num` FINITE_NUMBER_SEGMENT) THEN
 219   ASM_SIMP_TAC[PHI_ANOTHER; HAS_SIZE] THEN
 220   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN
 221   MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[] THEN
 222   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 223
 224 let PHI_0 = prove
 225  (`phi 0 = 0`,
 226   MP_TAC(SPEC `0` PHI_LIMIT) THEN REWRITE_TAC[ARITH] THEN ARITH_TAC);;
 227
 228 let PHI_1 = prove
 229  (`phi 1 = 1`,
 230   REWRITE_TAC[PHI_ALT; COPRIME_1; CARD_NUMSEG_LT]);;
 231
 232 let PHI_LOWERBOUND_1_STRONG = prove
 233  (`!n. 1 <= n ==> 1 <= phi(n)`,
 234   REPEAT STRIP_TAC THEN
 235   SUBGOAL_THEN `1 = CARD {1}` SUBST1_TAC THENL
 236    [SIMP_TAC[CARD_CLAUSES; NOT_IN_EMPTY; FINITE_RULES; ARITH]; ALL_TAC] THEN
 237   REWRITE_TAC[phi] THEN MATCH_MP_TAC CARD_SUBSET THEN CONJ_TAC THENL
 238    [SIMP_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN
 239     REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_1] THEN
 240     GEN_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 241     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{b | b <= n}` THEN
 242     REWRITE_TAC[CARD_NUMSEG_LE; FINITE_NUMSEG_LE] THEN
 243     SIMP_TAC[SUBSET; IN_ELIM_THM]]);;
 244
 245 let PHI_LOWERBOUND_1 = prove
 246  (`!n. 2 <= n ==> 1 <= phi(n)`,
 247   MESON_TAC[PHI_LOWERBOUND_1_STRONG; LE_TRANS; ARITH_RULE `1 <= 2`]);;
 248
 249 let PHI_LOWERBOUND_2 = prove
 250  (`!n. 3 <= n ==> 2 <= phi(n)`,
 251   REPEAT STRIP_TAC THEN
 252   SUBGOAL_THEN `2 = CARD {1,(n-1)}` SUBST1_TAC THENL
 253    [SIMP_TAC[CARD_CLAUSES; IN_INSERT; NOT_IN_EMPTY; FINITE_RULES; ARITH] THEN
 254     ASM_SIMP_TAC[ARITH_RULE `3 <= n ==> ~(1 = n - 1)`]; ALL_TAC] THEN
 255   REWRITE_TAC[phi] THEN MATCH_MP_TAC CARD_SUBSET THEN CONJ_TAC THENL
 256    [SIMP_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM] THEN
 257     GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 258     REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_1] THEN
 259     ASM_SIMP_TAC[ARITH;
 260                ARITH_RULE `3 <= n ==> 0 < n - 1 /\ n - 1 <= n /\ 1 <= n`] THEN
 261     REWRITE_TAC[coprime] THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
 262     MP_TAC(SPEC `n:num` COPRIME_1) THEN REWRITE_TAC[coprime] THEN
 263     DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 264     SUBGOAL_THEN `1 = n - (n - 1)` SUBST1_TAC THENL
 265      [UNDISCH_TAC `3 <= n` THEN ARITH_TAC;
 266       ASM_SIMP_TAC[DIVIDES_SUB]];
 267     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{b | b <= n}` THEN
 268     REWRITE_TAC[CARD_NUMSEG_LE; FINITE_NUMSEG_LE] THEN
 269     SIMP_TAC[SUBSET; IN_ELIM_THM]]);;
 270
 271 let PHI_PRIME_EQ = prove
 272  (`!n. (phi n = n - 1) /\ ~(n = 0) /\ ~(n = 1) <=> prime n`,
 273   GEN_TAC THEN REWRITE_TAC[PRIME] THEN
 274   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
 275   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[PHI_1; ARITH] THEN
 276   MP_TAC(SPEC `n:num` FINITE_NUMBER_SEGMENT) THEN
 277   ASM_SIMP_TAC[PHI_ANOTHER; HAS_SIZE] THEN
 278   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THEN
 279   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 280    `{m | 0 < m /\ m < n /\ coprime (m,n)} = {m | 0 < m /\ m < n}` THEN
 281   CONJ_TAC THENL
 282    [ALL_TAC;
 283     REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 284     AP_TERM_TAC THEN ABS_TAC THEN
 285     REWRITE_TAC[COPRIME_SYM] THEN CONV_TAC TAUT] THEN
 286   EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
 287   MATCH_MP_TAC CARD_SUBSET_EQ THEN ASM_REWRITE_TAC[] THEN
 288   SIMP_TAC[SUBSET; IN_ELIM_THM]);;
 289
 290 let PHI_PRIME = prove
 291  (`!p. prime p ==> phi p = p - 1`,
 292   MESON_TAC[PHI_PRIME_EQ]);;
 293
 294 (* ------------------------------------------------------------------------- *)
 295 (* Fermat's Little theorem.                                                  *)
 296 (* ------------------------------------------------------------------------- *)
 297
 298 let DIFFERENCE_POS_LEMMA = prove
 299  (`b <= a /\
 300    (?x1 x2. x1 * n + a = x2 * n + b)
 301    ==> ?x. a = x * n + b`,
 302   STRIP_TAC THEN EXISTS_TAC `x2 - x1` THEN
 303   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
 304   REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN ARITH_TAC);;
 305
 306 let ITSET_MODMULT = prove
 307  (`!n s. FINITE s /\ ~(n = 0) /\ ~(n = 1) /\ coprime(a,n)
 308        ==> (!b. b IN s ==> b < n)
 309            ==> (ITSET (\x y. (x * y) MOD n) (IMAGE (\b. (a * b) MOD n) s) 1 =
 310                 (a EXP (CARD s) * ITSET (\x y. (x * y) MOD n) s 1) MOD n)`,
 311   GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
 312   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[] THEN
 313   ASM_CASES_TAC `coprime(a,n)` THEN ASM_REWRITE_TAC[] THEN
 314   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 315   MP_TAC(ISPECL [`\x y. (x * y) MOD n`; `1`] FINITE_RECURSION) THEN
 316   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
 317    [ASM_SIMP_TAC[MOD_MULT_RMOD] THEN REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
 318   STRIP_TAC THEN
 319   ASM_SIMP_TAC[IMAGE_CLAUSES; CARD_CLAUSES; FINITE_IMAGE] THEN CONJ_TAC THENL
 320    [REWRITE_TAC[EXP; MULT_CLAUSES] THEN STRIP_TAC THEN CONV_TAC SYM_CONV THEN
 321     MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `0` THEN
 322     REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 323     MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
 324     ALL_TAC] THEN
 325   X_GEN_TAC `b:num` THEN X_GEN_TAC `s:num->bool` THEN
 326   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
 327   REWRITE_TAC[IN_INSERT] THEN
 328   REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
 329   REWRITE_TAC[FORALL_AND_THM] THEN
 330   ASM_CASES_TAC `!b. b IN s ==> b < n` THEN ASM_REWRITE_TAC[] THEN
 331   DISCH_TAC THEN SIMP_TAC[] THEN
 332   DISCH_THEN(MP_TAC o SPEC `b:num`) THEN REWRITE_TAC[] THEN DISCH_TAC THEN
 333   SUBGOAL_THEN `~((a * b) MOD n IN IMAGE (\b. (a * b) MOD n) s)`
 334    (fun th -> REWRITE_TAC[th])
 335   THENL
 336    [REWRITE_TAC[IN_IMAGE] THEN
 337     DISCH_THEN(X_CHOOSE_THEN `c:num` MP_TAC) THEN
 338     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 339     ASM_SIMP_TAC[GSYM CONG] THEN DISCH_TAC THEN
 340     UNDISCH_TAC `~(b:num IN s)` THEN REWRITE_TAC[] THEN
 341     SUBGOAL_THEN `b:num = c` (fun th -> ASM_REWRITE_TAC[th]) THEN
 342     SUBGOAL_THEN `b MOD n = c MOD n` MP_TAC THENL
 343      [ASM_SIMP_TAC[GSYM CONG] THEN
 344       MATCH_MP_TAC CONG_MULT_LCANCEL THEN
 345       EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 346     ASM_SIMP_TAC[MOD_LT]; ALL_TAC] THEN
 347   REWRITE_TAC[EXP] THEN
 348   ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD] THEN
 349   REWRITE_TAC[MULT_AC]);;
 350
 351 let ITSET_MODMULT_COPRIME = prove
 352  (`!n s. FINITE s /\ (!b. b IN s ==> coprime(b,n)) /\ ~(n = 0)
 353          ==> coprime(ITSET (\x y. (x * y) MOD n) s 1,n)`,
 354   GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
 355   REWRITE_TAC[IMP_CONJ] THEN
 356   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 357   MP_TAC(ISPECL [`\x y. (x * y) MOD n`; `1`] FINITE_RECURSION) THEN
 358   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
 359    [ASM_SIMP_TAC[MOD_MULT_RMOD] THEN REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
 360   STRIP_TAC THEN
 361   ASM_SIMP_TAC[IMAGE_CLAUSES; CARD_CLAUSES; FINITE_IMAGE] THEN
 362   REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_1] THEN
 363   REWRITE_TAC[IN_INSERT] THEN
 364   REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
 365   REWRITE_TAC[FORALL_AND_THM] THEN
 366   MAP_EVERY X_GEN_TAC [`x:num`; `s:num->bool`] THEN
 367   ASM_CASES_TAC `!b. b IN s ==> coprime(b,n)` THEN ASM_REWRITE_TAC[] THEN
 368   STRIP_TAC THEN DISCH_THEN(MP_TAC o SPEC `x:num`) THEN
 369   ASM_SIMP_TAC[COPRIME_MOD; ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_MUL]);;
 370
 371 let FERMAT_LITTLE = prove
 372  (`!a n. coprime(a,n) ==> (a EXP (phi n) == 1) (mod n)`,
 373   REPEAT GEN_TAC THEN
 374   ASM_CASES_TAC `n = 0` THEN
 375   ASM_SIMP_TAC[COPRIME_0; PHI_0; CONG_MOD_0] THEN CONV_TAC NUM_REDUCE_CONV THEN
 376   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[CONG_MOD_1] THEN DISCH_TAC THEN
 377   SUBGOAL_THEN
 378    `{ c | ?b. 0 < b /\ b < n /\ coprime(b,n) /\ (c = (a * b) MOD n) } =
 379     { b | 0 < b /\ b < n /\ coprime(b,n) }`
 380   MP_TAC THENL
 381    [REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 382     X_GEN_TAC `c:num` THEN EQ_TAC THENL
 383      [DISCH_THEN(X_CHOOSE_THEN `b:num` MP_TAC) THEN
 384       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 385       DISCH_THEN SUBST1_TAC THEN ASM_SIMP_TAC[DIVISION] THEN
 386       MATCH_MP_TAC(TAUT `b /\ (~a ==> ~b) ==> a /\ b`) THEN
 387       SIMP_TAC[ARITH_RULE `~(0 < n) <=> (n = 0)`] THEN
 388       ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_SIMP_TAC[COPRIME_0] THEN
 389       SUBGOAL_THEN `coprime(n,a * b)` MP_TAC THENL
 390        [MATCH_MP_TAC COPRIME_MUL THEN
 391         ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 392       SUBGOAL_THEN `a * b = (a * b) DIV n * n + (a * b) MOD n`
 393        (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 394       THENL [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 395       REWRITE_TAC[coprime] THEN REPEAT STRIP_TAC THEN
 396       FIRST_X_ASSUM MATCH_MP_TAC THEN
 397       ASM_SIMP_TAC[DIVIDES_ADD; DIVIDES_LMUL; DIVIDES_REFL]; ALL_TAC] THEN
 398     STRIP_TAC THEN MP_TAC(SPECL [`a:num`; `n:num`] BEZOUT) THEN
 399     DISCH_THEN(X_CHOOSE_THEN `d:num`
 400      (X_CHOOSE_THEN `x:num` (X_CHOOSE_THEN `y:num`
 401         (CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)))) THEN
 402     SUBGOAL_THEN `d = 1` SUBST_ALL_TAC THENL
 403      [ASM_MESON_TAC[coprime]; ALL_TAC] THEN
 404     STRIP_TAC THENL
 405      [EXISTS_TAC `(c * x) MOD n` THEN
 406       MATCH_MP_TAC(TAUT `(~a ==> ~c) /\ b /\ c /\ d ==> a /\ b /\ c /\ d`) THEN
 407       CONJ_TAC THENL
 408        [SIMP_TAC[ARITH_RULE `~(0 < n) <=> (n = 0)`] THEN
 409         ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_SIMP_TAC[COPRIME_0];
 410         ALL_TAC] THEN
 411       ASM_SIMP_TAC[DIVISION] THEN CONJ_TAC THENL
 412        [SUBGOAL_THEN `coprime(n,c * x)` MP_TAC THENL
 413          [MATCH_MP_TAC COPRIME_MUL THEN
 414           ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
 415           REWRITE_TAC[coprime; GSYM DIVIDES_ONE] THEN
 416           FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 417           SIMP_TAC[DIVIDES_SUB; DIVIDES_LMUL; DIVIDES_RMUL; DIVIDES_REFL];
 418           ALL_TAC] THEN
 419         SUBGOAL_THEN `c * x = (c * x) DIV n * n + (c * x) MOD n`
 420          (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 421         THENL [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 422         REWRITE_TAC[coprime] THEN REPEAT STRIP_TAC THEN
 423         FIRST_X_ASSUM MATCH_MP_TAC THEN
 424         ASM_SIMP_TAC[DIVIDES_ADD; DIVIDES_LMUL; DIVIDES_REFL]; ALL_TAC] THEN
 425       ASM_SIMP_TAC[MOD_MULT_RMOD] THEN CONV_TAC SYM_CONV THEN
 426       MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `c * y:num` THEN
 427       ASM_REWRITE_TAC[GSYM MULT_ASSOC] THEN
 428       ONCE_REWRITE_TAC[ARITH_RULE
 429        `(a * c * x = b:num) <=> (c * a * x = b)`] THEN
 430       FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
 431        `(a - b = 1) ==> (a = b + 1)`)) THEN
 432       REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_CLAUSES; MULT_AC];
 433
 434       EXISTS_TAC `(c * (n - y MOD n)) MOD n` THEN
 435       MATCH_MP_TAC(TAUT `(~a ==> ~c) /\ b /\ c /\ d ==> a /\ b /\ c /\ d`) THEN
 436       CONJ_TAC THENL
 437        [SIMP_TAC[ARITH_RULE `~(0 < n) <=> (n = 0)`] THEN
 438         ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_SIMP_TAC[COPRIME_0];
 439         ALL_TAC] THEN
 440       ASM_SIMP_TAC[DIVISION] THEN CONJ_TAC THENL
 441        [SUBGOAL_THEN `coprime(n,c * (n - y MOD n))` MP_TAC THENL
 442          [MATCH_MP_TAC COPRIME_MUL THEN
 443           ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[] THEN
 444           REWRITE_TAC[coprime; GSYM DIVIDES_ONE] THEN
 445           FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 446           X_GEN_TAC `e:num` THEN STRIP_TAC THEN MATCH_MP_TAC DIVIDES_SUB THEN
 447           ASM_SIMP_TAC[DIVIDES_RMUL; DIVIDES_REFL] THEN
 448           MATCH_MP_TAC DIVIDES_LMUL THEN
 449           SUBGOAL_THEN `y = (y DIV n) * n + y MOD n` SUBST1_TAC THENL
 450            [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 451           MATCH_MP_TAC DIVIDES_ADD THEN
 452           ASM_SIMP_TAC[DIVIDES_LMUL; DIVIDES_REFL] THEN
 453           MATCH_MP_TAC DIVIDES_ADD_REVR THEN
 454           EXISTS_TAC `n - y MOD n` THEN ASM_REWRITE_TAC[] THEN
 455           ASM_SIMP_TAC[ARITH_RULE `m < n ==> ((n - m) + m = n:num)`;
 456                        DIVISION];
 457           ALL_TAC] THEN
 458         SUBGOAL_THEN `!x. c * x = (c * x) DIV n * n + (c * x) MOD n`
 459          (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 460         THENL [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 461         REWRITE_TAC[coprime] THEN REPEAT STRIP_TAC THEN
 462         FIRST_X_ASSUM MATCH_MP_TAC THEN
 463         ASM_SIMP_TAC[DIVIDES_ADD; DIVIDES_LMUL; DIVIDES_REFL]; ALL_TAC] THEN
 464       ASM_SIMP_TAC[MOD_MULT_RMOD] THEN
 465       CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_UNIQ THEN
 466       ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIFFERENCE_POS_LEMMA THEN
 467       CONJ_TAC THENL
 468        [ONCE_REWRITE_TAC[ARITH_RULE
 469          `c <= a * c * x <=> c * 1 <= c * a * x`] THEN
 470         REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
 471         REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`; MULT_EQ_0;
 472                     SUB_EQ_0; DE_MORGAN_THM] THEN
 473         UNDISCH_TAC `coprime(a,n)` THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
 474         ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[COPRIME_0] THEN
 475         DISCH_TAC THEN ASM_SIMP_TAC[DIVISION; NOT_LE]; ALL_TAC] THEN
 476       MAP_EVERY EXISTS_TAC [`c * x`; `c * a * (1 + y DIV n)`] THEN
 477       REWRITE_TAC[LEFT_ADD_DISTRIB; LEFT_SUB_DISTRIB] THEN
 478       MATCH_MP_TAC(ARITH_RULE
 479        `y <= n /\ (a + n = x + y) ==> (a + (n - y) = x)`) THEN
 480       CONJ_TAC THENL
 481        [REWRITE_TAC[MULT_ASSOC] THEN REWRITE_TAC[LE_MULT_LCANCEL] THEN
 482         ASM_SIMP_TAC[LT_IMP_LE; DIVISION]; ALL_TAC] THEN
 483       REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
 484       REWRITE_TAC[GSYM ADD_ASSOC; GSYM MULT_ASSOC] THEN
 485       REWRITE_TAC[ARITH_RULE
 486        `(x + a * c * n = c * a * n + y) <=> (x = y)`] THEN
 487       FIRST_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
 488        `(n * x - a * y = 1) ==> (x * n = a * y + 1)`)) THEN
 489       SUBGOAL_THEN `y = (y DIV n) * n + y MOD n`
 490        (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 491       THENL [ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 492       REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
 493       REWRITE_TAC[MULT_AC; ADD_AC]];
 494     ALL_TAC] THEN
 495   SUBGOAL_THEN
 496    `{c | ?b. 0 < b /\ b < n /\ coprime (b,n) /\ (c = (a * b) MOD n)} =
 497     IMAGE (\b. (a * b) MOD n) {b | 0 < b /\ b < n /\ coprime (b,n)}`
 498   SUBST1_TAC THENL
 499    [REWRITE_TAC[IMAGE; EXTENSION; IN_ELIM_THM; CONJ_ASSOC]; ALL_TAC] THEN
 500   DISCH_THEN(MP_TAC o AP_TERM `ITSET (\x y. (x * y) MOD n)`) THEN
 501   DISCH_THEN(MP_TAC o C AP_THM `1`) THEN
 502   SUBGOAL_THEN `FINITE {b | 0 < b /\ b < n /\ coprime (b,n)} /\
 503                 !b. b IN {b | 0 < b /\ b < n /\ coprime (b,n)} ==> b < n`
 504   ASSUME_TAC THENL
 505    [CONJ_TAC THENL [ALL_TAC; SIMP_TAC[IN_ELIM_THM]] THEN
 506     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{b | 0 < b /\ b < n}` THEN
 507     REWRITE_TAC[REWRITE_RULE[HAS_SIZE] FINITE_NUMBER_SEGMENT] THEN
 508     SIMP_TAC[SUBSET; IN_ELIM_THM]; ALL_TAC] THEN
 509   ASM_SIMP_TAC[REWRITE_RULE[IMP_IMP]
 510     ITSET_MODMULT] THEN
 511   ASM_SIMP_TAC[GSYM PHI_ANOTHER] THEN
 512   DISCH_THEN(MP_TAC o AP_TERM `(MOD)`) THEN
 513   DISCH_THEN(MP_TAC o C AP_THM `n:num`) THEN
 514   ASM_SIMP_TAC[MOD_MOD_REFL] THEN ASM_SIMP_TAC[GSYM CONG] THEN
 515   GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o RAND_CONV)
 516    [ARITH_RULE `x = x * 1`] THEN
 517   GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [MULT_SYM] THEN
 518   DISCH_TAC THEN MATCH_MP_TAC CONG_MULT_LCANCEL THEN
 519   EXISTS_TAC `ITSET (\x y. (x * y) MOD n)
 520                     {b | 0 < b /\ b < n /\ coprime (b,n)} 1` THEN
 521   ASM_REWRITE_TAC[] THEN
 522   ASM_SIMP_TAC[ITSET_MODMULT_COPRIME; IN_ELIM_THM]);;
 523
 524 let FERMAT_LITTLE_PRIME = prove
 525  (`!p a. prime p ==> (a EXP p == a) (mod p)`,
 526   REPEAT STRIP_TAC THEN
 527   FIRST_ASSUM(MP_TAC o SPEC `a:num` o MATCH_MP PRIME_COPRIME) THEN
 528   ONCE_REWRITE_TAC[COPRIME_SYM] THEN STRIP_TAC THENL
 529    [ASM_REWRITE_TAC[EXP_ONE; CONG_REFL];
 530     MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC `0` THEN
 531     GEN_REWRITE_TAC RAND_CONV [CONG_SYM] THEN ASM_REWRITE_TAC[CONG_0] THEN
 532     ASM_MESON_TAC[DIVIDES_EXP; DIVIDES_EXP2; PRIME_0];
 533     ALL_TAC] THEN
 534   FIRST_ASSUM(MP_TAC o MATCH_MP FERMAT_LITTLE) THEN
 535   ASM_SIMP_TAC[snd(EQ_IMP_RULE (SPEC_ALL PHI_PRIME_EQ))] THEN
 536   REWRITE_TAC[cong; nat_mod] THEN
 537   DISCH_THEN(X_CHOOSE_THEN `q1:num` (X_CHOOSE_THEN `q2:num` MP_TAC)) THEN
 538   DISCH_THEN(MP_TAC o AP_TERM `( * ) a`) THEN
 539   REWRITE_TAC[LEFT_ADD_DISTRIB; GSYM(CONJUNCT2 EXP)] THEN
 540   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 541   REWRITE_TAC[MULT_CLAUSES; GSYM MULT_ASSOC] THEN
 542   ASM_MESON_TAC[ARITH_RULE `~(p = 0) ==> (SUC(p - 1) = p)`; PRIME_0]);;
 543
 544 (* ------------------------------------------------------------------------- *)
 545 (* Lucas's theorem.                                                          *)
 546 (* ------------------------------------------------------------------------- *)
 547
 548 let LUCAS_COPRIME_LEMMA = prove
 549  (`!m n a. ~(m = 0) /\ (a EXP m == 1) (mod n) ==> coprime(a,n)`,
 550   REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THENL
 551    [ASM_REWRITE_TAC[CONG_MOD_0; EXP_EQ_1] THEN
 552     ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[] THEN
 553     ONCE_REWRITE_TAC[COPRIME_SYM] THEN SIMP_TAC[COPRIME_1];
 554     ALL_TAC] THEN
 555   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[COPRIME_1] THEN
 556   REPEAT STRIP_TAC THEN
 557   REWRITE_TAC[coprime] THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
 558   UNDISCH_TAC `(a EXP m == 1) (mod n)` THEN
 559   ASM_SIMP_TAC[CONG] THEN
 560   SUBGOAL_THEN `1 MOD n = 1` SUBST1_TAC THENL
 561    [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `0` THEN
 562     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
 563     MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
 564     ALL_TAC] THEN
 565   DISCH_TAC THEN
 566   SUBGOAL_THEN `d divides (a EXP m) MOD n` MP_TAC THENL
 567    [ALL_TAC; ASM_SIMP_TAC[DIVIDES_ONE]] THEN
 568   MATCH_MP_TAC DIVIDES_ADD_REVR THEN
 569   EXISTS_TAC `a EXP m DIV n * n` THEN
 570   ASM_SIMP_TAC[GSYM DIVISION; DIVIDES_LMUL] THEN
 571   SUBGOAL_THEN `m = SUC(m - 1)` SUBST1_TAC THENL
 572    [UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC;
 573     ASM_SIMP_TAC[EXP; DIVIDES_RMUL]]);;
 574
 575 let LUCAS_WEAK = prove
 576  (`!a n. 2 <= n /\
 577          (a EXP (n - 1) == 1) (mod n) /\
 578          (!m. 0 < m /\ m < n - 1 ==> ~(a EXP m == 1) (mod n))
 579          ==> prime(n)`,
 580   REPEAT STRIP_TAC THEN
 581   ASM_SIMP_TAC[GSYM PHI_PRIME_EQ; PHI_LIMIT_STRONG; GSYM LE_ANTISYM;
 582                ARITH_RULE `2 <= n ==> ~(n = 0) /\ ~(n = 1)`] THEN
 583   FIRST_X_ASSUM(MP_TAC o SPEC `phi n`) THEN
 584   SUBGOAL_THEN `coprime(a,n)` (fun th -> SIMP_TAC[FERMAT_LITTLE; th]) THENL
 585    [MATCH_MP_TAC LUCAS_COPRIME_LEMMA THEN EXISTS_TAC `n - 1` THEN
 586     ASM_SIMP_TAC [ARITH_RULE `2 <= n ==> ~(n - 1 = 0)`]; ALL_TAC] THEN
 587   REWRITE_TAC[GSYM NOT_LT] THEN
 588   MATCH_MP_TAC(TAUT `a ==> ~(a /\ b) ==> ~b`) THEN
 589   ASM_SIMP_TAC[PHI_LOWERBOUND_1; ARITH_RULE `1 <= n ==> 0 < n`]);;
 590
 591 let LUCAS = prove
 592  (`!a n. 2 <= n /\
 593          (a EXP (n - 1) == 1) (mod n) /\
 594          (!p. prime(p) /\ p divides (n - 1)
 595               ==> ~(a EXP ((n - 1) DIV p) == 1) (mod n))
 596          ==> prime(n)`,
 597   REPEAT STRIP_TAC THEN
 598   FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `2 <= n ==> ~(n = 0)`)) THEN
 599   MATCH_MP_TAC LUCAS_WEAK THEN EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[] THEN
 600   REWRITE_TAC[TAUT `a ==> ~b <=> ~(a /\ b)`; GSYM NOT_EXISTS_THM] THEN
 601   ONCE_REWRITE_TAC[num_WOP] THEN
 602   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
 603   FIRST_ASSUM(ASSUME_TAC o MATCH_MP(ARITH_RULE `0 < n ==> ~(n = 0)`)) THEN
 604   SUBGOAL_THEN `m divides (n - 1)` MP_TAC THENL
 605    [REWRITE_TAC[divides] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
 606     ASM_SIMP_TAC[GSYM MOD_EQ_0] THEN
 607     MATCH_MP_TAC(ARITH_RULE `~(0 < n) ==> (n = 0)`) THEN DISCH_TAC THEN
 608     FIRST_X_ASSUM(MP_TAC o SPEC `(n - 1) MOD m`) THEN
 609     ASM_SIMP_TAC[DIVISION] THEN CONJ_TAC THENL
 610      [MATCH_MP_TAC LT_TRANS THEN EXISTS_TAC `m:num` THEN
 611       ASM_SIMP_TAC[DIVISION]; ALL_TAC] THEN
 612     MATCH_MP_TAC CONG_MULT_LCANCEL THEN
 613     EXISTS_TAC `a EXP ((n - 1) DIV m * m)` THEN CONJ_TAC THENL
 614      [ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_EXP THEN
 615       ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC LUCAS_COPRIME_LEMMA THEN
 616       EXISTS_TAC `m:num` THEN ASM_SIMP_TAC[]; ALL_TAC] THEN
 617     REWRITE_TAC[GSYM EXP_ADD] THEN
 618     ASM_SIMP_TAC[GSYM DIVISION] THEN REWRITE_TAC[MULT_CLAUSES] THEN
 619     ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[GSYM EXP_EXP] THEN
 620     UNDISCH_TAC `(a EXP (n - 1) == 1) (mod n)` THEN
 621     UNDISCH_TAC `(a EXP m == 1) (mod n)` THEN
 622     ASM_SIMP_TAC[CONG] THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 623     EXISTS_TAC `((a EXP m) MOD n) EXP ((n - 1) DIV m) MOD n` THEN
 624     CONJ_TAC THENL [ALL_TAC; ASM_SIMP_TAC[MOD_EXP_MOD]] THEN
 625     ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[MOD_EXP_MOD] THEN
 626     REWRITE_TAC[EXP_ONE]; ALL_TAC] THEN
 627   REWRITE_TAC[divides] THEN
 628   DISCH_THEN(X_CHOOSE_THEN `r:num` SUBST_ALL_TAC) THEN
 629   SUBGOAL_THEN `~(r = 1)` MP_TAC THENL
 630    [UNDISCH_TAC `m < m * r` THEN CONV_TAC CONTRAPOS_CONV THEN
 631     SIMP_TAC[MULT_CLAUSES; LT_REFL]; ALL_TAC] THEN
 632   DISCH_THEN(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
 633   DISCH_THEN(X_CHOOSE_THEN `p:num` MP_TAC) THEN STRIP_TAC THEN
 634   UNDISCH_TAC `!p. prime p /\ p divides m * r
 635                    ==> ~(a EXP ((m * r) DIV p) == 1) (mod n)` THEN
 636   DISCH_THEN(MP_TAC o SPEC `p:num`) THEN ASM_SIMP_TAC[DIVIDES_LMUL] THEN
 637   SUBGOAL_THEN `(m * r) DIV p = m * (r DIV p)` SUBST1_TAC THENL
 638    [MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
 639     UNDISCH_TAC `prime p` THEN
 640     ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
 641     ASM_SIMP_TAC[ARITH_RULE `~(p = 0) ==> 0 < p`] THEN
 642     DISCH_TAC THEN REWRITE_TAC[ADD_CLAUSES; GSYM MULT_ASSOC] THEN
 643     AP_TERM_TAC THEN UNDISCH_TAC `p divides r` THEN
 644     REWRITE_TAC[divides] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 645     ASM_SIMP_TAC[DIV_MULT] THEN REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
 646   UNDISCH_TAC `(a EXP m == 1) (mod n)` THEN
 647   ASM_SIMP_TAC[CONG] THEN
 648   DISCH_THEN(MP_TAC o C AP_THM `r DIV p` o AP_TERM `(EXP)`) THEN
 649   DISCH_THEN(MP_TAC o C AP_THM `n:num` o AP_TERM `(MOD)`) THEN
 650   ASM_SIMP_TAC[MOD_EXP_MOD] THEN
 651   REWRITE_TAC[EXP_EXP; EXP_ONE]);;
 652
 653 (* ------------------------------------------------------------------------- *)
 654 (* Prime factorizations.                                                     *)
 655 (* ------------------------------------------------------------------------- *)
 656
 657 let primefact = new_definition
 658   `primefact ps n <=> (ITLIST (*) ps 1 = n) /\ !p. MEM p ps ==> prime(p)`;;
 659
 660 let PRIMEFACT = prove
 661  (`!n. ~(n = 0) ==> ?ps. primefact ps n`,
 662   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN
 663   ASM_CASES_TAC `n = 1` THEN ASM_REWRITE_TAC[] THENL
 664    [REPEAT DISCH_TAC THEN EXISTS_TAC `[]:num list` THEN
 665     REWRITE_TAC[primefact; ITLIST; MEM]; ALL_TAC] THEN
 666   DISCH_TAC THEN DISCH_TAC THEN
 667   FIRST_ASSUM(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC o
 668     MATCH_MP PRIME_FACTOR) THEN
 669   UNDISCH_TAC `p divides n` THEN REWRITE_TAC[divides] THEN
 670   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
 671   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
 672   UNDISCH_TAC `~(p * m = 0)` THEN
 673   ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN DISCH_TAC THEN
 674   GEN_REWRITE_TAC (funpow 3 LAND_CONV) [ARITH_RULE `n = 1 * n`] THEN
 675   ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
 676   SUBGOAL_THEN `1 < p` (fun th -> REWRITE_TAC[th]) THENL
 677    [MATCH_MP_TAC(ARITH_RULE `~(p = 0) /\ ~(p = 1) ==> 1 < p`) THEN
 678     REPEAT STRIP_TAC THEN UNDISCH_TAC `prime p` THEN
 679     ASM_REWRITE_TAC[PRIME_0; PRIME_1]; ALL_TAC] THEN
 680   REWRITE_TAC[primefact] THEN
 681   DISCH_THEN(X_CHOOSE_THEN `ps:num list` ASSUME_TAC) THEN
 682   EXISTS_TAC `CONS (p:num) ps` THEN
 683   ASM_REWRITE_TAC[MEM; ITLIST] THEN ASM_MESON_TAC[]);;
 684
 685 let PRIMAFACT_CONTAINS = prove
 686  (`!ps n. primefact ps n ==> !p. prime p /\ p divides n ==> MEM p ps`,
 687   REPEAT GEN_TAC THEN REWRITE_TAC[primefact] THEN
 688   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 689   POP_ASSUM(SUBST1_TAC o SYM) THEN
 690   SPEC_TAC(`ps:num list`,`ps:num list`) THEN LIST_INDUCT_TAC THEN
 691   REWRITE_TAC[ITLIST; MEM] THENL
 692    [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
 693   STRIP_TAC THEN GEN_TAC THEN
 694   DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN
 695   DISCH_THEN(DISJ_CASES_TAC o MATCH_MP PRIME_DIVPROD) THEN
 696   ASM_MESON_TAC[prime; PRIME_1]);;
 697
 698 let PRIMEFACT_VARIANT = prove
 699  (`!ps n. primefact ps n <=> (ITLIST (*) ps 1 = n) /\ ALL prime ps`,
 700   REPEAT GEN_TAC THEN REWRITE_TAC[primefact] THEN AP_TERM_TAC THEN
 701   SPEC_TAC(`ps:num list`,`ps:num list`) THEN LIST_INDUCT_TAC THEN
 702   ASM_REWRITE_TAC[MEM; ALL] THEN ASM_MESON_TAC[]);;
 703
 704 (* ------------------------------------------------------------------------- *)
 705 (* Variant of Lucas theorem.                                                 *)
 706 (* ------------------------------------------------------------------------- *)
 707
 708 let LUCAS_PRIMEFACT = prove
 709  (`2 <= n /\
 710    (a EXP (n - 1) == 1) (mod n) /\
 711    (ITLIST (*) ps 1 = n - 1) /\
 712    ALL (\p. prime p /\ ~(a EXP ((n - 1) DIV p) == 1) (mod n)) ps
 713    ==> prime n`,
 714   REPEAT STRIP_TAC THEN MATCH_MP_TAC LUCAS THEN
 715   EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[] THEN
 716   SUBGOAL_THEN `primefact ps (n - 1)` MP_TAC THENL
 717    [ASM_REWRITE_TAC[PRIMEFACT_VARIANT] THEN MATCH_MP_TAC ALL_IMP THEN
 718     EXISTS_TAC `\p. prime p /\ ~(a EXP ((n - 1) DIV p) == 1) (mod n)` THEN
 719     ASM_SIMP_TAC[]; ALL_TAC] THEN
 720   DISCH_THEN(ASSUME_TAC o MATCH_MP PRIMAFACT_CONTAINS) THEN
 721   X_GEN_TAC `p:num` THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN UNDISCH_TAC
 722    `ALL (\p. prime p /\ ~(a EXP ((n - 1) DIV p) == 1) (mod n)) ps` THEN
 723   SPEC_TAC(`ps:num list`,`ps:num list`) THEN LIST_INDUCT_TAC THEN
 724   SIMP_TAC[ALL; MEM] THEN ASM_MESON_TAC[]);;
 725
 726 (* ------------------------------------------------------------------------- *)
 727 (* Utility functions.                                                        *)
 728 (* ------------------------------------------------------------------------- *)
 729
 730 let even_num n =
 731   mod_num n num_2 =/ num_0;;
 732
 733 let odd_num = not o even_num;;
 734
 735 (* ------------------------------------------------------------------------- *)
 736 (* Least p >= 0 with x <= 2^p.                                               *)
 737 (* ------------------------------------------------------------------------- *)
 738
 739 let log2 =
 740   let rec log2 x y =
 741     if x </ num_1 then y
 742     else log2 (quo_num x num_2) (y +/ num_1) in
 743   fun x -> log2 (x -/ num_1) num_0;;
 744
 745 (* ------------------------------------------------------------------------- *)
 746 (* Raise number to power (x^m) modulo n.                                     *)
 747 (* ------------------------------------------------------------------------- *)
 748
 749 let rec powermod x m n =
 750   if m =/ num_0 then num_1 else
 751   let y = powermod x (quo_num m num_2) n in
 752   let z = mod_num (y */ y) n in
 753   if even_num m then z else
 754   mod_num (x */ z) n;;
 755
 756 (* ------------------------------------------------------------------------- *)
 757 (* Make a call to PARI/GP to factor a number into (probable) primes.         *)
 758 (* ------------------------------------------------------------------------- *)
 759
 760 let factor =
 761   let suck_file s = let data = string_of_file s in Sys.remove s; data in
 762   let extract_output s =
 763     let l0 = explode s in
 764     let l0' = rev l0 in
 765     let l1 = snd(chop_list(index "]" l0') l0') in
 766     let l2 = "["::rev(fst(chop_list(index "[" l1) l1)) in
 767     let tm = parse_term (implode l2) in
 768     map ((dest_numeral F_F dest_numeral) o dest_pair) (dest_list tm) in
 769   fun n ->
 770     if n =/ num_1 then [] else
 771     let filename = Filename.temp_file "pocklington" ".out" in
 772     let s = "echo 'print(factorint(" ^
 773             (string_of_num n) ^
 774             "))  \n quit' | gp >" ^ filename ^ " 2>/dev/null" in
 775     if Sys.command s = 0 then
 776       let output = suck_file filename in
 777       extract_output output
 778     else
 779        failwith "factor: Call to GP/PARI failed";;
 780
 781 (* ------------------------------------------------------------------------- *)
 782 (* Alternative giving multiset instead of set plus indices.                  *)
 783 (* ------------------------------------------------------------------------- *)
 784
 785 let multifactor =
 786   let rec multilist l =
 787     if l = [] then [] else
 788     let (x,n) = hd l in
 789     replicate x (Num.int_of_num n) @ multilist (tl l) in
 790   fun n -> multilist (factor n);;
 791
 792 (* ------------------------------------------------------------------------- *)
 793 (* Recursive creation of Pratt primality certificates.                       *)
 794 (* ------------------------------------------------------------------------- *)
 795
 796 type certificate =
 797     Prime_2
 798   | Primroot_and_factors of
 799       ((num * num list) * num * (num * certificate) list);;
 800
 801 let find_primitive_root =
 802   let rec find_primitive_root a m ms n =
 803     if gcd_num a n =/ num_1 &
 804        powermod a m n =/ num_1 &
 805        forall (fun k -> powermod a k n <>/ num_1) ms
 806     then a
 807     else find_primitive_root (a +/ num_1) m ms n in
 808   let find_primitive_root_from_2 = find_primitive_root num_2 in
 809   fun m ms n ->
 810     if n </ num_2 then failwith "find_primitive_root: input too small"
 811     else find_primitive_root_from_2 m ms n;;
 812
 813 let uniq_num =
 814   let rec uniq x l =
 815     match l with
 816       [] -> raise Unchanged
 817     | (h::t) -> if x =/ h then
 818                   try uniq x t
 819                   with Unchanged -> l
 820                 else x::(uniq h t) in
 821   fun l -> if l = [] then [] else uniq (hd l) (tl l);;
 822
 823 let setify_num s =
 824   let s' = sort (<=/) s in
 825   try uniq_num s' with Unchanged -> s';;
 826
 827 let certify_prime =
 828   let rec cert_prime n =
 829     if n <=/ num_2 then
 830        if n =/ num_2 then Prime_2
 831        else failwith "certify_prime: not a prime!"
 832     else
 833       let m = n -/ num_1 in
 834       let pfact = multifactor m in
 835       let primes = setify_num pfact in
 836       let ms = map (fun d -> div_num m d) primes in
 837       let a = find_primitive_root m ms n in
 838       Primroot_and_factors((n,pfact),a,map (fun n -> n,cert_prime n) primes) in
 839   fun n -> if length(multifactor n) = 1 then cert_prime n
 840            else failwith "certify_prime: input is not a prime";;
 841
 842 (* ------------------------------------------------------------------------- *)
 843 (* Relatively efficient evaluation of "(a EXP m == 1) (mod n)".              *)
 844 (* ------------------------------------------------------------------------- *)
 845
 846 let EXP_EQ_MOD_CONV =
 847   let pth = prove
 848    (`~(n = 0)
 849      ==> ((a EXP 0) MOD n = 1 MOD n) /\
 850          ((a EXP (NUMERAL (BIT0 m))) MOD n =
 851                 let b = (a EXP (NUMERAL m)) MOD n in
 852                 (b * b) MOD n) /\
 853          ((a EXP (NUMERAL (BIT1 m))) MOD n =
 854                 let b = (a EXP (NUMERAL m)) MOD n in
 855                 (a * ((b * b) MOD n)) MOD n)`,
 856     DISCH_TAC THEN REWRITE_TAC[EXP] THEN
 857     REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN
 858     REWRITE_TAC[EXP; EXP_ADD] THEN
 859     CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 860     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD] THEN
 861     REWRITE_TAC[MULT_ASSOC] THEN
 862     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD] THEN
 863     ONCE_REWRITE_TAC[MULT_SYM] THEN
 864     REWRITE_TAC[MULT_ASSOC] THEN
 865     ASM_SIMP_TAC[MOD_MULT_LMOD; MOD_MULT_RMOD])
 866   and pth_cong = SPEC_ALL CONG
 867   and n_tm = `n:num` in
 868   let raw_conv tm =
 869     let ntm = rand(rand tm) in
 870     let th1 = INST [ntm,n_tm] pth_cong in
 871     let th2 = EQF_ELIM(NUM_EQ_CONV(rand(lhand(concl th1)))) in
 872     let th3 = REWR_CONV (MP th1 th2) tm in
 873     let th4 = MP (INST [ntm,n_tm] pth) th2 in
 874     let th4a,th4b = CONJ_PAIR th4 in
 875     let conv_base = GEN_REWRITE_CONV I [th4a]
 876     and conv_step = GEN_REWRITE_CONV I [th4b] in
 877     let rec conv tm =
 878       try conv_base tm with Failure _ ->
 879       (conv_step THENC
 880        RAND_CONV conv THENC
 881        let_CONV THENC
 882        NUM_REDUCE_CONV) tm in
 883     let th5 = (LAND_CONV conv THENC NUM_REDUCE_CONV) (rand(concl th3)) in
 884     TRANS th3 th5 in
 885   let gconv_net = itlist (uncurry net_of_conv)
 886    [`(a EXP m == 1) (mod n)`,raw_conv] empty_net in
 887   REWRITES_CONV gconv_net;;
 888
 889 (* ------------------------------------------------------------------------- *)
 890 (* HOL checking of such a certificate. We retain a cache for efficiency.     *)
 891 (* ------------------------------------------------------------------------- *)
 892
 893 let prime_theorem_cache = ref [];;
 894
 895 let rec lookup_under_num n l =
 896   if l = [] then failwith "lookup_under_num" else
 897   let h = hd l in
 898   if fst h =/ n then snd h
 899   else lookup_under_num n (tl l);;
 900
 901 let check_certificate =
 902   let n_tm = `n:num`
 903   and a_tm = `a:num`
 904   and ps_tm = `ps:num list`
 905   and SIMPLE_REWRITE_CONV = REWRITE_CONV[]
 906   and CONJ_AC_SORTED = TAUT `(a /\ a /\ b <=> a /\ b) /\ (a /\ a <=> a)` in
 907   let CLEAN_RULE = CONV_RULE
 908     (REWRITE_CONV[ITLIST; ALL; CONJ_AC_SORTED] THENC
 909      ONCE_DEPTH_CONV NUM_SUB_CONV THENC
 910      DEPTH_CONV NUM_MULT_CONV THENC
 911      ONCE_DEPTH_CONV NUM_DIV_CONV THENC
 912      ONCE_DEPTH_CONV(NUM_EQ_CONV ORELSEC NUM_LE_CONV) THENC
 913      SIMPLE_REWRITE_CONV) in
 914   let rec check_certificate cert =
 915     match cert with
 916       Prime_2 ->
 917           PRIME_2
 918     | Primroot_and_factors((n,ps),a,ncerts) ->
 919           try lookup_under_num n (!prime_theorem_cache) with Failure _ ->
 920           let th1 = INST [mk_numeral n,n_tm;
 921                           mk_flist (map mk_numeral ps),ps_tm;
 922                           mk_numeral a,a_tm]
 923                          LUCAS_PRIMEFACT in
 924           let th2 = CLEAN_RULE th1 in
 925           let th3 = ONCE_DEPTH_CONV EXP_EQ_MOD_CONV (concl th2) in
 926           let th4 = CONV_RULE SIMPLE_REWRITE_CONV (EQ_MP th3 th2) in
 927           let ants = conjuncts(lhand(concl th4)) in
 928           let certs =
 929             map (fun t -> lookup_under_num (dest_numeral(rand t)) ncerts)
 930                 ants in
 931           let ths = map check_certificate certs in
 932           let fth = MP th4 (end_itlist CONJ ths) in
 933           prime_theorem_cache := (n,fth)::(!prime_theorem_cache); fth in
 934   check_certificate;;
 935
 936 (* ------------------------------------------------------------------------- *)
 937 (* Hence a primality-proving rule.                                           *)
 938 (* ------------------------------------------------------------------------- *)
 939
 940 let PROVE_PRIME = check_certificate o certify_prime;;
 941
 942 (* ------------------------------------------------------------------------- *)
 943 (* Rule to generate prime factorization theorems.                            *)
 944 (* ------------------------------------------------------------------------- *)
 945
 946 let PROVE_PRIMEFACT =
 947   let pth = SPEC_ALL PRIMEFACT_VARIANT
 948   and start_CONV = PURE_REWRITE_CONV[ITLIST; ALL] THENC NUM_REDUCE_CONV
 949   and ps_tm = `ps:num list`
 950   and n_tm = `n:num` in
 951   fun n ->
 952      let pfact = multifactor n in
 953      let th1 = INST [mk_flist(map mk_numeral pfact),ps_tm;
 954                      mk_numeral n,n_tm] pth in
 955      let th2 = TRANS th1 (start_CONV(rand(concl th1))) in
 956      let ths = map PROVE_PRIME pfact in
 957      EQ_MP (SYM th2) (end_itlist CONJ ths);;
 958
 959 (* ------------------------------------------------------------------------- *)
 960 (* Conversion for truth or falsity of primality assertion.                   *)
 961 (* ------------------------------------------------------------------------- *)
 962
 963 let PRIME_TEST =
 964   let NOT_PRIME_THM = prove
 965    (`((m = 1) <=> F) ==> ((m = p) <=> F) ==> (m * n = p) ==> (prime(p) <=> F)`,
 966     MESON_TAC[prime; divides])
 967   and m_tm = `m:num` and n_tm = `n:num` and p_tm = `p:num` in
 968   fun tm ->
 969     let p = dest_numeral tm in
 970     if p =/ Int 0 then EQF_INTRO PRIME_0
 971     else if p =/ Int 1 then EQF_INTRO PRIME_1 else
 972     let pfact = multifactor p in
 973     if length pfact = 1 then
 974      (remark ("proving that " ^ string_of_num p ^ " is prime");
 975       EQT_INTRO(PROVE_PRIME p))
 976     else
 977      (remark ("proving that " ^ string_of_num p ^ " is composite");
 978       let m = hd pfact and n = end_itlist ( */ ) (tl pfact) in
 979       let th0 = INST [mk_numeral m,m_tm; mk_numeral n,n_tm; mk_numeral p,p_tm]
 980                      NOT_PRIME_THM in
 981       let th1 = MP th0 (NUM_EQ_CONV (lhand(lhand(concl th0)))) in
 982       let th2 = MP th1 (NUM_EQ_CONV (lhand(lhand(concl th1)))) in
 983       MP th2 (NUM_MULT_CONV(lhand(lhand(concl th2)))));;
 984
 985 let PRIME_CONV =
 986   let prime_tm = `prime` in
 987   fun tm0 ->
 988     let ptm,tm = dest_comb tm0 in
 989     if ptm <> prime_tm then failwith "expected term of form prime(n)"
 990     else PRIME_TEST tm;;
 991
 992 (* ------------------------------------------------------------------------- *)
 993 (* Example.                                                                  *)
 994 (* ------------------------------------------------------------------------- *)
 995
 996 map (time PRIME_TEST o mk_small_numeral) (0--50);;
 997
 998 time PRIME_TEST `65535`;;
 999
1000 time PRIME_TEST `65536`;;
1001
1002 time PRIME_TEST `65537`;;
1003
1004 time PROVE_PRIMEFACT (Int 222);;
1005
1006 time PROVE_PRIMEFACT (Int 151);;
1007
1008 (* ------------------------------------------------------------------------- *)
1009 (* The "Landau trick" in Erdos's proof of Chebyshev-Bertrand theorem.        *)
1010 (* ------------------------------------------------------------------------- *)
1011
1012 map (time PRIME_TEST o mk_small_numeral)
1013   [3; 5; 7; 13; 23; 43; 83; 163; 317; 631; 1259; 2503; 4001];;