1 (* ========================================================================= *)
2 (* #85: divisibility by 3 rule *)
3 (* ========================================================================= *)
5 needs "Library/prime.ml";;
6 needs "Library/pocklington.ml";;
8 let EXP_10_CONG_3 = prove
9 (`!n. (10 EXP n == 1) (mod 3)`,
10 INDUCT_TAC THEN REWRITE_TAC[EXP; CONG_REFL] THEN
11 MATCH_MP_TAC CONG_TRANS THEN EXISTS_TAC `10 * 1` THEN CONJ_TAC THEN
12 ASM_SIMP_TAC[CONG_MULT; CONG_REFL] THEN
13 SIMP_TAC[CONG; ARITH] THEN CONV_TAC NUM_REDUCE_CONV);;
15 let SUM_CONG_3 = prove
16 (`!d n. (nsum(0..n) (\i. 10 EXP i * d(i)) == nsum(0..n) (\i. d i)) (mod 3)`,
17 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THENL
18 [REWRITE_TAC[EXP; MULT_CLAUSES; CONG_REFL]; ALL_TAC] THEN
19 REWRITE_TAC[LE_0] THEN MATCH_MP_TAC CONG_ADD THEN
20 ASM_REWRITE_TAC[] THEN
21 GEN_REWRITE_TAC (LAND_CONV) [ARITH_RULE `d = 1 * d`] THEN
22 MATCH_MP_TAC CONG_MULT THEN REWRITE_TAC[CONG_REFL; EXP_10_CONG_3]);;
24 let DIVISIBILITY_BY_3 = prove
25 (`3 divides (nsum(0..n) (\i. 10 EXP i * d(i))) <=>
26 3 divides (nsum(0..n) (\i. d i))`,
27 MATCH_MP_TAC CONG_DIVIDES THEN REWRITE_TAC[SUM_CONG_3]);;