[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.