# HG changeset patch
# User hoelzl
# Date 1295017213 -3600
# Node ID 4638b1210d26009490ca30d5750a2d008333650c
# Parent  a5478b1c8b8aa594564287a23b566b56cf389234# Parent  2a12c23b7a34c08b8c2b73b60c67d16e312f19af
merged

diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -170,7 +170,7 @@
 qed
 
 lemma (in sigma_algebra) borel_measurable_subalgebra:
-  assumes "N \<subseteq> sets M" "f \<in> borel_measurable (M\<lparr>sets:=N\<rparr>)"
+  assumes "sets N \<subseteq> sets M" "space N = space M" "f \<in> borel_measurable N"
   shows "f \<in> borel_measurable M"
   using assms unfolding measurable_def by auto
 
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -463,12 +463,12 @@
 qed
 
 lemma (in sigma_algebra) simple_function_subalgebra:
-  assumes "sigma_algebra.simple_function (M\<lparr>sets:=N\<rparr>) f"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets:=N\<rparr>)"
+  assumes "sigma_algebra.simple_function N f"
+  and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M" "sigma_algebra N"
   shows "simple_function f"
   using assms
   unfolding simple_function_def
-  unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)]
+  unfolding sigma_algebra.simple_function_def[OF N_subalgebra(3)]
   by auto
 
 lemma (in sigma_algebra) simple_function_vimage:
@@ -489,7 +489,7 @@
 
 section "Simple integral"
 
-definition (in measure_space)
+definition (in measure_space) simple_integral (binder "\<integral>\<^isup>S " 10) where
   "simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M))"
 
 lemma (in measure_space) simple_integral_cong:
@@ -514,7 +514,7 @@
 qed
 
 lemma (in measure_space) simple_integral_const[simp]:
-  "simple_integral (\<lambda>x. c) = c * \<mu> (space M)"
+  "(\<integral>\<^isup>Sx. c) = c * \<mu> (space M)"
 proof (cases "space M = {}")
   case True thus ?thesis unfolding simple_integral_def by simp
 next
@@ -579,7 +579,7 @@
 
 lemma (in measure_space) simple_integral_add[simp]:
   assumes "simple_function f" and "simple_function g"
-  shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g"
+  shows "(\<integral>\<^isup>Sx. f x + g x) = simple_integral f + simple_integral g"
 proof -
   { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
     assume "x \<in> space M"
@@ -597,7 +597,7 @@
 
 lemma (in measure_space) simple_integral_setsum[simp]:
   assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)"
-  shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"
+  shows "(\<integral>\<^isup>Sx. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))"
 proof cases
   assume "finite P"
   from this assms show ?thesis
@@ -606,7 +606,7 @@
 
 lemma (in measure_space) simple_integral_mult[simp]:
   assumes "simple_function f"
-  shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f"
+  shows "(\<integral>\<^isup>Sx. c * f x) = c * simple_integral f"
 proof -
   note mult = simple_function_mult[OF simple_function_const[of c] assms]
   { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
@@ -700,11 +700,11 @@
 lemma (in measure_space) simple_integral_indicator:
   assumes "A \<in> sets M"
   assumes "simple_function f"
-  shows "simple_integral (\<lambda>x. f x * indicator A x) =
+  shows "(\<integral>\<^isup>Sx. f x * indicator A x) =
     (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
 proof cases
   assume "A = space M"
-  moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f"
+  moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x) = simple_integral f"
     by (auto intro!: simple_integral_cong)
   moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
   ultimately show ?thesis by (simp add: simple_integral_def)
@@ -720,7 +720,7 @@
   next
     show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
   qed
-  have *: "simple_integral (\<lambda>x. f x * indicator A x) =
+  have *: "(\<integral>\<^isup>Sx. f x * indicator A x) =
     (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
     unfolding simple_integral_def I
   proof (rule setsum_mono_zero_cong_left)
@@ -760,18 +760,18 @@
 
 lemma (in measure_space) simple_integral_null_set:
   assumes "simple_function u" "N \<in> null_sets"
-  shows "simple_integral (\<lambda>x. u x * indicator N x) = 0"
+  shows "(\<integral>\<^isup>Sx. u x * indicator N x) = 0"
 proof -
   have "AE x. indicator N x = (0 :: pextreal)"
     using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
-  then have "simple_integral (\<lambda>x. u x * indicator N x) = simple_integral (\<lambda>x. 0)"
+  then have "(\<integral>\<^isup>Sx. u x * indicator N x) = (\<integral>\<^isup>Sx. 0)"
     using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2)
   then show ?thesis by simp
 qed
 
 lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
   assumes sf: "simple_function f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
-  shows "simple_integral f = simple_integral (\<lambda>x. f x * indicator S x)"
+  shows "simple_integral f = (\<integral>\<^isup>Sx. f x * indicator S x)"
 proof (rule simple_integral_cong_AE)
   show "simple_function f" by fact
   show "simple_function (\<lambda>x. f x * indicator S x)"
@@ -783,7 +783,7 @@
 lemma (in measure_space) simple_integral_restricted:
   assumes "A \<in> sets M"
   assumes sf: "simple_function (\<lambda>x. f x * indicator A x)"
-  shows "measure_space.simple_integral (restricted_space A) \<mu> f = simple_integral (\<lambda>x. f x * indicator A x)"
+  shows "measure_space.simple_integral (restricted_space A) \<mu> f = (\<integral>\<^isup>Sx. f x * indicator A x)"
     (is "_ = simple_integral ?f")
   unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]]
   unfolding simple_integral_def
@@ -809,11 +809,11 @@
     unfolding pextreal_mult_cancel_left by auto
 qed
 
-lemma (in measure_space) simple_integral_subalgebra[simp]:
-  assumes "measure_space (M\<lparr>sets := N\<rparr>) \<mu>"
-  shows "measure_space.simple_integral (M\<lparr>sets := N\<rparr>) \<mu> = simple_integral"
+lemma (in measure_space) simple_integral_subalgebra:
+  assumes N: "measure_space N \<mu>" and [simp]: "space N = space M"
+  shows "measure_space.simple_integral N \<mu> = simple_integral"
   unfolding simple_integral_def_raw
-  unfolding measure_space.simple_integral_def_raw[OF assms] by simp
+  unfolding measure_space.simple_integral_def_raw[OF N] by simp
 
 lemma (in measure_space) simple_integral_vimage:
   fixes g :: "'a \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
@@ -842,7 +842,7 @@
 
 section "Continuous posititve integration"
 
-definition (in measure_space)
+definition (in measure_space) positive_integral (binder "\<integral>\<^isup>+ " 10) where
   "positive_integral f = SUPR {g. simple_function g \<and> g \<le> f} simple_integral"
 
 lemma (in measure_space) positive_integral_alt:
@@ -1071,7 +1071,7 @@
   fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
   assumes f: "bij_inv S (space M) f h"
   shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
-      positive_integral (\<lambda>x. g (h x))"
+      (\<integral>\<^isup>+x. g (h x))"
 proof -
   interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
     using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
@@ -1149,7 +1149,7 @@
     unfolding pextreal_SUP_cmult[symmetric]
   proof (safe intro!: SUP_mono bexI)
     fix i
-    have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
+    have "a * simple_integral (?uB i) = (\<integral>\<^isup>Sx. a * ?uB i x)"
       using B `simple_function u`
       by (subst simple_integral_mult[symmetric]) (auto simp: field_simps)
     also have "\<dots> \<le> positive_integral (f i)"
@@ -1193,7 +1193,7 @@
 lemma (in measure_space) positive_integral_monotone_convergence_SUP:
   assumes "\<And>i x. x \<in> space M \<Longrightarrow> f i x \<le> f (Suc i) x"
   assumes "\<And>i. f i \<in> borel_measurable M"
-  shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
+  shows "(SUP i. positive_integral (f i)) = (\<integral>\<^isup>+ x. SUP i. f i x)"
     (is "_ = positive_integral ?u")
 proof -
   show ?thesis
@@ -1236,7 +1236,7 @@
 qed
 
 lemma (in measure_space) positive_integral_const[simp]:
-  "positive_integral (\<lambda>x. c) = c * \<mu> (space M)"
+  "(\<integral>\<^isup>+ x. c) = c * \<mu> (space M)"
   by (subst positive_integral_eq_simple_integral) auto
 
 lemma (in measure_space) positive_integral_isoton_simple:
@@ -1248,7 +1248,7 @@
 lemma (in measure_space) positive_integral_linear:
   assumes f: "f \<in> borel_measurable M"
   and g: "g \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. a * f x + g x) =
+  shows "(\<integral>\<^isup>+ x. a * f x + g x) =
       a * positive_integral f + positive_integral g"
     (is "positive_integral ?L = _")
 proof -
@@ -1276,30 +1276,32 @@
 
 lemma (in measure_space) positive_integral_cmult:
   assumes "f \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
+  shows "(\<integral>\<^isup>+ x. c * f x) = c * positive_integral f"
   using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
 
 lemma (in measure_space) positive_integral_multc:
   assumes "f \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
+  shows "(\<integral>\<^isup>+ x. f x * c) = positive_integral f * c"
   unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
 
 lemma (in measure_space) positive_integral_indicator[simp]:
-  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
-by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
+  "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x) = \<mu> A"
+  by (subst positive_integral_eq_simple_integral)
+     (auto simp: simple_function_indicator simple_integral_indicator)
 
 lemma (in measure_space) positive_integral_cmult_indicator:
-  "A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. c * indicator A x) = c * \<mu> A"
-by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
+  "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x) = c * \<mu> A"
+  by (subst positive_integral_eq_simple_integral)
+     (auto simp: simple_function_indicator simple_integral_indicator)
 
 lemma (in measure_space) positive_integral_add:
   assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. f x + g x) = positive_integral f + positive_integral g"
+  shows "(\<integral>\<^isup>+ x. f x + g x) = positive_integral f + positive_integral g"
   using positive_integral_linear[OF assms, of 1] by simp
 
 lemma (in measure_space) positive_integral_setsum:
   assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"
+  shows "(\<integral>\<^isup>+ x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. positive_integral (f i))"
 proof cases
   assume "finite P"
   from this assms show ?thesis
