[isabelle] how to proof some lemmas containing "\<Sum>"?



dear,
  I'm an Isabelle newbie trying to verify a proof.  The statement of the proof  involves \<Sum>. I meet some prombles, the following are my proof;
theory sumlist
imports Main List
begin
consts
setn::"nat  \<Rightarrow>  nat set"
primrec
"setn 0 = {}"
"setn (Suc n) = insert (Suc n) (setn n)"

lemma f: " (\<Sum>i\<in>(setn (Suc j)). i)=(Suc j)+(\<Sum>i\<in>(setn j). i)"
apply auto
apply  ?????
 
The reslut is displayed in the next window
proof (prove): step 1
goal (1 subgoal):
 1. \<Sum>(insert (Suc j) (setn j)) = Suc (j + \<Sum>(setn j))


Which method or rule I can choose? How to use these methods and rules? I don't known any lemmas and themorems about \<Sum>.How can i get some informations about \<Sum>?
 
need help!
thanks in advance!
                                          yucy




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