# HG changeset patch
# User hoelzl
# Date 1296825415 -3600
# Node ID 1100512e16d8485b6b0f7065f7fee3f50aae0c2c
# Parent  8c539202f85426b5993bbbf6bfe66d4d6257b03f
add auto support for AE_mp

diff -r 8c539202f854 -r 1100512e16d8 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy	Fri Feb 04 14:16:55 2011 +0100
@@ -266,7 +266,7 @@
   proof (intro bexI)
     from AE[unfolded all_AE_countable]
     show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
-    proof (rule AE_mp, safe intro!: AE_cong)
+    proof (elim AE_mp, safe intro!: AE_I2)
       fix x assume eq: "\<forall>i. f i x = f' i x"
       moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
       ultimately show "g x = ?f x" by (simp add: SUPR_apply)
diff -r 8c539202f854 -r 1100512e16d8 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Feb 04 14:16:55 2011 +0100
@@ -694,10 +694,7 @@
   assumes "simple_function M f" and "simple_function M g"
   and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
   shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
-proof (rule simple_integral_mono_AE[OF assms(1, 2)])
-  show "AE x. f x \<le> g x"
-    using mono by (rule AE_cong) auto
-qed
+  using assms by (intro simple_integral_mono_AE) auto
 
 lemma (in measure_space) simple_integral_cong_AE:
   assumes "simple_function M f" "simple_function M g" and "AE x. f x = g x"
@@ -782,20 +779,14 @@
   have "AE x. indicator N x = (0 :: pextreal)"
     using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
   then have "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^isup>Sx. 0 \<partial>M)"
-    using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2)
+    using assms by (intro simple_integral_cong_AE) auto
   then show ?thesis by simp
 qed
 
 lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
   assumes sf: "simple_function M f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
   shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)"
-proof (rule simple_integral_cong_AE)
-  show "simple_function M f" by fact
-  show "simple_function M (\<lambda>x. f x * indicator S x)"
-    using sf `S \<in> sets M` by auto
-  from eq show "AE x. f x = f x * indicator S x"
-    by (rule AE_mp) simp
-qed
+  using assms by (intro simple_integral_cong_AE) auto
 
 lemma (in measure_space) simple_integral_restricted:
   assumes "A \<in> sets M"
@@ -1004,7 +995,7 @@
       have *: "{x \<in> space M. \<not> a x \<le> a x * indicator (space M - N) x} =
         N \<inter> {x \<in> space M. a x \<noteq> 0}" (is "?N = _")
         using `N \<in> sets M`[THEN sets_into_space] by (auto simp: indicator_def)
-      then show "?N \<in> sets M" 
+      then show "?N \<in> sets M"
         using `N \<in> sets M` `simple_function M a`[THEN borel_measurable_simple_function]
         by (auto intro!: measure_mono Int)
       then have "\<mu> ?N \<le> \<mu> N"
@@ -1032,9 +1023,8 @@
   by (auto simp: eq_iff intro!: positive_integral_mono_AE)
 
 lemma (in measure_space) positive_integral_mono:
-  assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x"
-  shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
-  using mono by (auto intro!: AE_cong positive_integral_mono_AE)
+  "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^isup>P M u \<le> integral\<^isup>P M v"
+  by (auto intro: positive_integral_mono_AE)
 
 lemma image_set_cong:
   assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
@@ -1487,6 +1477,16 @@
   qed
 qed
 
+lemma (in measure_space) positive_integral_0_iff_AE:
+  assumes u: "u \<in> borel_measurable M"
+  shows "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. u x = 0)"
+proof -
+  have sets: "{x\<in>space M. u x \<noteq> 0} \<in> sets M"
+    using u by auto
+  then show ?thesis
+    using positive_integral_0_iff[OF u] AE_iff_null_set[OF sets] by auto
+qed
+
 lemma (in measure_space) positive_integral_restricted:
   assumes "A \<in> sets M"
   shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
@@ -1585,10 +1585,8 @@
   assumes cong: "AE x. f x = g x"
   shows "integral\<^isup>L M f = integral\<^isup>L M g"
 proof -
