# HG changeset patch
# User nipkow
# Date 1241032246 -7200
# Node ID a438b4516dd3de4573dff4bbb1692c912d6fa71e
# Parent  53642251a04f803654b000d6962c679edc87a17d
added listsum lemmas

diff -r 53642251a04f -r a438b4516dd3 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 29 14:20:26 2009 +0200
+++ b/src/HOL/List.thy	Wed Apr 29 21:10:46 2009 +0200
@@ -2120,6 +2120,15 @@
   shows "listsum (rev xs) = listsum xs"
 by (induct xs) (simp_all add:add_ac)
 
+lemma listsum_map_remove1:
+fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
+shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
+by (induct xs)(auto simp add:add_ac)
+
+lemma list_size_conv_listsum:
+  "list_size f xs = listsum (map f xs) + size xs"
+by(induct xs) auto
+
 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
 by (induct xs) auto