100/div3.ml

   1 (* ========================================================================= *)
   2 (* #85: divisibility by 3 rule                                               *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/pocklington.ml";;
   7
   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);;
  14
  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]);;
  23
  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]);;