Re: [isabelle] Unfolding setsum

Hi Steve,

> axiomatization
> S :: "real set"
> and f :: "real => real"
> and a :: real
> and b :: real
> where ax1: "S = {a,b}"
> and ax2: "f a = 1"
> and ax3: "f b = 2"
> How would you go about proving the same lemma "setsum f S = f a + f b"?
> It seems to me apply (simp add: ax1 ax2 ax3)

in that case you have to establish "a \<noteq> b" first:

lemma "setsum f S = f a + f b"
proof -
  from ax2 ax3 have "a ≠ b" by auto
  then show ?thesis by (simp add: ax1 ax2 ax3)

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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