equal
deleted
inserted
replaced
1053 |
1053 |
1054 end |
1054 end |
1055 |
1055 |
1056 subsection {* Generalized summation over a set *} |
1056 subsection {* Generalized summation over a set *} |
1057 |
1057 |
1058 interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +" |
1058 interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add" |
1059 proof qed (auto intro: add_assoc add_commute) |
1059 proof qed (auto intro: add_assoc add_commute) |
1060 |
1060 |
1061 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" |
1061 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" |
1062 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0" |
1062 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0" |
1063 |
1063 |