@@ -1317,11 +1319,11 @@
   assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M"
   and fin: "positive_integral g \<noteq> \<omega>"
   and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x"
-  shows "positive_integral (\<lambda>x. f x - g x) = positive_integral f - positive_integral g"
+  shows "(\<integral>\<^isup>+ x. f x - g x) = positive_integral f - positive_integral g"
 proof -
   have borel: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
     using f g by (rule borel_measurable_pextreal_diff)
-  have "positive_integral (\<lambda>x. f x - g x) + positive_integral g =
+  have "(\<integral>\<^isup>+x. f x - g x) + positive_integral g =
     positive_integral f"
     unfolding positive_integral_add[OF borel g, symmetric]
   proof (rule positive_integral_cong)
@@ -1335,9 +1337,9 @@
 
 lemma (in measure_space) positive_integral_psuminf:
   assumes "\<And>i. f i \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"
+  shows "(\<integral>\<^isup>+ x. \<Sum>\<^isub>\<infinity> i. f i x) = (\<Sum>\<^isub>\<infinity> i. positive_integral (f i))"
 proof -
-  have "(\<lambda>i. positive_integral (\<lambda>x. \<Sum>i<i. f i x)) \<up> positive_integral (\<lambda>x. \<Sum>\<^isub>\<infinity>i. f i x)"
+  have "(\<lambda>i. (\<integral>\<^isup>+x. \<Sum>i<i. f i x)) \<up> (\<integral>\<^isup>+x. \<Sum>\<^isub>\<infinity>i. f i x)"
     by (rule positive_integral_isoton)
        (auto intro!: borel_measurable_pextreal_setsum assms positive_integral_mono
                      arg_cong[where f=Sup]
@@ -1350,11 +1352,11 @@
 lemma (in measure_space) positive_integral_lim_INF:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes "\<And>i. u i \<in> borel_measurable M"
-  shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
+  shows "(\<integral>\<^isup>+ x. SUP n. INF m. u (m + n) x) \<le>
     (SUP n. INF m. positive_integral (u (m + n)))"
 proof -
-  have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
-      = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
+  have "(\<integral>\<^isup>+x. SUP n. INF m. u (m + n) x)
+      = (SUP n. (\<integral>\<^isup>+x. INF m. u (m + n) x))"
     using assms
     by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
        (auto simp del: add_Suc simp add: add_Suc[symmetric])
@@ -1365,7 +1367,7 @@
 
 lemma (in measure_space) measure_space_density:
   assumes borel: "u \<in> borel_measurable M"
-  shows "measure_space M (\<lambda>A. positive_integral (\<lambda>x. u x * indicator A x))" (is "measure_space M ?v")
+  shows "measure_space M (\<lambda>A. (\<integral>\<^isup>+ x. u x * indicator A x))" (is "measure_space M ?v")
 proof
   show "?v {} = 0" by simp
   show "countably_additive M ?v"
@@ -1384,8 +1386,8 @@
 
 lemma (in measure_space) positive_integral_translated_density:
   assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)) g =
-    positive_integral (\<lambda>x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
+  shows "measure_space.positive_integral M (\<lambda>A. (\<integral>\<^isup>+ x. f x * indicator A x)) g = 
+         (\<integral>\<^isup>+ x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
 proof -
   from measure_space_density[OF assms(1)]
   interpret T: measure_space M ?T .
@@ -1399,30 +1401,30 @@
       using G(1) unfolding simple_function_def by auto
     have "T.positive_integral (G i) = T.simple_integral (G i)"
       using G T.positive_integral_eq_simple_integral by simp
-    also have "\<dots> = positive_integral (\<lambda>x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x))"
+    also have "\<dots> = (\<integral>\<^isup>+x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x))"
       apply (simp add: T.simple_integral_def)
       apply (subst positive_integral_cmult[symmetric])
       using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
       apply (subst positive_integral_setsum[symmetric])
       using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
       by (simp add: setsum_right_distrib field_simps)
-    also have "\<dots> = positive_integral (\<lambda>x. f x * G i x)"
+    also have "\<dots> = (\<integral>\<^isup>+x. f x * G i x)"
       by (auto intro!: positive_integral_cong
                simp: indicator_def if_distrib setsum_cases)
-    finally have "T.positive_integral (G i) = positive_integral (\<lambda>x. f x * G i x)" . }
-  with * have eq_Tg: "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> T.positive_integral g" by simp
+    finally have "T.positive_integral (G i) = (\<integral>\<^isup>+x. f x * G i x)" . }
+  with * have eq_Tg: "(\<lambda>i. (\<integral>\<^isup>+x. f x * G i x)) \<up> T.positive_integral g" by simp
   from G(2) have "(\<lambda>i x. f x * G i x) \<up> (\<lambda>x. f x * g x)"
     unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right)
-  then have "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> positive_integral (\<lambda>x. f x * g x)"
+  then have "(\<lambda>i. (\<integral>\<^isup>+x. f x * G i x)) \<up> (\<integral>\<^isup>+x. f x * g x)"
     using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pextreal_times)
-  with eq_Tg show "T.positive_integral g = positive_integral (\<lambda>x. f x * g x)"
+  with eq_Tg show "T.positive_integral g = (\<integral>\<^isup>+x. f x * g x)"
     unfolding isoton_def by simp
 qed
 
 lemma (in measure_space) positive_integral_null_set:
-  assumes "N \<in> null_sets" shows "positive_integral (\<lambda>x. u x * indicator N x) = 0"
+  assumes "N \<in> null_sets" shows "(\<integral>\<^isup>+ x. u x * indicator N x) = 0"
 proof -
-  have "positive_integral (\<lambda>x. u x * indicator N x) = positive_integral (\<lambda>x. 0)"
+  have "(\<integral>\<^isup>+ x. u x * indicator N x) = (\<integral>\<^isup>+ x. 0)"
   proof (intro positive_integral_cong_AE AE_I)
     show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
       by (auto simp: indicator_def)
@@ -1434,20 +1436,20 @@
 
 lemma (in measure_space) positive_integral_Markov_inequality:
   assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>"
-  shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * positive_integral (\<lambda>x. u x * indicator A x)"
+  shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^isup>+ x. u x * indicator A x)"
     (is "\<mu> ?A \<le> _ * ?PI")
 proof -
   have "?A \<in> sets M"
     using `A \<in> sets M` borel by auto
-  hence "\<mu> ?A = positive_integral (\<lambda>x. indicator ?A x)"
+  hence "\<mu> ?A = (\<integral>\<^isup>+ x. indicator ?A x)"
     using positive_integral_indicator by simp
-  also have "\<dots> \<le> positive_integral (\<lambda>x. c * (u x * indicator A x))"
+  also have "\<dots> \<le> (\<integral>\<^isup>+ x. c * (u x * indicator A x))"
   proof (rule positive_integral_mono)
     fix x assume "x \<in> space M"
     show "indicator ?A x \<le> c * (u x * indicator A x)"
       by (cases "x \<in> ?A") auto
   qed
-  also have "\<dots> = c * positive_integral (\<lambda>x. u x * indicator A x)"
+  also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x)"
     using assms
     by (auto intro!: positive_integral_cmult borel_measurable_indicator)
   finally show ?thesis .
@@ -1459,7 +1461,7 @@
     (is "_ \<longleftrightarrow> \<mu> ?A = 0")
 proof -
   have A: "?A \<in> sets M" using borel by auto
-  have u: "positive_integral (\<lambda>x. u x * indicator ?A x) = positive_integral u"
+  have u: "(\<integral>\<^isup>+ x. u x * indicator ?A x) = positive_integral u"
     by (auto intro!: positive_integral_cong simp: indicator_def)
 
   show ?thesis
@@ -1467,7 +1469,7 @@
     assume "\<mu> ?A = 0"
     hence "?A \<in> null_sets" using `?A \<in> sets M` by auto
     from positive_integral_null_set[OF this]
-    have "0 = positive_integral (\<lambda>x. u x * indicator ?A x)" by simp
+    have "0 = (\<integral>\<^isup>+ x. u x * indicator ?A x)" by simp
     thus "positive_integral u = 0" unfolding u by simp
   next
     assume *: "positive_integral u = 0"
@@ -1507,7 +1509,7 @@
 
 lemma (in measure_space) positive_integral_restricted:
   assumes "A \<in> sets M"
-  shows "measure_space.positive_integral (restricted_space A) \<mu> f = positive_integral (\<lambda>x. f x * indicator A x)"
+  shows "measure_space.positive_integral (restricted_space A) \<mu> f = (\<integral>\<^isup>+ x. f x * indicator A x)"
     (is "measure_space.positive_integral ?R \<mu> f = positive_integral ?f")
 proof -
   have msR: "measure_space ?R \<mu>" by (rule restricted_measure_space[OF `A \<in> sets M`])
@@ -1524,7 +1526,7 @@
     fix g assume "simple_function (\<lambda>x. g x * indicator A x)"
       "g \<le> f"
     then show "\<exists>x. simple_function x \<and> x \<le> (\<lambda>x. f x * indicator A x) \<and>
-      simple_integral (\<lambda>x. g x * indicator A x) = simple_integral x"
+      (\<integral>\<^isup>Sx. g x * indicator A x) = simple_integral x"
       apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
       by (auto simp: indicator_def le_fun_def)
   next
@@ -1541,39 +1543,36 @@
   qed
 qed
 
-lemma (in measure_space) positive_integral_subalgebra[simp]:
-  assumes borel: "f \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets := N\<rparr>)"
-  shows "measure_space.positive_integral (M\<lparr>sets := N\<rparr>) \<mu> f = positive_integral f"
+lemma (in measure_space) positive_integral_subalgebra:
+  assumes borel: "f \<in> borel_measurable N"
+  and N: "sets N \<subseteq> sets M" "space N = space M" and sa: "sigma_algebra N"
+  shows "measure_space.positive_integral N \<mu> f = positive_integral f"
 proof -
-  note msN = measure_space_subalgebra[OF N_subalgebra]
-  then interpret N: measure_space "M\<lparr>sets:=N\<rparr>" \<mu> .
+  interpret N: measure_space N \<mu> using measure_space_subalgebra[OF sa N] .
   from N.borel_measurable_implies_simple_function_sequence[OF borel]
   obtain fs where Nsf: "\<And>i. N.simple_function (fs i)" and "fs \<up> f" by blast
   then have sf: "\<And>i. simple_function (fs i)"
