100/inclusion_exclusion.ml

   1 (* ========================================================================= *)
   2 (* Inclusion-exclusion principle, the usual and generalized forms.           *)
   3 (* ========================================================================= *)
   4
   5 (* ------------------------------------------------------------------------- *)
   6 (* Simple set theory lemmas.                                                 *)
   7 (* ------------------------------------------------------------------------- *)
   8
   9 let SUBSET_INSERT_EXISTS = prove
  10  (`!s x:A t. s SUBSET (x INSERT t) <=>
  11                 s SUBSET t \/ ?u. u SUBSET t /\ s = x INSERT u`,
  12   REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
  13   MATCH_MP_TAC(TAUT `(a /\ ~b ==> c) ==> a ==> b \/ c`) THEN
  14   DISCH_TAC THEN EXISTS_TAC `s DELETE (x:A)` THEN ASM SET_TAC[]);;
  15
  16 let FINITE_SUBSETS_RESTRICT = prove
  17  (`!s:A->bool p. FINITE s ==> FINITE {t | t SUBSET s /\ p t}`,
  18   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
  19   EXISTS_TAC `{t:A->bool | t SUBSET s}` THEN
  20   ASM_SIMP_TAC[FINITE_POWERSET] THEN SET_TAC[]);;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* Versions for additive real functions, where the additivity applies only   *)
  24 (* to some specific subsets (e.g. cardinality of finite sets, measurable     *)
  25 (* sets with bounded measure).                                               *)
  26 (* ------------------------------------------------------------------------- *)
  27
  28 let INCLUSION_EXCLUSION_REAL_RESTRICTED_INDEXED = prove
  29  (`!P (f:(A->bool)->real) (A:I->bool) (x:I->(A->bool)).
  30         (!s t. P s /\ P t /\ DISJOINT s t
  31                ==> f(s UNION t) = f(s) + f(t)) /\
  32         P {} /\
  33         (!s t. P s /\ P t ==> P(s INTER t) /\ P(s UNION t) /\ P(s DIFF t)) /\
  34         FINITE A /\ (!a. a IN A ==> P(x a))
  35         ==> f(UNIONS(IMAGE x A)) =
  36             sum {B | B SUBSET A /\ ~(B = {})}
  37                 (\B. (-- &1) pow (CARD B + 1) * f(INTERS(IMAGE x B)))`,
  38   let lemma = prove
  39    (`{t | t SUBSET (a INSERT s) /\ P t} =
  40      {t | t SUBSET s /\ P t} UNION
  41      {a INSERT t |t| t SUBSET s /\ P(a INSERT t)}`,
  42     REWRITE_TAC[SUBSET_INSERT_EXISTS] THEN
  43     GEN_REWRITE_TAC I [EXTENSION] THEN
  44     REWRITE_TAC[IN_ELIM_THM; IN_UNION] THEN MESON_TAC[]) in
  45   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  46   REPEAT GEN_TAC THEN REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN
  47   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_FORALL_THM] THEN
  48   REWRITE_TAC[IMP_IMP] THEN STRIP_TAC THEN
  49   MATCH_MP_TAC(MESON[HAS_SIZE]
  50    `(!n s. s HAS_SIZE n ==> P s) ==> (!s. FINITE s ==> P s)`) THEN
  51   MATCH_MP_TAC num_WF THEN MATCH_MP_TAC num_INDUCTION THEN
  52   REWRITE_TAC[HAS_SIZE_CLAUSES; LEFT_IMP_EXISTS_THM] THEN CONJ_TAC THENL
  53    [DISCH_THEN(K ALL_TAC) THEN GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
  54     REWRITE_TAC[UNIONS_0; IMAGE_CLAUSES; SUBSET_EMPTY; TAUT `~(p /\ ~p)`] THEN
  55     ASM_REWRITE_TAC[EMPTY_GSPEC; SUM_CLAUSES] THEN REPEAT STRIP_TAC THEN
  56     REPEAT(FIRST_X_ASSUM(MP_TAC o SPECL [`{}:A->bool`; `{}:A->bool`])) THEN
  57     ASM_SIMP_TAC[UNION_EMPTY; DISJOINT_EMPTY] THEN REAL_ARITH_TAC;
  58     ALL_TAC] THEN
  59   X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN DISCH_TAC THEN
  60   MAP_EVERY X_GEN_TAC [`A0:I->bool`; `a:I`; `A:I->bool`] THEN
  61   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  62   DISCH_THEN SUBST1_TAC THEN X_GEN_TAC  `x:I->A->bool` THEN
  63   REWRITE_TAC[FORALL_IN_INSERT] THEN STRIP_TAC THEN
  64   REWRITE_TAC[IMAGE_CLAUSES; UNIONS_INSERT] THEN MATCH_MP_TAC EQ_TRANS THEN
  65   EXISTS_TAC `(f(x a) + f(UNIONS (IMAGE (x:I->(A->bool)) A))) -
  66               f(x a INTER UNIONS (IMAGE x A)):real` THEN
  67   CONJ_TAC THENL
  68    [SUBGOAL_THEN
  69      `P(x a) /\ P(UNIONS(IMAGE (x:I->(A->bool)) A))`
  70     MP_TAC THENL
  71      [ASM_REWRITE_TAC[] THEN
  72       UNDISCH_TAC `!b. b IN A ==> P((x:I->(A->bool)) b)` THEN
  73       SUBGOAL_THEN `FINITE(A:I->bool)` MP_TAC THENL
  74        [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
  75       SPEC_TAC(`A:I->bool`,`u:I->bool`) THEN
  76       MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  77       ASM_SIMP_TAC[IMAGE_CLAUSES; UNIONS_0; UNIONS_INSERT; FORALL_IN_INSERT];
  78       SPEC_TAC(`UNIONS(IMAGE (x:I->(A->bool)) A)`,`t:A->bool`) THEN
  79       SPEC_TAC(`(x:I->(A->bool)) a`,`s:A->bool`) THEN
  80       REPEAT STRIP_TAC THEN
  81       UNDISCH_TAC `!s t:A->bool. P s /\ P t /\ DISJOINT s t
  82                                  ==> f(s UNION t):real = f(s) + f(t)` THEN
  83       DISCH_THEN(fun th ->
  84      MP_TAC(ISPECL [`s INTER t:A->bool`; `t DIFF s:A->bool`] th) THEN
  85      MP_TAC(ISPECL [`s:A->bool`; `t DIFF s:A->bool`] th)) THEN
  86      ASM_SIMP_TAC[SET_RULE `s UNION (t DIFF s) = s UNION t`;
  87                   SET_RULE `(s INTER t) UNION (t DIFF s) = t`] THEN
  88      REPEAT(ANTS_TAC THENL [SET_TAC[]; DISCH_TAC]) THEN ASM_REAL_ARITH_TAC];
  89     ALL_TAC] THEN
  90   REWRITE_TAC[INTER_UNIONS; SIMPLE_IMAGE; GSYM IMAGE_o; o_DEF] THEN
  91   FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN REWRITE_TAC[LT] THEN
  92   DISCH_THEN(MP_TAC o SPEC `A:I->bool`) THEN ASM_REWRITE_TAC[] THEN
  93   DISCH_THEN(fun th ->
  94     MP_TAC(ISPEC `\s. (x:I->(A->bool)) a INTER x s` th) THEN
  95     MP_TAC(ISPEC `x:I->(A->bool)` th)) THEN
  96   ASM_SIMP_TAC[] THEN REPEAT(DISCH_THEN SUBST1_TAC) THEN
  97   FIRST_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [HAS_SIZE]) THEN
  98   REWRITE_TAC[lemma] THEN
  99   W(MP_TAC o PART_MATCH (lhand o rand) SUM_UNION o rand o snd) THEN
 100   ANTS_TAC THENL
 101    [ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
 102     ASM_SIMP_TAC[FINITE_SUBSETS_RESTRICT; FINITE_IMAGE] THEN
 103     REWRITE_TAC[GSYM SIMPLE_IMAGE_GEN] THEN
 104     REWRITE_TAC[IN_DISJOINT; EXISTS_IN_GSPEC] THEN
 105     ONCE_REWRITE_TAC[CONJ_SYM] THEN
 106     REWRITE_TAC[EXISTS_IN_GSPEC] THEN ASM SET_TAC[];
 107     DISCH_THEN SUBST1_TAC] THEN
 108   REWRITE_TAC[NOT_INSERT_EMPTY; REAL_ARITH
 109    `(fa + s) - fas:real = s + s' <=> fa - fas = s'`] THEN
 110   MATCH_MP_TAC EQ_TRANS THEN
 111   EXISTS_TAC `f((x:I->(A->bool)) a) +
 112               sum {B | B SUBSET A /\ ~(B = {})}
 113                   (\B. --(&1) pow (CARD B) *
 114                        f(INTERS(IMAGE x (a INSERT B))))` THEN
 115   CONJ_TAC THENL
 116    [REWRITE_TAC[REAL_ARITH `x - a:real = x + b <=> b = --a`] THEN
 117     REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_EQ THEN
 118     REWRITE_TAC[IMAGE_CLAUSES; INTERS_INSERT; o_DEF; FORALL_IN_GSPEC] THEN
 119     REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
 120     REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN
 121     REWRITE_TAC[REAL_NEG_NEG; REAL_MUL_RID] THEN AP_TERM_TAC THEN
 122     AP_TERM_TAC THEN REWRITE_TAC[INTERS_IMAGE] THEN ASM SET_TAC[];
 123     REWRITE_TAC[SET_RULE `{s | P s /\ ~(s = e)} = {s | P s} DELETE e`] THEN
 124     ASM_SIMP_TAC[SUM_DELETE_CASES; GSYM DELETE; FINITE_POWERSET] THEN
 125     REWRITE_TAC[IN_ELIM_THM; EMPTY_SUBSET; IMAGE_CLAUSES] THEN
 126     GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SIMPLE_IMAGE_GEN] THEN
 127     W(MP_TAC o PART_MATCH (lhand o rand) SUM_IMAGE o rand o snd) THEN
 128     ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
 129     REWRITE_TAC[o_DEF; INTERS_1; CARD_CLAUSES; real_pow; REAL_MUL_LID] THEN
 130     REWRITE_TAC[REAL_SUB_ADD2] THEN MATCH_MP_TAC SUM_EQ THEN
 131     REWRITE_TAC[FORALL_IN_GSPEC; REAL_POW_ADD; REAL_POW_1] THEN
 132     X_GEN_TAC `B:I->bool` THEN DISCH_TAC THEN
 133     SUBGOAL_THEN `FINITE(B:I->bool)` ASSUME_TAC THENL
 134      [ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
 135     ASM_SIMP_TAC[CARD_CLAUSES; REAL_POW_ADD; real_pow] THEN
 136     COND_CASES_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 137     REWRITE_TAC[IMAGE_CLAUSES; real_pow] THEN REAL_ARITH_TAC]);;
 138
 139 let INCLUSION_EXCLUSION_REAL_RESTRICTED = prove
 140  (`!P (f:(A->bool)->real) (A:(A->bool)->bool).
 141         (!s t. P s /\ P t /\ DISJOINT s t
 142                ==> f(s UNION t) = f(s) + f(t)) /\
 143         P {} /\
 144         (!s t. P s /\ P t ==> P(s INTER t) /\ P(s UNION t) /\ P(s DIFF t)) /\
 145         FINITE A /\ (!a. a IN A ==> P(a))
 146         ==> f(UNIONS A) =
 147             sum {B | B SUBSET A /\ ~(B = {})}
 148                 (\B. (-- &1) pow (CARD B + 1) * f(INTERS B))`,
 149   REPEAT STRIP_TAC THEN
 150   MP_TAC(ISPECL [`P:(A->bool)->bool`; `f:(A->bool)->real`;
 151                  `A:(A->bool)->bool`; `\x:A->bool. x`]
 152         INCLUSION_EXCLUSION_REAL_RESTRICTED_INDEXED) THEN
 153   ASM_REWRITE_TAC[IMAGE_ID]);;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* Versions for unrestrictedly additive functions.                           *)
 157 (* ------------------------------------------------------------------------- *)
 158
 159 let INCLUSION_EXCLUSION_REAL_INDEXED = prove
 160  (`!(f:(A->bool)->real) (A:I->bool) (x:I->(A->bool)).
 161         (!s t. DISJOINT s t ==> f(s UNION t) = f(s) + f(t)) /\ FINITE A
 162         ==> f(UNIONS(IMAGE x A)) =
 163             sum {B | B SUBSET A /\ ~(B = {})}
 164                 (\B. (-- &1) pow (CARD B + 1) * f(INTERS(IMAGE x B)))`,
 165   MP_TAC(ISPEC
 166    `\x:A->bool. T` INCLUSION_EXCLUSION_REAL_RESTRICTED_INDEXED) THEN
 167   REWRITE_TAC[]);;
 168
 169 let INCLUSION_EXCLUSION_REAL = prove
 170  (`!(f:(A->bool)->real) (A:(A->bool)->bool).
 171         (!s t. DISJOINT s t ==> f(s UNION t) = f(s) + f(t)) /\ FINITE A
 172         ==> f(UNIONS A) =
 173             sum {B | B SUBSET A /\ ~(B = {})}
 174                 (\B. (-- &1) pow (CARD B + 1) * f(INTERS B))`,
 175   REPEAT STRIP_TAC THEN
 176   MP_TAC(ISPECL [`f:(A->bool)->real`; `A:(A->bool)->bool`; `\x:A->bool. x`]
 177         INCLUSION_EXCLUSION_REAL_INDEXED) THEN
 178   ASM_REWRITE_TAC[IMAGE_ID]);;
 179
 180 (* ------------------------------------------------------------------------- *)
 181 (* Special case of cardinality, the most common case.                        *)
 182 (* ------------------------------------------------------------------------- *)
 183
 184 let INCLUSION_EXCLUSION = prove
 185  (`!s:(A->bool)->bool.
 186         FINITE s /\ (!k. k IN s ==> FINITE k)
 187         ==> &(CARD(UNIONS s)) =
 188                 sum {t | t SUBSET s /\ ~(t = {})}
 189                     (\t. (-- &1) pow (CARD t + 1) * &(CARD(INTERS t)))`,
 190   REPEAT STRIP_TAC THEN MP_TAC(ISPECL
 191    [`\s:A->bool. FINITE s`; `\s:A->bool. &(CARD s)`;
 192     `s:(A->bool)->bool`] INCLUSION_EXCLUSION_REAL_RESTRICTED) THEN
 193   ASM_SIMP_TAC[FINITE_INTER; FINITE_UNION; FINITE_DIFF; FINITE_EMPTY] THEN
 194   DISCH_THEN MATCH_MP_TAC THEN
 195   SIMP_TAC[CARD_UNION; DISJOINT; REAL_OF_NUM_ADD]);;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* A more conventional form.                                                 *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let INCLUSION_EXCLUSION_USUAL = prove
 202  (`!s:(A->bool)->bool.
 203         FINITE s /\ (!k. k IN s ==> FINITE k)
 204         ==> &(CARD(UNIONS s)) =
 205                 sum (1..CARD s) (\n. (-- &1) pow (n + 1) *
 206                                      sum {t | t SUBSET s /\ t HAS_SIZE n}
 207                                          (\t. &(CARD(INTERS t))))`,
 208   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[INCLUSION_EXCLUSION] THEN
 209   W(MP_TAC o PART_MATCH (lhs o rand) (ISPEC `CARD` SUM_IMAGE_GEN) o
 210      lhand o snd) THEN
 211   ASM_SIMP_TAC[FINITE_SUBSETS_RESTRICT] THEN DISCH_THEN SUBST1_TAC THEN
 212   MATCH_MP_TAC(MESON[] `s = t /\ sum t f = sum t g ==> sum s f = sum t g`) THEN
 213   CONJ_TAC THENL
 214    [GEN_REWRITE_TAC I [EXTENSION] THEN
 215     REWRITE_TAC[IN_IMAGE; IN_NUMSEG; IN_ELIM_THM] THEN
 216     REWRITE_TAC[ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
 217     ASM_MESON_TAC[CHOOSE_SUBSET; CARD_SUBSET; FINITE_SUBSET; CARD_EQ_0;
 218                   HAS_SIZE];
 219     ALL_TAC] THEN
 220   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[IN_NUMSEG] THEN
 221   STRIP_TAC THEN REWRITE_TAC[SUM_LMUL] THEN AP_TERM_TAC THEN
 222   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[IN_ELIM_THM; HAS_SIZE] THEN
 223   GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 224   ASM_MESON_TAC[CARD_EQ_0; ARITH_RULE `~(1 <= 0)`; FINITE_SUBSET]);;
 225
 226 (* ------------------------------------------------------------------------- *)
 227 (* A combinatorial lemma about subsets of a finite set.                      *)
 228 (* ------------------------------------------------------------------------- *)
 229
 230 let FINITE_SUBSETS_RESTRICT = prove
 231  (`!s:A->bool p. FINITE s ==> FINITE {t | t SUBSET s /\ p t}`,
 232   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 233   EXISTS_TAC `{t:A->bool | t SUBSET s}` THEN
 234   ASM_SIMP_TAC[FINITE_POWERSET] THEN SET_TAC[]);;
 235
 236 let CARD_ADJUST_LEMMA = prove
 237  (`!f:A->B s x y.
 238         FINITE s /\
 239         (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) /\
 240         x = y + CARD (IMAGE f s)
 241         ==> x = y + CARD s`,
 242   MESON_TAC[CARD_IMAGE_INJ]);;
 243
 244 let CARD_SUBSETS_STEP = prove
 245  (`!x:A s. FINITE s /\ ~(x IN s) /\ u SUBSET s
 246            ==> CARD {t | t SUBSET (x INSERT s) /\ u SUBSET t /\ ODD(CARD t)} =
 247                  CARD {t | t SUBSET s /\ u SUBSET t /\ ODD(CARD t)} +
 248                  CARD {t | t SUBSET s /\ u SUBSET t /\ EVEN(CARD t)} /\
 249                CARD {t | t SUBSET (x INSERT s) /\ u SUBSET t /\ EVEN(CARD t)} =
 250                  CARD {t | t SUBSET s /\ u SUBSET t /\ EVEN(CARD t)} +
 251                  CARD {t | t SUBSET s /\ u SUBSET t /\ ODD(CARD t)}`,
 252   REPEAT STRIP_TAC THEN
 253   MATCH_MP_TAC(INST_TYPE[`:A`,`:B`] CARD_ADJUST_LEMMA) THEN
 254   EXISTS_TAC `\u. (x:A) INSERT u` THEN
 255   ASM_SIMP_TAC[FINITE_SUBSETS_RESTRICT] THEN
 256   (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 257    CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
 258    ASM_SIMP_TAC[FINITE_SUBSETS_RESTRICT; FINITE_INSERT] THEN CONJ_TAC THENL
 259     [REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER] THEN
 260      REWRITE_TAC[TAUT `~(a /\ b) <=> b ==> ~a`; FORALL_IN_IMAGE] THEN
 261      ASM SET_TAC[];
 262      ALL_TAC] THEN
 263    GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `t:A->bool` THEN
 264    REWRITE_TAC[IN_ELIM_THM; IN_UNION; SUBSET_INSERT_EXISTS] THEN
 265    REWRITE_TAC[IN_IMAGE; IN_ELIM_THM] THEN
 266    REWRITE_TAC[RIGHT_OR_DISTRIB; LEFT_AND_EXISTS_THM] THEN AP_TERM_TAC THEN
 267    AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 268    X_GEN_TAC `v:A->bool` THEN
 269    ASM_CASES_TAC `t = (x:A) INSERT v` THEN ASM_REWRITE_TAC[] THEN
 270    ASM_CASES_TAC `(v:A->bool) SUBSET s` THEN ASM_REWRITE_TAC[] THEN
 271    BINOP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 272    ASM_MESON_TAC[CARD_CLAUSES; EVEN; NOT_ODD; FINITE_SUBSET; SUBSET] THEN
 273    ASM_MESON_TAC[CARD_CLAUSES; EVEN; NOT_ODD; FINITE_SUBSET; SUBSET]));;
 274
 275 let CARD_SUBSUPERSETS_EVEN_ODD = prove
 276  (`!s u:A->bool.
 277         FINITE u /\ s PSUBSET u
 278         ==> CARD {t | s SUBSET t /\ t SUBSET u /\ EVEN(CARD t)} =
 279             CARD {t | s SUBSET t /\ t SUBSET u /\ ODD(CARD t)}`,
 280   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
 281   REPEAT GEN_TAC THEN WF_INDUCT_TAC `CARD(u:A->bool)` THEN
 282   REWRITE_TAC[PSUBSET_MEMBER] THEN
 283   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 284   DISCH_THEN(X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC) THEN
 285   FIRST_X_ASSUM(SUBST_ALL_TAC o MATCH_MP (SET_RULE
 286    `x IN s ==> s = x INSERT (s DELETE x)`)) THEN
 287   MP_TAC(SET_RULE `~((x:A) IN (u DELETE x))`) THEN
 288   ABBREV_TAC `v:A->bool = u DELETE x` THEN STRIP_TAC THEN
 289   SUBGOAL_THEN `FINITE v /\ (s:A->bool) SUBSET v` STRIP_ASSUME_TAC THENL
 290    [ASM SET_TAC[FINITE_INSERT]; ALL_TAC] THEN
 291   ASM_SIMP_TAC[CARD_SUBSETS_STEP] THEN ASM_CASES_TAC `s:A->bool = v` THENL
 292    [REWRITE_TAC[CONJ_ASSOC; SUBSET_ANTISYM_EQ] THEN MATCH_ACCEPT_TAC ADD_SYM;
 293     ASM_SIMP_TAC[CARD_CLAUSES; LT; PSUBSET]]);;
 294
 295 let SUM_ALTERNATING_CANCELS = prove
 296  (`!s:A->bool f.
 297         FINITE s /\
 298         CARD {x | x IN s /\ EVEN(f x)} = CARD {x | x IN s /\ ODD(f x)}
 299         ==> sum s (\x. (-- &1) pow (f x)) = &0`,
 300   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 301   EXISTS_TAC `sum {x | x IN s /\ EVEN(f x)} (\x. (-- &1) pow (f x)) +
 302               sum {x:A | x IN s /\ ODD(f x)} (\x. (-- &1) pow (f x))` THEN
 303   CONJ_TAC THENL
 304    [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_UNION_EQ THEN
 305     ASM_SIMP_TAC[EXTENSION; IN_ELIM_THM; IN_INTER; IN_UNION; NOT_IN_EMPTY] THEN
 306     REWRITE_TAC[GSYM NOT_EVEN] THEN MESON_TAC[];
 307     ALL_TAC] THEN
 308   ASM_SIMP_TAC[REAL_POW_NEG; REAL_POW_ONE; GSYM NOT_EVEN; SUM_CONST;
 309                FINITE_RESTRICT; REAL_ARITH `x * &1 + x * -- &1 = &0`]);;
 310
 311 (* ------------------------------------------------------------------------- *)
 312 (* Hence a general "Moebius inversion" inclusion-exclusion principle.        *)
 313 (* This "symmetric" form is from Ira Gessel: "Symmetric Inclusion-Exclusion" *)
 314 (* ------------------------------------------------------------------------- *)
 315
 316 let INCLUSION_EXCLUSION_SYMMETRIC = prove
 317  (`!f g:(A->bool)->real.
 318     (!s. FINITE s
 319          ==> g(s) = sum {t | t SUBSET s} (\t. (-- &1) pow (CARD t) * f(t)))
 320     ==> !s. FINITE s
 321             ==> f(s) = sum {t | t SUBSET s} (\t. (-- &1) pow (CARD t) * g(t))`,
 322   REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC EQ_TRANS THEN
 323   EXISTS_TAC `sum {t:A->bool | t SUBSET s}
 324                   (\t. (-- &1) pow (CARD t) *
 325                        sum {u | u IN {u | u SUBSET s} /\ u SUBSET t}
 326                            (\u. (-- &1) pow (CARD u) * f(u)))` THEN
 327   CONJ_TAC THENL
 328    [MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC[IN_ELIM_THM; SET_RULE
 329      `s SUBSET t ==> (u SUBSET t /\ u SUBSET s <=> u SUBSET s)`] THEN
 330     ASM_MESON_TAC[FINITE_SUBSET];
 331     ALL_TAC] THEN
 332   REWRITE_TAC[GSYM SUM_LMUL] THEN
 333   W(MP_TAC o PART_MATCH (lhand o rand) SUM_SUM_RESTRICT o lhs o snd) THEN
 334   ASM_SIMP_TAC[FINITE_POWERSET] THEN DISCH_THEN SUBST1_TAC THEN
 335   REWRITE_TAC[SUM_RMUL; IN_ELIM_THM] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 336    `sum {u | u SUBSET s} (\u:A->bool. if u = s then f(s) else &0)` THEN
 337   CONJ_TAC THENL [ALL_TAC; SIMP_TAC[SUM_DELTA; IN_ELIM_THM; SUBSET_REFL]] THEN
 338   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `u:A->bool` THEN
 339   REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
 340   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
 341    [REWRITE_TAC[SUBSET_ANTISYM_EQ; SET_RULE `{x | x = a} = {a}`] THEN
 342     REWRITE_TAC[SUM_SING; REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN
 343     REWRITE_TAC[REAL_POW_NEG; EVEN_ADD; REAL_POW_ONE; REAL_MUL_LID];
 344     ALL_TAC] THEN
 345   REWRITE_TAC[REAL_ENTIRE] THEN REPEAT DISJ1_TAC THEN
 346   MATCH_MP_TAC SUM_ALTERNATING_CANCELS THEN
 347   ASM_SIMP_TAC[FINITE_SUBSETS_RESTRICT; IN_ELIM_THM] THEN
 348   ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
 349   MATCH_MP_TAC CARD_SUBSUPERSETS_EVEN_ODD THEN ASM SET_TAC[]);;
 350
 351 (* ------------------------------------------------------------------------- *)
 352 (* The more typical non-symmetric version.                                   *)
 353 (* ------------------------------------------------------------------------- *)
 354
 355 let INCLUSION_EXCLUSION_MOBIUS = prove
 356  (`!f g:(A->bool)->real.
 357         (!s. FINITE s ==> g(s) = sum {t | t SUBSET s} f)
 358         ==> !s. FINITE s
 359                 ==> f(s) = sum {t | t SUBSET s}
 360                                (\t. (-- &1) pow (CARD s - CARD t) * g(t))`,
 361   REPEAT STRIP_TAC THEN
 362   MP_TAC(ISPECL [`\t. -- &1 pow CARD(t:A->bool) * f t`; `g:(A->bool)->real`]
 363                 INCLUSION_EXCLUSION_SYMMETRIC) THEN
 364   REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN ANTS_TAC THENL
 365    [ASM_SIMP_TAC[EVEN_ADD; REAL_POW_ONE; REAL_POW_NEG; REAL_MUL_LID; ETA_AX];
 366     ALL_TAC] THEN
 367   DISCH_THEN(MP_TAC o SPEC `s:A->bool`) THEN ASM_REWRITE_TAC[] THEN
 368   DISCH_THEN(MP_TAC o AP_TERM `(*) ((-- &1) pow (CARD(s:A->bool)))`) THEN
 369   REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD; GSYM MULT_2] THEN
 370   REWRITE_TAC[GSYM REAL_POW_POW] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 371   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID] THEN DISCH_THEN SUBST1_TAC THEN
 372   REWRITE_TAC[GSYM SUM_LMUL] THEN MATCH_MP_TAC SUM_EQ THEN
 373   X_GEN_TAC `u:A->bool` THEN REWRITE_TAC[IN_ELIM_THM; REAL_MUL_ASSOC] THEN
 374   ASM_SIMP_TAC[REAL_POW_SUB; REAL_ARITH `~(-- &1 = &0)`; CARD_SUBSET] THEN
 375   REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE] THEN
 376   REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN REAL_ARITH_TAC);;
 377
 378 (* ------------------------------------------------------------------------- *)
 379 (* A related principle for real functions.                                   *)
 380 (* ------------------------------------------------------------------------- *)
 381
 382 (*** Not clear how useful this is
 383
 384 needs "Library/products.ml";;
 385
 386 let INCLUSION_EXCLUSION_REAL_FUNCTION = prove
 387  (`!f s:A->bool.
 388         FINITE s
 389         ==> product s (\x. &1 - f x) =
 390             sum {t | t SUBSET s} (\t. (-- &1) pow (CARD t) * product t f)`,
 391   let lemma = prove
 392    (`{t | ?u. u SUBSET s /\ t = x INSERT u} =
 393      IMAGE (\s. x INSERT s) {t | t SUBSET s}`,
 394     GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM; IN_IMAGE] THEN
 395     MESON_TAC[]) in
 396   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 397   SIMP_TAC[PRODUCT_CLAUSES; SUBSET_EMPTY; SUM_SING; CARD_CLAUSES; real_pow;
 398            SET_RULE `{x | x = a} = {a}`; REAL_MUL_RID] THEN
 399   REWRITE_TAC[SUBSET_INSERT_EXISTS] THEN
 400   MAP_EVERY X_GEN_TAC [`x:A`; `s:A->bool`] THEN STRIP_TAC THEN
 401   REWRITE_TAC[SET_RULE `{t | p t \/ q t} = {t | p t} UNION {t | q t}`] THEN
 402   W(MP_TAC o PART_MATCH (lhand o rand) SUM_UNION o rand o snd) THEN
 403   ANTS_TAC THENL
 404    [ASM_SIMP_TAC[FINITE_POWERSET; lemma; FINITE_IMAGE] THEN
 405     REWRITE_TAC[GSYM lemma] THEN ASM SET_TAC[];
 406     ALL_TAC] THEN
 407   DISCH_THEN SUBST1_TAC THEN
 408   REWRITE_TAC[GSYM SUM_LMUL; REAL_SUB_RDISTRIB; REAL_MUL_LID; real_sub] THEN
 409   AP_TERM_TAC THEN REWRITE_TAC[lemma] THEN
 410   W(MP_TAC o PART_MATCH (lhand o rand) SUM_IMAGE o rand o snd) THEN
 411   ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC] THEN
 412   REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_EQ THEN
 413   SIMP_TAC[o_THM; IN_ELIM_THM] THEN X_GEN_TAC `t:A->bool` THEN STRIP_TAC THEN
 414   SUBGOAL_THEN `FINITE(t:A->bool) /\ ~(x IN t)` STRIP_ASSUME_TAC THENL
 415    [ASM_MESON_TAC[SUBSET; FINITE_SUBSET]; ALL_TAC] THEN
 416   ASM_SIMP_TAC[PRODUCT_CLAUSES; CARD_CLAUSES; real_pow] THEN REAL_ARITH_TAC);;
 417
 418 ***)