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: "a = 1"
> and ax3: "b = 2"
> and ax4: "ALL x. f x = 1"
> 
> lemma "setsum f S = f a + f b"

apply (simp add: ax1 ax2 ax3)
is sufficient

In general, find_theorems "setsum _ _ = _" will provide you with a
couple of lemmas to rewrite setsum.

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.