# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1463567073 -7200
# Node ID 65f1d7829463d68e215d1b0cf4e4911fc7cbc48c
# Parent  aa5cffd8a6060d138847aaac13365a94388532e3
Resolved name clash

diff -r aa5cffd8a606 -r 65f1d7829463 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue May 17 19:27:42 2016 +0200
+++ b/src/HOL/Groups_List.thy	Wed May 18 12:24:33 2016 +0200
@@ -259,7 +259,7 @@
     "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
   by (induction xs) simp_all
 
-lemma listsum_map_filter:
+lemma (in monoid_add) listsum_map_filter':
   "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
   by (induction xs) simp_all
 
diff -r aa5cffd8a606 -r 65f1d7829463 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 17 19:27:42 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed May 18 12:24:33 2016 +0200
@@ -1809,7 +1809,7 @@
 proof -
   have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
             (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
-    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter) (auto intro: listsum_cong)
+    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter') (auto intro: listsum_cong)
   also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
     using assms(1)
   proof (induction xs)
@@ -1901,7 +1901,7 @@
     by (intro setsum.cong) (auto simp: indicator_def)
   also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
                      if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
-    by (intro setsum.cong refl, subst listsum_map_filter, subst listsum_setsum_nth) simp
+    by (intro setsum.cong refl, subst listsum_map_filter', subst listsum_setsum_nth) simp
   also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs). 
                      if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
     by (rule setsum.commute)
@@ -1911,7 +1911,7 @@
   also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
     by (intro setsum.cong refl) (simp_all add: setsum.delta)
   also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
-    by (subst listsum_map_filter, subst listsum_setsum_nth) simp_all
+    by (subst listsum_map_filter', subst listsum_setsum_nth) simp_all
   finally show ?thesis . 
 qed