src/HOL/Probability/Probability_Mass_Function.thy
changeset 66804 3f9bb52082c4
parent 66568 52b5cf533fd6
child 67226 ec32cdaab97b
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -797,7 +797,7 @@
     1.4           (insert assms, auto simp: scaleR_sum_left)
     1.5    qed
     1.6    also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R (\<Sum>i\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))"
     1.7 -    by (subst sum.commute) (simp add: scaleR_sum_right)
     1.8 +    by (subst sum.swap) (simp add: scaleR_sum_right)
     1.9    also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)"
    1.10    proof (intro sum.cong refl, goal_cases)
    1.11      case (1 x)
    1.12 @@ -2141,7 +2141,7 @@
    1.13      by (intro sum.cong refl, subst sum_list_map_filter', subst sum_list_sum_nth) simp
    1.14    also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
    1.15                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
    1.16 -    by (rule sum.commute)
    1.17 +    by (rule sum.swap)
    1.18    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
    1.19                       (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
    1.20      by (auto intro!: sum.cong sum.neutral simp del: sum.delta)