--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Sep 14 22:07:11 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Sep 15 11:48:20 2016 +0200
@@ -951,16 +951,16 @@
lemma setsum_ennreal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. ennreal (f i)) = ennreal (setsum f I)"
by (induction I rule: infinite_finite_induct) (auto simp: setsum_nonneg)
-lemma listsum_ennreal[simp]:
+lemma sum_list_ennreal[simp]:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> 0"
- shows "listsum (map (\<lambda>x. ennreal (f x)) xs) = ennreal (listsum (map f xs))"
+ shows "sum_list (map (\<lambda>x. ennreal (f x)) xs) = ennreal (sum_list (map f xs))"
using assms
proof (induction xs)
case (Cons x xs)
- from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (listsum (map f xs))"
+ from Cons have "(\<Sum>x\<leftarrow>x # xs. ennreal (f x)) = ennreal (f x) + ennreal (sum_list (map f xs))"
by simp
- also from Cons.prems have "\<dots> = ennreal (f x + listsum (map f xs))"
- by (intro ennreal_plus [symmetric] listsum_nonneg) auto
+ also from Cons.prems have "\<dots> = ennreal (f x + sum_list (map f xs))"
+ by (intro ennreal_plus [symmetric] sum_list_nonneg) auto
finally show ?case by simp
qed simp_all