[isabelle] Help with finite set comprehension proof



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.