Library/products.ml

   1 (* ========================================================================= *)
   2 (* Products of natural numbers and real numbers.                             *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Products over natural numbers.                                            *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let nproduct = new_definition
  12   `nproduct = iterate(( * ):num->num->num)`;;
  13
  14 let NPRODUCT_CLAUSES = prove
  15  (`(!f. nproduct {} f = 1) /\
  16    (!x f s. FINITE(s)
  17             ==> (nproduct (x INSERT s) f =
  18                  if x IN s then nproduct s f else f(x) * nproduct s f))`,
  19   REWRITE_TAC[nproduct; GSYM NEUTRAL_MUL] THEN
  20   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
  21   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MUL]);;
  22
  23 let NPRODUCT_SUPPORT = prove
  24  (`!f s. nproduct (support ( * ) f s) f = nproduct s f`,
  25   REWRITE_TAC[nproduct; ITERATE_SUPPORT]);;
  26
  27 let NPRODUCT_UNION = prove
  28  (`!f s t. FINITE s /\ FINITE t /\ DISJOINT s t
  29            ==> (nproduct (s UNION t) f = nproduct s f * nproduct t f)`,
  30   SIMP_TAC[nproduct; ITERATE_UNION; MONOIDAL_MUL]);;
  31
  32 let NPRODUCT_IMAGE = prove
  33  (`!f g s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)
  34            ==> (nproduct (IMAGE f s) g = nproduct s (g o f))`,
  35   REWRITE_TAC[nproduct; GSYM NEUTRAL_MUL] THEN
  36   MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_MUL]);;
  37
  38 let NPRODUCT_ADD_SPLIT = prove
  39  (`!f m n p.
  40         m <= n + 1
  41         ==> (nproduct (m..(n+p)) f = nproduct(m..n) f * nproduct(n+1..n+p) f)`,
  42   SIMP_TAC[NUMSEG_ADD_SPLIT; NPRODUCT_UNION; DISJOINT_NUMSEG; FINITE_NUMSEG;
  43            ARITH_RULE `x < x + 1`]);;
  44
  45 let NPRODUCT_POS_LT = prove
  46  (`!f s. FINITE s /\ (!x. x IN s ==> 0 < f x) ==> 0 < nproduct s f`,
  47   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
  48   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  49   SIMP_TAC[NPRODUCT_CLAUSES; ARITH; IN_INSERT; LT_MULT]);;
  50
  51 let NPRODUCT_POS_LT_NUMSEG = prove
  52  (`!f m n. (!x. m <= x /\ x <= n ==> 0 < f x) ==> 0 < nproduct(m..n) f`,
  53   SIMP_TAC[NPRODUCT_POS_LT; FINITE_NUMSEG; IN_NUMSEG]);;
  54
  55 let NPRODUCT_OFFSET = prove
  56  (`!f m p. nproduct(m+p..n+p) f = nproduct(m..n) (\i. f(i + p))`,
  57   SIMP_TAC[NUMSEG_OFFSET_IMAGE; NPRODUCT_IMAGE;
  58            EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
  59   REWRITE_TAC[o_DEF]);;
  60
  61 let NPRODUCT_SING = prove
  62  (`!f x. nproduct {x} f = f(x)`,
  63   SIMP_TAC[NPRODUCT_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; MULT_CLAUSES]);;
  64
  65 let NPRODUCT_SING_NUMSEG = prove
  66  (`!f n. nproduct(n..n) f = f(n)`,
  67   REWRITE_TAC[NUMSEG_SING; NPRODUCT_SING]);;
  68
  69 let NPRODUCT_CLAUSES_NUMSEG = prove
  70  (`(!m. nproduct(m..0) f = if m = 0 then f(0) else 1) /\
  71    (!m n. nproduct(m..SUC n) f = if m <= SUC n then nproduct(m..n) f * f(SUC n)
  72                                 else nproduct(m..n) f)`,
  73   REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
  74   COND_CASES_TAC THEN
  75   ASM_SIMP_TAC[NPRODUCT_SING; NPRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
  76   REWRITE_TAC[ARITH_RULE `~(SUC n <= n)`; MULT_AC]);;
  77
  78 let NPRODUCT_EQ = prove
  79  (`!f g s. (!x. x IN s ==> (f x = g x)) ==> nproduct s f = nproduct s g`,
  80   REWRITE_TAC[nproduct] THEN MATCH_MP_TAC ITERATE_EQ THEN
  81   REWRITE_TAC[MONOIDAL_MUL]);;
  82
  83 let NPRODUCT_EQ_NUMSEG = prove
  84  (`!f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
  85              ==> (nproduct(m..n) f = nproduct(m..n) g)`,
  86   MESON_TAC[NPRODUCT_EQ; FINITE_NUMSEG; IN_NUMSEG]);;
  87
  88 let NPRODUCT_EQ_0 = prove
  89  (`!f s. FINITE s ==> (nproduct s f = 0 <=> ?x. x IN s /\ f(x) = 0)`,
  90   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  91   SIMP_TAC[NPRODUCT_CLAUSES; MULT_EQ_0; IN_INSERT; ARITH; NOT_IN_EMPTY] THEN
  92   MESON_TAC[]);;
  93
  94 let NPRODUCT_EQ_0_NUMSEG = prove
  95  (`!f m n. nproduct(m..n) f = 0 <=> ?x. m <= x /\ x <= n /\ f(x) = 0`,
  96   SIMP_TAC[NPRODUCT_EQ_0; FINITE_NUMSEG; IN_NUMSEG; GSYM CONJ_ASSOC]);;
  97
  98 let NPRODUCT_LE = prove
  99  (`!f s. FINITE s /\ (!x. x IN s ==> 0 <= f(x) /\ f(x) <= g(x))
 100          ==> nproduct s f <= nproduct s g`,
 101   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 102   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 103   SIMP_TAC[IN_INSERT; NPRODUCT_CLAUSES; NOT_IN_EMPTY; LE_REFL] THEN
 104   MESON_TAC[LE_MULT2; LE_0]);;
 105
 106 let NPRODUCT_LE_NUMSEG = prove
 107  (`!f m n. (!i. m <= i /\ i <= n ==> 0 <= f(i) /\ f(i) <= g(i))
 108            ==> nproduct(m..n) f <= nproduct(m..n) g`,
 109   SIMP_TAC[NPRODUCT_LE; FINITE_NUMSEG; IN_NUMSEG]);;
 110
 111 let NPRODUCT_EQ_1 = prove
 112  (`!f s. (!x:A. x IN s ==> (f(x) = 1)) ==> (nproduct s f = 1)`,
 113   REWRITE_TAC[nproduct; GSYM NEUTRAL_MUL] THEN
 114   SIMP_TAC[ITERATE_EQ_NEUTRAL; MONOIDAL_MUL]);;
 115
 116 let NPRODUCT_EQ_1_NUMSEG = prove
 117  (`!f m n. (!i. m <= i /\ i <= n ==> (f(i) = 1)) ==> (nproduct(m..n) f = 1)`,
 118   SIMP_TAC[NPRODUCT_EQ_1; IN_NUMSEG]);;
 119
 120 let NPRODUCT_MUL = prove
 121  (`!f g s. FINITE s
 122            ==> nproduct s (\x. f x * g x) = nproduct s f * nproduct s g`,
 123   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 124   SIMP_TAC[NPRODUCT_CLAUSES; MULT_AC; MULT_CLAUSES]);;
 125
 126 let NPRODUCT_MUL_NUMSEG = prove
 127  (`!f g m n.
 128      nproduct(m..n) (\x. f x * g x) = nproduct(m..n) f * nproduct(m..n) g`,
 129   SIMP_TAC[NPRODUCT_MUL; FINITE_NUMSEG]);;
 130
 131 let NPRODUCT_CONST = prove
 132  (`!c s. FINITE s ==> nproduct s (\x. c) = c EXP (CARD s)`,
 133   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 134   SIMP_TAC[NPRODUCT_CLAUSES; CARD_CLAUSES; EXP]);;
 135
 136 let NPRODUCT_CONST_NUMSEG = prove
 137  (`!c m n. nproduct (m..n) (\x. c) = c EXP ((n + 1) - m)`,
 138   SIMP_TAC[NPRODUCT_CONST; CARD_NUMSEG; FINITE_NUMSEG]);;
 139
 140 let NPRODUCT_CONST_NUMSEG_1 = prove
 141  (`!c n. nproduct(1..n) (\x. c) = c EXP n`,
 142   SIMP_TAC[NPRODUCT_CONST; CARD_NUMSEG_1; FINITE_NUMSEG]);;
 143
 144 let NPRODUCT_ONE = prove
 145  (`!s. nproduct s (\n. 1) = 1`,
 146   SIMP_TAC[NPRODUCT_EQ_1]);;
 147
 148 let NPRODUCT_CLOSED = prove
 149  (`!P f:A->num s.
 150         P(1) /\ (!x y. P x /\ P y ==> P(x * y)) /\ (!a. a IN s ==> P(f a))
 151         ==> P(nproduct s f)`,
 152   REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_MUL) THEN
 153   DISCH_THEN(MP_TAC o SPEC `P:num->bool`) THEN
 154   ASM_SIMP_TAC[NEUTRAL_MUL; GSYM nproduct]);;
 155
 156 let NPRODUCT_CLAUSES_LEFT = prove
 157  (`!f m n. m <= n ==> nproduct(m..n) f = f(m) * nproduct(m+1..n) f`,
 158   SIMP_TAC[GSYM NUMSEG_LREC; NPRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
 159   ARITH_TAC);;
 160
 161 let NPRODUCT_CLAUSES_RIGHT = prove
 162  (`!f m n. 0 < n /\ m <= n ==> nproduct(m..n) f = nproduct(m..n-1) f * f(n)`,
 163   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 164   SIMP_TAC[LT_REFL; NPRODUCT_CLAUSES_NUMSEG; SUC_SUB1]);;
 165
 166 let NPRODUCT_SUPERSET = prove
 167  (`!f:A->num u v.
 168         u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> f(x) = 1)
 169         ==> nproduct v f = nproduct u f`,
 170   SIMP_TAC[nproduct; GSYM NEUTRAL_MUL; ITERATE_SUPERSET; MONOIDAL_MUL]);;
 171
 172 let NPRODUCT_PAIR = prove
 173  (`!f m n. nproduct(2*m..2*n+1) f = nproduct(m..n) (\i. f(2*i) * f(2*i+1))`,
 174   MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_MUL) THEN
 175   REWRITE_TAC[nproduct; NEUTRAL_MUL]);;
 176
 177 let NPRODUCT_DELETE = prove
 178  (`!f s a. FINITE s /\ a IN s
 179            ==> f(a) * nproduct(s DELETE a) f = nproduct s f`,
 180   SIMP_TAC[nproduct; ITERATE_DELETE; MONOIDAL_MUL]);;
 181
 182 let NPRODUCT_FACT = prove
 183  (`!n. nproduct(1..n) (\m. m) = FACT n`,
 184   INDUCT_TAC THEN REWRITE_TAC[NPRODUCT_CLAUSES_NUMSEG; FACT; ARITH] THEN
 185   ASM_REWRITE_TAC[ARITH_RULE `1 <= SUC n`; MULT_SYM]);;
 186
 187 let th = prove
 188    (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
 189                 ==> nproduct s (\i. f(i)) = nproduct s g) /\
 190      (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
 191                 ==> nproduct(a..b) (\i. f(i)) = nproduct(a..b) g) /\
 192      (!f g p.   (!x. p x ==> f x = g x)
 193                 ==> nproduct {y | p y} (\i. f(i)) = nproduct {y | p y} g)`,
 194     REPEAT STRIP_TAC THEN MATCH_MP_TAC NPRODUCT_EQ THEN
 195     ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
 196     extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;
 197
 198 (* ------------------------------------------------------------------------- *)
 199 (* Now products over real numbers.                                           *)
 200 (* ------------------------------------------------------------------------- *)
 201
 202 prioritize_real();;
 203
 204 let product = new_definition
 205   `product = iterate (( * ):real->real->real)`;;
 206
 207 let PRODUCT_CLAUSES = prove
 208  (`(!f. product {} f = &1) /\
 209    (!x f s. FINITE(s)
 210             ==> (product (x INSERT s) f =
 211                  if x IN s then product s f else f(x) * product s f))`,
 212   REWRITE_TAC[product; GSYM NEUTRAL_REAL_MUL] THEN
 213   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
 214   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_REAL_MUL]);;
 215
 216 let PRODUCT_SUPPORT = prove
 217  (`!f s. product (support ( * ) f s) f = product s f`,
 218   REWRITE_TAC[product; ITERATE_SUPPORT]);;
 219
 220 let PRODUCT_UNION = prove
 221  (`!f s t. FINITE s /\ FINITE t /\ DISJOINT s t
 222            ==> (product (s UNION t) f = product s f * product t f)`,
 223   SIMP_TAC[product; ITERATE_UNION; MONOIDAL_REAL_MUL]);;
 224
 225 let PRODUCT_IMAGE = prove
 226  (`!f g s. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)
 227            ==> (product (IMAGE f s) g = product s (g o f))`,
 228   REWRITE_TAC[product; GSYM NEUTRAL_REAL_MUL] THEN
 229   MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_REAL_MUL]);;
 230
 231 let PRODUCT_ADD_SPLIT = prove
 232  (`!f m n p.
 233         m <= n + 1
 234         ==> (product (m..(n+p)) f = product(m..n) f * product(n+1..n+p) f)`,
 235   SIMP_TAC[NUMSEG_ADD_SPLIT; PRODUCT_UNION; DISJOINT_NUMSEG; FINITE_NUMSEG;
 236            ARITH_RULE `x < x + 1`]);;
 237
 238 let PRODUCT_POS_LE = prove
 239  (`!f s. FINITE s /\ (!x. x IN s ==> &0 <= f x) ==> &0 <= product s f`,
 240   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 241   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 242   SIMP_TAC[PRODUCT_CLAUSES; REAL_POS; IN_INSERT; REAL_LE_MUL]);;
 243
 244 let PRODUCT_POS_LE_NUMSEG = prove
 245  (`!f m n. (!x. m <= x /\ x <= n ==> &0 <= f x) ==> &0 <= product(m..n) f`,
 246   SIMP_TAC[PRODUCT_POS_LE; FINITE_NUMSEG; IN_NUMSEG]);;
 247
 248 let PRODUCT_POS_LT = prove
 249  (`!f s. FINITE s /\ (!x. x IN s ==> &0 < f x) ==> &0 < product s f`,
 250   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 251   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 252   SIMP_TAC[PRODUCT_CLAUSES; REAL_LT_01; IN_INSERT; REAL_LT_MUL]);;
 253
 254 let PRODUCT_POS_LT_NUMSEG = prove
 255  (`!f m n. (!x. m <= x /\ x <= n ==> &0 < f x) ==> &0 < product(m..n) f`,
 256   SIMP_TAC[PRODUCT_POS_LT; FINITE_NUMSEG; IN_NUMSEG]);;
 257
 258 let PRODUCT_OFFSET = prove
 259  (`!f m p. product(m+p..n+p) f = product(m..n) (\i. f(i + p))`,
 260   SIMP_TAC[NUMSEG_OFFSET_IMAGE; PRODUCT_IMAGE;
 261            EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
 262   REWRITE_TAC[o_DEF]);;
 263
 264 let PRODUCT_SING = prove
 265  (`!f x. product {x} f = f(x)`,
 266   SIMP_TAC[PRODUCT_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; REAL_MUL_RID]);;
 267
 268 let PRODUCT_SING_NUMSEG = prove
 269  (`!f n. product(n..n) f = f(n)`,
 270   REWRITE_TAC[NUMSEG_SING; PRODUCT_SING]);;
 271
 272 let PRODUCT_CLAUSES_NUMSEG = prove
 273  (`(!m. product(m..0) f = if m = 0 then f(0) else &1) /\
 274    (!m n. product(m..SUC n) f = if m <= SUC n then product(m..n) f * f(SUC n)
 275                                 else product(m..n) f)`,
 276   REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
 277   COND_CASES_TAC THEN
 278   ASM_SIMP_TAC[PRODUCT_SING; PRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
 279   REWRITE_TAC[ARITH_RULE `~(SUC n <= n)`; REAL_MUL_AC]);;
 280
 281 let PRODUCT_EQ = prove
 282  (`!f g s. (!x. x IN s ==> (f x = g x)) ==> product s f = product s g`,
 283   REWRITE_TAC[product] THEN MATCH_MP_TAC ITERATE_EQ THEN
 284   REWRITE_TAC[MONOIDAL_REAL_MUL]);;
 285
 286 let PRODUCT_EQ_NUMSEG = prove
 287  (`!f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
 288              ==> (product(m..n) f = product(m..n) g)`,
 289   MESON_TAC[PRODUCT_EQ; FINITE_NUMSEG; IN_NUMSEG]);;
 290
 291 let PRODUCT_EQ_0 = prove
 292  (`!f s. FINITE s ==> (product s f = &0 <=> ?x. x IN s /\ f(x) = &0)`,
 293   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 294   SIMP_TAC[PRODUCT_CLAUSES; REAL_ENTIRE; IN_INSERT; REAL_OF_NUM_EQ; ARITH;
 295            NOT_IN_EMPTY] THEN
 296   MESON_TAC[]);;
 297
 298 let PRODUCT_EQ_0_NUMSEG = prove
 299  (`!f m n. product(m..n) f = &0 <=> ?x. m <= x /\ x <= n /\ f(x) = &0`,
 300   SIMP_TAC[PRODUCT_EQ_0; FINITE_NUMSEG; IN_NUMSEG; GSYM CONJ_ASSOC]);;
 301
 302 let PRODUCT_LE = prove
 303  (`!f s. FINITE s /\ (!x. x IN s ==> &0 <= f(x) /\ f(x) <= g(x))
 304          ==> product s f <= product s g`,
 305   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 306   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 307   SIMP_TAC[IN_INSERT; PRODUCT_CLAUSES; NOT_IN_EMPTY; REAL_LE_REFL] THEN
 308   MESON_TAC[REAL_LE_MUL2; PRODUCT_POS_LE]);;
 309
 310 let PRODUCT_LE_NUMSEG = prove
 311  (`!f m n. (!i. m <= i /\ i <= n ==> &0 <= f(i) /\ f(i) <= g(i))
 312            ==> product(m..n) f <= product(m..n) g`,
 313   SIMP_TAC[PRODUCT_LE; FINITE_NUMSEG; IN_NUMSEG]);;
 314
 315 let PRODUCT_EQ_1 = prove
 316  (`!f s. (!x:A. x IN s ==> (f(x) = &1)) ==> (product s f = &1)`,
 317   REWRITE_TAC[product; GSYM NEUTRAL_REAL_MUL] THEN
 318   SIMP_TAC[ITERATE_EQ_NEUTRAL; MONOIDAL_REAL_MUL]);;
 319
 320 let PRODUCT_EQ_1_NUMSEG = prove
 321  (`!f m n. (!i. m <= i /\ i <= n ==> (f(i) = &1)) ==> (product(m..n) f = &1)`,
 322   SIMP_TAC[PRODUCT_EQ_1; IN_NUMSEG]);;
 323
 324 let PRODUCT_MUL = prove
 325  (`!f g s. FINITE s ==> product s (\x. f x * g x) = product s f * product s g`,
 326   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 327   SIMP_TAC[PRODUCT_CLAUSES; REAL_MUL_AC; REAL_MUL_LID]);;
 328
 329 let PRODUCT_MUL_NUMSEG = prove
 330  (`!f g m n.
 331      product(m..n) (\x. f x * g x) = product(m..n) f * product(m..n) g`,
 332   SIMP_TAC[PRODUCT_MUL; FINITE_NUMSEG]);;
 333
 334 let PRODUCT_CONST = prove
 335  (`!c s. FINITE s ==> product s (\x. c) = c pow (CARD s)`,
 336   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 337   SIMP_TAC[PRODUCT_CLAUSES; CARD_CLAUSES; real_pow]);;
 338
 339 let PRODUCT_CONST_NUMSEG = prove
 340  (`!c m n. product (m..n) (\x. c) = c pow ((n + 1) - m)`,
 341   SIMP_TAC[PRODUCT_CONST; CARD_NUMSEG; FINITE_NUMSEG]);;
 342
 343 let PRODUCT_CONST_NUMSEG_1 = prove
 344  (`!c n. product(1..n) (\x. c) = c pow n`,
 345   SIMP_TAC[PRODUCT_CONST; CARD_NUMSEG_1; FINITE_NUMSEG]);;
 346
 347 let PRODUCT_NEG = prove
 348  (`!f s:A->bool.
 349      FINITE s ==> product s (\i. --(f i)) = --(&1) pow (CARD s) * product s f`,
 350   SIMP_TAC[GSYM PRODUCT_CONST; GSYM PRODUCT_MUL] THEN
 351   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_LID]);;
 352
 353 let PRODUCT_NEG_NUMSEG = prove
 354  (`!f m n. product(m..n) (\i. --(f i)) =
 355            --(&1) pow ((n + 1) - m) * product(m..n) f`,
 356   SIMP_TAC[PRODUCT_NEG; CARD_NUMSEG; FINITE_NUMSEG]);;
 357
 358 let PRODUCT_NEG_NUMSEG_1 = prove
 359  (`!f n. product(1..n) (\i. --(f i)) = --(&1) pow n * product(1..n) f`,
 360   REWRITE_TAC[PRODUCT_NEG_NUMSEG; ADD_SUB]);;
 361
 362 let PRODUCT_INV = prove
 363  (`!f s. FINITE s ==> product s (\x. inv(f x)) = inv(product s f)`,
 364   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 365   SIMP_TAC[PRODUCT_CLAUSES; REAL_INV_1; REAL_INV_MUL]);;
 366
 367 let PRODUCT_DIV = prove
 368  (`!f g s. FINITE s ==> product s (\x. f x / g x) = product s f / product s g`,
 369   SIMP_TAC[real_div; PRODUCT_MUL; PRODUCT_INV]);;
 370
 371 let PRODUCT_DIV_NUMSEG = prove
 372  (`!f g m n.
 373          product(m..n) (\x. f x / g x) = product(m..n) f / product(m..n) g`,
 374   SIMP_TAC[PRODUCT_DIV; FINITE_NUMSEG]);;
 375
 376 let PRODUCT_ONE = prove
 377  (`!s. product s (\n. &1) = &1`,
 378   SIMP_TAC[PRODUCT_EQ_1]);;
 379
 380 let PRODUCT_LE_1 = prove
 381  (`!f s. FINITE s /\ (!x. x IN s ==> &0 <= f x /\ f x <= &1)
 382          ==> product s f <= &1`,
 383   GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
 384   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 385   SIMP_TAC[PRODUCT_CLAUSES; REAL_LE_REFL; IN_INSERT] THEN
 386   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 387   MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC[PRODUCT_POS_LE]);;
 388
 389 let PRODUCT_ABS = prove
 390  (`!f s. FINITE s ==> product s (\x. abs(f x)) = abs(product s f)`,
 391   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 392   SIMP_TAC[PRODUCT_CLAUSES; REAL_ABS_MUL; REAL_ABS_NUM]);;
 393
 394 let PRODUCT_CLOSED = prove
 395  (`!P f:A->real s.
 396         P(&1) /\ (!x y. P x /\ P y ==> P(x * y)) /\ (!a. a IN s ==> P(f a))
 397         ==> P(product s f)`,
 398   REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_REAL_MUL) THEN
 399   DISCH_THEN(MP_TAC o SPEC `P:real->bool`) THEN
 400   ASM_SIMP_TAC[NEUTRAL_REAL_MUL; GSYM product]);;
 401
 402 let PRODUCT_CLAUSES_LEFT = prove
 403  (`!f m n. m <= n ==> product(m..n) f = f(m) * product(m+1..n) f`,
 404   SIMP_TAC[GSYM NUMSEG_LREC; PRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
 405   ARITH_TAC);;
 406
 407 let PRODUCT_CLAUSES_RIGHT = prove
 408  (`!f m n. 0 < n /\ m <= n ==> product(m..n) f = product(m..n-1) f * f(n)`,
 409   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 410   SIMP_TAC[LT_REFL; PRODUCT_CLAUSES_NUMSEG; SUC_SUB1]);;
 411
 412 let REAL_OF_NUM_NPRODUCT = prove
 413  (`!f:A->num s. FINITE s ==> &(nproduct s f) = product s (\x. &(f x))`,
 414   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 415   SIMP_TAC[PRODUCT_CLAUSES; NPRODUCT_CLAUSES; GSYM REAL_OF_NUM_MUL]);;
 416
 417 let PRODUCT_SUPERSET = prove
 418  (`!f:A->real u v.
 419         u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> f(x) = &1)
 420         ==> product v f = product u f`,
 421   SIMP_TAC[product; GSYM NEUTRAL_REAL_MUL;
 422            ITERATE_SUPERSET; MONOIDAL_REAL_MUL]);;
 423
 424 let PRODUCT_PAIR = prove
 425  (`!f m n. product(2*m..2*n+1) f = product(m..n) (\i. f(2*i) * f(2*i+1))`,
 426   MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_REAL_MUL) THEN
 427   REWRITE_TAC[product; NEUTRAL_REAL_MUL]);;
 428
 429 let PRODUCT_DELETE = prove
 430  (`!f s a. FINITE s /\ a IN s ==> f(a) * product(s DELETE a) f = product s f`,
 431   SIMP_TAC[product; ITERATE_DELETE; MONOIDAL_REAL_MUL]);;
 432
 433 (* ------------------------------------------------------------------------- *)
 434 (* Extend congruences.                                                       *)
 435 (* ------------------------------------------------------------------------- *)
 436
 437 let th = prove
 438    (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
 439                 ==> product s (\i. f(i)) = product s g) /\
 440      (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
 441                 ==> product(a..b) (\i. f(i)) = product(a..b) g) /\
 442      (!f g p.   (!x. p x ==> f x = g x)
 443                 ==> product {y | p y} (\i. f(i)) = product {y | p y} g)`,
 444     REPEAT STRIP_TAC THEN MATCH_MP_TAC PRODUCT_EQ THEN
 445     ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
 446     extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;