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

```At Wed, 8 Oct 2008 17:01:38 +0800 (CST),
=?gbk?B?087V5A==?= <yucy0405 at 163.com> wrote:
>

[...]

> 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>?

It seems obvious that you need something about \<Sum> and insert.
Isabelle has a very useful find-theorems command (I use it via C-c C-f
in Emacs) --- in this case it is a little tricky as \<Sum> is a
translation for setsum (which I found by greping for \<Sum> in
isabelle/HOL).  If you search for "\<Sum>_._" and insert (or setsum
and insert), you get a number of lemmas from Finite_Set, of which
setsum_insert is the one we want.

This requires a few helper lemmas, but the proof is more or less
straightforward (especially if you keep in mind that most lemmas to be
proved about setn will be via induction):

theory sumlist
imports Main List
begin

consts
setn::"nat  \<Rightarrow>  nat set"

primrec
"setn 0 = {}"
"setn (Suc n) = insert (Suc n) (setn n)"

lemma finite_setn:
"finite (setn n)"
apply (induct n)
apply simp
apply simp
done

lemma setn_n_le_n:
"x \<in> setn n \<Longrightarrow> x \<le> n"
apply (induct n)
apply simp
apply fastsimp
done

lemma f: " (\<Sum>i\<in>(setn (Suc j)). i)=(Suc j)+(\<Sum>i\<in>(setn j). i)"
proof (subst setn.simps, rule setsum_insert)
show "finite (setn j)" by (rule finite_setn)

show "Suc j \<notin> setn j"
proof
assume "Suc j \<in> setn j"
hence "Suc j \<le> j" by (rule setn_n_le_n)
thus False by simp
qed
qed

end

Simon

```

• References:

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