# HG changeset patch
# User hoelzl
# Date 1351862620 -3600
# Node ID ce0d316b5b44a7370145dcccdf630dbcf7dc0742
# Parent  382bd3173584d4d5fd3a5da7fbd8df00216053f7
add measurability prover; add support for Borel sets

diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -100,7 +100,9 @@
 
 lemma measurable_pair_iff:
   "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
-  using measurable_pair[of f M M1 M2] by auto
+  using measurable_pair[of f M M1 M2]
+  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
+  by auto
 
 lemma measurable_split_conv:
   "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -30,14 +30,20 @@
 lemma space_borel[simp]: "space borel = UNIV"
   unfolding borel_def by auto
 
-lemma borel_open[simp]:
+lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
+  unfolding borel_def by auto
+
+lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
+  unfolding borel_def pred_def by auto
+
+lemma borel_open[simp, measurable (raw generic)]:
   assumes "open A" shows "A \<in> sets borel"
 proof -
   have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
   thus ?thesis unfolding borel_def by auto
 qed
 
-lemma borel_closed[simp]:
+lemma borel_closed[simp, measurable (raw generic)]:
   assumes "closed A" shows "A \<in> sets borel"
 proof -
   have "space borel - (- A) \<in> sets borel"
@@ -45,23 +51,18 @@
   thus ?thesis by simp
 qed
 
-lemma borel_comp[intro,simp]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
-  unfolding Compl_eq_Diff_UNIV by (intro Diff) auto
+lemma borel_insert[measurable]:
+  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
+  unfolding insert_def by (rule Un) auto
+
+lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
+  unfolding Compl_eq_Diff_UNIV by simp
 
 lemma borel_measurable_vimage:
   fixes f :: "'a \<Rightarrow> 'x::t2_space"
-  assumes borel: "f \<in> borel_measurable M"
+  assumes borel[measurable]: "f \<in> borel_measurable M"
   shows "f -` {x} \<inter> space M \<in> sets M"
-proof (cases "x \<in> f ` space M")
-  case True then obtain y where "x = f y" by auto
-  from closed_singleton[of "f y"]
-  have "{f y} \<in> sets borel" by (rule borel_closed)
-  with assms show ?thesis
-    unfolding in_borel_measurable_borel `x = f y` by auto
-next
-  case False hence "f -` {x} \<inter> space M = {}" by auto
-  thus ?thesis by auto
-qed
+  by simp
 
 lemma borel_measurableI:
   fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
@@ -81,7 +82,7 @@
       using closed_singleton[of x] by (rule borel_closed)
   qed simp
 
-lemma borel_measurable_const[simp, intro]:
+lemma borel_measurable_const[simp, intro, measurable (raw)]:
   "(\<lambda>x. c) \<in> borel_measurable M"
   by auto
 
@@ -91,7 +92,7 @@
   unfolding indicator_def [abs_def] using A
   by (auto intro!: measurable_If_set)
 
-lemma borel_measurable_indicator': 
+lemma borel_measurable_indicator'[measurable]:
   "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
   unfolding indicator_def[abs_def]
   by (auto intro!: measurable_If)
@@ -119,115 +120,63 @@
   shows "f \<in> borel_measurable M"
   using assms unfolding measurable_def by auto
 
+lemma borel_measurable_continuous_on1:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "continuous_on UNIV f"
+  shows "f \<in> borel_measurable borel"
+  apply(rule borel_measurableI)
+  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
+
 section "Borel spaces on euclidean spaces"
 
-lemma lessThan_borel[simp, intro]:
-  fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "{..< a} \<in> sets borel"
-  by (blast intro: borel_open)
-
-lemma greaterThan_borel[simp, intro]:
-  fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a <..} \<in> sets borel"
-  by (blast intro: borel_open)
-
-lemma greaterThanLessThan_borel[simp, intro]:
-  fixes a b :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a<..<b} \<in> sets borel"
-  by (blast intro: borel_open)
+lemma borel_measurable_euclidean_component'[measurable]:
+  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
+  by (intro continuous_on_euclidean_component continuous_on_id borel_measurable_continuous_on1)
 
-lemma atMost_borel[simp, intro]:
-  fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "{..a} \<in> sets borel"
-  by (blast intro: borel_closed)
-
-lemma atLeast_borel[simp, intro]:
-  fixes a :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a..} \<in> sets borel"
-  by (blast intro: borel_closed)
-
-lemma atLeastAtMost_borel[simp, intro]:
-  fixes a b :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a..b} \<in> sets borel"
-  by (blast intro: borel_closed)
+lemma borel_measurable_euclidean_component:
+  "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
+  by simp
 
-lemma greaterThanAtMost_borel[simp, intro]:
-  fixes a b :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a<..b} \<in> sets borel"
-  unfolding greaterThanAtMost_def by blast
-
-lemma atLeastLessThan_borel[simp, intro]:
+lemma [simp, intro, measurable]:
   fixes a b :: "'a\<Colon>ordered_euclidean_space"
-  shows "{a..<b} \<in> sets borel"
-  unfolding atLeastLessThan_def by blast
-
-lemma hafspace_less_borel[simp, intro]:
-  fixes a :: real
-  shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
-  by (auto intro!: borel_open open_halfspace_component_gt)
+  shows lessThan_borel: "{..< a} \<in> sets borel"
+    and greaterThan_borel: "{a <..} \<in> sets borel"
+    and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
+    and atMost_borel: "{..a} \<in> sets borel"
+    and atLeast_borel: "{a..} \<in> sets borel"
+    and atLeastAtMost_borel: "{a..b} \<in> sets borel"
+    and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
+    and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
+  unfolding greaterThanAtMost_def atLeastLessThan_def
+  by (blast intro: borel_open borel_closed)+
 
-lemma hafspace_greater_borel[simp, intro]:
-  fixes a :: real
-  shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
-  by (auto intro!: borel_open open_halfspace_component_lt)
+lemma 
+  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
+    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
+    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
+    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
+  by simp_all
 
-lemma hafspace_less_eq_borel[simp, intro]:
-  fixes a :: real
-  shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
-  by (auto intro!: borel_closed closed_halfspace_component_ge)
-
-lemma hafspace_greater_eq_borel[simp, intro]:
-  fixes a :: real
-  shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
-  by (auto intro!: borel_closed closed_halfspace_component_le)
-
-lemma borel_measurable_less[simp, intro]:
+lemma borel_measurable_less[simp, intro, measurable]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
 proof -
-  have "{w \<in> space M. f w < g w} =
-        (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
+  have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}"
     using Rats_dense_in_real by (auto simp add: Rats_def)
