# HG changeset patch
# User hoelzl
# Date 1417709158 -3600
# Node ID ff2bd4a14ddb3ed49f2b74254478b9f5858a9b0f
# Parent  8535cfcfa4934afa892276adabb08d393a274fa2
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces

diff -r 8535cfcfa493 -r ff2bd4a14ddb src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Dec 04 17:05:58 2014 +0100
@@ -594,6 +594,65 @@
 
 subsection {* Products on counting spaces, densities and distributions *}
 
+lemma sigma_prod:
+  assumes X_cover: "\<exists>E\<subseteq>A. countable E \<and> X = \<Union>E" and A: "A \<subseteq> Pow X"
+  assumes Y_cover: "\<exists>E\<subseteq>B. countable E \<and> Y = \<Union>E" and B: "B \<subseteq> Pow Y"
+  shows "sigma X A \<Otimes>\<^sub>M sigma Y B = sigma (X \<times> Y) {a \<times> b | a b. a \<in> A \<and> b \<in> B}"
+    (is "?P = ?S")
+proof (rule measure_eqI)
+  have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
+    by auto
+  let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
+  have "sets ?P = 
+    sets (\<Squnion>\<^sub>\<sigma> xy\<in>?XY. sigma (X \<times> Y) xy)"
+    by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
+  also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
+    by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto
+  also have "\<dots> = sets ?S"
+  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI) 
+    show "\<Union>?XY \<subseteq> Pow (X \<times> Y)" "{a \<times> b |a b. a \<in> A \<and> b \<in> B} \<subseteq> Pow (X \<times> Y)"
+      using A B by auto
+  next
+    interpret XY: sigma_algebra "X \<times> Y" "sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+      using A B by (intro sigma_algebra_sigma_sets) auto
+    fix Z assume "Z \<in> \<Union>?XY"
+    then show "Z \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+    proof safe
+      fix a assume "a \<in> A"
+      from Y_cover obtain E where E: "E \<subseteq> B" "countable E" and "Y = \<Union>E"
+        by auto
+      with `a \<in> A` A have eq: "fst -` a \<inter> X \<times> Y = (\<Union>e\<in>E. a \<times> e)"
+        by auto
+      show "fst -` a \<inter> X \<times> Y \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+        using `a \<in> A` E unfolding eq by (auto intro!: XY.countable_UN')
+    next
+      fix b assume "b \<in> B"
+      from X_cover obtain E where E: "E \<subseteq> A" "countable E" and "X = \<Union>E"
+        by auto
+      with `b \<in> B` B have eq: "snd -` b \<inter> X \<times> Y = (\<Union>e\<in>E. e \<times> b)"
+        by auto
+      show "snd -` b \<inter> X \<times> Y \<in> sigma_sets (X \<times> Y) {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+        using `b \<in> B` E unfolding eq by (auto intro!: XY.countable_UN')
+    qed
+  next
+    fix Z assume "Z \<in> {a \<times> b |a b. a \<in> A \<and> b \<in> B}"
+    then obtain a b where "Z = a \<times> b" and ab: "a \<in> A" "b \<in> B"
+      by auto
+    then have Z: "Z = (fst -` a \<inter> X \<times> Y) \<inter> (snd -` b \<inter> X \<times> Y)"
+      using A B by auto
+    interpret XY: sigma_algebra "X \<times> Y" "sigma_sets (X \<times> Y) (\<Union>?XY)"
+      by (intro sigma_algebra_sigma_sets) auto
+    show "Z \<in> sigma_sets (X \<times> Y) (\<Union>?XY)"
+      unfolding Z by (rule XY.Int) (blast intro: ab)+
+  qed
+  finally show "sets ?P = sets ?S" .
+next
+  interpret finite_measure "sigma X A" for X A
+    proof qed (simp add: emeasure_sigma)
+  fix A assume "A \<in> sets ?P" then show "emeasure ?P A = emeasure ?S A"
+    by (simp add: emeasure_pair_measure_alt emeasure_sigma)
+qed
+
 lemma sigma_sets_pair_measure_generator_finite:
   assumes "finite A" and "finite B"
   shows "sigma_sets (A \<times> B) { a \<times> b | a b. a \<subseteq> A \<and> b \<subseteq> B} = Pow (A \<times> B)"
@@ -618,6 +677,18 @@
   show "a \<in> A" and "b \<in> B" by auto
 qed
 
+lemma borel_prod:
+  "(borel \<Otimes>\<^sub>M borel) = (borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
+  (is "?P = ?B")
+proof -
+  have "?B = sigma UNIV {A \<times> B | A B. open A \<and> open B}"
+    by (rule second_countable_borel_measurable[OF open_prod_generated])
+  also have "\<dots> = ?P"
+    unfolding borel_def
+    by (subst sigma_prod) (auto intro!: exI[of _ "{UNIV}"])
+  finally show ?thesis ..
+qed
+
 lemma pair_measure_count_space:
   assumes A: "finite A" and B: "finite B"
   shows "count_space A \<Otimes>\<^sub>M count_space B = count_space (A \<times> B)" (is "?P = ?C")
