*To*: grechukbogdan <grechukbogdan at yandex.ru>*Subject*: Re: [isabelle] How to use setsum for set addition?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 20 Aug 2010 11:22:21 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <302471282234919@web125.yandex.ru>*References*: <302471282234919@web125.yandex.ru>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

grechukbogdan wrote:

I have error “No type arity bool :: comm_monoid_add”. This is unpleasant: addition is defined for sets (see above), and setsum should be defined for any type in which addition is defined. Why I cannot use a convenient notation “setsum S I”? Can I correct this and make it work? Or should I introduce new definition for this? If so, do you have any suggestions how it should look like?

instance set :: (comm_monoid_add) comm_monoid_add

consts sss :: "('a => 'b::comm_monoid_add set) => 'a set => 'b::comm_monoid_add set" defs (overloaded) sss_def : "sss f S == setsum f S" However I suspect that this won't work from (I think) Isabelle2008 onwards, there were messages at the time about the changes to the way the set type is defined. So try it on Isabelle<=2007 Jeremy

**References**:**[isabelle] How to use setsum for set addition?***From:*grechukbogdan

- Previous by Date: [isabelle] How to use setsum for set addition?
- Next by Date: Re: [isabelle] How to use setsum for set addition?
- Previous by Thread: [isabelle] How to use setsum for set addition?
- Next by Thread: Re: [isabelle] How to use setsum for set addition?
- Cl-isabelle-users August 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list