(* ========================================================================= *)
(* The fundamental theorem of arithmetic (unique prime factorization).       *)
(* ========================================================================= *)

needs "Library/prime.ml";;

prioritize_num();;

(* ------------------------------------------------------------------------- *)
(* Definition of iterated product.                                           *)
(* ------------------------------------------------------------------------- *)

let nproduct = new_definition `nproduct = iterate ( * )`;;
let NPRODUCT_CLAUSES = 
prove
 (`(!f. nproduct {} f = 1) /\
   (!x f s. FINITE(s)
            ==> (nproduct (x INSERT s) f =
                 if x IN s then nproduct s f else f(x) * nproduct s f))`,

  REWRITE_TAC[nproduct; GSYM NEUTRAL_MUL] THEN
  ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MUL]);;
let NPRODUCT_EQ_1_EQ = 
prove
 (`!s f. FINITE s ==> (nproduct s f = 1 <=> !x. x IN s ==> f(x) = 1)`,

  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  ASM_SIMP_TAC[NPRODUCT_CLAUSES; IN_INSERT; MULT_EQ_1; NOT_IN_EMPTY] THEN
  ASM_MESON_TAC[]);;
let NPRODUCT_SPLITOFF = 
prove
 (`!x:A f s. FINITE s
             ==> nproduct s f =
                 (if x IN s then f(x) else 1) * nproduct (s DELETE x) f`,

  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
  ASM_SIMP_TAC[MULT_CLAUSES; SET_RULE `~(x IN s) ==> s DELETE x = s`] THEN
  SUBGOAL_THEN `s = (x:A) INSERT (s DELETE x)`
   (fun th -> GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [th] THEN
              ASM_SIMP_TAC[NPRODUCT_CLAUSES; FINITE_DELETE; IN_DELETE]) THEN
  REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[]);;
let NPRODUCT_SPLITOFF_HACK = 
prove
 (`!x:A f s. nproduct s f =
             if FINITE s then
               (if x IN s then f(x) else 1) * nproduct (s DELETE x) f
             else nproduct s f`,

  REPEAT STRIP_TAC THEN MESON_TAC[NPRODUCT_SPLITOFF]);;
let NPRODUCT_EQ = 
prove
 (`!f g s. FINITE s /\ (!x. x IN s ==> f x = g x)
           ==> nproduct s f = nproduct s g`,

  GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  SIMP_TAC[NPRODUCT_CLAUSES; IN_INSERT]);;
let NPRODUCT_EQ_GEN = 
prove
 (`!f g s t. FINITE s /\ s = t /\ (!x. x IN s ==> f x = g x)
             ==> nproduct s f = nproduct t g`,

  MESON_TAC[NPRODUCT_EQ]);;
let PRIME_DIVIDES_NPRODUCT = 
prove
 (`!p s f. prime p /\ FINITE s /\ p divides (nproduct s f)
           ==> ?x. x IN s /\ p divides (f x)`,

  GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  DISCH_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  SIMP_TAC[NPRODUCT_CLAUSES; IN_INSERT; NOT_IN_EMPTY] THEN
  ASM_MESON_TAC[PRIME_DIVPROD; DIVIDES_ONE; PRIME_1]);;
let NPRODUCT_CANCEL_PRIME = 
prove
 (`!s p m f j.
        p EXP j * nproduct (s DELETE p) (\p. p EXP (f p)) = p * m
        ==> prime p /\ FINITE s /\ (!x. x IN s ==> prime x)
            ==> ~(j = 0) /\
                p EXP (j - 1) * nproduct (s DELETE p) (\p. p EXP (f p)) = m`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `j = 0` THEN ASM_REWRITE_TAC[] THENL
   [ALL_TAC;
    FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
     `~(j = 0) ==> j = SUC(j - 1)`)) THEN
    REWRITE_TAC[SUC_SUB1; EXP; GSYM MULT_ASSOC; EQ_MULT_LCANCEL] THEN
    MESON_TAC[PRIME_0]] THEN
  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  REWRITE_TAC[EXP; MULT_CLAUSES] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`p:num`; `s DELETE (p:num)`; `\p. p EXP (f p)`]
                 PRIME_DIVIDES_NPRODUCT) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[divides; FINITE_DELETE]; ALL_TAC] THEN
  REWRITE_TAC[IN_DELETE] THEN ASM_MESON_TAC[PRIME_1; prime; PRIME_DIVEXP]);;
(* ------------------------------------------------------------------------- *)
(* Fundamental Theorem of Arithmetic.                                        *)
(* ------------------------------------------------------------------------- *)