-  have "AE x. Real (f x) = Real (g x)"
-    using cong by (rule AE_mp) simp
-  moreover have "AE x. Real (- f x) = Real (- g x)"
-    using cong by (rule AE_mp) simp
+  have "AE x. Real (f x) = Real (g x)" using cong by auto
+  moreover have "AE x. Real (- f x) = Real (- g x)" using cong by auto
   ultimately show ?thesis
     by (simp cong: positive_integral_cong_AE add: lebesgue_integral_def)
 qed
@@ -1756,20 +1754,18 @@
   shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
 proof -
   have "AE x. Real (f x) \<le> Real (g x)"
-    using mono by (rule AE_mp) (auto intro!: AE_cong)
+    using mono by auto
   moreover have "AE x. Real (- g x) \<le> Real (- f x)"
-    using mono by (rule AE_mp) (auto intro!: AE_cong)
+    using mono by auto
   ultimately show ?thesis using fg
     by (auto simp: lebesgue_integral_def integrable_def diff_minus
              intro!: add_mono real_of_pextreal_mono positive_integral_mono_AE)
 qed
 
 lemma (in measure_space) integral_mono:
-  assumes fg: "integrable M f" "integrable M g"
-  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+  assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
   shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
-  apply (rule integral_mono_AE[OF fg])
-  using mono by (rule AE_cong) auto
+  using assms by (auto intro: integral_mono_AE)
 
 lemma (in measure_space) integral_diff[simp, intro]:
   assumes f: "integrable M f" and g: "integrable M g"
@@ -2056,14 +2052,12 @@
 
 lemma (in measure_space) integral_real:
   fixes f :: "'a \<Rightarrow> pextreal"
-  assumes "AE x. f x \<noteq> \<omega>"
+  assumes [simp]: "AE x. f x \<noteq> \<omega>"
   shows "(\<integral>x. real (f x) \<partial>M) = real (integral\<^isup>P M f)" (is ?plus)
     and "(\<integral>x. - real (f x) \<partial>M) = - real (integral\<^isup>P M f)" (is ?minus)
 proof -
   have "(\<integral>\<^isup>+ x. Real (real (f x)) \<partial>M) = integral\<^isup>P M f"
-    apply (rule positive_integral_cong_AE)
-    apply (rule AE_mp[OF assms(1)])
-    by (auto intro!: AE_cong simp: Real_real)
+    by (auto intro!: positive_integral_cong_AE simp: Real_real)
   moreover
   have "(\<integral>\<^isup>+ x. Real (- real (f x)) \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)"
     by (intro positive_integral_cong) auto
@@ -2073,7 +2067,7 @@
 
 lemma (in measure_space) integral_dominated_convergence:
   assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
-  and w: "integrable M w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x"
+  and w: "integrable M w"
   and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
   shows "integrable M u'"
   and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
@@ -2089,13 +2083,18 @@
   have u'_borel: "u' \<in> borel_measurable M"
     using u' by (blast intro: borel_measurable_LIMSEQ[of u])
 
+  { fix x assume x: "x \<in> space M"
+    then have "0 \<le> \<bar>u 0 x\<bar>" by auto
+    also have "\<dots> \<le> w x" using bound[OF x] by auto
+    finally have "0 \<le> w x" . }
+  note w_pos = this
+
   show "integrable M u'"
   proof (rule integrable_bound)
     show "integrable M w" by fact
     show "u' \<in> borel_measurable M" by fact
   next
-    fix x assume x: "x \<in> space M"
-    thus "0 \<le> w x" by fact
+    fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact
     show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
   qed
 
@@ -2113,7 +2112,7 @@
 
   have PI_diff: "\<And>m n. (\<integral>\<^isup>+ x. Real (?diff (m + n) x) \<partial>M) =
     (\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)"
-    using diff w diff_less_2w
+    using diff w diff_less_2w w_pos
     by (subst positive_integral_diff[symmetric])
        (auto simp: integrable_def intro!: positive_integral_cong)
 
@@ -2155,7 +2154,7 @@
       unfolding PI_diff pextreal_INF_minus[OF I2w_fin] pextreal_SUP_minus ..
     finally show ?thesis using neq_0 I2w_fin by (rule pextreal_le_minus_imp_0)
   qed
- 
+
   have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto
 
   have [simp]: "\<And>n m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M) =
@@ -2230,13 +2229,11 @@
     show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
   qed
 
-  have 4: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> ?w x" using 2[of _ 0] by simp
-
   from summable[THEN summable_rabs_cancel]
-  have 5: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
+  have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
     by (auto intro: summable_sumr_LIMSEQ_suminf)
 
