--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Oct 08 22:28:20 2017 +0200
@@ -321,7 +321,7 @@
apply metis
done
also have "\<dots> = - (\<Sum>y\<in>Y`msgs. (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))))"
- by (subst sum.commute) rule
+ by (subst sum.swap) rule
also have "\<dots> = -(\<Sum>y\<in>Y`msgs. (\<P>(Y) {y}) * (\<Sum>x\<in>X`msgs. (\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}) * log b ((\<P>(X ; Y) {(x,y)}) / (\<P>(Y) {y}))))"
by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
finally show "- (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` msgs. (\<P>(X ; Y) {(x, y)}) * log b ((\<P>(X ; Y) {(x, y)}) / (\<P>(Y) {y}))) =