-  then show ?thesis using f g
-    by simp (blast intro: measurable_sets)
-qed
-
-lemma borel_measurable_le[simp, intro]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
-proof -
-  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
-    by auto
-  thus ?thesis using f g
-    by simp blast
+  with f g show ?thesis
+    by simp
 qed
 
-lemma borel_measurable_eq[simp, intro]:
+lemma [simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "{w \<in> space M. f w = g w} \<in> sets M"
-proof -
-  have "{w \<in> space M. f w = g w} =
-        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
-    by auto
-  thus ?thesis using f g by auto
-qed
-
-lemma borel_measurable_neq[simp, intro]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
-proof -
-  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
-    by auto
-  thus ?thesis using f g by auto
-qed
+  assumes f[measurable]: "f \<in> borel_measurable M"
+  assumes g[measurable]: "g \<in> borel_measurable M"
+  shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
+    and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
+    and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
+  unfolding eq_iff not_less[symmetric] by measurable+
 
 subsection "Borel space equals sigma algebras over intervals"
 
@@ -377,7 +326,7 @@
     by (intro sigma_algebra_sigma_sets) simp_all
   have *: "?set = (\<Union>n. UNIV - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
   proof (safe, simp_all add: not_less)
-    fix x assume "a < x $$ i"
+    fix x :: 'a assume "a < x $$ i"
     with reals_Archimedean[of "x $$ i - a"]
     obtain n where "a + 1 / real (Suc n) < x $$ i"
       by (auto simp: inverse_eq_divide field_simps)
@@ -390,7 +339,7 @@
     finally show "a < x" .
   qed
   show "?set \<in> ?SIGMA" unfolding *
-    by (auto intro!: Diff)
+    by (auto del: Diff intro!: Diff)
 qed
 
 lemma borel_eq_halfspace_less:
@@ -631,27 +580,13 @@
 
 lemma borel_measurable_iff_ge:
   "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
-  using borel_measurable_iff_halfspace_ge[where 'c=real] by simp
+  using borel_measurable_iff_halfspace_ge[where 'c=real]
+  by simp
 
 lemma borel_measurable_iff_greater:
   "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
   using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
 
-lemma borel_measurable_euclidean_component':
-  "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
-proof (rule borel_measurableI)
-  fix S::"real set" assume "open S"
-  from open_vimage_euclidean_component[OF this]
-  show "(\<lambda>x. x $$ i) -` S \<inter> space borel \<in> sets borel"
-    by (auto intro: borel_open)
-qed
-
-lemma borel_measurable_euclidean_component:
-  fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
-  assumes f: "f \<in> borel_measurable M"
-  shows "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
-  using measurable_comp[OF f borel_measurable_euclidean_component'] by (simp add: comp_def)
-
 lemma borel_measurable_euclidean_space:
   fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
@@ -667,13 +602,6 @@
 
 subsection "Borel measurable operators"
 
-lemma borel_measurable_continuous_on1:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes "continuous_on UNIV f"
-  shows "f \<in> borel_measurable borel"
-  apply(rule borel_measurableI)
-  using continuous_open_preimage[OF assms] unfolding vimage_def by auto
-
 lemma borel_measurable_continuous_on:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
@@ -693,7 +621,7 @@
     {x\<in>A. f x \<in> S} \<union> (if c \<in> S then space borel - A else {})"
     by (auto split: split_if_asm)
   also have "\<dots> \<in> sets borel"
-    using * `open A` by (auto simp del: space_borel intro!: Un)
+    using * `open A` by auto
   finally show "?f -` S \<inter> space borel \<in> sets borel" .
 qed
 
@@ -705,7 +633,7 @@
   using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
   by (simp add: comp_def)
 
-lemma borel_measurable_uminus[simp, intro]:
+lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
   fixes g :: "'a \<Rightarrow> real"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. - g x) \<in> borel_measurable M"
@@ -716,7 +644,7 @@
   shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
   unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
 
-lemma borel_measurable_Pair[simp, intro]:
+lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -726,7 +654,7 @@
   have [simp]: "\<And>P A B C. {w. (P \<longrightarrow> A w \<and> B w) \<and> (\<not> P \<longrightarrow> A w \<and> C w)} = 
     {w. A w \<and> (P \<longrightarrow> B w) \<and> (\<not> P \<longrightarrow> C w)}" by auto
   from i f g show "{w \<in> space M. (f w, g w) $$ i \<le> a} \<in> sets M"
-    by (auto simp: euclidean_component_prod intro!: sets_Collect borel_measurable_euclidean_component)
+    by (auto simp: euclidean_component_prod)
 qed
 
 lemma continuous_on_fst: "continuous_on UNIV fst"
@@ -757,7 +685,7 @@
     unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
 qed
 
-lemma borel_measurable_add[simp, intro]:
+lemma borel_measurable_add[simp, intro, measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -766,7 +694,7 @@
   by (rule borel_measurable_continuous_Pair)
      (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
 
-lemma borel_measurable_setsum[simp, intro]:
+lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
@@ -775,14 +703,14 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_diff[simp, intro]:
+lemma borel_measurable_diff[simp, intro, measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   unfolding diff_minus using assms by fast
 
-lemma borel_measurable_times[simp, intro]:
+lemma borel_measurable_times[simp, intro, measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -796,7 +724,7 @@
   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
 
-lemma borel_measurable_dist[simp, intro]:
+lemma borel_measurable_dist[simp, intro, measurable (raw)]:
   fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
@@ -805,6 +733,14 @@
   by (rule borel_measurable_continuous_Pair)
      (intro continuous_on_dist continuous_on_fst continuous_on_snd)
   
+lemma borel_measurable_scaleR[measurable (raw)]:
+  fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
+  by (rule borel_measurable_continuous_Pair[OF f g])
+     (auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd)
+
 lemma affine_borel_measurable_vector:
   fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
   assumes "f \<in> borel_measurable M"
@@ -825,13 +761,15 @@
   qed simp
 qed
 
-lemma affine_borel_measurable:
-  fixes g :: "'a \<Rightarrow> real"
-  assumes g: "g \<in> borel_measurable M"
-  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
-  using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)
+lemma borel_measurable_const_scaleR[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. b *\<^sub>R f x ::'a::real_normed_vector) \<in> borel_measurable M"
+  using affine_borel_measurable_vector[of f M 0 b] by simp
 
-lemma borel_measurable_setprod[simp, intro]:
+lemma borel_measurable_const_add[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
+  using affine_borel_measurable_vector[of f M a 1] by simp
+
+lemma borel_measurable_setprod[simp, intro, measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -840,7 +778,7 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_inverse[simp, intro]:
+lemma borel_measurable_inverse[simp, intro, measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
@@ -853,7 +791,7 @@
     done
 qed
 
-lemma borel_measurable_divide[simp, intro]:
+lemma borel_measurable_divide[simp, intro, measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M"
   and "g \<in> borel_measurable M"
@@ -861,21 +799,21 @@
   unfolding field_divide_inverse
   by (rule borel_measurable_inverse borel_measurable_times assms)+
 
-lemma borel_measurable_max[intro, simp]:
+lemma borel_measurable_max[intro, simp, measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   unfolding max_def by (auto intro!: assms measurable_If)
 
-lemma borel_measurable_min[intro, simp]:
+lemma borel_measurable_min[intro, simp, measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   unfolding min_def by (auto intro!: assms measurable_If)
 
-lemma borel_measurable_abs[simp, intro]:
+lemma borel_measurable_abs[simp, intro, measurable (raw)]:
   assumes "f \<in> borel_measurable M"
   shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
 proof -
@@ -883,7 +821,7 @@
   show ?thesis unfolding * using assms by auto
 qed
 
-lemma borel_measurable_nth[simp, intro]:
+lemma borel_measurable_nth[simp, intro, measurable (raw)]:
   "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
   using borel_measurable_euclidean_component'
   unfolding nth_conv_component by auto
@@ -900,12 +838,12 @@
     from this q show "continuous_on {a<..<b} q"
       by (rule convex_on_continuous)
   qed
-  moreover have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
+  also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
     using X by (intro measurable_cong) auto
-  ultimately show ?thesis by simp
+  finally show ?thesis .
 qed
 
-lemma borel_measurable_ln[simp,intro]:
+lemma borel_measurable_ln[simp, intro, measurable (raw)]:
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
 proof -
@@ -926,39 +864,55 @@
   finally show ?thesis .
 qed
 
-lemma borel_measurable_log[simp,intro]:
-  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log b (f x)) \<in> borel_measurable M"
+lemma borel_measurable_log[simp, intro, measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
   unfolding log_def by auto
 
-lemma borel_measurable_real_floor:
-  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
-  unfolding borel_measurable_iff_ge
-proof (intro allI)
-  fix a :: real
-  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
-      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
-      unfolding real_eq_of_int by simp }
-  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
-  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
+lemma measurable_count_space_eq2_countable:
+  fixes f :: "'a => 'c::countable"
+  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
+proof -
+  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
+    then have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
+      by auto
+    moreover assume "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
+    ultimately have "f -` X \<inter> space M \<in> sets M"
+      using `X \<subseteq> A` by (simp add: subset_eq del: UN_simps) }
+  then show ?thesis
+    unfolding measurable_def by auto
 qed
 
-lemma borel_measurable_real_natfloor[intro, simp]:
-  assumes "f \<in> borel_measurable M"
-  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
+lemma measurable_real_floor[measurable]:
+  "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
 proof -
-  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
-    by (auto simp: max_def natfloor_def)
-  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
-  show ?thesis by (simp add: comp_def)
+  have "\<And>a x. \<lfloor>x\<rfloor> = a \<longleftrightarrow> (real a \<le> x \<and> x < real (a + 1))"
+    by (auto intro: floor_eq2)
+  then show ?thesis
+    by (auto simp: vimage_def measurable_count_space_eq2_countable)
 qed
 
+lemma measurable_real_natfloor[measurable]:
+  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
+  by (simp add: natfloor_def[abs_def])
+
+lemma measurable_real_ceiling[measurable]:
+  "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
+  unfolding ceiling_def[abs_def] by simp
+
+lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
+  by simp
+
+lemma borel_measurable_real_natfloor[intro, simp]:
+  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
+  by simp
+
 subsection "Borel space on the extended reals"
 
-lemma borel_measurable_ereal[simp, intro]:
+lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   using continuous_on_ereal f by (rule borel_measurable_continuous_on)
 
-lemma borel_measurable_real_of_ereal[simp, intro]:
+lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
   fixes f :: "'a \<Rightarrow> ereal" 
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
@@ -977,20 +931,16 @@
   assumes H: "(\<lambda>x. H (ereal (real (f x)))) \<in> borel_measurable M"
   shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
 proof -
-  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then H \<infinity> else if x \<in> f -` {-\<infinity>} then H (-\<infinity>) else H (ereal (real (f x)))"
+  let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real (f x)))"
   { fix x have "H (f x) = ?F x" by (cases "f x") auto }
-  moreover 
-  have "?F \<in> borel_measurable M"
-    by (intro measurable_If_set f measurable_sets[OF f] H) auto
-  ultimately
-  show ?thesis by simp
+  with f H show ?thesis by simp
 qed
 
 lemma
   fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
-  shows borel_measurable_ereal_abs[intro, simp]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
-    and borel_measurable_ereal_inverse[simp, intro]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
-    and borel_measurable_uminus_ereal[intro]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
+  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
+    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
+    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
 
 lemma borel_measurable_uminus_eq_ereal[simp]:
@@ -999,44 +949,32 @@
   assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
 qed auto
 
-lemma sets_Collect_If_set:
-  assumes "A \<inter> space M \<in> sets M" "{x \<in> space M. P x} \<in> sets M" "{x \<in> space M. Q x} \<in> sets M"
-  shows "{x \<in> space M. if x \<in> A then P x else Q x} \<in> sets M"
-proof -
-  have *: "{x \<in> space M. if x \<in> A then P x else Q x} = 
-    {x \<in> space M. if x \<in> A \<inter> space M then P x else Q x}" by auto
-  show ?thesis unfolding * unfolding if_bool_eq_conj using assms
-    by (auto intro!: sets_Collect simp: Int_def conj_commute)
-qed
-
 lemma set_Collect_ereal2:
   fixes f g :: "'a \<Rightarrow> ereal" 
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   assumes H: "{x \<in> space M. H (ereal (real (f x))) (ereal (real (g x)))} \<in> sets M"
-    "{x \<in> space M. H (-\<infinity>) (ereal (real (g x)))} \<in> sets M"
-    "{x \<in> space M. H (\<infinity>) (ereal (real (g x)))} \<in> sets M"
-    "{x \<in> space M. H (ereal (real (f x))) (-\<infinity>)} \<in> sets M"
-    "{x \<in> space M. H (ereal (real (f x))) (\<infinity>)} \<in> sets M"
+    "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel"
+    "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel"
+    "{x \<in> space borel. H (ereal x) (-\<infinity>)} \<in> sets borel"
+    "{x \<in> space borel. H (ereal x) (\<infinity>)} \<in> sets borel"
   shows "{x \<in> space M. H (f x) (g x)} \<in> sets M"
 proof -
-  let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
-  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
+  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = -\<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
+  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = -\<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
-  moreover 
-  have "{x \<in> space M. ?F x} \<in> sets M"
-    by (intro sets_Collect H measurable_sets[OF f] measurable_sets[OF g] sets_Collect_If_set) auto
-  ultimately
-  show ?thesis by simp
+  note * = this
+  from assms show ?thesis
+    by (subst *) (simp del: space_borel split del: split_if)
 qed
 
 lemma
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
-  shows borel_measurable_ereal_le[intro,simp]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
-    and borel_measurable_ereal_less[intro,simp]: "{x \<in> space M. f x < g x} \<in> sets M"
-    and borel_measurable_ereal_eq[intro,simp]: "{w \<in> space M. f w = g w} \<in> sets M"
+  shows borel_measurable_ereal_le[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
+    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
+    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
     and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
 
@@ -1060,7 +998,7 @@
   have "?f \<in> borel_measurable M" using * ** by (intro measurable_If) auto
   also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
   finally show "f \<in> borel_measurable M" .
-qed (auto intro: measurable_sets borel_measurable_real_of_ereal)
+qed simp_all
 
 lemma borel_measurable_eq_atMost_ereal:
   fixes f :: "'a \<Rightarrow> ereal"
@@ -1080,7 +1018,8 @@
       qed }
     then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
       by (auto simp: not_le)
-    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
+    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
+      by (auto simp del: UN_simps)
     moreover
     have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
     then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
@@ -1150,14 +1089,11 @@
     "(\<lambda>x. H (ereal (real (f x))) (\<infinity>)) \<in> borel_measurable M"
   shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
 proof -
-  let ?G = "\<lambda>y x. if x \<in> g -` {\<infinity>} then H y \<infinity> else if x \<in> g -` {-\<infinity>} then H y (-\<infinity>) else H y (ereal (real (g x)))"
-  let ?F = "\<lambda>x. if x \<in> f -` {\<infinity>} then ?G \<infinity> x else if x \<in> f -` {-\<infinity>} then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
+  let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = - \<infinity> then H y (-\<infinity>) else H y (ereal (real (g x)))"
+  let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = - \<infinity> then ?G (-\<infinity>) x else ?G (ereal (real (f x))) x"
   { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
-  moreover 
-  have "?F \<in> borel_measurable M"
-    by (intro measurable_If_set measurable_sets[OF f] measurable_sets[OF g] H) auto
-  ultimately
-  show ?thesis by simp
+  note * = this
+  from assms show ?thesis unfolding * by simp
 qed
 
 lemma
@@ -1166,29 +1102,24 @@
     and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
   using f by auto
 
-lemma split_sets:
-  "{x\<in>space M. P x \<or> Q x} = {x\<in>space M. P x} \<union> {x\<in>space M. Q x}"
-  "{x\<in>space M. P x \<and> Q x} = {x\<in>space M. P x} \<inter> {x\<in>space M. Q x}"
-  by auto
-
-lemma
+lemma [intro, simp, measurable(raw)]:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows borel_measurable_ereal_add[intro, simp]: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
-    and borel_measurable_ereal_times[intro, simp]: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-    and borel_measurable_ereal_min[simp, intro]: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
-    and borel_measurable_ereal_max[simp, intro]: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
+  shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
+    and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
+    and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
+    and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
   by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
 
-lemma
+lemma [simp, intro, measurable(raw)]:
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
-  shows borel_measurable_ereal_diff[simp, intro]: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-    and borel_measurable_ereal_divide[simp, intro]: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+  shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
+    and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
   unfolding minus_ereal_def divide_ereal_def using assms by auto
 
-lemma borel_measurable_ereal_setsum[simp, intro]:
+lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1198,7 +1129,7 @@
     by induct auto
 qed simp
 
-lemma borel_measurable_ereal_setprod[simp, intro]:
+lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1207,7 +1138,7 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_SUP[simp, intro]:
+lemma borel_measurable_SUP[simp, intro,measurable (raw)]:
   fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
@@ -1220,7 +1151,7 @@
     using assms by auto
 qed
 
-lemma borel_measurable_INF[simp, intro]:
+lemma borel_measurable_INF[simp, intro,measurable (raw)]:
   fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
@@ -1233,11 +1164,11 @@
     using assms by auto
 qed
 
-lemma
+lemma [simp, intro, measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M"
-  shows borel_measurable_liminf[simp, intro]: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
-    and borel_measurable_limsup[simp, intro]: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
+  shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
+    and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
 
 lemma borel_measurable_ereal_LIMSEQ:
@@ -1251,7 +1182,7 @@
   then show ?thesis by (simp add: u cong: measurable_cong)
 qed
 
-lemma borel_measurable_psuminf[simp, intro]:
+lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
   shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
@@ -1275,38 +1206,38 @@
   ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
 qed
 
-lemma sets_Collect_Cauchy: 
+lemma sets_Collect_Cauchy[measurable]: 
   fixes f :: "nat \<Rightarrow> 'a => real"
-  assumes f: "\<And>i. f i \<in> borel_measurable M"
+  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
-  unfolding Cauchy_iff2 using f by (auto intro!: sets_Collect)
+  unfolding Cauchy_iff2 using f by auto
 
-lemma borel_measurable_lim:
+lemma borel_measurable_lim[measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
-  assumes f: "\<And>i. f i \<in> borel_measurable M"
+  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
 proof -
-  have *: "\<And>x. lim (\<lambda>i. f i x) =
-    (if Cauchy (\<lambda>i. f i x) then lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) else (THE x. False))"
+  def u' \<equiv> "\<lambda>x. lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
+  then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
     by (auto simp: lim_def convergent_eq_cauchy[symmetric])
-  { fix x have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
+  have "u' \<in> borel_measurable M"
+  proof (rule borel_measurable_LIMSEQ)
+    fix x
+    have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
       by (cases "Cauchy (\<lambda>i. f i x)")
-         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def) }
-  note convergent = this
-  show ?thesis
-    unfolding *
-    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
-    apply (rule borel_measurable_LIMSEQ)
-    apply (rule convergent_LIMSEQ_iff[THEN iffD1, OF convergent])
-    apply (intro measurable_If sets_Collect_Cauchy f borel_measurable_const)
-    done
+         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
+    then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) ----> u' x"
+      unfolding u'_def 
+      by (rule convergent_LIMSEQ_iff[THEN iffD1])
+  qed measurable
+  then show ?thesis
+    unfolding * by measurable
 qed
 
-lemma borel_measurable_suminf:
+lemma borel_measurable_suminf[measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
-  assumes f: "\<And>i. f i \<in> borel_measurable M"
+  assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
-  unfolding suminf_def sums_def[abs_def] lim_def[symmetric]
-  by (simp add: f borel_measurable_lim)
+  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
 end 
diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -446,7 +446,7 @@
   shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
   using assms unfolding finite_entropy_def
   using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
-  by (auto intro: distributed_real_measurable)
+  by (auto dest!: distributed_real_measurable)
 
 subsection {* Mutual Information *}
 
@@ -1578,7 +1578,7 @@
   have "random_variable (count_space (X ` space M)) X"
     by (simp add: comp_def)
   then have "simple_function M X"    
-    unfolding simple_function_def by auto
+    unfolding simple_function_def by (auto simp: measurable_count_space_eq2)
   then have "simple_distributed M X ?Px"
     by (rule simple_distributedI) auto
   then show "distributed M (count_space (X ` space M)) X ?Px"
diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -70,7 +70,7 @@
   have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
   also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
   finally show "g -` X \<inter> space M \<in> sets M" using assms
-    by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def)
+    by (auto simp del: UN_simps simp: simple_function_def)
 qed
 
 lemma simple_function_measurable2[intro]:
@@ -167,7 +167,7 @@
     (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
   show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
     using assms unfolding simple_function_def *
-    by (rule_tac finite_UN) (auto intro!: finite_UN)
+    by (rule_tac finite_UN) auto
 qed
 
 lemma simple_function_indicator[intro, simp]:
@@ -1210,7 +1210,7 @@
     case (insert i P)
     then have "f i \<in> borel_measurable M" "AE x in M. 0 \<le> f i x"
       "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x in M. 0 \<le> (\<Sum>i\<in>P. f i x)"
-      by (auto intro!: borel_measurable_ereal_setsum setsum_nonneg)
+      by (auto intro!: setsum_nonneg)
     from positive_integral_add[OF this]
     show ?case using insert by auto
   qed simp
@@ -1230,7 +1230,7 @@
       simp: indicator_def ereal_zero_le_0_iff)
   also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
     using assms
-    by (auto intro!: positive_integral_cmult borel_measurable_indicator simp: ereal_zero_le_0_iff)
+    by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff)
   finally show ?thesis .
 qed
 
@@ -1633,7 +1633,7 @@
 lemma integral_zero[simp, intro]:
   shows "integrable M (\<lambda>x. 0)" "(\<integral> x.0 \<partial>M) = 0"
   unfolding integrable_def lebesgue_integral_def
-  by (auto simp add: borel_measurable_const)
+  by auto
 
 lemma integral_cmult[simp, intro]:
   assumes "integrable M f"
@@ -1644,7 +1644,7 @@
   proof (cases rule: le_cases)
     assume "0 \<le> a" show ?thesis
       using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
-      by (simp add: integral_zero)
+      by simp
   next
     assume "a \<le> 0" hence "0 \<le> - a" by auto
     have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
@@ -1718,7 +1718,7 @@
     by (auto split: split_indicator simp: positive_integral_0_iff_AE one_ereal_def)
   show ?int ?able
     using assms unfolding lebesgue_integral_def integrable_def
-    by (auto simp: * positive_integral_indicator borel_measurable_indicator)
+    by (auto simp: *)
 qed
 
 lemma integral_cmul_indicator:
@@ -1850,7 +1850,7 @@
   assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
   shows "0 \<le> integral\<^isup>L M f"
 proof -
-  have "0 = (\<integral>x. 0 \<partial>M)" by (auto simp: integral_zero)
+  have "0 = (\<integral>x. 0 \<partial>M)" by auto
   also have "\<dots> \<le> integral\<^isup>L M f"
     using assms by (rule integral_mono[OF integral_zero(1)])
   finally show ?thesis .
@@ -2206,7 +2206,7 @@
     let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
     let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
     have "\<And>n. integrable M (?F n)"
-      using borel by (auto intro!: integral_setsum integrable_abs)
+      using borel by (auto intro!: integrable_abs)
     thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
     show "AE x in M. mono (\<lambda>n. ?w' n x)"
       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
@@ -2436,7 +2436,7 @@
   by (subst density_max_0) (auto intro!: arg_cong[where f="density M"] split: split_max)
 
 lemma emeasure_density:
-  assumes f: "f \<in> borel_measurable M" and A: "A \<in> sets M"
+  assumes f[measurable]: "f \<in> borel_measurable M" and A[measurable]: "A \<in> sets M"
   shows "emeasure (density M f) A = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
     (is "_ = ?\<mu> A")
   unfolding density_def
@@ -2453,8 +2453,9 @@
     unfolding \<mu>_eq
   proof (intro countably_additiveI)
     fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
+    then have "\<And>i. A i \<in> sets M" by auto
     then have *: "\<And>i. (\<lambda>x. max 0 (f x) * indicator (A i) x) \<in> borel_measurable M"
-      using f by (auto intro!: borel_measurable_ereal_times)
+      by (auto simp: set_eq_iff)
     assume disj: "disjoint_family A"
     have "(\<Sum>n. ?\<mu>' (A n)) = (\<integral>\<^isup>+ x. (\<Sum>n. max 0 (f x) * indicator (A n) x) \<partial>M)"
       using f * by (simp add: positive_integral_suminf)
@@ -2483,8 +2484,7 @@
       by (intro positive_integral_0_iff) auto
     also have "\<dots> \<longleftrightarrow> (AE x in M. max 0 (f x) * indicator A x = 0)"
       using f `A \<in> sets M`
-      by (intro AE_iff_measurable[OF _ refl, symmetric])
-         (auto intro!: sets_Collect borel_measurable_ereal_eq)
+      by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
     also have "(AE x in M. max 0 (f x) * indicator A x = 0) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)"
       by (auto simp add: indicator_def max_def split: split_if_asm)
     finally have "(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)" . }
@@ -2649,7 +2649,7 @@
   "finite A \<Longrightarrow>
    g \<in> measurable M (point_measure A f) \<longleftrightarrow>
     (g \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. g -` {a} \<inter> space M \<in> sets M))"
-  unfolding point_measure_def by simp
+  unfolding point_measure_def by (simp add: measurable_count_space_eq2)
 
 lemma simple_function_point_measure[simp]:
   "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)"
diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -447,14 +447,14 @@
 
 lemma emeasure_Diff:
   assumes finite: "emeasure M B \<noteq> \<infinity>"
-  and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
+  and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
   shows "emeasure M (A - B) = emeasure M A - emeasure M B"
 proof -
   have "0 \<le> emeasure M B" using assms by auto
   have "(A - B) \<union> B = A" using `B \<subseteq> A` by auto
   then have "emeasure M A = emeasure M ((A - B) \<union> B)" by simp
   also have "\<dots> = emeasure M (A - B) + emeasure M B"
-    using measurable by (subst plus_emeasure[symmetric]) auto
+    by (subst plus_emeasure[symmetric]) auto
   finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
     unfolding ereal_eq_minus_iff
     using finite `0 \<le> emeasure M B` by auto
@@ -519,12 +519,11 @@
   using INF_emeasure_decseq[OF A fin] by simp
 
 lemma emeasure_subadditive:
-  assumes measurable: "A \<in> sets M" "B \<in> sets M"
+  assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
   shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
 proof -
   from plus_emeasure[of A M "B - A"]
-  have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
-    using assms by (simp add: Diff)
+  have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)" by simp
   also have "\<dots> \<le> emeasure M A + emeasure M B"
     using assms by (auto intro!: add_left_mono emeasure_mono)
   finally show ?thesis .
@@ -538,7 +537,7 @@
   then have "emeasure M (\<Union>i\<in>insert i I. A i) = emeasure M (A i \<union> (\<Union>i\<in>I. A i))"
     by simp
   also have "\<dots> \<le> emeasure M (A i) + emeasure M (\<Union>i\<in>I. A i)"
-    using insert by (intro emeasure_subadditive finite_UN) auto
+    using insert by (intro emeasure_subadditive) auto
   also have "\<dots> \<le> emeasure M (A i) + (\<Sum>i\<in>I. emeasure M (A i))"
     using insert by (intro add_mono) auto
   also have "\<dots> = (\<Sum>i\<in>insert i I. emeasure M (A i))"
@@ -688,18 +687,17 @@
       by (auto simp: subset_eq)
     have "disjoint_family ?D"
       by (auto simp: disjoint_family_disjointed)
-     moreover
-    { fix i
+    moreover
+    have "(\<Sum>i. emeasure M (?D i)) = (\<Sum>i. emeasure N (?D i))"
+    proof (intro arg_cong[where f=suminf] ext)
+      fix i
       have "A i \<inter> ?D i = ?D i"
         by (auto simp: disjointed_def)
-      then have "emeasure M (?D i) = emeasure N (?D i)"
-        using *[of "A i" "?D i", OF _ A(3)] A(1) by auto }
-     ultimately show "emeasure M F = emeasure N F"
-      using N M
-      apply (subst (1 2) F_eq)
-      apply (subst (1 2) suminf_emeasure[symmetric])
-      apply auto
-      done
+      then show "emeasure M (?D i) = emeasure N (?D i)"
+        using *[of "A i" "?D i", OF _ A(3)] A(1) by auto
+    qed
+    ultimately show "emeasure M F = emeasure N F"
+      by (simp add: image_subset_iff `sets M = sets N`[symmetric] F_eq[symmetric] suminf_emeasure)
   qed
 qed
 
@@ -1112,32 +1110,23 @@
 qed
 
 lemma AE_distr_iff:
-  assumes f: "f \<in> measurable M N" and P: "{x \<in> space N. P x} \<in> sets N"
+  assumes f[measurable]: "f \<in> measurable M N" and P[measurable]: "{x \<in> space N. P x} \<in> sets N"
   shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
 proof (subst (1 2) AE_iff_measurable[OF _ refl])
-  from P show "{x \<in> space (distr M N f). \<not> P x} \<in> sets (distr M N f)"
-    by (auto intro!: sets_Collect_neg)
-  moreover
-  have "f -` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}"
-    using f by (auto dest: measurable_space)
-  then show "{x \<in> space M. \<not> P (f x)} \<in> sets M"
-    using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg)
-  moreover have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
-    using f by (auto dest: measurable_space)
-  ultimately show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
+  have "f -` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}"
+    using f[THEN measurable_space] by auto
+  then show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) =
     (emeasure M {x \<in> space M. \<not> P (f x)} = 0)"
-    using f by (simp add: emeasure_distr)
-qed
+    by (simp add: emeasure_distr)
+qed auto
 
 lemma null_sets_distr_iff:
   "f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
-  by (auto simp add: null_sets_def emeasure_distr measurable_sets)
+  by (auto simp add: null_sets_def emeasure_distr)
 
 lemma distr_distr:
-  assumes f: "g \<in> measurable N L" and g: "f \<in> measurable M N"
-  shows "distr (distr M N f) L g = distr M L (g \<circ> f)" (is "?L = ?R")
-  using measurable_comp[OF g f] f g
-  by (auto simp add: emeasure_distr measurable_sets measurable_space
+  "g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
+  by (auto simp add: emeasure_distr measurable_space
            intro!: arg_cong[where f="emeasure M"] measure_eqI)
 
 section {* Real measure values *}
@@ -1381,33 +1370,6 @@
 
 section {* Counting space *}
 
-definition count_space :: "'a set \<Rightarrow> 'a measure" where
-  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
-
-lemma 
-  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
-    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
-  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
-  by (auto simp: count_space_def)
-
-lemma measurable_count_space_eq1[simp]:
-  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
- unfolding measurable_def by simp
-
-lemma measurable_count_space_eq2[simp]:
-  assumes "finite A"
-  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
-proof -
-  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
-    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
-      by (auto dest: finite_subset)
-    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
-    ultimately have "f -` X \<inter> space M \<in> sets M"
-      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
-  then show ?thesis
-    unfolding measurable_def by auto
-qed
-
 lemma strict_monoI_Suc:
   assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
   unfolding strict_mono_def
diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -876,7 +876,7 @@
     then have "a \<notin> X`space M \<Longrightarrow> X -` {a} \<inter> space M = {}" by auto
     with A a X have "emeasure (distr M S X) {a} = P' a"
       by (subst emeasure_distr)
-         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure
+         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
                intro!: arg_cong[where f=prob])
     also have "\<dots> = (\<integral>\<^isup>+x. ereal (P' a) * indicator {a} x \<partial>S)"
       using A X a
@@ -934,7 +934,7 @@
 lemma simple_distributed_simple_function:
   "simple_distributed M X Px \<Longrightarrow> simple_function M X"
   unfolding simple_distributed_def distributed_def
-  by (auto simp: simple_function_def)
+  by (auto simp: simple_function_def measurable_count_space_eq2)
 
 lemma simple_distributed_measure:
   "simple_distributed M X P \<Longrightarrow> a \<in> X`space M \<Longrightarrow> P a = measure M (X -` {a} \<inter> space M)"
diff -r 382bd3173584 -r ce0d316b5b44 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:00:39 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 02 14:23:40 2012 +0100
@@ -100,7 +100,7 @@
   with assms show ?thesis by auto
 qed
 
-lemma (in semiring_of_sets) sets_Collect_finite_All:
+lemma (in semiring_of_sets) sets_Collect_finite_All':
   assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" "S \<noteq> {}"
   shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
 proof -
@@ -1209,6 +1209,15 @@
   "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
    unfolding measurable_def by auto
 
+lemma measurable_sets_Collect:
+  assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M"
+proof -
+  have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}"
+    using measurable_space[OF f] by auto
+  with measurable_sets[OF f P] show ?thesis
+    by simp
+qed
+
 lemma measurable_sigma_sets:
   assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>"
       and f: "f \<in> space M \<rightarrow> \<Omega>"
@@ -1302,6 +1311,9 @@
 lemma measurable_ident[intro, simp]: "id \<in> measurable M M"
   by (auto simp add: measurable_def)
 
+lemma measurable_ident'[intro, simp]: "(\<lambda>x. x) \<in> measurable M M"
+  by (auto simp add: measurable_def)
+
 lemma measurable_comp[intro]:
   fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
   shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
@@ -1314,7 +1326,7 @@
   "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> (\<lambda>x. g (f x)) \<in> measurable M L"
   using measurable_comp[of f M N g L] by (simp add: comp_def)
 
-lemma measurable_Least:
+lemma sets_Least:
   assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
   shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
 proof -
@@ -1371,6 +1383,368 @@
     measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
   using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
 
+section {* Counting space *}
+
+definition count_space :: "'a set \<Rightarrow> 'a measure" where
+  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
+
+lemma 
+  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
+    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
+  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
+  by (auto simp: count_space_def)
+
+lemma measurable_count_space_eq1[simp]:
+  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
+ unfolding measurable_def by simp
+
+lemma measurable_count_space_eq2:
+  assumes "finite A"
+  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
+proof -
+  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
+    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
+      by (auto dest: finite_subset)
+    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
+    ultimately have "f -` X \<inter> space M \<in> sets M"
+      using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
+  then show ?thesis
+    unfolding measurable_def by auto
+qed
+
+lemma measurable_compose_countable:
+  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
+  shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
+  unfolding measurable_def
+proof safe
+  fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
+    using f[THEN measurable_space] g[THEN measurable_space] by auto
+next
+  fix A assume A: "A \<in> sets N"
+  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
+    by auto
+  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
+    by (auto intro!: countable_UN measurable_sets)
+  finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
+qed
+
+subsection {* Measurable method *}
+
+lemma (in algebra) sets_Collect_finite_All:
+  assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
+  shows "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} \<in> M"
+proof -
+  have "{x\<in>\<Omega>. \<forall>i\<in>S. P i x} = (if S = {} then \<Omega> else \<Inter>i\<in>S. {x\<in>\<Omega>. P i x})"
+    by auto
+  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
+qed
+
+abbreviation "pred M P \<equiv> P \<in> measurable M (count_space (UNIV::bool set))"
+
+lemma pred_def: "pred M P \<longleftrightarrow> {x\<in>space M. P x} \<in> sets M"
+proof
+  assume "pred M P"
+  then have "P -` {True} \<inter> space M \<in> sets M"
+    by (auto simp: measurable_count_space_eq2)
+  also have "P -` {True} \<inter> space M = {x\<in>space M. P x}" by auto
+  finally show "{x\<in>space M. P x} \<in> sets M" .
+next
+  assume P: "{x\<in>space M. P x} \<in> sets M"
+  moreover
+  { fix X
+    have "X \<in> Pow (UNIV :: bool set)" by simp
+    then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
+      unfolding UNIV_bool Pow_insert Pow_empty by auto
+    then have "P -` X \<inter> space M \<in> sets M"
+      by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
+  then show "pred M P"
+    by (auto simp: measurable_def)
+qed
+
+lemma pred_sets1: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> f \<in> measurable N M \<Longrightarrow> pred N (\<lambda>x. P (f x))"
+  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)
+
+lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
+  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
+
+lemma measurable_count_space_const:
+  "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
+  by auto
+
+lemma measurable_count_space:
+  "f \<in> measurable (count_space A) (count_space UNIV)"
+  by simp
+
+lemma measurable_compose_rev:
+  assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
+  shows "(\<lambda>x. f (g x)) \<in> measurable M N"
+  using measurable_compose[OF g f] .
+
+ML {*
+
+structure Measurable =
+struct
+
+datatype level = Concrete | Generic;
+
+structure Data = Generic_Data
+(
+  type T = thm list * thm list;
+  val empty = ([], []);
+  val extend = I;
+  val merge = fn ((a, b), (c, d)) => (a @ c, b @ d);
+);
+
+val debug =
+  Attrib.setup_config_bool @{binding measurable_debug} (K false)
+
+val backtrack =
+  Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
+
+fun get lv = (case lv of Concrete => fst | Generic => snd) o Data.get o Context.Proof; 
+fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
+
+fun update f lv = Data.map (case lv of Concrete => apfst f | Generic => apsnd f);
+fun add thms' = update (fn thms => thms @ thms');
+
+fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
+
+fun is_too_generic thm =
+  let 
+    val concl = concl_of thm
+    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
+  in is_Var (head_of concl') end
+
+fun import_theorem thm = if is_too_generic thm then [] else
+  [thm] @ map_filter (try (fn th' => thm RS th'))
+    [@{thm measurable_compose_rev}, @{thm pred_sets1}, @{thm pred_sets2}, @{thm sets_into_space}];
+
+fun add_thm (raw, lv) thm = add (if raw then [thm] else import_theorem thm) lv;
+
+fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
+
+fun TAKE n f thm = Seq.take n (f thm)
+
+fun nth_hol_goal thm i =
+  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
+
+fun dest_measurable_fun t =
+  (case t of
+    (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
+  | _ => raise (TERM ("not a measurability predicate", [t])))
+
+fun indep (Bound i) t b = i < b orelse t <= i
+  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
+  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
+  | indep _ _ _ = true;
+
+fun cnt_prefixes ctxt (Abs (n, T, t)) = let
+      fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+      fun cnt_walk (Abs (ns, T, t)) Ts =
+          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
+        | cnt_walk (f $ g) Ts = let
+            val n = length Ts - 1
+          in
+            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
+            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
+            (if is_countable (fastype_of1 (Ts, g)) andalso loose_bvar1 (g, n)
+                andalso indep g n 0 andalso g <> Bound n
+              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
+              else [])
+          end
+        | cnt_walk _ _ = []
+    in map (fn (t1, t2) => let
+        val T1 = fastype_of1 ([T], t2)
+        val T2 = fastype_of1 ([T], t)
+      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
+        [SOME T1, SOME T, SOME T2])
+      end) (cnt_walk t [T])
+    end
+  | cnt_prefixes _ _ = []
+
+val split_fun_tac =
+  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+    let
+      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
+      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
+      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
+      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
+    in if null cps then no_tac else debug_tac ctxt (K "split fun") (resolve_tac cps) i end
+    handle TERM _ => no_tac) 1)
+
+fun single_measurable_tac ctxt facts =
+  debug_tac ctxt (fn () => "single + " ^ Pretty.str_of (Pretty.block (map (Syntax.pretty_term ctxt o prop_of) facts)))
+  (resolve_tac ((maps (import_theorem o Simplifier.norm_hhf) facts) @ get_all ctxt)
+    APPEND' (split_fun_tac ctxt));
+
+fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
+  (case nth_hol_goal thm n of
+    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
+  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
+  | _ => true)
+  handle TERM _ => true;
+
+fun measurable_tac' ctxt ss facts n =
+  TAKE (Config.get ctxt backtrack)
+  ((single_measurable_tac ctxt facts THEN'
+   REPEAT o (single_measurable_tac ctxt facts APPEND'
+             SOLVED' (fn n => COND (is_cond_formlua n) (debug_tac ctxt (K "simp") (asm_full_simp_tac ss) n) no_tac))) n);
+
+fun measurable_tac ctxt = measurable_tac' ctxt (simpset_of ctxt);
+
+val attr_add = Thm.declaration_attribute o add_thm;
+
+val attr : attribute context_parser =
+  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
+
+val method : (Proof.context -> Method.method) context_parser =
+  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
+
+fun simproc ss redex = let
+    val ctxt = Simplifier.the_context ss;
+    val t = HOLogic.mk_Trueprop (term_of redex);
+    fun tac {context = ctxt, ...} =
+      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss) 1);
+  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
+
+end
+
+*}
+
+attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
+method_setup measurable = {* Measurable.method *} "measurability prover"
+simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
+
+declare
+  top[measurable]
+  empty_sets[measurable (raw)]
+  Un[measurable (raw)]
+  Diff[measurable (raw)]
+
+declare
+  measurable_count_space[measurable (raw)]
+  measurable_ident[measurable (raw)]
+  measurable_ident'[measurable (raw)]
+  measurable_count_space_const[measurable (raw)]
+  measurable_const[measurable (raw)]
+  measurable_If[measurable (raw)]
+  measurable_comp[measurable (raw)]
+  measurable_sets[measurable (raw)]
+
+lemma predE[measurable (raw)]: 
+  "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
+  unfolding pred_def .
+
+lemma pred_intros_imp'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<longrightarrow> P x)"
+  by (cases K) auto
+
+lemma pred_intros_conj1'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<and> P x)"
+  by (cases K) auto
+
+lemma pred_intros_conj2'[measurable (raw)]:
+  "(K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<and> K)"
+  by (cases K) auto
+
+lemma pred_intros_disj1'[measurable (raw)]:
+  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. K \<or> P x)"
+  by (cases K) auto
+
+lemma pred_intros_disj2'[measurable (raw)]:
+  "(\<not> K \<Longrightarrow> pred M (\<lambda>x. P x)) \<Longrightarrow> pred M (\<lambda>x. P x \<or> K)"
+  by (cases K) auto
+
+lemma pred_intros_logic[measurable (raw)]:
+  "pred M (\<lambda>x. x \<in> space M)"
+  "pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. \<not> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<and> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<longrightarrow> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x \<or> P x)"
+  "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
+  "pred M (\<lambda>x. f x \<in> UNIV)"
+  "pred M (\<lambda>x. f x \<in> {})"
+  "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
+  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
+  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
+  "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<union> (B x))"
+  "pred M (\<lambda>x. g x (f x) \<in> (X x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (g x) -` (X x))"
+  by (auto intro!: sets_Collect simp: iff_conv_conj_imp pred_def)
+
+lemma pred_intros_countable[measurable (raw)]:
+  fixes P :: "'a \<Rightarrow> 'i :: countable \<Rightarrow> bool"
+  shows 
+    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
+    "(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
+  by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
+
+lemma pred_intros_countable_bounded[measurable (raw)]:
+  fixes X :: "'i :: countable set"
+  shows 
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>X. N x i))"
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
+    "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
+  by (auto simp: Bex_def Ball_def)
+
+lemma pred_intros_finite[measurable (raw)]:
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
+  by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+
+lemma countable_Un_Int[measurable (raw)]:
+  "(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
+  "I \<noteq> {} \<Longrightarrow> (\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Inter>i\<in>I. N i) \<in> sets M"
+  by auto
+
+declare
+  finite_UN[measurable (raw)]
+  finite_INT[measurable (raw)]
+
+lemma sets_Int_pred[measurable (raw)]:
+  assumes space: "A \<inter> B \<subseteq> space M" and [measurable]: "pred M (\<lambda>x. x \<in> A)" "pred M (\<lambda>x. x \<in> B)"
+  shows "A \<inter> B \<in> sets M"
+proof -
+  have "{x\<in>space M. x \<in> A \<inter> B} \<in> sets M" by auto
+  also have "{x\<in>space M. x \<in> A \<inter> B} = A \<inter> B"
+    using space by auto
+  finally show ?thesis .
+qed
+
+lemma [measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c} \<in> sets N"
+  shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
+    and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
+  using measurable_sets[OF f c] by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_le_const[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_le[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c ..} \<in> sets N" shows "pred M (\<lambda>x. c \<le> f x)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_less_const[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{..< c} \<in> sets N" shows "pred M (\<lambda>x. f x < c)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+lemma pred_const_less[measurable (raw generic)]:
+  assumes f: "f \<in> measurable M N" and c: "{c <..} \<in> sets N" shows "pred M (\<lambda>x. c < f x)"
+  using measurable_sets[OF f c]
+  by (auto simp: Int_def conj_commute eq_commute pred_def)
+
+declare
+  Int[measurable (raw)]
+
+hide_const (open) pred
+
 subsection {* Extend measure *}
 
 definition "extend_measure \<Omega> I G \<mu> =