@@ -821,50 +892,6 @@
     by auto
 qed
 
-lemma borel_prod: "sets (borel \<Otimes>\<^sub>M borel) =
-    (sets borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) set set)"
-  (is "?l = ?r")
-proof -
-  obtain A :: "'a set set" where A: "countable A" "topological_basis A"
-    by (metis ex_countable_basis)
-  moreover obtain B :: "'b set set" where B: "countable B" "topological_basis B"
-    by (metis ex_countable_basis)
-  ultimately have AB: "countable ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
-    by (auto intro!: topological_basis_prod)
-  have "sets (borel \<Otimes>\<^sub>M borel) = sigma_sets UNIV {a \<times> b |a b. a \<in> sigma_sets UNIV A \<and> b \<in> sigma_sets UNIV B}"
-    by (simp add: sets_pair_measure
-       borel_eq_countable_basis[OF A] borel_eq_countable_basis[OF B])
-  also have "\<dots> \<supseteq> sigma_sets UNIV ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" (is "... \<supseteq> ?A")
-    by (auto intro!: sigma_sets_mono)
-  also (xtrans) have "?A = sets borel"
-    by (simp add: borel_eq_countable_basis[OF AB])
-  finally have "?r \<subseteq> ?l" .
-  moreover have "?l \<subseteq> ?r"
-  proof (simp add: sets_pair_measure, safe intro!: sigma_sets_mono)
-    fix A::"('a \<times> 'b) set" assume "A \<in> sigma_sets UNIV {a \<times> b |a b. a \<in> sets borel \<and> b \<in> sets borel}"
-    then show "A \<in> sets borel"
-      by (induct A) (auto intro!: borel_Times)
-  qed
-  ultimately show ?thesis by auto
-qed
-
-lemma borel_prod':
-  "borel \<Otimes>\<^sub>M borel = (borel :: 
-      ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
-proof (rule measure_eqI[OF borel_prod])
-  interpret sigma_finite_measure "borel :: 'b measure"
-    proof qed (intro exI[of _ "{UNIV}"], auto simp: borel_def emeasure_sigma)
-  fix X :: "('a \<times> 'b) set" assume asm: "X \<in> sets (borel \<Otimes>\<^sub>M borel)"
-  have "UNIV \<times> UNIV \<in> sets (borel \<Otimes>\<^sub>M borel :: ('a \<times> 'b) measure)" 
-      by (simp add: borel_prod)
-  moreover have "emeasure (borel \<Otimes>\<^sub>M borel) (UNIV \<times> UNIV :: ('a \<times> 'b) set) = 0"
-      by (subst emeasure_pair_measure_Times, simp_all add: borel_def emeasure_sigma)
-  moreover have "X \<subseteq> UNIV \<times> UNIV" by auto
-  ultimately have "emeasure (borel \<Otimes>\<^sub>M borel) X = 0" by (rule emeasure_eq_0)
-  thus "emeasure (borel \<Otimes>\<^sub>M borel) X = emeasure borel X"
-      by (simp add: borel_def emeasure_sigma)
-qed
-
 lemma finite_measure_pair_measure:
   assumes "finite_measure M" "finite_measure N"
   shows "finite_measure (N  \<Otimes>\<^sub>M M)"
diff -r 8535cfcfa493 -r ff2bd4a14ddb src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Dec 04 17:05:58 2014 +0100
@@ -11,6 +11,17 @@
   "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
+lemma topological_basis_trivial: "topological_basis {A. open A}"
+  by (auto simp: topological_basis_def)
+
+lemma open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}"
+proof -
+  have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))"
+    by auto
+  then show ?thesis
+    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)  
+qed
+
 subsection {* Generic Borel spaces *}
 
 definition borel :: "'a::topological_space measure" where
@@ -147,6 +158,50 @@
 lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
   by (auto intro: borel_closed dest!: compact_imp_closed)
 
