100/fta.ml

   1 (* ========================================================================= *)
   2 (* The fundamental theorem of arithmetic (unique prime factorization).       *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6
   7 prioritize_num();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Definition of iterated product.                                           *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let nproduct = new_definition `nproduct = iterate ( * )`;;
  14
  15 let NPRODUCT_CLAUSES = prove
  16  (`(!f. nproduct {} f = 1) /\
  17    (!x f s. FINITE(s)
  18             ==> (nproduct (x INSERT s) f =
  19                  if x IN s then nproduct s f else f(x) * nproduct s f))`,
  20   REWRITE_TAC[nproduct; GSYM NEUTRAL_MUL] THEN
  21   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  22   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MUL]);;
  23
  24 let NPRODUCT_EQ_1_EQ = prove
  25  (`!s f. FINITE s ==> (nproduct s f = 1 <=> !x. x IN s ==> f(x) = 1)`,
  26   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  27   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  28   ASM_SIMP_TAC[NPRODUCT_CLAUSES; IN_INSERT; MULT_EQ_1; NOT_IN_EMPTY] THEN
  29   ASM_MESON_TAC[]);;
  30
  31 let NPRODUCT_SPLITOFF = prove
  32  (`!x:A f s. FINITE s
  33              ==> nproduct s f =
  34                  (if x IN s then f(x) else 1) * nproduct (s DELETE x) f`,
  35   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
  36   ASM_SIMP_TAC[MULT_CLAUSES; SET_RULE `~(x IN s) ==> s DELETE x = s`] THEN
  37   SUBGOAL_THEN `s = (x:A) INSERT (s DELETE x)`
  38    (fun th -> GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [th] THEN
  39               ASM_SIMP_TAC[NPRODUCT_CLAUSES; FINITE_DELETE; IN_DELETE]) THEN
  40   REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[]);;
  41
  42 let NPRODUCT_SPLITOFF_HACK = prove
  43  (`!x:A f s. nproduct s f =
  44              if FINITE s then
  45                (if x IN s then f(x) else 1) * nproduct (s DELETE x) f
  46              else nproduct s f`,
  47   REPEAT STRIP_TAC THEN MESON_TAC[NPRODUCT_SPLITOFF]);;
  48
  49 let NPRODUCT_EQ = prove
  50  (`!f g s. FINITE s /\ (!x. x IN s ==> f x = g x)
  51            ==> nproduct s f = nproduct s g`,
  52   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
  53   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  54   SIMP_TAC[NPRODUCT_CLAUSES; IN_INSERT]);;
  55
  56 let NPRODUCT_EQ_GEN = prove
  57  (`!f g s t. FINITE s /\ s = t /\ (!x. x IN s ==> f x = g x)
  58              ==> nproduct s f = nproduct t g`,
  59   MESON_TAC[NPRODUCT_EQ]);;
  60
  61 let PRIME_DIVIDES_NPRODUCT = prove
  62  (`!p s f. prime p /\ FINITE s /\ p divides (nproduct s f)
  63            ==> ?x. x IN s /\ p divides (f x)`,
  64   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  65   DISCH_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  66   SIMP_TAC[NPRODUCT_CLAUSES; IN_INSERT; NOT_IN_EMPTY] THEN
  67   ASM_MESON_TAC[PRIME_DIVPROD; DIVIDES_ONE; PRIME_1]);;
  68
  69 let NPRODUCT_CANCEL_PRIME = prove
  70  (`!s p m f j.
  71         p EXP j * nproduct (s DELETE p) (\p. p EXP (f p)) = p * m
  72         ==> prime p /\ FINITE s /\ (!x. x IN s ==> prime x)
  73             ==> ~(j = 0) /\
  74                 p EXP (j - 1) * nproduct (s DELETE p) (\p. p EXP (f p)) = m`,
  75   REPEAT GEN_TAC THEN ASM_CASES_TAC `j = 0` THEN ASM_REWRITE_TAC[] THENL
  76    [ALL_TAC;
  77     FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
  78      `~(j = 0) ==> j = SUC(j - 1)`)) THEN
  79     REWRITE_TAC[SUC_SUB1; EXP; GSYM MULT_ASSOC; EQ_MULT_LCANCEL] THEN
  80     MESON_TAC[PRIME_0]] THEN
  81   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  82   REWRITE_TAC[EXP; MULT_CLAUSES] THEN REPEAT STRIP_TAC THEN
  83   MP_TAC(ISPECL [`p:num`; `s DELETE (p:num)`; `\p. p EXP (f p)`]
  84                  PRIME_DIVIDES_NPRODUCT) THEN
  85   ANTS_TAC THENL [ASM_MESON_TAC[divides; FINITE_DELETE]; ALL_TAC] THEN
  86   REWRITE_TAC[IN_DELETE] THEN ASM_MESON_TAC[PRIME_1; prime; PRIME_DIVEXP]);;
  87
  88 (* ------------------------------------------------------------------------- *)
  89 (* Fundamental Theorem of Arithmetic.                                        *)
  90 (* ------------------------------------------------------------------------- *)
  91
  92 let FTA = prove
  93  (`!n. ~(n = 0)
  94        ==> ?!i. FINITE {p | ~(i p = 0)} /\
  95                 (!p. ~(i p = 0) ==> prime p) /\
  96                 n = nproduct {p | ~(i p = 0)} (\p. p EXP (i p))`,
  97   ONCE_REWRITE_TAC[ARITH_RULE `n = nproduct s f <=> nproduct s f = n`] THEN
  98   REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
  99   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN REPEAT DISCH_TAC THEN
 100   ASM_CASES_TAC `n = 1` THENL
 101    [ASM_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
 102     SIMP_TAC[NPRODUCT_EQ_1_EQ; EXP_EQ_1; IN_ELIM_THM] THEN
 103     REWRITE_TAC[FUN_EQ_THM; NOT_IMP; GSYM CONJ_ASSOC] THEN CONJ_TAC THENL
 104      [EXISTS_TAC `\n:num. 0` THEN
 105       REWRITE_TAC[SET_RULE `{p | F} = {}`; FINITE_RULES];
 106       REPEAT GEN_TAC THEN STRIP_TAC THEN
 107       X_GEN_TAC `q:num` THEN ASM_CASES_TAC `q = 1` THEN
 108       ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[PRIME_1]];
 109     ALL_TAC] THEN
 110   FIRST_X_ASSUM(MP_TAC o MATCH_MP PRIME_FACTOR) THEN
 111   REWRITE_TAC[divides; RIGHT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 112   MAP_EVERY X_GEN_TAC [`p:num`; `m:num`] THEN
 113   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
 114   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN ANTS_TAC THENL
 115    [ASM_MESON_TAC[PRIME_FACTOR_LT]; ALL_TAC] THEN
 116   RULE_ASSUM_TAC(REWRITE_RULE[MULT_EQ_0; DE_MORGAN_THM]) THEN
 117   FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
 118   MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
 119    [DISCH_THEN(X_CHOOSE_THEN `i:num->num` STRIP_ASSUME_TAC) THEN
 120     EXISTS_TAC `\q:num. if q = p then i(q) + 1 else i(q)` THEN
 121     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
 122     CONJ_TAC THENL
 123      [MATCH_MP_TAC FINITE_SUBSET THEN
 124       EXISTS_TAC `p INSERT {p:num | ~(i p = 0)}` THEN
 125       ASM_SIMP_TAC[SUBSET; FINITE_INSERT; IN_INSERT; IN_ELIM_THM] THEN
 126       MESON_TAC[];
 127       ALL_TAC] THEN
 128     DISCH_TAC THEN CONJ_TAC THEN ASM_REWRITE_TAC[] THENL
 129      [ASM_MESON_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
 130     FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
 131     MP_TAC(ISPEC `p:num` NPRODUCT_SPLITOFF_HACK) THEN
 132     DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
 133     ASM_REWRITE_TAC[IN_ELIM_THM; ADD_EQ_0; ARITH] THEN
 134     REWRITE_TAC[MULT_ASSOC] THEN BINOP_TAC THENL
 135      [ASM_CASES_TAC `(i:num->num) p = 0` THEN
 136       ASM_REWRITE_TAC[EXP_ADD; EXP_1; EXP; MULT_AC];
 137       ALL_TAC] THEN
 138     MATCH_MP_TAC NPRODUCT_EQ_GEN THEN RULE_ASSUM_TAC(SIMP_RULE[]) THEN
 139     ASM_SIMP_TAC[FINITE_DELETE; IN_DELETE; EXTENSION; IN_ELIM_THM] THEN
 140     ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
 141     REWRITE_TAC[ADD_EQ_0; ARITH] THEN MESON_TAC[];
 142     ALL_TAC] THEN
 143   MP_TAC(ISPEC `p:num` NPRODUCT_SPLITOFF_HACK) THEN
 144   DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
 145   REWRITE_TAC[TAUT
 146    `p /\ q /\ ((if p then x else y) = z) <=> p /\ q /\ x = z`] THEN
 147   REWRITE_TAC[IN_ELIM_THM] THEN
 148   REWRITE_TAC[MESON[EXP] `(if ~(x = 0) then p EXP x else 1) = p EXP x`] THEN
 149   REWRITE_TAC[FUN_EQ_THM] THEN DISCH_TAC THEN
 150   MAP_EVERY X_GEN_TAC [`j:num->num`; `k:num->num`] THEN STRIP_TAC THEN
 151   FIRST_X_ASSUM(MP_TAC o SPECL
 152    [`\i:num. if i = p then j(i) - 1 else j(i)`;
 153     `\i:num. if i = p then k(i) - 1 else k(i)`]) THEN
 154   REWRITE_TAC[] THEN
 155   REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP NPRODUCT_CANCEL_PRIME)) THEN
 156   ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN STRIP_TAC THEN
 157   REWRITE_TAC[SET_RULE
 158    `!j k. {q | ~((if q = p then j q else k q) = 0)} DELETE p =
 159           {q | ~(k q = 0)} DELETE p`] THEN
 160   ANTS_TAC THENL
 161    [ALL_TAC;
 162     MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN COND_CASES_TAC THEN
 163     ASM_REWRITE_TAC[] THEN MAP_EVERY UNDISCH_TAC
 164      [`~(j(p:num) = 0)`; `~(k(p:num) = 0)`] THEN ARITH_TAC] THEN
 165   ONCE_REWRITE_TAC[COND_RAND] THEN ONCE_REWRITE_TAC[COND_RATOR] THEN
 166   REPEAT CONJ_TAC THENL
 167    [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{p:num | ~(j p = 0)}` THEN
 168     ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ARITH_TAC;
 169     ASM_MESON_TAC[SUB_0];
 170     FIRST_X_ASSUM(fun th -> SUBST1_TAC(SYM th) THEN AP_TERM_TAC) THEN
 171     MATCH_MP_TAC NPRODUCT_EQ_GEN THEN ASM_REWRITE_TAC[FINITE_DELETE] THEN
 172     SIMP_TAC[IN_DELETE; IN_ELIM_THM];
 173     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{p:num | ~(k p = 0)}` THEN
 174     ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ARITH_TAC;
 175     ASM_MESON_TAC[SUB_0];
 176     FIRST_X_ASSUM(fun th -> SUBST1_TAC(SYM th) THEN AP_TERM_TAC) THEN
 177     MATCH_MP_TAC NPRODUCT_EQ_GEN THEN ASM_REWRITE_TAC[FINITE_DELETE] THEN
 178     SIMP_TAC[IN_DELETE; IN_ELIM_THM]]);;