|
1 (* Title: ZF/UNITY/MultusetSum.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety |
|
4 |
|
5 Setsum for multisets. |
|
6 *) |
|
7 |
|
8 MultisetSum = Multiset + |
|
9 constdefs |
|
10 |
|
11 lcomm :: "[i, i, [i,i]=>i]=>o" |
|
12 "lcomm(A, B, f) == |
|
13 (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))= f(y, f(x, z))) & |
|
14 (ALL x:A. ALL y:B. f(x, y):B)" |
|
15 |
|
16 general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i" |
|
17 "general_setsum(C, B, e, f, g) == |
|
18 if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e" |
|
19 |
|
20 msetsum :: "[i=>i, i, i]=>i" |
|
21 "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))" |
|
22 |
|
23 (* sum for naturals *) |
|
24 nsetsum :: "[i=>i, i] =>i" |
|
25 "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)" |
|
26 end |