100/wilson.ml

   1 (* ========================================================================= *)
   2 (* Wilson's theorem.                                                         *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/pocklington.ml";;
   7
   8 prioritize_num();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Definition of iterated product.                                           *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let product = new_definition `product = iterate ( * )`;;
  15
  16 let PRODUCT_CLAUSES = prove
  17  (`(!f. product {} f = 1) /\
  18    (!x f s. FINITE(s)
  19             ==> (product (x INSERT s) f =
  20                  if x IN s then product s f else f(x) * product s f))`,
  21   REWRITE_TAC[product; GSYM NEUTRAL_MUL] THEN
  22   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  23   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MUL]);;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Factorial in terms of products.                                           *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let FACT_PRODUCT = prove
  30  (`!n. FACT(n) = product(1..n) (\i. i)`,
  31   INDUCT_TAC THEN
  32   REWRITE_TAC[FACT; NUMSEG_CLAUSES; ARITH; PRODUCT_CLAUSES] THEN
  33   ASM_SIMP_TAC[ARITH_RULE `1 <= SUC n`; PRODUCT_CLAUSES; FINITE_NUMSEG] THEN
  34   REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
  35
  36 let FACT_PRODUCT_ALT = prove
  37  (`!n. FACT(n) = product(2..n) (\i. i)`,
  38   GEN_TAC THEN REWRITE_TAC[FACT_PRODUCT] THEN
  39   DISJ_CASES_TAC(ARITH_RULE `n = 0 \/ 1 <= n`) THEN
  40   ASM_REWRITE_TAC[num_CONV `1`; NUMSEG_CLAUSES] THEN
  41   REWRITE_TAC[ARITH; PRODUCT_CLAUSES; FACT] THEN
  42   ASM_SIMP_TAC[GSYM NUMSEG_LREC] THEN
  43   SIMP_TAC[PRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG; MULT_CLAUSES] THEN
  44   ARITH_TAC);;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* General "pairing up" theorem for products.                                *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let PRODUCT_PAIRUP_INDUCT = prove
  51  (`!f r n s. FINITE s /\ CARD s = n /\
  52              (!x:A. x IN s ==> ?!y. y IN s /\ ~(y = x) /\
  53                                     (f(x) * f(y) == 1) (mod r))
  54              ==> (product s f == 1) (mod r)`,
  55   GEN_TAC THEN GEN_TAC THEN
  56   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
  57   X_GEN_TAC `s:A->bool` THEN ASM_CASES_TAC `s:A->bool = {}` THEN
  58   ASM_REWRITE_TAC[PRODUCT_CLAUSES; CONG_REFL] THEN STRIP_TAC THEN
  59   ASM_CASES_TAC `n = 0` THENL [ASM_MESON_TAC[CARD_EQ_0]; ALL_TAC] THEN
  60   FIRST_X_ASSUM(X_CHOOSE_TAC `a:A` o
  61     GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
  62   FIRST_ASSUM(MP_TAC o SPEC `n - 2`) THEN
  63   ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 2 < n`] THEN
  64   FIRST_ASSUM(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[ASSUME `(a:A) IN s`] THEN
  65   REWRITE_TAC[EXISTS_UNIQUE] THEN
  66   DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
  67   DISCH_THEN(MP_TAC o SPEC `(s DELETE a) DELETE (b:A)`) THEN ANTS_TAC THENL
  68    [ASM_REWRITE_TAC[FINITE_DELETE] THEN
  69     SIMP_TAC[FINITE_DELETE; ASSUME `FINITE(s:A->bool)`; CARD_DELETE] THEN
  70     ASM_REWRITE_TAC[IN_DELETE] THEN CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
  71     X_GEN_TAC `x:A` THEN STRIP_TAC THEN
  72     FIRST_ASSUM(MP_TAC o C MATCH_MP (ASSUME `(x:A) IN s`)) THEN
  73     REWRITE_TAC[EXISTS_UNIQUE] THEN MATCH_MP_TAC MONO_EXISTS THEN
  74     X_GEN_TAC `y:A` THEN STRIP_TAC THEN CONJ_TAC THENL
  75      [ALL_TAC; ASM_MESON_TAC[]] THEN
  76     ASM_REWRITE_TAC[] THEN CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THENL
  77      [ASM_MESON_TAC[MULT_SYM]; ALL_TAC] THEN
  78     FIRST_X_ASSUM(MP_TAC o C MATCH_MP (ASSUME `(b:A) IN s`)) THEN
  79     REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
  80     DISCH_THEN(MP_TAC o SPECL [`a:A`; `x:A`] o CONJUNCT2) THEN
  81     ASM_MESON_TAC[MULT_SYM];
  82     ALL_TAC] THEN
  83   DISCH_TAC THEN
  84   SUBGOAL_THEN `s = (a:A) INSERT (b INSERT (s DELETE a DELETE b))`
  85   SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
  86   SIMP_TAC[PRODUCT_CLAUSES; FINITE_INSERT; FINITE_DELETE;
  87            ASSUME `FINITE(s:A->bool)`] THEN
  88   ASM_REWRITE_TAC[IN_INSERT; IN_DELETE; MULT_CLAUSES] THEN
  89   REWRITE_TAC[MULT_ASSOC] THEN
  90   ONCE_REWRITE_TAC[SYM(NUM_REDUCE_CONV `1 * 1`)] THEN
  91   MATCH_MP_TAC CONG_MULT THEN ASM_REWRITE_TAC[]);;
  92
  93 let PRODUCT_PAIRUP = prove
  94  (`!f r s. FINITE s /\
  95            (!x:A. x IN s ==> ?!y. y IN s /\ ~(y = x) /\
  96                                   (f(x) * f(y) == 1) (mod r))
  97            ==> (product s f == 1) (mod r)`,
  98   REPEAT STRIP_TAC THEN MATCH_MP_TAC PRODUCT_PAIRUP_INDUCT THEN
  99   EXISTS_TAC `CARD(s:A->bool)` THEN ASM_REWRITE_TAC[]);;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* Hence Wilson's theorem.                                                   *)
 103 (* ------------------------------------------------------------------------- *)
 104
 105 let WILSON = prove
 106  (`!p. prime(p) ==> (FACT(p - 1) == p - 1) (mod p)`,
 107   GEN_TAC THEN DISCH_TAC THEN
 108   ASM_CASES_TAC `p = 0` THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 109   ASM_CASES_TAC `p = 1` THENL [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
 110   ASM_CASES_TAC `p = 2` THENL
 111    [ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN
 112     REWRITE_TAC[CONG_REFL];
 113     ALL_TAC] THEN
 114   SUBGOAL_THEN `FACT(p - 1) = FACT(p - 2) * (p - 1)` SUBST1_TAC THENL
 115    [SUBGOAL_THEN `p - 1 = SUC(p - 2)`
 116      (fun th -> REWRITE_TAC[th; FACT; MULT_AC]) THEN
 117     ASM_ARITH_TAC;
 118     ALL_TAC] THEN
 119   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `x = 1 * x`] THEN
 120   MATCH_MP_TAC CONG_MULT THEN REWRITE_TAC[CONG_REFL] THEN
 121   REWRITE_TAC[FACT_PRODUCT_ALT] THEN MATCH_MP_TAC PRODUCT_PAIRUP THEN
 122   REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
 123   X_GEN_TAC `x:num` THEN STRIP_TAC THEN
 124   MP_TAC(SPECL [`p:num`; `x:num`] CONG_UNIQUE_INVERSE_PRIME) THEN
 125   ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
 126    [ASM_ARITH_TAC; ALL_TAC] THEN
 127   REWRITE_TAC[EXISTS_UNIQUE_THM] THEN MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
 128    [MATCH_MP_TAC MONO_EXISTS;
 129     REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 130     DISCH_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 131     ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC] THEN
 132   X_GEN_TAC `y:num` THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 133    [ASM_CASES_TAC `y = 1` THEN
 134     ASM_REWRITE_TAC[ARITH_RULE `2 <= y <=> 0 < y /\ ~(y = 1)`] THEN
 135     UNDISCH_TAC `(x * y == 1) (mod p)` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
 136     ASM_SIMP_TAC[CONG; MOD_LT; ARITH_RULE `x <= p - 2 /\ ~(p = 0) ==> x < p`;
 137                  ARITH_RULE `~(p = 0) /\ ~(p = 1) ==> 1 < p`] THEN
 138     UNDISCH_TAC `2 <= x` THEN ARITH_TAC;
 139     MATCH_MP_TAC(ARITH_RULE `y < p /\ ~(y = p - 1) ==> y <= p - 2`) THEN
 140     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 141     UNDISCH_TAC `(x * y == 1) (mod p)` THEN ASM_REWRITE_TAC[] THEN
 142     DISCH_TAC THEN SUBGOAL_THEN `(x + 1 == 0) (mod p)` MP_TAC THENL
 143      [ALL_TAC;
 144       REWRITE_TAC[CONG_0] THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 145       MAP_EVERY UNDISCH_TAC [`2 <= x`; `x <= p - 2`] THEN ARITH_TAC] THEN
 146     MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC `x * p:num` THEN CONJ_TAC THENL
 147      [ALL_TAC; REWRITE_TAC[CONG_0] THEN MESON_TAC[divides; MULT_SYM]] THEN
 148     SUBGOAL_THEN `x * p = x + x * (p - 1)` SUBST1_TAC THENL
 149      [REWRITE_TAC[LEFT_SUB_DISTRIB; MULT_CLAUSES] THEN
 150       ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_MP_TAC(GSYM SUB_ADD) THEN
 151       GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `x = x * 1`] THEN
 152       ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN
 153       UNDISCH_TAC `~(p = 0)` THEN ARITH_TAC;
 154       ALL_TAC] THEN
 155     ONCE_REWRITE_TAC[CONG_SYM] THEN MATCH_MP_TAC CONG_ADD THEN
 156     ASM_REWRITE_TAC[CONG_REFL];
 157     FIRST_X_ASSUM SUBST_ALL_TAC THEN
 158     SUBGOAL_THEN `((x + 1) * (x - 1) == 0) (mod p)` MP_TAC THENL
 159      [ALL_TAC;
 160       REWRITE_TAC[CONG_0] THEN
 161       DISCH_THEN(MP_TAC o CONJ (ASSUME `prime p`)) THEN
 162       DISCH_THEN(MP_TAC o MATCH_MP PRIME_DIVPROD) THEN
 163       DISCH_THEN(DISJ_CASES_THEN (MP_TAC o MATCH_MP DIVIDES_LE)) THEN
 164       MAP_EVERY UNDISCH_TAC
 165         [`2 <= x`; `x <= p - 2`; `~(p = 1)`; `~(p = 0)`] THEN
 166       ARITH_TAC] THEN
 167     ONCE_REWRITE_TAC[GSYM(SPEC `1` CONG_ADD_LCANCEL_EQ)] THEN
 168     SUBGOAL_THEN `1 + (x + 1) * (x - 1) = x * x`
 169      (fun th -> ASM_REWRITE_TAC[th; ARITH]) THEN
 170     REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
 171     MATCH_MP_TAC(ARITH_RULE
 172      `(x + 1) * 1 <= (x + 1) * x
 173       ==> 1 + (x + 1) * x - (x + 1) * 1 = x * x`) THEN
 174     REWRITE_TAC[LE_MULT_LCANCEL] THEN UNDISCH_TAC `2 <= x` THEN ARITH_TAC]);;
 175
 176 (* ------------------------------------------------------------------------- *)
 177 (* And in fact we have a converse.                                           *)
 178 (* ------------------------------------------------------------------------- *)
 179
 180 let WILSON_EQ = prove
 181  (`!p. ~(p = 1) ==> (prime p <=> (FACT(p - 1) == p - 1) (mod p))`,
 182   X_GEN_TAC `n:num` THEN DISCH_TAC THEN EQ_TAC THEN SIMP_TAC[WILSON] THEN
 183   FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
 184   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
 185   FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 186   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THENL
 187    [ASM_REWRITE_TAC[CONG_MOD_0] THEN CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN
 188   REWRITE_TAC[LE_LT] THEN ASM_CASES_TAC `n:num = p` THEN ASM_REWRITE_TAC[] THEN
 189   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE `x < y ==> x <= y - 1`)) THEN
 190   ASM_SIMP_TAC[GSYM DIVIDES_FACT_PRIME] THEN
 191   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 192   SUBGOAL_THEN `p divides FACT(n - 1) <=> p divides (n - 1)` SUBST1_TAC THENL
 193    [MATCH_MP_TAC CONG_DIVIDES THEN
 194     MATCH_MP_TAC CONG_MOD_MULT THEN EXISTS_TAC `n:num` THEN
 195     ASM_REWRITE_TAC[];
 196     ALL_TAC] THEN
 197   DISCH_TAC THEN SUBGOAL_THEN `p divides 1` MP_TAC THENL
 198    [MATCH_MP_TAC DIVIDES_ADD_REVR THEN EXISTS_TAC `n - 1` THEN
 199     ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 + 1 = n`];
 200     REWRITE_TAC[DIVIDES_ONE] THEN ASM_MESON_TAC[PRIME_1]]);;