-    using simple_function_subalgebra[OF _ N_subalgebra] by blast
+    using simple_function_subalgebra[OF _ N sa] by blast
   from positive_integral_isoton_simple[OF `fs \<up> f` sf] N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf]
-  show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
+  show ?thesis unfolding isoton_def simple_integral_def N.simple_integral_def `space N = space M` by simp
 qed
 
 section "Lebesgue Integral"
 
 definition (in measure_space) integrable where
   "integrable f \<longleftrightarrow> f \<in> borel_measurable M \<and>
-    positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega> \<and>
-    positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>"
+    (\<integral>\<^isup>+ x. Real (f x)) \<noteq> \<omega> \<and>
+    (\<integral>\<^isup>+ x. Real (- f x)) \<noteq> \<omega>"
 
 lemma (in measure_space) integrableD[dest]:
   assumes "integrable f"
   shows "f \<in> borel_measurable M"
-  "positive_integral (\<lambda>x. Real (f x)) \<noteq> \<omega>"
-  "positive_integral (\<lambda>x. Real (- f x)) \<noteq> \<omega>"
+  "(\<integral>\<^isup>+ x. Real (f x)) \<noteq> \<omega>"
+  "(\<integral>\<^isup>+ x. Real (- f x)) \<noteq> \<omega>"
   using assms unfolding integrable_def by auto
 
-definition (in measure_space) integral where
-  "integral f =
-    real (positive_integral (\<lambda>x. Real (f x))) -
-    real (positive_integral (\<lambda>x. Real (- f x)))"
+definition (in measure_space) integral (binder "\<integral> " 10) where
+  "integral f = real ((\<integral>\<^isup>+ x. Real (f x))) - real ((\<integral>\<^isup>+ x. Real (- f x)))"
 
 lemma (in measure_space) integral_cong:
   assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
@@ -1609,7 +1608,7 @@
 
 lemma (in measure_space) integral_eq_positive_integral:
   assumes "\<And>x. 0 \<le> f x"
-  shows "integral f = real (positive_integral (\<lambda>x. Real (f x)))"
+  shows "integral f = real ((\<integral>\<^isup>+ x. Real (f x)))"
 proof -
   have "\<And>x. Real (- f x) = 0" using assms by simp
   thus ?thesis by (simp del: Real_eq_0 add: integral_def)
@@ -1617,7 +1616,7 @@
 
 lemma (in measure_space) integral_vimage_inv:
   assumes f: "bij_betw f S (space M)"
-  shows "measure_space.integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g x) = integral (\<lambda>x. g (the_inv_into S f x))"
+  shows "measure_space.integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g x) = (\<integral>x. g (the_inv_into S f x))"
 proof -
   interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
     using f by (rule measure_space_isomorphic)
@@ -1634,7 +1633,7 @@
 
 lemma (in measure_space) integral_minus[intro, simp]:
   assumes "integrable f"
-  shows "integrable (\<lambda>x. - f x)" "integral (\<lambda>x. - f x) = - integral f"
+  shows "integrable (\<lambda>x. - f x)" "(\<integral>x. - f x) = - integral f"
   using assms by (auto simp: integrable_def integral_def)
 
 lemma (in measure_space) integral_of_positive_diff:
@@ -1685,7 +1684,7 @@
 lemma (in measure_space) integral_linear:
   assumes "integrable f" "integrable g" and "0 \<le> a"
   shows "integrable (\<lambda>t. a * f t + g t)"
-  and "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g"
+  and "(\<integral> t. a * f t + g t) = a * integral f + integral g"
 proof -
   let ?PI = positive_integral
   let "?f x" = "Real (f x)"
@@ -1718,7 +1717,7 @@
 
   show "integrable (\<lambda>t. a * f t + g t)" by (rule diff)
 
-  from assms show "integral (\<lambda>t. a * f t + g t) = a * integral f + integral g"
+  from assms show "(\<integral> t. a * f t + g t) = a * integral f + integral g"
     unfolding diff(2) unfolding integral_def * linear integrable_def
     by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?g", cases "?PI ?mg")
        (auto simp add: field_simps zero_le_mult_iff)
@@ -1727,21 +1726,21 @@
 lemma (in measure_space) integral_add[simp, intro]:
   assumes "integrable f" "integrable g"
   shows "integrable (\<lambda>t. f t + g t)"
-  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
+  and "(\<integral> t. f t + g t) = integral f + integral g"
   using assms integral_linear[where a=1] by auto
 
 lemma (in measure_space) integral_zero[simp, intro]:
   shows "integrable (\<lambda>x. 0)"
-  and "integral (\<lambda>x. 0) = 0"
+  and "(\<integral> x.0) = 0"
   unfolding integrable_def integral_def
   by (auto simp add: borel_measurable_const)
 
 lemma (in measure_space) integral_cmult[simp, intro]:
   assumes "integrable f"
   shows "integrable (\<lambda>t. a * f t)" (is ?P)
-  and "integral (\<lambda>t. a * f t) = a * integral f" (is ?I)
+  and "(\<integral> t. a * f t) = a * integral f" (is ?I)
 proof -
-  have "integrable (\<lambda>t. a * f t) \<and> integral (\<lambda>t. a * f t) = a * integral f"
+  have "integrable (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t) = a * integral f"
   proof (cases rule: le_cases)
     assume "0 \<le> a" show ?thesis
       using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
@@ -1758,7 +1757,7 @@
 
 lemma (in measure_space) integral_multc:
   assumes "integrable f"
-  shows "integral (\<lambda>x. f x * c) = integral f * c"
+  shows "(\<integral> x. f x * c) = integral f * c"
   unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
 
 lemma (in measure_space) integral_mono_AE:
@@ -1785,7 +1784,7 @@
 lemma (in measure_space) integral_diff[simp, intro]:
   assumes f: "integrable f" and g: "integrable g"
   shows "integrable (\<lambda>t. f t - g t)"
-  and "integral (\<lambda>t. f t - g t) = integral f - integral g"
+  and "(\<integral> t. f t - g t) = integral f - integral g"
   using integral_add[OF f integral_minus(1)[OF g]]
   unfolding diff_minus integral_minus(2)[OF g]
   by auto
@@ -1806,7 +1805,7 @@
 lemma (in measure_space) integral_cmul_indicator:
   assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<omega>"
   shows "integrable (\<lambda>x. c * indicator A x)" (is ?P)
-  and "integral (\<lambda>x. c * indicator A x) = c * real (\<mu> A)" (is ?I)
+  and "(\<integral>x. c * indicator A x) = c * real (\<mu> A)" (is ?I)
 proof -
   show ?P
   proof (cases "c = 0")
@@ -1821,7 +1820,7 @@
 
 lemma (in measure_space) integral_setsum[simp, intro]:
   assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
-  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
+  shows "(\<integral>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
     and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S")
 proof -
   have "?int S \<and> ?I S"
@@ -1847,6 +1846,22 @@
     using positive_integral_linear[OF f, of 1] by simp
 qed
 
+lemma (in measure_space) integral_subalgebra:
+  assumes borel: "f \<in> borel_measurable N"
+  and N: "sets N \<subseteq> sets M" "space N = space M" and sa: "sigma_algebra N"
+  shows "measure_space.integrable N \<mu> f \<longleftrightarrow> integrable f" (is ?P)
+    and "measure_space.integral N \<mu> f = integral f" (is ?I)
+proof -
+  interpret N: measure_space N \<mu> using measure_space_subalgebra[OF sa N] .
+  have "(\<lambda>x. Real (f x)) \<in> borel_measurable N" "(\<lambda>x. Real (- f x)) \<in> borel_measurable N"
+    using borel by auto
+  note * = this[THEN positive_integral_subalgebra[OF _ N sa]]
+  have "f \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable N"
+    using assms unfolding measurable_def by auto
+  then show ?P ?I unfolding integrable_def N.integrable_def integral_def N.integral_def
+    unfolding * by auto
+qed
+
 lemma (in measure_space) integrable_bound:
   assumes "integrable f"
   and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
@@ -1854,21 +1869,21 @@
   assumes borel: "g \<in> borel_measurable M"
   shows "integrable g"
 proof -
-  have "positive_integral (\<lambda>x. Real (g x)) \<le> positive_integral (\<lambda>x. Real \<bar>g x\<bar>)"
+  have "(\<integral>\<^isup>+ x. Real (g x)) \<le> (\<integral>\<^isup>+ x. Real \<bar>g x\<bar>)"
     by (auto intro!: positive_integral_mono)
-  also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))"
+  also have "\<dots> \<le> (\<integral>\<^isup>+ x. Real (f x))"
     using f by (auto intro!: positive_integral_mono)
   also have "\<dots> < \<omega>"
     using `integrable f` unfolding integrable_def by (auto simp: pextreal_less_\<omega>)
-  finally have pos: "positive_integral (\<lambda>x. Real (g x)) < \<omega>" .
+  finally have pos: "(\<integral>\<^isup>+ x. Real (g x)) < \<omega>" .
 
-  have "positive_integral (\<lambda>x. Real (- g x)) \<le> positive_integral (\<lambda>x. Real (\<bar>g x\<bar>))"
+  have "(\<integral>\<^isup>+ x. Real (- g x)) \<le> (\<integral>\<^isup>+ x. Real (\<bar>g x\<bar>))"
     by (auto intro!: positive_integral_mono)
-  also have "\<dots> \<le> positive_integral (\<lambda>x. Real (f x))"
+  also have "\<dots> \<le> (\<integral>\<^isup>+ x. Real (f x))"
     using f by (auto intro!: positive_integral_mono)
   also have "\<dots> < \<omega>"
     using `integrable f` unfolding integrable_def by (auto simp: pextreal_less_\<omega>)
-  finally have neg: "positive_integral (\<lambda>x. Real (- g x)) < \<omega>" .
+  finally have neg: "(\<integral>\<^isup>+ x. Real (- g x)) < \<omega>" .
 
   from neg pos borel show ?thesis
     unfolding integrable_def by auto
