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)
qed

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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