# HG changeset patch
# User nipkow
# Date 1415878555 -3600
# Node ID 42ba2b5cffacdb71ce2b3ade15828df9733f2959
# Parent  87d4ce309e04b6ef1da6d519e8be33ff998c2b94
added lemma

diff -r 87d4ce309e04 -r 42ba2b5cffac src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Wed Nov 12 19:30:56 2014 +0100
+++ b/src/HOL/Groups_List.thy	Thu Nov 13 12:35:55 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