Resolved name clash
authorManuel Eberl <eberlm@in.tum.de>
Wed May 18 12:24:33 2016 +0200 (2016-05-18)
changeset 6310165f1d7829463
parent 63100 aa5cffd8a606
child 63102 71059cf60658
Resolved name clash
src/HOL/Groups_List.thy
src/HOL/Probability/Probability_Mass_Function.thy
     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.8 +lemma (in monoid_add) 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