# HG changeset patch
# User nipkow
# Date 1273870018 -7200
# Node ID 8ea9395fa21dd952a27483ad44dd5284fb867cc6
# Parent  182774d56bd2279909dba0ada750c36cc313a782# Parent  62e4af74a70ad010b1f8d2bc7c13f8983176010b
merged

diff -r 182774d56bd2 -r 8ea9395fa21d src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 14 21:23:29 2010 +0200
+++ b/src/HOL/List.thy	Fri May 14 22:46:58 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: *}