[isabelle] Unfolding setsum



Hello,

I would like to prove a rather simple lemma, which unfolds a setsum. For
example

axiomatization
S :: "real set"
and f :: "real => real"
and a :: real
and b :: real
where ax1: "S = {a,b}"
and ax2: "a = 1"
and ax3: "b = 2"
and ax4: "ALL x. f x = 1"

lemma "setsum f S = f a + f b"

How would one go about this? I'm doing this just as an exercise.

Thank you for the help in advance.

Regards,
Steve




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