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!
thanks in advance!
                                          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







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