diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -167,7 +167,7 @@
 
 lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
   by transfer simp
-  
+
 lemma pmf_not_neg [simp]: "\<not>pmf p x < 0"
   by (simp add: not_less pmf_nonneg)
 
@@ -546,7 +546,7 @@
 
 lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
 proof -
-  have "ennreal (measure_pmf.prob (return_pmf x) A) = 
+  have "ennreal (measure_pmf.prob (return_pmf x) A) =
           emeasure (measure_pmf (return_pmf x)) A"
     by (simp add: measure_pmf.emeasure_eq_measure)
   also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator)
@@ -778,10 +778,10 @@
   have "1 = measure (measure_pmf M) UNIV" by simp
   also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
     by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
-  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" 
+  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
     by (simp add: measure_pmf_single)
   also have "measure (measure_pmf N) (UNIV - {x}) \<le> measure (measure_pmf M) (UNIV - {x})"
-    by (subst (1 2) integral_pmf [symmetric]) 
+    by (subst (1 2) integral_pmf [symmetric])
        (intro integral_mono integrable_pmf, simp_all add: ge)
   also have "measure (measure_pmf M) {x} + \<dots> = 1"
     by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
@@ -803,7 +803,7 @@
     by unfold_locales
 
   have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
-    by (rule integral_cong) (auto intro!: integral_pmf_restrict)
+    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict)
   also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
     by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
               countable_set_pmf borel_measurable_count_space)
@@ -815,7 +815,7 @@
     by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
               countable_set_pmf borel_measurable_count_space)
   also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
-    by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
+    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
   finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
 qed
 
@@ -1629,7 +1629,7 @@
 
 lemma map_pmf_of_set:
   assumes "finite A" "A \<noteq> {}"
-  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))" 
+  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
     (is "?lhs = ?rhs")
 proof (intro pmf_eqI)
   fix x
@@ -1641,13 +1641,13 @@
 
 lemma pmf_bind_pmf_of_set:
   assumes "A \<noteq> {}" "finite A"
-  shows   "pmf (bind_pmf (pmf_of_set A) f) x = 
+  shows   "pmf (bind_pmf (pmf_of_set A) f) x =
              (\<Sum>xa\<in>A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs")
 proof -
   from assms have "card A > 0" by auto
   with assms have "ennreal ?lhs = ennreal ?rhs"
-    by (subst ennreal_pmf_bind) 
-       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric] 
+    by (subst ennreal_pmf_bind)
+       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
         setsum_nonneg ennreal_of_nat_eq_real_of_nat)
   thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
 qed
@@ -1675,10 +1675,10 @@
 qed
 
 text \<open>
-  Choosing an element uniformly at random from the union of a disjoint family 
-  of finite non-empty sets with the same size is the same as first choosing a set 
-  from the family uniformly at random and then choosing an element from the chosen set 
-  uniformly at random.  
+  Choosing an element uniformly at random from the union of a disjoint family
+  of finite non-empty sets with the same size is the same as first choosing a set
+  from the family uniformly at random and then choosing an element from the chosen set
+  uniformly at random.
 \<close>
 lemma pmf_of_set_UN:
   assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
@@ -1694,8 +1694,8 @@
     by (subst pmf_of_set) auto
   also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
     by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
-  also from assms 
-    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> = 
+  also from assms
+    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
               indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
       by (simp add: setsum_divide_distrib [symmetric] mult_ac)
   also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
@@ -1794,17 +1794,17 @@
 
 lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\<lambda>x. [x]) p"
   by (simp add: map_pmf_def bind_return_pmf)
-  
-lemma set_replicate_pmf: 
+
+lemma set_replicate_pmf:
   "set_pmf (replicate_pmf n p) = {xs\<in>lists (set_pmf p). length xs = n}"
   by (induction n) (auto simp: length_Suc_conv)
 
 lemma replicate_pmf_distrib:
-  "replicate_pmf (m + n) p = 
+  "replicate_pmf (m + n) p =
      do {xs \<leftarrow> replicate_pmf m p; ys \<leftarrow> replicate_pmf n p; return_pmf (xs @ ys)}"
   by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf)
 
-lemma power_diff': 
+lemma power_diff':
   assumes "b \<le> a"
   shows   "x ^ (a - b) = (if x = 0 \<and> a = b then 1 else x ^ a / (x::'a::field) ^ b)"
 proof (cases "x = 0")
@@ -1812,12 +1812,12 @@
   with assms show ?thesis by (cases "a - b") simp_all
 qed (insert assms, simp_all add: power_diff)
 
-  
+
 lemma binomial_pmf_Suc:
   assumes "p \<in> {0..1}"
-  shows   "binomial_pmf (Suc n) p = 
-             do {b \<leftarrow> bernoulli_pmf p; 
-                 k \<leftarrow> binomial_pmf n p; 
+  shows   "binomial_pmf (Suc n) p =
+             do {b \<leftarrow> bernoulli_pmf p;
+                 k \<leftarrow> binomial_pmf n p;
                  return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs")
 proof (intro pmf_eqI)
   fix k
@@ -1835,14 +1835,14 @@
 lemma binomial_pmf_altdef:
   assumes "p \<in> {0..1}"
   shows   "binomial_pmf n p = map_pmf (length \<circ> filter id) (replicate_pmf n (bernoulli_pmf p))"
-  by (induction n) 
-     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf 
+  by (induction n)
+     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf
         bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong)
 
 
 subsection \<open>PMFs from assiciation lists\<close>
 
-definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where 
+definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
   "pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
 
 definition pmf_of_list_wf where
@@ -1870,12 +1870,12 @@
     from Cons.prems have "snd x \<ge> 0" by simp
     moreover have "b \<ge> 0" if "(a,b) \<in> set xs" for a b
       using Cons.prems[of b] that by force
-    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) = 
-            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + 
+    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) =
+            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
             ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
-      by (intro nn_integral_cong, subst ennreal_plus [symmetric]) 
+      by (intro nn_integral_cong, subst ennreal_plus [symmetric])
          (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
-    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) + 
+    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
                       (\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
       by (intro nn_integral_add)
          (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
@@ -1934,20 +1934,20 @@
 proof -
   have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
     by simp
-  also from assms 
+  also from assms
     have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
     by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
-  also from assms 
+  also from assms
     have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
     by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
-  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. 
+  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
       indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
     using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
   also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
     using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
   also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
     using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
-  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * 
+  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
                       sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
     using assms by (simp add: pmf_pmf_of_list)
   also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
@@ -1955,17 +1955,17 @@
   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 sum_list_map_filter', subst sum_list_setsum_nth) simp
-  also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs). 
+  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)
-  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then 
+  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
                      (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
     by (auto intro!: setsum.cong setsum.neutral)
   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> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
     by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
-  finally show ?thesis . 
+  finally show ?thesis .
 qed
 
 lemma measure_pmf_of_list:
@@ -1989,7 +1989,7 @@
   "sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
   by (induction xs) simp_all
 (* END MOVE *)
-  
+
 lemma set_pmf_of_list_eq:
   assumes "pmf_of_list_wf xs" "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0"
   shows   "set_pmf (pmf_of_list xs) = fst ` set xs"
@@ -2000,13 +2000,13 @@
     from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
       by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
     moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
-    ultimately have "y = 0" using assms(1) 
+    ultimately have "y = 0" using assms(1)
       by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
     with assms(2) y have False by force
   }
   thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
 qed (insert set_pmf_of_list[OF assms(1)], simp_all)
-  
+
 lemma pmf_of_list_remove_zeros:
   assumes "pmf_of_list_wf xs"
   defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"