# HG changeset patch
# User nipkow
# Date 1273870001 -7200
# Node ID 62e4af74a70ad010b1f8d2bc7c13f8983176010b
# Parent  e65f8d253fd15dd9ca4522d9312d48760436dbf1
added listsum lemmas

diff -r e65f8d253fd1 -r 62e4af74a70a src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/List.thy	Fri May 14 22:46:41 2010 +0200
@@ -2532,6 +2532,23 @@
   "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
 by (induct xs) simp_all
 
+lemma listsum_eq_0_nat_iff_nat[simp]:
+  "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
+by(simp add: listsum)
+
+lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
+apply(induct ns arbitrary: k)
+ apply simp
+apply(fastsimp simp add:nth_Cons split: nat.split)
+done
+
+lemma listsum_update_nat: "k<size ns \<Longrightarrow>
+  listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
+apply(induct ns arbitrary:k)
+ apply (auto split:nat.split)
+apply(drule elem_le_listsum_nat)
+apply arith
+done
 
 text{* Some syntactic sugar for summing a function over a list: *}