use measurability prover

--- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -50,7 +50,7 @@
   "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
   unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
 
-lemma pair_measureI[intro, simp]:
+lemma pair_measureI[intro, simp, measurable]:
   "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^isub>M B)"
   by (auto simp: sets_pair_measure)
 
@@ -61,7 +61,11 @@
   unfolding pair_measure_def using 1 2
   by (intro measurable_measure_of) (auto dest: sets_into_space)
 
-lemma measurable_Pair:
+lemma measurable_split_replace[measurable (raw)]:
+  "(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
+  unfolding split_beta' .
+
+lemma measurable_Pair[measurable (raw)]:
   assumes f: "f \<in> measurable M M1" and g: "g \<in> measurable M M2"
   shows "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
 proof (rule measurable_pair_measureI)
@@ -75,34 +79,38 @@
   finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
 qed
 
+lemma measurable_Pair_compose_split[measurable_dest]:
+  assumes f: "split f \<in> measurable (M1 \<Otimes>\<^isub>M M2) N"
+  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
+  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
+  using measurable_compose[OF measurable_Pair f, OF g h] by simp
+
 lemma measurable_pair:
   assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
   shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
   using measurable_Pair[OF assms] by simp
 
-lemma measurable_fst[intro!, simp]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
+lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
   by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
 
-lemma measurable_snd[intro!, simp]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
+lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
   by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
 
-lemma measurable_fst': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. fst (f x)) \<in> measurable M N"
-  using measurable_comp[OF _ measurable_fst] by (auto simp: comp_def)
-
-lemma measurable_snd': "f \<in> measurable M (N \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. snd (f x)) \<in> measurable M P"
-    using measurable_comp[OF _ measurable_snd] by (auto simp: comp_def)
+lemma 
+  assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)" 
+  shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
+    and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P"
+  by simp_all
 
-lemma measurable_fst'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
-  using measurable_comp[OF measurable_fst _] by (auto simp: comp_def)
-
-lemma measurable_snd'': "f \<in> measurable M N \<Longrightarrow> (\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
-  using measurable_comp[OF measurable_snd _] by (auto simp: comp_def)
+lemma
+  assumes f[measurable]: "f \<in> measurable M N"
+  shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^isub>M P) N"
+    and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^isub>M M) N"
+  by simp_all
 
 lemma measurable_pair_iff:
   "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
-  using measurable_pair[of f M M1 M2]
-  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
-  by auto
+  by (auto intro: measurable_pair[of f M M1 M2]) 
 
 lemma measurable_split_conv:
   "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
@@ -117,16 +125,13 @@
 
 lemma measurable_pair_swap_iff:
   "f \<in> measurable (M2 \<Otimes>\<^isub>M M1) M \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) \<in> measurable (M1 \<Otimes>\<^isub>M M2) M"
-  using measurable_pair_swap[of "\<lambda>(x,y). f (y, x)"]
-  by (auto intro!: measurable_pair_swap)
-
-lemma measurable_ident[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
-  unfolding measurable_def by auto
+  by (auto dest: measurable_pair_swap)
 
 lemma measurable_Pair1': "x \<in> space M1 \<Longrightarrow> Pair x \<in> measurable M2 (M1 \<Otimes>\<^isub>M M2)"
-  by (auto intro!: measurable_Pair)
+  by simp
 
-lemma sets_Pair1: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
+lemma sets_Pair1[measurable (raw)]:
+  assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
 proof -
   have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
     using A[THEN sets_into_space] by (auto simp: space_pair_measure)
@@ -163,8 +168,11 @@
   unfolding Int_stable_def
   by safe (auto simp add: times_Int_times)
 
+lemma disjoint_family_vimageI: "disjoint_family F \<Longrightarrow> disjoint_family (\<lambda>i. f -` F i)"
+  by (auto simp: disjoint_family_on_def)
+
 lemma (in finite_measure) finite_measure_cut_measurable:
-  assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
+  assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^isub>M M)"
   shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
     (is "?s Q \<in> _")
   using Int_stable_pair_measure_generator pair_measure_closed assms
@@ -179,11 +187,10 @@
     by (auto intro!: measurable_If simp: space_pair_measure)
 next
   case (union F)
-  moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
-    unfolding sets_pair_measure[symmetric]
-    by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
+  moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
+    by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
   ultimately show ?case
-    by (auto simp: vimage_UN)
+    unfolding sets_pair_measure[symmetric] by simp
 qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
 
 lemma (in sigma_finite_measure) measurable_emeasure_Pair:
@@ -226,6 +233,17 @@
     by auto
 qed
 
+lemma (in sigma_finite_measure) measurable_emeasure[measurable (raw)]:
+  assumes space: "\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M"
+  assumes A: "{x\<in>space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^isub>M M)"
+  shows "(\<lambda>x. emeasure M (A x)) \<in> borel_measurable N"
+proof -
+  from space have "\<And>x. x \<in> space N \<Longrightarrow> Pair x -` {x \<in> space (N \<Otimes>\<^isub>M M). snd x \<in> A (fst x)} = A x"
+    by (auto simp: space_pair_measure)
+  with measurable_emeasure_Pair[OF A] show ?thesis
+    by (auto cong: measurable_cong)
+qed
+
 lemma (in sigma_finite_measure) emeasure_pair_measure:
   assumes "X \<in> sets (N \<Otimes>\<^isub>M M)"
   shows "emeasure (N \<Otimes>\<^isub>M M) X = (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator X (x, y) \<partial>M \<partial>N)" (is "_ = ?\<mu> X")
@@ -476,7 +494,7 @@
 
 lemma measurable_compose_Pair1:
   "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^isub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
-  by (rule measurable_compose[OF measurable_Pair]) auto
+  by simp
 
 lemma (in sigma_finite_measure) borel_measurable_positive_integral_fst':
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M)" "\<And>x. 0 \<le> f x"
@@ -527,9 +545,13 @@
     positive_integral_fst[of "\<lambda>x. max 0 (f x)"]
   unfolding positive_integral_max_0 by auto
 
-lemma (in sigma_finite_measure) borel_measurable_positive_integral:
-  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable M1"
-  using positive_integral_fst_measurable(1)[of "split f" M1] by simp
+lemma (in sigma_finite_measure) borel_measurable_positive_integral[measurable (raw)]:
+  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M) \<in> borel_measurable N"
+  using positive_integral_fst_measurable(1)[of "split f" N] by simp
+
+lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
+  "split f \<in> borel_measurable (N \<Otimes>\<^isub>M M) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M) \<in> borel_measurable N"
+  by (simp add: lebesgue_integral_def)
 
 lemma (in pair_sigma_finite) positive_integral_snd_measurable:
   assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
@@ -650,29 +672,6 @@
     by simp
 qed
 
