iterate.ml

   1 (* ========================================================================= *)
   2 (* Generic iterated operations and special cases of sums over N and R.       *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2007                       *)
   5 (*              (c) Copyright, Lars Schewe 2007                              *)
   6 (* ========================================================================= *)
   7
   8 needs "sets.ml";;
   9
  10 prioritize_num();;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* A natural notation for segments of the naturals.                          *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 parse_as_infix("..",(15,"right"));;
  17
  18 let numseg = new_definition
  19   `m..n = {x:num | m <= x /\ x <= n}`;;
  20
  21 let FINITE_NUMSEG = prove
  22  (`!m n. FINITE(m..n)`,
  23   REPEAT GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
  24   EXISTS_TAC `{x:num | x <= n}` THEN REWRITE_TAC[FINITE_NUMSEG_LE] THEN
  25   SIMP_TAC[SUBSET; IN_ELIM_THM; numseg]);;
  26
  27 let NUMSEG_COMBINE_R = prove
  28  (`!m p n. m <= p + 1 /\ p <= n ==> ((m..p) UNION ((p+1)..n) = m..n)`,
  29   REWRITE_TAC[EXTENSION; IN_UNION; numseg; IN_ELIM_THM] THEN ARITH_TAC);;
  30
  31 let NUMSEG_COMBINE_L = prove
  32  (`!m p n. m <= p /\ p <= n + 1 ==> ((m..(p-1)) UNION (p..n) = m..n)`,
  33   REWRITE_TAC[EXTENSION; IN_UNION; numseg; IN_ELIM_THM] THEN ARITH_TAC);;
  34
  35 let NUMSEG_LREC = prove
  36  (`!m n. m <= n ==> (m INSERT ((m+1)..n) = m..n)`,
  37   REWRITE_TAC[EXTENSION; IN_INSERT; numseg; IN_ELIM_THM] THEN ARITH_TAC);;
  38
  39 let NUMSEG_RREC = prove
  40  (`!m n. m <= n ==> (n INSERT (m..(n-1)) = m..n)`,
  41   REWRITE_TAC[EXTENSION; IN_INSERT; numseg; IN_ELIM_THM] THEN ARITH_TAC);;
  42
  43 let NUMSEG_REC = prove
  44  (`!m n. m <= SUC n ==> (m..SUC n = (SUC n) INSERT (m..n))`,
  45   SIMP_TAC[GSYM NUMSEG_RREC; SUC_SUB1]);;
  46
  47 let IN_NUMSEG = prove
  48  (`!m n p. p IN (m..n) <=> m <= p /\ p <= n`,
  49   REWRITE_TAC[numseg; IN_ELIM_THM]);;
  50
  51 let IN_NUMSEG_0 = prove
  52  (`!m n. m IN (0..n) <=> m <= n`,
  53   REWRITE_TAC[IN_NUMSEG; LE_0]);;
  54
  55 let NUMSEG_SING = prove
  56  (`!n. n..n = {n}`,
  57   REWRITE_TAC[EXTENSION; IN_SING; IN_NUMSEG] THEN ARITH_TAC);;
  58
  59 let NUMSEG_EMPTY = prove
  60  (`!m n. (m..n = {}) <=> n < m`,
  61   REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_NUMSEG] THEN
  62   MESON_TAC[NOT_LE; LE_TRANS; LE_REFL]);;
  63
  64 let CARD_NUMSEG_LEMMA = prove
  65  (`!m d. CARD(m..(m+d)) = d + 1`,
  66   GEN_TAC THEN INDUCT_TAC THEN
  67   ASM_SIMP_TAC[ADD_CLAUSES; NUMSEG_REC; NUMSEG_SING; FINITE_RULES;
  68                ARITH_RULE `m <= SUC(m + d)`; CARD_CLAUSES; FINITE_NUMSEG;
  69                NOT_IN_EMPTY; ARITH; IN_NUMSEG; ARITH_RULE `~(SUC n <= n)`]);;
  70
  71 let CARD_NUMSEG = prove
  72  (`!m n. CARD(m..n) = (n + 1) - m`,
  73   REPEAT GEN_TAC THEN
  74   DISJ_CASES_THEN MP_TAC (ARITH_RULE `n:num < m \/ m <= n`) THENL
  75    [ASM_MESON_TAC[NUMSEG_EMPTY; CARD_CLAUSES;
  76                   ARITH_RULE `n < m ==> ((n + 1) - m = 0)`];
  77     SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; CARD_NUMSEG_LEMMA] THEN
  78     REPEAT STRIP_TAC THEN ARITH_TAC]);;
  79
  80 let HAS_SIZE_NUMSEG = prove
  81  (`!m n. (m..n) HAS_SIZE ((n + 1) - m)`,
  82   REWRITE_TAC[HAS_SIZE; FINITE_NUMSEG; CARD_NUMSEG]);;
  83
  84 let CARD_NUMSEG_1 = prove
  85  (`!n. CARD(1..n) = n`,
  86   REWRITE_TAC[CARD_NUMSEG] THEN ARITH_TAC);;
  87
  88 let HAS_SIZE_NUMSEG_1 = prove
  89  (`!n. (1..n) HAS_SIZE n`,
  90   REWRITE_TAC[CARD_NUMSEG; HAS_SIZE; FINITE_NUMSEG] THEN ARITH_TAC);;
  91
  92 let NUMSEG_CLAUSES = prove
  93  (`(!m. m..0 = if m = 0 then {0} else {}) /\
  94    (!m n. m..SUC n = if m <= SUC n then (SUC n) INSERT (m..n) else m..n)`,
  95   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
  96   GEN_REWRITE_TAC I [EXTENSION] THEN
  97   REWRITE_TAC[IN_NUMSEG; NOT_IN_EMPTY; IN_INSERT] THEN
  98   POP_ASSUM MP_TAC THEN ARITH_TAC);;
  99
 100 let FINITE_INDEX_NUMSEG = prove
 101  (`!s:A->bool.
 102         FINITE s =
 103         ?f. (!i j. i IN (1..CARD(s)) /\ j IN (1..CARD(s)) /\ (f i = f j)
 104                    ==> (i = j)) /\
 105             (s = IMAGE f (1..CARD(s)))`,
 106   GEN_TAC THEN EQ_TAC THENL
 107    [ALL_TAC; MESON_TAC[FINITE_NUMSEG; FINITE_IMAGE]] THEN
 108   DISCH_TAC THEN
 109   MP_TAC(ISPECL [`s:A->bool`; `CARD(s:A->bool)`] HAS_SIZE_INDEX) THEN
 110   ASM_REWRITE_TAC[HAS_SIZE] THEN
 111   DISCH_THEN(X_CHOOSE_THEN `f:num->A` STRIP_ASSUME_TAC) THEN
 112   EXISTS_TAC `\n. f(n - 1):A` THEN
 113   ASM_REWRITE_TAC[EXTENSION; IN_IMAGE; IN_NUMSEG] THEN
 114   CONJ_TAC THENL
 115    [REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= n <=> ~(i = 0) /\ i - 1 < n`] THEN
 116     ASM_MESON_TAC[ARITH_RULE
 117      `~(x = 0) /\ ~(y = 0) /\ (x - 1 = y - 1) ==> (x = y)`];
 118     ASM_MESON_TAC
 119      [ARITH_RULE `m < C ==> (m = (m + 1) - 1) /\ 1 <= m + 1 /\ m + 1 <= C`;
 120       ARITH_RULE `1 <= i /\ i <= n <=> ~(i = 0) /\ i - 1 < n`]]);;
 121
 122 let FINITE_INDEX_NUMBERS = prove
 123  (`!s:A->bool.
 124         FINITE s =
 125          ?k:num->bool f. (!i j. i IN k /\ j IN k /\ (f i = f j) ==> (i = j)) /\
 126                          FINITE k /\ (s = IMAGE f k)`,
 127   MESON_TAC[FINITE_INDEX_NUMSEG; FINITE_NUMSEG; FINITE_IMAGE]);;
 128
 129 let DISJOINT_NUMSEG = prove
 130  (`!m n p q. DISJOINT (m..n) (p..q) <=> n < p \/ q < m \/ n < m \/ q < p`,
 131   REWRITE_TAC[DISJOINT; IN_NUMSEG; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
 132   REPEAT GEN_TAC THEN REWRITE_TAC[DE_MORGAN_THM; NOT_LE] THEN
 133   EQ_TAC THENL [MESON_TAC[LT_ANTISYM]; ARITH_TAC]);;
 134
 135 let NUMSEG_ADD_SPLIT = prove
 136  (`!m n p. m <= n + 1 ==> (m..(n+p) = (m..n) UNION (n+1..n+p))`,
 137   REWRITE_TAC[EXTENSION; IN_UNION; IN_NUMSEG] THEN ARITH_TAC);;
 138
 139 let NUMSEG_OFFSET_IMAGE = prove
 140  (`!m n p. (m+p..n+p) = IMAGE (\i. i + p) (m..n)`,
 141   REWRITE_TAC[EXTENSION; IN_IMAGE; IN_NUMSEG] THEN
 142   REPEAT GEN_TAC THEN EQ_TAC THENL
 143    [DISCH_THEN(fun th -> EXISTS_TAC `x - p:num` THEN MP_TAC th); ALL_TAC] THEN
 144   ARITH_TAC);;
 145
 146 let SUBSET_NUMSEG = prove
 147  (`!m n p q. (m..n) SUBSET (p..q) <=> n < m \/ p <= m /\ n <= q`,
 148   REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET; IN_NUMSEG] THEN
 149   EQ_TAC THENL [MESON_TAC[LE_TRANS; NOT_LE; LE_REFL]; ARITH_TAC]);;
 150
 151 (* ------------------------------------------------------------------------- *)
 152 (* Equivalence with the more ad-hoc comprehension notation.                  *)
 153 (* ------------------------------------------------------------------------- *)
 154
 155 let NUMSEG_LE = prove
 156  (`!n. {x | x <= n} = 0..n`,
 157   REWRITE_TAC[EXTENSION; IN_NUMSEG; IN_ELIM_THM] THEN ARITH_TAC);;
 158
 159 let NUMSEG_LT = prove
 160  (`!n. {x | x < n} = if n = 0 then {} else 0..(n-1)`,
 161   GEN_TAC THEN COND_CASES_TAC THEN
 162   REWRITE_TAC[EXTENSION; IN_NUMSEG; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 163   ASM_ARITH_TAC);;
 164
 165 (* ------------------------------------------------------------------------- *)
 166 (* Conversion to evaluate m..n for specific numerals.                        *)
 167 (* ------------------------------------------------------------------------- *)
 168
 169 let NUMSEG_CONV =
 170   let pth_0 = MESON[NUMSEG_EMPTY] `n < m ==> m..n = {}`
 171   and pth_1 = MESON[NUMSEG_SING] `m..m = {m}`
 172   and pth_2 = MESON[NUMSEG_LREC; ADD1] `m <= n ==> m..n = m INSERT (SUC m..n)`
 173   and ns_tm = `(..)` and m_tm = `m:num` and n_tm = `n:num` in
 174   let rec NUMSEG_CONV tm =
 175     let nstm,nt = dest_comb tm in
 176     let nst,mt = dest_comb nstm in
 177     if nst <> ns_tm then failwith "NUMSEG_CONV" else
 178     let m = dest_numeral mt and n = dest_numeral nt in
 179     if n </ m then MP_CONV NUM_LT_CONV (INST [mt,m_tm; nt,n_tm] pth_0)
 180     else if n =/ m then INST [mt,m_tm] pth_1
 181     else let th = MP_CONV NUM_LE_CONV (INST [mt,m_tm; nt,n_tm] pth_2) in
 182          CONV_RULE(funpow 2 RAND_CONV
 183           (LAND_CONV NUM_SUC_CONV THENC NUMSEG_CONV)) th in
 184   NUMSEG_CONV;;
 185
 186 (* ------------------------------------------------------------------------- *)
 187 (* Topological sorting of a finite set.                                      *)
 188 (* ------------------------------------------------------------------------- *)
 189
 190 let TOPOLOGICAL_SORT = prove
 191  (`!(<<). (!x y:A. x << y /\ y << x ==> x = y) /\
 192           (!x y z. x << y /\ y << z ==> x << z)
 193           ==> !n s. s HAS_SIZE n
 194                     ==> ?f. s = IMAGE f (1..n) /\
 195                             (!j k. j IN 1..n /\ k IN 1..n /\ j < k
 196                                    ==> ~(f k << f j))`,
 197   GEN_TAC THEN DISCH_TAC THEN
 198   SUBGOAL_THEN `!n s. s HAS_SIZE n /\ ~(s = {})
 199                       ==> ?a:A. a IN s /\ !b. b IN (s DELETE a) ==> ~(b << a)`
 200   ASSUME_TAC THENL
 201    [INDUCT_TAC THEN
 202     REWRITE_TAC[HAS_SIZE_0; HAS_SIZE_SUC; TAUT `~(a /\ ~a)`] THEN
 203     X_GEN_TAC `s:A->bool` THEN STRIP_TAC THEN
 204     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
 205     DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
 206     FIRST_X_ASSUM(MP_TAC o SPEC `a:A`) THEN ASM_REWRITE_TAC[] THEN
 207     DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (a:A)`) THEN
 208     ASM_SIMP_TAC[SET_RULE `a IN s ==> (s DELETE a = {} <=> s = {a})`] THEN
 209     ASM_CASES_TAC `s = {a:A}` THEN ASM_REWRITE_TAC[] THENL
 210      [EXISTS_TAC `a:A` THEN SET_TAC[]; ALL_TAC] THEN
 211     DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
 212     ASM_CASES_TAC `((a:A) << (b:A)) :bool` THENL
 213      [EXISTS_TAC `a:A`; EXISTS_TAC `b:A`] THEN ASM SET_TAC[];
 214     ALL_TAC] THEN
 215   INDUCT_TAC THENL
 216    [SIMP_TAC[HAS_SIZE_0; NUMSEG_CLAUSES; ARITH; IMAGE_CLAUSES; NOT_IN_EMPTY];
 217     ALL_TAC] THEN
 218   REWRITE_TAC[HAS_SIZE_SUC] THEN X_GEN_TAC `s:A->bool` THEN STRIP_TAC THEN
 219   FIRST_X_ASSUM(MP_TAC o SPECL [`SUC n`; `s:A->bool`]) THEN
 220   ASM_REWRITE_TAC[HAS_SIZE_SUC] THEN
 221   DISCH_THEN(X_CHOOSE_THEN `a:A` MP_TAC) THEN STRIP_TAC THEN
 222   FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (a:A)`) THEN ASM_SIMP_TAC[] THEN
 223   DISCH_THEN(X_CHOOSE_THEN `f:num->A` STRIP_ASSUME_TAC) THEN
 224   EXISTS_TAC `\k. if k = 1 then a:A else f(k - 1)` THEN
 225   SIMP_TAC[ARITH_RULE `1 <= k ==> ~(SUC k = 1)`; SUC_SUB1] THEN
 226   SUBGOAL_THEN `!i. i IN 1..SUC n <=> i = 1 \/ 1 < i /\ (i - 1) IN 1..n`
 227    (fun th -> REWRITE_TAC[EXTENSION; IN_IMAGE; th])
 228   THENL [REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC] THEN CONJ_TAC THENL
 229    [X_GEN_TAC `b:A` THEN ASM_CASES_TAC `b:A = a` THENL
 230      [ASM_MESON_TAC[]; ALL_TAC] THEN
 231     FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP
 232      (SET_RULE `~(b = a) ==> (b IN s <=> b IN (s DELETE a))`) th]) THEN
 233     ONCE_REWRITE_TAC[COND_RAND] THEN
 234     ASM_REWRITE_TAC[IN_IMAGE; IN_NUMSEG] THEN
 235     EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 236     DISCH_THEN(X_CHOOSE_TAC `i:num`) THEN EXISTS_TAC `i + 1` THEN
 237     ASM_SIMP_TAC[ARITH_RULE `1 <= x ==> 1 < x + 1 /\ ~(x + 1 = 1)`; ADD_SUB];
 238     MAP_EVERY X_GEN_TAC [`j:num`; `k:num`] THEN
 239     MAP_EVERY ASM_CASES_TAC [`j = 1`; `k = 1`] THEN
 240     ASM_REWRITE_TAC[LT_REFL] THENL
 241      [STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[];
 242       ARITH_TAC;
 243       STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 244       ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]]);;
 245
 246 (* ------------------------------------------------------------------------- *)
 247 (* Analogous finiteness theorem for segments of integers.                    *)
 248 (* ------------------------------------------------------------------------- *)
 249
 250 let FINITE_INTSEG = prove
 251  (`(!l r. FINITE {x:int | l <= x /\ x <= r}) /\
 252    (!l r. FINITE {x:int | l <= x /\ x < r}) /\
 253    (!l r. FINITE {x:int | l < x /\ x <= r}) /\
 254    (!l r. FINITE {x:int | l < x /\ x < r})`,
 255   MATCH_MP_TAC(TAUT `(a ==> b) /\ a ==> a /\ b`) THEN CONJ_TAC THENL
 256    [DISCH_TAC THEN REPEAT CONJ_TAC THEN POP_ASSUM MP_TAC THEN
 257     REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 258     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET) THEN
 259     REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN INT_ARITH_TAC;
 260     REPEAT GEN_TAC THEN ASM_CASES_TAC `&0:int <= r - l` THEN
 261     ASM_SIMP_TAC[INT_ARITH `~(&0 <= r - l:int) ==> ~(l <= x /\ x <= r)`] THEN
 262     ASM_SIMP_TAC[EMPTY_GSPEC; FINITE_EMPTY] THEN
 263     MATCH_MP_TAC FINITE_SUBSET THEN
 264     EXISTS_TAC `IMAGE (\n. l + &n) (0..num_of_int(r - l))` THEN
 265     ASM_SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG] THEN
 266     REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
 267     REWRITE_TAC[GSYM INT_OF_NUM_LE; IN_NUMSEG] THEN
 268     X_GEN_TAC `x:int` THEN STRIP_TAC THEN EXISTS_TAC `num_of_int(x - l)` THEN
 269     ASM_SIMP_TAC[INT_OF_NUM_OF_INT; INT_SUB_LE] THEN ASM_INT_ARITH_TAC]);;
 270
 271 (* ------------------------------------------------------------------------- *)
 272 (* Generic iteration of operation over set with finite support.              *)
 273 (* ------------------------------------------------------------------------- *)
 274
 275 let neutral = new_definition
 276   `neutral op = @x. !y. (op x y = y) /\ (op y x = y)`;;
 277
 278 let monoidal = new_definition
 279   `monoidal op <=> (!x y. op x y = op y x) /\
 280                    (!x y z. op x (op y z) = op (op x y) z) /\
 281                    (!x:A. op (neutral op) x = x)`;;
 282
 283 let MONOIDAL_AC = prove
 284  (`!op. monoidal op
 285         ==> (!a. op (neutral op) a = a) /\
 286             (!a. op a (neutral op) = a) /\
 287             (!a b. op a b = op b a) /\
 288             (!a b c. op (op a b) c = op a (op b c)) /\
 289             (!a b c. op a (op b c) = op b (op a c))`,
 290   REWRITE_TAC[monoidal] THEN MESON_TAC[]);;
 291
 292 let support = new_definition
 293   `support op (f:A->B) s = {x | x IN s /\ ~(f x = neutral op)}`;;
 294
 295 let iterate = new_definition
 296   `iterate op (s:A->bool) f =
 297         if FINITE(support op f s)
 298         then ITSET (\x a. op (f x) a) (support op f s) (neutral op)
 299         else neutral op`;;
 300
 301 let IN_SUPPORT = prove
 302  (`!op f x s. x IN (support op f s) <=> x IN s /\ ~(f x = neutral op)`,
 303   REWRITE_TAC[support; IN_ELIM_THM]);;
 304
 305 let SUPPORT_SUPPORT = prove
 306  (`!op f s. support op f (support op f s) = support op f s`,
 307   REWRITE_TAC[support; IN_ELIM_THM; EXTENSION] THEN REWRITE_TAC[CONJ_ACI]);;
 308
 309 let SUPPORT_EMPTY = prove
 310  (`!op f s. (!x. x IN s ==> (f(x) = neutral op)) <=> (support op f s = {})`,
 311   REWRITE_TAC[IN_SUPPORT; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 312   MESON_TAC[]);;
 313
 314 let SUPPORT_SUBSET = prove
 315  (`!op f s. (support op f s) SUBSET s`,
 316   SIMP_TAC[SUBSET; IN_SUPPORT]);;
 317
 318 let FINITE_SUPPORT = prove
 319  (`!op f s. FINITE s ==> FINITE(support op f s)`,
 320   MESON_TAC[SUPPORT_SUBSET; FINITE_SUBSET]);;
 321
 322 let SUPPORT_CLAUSES = prove
 323  (`(!f. support op f {} = {}) /\
 324    (!f x s. support op f (x INSERT s) =
 325        if f(x) = neutral op then support op f s
 326        else x INSERT (support op f s)) /\
 327    (!f x s. support op f (s DELETE x) = (support op f s) DELETE x) /\
 328    (!f s t. support op f (s UNION t) =
 329                     (support op f s) UNION (support op f t)) /\
 330    (!f s t. support op f (s INTER t) =
 331                     (support op f s) INTER (support op f t)) /\
 332    (!f s t. support op f (s DIFF t) =
 333                     (support op f s) DIFF (support op f t)) /\
 334    (!f g s.  support op g (IMAGE f s) = IMAGE f (support op (g o f) s))`,
 335   REWRITE_TAC[support; EXTENSION; IN_ELIM_THM; IN_INSERT; IN_DELETE; o_THM;
 336     IN_IMAGE; NOT_IN_EMPTY; IN_UNION; IN_INTER; IN_DIFF; COND_RAND] THEN
 337   REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN ASM_MESON_TAC[]);;
 338
 339 let SUPPORT_DELTA = prove
 340  (`!op s f a. support op (\x. if x = a then f(x) else neutral op) s =
 341               if a IN s then support op f {a} else {}`,
 342   REWRITE_TAC[EXTENSION; support; IN_ELIM_THM; IN_SING] THEN
 343   REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN
 344   ASM_REWRITE_TAC[IN_ELIM_THM; NOT_IN_EMPTY]);;
 345
 346 let FINITE_SUPPORT_DELTA = prove
 347  (`!op f a. FINITE(support op (\x. if x = a then f(x) else neutral op) s)`,
 348   REWRITE_TAC[SUPPORT_DELTA] THEN REPEAT GEN_TAC THEN
 349   COND_CASES_TAC THEN SIMP_TAC[FINITE_RULES; FINITE_SUPPORT]);;
 350
 351 (* ------------------------------------------------------------------------- *)
 352 (* Key lemmas about the generic notion.                                      *)
 353 (* ------------------------------------------------------------------------- *)
 354
 355 let ITERATE_SUPPORT = prove
 356  (`!op f s. iterate op (support op f s) f = iterate op s f`,
 357   SIMP_TAC[iterate; SUPPORT_SUPPORT]);;
 358
 359 let ITERATE_EXPAND_CASES = prove
 360  (`!op f s. iterate op s f =
 361               if FINITE(support op f s) then iterate op (support op f s) f
 362               else neutral op`,
 363   SIMP_TAC[iterate; SUPPORT_SUPPORT]);;
 364
 365 let ITERATE_CLAUSES_GEN = prove
 366  (`!op. monoidal op
 367         ==> (!(f:A->B). iterate op {} f = neutral op) /\
 368             (!f x s. monoidal op /\ FINITE(support op (f:A->B) s)
 369                      ==> (iterate op (x INSERT s) f =
 370                                 if x IN s then iterate op s f
 371                                 else op (f x) (iterate op s f)))`,
 372   GEN_TAC THEN STRIP_TAC THEN
 373   ONCE_REWRITE_TAC[AND_FORALL_THM] THEN GEN_TAC THEN
 374   MP_TAC(ISPECL [`\x a. (op:B->B->B) ((f:A->B)(x)) a`; `neutral op :B`]
 375    FINITE_RECURSION) THEN
 376   ANTS_TAC THENL [ASM_MESON_TAC[monoidal]; ALL_TAC] THEN
 377   REPEAT STRIP_TAC THEN
 378   ASM_REWRITE_TAC[iterate; SUPPORT_CLAUSES; FINITE_RULES] THEN
 379   GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [COND_RAND] THEN
 380   ASM_REWRITE_TAC[SUPPORT_CLAUSES; FINITE_INSERT; COND_ID] THEN
 381   ASM_CASES_TAC `(f:A->B) x = neutral op` THEN
 382   ASM_SIMP_TAC[IN_SUPPORT] THEN COND_CASES_TAC THEN ASM_MESON_TAC[monoidal]);;
 383
 384 let ITERATE_CLAUSES = prove
 385  (`!op. monoidal op
 386         ==> (!f. iterate op {} f = neutral op) /\
 387             (!f x s. FINITE(s)
 388                      ==> (iterate op (x INSERT s) f =
 389                           if x IN s then iterate op s f
 390                           else op (f x) (iterate op s f)))`,
 391   SIMP_TAC[ITERATE_CLAUSES_GEN; FINITE_SUPPORT]);;
 392
 393 let ITERATE_UNION = prove
 394  (`!op. monoidal op
 395         ==> !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
 396                     ==> (iterate op (s UNION t) f =
 397                          op (iterate op s f) (iterate op t f))`,
 398   let lemma = prove
 399    (`(s UNION (x INSERT t) = x INSERT (s UNION t)) /\
 400      (DISJOINT s (x INSERT t) <=> ~(x IN s) /\ DISJOINT s t)`,
 401     SET_TAC[]) in
 402   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
 403   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REPEAT DISCH_TAC THEN
 404   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 405   ASM_SIMP_TAC[ITERATE_CLAUSES; IN_UNION; UNION_EMPTY; REAL_ADD_RID; lemma;
 406                FINITE_UNION] THEN
 407   ASM_MESON_TAC[monoidal]);;
 408
 409 let ITERATE_UNION_GEN = prove
 410  (`!op. monoidal op
 411         ==> !(f:A->B) s t. FINITE(support op f s) /\ FINITE(support op f t) /\
 412                            DISJOINT (support op f s) (support op f t)
 413                            ==> (iterate op (s UNION t) f =
 414                                 op (iterate op s f) (iterate op t f))`,
 415   ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
 416   SIMP_TAC[SUPPORT_CLAUSES; ITERATE_UNION]);;
 417
 418 let ITERATE_DIFF = prove
 419  (`!op. monoidal op
 420         ==> !f s t. FINITE s /\ t SUBSET s
 421                     ==> (op (iterate op (s DIFF t) f) (iterate op t f) =
 422                          iterate op s f)`,
 423   let lemma = prove
 424    (`t SUBSET s ==> (s = (s DIFF t) UNION t) /\ DISJOINT (s DIFF t) t`,
 425     SET_TAC[]) in
 426   MESON_TAC[lemma; ITERATE_UNION; FINITE_UNION; FINITE_SUBSET; SUBSET_DIFF]);;
 427
 428 let ITERATE_DIFF_GEN = prove
 429  (`!op. monoidal op
 430         ==> !f:A->B s t. FINITE (support op f s) /\
 431                          (support op f t) SUBSET (support op f s)
 432                          ==> (op (iterate op (s DIFF t) f) (iterate op t f) =
 433                               iterate op s f)`,
 434   ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
 435   SIMP_TAC[SUPPORT_CLAUSES; ITERATE_DIFF]);;
 436
 437 let ITERATE_INCL_EXCL = prove
 438  (`!op. monoidal op
 439         ==> !s t f. FINITE s /\ FINITE t
 440                     ==> op (iterate op s f) (iterate op t f) =
 441                         op (iterate op (s UNION t) f)
 442                            (iterate op (s INTER t) f)`,
 443   REPEAT STRIP_TAC THEN
 444   ONCE_REWRITE_TAC[SET_RULE
 445     `a UNION b = ((a DIFF b) UNION (b DIFF a)) UNION (a INTER b)`] THEN
 446   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)
 447     [SET_RULE `s:A->bool = s DIFF t UNION s INTER t`] THEN
 448   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)
 449     [SET_RULE `t:A->bool = t DIFF s UNION s INTER t`] THEN
 450   ASM_SIMP_TAC[ITERATE_UNION; FINITE_UNION; FINITE_DIFF; FINITE_INTER;
 451     SET_RULE `DISJOINT (s DIFF s' UNION s' DIFF s) (s INTER s')`;
 452     SET_RULE `DISJOINT (s DIFF s') (s' DIFF s)`;
 453     SET_RULE `DISJOINT (s DIFF s') (s' INTER s)`;
 454     SET_RULE `DISJOINT (s DIFF s') (s INTER s')`] THEN
 455   FIRST_X_ASSUM(fun th -> REWRITE_TAC[MATCH_MP MONOIDAL_AC th]));;
 456
 457 let ITERATE_CLOSED = prove
 458  (`!op. monoidal op
 459         ==> !P. P(neutral op) /\ (!x y. P x /\ P y ==> P (op x y))
 460                 ==> !f:A->B s. (!x. x IN s /\ ~(f x = neutral op) ==> P(f x))
 461                                ==> P(iterate op s f)`,
 462   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
 463   REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM IN_SUPPORT] THEN
 464   COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN POP_ASSUM MP_TAC THEN
 465   SPEC_TAC(`support op (f:A->B) s`,`s:A->bool`) THEN
 466   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 467   ASM_SIMP_TAC[ITERATE_CLAUSES; FINITE_INSERT; IN_INSERT]);;
 468
 469 let ITERATE_RELATED = prove
 470  (`!op. monoidal op
 471         ==> !R. R (neutral op) (neutral op) /\
 472                 (!x1 y1 x2 y2. R x1 x2 /\ R y1 y2 ==> R (op x1 y1) (op x2 y2))
 473                 ==> !f:A->B g s.
 474                       FINITE s /\
 475                       (!x. x IN s ==> R (f x) (g x))
 476                       ==> R (iterate op s f) (iterate op s g)`,
 477   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
 478   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 479   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 480   ASM_SIMP_TAC[ITERATE_CLAUSES; FINITE_INSERT; IN_INSERT]);;
 481
 482 let ITERATE_EQ_NEUTRAL = prove
 483  (`!op. monoidal op
 484         ==> !f:A->B s. (!x. x IN s ==> (f(x) = neutral op))
 485                        ==> (iterate op s f = neutral op)`,
 486   REPEAT STRIP_TAC THEN
 487   SUBGOAL_THEN `support op (f:A->B) s = {}` ASSUME_TAC THENL
 488    [ASM_MESON_TAC[EXTENSION; NOT_IN_EMPTY; IN_SUPPORT];
 489     ASM_MESON_TAC[ITERATE_CLAUSES; FINITE_RULES; ITERATE_SUPPORT]]);;
 490
 491 let ITERATE_SING = prove
 492  (`!op. monoidal op ==> !f:A->B x. (iterate op {x} f = f x)`,
 493   SIMP_TAC[ITERATE_CLAUSES; FINITE_RULES; NOT_IN_EMPTY] THEN
 494   MESON_TAC[monoidal]);;
 495
 496 let ITERATE_DELETE = prove
 497  (`!op. monoidal op
 498         ==> !f:A->B s a. FINITE s /\ a IN s
 499                          ==> op (f a) (iterate op (s DELETE a) f) =
 500                              iterate op s f`,
 501   MESON_TAC[ITERATE_CLAUSES; FINITE_DELETE; IN_DELETE; INSERT_DELETE]);;
 502
 503 let ITERATE_DELTA = prove
 504  (`!op. monoidal op
 505         ==> !f a s. iterate op s (\x. if x = a then f(x) else neutral op) =
 506                     if a IN s then f(a) else neutral op`,
 507   GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
 508   REWRITE_TAC[SUPPORT_DELTA] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 509   ASM_SIMP_TAC[ITERATE_CLAUSES] THEN REWRITE_TAC[SUPPORT_CLAUSES] THEN
 510   COND_CASES_TAC THEN ASM_SIMP_TAC[ITERATE_CLAUSES; ITERATE_SING]);;
 511
 512 let ITERATE_IMAGE = prove
 513  (`!op. monoidal op
 514        ==> !f:A->B g:B->C s.
 515                 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
 516                 ==> (iterate op (IMAGE f s) g = iterate op s (g o f))`,
 517   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
 518   SUBGOAL_THEN
 519    `!s. FINITE s /\
 520         (!x y:A. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
 521         ==> (iterate op (IMAGE f s) (g:B->C) = iterate op s (g o f))`
 522   ASSUME_TAC THENL
 523    [REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 524     ASM_SIMP_TAC[ITERATE_CLAUSES; IMAGE_CLAUSES; FINITE_IMAGE] THEN
 525     REWRITE_TAC[o_THM; IN_INSERT] THEN ASM_MESON_TAC[IN_IMAGE];
 526     GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
 527     REPEAT STRIP_TAC THEN MATCH_MP_TAC(TAUT
 528      `(a <=> a') /\ (a' ==> (b = b'))
 529       ==> (if a then b else c) = (if a' then b' else c)`) THEN
 530     REWRITE_TAC[SUPPORT_CLAUSES] THEN REPEAT STRIP_TAC THENL
 531      [MATCH_MP_TAC FINITE_IMAGE_INJ_EQ THEN ASM_MESON_TAC[IN_SUPPORT];
 532       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[IN_SUPPORT]]]);;
 533
 534 let ITERATE_BIJECTION = prove
 535  (`!op. monoidal op
 536         ==>  !f:A->B p s.
 537                 (!x. x IN s ==> p(x) IN s) /\
 538                 (!y. y IN s ==> ?!x. x IN s /\ p(x) = y)
 539                 ==> iterate op s f = iterate op s (f o p)`,
 540   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 541   EXISTS_TAC `iterate op (IMAGE (p:A->A) s) (f:A->B)` THEN CONJ_TAC THENL
 542    [AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_IMAGE];
 543     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
 544       (INST_TYPE [aty,bty] ITERATE_IMAGE))] THEN
 545   ASM_MESON_TAC[]);;
 546
 547 let ITERATE_ITERATE_PRODUCT = prove
 548  (`!op. monoidal op
 549         ==> !s:A->bool t:A->B->bool x:A->B->C.
 550                 FINITE s /\ (!i. i IN s ==> FINITE(t i))
 551                 ==> iterate op s (\i. iterate op (t i) (x i)) =
 552                     iterate op {i,j | i IN s /\ j IN t i} (\(i,j). x i j)`,
 553   GEN_TAC THEN DISCH_TAC THEN
 554   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 555   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 556   ASM_SIMP_TAC[NOT_IN_EMPTY; SET_RULE `{a,b | F} = {}`; ITERATE_CLAUSES] THEN
 557   REWRITE_TAC[SET_RULE `{i,j | i IN a INSERT s /\ j IN t i} =
 558             IMAGE (\j. a,j) (t a) UNION {i,j | i IN s /\ j IN t i}`] THEN
 559   ASM_SIMP_TAC[FINITE_INSERT; ITERATE_CLAUSES; IN_INSERT] THEN
 560   REPEAT STRIP_TAC THEN
 561   FIRST_ASSUM(fun th ->
 562    W(MP_TAC o PART_MATCH (lhand o rand) (MATCH_MP ITERATE_UNION th) o
 563    rand o snd)) THEN
 564   ANTS_TAC THENL
 565    [ASM_SIMP_TAC[FINITE_IMAGE; FINITE_PRODUCT_DEPENDENT; IN_INSERT] THEN
 566     REWRITE_TAC[DISJOINT; EXTENSION; IN_IMAGE; IN_INTER; NOT_IN_EMPTY;
 567                 IN_ELIM_THM; EXISTS_PAIR_THM; FORALL_PAIR_THM; PAIR_EQ] THEN
 568     ASM_MESON_TAC[];
 569     ALL_TAC] THEN
 570   DISCH_THEN SUBST1_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 571   FIRST_ASSUM(fun th ->
 572    W(MP_TAC o PART_MATCH (lhand o rand) (MATCH_MP ITERATE_IMAGE th) o
 573    rand o snd)) THEN
 574   ANTS_TAC THENL
 575    [SIMP_TAC[FORALL_PAIR_THM] THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 576     ASM_SIMP_TAC[PAIR_EQ];
 577     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
 578     CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[ETA_AX]]);;
 579
 580 let ITERATE_EQ = prove
 581  (`!op. monoidal op
 582         ==> !f:A->B g s.
 583               (!x. x IN s ==> f x = g x) ==> iterate op s f = iterate op s g`,
 584   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
 585   SUBGOAL_THEN `support op g s = support op (f:A->B) s` SUBST1_TAC THENL
 586    [REWRITE_TAC[EXTENSION; IN_SUPPORT] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
 587   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 588   SUBGOAL_THEN
 589    `FINITE(support op (f:A->B) s) /\
 590     (!x. x IN (support op f s) ==> f x = g x)`
 591   MP_TAC THENL [ASM_MESON_TAC[IN_SUPPORT]; REWRITE_TAC[IMP_CONJ]] THEN
 592   SPEC_TAC(`support op (f:A->B) s`,`t:A->bool`) THEN
 593   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN ASM_SIMP_TAC[ITERATE_CLAUSES] THEN
 594   MESON_TAC[IN_INSERT]);;
 595
 596 let ITERATE_EQ_GENERAL = prove
 597  (`!op. monoidal op
 598         ==> !s:A->bool t:B->bool f:A->C g h.
 599                 (!y. y IN t ==> ?!x. x IN s /\ h(x) = y) /\
 600                 (!x. x IN s ==> h(x) IN t /\ g(h x) = f x)
 601                 ==> iterate op s f = iterate op t g`,
 602   REPEAT STRIP_TAC THEN
 603   SUBGOAL_THEN `t = IMAGE (h:A->B) s` SUBST1_TAC THENL
 604    [REWRITE_TAC[EXTENSION; IN_IMAGE] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
 605   MATCH_MP_TAC EQ_TRANS THEN
 606   EXISTS_TAC `iterate op s ((g:B->C) o (h:A->B))` THEN CONJ_TAC THENL
 607    [ASM_MESON_TAC[ITERATE_EQ; o_THM];
 608     CONV_TAC SYM_CONV THEN
 609     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_IMAGE) THEN
 610     ASM_MESON_TAC[]]);;
 611
 612 let ITERATE_EQ_GENERAL_INVERSES = prove
 613  (`!op. monoidal op
 614         ==> !s:A->bool t:B->bool f:A->C g h k.
 615                 (!y. y IN t ==> k(y) IN s /\ h(k y) = y) /\
 616                 (!x. x IN s ==> h(x) IN t /\ k(h x) = x /\ g(h x) = f x)
 617                 ==> iterate op s f = iterate op t g`,
 618   REPEAT STRIP_TAC THEN
 619   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_EQ_GENERAL) THEN
 620   EXISTS_TAC `h:A->B` THEN ASM_MESON_TAC[]);;
 621
 622 let ITERATE_INJECTION = prove
 623  (`!op. monoidal op
 624           ==> !f:A->B p:A->A s.
 625                       FINITE s /\
 626                       (!x. x IN s ==> p x IN s) /\
 627                       (!x y. x IN s /\ y IN s /\ p x = p y ==> x = y)
 628                       ==> iterate op s (f o p) = iterate op s f`,
 629   REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
 630   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_BIJECTION) THEN
 631   MP_TAC(ISPECL [`s:A->bool`; `p:A->A`] SURJECTIVE_IFF_INJECTIVE) THEN
 632   ASM_REWRITE_TAC[SUBSET; IN_IMAGE] THEN ASM_MESON_TAC[]);;
 633
 634 let ITERATE_UNION_NONZERO = prove
 635  (`!op. monoidal op
 636         ==> !f:A->B s t.
 637                 FINITE(s) /\ FINITE(t) /\
 638                 (!x. x IN (s INTER t) ==> f x = neutral(op))
 639                 ==> iterate op (s UNION t) f =
 640                     op (iterate op s f) (iterate op t f)`,
 641   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
 642   REWRITE_TAC[SUPPORT_CLAUSES] THEN
 643   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_UNION) THEN
 644   ASM_SIMP_TAC[FINITE_SUPPORT; DISJOINT; IN_INTER; IN_SUPPORT; EXTENSION] THEN
 645   ASM_MESON_TAC[IN_INTER; NOT_IN_EMPTY]);;
 646
 647 let ITERATE_OP = prove
 648  (`!op. monoidal op
 649         ==> !f g s. FINITE s
 650                     ==> iterate op s (\x. op (f x) (g x)) =
 651                         op (iterate op s f) (iterate op s g)`,
 652   GEN_TAC THEN DISCH_TAC THEN
 653   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 654   ASM_SIMP_TAC[ITERATE_CLAUSES; MONOIDAL_AC]);;
 655
 656 let ITERATE_SUPERSET = prove
 657  (`!op. monoidal op
 658         ==> !f:A->B u v.
 659             u SUBSET v /\
 660             (!x. x IN v /\ ~(x IN u) ==> f(x) = neutral op)
 661             ==> iterate op v f = iterate op u f`,
 662   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
 663   AP_THM_TAC THEN AP_TERM_TAC THEN
 664   REWRITE_TAC[support; EXTENSION; IN_ELIM_THM] THEN ASM_MESON_TAC[SUBSET]);;
 665
 666 let ITERATE_IMAGE_NONZERO = prove
 667  (`!op. monoidal op
 668         ==> !g:B->C f:A->B s.
 669                     FINITE s /\
 670                     (!x y. x IN s /\ y IN s /\ ~(x = y) /\ f x = f y
 671                            ==> g(f x) = neutral op)
 672                     ==> iterate op (IMAGE f s) g = iterate op s (g o f)`,
 673   GEN_TAC THEN DISCH_TAC THEN
 674   GEN_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN
 675   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 676   ASM_SIMP_TAC[IMAGE_CLAUSES; ITERATE_CLAUSES; FINITE_IMAGE] THEN
 677   MAP_EVERY X_GEN_TAC [`a:A`; `s:A->bool`] THEN
 678   REWRITE_TAC[IN_INSERT] THEN REPEAT STRIP_TAC THEN
 679   SUBGOAL_THEN `iterate op s ((g:B->C) o (f:A->B)) = iterate op (IMAGE f s) g`
 680   SUBST1_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 681   REWRITE_TAC[IN_IMAGE] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[o_THM] THEN
 682   SUBGOAL_THEN `(g:B->C) ((f:A->B) a) = neutral op` SUBST1_TAC THEN
 683   ASM_MESON_TAC[MONOIDAL_AC]);;
 684
 685 let ITERATE_CASES = prove
 686  (`!op. monoidal op
 687         ==> !s P f g:A->B.
 688                 FINITE s
 689                 ==> iterate op s (\x. if P x then f x else g x) =
 690                     op (iterate op {x | x IN s /\ P x} f)
 691                        (iterate op {x | x IN s /\ ~P x} g)`,
 692   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 693   EXISTS_TAC
 694    `op (iterate op {x | x IN s /\ P x} (\x. if P x then f x else (g:A->B) x))
 695        (iterate op {x | x IN s /\ ~P x} (\x. if P x then f x else g x))` THEN
 696   CONJ_TAC THENL
 697    [FIRST_ASSUM(fun th -> ASM_SIMP_TAC[GSYM(MATCH_MP ITERATE_UNION th);
 698       FINITE_RESTRICT;
 699       SET_RULE `DISJOINT {x | x IN s /\ P x} {x | x IN s /\ ~P x}`]) THEN
 700     AP_THM_TAC THEN AP_TERM_TAC THEN SET_TAC[];
 701     BINOP_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_EQ) THEN
 702     SIMP_TAC[IN_ELIM_THM]]);;
 703
 704 let ITERATE_OP_GEN = prove
 705  (`!op. monoidal op
 706         ==> !f g:A->B s.
 707                 FINITE(support op f s) /\ FINITE(support op g s)
 708                 ==> iterate op s (\x. op (f x) (g x)) =
 709                     op (iterate op s f) (iterate op s g)`,
 710   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
 711   MATCH_MP_TAC EQ_TRANS THEN
 712   EXISTS_TAC `iterate op (support op f s UNION support op g s)
 713                          (\x. op ((f:A->B) x) (g x))` THEN
 714   CONJ_TAC THENL
 715    [CONV_TAC SYM_CONV;
 716     ASM_SIMP_TAC[ITERATE_OP; FINITE_UNION] THEN BINOP_TAC] THEN
 717   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_SUPERSET) THEN
 718   REWRITE_TAC[support; IN_ELIM_THM; SUBSET; IN_UNION] THEN
 719   ASM_MESON_TAC[monoidal]);;
 720
 721 let ITERATE_CLAUSES_NUMSEG = prove
 722  (`!op. monoidal op
 723         ==> (!m. iterate op (m..0) f = if m = 0 then f(0) else neutral op) /\
 724             (!m n. iterate op (m..SUC n) f =
 725                       if m <= SUC n then op (iterate op (m..n) f) (f(SUC n))
 726                       else iterate op (m..n) f)`,
 727   REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
 728   COND_CASES_TAC THEN
 729   ASM_SIMP_TAC[ITERATE_CLAUSES; FINITE_NUMSEG; IN_NUMSEG; FINITE_EMPTY] THEN
 730   REWRITE_TAC[ARITH_RULE `~(SUC n <= n)`; NOT_IN_EMPTY] THEN
 731   ASM_MESON_TAC[monoidal]);;
 732
 733 let ITERATE_PAIR = prove
 734  (`!op. monoidal op
 735         ==> !f m n. iterate op (2*m..2*n+1) f =
 736                     iterate op (m..n) (\i. op (f(2*i)) (f(2*i+1)))`,
 737   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
 738   INDUCT_TAC THEN CONV_TAC NUM_REDUCE_CONV THENL
 739    [ASM_SIMP_TAC[num_CONV `1`; ITERATE_CLAUSES_NUMSEG] THEN
 740     REWRITE_TAC[ARITH_RULE `2 * m <= SUC 0 <=> m = 0`] THEN
 741     COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_EQ_0; ARITH];
 742     REWRITE_TAC[ARITH_RULE `2 * SUC n + 1 = SUC(SUC(2 * n + 1))`] THEN
 743     ASM_SIMP_TAC[ITERATE_CLAUSES_NUMSEG] THEN
 744     REWRITE_TAC[ARITH_RULE `2 * m <= SUC(SUC(2 * n + 1)) <=> m <= SUC n`;
 745                 ARITH_RULE `2 * m <= SUC(2 * n + 1) <=> m <= SUC n`] THEN
 746     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 747     REWRITE_TAC[ARITH_RULE `2 * SUC n = SUC(2 * n + 1)`;
 748                 ARITH_RULE `2 * SUC n + 1 = SUC(SUC(2 * n + 1))`] THEN
 749     ASM_MESON_TAC[monoidal]]);;
 750
 751 (* ------------------------------------------------------------------------- *)
 752 (* Sums of natural numbers.                                                  *)
 753 (* ------------------------------------------------------------------------- *)
 754
 755 prioritize_num();;
 756
 757 let nsum = new_definition
 758   `nsum = iterate (+)`;;
 759
 760 let NEUTRAL_ADD = prove
 761  (`neutral((+):num->num->num) = 0`,
 762   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 763   MESON_TAC[ADD_CLAUSES]);;
 764
 765 let NEUTRAL_MUL = prove
 766  (`neutral(( * ):num->num->num) = 1`,
 767   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 768   MESON_TAC[MULT_CLAUSES; MULT_EQ_1]);;
 769
 770 let MONOIDAL_ADD = prove
 771  (`monoidal((+):num->num->num)`,
 772   REWRITE_TAC[monoidal; NEUTRAL_ADD] THEN ARITH_TAC);;
 773
 774 let MONOIDAL_MUL = prove
 775  (`monoidal(( * ):num->num->num)`,
 776   REWRITE_TAC[monoidal; NEUTRAL_MUL] THEN ARITH_TAC);;
 777
 778 let NSUM_DEGENERATE = prove
 779  (`!f s. ~(FINITE {x | x IN s /\ ~(f x = 0)}) ==> nsum s f = 0`,
 780   REPEAT GEN_TAC THEN REWRITE_TAC[nsum] THEN
 781   SIMP_TAC[iterate; support; NEUTRAL_ADD]);;
 782
 783 let NSUM_CLAUSES = prove
 784  (`(!f. nsum {} f = 0) /\
 785    (!x f s. FINITE(s)
 786             ==> (nsum (x INSERT s) f =
 787                  if x IN s then nsum s f else f(x) + nsum s f))`,
 788   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
 789   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
 790   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_ADD]);;
 791
 792 let NSUM_UNION = prove
 793  (`!f s t. FINITE s /\ FINITE t /\ DISJOINT s t
 794            ==> (nsum (s UNION t) f = nsum s f + nsum t f)`,
 795   SIMP_TAC[nsum; ITERATE_UNION; MONOIDAL_ADD]);;
 796
 797 let NSUM_DIFF = prove
 798  (`!f s t. FINITE s /\ t SUBSET s
 799            ==> (nsum (s DIFF t) f = nsum s f - nsum t f)`,
 800   REPEAT STRIP_TAC THEN
 801   MATCH_MP_TAC(ARITH_RULE `(x + z = y:num) ==> (x = y - z)`) THEN
 802   ASM_SIMP_TAC[nsum; ITERATE_DIFF; MONOIDAL_ADD]);;
 803
 804 let NSUM_INCL_EXCL = prove
 805  (`!s t (f:A->num).
 806      FINITE s /\ FINITE t
 807      ==> nsum s f + nsum t f = nsum (s UNION t) f + nsum (s INTER t) f`,
 808   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
 809   MATCH_MP_TAC ITERATE_INCL_EXCL THEN REWRITE_TAC[MONOIDAL_ADD]);;
 810
 811 let NSUM_SUPPORT = prove
 812  (`!f s. nsum (support (+) f s) f = nsum s f`,
 813   SIMP_TAC[nsum; iterate; SUPPORT_SUPPORT]);;
 814
 815 let NSUM_ADD = prove
 816  (`!f g s. FINITE s ==> (nsum s (\x. f(x) + g(x)) = nsum s f + nsum s g)`,
 817   SIMP_TAC[nsum; ITERATE_OP; MONOIDAL_ADD]);;
 818
 819 let NSUM_ADD_GEN = prove
 820  (`!f g s.
 821        FINITE {x | x IN s /\ ~(f x = 0)} /\ FINITE {x | x IN s /\ ~(g x = 0)}
 822        ==> nsum s (\x. f x + g x) = nsum s f + nsum s g`,
 823   REWRITE_TAC[GSYM NEUTRAL_ADD; GSYM support; nsum] THEN
 824   MATCH_MP_TAC ITERATE_OP_GEN THEN ACCEPT_TAC MONOIDAL_ADD);;
 825
 826 let NSUM_EQ_0 = prove
 827  (`!f s. (!x:A. x IN s ==> (f(x) = 0)) ==> (nsum s f = 0)`,
 828   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
 829   SIMP_TAC[ITERATE_EQ_NEUTRAL; MONOIDAL_ADD]);;
 830
 831 let NSUM_0 = prove
 832  (`!s:A->bool. nsum s (\n. 0) = 0`,
 833   SIMP_TAC[NSUM_EQ_0]);;
 834
 835 let NSUM_LMUL = prove
 836  (`!f c s:A->bool. nsum s (\x. c * f(x)) = c * nsum s f`,
 837   REPEAT GEN_TAC THEN ASM_CASES_TAC `c = 0` THEN
 838   ASM_REWRITE_TAC[MULT_CLAUSES; NSUM_0] THEN REWRITE_TAC[nsum] THEN
 839   ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
 840   SUBGOAL_THEN `support (+) (\x:A. c * f(x)) s = support (+) f s` SUBST1_TAC
 841   THENL [ASM_SIMP_TAC[support; MULT_EQ_0; NEUTRAL_ADD]; ALL_TAC] THEN
 842   COND_CASES_TAC THEN REWRITE_TAC[NEUTRAL_ADD; MULT_CLAUSES] THEN
 843   UNDISCH_TAC `FINITE (support (+) f (s:A->bool))` THEN
 844   SPEC_TAC(`support (+) f (s:A->bool)`,`t:A->bool`) THEN
 845   REWRITE_TAC[GSYM nsum] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 846   SIMP_TAC[NSUM_CLAUSES; MULT_CLAUSES; LEFT_ADD_DISTRIB]);;
 847
 848 let NSUM_RMUL = prove
 849  (`!f c s:A->bool. nsum s (\x. f(x) * c) = nsum s f * c`,
 850   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[NSUM_LMUL]);;
 851
 852 let NSUM_LE = prove
 853  (`!f g s. FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x))
 854            ==> nsum s f <= nsum s g`,
 855   ONCE_REWRITE_TAC[IMP_CONJ] THEN
 856   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 857   SIMP_TAC[NSUM_CLAUSES; LE_REFL; LE_ADD2; IN_INSERT]);;
 858
 859 let NSUM_LT = prove
 860  (`!f g s:A->bool.
 861         FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x)) /\
 862         (?x. x IN s /\ f(x) < g(x))
 863          ==> nsum s f < nsum s g`,
 864   REPEAT GEN_TAC THEN
 865   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 866   DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN
 867   SUBGOAL_THEN `s = (a:A) INSERT (s DELETE a)` SUBST1_TAC THENL
 868    [UNDISCH_TAC `a:A IN s` THEN SET_TAC[]; ALL_TAC] THEN
 869   ASM_SIMP_TAC[NSUM_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
 870   ASM_SIMP_TAC[LTE_ADD2; NSUM_LE; IN_DELETE; FINITE_DELETE]);;
 871
 872 let NSUM_LT_ALL = prove
 873  (`!f g s. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < g(x))
 874            ==> nsum s f < nsum s g`,
 875   MESON_TAC[MEMBER_NOT_EMPTY; LT_IMP_LE; NSUM_LT]);;
 876
 877 let NSUM_EQ = prove
 878  (`!f g s. (!x. x IN s ==> (f x = g x)) ==> (nsum s f = nsum s g)`,
 879   REWRITE_TAC[nsum] THEN
 880   MATCH_MP_TAC ITERATE_EQ THEN REWRITE_TAC[MONOIDAL_ADD]);;
 881
 882 let NSUM_CONST = prove
 883  (`!c s. FINITE s ==> (nsum s (\n. c) = (CARD s) * c)`,
 884   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 885   SIMP_TAC[NSUM_CLAUSES; CARD_CLAUSES] THEN
 886   REPEAT STRIP_TAC THEN ARITH_TAC);;
 887
 888 let NSUM_POS_BOUND = prove
 889  (`!f b s. FINITE s /\ nsum s f <= b ==> !x:A. x IN s ==> f x <= b`,
 890   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 891   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 892   SIMP_TAC[NSUM_CLAUSES; NOT_IN_EMPTY; IN_INSERT] THEN
 893   MESON_TAC[LE_0; ARITH_RULE
 894    `0 <= x /\ 0 <= y /\ x + y <= b ==> x <= b /\ y <= b`]);;
 895
 896 let NSUM_EQ_0_IFF = prove
 897  (`!s. FINITE s ==> (nsum s f = 0 <=> !x. x IN s ==> f x = 0)`,
 898   REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[NSUM_EQ_0] THEN
 899   ASM_MESON_TAC[ARITH_RULE `n = 0 <=> n <= 0`; NSUM_POS_BOUND]);;
 900
 901 let NSUM_POS_LT = prove
 902  (`!f s:A->bool.
 903         FINITE s /\ (?x. x IN s /\ 0 < f x)
 904         ==> 0 < nsum s f`,
 905   SIMP_TAC[ARITH_RULE `0 < n <=> ~(n = 0)`; NSUM_EQ_0_IFF] THEN MESON_TAC[]);;
 906
 907 let NSUM_POS_LT_ALL = prove
 908  (`!s f:A->num.
 909      FINITE s /\ ~(s = {}) /\ (!i. i IN s ==> 0 < f i) ==> 0 < nsum s f`,
 910   REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_POS_LT THEN
 911   ASM_MESON_TAC[MEMBER_NOT_EMPTY; REAL_LT_IMP_LE]);;
 912
 913 let NSUM_DELETE = prove
 914  (`!f s a. FINITE s /\ a IN s ==> f(a) + nsum(s DELETE a) f = nsum s f`,
 915   SIMP_TAC[nsum; ITERATE_DELETE; MONOIDAL_ADD]);;
 916
 917 let NSUM_SING = prove
 918  (`!f x. nsum {x} f = f(x)`,
 919   SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ADD_CLAUSES]);;
 920
 921 let NSUM_DELTA = prove
 922  (`!s a. nsum s (\x. if x = a:A then b else 0) = if a IN s then b else 0`,
 923   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
 924   SIMP_TAC[ITERATE_DELTA; MONOIDAL_ADD]);;
 925
 926 let NSUM_SWAP = prove
 927  (`!f:A->B->num s t.
 928       FINITE(s) /\ FINITE(t)
 929       ==> (nsum s (\i. nsum t (f i)) = nsum t (\j. nsum s (\i. f i j)))`,
 930   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 931   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 932   SIMP_TAC[NSUM_CLAUSES; NSUM_0; NSUM_ADD; ETA_AX]);;
 933
 934 let NSUM_IMAGE = prove
 935  (`!f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
 936            ==> (nsum (IMAGE f s) g = nsum s (g o f))`,
 937   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
 938   MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_ADD]);;
 939
 940 let NSUM_SUPERSET = prove
 941  (`!f:A->num u v.
 942         u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = 0))
 943         ==> (nsum v f = nsum u f)`,
 944   SIMP_TAC[nsum; GSYM NEUTRAL_ADD; ITERATE_SUPERSET; MONOIDAL_ADD]);;
 945
 946 let NSUM_UNION_RZERO = prove
 947  (`!f:A->num u v.
 948         FINITE u /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = 0))
 949         ==> (nsum (u UNION v) f = nsum u f)`,
 950   let lemma = prove(`u UNION v = u UNION (v DIFF u)`,SET_TAC[]) in
 951   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[lemma] THEN
 952   MATCH_MP_TAC NSUM_SUPERSET THEN ASM_MESON_TAC[IN_UNION; IN_DIFF; SUBSET]);;
 953
 954 let NSUM_UNION_LZERO = prove
 955  (`!f:A->num u v.
 956         FINITE v /\ (!x. x IN u /\ ~(x IN v) ==> (f(x) = 0))
 957         ==> (nsum (u UNION v) f = nsum v f)`,
 958   MESON_TAC[NSUM_UNION_RZERO; UNION_COMM]);;
 959
 960 let NSUM_RESTRICT = prove
 961  (`!f s. FINITE s ==> (nsum s (\x. if x IN s then f(x) else 0) = nsum s f)`,
 962   REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_EQ THEN ASM_SIMP_TAC[]);;
 963
 964 let NSUM_BOUND = prove
 965  (`!s f b. FINITE s /\ (!x:A. x IN s ==> f(x) <= b)
 966            ==> nsum s f <= (CARD s) * b`,
 967   SIMP_TAC[GSYM NSUM_CONST; NSUM_LE]);;
 968
 969 let NSUM_BOUND_GEN = prove
 970  (`!s f b. FINITE s /\ ~(s = {}) /\ (!x:A. x IN s ==> f(x) <= b DIV (CARD s))
 971            ==> nsum s f <= b`,
 972   SIMP_TAC[IMP_CONJ; CARD_EQ_0; LE_RDIV_EQ] THEN REPEAT STRIP_TAC THEN
 973   SUBGOAL_THEN `nsum s (\x. CARD(s:A->bool) * f x) <= CARD s * b` MP_TAC THENL
 974    [ASM_SIMP_TAC[NSUM_BOUND];
 975     ASM_SIMP_TAC[NSUM_LMUL; LE_MULT_LCANCEL; CARD_EQ_0]]);;
 976
 977 let NSUM_BOUND_LT = prove
 978  (`!s f b. FINITE s /\ (!x:A. x IN s ==> f x <= b) /\ (?x. x IN s /\ f x < b)
 979            ==> nsum s f < (CARD s) * b`,
 980   REPEAT STRIP_TAC THEN MATCH_MP_TAC LTE_TRANS THEN
 981   EXISTS_TAC `nsum s (\x:A. b)` THEN CONJ_TAC THENL
 982    [MATCH_MP_TAC NSUM_LT THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
 983     ASM_SIMP_TAC[NSUM_CONST; LE_REFL]]);;
 984
 985 let NSUM_BOUND_LT_ALL = prove
 986  (`!s f b. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < b)
 987            ==> nsum s f <  (CARD s) * b`,
 988   MESON_TAC[MEMBER_NOT_EMPTY; LT_IMP_LE; NSUM_BOUND_LT]);;
 989
 990 let NSUM_BOUND_LT_GEN = prove
 991  (`!s f b. FINITE s /\ ~(s = {}) /\ (!x:A. x IN s ==> f(x) < b DIV (CARD s))
 992            ==> nsum s f < b`,
 993   REPEAT STRIP_TAC THEN MATCH_MP_TAC LTE_TRANS THEN
 994   EXISTS_TAC `nsum (s:A->bool) (\a. f(a) + 1)` THEN CONJ_TAC THENL
 995    [MATCH_MP_TAC NSUM_LT_ALL THEN ASM_SIMP_TAC[] THEN ARITH_TAC;
 996     MATCH_MP_TAC NSUM_BOUND_GEN THEN
 997     ASM_REWRITE_TAC[ARITH_RULE `a + 1 <= b <=> a < b`]]);;
 998
 999 let NSUM_UNION_EQ = prove