-  note int = integral_dominated_convergence(1,3)[OF 1 2 3 4 5]
+  note int = integral_dominated_convergence(1,3)[OF 1 2 3 4]
 
   from int show "integrable M ?S" by simp
 
diff -r 8c539202f854 -r 1100512e16d8 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Feb 04 14:16:55 2011 +0100
@@ -739,12 +739,25 @@
   obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
   using assms unfolding almost_everywhere_def by auto
 
+lemma (in measure_space) AE_E2:
+  assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
+  shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
+proof -
+  obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
+    using assms by (auto elim!: AE_E)
+  have "?P = space M - {x\<in>space M. P x}" by auto
+  then have "?P \<in> sets M" using assms by auto
+  with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
+    by (auto intro!: measure_mono)
+  then show "\<mu> ?P = 0" using A by simp
+qed
+
 lemma (in measure_space) AE_I:
   assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
   shows "AE x. P x"
   using assms unfolding almost_everywhere_def by auto
 
-lemma (in measure_space) AE_mp:
+lemma (in measure_space) AE_mp[elim!]:
   assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \<longrightarrow> Q x"
   shows "AE x. Q x"
 proof -
@@ -765,56 +778,28 @@
   qed
 qed
 
-lemma (in measure_space) AE_iffI:
-  assumes P: "AE x. P x" and Q: "AE x. P x \<longleftrightarrow> Q x" shows "AE x. Q x"
-  using AE_mp[OF Q, of "\<lambda>x. P x \<longrightarrow> Q x"] AE_mp[OF P, of Q] by auto
-
-lemma (in measure_space) AE_disjI1:
-  assumes P: "AE x. P x" shows "AE x. P x \<or> Q x"
-  by (rule AE_mp[OF P]) auto
-
-lemma (in measure_space) AE_disjI2:
-  assumes P: "AE x. Q x" shows "AE x. P x \<or> Q x"
-  by (rule AE_mp[OF P]) auto
-
-lemma (in measure_space) AE_conjI:
-  assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
-  shows "AE x. P x \<and> Q x"
-  apply (rule AE_mp[OF AE_P])
-  apply (rule AE_mp[OF AE_Q])
-  by simp
+lemma (in measure_space)
+  shows AE_iffI: "AE x. P x \<Longrightarrow> AE x. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x. Q x"
+    and AE_disjI1: "AE x. P x \<Longrightarrow> AE x. P x \<or> Q x"
+    and AE_disjI2: "AE x. Q x \<Longrightarrow> AE x. P x \<or> Q x"
+    and AE_conjI: "AE x. P x \<Longrightarrow> AE x. Q x \<Longrightarrow> AE x. P x \<and> Q x"
+    and AE_conj_iff[simp]: "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
+  by auto
 
-lemma (in measure_space) AE_conj_iff[simp]:
-  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
-proof (intro conjI iffI AE_conjI)
-  assume *: "AE x. P x \<and> Q x"
-  from * show "AE x. P x" by (rule AE_mp) auto
-  from * show "AE x. Q x" by (rule AE_mp) auto
-qed auto
-
-lemma (in measure_space) AE_E2:
-  assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
-  shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
-proof -
-  obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
-    using assms by (auto elim!: AE_E)
-  have "?P = space M - {x\<in>space M. P x}" by auto
-  then have "?P \<in> sets M" using assms by auto
-  with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
-    by (auto intro!: measure_mono)
-  then show "\<mu> ?P = 0" using A by simp
-qed
-
-lemma (in measure_space) AE_space[simp, intro]: "AE x. x \<in> space M"
+lemma (in measure_space) AE_space: "AE x. x \<in> space M"
   by (rule AE_I[where N="{}"]) auto
 
-lemma (in measure_space) AE_cong:
-  assumes "\<And>x. x \<in> space M \<Longrightarrow> P x" shows "AE x. P x"
-proof -
-  have [simp]: "\<And>x. (x \<in> space M \<longrightarrow> P x) \<longleftrightarrow> True" using assms by auto
-  show ?thesis
-    by (rule AE_mp[OF AE_space]) auto
-qed
+lemma (in measure_space) AE_I2[simp, intro]:
+  "(\<And>x. x \<in> space M \<Longrightarrow> P x) \<Longrightarrow> AE x. P x"
+  using AE_space by auto
+
+lemma (in measure_space) AE_Ball_mp:
+  "\<forall>x\<in>space M. P x \<Longrightarrow> AE x. P x \<longrightarrow> Q x \<Longrightarrow> AE x. Q x"
+  by auto
+
+lemma (in measure_space) AE_cong[cong]:
+  "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x. P x) \<longleftrightarrow> (AE x. Q x)"
+  by auto
 
 lemma (in measure_space) all_AE_countable:
   "(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