@@ -1908,10 +1923,10 @@
 
 lemma (in measure_space) integral_triangle_inequality:
   assumes "integrable f"
-  shows "\<bar>integral f\<bar> \<le> integral (\<lambda>x. \<bar>f x\<bar>)"
+  shows "\<bar>integral f\<bar> \<le> (\<integral>x. \<bar>f x\<bar>)"
 proof -
   have "\<bar>integral f\<bar> = max (integral f) (- integral f)" by auto
-  also have "\<dots> \<le> integral (\<lambda>x. \<bar>f x\<bar>)"
+  also have "\<dots> \<le> (\<integral>x. \<bar>f x\<bar>)"
       using assms integral_minus(2)[of f, symmetric]
       by (auto intro!: integral_mono integrable_abs simp del: integral_minus)
   finally show ?thesis .
@@ -1921,7 +1936,7 @@
   assumes "integrable f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
   shows "0 \<le> integral f"
 proof -
-  have "0 = integral (\<lambda>x. 0)" by (auto simp: integral_zero)
+  have "0 = (\<integral>x. 0)" by (auto simp: integral_zero)
   also have "\<dots> \<le> integral f"
     using assms by (rule integral_mono[OF integral_zero(1)])
   finally show ?thesis .
@@ -1953,7 +1968,7 @@
   hence borel_u: "u \<in> borel_measurable M"
     using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
 
-  have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
+  have integral_eq: "\<And>n. (\<integral>\<^isup>+ x. Real (f n x)) = Real (integral (f n))"
     using i unfolding integral_def integrable_def by (auto simp: Real_real)
 
   have pos_integral: "\<And>n. 0 \<le> integral (f n)"
@@ -1961,14 +1976,14 @@
   hence "0 \<le> x"
     using LIMSEQ_le_const[OF ilim, of 0] by auto
 
-  have "(\<lambda>i. positive_integral (\<lambda>x. Real (f i x))) \<up> positive_integral (\<lambda>x. Real (u x))"
+  have "(\<lambda>i. (\<integral>\<^isup>+ x. Real (f i x))) \<up> (\<integral>\<^isup>+ x. Real (u x))"
   proof (rule positive_integral_isoton)
     from SUP_F mono pos
     show "(\<lambda>i x. Real (f i x)) \<up> (\<lambda>x. Real (u x))"
       unfolding isoton_fun_expand by (auto simp: isoton_def mono_def)
   qed (rule borel_f)
-  hence pI: "positive_integral (\<lambda>x. Real (u x)) =
-      (SUP n. positive_integral (\<lambda>x. Real (f n x)))"
+  hence pI: "(\<integral>\<^isup>+ x. Real (u x)) =
+      (SUP n. (\<integral>\<^isup>+ x. Real (f n x)))"
     unfolding isoton_def by simp
   also have "\<dots> = Real x" unfolding integral_eq
   proof (rule SUP_eq_LIMSEQ[THEN iffD2])
@@ -1997,7 +2012,7 @@
       unfolding mono_def le_fun_def by (auto simp: field_simps)
   have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
     using lim by (auto intro!: LIMSEQ_diff)
-  have 5: "(\<lambda>i. integral (\<lambda>x. f i x - f 0 x)) ----> x - integral (f 0)"
+  have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x)) ----> x - integral (f 0)"
     using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
   note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
   have "integrable (\<lambda>x. (u x - f 0 x) + f 0 x)"
@@ -2008,12 +2023,12 @@
 
 lemma (in measure_space) integral_0_iff:
   assumes "integrable f"
-  shows "integral (\<lambda>x. \<bar>f x\<bar>) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
+  shows "(\<integral>x. \<bar>f x\<bar>) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
 proof -
   have *: "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto
   have "integrable (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs)
   hence "(\<lambda>x. Real (\<bar>f x\<bar>)) \<in> borel_measurable M"
-    "positive_integral (\<lambda>x. Real \<bar>f x\<bar>) \<noteq> \<omega>" unfolding integrable_def by auto
+    "(\<integral>\<^isup>+ x. Real \<bar>f x\<bar>) \<noteq> \<omega>" unfolding integrable_def by auto
   from positive_integral_0_iff[OF this(1)] this(2)
   show ?thesis unfolding integral_def *
     by (simp add: real_of_pextreal_eq_0)
@@ -2024,7 +2039,7 @@
   and "positive_integral f \<noteq> \<omega>"
   shows "\<mu> (f -` {\<omega>} \<inter> space M) = 0"
 proof -
-  have "\<omega> * \<mu> (f -` {\<omega>} \<inter> space M) = positive_integral (\<lambda>x. \<omega> * indicator (f -` {\<omega>} \<inter> space M) x)"
+  have "\<omega> * \<mu> (f -` {\<omega>} \<inter> space M) = (\<integral>\<^isup>+ x. \<omega> * indicator (f -` {\<omega>} \<inter> space M) x)"
     using positive_integral_cmult_indicator[OF borel_measurable_vimage, OF assms(1), of \<omega> \<omega>] by simp
   also have "\<dots> \<le> positive_integral f"
     by (auto intro!: positive_integral_mono simp: indicator_def)
@@ -2054,15 +2069,15 @@
 lemma (in measure_space) integral_real:
   fixes f :: "'a \<Rightarrow> pextreal"
   assumes "AE x. f x \<noteq> \<omega>"
-  shows "integral (\<lambda>x. real (f x)) = real (positive_integral f)" (is ?plus)
-    and "integral (\<lambda>x. - real (f x)) = - real (positive_integral f)" (is ?minus)
+  shows "(\<integral>x. real (f x)) = real (positive_integral f)" (is ?plus)
+    and "(\<integral>x. - real (f x)) = - real (positive_integral f)" (is ?minus)
 proof -
-  have "positive_integral (\<lambda>x. Real (real (f x))) = positive_integral f"
+  have "(\<integral>\<^isup>+ x. Real (real (f x))) = positive_integral f"
     apply (rule positive_integral_cong_AE)
     apply (rule AE_mp[OF assms(1)])
     by (auto intro!: AE_cong simp: Real_real)
   moreover
-  have "positive_integral (\<lambda>x. Real (- real (f x))) = positive_integral (\<lambda>x. 0)"
+  have "(\<integral>\<^isup>+ x. Real (- real (f x))) = (\<integral>\<^isup>+ x. 0)"
     by (intro positive_integral_cong) auto
   ultimately show ?plus ?minus
     by (auto simp: integral_def integrable_def)
@@ -2073,7 +2088,7 @@
   and w: "integrable w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x"
   and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
   shows "integrable u'"
-  and "(\<lambda>i. integral (\<lambda>x. \<bar>u i x - u' x\<bar>)) ----> 0" (is "?lim_diff")
+  and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar>)) ----> 0" (is "?lim_diff")
   and "(\<lambda>i. integral (u i)) ----> integral u'" (is ?lim)
 proof -
   { fix x j assume x: "x \<in> space M"
@@ -2108,31 +2123,31 @@
     finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp }
   note diff_less_2w = this
 
-  have PI_diff: "\<And>m n. positive_integral (\<lambda>x. Real (?diff (m + n) x)) =
-    positive_integral (\<lambda>x. Real (2 * w x)) - positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)"
+  have PI_diff: "\<And>m n. (\<integral>\<^isup>+ x. Real (?diff (m + n) x)) =
+    (\<integral>\<^isup>+ x. Real (2 * w x)) - (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>)"
     using diff w diff_less_2w
     by (subst positive_integral_diff[symmetric])
        (auto simp: integrable_def intro!: positive_integral_cong)
 
   have "integrable (\<lambda>x. 2 * w x)"
     using w by (auto intro: integral_cmult)
-  hence I2w_fin: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> \<omega>" and
+  hence I2w_fin: "(\<integral>\<^isup>+ x. Real (2 * w x)) \<noteq> \<omega>" and
     borel_2w: "(\<lambda>x. Real (2 * w x)) \<in> borel_measurable M"
     unfolding integrable_def by auto
 
-  have "(INF n. SUP m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)) = 0" (is "?lim_SUP = 0")
+  have "(INF n. SUP m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>)) = 0" (is "?lim_SUP = 0")
   proof cases
-    assume eq_0: "positive_integral (\<lambda>x. Real (2 * w x)) = 0"
-    have "\<And>i. positive_integral (\<lambda>x. Real \<bar>u i x - u' x\<bar>) \<le> positive_integral (\<lambda>x. Real (2 * w x))"
+    assume eq_0: "(\<integral>\<^isup>+ x. Real (2 * w x)) = 0"
+    have "\<And>i. (\<integral>\<^isup>+ x. Real \<bar>u i x - u' x\<bar>) \<le> (\<integral>\<^isup>+ x. Real (2 * w x))"
     proof (rule positive_integral_mono)
       fix i x assume "x \<in> space M" from diff_less_2w[OF this, of i]
       show "Real \<bar>u i x - u' x\<bar> \<le> Real (2 * w x)" by auto
     qed
-    hence "\<And>i. positive_integral (\<lambda>x. Real \<bar>u i x - u' x\<bar>) = 0" using eq_0 by auto
+    hence "\<And>i. (\<integral>\<^isup>+ x. Real \<bar>u i x - u' x\<bar>) = 0" using eq_0 by auto
     thus ?thesis by simp
   next
-    assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
-    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
+    assume neq_0: "(\<integral>\<^isup>+ x. Real (2 * w x)) \<noteq> 0"
+    have "(\<integral>\<^isup>+ x. Real (2 * w x)) = (\<integral>\<^isup>+ x. SUP n. INF m. Real (?diff (m + n) x))"
     proof (rule positive_integral_cong, subst add_commute)
       fix x assume x: "x \<in> space M"
       show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
@@ -2144,22 +2159,22 @@
         thus "(\<lambda>i. ?diff i x) ----> 2 * w x" by simp
       qed
     qed
-    also have "\<dots> \<le> (SUP n. INF m. positive_integral (\<lambda>x. Real (?diff (m + n) x)))"
+    also have "\<dots> \<le> (SUP n. INF m. (\<integral>\<^isup>+ x. Real (?diff (m + n) x)))"
       using u'_borel w u unfolding integrable_def
       by (auto intro!: positive_integral_lim_INF)