1000  (`!s t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
1001            ==> (nsum s f + nsum t f = nsum u f)`,
1002   MESON_TAC[NSUM_UNION; DISJOINT; FINITE_SUBSET; SUBSET_UNION]);;
1003
1004 let NSUM_EQ_SUPERSET = prove
1005  (`!f s t:A->bool.
1006         FINITE t /\ t SUBSET s /\
1007         (!x. x IN t ==> (f x = g x)) /\
1008         (!x. x IN s /\ ~(x IN t) ==> (f(x) = 0))
1009         ==> (nsum s f = nsum t g)`,
1010   MESON_TAC[NSUM_SUPERSET; NSUM_EQ]);;
1011
1012 let NSUM_RESTRICT_SET = prove
1013  (`!P s f. nsum {x:A | x IN s /\ P x} f = nsum s (\x. if P x then f(x) else 0)`,
1014   ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
1015   REWRITE_TAC[support; NEUTRAL_ADD; IN_ELIM_THM] THEN
1016   REWRITE_TAC[MESON[] `~((if P x then f x else a) = a) <=> P x /\ ~(f x = a)`;
1017               GSYM CONJ_ASSOC] THEN
1018   REPEAT GEN_TAC THEN MATCH_MP_TAC NSUM_EQ THEN SIMP_TAC[IN_ELIM_THM]);;
1019
1020 let NSUM_NSUM_RESTRICT = prove
1021  (`!R f s t.
1022         FINITE s /\ FINITE t
1023         ==> (nsum s (\x. nsum {y | y IN t /\ R x y} (\y. f x y)) =
1024              nsum t (\y. nsum {x | x IN s /\ R x y} (\x. f x y)))`,
1025   REPEAT GEN_TAC THEN SIMP_TAC[NSUM_RESTRICT_SET] THEN
1026   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP NSUM_SWAP th]));;
1027
1028 let CARD_EQ_NSUM = prove
1029  (`!s. FINITE s ==> ((CARD s) = nsum s (\x. 1))`,
1030   SIMP_TAC[NSUM_CONST; MULT_CLAUSES]);;
1031
1032 let NSUM_MULTICOUNT_GEN = prove
1033  (`!R:A->B->bool s t k.
1034         FINITE s /\ FINITE t /\
1035         (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k(j)))
1036         ==> (nsum s (\i. (CARD {j | j IN t /\ R i j})) =
1037              nsum t (\i. (k i)))`,
1038   REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
1039   DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
1040   MATCH_MP_TAC EQ_TRANS THEN
1041   EXISTS_TAC `nsum s (\i:A. nsum {j:B | j IN t /\ R i j} (\j. 1))` THEN
1042   CONJ_TAC THENL
1043    [MATCH_MP_TAC NSUM_EQ THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1044     ASM_SIMP_TAC[CARD_EQ_NSUM; FINITE_RESTRICT];
1045     FIRST_ASSUM(fun t -> ONCE_REWRITE_TAC[MATCH_MP NSUM_NSUM_RESTRICT t]) THEN
1046     MATCH_MP_TAC NSUM_EQ THEN ASM_SIMP_TAC[NSUM_CONST; FINITE_RESTRICT] THEN
1047     REWRITE_TAC[MULT_CLAUSES]]);;
1048
1049 let NSUM_MULTICOUNT = prove
1050  (`!R:A->B->bool s t k.
1051         FINITE s /\ FINITE t /\
1052         (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k))
1053         ==> (nsum s (\i. (CARD {j | j IN t /\ R i j})) = (k * CARD t))`,
1054   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1055   EXISTS_TAC `nsum t (\i:B. k)` THEN CONJ_TAC THENL
1056    [MATCH_MP_TAC NSUM_MULTICOUNT_GEN THEN ASM_REWRITE_TAC[];
1057     ASM_SIMP_TAC[NSUM_CONST] THEN REWRITE_TAC[MULT_AC]]);;
1058
1059 let NSUM_IMAGE_GEN = prove
1060  (`!f:A->B g s.
1061         FINITE s
1062         ==> (nsum s g =
1063              nsum (IMAGE f s) (\y. nsum {x | x IN s /\ (f(x) = y)} g))`,
1064   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1065    `nsum s (\x:A. nsum {y:B | y IN IMAGE f s /\ (f x = y)} (\y. g x))` THEN
1066   CONJ_TAC THENL
1067    [MATCH_MP_TAC NSUM_EQ THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:A` THEN
1068     DISCH_TAC THEN
1069     SUBGOAL_THEN `{y | y IN IMAGE (f:A->B) s /\ (f x = y)} = {(f x)}`
1070      (fun th -> REWRITE_TAC[th; NSUM_SING; o_THM]) THEN
1071     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING; IN_IMAGE] THEN
1072     ASM_MESON_TAC[];
1073     GEN_REWRITE_TAC (funpow 2 RAND_CONV o ABS_CONV o RAND_CONV)
1074      [GSYM ETA_AX] THEN
1075     ASM_SIMP_TAC[NSUM_NSUM_RESTRICT; FINITE_IMAGE]]);;
1076
1077 let NSUM_GROUP = prove
1078  (`!f:A->B g s t.
1079         FINITE s /\ IMAGE f s SUBSET t
1080         ==> nsum t (\y. nsum {x | x IN s /\ f(x) = y} g) = nsum s g`,
1081   REPEAT STRIP_TAC THEN
1082   MP_TAC(ISPECL [`f:A->B`; `g:A->num`; `s:A->bool`] NSUM_IMAGE_GEN) THEN
1083   ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
1084   MATCH_MP_TAC NSUM_SUPERSET THEN ASM_REWRITE_TAC[] THEN
1085   REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_EQ_0 THEN ASM SET_TAC[]);;
1086
1087 let NSUM_SUBSET = prove
1088  (`!u v f. FINITE u /\ FINITE v /\ (!x:A. x IN (u DIFF v) ==> f(x) = 0)
1089            ==> nsum u f <= nsum v f`,
1090   REPEAT STRIP_TAC THEN
1091   MP_TAC(ISPECL [`f:A->num`; `u INTER v :A->bool`] NSUM_UNION) THEN
1092   DISCH_THEN(fun th -> MP_TAC(SPEC `v DIFF u :A->bool` th) THEN
1093                        MP_TAC(SPEC `u DIFF v :A->bool` th)) THEN
1094   REWRITE_TAC[SET_RULE `(u INTER v) UNION (u DIFF v) = u`;
1095               SET_RULE `(u INTER v) UNION (v DIFF u) = v`] THEN
1096   ASM_SIMP_TAC[FINITE_DIFF; FINITE_INTER] THEN
1097   REPEAT(ANTS_TAC THENL [SET_TAC[]; DISCH_THEN SUBST1_TAC]) THEN
1098   ASM_SIMP_TAC[NSUM_EQ_0] THEN ARITH_TAC);;
1099
1100 let NSUM_SUBSET_SIMPLE = prove
1101  (`!u v f. FINITE v /\ u SUBSET v ==> nsum u f <= nsum v f`,
1102   REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_SUBSET THEN
1103   ASM_MESON_TAC[IN_DIFF; SUBSET; FINITE_SUBSET]);;
1104
1105 let NSUM_LE_GEN = prove
1106  (`!f g s. (!x:A. x IN s ==> f x <= g x) /\ FINITE {x | x IN s /\ ~(g x = 0)}
1107            ==> nsum s f <= nsum s g`,
1108   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
1109   REWRITE_TAC[support; NEUTRAL_ADD] THEN
1110   TRANS_TAC LE_TRANS `nsum {x | x IN s /\ ~(g(x:A) = 0)} f` THEN
1111   CONJ_TAC THENL
1112    [MATCH_MP_TAC NSUM_SUBSET THEN
1113     ASM_REWRITE_TAC[IN_ELIM_THM; IN_DIFF] THEN
1114     CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[LE]] THEN
1115     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
1116       FINITE_SUBSET)) THEN
1117     REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[LE];
1118     MATCH_MP_TAC NSUM_LE THEN ASM_SIMP_TAC[IN_ELIM_THM]]);;
1119
1120 let NSUM_IMAGE_NONZERO = prove
1121  (`!d:B->num i:A->B s.
1122     FINITE s /\
1123     (!x y. x IN s /\ y IN s /\ ~(x = y) /\ i x = i y ==> d(i x) = 0)
1124     ==> nsum (IMAGE i s) d = nsum s (d o i)`,
1125   REWRITE_TAC[GSYM NEUTRAL_ADD; nsum] THEN
1126   MATCH_MP_TAC ITERATE_IMAGE_NONZERO THEN REWRITE_TAC[MONOIDAL_ADD]);;
1127
1128 let NSUM_BIJECTION = prove
1129  (`!f p s:A->bool.
1130                 (!x. x IN s ==> p(x) IN s) /\
1131                 (!y. y IN s ==> ?!x. x IN s /\ p(x) = y)
1132                 ==> nsum s f = nsum s (f o p)`,
1133   REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_BIJECTION THEN
1134   REWRITE_TAC[MONOIDAL_ADD]);;
1135
1136 let NSUM_NSUM_PRODUCT = prove
1137  (`!s:A->bool t:A->B->bool x.
1138         FINITE s /\ (!i. i IN s ==> FINITE(t i))
1139         ==> nsum s (\i. nsum (t i) (x i)) =
1140             nsum {i,j | i IN s /\ j IN t i} (\(i,j). x i j)`,
1141   REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_ITERATE_PRODUCT THEN
1142   REWRITE_TAC[MONOIDAL_ADD]);;
1143
1144 let NSUM_EQ_GENERAL = prove
1145  (`!s:A->bool t:B->bool f g h.
1146         (!y. y IN t ==> ?!x. x IN s /\ h(x) = y) /\
1147         (!x. x IN s ==> h(x) IN t /\ g(h x) = f x)
1148         ==> nsum s f = nsum t g`,
1149   REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL THEN
1150   REWRITE_TAC[MONOIDAL_ADD]);;
1151
1152 let NSUM_EQ_GENERAL_INVERSES = prove
1153  (`!s:A->bool t:B->bool f g h k.
1154         (!y. y IN t ==> k(y) IN s /\ h(k y) = y) /\
1155         (!x. x IN s ==> h(x) IN t /\ k(h x) = x /\ g(h x) = f x)
1156         ==> nsum s f = nsum t g`,
1157   REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL_INVERSES THEN
1158   REWRITE_TAC[MONOIDAL_ADD]);;
1159
1160 let NSUM_INJECTION = prove
1161  (`!f p s. FINITE s /\
1162            (!x. x IN s ==> p x IN s) /\
1163            (!x y. x IN s /\ y IN s /\ p x = p y ==> x = y)
1164            ==> nsum s (f o p) = nsum s f`,
1165   REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_INJECTION THEN
1166   REWRITE_TAC[MONOIDAL_ADD]);;
1167
1168 let NSUM_UNION_NONZERO = prove
1169  (`!f s t. FINITE s /\ FINITE t /\ (!x. x IN s INTER t ==> f(x) = 0)
1170            ==> nsum (s UNION t) f = nsum s f + nsum t f`,
1171   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
1172   MATCH_MP_TAC ITERATE_UNION_NONZERO THEN REWRITE_TAC[MONOIDAL_ADD]);;
1173
1174 let NSUM_UNIONS_NONZERO = prove
1175  (`!f s. FINITE s /\ (!t:A->bool. t IN s ==> FINITE t) /\
1176          (!t1 t2 x. t1 IN s /\ t2 IN s /\ ~(t1 = t2) /\ x IN t1 /\ x IN t2
1177                     ==> f x = 0)
1178          ==> nsum (UNIONS s) f = nsum s (\t. nsum t f)`,
1179   GEN_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN
1180   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1181   REWRITE_TAC[UNIONS_0; UNIONS_INSERT; NSUM_CLAUSES; IN_INSERT] THEN
1182   MAP_EVERY X_GEN_TAC [`t:A->bool`; `s:(A->bool)->bool`] THEN
1183   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
1184   ONCE_REWRITE_TAC[IMP_CONJ] THEN ASM_SIMP_TAC[NSUM_CLAUSES] THEN
1185   ANTS_TAC THENL  [ASM_MESON_TAC[]; DISCH_THEN(SUBST_ALL_TAC o SYM)] THEN
1186   STRIP_TAC THEN MATCH_MP_TAC NSUM_UNION_NONZERO THEN
1187   ASM_SIMP_TAC[FINITE_UNIONS; IN_INTER; IN_UNIONS] THEN ASM_MESON_TAC[]);;
1188
1189 let NSUM_CASES = prove
1190  (`!s P f g. FINITE s
1191              ==> nsum s (\x:A. if P x then f x else g x) =
1192                  nsum {x | x IN s /\ P x} f + nsum {x | x IN s /\ ~P x} g`,
1193   REWRITE_TAC[nsum; GSYM NEUTRAL_ADD] THEN
1194   MATCH_MP_TAC ITERATE_CASES THEN REWRITE_TAC[MONOIDAL_ADD]);;
1195
1196 let NSUM_CLOSED = prove
1197  (`!P f:A->num s.
1198         P(0) /\ (!x y. P x /\ P y ==> P(x + y)) /\ (!a. a IN s ==> P(f a))
1199         ==> P(nsum s f)`,
1200   REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_ADD) THEN
1201   DISCH_THEN(MP_TAC o SPEC `P:num->bool`) THEN
1202   ASM_SIMP_TAC[NEUTRAL_ADD; GSYM nsum]);;
1203
1204 let NSUM_ADD_NUMSEG = prove
1205  (`!f g m n. nsum(m..n) (\i. f(i) + g(i)) = nsum(m..n) f + nsum(m..n) g`,
1206   SIMP_TAC[NSUM_ADD; FINITE_NUMSEG]);;
1207
1208 let NSUM_LE_NUMSEG = prove
1209  (`!f g m n. (!i. m <= i /\ i <= n ==> f(i) <= g(i))
1210              ==> nsum(m..n) f <= nsum(m..n) g`,
1211   SIMP_TAC[NSUM_LE; FINITE_NUMSEG; IN_NUMSEG]);;
1212
1213 let NSUM_EQ_NUMSEG = prove
1214  (`!f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
1215              ==> (nsum(m..n) f = nsum(m..n) g)`,
1216   MESON_TAC[NSUM_EQ; FINITE_NUMSEG; IN_NUMSEG]);;
1217
1218 let NSUM_CONST_NUMSEG = prove
1219  (`!c m n. nsum(m..n) (\n. c) = ((n + 1) - m) * c`,
1220   SIMP_TAC[NSUM_CONST; FINITE_NUMSEG; CARD_NUMSEG]);;
1221
1222 let NSUM_EQ_0_NUMSEG = prove
1223  (`!f m n. (!i. m <= i /\ i <= n ==> (f(i) = 0)) ==> (nsum(m..n) f = 0)`,
1224   SIMP_TAC[NSUM_EQ_0; IN_NUMSEG]);;
1225
1226 let NSUM_EQ_0_IFF_NUMSEG = prove
1227  (`!f m n. nsum (m..n) f = 0 <=> !i. m <= i /\ i <= n ==> f i = 0`,
1228   SIMP_TAC[NSUM_EQ_0_IFF; FINITE_NUMSEG; IN_NUMSEG]);;
1229
1230 let NSUM_TRIV_NUMSEG = prove
1231  (`!f m n. n < m ==> (nsum(m..n) f = 0)`,
1232   MESON_TAC[NSUM_EQ_0_NUMSEG; LE_TRANS; NOT_LT]);;
1233
1234 let NSUM_SING_NUMSEG = prove
1235  (`!f n. nsum(n..n) f = f(n)`,
1236   SIMP_TAC[NSUM_SING; NUMSEG_SING]);;
1237
1238 let NSUM_CLAUSES_NUMSEG = prove
1239  (`(!m. nsum(m..0) f = if m = 0 then f(0) else 0) /\
1240    (!m n. nsum(m..SUC n) f = if m <= SUC n then nsum(m..n) f + f(SUC n)
1241                              else nsum(m..n) f)`,
1242   MP_TAC(MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_ADD) THEN
1243   REWRITE_TAC[NEUTRAL_ADD; nsum]);;
1244
1245 let NSUM_SWAP_NUMSEG = prove
1246  (`!a b c d f.
1247      nsum(a..b) (\i. nsum(c..d) (f i)) =
1248      nsum(c..d) (\j. nsum(a..b) (\i. f i j))`,
1249   REPEAT GEN_TAC THEN MATCH_MP_TAC NSUM_SWAP THEN REWRITE_TAC[FINITE_NUMSEG]);;
1250
1251 let NSUM_ADD_SPLIT = prove
1252  (`!f m n p.
1253         m <= n + 1 ==> (nsum (m..(n+p)) f = nsum(m..n) f + nsum(n+1..n+p) f)`,
1254   SIMP_TAC[NUMSEG_ADD_SPLIT; NSUM_UNION; DISJOINT_NUMSEG; FINITE_NUMSEG;
1255            ARITH_RULE `x < x + 1`]);;
1256
1257 let NSUM_OFFSET = prove
1258  (`!p f m n. nsum(m+p..n+p) f = nsum(m..n) (\i. f(i + p))`,
1259   SIMP_TAC[NUMSEG_OFFSET_IMAGE; NSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
1260   REWRITE_TAC[o_DEF]);;
1261
1262 let NSUM_OFFSET_0 = prove
1263  (`!f m n. m <= n ==> (nsum(m..n) f = nsum(0..n-m) (\i. f(i + m)))`,
1264   SIMP_TAC[GSYM NSUM_OFFSET; ADD_CLAUSES; SUB_ADD]);;
1265
1266 let NSUM_CLAUSES_LEFT = prove
1267  (`!f m n. m <= n ==> nsum(m..n) f = f(m) + nsum(m+1..n) f`,
1268   SIMP_TAC[GSYM NUMSEG_LREC; NSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
1269   ARITH_TAC);;
1270
1271 let NSUM_CLAUSES_RIGHT = prove
1272  (`!f m n. 0 < n /\ m <= n ==> nsum(m..n) f = nsum(m..n-1) f + f(n)`,
1273   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1274   SIMP_TAC[LT_REFL; NSUM_CLAUSES_NUMSEG; SUC_SUB1]);;
1275
1276 let NSUM_PAIR = prove
1277  (`!f m n. nsum(2*m..2*n+1) f = nsum(m..n) (\i. f(2*i) + f(2*i+1))`,
1278   MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_ADD) THEN
1279   REWRITE_TAC[nsum; NEUTRAL_ADD]);;
1280
1281 let MOD_NSUM_MOD = prove
1282  (`!f:A->num n s.
1283         FINITE s /\ ~(n = 0)
1284         ==> (nsum s f) MOD n = nsum s (\i. f(i) MOD n) MOD n`,
1285   GEN_TAC THEN GEN_TAC THEN
1286   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
1287   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[NSUM_CLAUSES] THEN
1288   REPEAT STRIP_TAC THEN
1289   W(MP_TAC o PART_MATCH (rand o rand) MOD_ADD_MOD o lhand o snd) THEN
1290   ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
1291   W(MP_TAC o PART_MATCH (rand o rand) MOD_ADD_MOD o rand o snd) THEN
1292   ASM_SIMP_TAC[MOD_MOD_REFL]);;
1293
1294 let MOD_NSUM_MOD_NUMSEG = prove
1295  (`!f a b n.
1296         ~(n = 0)
1297         ==> (nsum(a..b) f) MOD n = nsum(a..b) (\i. f i MOD n) MOD n`,
1298   MESON_TAC[MOD_NSUM_MOD; FINITE_NUMSEG]);;
1299
1300 let th = prove
1301  (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
1302               ==> nsum s (\i. f(i)) = nsum s g) /\
1303    (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
1304               ==> nsum(a..b) (\i. f(i)) = nsum(a..b) g) /\
1305    (!f g p.   (!x. p x ==> f x = g x)
1306               ==> nsum {y | p y} (\i. f(i)) = nsum {y | p y} g)`,
1307   REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_EQ THEN
1308   ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
1309   extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;
1310
1311 (* ------------------------------------------------------------------------- *)
1312 (* Thanks to finite sums, we can express cardinality of finite union.        *)
1313 (* ------------------------------------------------------------------------- *)
1314
1315 let CARD_UNIONS = prove
1316  (`!s:(A->bool)->bool.
1317         FINITE s /\ (!t. t IN s ==> FINITE t) /\
1318         (!t u. t IN s /\ u IN s /\ ~(t = u) ==> t INTER u = {})
1319         ==> CARD(UNIONS s) = nsum s CARD`,
1320   ONCE_REWRITE_TAC[IMP_CONJ] THEN
1321   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1322   REWRITE_TAC[UNIONS_0; UNIONS_INSERT; NOT_IN_EMPTY; IN_INSERT] THEN
1323   REWRITE_TAC[CARD_CLAUSES; NSUM_CLAUSES] THEN
1324   MAP_EVERY X_GEN_TAC [`t:A->bool`; `f:(A->bool)->bool`] THEN
1325   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
1326   ASM_SIMP_TAC[NSUM_CLAUSES] THEN
1327   DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) STRIP_ASSUME_TAC) THEN
1328   CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN
1329   ASM_SIMP_TAC[FINITE_UNIONS; FINITE_UNION; INTER_UNIONS] THEN
1330   REWRITE_TAC[EMPTY_UNIONS; IN_ELIM_THM] THEN ASM MESON_TAC[]);;
1331
1332 (* ------------------------------------------------------------------------- *)
1333 (* Sums of real numbers.                                                     *)
1334 (* ------------------------------------------------------------------------- *)
1335
1336 prioritize_real();;
1337
1338 let sum = new_definition
1339   `sum = iterate (+)`;;
1340
1341 let NEUTRAL_REAL_ADD = prove
1342  (`neutral((+):real->real->real) = &0`,
1343   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
1344   MESON_TAC[REAL_ADD_LID; REAL_ADD_RID]);;
1345
1346 let NEUTRAL_REAL_MUL = prove
1347  (`neutral(( * ):real->real->real) = &1`,
1348   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
1349   MESON_TAC[REAL_MUL_LID; REAL_MUL_RID]);;
1350
1351 let MONOIDAL_REAL_ADD = prove
1352  (`monoidal((+):real->real->real)`,
1353   REWRITE_TAC[monoidal; NEUTRAL_REAL_ADD] THEN REAL_ARITH_TAC);;
1354
1355 let MONOIDAL_REAL_MUL = prove
1356  (`monoidal(( * ):real->real->real)`,
1357   REWRITE_TAC[monoidal; NEUTRAL_REAL_MUL] THEN REAL_ARITH_TAC);;
1358
1359 let SUM_DEGENERATE = prove
1360  (`!f s. ~(FINITE {x | x IN s /\ ~(f x = &0)}) ==> sum s f = &0`,
1361   REPEAT GEN_TAC THEN REWRITE_TAC[sum] THEN
1362   SIMP_TAC[iterate; support; NEUTRAL_REAL_ADD]);;
1363
1364 let SUM_CLAUSES = prove
1365  (`(!f. sum {} f = &0) /\
1366    (!x f s. FINITE(s)
1367             ==> (sum (x INSERT s) f =
1368                  if x IN s then sum s f else f(x) + sum s f))`,
1369   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1370   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1371   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1372
1373 let SUM_UNION = prove
1374  (`!f s t. FINITE s /\ FINITE t /\ DISJOINT s t
1375            ==> (sum (s UNION t) f = sum s f + sum t f)`,
1376   SIMP_TAC[sum; ITERATE_UNION; MONOIDAL_REAL_ADD]);;
1377
1378 let SUM_DIFF = prove
1379  (`!f s t. FINITE s /\ t SUBSET s ==> (sum (s DIFF t) f = sum s f - sum t f)`,
1380   SIMP_TAC[REAL_EQ_SUB_LADD; sum; ITERATE_DIFF; MONOIDAL_REAL_ADD]);;
1381
1382 let SUM_INCL_EXCL = prove
1383  (`!s t (f:A->real).
1384      FINITE s /\ FINITE t
1385      ==> sum s f + sum t f = sum (s UNION t) f + sum (s INTER t) f`,
1386   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1387   MATCH_MP_TAC ITERATE_INCL_EXCL THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1388
1389 let SUM_SUPPORT = prove
1390  (`!f s. sum (support (+) f s) f = sum s f`,
1391   SIMP_TAC[sum; iterate; SUPPORT_SUPPORT]);;
1392
1393 let SUM_ADD = prove
1394  (`!f g s. FINITE s ==> (sum s (\x. f(x) + g(x)) = sum s f + sum s g)`,
1395   SIMP_TAC[sum; ITERATE_OP; MONOIDAL_REAL_ADD]);;
1396
1397 let SUM_ADD_GEN = prove
1398  (`!f g s.
1399        FINITE {x | x IN s /\ ~(f x = &0)} /\ FINITE {x | x IN s /\ ~(g x = &0)}
1400        ==> sum s (\x. f x + g x) = sum s f + sum s g`,
1401   REWRITE_TAC[GSYM NEUTRAL_REAL_ADD; GSYM support; sum] THEN
1402   MATCH_MP_TAC ITERATE_OP_GEN THEN ACCEPT_TAC MONOIDAL_REAL_ADD);;
1403
1404 let SUM_EQ_0 = prove
1405  (`!f s. (!x:A. x IN s ==> (f(x) = &0)) ==> (sum s f = &0)`,
1406   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1407   SIMP_TAC[ITERATE_EQ_NEUTRAL; MONOIDAL_REAL_ADD]);;
1408
1409 let SUM_0 = prove
1410  (`!s:A->bool. sum s (\n. &0) = &0`,
1411   SIMP_TAC[SUM_EQ_0]);;
1412
1413 let SUM_LMUL = prove
1414  (`!f c s:A->bool. sum s (\x. c * f(x)) = c * sum s f`,
1415   REPEAT GEN_TAC THEN ASM_CASES_TAC `c = &0` THEN
1416   ASM_REWRITE_TAC[REAL_MUL_LZERO; SUM_0] THEN REWRITE_TAC[sum] THEN
1417   ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
1418   SUBGOAL_THEN `support (+) (\x:A. c * f(x)) s = support (+) f s` SUBST1_TAC
1419   THENL [ASM_SIMP_TAC[support; REAL_ENTIRE; NEUTRAL_REAL_ADD]; ALL_TAC] THEN
1420   COND_CASES_TAC THEN REWRITE_TAC[NEUTRAL_REAL_ADD; REAL_MUL_RZERO] THEN
1421   UNDISCH_TAC `FINITE (support (+) f (s:A->bool))` THEN
1422   SPEC_TAC(`support (+) f (s:A->bool)`,`t:A->bool`) THEN
1423   REWRITE_TAC[GSYM sum] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1424   SIMP_TAC[SUM_CLAUSES; REAL_MUL_RZERO; REAL_MUL_LZERO;
1425            REAL_ADD_LDISTRIB]);;
1426
1427 let SUM_RMUL = prove
1428  (`!f c s:A->bool. sum s (\x. f(x) * c) = sum s f * c`,
1429   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[SUM_LMUL]);;
1430
1431 let SUM_NEG = prove
1432  (`!f s. sum s (\x. --(f(x))) = --(sum s f)`,
1433   ONCE_REWRITE_TAC[REAL_ARITH `--x = --(&1) * x`] THEN
1434   SIMP_TAC[SUM_LMUL]);;
1435
1436 let SUM_SUB = prove
1437  (`!f g s. FINITE s ==> (sum s (\x. f(x) - g(x)) = sum s f - sum s g)`,
1438   ONCE_REWRITE_TAC[real_sub] THEN SIMP_TAC[SUM_NEG; SUM_ADD]);;
1439
1440 let SUM_LE = prove
1441  (`!f g s. FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x)) ==> sum s f <= sum s g`,
1442   ONCE_REWRITE_TAC[IMP_CONJ] THEN
1443   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1444   SIMP_TAC[SUM_CLAUSES; REAL_LE_REFL; REAL_LE_ADD2; IN_INSERT]);;
1445
1446 let SUM_LT = prove
1447  (`!f g s:A->bool.
1448         FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x)) /\
1449         (?x. x IN s /\ f(x) < g(x))
1450          ==> sum s f < sum s g`,
1451   REPEAT GEN_TAC THEN
1452   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1453   DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN
1454   SUBGOAL_THEN `s = (a:A) INSERT (s DELETE a)` SUBST1_TAC THENL
1455    [UNDISCH_TAC `a:A IN s` THEN SET_TAC[]; ALL_TAC] THEN
1456   ASM_SIMP_TAC[SUM_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
1457   ASM_SIMP_TAC[REAL_LTE_ADD2; SUM_LE; IN_DELETE; FINITE_DELETE]);;
1458
1459 let SUM_LT_ALL = prove
1460  (`!f g s. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < g(x))
1461            ==> sum s f < sum s g`,
1462   MESON_TAC[MEMBER_NOT_EMPTY; REAL_LT_IMP_LE; SUM_LT]);;
1463
1464 let SUM_POS_LT = prove
1465  (`!f s:A->bool.
1466         FINITE s /\
1467         (!x. x IN s ==> &0 <= f x) /\
1468         (?x. x IN s /\ &0 < f x)
1469         ==> &0 < sum s f`,
1470   REPEAT STRIP_TAC THEN
1471   MATCH_MP_TAC REAL_LET_TRANS THEN
1472   EXISTS_TAC `sum (s:A->bool) (\i. &0)` THEN CONJ_TAC THENL
1473    [REWRITE_TAC[SUM_0; REAL_LE_REFL]; MATCH_MP_TAC SUM_LT] THEN
1474   ASM_MESON_TAC[]);;
1475
1476 let SUM_POS_LT_ALL = prove
1477  (`!s f:A->real.
1478      FINITE s /\ ~(s = {}) /\ (!i. i IN s ==> &0 < f i) ==> &0 < sum s f`,
1479   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_POS_LT THEN
1480   ASM_MESON_TAC[MEMBER_NOT_EMPTY; REAL_LT_IMP_LE]);;
1481
1482 let SUM_EQ = prove
1483  (`!f g s. (!x. x IN s ==> (f x = g x)) ==> (sum s f = sum s g)`,
1484   REWRITE_TAC[sum] THEN
1485   MATCH_MP_TAC ITERATE_EQ THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1486
1487 let SUM_ABS = prove
1488  (`!f s. FINITE(s) ==> abs(sum s f) <= sum s (\x. abs(f x))`,
1489   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1490   SIMP_TAC[SUM_CLAUSES; REAL_ABS_NUM; REAL_LE_REFL;
1491            REAL_ARITH `abs(a) <= b ==> abs(x + a) <= abs(x) + b`]);;
1492
1493 let SUM_ABS_LE = prove
1494  (`!f:A->real g s.
1495         FINITE s /\ (!x. x IN s ==> abs(f x) <= g x)
1496         ==> abs(sum s f) <= sum s g`,
1497   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1498   EXISTS_TAC `sum s (\x:A. abs(f x))` THEN
1499   ASM_SIMP_TAC[SUM_ABS] THEN MATCH_MP_TAC SUM_LE THEN
1500   ASM_REWRITE_TAC[]);;
1501
1502 let SUM_CONST = prove
1503  (`!c s. FINITE s ==> (sum s (\n. c) = &(CARD s) * c)`,
1504   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1505   SIMP_TAC[SUM_CLAUSES; CARD_CLAUSES; GSYM REAL_OF_NUM_SUC] THEN
1506   REPEAT STRIP_TAC THEN REAL_ARITH_TAC);;
1507
1508 let SUM_POS_LE = prove
1509  (`!s:A->bool. (!x. x IN s ==> &0 <= f x) ==> &0 <= sum s f`,
1510   REPEAT STRIP_TAC THEN
1511   ASM_CASES_TAC `FINITE {x:A | x IN s /\ ~(f x = &0)}` THEN
1512   ASM_SIMP_TAC[SUM_DEGENERATE; REAL_LE_REFL] THEN
1513   ONCE_REWRITE_TAC[GSYM SUM_SUPPORT] THEN
1514   REWRITE_TAC[support; NEUTRAL_REAL_ADD] THEN
1515   MP_TAC(ISPECL [`\x:A. &0`; `f:A->real`; `{x:A | x IN s /\ ~(f x = &0)}`]
1516         SUM_LE) THEN
1517   ASM_SIMP_TAC[SUM_0; IN_ELIM_THM]);;
1518
1519 let SUM_POS_BOUND = prove
1520  (`!f b s. FINITE s /\ (!x. x IN s ==> &0 <= f x) /\ sum s f <= b
1521            ==> !x:A. x IN s ==> f x <= b`,
1522   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
1523   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1524   SIMP_TAC[SUM_CLAUSES; NOT_IN_EMPTY; IN_INSERT] THEN
1525   MESON_TAC[SUM_POS_LE;
1526    REAL_ARITH `&0 <= x /\ &0 <= y /\ x + y <= b ==> x <= b /\ y <= b`]);;
1527
1528 let SUM_POS_EQ_0 = prove
1529  (`!f s. FINITE s /\ (!x. x IN s ==> &0 <= f x) /\ (sum s f = &0)
1530          ==> !x. x IN s ==> f x = &0`,
1531   REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
1532   MESON_TAC[SUM_POS_BOUND; SUM_POS_LE]);;
1533
1534 let SUM_ZERO_EXISTS = prove
1535  (`!(u:A->real) s.
1536          FINITE s /\ sum s u = &0
1537          ==> (!i. i IN s ==> u i = &0) \/
1538              (?j k. j IN s /\ u j < &0 /\ k IN s /\ u k > &0)`,
1539   REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1540    (MESON[REAL_ARITH `(&0 <= --u <=> ~(u > &0)) /\ (&0 <= u <=> ~(u < &0))`]
1541      `(?j k:A. j IN s /\ u j < &0 /\ k IN s /\ u k > &0) \/
1542       (!i. i IN s ==> &0 <= u i) \/ (!i. i IN s ==> &0 <= --(u i))`) THEN
1543   ASM_REWRITE_TAC[] THEN DISJ1_TAC THENL
1544    [ALL_TAC; ONCE_REWRITE_TAC[REAL_ARITH `x = &0 <=> --x = &0`]] THEN
1545   MATCH_MP_TAC SUM_POS_EQ_0 THEN ASM_REWRITE_TAC[SUM_NEG; REAL_NEG_0]);;
1546
1547 let SUM_DELETE = prove
1548  (`!f s a. FINITE s /\ a IN s ==> sum (s DELETE a) f = sum s f - f(a)`,
1549   SIMP_TAC[REAL_ARITH `y = z - x <=> x + y = z:real`; sum; ITERATE_DELETE;
1550            MONOIDAL_REAL_ADD]);;
1551
1552 let SUM_DELETE_CASES = prove
1553  (`!f s a. FINITE s
1554            ==> sum (s DELETE a) f = if a IN s then sum s f - f(a)
1555                                     else sum s f`,
1556   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
1557   ASM_SIMP_TAC[SET_RULE `~(a IN s) ==> (s DELETE a = s)`; SUM_DELETE]);;
1558
1559 let SUM_SING = prove
1560  (`!f x. sum {x} f = f(x)`,
1561   SIMP_TAC[SUM_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; REAL_ADD_RID]);;
1562
1563 let SUM_DELTA = prove
1564  (`!s a. sum s (\x. if x = a:A then b else &0) = if a IN s then b else &0`,
1565   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1566   SIMP_TAC[ITERATE_DELTA; MONOIDAL_REAL_ADD]);;
1567
1568 let SUM_SWAP = prove
1569  (`!f:A->B->real s t.
1570       FINITE(s) /\ FINITE(t)
1571       ==> (sum s (\i. sum t (f i)) = sum t (\j. sum s (\i. f i j)))`,
1572   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
1573   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1574   SIMP_TAC[SUM_CLAUSES; SUM_0; SUM_ADD; ETA_AX]);;
1575
1576 let SUM_IMAGE = prove
1577  (`!f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
1578            ==> (sum (IMAGE f s) g = sum s (g o f))`,
1579   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1580   MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1581
1582 let SUM_SUPERSET = prove
1583  (`!f:A->real u v.
1584         u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = &0))
1585         ==> (sum v f = sum u f)`,
1586   SIMP_TAC[sum; GSYM NEUTRAL_REAL_ADD; ITERATE_SUPERSET; MONOIDAL_REAL_ADD]);;
1587
1588 let SUM_UNION_RZERO = prove
1589  (`!f:A->real u v.
1590         FINITE u /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = &0))
1591         ==> (sum (u UNION v) f = sum u f)`,
1592   let lemma = prove(`u UNION v = u UNION (v DIFF u)`,SET_TAC[]) in
1593   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[lemma] THEN
1594   MATCH_MP_TAC SUM_SUPERSET THEN
1595   ASM_MESON_TAC[IN_UNION; IN_DIFF; SUBSET]);;
1596
1597 let SUM_UNION_LZERO = prove
1598  (`!f:A->real u v.
1599         FINITE v /\ (!x. x IN u /\ ~(x IN v) ==> (f(x) = &0))
1600         ==> (sum (u UNION v) f = sum v f)`,
1601   MESON_TAC[SUM_UNION_RZERO; UNION_COMM]);;
1602
1603 let SUM_RESTRICT = prove
1604  (`!f s. FINITE s ==> (sum s (\x. if x IN s then f(x) else &0) = sum s f)`,
1605   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC[]);;
1606
1607 let SUM_BOUND = prove
1608  (`!s f b. FINITE s /\ (!x:A. x IN s ==> f(x) <= b)
1609            ==> sum s f <= &(CARD s) * b`,
1610   SIMP_TAC[GSYM SUM_CONST; SUM_LE]);;
1611
1612 let SUM_BOUND_GEN = prove
1613  (`!s f b. FINITE s /\ ~(s = {}) /\ (!x:A. x IN s ==> f(x) <= b / &(CARD s))
1614            ==> sum s f <= b`,
1615   MESON_TAC[SUM_BOUND; REAL_DIV_LMUL; REAL_OF_NUM_EQ; HAS_SIZE_0;
1616             HAS_SIZE]);;
1617
1618 let SUM_ABS_BOUND = prove
1619  (`!s f b. FINITE s /\ (!x:A. x IN s ==> abs(f(x)) <= b)
1620            ==> abs(sum s f) <= &(CARD s) * b`,
1621   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1622   EXISTS_TAC `sum s (\x:A. abs(f x))` THEN
1623   ASM_SIMP_TAC[SUM_BOUND; SUM_ABS]);;
1624
1625 let SUM_BOUND_LT = prove
1626  (`!s f b. FINITE s /\ (!x:A. x IN s ==> f x <= b) /\ (?x. x IN s /\ f x < b)
1627            ==> sum s f < &(CARD s) * b`,
1628   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
1629   EXISTS_TAC `sum s (\x:A. b)` THEN CONJ_TAC THENL
1630    [MATCH_MP_TAC SUM_LT THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
1631     ASM_SIMP_TAC[SUM_CONST; REAL_LE_REFL]]);;
1632
1633 let SUM_BOUND_LT_ALL = prove
1634  (`!s f b. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < b)
1635            ==> sum s f <  &(CARD s) * b`,
1636   MESON_TAC[MEMBER_NOT_EMPTY; REAL_LT_IMP_LE; SUM_BOUND_LT]);;
1637
1638 let SUM_BOUND_LT_GEN = prove
1639  (`!s f b. FINITE s /\ ~(s = {}) /\ (!x:A. x IN s ==> f(x) < b / &(CARD s))
1640            ==> sum s f < b`,
1641   MESON_TAC[SUM_BOUND_LT_ALL; REAL_DIV_LMUL; REAL_OF_NUM_EQ; HAS_SIZE_0;
1642             HAS_SIZE]);;
1643
1644 let SUM_UNION_EQ = prove
1645  (`!s t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
1646            ==> (sum s f + sum t f = sum u f)`,
1647   MESON_TAC[SUM_UNION; DISJOINT; FINITE_SUBSET; SUBSET_UNION]);;
1648
1649 let SUM_EQ_SUPERSET = prove
1650  (`!f s t:A->bool.
1651         FINITE t /\ t SUBSET s /\
1652         (!x. x IN t ==> (f x = g x)) /\
1653         (!x. x IN s /\ ~(x IN t) ==> (f(x) = &0))
1654         ==> (sum s f = sum t g)`,
1655   MESON_TAC[SUM_SUPERSET; SUM_EQ]);;
1656
1657 let SUM_RESTRICT_SET = prove
1658  (`!P s f. sum {x | x IN s /\ P x} f = sum s (\x. if P x then f x else &0)`,
1659   ONCE_REWRITE_TAC[GSYM SUM_SUPPORT] THEN
1660   REWRITE_TAC[support; NEUTRAL_REAL_ADD; IN_ELIM_THM] THEN
1661   REWRITE_TAC[MESON[] `~((if P x then f x else a) = a) <=> P x /\ ~(f x = a)`;
1662               GSYM CONJ_ASSOC] THEN
1663   REPEAT GEN_TAC THEN MATCH_MP_TAC SUM_EQ THEN SIMP_TAC[IN_ELIM_THM]);;
1664
1665 let SUM_SUM_RESTRICT = prove
1666  (`!R f s t.
1667         FINITE s /\ FINITE t
1668         ==> (sum s (\x. sum {y | y IN t /\ R x y} (\y. f x y)) =
1669              sum t (\y. sum {x | x IN s /\ R x y} (\x. f x y)))`,
1670   REPEAT GEN_TAC THEN SIMP_TAC[SUM_RESTRICT_SET] THEN
1671   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP SUM_SWAP th]));;
1672
1673 let CARD_EQ_SUM = prove
1674  (`!s. FINITE s ==> (&(CARD s) = sum s (\x. &1))`,
1675   SIMP_TAC[SUM_CONST; REAL_MUL_RID]);;
1676
1677 let SUM_MULTICOUNT_GEN = prove
1678  (`!R:A->B->bool s t k.
1679         FINITE s /\ FINITE t /\
1680         (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k(j)))
1681         ==> (sum s (\i. &(CARD {j | j IN t /\ R i j})) =
1682              sum t (\i. &(k i)))`,
1683   REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
1684   DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
1685   MATCH_MP_TAC EQ_TRANS THEN
1686   EXISTS_TAC `sum s (\i:A. sum {j:B | j IN t /\ R i j} (\j. &1))` THEN
1687   CONJ_TAC THENL
1688    [MATCH_MP_TAC SUM_EQ THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
1689     ASM_SIMP_TAC[CARD_EQ_SUM; FINITE_RESTRICT];
1690     FIRST_ASSUM(fun th ->
1691       ONCE_REWRITE_TAC[MATCH_MP SUM_SUM_RESTRICT th]) THEN
1692     MATCH_MP_TAC SUM_EQ THEN
1693     ASM_SIMP_TAC[SUM_CONST; FINITE_RESTRICT] THEN
1694     REWRITE_TAC[REAL_MUL_RID]]);;
1695
1696 let SUM_MULTICOUNT = prove
1697  (`!R:A->B->bool s t k.
1698         FINITE s /\ FINITE t /\
1699         (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k))
1700         ==> (sum s (\i. &(CARD {j | j IN t /\ R i j})) = &(k * CARD t))`,
1701   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1702   EXISTS_TAC `sum t (\i:B. &k)` THEN CONJ_TAC THENL
1703    [MATCH_MP_TAC SUM_MULTICOUNT_GEN THEN ASM_REWRITE_TAC[];
1704     ASM_SIMP_TAC[SUM_CONST; REAL_OF_NUM_MUL] THEN REWRITE_TAC[MULT_AC]]);;
1705
1706 let SUM_IMAGE_GEN = prove
1707  (`!f:A->B g s.
1708         FINITE s
1709         ==> (sum s g =
1710              sum (IMAGE f s) (\y. sum {x | x IN s /\ (f(x) = y)} g))`,
1711   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1712    `sum s (\x:A. sum {y:B | y IN IMAGE f s /\ (f x = y)} (\y. g x))` THEN
1713   CONJ_TAC THENL
1714    [MATCH_MP_TAC SUM_EQ THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:A` THEN
1715     DISCH_TAC THEN
1716     SUBGOAL_THEN `{y | y IN IMAGE (f:A->B) s /\ (f x = y)} = {(f x)}`
1717      (fun th -> REWRITE_TAC[th; SUM_SING; o_THM]) THEN
1718     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING; IN_IMAGE] THEN
1719     ASM_MESON_TAC[];
1720     GEN_REWRITE_TAC (funpow 2 RAND_CONV o ABS_CONV o RAND_CONV)
1721      [GSYM ETA_AX] THEN
1722     ASM_SIMP_TAC[SUM_SUM_RESTRICT; FINITE_IMAGE]]);;
1723
1724 let SUM_GROUP = prove
1725  (`!f:A->B g s t.
1726         FINITE s /\ IMAGE f s SUBSET t
1727         ==> sum t (\y. sum {x | x IN s /\ f(x) = y} g) = sum s g`,
1728   REPEAT STRIP_TAC THEN
1729   MP_TAC(ISPECL [`f:A->B`; `g:A->real`; `s:A->bool`] SUM_IMAGE_GEN) THEN
1730   ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
1731   MATCH_MP_TAC SUM_SUPERSET THEN ASM_REWRITE_TAC[] THEN
1732   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_EQ_0 THEN ASM SET_TAC[]);;
1733
1734 let REAL_OF_NUM_SUM = prove
1735  (`!f s. FINITE s ==> (&(nsum s f) = sum s (\x. &(f x)))`,
1736   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1737   SIMP_TAC[SUM_CLAUSES; NSUM_CLAUSES; GSYM REAL_OF_NUM_ADD]);;
1738
1739 let SUM_SUBSET = prove
1740  (`!u v f. FINITE u /\ FINITE v /\
1741            (!x. x IN (u DIFF v) ==> f(x) <= &0) /\
1742            (!x:A. x IN (v DIFF u) ==> &0 <= f(x))
1743            ==> sum u f <= sum v f`,
1744   REPEAT STRIP_TAC THEN
1745   MP_TAC(ISPECL [`f:A->real`; `u INTER v :A->bool`] SUM_UNION) THEN
1746   DISCH_THEN(fun th -> MP_TAC(SPEC `v DIFF u :A->bool` th) THEN
1747                        MP_TAC(SPEC `u DIFF v :A->bool` th)) THEN
1748   REWRITE_TAC[SET_RULE `(u INTER v) UNION (u DIFF v) = u`;
1749               SET_RULE `(u INTER v) UNION (v DIFF u) = v`] THEN
1750   ASM_SIMP_TAC[FINITE_DIFF; FINITE_INTER] THEN
1751   REPEAT(ANTS_TAC THENL [SET_TAC[]; DISCH_THEN SUBST1_TAC]) THEN
1752   MATCH_MP_TAC(REAL_ARITH `&0 <= --x /\ &0 <= y ==> a + x <= a + y`) THEN
1753   ASM_SIMP_TAC[GSYM SUM_NEG; FINITE_DIFF] THEN CONJ_TAC THEN
1754   MATCH_MP_TAC SUM_POS_LE THEN
1755   ASM_SIMP_TAC[FINITE_DIFF; REAL_LE_RNEG; REAL_ADD_LID]);;
1756
1757 let SUM_SUBSET_SIMPLE = prove
1758  (`!u v f. FINITE v /\ u SUBSET v /\ (!x:A. x IN (v DIFF u) ==> &0 <= f(x))
1759
1760            ==> sum u f <= sum v f`,
1761   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_SUBSET THEN
1762   ASM_MESON_TAC[IN_DIFF; SUBSET; FINITE_SUBSET]);;
1763
1764 let SUM_IMAGE_NONZERO = prove
1765  (`!d:B->real i:A->B s.
1766     FINITE s /\
1767     (!x y. x IN s /\ y IN s /\ ~(x = y) /\ i x = i y ==> d(i x) = &0)
1768     ==> sum (IMAGE i s) d = sum s (d o i)`,
1769   REWRITE_TAC[GSYM NEUTRAL_REAL_ADD; sum] THEN
1770   MATCH_MP_TAC ITERATE_IMAGE_NONZERO THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1771
1772 let SUM_BIJECTION = prove
1773  (`!f p s:A->bool.
1774                 (!x. x IN s ==> p(x) IN s) /\
1775                 (!y. y IN s ==> ?!x. x IN s /\ p(x) = y)
1776                 ==> sum s f = sum s (f o p)`,
1777   REWRITE_TAC[sum] THEN MATCH_MP_TAC ITERATE_BIJECTION THEN
1778   REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1779
1780 let SUM_SUM_PRODUCT = prove
1781  (`!s:A->bool t:A->B->bool x.
1782         FINITE s /\ (!i. i IN s ==> FINITE(t i))
1783         ==> sum s (\i. sum (t i) (x i)) =
1784             sum {i,j | i IN s /\ j IN t i} (\(i,j). x i j)`,
1785   REWRITE_TAC[sum] THEN MATCH_MP_TAC ITERATE_ITERATE_PRODUCT THEN
1786   REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1787
1788 let SUM_EQ_GENERAL = prove
1789  (`!s:A->bool t:B->bool f g h.
1790         (!y. y IN t ==> ?!x. x IN s /\ h(x) = y) /\
1791         (!x. x IN s ==> h(x) IN t /\ g(h x) = f x)
1792         ==> sum s f = sum t g`,
1793   REWRITE_TAC[sum] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL THEN
1794   REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1795
1796 let SUM_EQ_GENERAL_INVERSES = prove
1797  (`!s:A->bool t:B->bool f g h k.
1798         (!y. y IN t ==> k(y) IN s /\ h(k y) = y) /\
1799         (!x. x IN s ==> h(x) IN t /\ k(h x) = x /\ g(h x) = f x)
1800         ==> sum s f = sum t g`,
1801   REWRITE_TAC[sum] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL_INVERSES THEN
1802   REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1803
1804 let SUM_INJECTION = prove
1805  (`!f p s. FINITE s /\
1806            (!x. x IN s ==> p x IN s) /\
1807            (!x y. x IN s /\ y IN s /\ p x = p y ==> x = y)
1808            ==> sum s (f o p) = sum s f`,
1809   REWRITE_TAC[sum] THEN MATCH_MP_TAC ITERATE_INJECTION THEN
1810   REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1811
1812 let SUM_UNION_NONZERO = prove
1813  (`!f s t. FINITE s /\ FINITE t /\ (!x. x IN s INTER t ==> f(x) = &0)
1814            ==> sum (s UNION t) f = sum s f + sum t f`,
1815   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1816   MATCH_MP_TAC ITERATE_UNION_NONZERO THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1817
1818 let SUM_UNIONS_NONZERO = prove
1819  (`!f s. FINITE s /\ (!t:A->bool. t IN s ==> FINITE t) /\
1820          (!t1 t2 x. t1 IN s /\ t2 IN s /\ ~(t1 = t2) /\ x IN t1 /\ x IN t2
1821                     ==> f x = &0)
1822          ==> sum (UNIONS s) f = sum s (\t. sum t f)`,
1823   GEN_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN
1824   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1825   REWRITE_TAC[UNIONS_0; UNIONS_INSERT; SUM_CLAUSES; IN_INSERT] THEN
1826   MAP_EVERY X_GEN_TAC [`t:A->bool`; `s:(A->bool)->bool`] THEN
1827   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
1828   ONCE_REWRITE_TAC[IMP_CONJ] THEN ASM_SIMP_TAC[SUM_CLAUSES] THEN
1829   ANTS_TAC THENL  [ASM_MESON_TAC[]; DISCH_THEN(SUBST_ALL_TAC o SYM)] THEN
1830   STRIP_TAC THEN MATCH_MP_TAC SUM_UNION_NONZERO THEN
1831   ASM_SIMP_TAC[FINITE_UNIONS; IN_INTER; IN_UNIONS] THEN ASM_MESON_TAC[]);;
1832
1833 let SUM_CASES = prove
1834  (`!s P f g. FINITE s
1835              ==> sum s (\x:A. if P x then f x else g x) =
1836                  sum {x | x IN s /\ P x} f + sum {x | x IN s /\ ~P x} g`,
1837   REWRITE_TAC[sum; GSYM NEUTRAL_REAL_ADD] THEN
1838   MATCH_MP_TAC ITERATE_CASES THEN REWRITE_TAC[MONOIDAL_REAL_ADD]);;
1839
1840 let SUM_CASES_1 = prove
1841  (`!s a. FINITE s /\ a IN s
1842          ==> sum s (\x. if x = a then y else f(x)) = sum s f + (y - f a)`,
1843   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[SUM_CASES] THEN
1844   ASM_SIMP_TAC[GSYM DELETE; SUM_DELETE] THEN
1845   ASM_SIMP_TAC[SET_RULE `a IN s ==> {x | x IN s /\ x = a} = {a}`] THEN
1846   REWRITE_TAC[SUM_SING] THEN REAL_ARITH_TAC);;
1847
1848 let SUM_LE_INCLUDED = prove
1849  (`!f:A->real g:B->real s t i.
1850         FINITE s /\ FINITE t /\
1851         (!y. y IN t ==> &0 <= g y) /\
1852         (!x. x IN s ==> ?y. y IN t /\ i y = x /\ f(x) <= g(y))
1853         ==> sum s f <= sum t g`,
1854   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1855   EXISTS_TAC `sum (IMAGE (i:B->A) t) (\y. sum {x | x IN t /\ i x = y} g)` THEN
1856   CONJ_TAC THENL
1857    [ALL_TAC;
1858     MATCH_MP_TAC REAL_EQ_IMP_LE THEN
1859     MATCH_MP_TAC(GSYM SUM_IMAGE_GEN) THEN ASM_REWRITE_TAC[]] THEN
1860   MATCH_MP_TAC REAL_LE_TRANS THEN
1861   EXISTS_TAC `sum s (\y. sum {x | x IN t /\ (i:B->A) x = y} g)` THEN
1862   CONJ_TAC THENL
1863    [MATCH_MP_TAC SUM_LE THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:A` THEN
1864     DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN
1865     ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `y:B` THEN
1866     STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1867     EXISTS_TAC `sum {y:B} g` THEN CONJ_TAC THENL
1868      [ASM_REWRITE_TAC[SUM_SING]; ALL_TAC];
1869     ALL_TAC] THEN
1870   MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN
1871   ASM_SIMP_TAC[SUM_POS_LE; FINITE_RESTRICT; IN_ELIM_THM] THEN
1872   ASM SET_TAC[]);;
1873
1874 let SUM_IMAGE_LE = prove
1875  (`!f:A->B g s.
1876         FINITE s /\
1877         (!x. x IN s ==> &0 <= g(f x))
1878         ==> sum (IMAGE f s) g <= sum s (g o f)`,
1879   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_LE_INCLUDED THEN
1880   ASM_SIMP_TAC[FINITE_IMAGE; FORALL_IN_IMAGE] THEN
1881   ASM_REWRITE_TAC[o_THM] THEN EXISTS_TAC `f:A->B` THEN
1882   MESON_TAC[REAL_LE_REFL]);;
1883
1884 let SUM_CLOSED = prove
1885  (`!P f:A->real s.
1886         P(&0) /\ (!x y. P x /\ P y ==> P(x + y)) /\ (!a. a IN s ==> P(f a))
1887         ==> P(sum s f)`,
1888   REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_REAL_ADD) THEN
1889   DISCH_THEN(MP_TAC o SPEC `P:real->bool`) THEN
1890   ASM_SIMP_TAC[NEUTRAL_REAL_ADD; GSYM sum]);;
1891
1892 (* ------------------------------------------------------------------------- *)
1893 (* Specialize them to sums over intervals of numbers.                        *)
1894 (* ------------------------------------------------------------------------- *)
1895
1896 let SUM_ADD_NUMSEG = prove
1897  (`!f g m n. sum(m..n) (\i. f(i) + g(i)) = sum(m..n) f + sum(m..n) g`,
1898   SIMP_TAC[SUM_ADD; FINITE_NUMSEG]);;
1899
1900 let SUM_SUB_NUMSEG = prove
1901  (`!f g m n. sum(m..n) (\i. f(i) - g(i)) = sum(m..n) f - sum(m..n) g`,
1902    SIMP_TAC[SUM_SUB; FINITE_NUMSEG]);;
1903
1904 let SUM_LE_NUMSEG = prove
1905  (`!f g m n. (!i. m <= i /\ i <= n ==> f(i) <= g(i))
1906              ==> sum(m..n) f <= sum(m..n) g`,
1907   SIMP_TAC[SUM_LE; FINITE_NUMSEG; IN_NUMSEG]);;
1908
1909 let SUM_EQ_NUMSEG = prove
1910  (`!f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
1911              ==> (sum(m..n) f = sum(m..n) g)`,
1912   MESON_TAC[SUM_EQ; FINITE_NUMSEG; IN_NUMSEG]);;
1913
1914 let SUM_ABS_NUMSEG = prove
1915  (`!f m n. abs(sum(m..n) f) <= sum(m..n) (\i. abs(f i))`,
1916   SIMP_TAC[SUM_ABS; FINITE_NUMSEG]);;
1917
1918 let SUM_CONST_NUMSEG = prove
1919  (`!c m n. sum(m..n) (\n. c) = &((n + 1) - m) * c`,
1920   SIMP_TAC[SUM_CONST; FINITE_NUMSEG; CARD_NUMSEG]);;
1921
1922 let SUM_EQ_0_NUMSEG = prove
1923  (`!f m n. (!i. m <= i /\ i <= n ==> (f(i) = &0)) ==> (sum(m..n) f = &0)`,
1924   SIMP_TAC[SUM_EQ_0; IN_NUMSEG]);;
1925
1926 let SUM_TRIV_NUMSEG = prove
1927  (`!f m n. n < m ==> (sum(m..n) f = &0)`,
1928   MESON_TAC[SUM_EQ_0_NUMSEG; LE_TRANS; NOT_LT]);;
1929
1930 let SUM_POS_LE_NUMSEG = prove
1931  (`!m n f. (!p. m <= p /\ p <= n ==> &0 <= f(p)) ==> &0 <= sum(m..n) f`,
1932   SIMP_TAC[SUM_POS_LE; FINITE_NUMSEG; IN_NUMSEG]);;
1933
1934 let SUM_POS_EQ_0_NUMSEG = prove
1935  (`!f m n. (!p. m <= p /\ p <= n ==> &0 <= f(p)) /\ (sum(m..n) f = &0)
1936            ==> !p. m <= p /\ p <= n ==> (f(p) = &0)`,
1937   MESON_TAC[SUM_POS_EQ_0; FINITE_NUMSEG; IN_NUMSEG]);;
1938
1939 let SUM_SING_NUMSEG = prove
1940  (`!f n. sum(n..n) f = f(n)`,
1941   SIMP_TAC[SUM_SING; NUMSEG_SING]);;
1942
1943 let SUM_CLAUSES_NUMSEG = prove
1944  (`(!m. sum(m..0) f = if m = 0 then f(0) else &0) /\
1945    (!m n. sum(m..SUC n) f = if m <= SUC n then sum(m..n) f + f(SUC n)
1946                             else sum(m..n) f)`,
1947   MP_TAC(MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_REAL_ADD) THEN
1948   REWRITE_TAC[NEUTRAL_REAL_ADD; sum]);;
1949
1950 let SUM_SWAP_NUMSEG = prove
1951  (`!a b c d f.
1952      sum(a..b) (\i. sum(c..d) (f i)) = sum(c..d) (\j. sum(a..b) (\i. f i j))`,
1953   REPEAT GEN_TAC THEN MATCH_MP_TAC SUM_SWAP THEN
1954   REWRITE_TAC[FINITE_NUMSEG]);;
1955
1956 let SUM_ADD_SPLIT = prove
1957  (`!f m n p.
1958         m <= n + 1 ==> (sum (m..(n+p)) f = sum(m..n) f + sum(n+1..n+p) f)`,
1959   SIMP_TAC[NUMSEG_ADD_SPLIT; SUM_UNION; DISJOINT_NUMSEG; FINITE_NUMSEG;
1960            ARITH_RULE `x < x + 1`]);;
1961
1962 let SUM_OFFSET = prove
1963  (`!p f m n. sum(m+p..n+p) f = sum(m..n) (\i. f(i + p))`,
1964   SIMP_TAC[NUMSEG_OFFSET_IMAGE; SUM_IMAGE;
1965            EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
1966   REWRITE_TAC[o_DEF]);;
1967
1968 let SUM_OFFSET_0 = prove
1969  (`!f m n. m <= n ==> (sum(m..n) f = sum(0..n-m) (\i. f(i + m)))`,
1970   SIMP_TAC[GSYM SUM_OFFSET; ADD_CLAUSES; SUB_ADD]);;
1971
1972 let SUM_CLAUSES_LEFT = prove
1973  (`!f m n. m <= n ==> sum(m..n) f = f(m) + sum(m+1..n) f`,
1974   SIMP_TAC[GSYM NUMSEG_LREC; SUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
1975   ARITH_TAC);;
1976
1977 let SUM_CLAUSES_RIGHT = prove
1978  (`!f m n. 0 < n /\ m <= n ==> sum(m..n) f = sum(m..n-1) f + f(n)`,
1979   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1980   SIMP_TAC[LT_REFL; SUM_CLAUSES_NUMSEG; SUC_SUB1]);;
1981
1982 let SUM_PAIR = prove
1983  (`!f m n. sum(2*m..2*n+1) f = sum(m..n) (\i. f(2*i) + f(2*i+1))`,
1984   MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_REAL_ADD) THEN
1985   REWRITE_TAC[sum; NEUTRAL_REAL_ADD]);;
1986
1987 let REAL_OF_NUM_SUM_NUMSEG = prove
1988  (`!f m n. (&(nsum(m..n) f) = sum (m..n) (\i. &(f i)))`,
1989   SIMP_TAC[REAL_OF_NUM_SUM; FINITE_NUMSEG]);;
1990
1991 (* ------------------------------------------------------------------------- *)
1992 (* Partial summation and other theorems specific to number segments.         *)
1993 (* ------------------------------------------------------------------------- *)
1994
1995 let SUM_PARTIAL_SUC = prove
1996  (`!f g m n.
1997         sum (m..n) (\k. f(k) * (g(k + 1) - g(k))) =
1998             if m <= n then f(n + 1) * g(n + 1) - f(m) * g(m) -
1999                            sum (m..n) (\k. g(k + 1) * (f(k + 1) - f(k)))
2000             else &0`,
2001   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
2002   COND_CASES_TAC THEN ASM_SIMP_TAC[SUM_TRIV_NUMSEG; GSYM NOT_LE] THEN
2003   ASM_REWRITE_TAC[SUM_CLAUSES_NUMSEG] THENL
2004    [COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL [REAL_ARITH_TAC; ASM_ARITH_TAC];
2005     ALL_TAC] THEN
2006   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE]) THEN
2007   DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
2008   ASM_SIMP_TAC[GSYM NOT_LT; SUM_TRIV_NUMSEG; ARITH_RULE `n < SUC n`] THEN
2009   ASM_SIMP_TAC[GSYM ADD1; ADD_CLAUSES] THEN REAL_ARITH_TAC);;
2010
2011 let SUM_PARTIAL_PRE = prove
2012  (`!f g m n.
2013         sum (m..n) (\k. f(k) * (g(k) - g(k - 1))) =
2014             if m <= n then f(n + 1) * g(n) - f(m) * g(m - 1) -
2015                            sum (m..n) (\k. g k * (f(k + 1) - f(k)))
2016             else &0`,
2017   REPEAT GEN_TAC THEN
2018   MP_TAC(ISPECL [`f:num->real`; `\k. (g:num->real)(k - 1)`;
2019                  `m:num`; `n:num`] SUM_PARTIAL_SUC) THEN
2020   REWRITE_TAC[ADD_SUB] THEN DISCH_THEN SUBST1_TAC THEN
2021   COND_CASES_TAC THEN REWRITE_TAC[]);;
2022
2023 let SUM_DIFFS = prove
2024  (`!m n. sum(m..n) (\k. f(k) - f(k + 1)) =
2025           if m <= n then f(m) - f(n + 1) else &0`,
2026   ONCE_REWRITE_TAC[REAL_ARITH `a - b = -- &1 * (b - a)`] THEN
2027   ONCE_REWRITE_TAC[SUM_PARTIAL_SUC] THEN
2028   REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO; SUM_0] THEN
2029   REAL_ARITH_TAC);;
2030
2031 let SUM_DIFFS_ALT = prove
2032  (`!m n. sum(m..n) (\k. f(k + 1) - f(k)) =
2033           if m <= n then f(n + 1) - f(m) else &0`,
2034   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NEG_SUB] THEN
2035   SIMP_TAC[SUM_NEG; SUM_DIFFS] THEN
2036   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_NEG_SUB; REAL_NEG_0]);;
2037
2038 let SUM_COMBINE_R = prove
2039  (`!f m n p. m <= n + 1 /\ n <= p
2040              ==> sum(m..n) f + sum(n+1..p) f = sum(m..p) f`,
2041   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_UNION_EQ THEN
2042   REWRITE_TAC[FINITE_NUMSEG; EXTENSION; IN_INTER; IN_UNION; NOT_IN_EMPTY;
2043               IN_NUMSEG] THEN
2044   ASM_ARITH_TAC);;
2045
2046 let SUM_COMBINE_L = prove
2047  (`!f m n p. 0 < n /\ m <= n /\ n <= p + 1
2048              ==> sum(m..n-1) f + sum(n..p) f = sum(m..p) f`,
2049   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_UNION_EQ THEN
2050   REWRITE_TAC[FINITE_NUMSEG; EXTENSION; IN_INTER; IN_UNION; NOT_IN_EMPTY;
2051               IN_NUMSEG] THEN
2052   ASM_ARITH_TAC);;
2053
2054 (* ------------------------------------------------------------------------- *)
2055 (* Extend congruences to deal with sum. Note that we must have the eta       *)
2056 (* redex or we'll get a loop since f(x) will lambda-reduce recursively.      *)
2057 (* ------------------------------------------------------------------------- *)
2058
2059 let th = prove
2060  (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
2061               ==> sum s (\i. f(i)) = sum s g) /\
2062    (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
2063               ==> sum(a..b) (\i. f(i)) = sum(a..b) g) /\
2064    (!f g p.   (!x. p x ==> f x = g x)
2065               ==> sum {y | p y} (\i. f(i)) = sum {y | p y} g)`,
2066   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUM_EQ THEN
2067   ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
2068   extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;
2069
2070 (* ------------------------------------------------------------------------- *)
2071 (* Expand "sum (m..n) f" where m and n are numerals.                         *)
2072 (* ------------------------------------------------------------------------- *)
2073
2074 let EXPAND_SUM_CONV =
2075   let [pth_0; pth_1; pth_2] = (CONJUNCTS o prove)
2076    (`(n < m ==> sum(m..n) f = &0) /\
2077      sum(m..m) f = f m /\
2078      (m <= n ==> sum (m..n) f = f m + sum (m + 1..n) f)`,
2079     REWRITE_TAC[SUM_CLAUSES_LEFT; SUM_SING_NUMSEG; SUM_TRIV_NUMSEG])
2080   and ns_tm = `..` and f_tm = `f:num->real`
2081   and m_tm = `m:num` and n_tm = `n:num` in
2082   let rec conv tm =
2083     let smn,ftm = dest_comb tm in
2084     let s,mn = dest_comb smn in
2085     if not(is_const s & fst(dest_const s) = "sum")
2086     then failwith "EXPAND_SUM_CONV" else
2087     let mtm,ntm = dest_binop ns_tm mn in
2088     let m = dest_numeral mtm and n = dest_numeral ntm in
2089     if n < m then
2090       let th1 = INST [ftm,f_tm; mtm,m_tm; ntm,n_tm] pth_0 in
2091       MP th1 (EQT_ELIM(NUM_LT_CONV(lhand(concl th1))))
2092     else if n = m then CONV_RULE (RAND_CONV(TRY_CONV BETA_CONV))
2093                                  (INST [ftm,f_tm; mtm,m_tm] pth_1)
2094     else
2095       let th1 = INST [ftm,f_tm; mtm,m_tm; ntm,n_tm] pth_2 in
2096       let th2 = MP th1 (EQT_ELIM(NUM_LE_CONV(lhand(concl th1)))) in
2097       CONV_RULE (RAND_CONV(COMB2_CONV (RAND_CONV(TRY_CONV BETA_CONV))
2098        (LAND_CONV(LAND_CONV NUM_ADD_CONV) THENC conv))) th2 in
2099   conv;;
2100
2101 (* ------------------------------------------------------------------------- *)
2102 (* Some special algebraic rearrangements.                                    *)
2103 (* ------------------------------------------------------------------------- *)
2104
2105 let REAL_SUB_POW = prove
2106  (`!x y n.
2107         1 <= n ==> x pow n - y pow n =
2108                    (x - y) * sum(0..n-1) (\i. x pow i * y pow (n - 1 - i))`,
2109   REWRITE_TAC[GSYM SUM_LMUL] THEN
2110   REWRITE_TAC[REAL_ARITH
2111    `(x - y) * (a * b):real = (x * a) * b - a * (y * b)`] THEN
2112   SIMP_TAC[GSYM real_pow; ADD1; ARITH_RULE
2113     `1 <= n /\ x <= n - 1
2114      ==> n - 1 - x = n - (x + 1) /\ SUC(n - 1 - x) = n - x`] THEN
2115   REWRITE_TAC[SUM_DIFFS_ALT; LE_0] THEN
2116   SIMP_TAC[SUB_0; SUB_ADD; SUB_REFL; real_pow; REAL_MUL_LID; REAL_MUL_RID]);;
2117
2118 let REAL_SUB_POW_R1 = prove
2119  (`!x n. 1 <= n ==> x pow n - &1 = (x - &1) * sum(0..n-1) (\i. x pow i)`,
2120   REPEAT GEN_TAC THEN
2121   DISCH_THEN(MP_TAC o SPECL [`x:real`; `&1`] o MATCH_MP REAL_SUB_POW) THEN
2122   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_RID]);;
2123
2124 let REAL_SUB_POW_L1 = prove
2125  (`!x n. 1 <= n ==> &1 - x pow n = (&1 - x) * sum(0..n-1) (\i. x pow i)`,
2126   ONCE_REWRITE_TAC[GSYM REAL_NEG_SUB] THEN
2127   SIMP_TAC[REAL_SUB_POW_R1] THEN REWRITE_TAC[REAL_MUL_LNEG]);;
2128
2129 (* ------------------------------------------------------------------------- *)
2130 (* Some useful facts about real polynomial functions.                        *)
2131 (* ------------------------------------------------------------------------- *)
2132
2133 let REAL_SUB_POLYFUN = prove
2134  (`!a x y n.
2135     1 <= n
2136     ==> sum(0..n) (\i. a i * x pow i) - sum(0..n) (\i. a i * y pow i) =
2137         (x - y) *
2138         sum(0..n-1) (\j. sum(j+1..n) (\i. a i * y pow (i - j - 1)) * x pow j)`,
2139   REPEAT STRIP_TAC THEN
2140   REWRITE_TAC[GSYM SUM_SUB_NUMSEG; GSYM REAL_SUB_LDISTRIB] THEN
2141   GEN_REWRITE_TAC LAND_CONV [MATCH_MP SUM_CLAUSES_LEFT (SPEC_ALL LE_0)] THEN
2142   REWRITE_TAC[REAL_SUB_REFL; real_pow; REAL_MUL_RZERO; REAL_ADD_LID] THEN
2143   SIMP_TAC[REAL_SUB_POW; ADD_CLAUSES] THEN
2144   ONCE_REWRITE_TAC[REAL_ARITH `a * x * s:real = x * a * s`] THEN
2145   REWRITE_TAC[SUM_LMUL] THEN AP_TERM_TAC THEN
2146   SIMP_TAC[GSYM SUM_LMUL; GSYM SUM_RMUL; SUM_SUM_PRODUCT; FINITE_NUMSEG] THEN
2147   MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
2148   REPEAT(EXISTS_TAC `\(x:num,y:num). (y,x)`) THEN
2149   REWRITE_TAC[FORALL_IN_GSPEC; IN_ELIM_PAIR_THM; IN_NUMSEG] THEN
2150   REWRITE_TAC[ARITH_RULE `a - b - c:num = a - (b + c)`; ADD_SYM] THEN
2151   REWRITE_TAC[REAL_MUL_AC] THEN ARITH_TAC);;
2152
2153 let REAL_SUB_POLYFUN_ALT = prove
2154  (`!a x y n.
2155     1 <= n
2156     ==> sum(0..n) (\i. a i * x pow i) - sum(0..n) (\i. a i * y pow i) =
2157         (x - y) *
2158         sum(0..n-1) (\j. sum(0..n-j-1) (\k. a(j+k+1) * y pow k) * x pow j)`,
2159   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[REAL_SUB_POLYFUN] THEN AP_TERM_TAC THEN
2160   MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `j:num` THEN REPEAT STRIP_TAC THEN
2161   REWRITE_TAC[] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2162   MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
2163   MAP_EVERY EXISTS_TAC
2164    [`\i. i - (j + 1)`; `\k. j + k + 1`] THEN
2165   REWRITE_TAC[IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
2166   TRY(BINOP_TAC THEN AP_TERM_TAC) THEN ASM_ARITH_TAC);;
2167
2168 let REAL_POLYFUN_ROOTBOUND = prove
2169  (`!n c. ~(!i. i IN 0..n ==> c i = &0)
2170          ==> FINITE {x | sum(0..n) (\i. c i * x pow i) = &0} /\
2171              CARD {x | sum(0..n) (\i. c i * x pow i) = &0} <= n`,
2172   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN INDUCT_TAC THENL
2173    [REWRITE_TAC[NUMSEG_SING; IN_SING; UNWIND_THM2; SUM_CLAUSES_NUMSEG] THEN
2174     SIMP_TAC[real_pow; REAL_MUL_RID; EMPTY_GSPEC; CARD_CLAUSES; FINITE_EMPTY;
2175              LE_REFL];
2176     X_GEN_TAC `c:num->real` THEN REWRITE_TAC[IN_NUMSEG] THEN
2177     DISCH_TAC THEN ASM_CASES_TAC `(c:num->real) (SUC n) = &0` THENL
2178      [ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG; LE_0; REAL_MUL_LZERO; REAL_ADD_RID] THEN
2179       REWRITE_TAC[LE; LEFT_OR_DISTRIB] THEN DISJ2_TAC THEN
2180       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[IN_NUMSEG; LE];
2181       ASM_CASES_TAC `{x | sum (0..SUC n) (\i. c i * x pow i) = &0} = {}` THEN
2182       ASM_REWRITE_TAC[FINITE_RULES; CARD_CLAUSES; LE_0] THEN
2183       FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
2184       REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
2185       X_GEN_TAC `r:real` THEN DISCH_TAC THEN
2186       MP_TAC(GEN `x:real` (ISPECL [`c:num->real`; `x:real`; `r:real`; `SUC n`]
2187         REAL_SUB_POLYFUN)) THEN
2188       ASM_REWRITE_TAC[ARITH_RULE `1 <= SUC n`; REAL_SUB_RZERO] THEN
2189       DISCH_THEN(fun th -> REWRITE_TAC[th; REAL_ENTIRE; REAL_SUB_0]) THEN
2190       REWRITE_TAC[SET_RULE `{x | x = c \/ P x} = c INSERT {x | P x}`] THEN
2191       MATCH_MP_TAC(MESON[FINITE_INSERT; CARD_CLAUSES;
2192                          ARITH_RULE `x <= n ==> SUC x <= SUC n /\ x <= SUC n`]
2193         `FINITE s /\ CARD s <= n
2194          ==> FINITE(r INSERT s) /\ CARD(r INSERT s) <= SUC n`) THEN
2195       REWRITE_TAC[SUC_SUB1] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
2196       EXISTS_TAC `n:num` THEN REWRITE_TAC[IN_NUMSEG; ADD1; LE_REFL; LE_0] THEN
2197       REWRITE_TAC[SUM_SING_NUMSEG; ARITH_RULE `(n + 1) - n - 1 = 0`] THEN
2198       ASM_REWRITE_TAC[GSYM ADD1; real_pow; REAL_MUL_RID]]]);;
2199
2200 let REAL_POLYFUN_FINITE_ROOTS = prove
2201  (`!n c. FINITE {x | sum(0..n) (\i. c i * x pow i) = &0} <=>
2202          ?i. i IN 0..n /\ ~(c i = &0)`,
2203   REPEAT GEN_TAC THEN REWRITE_TAC[TAUT `a /\ ~b <=> ~(a ==> b)`] THEN
2204   REWRITE_TAC[GSYM NOT_FORALL_THM] THEN EQ_TAC THEN
2205   SIMP_TAC[REAL_POLYFUN_ROOTBOUND] THEN
2206   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
2207   SIMP_TAC[REAL_MUL_LZERO; SUM_0] THEN
2208   REWRITE_TAC[SET_RULE `{x | T} = (:real)`; real_INFINITE; GSYM INFINITE]);;
2209
2210 let REAL_POLYFUN_EQ_0 = prove
2211  (`!n c. (!x. sum(0..n) (\i. c i * x pow i) = &0) <=>
2212          (!i. i IN 0..n ==> c i = &0)`,
2213   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
2214    [GEN_REWRITE_TAC I [TAUT `p <=> ~ ~p`] THEN DISCH_THEN(MP_TAC o MATCH_MP
2215      REAL_POLYFUN_ROOTBOUND) THEN
2216     ASM_REWRITE_TAC[real_INFINITE; GSYM INFINITE; DE_MORGAN_THM;
2217                     SET_RULE `{x | T} = (:real)`];
2218     ASM_SIMP_TAC[IN_NUMSEG; LE_0; REAL_MUL_LZERO; SUM_0]]);;
2219
2220 let REAL_POLYFUN_EQ_CONST = prove
2221  (`!n c k. (!x. sum(0..n) (\i. c i * x pow i) = k) <=>
2222            c 0 = k /\ (!i. i IN 1..n ==> c i = &0)`,
2223   REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
2224    `!x. sum(0..n) (\i. (if i = 0 then c 0 - k else c i) * x pow i) = &0` THEN
2225   CONJ_TAC THENL
2226    [SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; real_pow; REAL_MUL_RID] THEN
2227     REWRITE_TAC[REAL_ARITH `(c - k) + s = &0 <=> c + s = k`] THEN
2228     AP_TERM_TAC THEN ABS_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2229     AP_TERM_TAC THEN MATCH_MP_TAC SUM_EQ THEN GEN_TAC THEN
2230     REWRITE_TAC[IN_NUMSEG] THEN
2231     COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH];
2232     REWRITE_TAC[REAL_POLYFUN_EQ_0; IN_NUMSEG; LE_0] THEN
2233     GEN_REWRITE_TAC LAND_CONV [MESON[]
2234      `(!n. P n) <=> P 0 /\ (!n. ~(n = 0) ==> P n)`] THEN
2235     SIMP_TAC[LE_0; REAL_SUB_0] THEN MESON_TAC[LE_1]]);;
2236
2237 (* ------------------------------------------------------------------------- *)
2238 (* A general notion of polynomial function.                                  *)
2239 (* ------------------------------------------------------------------------- *)
2240
2241 let polynomial_function = new_definition
2242  `polynomial_function p <=> ?m c. !x. p x = sum(0..m) (\i. c i * x pow i)`;;
2243
2244 let POLYNOMIAL_FUNCTION_CONST = prove
2245  (`!c. polynomial_function (\x. c)`,
2246   GEN_TAC THEN REWRITE_TAC[polynomial_function] THEN
2247   MAP_EVERY EXISTS_TAC [`0`; `(\i. c):num->real`] THEN
2248   REWRITE_TAC[SUM_SING_NUMSEG; real_pow; REAL_MUL_RID]);;
2249
2250 let POLYNOMIAL_FUNCTION_ID = prove
2251  (`polynomial_function (\x. x)`,
2252   REWRITE_TAC[polynomial_function] THEN
2253   MAP_EVERY EXISTS_TAC [`SUC 0`; `\i. if i = 1 then &1 else &0`] THEN
2254   REWRITE_TAC[SUM_CLAUSES_NUMSEG; LE_0; ARITH] THEN REAL_ARITH_TAC);;
2255
2256 let POLYNOMIAL_FUNCTION_I = prove
2257  (`polynomial_function I`,
2258   REWRITE_TAC[I_DEF; POLYNOMIAL_FUNCTION_ID]);;
2259
2260 let POLYNOMIAL_FUNCTION_ADD = prove
2261  (`!p q. polynomial_function p /\ polynomial_function q
2262          ==> polynomial_function (\x. p x + q x)`,
2263   REPEAT GEN_TAC THEN
2264   REWRITE_TAC[IMP_CONJ; polynomial_function; LEFT_IMP_EXISTS_THM] THEN
2265   MAP_EVERY X_GEN_TAC  [`m:num`; `a:num->real`] THEN STRIP_TAC THEN
2266   MAP_EVERY X_GEN_TAC [`n:num`; `b:num->real`] THEN STRIP_TAC THEN
2267   ASM_REWRITE_TAC[] THEN EXISTS_TAC `MAX m n` THEN EXISTS_TAC
2268    `\i:num. (if i <= m then a i else &0) + (if i <= n then b i else &0)` THEN
2269   GEN_TAC THEN REWRITE_TAC[REAL_ADD_RDISTRIB; SUM_ADD_NUMSEG] THEN
2270   REWRITE_TAC[COND_RAND; COND_RATOR; REAL_MUL_LZERO] THEN
2271   REWRITE_TAC[GSYM SUM_RESTRICT_SET] THEN BINOP_TAC THEN
2272   BINOP_TAC THEN REWRITE_TAC[] THEN
2273   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_NUMSEG] THEN ARITH_TAC);;
2274
2275 let POLYNOMIAL_FUNCTION_LMUL = prove
2276  (`!p c. polynomial_function p ==> polynomial_function (\x. c * p x)`,
2277   REPEAT GEN_TAC THEN
2278   REWRITE_TAC[IMP_CONJ; polynomial_function; LEFT_IMP_EXISTS_THM] THEN
2279   MAP_EVERY X_GEN_TAC  [`n:num`; `a:num->real`] THEN STRIP_TAC THEN
2280   MAP_EVERY EXISTS_TAC [`n:num`; `\i. c * (a:num->real) i`] THEN
2281   ASM_REWRITE_TAC[SUM_LMUL; GSYM REAL_MUL_ASSOC]);;
2282
2283 let POLYNOMIAL_FUNCTION_RMUL = prove
2284  (`!p c. polynomial_function p ==> polynomial_function (\x. p x * c)`,
2285   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[POLYNOMIAL_FUNCTION_LMUL]);;
2286
2287 let POLYNOMIAL_FUNCTION_NEG = prove
2288  (`!p. polynomial_function(\x. --(p x)) <=> polynomial_function p`,
2289   GEN_TAC THEN EQ_TAC THEN
2290   DISCH_THEN(MP_TAC o SPEC `--(&1)` o MATCH_MP POLYNOMIAL_FUNCTION_LMUL) THEN
2291   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_LID; ETA_AX; REAL_NEG_NEG]);;
2292
2293 let POLYNOMIAL_FUNCTION_SUB = prove
2294  (`!p q. polynomial_function p /\ polynomial_function q
2295          ==> polynomial_function (\x. p x - q x)`,
2296   SIMP_TAC[real_sub; POLYNOMIAL_FUNCTION_NEG; POLYNOMIAL_FUNCTION_ADD]);;
2297
2298 let POLYNOMIAL_FUNCTION_MUL = prove
2299  (`!p q. polynomial_function p /\ polynomial_function q
2300          ==> polynomial_function (\x. p x * q x)`,
2301   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
2302   GEN_TAC THEN DISCH_TAC THEN
2303   GEN_REWRITE_TAC (BINDER_CONV o LAND_CONV) [polynomial_function] THEN
2304   SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
2305   ONCE_REWRITE_TAC[MESON[] `(!q m c. P q m c) <=> (!m c q. P q m c)`] THEN
2306   ONCE_REWRITE_TAC[GSYM FUN_EQ_THM] THEN
2307   REWRITE_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
2308   INDUCT_TAC THEN
2309   ASM_SIMP_TAC[SUM_SING_NUMSEG; real_pow; POLYNOMIAL_FUNCTION_RMUL] THEN
2310   X_GEN_TAC `c:num->real` THEN SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; ADD1] THEN
2311   REWRITE_TAC[REAL_ADD_LDISTRIB; real_pow] THEN
2312   MATCH_MP_TAC POLYNOMIAL_FUNCTION_ADD THEN
2313   ASM_SIMP_TAC[POLYNOMIAL_FUNCTION_RMUL] THEN
2314   REWRITE_TAC[SPEC `1` SUM_OFFSET] THEN
2315   REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; REAL_MUL_ASSOC; SUM_RMUL] THEN
2316   FIRST_X_ASSUM(MP_TAC o SPEC `\i. (c:num->real)(i + 1)`) THEN
2317   ABBREV_TAC `q = \x. p x * sum (0..m) (\i. c (i + 1) * x pow i)` THEN
2318   RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM]) THEN ASM_REWRITE_TAC[] THEN
2319   REWRITE_TAC[polynomial_function; LEFT_IMP_EXISTS_THM] THEN
2320   MAP_EVERY X_GEN_TAC [`n:num`; `a:num->real`] THEN STRIP_TAC THEN
2321   EXISTS_TAC `n + 1` THEN
2322   EXISTS_TAC `\i. if i = 0 then &0 else (a:num->real)(i - 1)` THEN
2323   SIMP_TAC[SUM_CLAUSES_LEFT; LE_0] THEN
2324   ASM_REWRITE_TAC[SPEC `1` SUM_OFFSET; ADD_EQ_0; ARITH_EQ; ADD_SUB] THEN
2325   REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC; SUM_RMUL] THEN REAL_ARITH_TAC);;
2326
2327 let POLYNOMIAL_FUNCTION_SUM = prove
2328  (`!s:A->bool p.
2329         FINITE s /\ (!i. i IN s ==> polynomial_function(\x. p x i))
2330         ==> polynomial_function (\x. sum s (p x))`,
2331   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
2332   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2333   SIMP_TAC[SUM_CLAUSES; POLYNOMIAL_FUNCTION_CONST] THEN
2334   SIMP_TAC[FORALL_IN_INSERT; POLYNOMIAL_FUNCTION_ADD]);;
2335
2336 let POLYNOMIAL_FUNCTION_POW = prove
2337  (`!p n. polynomial_function p ==> polynomial_function (\x. p x pow n)`,
2338   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
2339   INDUCT_TAC THEN
2340   ASM_SIMP_TAC[real_pow; POLYNOMIAL_FUNCTION_CONST; POLYNOMIAL_FUNCTION_MUL]);;
2341
2342 let POLYNOMIAL_FUNCTION_INDUCT = prove
2343  (`!P. P (\x. x) /\ (!c. P (\x. c)) /\
2344       (!p q. P p /\ P q ==> P (\x. p x + q x)) /\
2345       (!p q. P p /\ P q ==> P (\x. p x * q x))
2346       ==> !p. polynomial_function p ==> P p`,
2347   GEN_TAC THEN STRIP_TAC THEN
2348   REWRITE_TAC[polynomial_function; LEFT_IMP_EXISTS_THM] THEN
2349   ONCE_REWRITE_TAC[MESON[] `(!q m c. P q m c) <=> (!m c q. P q m c)`] THEN
2350   ONCE_REWRITE_TAC[GSYM FUN_EQ_THM] THEN
2351   SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN INDUCT_TAC THEN
2352   ASM_REWRITE_TAC[SUM_SING_NUMSEG; real_pow] THEN
2353   GEN_TAC THEN SIMP_TAC[SUM_CLAUSES_LEFT; ADD1; LE_0] THEN
2354   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[real_pow] THEN
2355   REWRITE_TAC[SPEC `1` SUM_OFFSET] THEN
2356   REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; REAL_MUL_ASSOC; SUM_RMUL] THEN
2357   ASM_SIMP_TAC[]);;
2358
2359 let POLYNOMIAL_FUNCTION_o = prove
2360  (`!p q. polynomial_function p /\ polynomial_function q
2361          ==> polynomial_function (p o q)`,
2362   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
2363   REWRITE_TAC[IMP_CONJ_ALT; RIGHT_FORALL_IMP_THM] THEN
2364   GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC POLYNOMIAL_FUNCTION_INDUCT THEN
2365   SIMP_TAC[o_DEF; POLYNOMIAL_FUNCTION_ADD; POLYNOMIAL_FUNCTION_MUL] THEN
2366   ASM_REWRITE_TAC[ETA_AX; POLYNOMIAL_FUNCTION_CONST]);;
2367
2368 let POLYNOMIAL_FUNCTION_FINITE_ROOTS = prove
2369  (`!p a. polynomial_function p
2370          ==> (FINITE {x | p x = a} <=> ~(!x. p x = a))`,
2371   ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
2372   SUBGOAL_THEN
2373    `!p. polynomial_function p ==> (FINITE {x | p x = &0} <=> ~(!x. p x = &0))`
2374    (fun th ->
2375       SIMP_TAC[th; POLYNOMIAL_FUNCTION_SUB; POLYNOMIAL_FUNCTION_CONST]) THEN
2376   GEN_TAC THEN REWRITE_TAC[polynomial_function] THEN
2377   STRIP_TAC THEN EQ_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THENL
2378    [SIMP_TAC[UNIV_GSPEC; GSYM INFINITE; real_INFINITE];
2379     ASM_REWRITE_TAC[REAL_POLYFUN_FINITE_ROOTS] THEN
2380     SIMP_TAC[NOT_EXISTS_THM; TAUT `~(p /\ ~q) <=> p ==> q`] THEN
2381     REWRITE_TAC[REAL_MUL_LZERO; SUM_0]]);;
2382
2383 (* ------------------------------------------------------------------------- *)
2384 (* Make natural numbers the default again.                                   *)
2385 (* ------------------------------------------------------------------------- *)
2386
2387 prioritize_num();;