1 needs "Library/prime.ml";;
2 needs "Library/pocklington.ml";;
3 needs "Library/binomial.ml";;
7 let FERMAT_PRIME_CONV n =
8 let tm = subst [mk_small_numeral n,`x:num`] `prime(2 EXP (2 EXP x) + 1)` in
9 (RAND_CONV NUM_REDUCE_CONV THENC PRIME_CONV) tm;;
21 let CONG_TRIVIAL = prove
22 (`!x y. n divides x /\ n divides y ==> (x == y) (mod n)`,
23 MESON_TAC[CONG_0; CONG_SYM; CONG_TRANS]);;
25 let LITTLE_CHECK_CONV tm =
26 EQT_ELIM((RATOR_CONV(LAND_CONV NUM_EXP_CONV) THENC CONG_CONV) tm);;
28 LITTLE_CHECK_CONV `(9 EXP 8 == 9) (mod 3)`;;
29 LITTLE_CHECK_CONV `(9 EXP 3 == 9) (mod 3)`;;
30 LITTLE_CHECK_CONV `(10 EXP 7 == 10) (mod 7)`;;
31 LITTLE_CHECK_CONV `(2 EXP 7 == 2) (mod 7)`;;
32 LITTLE_CHECK_CONV `(777 EXP 13 == 777) (mod 13)`;;
34 let DIVIDES_FACT_PRIME = prove
35 (`!p. prime p ==> !n. p divides (FACT n) <=> p <= n`,
36 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT; LE] THENL
37 [ASM_MESON_TAC[DIVIDES_ONE; PRIME_0; PRIME_1];
38 ASM_MESON_TAC[PRIME_DIVPROD_EQ; DIVIDES_LE; NOT_SUC; DIVIDES_REFL;
39 ARITH_RULE `~(p <= n) /\ p <= SUC n ==> p = SUC n`]]);;
41 let DIVIDES_BINOM_PRIME = prove
42 (`!n p. prime p /\ 0 < n /\ n < p ==> p divides binom(p,n)`,
44 MP_TAC(AP_TERM `(divides) p` (SPECL [`p - n`; `n:num`] BINOM_FACT)) THEN
45 ASM_SIMP_TAC[DIVIDES_FACT_PRIME; PRIME_DIVPROD_EQ; SUB_ADD; LT_IMP_LE] THEN
46 ASM_REWRITE_TAC[GSYM NOT_LT; LT_REFL] THEN
47 ASM_SIMP_TAC[ARITH_RULE `0 < n /\ n < p ==> p - n < p`]);;
49 let DIVIDES_NSUM = prove
50 (`!m n. (!i. m <= i /\ i <= n ==> p divides f(i)) ==> p divides nsum(m..n) f`,
51 GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
52 ASM_MESON_TAC[LE; LE_TRANS; DIVIDES_0; DIVIDES_ADD; LE_REFL]);;
55 (`!p a b. prime p ==> ((a + b) EXP p == a EXP p + b EXP p) (mod p)`,
56 REPEAT STRIP_TAC THEN REWRITE_TAC[BINOMIAL_THEOREM] THEN
57 SUBGOAL_THEN `1 <= p /\ 0 < p` STRIP_ASSUME_TAC THENL
58 [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_IMP_NZ) THEN ARITH_TAC; ALL_TAC] THEN
59 ASM_SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0; ARITH; NSUM_CLAUSES_RIGHT] THEN
60 REWRITE_TAC[SUB_0; SUB_REFL; EXP; binom; BINOM_REFL; MULT_CLAUSES] THEN
61 GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a + b = (b + 0) + a`] THEN
62 REPEAT(MATCH_MP_TAC CONG_ADD THEN REWRITE_TAC[CONG_REFL]) THEN
63 REWRITE_TAC[CONG_0] THEN MATCH_MP_TAC DIVIDES_NSUM THEN
64 ASM_MESON_TAC[DIVIDES_RMUL; DIVIDES_BINOM_PRIME; ARITH_RULE
65 `0 < p /\ 1 <= i /\ i <= p - 1 ==> 0 < i /\ i < p`]);;
67 let FERMAT_LITTLE = prove
68 (`!p a. prime p ==> (a EXP p == a) (mod p)`,
69 GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
71 [ASM_MESON_TAC[EXP_EQ_0; CONG_REFL; PRIME_0];
72 ASM_MESON_TAC[ADD1; FLT_LEMMA; EXP_ONE; CONG_ADD; CONG_TRANS; CONG_REFL]]);;
74 let FERMAT_LITTLE_COPRIME = prove
75 (`!p a. prime p /\ coprime(a,p) ==> (a EXP (p - 1) == 1) (mod p)`,
76 REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_MULT_LCANCEL THEN
77 EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
78 ASM_SIMP_TAC[PRIME_IMP_NZ; ARITH_RULE `~(p = 0) ==> SUC(p - 1) = p`] THEN
79 ASM_SIMP_TAC[FERMAT_LITTLE; MULT_CLAUSES]);;
81 let FERMAT_LITTLE_VARIANT = prove
82 (`!p a. prime p ==> (a EXP (1 + m * (p - 1)) == a) (mod p)`,
84 FIRST_ASSUM(DISJ_CASES_TAC o SPEC `a:num` o MATCH_MP PRIME_COPRIME_STRONG)
85 THENL [ASM_MESON_TAC[CONG_TRIVIAL; ADD_AC; ADD1; DIVIDES_REXP_SUC];
87 GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
88 REWRITE_TAC[EXP_ADD; EXP_1] THEN MATCH_MP_TAC CONG_MULT THEN
89 REWRITE_TAC[GSYM EXP_EXP; CONG_REFL] THEN
90 ASM_MESON_TAC[COPRIME_SYM; COPRIME_EXP; PHI_PRIME; FERMAT_LITTLE_COPRIME]);;
93 (`prime p /\ prime q /\ ~(p = q) /\
94 (d * e == 1) (mod ((p - 1) * (q - 1))) /\
95 plaintext < p * q /\ (ciphertext = (plaintext EXP e) MOD (p * q))
96 ==> (plaintext = (ciphertext EXP d) MOD (p * q))`,
97 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
98 ASM_SIMP_TAC[MOD_EXP_MOD; MULT_EQ_0; PRIME_IMP_NZ; EXP_EXP] THEN
99 SUBGOAL_THEN `(plaintext == plaintext EXP (e * d)) (mod (p * q))` MP_TAC THENL
100 [ALL_TAC; ASM_SIMP_TAC[CONG; MULT_EQ_0; PRIME_IMP_NZ; MOD_LT]] THEN
101 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
102 FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [CONG_TO_1]) THENL
103 [ASM_MESON_TAC[MULT_EQ_1; ARITH_RULE `p - 1 = 1 <=> p = 2`]; ALL_TAC] THEN
104 MATCH_MP_TAC CONG_CHINESE THEN ASM_SIMP_TAC[DISTINCT_PRIME_COPRIME] THEN
105 ASM_MESON_TAC[FERMAT_LITTLE_VARIANT; MULT_AC; CONG_SYM]);;