let FTA = 
prove
 (`!n. ~(n = 0)
       ==> ?!i. FINITE {p | ~(i p = 0)} /\
                (!p. ~(i p = 0) ==> prime p) /\
                n = nproduct {p | ~(i p = 0)} (\p. p EXP (i p))`,

  ONCE_REWRITE_TAC[ARITH_RULE `n = nproduct s f <=> nproduct s f = n`] THEN
  REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
  MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN REPEAT DISCH_TAC THEN
  ASM_CASES_TAC `n = 1` THENL
   [ASM_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
    SIMP_TAC[NPRODUCT_EQ_1_EQ; EXP_EQ_1; IN_ELIM_THM] THEN
    REWRITE_TAC[FUN_EQ_THM; NOT_IMP; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
     [EXISTS_TAC `\n:num. 0` THEN
      REWRITE_TAC[SET_RULE `{p | F} = {}`; FINITE_RULES];
      REPEAT GEN_TAC THEN STRIP_TAC THEN
      X_GEN_TAC `q:num` THEN ASM_CASES_TAC `q = 1` THEN
      ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[PRIME_1]];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
  REWRITE_TAC[divides; RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`p:num`; `m:num`] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN ANTS_TAC THENL
   [ASM_MESON_TAC[PRIME_FACTOR_LT]; ALL_TAC] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
  FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
   [DISCH_THEN(X_CHOOSE_THEN `i:num->num` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `\q:num. if q = p then i(q) + 1 else i(q)` THEN
    ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC FINITE_SUBSET THEN
      EXISTS_TAC `p INSERT {p:num | ~(i p = 0)}` THEN
      ASM_SIMP_TAC[SUBSET; FINITE_INSERT; IN_INSERT; IN_ELIM_THM] THEN
      MESON_TAC[];
      ALL_TAC] THEN
    DISCH_TAC THEN CONJ_TAC THEN ASM_REWRITE_TAC[] THENL
     [ASM_MESON_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
    FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
    MP_TAC(ISPEC `p:num` NPRODUCT_SPLITOFF_HACK) THEN
    DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
    ASM_REWRITE_TAC[IN_ELIM_THM; ADD_EQ_0; ARITH] THEN
    REWRITE_TAC[MULT_ASSOC] THEN BINOP_TAC THENL
     [ASM_CASES_TAC `(i:num->num) p = 0` THEN
      ASM_REWRITE_TAC[EXP_ADD; EXP_1; EXP; MULT_AC];
      ALL_TAC] THEN
    MATCH_MP_TAC NPRODUCT_EQ_GEN THEN RULE_ASSUM_TAC(SIMP_RULE[]) THEN
    ASM_SIMP_TAC[FINITE_DELETE; IN_DELETE; EXTENSION; IN_ELIM_THM] THEN
    ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
    REWRITE_TAC[ADD_EQ_0; ARITH] THEN MESON_TAC[];
    ALL_TAC] THEN
  MP_TAC(ISPEC `p:num` NPRODUCT_SPLITOFF_HACK) THEN
  DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
  REWRITE_TAC[TAUT
   `p /\ q /\ ((if p then x else y) = z) <=> p /\ q /\ x = z`] THEN
  REWRITE_TAC[IN_ELIM_THM] THEN
  REWRITE_TAC[MESON[EXP] `(if ~(x = 0) then p EXP x else 1) = p EXP x`] THEN
  REWRITE_TAC[FUN_EQ_THM] THEN DISCH_TAC THEN
  MAP_EVERY X_GEN_TAC [`j:num->num`; `k:num->num`] THEN STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPECL
   [`\i:num. if i = p then j(i) - 1 else j(i)`;
    `\i:num. if i = p then k(i) - 1 else k(i)`]) THEN
  REWRITE_TAC[] THEN
  REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP NPRODUCT_CANCEL_PRIME)) THEN
  ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN STRIP_TAC THEN
  REWRITE_TAC[SET_RULE
   `!j k. {q | ~((if q = p then j q else k q) = 0)} DELETE p =
          {q | ~(k q = 0)} DELETE p`] THEN
  ANTS_TAC THENL
   [ALL_TAC;
    MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN COND_CASES_TAC THEN
    ASM_REWRITE_TAC[] THEN MAP_EVERY UNDISCH_TAC
     [`~(j(p:num) = 0)`; `~(k(p:num) = 0)`] THEN ARITH_TAC] THEN
  ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
  REPEAT CONJ_TAC THENL
   [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{p:num | ~(j p = 0)}` THEN
    ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ARITH_TAC;
    ASM_MESON_TAC[SUB_0];
    FIRST_X_ASSUM(fun th -> SUBST1_TAC(SYM th) THEN AP_TERM_TAC) THEN
    MATCH_MP_TAC NPRODUCT_EQ_GEN THEN ASM_REWRITE_TAC[FINITE_DELETE] THEN
    SIMP_TAC[IN_DELETE; IN_ELIM_THM];
    MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{p:num | ~(k p = 0)}` THEN
    ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ARITH_TAC;
    ASM_MESON_TAC[SUB_0];
    FIRST_X_ASSUM(fun th -> SUBST1_TAC(SYM th) THEN AP_TERM_TAC) THEN
    MATCH_MP_TAC NPRODUCT_EQ_GEN THEN ASM_REWRITE_TAC[FINITE_DELETE] THEN
    SIMP_TAC[IN_DELETE; IN_ELIM_THM]]);;