author Manuel Eberl Wed May 18 12:24:33 2016 +0200 (2016-05-18 ago) changeset 63101 65f1d7829463 parent 63100 aa5cffd8a606 child 63102 71059cf60658
Resolved name clash
```     1.1 --- a/src/HOL/Groups_List.thy	Tue May 17 19:27:42 2016 +0200
1.2 +++ b/src/HOL/Groups_List.thy	Wed May 18 12:24:33 2016 +0200
1.3 @@ -259,7 +259,7 @@
1.4      "(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> listsum xs \<ge> 0"
1.5    by (induction xs) simp_all
1.6
1.7 -lemma listsum_map_filter:
1.9    "listsum (map f (filter P xs)) = listsum (map (\<lambda>x. if P x then f x else 0) xs)"
1.10    by (induction xs) simp_all
1.11
```
```     2.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 17 19:27:42 2016 +0200
2.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed May 18 12:24:33 2016 +0200
2.3 @@ -1809,7 +1809,7 @@
2.4  proof -
2.5    have "(\<integral>\<^sup>+ x. ennreal (listsum (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
2.6              (\<integral>\<^sup>+ x. ennreal (listsum (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
2.7 -    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter) (auto intro: listsum_cong)
2.8 +    by (intro nn_integral_cong ennreal_cong, subst listsum_map_filter') (auto intro: listsum_cong)
2.9    also have "\<dots> = (\<Sum>(x',p)\<leftarrow>xs. (\<integral>\<^sup>+ x. ennreal (indicator {x'} x * p) \<partial>count_space UNIV))"
2.10      using assms(1)
2.11    proof (induction xs)
2.12 @@ -1901,7 +1901,7 @@
2.13      by (intro setsum.cong) (auto simp: indicator_def)
2.14    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
2.15                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
2.16 -    by (intro setsum.cong refl, subst listsum_map_filter, subst listsum_setsum_nth) simp
2.17 +    by (intro setsum.cong refl, subst listsum_map_filter', subst listsum_setsum_nth) simp
2.18    also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
2.19                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
2.20      by (rule setsum.commute)
2.21 @@ -1911,7 +1911,7 @@
2.22    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
2.23      by (intro setsum.cong refl) (simp_all add: setsum.delta)
2.24    also have "\<dots> = listsum (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
2.25 -    by (subst listsum_map_filter, subst listsum_setsum_nth) simp_all
2.26 +    by (subst listsum_map_filter', subst listsum_setsum_nth) simp_all
2.27    finally show ?thesis .
2.28  qed
2.29
```