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