# HG changeset patch
# User blanchet
# Date 1273872935 -7200
# Node ID 4ef12072b94a657f25520a496e60af8d9735c1c1
# Parent  15d9f4373f78fc4ae3b5f474dfc1a8b313316beb# Parent  8ea9395fa21dd952a27483ad44dd5284fb867cc6
merge

diff -r 15d9f4373f78 -r 4ef12072b94a src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 14 23:34:24 2010 +0200
+++ b/src/HOL/List.thy	Fri May 14 23:35:35 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: *}