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

```Quoting 游珍 <yucy0405 at 163.com>:

```
```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!
yucy

```
```
```
At this point in your proof, you need to you can search for relevant lemmas by typing ctrl-c, ctrl-f, and using the patterns "\<Sum>_\<in>_. _" or "SUM _:_. _" together with "insert". The lemma you need is setsum_insert. In fact, setsum_insert is declared as a simp rule, but it has a couple of side conditions which prevent it from rewriting automatically.
```
If you type:
apply (subst setsum_insert)

you get the following subgoals:
goal (3 subgoals):
1. finite (setn j)
2. Suc j \<notin> setn j
3. Suc j + \<Sum>(setn j) = Suc (j + \<Sum>(setn j))

```
If you prove the first two subgoals as separate lemmas, and declare them both as [simp] rules, then your lemma f can be proved completely by auto.
```
Hope this helps,
- Brian

```

• References:

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