src/ZF/UNITY/MultisetSum.thy

some new ZF/UNITY material from Sidi Ehmety

(*  Title:      ZF/UNITY/MultusetSum.thy
    ID:         $Id$
    Author:     Sidi O Ehmety

Setsum for multisets.
*)

MultisetSum = Multiset +
constdefs

  lcomm :: "[i, i, [i,i]=>i]=>o"
  "lcomm(A, B, f) ==
   (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))= f(y, f(x, z)))  &
   (ALL x:A. ALL y:B. f(x, y):B)"

  general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i"
   "general_setsum(C, B, e, f, g) ==
    if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e"

  msetsum :: "[i=>i, i, i]=>i"
  "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))"

  (* sum for naturals *)
  nsetsum :: "[i=>i, i] =>i"
  "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)"
end