1 (* ========================================================================= *)
2 (* The fundamental theorem of arithmetic (unique prime factorization). *)
3 (* ========================================================================= *)
5 needs "Library/prime.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* Definition of iterated product. *)
11 (* ------------------------------------------------------------------------- *)
13 let nproduct = new_definition `nproduct = iterate ( * )`;;
15 let NPRODUCT_CLAUSES = prove
16 (`(!f. nproduct {} f = 1) /\
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]);;
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
31 let NPRODUCT_SPLITOFF = prove
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[]);;
42 let NPRODUCT_SPLITOFF_HACK = prove
43 (`!x:A f s. nproduct s f =
45 (if x IN s then f(x) else 1) * nproduct (s DELETE x) f
47 REPEAT STRIP_TAC THEN MESON_TAC[NPRODUCT_SPLITOFF]);;
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]);;
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]);;
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]);;
69 let NPRODUCT_CANCEL_PRIME = prove
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)
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
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]);;
88 (* ------------------------------------------------------------------------- *)
89 (* Fundamental Theorem of Arithmetic. *)
90 (* ------------------------------------------------------------------------- *)
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]];
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
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
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];
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[];
143 MP_TAC(ISPEC `p:num` NPRODUCT_SPLITOFF_HACK) THEN
144 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
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
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
158 `!j k. {q | ~((if q = p then j q else k q) = 0)} DELETE p =
159 {q | ~(k q = 0)} DELETE p`] THEN
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]]);;