Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unfolding setsum

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

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

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

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

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: Nov 21 2024 at 12:39 UTC