src/HOL/Probability/Binary_Product_Measure.thy

--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Jun 16 23:03:27 2016 +0200
@@ -37,12 +37,6 @@
   unfolding pair_measure_def using pair_measure_closed[of A B]
   by (rule sets_measure_of)
 
-lemma sets_pair_in_sets:
-  assumes N: "space A \<times> space B = space N"
-  assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N"
-  shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
-  using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N)
-
 lemma sets_pair_measure_cong[measurable_cong, cong]:
   "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')"
   unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
@@ -122,23 +116,45 @@
     and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N"
   by simp_all
 
+lemma sets_pair_in_sets:
+  assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N"
+  shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
+  unfolding sets_pair_measure
+  by (intro sets.sigma_sets_subset') (auto intro!: assms)
+
 lemma sets_pair_eq_sets_fst_snd:
-  "sets (A \<Otimes>\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})"
-    (is "?P = sets (Sup_sigma {?fst, ?snd})")
+  "sets (A \<Otimes>\<^sub>M B) = sets (Sup {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})"
+    (is "?P = sets (Sup {?fst, ?snd})")
 proof -
   { fix a b assume ab: "a \<in> sets A" "b \<in> sets B"
     then have "a \<times> b = (fst -` a \<inter> (space A \<times> space B)) \<inter> (snd -` b \<inter> (space A \<times> space B))"
       by (auto dest: sets.sets_into_space)
-    also have "\<dots> \<in> sets (Sup_sigma {?fst, ?snd})"
-      using ab by (auto intro: in_Sup_sigma in_vimage_algebra)
-    finally have "a \<times> b \<in> sets (Sup_sigma {?fst, ?snd})" . }
+    also have "\<dots> \<in> sets (Sup {?fst, ?snd})"
+      apply (rule sets.Int)
+      apply (rule in_sets_Sup)
+      apply auto []
+      apply (rule insertI1)
+      apply (auto intro: ab in_vimage_algebra) []
+      apply (rule in_sets_Sup)
+      apply auto []
+      apply (rule insertI2)
+      apply (auto intro: ab in_vimage_algebra)
+      done
+    finally have "a \<times> b \<in> sets (Sup {?fst, ?snd})" . }
   moreover have "sets ?fst \<subseteq> sets (A \<Otimes>\<^sub>M B)"
     by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric])
   moreover have "sets ?snd \<subseteq> sets (A \<Otimes>\<^sub>M B)"
     by (rule sets_image_in_sets) (auto simp: space_pair_measure)
   ultimately show ?thesis
-    by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets )
-       (auto simp add: space_Sup_sigma space_pair_measure)
+    apply (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets)
+    apply simp
+    apply simp
+    apply simp
+    apply (elim disjE)
+    apply (simp add: space_pair_measure)
+    apply (simp add: space_pair_measure)
+    apply (auto simp add: space_pair_measure)
+    done
 qed
 
 lemma measurable_pair_iff:
@@ -597,11 +613,10 @@
   have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
     by auto
   let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
-  have "sets ?P =
-    sets (\<Squnion>\<^sub>\<sigma> xy\<in>?XY. sigma (X \<times> Y) xy)"
+  have "sets ?P = sets (SUP xy:?XY. sigma (X \<times> Y) xy)"
     by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
   also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
-    by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto
+    by (intro Sup_sigma arg_cong[where f=sets]) auto
   also have "\<dots> = sets ?S"
   proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
     show "\<Union>?XY \<subseteq> Pow (X \<times> Y)" "{a \<times> b |a b. a \<in> A \<and> b \<in> B} \<subseteq> Pow (X \<times> Y)"