+lemma second_countable_borel_measurable:
+  fixes X :: "'a::second_countable_topology set set"
+  assumes eq: "open = generate_topology X"
+  shows "borel = sigma UNIV X"
+  unfolding borel_def
+proof (intro sigma_eqI sigma_sets_eqI)
+  interpret X: sigma_algebra UNIV "sigma_sets UNIV X"
+    by (rule sigma_algebra_sigma_sets) simp
+
+  fix S :: "'a set" assume "S \<in> Collect open"
+  then have "generate_topology X S"
+    by (auto simp: eq)
+  then show "S \<in> sigma_sets UNIV X"
+  proof induction
+    case (UN K)
+    then have K: "\<And>k. k \<in> K \<Longrightarrow> open k"
+      unfolding eq by auto
+    from ex_countable_basis obtain B :: "'a set set" where
+      B:  "\<And>b. b \<in> B \<Longrightarrow> open b" "\<And>X. open X \<Longrightarrow> \<exists>b\<subseteq>B. (\<Union>b) = X" and "countable B"
+      by (auto simp: topological_basis_def)
+    from B(2)[OF K] obtain m where m: "\<And>k. k \<in> K \<Longrightarrow> m k \<subseteq> B" "\<And>k. k \<in> K \<Longrightarrow> (\<Union>m k) = k"
+      by metis
+    def U \<equiv> "(\<Union>k\<in>K. m k)"
+    with m have "countable U"
+      by (intro countable_subset[OF _ `countable B`]) auto
+    have "\<Union>U = (\<Union>A\<in>U. A)" by simp
+    also have "\<dots> = \<Union>K"
+      unfolding U_def UN_simps by (simp add: m)
+    finally have "\<Union>U = \<Union>K" .
+
+    have "\<forall>b\<in>U. \<exists>k\<in>K. b \<subseteq> k"
+      using m by (auto simp: U_def)
+    then obtain u where u: "\<And>b. b \<in> U \<Longrightarrow> u b \<in> K" and "\<And>b. b \<in> U \<Longrightarrow> b \<subseteq> u b"
+      by metis
+    then have "(\<Union>b\<in>U. u b) \<subseteq> \<Union>K" "\<Union>U \<subseteq> (\<Union>b\<in>U. u b)"
+      by auto
+    then have "\<Union>K = (\<Union>b\<in>U. u b)"
+      unfolding `\<Union>U = \<Union>K` by auto
+    also have "\<dots> \<in> sigma_sets UNIV X"
+      using u UN by (intro X.countable_UN' `countable U`) auto
+    finally show "\<Union>K \<in> sigma_sets UNIV X" .
+  qed auto
+qed (auto simp: eq intro: generate_topology.Basis)
+
 lemma borel_measurable_continuous_on_if:
   assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
   shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
@@ -261,6 +316,145 @@
     unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
 qed
 
+subsection {* Borel spaces on order topologies *}
+
+
+lemma borel_Iio:
+  "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
+  unfolding second_countable_borel_measurable[OF open_generated_order]
+proof (intro sigma_eqI sigma_sets_eqI)
+  from countable_dense_setE guess D :: "'a set" . note D = this
+
+  interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
+    by (rule sigma_algebra_sigma_sets) simp
+
+  fix A :: "'a set" assume "A \<in> range lessThan \<union> range greaterThan"
+  then obtain y where "A = {y <..} \<or> A = {..< y}"
+    by blast
+  then show "A \<in> sigma_sets UNIV (range lessThan)"
+  proof
+    assume A: "A = {y <..}"
+    show ?thesis
+    proof cases
+      assume "\<forall>x>y. \<exists>d. y < d \<and> d < x"
+      with D(2)[of "{y <..< x}" for x] have "\<forall>x>y. \<exists>d\<in>D. y < d \<and> d < x"
+        by (auto simp: set_eq_iff)
+      then have "A = UNIV - (\<Inter>d\<in>{d\<in>D. y < d}. {..< d})"
+        by (auto simp: A) (metis less_asym)
+      also have "\<dots> \<in> sigma_sets UNIV (range lessThan)"
+        using D(1) by (intro L.Diff L.top L.countable_INT'') auto
+      finally show ?thesis .
+    next
+      assume "\<not> (\<forall>x>y. \<exists>d. y < d \<and> d < x)"
+      then obtain x where "y < x"  "\<And>d. y < d \<Longrightarrow> \<not> d < x"
+        by auto
+      then have "A = UNIV - {..< x}"
+        unfolding A by (auto simp: not_less[symmetric])
+      also have "\<dots> \<in> sigma_sets UNIV (range lessThan)"
+        by auto
+      finally show ?thesis .
+    qed
+  qed auto
+qed auto
+
+lemma borel_Ioi:
+  "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
+  unfolding second_countable_borel_measurable[OF open_generated_order]
+proof (intro sigma_eqI sigma_sets_eqI)
+  from countable_dense_setE guess D :: "'a set" . note D = this
+
+  interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
+    by (rule sigma_algebra_sigma_sets) simp
+
+  fix A :: "'a set" assume "A \<in> range lessThan \<union> range greaterThan"
+  then obtain y where "A = {y <..} \<or> A = {..< y}"
+    by blast
+  then show "A \<in> sigma_sets UNIV (range greaterThan)"
+  proof
+    assume A: "A = {..< y}"
+    show ?thesis
+    proof cases
+      assume "\<forall>x<y. \<exists>d. x < d \<and> d < y"
+      with D(2)[of "{x <..< y}" for x] have "\<forall>x<y. \<exists>d\<in>D. x < d \<and> d < y"
+        by (auto simp: set_eq_iff)
+      then have "A = UNIV - (\<Inter>d\<in>{d\<in>D. d < y}. {d <..})"
+        by (auto simp: A) (metis less_asym)
+      also have "\<dots> \<in> sigma_sets UNIV (range greaterThan)"
+        using D(1) by (intro L.Diff L.top L.countable_INT'') auto
+      finally show ?thesis .
+    next
+      assume "\<not> (\<forall>x<y. \<exists>d. x < d \<and> d < y)"
+      then obtain x where "x < y"  "\<And>d. y > d \<Longrightarrow> x \<ge> d"
+        by (auto simp: not_less[symmetric])
+      then have "A = UNIV - {x <..}"
+        unfolding A Compl_eq_Diff_UNIV[symmetric] by auto
+      also have "\<dots> \<in> sigma_sets UNIV (range greaterThan)"
+        by auto
+      finally show ?thesis .
+    qed
+  qed auto
+qed auto
+
+lemma borel_measurableI_less:
+  fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
+  shows "(\<And>y. {x\<in>space M. f x < y} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
+  unfolding borel_Iio
+  by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
+
+lemma borel_measurableI_greater:
+  fixes f :: "'a \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
+  shows "(\<And>y. {x\<in>space M. y < f x} \<in> sets M) \<Longrightarrow> f \<in> borel_measurable M"
+  unfolding borel_Ioi
+  by (rule measurable_measure_of) (auto simp: Int_def conj_commute)
+
+lemma borel_measurable_SUP[measurable (raw)]:
+  fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
+  assumes [simp]: "countable I"
+  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
+  shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+  by (rule borel_measurableI_greater) (simp add: less_SUP_iff)
+
+lemma borel_measurable_INF[measurable (raw)]:
+  fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
+  assumes [simp]: "countable I"
+  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
+  shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+  by (rule borel_measurableI_less) (simp add: INF_less_iff)
+
+lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
+  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
+  assumes "Order_Continuity.continuous F"
+  assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
+  shows "lfp F \<in> borel_measurable M"
+proof -
+  { fix i have "((F ^^ i) bot) \<in> borel_measurable M"
+      by (induct i) (auto intro!: *) }
+  then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> borel_measurable M"
+    by measurable
+  also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
+    by auto
+  also have "(SUP i. (F ^^ i) bot) = lfp F"
+    by (rule continuous_lfp[symmetric]) fact
+  finally show ?thesis .
+qed
+
+lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
+  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_linorder, linorder_topology, second_countable_topology})"
+  assumes "Order_Continuity.down_continuous F"
+  assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
+  shows "gfp F \<in> borel_measurable M"
+proof -
+  { fix i have "((F ^^ i) top) \<in> borel_measurable M"
+      by (induct i) (auto intro!: * simp: bot_fun_def) }
+  then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> borel_measurable M"
+    by measurable
+  also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
+    by auto
+  also have "\<dots> = gfp F"
+    by (rule down_continuous_gfp[symmetric]) fact
+  finally show ?thesis .
+qed
+
 subsection {* Borel spaces on euclidean spaces *}
 
 lemma borel_measurable_inner[measurable (raw)]:
