|
14052
|
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 |