# HG changeset patch
# User traytel
# Date 1415886006 -3600
# Node ID fc571ebb04e150ab93a68f28595f150327703c35
# Parent  1ae67039b14f66c8ca27942dbc4f9b3be6e75693# Parent  42ba2b5cffacdb71ce2b3ade15828df9733f2959
merged

diff -r 1ae67039b14f -r fc571ebb04e1 src/HOL/Groups_List.thy
--- 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