Re: [isabelle] Solved it: Setsum Subgoal with play on the indices



Hi,

I used "setsum_reindex_cong[of "(%x. Suc x)"])"  
and that worked (with some other stuff but it was basically what I was
missing). 

Thanks to anyone who spent anytime on this.

Regards,
Primrose

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk
[mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Mbanefo
Primrose (COM PS CE)
Sent: Thursday, March 30, 2006 6:15 AM
To: cl-isabelle-users at lists.cam.ac.uk
Subject: [isabelle] Setsum Subgoal with play on the indices

Hi,

I have a subgoal which basically looks like:
\<Sum>i=0..<X. f (Suc i) = \<Sum>i=1..X. f i

And one of the assumptions is that 0 < X.

I have tried looking it up and came upon setsum_reindex which seems to
fit but I do not know how to use it in this case.
How can I go about proving this?

Thanks in advance for any help.

Primrose





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