1 (* ========================================================================= *)
2 (* Euler's partition theorem and other elementary partition theorems. *)
3 (* ========================================================================= *)
5 loadt "Library/binary.ml";;
7 (* ------------------------------------------------------------------------- *)
9 (* ------------------------------------------------------------------------- *)
11 let NSUM_BOUND_LEMMA = prove
12 (`!f a b n. nsum(a..b) f = n ==> !i. a <= i /\ i <= b ==> f(i) <= n`,
13 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[GSYM IN_NUMSEG] THEN
14 MATCH_MP_TAC NSUM_POS_BOUND THEN ASM_REWRITE_TAC[LE_REFL; FINITE_NUMSEG]);;
16 let CARD_EQ_LEMMA = prove
18 FINITE s /\ FINITE t /\
19 (!x. x IN s ==> f(x) IN t) /\
20 (!y. y IN t ==> g(y) IN s) /\
21 (!x. x IN s ==> g(f x) = x) /\
22 (!y. y IN t ==> f(g y) = y)
23 ==> FINITE s /\ FINITE t /\ CARD s = CARD t`,
24 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
25 MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN
26 EXISTS_TAC `g:B->A` THEN ASM_MESON_TAC[]);;
28 (* ------------------------------------------------------------------------- *)
29 (* Breaking a number up into 2^something * odd_number. *)
30 (* ------------------------------------------------------------------------- *)
33 `index n = if n = 0 then 0 else if ODD n then 0 else SUC(index(n DIV 2))`;;
36 `oddpart n = if n = 0 then 0 else if ODD n then n else oddpart(n DIV 2)`;;
38 let INDEX_ODDPART_WORK = prove
39 (`!n. n = 2 EXP (index n) * oddpart n /\ (ODD(oddpart n) <=> ~(n = 0))`,
40 MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
41 ONCE_REWRITE_TAC[index; oddpart] THEN
42 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN
43 COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH; MULT_CLAUSES] THEN
44 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_ODD]) THEN
45 SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM; EXP; GSYM MULT_ASSOC;
46 ARITH; ARITH_RULE `(2 * x) DIV 2 = x`; EQ_MULT_LCANCEL] THEN
47 ASM_MESON_TAC[ARITH_RULE `~(n = 0) /\ n = 2 * m ==> m < n /\ ~(m = 0)`]);;
49 let INDEX_ODDPART_DECOMPOSITION = prove
50 (`!n. n = 2 EXP (index n) * oddpart n`,
51 MESON_TAC[INDEX_ODDPART_WORK]);;
53 let ODD_ODDPART = prove
54 (`!n. ODD(oddpart n) <=> ~(n = 0)`,
55 MESON_TAC[INDEX_ODDPART_WORK]);;
57 let ODDPART_LE = prove
58 (`!n. oddpart n <= n`,
59 GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [INDEX_ODDPART_DECOMPOSITION] THEN
60 MATCH_MP_TAC(ARITH_RULE `1 * x <= y * x ==> x <= y * x`) THEN
61 REWRITE_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
62 REWRITE_TAC[EXP_EQ_0; ARITH]);;
64 let INDEX_ODDPART_UNIQUE = prove
65 (`!i m i' m'. ODD m /\ ODD m'
66 ==> (2 EXP i * m = 2 EXP i' * m' <=> i = i' /\ m = m')`,
67 REWRITE_TAC[ODD_EXISTS; ADD1] THEN
68 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[GSYM NUMPAIR; NUMPAIR_INJ] THEN
71 let INDEX_ODDPART = prove
72 (`!i m. ODD m ==> index(2 EXP i * m) = i /\ oddpart(2 EXP i * m) = m`,
73 REPEAT GEN_TAC THEN STRIP_TAC THEN
74 MP_TAC(SPECL [`i:num`; `m:num`; `index(2 EXP i * m)`; `oddpart(2 EXP i * m)`]
75 INDEX_ODDPART_UNIQUE) THEN
76 REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION; ODD_ODDPART] THEN
77 ASM_REWRITE_TAC[MULT_EQ_0; EXP_EQ_0; ARITH] THEN ASM_MESON_TAC[ODD]);;
79 (* ------------------------------------------------------------------------- *)
81 (* ------------------------------------------------------------------------- *)
83 parse_as_infix("partitions",(12,"right"));;
85 let partitions = new_definition
86 `p partitions n <=> (!i. ~(p i = 0) ==> 1 <= i /\ i <= n) /\
87 nsum(1..n) (\i. p(i) * i) = n`;;
89 let PARTITIONS_BOUND = prove
90 (`!p n. p partitions n ==> !i. p(i) <= n`,
91 REWRITE_TAC[GSYM NOT_LT] THEN SIMP_TAC[partitions] THEN REPEAT STRIP_TAC THEN
92 SUBGOAL_THEN `1 <= i /\ i <= n` STRIP_ASSUME_TAC THENL
93 [ASM_MESON_TAC[ARITH_RULE `m < n ==> ~(n = 0)`]; ALL_TAC] THEN
94 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
95 `m = n ==> n < m ==> F`)) THEN
96 MATCH_MP_TAC LET_TRANS THEN
97 EXISTS_TAC `nsum(1..n) (\j. if j = i then n else 0)` THEN CONJ_TAC THENL
98 [ASM_REWRITE_TAC[NSUM_DELTA; IN_NUMSEG; LE_REFL]; ALL_TAC] THEN
99 MATCH_MP_TAC NSUM_LT THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
101 [GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[LE_0] THEN
102 MATCH_MP_TAC LT_IMP_LE;
103 EXISTS_TAC `i:num` THEN ASM_REWRITE_TAC[]] THEN
104 MATCH_MP_TAC(ARITH_RULE `n < p /\ p * 1 <= p * k ==> n < p * k`) THEN
105 ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
107 let FINITE_PARTITIONS_LEMMA = prove
108 (`!m n. FINITE {p | (!i. p(i) <= n) /\ !i. m <= i ==> p(i) = 0}`,
109 INDUCT_TAC THEN GEN_TAC THENL
110 [SIMP_TAC[LE_0; TAUT `a /\ b <=> ~(b ==> ~a)`] THEN
111 SUBGOAL_THEN `{p | !i:num. p i = 0} = {(\n. 0)}`
112 (fun th -> SIMP_TAC[th; FINITE_RULES]) THEN
113 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN REWRITE_TAC[FUN_EQ_THM];
116 `{p | (!i. p i <= n) /\ (!i. SUC m <= i ==> p i = 0)} =
117 IMAGE (\(a,p) j. if j = m then a else p(j))
119 p IN {p | (!i. p i <= n) /\ (!i. m <= i ==> p i = 0)}}`
120 (fun t -> ASM_SIMP_TAC[t; FINITE_IMAGE; FINITE_PRODUCT; FINITE_NUMSEG]) THEN
121 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN
122 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN X_GEN_TAC `p:num->num` THEN
124 [STRIP_TAC THEN MAP_EVERY EXISTS_TAC
125 [`(p:num->num) m`; `\i:num. if i = m then 0 else p i`] THEN
126 REWRITE_TAC[FUN_EQ_THM] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
127 ONCE_REWRITE_TAC[CONJ_SYM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
128 REWRITE_TAC[PAIR_EQ; UNWIND_THM1; GSYM CONJ_ASSOC; IN_NUMSEG; LE_0] THEN
129 ASM_MESON_TAC[LE; ARITH_RULE `m <= i /\ ~(i = m) ==> SUC m <= i`];
130 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
131 MAP_EVERY X_GEN_TAC [`a:num`; `q:num->num`] THEN
132 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
133 POP_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN
134 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SYM) THEN
135 REWRITE_TAC[PAIR_EQ] THEN DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
136 ASM_MESON_TAC[ARITH_RULE `SUC m <= i ==> m <= i /\ ~(i = m)`]]);;
138 let FINITE_PARTITIONS = prove
139 (`!n. FINITE {p | p partitions n}`,
140 GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
141 EXISTS_TAC `{p | (!i. p(i) <= n) /\ (!i. SUC n <= i ==> p(i) = 0)}` THEN
142 SIMP_TAC[FINITE_PARTITIONS_LEMMA; IN_ELIM_THM; SUBSET; PARTITIONS_BOUND] THEN
143 REWRITE_TAC[partitions; LE_SUC_LT] THEN MESON_TAC[NOT_LE]);;
145 let FINITE_SUBSET_PARTITIONS = prove
146 (`!P n. FINITE {p | p partitions n /\ P p}`,
147 REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
148 EXISTS_TAC `{p | p partitions n}` THEN
149 SIMP_TAC[FINITE_PARTITIONS; IN_ELIM_THM; SUBSET]);;
151 (* ------------------------------------------------------------------------- *)
152 (* Mappings between "odd only" and "all distinct" partitions. *)
153 (* ------------------------------------------------------------------------- *)
155 let odd_of_distinct = new_definition
157 \i. if ODD i then nsum {j | p(2 EXP j * i) = 1} (\j. 2 EXP j) else 0`;;
159 let distinct_of_odd = new_definition
160 `distinct_of_odd p = \i. if (index i) IN bitset (p(oddpart i)) then 1 else 0`;;
162 (* ------------------------------------------------------------------------- *)
163 (* The critical properties. *)
164 (* ------------------------------------------------------------------------- *)
166 let ODD_ODD_OF_DISTINCT = prove
167 (`!p i. ~(odd_of_distinct p i = 0) ==> ODD i`,
168 REWRITE_TAC[odd_of_distinct] THEN MESON_TAC[]);;
170 let DISTINCT_DISTINCT_OF_ODD = prove
171 (`!p i. distinct_of_odd p i <= 1`,
172 REWRITE_TAC[distinct_of_odd] THEN ARITH_TAC);;
174 let SUPPORT_ODD_OF_DISTINCT = prove
175 (`!p. (!i. ~(p i = 0) ==> i <= n)
176 ==> !i. ~(odd_of_distinct p i = 0) ==> 1 <= i /\ i <= n`,
177 REPEAT STRIP_TAC THENL
178 [ASM_MESON_TAC[ODD; ARITH_RULE `1 <= i <=> ~(i = 0)`; ODD_ODD_OF_DISTINCT];
179 FIRST_X_ASSUM(MP_TAC o check (is_neg o concl))] THEN
180 REWRITE_TAC[odd_of_distinct] THEN
181 ASM_CASES_TAC `i = 0` THEN ASM_REWRITE_TAC[LE_0] THEN
182 SUBGOAL_THEN `FINITE {j | p (2 EXP j * i) = 1}` ASSUME_TAC THENL
183 [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
184 REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; SUBSET] THEN X_GEN_TAC `j:num` THEN
185 REWRITE_TAC[IN_ELIM_THM; LE_0] THEN DISCH_TAC THEN
186 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP j * i` THEN
187 ASM_SIMP_TAC[ARITH_EQ] THEN
188 MATCH_MP_TAC(ARITH_RULE `j < ej /\ ej * 1 <= ej * i ==> j <= ej * i`) THEN
189 REWRITE_TAC[LT_POW2_REFL; LE_MULT_LCANCEL; EXP_EQ_0; ARITH] THEN
190 UNDISCH_TAC `~(i = 0)` THEN ARITH_TAC;
191 SIMP_TAC[ARITH_RULE `~((if p then x else 0) = 0) <=> p /\ ~(x = 0)`] THEN
192 ASM_SIMP_TAC[NSUM_EQ_0_IFF; EXP_EQ_0; ARITH] THEN
193 REWRITE_TAC[NOT_FORALL_THM; IN_ELIM_THM] THEN
194 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC `j:num`)) THEN
195 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 EXP j * i` THEN
196 ASM_SIMP_TAC[ARITH; ARITH_RULE `i <= j * i <=> 1 * i <= j * i`] THEN
197 REWRITE_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= i <=> ~(i = 0)`] THEN
198 REWRITE_TAC[EXP_EQ_0; ARITH]]);;
200 let SUPPORT_DISTINCT_OF_ODD = prove
201 (`!p. (!i. p(i) * i <= n) /\
202 (!i. ~(p i = 0) ==> ODD i)
203 ==> !i. ~(distinct_of_odd p i = 0) ==> 1 <= i /\ i <= n`,
204 REWRITE_TAC[distinct_of_odd] THEN
205 REWRITE_TAC[ARITH_RULE `(if a then 1 else 0) = 0 <=> ~a`] THEN
206 GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN REPEAT STRIP_TAC THENL
207 [REWRITE_TAC[ARITH_RULE `1 <= i <=> ~(i = 0)`] THEN
208 DISCH_THEN SUBST_ALL_TAC THEN
209 UNDISCH_TAC `index 0 IN bitset (p (oddpart 0))` THEN
210 REWRITE_TAC[index; oddpart; ARITH] THEN
211 UNDISCH_THEN `!i. ~(p i = 0) ==> ODD i` (MP_TAC o SPEC `0`) THEN
212 SIMP_TAC[ARITH; BITSET_0; NOT_IN_EMPTY];
214 FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP BITSET_BOUND_LEMMA) THEN
215 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `p(oddpart i) * oddpart i` THEN
216 ASM_REWRITE_TAC[] THEN
217 GEN_REWRITE_TAC LAND_CONV [INDEX_ODDPART_DECOMPOSITION] THEN
218 ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;
220 let ODD_OF_DISTINCT_OF_ODD = prove
221 (`!p. (!i. ~(p(i) = 0) ==> ODD i)
222 ==> odd_of_distinct (distinct_of_odd p) = p`,
223 REWRITE_TAC[IN_ELIM_THM; odd_of_distinct; distinct_of_odd] THEN
224 REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
225 COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
226 ASM_SIMP_TAC[INDEX_ODDPART] THEN
227 GEN_REWRITE_TAC RAND_CONV [GSYM BINARYSUM_BITSET] THEN
228 REWRITE_TAC[binarysum] THEN
229 AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
230 GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ]);;
232 let DISTINCT_OF_ODD_OF_DISTINCT = prove
233 (`!p. (!i. ~(p i = 0) ==> 1 <= i /\ i <= n) /\ (!i. p(i) <= 1)
234 ==> distinct_of_odd (odd_of_distinct p) = p`,
235 REWRITE_TAC[distinct_of_odd; odd_of_distinct; IN_ELIM_THM] THEN
236 REWRITE_TAC[partitions; ODD_ODDPART] THEN REPEAT STRIP_TAC THEN
237 REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
238 ASM_CASES_TAC `i = 0` THEN ASM_REWRITE_TAC[BITSET_0; NOT_IN_EMPTY] THENL
239 [ASM_MESON_TAC[ARITH_RULE `~(1 <= 0)`]; ALL_TAC] THEN
240 SUBGOAL_THEN `FINITE {j | p (2 EXP j * oddpart i) = 1}` ASSUME_TAC THENL
241 [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
242 REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; SUBSET; IN_ELIM_THM] THEN
243 X_GEN_TAC `j:num` THEN DISCH_TAC THEN REWRITE_TAC[LE_0] THEN
244 MATCH_MP_TAC(ARITH_RULE `!x. y <= x /\ 1 <= x /\ x <= n ==> y <= n`) THEN
245 EXISTS_TAC `2 EXP j * oddpart i` THEN ASM_SIMP_TAC[ARITH] THEN
246 MATCH_MP_TAC(ARITH_RULE `j < ej /\ 1 * ej <= i * ej ==> j <= ej * i`) THEN
247 REWRITE_TAC[LT_POW2_REFL; LE_MULT_RCANCEL] THEN
248 ASM_MESON_TAC[ODD_ODDPART; ODD; ARITH_RULE `1 <= n <=> ~(n = 0)`];
249 ASM_SIMP_TAC[BITSET_BINARYSUM; GSYM binarysum; IN_ELIM_THM] THEN
250 REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION] THEN
251 COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
252 ASM_MESON_TAC[ARITH_RULE `i <= 1 ==> i = 0 \/ i = 1`]]);;
254 let NSUM_DISTINCT_OF_ODD = prove
255 (`!p. (!i. ~(p i = 0) ==> 1 <= i /\ i <= n) /\
256 (!i. p(i) * i <= n) /\
257 (!i. ~(p(i) = 0) ==> ODD i)
258 ==> nsum(1..n) (\i. distinct_of_odd p i * i) =
259 nsum(1..n) (\i. p i * i)`,
260 REPEAT STRIP_TAC THEN REWRITE_TAC[distinct_of_odd] THEN
261 GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV o LAND_CONV)
262 [GSYM BINARYSUM_BITSET] THEN
263 REWRITE_TAC[binarysum] THEN REWRITE_TAC[GSYM NSUM_RMUL] THEN
264 SIMP_TAC[NSUM_NSUM_PRODUCT; FINITE_BITSET; FINITE_NUMSEG] THEN
265 CONV_TAC SYM_CONV THEN ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
266 REWRITE_TAC[support; NEUTRAL_ADD] THEN
268 `{x | x IN {i,j | i IN 1..n /\ j IN bitset(p i)} /\
269 ~((\(i,j). 2 EXP j * i) x = 0)} =
270 {i,j | i IN 1..n /\ j IN bitset(p i)}`
272 [REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM] THEN
273 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
274 REWRITE_TAC[IN_NUMSEG; EXP_EQ_0; MULT_EQ_0; ARITH] THEN
275 MESON_TAC[ARITH_RULE `~(1 <= 0)`];
279 ~((if index x IN bitset (p (oddpart x)) then 1 else 0) * x = 0)} =
280 {i | i IN 1..n /\ (index i) IN bitset (p(oddpart i))}`
282 [REWRITE_TAC[EXTENSION; IN_ELIM_THM; MULT_EQ_0] THEN
283 REWRITE_TAC[IN_NUMSEG; ARITH_RULE `(if p then 1 else 0) = 0 <=> ~p`] THEN
284 MESON_TAC[ARITH_RULE `~(1 <= 0)`];
286 MATCH_MP_TAC NSUM_EQ_GENERAL THEN
287 EXISTS_TAC `\(i,b). 2 EXP b * i` THEN
288 SIMP_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
289 CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN
290 REWRITE_TAC[ARITH_RULE
291 `(if p then 1 else 0) * x * y = (if p then x * y else 0)`] THEN
292 GEN_REWRITE_TAC (RAND_CONV o TOP_DEPTH_CONV) [IN_ELIM_THM] THEN
293 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> a /\ b /\ (b ==> c)`] THEN
294 SIMP_TAC[] THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
295 REWRITE_TAC[FORALL_PAIR_THM; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
296 CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN
297 REWRITE_TAC[IN_ELIM_THM; IN_NUMSEG] THEN
298 SUBGOAL_THEN `!i j. j IN bitset(p i) ==> ODD i` ASSUME_TAC THENL
299 [ASM_MESON_TAC[BITSET_0; NOT_IN_EMPTY]; ALL_TAC] THEN
301 [X_GEN_TAC `m:num` THEN STRIP_TAC THEN CONJ_TAC THENL
302 [MAP_EVERY EXISTS_TAC [`oddpart m`; `index m`] THEN
303 ASM_REWRITE_TAC[GSYM INDEX_ODDPART_DECOMPOSITION] THEN
304 ASM_MESON_TAC[ODDPART_LE; LE_TRANS; ARITH_RULE `1 <= x <=> ~(x = 0)`;
306 ASM_MESON_TAC[INDEX_ODDPART_UNIQUE]];
307 MAP_EVERY X_GEN_TAC [`m:num`; `i:num`] THEN STRIP_TAC THEN
308 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[INDEX_ODDPART]] THEN CONJ_TAC THENL
309 [REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`] THEN
310 REWRITE_TAC[MULT_EQ_0; EXP_EQ_0; ARITH] THEN
311 ASM_MESON_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`];
312 ASM_MESON_TAC[BITSET_BOUND_LEMMA; LE_MULT_RCANCEL; LE_TRANS]]]);;
314 let DISTINCT_OF_ODD = prove
315 (`!p. p IN {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}
316 ==> (distinct_of_odd p) IN {p | p partitions n /\ !i. p(i) <= 1}`,
317 GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; partitions] THEN STRIP_TAC THEN
318 REWRITE_TAC[DISTINCT_DISTINCT_OF_ODD] THEN CONJ_TAC THENL
319 [MATCH_MP_TAC SUPPORT_DISTINCT_OF_ODD;
320 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
321 MATCH_MP_TAC NSUM_DISTINCT_OF_ODD] THEN
322 ASM_REWRITE_TAC[] THEN
323 X_GEN_TAC `i:num` THEN ASM_CASES_TAC `(p:num->num) i = 0` THEN
324 ASM_REWRITE_TAC[MULT_CLAUSES; LE_0] THEN
325 ASM_MESON_TAC[NSUM_BOUND_LEMMA]);;
327 let ODD_OF_DISTINCT = prove
328 (`!p. p IN {p | p partitions n /\ !i. p(i) <= 1}
329 ==> (odd_of_distinct p) IN
330 {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}`,
331 GEN_TAC THEN REWRITE_TAC[partitions; IN_ELIM_THM] THEN STRIP_TAC THEN
332 REWRITE_TAC[ODD_ODD_OF_DISTINCT] THEN
333 CONJ_TAC THENL [ASM_MESON_TAC[SUPPORT_ODD_OF_DISTINCT]; ALL_TAC] THEN
334 MATCH_MP_TAC EQ_TRANS THEN
335 EXISTS_TAC `nsum(1..n) (\i. distinct_of_odd(odd_of_distinct p) i * i)` THEN
338 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
339 AP_TERM_TAC THEN ABS_TAC THEN AP_THM_TAC THEN
340 ASM_MESON_TAC[DISTINCT_OF_ODD_OF_DISTINCT]] THEN
341 CONV_TAC SYM_CONV THEN MATCH_MP_TAC NSUM_DISTINCT_OF_ODD THEN
342 REWRITE_TAC[ODD_ODD_OF_DISTINCT] THEN
343 CONJ_TAC THENL [ASM_MESON_TAC[SUPPORT_ODD_OF_DISTINCT]; ALL_TAC] THEN
344 X_GEN_TAC `i:num` THEN REWRITE_TAC[odd_of_distinct] THEN
345 COND_CASES_TAC THEN ASM_REWRITE_TAC[LE_0; MULT_CLAUSES] THEN
346 REWRITE_TAC[GSYM NSUM_RMUL] THEN
347 SUBGOAL_THEN `FINITE {i:num | p(i) = 1}` ASSUME_TAC THENL
348 [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `1..n` THEN
349 REWRITE_TAC[FINITE_NUMSEG; SUBSET; IN_NUMSEG; IN_ELIM_THM] THEN
350 ASM_MESON_TAC[ARITH_RULE `~(1 = 0)`];
352 ONCE_REWRITE_TAC[GSYM(REWRITE_CONV[o_DEF]
353 `(\j. j) o (\j. 2 EXP j * i)`)] THEN
354 ASM_SIMP_TAC[GSYM NSUM_IMAGE; INDEX_ODDPART_UNIQUE] THEN
355 MATCH_MP_TAC LE_TRANS THEN
356 EXISTS_TAC `nsum {i | p(i) = 1} (\j. j)` THEN CONJ_TAC THENL
357 [MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
359 MATCH_MP_TAC LE_TRANS THEN
360 EXISTS_TAC `nsum {i | p(i) = 1} (\j. p(j) * j)` THEN CONJ_TAC THENL
361 [MATCH_MP_TAC EQ_IMP_LE THEN MATCH_MP_TAC NSUM_EQ THEN
362 SIMP_TAC[IN_ELIM_THM; MULT_CLAUSES];
363 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
364 MATCH_MP_TAC NSUM_SUBSET_SIMPLE THEN
365 REWRITE_TAC[FINITE_NUMSEG; SUBSET; IN_NUMSEG; IN_ELIM_THM] THEN
366 ASM_MESON_TAC[ARITH_RULE `~(1 = 0)`]]);;
368 (* ------------------------------------------------------------------------- *)
369 (* Euler's partition theorem: *)
371 (* The number of partitions into distinct numbers is equal to the number of *)
372 (* partitions into odd numbers (and there are only finitely many of each). *)
373 (* ------------------------------------------------------------------------- *)
375 let EULER_PARTITION_THEOREM = prove
376 (`FINITE {p | p partitions n /\ !i. p(i) <= 1} /\
377 FINITE {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i} /\
378 CARD {p | p partitions n /\ !i. p(i) <= 1} =
379 CARD {p | p partitions n /\ !i. ~(p(i) = 0) ==> ODD i}`,
380 MATCH_MP_TAC CARD_EQ_LEMMA THEN REWRITE_TAC[FINITE_SUBSET_PARTITIONS] THEN
381 MAP_EVERY EXISTS_TAC [`odd_of_distinct`; `distinct_of_odd`] THEN
382 REWRITE_TAC[ODD_OF_DISTINCT; DISTINCT_OF_ODD] THEN
383 CONJ_TAC THEN X_GEN_TAC `p:num->num` THEN
384 REWRITE_TAC[IN_ELIM_THM; partitions] THEN STRIP_TAC THENL
385 [MATCH_MP_TAC DISTINCT_OF_ODD_OF_DISTINCT;
386 MATCH_MP_TAC ODD_OF_DISTINCT_OF_ODD] THEN