primeFactorScript.sml
1(*---------------------------------------------------------------------------*)
2(* Fundamental theorem of arithmetic for num. *)
3(*---------------------------------------------------------------------------*)
4Theory primeFactor
5Ancestors
6 bag divides arithmetic
7Libs
8 simpLib BasicProvers metisLib
9
10
11val std_ss =
12 (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
13 numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ combinSimps.COMBIN_ss ++
14 numSimps.ARITH_RWTS_ss);
15
16val arith_ss = std_ss ++ numSimps.ARITH_DP_ss
17val DECIDE = numLib.ARITH_PROVE;
18
19fun DECIDE_TAC (g as (asl,_)) =
20((MAP_EVERY UNDISCH_TAC (filter numSimps.is_arith_asm asl)
21 THEN numLib.ARITH_TAC)
22 ORELSE
23 tautLib.TAUT_TAC ORELSE NO_TAC) g;
24
25Theorem MULT_LEFT_CANCEL[local]:
26 !m n p. 0 < m ==> ((m*n = m*p) = (n=p))
27Proof
28 Cases_on `m` THEN RW_TAC arith_ss []
29QED
30
31Theorem PRIME_FACTORS_EXIST:
32 !n. 0 < n ==>
33 ?b. FINITE_BAG b /\
34 (!m. BAG_IN m b ==> prime m) /\
35 (n = BAG_GEN_PROD b 1)
36Proof
37 numLib.completeInduct_on `n` THEN STRIP_TAC THEN Cases_on `prime n` THENL
38 [Q.EXISTS_TAC `{|n|}` THEN
39 SRW_TAC [] [BAG_GEN_PROD_TAILREC,BAG_GEN_PROD_EMPTY],
40 Cases_on `n=1` THENL
41 [RW_TAC arith_ss [] THEN Q.EXISTS_TAC `{||}` THEN
42 METIS_TAC [FINITE_BAG_THM,BAG_GEN_PROD_EMPTY,NOT_IN_EMPTY_BAG],
43 `?m. prime m /\ divides m n` by RW_TAC arith_ss [PRIME_FACTOR] THEN
44 `?q. m * q = n` by METIS_TAC [divides_def,MULT_SYM] THEN
45 `q < n` by
46 (STRIP_ASSUME_TAC (DECIDE ``q < n \/ (q=n) \/ n < q``) THENL
47 [FULL_SIMP_TAC arith_ss [MULT_EQ_ID] THEN METIS_TAC [NOT_PRIME_1],
48 `0 < m /\ 0 < q`
49 by METIS_TAC [ZERO_LESS_MULT,DECIDE ``0 < 1``,LESS_TRANS] THEN
50 RW_TAC arith_ss [] THEN
51 `(m=1) \/ 1 < m` by DECIDE_TAC THEN METIS_TAC [NOT_PRIME_1]]) THEN
52 `1 < q` by
53 (STRIP_ASSUME_TAC (DECIDE ``(q = 0) \/ (q=1) \/ 1 < q``) THEN
54 RW_TAC arith_ss [] THEN METIS_TAC [MULT_RIGHT_1]) THEN
55 (* use IH *)
56 `0 < q` by DECIDE_TAC THEN
57 `?b. FINITE_BAG b /\ (!k. BAG_IN k b ==> prime k) /\
58 (q = BAG_GEN_PROD b 1)` by METIS_TAC [] THEN
59 Q.EXISTS_TAC `BAG_INSERT m b` THEN SRW_TAC [][] THENL
60 [METIS_TAC [], METIS_TAC [], METIS_TAC [BAG_GEN_PROD_REC]]]]
61QED
62
63
64(*---------------------------------------------------------------------------*)
65(* PRIME_FACTORS_def = *)
66(* |- !n. 0 < n ==> *)
67(* FINITE_BAG (PRIME_FACTORS n) /\ *)
68(* (!m. BAG_IN m (PRIME_FACTORS n) ==> prime m) /\ *)
69(* (n = BAG_GEN_PROD (PRIME_FACTORS n) 1) *)
70(*---------------------------------------------------------------------------*)
71
72val PRIME_FACTORS_def = new_specification
73("PRIME_FACTORS_def",
74 ["PRIME_FACTORS"],
75 SIMP_RULE bool_ss [SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] PRIME_FACTORS_EXIST);
76
77Theorem lem1[local]:
78 !b. FINITE_BAG b
79 ==> !m. prime m /\
80 divides m (BAG_GEN_PROD b 1) /\
81 (!x. BAG_IN x b ==> prime x)
82 ==> BAG_IN m b
83Proof
84 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL
85 [FULL_SIMP_TAC arith_ss [BAG_GEN_PROD_EMPTY] THEN
86 METIS_TAC [DIVIDES_ONE,NOT_PRIME_1],
87 Q.PAT_X_ASSUM `divides p q` MP_TAC THEN RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN
88 METIS_TAC [gcdTheory.P_EUCLIDES,prime_divides_only_self,BAG_IN_BAG_INSERT]]
89QED
90
91(*---------------------------------------------------------------------------*)
92(* Uniqueness. *)
93(* Sketch of the proof. When bag b1 is non-empty it has a prime p in it. We *)
94(* can show p divides BAG_PROD b2, so p is also in b2 (because p is prime). *)
95(* Let b1' = b1-p and b2' = b2-p. Then b1' = b2', by induction hypothesis. *)
96(* Thus b1=b2. The argument uses a lemma derived from gcdTheory.P_EUCLIDES, *)
97(* which says that p divides (a*b) ==> p divides a or p divides b. *)
98(*---------------------------------------------------------------------------*)
99
100Theorem UNIQUE_PRIME_FACTORS:
101 !n b1 b2.
102 (FINITE_BAG b1 /\ (!m. BAG_IN m b1 ==> prime m) /\ (n=BAG_GEN_PROD b1 1)) /\
103 (FINITE_BAG b2 /\ (!m. BAG_IN m b2 ==> prime m) /\ (n=BAG_GEN_PROD b2 1))
104 ==> (b1 = b2)
105Proof
106numLib.completeInduct_on `n` THEN
107 REPEAT STRIP_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN
108 `(b1 = {||}) \/ ?b1' e. b1 = BAG_INSERT e b1'` by METIS_TAC [BAG_cases] THENL
109 [RW_TAC arith_ss [] THEN
110 STRIP_ASSUME_TAC (ISPEC ``b2:num bag`` BAG_cases) THEN
111 FULL_SIMP_TAC arith_ss [] THEN RW_TAC std_ss [] THEN
112 Q.PAT_X_ASSUM `BAG_GEN_PROD a b = BAG_GEN_PROD c d` MP_TAC THEN
113 `FINITE_BAG b0` by METIS_TAC [FINITE_BAG_THM] THEN
114 ASM_SIMP_TAC arith_ss [BAG_GEN_PROD_EMPTY,BAG_GEN_PROD_TAILREC] THEN
115 STRIP_TAC THEN `e = 1` by METIS_TAC [BAG_GEN_PROD_EQ_1] THEN
116 METIS_TAC [BAG_GEN_PROD_ALL_ONES, NOT_PRIME_1, BAG_IN_BAG_INSERT],
117 `prime e` by METIS_TAC [BAG_IN_BAG_INSERT] THEN RW_TAC std_ss [] THEN
118 `FINITE_BAG b1'` by METIS_TAC [FINITE_BAG_THM] THEN
119 Q.PAT_X_ASSUM `p = q` MP_TAC THEN RW_TAC std_ss [BAG_GEN_PROD_REC] THEN
120 `divides e (BAG_GEN_PROD b2 1)` by METIS_TAC [divides_def,MULT_SYM] THEN
121 `BAG_IN e b2` by METIS_TAC [lem1] THEN
122 `?b2'. b2 = BAG_INSERT e b2'` by METIS_TAC [BAG_DECOMPOSE] THEN
123 RW_TAC std_ss [] THEN
124 `FINITE_BAG b2'` by METIS_TAC [FINITE_BAG_THM] THEN
125 Q.PAT_X_ASSUM `p = q` MP_TAC THEN RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN
126 `0 < e` by METIS_TAC [NOT_ZERO_LT_ZERO,NOT_PRIME_0] THEN
127 FULL_SIMP_TAC arith_ss [MULT_LEFT_CANCEL] THEN POP_ASSUM (K ALL_TAC) THEN
128 `BAG_GEN_PROD b2' 1 < BAG_GEN_PROD (BAG_INSERT e b2') 1`
129 by (RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN
130 METIS_TAC [BAG_GEN_PROD_POSITIVE,BAG_IN_BAG_INSERT,NOT_ZERO_LT_ZERO,
131 NOT_PRIME_0,DECIDE``!n.(n=0) \/ (n=1) \/ 1<n``,NOT_PRIME_1]) THEN
132 `b2' = b1'` by METIS_TAC[FINITE_BAG_THM,BAG_IN_BAG_INSERT] THEN
133METIS_TAC [BAG_INSERT_ONE_ONE]]
134QED
135
136
137Theorem PRIME_FACTORIZATION:
138 !n. 0 < n ==>
139 !b. FINITE_BAG b /\ (!x. BAG_IN x b ==> prime x) /\
140 (BAG_GEN_PROD b 1 = n) ==>
141 (b = PRIME_FACTORS n)
142Proof
143 METIS_TAC [PRIME_FACTORS_def,UNIQUE_PRIME_FACTORS]
144QED
145
146
147Theorem PRIME_FACTORS_1:
148 PRIME_FACTORS 1 = {||}
149Proof
150 METIS_TAC [FINITE_BAG_THM,BAG_GEN_PROD_EMPTY,
151 NOT_IN_EMPTY_BAG,PRIME_FACTORIZATION,DECIDE``0 < 1``]
152QED
153
154Theorem PRIME_FACTOR_DIVIDES:
155 !x n. 0 < n /\ BAG_IN x (PRIME_FACTORS n) ==> divides x n
156Proof
157 METIS_TAC [BAG_IN_DIVIDES,PRIME_FACTORS_def]
158QED
159
160Theorem DIVISOR_IN_PRIME_FACTORS:
161 !p n. 0 < n /\ prime p /\ divides p n ==> BAG_IN p (PRIME_FACTORS n)
162Proof
163 REPEAT STRIP_TAC THEN
164 `FINITE_BAG (PRIME_FACTORS n) /\
165 (!m. BAG_IN m (PRIME_FACTORS n) ==> prime m) /\
166 (n = BAG_GEN_PROD (PRIME_FACTORS n) 1)` by METIS_TAC [PRIME_FACTORS_def] THEN
167 FULL_SIMP_TAC arith_ss [divides_def] THEN
168 FULL_SIMP_TAC arith_ss [ZERO_LESS_MULT] THEN RW_TAC arith_ss [] THEN
169 `FINITE_BAG (PRIME_FACTORS q) /\
170 (!m. BAG_IN m (PRIME_FACTORS q) ==> prime m) /\
171 (q = BAG_GEN_PROD (PRIME_FACTORS q) 1)` by METIS_TAC [PRIME_FACTORS_def] THEN
172 `FINITE_BAG (BAG_INSERT p (PRIME_FACTORS q))` by METIS_TAC [FINITE_BAG_INSERT] THEN
173 Q.ABBREV_TAC `b = BAG_INSERT p (PRIME_FACTORS q)` THEN
174 `!m. BAG_IN m b ==> prime m` by METIS_TAC [BAG_IN_BAG_INSERT] THEN
175 `BAG_GEN_PROD b 1 = p * q`
176 by (Q.UNABBREV_TAC `b` THEN
177 RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN METIS_TAC[]) THEN
178 `b = PRIME_FACTORS (p * q)` by METIS_TAC [PRIME_FACTORIZATION,ZERO_LESS_MULT] THEN
179 METIS_TAC [BAG_IN_BAG_INSERT]
180QED
181
182Theorem PRIME_FACTORS_MULT:
183 !a b. 0 < a /\ 0 < b ==>
184 (PRIME_FACTORS (a*b) = BAG_UNION (PRIME_FACTORS a) (PRIME_FACTORS b))
185Proof
186 RW_TAC arith_ss [] THEN
187 `FINITE_BAG (PRIME_FACTORS a) /\
188 (!m. BAG_IN m (PRIME_FACTORS a) ==> prime m) /\
189 (a = BAG_GEN_PROD (PRIME_FACTORS a) 1) /\
190 FINITE_BAG (PRIME_FACTORS b) /\
191 (!m. BAG_IN m (PRIME_FACTORS b) ==> prime m) /\
192 (b = BAG_GEN_PROD (PRIME_FACTORS b) 1)`
193 by METIS_TAC [PRIME_FACTORS_def] THEN
194 `FINITE_BAG (BAG_UNION (PRIME_FACTORS a) (PRIME_FACTORS b))`
195 by METIS_TAC [FINITE_BAG_UNION] THEN
196 `BAG_GEN_PROD (PRIME_FACTORS a) 1 *
197 BAG_GEN_PROD (PRIME_FACTORS b) 1 =
198 BAG_GEN_PROD (BAG_UNION (PRIME_FACTORS a) (PRIME_FACTORS b)) 1`
199 by METIS_TAC [BAG_GEN_PROD_UNION] THEN
200 `a * b = BAG_GEN_PROD (BAG_UNION (PRIME_FACTORS a) (PRIME_FACTORS b)) 1`
201 by METIS_TAC[] THEN
202 `!x. BAG_IN x (BAG_UNION (PRIME_FACTORS a) (PRIME_FACTORS b))
203 ==> prime x` by METIS_TAC [BAG_IN_BAG_UNION] THEN
204 METIS_TAC [PRIME_FACTORIZATION,LESS_MULT2]
205QED
206
207Theorem FACTORS_prime:
208 !p. prime p ==> (PRIME_FACTORS p = {|p|})
209Proof
210 REPEAT STRIP_TAC THEN
211 `0 < p` by METIS_TAC [ONE_LT_PRIME,DECIDE ``0<1``,LESS_TRANS] THEN
212 `FINITE_BAG {|p|}` by METIS_TAC [FINITE_EMPTY_BAG,FINITE_BAG_INSERT] THEN
213 `!x. BAG_IN x {|p|} ==> prime x`
214 by METIS_TAC [BAG_IN_BAG_INSERT,NOT_IN_EMPTY_BAG] THEN
215 `BAG_GEN_PROD {|p|} 1 = p`
216 by METIS_TAC [BAG_GEN_PROD_REC,BAG_GEN_PROD_EMPTY,
217 DECIDE``x*1 = x``,FINITE_EMPTY_BAG] THEN
218 METIS_TAC [PRIME_FACTORIZATION]
219QED
220
221Theorem PRIME_FACTORS_EXP:
222 !p e. prime p ==> (PRIME_FACTORS (p ** e) p = e)
223Proof
224 Induct_on `e` THEN RW_TAC arith_ss [EXP,PRIME_FACTORS_1,EMPTY_BAG_alt] THEN
225 `0 < p` by METIS_TAC [ONE_LT_PRIME,DECIDE ``0<1``,LESS_TRANS] THEN
226 `0 < p ** e` by METIS_TAC [ZERO_LT_EXP] THEN
227 RW_TAC arith_ss [PRIME_FACTORS_MULT] THEN
228 `PRIME_FACTORS p = {|p|}` by METIS_TAC [FACTORS_prime] THEN
229 POP_ASSUM SUBST_ALL_TAC THEN
230 RW_TAC arith_ss [BAG_UNION_INSERT,BAG_UNION_EMPTY] THEN
231 RW_TAC arith_ss [BAG_INSERT]
232QED
233
234Theorem LESS_EQ_BAG_CARD_PRIME_FACTORS_PROD:
235 !b n.
236 FINITE_BAG b /\ BAG_GEN_PROD b 1 = n /\ (!x. BAG_IN x b ==> 2 <= x) ==>
237 BAG_CARD b <= BAG_CARD (PRIME_FACTORS n)
238Proof
239 rpt gen_tac \\ simp[GSYM AND_IMP_INTRO]
240 \\ strip_tac
241 \\ qid_spec_tac`n`
242 \\ pop_assum mp_tac
243 \\ qid_spec_tac`b`
244 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
245 \\ rw[]
246 \\ simp[BAG_CARD_THM, BAG_GEN_PROD_REC]
247 \\ fsrw_tac[DNF_ss][]
248 \\ `0 < e` by simp[]
249 \\ Cases_on`BAG_GEN_PROD b 1 = 0`
250 >- (
251 gs[BAG_GEN_PROD_EQ_0]
252 \\ res_tac \\ fs[])
253 \\ simp[PRIME_FACTORS_MULT]
254 \\ simp[BAG_CARD_UNION, PRIME_FACTORS_def]
255 \\ `0 < BAG_CARD (PRIME_FACTORS e)` suffices_by simp[]
256 \\ `PRIME_FACTORS e <> {||}` suffices_by
257 metis_tac[BCARD_0, PRIME_FACTORS_def, NOT_LT_ZERO_EQ_ZERO]
258 \\ qspec_then`e`mp_tac PRIME_FACTORS_def
259 \\ simp[] \\ rpt strip_tac
260 \\ gs[]
261 \\ gs[BAG_GEN_PROD_def]
262QED
263