diff -r f17602cbf76a -r 1d066f6ab25d src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Thu Apr 14 12:17:44 2016 +0200
+++ b/src/HOL/Probability/Projective_Family.thy	Thu Apr 14 15:48:11 2016 +0200
@@ -88,7 +88,7 @@
     by (intro generator.intros J sets.Diff sets.top X)
   with J show "space (Pi\<^sub>M I M) - emb I J X \<in> generator"
     by (simp add: space_PiM prod_emb_PiE)
-  
+
   fix K Y assume K: "finite K" "K \<subseteq> I" and Y: "Y \<in> sets (PiM K M)"
   have "emb I (J \<union> K) (emb (J \<union> K) J X) \<inter> emb I (J \<union> K) (emb (J \<union> K) K Y) \<in> generator"
     unfolding prod_emb_Int[symmetric]
@@ -150,7 +150,7 @@
     then have "\<mu>G (emb I J {}) = 0"
       by (subst mu_G_spec) auto
     then show "\<mu>G {} = 0" by simp
-  qed (auto simp: mu_G_spec elim!: generator.cases)
+  qed
 qed
 
 lemma additive_mu_G: "additive generator \<mu>G"
@@ -182,7 +182,7 @@
     proof (clarsimp elim!: generator.cases simp: mu_G_spec del: notI)
       fix J assume "finite J" "J \<subseteq> I"
       then interpret prob_space "P J" by (rule prob_space_P)
-      show "\<And>X. X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emeasure (P J) X \<noteq> \<infinity>"
+      show "\<And>X. X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> emeasure (P J) X \<noteq> top"
         by simp
     qed
   next
@@ -312,7 +312,7 @@
   apply (auto simp add: sets_P atLeastLessThanSuc space_P simp del: nn_integral_indicator
      intro!: nn_integral_cong split: split_indicator)
   done
-  
+
 
 primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>"
@@ -446,7 +446,7 @@
   have sets_X[measurable]: "X n \<in> sets (PiM {0..<n} M)" for n
     by (cases "{i. J i \<subseteq> {0..< n}} = {}")
        (simp_all add: X_def, auto intro!: sets.countable_INT' sets.Int)
-  
+
   have dec_X: "n \<le> m \<Longrightarrow> X m \<subseteq> PF.emb {0..<m} {0..<n} (X n)" for n m
     unfolding X_def using ivl_subset[of 0 n 0 m]
     by (cases "{i. J i \<subseteq> {0..< n}} = {}")
@@ -502,24 +502,32 @@
       apply (simp add: bind_return[OF measurable_eP] nn_integral_eP)
       done
     also have "\<dots> = (\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>)"
-    proof (rule nn_integral_monotone_convergence_INF[symmetric])
+    proof (rule nn_integral_monotone_convergence_INF_AE[symmetric])
       have "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) \<le> (\<integral>\<^sup>+x. 1 \<partial>P n \<omega>)"
         by (intro nn_integral_mono) (auto split: split_indicator)
       also have "\<dots> < \<infinity>"
         using prob_space_P[OF \<omega>, THEN prob_space.emeasure_space_1] by simp
       finally show "(\<integral>\<^sup>+x. ?C' 0 x \<partial>P n \<omega>) < \<infinity>" .
     next
-      fix i j :: nat and x assume "i \<le> j" "x \<in> space (P n \<omega>)"
-      with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)"
-        by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
-      show "?C' j x \<le> ?C' i x"
-        using \<open>i \<le> j\<close> by (subst emeasure_C[symmetric, of i]) (auto intro!: emeasure_mono dec_X del: subsetI simp: sets_C space_P \<omega> \<omega>')
+      show "AE x in P n \<omega>. ?C' (Suc i) x \<le> ?C' i x" for i
+      proof (rule AE_I2)
+        fix x assume "x \<in> space (P n \<omega>)"
+        with \<omega> have \<omega>': "\<omega>(n := x) \<in> space (PiM {0..<Suc n} M)"
+          by (auto simp: space_P[OF \<omega>] space_PiM PiE_iff extensional_def)
+        with \<omega> show "?C' (Suc i) x \<le> ?C' i x"
+          apply (subst emeasure_C[symmetric, of i "Suc i"])
+          apply (auto intro!: emeasure_mono[OF dec_X] del: subsetI
+                      simp: sets_C space_P)
+          apply (subst sets_bind[OF sets_eP])
+          apply (simp_all add: space_C space_P)
+          done
+      qed
     qed fact
     finally have "(\<integral>\<^sup>+x. (INF i. ?C' i x) \<partial>P n \<omega>) \<noteq> 0"
       by simp
-    then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). 0 < (INF i. ?C' i x)"
-       using M by (subst (asm) nn_integral_0_iff_AE)
-         (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le)
+    with M have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). 0 < (INF i. ?C' i x)"
+       by (subst (asm) nn_integral_0_iff_AE)
+          (auto intro!: borel_measurable_INF simp: Filter.not_eventually not_le zero_less_iff_neq_zero)
     then have "\<exists>\<^sub>F x in ae_filter (P n \<omega>). x \<in> space (M n) \<and> 0 < (INF i. ?C' i x)"
       by (rule frequently_mp[rotated]) (auto simp: space_P \<omega>)
     then obtain x where "x \<in> space (M n)" "0 < (INF i. ?C' i x)"
@@ -585,7 +593,7 @@
   shows "emeasure lim (emb I J X) = emeasure (Pi\<^sub>M J M) X"
 proof (rule emeasure_lim[OF *], goal_cases)
   case (1 J X)
-  
+
   have "\<exists>Q. (\<forall>i. sets Q = PiM (\<Union>i. J i) M \<and> distr Q (PiM (J i) M) (\<lambda>x. restrict x (J i)) = Pi\<^sub>M (J i) M)"
   proof cases
     assume "finite (\<Union>i. J i)"
@@ -626,7 +634,7 @@
 
     let ?Q = "distr IT.PF.lim (PiM (\<Union>i. J i) M) (\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x))"
     { fix i
-      have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) = 
+      have "distr ?Q (Pi\<^sub>M (J i) M) (\<lambda>x. restrict x (J i)) =
         distr IT.PF.lim (Pi\<^sub>M (J i) M) ((\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n)) \<circ> (\<lambda>\<omega>. restrict \<omega> (t`J i)))"
       proof (subst distr_distr)
         have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M UNIV (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x i