@@ -829,11 +814,7 @@
     by (intro null_sets_UN) auto
   ultimately show "AE x. \<forall>i. P i x"
     unfolding almost_everywhere_def by auto
-next
-  assume *: "AE x. \<forall>i. P i x"
-  show "\<forall>i. AE x. P i x"
-    by (rule allI, rule AE_mp[OF *]) simp
-qed
+qed auto
 
 lemma (in measure_space) restricted_measure_space:
   assumes "S \<in> sets M"
diff -r 8c539202f854 -r 1100512e16d8 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Fri Feb 04 14:16:55 2011 +0100
@@ -1061,46 +1061,28 @@
   have AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)"
     "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (- f (x, y)) \<partial>M2) \<noteq> \<omega>)"
     by (auto intro!: M1.positive_integral_omega_AE)
-  then show ?AE
-    apply (rule M1.AE_mp[OF _ M1.AE_mp])
-    apply (rule M1.AE_cong)
-    using assms unfolding integrable_def
-    by (auto intro!: measurable_pair_image_snd)
-  have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
-  proof (intro integrable_def[THEN iffD2] conjI)
-    show "?f \<in> borel_measurable M1"
-      using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
-    have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y))  \<partial>M2) \<partial>M1)"
-      apply (rule M1.positive_integral_cong_AE)
-      apply (rule M1.AE_mp[OF AE(1)])
-      apply (rule M1.AE_cong)
-      by (auto simp: Real_real)
-    then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
-      using positive_integral_fst_measurable[OF borel(2)] int by simp
-    have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
-      by (intro M1.positive_integral_cong) simp
-    then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
-  qed
-  moreover have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+ y. Real (- f (x, y)) \<partial>M2))"
-    (is "integrable M1 ?f")
-  proof (intro integrable_def[THEN iffD2] conjI)
-    show "?f \<in> borel_measurable M1"
-      using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
-    have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (- f (x, y))  \<partial>M2) \<partial>M1)"
-      apply (rule M1.positive_integral_cong_AE)
-      apply (rule M1.AE_mp[OF AE(2)])
-      apply (rule M1.AE_cong)
-      by (auto simp: Real_real)
-    then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
-      using positive_integral_fst_measurable[OF borel(1)] int by simp
-    have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
-      by (intro M1.positive_integral_cong) simp
-    then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
-  qed
-  ultimately show ?INT
+  then show ?AE using assms
+    by (simp add: measurable_pair_image_snd integrable_def)
+  { fix f assume borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable P"
+      and int: "integral\<^isup>P P (\<lambda>x. Real (f x)) \<noteq> \<omega>"
+      and AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)"
+    have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
+    proof (intro integrable_def[THEN iffD2] conjI)
+      show "?f \<in> borel_measurable M1"
+        using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
+      have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y))  \<partial>M2) \<partial>M1)"
+        using AE by (auto intro!: M1.positive_integral_cong_AE simp: Real_real)
+      then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
+        using positive_integral_fst_measurable[OF borel] int by simp
+      have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
+        by (intro M1.positive_integral_cong) simp
+      then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
+    qed }
+  from this[OF borel(1) int(1) AE(2)] this[OF borel(2) int(2) AE(1)]
+  show ?INT
     unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2]
       borel[THEN positive_integral_fst_measurable(2), symmetric]
-    by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)])
+    using AE by (simp add: M1.integral_real)
 qed
 
 lemma (in pair_sigma_finite) integrable_snd_measurable:
