1.1 --- a/src/HOL/List.thy	Wed Apr 29 14:20:26 2009 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Apr 29 21:10:46 2009 +0200
     1.3 @@ -2120,6 +2120,15 @@
     1.4    shows "listsum (rev xs) = listsum xs"
     1.5  by (induct xs) (simp_all add:add_ac)
     1.6  
     1.7 +lemma listsum_map_remove1:
     1.8 +fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
     1.9 +shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
    1.10 +by (induct xs)(auto simp add:add_ac)
    1.11 +
    1.12 +lemma list_size_conv_listsum:
    1.13 +  "list_size f xs = listsum (map f xs) + size xs"
    1.14 +by(induct xs) auto
    1.15 +
    1.16  lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
    1.17  by (induct xs) auto
    1.18