@@ -1169,32 +1363,6 @@
   thus ?thesis using assms by induct auto
 qed simp
 
-lemma borel_measurable_SUP[measurable (raw)]:
-  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
-  unfolding borel_measurable_ereal_iff_ge
-proof
-  fix a
-  have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
-    by (auto simp: less_SUP_iff)
-  then show "?sup -` {a<..} \<inter> space M \<in> sets M"
-    using assms by auto
-qed
-
-lemma borel_measurable_INF[measurable (raw)]:
-  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
-  unfolding borel_measurable_ereal_iff_less
-proof
-  fix a
-  have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
-    by (auto simp: INF_less_iff)
-  then show "?inf -` {..<a} \<inter> space M \<in> sets M"
-    using assms by auto
-qed
-
 lemma [measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M"
@@ -1325,23 +1493,6 @@
     (\<lambda>x. sup (f x) (g x)::ereal) \<in> borel_measurable M"
   by simp
 
-lemma borel_measurable_lfp[consumes 1, case_names continuity step]:
-  fixes F :: "('a \<Rightarrow> ereal) \<Rightarrow> ('a \<Rightarrow> ereal)"
-  assumes "Order_Continuity.continuous F"
-  assumes *: "\<And>f. f \<in> borel_measurable M \<Longrightarrow> F f \<in> borel_measurable M"
-  shows "lfp F \<in> borel_measurable M"
-proof -
-  { fix i have "((F ^^ i) (\<lambda>t. bot)) \<in> borel_measurable M"
-      by (induct i) (auto intro!: * simp: bot_fun_def) }
-  then have "(\<lambda>x. SUP i. (F ^^ i) (\<lambda>t. bot) x) \<in> borel_measurable M"
-    by measurable
-  also have "(\<lambda>x. SUP i. (F ^^ i) (\<lambda>t. bot) x) = (SUP i. (F ^^ i) bot)"
-    by (auto simp add: bot_fun_def)
-  also have "(SUP i. (F ^^ i) bot) = lfp F"
-    by (rule continuous_lfp[symmetric]) fact
-  finally show ?thesis .
-qed
-
 (* Proof by Jeremy Avigad and Luke Serafin *)
 lemma isCont_borel:
   fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
diff -r 8535cfcfa493 -r ff2bd4a14ddb src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Thu Dec 04 17:05:58 2014 +0100
@@ -1005,7 +1005,7 @@
   then show "f \<in> (\<Union>n. Pi' I (A n))" by auto
 qed (auto simp: Pi'_def `finite I`)
 
-text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *}
+text {* adapted from @{thm sets_PiM_sigma} *}
 
 lemma sigma_fprod_algebra_sigma_eq:
   fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
diff -r 8535cfcfa493 -r ff2bd4a14ddb src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Dec 04 17:05:58 2014 +0100
@@ -362,6 +362,101 @@
   apply (auto intro!: arg_cong2[where f=sigma_sets])
   done
 
+lemma
+  shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
+    and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
+  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
+
+lemma sets_PiM_sigma:
+  assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
+  assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
+  assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
+  defines "P \<equiv> {{f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i} | A j. j \<in> J \<and> A \<in> Pi j E}"
+  shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
+proof cases
+  assume "I = {}" 
+  with `\<Union>J = I` have "P = {{\<lambda>_. undefined}} \<or> P = {}"
+    by (auto simp: P_def)
+  with `I = {}` show ?thesis
+    by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
+next
+  let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
+  assume "I \<noteq> {}"
+  then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) = 
+      sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
+    by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
+  also have "\<dots> = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
+    using E by (intro SUP_sigma_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
+  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
+    using `I \<noteq> {}` by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
+  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
+  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
+    show "(\<Union>i\<in>I. ?F i) \<subseteq> Pow (Pi\<^sub>E I \<Omega>)" "P \<subseteq> Pow (Pi\<^sub>E I \<Omega>)"
+      by (auto simp: P_def)
+  next
+    interpret P: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
+      by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
+
+    fix Z assume "Z \<in> (\<Union>i\<in>I. ?F i)"
+    then obtain i A where i: "i \<in> I" "A \<in> E i" and Z_def: "Z = (\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega>"
+      by auto
+    from `i \<in> I` J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j"
+      by auto
+    obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)"
+      "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)"
+      by (metis subset_eq \<Omega>_cover `j \<subseteq> I`)
+    def A' \<equiv> "\<lambda>n. n(i := A)"
+    then have A'_i: "\<And>n. A' n i = A"
+      by simp
+    { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S"
+      then have "A' n \<in> Pi j E"
+        unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def `A \<in> E i` )
+      with `j \<in> J` have "{f \<in> Pi\<^sub>E I \<Omega>. \<forall>i\<in>j. f i \<in> A' n i} \<in> P"
+        by (auto simp: P_def) }
+    note A'_in_P = this
+
+    { fix x assume "x i \<in> A" "x \<in> Pi\<^sub>E I \<Omega>"
+      with S(3) `j \<subseteq> I` have "\<forall>i\<in>j. \<exists>s\<in>S i. x i \<in> s"
+        by (auto simp: PiE_def Pi_def)
+      then obtain s where s: "\<And>i. i \<in> j \<Longrightarrow> s i \<in> S i" "\<And>i. i \<in> j \<Longrightarrow> x i \<in> s i"
+        by metis
+      with `x i \<in> A` have "\<exists>n\<in>PiE (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
+        by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
+    then have "Z = (\<Union>n\<in>PiE (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
+      unfolding Z_def
+      by (auto simp add: set_eq_iff ball_conj_distrib `i\<in>j` A'_i dest: bspec[OF _ `i\<in>j`]
+               cong: conj_cong)
+    also have "\<dots> \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
+      using `finite j` S(2)
+      by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
+    finally show "Z \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P" .
+  next
+    interpret F: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<Union>i\<in>I. ?F i)"
+      by (auto intro!: sigma_algebra_sigma_sets)
+
+    fix b assume "b \<in> P"
+    then obtain A j where b: "b = {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i}" "j \<in> J" "A \<in> Pi j E"
+      by (auto simp: P_def)
+    show "b \<in> sigma_sets (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i)"
+    proof cases
+      assume "j = {}"
+      with b have "b = (\<Pi>\<^sub>E i\<in>I. \<Omega> i)"
+        by auto
+      then show ?thesis
+        by blast
+    next
+      assume "j \<noteq> {}"
+      with J b(2,3) have eq: "b = (\<Inter>i\<in>j. ((\<lambda>x. x i) -` A i \<inter> Pi\<^sub>E I \<Omega>))"
+        unfolding b(1)
+        by (auto simp: PiE_def Pi_def)
+      show ?thesis
+        unfolding eq using `A \<in> Pi j E` `j \<in> J` J(2)
+        by (intro F.finite_INT J `j \<in> J` `j \<noteq> {}` sigma_sets.Basic) blast
+    qed
+  qed
+  finally show "?thesis" .
+qed
+
 lemma sets_PiM_in_sets:
   assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
