added lemma
authornipkow
Thu Nov 13 12:35:55 2014 +0100 (2014-11-13)
changeset 5899542ba2b5cffac
parent 58994 87d4ce309e04
child 58997 fc571ebb04e1
added lemma
src/HOL/Groups_List.thy
     1.1 --- a/src/HOL/Groups_List.thy	Wed Nov 12 19:30:56 2014 +0100
     1.2 +++ b/src/HOL/Groups_List.thy	Thu Nov 13 12:35:55 2014 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  (* Author: Tobias Nipkow, TU Muenchen *)
     1.6  
     1.7  section {* Sum and product over lists *}
     1.8 @@ -159,6 +158,10 @@
     1.9    "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
    1.10    by (induct xs) simp_all
    1.11  
    1.12 +lemma listsum_upt[simp]:
    1.13 +  "m \<le> n \<Longrightarrow> listsum [m..<n] = \<Sum> {m..<n}"
    1.14 +by(simp add: distinct_listsum_conv_Setsum)
    1.15 +
    1.16  lemma listsum_eq_0_nat_iff_nat [simp]:
    1.17    "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
    1.18    by (induct ns) simp_all