Examples/lucas_lehmer.ml

   1 (* ========================================================================= *)
   2 (* The Lucas-Lehmer test.                                                    *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/iter.ml";;
   6 needs "Library/pocklington.ml";;
   7 needs "Library/floor.ml";;
   8 needs "Multivariate/vectors.ml";;
   9 needs "100/sqrt.ml";;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Relate real powers to iteration.                                          *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let REAL_POW_ITER = prove
  16  (`!x n. x pow n = ITER n (\y. x * y) (&1)`,
  17   GEN_TAC THEN INDUCT_TAC THEN
  18   ASM_REWRITE_TAC[ITER; real_pow]);;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Basic definition of the Lucas-Lehmer sequence. To avoid troubles with     *)
  22 (* cutoff subtraction and keep things in N we use m^2 + (p - 2) not m^2 - 2. *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let llseq = define
  26  `llseq p 0 = 4 MOD p /\
  27   llseq p (SUC n) = ((llseq p n) EXP 2 + (p - 2)) MOD p`;;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Closed form for the Lucas-Lehmer sequence.                                *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let LLSEQ_CLOSEDFORM = prove
  34  (`!p n. ~(p = 0)
  35          ==> ?x. llseq p n = x MOD p /\
  36                  &x = (&2 + sqrt(&3)) pow (2 EXP n) +
  37                       (&2 - sqrt(&3)) pow (2 EXP n)`,
  38   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
  39   INDUCT_TAC THENL
  40    [EXISTS_TAC `4` THEN REWRITE_TAC[llseq; EXP] THEN REAL_ARITH_TAC;
  41     ALL_TAC] THEN
  42   FIRST_X_ASSUM(X_CHOOSE_THEN `x:num` STRIP_ASSUME_TAC) THEN
  43   EXISTS_TAC `x EXP 2 - 2` THEN ASM_REWRITE_TAC[llseq] THEN
  44   SUBGOAL_THEN `2 <= x EXP 2` ASSUME_TAC THENL
  45    [MATCH_MP_TAC(ARITH_RULE `2 EXP 2 <= x ==> 2 <= x`) THEN
  46     REWRITE_TAC[EXP_MONO_LE; ARITH_EQ] THEN
  47     ASM_REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN
  48     MATCH_MP_TAC(REAL_ARITH
  49      `x <= y /\ y pow 1 <= y pow n /\ &0 <= z pow n
  50       ==> x <= y pow n + z pow n`) THEN
  51     REPEAT CONJ_TAC THENL
  52      [SIMP_TAC[REAL_LE_ADDR; SQRT_POS_LE; REAL_POS];
  53       MATCH_MP_TAC REAL_POW_MONO THEN
  54       SIMP_TAC[LE_1; EXP_EQ_0; ARITH_EQ] THEN
  55       MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> &1 <= &2 + x`) THEN
  56       SIMP_TAC[SQRT_POS_LE; REAL_POS];
  57       MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_SUB_LE] THEN
  58       MATCH_MP_TAC REAL_LE_LSQRT THEN CONV_TAC REAL_RAT_REDUCE_CONV];
  59     ALL_TAC] THEN
  60   CONJ_TAC THENL
  61    [ASM_CASES_TAC `p = 1` THENL [ASM_REWRITE_TAC[MOD_1]; ALL_TAC] THEN
  62     TRANS_TAC EQ_TRANS `(x EXP 2 + (p - 2)) MOD p` THEN CONJ_TAC THENL
  63      [ALL_TAC;
  64       ASM_SIMP_TAC[ARITH_RULE
  65        `2 <= x /\ ~(p = 0) /\ ~(p = 1) ==> x + p - 2 = (x - 2) + p`]] THEN
  66     FIRST_ASSUM(fun t -> ONCE_REWRITE_TAC[GSYM(MATCH_MP MOD_ADD_MOD t)]) THENL
  67      [ASM_MESON_TAC[MOD_EXP_MOD];
  68       ASM_SIMP_TAC[MOD_REFL; ADD_CLAUSES; MOD_MOD_REFL]];
  69     ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB; GSYM REAL_OF_NUM_POW] THEN
  70     REWRITE_TAC[ADD1; EXP_ADD; GSYM REAL_POW_MUL; REAL_ARITH
  71      `(x + y) pow 2 = x pow 2 + y pow 2 + &2 * x * y`] THEN
  72     REWRITE_TAC[REAL_ARITH `(&2 + s) * (&2 - s) = &4 - s pow 2`] THEN
  73     REWRITE_TAC[REAL_SQRT_POW_2; REAL_ABS_NUM; GSYM REAL_POW_POW] THEN
  74     CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  75     REWRITE_TAC[REAL_POW_ONE] THEN CONV_TAC REAL_RING]);;
  76
  77 (* ------------------------------------------------------------------------- *)
  78 (* The main Lucas-Lehmer theorem.                                            *)
  79 (* ------------------------------------------------------------------------- *)
  80
  81 let LUCAS_LEHMER = prove
  82  (`!p. 2 <= p /\ llseq (2 EXP p - 1) (p - 2) = 0 ==> prime(2 EXP p - 1)`,
  83   REPEAT STRIP_TAC THEN
  84   ONCE_REWRITE_TAC[PRIME_PRIME_FACTOR_SQRT] THEN
  85   SUBGOAL_THEN `2 <= 2 EXP p - 1` ASSUME_TAC THENL
  86    [MATCH_MP_TAC(ARITH_RULE `2 EXP 2 <= x ==> 2 <= x - 1`) THEN
  87     REWRITE_TAC[LE_EXP] THEN ASM_ARITH_TAC;
  88     ALL_TAC] THEN
  89   REPEAT(MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN
  90          CONJ_TAC THENL [ASM_ARITH_TAC; DISCH_TAC]) THEN
  91   DISCH_THEN(X_CHOOSE_THEN `q:num` STRIP_ASSUME_TAC) THEN
  92   FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_GE_2) THEN
  93   FIRST_ASSUM(ASSUME_TAC o MATCH_MP PRIME_IMP_NZ) THEN
  94   ABBREV_TAC
  95    `equiv =
  96     \x y. ?a b. integer a /\ integer b /\
  97                 x - y = (a + b * sqrt(&3)) * &q` THEN
  98   SUBGOAL_THEN `!x:real. (x == x) equiv` ASSUME_TAC THENL
  99    [REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 100     GEN_TAC THEN REPEAT(EXISTS_TAC `&0`) THEN
 101     REWRITE_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC;
 102     ALL_TAC] THEN
 103   SUBGOAL_THEN
 104    `!x y:real. (x == y) equiv <=> (y == x) equiv`
 105   ASSUME_TAC THENL
 106    [MATCH_MP_TAC(MESON[]
 107      `(!x y. P x y ==> P y x) ==> (!x y. P x y <=> P y x)`) THEN
 108     REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 109     MESON_TAC[INTEGER_CLOSED; REAL_ARITH
 110       `x - y:real = (a + b * s) * q ==> y - x = (--a + --b * s) * q`];
 111     ALL_TAC] THEN
 112   SUBGOAL_THEN
 113    `!x y z:real. (x == y) equiv /\ (y == z) equiv ==> (x == z) equiv`
 114   ASSUME_TAC THENL
 115    [REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 116     MESON_TAC[INTEGER_CLOSED; REAL_ARITH
 117       `x - y = (a + b * s) * q /\
 118        y - z = (a' + b' * s) * q
 119        ==> x - z:real = ((a + a') + (b + b') * s) * q`];
 120     ALL_TAC] THEN
 121   SUBGOAL_THEN
 122    `!k. ?a b. (&2 + sqrt(&3)) pow k = &a + &b * sqrt(&3)`
 123   STRIP_ASSUME_TAC THENL
 124    [INDUCT_TAC THENL
 125      [MAP_EVERY EXISTS_TAC [`1`; `0`] THEN REAL_ARITH_TAC;
 126       FIRST_X_ASSUM(X_CHOOSE_THEN `a:num` MP_TAC) THEN
 127       REWRITE_TAC[real_pow; LEFT_IMP_EXISTS_THM] THEN
 128       X_GEN_TAC `b:num` THEN DISCH_THEN SUBST1_TAC THEN
 129       MAP_EVERY EXISTS_TAC [`2 * a + 3 * b`; `2 * b + a`] THEN
 130       REWRITE_TAC[GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN
 131       MP_TAC(SPEC `&3` SQRT_POW_2) THEN REWRITE_TAC[REAL_POS] THEN
 132       CONV_TAC REAL_RING];
 133     ALL_TAC] THEN
 134   SUBGOAL_THEN
 135    `!x y. ((&2 + sqrt(&3)) * x == (&2 + sqrt(&3)) * y) equiv <=>
 136           (x == y) equiv`
 137   ASSUME_TAC THENL
 138    [SUBGOAL_THEN
 139      `!x y:real. (x == y) equiv <=> (x - y == &0) equiv`
 140      (fun th -> ONCE_REWRITE_TAC[th])
 141     THENL
 142      [REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN SIMP_TAC[REAL_SUB_RZERO];
 143       REWRITE_TAC[GSYM REAL_SUB_LDISTRIB]] THEN
 144     REPEAT GEN_TAC THEN SPEC_TAC(`x - y:real`,`x:real`) THEN
 145     X_GEN_TAC `x:real` THEN REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 146     REWRITE_TAC[REAL_SUB_RZERO] THEN EQ_TAC THEN
 147     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 148     MAP_EVERY X_GEN_TAC [`u:real`; `v:real`] THEN
 149     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 150     REWRITE_TAC[REAL_SUB_RZERO] THEN DISCH_TAC THENL
 151      [MAP_EVERY EXISTS_TAC [`&2 * u - &3 * v`; `&2 * v - u`];
 152       MAP_EVERY EXISTS_TAC [`&2 * u + &3 * v`; `&2 * v + u`]] THEN
 153     ASM_SIMP_TAC[INTEGER_CLOSED] THEN
 154     FIRST_X_ASSUM(MP_TAC o SYM) THEN
 155     MP_TAC(SPEC `&3` SQRT_POW_2) THEN REWRITE_TAC[REAL_POS] THEN
 156     CONV_TAC REAL_RING;
 157     ALL_TAC] THEN
 158   SUBGOAL_THEN
 159    `((&2 + sqrt(&3)) pow (2 EXP (p - 1)) == -- &1) equiv`
 160   ASSUME_TAC THENL
 161    [UNDISCH_THEN `!x y:real. (x == y) equiv <=> (y == x) equiv`
 162       (K ALL_TAC) THEN
 163     MP_TAC(ISPECL [`2 EXP p - 1`; `p - 2`] LLSEQ_CLOSEDFORM) THEN
 164     ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
 165     ASM_SIMP_TAC[MOD_EQ_0; LEFT_AND_EXISTS_THM] THEN
 166     ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
 167     DISCH_THEN(X_CHOOSE_THEN `r:num` (MP_TAC o
 168      AP_TERM `(*) ((&2 + sqrt(&3)) pow (2 EXP (p - 2)))`)) THEN
 169     REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
 170     REWRITE_TAC[GSYM REAL_POW_MUL; GSYM REAL_POW_2; REAL_POW_POW] THEN
 171     REWRITE_TAC[REAL_ARITH `(&2 + s) * (&2 - s) = &4 - s pow 2`] THEN
 172     REWRITE_TAC[REAL_SQRT_POW_2; REAL_ABS_NUM] THEN
 173     CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_POW_ONE] THEN
 174     REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
 175     ASM_SIMP_TAC[ARITH_RULE `2 <= p ==> SUC(p - 2) = p - 1`] THEN
 176     SUBGOAL_THEN
 177      `?a b. (&2 + sqrt(&3)) pow (2 EXP (p - 2)) = &a + &b * sqrt(&3)`
 178     STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 179     REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 180     REWRITE_TAC[REAL_SUB_RNEG] THEN DISCH_THEN SUBST1_TAC THEN
 181     ASM_REWRITE_TAC[] THEN
 182     FIRST_X_ASSUM(X_CHOOSE_THEN `s:num` SUBST1_TAC o
 183        REWRITE_RULE[divides]) THEN
 184     MAP_EVERY EXISTS_TAC [`&a * &r * &s`; `&b * &r * &s`] THEN
 185     SIMP_TAC[INTEGER_CLOSED; GSYM REAL_OF_NUM_MUL] THEN REAL_ARITH_TAC;
 186     ALL_TAC] THEN
 187   SUBGOAL_THEN
 188    `((&2 + sqrt(&3)) pow (2 EXP p) == &1) equiv`
 189   ASSUME_TAC THENL
 190    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cong]) THEN
 191     REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 192     REWRITE_TAC[LEFT_IMP_EXISTS_THM; REAL_ARITH
 193      `a - -- &1  = b <=> a = b - &1`] THEN
 194     MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
 195     SUBGOAL_THEN `p = (p - 1) + 1` SUBST1_TAC THENL
 196      [UNDISCH_TAC `2 <= p` THEN ARITH_TAC; ALL_TAC] THEN
 197     ASM_REWRITE_TAC[EXP_ADD; GSYM REAL_POW_POW] THEN
 198     EXISTS_TAC `&q * (a pow 2 + &3 * b pow 2) - &2 * a` THEN
 199     EXISTS_TAC `&2 * a * b * &q - &2 * b` THEN
 200     REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[INTEGER_CLOSED]; ALL_TAC]) THEN
 201     CONV_TAC NUM_REDUCE_CONV THEN
 202     MP_TAC(SPEC `&3` SQRT_POW_2) THEN REWRITE_TAC[REAL_POS] THEN
 203     CONV_TAC REAL_RING;
 204     ALL_TAC] THEN
 205   SUBGOAL_THEN
 206    `?k. 0 < k /\ k <= 2 EXP p - 1 /\
 207         !n. ((&2 + sqrt(&3)) pow n == &1) equiv <=> k divides n`
 208   STRIP_ASSUME_TAC THENL
 209    [MP_TAC(ISPEC `\x y:real. (x == y) equiv` ORDER_EXISTENCE_CARD) THEN
 210     REWRITE_TAC[REAL_POW_ITER] THEN DISCH_THEN MATCH_MP_TAC THEN
 211     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
 212      (MESON[CARD_SUBSET; FINITE_SUBSET; LE_TRANS; CARD_IMAGE_LE; FINITE_IMAGE]
 213      `!f:num#num->A t. s SUBSET IMAGE f t /\ FINITE t /\ CARD t <= n
 214             ==> FINITE s /\ CARD s <= n`) THEN
 215     EXISTS_TAC `\(a,b) y. (y == &a + &b * sqrt(&3)) equiv` THEN
 216     EXISTS_TAC `(0..q-1) CROSS (0..q-1)` THEN
 217     SIMP_TAC[CARD_CROSS; FINITE_CROSS; FINITE_NUMSEG; CARD_NUMSEG] THEN
 218     ASM_SIMP_TAC[SUB_ADD; SUB_0; LE_1; GSYM EXP_2; SUBSET] THEN
 219     REWRITE_TAC[FORALL_IN_GSPEC; IN_UNIV; IN_IMAGE; EXISTS_PAIR_THM] THEN
 220     X_GEN_TAC `n:num` THEN REWRITE_TAC[IN_CROSS; GSYM REAL_POW_ITER] THEN
 221     FIRST_X_ASSUM(X_CHOOSE_THEN `a:num` MP_TAC o SPEC `n:num`) THEN
 222     DISCH_THEN(X_CHOOSE_TAC `b:num`) THEN
 223     MAP_EVERY EXISTS_TAC [`a MOD q`; `b MOD q`] THEN
 224     ASM_SIMP_TAC[IN_NUMSEG; LE_0; DIVISION; FUN_EQ_THM;
 225                  ARITH_RULE `a <= q - 1 <=> a = 0 \/ a < q`] THEN
 226     MATCH_MP_TAC(MESON[]
 227      `(a == b) equiv /\
 228       ((a == b) equiv ==> !x. (x == a) equiv <=> (x == b) equiv)
 229       ==> !x. (x == a) equiv <=> (x == b) equiv`) THEN
 230     CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 231     REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 232     MAP_EVERY EXISTS_TAC [`&(a DIV q)`; `&(b DIV q)`] THEN
 233     REWRITE_TAC[INTEGER_CLOSED; REAL_RING
 234      `(a + b * s) - (a' + b' * s):real = (a'' + b'' * s) * q <=>
 235       a + b * s = (a'' * q + a') + (b'' * q + b') * s`] THEN
 236     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] THEN
 237     ASM_SIMP_TAC[GSYM DIVISION];
 238     SUBGOAL_THEN `k divides 2 EXP p` MP_TAC THENL
 239      [ASM_MESON_TAC[]; SIMP_TAC[DIVIDES_PRIMEPOW; PRIME_2]] THEN
 240     REWRITE_TAC[LE_LT; RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2] THEN
 241     ASM_SIMP_TAC[ARITH_RULE `k <= p - 1 ==> (k = p <=> p = 0)`] THEN
 242     REWRITE_TAC[EXP_EQ_0; ARITH_EQ] THEN
 243     DISCH_THEN(X_CHOOSE_THEN `i:num` STRIP_ASSUME_TAC) THEN
 244     SUBGOAL_THEN
 245      `((&2 + sqrt (&3)) pow (2 EXP (p - 1)) == &1) (equiv)`
 246     ASSUME_TAC THENL
 247      [ASM_REWRITE_TAC[] THEN SIMP_TAC[DIVIDES_EXP_LE; LE_REFL] THEN
 248       ASM_SIMP_TAC[ARITH_RULE `i < p ==> i <= p - 1`];
 249       ALL_TAC] THEN
 250     SUBGOAL_THEN `(&1 == -- &1) (equiv)` MP_TAC THENL
 251      [ASM_MESON_TAC[]; ALL_TAC] THEN
 252     REWRITE_TAC[cong] THEN EXPAND_TAC "equiv" THEN
 253     REWRITE_TAC[NOT_EXISTS_THM] THEN
 254     MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
 255     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 256     REWRITE_TAC[REAL_ARITH `&1 - -- &1 = &2`] THEN
 257     ASM_CASES_TAC `b = &0` THENL
 258      [ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
 259       DISCH_THEN(MP_TAC o AP_TERM `abs`) THEN REWRITE_TAC[REAL_ABS_MUL] THEN
 260       SUBGOAL_THEN `?q. abs a = &q` (CHOOSE_THEN SUBST1_TAC)
 261       THENL [ASM_MESON_TAC[integer]; REWRITE_TAC[REAL_ABS_NUM]] THEN
 262       REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
 263       DISCH_THEN(ASSUME_TAC o SYM) THEN
 264       MP_TAC PRIME_2 THEN REWRITE_TAC[prime; ARITH_EQ] THEN
 265       DISCH_THEN(MP_TAC o SPEC `q:num`) THEN ANTS_TAC THENL
 266        [REWRITE_TAC[divides] THEN ASM_MESON_TAC[MULT_SYM]; ALL_TAC] THEN
 267       DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THENL
 268        [ASM_MESON_TAC[NUM_REDUCE_CONV `2 <= 1`]; ALL_TAC] THEN
 269       SUBGOAL_THEN `2 divides (2 EXP p - 1) + 2` MP_TAC THENL
 270        [MATCH_MP_TAC DIVIDES_ADD THEN ASM_REWRITE_TAC[DIVIDES_REFL];
 271         ASM_SIMP_TAC[ARITH_RULE `~(n - 1 = 0) ==> n - 1 + 2 = n + 1`]] THEN
 272       REWRITE_TAC[DIVIDES_2; EVEN_ADD; EVEN_EXP; ARITH] THEN
 273       UNDISCH_TAC `2 <= p` THEN ARITH_TAC;
 274       DISCH_THEN(MP_TAC o MATCH_MP (REAL_FIELD
 275        `&2 = (a + b * x) * q
 276         ==> ~(b = &0) ==> x = (&2 - a * q) / (b * q)`)) THEN
 277       ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o AP_TERM `rational`) THEN
 278       SIMP_TAC[IRRATIONAL_SQRT_PRIME; PRIME_CONV `prime 3`] THEN
 279       ASM_MESON_TAC[RATIONAL_CLOSED; INTEGER_CLOSED]]]);;
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* Actual evaluation of the LL sequence.                                     *)
 283 (* ------------------------------------------------------------------------- *)
 284
 285 let ll_verbose = ref false;;
 286
 287 let LUCAS_LEHMER_RULE =
 288   let pth_base = prove
 289    (`llseq (2 EXP p - 1) 0 = 4 MOD (2 EXP p - 1)`,
 290     REWRITE_TAC[llseq])
 291   and pth_step = prove
 292    (`llseq (2 EXP p - 1) n = m
 293      ==> m * m + q = 2 EXP p * q + 2 + r /\ r < 2 EXP p - 1
 294          ==> llseq (2 EXP p - 1) (SUC n) = r`,
 295     REWRITE_TAC[llseq] THEN
 296     ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THEN
 297     CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[LT] THEN
 298     ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[] THEN
 299     CONV_TAC NUM_REDUCE_CONV THEN
 300     SIMP_TAC[MOD_1; ARITH_RULE `r < 1 <=> r = 0`] THEN
 301     REPEAT STRIP_TAC THEN MATCH_MP_TAC MOD_UNIQ THEN
 302     EXISTS_TAC `q + 1` THEN ASM_REWRITE_TAC[EXP_2] THEN
 303     MATCH_MP_TAC(ARITH_RULE `!p:num. (x + p) + y = p + z ==> x + y = z`) THEN
 304     EXISTS_TAC `q:num` THEN
 305     ASM_REWRITE_TAC[RIGHT_ADD_DISTRIB; LEFT_SUB_DISTRIB; MULT_CLAUSES] THEN
 306     MATCH_MP_TAC(ARITH_RULE
 307      `x + y - 1 + w = u + v + z + r + 2 /\ 2 EXP 2 <= y /\ w * 1 <= v
 308       ==> x + y - 1 - 2 = u + (v - w + z) + r`) THEN
 309     REWRITE_TAC[LE_MULT_LCANCEL; LE_EXP; EXP_EQ_0; ARITH_RULE
 310       `1 <= n <=> ~(n = 0)`] THEN
 311     CONV_TAC NUM_REDUCE_CONV THEN ASM_ARITH_TAC)
 312   and pconv_tt = GEN_REWRITE_CONV I [TAUT `T /\ T <=> T`]
 313   and p_tm = `p:num` and n_tm = `n:num` and m_tm = `m:num`
 314   and q_tm = `q:num` and r_tm = `r:num` in
 315   let ariconv =
 316     let BINOP2_CONV conv1 conv2 = COMB2_CONV (RAND_CONV conv1) conv2 in
 317     (BINOP2_CONV (BINOP2_CONV (LAND_CONV NUM_MULT_CONV THENC NUM_ADD_CONV)
 318                              (BINOP2_CONV NUM_MULT_CONV NUM_ADD_CONV THENC
 319                               NUM_ADD_CONV) THENC
 320                             NUM_EQ_CONV)
 321                  NUM_LT_CONV THENC pconv_tt) in
 322   fun p ->
 323     let th_base = CONV_RULE(RAND_CONV NUM_REDUCE_CONV)
 324      (INST [mk_small_numeral p,p_tm] pth_base)
 325     and th_step =  CONV_RULE(RAND_CONV(LAND_CONV NUM_REDUCE_CONV))
 326      (INST [mk_small_numeral p,p_tm] pth_step)
 327     and pp1 = pow2 p -/ Int 1 in
 328     let rec lucas_lehmer k =
 329       if k = 0 then th_base,dest_numeral(rand(concl th_base)) else
 330       let th1,mval = lucas_lehmer (k - 1) in
 331       let gofer() =
 332         let mtm = rand(concl th1) in
 333         let yval = power_num mval (Int 2) in
 334         let qval = quo_num yval pp1 and rval = mod_num yval pp1 -/ Int 2 in
 335         let th3 = INST [mk_small_numeral(k - 1),n_tm; mtm,m_tm;
 336                         mk_numeral qval,q_tm; mk_numeral rval,r_tm] th_step in
 337         let th4 = MP th3 th1 in
 338         let th5 = MP th4 (EQT_ELIM(ariconv(lhand(concl th4)))) in
 339         CONV_RULE (LAND_CONV(RAND_CONV NUM_SUC_CONV)) th5,rval in
 340       if !ll_verbose then
 341        (Format.print_string("Iteration "^string_of_int k^" of "^
 342                             string_of_int(p-2));
 343         Format.print_newline();
 344         time gofer())
 345       else gofer() in
 346     let th1,y = lucas_lehmer (p - 2) in
 347     if y <>/ Int 0 then failwith "LUCAS_LEHMER_RULE: not a prime" else
 348     let th2 = SPEC(mk_small_numeral p) LUCAS_LEHMER in
 349     let th3 = CONV_RULE
 350      (LAND_CONV(RAND_CONV(LAND_CONV
 351        (RAND_CONV NUM_SUB_CONV THENC K th1)))) th2 in
 352     MP th3 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th3))));;
 353
 354 (* ------------------------------------------------------------------------- *)
 355 (* Time a few small examples.                                                *)
 356 (* ------------------------------------------------------------------------- *)
 357
 358 ll_verbose := false;;
 359
 360 time LUCAS_LEHMER_RULE 3;;
 361 time LUCAS_LEHMER_RULE 5;;
 362 time LUCAS_LEHMER_RULE 7;;
 363 time LUCAS_LEHMER_RULE 13;;
 364 time LUCAS_LEHMER_RULE 17;;
 365 time LUCAS_LEHMER_RULE 19;;
 366 time LUCAS_LEHMER_RULE 31;;
 367 time LUCAS_LEHMER_RULE 61;;
 368 time LUCAS_LEHMER_RULE 89;;
 369 time LUCAS_LEHMER_RULE 107;;
 370 time LUCAS_LEHMER_RULE 127;;
 371 time LUCAS_LEHMER_RULE 521;;
 372 time LUCAS_LEHMER_RULE 607;;
 373
 374 (* ------------------------------------------------------------------------- *)
 375 (* These take a while, so they're commented out here.                        *)
 376 (* ------------------------------------------------------------------------- *)
 377
 378 (***
 379
 380 ll_verbose := true;;
 381
 382 time LUCAS_LEHMER_RULE 1279;;
 383 time LUCAS_LEHMER_RULE 2203;;
 384 time LUCAS_LEHMER_RULE 2281;;
 385 time LUCAS_LEHMER_RULE 3217;;
 386 time LUCAS_LEHMER_RULE 4253;;
 387 time LUCAS_LEHMER_RULE 4423;;
 388 time LUCAS_LEHMER_RULE 9689;;
 389 time LUCAS_LEHMER_RULE 9941;;
 390 time LUCAS_LEHMER_RULE 11213;;
 391 time LUCAS_LEHMER_RULE 19937;;
 392 time LUCAS_LEHMER_RULE 21701;;
 393 time LUCAS_LEHMER_RULE 23209;;
 394 time LUCAS_LEHMER_RULE 44497;;
 395 time LUCAS_LEHMER_RULE 86243;;
 396 time LUCAS_LEHMER_RULE 110503;;
 397 time LUCAS_LEHMER_RULE 132049;;
 398 time LUCAS_LEHMER_RULE 216091;;
 399 time LUCAS_LEHMER_RULE 756839;;
 400 time LUCAS_LEHMER_RULE 859433;;
 401 time LUCAS_LEHMER_RULE 1257787;;
 402 time LUCAS_LEHMER_RULE 1398269;;
 403 time LUCAS_LEHMER_RULE 2976221;;
 404 time LUCAS_LEHMER_RULE 3021377;;
 405 time LUCAS_LEHMER_RULE 6972593;;
 406 time LUCAS_LEHMER_RULE 13466917;;
 407 time LUCAS_LEHMER_RULE 20996011;;
 408 time LUCAS_LEHMER_RULE 24036583;;
 409 time LUCAS_LEHMER_RULE 25964951;;
 410 time LUCAS_LEHMER_RULE 30402457;;
 411
 412 ****)