@@ -600,11 +695,6 @@
   qed
 qed
 
-lemma
-  shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
-    and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
-  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
-
 lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
 proof -
   let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
@@ -927,116 +1017,6 @@
   "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
   by simp
 
-lemma sigma_prod_algebra_sigma_eq_infinite:
-  fixes E :: "'i \<Rightarrow> 'a set set"
-  assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
-    and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
-  assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
-    and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
-  defines "P == {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> E i}"
-  shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
-proof
-  let ?P = "sigma (space (Pi\<^sub>M I M)) P"
-  have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>M I M))"
-    using E_closed by (auto simp: space_PiM P_def subset_eq)
-  then have space_P: "space ?P = (\<Pi>\<^sub>E i\<in>I. space (M i))"
-    by (simp add: space_PiM)
-  have "sets (PiM I M) =
-      sigma_sets (space ?P) {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
-    using sets_PiM_single[of I M] by (simp add: space_P)
-  also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
-  proof (safe intro!: sets.sigma_sets_subset)
-    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
-    then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
-      apply (subst measurable_iff_measure_of)
-      apply (simp_all add: P_closed)
-      using E_closed
-      apply (force simp: subset_eq space_PiM)
-      apply (force simp: subset_eq space_PiM)
-      apply (auto simp: P_def intro!: sigma_sets.Basic exI[of _ i])
-      apply (rule_tac x=Aa in exI)
-      apply (auto simp: space_PiM)
-      done
-    from measurable_sets[OF this, of A] A `i \<in> I` E_closed
-    have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
-      by (simp add: E_generates)
-    also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A}"
-      using P_closed by (auto simp: space_PiM)
-    finally show "\<dots> \<in> sets ?P" .
-  qed
-  finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
-    by (simp add: P_closed)
-  show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
-    unfolding P_def space_PiM[symmetric]
-    by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
-qed
-
-lemma sigma_prod_algebra_sigma_eq:
-  fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
-  assumes "finite I"
-  assumes S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
-    and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
-  assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
-    and E_generates: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sigma_sets (space (M i)) (E i)"
-  defines "P == { Pi\<^sub>E I F | F. \<forall>i\<in>I. F i \<in> E i }"
-  shows "sets (PiM I M) = sigma_sets (space (PiM I M)) P"
-proof
-  let ?P = "sigma (space (Pi\<^sub>M I M)) P"
-  from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
-  then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
-    by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f)
-  have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>M I M))"
-    using E_closed by (auto simp: space_PiM P_def subset_eq)
-  then have space_P: "space ?P = (\<Pi>\<^sub>E i\<in>I. space (M i))"
-    by (simp add: space_PiM)
-  have "sets (PiM I M) =
-      sigma_sets (space ?P) {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
-    using sets_PiM_single[of I M] by (simp add: space_P)
-  also have "\<dots> \<subseteq> sets (sigma (space (PiM I M)) P)"
-  proof (safe intro!: sets.sigma_sets_subset)
-    fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
-    have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
-    proof (subst measurable_iff_measure_of)
-      show "E i \<subseteq> Pow (space (M i))" using `i \<in> I` by fact
-      from space_P `i \<in> I` show "(\<lambda>x. x i) \<in> space ?P \<rightarrow> space (M i)" by auto
-      show "\<forall>A\<in>E i. (\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
-      proof
-        fix A assume A: "A \<in> E i"
-        then have "(\<lambda>x. x i) -` A \<inter> space ?P = (\<Pi>\<^sub>E j\<in>I. if i = j then A else space (M j))"
-          using E_closed `i \<in> I` by (auto simp: space_P subset_eq split: split_if_asm)
-        also have "\<dots> = (\<Pi>\<^sub>E j\<in>I. \<Union>n. if i = j then A else S j n)"
-          by (intro PiE_cong) (simp add: S_union)
-        also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>\<^sub>E j\<in>I. if i = j then A else S j (xs ! T j))"
-          using T
-          apply (auto simp: PiE_iff bchoice_iff)
-          apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
-          apply (auto simp: bij_betw_def)
-          done
-        also have "\<dots> \<in> sets ?P"
-        proof (safe intro!: sets.countable_UN)
-          fix xs show "(\<Pi>\<^sub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
-            using A S_in_E
-            by (simp add: P_closed)
-               (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
-        qed
-        finally show "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
-          using P_closed by simp
-      qed
-    qed
-    from measurable_sets[OF this, of A] A `i \<in> I` E_closed
-    have "(\<lambda>x. x i) -` A \<inter> space ?P \<in> sets ?P"
-      by (simp add: E_generates)
-    also have "(\<lambda>x. x i) -` A \<inter> space ?P = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A}"
-      using P_closed by (auto simp: space_PiM)
-    finally show "\<dots> \<in> sets ?P" .
-  qed
-  finally show "sets (PiM I M) \<subseteq> sigma_sets (space (PiM I M)) P"
-    by (simp add: P_closed)
-  show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
-    using `finite I`
-    by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
-qed
-
 lemma pair_measure_eq_distr_PiM:
   fixes M1 :: "'a measure" and M2 :: "'a measure"
   assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
diff -r 8535cfcfa493 -r ff2bd4a14ddb src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Thu Dec 04 17:05:58 2014 +0100
@@ -377,105 +377,129 @@
   qed
 qed rule
 
+lemma measurable_pred_countable[measurable (raw)]:
+  assumes "countable X"
+  shows 
+    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
+    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
+  unfolding pred_def
+  by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
+
 subsection {* Measurability for (co)inductive predicates *}
 
+lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
+  by (simp add: bot_fun_def)
+
+lemma measurable_top[measurable]: "top \<in> measurable M (count_space UNIV)"
+  by (simp add: top_fun_def)
+
+lemma measurable_SUP[measurable]:
+  fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
+  assumes [simp]: "countable I"
+  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
+  shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_count_space_eq2_countable
+proof (safe intro!: UNIV_I)
+  fix a 
+  have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M =
+    {x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
+    unfolding SUP_le_iff[symmetric] by auto
+  also have "\<dots> \<in> sets M"
+    by measurable
+  finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+qed
+
+lemma measurable_INF[measurable]:
+  fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
+  assumes [simp]: "countable I"
+  assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
+  shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_count_space_eq2_countable
+proof (safe intro!: UNIV_I)
+  fix a 
+  have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M =
+    {x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
+    unfolding le_INF_iff[symmetric] by auto
+  also have "\<dots> \<in> sets M"
+    by measurable
+  finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+qed
+
+lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
+  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+  assumes "P M"
+  assumes F: "Order_Continuity.continuous F"
+  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
+  shows "lfp F \<in> measurable M (count_space UNIV)"
+proof -
+  { fix i from `P M` have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)"
+      by (induct i arbitrary: M) (auto intro!: *) }
+  then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
+    by measurable
+  also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
+    by (subst continuous_lfp) (auto intro: F)
+  finally show ?thesis .
+qed
+
 lemma measurable_lfp:
-  assumes "Order_Continuity.continuous F"
-  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
-  shows "pred M (lfp F)"
+  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+  assumes F: "Order_Continuity.continuous F"
+  assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
+  shows "lfp F \<in> measurable M (count_space UNIV)"
+  by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)
+
+lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
+  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+  assumes "P M"
+  assumes F: "Order_Continuity.down_continuous F"
+  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
+  shows "gfp F \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
-      by (induct i) (auto intro!: *) }
-  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
+  { fix i from `P M` have "((F ^^ i) top) \<in> measurable M (count_space UNIV)"
+      by (induct i arbitrary: M) (auto intro!: *) }
+  then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
     by measurable