-    also have "\<dots> = positive_integral (\<lambda>x. Real (2 * w x)) -
-        (INF n. SUP m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>))"
+    also have "\<dots> = (\<integral>\<^isup>+ x. Real (2 * w x)) -
+        (INF n. SUP m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>))"
       unfolding PI_diff pextreal_INF_minus[OF I2w_fin] pextreal_SUP_minus ..
     finally show ?thesis using neq_0 I2w_fin by (rule pextreal_le_minus_imp_0)
   qed
 
   have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto
 
-  have [simp]: "\<And>n m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>) =
-    Real (integral (\<lambda>x. \<bar>u (n + m) x - u' x\<bar>))"
+  have [simp]: "\<And>n m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>) =
+    Real ((\<integral>x. \<bar>u (n + m) x - u' x\<bar>))"
     using diff by (subst add_commute) (simp add: integral_def integrable_def Real_real)
 
-  have "(SUP n. INF m. positive_integral (\<lambda>x. Real \<bar>u (m + n) x - u' x\<bar>)) \<le> ?lim_SUP"
+  have "(SUP n. INF m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar>)) \<le> ?lim_SUP"
     (is "?lim_INF \<le> _") by (subst (1 2) add_commute) (rule lim_INF_le_lim_SUP)
   hence "?lim_INF = Real 0" "?lim_SUP = Real 0" using `?lim_SUP = 0` by auto
   thus ?lim_diff using diff by (auto intro!: integral_positive lim_INF_eq_lim_SUP)
@@ -2168,15 +2183,15 @@
   proof (rule LIMSEQ_I)
     fix r :: real assume "0 < r"
     from LIMSEQ_D[OF `?lim_diff` this]
-    obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> integral (\<lambda>x. \<bar>u n x - u' x\<bar>) < r"
+    obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> (\<integral>x. \<bar>u n x - u' x\<bar>) < r"
       using diff by (auto simp: integral_positive)
 
     show "\<exists>N. \<forall>n\<ge>N. norm (integral (u n) - integral u') < r"
     proof (safe intro!: exI[of _ N])
       fix n assume "N \<le> n"
-      have "\<bar>integral (u n) - integral u'\<bar> = \<bar>integral (\<lambda>x. u n x - u' x)\<bar>"
+      have "\<bar>integral (u n) - integral u'\<bar> = \<bar>(\<integral>x. u n x - u' x)\<bar>"
         using u `integrable u'` by (auto simp: integral_diff)
-      also have "\<dots> \<le> integral (\<lambda>x. \<bar>u n x - u' x\<bar>)" using u `integrable u'`
+      also have "\<dots> \<le> (\<integral>x. \<bar>u n x - u' x\<bar>)" using u `integrable u'`
         by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff)
       also note N[OF `N \<le> n`]
       finally show "norm (integral (u n) - integral u') < r" by simp
@@ -2187,9 +2202,9 @@
 lemma (in measure_space) integral_sums:
   assumes borel: "\<And>i. integrable (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 (\<lambda>x. \<bar>f i x\<bar>))"
+  and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar>))"
   shows "integrable (\<lambda>x. (\<Sum>i. f i x))" (is "integrable ?S")
-  and "(\<lambda>i. integral (f i)) sums integral (\<lambda>x. (\<Sum>i. f i x))" (is ?integral)
+  and "(\<lambda>i. integral (f i)) sums (\<integral>x. (\<Sum>i. f i x))" (is ?integral)
 proof -
   have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
     using summable unfolding summable_def by auto
@@ -2198,7 +2213,7 @@
 
   let "?w y" = "if y \<in> space M then w y else 0"
 
-  obtain x where abs_sum: "(\<lambda>i. integral (\<lambda>x. \<bar>f i x\<bar>)) sums x"
+  obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar>)) sums x"
     using sums unfolding summable_def ..
 
   have 1: "\<And>n. integrable (\<lambda>x. \<Sum>i = 0..<n. f i x)"
@@ -2221,7 +2236,7 @@
       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
     { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
         using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
-    have *: "\<And>n. integral (?w' n) = (\<Sum>i = 0..< n. integral (\<lambda>x. \<bar>f i x\<bar>))"
+    have *: "\<And>n. integral (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar>))"
       using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
     from abs_sum
     show "(\<lambda>i. integral (?w' i)) ----> x" unfolding * sums_def .
@@ -2275,15 +2290,15 @@
       by (auto intro!: sums_single simp: F F_abs) }
   note F_sums_f = this(1) and F_abs_sums_f = this(2)
 
-  have int_f: "integral f = integral (\<lambda>x. \<Sum>r. ?F r x)" "integrable f = integrable (\<lambda>x. \<Sum>r. ?F r x)"
+  have int_f: "integral f = (\<integral>x. \<Sum>r. ?F r x)" "integrable f = integrable (\<lambda>x. \<Sum>r. ?F r x)"
     using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff)
 
   { fix r
-    have "integral (\<lambda>x. \<bar>?F r x\<bar>) = integral (\<lambda>x. \<bar>enum r\<bar> * indicator (?A r) x)"
+    have "(\<integral>x. \<bar>?F r x\<bar>) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x)"
       by (auto simp: indicator_def intro!: integral_cong)
     also have "\<dots> = \<bar>enum r\<bar> * real (\<mu> (?A r))"
       using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
-    finally have "integral (\<lambda>x. \<bar>?F r x\<bar>) = \<bar>enum r * real (\<mu> (?A r))\<bar>"
+    finally have "(\<integral>x. \<bar>?F r x\<bar>) = \<bar>enum r * real (\<mu> (?A r))\<bar>"
       by (simp add: abs_mult_pos real_pextreal_pos) }
   note int_abs_F = this
 
@@ -2306,7 +2321,7 @@
   assumes f: "f \<in> borel_measurable M" and finite: "finite (f`space M)"
   and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>"
   shows "integrable f"
