--- a/src/HOL/Groups_List.thy Thu Nov 13 14:14:13 2014 +0100
+++ b/src/HOL/Groups_List.thy Thu Nov 13 14:40:06 2014 +0100
@@ -1,4 +1,3 @@
-
(* Author: Tobias Nipkow, TU Muenchen *)
section {* Sum and product over lists *}
@@ -159,6 +158,10 @@
"distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
by (induct xs) simp_all
+lemma listsum_upt[simp]:
+ "m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}"
+by(simp add: distinct_listsum_conv_Setsum)
+
lemma listsum_eq_0_nat_iff_nat [simp]:
"listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
by (induct ns) simp_all