# [isabelle] How to use setsum for set addition?

Dear Isabelle Users
I have to prove that for n convex sets in an Euclidean space A_1 A_2 ,..., A_n we have
rel_interior (A_1 + A_2 + … + A_n ) = (rel_interior A_1 + rel_interior A_2 + … + rel_interior A_n )
(for this letter, it is not important what rel_interior is).
My first problem, is how to write this down conveniently. Notation for sum of TWO sets is defined in SetsAndFunctions.thy
definition
set_plus :: "('a::plus) set => 'a set => 'a set" (infixl "\oplus" 65) where
"A \oplus B == {c. EX a:A. EX b:B. c = a + b}"
Now I need to write it for n sets. Let I be finite index set. If I try
lemma test:
assumes "finite I"
assumes "!i:I. convex ((S i) :: ('n::euclidean_space) set)"
shows "setsum S I=..."
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?
Next, I have already proved my lemma for two sets:
rel_interior (A \oplus B ) = (rel_interior A \oplus rel_interior B)
Also, I have lemma linear_setsum, stating that if for function f we have f(a+b)=f(a)+f(b), then we have f(a_1+...+a_n)=f(a_1)+...+f(a_n). Implication of this lemma would immediately finish the proof. And my feeling that it should work. The system should just recognize \oplus as a regular addition. How can I tell it to do so?
Sincerely,
Bogdan.

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