Re: [isabelle] How to use setsum for set addition?
Well, you need to tell Isabelle that your type of sets of things is in
the class comm_monoid_add, thus:
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
Then you can do definitions such as:
sss :: "('a => 'b::comm_monoid_add set)
=> 'a set => 'b::comm_monoid_add set"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and