-  and "integral (\<lambda>x. f x) =
+  and "(\<integral>x. f x) =
     (\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
 proof -
   let "?A r" = "f -` {r} \<inter> space M"
@@ -2336,7 +2351,7 @@
 lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
   "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
 proof -
-  have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
+  have *: "positive_integral f = (\<integral>\<^isup>+ x. \<Sum>y\<in>space M. f y * indicator {y} x)"
     by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
   show ?thesis unfolding * using borel_measurable_finite[of f]
     by (simp add: positive_integral_setsum positive_integral_cmult_indicator)
@@ -2347,8 +2362,8 @@
   and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
 proof -
   have [simp]:
-    "positive_integral (\<lambda>x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
-    "positive_integral (\<lambda>x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
+    "(\<integral>\<^isup>+ x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
+    "(\<integral>\<^isup>+ x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
     unfolding positive_integral_finite_eq_setsum by auto
   show "integrable f" using finite_space finite_measure
     by (simp add: setsum_\<omega> integrable_def)
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -626,11 +626,38 @@
   qed
 qed
 
+lemma lebesgue_positive_integral_eq_borel:
+  "f \<in> borel_measurable borel \<Longrightarrow> lebesgue.positive_integral f = borel.positive_integral f "
+  by (auto intro!: lebesgue.positive_integral_subalgebra[symmetric]) default
+
+lemma lebesgue_integral_eq_borel:
+  assumes "f \<in> borel_measurable borel"
+  shows "lebesgue.integrable f = borel.integrable f" (is ?P)
+    and "lebesgue.integral f = borel.integral f" (is ?I)
+proof -
+  have *: "sigma_algebra borel" by default
+  have "sets borel \<subseteq> sets lebesgue" by auto
+  from lebesgue.integral_subalgebra[OF assms this _ *]
+  show ?P ?I by auto
+qed
+
+lemma borel_integral_has_integral:
+  fixes f::"'a::ordered_euclidean_space => real"
+  assumes f:"borel.integrable f"
+  shows "(f has_integral (borel.integral f)) UNIV"
+proof -
+  have borel: "f \<in> borel_measurable borel"
+    using f unfolding borel.integrable_def by auto
+  from f show ?thesis
+    using lebesgue_integral_has_integral[of f]
+    unfolding lebesgue_integral_eq_borel[OF borel] by simp
+qed
+
 lemma continuous_on_imp_borel_measurable:
   fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
   assumes "continuous_on UNIV f"
-  shows "f \<in> borel_measurable lebesgue"
-  apply(rule lebesgue.borel_measurableI)
+  shows "f \<in> borel_measurable borel"
+  apply(rule borel.borel_measurableI)
   using continuous_open_preimage[OF assms] unfolding vimage_def by auto
 
 lemma (in measure_space) integral_monotone_convergence_pos':
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -919,16 +919,15 @@
 qed
 
 lemma (in measure_space) measure_space_subalgebra:
-  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
-  shows "measure_space (M\<lparr> sets := N \<rparr>) \<mu>"
+  assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M"
+  shows "measure_space N \<mu>"
 proof -
-  interpret N: sigma_algebra "M\<lparr> sets := N \<rparr>" by fact
+  interpret N: sigma_algebra N by fact
   show ?thesis
   proof
-    show "countably_additive (M\<lparr>sets := N\<rparr>) \<mu>"
-      using `N \<subseteq> sets M`
-      by (auto simp add: countably_additive_def
-               intro!: measure_countably_additive)
+    from `sets N \<subseteq> sets M` have "\<And>A. range A \<subseteq> sets N \<Longrightarrow> range A \<subseteq> sets M" by blast
+    then show "countably_additive N \<mu>"
+      by (auto intro!: measure_countably_additive simp: countably_additive_def)
   qed simp
 qed
 
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Positive_Extended_Real.thy
--- a/src/HOL/Probability/Positive_Extended_Real.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Positive_Extended_Real.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -1603,6 +1603,136 @@
 qed
 end
 
+lemma minus_omega[simp]: "x - \<omega> = 0" by (cases x) auto
+
+lemma open_pextreal_alt: "open A \<longleftrightarrow>
+  (\<forall>x\<in>A. \<exists>e>0. {x-e <..< x+e} \<subseteq> A) \<and> (\<omega> \<in> A \<longrightarrow> (\<exists>x\<ge>0. {Real x <..} \<subseteq> A))"
+proof -
+  have *: "(\<exists>T. open T \<and> (Real ` (T\<inter>{0..}) = A - {\<omega>})) \<longleftrightarrow>
+    open (real ` (A - {\<omega>}) \<union> {..<0})"
+  proof safe
+    fix T assume "open T" and A: "Real ` (T \<inter> {0..}) = A - {\<omega>}"
+    have *: "(\<lambda>x. real (Real x)) ` (T \<inter> {0..}) = T \<inter> {0..}"
+      by auto
+    have **: "T \<inter> {0..} \<union> {..<0} = T \<union> {..<0}" by auto
+    show "open (real ` (A - {\<omega>}) \<union> {..<0})"
+      unfolding A[symmetric] image_image * ** using `open T` by auto
+  next
+    assume "open (real ` (A - {\<omega>}) \<union> {..<0})"
+    moreover have "Real ` ((real ` (A - {\<omega>}) \<union> {..<0}) \<inter> {0..}) = A - {\<omega>}"
+      apply auto
+      apply (case_tac xb)
+      apply auto
+      apply (case_tac x)
+      apply (auto simp: image_iff)
+      apply (erule_tac x="Real r" in ballE)
+      apply auto
+      done
+    ultimately show "\<exists>T. open T \<and> Real ` (T \<inter> {0..}) = A - {\<omega>}" by auto
+  qed
+  also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>A. \<exists>e>0. {x-e <..< x+e} \<subseteq> A)"
+  proof (intro iffI ballI open_subopen[THEN iffD2])
+    fix x assume *: "\<forall>x\<in>A. \<exists>e>0. {x - e<..<x + e} \<subseteq> A" and x: "x \<in> real ` (A - {\<omega>}) \<union> {..<0}"
+    show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
+    proof (cases rule: linorder_cases)
+      assume "x < 0" then show ?thesis by (intro exI[of _ "{..<0}"]) auto
+    next
+      assume "x = 0" with x
+      have "0 \<in> A"
+        apply auto by (case_tac x) auto
+      with * obtain e where "e > 0" "{0 - e<..<0 + e} \<subseteq> A" by auto
+      then have "{..<e} \<subseteq> A" using `0 \<in> A`
+        apply auto
+        apply (case_tac "x = 0")
+        by (auto dest!: pextreal_zero_lessI)
+      then have *: "{..<e} \<subseteq> A - {\<omega>}" by auto
+      def e' \<equiv> "if e = \<omega> then 1 else real e"
+      then have "0 < e'" using `e > 0` by (cases e) auto
+      have "{0..<e'} \<subseteq> real ` (A - {\<omega>})"
+      proof (cases e)
+        case infinite
+        then have "{..<e} = UNIV - {\<omega>}" by auto
+        then have A: "A - {\<omega>} = UNIV - {\<omega>}" using * by auto
+        show ?thesis unfolding e'_def infinite A
+          apply safe
+          apply (rule_tac x="Real x" in image_eqI)
+          apply auto
+          done
+      next
+        case (preal r)
+        then show ?thesis unfolding e'_def using *
+          apply safe
+          apply (rule_tac x="Real x" in image_eqI)
+          by (auto simp: subset_eq)
+      qed
+      then have "{0..<e'} \<union> {..<0} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}" by auto
+      moreover have "{0..<e'} \<union> {..<0} = {..<e'}" using `0 < e'` by auto
+      ultimately have "{..<e'} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}" by simp
+      then show ?thesis using `0 < e'` `x = 0` by auto
+    next
+      assume "0 < x"
+      with x have "Real x \<in> A" apply auto by (case_tac x) auto
+      with * obtain e where "0 < e" and e: "{Real x - e<..<Real x + e} \<subseteq> A" by auto
+      show ?thesis
+      proof cases
+        assume "e < Real x"
+        with `0 < e` obtain r where r: "e = Real r" "0 < r" by (cases e) auto
+        then have "r < x" using `e < Real x` `0 < e` by (auto split: split_if_asm)
+        then have "{x - r <..< x + r} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
+          using e unfolding r
+          apply (auto simp: subset_eq)
+          apply (rule_tac x="Real xa" in image_eqI)
+          by auto
+        then show ?thesis using `0 < r` by (intro exI[of _ "{x - r <..< x + r}"]) auto
+      next
+        assume "\<not> e < Real x"
+        moreover then have "Real x - e = 0" by (cases e) auto
+        moreover have "\<And>z. 0 < z \<Longrightarrow>  z * 2 < 3 * x \<Longrightarrow> Real z < Real x + e"
+          using `\<not> e < Real x` by (cases e) auto
+        ultimately have "{0 <..< x + x / 2} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
+          using e
+          apply (auto simp: subset_eq)
+          apply (erule_tac x="Real xa" in ballE)
+          apply (auto simp: not_less)
+          apply (rule_tac x="Real xa" in image_eqI)
+          apply auto
+          done
+        moreover have "x \<in> {0 <..< x + x / 2}" using `0 < x` by auto
+        ultimately show ?thesis by (intro exI[of _ "{0 <..< x + x / 2}"]) auto
+      qed
+    qed
+  next
+    fix x assume x: "x \<in> A" "open (real ` (A - {\<omega>}) \<union> {..<0})"
+    then show "\<exists>e>0. {x - e<..<x + e} \<subseteq> A"
+    proof (cases x)
+      case infinite then show ?thesis by (intro exI[of _ 2]) auto
+    next
+      case (preal r)
+      with `x \<in> A` have r: "r \<in> real ` (A - {\<omega>}) \<union> {..<0}" by force
+      from x(2)[unfolded open_real, THEN bspec, OF r]
+      obtain e where e: "0 < e" "\<And>x'. \<bar>x' - r\<bar> < e \<Longrightarrow> x' \<in> real ` (A - {\<omega>}) \<union> {..<0}"
+        by auto
+      show ?thesis using `0 < e` preal
+      proof (auto intro!: exI[of _ "Real e"] simp: greaterThanLessThan_iff not_less 
+                  split: split_if_asm)
+        fix z assume *: "Real (r - e) < z" "z < Real (r + e)"
+        then obtain q where [simp]: "z = Real q" "0 \<le> q" by (cases z) auto
+        with * have "r - e < q" "q < r + e" by (auto split: split_if_asm)
+        with e(2)[of q] have "q \<in> real ` (A - {\<omega>}) \<union> {..<0}" by auto
+        then show "z \<in> A" using `0 \<le> q` apply auto apply (case_tac x) apply auto done
+      next
+        fix z assume *: "0 < z" "z < Real (r + e)" "r \<le> e"
+        then obtain q where [simp]: "z = Real q" and "0 < q" by (cases z) auto
+        with * have "q < r + e" by (auto split: split_if_asm)
+        moreover have "r - e < q" using `r \<le> e` `0 < q` by auto
+        ultimately have "q \<in> real ` (A - {\<omega>}) \<union> {..<0}" using e(2)[of q] by auto
+        then show "z \<in> A" using `0 < q` apply auto apply (case_tac x) apply auto done
+      qed
+    qed
+  qed
+  finally show ?thesis unfolding open_pextreal_def by simp
+qed
+
 lemma open_pextreal_lessThan[simp]:
   "open {..< a :: pextreal}"
 proof (cases a)
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -851,13 +851,13 @@
 qed
 
 lemma (in prob_space) prob_space_subalgebra:
-  assumes "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
-  shows "prob_space (M\<lparr> sets := N \<rparr>) \<mu>"
+  assumes "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
+  shows "prob_space N \<mu>"
 proof -
-  interpret N: measure_space "M\<lparr> sets := N \<rparr>" \<mu>
+  interpret N: measure_space N \<mu>
     using measure_space_subalgebra[OF assms] .
   show ?thesis
-    proof qed (simp add: measure_space_1)
+    proof qed (simp add: `space N = space M` measure_space_1)
 qed
 
 lemma (in prob_space) prob_space_of_restricted_space:
@@ -955,46 +955,46 @@
 lemma (in prob_space) conditional_expectation_exists:
   fixes X :: "'a \<Rightarrow> pextreal"
   assumes borel: "X \<in> borel_measurable M"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
-  shows "\<exists>Y\<in>borel_measurable (M\<lparr> sets := N \<rparr>). \<forall>C\<in>N.
-      positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)"
+  and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
+  shows "\<exists>Y\<in>borel_measurable N. \<forall>C\<in>sets N.
+      (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)"
 proof -
-  interpret P: prob_space "M\<lparr> sets := N \<rparr>" \<mu>
-    using prob_space_subalgebra[OF N_subalgebra] .
+  interpret P: prob_space N \<mu>
+    using prob_space_subalgebra[OF N] .
 
   let "?f A" = "\<lambda>x. X x * indicator A x"
   let "?Q A" = "positive_integral (?f A)"
 
   from measure_space_density[OF borel]
-  have Q: "measure_space (M\<lparr> sets := N \<rparr>) ?Q"
-    by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra])
-  then interpret Q: measure_space "M\<lparr> sets := N \<rparr>" ?Q .
+  have Q: "measure_space N ?Q"
+    by (rule measure_space.measure_space_subalgebra[OF _ N])
+  then interpret Q: measure_space N ?Q .
 
   have "P.absolutely_continuous ?Q"
     unfolding P.absolutely_continuous_def
-  proof (safe, simp)
-    fix A assume "A \<in> N" "\<mu> A = 0"
+  proof safe
+    fix A assume "A \<in> sets N" "\<mu> A = 0"
     moreover then have f_borel: "?f A \<in> borel_measurable M"
-      using borel N_subalgebra by (auto intro: borel_measurable_indicator)
+      using borel N by (auto intro: borel_measurable_indicator)
     moreover have "{x\<in>space M. ?f A x \<noteq> 0} = (?f A -` {0<..} \<inter> space M) \<inter> A"
       by (auto simp: indicator_def)
     moreover have "\<mu> \<dots> \<le> \<mu> A"
-      using `A \<in> N` N_subalgebra f_borel
+      using `A \<in> sets N` N f_borel
       by (auto intro!: measure_mono Int[of _ A] measurable_sets)
     ultimately show "?Q A = 0"
       by (simp add: positive_integral_0_iff)
   qed
   from P.Radon_Nikodym[OF Q this]