-  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
-    by (auto simp add: bot_fun_def)
-  also have "\<dots> = lfp F"
-    by (rule continuous_lfp[symmetric]) fact
+  also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
+    by (subst down_continuous_gfp) (auto intro: F)
   finally show ?thesis .
 qed
 
 lemma measurable_gfp:
-  assumes "Order_Continuity.down_continuous F"
-  assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
-  shows "pred M (gfp F)"
-proof -
-  { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
-      by (induct i) (auto intro!: *) }
-  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
-    by measurable
-  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
-    by (auto simp add: top_fun_def)
-  also have "\<dots> = gfp F"
-    by (rule down_continuous_gfp[symmetric]) fact
-  finally show ?thesis .
-qed
-
-lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
-  assumes "P M"
-  assumes "Order_Continuity.continuous F"
-  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
-  shows "Measurable.pred M (lfp F)"
-proof -
-  { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
-      by (induct i arbitrary: M) (auto intro!: *) }
-  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x)"
-    by measurable
-  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
-    by (auto simp add: bot_fun_def)
-  also have "\<dots> = lfp F"
-    by (rule continuous_lfp[symmetric]) fact
-  finally show ?thesis .
-qed
-
-lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
-  assumes "P M"
-  assumes "Order_Continuity.down_continuous F"
-  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
-  shows "Measurable.pred M (gfp F)"
-proof -
-  { fix i from `P M` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
-      by (induct i arbitrary: M) (auto intro!: *) }
-  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x)"
-    by measurable
-  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
-    by (auto simp add: top_fun_def)
-  also have "\<dots> = gfp F"
-    by (rule down_continuous_gfp[symmetric]) fact
-  finally show ?thesis .
-qed
+  fixes F :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b::{complete_lattice, countable})"
+  assumes F: "Order_Continuity.down_continuous F"
+  assumes *: "\<And>A. A \<in> measurable M (count_space UNIV) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
+  shows "gfp F \<in> measurable M (count_space UNIV)"
+  by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)
 
 lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
