Re: [isabelle] How to use setsum for set addition?



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?
Well, you need to tell Isabelle that your type of sets of things is in the class comm_monoid_add, thus:

instance set :: (comm_monoid_add) comm_monoid_add
Then you can do definitions such as:

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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.