Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unfolding setsum


view this post on Zulip Email Gateway (Aug 18 2022 at 15:48):

From: Steve W <s.wong.731@gmail.com>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 15:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

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
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

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
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

I see. May i ask why is "a ~= b" needed here?

If not, then S = {a, b} = {a, a} = {a}, and setum f {a} = f a + f a does
not hold in general.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:49):

From: Steve W <s.wong.731@gmail.com>
On Fri, Aug 13, 2010 at 8:42 AM, Florian Haftmann <
florian.haftmann@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


Last updated: Mar 29 2024 at 08:18 UTC