Re: [isabelle] Solved it: Setsum Subgoal with play on the indices
I used "setsum_reindex_cong[of "(%x. Suc x)"])"
and that worked (with some other stuff but it was basically what I was
Thanks to anyone who spent anytime on this.
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and