src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
 changeset 66804 3f9bb52082c4 parent 66453 cc19f7ca2ed6 child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Oct 08 22:28:20 2017 +0200
1.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Oct 08 22:28:20 2017 +0200
1.3 @@ -321,7 +321,7 @@
1.4      apply metis
1.5      done
1.6    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}))))"
1.7 -    by (subst sum.commute) rule
1.8 +    by (subst sum.swap) rule
1.9    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}))))"
1.10      by (auto simp add: sum_distrib_left vimage_def intro!: sum.cong prob_conj_imp1)
1.11    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}))) =
```