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[]);;