diff -r 8c539202f854 -r 1100512e16d8 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 04 14:16:48 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 04 14:16:55 2011 +0100
@@ -817,8 +817,8 @@
     (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
 proof (intro iffI ballI)
   fix A assume eq: "AE x. f x = g x"
-  show "?P f A = ?P g A"
-    by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp
+  then show "?P f A = ?P g A"
+    by (auto intro: positive_integral_cong_AE)
 next
   assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
   from this[THEN bspec, OF top] fin
@@ -879,11 +879,10 @@
   have "?N \<in> sets M" using borel by auto
   have *: "\<And>i x A. \<And>y::pextreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
     unfolding indicator_def by auto
-  have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
-    using borel Q_fin Q
+  have "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q
     by (intro finite_density_unique[THEN iffD1] allI)
        (auto intro!: borel_measurable_pextreal_times f Int simp: *)
-  have 2: "AE x. ?f Q0 x = ?f' Q0 x"
+  moreover have "AE x. ?f Q0 x = ?f' Q0 x"
   proof (rule AE_I')
     { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
         and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
@@ -911,13 +910,12 @@
     show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
       (Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def)
   qed
-  have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
+  moreover have "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
     ?f (space M) x = ?f' (space M) x"
     by (auto simp: indicator_def Q0)
-  have 3: "AE x. ?f (space M) x = ?f' (space M) x"
-    by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **)
-  then show "AE x. f x = f' x"
-    by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
+  ultimately have "AE x. ?f (space M) x = ?f' (space M) x"
+    by (auto simp: all_AE_countable)
+  then show "AE x. f x = f' x" by auto
 qed
 
 lemma (in sigma_finite_measure) density_unique:
@@ -978,25 +976,20 @@
     and "sets ?N = sets M" and "space ?N = space M" by (auto simp: measurable_def)
   from \<nu>.Ex_finite_integrable_function obtain h where
     h: "h \<in> borel_measurable M" "integral\<^isup>P ?N h \<noteq> \<omega>"
-    and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
+    and fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>" by auto
   have "AE x. f x * h x \<noteq> \<omega>"
   proof (rule AE_I')
-    have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)"
-      apply (subst \<nu>.positive_integral_cong_measure[symmetric,
-        of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"])
-      apply (simp_all add: eq)
-      apply (rule positive_integral_translated_density)
-      using f h by auto
+    have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)" using f h
+      by (subst \<nu>.positive_integral_cong_measure[symmetric,
+          of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"])
+         (auto intro!: positive_integral_translated_density simp: eq)
     then have "(\<integral>\<^isup>+x. f x * h x \<partial>M) \<noteq> \<omega>"
       using h(2) by simp
     then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
       using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
   qed auto
   then show "AE x. f x \<noteq> \<omega>"
-  proof (rule AE_mp, intro AE_cong)
-    fix x assume "x \<in> space M" from this[THEN fin]
-    show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto
-  qed
+    using fin by (auto elim!: AE_Ball_mp)
 next
   assume AE: "AE x. f x \<noteq> \<omega>"
   from sigma_finite guess Q .. note Q = this
@@ -1043,16 +1036,8 @@
     proof (cases i)
       case 0
       have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
-        using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
-      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) = 0"
-        using A_in_sets f
-        apply (subst positive_integral_0_iff)
-        apply fast
-        apply (subst (asm) AE_iff_null_set)
-        apply (intro borel_measurable_pextreal_neq_const)
-        apply fast
-        by simp
-      then show ?thesis by simp
+        using AE by (auto simp: A_def `i = 0`)
+      from positive_integral_cong_AE[OF this] show ?thesis by simp
     next
       case (Suc n)
       then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
@@ -1157,11 +1142,8 @@
         by (simp add: mult_le_0_iff)
       then have "RN_deriv M \<nu> x * Real (f x) = Real (real (RN_deriv M \<nu> x) * f x)"
         using * by (simp add: Real_real) }
-    note * = this
-    have "(\<integral>\<^isup>+x. RN_deriv M \<nu> x * Real (f x) \<partial>M) = (\<integral>\<^isup>+x. Real (real (RN_deriv M \<nu> x) * f x) \<partial>M)"
-      apply (rule positive_integral_cong_AE)
-      apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
-      by (auto intro!: AE_cong simp: *) }
+    then have "(\<integral>\<^isup>+x. RN_deriv M \<nu> x * Real (f x) \<partial>M) = (\<integral>\<^isup>+x. Real (real (RN_deriv M \<nu> x) * f x) \<partial>M)"
+      using RN_deriv_finite[OF \<nu>] by (auto intro: positive_integral_cong_AE) }
   with this this f f' Nf
   show ?integral ?integrable
     unfolding lebesgue_integral_def integrable_def