+  fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
   assumes "P M s"
-  assumes "Order_Continuity.continuous F"
-  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> Measurable.pred N (A t)) \<Longrightarrow> Measurable.pred M (F A s)"
-  shows "Measurable.pred M (lfp F s)"
+  assumes F: "Order_Continuity.continuous F"
+  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
+  shows "lfp F s \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. False) s x)"
+  { fix i from `P M s` have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
       by (induct i arbitrary: M s) (auto intro!: *) }
-  then have "Measurable.pred M (\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x)"
+  then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
     by measurable
-  also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>t x. False) s x) = (SUP i. (F ^^ i) bot) s"
-    by (auto simp add: bot_fun_def)
-  also have "(SUP i. (F ^^ i) bot) = lfp F"
-    by (rule continuous_lfp[symmetric]) fact
+  also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
+    by (subst continuous_lfp) (auto simp: F)
   finally show ?thesis .
 qed
 
 lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
+  fixes F :: "('a \<Rightarrow> 'c \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c \<Rightarrow> 'b::{complete_lattice, countable})"
   assumes "P M s"
-  assumes "Order_Continuity.down_continuous F"
-  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> Measurable.pred N (A t)) \<Longrightarrow> Measurable.pred M (F A s)"
-  shows "Measurable.pred M (gfp F s)"
+  assumes F: "Order_Continuity.down_continuous F"
+  assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
+  shows "gfp F s \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. True) s x)"
+  { fix i from `P M s` have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
       by (induct i arbitrary: M s) (auto intro!: *) }
