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







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