# Re: [isabelle] Help with finite set comprehension proof

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

On Sat, Jul 12, 2008 at 8:48 AM, Tobias Nipkow <nipkow at 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"

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

```
```
```
```

```

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