summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Wed, 18 May 2016 12:24:33 +0200 | |

changeset 63101 | 65f1d7829463 |

parent 63100 | aa5cffd8a606 |

child 63102 | 71059cf60658 |

Resolved name clash

src/HOL/Groups_List.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Probability/Probability_Mass_Function.thy | file | annotate | diff | comparison | revisions |

--- 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

--- 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