Re: [isabelle] Unfolding setsum



On Fri, Aug 13, 2010 at 8:42 AM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:

> 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.
>
>
Thanks for the reply. But what if the axioms were:

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) can only simplify the RHS.

Thanks again
Steve


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




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