-  obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
-    "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
+  obtain Y where Y: "Y \<in> borel_measurable N"
+    "\<And>A. A \<in> sets N \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
     by blast
-  with N_subalgebra show ?thesis
-    by (auto intro!: bexI[OF _ Y(1)])
+  with N(2) show ?thesis
+    by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ N(2,3,1)])
 qed
 
 definition (in prob_space)
-  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
-    \<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))"
+  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable N
+    \<and> (\<forall>C\<in>sets N. (\<integral>\<^isup>+x. Y x * indicator C x) = (\<integral>\<^isup>+x. X x * indicator C x)))"
 
 abbreviation (in prob_space)
   "conditional_prob N A \<equiv> conditional_expectation N (indicator A)"
@@ -1002,19 +1002,19 @@
 lemma (in prob_space)
   fixes X :: "'a \<Rightarrow> pextreal"
   assumes borel: "X \<in> borel_measurable M"
-  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
   shows borel_measurable_conditional_expectation:
-    "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
-  and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
-      positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) =
-      positive_integral (\<lambda>x. X x * indicator C x)"
-   (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
+    "conditional_expectation N X \<in> borel_measurable N"
+  and conditional_expectation: "\<And>C. C \<in> sets N \<Longrightarrow>
+      (\<integral>\<^isup>+x. conditional_expectation N X x * indicator C x) =
+      (\<integral>\<^isup>+x. X x * indicator C x)"
+   (is "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C")
 proof -
   note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
-  then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+  then show "conditional_expectation N X \<in> borel_measurable N"
     unfolding conditional_expectation_def by (rule someI2_ex) blast
 
-  from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
+  from CE show "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C"
     unfolding conditional_expectation_def by (rule someI2_ex) blast
 qed
 
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -784,7 +784,7 @@
   note SUPR_C = this
   ultimately show "?C f \<in> borel_measurable M1"
     by (simp cong: measurable_cong)
-  have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
+  have "positive_integral (\<lambda>x. (SUP i. F i x)) = (SUP i. positive_integral (F i))"
     using F_borel F_mono
     by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
   also have "(SUP i. positive_integral (F i)) =
@@ -1935,8 +1935,7 @@
   proof (unfold integrable_def, intro conjI)
     show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
       using borel by auto
-    have "positive_integral (\<lambda>x. Real (abs (?f x))) =
-      positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
+    have "positive_integral (\<lambda>x. Real (abs (?f x))) = positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
       by (simp add: Real_setprod abs_setprod)
     also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
       using f by (subst product_positive_integral_setprod) auto
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -114,7 +114,7 @@
 qed
 
 lemma (in measure_space) density_is_absolutely_continuous:
-  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   shows "absolutely_continuous \<nu>"
   using assms unfolding absolutely_continuous_def
   by (simp add: positive_integral_null_set)
@@ -289,10 +289,10 @@
 lemma (in finite_measure) Radon_Nikodym_finite_measure:
   assumes "finite_measure M \<nu>"
   assumes "absolutely_continuous \<nu>"
-  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
 proof -
   interpret M': finite_measure M \<nu> using assms(1) .
-  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}"
+  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A}"
   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"
@@ -308,16 +308,16 @@
       have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
         g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
         by (auto simp: indicator_def max_def)
-      hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
-        positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
-        positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
+      hence "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) =
+        (\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x) +
+        (\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x)"
         using f g sets unfolding G_def
         by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
       also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
         using f g sets unfolding G_def by (auto intro!: add_mono)
       also have "\<dots> = \<nu> A"
         using M'.measure_additive[OF sets] union by auto
-      finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
+      finally show "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
     qed }
   note max_in_G = this
   { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
@@ -331,17 +331,17 @@
       hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
         using f_borel by (auto intro!: borel_measurable_indicator)
       from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
-      have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
-          (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
+      have SUP: "(\<integral>\<^isup>+x. g x * indicator A x) =
+          (SUP i. (\<integral>\<^isup>+x. f i x * indicator A x))"
         unfolding isoton_def by simp
-      show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
+      show "(\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
         using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
     qed }
   note SUP_in_G = this
   let ?y = "SUP g : G. positive_integral g"
   have "?y \<le> \<nu> (space M)" unfolding G_def
   proof (safe intro!: SUP_leI)
-    fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
+    fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A"
     from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
       by (simp cong: positive_integral_cong)
   qed
@@ -384,7 +384,7 @@
       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   qed
   finally have int_f_eq_y: "positive_integral f = ?y" .
-  let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
+  let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. f x * indicator A x)"
   have "finite_measure M ?t"
   proof
     show "?t {} = 0" by simp
@@ -392,26 +392,26 @@
     show "countably_additive M ?t" unfolding countably_additive_def
     proof safe
       fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
-      have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
-        = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
+      have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
+        = (\<integral>\<^isup>+x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
         using `range A \<subseteq> sets M`
         by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
-      also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
+      also have "\<dots> = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)"
         apply (rule positive_integral_cong)
         apply (subst psuminf_cmult_right)
         unfolding psuminf_indicator[OF `disjoint_family A`] ..
-      finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
-        = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
+      finally have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
+        = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)" .
       moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
         using M'.measure_countably_additive A by (simp add: comp_def)
-      moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
+      moreover have "\<And>i. (\<integral>\<^isup>+x. f x * indicator (A i) x) \<le> \<nu> (A i)"
           using A `f \<in> G` unfolding G_def by auto
       moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
       moreover {
-        have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
+        have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
           using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
         also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>)
-        finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
+        finally have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
           by (simp add: pextreal_less_\<omega>) }
       ultimately
       show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
@@ -433,9 +433,9 @@
     hence pos_M: "0 < \<mu> (space M)"
       using ac top unfolding absolutely_continuous_def by auto
     moreover
-    have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
+    have "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<le> \<nu> (space M)"
       using `f \<in> G` unfolding G_def by auto
-    hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
+    hence "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<noteq> \<omega>"
       using M'.finite_measure_of_space by auto
     moreover
     def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
@@ -462,30 +462,30 @@
     let "?f0 x" = "f x + b * indicator A0 x"
     { fix A assume A: "A \<in> sets M"
       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
-      have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
-        positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
+      have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x) =
+        (\<integral>\<^isup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
         by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
-      hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
-          positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
+      hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x) =
+          (\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
         by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
     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
-      have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
+      have f_le_v: "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
         using `f \<in> G` A unfolding G_def by auto
       note f0_eq[OF A]
-      also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
-          positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
+      also have "(\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
+          (\<integral>\<^isup>+x. f x * indicator A x) + ?t (A \<inter> A0)"
         using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
         by (auto intro!: add_left_mono)
-      also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
+      also have "\<dots> \<le> (\<integral>\<^isup>+x. f x * indicator A x) + ?t A"
         using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
         by (auto intro!: add_left_mono)
       also have "\<dots> \<le> \<nu> A"
         using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
-        by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
-      finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
+        by (cases "(\<integral>\<^isup>+x. f x * indicator A x)", cases "\<nu> A", auto)
+      finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x) \<le> \<nu> A" . }
     hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
       by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times)
     have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
@@ -525,11 +525,11 @@
   show ?thesis
   proof (safe intro!: bexI[of _ f])
     fix A assume "A\<in>sets M"
-    show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+    show "\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
     proof (rule antisym)
-      show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
+      show "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
         using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
-      show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
+      show "\<nu> A \<le> (\<integral>\<^isup>+x. f x * indicator A x)"
         using upper_bound[THEN bspec, OF `A \<in> sets M`]
          by (simp add: pextreal_zero_le_diff)
     qed
@@ -669,7 +669,7 @@
 lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   assumes "measure_space M \<nu>"
   assumes "absolutely_continuous \<nu>"
-  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
 proof -
   interpret v: measure_space M \<nu> by fact
   from split_space_into_finite_sets_and_rest[OF assms]
@@ -680,7 +680,7 @@
     and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
   from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
   have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
-    \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
+    \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   proof
     fix i
     have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
@@ -702,17 +702,17 @@
       by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
     from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
     obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
-      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)"
+      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. (f x * indicator (Q i) x) * indicator A x)"
       unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
         positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
     then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
-      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
+      \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
       by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
           simp: indicator_def)
   qed
   from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
     and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
-      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
+      \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x)"
     by auto
   let "?f x" =
     "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
@@ -728,7 +728,7 @@
         f i x * indicator (Q i \<inter> A) x"
       "\<And>x i. (indicator A x * indicator Q0 x :: pextreal) =
         indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
-    have "positive_integral (\<lambda>x. ?f x * indicator A x) =
+    have "(\<integral>\<^isup>+x. ?f x * indicator A x) =
       (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
       unfolding f[OF `A \<in> sets M`]
       apply (simp del: pextreal_times(2) add: field_simps *)
@@ -755,7 +755,7 @@
       using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
     moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
       using `A \<in> sets M` sets_into_space Q0 by auto
-    ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
+    ultimately show "\<nu> A = (\<integral>\<^isup>+x. ?f x * indicator A x)"
       using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
       by simp
   qed
@@ -764,14 +764,14 @@
 lemma (in sigma_finite_measure) Radon_Nikodym:
   assumes "measure_space M \<nu>"
   assumes "absolutely_continuous \<nu>"
-  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
 proof -
   from Ex_finite_integrable_function
   obtain h where finite: "positive_integral h \<noteq> \<omega>" and
     borel: "h \<in> borel_measurable M" and
     pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
     "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
-  let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
+  let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x)"
   from measure_space_density[OF borel] finite
   interpret T: finite_measure M ?T
     unfolding finite_measure_def finite_measure_axioms_def
@@ -792,7 +792,7 @@
     then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
       using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator)
     from positive_integral_translated_density[OF borel this]
-    show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
+    show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x)"
       unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
   qed
 qed
@@ -802,7 +802,7 @@
 lemma (in measure_space) finite_density_unique:
   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   and fin: "positive_integral f < \<omega>"
-  shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
+  shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. g x * indicator A x))
     \<longleftrightarrow> (AE x. f x = g x)"
     (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
 proof (intro iffI ballI)
@@ -817,7 +817,7 @@
       and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
     let ?N = "{x\<in>space M. g x < f x}"
     have N: "?N \<in> sets M" using borel by simp
-    have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
+    have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^isup>+x. f x * indicator ?N x - g x * indicator ?N x)"
       by (auto intro!: positive_integral_cong simp: indicator_def)
     also have "\<dots> = ?P f ?N - ?P g ?N"
     proof (rule positive_integral_diff)
