--- a/src/HOL/Library/Extended_Real.thy Tue May 17 08:40:24 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue May 17 17:05:35 2016 +0200
@@ -228,6 +228,8 @@
datatype ereal = ereal real | PInfty | MInfty
+lemma ereal_cong: "x = y \<Longrightarrow> ereal x = ereal y" by simp
+
instantiation ereal :: uminus
begin
@@ -771,6 +773,9 @@
then show ?thesis by simp
qed
+lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))"
+ by (induction xs) simp_all
+
lemma setsum_Pinfty:
fixes f :: "'a \<Rightarrow> ereal"
shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"