Re: [isabelle] Help with finite set comprehension proof



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.