@@ -848,7 +848,7 @@
 
 lemma (in finite_measure) density_unique_finite_measure:
   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
-  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
+  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   shows "AE x. f x = f' x"
 proof -
@@ -876,13 +876,13 @@
   have 2: "AE x. ?f Q0 x = ?f' Q0 x"
   proof (rule AE_I')
     { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
-        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
       let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
       have "(\<Union>i. ?A i) \<in> null_sets"
       proof (rule null_sets_UN)
         fix i have "?A i \<in> sets M"
           using borel Q0(1) by auto
-        have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
+        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x)"
           unfolding eq[OF `?A i \<in> sets M`]
           by (auto intro!: positive_integral_mono simp: indicator_def)
         also have "\<dots> = of_nat i * \<mu> (?A i)"
@@ -912,38 +912,38 @@
 
 lemma (in sigma_finite_measure) density_unique:
   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
-  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
+  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   shows "AE x. f x = f' x"
 proof -
   obtain h where h_borel: "h \<in> borel_measurable M"
     and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
     using Ex_finite_integrable_function by auto
-  interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
+  interpret h: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
     using h_borel by (rule measure_space_density)
-  interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
+  interpret h: finite_measure M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
     by default (simp cong: positive_integral_cong add: fin)
-  interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
+  interpret f: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x)"
     using borel(1) by (rule measure_space_density)
-  interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
+  interpret f': measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f' x * indicator A x)"
     using borel(2) by (rule measure_space_density)
   { fix A assume "A \<in> sets M"
     then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A"
       using pos sets_into_space by (force simp: indicator_def)
-    then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
+    then have "(\<integral>\<^isup>+x. h x * indicator A x) = 0 \<longleftrightarrow> A \<in> null_sets"
       using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
   note h_null_sets = this
   { fix A assume "A \<in> sets M"
-    have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
+    have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) =
       f.positive_integral (\<lambda>x. h x * indicator A x)"
       using `A \<in> sets M` h_borel borel
       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
     also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
       by (rule f'.positive_integral_cong_measure) (rule f)
-    also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
+    also have "\<dots> = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))"
       using `A \<in> sets M` h_borel borel
       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
-    finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
+    finally have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))" . }
   then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
     using h_borel borel
     by (intro h.density_unique_finite_measure[OF borel])
@@ -955,7 +955,7 @@
 
 lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
   assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
-    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
 proof
   assume "sigma_finite_measure M \<nu>"
@@ -965,10 +965,10 @@
     and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
   have "AE x. f x * h x \<noteq> \<omega>"
   proof (rule AE_I')
-    have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
+    have "\<nu>.positive_integral h = (\<integral>\<^isup>+x. f x * h x)"
       by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
          (intro positive_integral_translated_density f h)
-    then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
+    then have "(\<integral>\<^isup>+x. f x * h x) \<noteq> \<omega>"
       using h(2) by simp
     then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
       using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
@@ -1018,12 +1018,12 @@
   next
     fix n obtain i j where
       [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
-    have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
+    have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
     proof (cases i)
       case 0
       have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
         using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
-      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
+      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) = 0"
         using A_in_sets f
         apply (subst positive_integral_0_iff)
         apply fast
@@ -1034,8 +1034,8 @@
       then show ?thesis by simp
     next
       case (Suc n)
-      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
-        positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
+      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<le>
+        (\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x)"
         by (auto intro!: positive_integral_mono simp: indicator_def A_def)
       also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
         using Q by (auto intro!: positive_integral_cmult_indicator)
@@ -1052,7 +1052,7 @@
 
 definition (in sigma_finite_measure)
   "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
-    (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
+    (\<forall>A \<in> sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x))"
 
 lemma (in sigma_finite_measure) RN_deriv_cong:
   assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
@@ -1069,7 +1069,7 @@
   assumes "measure_space M \<nu>"
   assumes "absolutely_continuous \<nu>"
   shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
-  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
+  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
     (is "\<And>A. _ \<Longrightarrow> ?int A")
 proof -
   note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
@@ -1082,13 +1082,13 @@
 lemma (in sigma_finite_measure) RN_deriv_positive_integral:
   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
     and f: "f \<in> borel_measurable M"
-  shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
+  shows "measure_space.positive_integral M \<nu> f = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
 proof -
   interpret \<nu>: measure_space M \<nu> by fact
   have "\<nu>.positive_integral f =
-    measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
+    measure_space.positive_integral M (\<lambda>A. (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)) f"
     by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
-  also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
+  also have "\<dots> = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
     by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
   finally show ?thesis .
 qed
@@ -1096,11 +1096,11 @@
 lemma (in sigma_finite_measure) RN_deriv_unique:
   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
   and f: "f \<in> borel_measurable M"
-  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
+  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   shows "AE x. f x = RN_deriv \<nu> x"
 proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
   fix A assume A: "A \<in> sets M"
-  show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
+  show "(\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
 qed
 
@@ -1130,10 +1130,10 @@
     using f by (auto simp: bij_inv_def indicator_def)
   have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
     using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
-  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
+  also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
     unfolding positive_integral_vimage_inv[OF f]
     by (simp add: * cong: positive_integral_cong)
-  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
+  finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
     unfolding A_f[OF `A \<in> sets M`] .
 qed
 
@@ -1150,7 +1150,7 @@
 lemma (in sigma_finite_measure)
   assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
     and f: "f \<in> borel_measurable M"
-  shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
+  shows RN_deriv_integral: "measure_space.integral M \<nu> f = (\<integral>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
     and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
 proof -
   interpret \<nu>: sigma_finite_measure M \<nu> by fact
@@ -1164,7 +1164,7 @@
       then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
         using * by (simp add: Real_real) }
     note * = this
-    have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
+    have "(\<integral>\<^isup>+x. RN_deriv \<nu> x * Real (f x)) = (\<integral>\<^isup>+x. Real (real (RN_deriv \<nu> x) * f x))"
       apply (rule positive_integral_cong_AE)
       apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
       by (auto intro!: AE_cong simp: *) }
@@ -1182,7 +1182,7 @@
 proof -
   note deriv = RN_deriv[OF assms(1, 2)]
   from deriv(2)[OF `{x} \<in> sets M`]
-  have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
+  have "\<nu> {x} = (\<integral>\<^isup>+w. RN_deriv \<nu> x * indicator {x} w)"
     by (auto simp: indicator_def intro!: positive_integral_cong)
   thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
     by auto
diff -r a5478b1c8b8a -r 4638b1210d26 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Jan 14 13:59:06 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Jan 14 16:00:13 2011 +0100
@@ -222,7 +222,44 @@
   | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
 
 definition
-  "sigma M = (| space = space M, sets = sigma_sets (space M) (sets M) |)"
+  "sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M) \<rparr>"
+
+lemma (in sigma_algebra) sigma_sets_subset:
+  assumes a: "a \<subseteq> sets M"
+  shows "sigma_sets (space M) a \<subseteq> sets M"
+proof
+  fix x
+  assume "x \<in> sigma_sets (space M) a"
+  from this show "x \<in> sets M"
+    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
+qed
+
+lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
+  by (erule sigma_sets.induct, auto)
+
+lemma sigma_algebra_sigma_sets:
+     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
+  by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp
+           intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl)
+
+lemma sigma_sets_least_sigma_algebra:
+  assumes "A \<subseteq> Pow S"
+  shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
+proof safe
+  fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
+    and X: "X \<in> sigma_sets S A"
+  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
+  show "X \<in> B" by auto
+next
+  fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
+  then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
+     by simp
+  have "A \<subseteq> sigma_sets S A" using assms
+    by (auto intro!: sigma_sets.Basic)
+  moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
+    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
+  ultimately show "X \<in> sigma_sets S A" by auto
+qed
 
 lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)"
   unfolding sigma_def by simp
@@ -233,9 +270,6 @@
 lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
   by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
 
-lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
-  by (erule sigma_sets.induct, auto)
-
 lemma sigma_sets_Un:
   "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
 apply (simp add: Un_range_binary range_binary_eq)
@@ -274,16 +308,6 @@
   finally show ?thesis .
 qed
 
-lemma (in sigma_algebra) sigma_sets_subset:
-  assumes a: "a \<subseteq> sets M"
-  shows "sigma_sets (space M) a \<subseteq> sets M"
-proof
-  fix x
-  assume "x \<in> sigma_sets (space M) a"
-  from this show "x \<in> sets M"
-    by (induct rule: sigma_sets.induct, auto) (metis a subsetD)
-qed
-
 lemma (in sigma_algebra) sigma_sets_eq:
      "sigma_sets (space M) (sets M) = sets M"
 proof
@@ -294,14 +318,6 @@
     by (metis sigma_sets_subset subset_refl)
 qed
 
-lemma sigma_algebra_sigma_sets:
-     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
-  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
-      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un)
-  apply (blast dest: sigma_sets_into_sp)
-  apply (rule sigma_sets.Union, fast)
-  done
-
 lemma sigma_algebra_sigma:
     "sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)"
   apply (rule sigma_algebra_sigma_sets)
@@ -312,25 +328,6 @@
     "sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)"
   by (simp add: sigma_def sigma_sets_subset)
 
-lemma sigma_sets_least_sigma_algebra:
-  assumes "A \<subseteq> Pow S"
-  shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
-proof safe
-  fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>"
-    and X: "X \<in> sigma_sets S A"
-  from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X
-  show "X \<in> B" by auto
-next
-  fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}"
-  then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B"
-     by simp
-  have "A \<subseteq> sigma_sets S A" using assms
-    by (auto intro!: sigma_sets.Basic)
-  moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>"
-    using assms by (intro sigma_algebra_sigma_sets[of A]) auto
-  ultimately show "X \<in> sigma_sets S A" by auto
-qed
-
 lemma (in sigma_algebra) restriction_in_sets:
   fixes A :: "nat \<Rightarrow> 'a set"
   assumes "S \<in> sets M"