-lemma (in pair_sigma_finite) positive_integral_fst_measurable':
-  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
-  shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
-  using M2.positive_integral_fst_measurable(1)[OF f] by simp
-
-lemma (in pair_sigma_finite) integral_fst_measurable:
-  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral> y. f x y \<partial>M2) \<in> borel_measurable M1"
-  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_fst_measurable')
-
-lemma (in pair_sigma_finite) positive_integral_snd_measurable':
-  assumes f: "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
-  shows "(\<lambda>y. \<integral>\<^isup>+ x. f x y \<partial>M1) \<in> borel_measurable M2"
-proof -
-  interpret Q: pair_sigma_finite M2 M1 ..
-  show ?thesis
-    using measurable_pair_swap[OF f]
-    by (intro Q.positive_integral_fst_measurable') (simp add: split_beta')
-qed
-
-lemma (in pair_sigma_finite) integral_snd_measurable:
-  "(\<lambda>x. f (fst x) (snd x)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>y. \<integral> x. f x y \<partial>M1) \<in> borel_measurable M2"
-  by (auto simp: lebesgue_integral_def intro!: borel_measurable_diff positive_integral_snd_measurable')
-
 lemma (in pair_sigma_finite) Fubini_integral:
   assumes f: "integrable (M1 \<Otimes>\<^isub>M M2) f"
   shows "(\<integral>y. (\<integral>x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1)"
@@ -739,48 +738,21 @@
 lemma pair_measure_density:
   assumes f: "f \<in> borel_measurable M1" "AE x in M1. 0 \<le> f x"
   assumes g: "g \<in> borel_measurable M2" "AE x in M2. 0 \<le> g x"
-  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
-  assumes "sigma_finite_measure (density M1 f)" "sigma_finite_measure (density M2 g)"
+  assumes "sigma_finite_measure M2" "sigma_finite_measure (density M2 g)"
   shows "density M1 f \<Otimes>\<^isub>M density M2 g = density (M1 \<Otimes>\<^isub>M M2) (\<lambda>(x,y). f x * g y)" (is "?L = ?R")
 proof (rule measure_eqI)
-  interpret M1: sigma_finite_measure M1 by fact
   interpret M2: sigma_finite_measure M2 by fact
-  interpret D1: sigma_finite_measure "density M1 f" by fact
   interpret D2: sigma_finite_measure "density M2 g" by fact
-  interpret L: pair_sigma_finite "density M1 f" "density M2 g" ..
-  interpret R: pair_sigma_finite M1 M2 ..
 
   fix A assume A: "A \<in> sets ?L"
-  then have indicator_eq: "\<And>x y. indicator A (x, y) = indicator (Pair x -` A) y"
-   and Pair_A: "\<And>x. Pair x -` A \<in> sets M2"
-    by (auto simp: indicator_def sets_Pair1)
-  have f_fst: "(\<lambda>p. f (fst p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
-    using measurable_comp[OF measurable_fst f(1)] by (simp add: comp_def)
-  have g_snd: "(\<lambda>p. g (snd p)) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2)"
-    using measurable_comp[OF measurable_snd g(1)] by (simp add: comp_def)
-  have "(\<lambda>x. \<integral>\<^isup>+ y. g (snd (x, y)) * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
-    using g_snd Pair_A A by (intro M2.positive_integral_fst_measurable) auto
-  then have int_g: "(\<lambda>x. \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2) \<in> borel_measurable M1"
-    by simp
-
-  show "emeasure ?L A = emeasure ?R A"
-    apply (subst D2.emeasure_pair_measure[OF A])
-    apply (subst emeasure_density)
-        using f_fst g_snd apply (simp add: split_beta')
-      using A apply simp
-    apply (subst positive_integral_density[OF g])
-      apply (simp add: indicator_eq Pair_A)
-    apply (subst positive_integral_density[OF f])
-      apply (rule int_g)
-    apply (subst M2.positive_integral_fst_measurable(2)[symmetric])
-      using f g A Pair_A f_fst g_snd
-      apply (auto intro!: positive_integral_cong_AE R.measurable_emeasure_Pair1
-                  simp: positive_integral_cmult indicator_eq split_beta')
-    apply (intro AE_I2 impI)
-    apply (subst mult_assoc)
-    apply (subst positive_integral_cmult)
-          apply auto
-    done
+  with f g have "(\<integral>\<^isup>+ x. f x * \<integral>\<^isup>+ y. g y * indicator A (x, y) \<partial>M2 \<partial>M1) =
+    (\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. f x * g y * indicator A (x, y) \<partial>M2 \<partial>M1)"
+    by (intro positive_integral_cong_AE)
+       (auto simp add: positive_integral_cmult[symmetric] ac_simps)
+  with A f g show "emeasure ?L A = emeasure ?R A"
+    by (simp add: D2.emeasure_pair_measure emeasure_density positive_integral_density
+                  M2.positive_integral_fst_measurable(2)[symmetric]
+             cong: positive_integral_cong)
 qed simp
 
 lemma sigma_finite_measure_distr:
@@ -792,7 +764,7 @@
   show ?thesis
   proof (unfold_locales, intro conjI exI allI)
     show "range (\<lambda>i. f -` A i \<inter> space M) \<subseteq> sets M"
-      using A f by (auto intro!: measurable_sets)
+      using A f by auto
     show "(\<Union>i. f -` A i \<inter> space M) = space M"
       using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def)
     fix i show "emeasure M (f -` A i \<inter> space M) \<noteq> \<infinity>"
@@ -800,47 +772,19 @@
   qed
 qed
 
-lemma measurable_cong':
-  assumes sets: "sets M = sets M'" "sets N = sets N'"
-  shows "measurable M N = measurable M' N'"
-  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
-
 lemma pair_measure_distr:
   assumes f: "f \<in> measurable M S" and g: "g \<in> measurable N T"
-  assumes "sigma_finite_measure (distr M S f)" "sigma_finite_measure (distr N T g)"
+  assumes "sigma_finite_measure (distr N T g)"
   shows "distr M S f \<Otimes>\<^isub>M distr N T g = distr (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). (f x, g y))" (is "?P = ?D")
 proof (rule measure_eqI)
-  show "sets ?P = sets ?D"
-    by simp
-  interpret S: sigma_finite_measure "distr M S f" by fact
   interpret T: sigma_finite_measure "distr N T g" by fact
-  interpret ST: pair_sigma_finite "distr M S f"  "distr N T g" ..
-  interpret M: sigma_finite_measure M by (rule sigma_finite_measure_distr) fact+
   interpret N: sigma_finite_measure N by (rule sigma_finite_measure_distr) fact+
-  interpret MN: pair_sigma_finite M N ..
-  interpret SN: pair_sigma_finite "distr M S f" N ..
-  have [simp]: 
-    "\<And>f g. fst \<circ> (\<lambda>(x, y). (f x, g y)) = f \<circ> fst" "\<And>f g. snd \<circ> (\<lambda>(x, y). (f x, g y)) = g \<circ> snd"
-    by auto
-  then have fg: "(\<lambda>(x, y). (f x, g y)) \<in> measurable (M \<Otimes>\<^isub>M N) (S \<Otimes>\<^isub>M T)"
-    using measurable_comp[OF measurable_fst f] measurable_comp[OF measurable_snd g]
-    by (auto simp: measurable_pair_iff)
+
   fix A assume A: "A \<in> sets ?P"
-  then have "emeasure ?P A = (\<integral>\<^isup>+x. emeasure (distr N T g) (Pair x -` A) \<partial>distr M S f)"
-    by (rule T.emeasure_pair_measure_alt)
-  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair x -` A) \<inter> space N) \<partial>distr M S f)"
-    using g A by (simp add: sets_Pair1 emeasure_distr)
-  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (g -` (Pair (f x) -` A) \<inter> space N) \<partial>M)"
-    using f g A ST.measurable_emeasure_Pair1[OF A]
-    by (intro positive_integral_distr) (auto simp add: sets_Pair1 emeasure_distr)
-  also have "\<dots> = (\<integral>\<^isup>+x. emeasure N (Pair x -` ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))) \<partial>M)"
-    by (intro positive_integral_cong arg_cong2[where f=emeasure]) (auto simp: space_pair_measure)
-  also have "\<dots> = emeasure (M \<Otimes>\<^isub>M N) ((\<lambda>(x, y). (f x, g y)) -` A \<inter> space (M \<Otimes>\<^isub>M N))"
-    using fg by (intro N.emeasure_pair_measure_alt[symmetric] measurable_sets[OF _ A])
-                (auto cong: measurable_cong')
-  also have "\<dots> = emeasure ?D A"
-    using fg A by (subst emeasure_distr) auto
-  finally show "emeasure ?P A = emeasure ?D A" .
-qed
+  with f g show "emeasure ?P A = emeasure ?D A"
+    by (auto simp add: N.emeasure_pair_measure_alt space_pair_measure emeasure_distr
+                       T.emeasure_pair_measure_alt positive_integral_distr
+             intro!: positive_integral_cong arg_cong[where f="emeasure N"])
+qed simp
 
 end
\ No newline at end of file

--- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -36,14 +36,14 @@
 lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
   unfolding borel_def pred_def by auto
 
-lemma borel_open[simp, measurable (raw generic)]:
+lemma borel_open[measurable (raw generic)]:
   assumes "open A" shows "A \<in> sets borel"
 proof -
   have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
   thus ?thesis unfolding borel_def by auto
 qed
 
-lemma borel_closed[simp, measurable (raw generic)]:
+lemma borel_closed[measurable (raw generic)]:
   assumes "closed A" shows "A \<in> sets borel"
 proof -
   have "space borel - (- A) \<in> sets borel"
@@ -51,11 +51,11 @@
   thus ?thesis by simp
 qed
 
-lemma borel_insert[measurable]:
-  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
+lemma borel_singleton[measurable]:
+  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
   unfolding insert_def by (rule Un) auto
 
-lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
+lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
   unfolding Compl_eq_Diff_UNIV by simp
 
 lemma borel_measurable_vimage:
@@ -74,19 +74,11 @@
     using assms[of S] by simp
 qed
 
-lemma borel_singleton[simp, intro]:
-  fixes x :: "'a::t1_space"
-  shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
-  proof (rule insert_in_sets)
-    show "{x} \<in> sets borel"
-      using closed_singleton[of x] by (rule borel_closed)
-  qed simp
-
-lemma borel_measurable_const[simp, intro, measurable (raw)]:
+lemma borel_measurable_const[measurable (raw)]:
   "(\<lambda>x. c) \<in> borel_measurable M"
   by auto
 
-lemma borel_measurable_indicator[simp, intro!]:
+lemma borel_measurable_indicator:
   assumes A: "A \<in> sets M"
   shows "indicator A \<in> borel_measurable M"
   unfolding indicator_def [abs_def] using A
@@ -137,7 +129,7 @@
   "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
   by simp
 
-lemma [simp, intro, measurable]:
+lemma [measurable]:
   fixes a b :: "'a\<Colon>ordered_euclidean_space"
   shows lessThan_borel: "{..< a} \<in> sets borel"
     and greaterThan_borel: "{a <..} \<in> sets borel"
@@ -151,13 +143,13 @@
   by (blast intro: borel_open borel_closed)+
 
 lemma 
-  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
-    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
-    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
-    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
+  shows hafspace_less_borel: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
+    and hafspace_greater_borel: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
+    and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
+    and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
   by simp_all
 
-lemma borel_measurable_less[simp, intro, measurable]:
+lemma borel_measurable_less[measurable]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -169,7 +161,7 @@
     by simp
 qed
 
-lemma [simp, intro]:
+lemma
   fixes f :: "'a \<Rightarrow> real"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
@@ -633,7 +625,7 @@
   using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
   by (simp add: comp_def)
 
-lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
+lemma borel_measurable_uminus[measurable (raw)]:
   fixes g :: "'a \<Rightarrow> real"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. - g x) \<in> borel_measurable M"
@@ -644,7 +636,7 @@
   shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
   unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
 
-lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
+lemma borel_measurable_Pair[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -675,8 +667,8 @@
 
 lemma borel_measurable_continuous_Pair:
   fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
-  assumes [simp]: "f \<in> borel_measurable M"
-  assumes [simp]: "g \<in> borel_measurable M"
+  assumes [measurable]: "f \<in> borel_measurable M"
+  assumes [measurable]: "g \<in> borel_measurable M"
   assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
   shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
 proof -
@@ -685,7 +677,7 @@
     unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
 qed
 
-lemma borel_measurable_add[simp, intro, measurable (raw)]:
+lemma borel_measurable_add[measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -694,7 +686,7 @@
   by (rule borel_measurable_continuous_Pair)
      (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
 
-lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
+lemma borel_measurable_setsum[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
@@ -703,14 +695,14 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_diff[simp, intro, measurable (raw)]:
+lemma borel_measurable_diff[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-  unfolding diff_minus using assms by fast
+  unfolding diff_minus using assms by simp
 
-lemma borel_measurable_times[simp, intro, measurable (raw)]:
+lemma borel_measurable_times[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -724,7 +716,7 @@
   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
 
-lemma borel_measurable_dist[simp, intro, measurable (raw)]:
+lemma borel_measurable_dist[measurable (raw)]:
   fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -769,7 +761,7 @@
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
   using affine_borel_measurable_vector[of f M a 1] by simp
 
-lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
+lemma borel_measurable_setprod[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -778,53 +770,36 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
+lemma borel_measurable_inverse[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
 proof -
-  have *: "\<And>x::real. inverse x = (if x \<in> UNIV - {0} then inverse x else 0)" by auto
-  show ?thesis
-    apply (subst *)
-    apply (rule borel_measurable_continuous_on_open)
-    apply (auto intro!: f continuous_on_inverse continuous_on_id)
-    done
+  have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) \<in> borel_measurable borel"
+    by (intro borel_measurable_continuous_on_open' continuous_on_inverse continuous_on_id) auto
+  also have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) = inverse" by (intro ext) auto
+  finally show ?thesis using f by simp
 qed
 
-lemma borel_measurable_divide[simp, intro, measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
-  and "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
-  unfolding field_divide_inverse
-  by (rule borel_measurable_inverse borel_measurable_times assms)+
+lemma borel_measurable_divide[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x::real) \<in> borel_measurable M"
+  by (simp add: field_divide_inverse)
 
-lemma borel_measurable_max[intro, simp, measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  unfolding max_def by (auto intro!: assms measurable_If)
+lemma borel_measurable_max[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: real) \<in> borel_measurable M"
+  by (simp add: max_def)
 
-lemma borel_measurable_min[intro, simp, measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
-  unfolding min_def by (auto intro!: assms measurable_If)
+lemma borel_measurable_min[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: real) \<in> borel_measurable M"
+  by (simp add: min_def)
 
-lemma borel_measurable_abs[simp, intro, measurable (raw)]:
-  assumes "f \<in> borel_measurable M"
-  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
-proof -
-  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
-  show ?thesis unfolding * using assms by auto
-qed
+lemma borel_measurable_abs[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
+  unfolding abs_real_def by simp
 
-lemma borel_measurable_nth[simp, intro, measurable (raw)]:
+lemma borel_measurable_nth[measurable (raw)]:
   "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
-  using borel_measurable_euclidean_component'
-  unfolding nth_conv_component by auto
+  by (simp add: nth_conv_component)
 
 lemma convex_measurable:
   fixes a b :: real
@@ -843,7 +818,7 @@
   finally show ?thesis .
 qed
 
-lemma borel_measurable_ln[simp, intro, measurable (raw)]:
+lemma borel_measurable_ln[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
 proof -
@@ -864,7 +839,7 @@
   finally show ?thesis .
 qed
 
-lemma borel_measurable_log[simp, intro, measurable (raw)]:
+lemma borel_measurable_log[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
   unfolding log_def by auto
 
@@ -902,17 +877,17 @@
 lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   by simp
 
-lemma borel_measurable_real_natfloor[intro, simp]:
+lemma borel_measurable_real_natfloor:
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   by simp
 
 subsection "Borel space on the extended reals"
 
-lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
+lemma borel_measurable_ereal[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   using continuous_on_ereal f by (rule borel_measurable_continuous_on)
 
-lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
+lemma borel_measurable_real_of_ereal[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> ereal" 
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
@@ -937,10 +912,10 @@
 qed
 
 lemma
-  fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
-  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
-    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
-    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
+  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
+  shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
+    and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
+    and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
 
 lemma borel_measurable_uminus_eq_ereal[simp]:
@@ -968,15 +943,18 @@
     by (subst *) (simp del: space_borel split del: split_if)
 qed
 
-lemma
+lemma [measurable]:
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
-  shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
-    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
-    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
-    and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
-  using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
+  shows borel_measurable_ereal_le: "{x \<in> space M. f x \<le> g x} \<in> sets M"
+    and borel_measurable_ereal_less: "{x \<in> space M. f x < g x} \<in> sets M"
+    and borel_measurable_ereal_eq: "{w \<in> space M. f w = g w} \<in> sets M"
+  using f g by (simp_all add: set_Collect_ereal2)
+
+lemma borel_measurable_ereal_neq:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> {w \<in> space M. f w \<noteq> (g w :: ereal)} \<in> sets M"
+  by simp
 
 lemma borel_measurable_ereal_iff:
   shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
@@ -1102,24 +1080,24 @@
     and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
   using f by auto
 
-lemma [intro, simp, measurable(raw)]:
+lemma [measurable(raw)]:
   fixes f :: "'a \<Rightarrow> ereal"
-  assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
     and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
     and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
     and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
+  by (simp_all add: borel_measurable_ereal2 min_def max_def)
 
-lemma [simp, intro, measurable(raw)]:
+lemma [measurable(raw)]:
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
     and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
-  unfolding minus_ereal_def divide_ereal_def using assms by auto
+  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
 
-lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
+lemma borel_measurable_ereal_setsum[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1129,7 +1107,7 @@
     by induct auto
 qed simp
 
-lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
+lemma borel_measurable_ereal_setprod[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1138,7 +1116,7 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_SUP[simp, intro,measurable (raw)]:
+lemma borel_measurable_SUP[measurable (raw)]:
   fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
@@ -1151,7 +1129,7 @@
     using assms by auto
 qed
 
-lemma borel_measurable_INF[simp, intro,measurable (raw)]:
+lemma borel_measurable_INF[measurable (raw)]:
   fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
@@ -1164,13 +1142,45 @@
     using assms by auto
 qed
 
-lemma [simp, intro, measurable (raw)]:
+lemma [measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M"
   shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
     and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
 
+lemma sets_Collect_eventually_sequientially[measurable]:
+  "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
+  unfolding eventually_sequentially by simp
+
+lemma convergent_ereal:
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
+  using ereal_Liminf_eq_Limsup_iff[of sequentially]
+  by (auto simp: convergent_def)
+
+lemma convergent_ereal_limsup:
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "convergent X \<Longrightarrow> limsup X = lim X"
+  by (auto simp: convergent_def limI lim_imp_Limsup)
+
+lemma sets_Collect_ereal_convergent[measurable]: 
+  fixes f :: "nat \<Rightarrow> 'a => ereal"
+  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
+  shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
+  unfolding convergent_ereal by auto
+
+lemma borel_measurable_extreal_lim[measurable (raw)]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
+  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
+  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
+proof -
+  have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
+    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
+  then show ?thesis
+    by simp
+qed
+
 lemma borel_measurable_ereal_LIMSEQ:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
@@ -1179,17 +1189,14 @@
 proof -
   have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
     using u' by (simp add: lim_imp_Liminf[symmetric])
-  then show ?thesis by (simp add: u cong: measurable_cong)
+  with u show ?thesis by (simp cong: measurable_cong)
 qed
 
-lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
+lemma borel_measurable_extreal_suminf[measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
+  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
-  apply (subst measurable_cong)
-  apply (subst suminf_ereal_eq_SUPR)
-  apply (rule pos)
-  using assms by auto
+  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
 section "LIMSEQ is borel measurable"
 

--- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -56,7 +56,7 @@
 
 lemma merge_commute:
   "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
-  by (auto simp: merge_def intro!: ext)
+  by (force simp: merge_def)
 
 lemma Pi_cancel_merge_range[simp]:
   "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
@@ -430,7 +430,7 @@
     by (auto simp add: sets_PiM intro!: sigma_sets_top)
 next
   assume "J \<noteq> {}" with assms show ?thesis
-    by (auto simp add: sets_PiM prod_algebra_def intro!: sigma_sets.Basic)
+    by (force simp add: sets_PiM prod_algebra_def)
 qed
 
 lemma measurable_PiM:
@@ -475,24 +475,12 @@
   finally show "f -` A \<inter> space N \<in> sets N" .
 qed (auto simp: space)
 
-lemma sets_PiM_I_finite[simp, intro]:
+lemma sets_PiM_I_finite[measurable]:
   assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
   shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
   using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
 
-lemma measurable_component_update:
-  assumes "x \<in> space (Pi\<^isub>M I M)" and "i \<notin> I"
-  shows "(\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)" (is "?f \<in> _")
-proof (intro measurable_PiM_single)
-  fix j A assume "j \<in> insert i I" "A \<in> sets (M j)"
-  moreover have "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} =
-    (if i = j then space (M i) \<inter> A else if x j \<in> A then space (M i) else {})"
-    by auto
-  ultimately show "{\<omega> \<in> space (M i). (x(i := \<omega>)) j \<in> A} \<in> sets (M i)"
-    by auto
-qed (insert sets_into_space assms, auto simp: space_PiM)
-
-lemma measurable_component_singleton:
+lemma measurable_component_singleton[measurable (raw)]:
   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
 proof (unfold measurable_def, intro CollectI conjI ballI)
   fix A assume "A \<in> sets (M i)"
@@ -503,7 +491,7 @@
     using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
 qed (insert `i \<in> I`, auto simp: space_PiM)
 
-lemma measurable_add_dim:
+lemma measurable_add_dim[measurable]:
   "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
     (is "?f \<in> measurable ?P ?I")
 proof (rule measurable_PiM_single)
@@ -517,7 +505,11 @@
   finally show "{\<omega> \<in> space ?P. prod_case (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
 qed (auto simp: space_pair_measure space_PiM)
 
-lemma measurable_merge:
+lemma measurable_component_update:
+  "x \<in> space (Pi\<^isub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^isub>M (insert i I) M)"
+  by simp
+
+lemma measurable_merge[measurable]:
   "merge I J \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) (Pi\<^isub>M (I \<union> J) M)"
     (is "?f \<in> measurable ?P ?U")
 proof (rule measurable_PiM_single)
@@ -531,7 +523,7 @@
   finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
 qed (auto simp: space_pair_measure space_PiM Pi_iff merge_def extensional_def)
 
-lemma measurable_restrict:
+lemma measurable_restrict[measurable (raw)]:
   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
   shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^isub>M I M)"
 proof (rule measurable_PiM_single)
@@ -542,6 +534,31 @@
     using A X by (auto intro!: measurable_sets)
 qed (insert X, auto dest: measurable_space)
 
+lemma sets_in_Pi_aux:
+  "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
+  {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
+  by (simp add: subset_eq Pi_iff)
+
+lemma sets_in_Pi[measurable (raw)]:
+  "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
+  (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
+  Sigma_Algebra.pred N (\<lambda>x. f x \<in> Pi I F)"
+  unfolding pred_def
+  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
+
+lemma sets_in_extensional_aux:
+  "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
+proof -
+  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
+    by (auto simp add: extensional_def space_PiM)
+  then show ?thesis by simp
+qed
+
+lemma sets_in_extensional[measurable (raw)]:
+  "f \<in> measurable N (PiM I M) \<Longrightarrow> Sigma_Algebra.pred N (\<lambda>x. f x \<in> extensional I)"
+  unfolding pred_def
+  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
+
 locale product_sigma_finite =
   fixes M :: "'i \<Rightarrow> 'a measure"
   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
@@ -665,7 +682,7 @@
   qed (auto intro!: setprod_cong)
   with insert show ?case
     by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
-qed (simp add: emeasure_PiM_empty)
+qed simp
 
 lemma (in product_sigma_finite) sigma_finite: 
   assumes "finite I"
@@ -759,18 +776,18 @@
     show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
   next
     fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
-    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>I \<union> J. F i \<in> sets (M i)"
+    with fin obtain F where A_eq: "A = (Pi\<^isub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
       by (auto simp add: prod_algebra_eq_finite)
     let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
     let ?X = "?g -` A \<inter> space ?B"
     have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
-      using F[rule_format, THEN sets_into_space] by (auto simp: space_PiM)
+      using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
     then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
       unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
     have "emeasure ?D A = emeasure ?B ?X"
       using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
     also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
-      using `finite J` `finite I` F X
+      using `finite J` `finite I` F unfolding X
       by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times Pi_iff)
     also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
       using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod_Un_one)
@@ -1013,8 +1030,7 @@
 
 lemma sets_Collect_single:
   "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^isub>M I M). x i \<in> A } \<in> sets (Pi\<^isub>M I M)"
-  unfolding sets_PiM_single
-  by (auto intro!: sigma_sets.Basic exI[of _ i] exI[of _ A]) (auto simp: space_PiM)
+  by simp
 
 lemma sigma_prod_algebra_sigma_eq_infinite:
   fixes E :: "'i \<Rightarrow> 'a set set"
@@ -1127,7 +1143,7 @@
     by (simp add: P_closed)
   show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
     using `finite I`
-    by (auto intro!: sigma_sets_subset simp: E_generates P_def)
+    by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
 qed
 
 end

--- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -1004,6 +1004,9 @@
   "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
   using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
 
+lemma measurable_id_prod[measurable (raw)]: "i = j \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)"
+  by simp
+
 lemma (in product_sigma_finite) distr_component:
   "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
 proof (intro measure_eqI[symmetric])
@@ -1015,15 +1018,10 @@
   fix A assume A: "A \<in> sets ?P"
   then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 
     by simp
-  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) x \<partial>M i)" 
-    apply (subst product_positive_integral_singleton[symmetric])
-    apply (force intro!: measurable_restrict measurable_sets A)
-    apply (auto intro!: positive_integral_cong simp: space_PiM indicator_def simp: eq)
-    done
-  also have "\<dots> = emeasure (M i) ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i))"
-    by (force intro!: measurable_restrict measurable_sets A positive_integral_indicator)
+  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
+    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
   also have "\<dots> = emeasure ?D A"
-    using A by (auto intro!: emeasure_distr[symmetric] measurable_restrict) 
+    using A by (simp add: product_positive_integral_singleton emeasure_distr)
   finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
 qed simp
 

--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -99,7 +99,8 @@
   
   fix X assume "X \<in> ?J"
   then obtain E where [simp]: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
-  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)" by auto
+  with `finite J` have X: "X \<in> sets (Pi\<^isub>M J M)"
+    by simp
 
   have "emeasure ?P X = (\<Prod> i\<in>J. emeasure (M i) (E i))"
     using E by (simp add: J.measure_times)
@@ -190,7 +191,7 @@
       unfolding sets_PiM
     proof (safe intro!: sigma_sets_subseteq)
       fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
-        by (auto intro!: generatorI' elim!: prod_algebraE)
+        by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
     qed
   qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
 qed
@@ -242,10 +243,8 @@
 qed
 
 lemma (in product_prob_space) merge_sets:
-  assumes "J \<inter> K = {}" and A: "A \<in> sets (Pi\<^isub>M (J \<union> K) M)" and x: "x \<in> space (Pi\<^isub>M J M)"
-  shows "(\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
-  by (rule measurable_sets[OF _ A] measurable_compose[OF measurable_Pair measurable_merge]  
-           measurable_const x measurable_ident)+
+  "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
+  by simp
 
 lemma (in product_prob_space) merge_emb:
   assumes "K \<subseteq> I" "J \<subseteq> I" and y: "y \<in> space (Pi\<^isub>M J M)"
@@ -622,7 +621,7 @@
     then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
       by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
     have "emb I J (Pi\<^isub>E J X) \<in> generator"
-      using J `I \<noteq> {}` by (intro generatorI') auto
+      using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
     then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
       using \<mu> by simp
     also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"

--- a/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -84,10 +84,14 @@
   shows "entropy_density b M N \<in> borel_measurable M"
 proof -
   from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
-    unfolding entropy_density_def
-    by (intro measurable_comp) auto
+    unfolding entropy_density_def by auto
 qed
 
+lemma borel_measurable_RN_deriv_density[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> RN_deriv M (density M f) \<in> borel_measurable M"
+  using borel_measurable_RN_deriv_density[of "\<lambda>x. max 0 (f x )" M]
+  by (simp add: density_max_0[symmetric])
+
 lemma (in sigma_finite_measure) KL_density:
   fixes f :: "'a \<Rightarrow> real"
   assumes "1 < b"
@@ -97,7 +101,7 @@
 proof (subst integral_density)
   show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
     using f
-    by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
+    by (auto simp: comp_def entropy_density_def)
   have "density M (RN_deriv M (density M f)) = density M f"
     using f by (intro density_RN_deriv_density) auto
   then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
@@ -366,7 +370,7 @@
   shows "AE x in P. 0 \<le> g (T x)"
   using g
   apply (subst AE_distr_iff[symmetric, OF T(1)])
-  apply (simp add: distributed_borel_measurable)
+  apply simp
   apply (rule absolutely_continuous_AE[OF _ T(2)])
   apply simp
   apply (simp add: distributed_AE)
@@ -409,7 +413,7 @@
 lemma distributed_integrable:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
     integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
-  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
+  by (auto simp: distributed_real_AE
                     distributed_distr_eq_density[symmetric] integral_density[symmetric] integrable_distr_eq)
   
 lemma distributed_transform_integrable:
@@ -446,7 +450,7 @@
   shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
   using assms unfolding finite_entropy_def
   using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
-  by (auto dest!: distributed_real_measurable)
+  by auto
 
 subsection {* Mutual Information *}
 
@@ -464,7 +468,7 @@
       mutual_information b S T X Y = 0)"
   unfolding indep_var_distribution_eq
 proof safe
-  assume rv: "random_variable S X" "random_variable T Y"
+  assume rv[measurable]: "random_variable S X" "random_variable T Y"
 
   interpret X: prob_space "distr M S X"
     by (rule prob_space_distr) fact
@@ -474,7 +478,7 @@
   interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
 
   interpret Q: prob_space Q unfolding Q_def
-    by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)
+    by (rule prob_space_distr) simp
 
   { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
     then have [simp]: "Q = P"  unfolding Q_def P_def by simp
@@ -536,9 +540,9 @@
     using Fxy by (auto simp: finite_entropy_def)
 
   have X: "random_variable S X"
-    using Px by (auto simp: distributed_def finite_entropy_def)
+    using Px by auto
   have Y: "random_variable T Y"
-    using Py by (auto simp: distributed_def finite_entropy_def)
+    using Py by auto
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T ..
@@ -568,7 +572,6 @@
     show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
       "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
       using Px Py by (auto simp: distributed_def)
-    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
     show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   qed (fact | simp)+
   
@@ -675,7 +678,6 @@
     show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
       "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
       using Px Py by (auto simp: distributed_def)
-    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
     show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
   qed (fact | simp)+
   
@@ -1009,11 +1011,11 @@
 
 lemma (in information_space)
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
-  assumes Px: "distributed M S X Px"
-  assumes Pz: "distributed M P Z Pz"
-  assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
-  assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
-  assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
+  assumes Px[measurable]: "distributed M S X Px"
+  assumes Pz[measurable]: "distributed M P Z Pz"
+  assumes Pyz[measurable]: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
+  assumes Pxz[measurable]: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
+  assumes Pxyz[measurable]: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
   assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
   assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
   shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
@@ -1033,56 +1035,38 @@
   have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
   have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
     using Pyz by (simp add: distributed_measurable)
-
-  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
-    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
-
-  { fix f g h M
-    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
-    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
-         measurable_comp[OF f Px[THEN distributed_real_measurable]]
-         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
-    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
-      by (simp add: comp_def b_gt_1) }
-  note borel_log = this
-
-  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
-    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
   
   from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
     distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
-    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
+    by (simp add: comp_def distr_distr)
 
   have "mutual_information b S P X Z =
     (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
     by (rule mutual_information_distr[OF S P Px Pz Pxz])
   also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
     using b_gt_1 Pxz Px Pz
-    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
-       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
-             dest!: distributed_real_measurable)
+    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"]) (auto simp: split_beta')
   finally have mi_eq:
     "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
   
   have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
     by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
   moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
-    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
+    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
   moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
-    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
+    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
   moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
-    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
+    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
   moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
-    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
+    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
   moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
-    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
+    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
   moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
-    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
+    using Pz Pz[THEN distributed_real_measurable]
+    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
     using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
-    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
-    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
-    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
+    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure)
   moreover note Pxyz[THEN distributed_real_AE]
   ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
     Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
@@ -1110,52 +1094,36 @@
   let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
   interpret P: prob_space ?P
     unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
-    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
+    by (rule prob_space_distr) simp
 
   let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
   interpret Q: prob_space ?Q
     unfolding distributed_distr_eq_density[OF Pyz, symmetric]
-    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
+    by (rule prob_space_distr) simp
 
   let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
 
   from subdensity_real[of snd, OF _ Pyz Pz]
   have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
   have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
-    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
+    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
 
   have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
     using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
-    apply (intro TP.AE_pair_measure)
-    apply (auto simp: comp_def measurable_split_conv
-                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
-                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
-                        measurable_Pair
-                dest: distributed_real_AE distributed_real_measurable)
-    done
+    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
 
-  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
-           measurable_compose[OF _ measurable_snd]
-           measurable_Pair
-           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
-           TP.borel_measurable_positive_integral
   have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
     apply (subst positive_integral_density)
-    apply (rule distributed_borel_measurable[OF Pxyz])
+    apply simp
     apply (rule distributed_AE[OF Pxyz])
-    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
+    apply auto []
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
     apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
     done
   also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
-    by (subst STP.positive_integral_snd_measurable[symmetric])
-       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
+    by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
   also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
     apply (rule positive_integral_cong_AE)
     using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
@@ -1164,44 +1132,41 @@
     fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
       "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
-      apply (subst positive_integral_multc)
-      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
-                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
-                  split: prod.split)
-      done
+      by (subst positive_integral_multc)
+         (auto intro!: divide_nonneg_nonneg split: prod.split)
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
-    by (subst positive_integral_density[symmetric]) (auto intro!: M)
+    by (subst positive_integral_density[symmetric]) auto
   finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
   also have "\<dots> < \<infinity>" by simp
   finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
 
   have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
     apply (subst positive_integral_density)
-    apply (rule distributed_borel_measurable[OF Pxyz])
+    apply simp
     apply (rule distributed_AE[OF Pxyz])
-    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
+    apply auto []
     apply (simp add: split_beta')
   proof
     let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
     assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
-      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
+      by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
       by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
     then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
       by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
     with P.emeasure_space_1 show False
-      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
+      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
   qed
 
   have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
     apply (rule positive_integral_0_iff_AE[THEN iffD2])
-    apply (auto intro!: M simp: split_beta') []
+    apply simp
     apply (subst AE_density)
-    apply (auto intro!: M simp: split_beta') []
+    apply simp
     using ae5 ae6 ae7 ae8
     apply eventually_elim
     apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
@@ -1210,7 +1175,7 @@
   have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
     apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
     using ae
-    apply (auto intro!: M simp: split_beta')
+    apply (auto simp: split_beta')
     done
 
   have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
@@ -1230,15 +1195,15 @@
       by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
     show "integrable ?P ?f"
       unfolding integrable_def 
-      using fin neg by (auto intro!: M simp: split_beta')
+      using fin neg by (auto simp: split_beta')
     show "integrable ?P (\<lambda>x. - log b (?f x))"
       apply (subst integral_density)
-      apply (auto intro!: M) []
-      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
-      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
+      apply simp
+      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
+      apply simp
       apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
-      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
-      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
+      apply simp
+      apply simp
       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
       apply eventually_elim
       apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
@@ -1247,9 +1212,9 @@
   also have "\<dots> = conditional_mutual_information b S T P X Y Z"
     unfolding `?eq`
     apply (subst integral_density)
-    apply (auto intro!: M) []
-    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
-    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
+    apply simp
+    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
+    apply simp
     apply (intro integral_cong_AE)
     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
     apply eventually_elim
@@ -1271,11 +1236,11 @@
     = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" (is "?eq")
     and conditional_mutual_information_generic_nonneg': "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
 proof -
-  note Px = Fx[THEN finite_entropy_distributed]
-  note Pz = Fz[THEN finite_entropy_distributed]
-  note Pyz = Fyz[THEN finite_entropy_distributed]
-  note Pxz = Fxz[THEN finite_entropy_distributed]
-  note Pxyz = Fxyz[THEN finite_entropy_distributed]
+  note Px = Fx[THEN finite_entropy_distributed, measurable]
+  note Pz = Fz[THEN finite_entropy_distributed, measurable]
+  note Pyz = Fyz[THEN finite_entropy_distributed, measurable]
+  note Pxz = Fxz[THEN finite_entropy_distributed, measurable]
+  note Pxyz = Fxyz[THEN finite_entropy_distributed, measurable]
 
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
@@ -1288,27 +1253,10 @@
   interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
   have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
   have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
-  have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
-    using Pyz by (simp add: distributed_measurable)
 
-  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
-    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
-
-  { fix f g h M
-    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
-    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
-         measurable_comp[OF f Px[THEN distributed_real_measurable]]
-         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
-    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
-      by (simp add: comp_def b_gt_1) }
-  note borel_log = this
-
-  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
-    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
-  
   from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
     distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
-    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
+    by (simp add: distr_distr comp_def)
 
   have "mutual_information b S P X Z =
     (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
@@ -1316,29 +1264,26 @@
   also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
     using b_gt_1 Pxz Px Pz
     by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
-       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
-             dest!: distributed_real_measurable)
+       (auto simp: split_beta')
   finally have mi_eq:
     "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
   
   have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
     by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
   moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
-    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
+    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
   moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
-    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
+    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
   moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
-    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
+    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
   moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
-    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
+    using Px by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
   moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
-    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
+    using Pyz by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
   moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
-    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
+    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
   moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
     using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
-    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
-    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
     by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
   moreover note ae9 = Pxyz[THEN distributed_real_AE]
   ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
@@ -1364,8 +1309,7 @@
     using finite_entropy_integrable_transform[OF Fyz Pxyz, of snd]
     by simp
   moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z)))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
-    using Pxyz Px Pyz
-    by (auto intro!: borel_measurable_times measurable_fst'' measurable_snd'' dest!: distributed_real_measurable simp: split_beta')
+    using Pxyz Px Pyz by simp
   ultimately have I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
     apply (rule integrable_cong_AE_imp)
     using ae1 ae4 ae5 ae6 ae9
@@ -1377,12 +1321,10 @@
     using finite_entropy_integrable_transform[OF Fxz Pxyz, of "\<lambda>x. (fst x, snd (snd x))"]
     using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
     using finite_entropy_integrable_transform[OF Fz Pxyz, of "snd \<circ> snd"]
-    by (simp add: measurable_Pair measurable_snd'' comp_def)
+    by simp
   moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z))) \<in> borel_measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)"
     using Pxyz Px Pz
-    by (auto intro!: measurable_compose[OF _ distributed_real_measurable[OF Pxz]]
-                     measurable_Pair borel_measurable_times measurable_fst'' measurable_snd''
-             dest!: distributed_real_measurable simp: split_beta')
+    by auto
   ultimately have I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
     apply (rule integrable_cong_AE_imp)
     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
@@ -1399,45 +1341,27 @@
 
   let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
   interpret P: prob_space ?P
-    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
-    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
+    unfolding distributed_distr_eq_density[OF Pxyz, symmetric] by (rule prob_space_distr) simp
 
   let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
   interpret Q: prob_space ?Q
-    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
-    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
+    unfolding distributed_distr_eq_density[OF Pyz, symmetric] by (rule prob_space_distr) simp
 
   let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
 
   from subdensity_real[of snd, OF _ Pyz Pz]
   have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
   have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
-    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
+    using Pz by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
 
   have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
     using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
-    apply (intro TP.AE_pair_measure)
-    apply (auto simp: comp_def measurable_split_conv
-                intro!: measurable_snd'' measurable_fst'' borel_measurable_ereal_eq borel_measurable_ereal
-                        S.borel_measurable_positive_integral measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
-                        measurable_Pair
-                dest: distributed_real_AE distributed_real_measurable)
-    done
-
-  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
-           measurable_compose[OF _ measurable_snd]
-           measurable_Pair
-           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
-           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
-           TP.borel_measurable_positive_integral
+    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
   have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
     apply (subst positive_integral_density)
     apply (rule distributed_borel_measurable[OF Pxyz])
     apply (rule distributed_AE[OF Pxyz])
-    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
+    apply simp
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
@@ -1445,7 +1369,7 @@
     done
   also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric])
-       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
+       (auto simp add: split_beta')
   also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
     apply (rule positive_integral_cong_AE)
     using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
@@ -1454,44 +1378,40 @@
     fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
       "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
     then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
-      apply (subst positive_integral_multc)
-      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
-                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
-                  split: prod.split)
-      done
+      by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
   qed
   also have "\<dots> = 1"
     using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
-    by (subst positive_integral_density[symmetric]) (auto intro!: M)
+    by (subst positive_integral_density[symmetric]) auto
   finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
   also have "\<dots> < \<infinity>" by simp
   finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
 
   have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
     apply (subst positive_integral_density)
-    apply (rule distributed_borel_measurable[OF Pxyz])
+    apply simp
     apply (rule distributed_AE[OF Pxyz])
-    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
+    apply simp
     apply (simp add: split_beta')
   proof
     let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
     assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
-      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
+      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
     then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
       by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
     then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
       by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
     with P.emeasure_space_1 show False
-      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
+      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
   qed
 
   have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
     apply (rule positive_integral_0_iff_AE[THEN iffD2])
-    apply (auto intro!: M simp: split_beta') []
+    apply (auto simp: split_beta') []
     apply (subst AE_density)
-    apply (auto intro!: M simp: split_beta') []
+    apply (auto simp: split_beta') []
     using ae5 ae6 ae7 ae8
     apply eventually_elim
     apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
@@ -1500,7 +1420,7 @@
   have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
     apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
     using ae
-    apply (auto intro!: M simp: split_beta')
+    apply (auto simp: split_beta')
     done
 
   have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
@@ -1520,15 +1440,15 @@
       by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
     show "integrable ?P ?f"
       unfolding integrable_def 
-      using fin neg by (auto intro!: M simp: split_beta')
+      using fin neg by (auto simp: split_beta')
     show "integrable ?P (\<lambda>x. - log b (?f x))"
       apply (subst integral_density)
-      apply (auto intro!: M) []
-      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
-      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
+      apply simp
+      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
+      apply simp
       apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
-      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
-      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
+      apply simp
+      apply simp
       using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
       apply eventually_elim
       apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
@@ -1537,9 +1457,9 @@
   also have "\<dots> = conditional_mutual_information b S T P X Y Z"
     unfolding `?eq`
     apply (subst integral_density)
-    apply (auto intro!: M) []
-    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
-    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
+    apply simp
+    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
+    apply simp
     apply (intro integral_cong_AE)
     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
     apply eventually_elim
@@ -1633,8 +1553,8 @@
 lemma (in information_space) conditional_entropy_generic_eq:
   fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
-  assumes Py: "distributed M T Y Py"
-  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
+  assumes Py[measurable]: "distributed M T Y Py"
+  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
 proof -
   interpret S: sigma_finite_measure S by fact

--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -121,7 +121,7 @@
   shows "simple_function M f \<longleftrightarrow> simple_function N f"
   unfolding simple_function_def assms ..
 
-lemma borel_measurable_simple_function:
+lemma borel_measurable_simple_function[measurable_dest]:
   assumes "simple_function M f"
   shows "f \<in> borel_measurable M"
 proof (rule borel_measurableI)
@@ -918,7 +918,7 @@
   hence "a \<noteq> 0" by auto
   let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}"
   have B: "\<And>i. ?B i \<in> sets M"
-    using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
+    using f `simple_function M u` by auto
 
   let ?uB = "\<lambda>i x. u x * indicator (?B i) x"
 
@@ -1436,6 +1436,10 @@
   "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
     (\<integral>\<^isup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
 
+lemma borel_measurable_integrable[measurable_dest]:
+  "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
+  by (auto simp: integrable_def)
+
 lemma integrableD[dest]:
   assumes "integrable M f"
   shows "f \<in> borel_measurable M" "(\<integral>\<^isup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>"
@@ -1776,7 +1780,7 @@
 qed
 
 lemma integrable_abs:
-  assumes f: "integrable M f"
+  assumes f[measurable]: "integrable M f"
   shows "integrable M (\<lambda> x. \<bar>f x\<bar>)"
 proof -
   from assms have *: "(\<integral>\<^isup>+x. ereal (- \<bar>f x\<bar>)\<partial>M) = 0"
@@ -1871,7 +1875,7 @@
     from mono pos show "AE x in M. ereal (f i x) \<le> ereal (f (Suc i) x) \<and> 0 \<le> ereal (f i x)"
       by eventually_elim (auto simp: mono_def)
     show "(\<lambda>x. ereal (f i x)) \<in> borel_measurable M"
-      using i by (auto simp: integrable_def)
+      using i by auto
   next
     show "(\<integral>\<^isup>+ x. ereal (u x) \<partial>M) = \<integral>\<^isup>+ x. (SUP i. ereal (f i x)) \<partial>M"
       apply (rule positive_integral_cong_AE)
@@ -2045,10 +2049,10 @@
   using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
 
 lemma integral_dominated_convergence:
-  assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
-  and w: "integrable M w"
+  assumes u[measurable]: "\<And>i. integrable M (u i)" and bound: "\<And>j. AE x in M. \<bar>u j x\<bar> \<le> w x"
+  and w[measurable]: "integrable M w"
   and u': "AE x in M. (\<lambda>i. u i x) ----> u' x"
-  and borel: "u' \<in> borel_measurable M"
+  and [measurable]: "u' \<in> borel_measurable M"
   shows "integrable M u'"
   and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
   and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
@@ -2120,7 +2124,7 @@
       qed (rule trivial_limit_sequentially)
     qed
     also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^isup>+ x. max 0 (ereal (?diff n x)) \<partial>M)"
-      using borel w u unfolding integrable_def
+      using w u unfolding integrable_def
       by (intro positive_integral_lim_INF) (auto intro!: positive_integral_lim_INF)
     also have "\<dots> = (\<integral>\<^isup>+ x. ereal (2 * w x) \<partial>M) -
         limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
@@ -2171,7 +2175,7 @@
 qed
 
 lemma integral_sums:
-  assumes borel: "\<And>i. integrable M (f i)"
+  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
   and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
   and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
   shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
@@ -2182,7 +2186,7 @@
   from bchoice[OF this]
   obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
   then have w_borel: "w \<in> borel_measurable M" unfolding sums_def
-    by (rule borel_measurable_LIMSEQ) (auto simp: borel[THEN integrableD(1)])
+    by (rule borel_measurable_LIMSEQ) auto
 
   let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
 
@@ -2190,7 +2194,7 @@
     using sums unfolding summable_def ..
 
   have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)"
-    using borel by auto
+    using integrable by auto
 
   have 2: "\<And>j. AE x in M. \<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x"
     using AE_space
@@ -2206,14 +2210,14 @@
     let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
     let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
     have "\<And>n. integrable M (?F n)"
-      using borel by (auto intro!: integrable_abs)
+      using integrable by (auto intro!: integrable_abs)
     thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
     show "AE x in M. mono (\<lambda>n. ?w' n x)"
       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
     show "AE x in M. (\<lambda>n. ?w' n x) ----> ?w x"
         using w by (simp_all add: tendsto_const sums_def)
     have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
-      using borel by (simp add: integrable_abs cong: integral_cong)
+      using integrable by (simp add: integrable_abs cong: integral_cong)
     from abs_sum
     show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
   qed (simp add: w_borel measurable_If_set)
@@ -2223,11 +2227,11 @@
     by (auto intro: summable_sumr_LIMSEQ_suminf)
 
   note int = integral_dominated_convergence(1,3)[OF 1 2 3 4
-    borel_measurable_suminf[OF integrableD(1)[OF borel]]]
+    borel_measurable_suminf[OF integrableD(1)[OF integrable]]]
 
   from int show "integrable M ?S" by simp
 
-  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel]
+  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF integrable]
     using int(2) by simp
 qed
 
@@ -2317,13 +2321,9 @@
                    positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
 
 lemma positive_integral_distr:
-  assumes T: "T \<in> measurable M M'"
-  and f: "f \<in> borel_measurable M'"
-  shows "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
-  apply (subst (1 2) positive_integral_max_0[symmetric])
-  apply (rule positive_integral_distr')
-  apply (auto simp: f T)
-  done
+  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
+  by (subst (1 2) positive_integral_max_0[symmetric])
+     (simp add: positive_integral_distr')
 
 lemma integral_distr:
   "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^isup>L (distr M M' T) f = (\<integral> x. f (T x) \<partial>M)"
@@ -2331,15 +2331,13 @@
   by (subst (1 2) positive_integral_distr) auto
 
 lemma integrable_distr_eq:
-  assumes T: "T \<in> measurable M M'" "f \<in> borel_measurable M'"
-  shows "integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
-  using T measurable_comp[OF T]
+  "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integrable (distr M M' T) f \<longleftrightarrow> integrable M (\<lambda>x. f (T x))"
   unfolding integrable_def 
   by (subst (1 2) positive_integral_distr) (auto simp: comp_def)
 
 lemma integrable_distr:
-  assumes T: "T \<in> measurable M M'" shows "integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
-  by (subst integrable_distr_eq[symmetric, OF T]) auto
+  "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
+  by (subst integrable_distr_eq[symmetric]) auto
 
 section {* Lebesgue integration on @{const count_space} *}
 
@@ -2414,6 +2412,10 @@
     and space_density[simp]: "space (density M f) = space M"
   by (auto simp: density_def)
 
+(* FIXME: add conversion to simplify space, sets and measurable *)
+lemma space_density_imp[measurable_dest]:
+  "\<And>x M f. x \<in> space (density M f) \<Longrightarrow> x \<in> space M" by auto
+
 lemma 
   shows measurable_density_eq1[simp]: "g \<in> measurable (density Mg f) Mg' \<longleftrightarrow> g \<in> measurable Mg Mg'"
     and measurable_density_eq2[simp]: "h \<in> measurable Mh (density Mh' f) \<longleftrightarrow> h \<in> measurable Mh Mh'"
@@ -2533,7 +2535,7 @@
   case (mult u c)
   moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
   ultimately show ?case
-    by (simp add: f positive_integral_cmult)
+    using f by (simp add: positive_integral_cmult)
 next
   case (add u v)
   moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"

--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -695,66 +695,6 @@
   qed
 qed
 
-lemma borel_measurable_real_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:
-  fixes u :: "'a \<Rightarrow> real"
-  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
-  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
-  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
-  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
-  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
-  assumes seq: "\<And>U u. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>x. (\<lambda>i. U i x) ----> u x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P u"
-  shows "P u"
-proof -
-  have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M"
-    using u by auto
-  then obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
-    "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x"
-    using borel_measurable_implies_simple_function_sequence'[of u M] by auto
-  then have u_eq: "\<And>x. ereal (u x) = (SUP i. U i x)"
-    using u by (auto simp: max_def)
-
-  have [simp]: "\<And>i x. U i x \<noteq> \<infinity>" using U by (auto simp: image_def eq_commute)
-
-  { fix i x have [simp]: "U i x \<noteq> -\<infinity>" using nn[of i x] by auto }
-  note this[simp]
-
-  show "P u"
-  proof (rule seq)
-    show "\<And>i. (\<lambda>x. real (U i x)) \<in> borel_measurable M"
-      using U by (auto intro: borel_measurable_simple_function)
-    show "\<And>i x. 0 \<le> real (U i x)"
-      using nn by (auto simp: real_of_ereal_pos)
-    show "incseq (\<lambda>i x. real (U i x))"
-      using U(2) by (auto simp: incseq_def image_iff le_fun_def intro!: real_of_ereal_positive_mono nn)
-    then show "\<And>x. (\<lambda>i. real (U i x)) ----> u x"
-      by (intro SUP_eq_LIMSEQ[THEN iffD1])
-         (auto simp: incseq_mono incseq_def le_fun_def u_eq ereal_real
-               intro!: arg_cong2[where f=SUPR] ext)
-    show "\<And>i. P (\<lambda>x. real (U i x))"
-    proof (rule cong)
-      fix x i assume x: "x \<in> space M"
-      have [simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x"
-        by (auto simp: indicator_def one_ereal_def)
-      { fix y assume "y \<in> U i ` space M"
-        then have "0 \<le> y" "y \<noteq> \<infinity>" using nn by auto
-        then have "\<bar>y * indicator (U i -` {y} \<inter> space M) x\<bar> \<noteq> \<infinity>"
-          by (auto simp: indicator_def) }
-      then show "real (U i x) = (\<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
-        unfolding simple_function_indicator_representation[OF U(1) x]
-        by (subst setsum_real_of_ereal[symmetric]) auto
-    next
-      fix i
-      have "finite (U i ` space M)" "\<And>x. x \<in> U i ` space M \<Longrightarrow> 0 \<le> x""\<And>x. x \<in> U i ` space M \<Longrightarrow> x \<noteq> \<infinity>"
-        using U(1) nn by (auto simp: simple_function_def)
-      then show "P (\<lambda>x. \<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
-      proof induct
-        case empty then show ?case
-          using set[of "{}"] by (simp add: indicator_def[abs_def])
-      qed (auto intro!: add mult set simple_functionD U setsum_nonneg borel_measurable_setsum mult_nonneg_nonneg real_of_ereal_pos)
-    qed (auto intro: borel_measurable_simple_function U simple_functionD intro!: borel_measurable_setsum borel_measurable_times)
-  qed
-qed
-
 lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
   by (auto simp: indicator_def one_ereal_def)
 
@@ -1054,7 +994,7 @@
     by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
 qed (auto simp: borel_eq_lessThan reals_Archimedean2)
 
-lemma measurable_e2p:
+lemma measurable_e2p[measurable]:
   "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))"
 proof (rule measurable_sigma_sets[OF sets_product_borel])
   fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
@@ -1065,7 +1005,11 @@
   then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
 qed (auto simp: e2p_def)
 
-lemma measurable_p2e:
+(* FIXME: conversion in measurable prover *)
+lemma lborelD_Collect[measurable]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
+lemma lborelD[measurable]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
+
+lemma measurable_p2e[measurable]:
   "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))
     (borel :: 'a::ordered_euclidean_space measure)"
   (is "p2e \<in> measurable ?P _")

--- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -522,23 +522,50 @@
   f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
 
 lemma
-  shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f"
-    and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N"
-    and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N"
-    and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)"
-  by (simp_all add: distributed_def)
+  assumes "distributed M N X f"
+  shows distributed_distr_eq_density: "distr M N X = density N f"
+    and distributed_measurable: "X \<in> measurable M N"
+    and distributed_borel_measurable: "f \<in> borel_measurable N"
+    and distributed_AE: "(AE x in N. 0 \<le> f x)"
+  using assms by (simp_all add: distributed_def)
+
+lemma
+  assumes D: "distributed M N X f"
+  shows distributed_measurable'[measurable_dest]:
+      "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
+    and distributed_borel_measurable'[measurable_dest]:
+      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
+  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
+  by simp_all
 
 lemma
   shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
     and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
   by (simp_all add: distributed_def borel_measurable_ereal_iff)
 
+lemma
+  assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
+  shows distributed_real_measurable'[measurable_dest]:
+      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
+  using distributed_real_measurable[OF D]
+  by simp_all
+
+lemma
+  assumes D: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
+  shows joint_distributed_measurable1[measurable_dest]:
+      "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
+    and joint_distributed_measurable2[measurable_dest]:
+      "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
+  using measurable_compose[OF distributed_measurable[OF D] measurable_fst]
+  using measurable_compose[OF distributed_measurable[OF D] measurable_snd]
+  by auto
+
 lemma distributed_count_space:
   assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
   shows "P a = emeasure M (X -` {a} \<inter> space M)"
 proof -
   have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
-    using X a A by (simp add: distributed_measurable emeasure_distr)
+    using X a A by (simp add: emeasure_distr)
   also have "\<dots> = emeasure (density (count_space A) P) {a}"
     using X by (simp add: distributed_distr_eq_density)
   also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
@@ -583,17 +610,17 @@
 
 lemma distributed_emeasure:
   "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
-  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
+  by (auto simp: distributed_AE
                  distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
 
 lemma distributed_positive_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
-  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
+  by (auto simp: distributed_AE
                  distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
 
 lemma distributed_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
-  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
+  by (auto simp: distributed_real_AE
                  distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
   
 lemma distributed_transform_integral:
@@ -617,7 +644,7 @@
   shows "AE x in S. Px x = Py x"
 proof -
   interpret X: prob_space "distr M S X"
-    using distributed_measurable[OF Px] by (rule prob_space_distr)
+    using Px by (intro prob_space_distr) simp
   have "sigma_finite_measure (distr M S X)" ..
   with sigma_finite_density_unique[of Px S Py ] Px Py
   show ?thesis
@@ -626,8 +653,8 @@
 
 lemma (in prob_space) distributed_jointI:
   assumes "sigma_finite_measure S" "sigma_finite_measure T"
-  assumes X[simp]: "X \<in> measurable M S" and Y[simp]: "Y \<in> measurable M T"
-  assumes f[simp]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
+  assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
+  assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
   assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
     emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
   shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
@@ -655,18 +682,18 @@
       using F by (auto simp: space_pair_measure)
   next
     fix E assume "E \<in> ?E"
-    then obtain A B where E[simp]: "E = A \<times> B" and A[simp]: "A \<in> sets S" and B[simp]: "B \<in> sets T" by auto
+    then obtain A B where E[simp]: "E = A \<times> B"
+      and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
     have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
       by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
     also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
-      by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc
-               intro!: positive_integral_cong)
+      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
     also have "\<dots> = emeasure ?R E"
       by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
                intro!: positive_integral_cong split: split_indicator)
     finally show "emeasure ?L E = emeasure ?R E" .
   qed
-qed (auto intro!: measurable_Pair)
+qed (auto simp: f)
 
 lemma (in prob_space) distributed_swap:
   assumes "sigma_finite_measure S" "sigma_finite_measure T"
@@ -678,14 +705,14 @@
   interpret ST: pair_sigma_finite S T by default
   interpret TS: pair_sigma_finite T S by default
 
-  note measurable_Pxy = measurable_compose[OF _ distributed_borel_measurable[OF Pxy]]
+  note Pxy[measurable]
   show ?thesis 
     apply (subst TS.distr_pair_swap)
     unfolding distributed_def
   proof safe
     let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
     show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
-      by (auto simp: measurable_split_conv intro!: measurable_Pair measurable_Pxy)
+      by auto
     with Pxy
     show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
       by (subst AE_distr_iff)
@@ -693,9 +720,7 @@
                simp: measurable_split_conv split_beta
                intro!: measurable_Pair borel_measurable_ereal_le)
     show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
-      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_fst]
-      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_snd]
-      by (auto intro!: measurable_Pair)
+      using Pxy by auto
     { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
       let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
       from sets_into_space[OF A]
@@ -703,7 +728,7 @@
         emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
         by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
       also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
-        using Pxy A by (intro distributed_emeasure measurable_sets) (auto simp: measurable_split_conv measurable_Pair)
+        using Pxy A by (intro distributed_emeasure) auto
       finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
         (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
         by (auto intro!: positive_integral_cong split: split_indicator) }
@@ -712,7 +737,7 @@
       apply (intro measure_eqI)
       apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
       apply (subst positive_integral_distr)
-      apply (auto intro!: measurable_pair measurable_Pxy * simp: comp_def split_beta)
+      apply (auto intro!: * simp: comp_def split_beta)
       done
   qed
 qed
@@ -728,33 +753,29 @@
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T by default
 
-  have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
-    using Pxy by (rule distributed_measurable)
-  then show X: "X \<in> measurable M S"
-    unfolding measurable_pair_iff by (simp add: comp_def)
-  from XY have Y: "Y \<in> measurable M T"
-    unfolding measurable_pair_iff by (simp add: comp_def)
+  note Pxy[measurable]
+  show X: "X \<in> measurable M S" by simp
 
-  from Pxy show borel: "Px \<in> borel_measurable S"
-    by (auto intro!: T.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
+  show borel: "Px \<in> borel_measurable S"
+    by (auto intro!: T.positive_integral_fst_measurable simp: Px_def)
 
   interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
-    using XY by (rule prob_space_distr)
+    by (intro prob_space_distr) simp
   have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
     using Pxy
-    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_borel_measurable distributed_AE)
+    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
 
   show "distr M S X = density S Px"
   proof (rule measure_eqI)
     fix A assume A: "A \<in> sets (distr M S X)"
-    with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
-      by (auto simp add: emeasure_distr
-               intro!: arg_cong[where f="emeasure M"] dest: measurable_space)
+    with X measurable_space[of Y M T]
+    have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
+      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
     also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
       using Pxy by (simp add: distributed_def)
     also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
       using A borel Pxy
-      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric] distributed_def)
+      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric])
     also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
       apply (rule positive_integral_cong_AE)
       using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
@@ -763,7 +784,7 @@
       moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
         by (auto simp: indicator_def)
       ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
-        using Pxy[THEN distributed_borel_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
+        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
       also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
         by (simp add: Px_def ereal_real positive_integral_positive)
       finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
@@ -800,7 +821,7 @@
 
 lemma (in prob_space) distributed_joint_indep':
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
-  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
+  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
   assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   unfolding distributed_def
@@ -811,30 +832,23 @@
 
   interpret X: prob_space "density S Px"
     unfolding distributed_distr_eq_density[OF X, symmetric]
-    using distributed_measurable[OF X]
-    by (rule prob_space_distr)
+    by (rule prob_space_distr) simp
   have sf_X: "sigma_finite_measure (density S Px)" ..
 
   interpret Y: prob_space "density T Py"
     unfolding distributed_distr_eq_density[OF Y, symmetric]
-    using distributed_measurable[OF Y]
-    by (rule prob_space_distr)
+    by (rule prob_space_distr) simp
   have sf_Y: "sigma_finite_measure (density T Py)" ..
 
   show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
     unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
     using distributed_borel_measurable[OF X] distributed_AE[OF X]
     using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
-    by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y])
+    by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
 
-  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
-    using distributed_measurable[OF X] distributed_measurable[OF Y]
-    by (auto intro: measurable_Pair)
+  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto
 
-  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
-    by (auto simp: split_beta' 
-             intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]]
-                     measurable_compose[OF _ distributed_borel_measurable[OF Y]])
+  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto
 
   show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
     apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const)

--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -47,7 +47,7 @@
   shows "\<exists>h\<in>borel_measurable M. integral\<^isup>P M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)"
 proof -
   obtain A :: "nat \<Rightarrow> 'a set" where
-    range: "range A \<subseteq> sets M" and
+    range[measurable]: "range A \<subseteq> sets M" and
     space: "(\<Union>i. A i) = space M" and
     measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" and
     disjoint: "disjoint_family A"
@@ -97,10 +97,7 @@
       assume "x \<notin> space M" then have "\<And>i. x \<notin> A i" using space by auto
       then show "0 \<le> ?h x" by auto
     qed
-  next
-    show "?h \<in> borel_measurable M" using range n
-      by (auto intro!: borel_measurable_psuminf borel_measurable_ereal_times ereal_0_le_mult intro: less_imp_le)
-  qed
+  qed measurable
 qed
 
 subsection "Absolutely continuous"
@@ -298,6 +295,8 @@
 proof -
   interpret N: finite_measure N by fact
   def G \<equiv> "{g \<in> borel_measurable M. (\<forall>x. 0 \<le> g x) \<and> (\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A)}"
+  { fix f have "f \<in> G \<Longrightarrow> f \<in> borel_measurable M" by (auto simp: G_def) }
+  note this[measurable_dest]
   have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
   hence "G \<noteq> {}" by auto
   { fix f g assume f: "f \<in> G" and g: "g \<in> G"
@@ -329,10 +328,10 @@
     qed }
   note max_in_G = this
   { fix f assume  "incseq f" and f: "\<And>i. f i \<in> G"
+    then have [measurable]: "\<And>i. f i \<in> borel_measurable M" by (auto simp: G_def)
     have "(\<lambda>x. SUP i. f i x) \<in> G" unfolding G_def
     proof safe
-      show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
-        using f by (auto simp: G_def)
+      show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M" by measurable
       { fix x show "0 \<le> (SUP i. f i x)"
           using f by (auto simp: G_def intro: SUP_upper2) }
     next
@@ -379,7 +378,7 @@
   note g_in_G = this
   have "incseq ?g" using gs_not_empty
     by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)
-  from SUP_in_G[OF this g_in_G] have "f \<in> G" unfolding f_def .
+  from SUP_in_G[OF this g_in_G] have [measurable]: "f \<in> G" unfolding f_def .
   then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
   have "integral\<^isup>P M f = (SUP i. integral\<^isup>P M (?g i))" unfolding f_def
     using g_in_G `incseq ?g`
@@ -467,7 +466,7 @@
       hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) =
           (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + b * emeasure M (A \<inter> A0)"
         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G`
-        by (simp add: G_def positive_integral_add positive_integral_cmult_indicator) }
+        by (simp add: positive_integral_add positive_integral_cmult_indicator G_def) }
     note f0_eq = this
     { fix A assume A: "A \<in> sets M"
       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
@@ -484,8 +483,8 @@
         using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
         by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "N A") auto
       finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
-    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
-      by (auto intro!: ereal_add_nonneg_nonneg)
+    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G`
+      by (auto intro!: ereal_add_nonneg_nonneg simp: G_def)
     have int_f_finite: "integral\<^isup>P M f \<noteq> \<infinity>"
       by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
     have  "0 < ?M (space M) - emeasure ?Mb (space M)"
@@ -676,6 +675,7 @@
     with Q_fin show "finite_measure (?N i)"
       by (auto intro!: finite_measureI)
     show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
+    have [measurable]: "\<And>A. A \<in> sets M \<Longrightarrow> A \<in> sets N" by (simp add: sets_eq)
     show "absolutely_continuous (?M i) (?N i)"
       using `absolutely_continuous M N` `Q i \<in> sets M`
       by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq
@@ -731,9 +731,7 @@
       ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
         using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
       with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
-        by (subst emeasure_density)
-           (auto intro!: borel_measurable_ereal_add borel_measurable_psuminf measurable_If
-                 simp: subset_eq)
+        by (auto simp: subset_eq emeasure_density)
     qed (simp add: sets_eq)
   qed
 qed
@@ -845,7 +843,7 @@
     unfolding indicator_def by auto
   have "\<forall>i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
     by (intro finite_density_unique[THEN iffD1] allI)
-       (auto intro!: borel_measurable_ereal_times f measure_eqI Int simp: emeasure_density * subset_eq)
+       (auto intro!: f measure_eqI simp: emeasure_density * subset_eq)
   moreover have "AE x in M. ?f Q0 x = ?f' Q0 x"
   proof (rule AE_I')
     { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
@@ -1083,7 +1081,7 @@
 
 lemma (in sigma_finite_measure) RN_deriv:
   assumes "absolutely_continuous M N" "sets N = sets M"
-  shows borel_measurable_RN_deriv: "RN_deriv M N \<in> borel_measurable M" (is ?borel)
+  shows borel_measurable_RN_deriv[measurable]: "RN_deriv M N \<in> borel_measurable M" (is ?borel)
     and density_RN_deriv: "density M (RN_deriv M N) = N" (is ?density)
     and RN_deriv_nonneg: "0 \<le> RN_deriv M N x" (is ?pos)
 proof -
@@ -1164,7 +1162,7 @@
     qed
   qed
   have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
-    using T ac by (intro measurable_comp[where b="?M'"] M'.borel_measurable_RN_deriv) simp_all
+    using T ac by measurable simp
   then show "(\<lambda>x. RN_deriv ?M' ?N' (T x)) \<in> borel_measurable M"
     by (simp add: comp_def)
   show "AE x in M. 0 \<le> RN_deriv ?M' ?N' (T x)" using M'.RN_deriv_nonneg[OF ac] by auto

--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:40 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:54 2012 +0100
@@ -1263,6 +1263,11 @@
   shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)"
   by (metis assms in_measure_of measurable_measure_of assms measurable_sets)
 
+lemma measurable_cong_sets:
+  assumes sets: "sets M = sets M'" "sets N = sets N'"
+  shows "measurable M N = measurable M' N'"
+  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
+
 lemma measurable_cong:
   assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
   shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
@@ -1275,7 +1280,22 @@
       \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
   by (simp add: measurable_def sigma_algebra_iff2)
 
-lemma measurable_const[intro, simp]:
+lemma measurable_compose:
+  assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
+  shows "(\<lambda>x. g (f x)) \<in> measurable M L"
+proof -
+  have "\<And>A. (\<lambda>x. g (f x)) -` A \<inter> space M = f -` (g -` A \<inter> space N) \<inter> space M"
+    using measurable_space[OF f] by auto
+  with measurable_space[OF f] measurable_space[OF g] show ?thesis
+    by (auto intro: measurable_sets[OF f] measurable_sets[OF g]
+             simp del: vimage_Int simp add: measurable_def)
+qed
+
+lemma measurable_comp:
+  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> g \<circ> f \<in> measurable M L"
+  using measurable_compose[of f M N g L] by (simp add: comp_def)
+
+lemma measurable_const:
   "c \<in> space M' \<Longrightarrow> (\<lambda>x. c) \<in> measurable M M'"
   by (auto simp add: measurable_def)
 
@@ -1308,23 +1328,11 @@
   thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<inter> space M \<in> sets M` by auto
 qed
 
-lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
-  by (auto simp add: measurable_def)
-
-lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
+lemma measurable_ident: "id \<in> measurable M M"
   by (auto simp add: measurable_def)
 
-lemma measurable_comp[intro]:
-  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
-  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
-  apply (auto simp add: measurable_def vimage_compose)
-  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
-  apply force+
-  done
-
-lemma measurable_compose:
-  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
-  using measurable_comp[of f M N g L] by (simp add: comp_def)
+lemma measurable_ident': "(\<lambda>x. x) \<in> measurable M M"
+  by (auto simp add: measurable_def)
 
 lemma sets_Least:
   assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
@@ -1469,7 +1477,7 @@
 
 lemma measurable_count_space_const:
   "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
-  by auto
+  by (simp add: measurable_const)
 
 lemma measurable_count_space:
   "f \<in> measurable (count_space A) (count_space UNIV)"
@@ -1489,10 +1497,10 @@
 
 structure Data = Generic_Data
 (
-  type T = thm list * thm list;
-  val empty = ([], []);
+  type T = (thm list * thm list) * thm list;
+  val empty = (([], []), []);
   val extend = I;
-  val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
+  val merge = fn (((c1, g1), d1), ((c2, g2), d2)) => ((c1 @ c2, g1 @ g2), d1 @ d2);
 );
 
 val debug =
@@ -1501,12 +1509,15 @@
 val backtrack =
   Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
 
-fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof; 
+fun get lv = (case lv of Concrete => fst | Generic => snd) o fst o Data.get o Context.Proof; 
 fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
 
-fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
+fun update f lv = Data.map (apfst (case lv of Concrete => apfst f | Generic => apsnd f));
 fun add thms' = update (fn thms => thms @ thms');
 
+val get_dest = snd o Data.get;
+fun add_dest thm = Data.map (apsnd (fn thms => thms @ [thm]));
+
 fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
 
 fun is_too_generic thm =
@@ -1515,11 +1526,10 @@
     val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
   in is_Var (head_of concl') end
 
-fun import_theorem thm = if is_too_generic thm then [] else
-  [thm] @ map_filter (try (fn th' => thm RS th'))
-    [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
+fun import_theorem ctxt thm = if is_too_generic thm then [] else
+  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
 
-fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
+fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
 
 fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
 
@@ -1573,8 +1583,9 @@
     handle TERM _ => no_tac) 1)
 
 fun single_measurable_tac ctxt facts =
-  debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
-  (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
+  debug_tac ctxt (fn () => "single + " ^
+    Pretty.str_of (Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)))))
+  (resolve_tac ((maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt)
     APPEND' (split_fun_tac ctxt));
 
 fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
@@ -1598,6 +1609,9 @@
   Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
      Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
 
+val dest_attr : attribute context_parser =
+  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
+
 val method : (Proof.context -> Method.method) context_parser =
   Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
 
@@ -1613,10 +1627,17 @@
 *}
 
 attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
+attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
 method_setup measurable = {* Measurable.method *} "measurability prover"
 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
 
 declare
+  measurable_compose_rev[measurable_dest]
+  pred_sets1[measurable_dest]
+  pred_sets2[measurable_dest]
+  sets_into_space[measurable_dest]
+
+declare
   top[measurable]
   empty_sets[measurable (raw)]
   Un[measurable (raw)]
@@ -1670,7 +1691,7 @@
   "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
   "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
   "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
-  by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
+  by (auto simp: iff_conv_conj_imp pred_def)
 
 lemma pred_intros_countable[measurable (raw)]:
   fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
@@ -1743,6 +1764,34 @@
 declare
   Int[measurable (raw)]
 
+lemma pred_in_If[measurable (raw)]:
+  "pred M (\<lambda>x. (P x \<longrightarrow> x \<in> A x) \<and> (\<not> P x \<longrightarrow> x \<in> B x)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (if P x then A x else B x))"
+  by auto
+
+lemma sets_range[measurable_dest]:
+  "A ` I \<subseteq> sets M \<Longrightarrow> i \<in> I \<Longrightarrow> A i \<in> sets M"
+  by auto
+
+lemma pred_sets_range[measurable_dest]:
+  "A ` I \<subseteq> sets N \<Longrightarrow> i \<in> I \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
+  using pred_sets2[OF sets_range] by auto
+
+lemma sets_All[measurable_dest]:
+  "\<forall>i. A i \<in> sets (M i) \<Longrightarrow> A i \<in> sets (M i)"
+  by auto
+
+lemma pred_sets_All[measurable_dest]:
+  "\<forall>i. A i \<in> sets (N i) \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
+  using pred_sets2[OF sets_All, of A N f] by auto
+
+lemma sets_Ball[measurable_dest]:
+  "\<forall>i\<in>I. A i \<in> sets (M i) \<Longrightarrow> i\<in>I \<Longrightarrow> A i \<in> sets (M i)"
+  by auto
+
+lemma pred_sets_Ball[measurable_dest]:
+  "\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
+  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
+
 hide_const (open) pred
 
 subsection {* Extend measure *}