Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help with finite set comprehension proof

Email Gateway (Aug 18 2022 at 12:10):

From: George Karabotsos <g_karab@encs.concordia.ca>
Hello all,

I am having difficutly proving the following lemma

lemma "\<lbrakk> A = {x. 1 \<le> x \<and> x \<le> (3::int)}\<rbrakk> \<Longrightarrow> (\<Sum> A) = 6"

These are the steps I have followed by studying the HOL/Finite_Set.thy theory but I got stuck at the last one which I have commented out.

apply(auto)
apply(unfold setsum_def)
apply(auto)
apply(unfold fold_def)
apply(rule the_equality)
apply(induct set: finite)
thm foldSet.emptyI
(* apply(rule foldSet.emptyI) *)
oops

Any help will be much appreciated!

TIA,

George

Email Gateway (Aug 18 2022 at 12:11):

From: Tobias Nipkow <nipkow@in.tum.de>
lemma enum3: "{x::int. 1 <= x & x <= 3} = {1,2,3}"
by auto

lemma "(\<Sum> {x. 1 <= x & x <= (3::int)}) = 6"
by(simp add:enum3)

Regards
Tobias

George Karabotsos schrieb:

Email Gateway (Aug 18 2022 at 12:11):

From: Perry James <perry@dsrg.org>
Thanks for the proof. What if we have a lemma that does not use constants?
Is there a general approach to dealing with set comprehensions?
e.g.,
lemma "[| 0 < (n::int) |] ==> (\<Sum> {x. 1 <= x & x <= n}) = n + (\<Sum>
{x. 1 <= x & x <= n - 1})"

Thanks again,
Perry

Email Gateway (Aug 18 2022 at 12:11):

From: Amine Chaieb <chaieb@in.tum.de>
The following works for me:

lemma setinterval_iff: "{x. a <= x & x <= b} = {a .. b}"
by auto

lemma
assumes n: "0 < (n::int)"
shows "\<Sum> {x. 1 <= x & x <= n} = n + \<Sum> {x. 1 <= x & x <= n - 1}"
proof-
let ?A = "{1 .. n}"
let ?B = "{1 .. n - 1}"
let ?C = "{n}"
have abc: "finite ?B" "finite ?C" "?B Int ?C = {}" "?B Un ?C = ?A"
using n by auto
from setsum_Un_disjoint[OF abc(1-3), of "%x. x"]
show ?thesis unfolding abc(4) setinterval_iff by simp
qed

Amine.

Perry James wrote:

Email Gateway (Aug 18 2022 at 12:11):

From: Tobias Nipkow <nipkow@in.tum.de>

Thanks for the proof. What if we have a lemma that does not use constants?
Is there a general approach to dealing with set comprehensions?

Yes: avoid them when dealing with sums, use intervals like {i..j} instead.

e.g.,
lemma "[| 0 < (n::int) |] ==> (\<Sum> {x. 1 <= x & x <= n}) = n + (\<Sum>
{x. 1 <= x & x <= n - 1})"

I would not use such a recursive formulation but prove a closed formula
for the sum over an interger interval. There are some examples at the
end of SetInterval.thy.

Tobias

Thanks again,
Perry

On Sat, Jul 12, 2008 at 8:48 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:

lemma enum3: "{x::int. 1 <= x & x <= 3} = {1,2,3}"
by auto

lemma "(\<Sum> {x. 1 <= x & x <= (3::int)}) = 6"
by(simp add:enum3)

Regards
Tobias

George Karabotsos schrieb:

Hello all,

I am having difficutly proving the following lemma

lemma "\<lbrakk> A = {x. 1 \<le> x \<and> x \<le> (3::int)}\<rbrakk>
\<Longrightarrow> (\<Sum> A) = 6"

These are the steps I have followed by studying the HOL/Finite_Set.thy
theory but I got stuck at the last one which I have commented out.

apply(auto)
apply(unfold setsum_def)
apply(auto)
apply(unfold fold_def)
apply(rule the_equality)
apply(induct set: finite)
thm foldSet.emptyI
(* apply(rule foldSet.emptyI) *)
oops

Any help will be much appreciated!

TIA,

George

Last updated: May 03 2024 at 04:19 UTC