Update from HH
[hl193./.git] / 100 / euler.ml
1 (* ========================================================================= *)
2 (* Euler's partition theorem and other elementary partition theorems.        *)
3 (* ========================================================================= *)
4
5 loadt "Library/binary.ml";;
6
7 (* ------------------------------------------------------------------------- *)
8 (* Some lemmas.                                                              *)
9 (* ------------------------------------------------------------------------- *)
10
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]);;
15
16 let CARD_EQ_LEMMA = prove
17  (`!f:A->B g s t.
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[]);;
27
28 (* ------------------------------------------------------------------------- *)
29 (* Breaking a number up into 2^something * odd_number.                       *)
30 (* ------------------------------------------------------------------------- *)
31
32 let index = define
33  `index n = if n = 0 then 0 else if ODD n then 0 else SUC(index(n DIV 2))`;;
34
35 let oddpart = define
36  `oddpart n = if n = 0 then 0 else if ODD n then n else oddpart(n DIV 2)`;;
37
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)`]);;
48
49 let INDEX_ODDPART_DECOMPOSITION = prove
50  (`!n. n = 2 EXP (index n) * oddpart n`,
51   MESON_TAC[INDEX_ODDPART_WORK]);;
52
53 let ODD_ODDPART = prove
54  (`!n. ODD(oddpart n) <=> ~(n = 0)`,
55   MESON_TAC[INDEX_ODDPART_WORK]);;
56
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]);;
63
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
69   ARITH_TAC);;
70
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]);;
78
79 (* ------------------------------------------------------------------------- *)
80 (* Partitions.                                                               *)
81 (* ------------------------------------------------------------------------- *)
82
83 parse_as_infix("partitions",(12,"right"));;
84
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`;;
88
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
100   CONJ_TAC THENL
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]);;
106
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];
114     ALL_TAC] THEN
115   SUBGOAL_THEN
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))
118         {a,p | a IN 0..n /\
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
123   EQ_TAC THENL
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)`]]);;
137
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]);;
144
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]);;
150
151 (* ------------------------------------------------------------------------- *)
152 (* Mappings between "odd only" and "all distinct" partitions.                *)
153 (* ------------------------------------------------------------------------- *)
154
155 let odd_of_distinct = new_definition
156  `odd_of_distinct p =
157     \i. if ODD i then nsum {j | p(2 EXP j * i) = 1} (\j. 2 EXP j) else 0`;;
158
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`;;
161
162 (* ------------------------------------------------------------------------- *)
163 (* The critical properties.                                                  *)
164 (* ------------------------------------------------------------------------- *)
165
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[]);;
169
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);;
173
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]]);;
199
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];
213     ALL_TAC] THEN
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]);;
219
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]);;
231
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`]]);;
253
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
267   SUBGOAL_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)}`
271   SUBST1_TAC THENL
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)`];
276     ALL_TAC] THEN
277   SUBGOAL_THEN
278    `{x | x IN 1 .. n /\
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))}`
281   SUBST1_TAC THENL
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)`];
285     ALL_TAC] THEN
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
300   CONJ_TAC THENL
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)`;
305                     ODD_ODDPART; ODD];
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]]]);;
313
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]);;
326
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
336   CONJ_TAC THENL
337    [ALL_TAC;
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)`];
351     ALL_TAC] THEN
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[];
358     ALL_TAC] THEN
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)`]]);;
367
368 (* ------------------------------------------------------------------------- *)
369 (* Euler's partition theorem:                                                *)
370 (*                                                                           *)
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 (* ------------------------------------------------------------------------- *)
374
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
387   ASM_REWRITE_TAC[]);;