-  then have "Measurable.pred M (\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x)"
+  then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
     by measurable
-  also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>t x. True) s x) = (INF i. (F ^^ i) top) s"
-    by (auto simp add: top_fun_def)
-  also have "(INF i. (F ^^ i) top) = gfp F"
-    by (rule down_continuous_gfp[symmetric]) fact
+  also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
+    by (subst down_continuous_gfp) (auto simp: F)
   finally show ?thesis .
 qed
 
@@ -531,14 +555,6 @@
   qed (simp add: fin)
 qed
 
-lemma measurable_pred_countable[measurable (raw)]:
-  assumes "countable X"
-  shows 
-    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
-    "(\<And>i. i \<in> X \<Longrightarrow> Measurable.pred M (\<lambda>x. P x i)) \<Longrightarrow> Measurable.pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
-  unfolding pred_def
-  by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
-
 lemma measurable_THE:
   fixes P :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   assumes [measurable]: "\<And>i. Measurable.pred M (P i)"
@@ -565,12 +581,6 @@
   finally show "f -` X \<inter> space M \<in> sets M" .
 qed simp
 
-lemma measurable_bot[measurable]: "Measurable.pred M bot"
-  by (simp add: bot_fun_def)
-
-lemma measurable_top[measurable]: "Measurable.pred M top"
-  by (simp add: top_fun_def)
-
 lemma measurable_Ex1[measurable (raw)]:
   assumes [simp]: "countable I" and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> Measurable.pred M (P i)"
   shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)"
diff -r 8535cfcfa493 -r ff2bd4a14ddb src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 03 22:44:24 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 04 17:05:58 2014 +0100
@@ -364,6 +364,9 @@
   finally show ?thesis .
 qed
 
+lemma (in sigma_algebra) countable_INT'':
+  "UNIV \<in> M \<Longrightarrow> countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> M) \<Longrightarrow> (\<Inter>i\<in>I. F i) \<in> M"
+  by (cases "I = {}") (auto intro: countable_INT')
 
 lemma (in sigma_algebra) countable:
   assumes "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> M" "countable A"
@@ -2285,6 +2288,30 @@
     using measurable_space[OF f] M by auto
 qed (auto intro: measurable_sets f dest: sets.sets_into_space)
 
+lemma Sup_sigma_sigma:
+  assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
+  shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sigma \<Omega> (\<Union>M)"
+proof (rule measure_eqI)
+  { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
+    then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
+     by induction (auto intro: sigma_sets.intros) }
+  then show "sets (\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+    apply (simp add: sets_Sup_sigma space_measure_of_conv M Union_least)
+    apply (rule sigma_sets_eqI)
+    apply auto
+    done
+qed (simp add: Sup_sigma_def emeasure_sigma)
+
+lemma SUP_sigma_sigma:
+  assumes M: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>"
+  shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
+proof -
+  have "Sup_sigma (sigma \<Omega> ` f ` M) = sigma \<Omega> (\<Union>(f ` M))"
+    using M by (intro Sup_sigma_sigma) auto
+  then show ?thesis
+    by (simp add: image_image)
+qed
+
 subsection {* The smallest $\sigma$-algebra regarding a function *}
 
 definition
@@ -2332,10 +2359,20 @@
   finally show "g -` A \<inter> space N \<in> sets N" .
 qed (insert g, auto)
 
+lemma vimage_algebra_sigma:
+  assumes X: "X \<subseteq> Pow \<Omega>'" and f: "f \<in> \<Omega> \<rightarrow> \<Omega>'"
+  shows "vimage_algebra \<Omega> f (sigma \<Omega>' X) = sigma \<Omega> {f -` A \<inter> \<Omega> | A. A \<in> X }" (is "?V = ?S")
+proof (rule measure_eqI)
+  have \<Omega>: "{f -` A \<inter> \<Omega> |A. A \<in> X} \<subseteq> Pow \<Omega>" by auto
+  show "sets ?V = sets ?S"
+    using sigma_sets_vimage_commute[OF f, of X]
+    by (simp add: space_measure_of_conv f sets_vimage_algebra2 \<Omega> X)
+qed (simp add: vimage_algebra_def emeasure_sigma)
+
 lemma vimage_algebra_vimage_algebra_eq:
   assumes *: "f \<in> X \<rightarrow> Y" "g \<in> Y \<rightarrow> space M"
   shows "vimage_algebra X f (vimage_algebra Y g M) = vimage_algebra X (\<lambda>x. g (f x)) M"
-  (is "?VV = ?V")
+    (is "?VV = ?V")
 proof (rule measure_eqI)
   have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
     using * by auto