import general theorems from AFP/Markov_Models

--- a/src/HOL/Complex.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Complex.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -132,7 +132,8 @@
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
 
-declare [[coercion complex_of_real]]
+declare [[coercion "of_real :: real \<Rightarrow> complex"]]
+declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
 declare [[coercion "of_int :: int \<Rightarrow> complex"]]
 declare [[coercion "of_nat :: nat \<Rightarrow> complex"]]
 

--- a/src/HOL/Divides.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Divides.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1117,6 +1117,8 @@
   with `n > 0` show ?thesis by simp
 qed
 
+lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
+  by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
 
 subsubsection {* Remainder *}
 

--- a/src/HOL/Hilbert_Choice.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -66,6 +66,9 @@
 lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
 by (blast intro: someI)
 
+lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}"
+  unfolding ex_in_conv[symmetric] by (rule some_eq_ex)
+
 lemma some_eq_trivial [simp]: "(SOME y. y=x) = x"
 apply (rule some_equality)
 apply (rule refl, assumption)

--- a/src/HOL/Int.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Int.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -493,7 +493,6 @@
 apply (rule_tac x="b - Suc a" in exI, arith)
 done
 
-
 subsection {* Cases and induction *}
 
 text{*Now we replace the case analysis rule by a more conventional one:
@@ -817,6 +816,12 @@
   with False show ?thesis by simp
 qed
 
+lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
+  by auto
+
+lemma nat_int_add: "nat (int a + int b) = a + b"
+  by auto
+
 context ring_1
 begin
 

--- a/src/HOL/Lattices_Big.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Lattices_Big.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -764,6 +764,18 @@
   } from this [of "{a. P a}"] assms show ?thesis by simp
 qed
 
+lemma infinite_growing:
+  assumes "X \<noteq> {}"
+  assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
+  shows "\<not> finite X"
+proof
+  assume "finite X"
+  with `X \<noteq> {}` have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
+    by auto
+  with *[of "Max X"] show False
+    by auto
+qed
+
 end
 
 context linordered_ab_semigroup_add

--- a/src/HOL/Library/Extended_Nat.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -135,6 +135,12 @@
 lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n"
   by (simp add: eSuc_def split: enat.splits)
 
+lemma eSuc_enat_iff: "eSuc x = enat y \<longleftrightarrow> (\<exists>n. y = Suc n \<and> x = enat n)"
+  by (cases y) (auto simp: enat_0 eSuc_enat[symmetric])
+
+lemma enat_eSuc_iff: "enat y = eSuc x \<longleftrightarrow> (\<exists>n. y = Suc n \<and> enat n = x)"
+  by (cases y) (auto simp: enat_0 eSuc_enat[symmetric])
+
 subsection {* Addition *}
 
 instantiation enat :: comm_monoid_add

--- a/src/HOL/Library/Extended_Real.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -570,6 +570,108 @@
   using assms
   unfolding incseq_def by (auto intro: setsum_mono)
 
+lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct auto
+next
+  case False
+  then show ?thesis by simp
+qed
+
+lemma setsum_Pinfty:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
+proof safe
+  assume *: "setsum f P = \<infinity>"
+  show "finite P"
+  proof (rule ccontr)
+    assume "\<not> finite P"
+    with * show False
+      by auto
+  qed
+  show "\<exists>i\<in>P. f i = \<infinity>"
+  proof (rule ccontr)
+    assume "\<not> ?thesis"
+    then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
+      by auto
+    with `finite P` have "setsum f P \<noteq> \<infinity>"
+      by induct auto
+    with * show False
+      by auto
+  qed
+next
+  fix i
+  assume "finite P" and "i \<in> P" and "f i = \<infinity>"
+  then show "setsum f P = \<infinity>"
+  proof induct
+    case (insert x A)
+    show ?case using insert by (cases "x = i") auto
+  qed simp
+qed
+
+lemma setsum_Inf:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
+proof
+  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
+  have "finite A"
+    by (rule ccontr) (insert *, auto)
+  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
+  proof (rule ccontr)
+    assume "\<not> ?thesis"
+    then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
+      by auto
+    from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
+    with * show False
+      by auto
+  qed
+  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
+    by auto
+next
+  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
+  then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
+    by auto
+  then show "\<bar>setsum f A\<bar> = \<infinity>"
+  proof induct
+    case (insert j A)
+    then show ?case
+      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
+  qed simp
+qed
+
+lemma setsum_real_of_ereal:
+  fixes f :: "'i \<Rightarrow> ereal"
+  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
+  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
+proof -
+  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
+  proof
+    fix x
+    assume "x \<in> S"
+    from assms[OF this] show "\<exists>r. f x = ereal r"
+      by (cases "f x") auto
+  qed
+  from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
+  then show ?thesis
+    by simp
+qed
+
+lemma setsum_ereal_0:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "finite A"
+    and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
+  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
+proof
+  assume "setsum f A = 0" with assms show "\<forall>i\<in>A. f i = 0"
+  proof (induction A)
+    case (insert a A)
+    then have "f a = 0 \<and> (\<Sum>a\<in>A. f a) = 0"
+      by (subst ereal_add_nonneg_eq_0_iff[symmetric]) (simp_all add: setsum_nonneg)
+    with insert show ?case
+      by simp
+  qed simp
+qed auto
 
 subsubsection "Multiplication"
 
@@ -616,6 +718,9 @@
 
 end
 
+lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
+  by (simp add: one_ereal_def zero_ereal_def)
+
 lemma real_ereal_1[simp]: "real (1::ereal) = 1"
   unfolding one_ereal_def by simp
 
@@ -761,10 +866,10 @@
   shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
   by (cases "c = 0") simp_all
 
-lemma ereal_right_mult_cong:
-  fixes a b c :: ereal
-  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c"
-  by (cases "c = 0") simp_all
+lemma ereal_right_mult_cong: 
+  fixes a b c d :: ereal
+  shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
+  by (cases "d = 0") simp_all
 
 lemma ereal_distrib:
   fixes a b c :: ereal
@@ -781,6 +886,11 @@
   apply (simp only: numeral_inc ereal_plus_1)
   done
 
+lemma setsum_ereal_right_distrib:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
+  by (induct A rule: infinite_finite_induct)  (auto simp: ereal_right_distrib setsum_nonneg)
+
 lemma ereal_le_epsilon:
   fixes x y :: ereal
   assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
@@ -1167,6 +1277,9 @@
 lemma ereal_divide_ereal[simp]: "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
   unfolding divide_ereal_def by simp
 
+lemma ereal_inverse_nonneg_iff: "0 \<le> inverse (x :: ereal) \<longleftrightarrow> 0 \<le> x \<or> x = -\<infinity>"
+  by (cases x) auto
+
 lemma zero_le_divide_ereal[simp]:
   fixes a :: ereal
   assumes "0 \<le> a"
@@ -1229,6 +1342,9 @@
   by (cases rule: ereal3_cases[of a b c])
      (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
 
+lemma ereal_mult_divide: fixes a b :: ereal shows "0 < b \<Longrightarrow> b < \<infinity> \<Longrightarrow> b * (a / b) = a"
+  by (cases a b rule: ereal2_cases) auto
+
 lemma ereal_power_divide:
   fixes x y :: ereal
   shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
@@ -1290,6 +1406,9 @@
   shows "b / c * a = b * a / c"
   by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff mult_less_0_iff)
 
+lemma ereal_times_divide_eq: "a * (b / c :: ereal) = a * b / c"
+  by (cases a b c rule: ereal3_cases)
+     (auto simp: field_simps zero_less_mult_iff)
 
 subsection "Complete lattice"
 
@@ -1653,6 +1772,71 @@
   qed
 qed
 
+lemma SUP_ereal_mult_right:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "I \<noteq> {}"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
+    and "0 \<le> c"
+  shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
+proof (rule SUP_eqI)
+  fix i assume "i \<in> I"
+  then have "f i \<le> SUPREMUM I f"
+    by (rule SUP_upper)
+  then show "c * f i \<le> c * SUPREMUM I f"
+    using `0 \<le> c` by (rule ereal_mult_left_mono)
+next
+  fix y assume *: "\<And>i. i \<in> I \<Longrightarrow> c * f i \<le> y"
+  { assume "c = \<infinity>" have "c * SUPREMUM I f \<le> y"
+    proof cases
+      assume "\<forall>i\<in>I. f i = 0"
+      then show ?thesis
+        using * `c = \<infinity>` by (auto simp: SUP_constant bot_ereal_def)
+    next
+      assume "\<not> (\<forall>i\<in>I. f i = 0)"
+      then obtain i where "f i \<noteq> 0" "i \<in> I"
+        by auto
+      with *[of i] `c = \<infinity>` `i \<in> I \<Longrightarrow> 0 \<le> f i` show ?thesis
+        by (auto split: split_if_asm)
+    qed }
+  moreover
+  { assume "c \<noteq> 0" "c \<noteq> \<infinity>"
+    moreover with `0 \<le> c` * have "SUPREMUM I f \<le> y / c"
+      by (intro SUP_least) (auto simp: ereal_le_divide_pos)
+    ultimately have "c * SUPREMUM I f \<le> y"
+      using `0 \<le> c` * by (auto simp: ereal_le_divide_pos) }
+  moreover { assume "c = 0" with * `I \<noteq> {}` have "c * SUPREMUM I f \<le> y" by auto }
+  ultimately show "c * SUPREMUM I f \<le> y"
+    by blast
+qed
+
+lemma SUP_ereal_add_left:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "I \<noteq> {}"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
+    and "0 \<le> c"
+  shows "(SUP i:I. f i + c) = SUPREMUM I f + c"
+proof (intro SUP_eqI)
+  fix B assume *: "\<And>i. i \<in> I \<Longrightarrow> f i + c \<le> B"
+  show "SUPREMUM I f + c \<le> B"
+  proof cases
+    assume "c = \<infinity>" with `I \<noteq> {}` * show ?thesis
+      by auto
+  next
+    assume "c \<noteq> \<infinity>"
+    with `0 \<le> c` have [simp]: "\<bar>c\<bar> \<noteq> \<infinity>"
+      by simp
+    have "SUPREMUM I f \<le> B - c"
+      by (simp add: SUP_le_iff ereal_le_minus *)
+    then show ?thesis
+      by (simp add: ereal_le_minus)
+  qed
+qed (auto intro: ereal_add_mono SUP_upper)
+
+lemma SUP_ereal_add_right:
+  fixes c :: ereal
+  shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f"
+  using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
+
 lemma SUP_PInfty:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"

--- a/src/HOL/Library/Infinite_Set.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -67,39 +67,14 @@
   infinite.
 *}
 
-lemma finite_nat_bounded:
-  assumes S: "finite (S::nat set)"
-  shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
-  using S
-proof induct
-  have "?bounded {} 0" by simp
-  then show "\<exists>k. ?bounded {} k" ..
-next
-  fix S x
-  assume "\<exists>k. ?bounded S k"
-  then obtain k where k: "?bounded S k" ..
-  show "\<exists>k. ?bounded (insert x S) k"
-  proof (cases "x < k")
-    case True
-    with k show ?thesis by auto
-  next
-    case False
-    with k have "?bounded S (Suc x)" by auto
-    then show ?thesis by auto
-  qed
-qed
+lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\<exists>k. S \<subseteq> {..<k}"
+proof cases
+  assume "S \<noteq> {}" with Max_less_iff[OF S this] show ?thesis
+    by auto
+qed simp
 
-lemma finite_nat_iff_bounded:
-  "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs by (rule finite_nat_bounded)
-next
-  assume ?rhs
-  then obtain k where "S \<subseteq> {..<k}" ..
-  then show "finite S"
-    by (rule finite_subset) simp
-qed
+lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
+  by (auto intro: finite_nat_bounded dest: finite_subset)
 
 lemma finite_nat_iff_bounded_le:
   "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})"  (is "?lhs \<longleftrightarrow> ?rhs")
@@ -116,56 +91,12 @@
     by (rule finite_subset) simp
 qed
 
-lemma infinite_nat_iff_unbounded:
-  "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  show ?rhs
-  proof (rule ccontr)
-    assume "\<not> ?rhs"
-    then obtain m where m: "\<forall>n. m < n \<longrightarrow> n \<notin> S" by blast
-    then have "S \<subseteq> {..m}"
-      by (auto simp add: sym [OF linorder_not_less])
-    with `?lhs` show False
-      by (simp add: finite_nat_iff_bounded_le)
-  qed
-next
-  assume ?rhs
-  show ?lhs
-  proof
-    assume "finite S"
-    then obtain m where "S \<subseteq> {..m}"
-      by (auto simp add: finite_nat_iff_bounded_le)
-    then have "\<forall>n. m < n \<longrightarrow> n \<notin> S" by auto
-    with `?rhs` show False by blast
-  qed
-qed
+lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
+  unfolding finite_nat_iff_bounded_le by (auto simp: subset_eq not_le)
 
 lemma infinite_nat_iff_unbounded_le:
   "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  show ?rhs
-  proof
-    fix m
-    from `?lhs` obtain n where "m < n \<and> n \<in> S"
-      by (auto simp add: infinite_nat_iff_unbounded)
-    then have "m \<le> n \<and> n \<in> S" by simp
-    then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
-  qed
-next
-  assume ?rhs
-  show ?lhs
-  proof (auto simp add: infinite_nat_iff_unbounded)
-    fix m
-    from `?rhs` obtain n where "Suc m \<le> n \<and> n \<in> S"
-      by blast
-    then have "m < n \<and> n \<in> S" by simp
-    then show "\<exists>n. m < n \<and> n \<in> S" ..
-  qed
-qed
+  unfolding finite_nat_iff_bounded by (auto simp: subset_eq not_less)
 
 text {*
   For a set of natural numbers to be infinite, it is enough to know

--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -6,7 +6,7 @@
 section {* Linear Temporal Logic on Streams *}
 
 theory Linear_Temporal_Logic_on_Streams
-  imports Stream Sublist
+  imports Stream Sublist Extended_Nat Infinite_Set
 begin
 
 section{* Preliminaries *}
@@ -59,6 +59,11 @@
 fun holds where "holds P xs \<longleftrightarrow> P (shd xs)"
 fun nxt where "nxt \<phi> xs = \<phi> (stl xs)"
 
+definition "HLD s = holds (\<lambda>x. x \<in> s)"
+
+abbreviation HLD_nxt (infixr "\<cdot>" 65) where
+  "s \<cdot> P \<equiv> HLD s aand nxt P"
+
 inductive ev for \<phi> where
 base: "\<phi> xs \<Longrightarrow> ev \<phi> xs"
 |
@@ -81,11 +86,28 @@
 lemma holds_aand:
 "(holds P aand holds Q) steps \<longleftrightarrow> holds (\<lambda> step. P step \<and> Q step) steps" by auto
 
+lemma HLD_iff: "HLD s \<omega> \<longleftrightarrow> shd \<omega> \<in> s"
+  by (simp add: HLD_def)
+
+lemma HLD_Stream[simp]: "HLD X (x ## \<omega>) \<longleftrightarrow> x \<in> X"
+  by (simp add: HLD_iff)
+
 lemma nxt_mono:
 assumes nxt: "nxt \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs"
 shows "nxt \<psi> xs"
 using assms by auto
 
+declare ev.intros[intro]
+declare alw.cases[elim]
+
+lemma ev_induct_strong[consumes 1, case_names base step]:
+  "ev \<phi> x \<Longrightarrow> (\<And>xs. \<phi> xs \<Longrightarrow> P xs) \<Longrightarrow> (\<And>xs. ev \<phi> (stl xs) \<Longrightarrow> \<not> \<phi> xs \<Longrightarrow> P (stl xs) \<Longrightarrow> P xs) \<Longrightarrow> P x"
+  by (induct rule: ev.induct) auto
+
+lemma alw_coinduct[consumes 1, case_names alw stl]:
+  "X x \<Longrightarrow> (\<And>x. X x \<Longrightarrow> \<phi> x) \<Longrightarrow> (\<And>x. X x \<Longrightarrow> \<not> alw \<phi> (stl x) \<Longrightarrow> X (stl x)) \<Longrightarrow> alw \<phi> x"
+  using alw.coinduct[of X x \<phi>] by auto
+
 lemma ev_mono:
 assumes ev: "ev \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs"
 shows "ev \<psi> xs"
@@ -387,5 +409,352 @@
 qed
 
 
+inductive ev_at :: "('a stream \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a stream \<Rightarrow> bool" for P :: "'a stream \<Rightarrow> bool" where
+  base: "P \<omega> \<Longrightarrow> ev_at P 0 \<omega>"
+| step:"\<not> P \<omega> \<Longrightarrow> ev_at P n (stl \<omega>) \<Longrightarrow> ev_at P (Suc n) \<omega>"
+
+inductive_simps ev_at_0[simp]: "ev_at P 0 \<omega>"
+inductive_simps ev_at_Suc[simp]: "ev_at P (Suc n) \<omega>"
+
+lemma ev_at_imp_snth: "ev_at P n \<omega> \<Longrightarrow> P (sdrop n \<omega>)"
+  by (induction n arbitrary: \<omega>) auto
+
+lemma ev_at_HLD_imp_snth: "ev_at (HLD X) n \<omega> \<Longrightarrow> \<omega> !! n \<in> X"
+  by (auto dest!: ev_at_imp_snth simp: HLD_iff)
+
+lemma ev_at_HLD_single_imp_snth: "ev_at (HLD {x}) n \<omega> \<Longrightarrow> \<omega> !! n = x"
+  by (drule ev_at_HLD_imp_snth) simp
+
+lemma ev_at_unique: "ev_at P n \<omega> \<Longrightarrow> ev_at P m \<omega> \<Longrightarrow> n = m"
+proof (induction arbitrary: m rule: ev_at.induct)
+  case (base \<omega>) then show ?case
+    by (simp add: ev_at.simps[of _ _ \<omega>])
+next
+  case (step \<omega> n) from step.prems step.hyps step.IH[of "m - 1"] show ?case
+    by (auto simp add: ev_at.simps[of _ _ \<omega>])
+qed
+
+lemma ev_iff_ev_at: "ev P \<omega> \<longleftrightarrow> (\<exists>n. ev_at P n \<omega>)"
+proof
+  assume "ev P \<omega>" then show "\<exists>n. ev_at P n \<omega>"
+    by (induction rule: ev_induct_strong) (auto intro: ev_at.intros)
+next
+  assume "\<exists>n. ev_at P n \<omega>"
+  then obtain n where "ev_at P n \<omega>"
+    by auto
+  then show "ev P \<omega>"
+    by induction auto
+qed
+
+lemma ev_at_shift: "ev_at (HLD X) i (stake (Suc i) \<omega> @- \<omega>' :: 's stream) \<longleftrightarrow> ev_at (HLD X) i \<omega>"
+  by (induction i arbitrary: \<omega>) (auto simp: HLD_iff)
+
+lemma ev_iff_ev_at_unqiue: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
+  by (auto intro: ev_at_unique simp: ev_iff_ev_at)
+
+lemma alw_HLD_iff_streams: "alw (HLD X) \<omega> \<longleftrightarrow> \<omega> \<in> streams X"
+proof
+  assume "alw (HLD X) \<omega>" then show "\<omega> \<in> streams X"
+  proof (coinduction arbitrary: \<omega>)
+    case (streams \<omega>) then show ?case by (cases \<omega>) auto
+  qed
+next
+  assume "\<omega> \<in> streams X" then show "alw (HLD X) \<omega>"
+  proof (coinduction arbitrary: \<omega>)
+    case (alw \<omega>) then show ?case by (cases \<omega>) auto
+  qed
+qed
+
+lemma not_HLD: "not (HLD X) = HLD (- X)"
+  by (auto simp: HLD_iff)
+
+lemma not_alw_iff: "\<not> (alw P \<omega>) \<longleftrightarrow> ev (not P) \<omega>"
+  using not_alw[of P] by (simp add: fun_eq_iff)
+
+lemma not_ev_iff: "\<not> (ev P \<omega>) \<longleftrightarrow> alw (not P) \<omega>"
+  using not_alw_iff[of "not P" \<omega>, symmetric]  by simp
+
+lemma ev_Stream: "ev P (x ## s) \<longleftrightarrow> P (x ## s) \<or> ev P s"
+  by (auto elim: ev.cases)
+
+lemma alw_ev_imp_ev_alw:
+  assumes "alw (ev P) \<omega>" shows "ev (P aand alw (ev P)) \<omega>"
+proof -
+  have "ev P \<omega>" using assms by auto
+  from this assms show ?thesis
+    by induct auto
+qed
+
+lemma ev_False: "ev (\<lambda>x. False) \<omega> \<longleftrightarrow> False"
+proof
+  assume "ev (\<lambda>x. False) \<omega>" then show False
+    by induct auto
+qed auto
+
+lemma alw_False: "alw (\<lambda>x. False) \<omega> \<longleftrightarrow> False"
+  by auto
+
+lemma ev_iff_sdrop: "ev P \<omega> \<longleftrightarrow> (\<exists>m. P (sdrop m \<omega>))"
+proof safe
+  assume "ev P \<omega>" then show "\<exists>m. P (sdrop m \<omega>)"
+    by (induct rule: ev_induct_strong) (auto intro: exI[of _ 0] exI[of _ "Suc n" for n])
+next
+  fix m assume "P (sdrop m \<omega>)" then show "ev P \<omega>"
+    by (induct m arbitrary: \<omega>) auto
+qed
+
+lemma alw_iff_sdrop: "alw P \<omega> \<longleftrightarrow> (\<forall>m. P (sdrop m \<omega>))"
+proof safe
+  fix m assume "alw P \<omega>" then show "P (sdrop m \<omega>)"
+    by (induct m arbitrary: \<omega>) auto
+next
+  assume "\<forall>m. P (sdrop m \<omega>)" then show "alw P \<omega>"
+    by (coinduction arbitrary: \<omega>) (auto elim: allE[of _ 0] allE[of _ "Suc n" for n])
+qed
+
+lemma infinite_iff_alw_ev: "infinite {m. P (sdrop m \<omega>)} \<longleftrightarrow> alw (ev P) \<omega>"
+  unfolding infinite_nat_iff_unbounded_le alw_iff_sdrop ev_iff_sdrop
+  by simp (metis le_Suc_ex le_add1)
+
+lemma alw_inv:
+  assumes stl: "\<And>s. f (stl s) = stl (f s)"
+  shows "alw P (f s) \<longleftrightarrow> alw (\<lambda>x. P (f x)) s"
+proof
+  assume "alw P (f s)" then show "alw (\<lambda>x. P (f x)) s"
+    by (coinduction arbitrary: s rule: alw_coinduct)
+       (auto simp: stl)
+next
+  assume "alw (\<lambda>x. P (f x)) s" then show "alw P (f s)"
+    by (coinduction arbitrary: s rule: alw_coinduct) (auto simp: stl[symmetric])
+qed
+
+lemma ev_inv:
+  assumes stl: "\<And>s. f (stl s) = stl (f s)"
+  shows "ev P (f s) \<longleftrightarrow> ev (\<lambda>x. P (f x)) s"
+proof
+  assume "ev P (f s)" then show "ev (\<lambda>x. P (f x)) s"
+    by (induction "f s" arbitrary: s) (auto simp: stl)
+next
+  assume "ev (\<lambda>x. P (f x)) s" then show "ev P (f s)"
+    by induction (auto simp: stl[symmetric])
+qed
+
+lemma alw_smap: "alw P (smap f s) \<longleftrightarrow> alw (\<lambda>x. P (smap f x)) s"
+  by (rule alw_inv) simp
+
+lemma ev_smap: "ev P (smap f s) \<longleftrightarrow> ev (\<lambda>x. P (smap f x)) s"
+  by (rule ev_inv) simp
+
+lemma alw_cong:
+  assumes P: "alw P \<omega>" and eq: "\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<longleftrightarrow> Q2 \<omega>"
+  shows "alw Q1 \<omega> \<longleftrightarrow> alw Q2 \<omega>"
+proof -
+  from eq have "(alw P aand Q1) = (alw P aand Q2)" by auto
+  then have "alw (alw P aand Q1) \<omega> = alw (alw P aand Q2) \<omega>" by auto
+  with P show "alw Q1 \<omega> \<longleftrightarrow> alw Q2 \<omega>"
+    by (simp add: alw_aand)
+qed
+
+lemma ev_cong:
+  assumes P: "alw P \<omega>" and eq: "\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<longleftrightarrow> Q2 \<omega>"
+  shows "ev Q1 \<omega> \<longleftrightarrow> ev Q2 \<omega>"
+proof -
+  from P have "alw (\<lambda>xs. Q1 xs \<longrightarrow> Q2 xs) \<omega>" by (rule alw_mono) (simp add: eq)
+  moreover from P have "alw (\<lambda>xs. Q2 xs \<longrightarrow> Q1 xs) \<omega>" by (rule alw_mono) (simp add: eq)
+  moreover note ev_alw_impl[of Q1 \<omega> Q2] ev_alw_impl[of Q2 \<omega> Q1]
+  ultimately show "ev Q1 \<omega> \<longleftrightarrow> ev Q2 \<omega>"
+    by auto
+qed
+
+lemma alwD: "alw P x \<Longrightarrow> P x"
+  by auto
+
+lemma alw_alwD: "alw P \<omega> \<Longrightarrow> alw (alw P) \<omega>"
+  by simp
+
+lemma alw_ev_stl: "alw (ev P) (stl \<omega>) \<longleftrightarrow> alw (ev P) \<omega>"
+  by (auto intro: alw.intros)
+
+lemma holds_Stream: "holds P (x ## s) \<longleftrightarrow> P x"
+  by simp
+
+lemma holds_eq1[simp]: "holds (op = x) = HLD {x}"
+  by rule (auto simp: HLD_iff)
+
+lemma holds_eq2[simp]: "holds (\<lambda>y. y = x) = HLD {x}"
+  by rule (auto simp: HLD_iff)
+
+lemma not_holds_eq[simp]: "holds (- op = x) = not (HLD {x})"
+  by rule (auto simp: HLD_iff)
+
+text {* Strong until *}
+
+inductive suntil (infix "suntil" 60) for \<phi> \<psi> where
+  base: "\<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
+| step: "\<phi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
+
+inductive_simps suntil_Stream: "(\<phi> suntil \<psi>) (x ## s)"
+
+lemma suntil_induct_strong[consumes 1, case_names base step]:
+  "(\<phi> suntil \<psi>) x \<Longrightarrow>
+    (\<And>\<omega>. \<psi> \<omega> \<Longrightarrow> P \<omega>) \<Longrightarrow>
+    (\<And>\<omega>. \<phi> \<omega> \<Longrightarrow> \<not> \<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> P (stl \<omega>) \<Longrightarrow> P \<omega>) \<Longrightarrow> P x"
+  using suntil.induct[of \<phi> \<psi> x P] by blast
+
+lemma ev_suntil: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>"
+  by (induct rule: suntil.induct) (auto intro: ev.intros)
+
+lemma suntil_inv:
+  assumes stl: "\<And>s. f (stl s) = stl (f s)"
+  shows "(P suntil Q) (f s) \<longleftrightarrow> ((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s"
+proof
+  assume "(P suntil Q) (f s)" then show "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s"
+    by (induction "f s" arbitrary: s) (auto simp: stl intro: suntil.intros)
+next
+  assume "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" then show "(P suntil Q) (f s)"
+    by induction (auto simp: stl[symmetric] intro: suntil.intros)
+qed
+
+lemma suntil_smap: "(P suntil Q) (smap f s) \<longleftrightarrow> ((\<lambda>x. P (smap f x)) suntil (\<lambda>x. Q (smap f x))) s"
+  by (rule suntil_inv) simp
+
+lemma hld_smap: "HLD x (smap f s) = holds (\<lambda>y. f y \<in> x) s"
+  by (simp add: HLD_def)
+
+lemma suntil_mono:
+  assumes eq: "\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<Longrightarrow> Q2 \<omega>" "\<And>\<omega>. P \<omega> \<Longrightarrow> R1 \<omega> \<Longrightarrow> R2 \<omega>"
+  assumes *: "(Q1 suntil R1) \<omega>" "alw P \<omega>" shows "(Q2 suntil R2) \<omega>"
+  using * by induct (auto intro: eq suntil.intros)
+
+lemma suntil_cong:
+  "alw P \<omega> \<Longrightarrow> (\<And>\<omega>. P \<omega> \<Longrightarrow> Q1 \<omega> \<longleftrightarrow> Q2 \<omega>) \<Longrightarrow> (\<And>\<omega>. P \<omega> \<Longrightarrow> R1 \<omega> \<longleftrightarrow> R2 \<omega>) \<Longrightarrow>
+    (Q1 suntil R1) \<omega> \<longleftrightarrow> (Q2 suntil R2) \<omega>"
+  using suntil_mono[of P Q1 Q2 R1 R2 \<omega>] suntil_mono[of P Q2 Q1 R2 R1 \<omega>] by auto
+
+lemma ev_suntil_iff: "ev (P suntil Q) \<omega> \<longleftrightarrow> ev Q \<omega>"
+proof
+  assume "ev (P suntil Q) \<omega>" then show "ev Q \<omega>"
+   by induct (auto dest: ev_suntil)
+next
+  assume "ev Q \<omega>" then show "ev (P suntil Q) \<omega>"
+    by induct (auto intro: suntil.intros)
+qed
+
+lemma true_suntil: "((\<lambda>_. True) suntil P) = ev P"
+  by (simp add: suntil_def ev_def)
+
+lemma suntil_lfp: "(\<phi> suntil \<psi>) = lfp (\<lambda>P s. \<psi> s \<or> (\<phi> s \<and> P (stl s)))"
+  by (simp add: suntil_def)
+
+lemma sfilter_P[simp]: "P (shd s) \<Longrightarrow> sfilter P s = shd s ## sfilter P (stl s)"
+  using sfilter_Stream[of P "shd s" "stl s"] by simp
+
+lemma sfilter_not_P[simp]: "\<not> P (shd s) \<Longrightarrow> sfilter P s = sfilter P (stl s)"
+  using sfilter_Stream[of P "shd s" "stl s"] by simp
+
+lemma sfilter_eq: 
+  assumes "ev (holds P) s"
+  shows "sfilter P s = x ## s' \<longleftrightarrow>
+    P x \<and> (not (holds P) suntil (HLD {x} aand nxt (\<lambda>s. sfilter P s = s'))) s"
+  using assms
+  by (induct rule: ev_induct_strong)
+     (auto simp add: HLD_iff intro: suntil.intros elim: suntil.cases)
+
+lemma sfilter_streams:
+  "alw (ev (holds P)) \<omega> \<Longrightarrow> \<omega> \<in> streams A \<Longrightarrow> sfilter P \<omega> \<in> streams {x\<in>A. P x}"
+proof (coinduction arbitrary: \<omega>)
+  case (streams \<omega>)
+  then have "ev (holds P) \<omega>" by blast
+  from this streams show ?case
+    by (induct rule: ev_induct_strong) (auto elim: streamsE)
+qed
+
+lemma alw_sfilter:
+  assumes *: "alw (ev (holds P)) s"
+  shows "alw Q (sfilter P s) \<longleftrightarrow> alw (\<lambda>x. Q (sfilter P x)) s"
+proof
+  assume "alw Q (sfilter P s)" with * show "alw (\<lambda>x. Q (sfilter P x)) s"
+  proof (coinduction arbitrary: s rule: alw_coinduct)
+    case (stl s) 
+    then have "ev (holds P) s"
+      by blast
+    from this stl show ?case
+      by (induct rule: ev_induct_strong) auto
+  qed auto
+next
+  assume "alw (\<lambda>x. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
+  proof (coinduction arbitrary: s rule: alw_coinduct)
+    case (stl s) 
+    then have "ev (holds P) s"
+      by blast
+    from this stl show ?case
+      by (induct rule: ev_induct_strong) auto
+  qed auto
+qed
+
+lemma ev_sfilter:
+  assumes *: "alw (ev (holds P)) s"
+  shows "ev Q (sfilter P s) \<longleftrightarrow> ev (\<lambda>x. Q (sfilter P x)) s"
+proof
+  assume "ev Q (sfilter P s)" from this * show "ev (\<lambda>x. Q (sfilter P x)) s"
+  proof (induction "sfilter P s" arbitrary: s rule: ev_induct_strong)
+    case (step s)
+    then have "ev (holds P) s"
+      by blast
+    from this step show ?case
+      by (induct rule: ev_induct_strong) auto
+  qed auto
+next
+  assume "ev (\<lambda>x. Q (sfilter P x)) s" then show "ev Q (sfilter P s)"
+  proof (induction rule: ev_induct_strong)
+    case (step s) then show ?case
+      by (cases "P (shd s)") auto
+  qed auto
+qed
+
+lemma holds_sfilter:
+  assumes "ev (holds Q) s" shows "holds P (sfilter Q s) \<longleftrightarrow> (not (holds Q) suntil (holds (Q aand P))) s"
+proof
+  assume "holds P (sfilter Q s)" with assms show "(not (holds Q) suntil (holds (Q aand P))) s"
+    by (induct rule: ev_induct_strong) (auto intro: suntil.intros)
+next
+  assume "(not (holds Q) suntil (holds (Q aand P))) s" then show "holds P (sfilter Q s)"
+    by induct auto
+qed
+
+lemma suntil_aand_nxt:
+  "(\<phi> suntil (\<phi> aand nxt \<psi>)) \<omega> \<longleftrightarrow> (\<phi> aand nxt (\<phi> suntil \<psi>)) \<omega>"
+proof
+  assume "(\<phi> suntil (\<phi> aand nxt \<psi>)) \<omega>" then show "(\<phi> aand nxt (\<phi> suntil \<psi>)) \<omega>"
+    by induction (auto intro: suntil.intros)
+next
+  assume "(\<phi> aand nxt (\<phi> suntil \<psi>)) \<omega>"
+  then have "(\<phi> suntil \<psi>) (stl \<omega>)" "\<phi> \<omega>"
+    by auto
+  then show "(\<phi> suntil (\<phi> aand nxt \<psi>)) \<omega>"
+    by (induction "stl \<omega>" arbitrary: \<omega>)
+       (auto elim: suntil.cases intro: suntil.intros)
+qed
+
+lemma alw_sconst: "alw P (sconst x) \<longleftrightarrow> P (sconst x)"
+proof
+  assume "P (sconst x)" then show "alw P (sconst x)"
+    by coinduction auto
+qed auto
+
+lemma ev_sconst: "ev P (sconst x) \<longleftrightarrow> P (sconst x)"
+proof
+  assume "ev P (sconst x)" then show "P (sconst x)"
+    by (induction "sconst x") auto
+qed auto
+
+lemma suntil_sconst: "(\<phi> suntil \<psi>) (sconst x) \<longleftrightarrow> \<psi> (sconst x)"
+proof
+  assume "(\<phi> suntil \<psi>) (sconst x)" then show "\<psi> (sconst x)"
+    by (induction "sconst x") auto
+qed (auto intro: suntil.intros)
+
+lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
+  by (simp add: HLD_def)
 
 end
\ No newline at end of file

--- a/src/HOL/Library/Stream.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Library/Stream.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -36,6 +36,8 @@
   shows "P y s"
 using assms by induct (metis stream.sel(1), auto)
 
+lemma smap_ctr: "smap f s = x ## s' \<longleftrightarrow> f (shd s) = x \<and> smap f (stl s) = s'"
+  by (cases s) simp
 
 subsection {* prepend list to stream *}
 
@@ -69,6 +71,15 @@
 where
   Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
 
+lemma in_streams: "stl s \<in> streams S \<Longrightarrow> shd s \<in> S \<Longrightarrow> s \<in> streams S"
+  by (cases s) auto
+
+lemma streamsE: "s \<in> streams A \<Longrightarrow> (shd s \<in> A \<Longrightarrow> stl s \<in> streams A \<Longrightarrow> P) \<Longrightarrow> P"
+  by (erule streams.cases) simp_all
+
+lemma Stream_image: "x ## y \<in> (op ## x') ` Y \<longleftrightarrow> x = x' \<and> y \<in> Y"
+  by auto
+
 lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
   by (induct w) auto
 
@@ -102,6 +113,9 @@
 lemma streams_mono:  "s \<in> streams A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> s \<in> streams B"
   unfolding streams_iff_sset by auto
 
+lemma streams_mono2: "S \<subseteq> T \<Longrightarrow> streams S \<subseteq> streams T"
+  by (auto intro: streams_mono)
+
 lemma smap_streams: "s \<in> streams A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> smap f s \<in> streams B"
   unfolding streams_iff_sset stream.set_map by auto
 
@@ -117,6 +131,9 @@
   "s !! 0 = shd s"
 | "s !! Suc n = stl s !! n"
 
+lemma snth_Stream: "(x ## s) !! Suc i = s !! i"
+  by simp
+
 lemma snth_smap[simp]: "smap f s !! n = f (s !! n)"
   by (induct n arbitrary: s) auto
 
@@ -143,6 +160,12 @@
   qed (auto intro: range_eqI[of _ _ 0])
 qed auto
 
+lemma streams_iff_snth: "s \<in> streams X \<longleftrightarrow> (\<forall>n. s !! n \<in> X)"
+  by (force simp: streams_iff_sset sset_range)
+
+lemma snth_in: "s \<in> streams X \<Longrightarrow> s !! n \<in> X"
+  by (simp add: streams_iff_snth)
+
 primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
   "stake 0 s = []"
 | "stake (Suc n) s = shd s # stake n (stl s)"

--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -774,120 +774,6 @@
 
 subsection {* Sums *}
 
-lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
-proof (cases "finite A")
-  case True
-  then show ?thesis by induct auto
-next
-  case False
-  then show ?thesis by simp
-qed
-
-lemma setsum_Pinfty:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
-proof safe
-  assume *: "setsum f P = \<infinity>"
-  show "finite P"
-  proof (rule ccontr)
-    assume "infinite P"
-    with * show False
-      by auto
-  qed
-  show "\<exists>i\<in>P. f i = \<infinity>"
-  proof (rule ccontr)
-    assume "\<not> ?thesis"
-    then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
-      by auto
-    with `finite P` have "setsum f P \<noteq> \<infinity>"
-      by induct auto
-    with * show False
-      by auto
-  qed
-next
-  fix i
-  assume "finite P" and "i \<in> P" and "f i = \<infinity>"
-  then show "setsum f P = \<infinity>"
-  proof induct
-    case (insert x A)
-    show ?case using insert by (cases "x = i") auto
-  qed simp
-qed
-
-lemma setsum_Inf:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
-proof
-  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
-  have "finite A"
-    by (rule ccontr) (insert *, auto)
-  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
-  proof (rule ccontr)
-    assume "\<not> ?thesis"
-    then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
-      by auto
-    from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
-    with * show False
-      by auto
-  qed
-  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
-    by auto
-next
-  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
-  then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
-    by auto
-  then show "\<bar>setsum f A\<bar> = \<infinity>"
-  proof induct
-    case (insert j A)
-    then show ?case
-      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
-  qed simp
-qed
-
-lemma setsum_real_of_ereal:
-  fixes f :: "'i \<Rightarrow> ereal"
-  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
-  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
-proof -
-  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
-  proof
-    fix x
-    assume "x \<in> S"
-    from assms[OF this] show "\<exists>r. f x = ereal r"
-      by (cases "f x") auto
-  qed
-  from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
-  then show ?thesis
-    by simp
-qed
-
-lemma setsum_ereal_0:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "finite A"
-    and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
-  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
-proof
-  assume *: "(\<Sum>x\<in>A. f x) = 0"
-  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>"
-    by auto
-  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>"
-    using assms by (force simp: setsum_Pinfty)
-  then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
-    by auto
-  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
-    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
-qed (rule setsum.neutral)
-
-lemma setsum_ereal_right_distrib:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
-  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
-proof cases
-  assume "finite A"
-  then show ?thesis using assms
-    by induct (auto simp: ereal_right_distrib setsum_nonneg)
-qed simp
-
 lemma sums_ereal_positive:
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "\<And>i. 0 \<le> f i"
@@ -1463,6 +1349,9 @@
 
 subsection "Relate extended reals and the indicator function"
 
+lemma ereal_indicator_le_0: "(indicator S x::ereal) \<le> 0 \<longleftrightarrow> x \<notin> S"
+  by (auto split: split_indicator simp: one_ereal_def)
+
 lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
   by (auto simp: indicator_def one_ereal_def)
 

--- a/src/HOL/Nat.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Nat.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1391,6 +1391,12 @@
 lemma id_funpow[simp]: "id ^^ n = id"
   by (induct n) simp_all
 
+lemma funpow_mono:
+  fixes f :: "'a \<Rightarrow> ('a::lattice)"
+  shows "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
+  by (induct n arbitrary: A B)
+     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
+
 subsection {* Kleene iteration *}
 
 lemma Kleene_iter_lpfp:
@@ -1848,7 +1854,27 @@
 lemma dec_induct[consumes 1, case_names base step]:
   "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
   by (induct j arbitrary: i) (auto simp: le_Suc_eq)
- 
+
+subsection \<open> Monotonicity of funpow \<close>
+
+lemma funpow_increasing:
+  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_top})"
+  shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
+  by (induct rule: inc_induct)
+     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
+           intro: order_trans[OF _ funpow_mono])
+
+lemma funpow_decreasing:
+  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_bot})"
+  shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
+  by (induct rule: dec_induct)
+     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
+           intro: order_trans[OF _ funpow_mono])
+
+lemma mono_funpow:
+  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+  shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
+  by (auto intro!: funpow_decreasing simp: mono_def)
 
 subsection {* The divides relation on @{typ nat} *}
 

--- a/src/HOL/Orderings.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Orderings.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1524,6 +1524,9 @@
 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   by (rule le_funE)
 
+lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
+  unfolding mono_def le_fun_def by auto
+
 
 subsection {* Order on unary and binary predicates *}
 

--- a/src/HOL/Probability/Binary_Product_Measure.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -29,6 +29,9 @@
   unfolding pair_measure_def using pair_measure_closed[of A B]
   by (rule space_measure_of)
 
+lemma SIGMA_Collect_eq: "(SIGMA x:space M. {y\<in>space N. P x y}) = {x\<in>space (M \<Otimes>\<^sub>M N). P (fst x) (snd x)}"
+  by (auto simp: space_pair_measure)
+
 lemma sets_pair_measure:
   "sets (A \<Otimes>\<^sub>M B) = sigma_sets (space A \<times> space B) {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
   unfolding pair_measure_def using pair_measure_closed[of A B]

--- a/src/HOL/Probability/Bochner_Integration.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1296,6 +1296,11 @@
   shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
   by (rule integrable_bound[of M f]) (auto split: split_indicator)
 
+lemma integrable_real_mult_indicator:
+  fixes f :: "'a \<Rightarrow> real"
+  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
+  using integrable_mult_indicator[of A M f] by (simp add: mult_ac)
+
 lemma integrable_abs[simp, intro]:
   fixes f :: "'a \<Rightarrow> real"
   assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
@@ -2255,6 +2260,36 @@
   apply auto
   done
 
+lemma integral_indicator_finite_real:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes [simp]: "finite A"
+  assumes [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"
+  assumes finite: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} < \<infinity>"
+  shows "(\<integral>x. f x * indicator A x \<partial>M) = (\<Sum>a\<in>A. f a * measure M {a})"
+proof -
+  have "(\<integral>x. f x * indicator A x \<partial>M) = (\<integral>x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
+  proof (intro integral_cong refl)
+    fix x show "f x * indicator A x = (\<Sum>a\<in>A. f a * indicator {a} x)"
+      by (auto split: split_indicator simp: eq_commute[of x] cong: conj_cong)
+  qed
+  also have "\<dots> = (\<Sum>a\<in>A. f a * measure M {a})"
+    using finite by (subst integral_setsum) (auto simp add: integrable_mult_left_iff)
+  finally show ?thesis .
+qed
+
+lemma (in finite_measure) ereal_integral_real:
+  assumes [measurable]: "f \<in> borel_measurable M" 
+  assumes ae: "AE x in M. 0 \<le> f x" "AE x in M. f x \<le> ereal B"
+  shows "ereal (\<integral>x. real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
+proof (subst nn_integral_eq_integral[symmetric])
+  show "integrable M (\<lambda>x. real (f x))"
+    using ae by (intro integrable_const_bound[where B=B]) (auto simp: real_le_ereal_iff)
+  show "AE x in M. 0 \<le> real (f x)"
+    using ae by (auto simp: real_of_ereal_pos)
+  show "(\<integral>\<^sup>+ x. ereal (real (f x)) \<partial>M) = integral\<^sup>N M f"
+    using ae by (intro nn_integral_cong_AE) (auto simp: ereal_real)
+qed
+
 lemma (in finite_measure) integral_less_AE:
   fixes X Y :: "'a \<Rightarrow> real"
   assumes int: "integrable M X" "integrable M Y"

--- a/src/HOL/Probability/Borel_Space.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1320,6 +1320,28 @@
   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
 
+lemma borel_measurable_sup[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
+    (\<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"

--- a/src/HOL/Probability/Distributions.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Distributions.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -873,7 +873,7 @@
       then show "((\<lambda>a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) ---> 0) at_top"
         by (simp add: field_simps)
     qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff)
-  qed
+  qed rule
   also have "... = ereal (pi / 4)"
   proof (subst nn_integral_FTC_atLeast)
     show "((\<lambda>a. arctan a / 2) ---> (pi / 2) / 2 ) at_top"

--- a/src/HOL/Probability/Giry_Monad.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -44,9 +44,12 @@
   show "space (distr M M' f) \<noteq> {}" by (simp add: assms)
 qed
 
-lemma (in subprob_space) subprob_measure_le_1: "emeasure M X \<le> 1"
+lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1"
   by (rule order.trans[OF emeasure_space emeasure_space_le_1])
 
+lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
+  using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
+
 locale pair_subprob_space = 
   pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
 
@@ -75,6 +78,15 @@
   "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
   by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
 
+lemma subprob_measurableD:
+  assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M"
+  shows "space (N x) = space S"
+    and "sets (N x) = sets S"
+    and "measurable (N x) K = measurable S K"
+    and "measurable K (N x) = measurable K S"
+  using measurable_space[OF N x]
+  by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
+
 context
   fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
 begin
@@ -113,6 +125,43 @@
   ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
 qed
 
+lemma nn_integral_measurable_subprob_algebra:
+  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
+  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
+  using f
+proof induct
+  case (cong f g)
+  moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B"
+    by (intro measurable_cong nn_integral_cong cong)
+       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case by simp
+next
+  case (set B)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
+    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: measurable_emeasure_subprob_algebra)
+next
+  case (mult f c)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
+    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
+  ultimately show ?case
+    by simp
+next
+  case (add f g)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
+    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: ac_simps)
+next
+  case (seq F)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
+    unfolding SUP_apply
+    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: ac_simps)
+qed
+
 lemma measurable_distr:
   assumes [measurable]: "f \<in> measurable M N"
   shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
@@ -131,6 +180,118 @@
   qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty)
 qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
 
+lemma emeasure_space_subprob_algebra[measurable]:
+  "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
+proof-
+  have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")
+    by (rule measurable_emeasure_subprob_algebra) simp
+  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
+    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
+  finally show ?thesis .
+qed
+
+(* TODO: Rename. This name is too general – Manuel *)
+lemma measurable_pair_measure:
+  assumes f: "f \<in> measurable M (subprob_algebra N)"
+  assumes g: "g \<in> measurable M (subprob_algebra L)"
+  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
+proof (rule measurable_subprob_algebra)
+  { fix x assume "x \<in> space M"
+    with measurable_space[OF f] measurable_space[OF g]
+    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
+      by auto
+    interpret F: subprob_space "f x"
+      using fx by (simp add: space_subprob_algebra)
+    interpret G: subprob_space "g x"
+      using gx by (simp add: space_subprob_algebra)
+
+    interpret pair_subprob_space "f x" "g x" ..
+    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
+    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
+      using fx gx by (simp add: space_subprob_algebra)
+
+    have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B"
+      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
+    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
+              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
+      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
+    hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L - A) =
+                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
+      using emeasure_compl[OF _ P.emeasure_finite]
+      unfolding sets_eq
+      unfolding sets_eq_imp_space_eq[OF sets_eq]
+      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
+    note 1 2 sets_eq }
+  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
+
+  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
+  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
+    using Int_stable_pair_measure_generator pair_measure_closed A
+    unfolding sets_pair_measure
+  proof (induct A rule: sigma_sets_induct_disjoint)
+    case (basic A) then show ?case
+      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
+         (auto intro!: measurable_emeasure_kernel f g)
+  next
+    case (compl A)
+    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
+      by (auto simp: sets_pair_measure)
+    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
+                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
+      using compl(2) f g by measurable
+    thus ?case by (simp add: Compl A cong: measurable_cong)
+  next
+    case (union A)
+    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
+      by (auto simp: sets_pair_measure)
+    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
+      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
+      by (intro measurable_cong suminf_emeasure[symmetric])
+         (auto simp: sets_eq)
+    also have "\<dots>"
+      using union by auto
+    finally show ?case .
+  qed simp
+qed
+
+lemma restrict_space_measurable:
+  assumes X: "X \<noteq> {}" "X \<in> sets K"
+  assumes N: "N \<in> measurable M (subprob_algebra K)"
+  shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))"
+proof (rule measurable_subprob_algebra)
+  fix a assume a: "a \<in> space M"
+  from N[THEN measurable_space, OF this]
+  have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K"
+    by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+  then interpret subprob_space "N a"
+    by simp
+  show "subprob_space (restrict_space (N a) X)"
+  proof
+    show "space (restrict_space (N a) X) \<noteq> {}"
+      using X by (auto simp add: space_restrict_space)
+    show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1"
+      using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1)
+  qed
+  show "sets (restrict_space (N a) X) = sets (restrict_space K X)"
+    by (intro sets_restrict_space_cong) fact
+next
+  fix A assume A: "A \<in> sets (restrict_space K X)"
+  show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M"
+  proof (subst measurable_cong)
+    fix a assume "a \<in> space M"
+    from N[THEN measurable_space, OF this]
+    have [simp]: "sets (N a) = sets K" "space (N a) = space K"
+      by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+    show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)"
+      using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps)
+  next
+    show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M"
+      using A X
+      by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra])
+         (auto simp: sets_restrict_space)
+  qed
+qed
+
 section {* Properties of return *}
 
 definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
@@ -148,6 +309,12 @@
 lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
   by (simp cong: measurable_cong_sets) 
 
+lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N"
+  by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def)
+
+lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x"
+  by (auto simp add: return_def dest: sets_eq_imp_space_eq)
+
 lemma emeasure_return[simp]:
   assumes "A \<in> sets M"
   shows "emeasure (return M x) A = indicator A x"
@@ -165,6 +332,16 @@
 lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
   by (intro prob_space_return prob_space_imp_subprob_space)
 
+lemma subprob_space_return_ne: 
+  assumes "space M \<noteq> {}" shows "subprob_space (return M x)"
+proof
+  show "emeasure (return M x) (space (return M x)) \<le> 1"
+    by (subst emeasure_return) (auto split: split_indicator)
+qed (simp, fact)
+
+lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x"
+  unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator)
+
 lemma AE_return:
   assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
   shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
@@ -188,7 +365,19 @@
   finally show ?thesis .
 qed
 
-lemma return_measurable: "return N \<in> measurable N (subprob_algebra N)"
+lemma integral_return:
+  fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes "x \<in> space M" "g \<in> borel_measurable M"
+  shows "(\<integral>a. g a \<partial>return M x) = g x"
+proof-
+  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
+  have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms
+    by (intro integral_cong_AE) (auto simp: AE_return)
+  then show ?thesis
+    using prob_space by simp
+qed
+
+lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)"
   by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
 
 lemma distr_return:
@@ -196,6 +385,121 @@
   shows "distr (return M x) N f = return N (f x)"
   using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
 
+lemma return_restrict_space:
+  "\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>"
+  by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
+
+lemma measurable_distr2:
+  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
+  assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
+  shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
+proof -
+  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
+    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
+  proof (rule measurable_cong)
+    fix x assume x: "x \<in> space L"
+    have gx: "g x \<in> space (subprob_algebra M)"
+      using measurable_space[OF g x] .
+    then have [simp]: "sets (g x) = sets M"
+      by (simp add: space_subprob_algebra)
+    then have [simp]: "space (g x) = space M"
+      by (rule sets_eq_imp_space_eq)
+    let ?R = "return L x"
+    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
+      by simp
+    interpret subprob_space "g x"
+      using gx by (simp add: space_subprob_algebra)
+    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
+      by (simp add: space_pair_measure)
+    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
+    proof (rule measure_eqI)
+      show "sets ?l = sets ?r"
+        by simp
+    next
+      fix A assume "A \<in> sets ?l"
+      then have A[measurable]: "A \<in> sets N"
+        by simp
+      then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) -` A \<inter> space (?R \<Otimes>\<^sub>M g x))"
+        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
+      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
+        apply (subst emeasure_pair_measure_alt)
+        apply (rule measurable_sets[OF _ A])
+        apply (auto simp add: f_M' cong: measurable_cong_sets)
+        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
+        apply (auto simp: space_subprob_algebra space_pair_measure)
+        done
+      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
+        by (subst nn_integral_return)
+           (auto simp: x intro!: measurable_emeasure)
+      also have "\<dots> = emeasure ?l A"
+        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
+      finally show "emeasure ?l A = emeasure ?r A" ..
+    qed
+  qed
+  also have "\<dots>"
+    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
+    apply (rule return_measurable)
+    apply measurable
+    done
+  finally show ?thesis .
+qed
+
+lemma nn_integral_measurable_subprob_algebra2:
+  assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" and [simp]: "\<And>x y. 0 \<le> f x y"
+  assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"
+  shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
+proof -
+  have "(\<lambda>x. integral\<^sup>N (distr (L x) (M \<Otimes>\<^sub>M N) (\<lambda>y. (x, y))) (\<lambda>(x, y). f x y)) \<in> borel_measurable M"
+    apply (rule measurable_compose[OF _ nn_integral_measurable_subprob_algebra])
+    apply (rule measurable_distr2)
+    apply measurable
+    apply (simp split: prod.split)
+    done
+  then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
+    apply (rule measurable_cong[THEN iffD1, rotated])
+    apply (subst nn_integral_distr)
+    apply measurable
+    apply (rule subprob_measurableD(2)[OF N], assumption)
+    apply measurable
+    done
+qed
+
+lemma emeasure_measurable_subprob_algebra2:
+  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
+  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
+  shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
+proof -
+  { fix x assume "x \<in> space M"
+    then have "Pair x -` Sigma (space M) A = A x"
+      by auto
+    with sets_Pair1[OF A, of x] have "A x \<in> sets N"
+      by auto }
+  note ** = this
+
+  have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)"
+    by (auto simp: fun_eq_iff)
+  have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
+    apply measurable
+    apply (subst measurable_cong)
+    apply (rule *)
+    apply (auto simp: space_pair_measure)
+    done
+  then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M"
+    by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L)
+  then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
+    apply (rule measurable_cong[THEN iffD1, rotated])
+    apply (rule nn_integral_indicator)
+    apply (simp add: subprob_measurableD[OF L] **)
+    done
+qed
+
+lemma measure_measurable_subprob_algebra2:
+  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
+  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
+  shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M"
+  unfolding measure_def
+  by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms])
+
 definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
 
 lemma select_sets1:
@@ -261,44 +565,6 @@
   qed
 qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
 
-lemma nn_integral_measurable_subprob_algebra:
-  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
-  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
-  using f
-proof induct
-  case (cong f g)
-  moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B"
-    by (intro measurable_cong nn_integral_cong cong)
-       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
-  ultimately show ?case by simp
-next
-  case (set B)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
-    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
-  ultimately show ?case
-    by (simp add: measurable_emeasure_subprob_algebra)
-next
-  case (mult f c)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
-    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
-  ultimately show ?case
-    by simp
-next
-  case (add f g)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
-    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
-  ultimately show ?case
-    by (simp add: ac_simps)
-next
-  case (seq F)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
-    unfolding SUP_apply
-    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
-  ultimately show ?case
-    by (simp add: ac_simps)
-qed
-
-
 lemma measurable_join:
   "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
 proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
@@ -519,29 +785,129 @@
       \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
   by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
 
-lemma bind_return: 
-  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
-  shows "bind (return M x) f = f x"
-  using sets_kernel[OF assms] assms
-  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
-               cong: subprob_algebra_cong)
+lemma nn_integral_bind:
+  assumes f: "f \<in> borel_measurable B" "\<And>x. 0 \<le> f x"
+  assumes N: "N \<in> measurable M (subprob_algebra B)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
+proof cases
+  assume M: "space M \<noteq> {}" show ?thesis
+    unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
+    by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
+qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
+
+lemma AE_bind:
+  assumes P[measurable]: "Measurable.pred B P"
+  assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
+  shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
+proof cases
+  assume M: "space M = {}" show ?thesis
+    unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
+next
+  assume M: "space M \<noteq> {}"
+  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))"
+    by (intro nn_integral_cong) (simp add: space_bind[OF N M] split: split_indicator)
+
+  have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
+    by (simp add: AE_iff_nn_integral sets_bind[OF N M] space_bind[OF N M] * nn_integral_bind[where B=B]
+             del: nn_integral_indicator)
+  also have "\<dots> = (AE x in M. AE y in N x. P y)"
+    apply (subst nn_integral_0_iff_AE)
+    apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
+    apply measurable
+    apply (intro eventually_subst AE_I2)
+    apply simp
+    apply (subst nn_integral_0_iff_AE)
+    apply (simp add: subprob_measurableD(3)[OF N])
+    apply (auto simp add: ereal_indicator_le_0 subprob_measurableD(1)[OF N] intro!: eventually_subst)
+    done
+  finally show ?thesis .
+qed
+
+lemma measurable_bind':
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
+          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
+proof (subst measurable_cong)
+  fix x assume x_in_M: "x \<in> space M"
+  with assms have "space (f x) \<noteq> {}" 
+      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
+  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
+      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
+         (auto dest: measurable_Pair2)
+  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
+      by (simp_all add: bind_nonempty'')
+next
+  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
+    apply (rule measurable_compose[OF _ measurable_join])
+    apply (rule measurable_distr2[OF M2 M1])
+    done
+qed
 
-lemma bind_return':
-  shows "bind M (return M) = M"
-  by (cases "space M = {}")
-     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
-               cong: subprob_algebra_cong)
+lemma measurable_bind:
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
+          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
+  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
+
+lemma measurable_bind2:
+  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
+    using assms by (intro measurable_bind' measurable_const) auto
+
+lemma subprob_space_bind:
+  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
+  shows "subprob_space (M \<guillemotright>= f)"
+proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
+  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
+    by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
+        rule measurable_compose[OF measurable_snd assms(2)])
+  from assms(1) show "M \<in> space (subprob_algebra M)"
+    by (simp add: space_subprob_algebra)
+qed
 
-lemma bind_count_space_singleton:
-  assumes "subprob_space (f x)"
-  shows "count_space {x} \<guillemotright>= f = f x"
-proof-
-  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
-  have "count_space {x} = return (count_space {x}) x"
-    by (intro measure_eqI) (auto dest: A)
-  also have "... \<guillemotright>= f = f x"
-    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
-  finally show ?thesis .
+lemma (in prob_space) prob_space_bind: 
+  assumes ae: "AE x in M. prob_space (N x)"
+    and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
+  shows "prob_space (M \<guillemotright>= N)"
+proof
+  have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
+    by (subst emeasure_bind[where N=S])
+       (auto simp: not_empty space_bind[OF N] subprob_measurableD[OF N] intro!: nn_integral_cong)
+  also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
+    using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
+  finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
+    by (simp add: emeasure_space_1)
+qed
+
+lemma (in subprob_space) bind_in_space:
+  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
+  by (auto simp add: space_subprob_algebra subprob_not_empty intro!: subprob_space_bind)
+     unfold_locales
+
+lemma (in subprob_space) measure_bind:
+  assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N"
+  shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M"
+proof -
+  interpret Mf: subprob_space "M \<guillemotright>= f"
+    by (rule subprob_space_bind[OF _ f]) unfold_locales
+
+  { fix x assume "x \<in> space M"
+    from f[THEN measurable_space, OF this] interpret subprob_space "f x"
+      by (simp add: space_subprob_algebra)
+    have "emeasure (f x) X = ereal (measure (f x) X)" "measure (f x) X \<le> 1"
+      by (auto simp: emeasure_eq_measure subprob_measure_le_1) }
+  note this[simp]
+
+  have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
+    using subprob_not_empty f X by (rule emeasure_bind)
+  also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M"
+    by (intro nn_integral_cong) simp
+  also have "\<dots> = \<integral>x. measure (f x) X \<partial>M"
+    by (intro nn_integral_eq_integral integrable_const_bound[where B=1]
+              measure_measurable_subprob_algebra2[OF _ f] pair_measureI X)
+       (auto simp: measure_nonneg)
+  finally show ?thesis
+    by (simp add: Mf.emeasure_eq_measure)
 qed
 
 lemma emeasure_bind_const: 
@@ -572,6 +938,73 @@
   using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
                             prob_space.emeasure_space_1)
 
+lemma bind_return: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
+  shows "bind (return M x) f = f x"
+  using sets_kernel[OF assms] assms
+  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
+               cong: subprob_algebra_cong)
+
+lemma bind_return':
+  shows "bind M (return M) = M"
+  by (cases "space M = {}")
+     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
+               cong: subprob_algebra_cong)
+
+lemma distr_bind:
+  assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}"
+  assumes f: "f \<in> measurable K R"
+  shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))"
+  unfolding bind_nonempty''[OF N]
+  apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)])
+  apply (rule f)
+  apply (simp add: join_distr_distr[OF _ f, symmetric])
+  apply (subst distr_distr[OF measurable_distr, OF f N(1)])
+  apply (simp add: comp_def)
+  done
+
+lemma bind_distr:
+  assumes f[measurable]: "f \<in> measurable M X"
+  assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}"
+  shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))"
+proof -
+  have "space X \<noteq> {}" "space M \<noteq> {}"
+    using `space M \<noteq> {}` f[THEN measurable_space] by auto
+  then show ?thesis
+    by (simp add: bind_nonempty''[where N=K] distr_distr comp_def)
+qed
+
+lemma bind_count_space_singleton:
+  assumes "subprob_space (f x)"
+  shows "count_space {x} \<guillemotright>= f = f x"
+proof-
+  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
+  have "count_space {x} = return (count_space {x}) x"
+    by (intro measure_eqI) (auto dest: A)
+  also have "... \<guillemotright>= f = f x"
+    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
+  finally show ?thesis .
+qed
+
+lemma restrict_space_bind:
+  assumes N: "N \<in> measurable M (subprob_algebra K)"
+  assumes "space M \<noteq> {}"
+  assumes X[simp]: "X \<in> sets K" "X \<noteq> {}"
+  shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)"
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
+  with X have "A \<in> sets K" "A \<subseteq> X"
+    by (auto simp: sets_restrict_space sets_bind[OF assms(1,2)])
+  then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
+    using assms
+    apply (subst emeasure_restrict_space)
+    apply (simp_all add: space_bind[OF assms(1,2)] sets_bind[OF assms(1,2)] emeasure_bind[OF assms(2,1)])
+    apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]])
+    apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra
+                intro!: nn_integral_cong dest!: measurable_space)
+    done
+qed (simp add: sets_restrict_space sets_bind[OF assms(1,2)] sets_bind[OF restrict_space_measurable[OF assms(4,3,1)] assms(2)])
+
 lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
   by (intro measure_eqI) 
      (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
@@ -618,180 +1051,6 @@
   finally show ?thesis ..
 qed (simp add: bind_empty)
 
-lemma emeasure_space_subprob_algebra[measurable]:
-  "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
-proof-
-  have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")
-    by (rule measurable_emeasure_subprob_algebra) simp
-  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
-    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
-  finally show ?thesis .
-qed
-
-(* TODO: Rename. This name is too general – Manuel *)
-lemma measurable_pair_measure:
-  assumes f: "f \<in> measurable M (subprob_algebra N)"
-  assumes g: "g \<in> measurable M (subprob_algebra L)"
-  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
-proof (rule measurable_subprob_algebra)
-  { fix x assume "x \<in> space M"
-    with measurable_space[OF f] measurable_space[OF g]
-    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
-      by auto
-    interpret F: subprob_space "f x"
-      using fx by (simp add: space_subprob_algebra)
-    interpret G: subprob_space "g x"
-      using gx by (simp add: space_subprob_algebra)
-
-    interpret pair_subprob_space "f x" "g x" ..
-    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
-    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
-      using fx gx by (simp add: space_subprob_algebra)
-
-    have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B"
-      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
-    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
-              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
-      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
-    hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L - A) =
-                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
-      using emeasure_compl[OF _ P.emeasure_finite]
-      unfolding sets_eq
-      unfolding sets_eq_imp_space_eq[OF sets_eq]
-      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
-    note 1 2 sets_eq }
-  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
-
-  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
-  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
-    using Int_stable_pair_measure_generator pair_measure_closed A
-    unfolding sets_pair_measure
-  proof (induct A rule: sigma_sets_induct_disjoint)
-    case (basic A) then show ?case
-      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
-         (auto intro!: measurable_emeasure_kernel f g)
-  next
-    case (compl A)
-    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
-      by (auto simp: sets_pair_measure)
-    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
-                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
-      using compl(2) f g by measurable
-    thus ?case by (simp add: Compl A cong: measurable_cong)
-  next
-    case (union A)
-    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
-      by (auto simp: sets_pair_measure)
-    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
-      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
-      by (intro measurable_cong suminf_emeasure[symmetric])
-         (auto simp: sets_eq)
-    also have "\<dots>"
-      using union by auto
-    finally show ?case .
-  qed simp
-qed
-
-(* TODO: Move *)
-lemma measurable_distr2:
-  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
-  assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
-  shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
-proof -
-  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
-    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
-  proof (rule measurable_cong)
-    fix x assume x: "x \<in> space L"
-    have gx: "g x \<in> space (subprob_algebra M)"
-      using measurable_space[OF g x] .
-    then have [simp]: "sets (g x) = sets M"
-      by (simp add: space_subprob_algebra)
-    then have [simp]: "space (g x) = space M"
-      by (rule sets_eq_imp_space_eq)
-    let ?R = "return L x"
-    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
-      by simp
-    interpret subprob_space "g x"
-      using gx by (simp add: space_subprob_algebra)
-    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
-      by (simp add: space_pair_measure)
-    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
-    proof (rule measure_eqI)
-      show "sets ?l = sets ?r"
-        by simp
-    next
-      fix A assume "A \<in> sets ?l"
-      then have A[measurable]: "A \<in> sets N"
-        by simp
-      then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) -` A \<inter> space (?R \<Otimes>\<^sub>M g x))"
-        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
-      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
-        apply (subst emeasure_pair_measure_alt)
-        apply (rule measurable_sets[OF _ A])
-        apply (auto simp add: f_M' cong: measurable_cong_sets)
-        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
-        apply (auto simp: space_subprob_algebra space_pair_measure)
-        done
-      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
-        by (subst nn_integral_return)
-           (auto simp: x intro!: measurable_emeasure)
-      also have "\<dots> = emeasure ?l A"
-        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
-      finally show "emeasure ?l A = emeasure ?r A" ..
-    qed
-  qed
-  also have "\<dots>"
-    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
-    apply (rule return_measurable)
-    apply measurable
-    done
-  finally show ?thesis .
-qed
-
-(* END TODO *)
-
-lemma measurable_bind':
-  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
-          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
-  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
-proof (subst measurable_cong)
-  fix x assume x_in_M: "x \<in> space M"
-  with assms have "space (f x) \<noteq> {}" 
-      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
-  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
-      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
-         (auto dest: measurable_Pair2)
-  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
-      by (simp_all add: bind_nonempty'')
-next
-  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
-    apply (rule measurable_compose[OF _ measurable_join])
-    apply (rule measurable_distr2[OF M2 M1])
-    done
-qed
-
-lemma measurable_bind:
-  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
-          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
-  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
-  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
-
-lemma measurable_bind2:
-  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
-  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
-    using assms by (intro measurable_bind' measurable_const) auto
-
-lemma subprob_space_bind:
-  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
-  shows "subprob_space (M \<guillemotright>= f)"
-proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
-  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
-    by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
-        rule measurable_compose[OF measurable_snd assms(2)])
-  from assms(1) show "M \<in> space (subprob_algebra M)"
-    by (simp add: space_subprob_algebra)
-qed
-
 lemma double_bind_assoc:
   assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   assumes Mf: "f \<in> measurable M (subprob_algebra M')"
@@ -817,6 +1076,45 @@
   finally show ?thesis ..
 qed
 
+lemma (in pair_prob_space) pair_measure_eq_bind:
+  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
+proof (rule measure_eqI)
+  have ps_M2: "prob_space M2" by unfold_locales
+  note return_measurable[measurable]
+  have 1: "(\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))) \<in> measurable M1 (subprob_algebra (M1 \<Otimes>\<^sub>M M2))"
+    by (auto simp add: space_subprob_algebra ps_M2
+             intro!: measurable_bind[where N=M2] measurable_const prob_space_imp_subprob_space)
+  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
+    by (simp add: M1.not_empty sets_bind[OF 1])
+  fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
+  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
+    by (auto simp: M2.emeasure_pair_measure emeasure_bind[OF _ 1] M1.not_empty
+                          emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] M2.not_empty
+             intro!: nn_integral_cong)
+qed
+
+lemma (in pair_prob_space) bind_rotate:
+  assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)"
+  shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
+proof - 
+  interpret swap: pair_prob_space M2 M1 by unfold_locales
+  note measurable_bind[where N="M2", measurable]
+  note measurable_bind[where N="M1", measurable]
+  have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)"
+    by (auto simp: space_subprob_algebra) unfold_locales
+  have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = 
+    (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)"
+    by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N])
+  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)"
+    unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] ..
+  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)"
+    unfolding swap.pair_measure_eq_bind[symmetric]
+    by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong)
+  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
+    by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N])
+  finally show ?thesis .
+qed
+
 section {* Measures form a $\omega$-chain complete partial order *}
 
 definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where

--- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -28,6 +28,10 @@
   apply auto
   done
 
+lemma (in prob_space) indep_eventsI:
+  "(\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M) \<Longrightarrow> (\<And>J. J \<subseteq> I \<Longrightarrow> finite J \<Longrightarrow> J \<noteq> {} \<Longrightarrow> prob (\<Inter>i\<in>J. F i) = (\<Prod>i\<in>J. prob (F i))) \<Longrightarrow> indep_events F I"
+  by (auto simp: indep_events_def)
+
 definition (in prob_space)
   "indep_event A B \<longleftrightarrow> indep_events (case_bool A B) UNIV"
 
@@ -380,6 +384,25 @@
     by (rule indep_sets_mono_sets) (auto split: bool.split)
 qed
 
+lemma (in prob_space) indep_eventsI_indep_vars:
+  assumes indep: "indep_vars N X I"
+  assumes P: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space (N i). P i x} \<in> sets (N i)"
+  shows "indep_events (\<lambda>i. {x\<in>space M. P i (X i x)}) I"
+proof -
+  have "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (N i)}) I"
+    using indep unfolding indep_vars_def2 by auto
+  then show ?thesis
+    unfolding indep_events_def_alt
+  proof (rule indep_sets_mono_sets)
+    fix i assume "i \<in> I"
+    then have "{{x \<in> space M. P i (X i x)}} = {X i -` {x\<in>space (N i). P i x} \<inter> space M}"
+      using indep by (auto simp: indep_vars_def dest: measurable_space)
+    also have "\<dots> \<subseteq> {X i -` A \<inter> space M |A. A \<in> sets (N i)}"
+      using P[OF `i \<in> I`] by blast
+    finally show "{{x \<in> space M. P i (X i x)}} \<subseteq> {X i -` A \<inter> space M |A. A \<in> sets (N i)}" .
+  qed
+qed                              
+
 lemma (in prob_space) indep_sets_collect_sigma:
   fixes I :: "'j \<Rightarrow> 'i set" and J :: "'j set" and E :: "'i \<Rightarrow> 'a set set"
   assumes indep: "indep_sets E (\<Union>j\<in>J. I j)"
@@ -774,6 +797,23 @@
   qed
 qed
 
+lemma (in prob_space) borel_0_1_law_AE:
+  fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> bool"
+  assumes "indep_events (\<lambda>m. {x\<in>space M. P m x}) UNIV" (is "indep_events ?P _")
+  shows "(AE x in M. infinite {m. P m x}) \<or> (AE x in M. finite {m. P m x})"
+proof -
+  have [measurable]: "\<And>m. {x\<in>space M. P m x} \<in> sets M"
+    using assms by (auto simp: indep_events_def)
+  have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
+    by (rule borel_0_1_law) fact
+  also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<longleftrightarrow> (AE x in M. finite {m. P m x})"
+    by (subst prob_eq_0) (auto simp add: finite_nat_iff_bounded Ball_def not_less[symmetric])
+  also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
+    by (subst prob_eq_1) (simp_all add: Bex_def infinite_nat_iff_unbounded_le)
+  finally show ?thesis
+    by metis
+qed
+
 lemma (in prob_space) indep_sets_finite:
   assumes I: "I \<noteq> {}" "finite I"
     and F: "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> events" "\<And>i. i \<in> I \<Longrightarrow> space M \<in> F i"

--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -425,6 +425,13 @@
   finally show "emeasure (PiM I M) X = emeasure M' X" ..
 qed
 
+lemma (in product_prob_space) AE_component: "i \<in> I \<Longrightarrow> AE x in M i. P x \<Longrightarrow> AE x in PiM I M. P (x i)"
+  apply (rule AE_distrD[of "\<lambda>\<omega>. \<omega> i" "PiM I M" "M i" P])
+  apply simp
+  apply (subst PiM_component)
+  apply simp_all
+  done
+
 subsection {* Sequence space *}
 
 definition comb_seq :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" where

--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1193,8 +1193,6 @@
       using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
     show "\<And>i. (?f i) \<in> borel_measurable lborel"
       using f_borel by auto
-    show "\<And>i x. 0 \<le> ?f i x"
-      using nonneg by (auto split: split_indicator)
   qed
   also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
     by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto

--- a/src/HOL/Probability/Measurable.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -198,6 +198,14 @@
     by (simp add: eq_commute)
 qed
 
+lemma pred_count_space_const1[measurable (raw)]:
+  "f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. f x = c)"
+  by (intro pred_eq_const1[where N="count_space UNIV"]) (auto )
+
+lemma pred_count_space_const2[measurable (raw)]:
+  "f \<in> measurable M (count_space UNIV) \<Longrightarrow> Measurable.pred M (\<lambda>x. c = f x)"
+  by (intro pred_eq_const2[where N="count_space UNIV"]) (auto )
+
 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]
@@ -335,6 +343,9 @@
   "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   by simp
 
+lemma sets_UNIV [measurable (raw)]: "A \<in> sets (count_space UNIV)"
+  by simp
+
 lemma measurable_card[measurable]:
   fixes S :: "'a \<Rightarrow> nat set"
   assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
@@ -394,6 +405,187 @@
   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
+
+lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
+  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)"
+proof -
+  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. False) s x)"
+      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)"
+    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
+  finally show ?thesis .
+qed
+
+lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
+  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)"
+proof -
+  { fix i from `P M s` have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>t x. True) s x)"
+      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)"
+    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
+  finally show ?thesis .
+qed
+
+lemma measurable_enat_coinduct:
+  fixes f :: "'a \<Rightarrow> enat"
+  assumes "R f"
+  assumes *: "\<And>f. R f \<Longrightarrow> \<exists>g h i P. R g \<and> f = (\<lambda>x. if P x then h x else eSuc (g (i x))) \<and> 
+    Measurable.pred M P \<and>
+    i \<in> measurable M M \<and>
+    h \<in> measurable M (count_space UNIV)"
+  shows "f \<in> measurable M (count_space UNIV)"
+proof (simp add: measurable_count_space_eq2_countable, rule )
+  fix a :: enat
+  have "f -` {a} \<inter> space M = {x\<in>space M. f x = a}"
+    by auto
+  { fix i :: nat
+    from `R f` have "Measurable.pred M (\<lambda>x. f x = enat i)"
+    proof (induction i arbitrary: f)
+      case 0
+      from *[OF this] obtain g h i P
+        where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and
+          [measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
+        by auto
+      have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)"
+        by measurable
+      also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)"
+        by (auto simp: f zero_enat_def[symmetric])
+      finally show ?case .
+    next
+      case (Suc n)
+      from *[OF Suc.prems] obtain g h i P
+        where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and
+          M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
+        by auto
+      have "(\<lambda>x. f x = enat (Suc n)) =
+        (\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))"
+        by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric])
+      also have "Measurable.pred M \<dots>"
+        by (intro pred_intros_logic measurable_compose[OF M(2)] Suc `R g`) measurable
+      finally show ?case .
+    qed
+    then have "f -` {enat i} \<inter> space M \<in> sets M"
+      by (simp add: pred_def Int_def conj_commute) }
+  note fin = this
+  show "f -` {a} \<inter> space M \<in> sets M"
+  proof (cases a)
+    case infinity
+    then have "f -` {a} \<inter> space M = space M - (\<Union>n. f -` {enat n} \<inter> space M)"
+      by auto
+    also have "\<dots> \<in> sets M"
+      by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin)
+    finally show ?thesis .
+  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)"
+  assumes I[simp]: "countable I" "\<And>i x. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> i \<in> I"
+  assumes unique: "\<And>x i j. x \<in> space M \<Longrightarrow> P i x \<Longrightarrow> P j x \<Longrightarrow> i = j"
+  shows "(\<lambda>x. THE i. P i x) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_def
+proof safe
+  fix X
+  def f \<equiv> "\<lambda>x. THE i. P i x" def undef \<equiv> "THE i::'a. False"
+  { fix i x assume "x \<in> space M" "P i x" then have "f x = i"
+      unfolding f_def using unique by auto }
+  note f_eq = this
+  { fix x assume "x \<in> space M" "\<forall>i\<in>I. \<not> P i x"
+    then have "\<And>i. \<not> P i x"
+      using I(2)[of x] by auto
+    then have "f x = undef"
+      by (auto simp: undef_def f_def) }
+  then have "f -` X \<inter> space M = (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union>
+     (if undef \<in> X then space M - (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})"
+    by (auto dest: f_eq)
+  also have "\<dots> \<in> sets M"
+    by (auto intro!: sets.Diff sets.countable_UN')
+  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)"
+  unfolding bex1_def by measurable
+
+lemma measurable_split_if[measurable (raw)]:
+  "(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow>
+   Measurable.pred M (if c then f else g)"
+  by simp
+
+lemma pred_restrict_space:
+  assumes "S \<in> sets M"
+  shows "Measurable.pred (restrict_space M S) P \<longleftrightarrow> Measurable.pred M (\<lambda>x. x \<in> S \<and> P x)"
+  unfolding pred_def sets_Collect_restrict_space_iff[OF assms] ..
+
+lemma measurable_predpow[measurable]:
+  assumes "Measurable.pred M T"
+  assumes "\<And>Q. Measurable.pred M Q \<Longrightarrow> Measurable.pred M (R Q)"
+  shows "Measurable.pred M ((R ^^ n) T)"
+  by (induct n) (auto intro: assms)
+
 hide_const (open) pred
 
 end

--- a/src/HOL/Probability/Measure_Space.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -422,7 +422,10 @@
 
 lemma emeasure_less_0_iff: "emeasure M A < 0 \<longleftrightarrow> False"
   using emeasure_nonneg[of M A] by auto
-  
+
+lemma emeasure_single_in_space: "emeasure M {x} \<noteq> 0 \<Longrightarrow> x \<in> space M"
+  using emeasure_notin_sets[of "{x}" M] by (auto dest: sets.sets_into_space)
+
 lemma emeasure_countably_additive: "countably_additive (sets M) (emeasure M)"
   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
 
@@ -545,6 +548,32 @@
   using LIMSEQ_INF[OF decseq_emeasure, OF A]
   using INF_emeasure_decseq[OF A fin] by simp
 
+lemma emeasure_lfp[consumes 1, case_names cont measurable]:
+  assumes "P M"
+  assumes cont: "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 "emeasure M {x\<in>space M. lfp F x} = (SUP i. emeasure M {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
+proof -
+  have "emeasure M {x\<in>space M. lfp F x} = emeasure M (\<Union>i. {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
+    using continuous_lfp[OF cont] by (auto simp add: bot_fun_def intro!: arg_cong2[where f=emeasure])
+  moreover { fix i from `P M` have "{x\<in>space M. (F ^^ i) (\<lambda>x. False) x} \<in> sets M"
+    by (induct i arbitrary: M) (auto simp add: pred_def[symmetric] intro: *) }
+  moreover have "incseq (\<lambda>i. {x\<in>space M. (F ^^ i) (\<lambda>x. False) x})"
+  proof (rule incseq_SucI)
+    fix i
+    have "(F ^^ i) (\<lambda>x. False) \<le> (F ^^ (Suc i)) (\<lambda>x. False)"
+    proof (induct i)
+      case 0 show ?case by (simp add: le_fun_def)
+    next
+      case Suc thus ?case using monoD[OF continuous_mono[OF cont] Suc] by auto
+    qed
+    then show "{x \<in> space M. (F ^^ i) (\<lambda>x. False) x} \<subseteq> {x \<in> space M. (F ^^ Suc i) (\<lambda>x. False) x}"
+      by auto
+  qed
+  ultimately show ?thesis
+    by (subst SUP_emeasure_incseq) auto
+qed
+
 lemma emeasure_subadditive:
   assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
   shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
@@ -997,6 +1026,25 @@
     unfolding eventually_ae_filter by auto
 qed auto
 
+lemma AE_ball_countable: 
+  assumes [intro]: "countable X"
+  shows "(AE x in M. \<forall>y\<in>X. P x y) \<longleftrightarrow> (\<forall>y\<in>X. AE x in M. P x y)"
+proof
+  assume "\<forall>y\<in>X. AE x in M. P x y"
+  from this[unfolded eventually_ae_filter Bex_def, THEN bchoice]
+  obtain N where N: "\<And>y. y \<in> X \<Longrightarrow> N y \<in> null_sets M" "\<And>y. y \<in> X \<Longrightarrow> {x\<in>space M. \<not> P x y} \<subseteq> N y"
+    by auto
+  have "{x\<in>space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. {x\<in>space M. \<not> P x y})"
+    by auto
+  also have "\<dots> \<subseteq> (\<Union>y\<in>X. N y)"
+    using N by auto
+  finally have "{x\<in>space M. \<not> (\<forall>y\<in>X. P x y)} \<subseteq> (\<Union>y\<in>X. N y)" .
+  moreover from N have "(\<Union>y\<in>X. N y) \<in> null_sets M"
+    by (intro null_sets_UN') auto
+  ultimately show "AE x in M. \<forall>y\<in>X. P x y"
+    unfolding eventually_ae_filter by auto
+qed auto
+
 lemma AE_discrete_difference:
   assumes X: "countable X"
   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" 
@@ -1041,6 +1089,15 @@
   shows "emeasure M A = emeasure M B"
   using assms by (safe intro!: antisym emeasure_mono_AE) auto
 
+lemma emeasure_Collect_eq_AE:
+  "AE x in M. P x \<longleftrightarrow> Q x \<Longrightarrow> Measurable.pred M Q \<Longrightarrow> Measurable.pred M P \<Longrightarrow>
+   emeasure M {x\<in>space M. P x} = emeasure M {x\<in>space M. Q x}"
+   by (intro emeasure_eq_AE) auto
+
+lemma emeasure_eq_0_AE: "AE x in M. \<not> P x \<Longrightarrow> emeasure M {x\<in>space M. P x} = 0"
+  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"]
+  by (cases "{x\<in>space M. P x} \<in> sets M") (simp_all add: emeasure_notin_sets)
+
 subsection {* @{text \<sigma>}-finite Measures *}
 
 locale sigma_finite_measure =
@@ -1162,6 +1219,42 @@
   show "sigma_algebra (space N) (sets N)" ..
 qed fact
 
+lemma emeasure_Collect_distr:
+  assumes X[measurable]: "X \<in> measurable M N" "Measurable.pred N P"
+  shows "emeasure (distr M N X) {x\<in>space N. P x} = emeasure M {x\<in>space M. P (X x)}"
+  by (subst emeasure_distr)
+     (auto intro!: arg_cong2[where f=emeasure] X(1)[THEN measurable_space])
+
+lemma emeasure_lfp2[consumes 1, case_names cont f measurable]:
+  assumes "P M"
+  assumes cont: "Order_Continuity.continuous F"
+  assumes f: "\<And>M. P M \<Longrightarrow> f \<in> measurable M' M"
+  assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
+  shows "emeasure M' {x\<in>space M'. lfp F (f x)} = (SUP i. emeasure M' {x\<in>space M'. (F ^^ i) (\<lambda>x. False) (f x)})"
+proof (subst (1 2) emeasure_Collect_distr[symmetric, where X=f])
+  show "f \<in> measurable M' M"  "f \<in> measurable M' M"
+    using f[OF `P M`] by auto
+  { fix i show "Measurable.pred M ((F ^^ i) (\<lambda>x. False))"
+    using `P M` by (induction i arbitrary: M) (auto intro!: *) }
+  show "Measurable.pred M (lfp F)"
+    using `P M` cont * by (rule measurable_lfp_coinduct[of P])
+
+  have "emeasure (distr M' M f) {x \<in> space (distr M' M f). lfp F x} =
+    (SUP i. emeasure (distr M' M f) {x \<in> space (distr M' M f). (F ^^ i) (\<lambda>x. False) x})"
+    using `P M`
+  proof (coinduction arbitrary: M rule: emeasure_lfp)
+    case (measurable A N) then have "\<And>N. P N \<Longrightarrow> Measurable.pred (distr M' N f) A"
+      by metis
+    then have "\<And>N. P N \<Longrightarrow> Measurable.pred N A"
+      by simp
+    with `P N`[THEN *] show ?case
+      by auto
+  qed fact
+  then show "emeasure (distr M' M f) {x \<in> space M. lfp F x} =
+    (SUP i. emeasure (distr M' M f) {x \<in> space M. (F ^^ i) (\<lambda>x. False) x})"
+   by simp
+qed
+
 lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
   by (rule measure_eqI) (auto simp: emeasure_distr)
 
@@ -1217,6 +1310,9 @@
 lemma measure_nonneg: "0 \<le> measure M A"
   using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
 
+lemma measure_le_0_iff: "measure M X \<le> 0 \<longleftrightarrow> measure M X = 0"
+  using measure_nonneg[of M X] by auto
+
 lemma measure_empty[simp]: "measure M {} = 0"
   unfolding measure_def by simp
 
@@ -1781,5 +1877,38 @@
              intro!: measurable_restrict_space2)
 qed (simp add: sets_restrict_space)
 
+lemma measure_eqI_restrict_generator:
+  assumes E: "Int_stable E" "E \<subseteq> Pow \<Omega>" "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X"
+  assumes sets_eq: "sets M = sets N" and \<Omega>: "\<Omega> \<in> sets M"
+  assumes "sets (restrict_space M \<Omega>) = sigma_sets \<Omega> E"
+  assumes "sets (restrict_space N \<Omega>) = sigma_sets \<Omega> E" 
+  assumes ae: "AE x in M. x \<in> \<Omega>" "AE x in N. x \<in> \<Omega>"
+  assumes A: "countable A" "A \<noteq> {}" "A \<subseteq> E" "\<Union>A = \<Omega>" "\<And>a. a \<in> A \<Longrightarrow> emeasure M a \<noteq> \<infinity>"
+  shows "M = N"
+proof (rule measure_eqI)
+  fix X assume X: "X \<in> sets M"
+  then have "emeasure M X = emeasure (restrict_space M \<Omega>) (X \<inter> \<Omega>)"
+    using ae \<Omega> by (auto simp add: emeasure_restrict_space intro!: emeasure_eq_AE)
+  also have "restrict_space M \<Omega> = restrict_space N \<Omega>"
+  proof (rule measure_eqI_generator_eq)
+    fix X assume "X \<in> E"
+    then show "emeasure (restrict_space M \<Omega>) X = emeasure (restrict_space N \<Omega>) X"
+      using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
+  next
+    show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
+      unfolding Sup_image_eq[symmetric, where f="from_nat_into A"] using A by auto
+  next
+    fix i
+    have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
+      using A \<Omega> by (subst emeasure_restrict_space)
+                   (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq] intro: from_nat_into)
+    with A show "emeasure (restrict_space M \<Omega>) (from_nat_into A i) \<noteq> \<infinity>"
+      by (auto intro: from_nat_into)
+  qed fact+
+  also have "emeasure (restrict_space N \<Omega>) (X \<inter> \<Omega>) = emeasure N X"
+    using X ae \<Omega> by (auto simp add: emeasure_restrict_space sets_eq intro!: emeasure_eq_AE)
+  finally show "emeasure M X = emeasure N X" .
+qed fact
+
 end
 

--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -967,25 +967,35 @@
     by (auto intro!: incseq_SucI nn_integral_mono)
 qed
 
+lemma nn_integral_max_0: "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>N M f"
+  by (simp add: le_fun_def nn_integral_def)
+
 text {* Beppo-Levi monotone convergence theorem *}
 lemma nn_integral_monotone_convergence_SUP:
-  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
+  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M"
   shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))"
 proof (rule antisym)
   show "(SUP j. integral\<^sup>N M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)"
     by (auto intro!: SUP_least SUP_upper nn_integral_mono)
 next
-  show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>N M (f j))"
-    unfolding nn_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
+  have f': "incseq (\<lambda>i x. max 0 (f i x))"
+    using f by (auto simp: incseq_def le_fun_def not_le split: split_max)
+               (blast intro: order_trans less_imp_le)
+  have "(\<integral>\<^sup>+ x. max 0 (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. max 0 (f i x)) \<partial>M)"
+    unfolding sup_max[symmetric] Complete_Lattices.SUP_sup_distrib[symmetric] by simp
+  also have "\<dots> \<le> (SUP i. (\<integral>\<^sup>+ x. max 0 (f i x) \<partial>M))"
+    unfolding nn_integral_def_finite[of _ "\<lambda>x. SUP i. max 0 (f i x)"]
   proof (safe intro!: SUP_least)
     fix g assume g: "simple_function M g"
-      and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
-    then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
+      and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. max 0 (f i x))" "range g \<subseteq> {0..<\<infinity>}"
+    then have "\<And>x. 0 \<le> (SUP i. max 0 (f i x))" and g': "g`space M \<subseteq> {0..<\<infinity>}"
       using f by (auto intro!: SUP_upper2)
-    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>N M (f j))"
-      by (intro  nn_integral_SUP_approx[OF f g _ g'])
-         (auto simp: le_fun_def max_def)
+    with * show "integral\<^sup>S M g \<le> (SUP j. \<integral>\<^sup>+x. max 0 (f j x) \<partial>M)"
+      by (intro nn_integral_SUP_approx[OF f' _ _ g _ g'])
+         (auto simp: le_fun_def max_def intro!: measurable_If f borel_measurable_le)
   qed
+  finally show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>N M (f j))"
+    unfolding nn_integral_max_0 .
 qed
 
 lemma nn_integral_monotone_convergence_SUP_AE:
@@ -1003,9 +1013,7 @@
   proof (rule nn_integral_monotone_convergence_SUP)
     show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
     { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
-        using f N(3) by (intro measurable_If_set) auto
-      fix x show "0 \<le> ?f i x"
-        using N(1) by auto }
+        using f N(3) by (intro measurable_If_set) auto }
   qed
   also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
     using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext)
@@ -1023,13 +1031,9 @@
   assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
   shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   using assms unfolding nn_integral_monotone_convergence_SUP[OF f(1)
-    f(3)[THEN borel_measurable_simple_function] f(2)]
+    f(3)[THEN borel_measurable_simple_function]]
   by (auto intro!: nn_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
 
-lemma nn_integral_max_0:
-  "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>N M f"
-  by (simp add: le_fun_def nn_integral_def)
-
 lemma nn_integral_cong_pos:
   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
   shows "integral\<^sup>N M f = integral\<^sup>N M g"
@@ -1134,6 +1138,15 @@
   shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
   unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
 
+lemma nn_integral_divide:
+  "0 < c \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+x. f x / c \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M) / c"
+  unfolding divide_ereal_def
+  apply (rule nn_integral_multc)
+  apply assumption
+  apply (cases c)
+  apply auto
+  done
+
 lemma nn_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"
   by (subst nn_integral_eq_simple_integral)
@@ -1550,6 +1563,28 @@
   by (subst nn_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
     sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
 
+lemma nn_integral_less:
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  assumes f: "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) \<noteq> \<infinity>"
+  assumes ord: "AE x in M. f x \<le> g x" "\<not> (AE x in M. g x \<le> f x)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>M) < (\<integral>\<^sup>+x. g x \<partial>M)"
+proof -
+  have "0 < (\<integral>\<^sup>+x. g x - f x \<partial>M)"
+  proof (intro order_le_neq_trans nn_integral_nonneg notI)
+    assume "0 = (\<integral>\<^sup>+x. g x - f x \<partial>M)"
+    then have "AE x in M. g x - f x \<le> 0"
+      using nn_integral_0_iff_AE[of "\<lambda>x. g x - f x" M] by simp
+    with f(1) ord(1) have "AE x in M. g x \<le> f x"
+      by eventually_elim (auto simp: ereal_minus_le_iff)
+    with ord show False
+      by simp
+  qed
+  also have "\<dots> = (\<integral>\<^sup>+x. g x \<partial>M) - (\<integral>\<^sup>+x. f x \<partial>M)"
+    by (subst nn_integral_diff) (auto simp: f ord)
+  finally show ?thesis
+    by (simp add: ereal_less_minus_iff f nn_integral_nonneg)
+qed
+
 lemma nn_integral_const_If:
   "(\<integral>\<^sup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
   by (auto intro!: nn_integral_0_iff_AE[THEN iffD2])
@@ -1658,6 +1693,30 @@
   by (subst nn_integral_max_0[symmetric])
      (auto intro!: setsum.mono_neutral_left simp: nn_integral_count_space less_le)
 
+lemma nn_integral_count_space':
+  assumes "finite A" "\<And>x. x \<in> B \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = 0" "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "A \<subseteq> B"
+  shows "(\<integral>\<^sup>+x. f x \<partial>count_space B) = (\<Sum>x\<in>A. f x)"
+proof -
+  have "(\<integral>\<^sup>+x. f x \<partial>count_space B) = (\<Sum>a | a \<in> B \<and> 0 < f a. f a)"
+    using assms(2,3)
+    by (intro nn_integral_count_space finite_subset[OF _ `finite A`]) (auto simp: less_le)
+  also have "\<dots> = (\<Sum>a\<in>A. f a)"
+    using assms by (intro setsum.mono_neutral_cong_left) (auto simp: less_le)
+  finally show ?thesis .
+qed
+
+lemma nn_integral_indicator_finite:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes f: "finite A" and nn: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" and [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"
+  shows "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<Sum>x\<in>A. f x * emeasure M {x})"
+proof -
+  from f have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
+    by (intro nn_integral_cong) (auto simp: indicator_def if_distrib[where f="\<lambda>a. x * a" for x] setsum.If_cases)
+  also have "\<dots> = (\<Sum>a\<in>A. f a * emeasure M {a})"
+    using nn by (subst nn_integral_setsum) (auto simp: nn_integral_cmult_indicator)
+  finally show ?thesis .
+qed
+
 lemma emeasure_UN_countable:
   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I: "countable I" 
   assumes disj: "disjoint_family_on X I"
@@ -1760,6 +1819,26 @@
     by simp
 qed simp
 
+lemma measure_eqI_countable_AE:
+  assumes [simp]: "sets M = UNIV" "sets N = UNIV"
+  assumes ae: "AE x in M. x \<in> \<Omega>" "AE x in N. x \<in> \<Omega>" and [simp]: "countable \<Omega>"
+  assumes eq: "\<And>x. x \<in> \<Omega> \<Longrightarrow> emeasure M {x} = emeasure N {x}"
+  shows "M = N"
+proof (rule measure_eqI)
+  fix A
+  have "emeasure N A = emeasure N {x\<in>\<Omega>. x \<in> A}"
+    using ae by (intro emeasure_eq_AE) auto
+  also have "\<dots> = (\<integral>\<^sup>+x. emeasure N {x} \<partial>count_space {x\<in>\<Omega>. x \<in> A})"
+    by (intro emeasure_countable_singleton) auto
+  also have "\<dots> = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space {x\<in>\<Omega>. x \<in> A})"
+    by (intro nn_integral_cong eq[symmetric]) auto
+  also have "\<dots> = emeasure M {x\<in>\<Omega>. x \<in> A}"
+    by (intro emeasure_countable_singleton[symmetric]) auto
+  also have "\<dots> = emeasure M A"
+    using ae by (intro emeasure_eq_AE) auto
+  finally show "emeasure M A = emeasure N A" ..
+qed simp
+
 subsubsection {* Measures with Restricted Space *}
 
 lemma simple_function_iff_borel_measurable:
@@ -1860,6 +1939,11 @@
     unfolding nn_integral_def_finite SUP_def by simp
 qed
 
+lemma nn_integral_count_space_indicator:
+  assumes "NO_MATCH (X::'a set) (UNIV::'a set)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
+  by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
+
 subsubsection {* Measure spaces with an associated density *}
 
 definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
@@ -2052,7 +2136,7 @@
   by (auto simp: nn_integral_cmult_indicator emeasure_density)
 
 lemma measure_density_const:
-  "A \<in> sets M \<Longrightarrow> 0 < c \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> measure (density M (\<lambda>_. c)) A = real c * measure M A"
+  "A \<in> sets M \<Longrightarrow> 0 \<le> c \<Longrightarrow> c \<noteq> \<infinity> \<Longrightarrow> measure (density M (\<lambda>_. c)) A = real c * measure M A"
   by (auto simp: emeasure_density_const measure_def)
 
 lemma density_density_eq:
@@ -2194,6 +2278,55 @@
   "A \<in> sets M \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> P x) \<Longrightarrow> (AE x in uniform_measure M A. P x)"
   unfolding uniform_measure_def by (auto simp: AE_density)
 
+lemma emeasure_uniform_measure_1:
+  "emeasure M S \<noteq> 0 \<Longrightarrow> emeasure M S \<noteq> \<infinity> \<Longrightarrow> emeasure (uniform_measure M S) S = 1"
+  by (subst emeasure_uniform_measure)
+     (simp_all add: emeasure_nonneg emeasure_neq_0_sets)
+
+lemma nn_integral_uniform_measure:
+  assumes f[measurable]: "f \<in> borel_measurable M" and "\<And>x. 0 \<le> f x" and S[measurable]: "S \<in> sets M"
+  shows "(\<integral>\<^sup>+x. f x \<partial>uniform_measure M S) = (\<integral>\<^sup>+x. f x * indicator S x \<partial>M) / emeasure M S"
+proof -
+  { assume "emeasure M S = \<infinity>"
+    then have ?thesis
+      by (simp add: uniform_measure_def nn_integral_density f) }
+  moreover
+  { assume [simp]: "emeasure M S = 0"
+    then have ae: "AE x in M. x \<notin> S"
+      using sets.sets_into_space[OF S]
+      by (subst AE_iff_measurable[OF _ refl]) (simp_all add: subset_eq cong: rev_conj_cong)
+    from ae have "(\<integral>\<^sup>+ x. indicator S x * f x / 0 \<partial>M) = 0"
+      by (subst nn_integral_0_iff_AE) auto
+    moreover from ae have "(\<integral>\<^sup>+ x. f x * indicator S x \<partial>M) = 0"
+      by (subst nn_integral_0_iff_AE) auto
+    ultimately have ?thesis
+      by (simp add: uniform_measure_def nn_integral_density f) }
+  moreover
+  { assume "emeasure M S \<noteq> 0" "emeasure M S \<noteq> \<infinity>"
+    moreover then have "0 < emeasure M S"
+      by (simp add: emeasure_nonneg less_le)
+    ultimately have ?thesis
+      unfolding uniform_measure_def
+      apply (subst nn_integral_density)
+      apply (auto simp: f nn_integral_divide intro!: zero_le_divide_ereal)
+      apply (simp add: mult.commute)
+      done }
+  ultimately show ?thesis by blast
+qed
+
+lemma AE_uniform_measure:
+  assumes "emeasure M A \<noteq> 0" "emeasure M A < \<infinity>"
+  shows "(AE x in uniform_measure M A. P x) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> P x)"
+proof -
+  have "A \<in> sets M"
+    using `emeasure M A \<noteq> 0` by (metis emeasure_notin_sets)
+  moreover have "\<And>x. 0 < indicator A x / emeasure M A \<longleftrightarrow> x \<in> A"
+    using emeasure_nonneg[of M A] assms
+    by (cases "emeasure M A") (auto split: split_indicator simp: one_ereal_def)
+  ultimately show ?thesis
+    unfolding uniform_measure_def by (simp add: AE_density)
+qed
+
 subsubsection {* Uniform count measure *}
 
 definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"

--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1,41 +1,85 @@
 (*  Title:      HOL/Probability/Probability_Mass_Function.thy
     Author:     Johannes Hölzl, TU München *)
 
+section \<open> Probability mass function \<close>
+
 theory Probability_Mass_Function
-  imports Probability_Measure
+imports
+  Giry_Monad
+  "~~/src/HOL/Library/Multiset"
 begin
 
-lemma (in prob_space) countable_support:
+lemma (in finite_measure) countable_support: (* replace version in pmf *)
   "countable {x. measure M {x} \<noteq> 0}"
-proof -
-  let ?m = "\<lambda>x. measure M {x}"
-  have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. inverse (real (Suc n)) < ?m x})"
-    by (auto intro!: measure_nonneg reals_Archimedean order_le_neq_trans)
-  have **: "\<And>n. finite {x. inverse (Suc n) < ?m x}"
+proof cases
+  assume "measure M (space M) = 0"
+  with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}"
+    by auto
+  then show ?thesis
+    by simp
+next
+  let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}"
+  assume "?M \<noteq> 0"
+  then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})"
+    using reals_Archimedean[of "?m x / ?M" for x]
+    by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
+  have **: "\<And>n. finite {x. ?M / Suc n < ?m x}"
   proof (rule ccontr)
-    fix n assume "infinite {x. inverse (Suc n) < ?m x}" (is "infinite ?X")
+    fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
     then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
       by (metis infinite_arbitrarily_large)
-    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> 1 / Suc n \<le> ?m x" 
-      by (auto simp: inverse_eq_divide)
+    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x" 
+      by auto
     { fix x assume "x \<in> X"
-      from *[OF this] have "?m x \<noteq> 0" by auto
+      from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
       then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
     note singleton_sets = this
-    have "1 < (\<Sum>x\<in>X. 1 / Suc n)"
-      by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc)
+    have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
+      using `?M \<noteq> 0` 
+      by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg)
     also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
       by (rule setsum_mono) fact
     also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
       using singleton_sets `finite X`
       by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
-    finally show False
-      using prob_le_1[of "\<Union>x\<in>X. {x}"] by arith
+    finally have "?M < measure M (\<Union>x\<in>X. {x})" .
+    moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M"
+      using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
+    ultimately show False by simp
   qed
   show ?thesis
     unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
 qed
 
+lemma (in finite_measure) AE_support_countable:
+  assumes [simp]: "sets M = UNIV"
+  shows "(AE x in M. measure M {x} \<noteq> 0) \<longleftrightarrow> (\<exists>S. countable S \<and> (AE x in M. x \<in> S))"
+proof
+  assume "\<exists>S. countable S \<and> (AE x in M. x \<in> S)"
+  then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \<in> S"
+    by auto
+  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) = 
+    (\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)"
+    by (subst emeasure_UN_countable)
+       (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
+  also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} * indicator S x \<partial>count_space UNIV)"
+    by (auto intro!: nn_integral_cong split: split_indicator)
+  also have "\<dots> = emeasure M (\<Union>x\<in>S. {x})"
+    by (subst emeasure_UN_countable)
+       (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
+  also have "\<dots> = emeasure M (space M)"
+    using ae by (intro emeasure_eq_AE) auto
+  finally have "emeasure M {x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0} = emeasure M (space M)"
+    by (simp add: emeasure_single_in_space cong: rev_conj_cong)
+  with finite_measure_compl[of "{x \<in> space M. x\<in>S \<and> emeasure M {x} \<noteq> 0}"]
+  have "AE x in M. x \<in> S \<and> emeasure M {x} \<noteq> 0"
+    by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure set_diff_eq cong: conj_cong)
+  then show "AE x in M. measure M {x} \<noteq> 0"
+    by (auto simp: emeasure_eq_measure)
+qed (auto intro!: exI[of _ "{x. measure M {x} \<noteq> 0}"] countable_support)
+
+subsection {* PMF as measure *}
+
 typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
   morphisms measure_pmf Abs_pmf
   by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
@@ -49,6 +93,9 @@
 interpretation measure_pmf!: prob_space "measure_pmf M" for M
   by (rule prob_space_measure_pmf)
 
+interpretation measure_pmf!: subprob_space "measure_pmf M" for M
+  by (rule prob_space_imp_subprob_space) unfold_locales
+
 locale pmf_as_measure
 begin
 
@@ -87,11 +134,14 @@
 declare [[coercion set_pmf]]
 
 lemma countable_set_pmf: "countable (set_pmf p)"
-  by transfer (metis prob_space.countable_support)
+  by transfer (metis prob_space.finite_measure finite_measure.countable_support)
 
 lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
   by transfer metis
 
+lemma sets_measure_pmf_count_space: "sets (measure_pmf M) = sets (count_space UNIV)"
+  by simp
+
 lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
   using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
 
@@ -107,6 +157,9 @@
 lemma pmf_nonneg: "0 \<le> pmf p x"
   by transfer (simp add: measure_nonneg)
 
+lemma pmf_le_1: "pmf p x \<le> 1"
+  by (simp add: pmf.rep_eq)
+
 lemma emeasure_pmf_single:
   fixes M :: "'a pmf"
   shows "emeasure M {x} = pmf M x"
@@ -131,34 +184,80 @@
     using AE_measure_pmf[of M] by auto
 qed
 
-lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)"
-proof (transfer, elim conjE)
-  fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0"
-  assume "prob_space M" then interpret prob_space M .
-  show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
-  proof (rule measure_eqI)
-    fix A :: "'a set"
-    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 
-      (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
-      by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
-    also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
-      by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space)
-    also have "\<dots> = emeasure M (\<Union>x\<in>(A \<inter> {x. measure M {x} \<noteq> 0}). {x})"
-      by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support)
-         (auto simp: disjoint_family_on_def)
-    also have "\<dots> = emeasure M A"
-      using ae by (intro emeasure_eq_AE) auto
-    finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))) A"
-      using emeasure_space_1 by (simp add: emeasure_density)
-  qed simp
-qed
-
 lemma set_pmf_not_empty: "set_pmf M \<noteq> {}"
   using AE_measure_pmf[of M] by (intro notI) simp
 
 lemma set_pmf_iff: "x \<in> set_pmf M \<longleftrightarrow> pmf M x \<noteq> 0"
   by transfer simp
 
+lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)"
+  by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
+
+lemma nn_integral_measure_pmf_support:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes f: "finite A" and nn: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> set_pmf M \<Longrightarrow> x \<notin> A \<Longrightarrow> f x = 0"
+  shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>A. f x * pmf M x)"
+proof -
+  have "(\<integral>\<^sup>+x. f x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M)"
+    using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator)
+  also have "\<dots> = (\<Sum>x\<in>A. f x * emeasure M {x})"
+    using assms by (intro nn_integral_indicator_finite) auto
+  finally show ?thesis
+    by (simp add: emeasure_measure_pmf_finite)
+qed
+
+lemma nn_integral_measure_pmf_finite:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes f: "finite (set_pmf M)" and nn: "\<And>x. x \<in> set_pmf M \<Longrightarrow> 0 \<le> f x"
+  shows "(\<integral>\<^sup>+x. f x \<partial>measure_pmf M) = (\<Sum>x\<in>set_pmf M. f x * pmf M x)"
+  using assms by (intro nn_integral_measure_pmf_support) auto
+lemma integrable_measure_pmf_finite:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  shows "finite (set_pmf M) \<Longrightarrow> integrable M f"
+  by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite)
+
+lemma integral_measure_pmf:
+  assumes [simp]: "finite A" and "\<And>a. a \<in> set_pmf M \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow> a \<in> A"
+  shows "(\<integral>x. f x \<partial>measure_pmf M) = (\<Sum>a\<in>A. f a * pmf M a)"
+proof -
+  have "(\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x * indicator A x \<partial>measure_pmf M)"
+    using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff)
+  also have "\<dots> = (\<Sum>a\<in>A. f a * pmf M a)"
+    by (subst integral_indicator_finite_real) (auto simp: measure_def emeasure_measure_pmf_finite)
+  finally show ?thesis .
+qed
+
+lemma integrable_pmf: "integrable (count_space X) (pmf M)"
+proof -
+  have " (\<integral>\<^sup>+ x. pmf M x \<partial>count_space X) = (\<integral>\<^sup>+ x. pmf M x \<partial>count_space (M \<inter> X))"
+    by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator)
+  then have "integrable (count_space X) (pmf M) = integrable (count_space (M \<inter> X)) (pmf M)"
+    by (simp add: integrable_iff_bounded pmf_nonneg)
+  then show ?thesis
+    by (simp add: pmf.rep_eq measure_pmf.integrable_measure countable_set_pmf disjoint_family_on_def)
+qed
+
+lemma integral_pmf: "(\<integral>x. pmf M x \<partial>count_space X) = measure M X"
+proof -
+  have "(\<integral>x. pmf M x \<partial>count_space X) = (\<integral>\<^sup>+x. pmf M x \<partial>count_space X)"
+    by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral)
+  also have "\<dots> = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space (X \<inter> M))"
+    by (auto intro!: nn_integral_cong_AE split: split_indicator
+             simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator
+                   AE_count_space set_pmf_iff)
+  also have "\<dots> = emeasure M (X \<inter> M)"
+    by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf)
+  also have "\<dots> = emeasure M X"
+    by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff)
+  finally show ?thesis
+    by (simp add: measure_pmf.emeasure_eq_measure)
+qed
+
+lemma integral_pmf_restrict:
+  "(f::'a \<Rightarrow> 'b::{banach, second_countable_topology}) \<in> borel_measurable (count_space UNIV) \<Longrightarrow>
+    (\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x \<partial>restrict_space M M)"
+  by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff)
+
 lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1"
 proof -
   have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)"
@@ -173,6 +272,9 @@
 lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g"
   by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) 
 
+lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\<lambda>x. f (g x)) M"
+  using map_pmf_compose[of f g] by (simp add: comp_def)
+
 lemma map_pmf_cong:
   assumes "p = q"
   shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g q"
@@ -206,6 +308,11 @@
   qed
 qed
 
+lemma set_map_pmf: "set_pmf (map_pmf f M) = f`set_pmf M"
+  using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff)
+
+subsection {* PMFs as function *}
+
 context
   fixes f :: "'a \<Rightarrow> real"
   assumes nonneg: "\<And>x. 0 \<le> f x"
@@ -237,6 +344,28 @@
   "rel_fun (eq_onp (\<lambda>f. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
   by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)
 
+lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)"
+proof (transfer, elim conjE)
+  fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0"
+  assume "prob_space M" then interpret prob_space M .
+  show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
+  proof (rule measure_eqI)
+    fix A :: "'a set"
+    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 
+      (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
+      by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
+    also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
+      by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space)
+    also have "\<dots> = emeasure M (\<Union>x\<in>(A \<inter> {x. measure M {x} \<noteq> 0}). {x})"
+      by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support)
+         (auto simp: disjoint_family_on_def)
+    also have "\<dots> = emeasure M A"
+      using ae by (intro emeasure_eq_AE) auto
+    finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))) A"
+      using emeasure_space_1 by (simp add: emeasure_density)
+  qed simp
+qed
+
 lemma td_pmf_embed_pmf:
   "type_definition pmf embed_pmf {f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1}"
   unfolding type_definition_def
@@ -270,21 +399,349 @@
   by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
      metis+
 
-end 
+end
+
+context
+begin
+
+interpretation pmf_as_function .
+
+lemma pmf_eqI: "(\<And>i. pmf M i = pmf N i) \<Longrightarrow> M = N"
+  by transfer auto
+
+lemma pmf_eq_iff: "M = N \<longleftrightarrow> (\<forall>i. pmf M i = pmf N i)"
+  by (auto intro: pmf_eqI)
+
+end
+
+context
+begin
+
+interpretation pmf_as_function .
+
+lift_definition bernoulli_pmf :: "real \<Rightarrow> bool pmf" is
+  "\<lambda>p b. ((\<lambda>p. if b then p else 1 - p) \<circ> min 1 \<circ> max 0) p"
+  by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool
+           split: split_max split_min)
+
+lemma pmf_bernoulli_True[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) True = p"
+  by transfer simp
+
+lemma pmf_bernoulli_False[simp]: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> pmf (bernoulli_pmf p) False = 1 - p"
+  by transfer simp
+
+lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
+  by (auto simp add: set_pmf_iff UNIV_bool)
+
+lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
+proof
+  note geometric_sums[of "1 / 2"]
+  note sums_mult[OF this, of "1 / 2"]
+  from sums_suminf_ereal[OF this]
+  show "(\<integral>\<^sup>+ x. ereal (1 / 2 ^ Suc x) \<partial>count_space UNIV) = 1"
+    by (simp add: nn_integral_count_space_nat field_simps)
+qed simp
+
+lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n"
+  by transfer rule
+
+lemma set_pmf_geometric: "set_pmf geometric_pmf = UNIV"
+  by (auto simp: set_pmf_iff)
+
+context
+  fixes M :: "'a multiset" assumes M_not_empty: "M \<noteq> {#}"
+begin
+
+lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M"
+proof
+  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"  
+    using M_not_empty
+    by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size
+                  setsum_divide_distrib[symmetric])
+       (auto simp: size_multiset_overloaded_eq intro!: setsum.cong)
+qed simp
+
+lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M"
+  by transfer rule
+
+lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M"
+  by (auto simp: set_pmf_iff)
+
+end
+
+context
+  fixes S :: "'a set" assumes S_not_empty: "S \<noteq> {}" and S_finite: "finite S"
+begin
+
+lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S"
+proof
+  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"  
+    using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto
+qed simp
+
+lemma pmf_of_set[simp]: "pmf pmf_of_set x = indicator S x / card S"
+  by transfer rule
+
+lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
+  using S_finite S_not_empty by (auto simp: set_pmf_iff)
+
+end
+
+end
+
+subsection {* Monad interpretation *}
+
+lemma measurable_measure_pmf[measurable]:
+  "(\<lambda>x. measure_pmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
+  by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales
+
+lemma bind_pmf_cong:
+  assumes "\<And>x. A x \<in> space (subprob_algebra N)" "\<And>x. B x \<in> space (subprob_algebra N)"
+  assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i"
+  shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
+proof (rule measure_eqI)
+  show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
+    using assms by (subst (1 2) sets_bind) auto
+next
+  fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
+  then have X: "X \<in> sets N"
+    using assms by (subst (asm) sets_bind) auto
+  show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
+    using assms
+    by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
+       (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
+qed
+
+context
+begin
+
+interpretation pmf_as_measure .
+
+lift_definition join_pmf :: "'a pmf pmf \<Rightarrow> 'a pmf" is "\<lambda>M. measure_pmf M \<guillemotright>= measure_pmf"
+proof (intro conjI)
+  fix M :: "'a pmf pmf"
+
+  have *: "measure_pmf \<in> measurable (measure_pmf M) (subprob_algebra (count_space UNIV))"
+    using measurable_measure_pmf[of "\<lambda>x. x"] by simp
+  
+  interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf"
+    apply (rule measure_pmf.prob_space_bind[OF _ *])
+    apply (auto intro!: AE_I2)
+    apply unfold_locales
+    done
+  show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)"
+    by intro_locales
+  show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV"
+    by (subst sets_bind[OF *]) auto
+  have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
+    by (auto simp add: AE_bind[OF _ *] AE_measure_pmf_iff emeasure_bind[OF _ *]
+        nn_integral_0_iff_AE measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
+  then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
+    unfolding bind.emeasure_eq_measure by simp
+qed
+
+lemma pmf_join: "pmf (join_pmf N) i = (\<integral>M. pmf M i \<partial>measure_pmf N)"
+proof (transfer fixing: N i)
+  have N: "subprob_space (measure_pmf N)"
+    by (rule prob_space_imp_subprob_space) intro_locales
+  show "measure (measure_pmf N \<guillemotright>= measure_pmf) {i} = integral\<^sup>L (measure_pmf N) (\<lambda>M. measure M {i})"
+    using measurable_measure_pmf[of "\<lambda>x. x"]
+    by (intro subprob_space.measure_bind[where N="count_space UNIV", OF N]) auto
+qed (auto simp: Transfer.Rel_def rel_fun_def cr_pmf_def)
+
+lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)"
+  by (auto intro!: prob_space_return simp: AE_return measure_return)
+
+lemma join_return_pmf: "join_pmf (return_pmf M) = M"
+  by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq)
+
+lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
+  by transfer (simp add: distr_return)
+
+lemma set_pmf_return: "set_pmf (return_pmf x) = {x}"
+  by transfer (auto simp add: measure_return split: split_indicator)
+
+lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
+  by transfer (simp add: measure_return)
+
+end
+
+definition "bind_pmf M f = join_pmf (map_pmf f M)"
+
+lemma (in pmf_as_measure) bind_transfer[transfer_rule]:
+  "rel_fun pmf_as_measure.cr_pmf (rel_fun (rel_fun op = pmf_as_measure.cr_pmf) pmf_as_measure.cr_pmf) op \<guillemotright>= bind_pmf"
+proof (auto simp: pmf_as_measure.cr_pmf_def rel_fun_def bind_pmf_def join_pmf.rep_eq map_pmf.rep_eq)
+  fix M f and g :: "'a \<Rightarrow> 'b pmf" assume "\<forall>x. f x = measure_pmf (g x)"
+  then have f: "f = (\<lambda>x. measure_pmf (g x))"
+    by auto
+  show "measure_pmf M \<guillemotright>= f = distr (measure_pmf M) (count_space UNIV) g \<guillemotright>= measure_pmf"
+    unfolding f by (subst bind_distr[OF _ measurable_measure_pmf]) auto
+qed
+
+lemma pmf_bind: "pmf (bind_pmf N f) i = (\<integral>x. pmf (f x) i \<partial>measure_pmf N)"
+  by (auto intro!: integral_distr simp: bind_pmf_def pmf_join map_pmf.rep_eq)
+
+lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
+  unfolding bind_pmf_def map_return_pmf join_return_pmf ..
+
+lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
+  unfolding pmf_eq_iff pmf_bind
+proof
+  fix i
+  interpret B: prob_space "restrict_space B B"
+    by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE)
+       (auto simp: AE_measure_pmf_iff)
+  interpret A: prob_space "restrict_space A A"
+    by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE)
+       (auto simp: AE_measure_pmf_iff)
+
+  interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B"
+    by unfold_locales
+
+  have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
+    by (rule integral_cong) (auto intro!: integral_pmf_restrict)
+  also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
+    apply (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral)
+    apply (auto simp: measurable_split_conv)
+    apply (subst measurable_cong_sets)
+    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
+    apply (simp add: restrict_count_space)
+    apply (rule measurable_compose_countable'[OF _ measurable_snd])
+    apply (rule measurable_compose[OF measurable_fst])
+    apply (auto intro: countable_set_pmf)
+    done
+  also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>restrict_space B B)"
+    apply (rule AB.Fubini_integral[symmetric])
+    apply (auto intro!: AB.integrable_const_bound[where B=1] simp: pmf_nonneg pmf_le_1)
+    apply (auto simp: measurable_split_conv)
+    apply (subst measurable_cong_sets)
+    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
+    apply (simp add: restrict_count_space)
+    apply (rule measurable_compose_countable'[OF _ measurable_snd])
+    apply (rule measurable_compose[OF measurable_fst])
+    apply (auto intro: countable_set_pmf)
+    done
+  also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>B)"
+    apply (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral)
+    apply (auto simp: measurable_split_conv)
+    apply (subst measurable_cong_sets)
+    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
+    apply (simp add: restrict_count_space)
+    apply (rule measurable_compose_countable'[OF _ measurable_snd])
+    apply (rule measurable_compose[OF measurable_fst])
+    apply (auto intro: countable_set_pmf)
+    done
+  also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
+    by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
+  finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
+qed
+
+
+context
+begin
+
+interpretation pmf_as_measure .
+
+lemma bind_return_pmf': "bind_pmf N return_pmf = N"
+proof (transfer, clarify)
+  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
+    by (subst return_sets_cong[where N=N]) (simp_all add: bind_return')
+qed
+
+lemma bind_return_pmf'': "bind_pmf N (\<lambda>x. return_pmf (f x)) = map_pmf f N"
+proof (transfer, clarify)
+  fix N :: "'b measure" and f :: "'b \<Rightarrow> 'a" assume "prob_space N" "sets N = UNIV"
+  then show "N \<guillemotright>= (\<lambda>x. return (count_space UNIV) (f x)) = distr N (count_space UNIV) f"
+    by (subst bind_return_distr[symmetric])
+       (auto simp: prob_space.not_empty measurable_def comp_def)
+qed
+
+lemma bind_assoc_pmf: "bind_pmf (bind_pmf A B) C = bind_pmf A (\<lambda>x. bind_pmf (B x) C)"
+  by transfer
+     (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"]
+           simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space)
+
+lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
+  by transfer simp
+
+end
+
+definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
+
+lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
+  unfolding pair_pmf_def pmf_bind pmf_return
+  apply (subst integral_measure_pmf[where A="{b}"])
+  apply (auto simp: indicator_eq_0_iff)
+  apply (subst integral_measure_pmf[where A="{a}"])
+  apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
+  done
+
+lemma bind_pair_pmf:
+  assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
+  shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
+    (is "?L = ?R")
+proof (rule measure_eqI)
+  have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
+    using M[THEN measurable_space] by (simp_all add: space_pair_measure)
+
+  have sets_eq_N: "sets ?L = N"
+    by (simp add: sets_bind[OF M'])
+  show "sets ?L = sets ?R"
+    unfolding sets_eq_N
+    apply (subst sets_bind[where N=N])
+    apply (rule measurable_bind)
+    apply (rule measurable_compose[OF _ measurable_measure_pmf])
+    apply measurable
+    apply (auto intro!: sets_pair_measure_cong sets_measure_pmf_count_space)
+    done
+  fix X assume "X \<in> sets ?L"
+  then have X[measurable]: "X \<in> sets N"
+    unfolding sets_eq_N .
+  then show "emeasure ?L X = emeasure ?R X"
+    apply (simp add: emeasure_bind[OF _ M' X])
+    unfolding pair_pmf_def measure_pmf_bind[of A]
+    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
+    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
+    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
+    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
+    apply measurable
+    unfolding measure_pmf_bind
+    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
+    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
+    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
+    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
+    apply measurable
+    apply (simp add: nn_integral_measure_pmf_finite set_pmf_return emeasure_nonneg pmf_return one_ereal_def[symmetric])
+    apply (subst emeasure_bind[OF _ _ X])
+    apply simp
+    apply (rule measurable_bind[where N="count_space UNIV"])
+    apply (rule measurable_compose[OF _ measurable_measure_pmf])
+    apply measurable
+    apply (rule sets_pair_measure_cong sets_measure_pmf_count_space refl)+
+    apply (subst measurable_cong_sets[OF sets_pair_measure_cong[OF sets_measure_pmf_count_space refl] refl])
+    apply simp
+    apply (subst emeasure_bind[OF _ _ X])
+    apply simp
+    apply (rule measurable_compose[OF _ M])
+    apply (auto simp: space_pair_measure)
+    done
+qed
+
+lemma set_pmf_bind: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
+  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
+  apply (subst integral_nonneg_eq_0_iff_AE)
+  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
+              intro!: measure_pmf.integrable_const_bound[where B=1])
+  done
+
+lemma set_pmf_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
+  unfolding pair_pmf_def set_pmf_bind set_pmf_return by auto
 
 (*
 
 definition
   "rel_pmf P d1 d2 \<longleftrightarrow> (\<exists>p3. (\<forall>(x, y) \<in> set_pmf p3. P x y) \<and> map_pmf fst p3 = d1 \<and> map_pmf snd p3 = d2)"
 
-lift_definition pmf_join :: "real \<Rightarrow> 'a pmf \<Rightarrow> 'a pmf \<Rightarrow> 'a pmf" is
-  "\<lambda>p M1 M2. density (count_space UNIV) (\<lambda>x. p * measure M1 {x} + (1 - p) * measure M2 {x})"
-sorry
-
-lift_definition pmf_single :: "'a \<Rightarrow> 'a pmf" is
-  "\<lambda>x. uniform_measure (count_space UNIV) {x}"
-sorry
-
 bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: pmf_rel
 proof -
   show "map_pmf id = id" by (rule map_pmf_id)

--- a/src/HOL/Probability/Probability_Measure.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -60,6 +60,11 @@
     using assms emeasure_space_1 by (simp add: emeasure_compl)
 qed (insert assms, auto)
 
+lemma prob_space_restrict_space:
+  "S \<in> sets M \<Longrightarrow> emeasure M S = 1 \<Longrightarrow> prob_space (restrict_space M S)"
+  by (intro prob_spaceI)
+     (simp add: emeasure_restrict_space space_restrict_space)
+
 lemma (in prob_space) prob_compl:
   assumes A: "A \<in> events"
   shows "prob (space M - A) = 1 - prob A"
@@ -107,6 +112,9 @@
 lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
   by (cases P) (auto simp: AE_False)
 
+lemma (in prob_space) ae_filter_bot: "ae_filter M \<noteq> bot"
+  by (simp add: trivial_limit_def)
+
 lemma (in prob_space) AE_contr:
   assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
   shows False
@@ -115,6 +123,10 @@
   then show False by auto
 qed
 
+lemma (in prob_space) emeasure_eq_1_AE:
+  "S \<in> sets M \<Longrightarrow> AE x in M. x \<in> S \<Longrightarrow> emeasure M S = 1"
+  by (subst emeasure_eq_AE[where B="space M"]) (auto simp: emeasure_space_1)
+
 lemma (in prob_space) integral_ge_const:
   fixes c :: real
   shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)"
@@ -357,6 +369,31 @@
     by (intro finite_measure_UNION) auto
 qed
 
+lemma (in prob_space) prob_setsum:
+  assumes [simp, intro]: "finite I"
+  assumes P: "\<And>n. n \<in> I \<Longrightarrow> {x\<in>space M. P n x} \<in> events"
+  assumes Q: "{x\<in>space M. Q x} \<in> events"
+  assumes ae: "AE x in M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n\<in>I. P n x))"
+  shows "\<P>(x in M. Q x) = (\<Sum>n\<in>I. \<P>(x in M. P n x))"
+proof -
+  from ae[THEN AE_E_prob] guess S . note S = this
+  then have disj: "disjoint_family_on (\<lambda>n. {x\<in>space M. P n x} \<inter> S) I"
+    by (auto simp: disjoint_family_on_def)
+  from S have ae_S:
+    "AE x in M. x \<in> {x\<in>space M. Q x} \<longleftrightarrow> x \<in> (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)"
+    "\<And>n. n \<in> I \<Longrightarrow> AE x in M. x \<in> {x\<in>space M. P n x} \<longleftrightarrow> x \<in> {x\<in>space M. P n x} \<inter> S"
+    using ae by (auto dest!: AE_prob_1)
+  from ae_S have *:
+    "\<P>(x in M. Q x) = prob (\<Union>n\<in>I. {x\<in>space M. P n x} \<inter> S)"
+    using P Q S by (intro finite_measure_eq_AE) (auto intro!: sets.Int)
+  from ae_S have **:
+    "\<And>n. n \<in> I \<Longrightarrow> \<P>(x in M. P n x) = prob ({x\<in>space M. P n x} \<inter> S)"
+    using P Q S by (intro finite_measure_eq_AE) auto
+  show ?thesis
+    using S P disj
+    by (auto simp add: * ** simp del: UN_simps intro!: finite_measure_finite_Union)
+qed
+
 lemma (in prob_space) prob_EX_countable:
   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" and I: "countable I" 
   assumes disj: "AE x in M. \<forall>i\<in>I. \<forall>j\<in>I. P i x \<longrightarrow> P j x \<longrightarrow> i = j"
@@ -1105,4 +1142,21 @@
 lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
   by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
 
+lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
+  assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
+  shows "\<P>(x in uniform_measure M {x\<in>space M. Q x}. P x) = \<P>(x in M. P x \<bar> Q x)"
+proof cases
+  assume Q: "measure M {x\<in>space M. Q x} = 0"
+  then have "AE x in M. \<not> Q x"
+    by (simp add: prob_eq_0)
+  then have "AE x in M. indicator {x\<in>space M. Q x} x / ereal 0 = 0"
+    by (auto split: split_indicator)
+  from density_cong[OF _ _ this] show ?thesis
+    by (simp add: uniform_measure_def emeasure_eq_measure cond_prob_def Q measure_density_const)
+qed (auto simp add: emeasure_eq_measure cond_prob_def intro!: arg_cong[where f=prob])
+
+lemma prob_space_point_measure:
+  "finite S \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> 0 \<le> p s) \<Longrightarrow> (\<Sum>s\<in>S. p s) = 1 \<Longrightarrow> prob_space (point_measure S p)"
+  by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite)
+
 end

--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1732,6 +1732,12 @@
 lemma measure_of_subset: "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
   by (auto intro!: sigma_sets_subseteq)
 
+lemma emeasure_sigma: "emeasure (sigma \<Omega> A) = (\<lambda>x. 0)"
+  unfolding measure_of_def emeasure_def
+  by (subst Abs_measure_inverse)
+     (auto simp: measure_space_def positive_def countably_additive_def
+           intro!: sigma_algebra_sigma_sets sigma_algebra_trivial)
+
 lemma sigma_sets_mono'':
   assumes "A \<in> sigma_sets C D"
   assumes "B \<subseteq> D"
@@ -1839,10 +1845,6 @@
     by (simp add: measure_measure)
 qed
 
-lemma emeasure_sigma: "A \<subseteq> Pow \<Omega> \<Longrightarrow> emeasure (sigma \<Omega> A) = (\<lambda>_. 0)"
-  using measure_space_0[of A \<Omega>]
-  by (simp add: measure_of_def emeasure_def Abs_measure_inverse)
-
 lemma sigma_eqI:
   assumes [simp]: "M \<subseteq> Pow \<Omega>" "N \<subseteq> Pow \<Omega>" "sigma_sets \<Omega> M = sigma_sets \<Omega> N"
   shows "sigma \<Omega> M = sigma \<Omega> N"
@@ -2115,22 +2117,30 @@
     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)"
+lemma measurable_compose_countable':
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f i x) \<in> measurable M N"
+  and g: "g \<in> measurable M (count_space I)" and I: "countable I"
   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
+    using measurable_space[OF f] 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!: sets.countable_UN measurable_sets)
+  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i\<in>I. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
+    using measurable_space[OF g] by auto
+  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF _ A] g[THEN measurable_sets]
+    apply (auto intro!: sets.countable_UN' measurable_sets I)
+    apply (rule sets.Int)
+    apply auto
+    done
   finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 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"
+  by (rule measurable_compose_countable'[OF assms]) auto
 lemma measurable_count_space_const:
   "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
   by (simp add: measurable_const)
@@ -2241,6 +2251,10 @@
 lemma in_Sup_sigma: "m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup_sigma M)"
   unfolding sets_Sup_sigma by auto
 
+lemma SUP_sigma_cong: 
+  assumes *: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (\<Squnion>\<^sub>\<sigma> i\<in>I. M i) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. N i)"
+  using * sets_eq_imp_space_eq[OF *] by (simp add: Sup_sigma_def)
+
 lemma sets_Sup_in_sets: 
   assumes "M \<noteq> {}"
   assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N"
@@ -2290,6 +2304,9 @@
   using sigma_sets_vimage_commute[of f X "space M" "sets M"]
   unfolding sets_vimage_algebra sets.sigma_sets_eq by simp
 
+lemma vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)"
+  by (simp add: sets_vimage_algebra)
+
 lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)"
   by (auto simp: vimage_algebra_def)
 
@@ -2318,6 +2335,34 @@
   finally show "g -` A \<inter> space N \<in> sets N" .
 qed (insert g, auto)
 
+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")
+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
+  with * show "sets ?VV = sets ?V"
+    by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps)
+qed (simp add: vimage_algebra_def emeasure_sigma)
+
+lemma sets_vimage_Sup_eq:
+  assumes *: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f \<in> X \<rightarrow> space m"
+  shows "sets (vimage_algebra X f (Sup_sigma M)) = sets (\<Squnion>\<^sub>\<sigma> m \<in> M. vimage_algebra X f m)"
+  (is "?IS = ?SI")
+proof
+  show "?IS \<subseteq> ?SI"
+    by (intro sets_image_in_sets measurable_Sup_sigma2 measurable_Sup_sigma1)
+       (auto simp: space_Sup_sigma measurable_vimage_algebra1 *)
+  { fix m assume "m \<in> M"
+    moreover then have "f \<in> X \<rightarrow> space (Sup_sigma M)" "f \<in> X \<rightarrow> space m"
+      using * by (auto simp: space_Sup_sigma)
+    ultimately have "f \<in> measurable (vimage_algebra X f (Sup_sigma M)) m"
+      by (auto simp add: measurable_def sets_vimage_algebra2 intro: in_Sup_sigma) }
+  then show "?SI \<subseteq> ?IS"
+    by (auto intro!: sets_image_in_sets sets_Sup_in_sets del: subsetI simp: *)
+qed
+
 subsubsection {* Restricted Space Sigma Algebra *}
 
 definition restrict_space where
@@ -2358,6 +2403,27 @@
     by auto
 qed auto
 
+lemma sets_restrict_space_cong: "sets M = sets N \<Longrightarrow> sets (restrict_space M \<Omega>) = sets (restrict_space N \<Omega>)"
+  by (simp add: sets_restrict_space)
+
+lemma restrict_space_eq_vimage_algebra:
+  "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = sets (vimage_algebra \<Omega> (\<lambda>x. x) M)"
+  unfolding restrict_space_def
+  apply (subst sets_measure_of)
+  apply (auto simp add: image_subset_iff dest: sets.sets_into_space) []
+  apply (auto simp add: sets_vimage_algebra intro!: arg_cong2[where f=sigma_sets])
+  done
+
+lemma sets_Collect_restrict_space_iff: 
+  assumes "S \<in> sets M"
+  shows "{x\<in>space (restrict_space M S). P x} \<in> sets (restrict_space M S) \<longleftrightarrow> {x\<in>space M. x \<in> S \<and> P x} \<in> sets M"
+proof -
+  have "{x\<in>S. P x} = {x\<in>space M. x \<in> S \<and> P x}"
+    using sets.sets_into_space[OF assms] by auto
+  then show ?thesis
+    by (subst sets_restrict_space_iff) (auto simp add: space_restrict_space assms)
+qed
+
 lemma measurable_restrict_space1:
   assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" and f: "f \<in> measurable M N"
   shows "f \<in> measurable (restrict_space M \<Omega>) N"

--- a/src/HOL/Probability/Stream_Space.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Stream_Space.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -5,6 +5,7 @@
 imports
   Infinite_Product_Measure
   "~~/src/HOL/Library/Stream"
+  "~~/src/HOL/Library/Linear_Temporal_Logic_on_Streams"
 begin
 
 lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
@@ -20,6 +21,9 @@
   unfolding to_stream_def
   by (subst siterate.ctr) (simp add: smap_siterate[symmetric] stream.map_comp comp_def)
 
+lemma to_stream_in_streams: "to_stream X \<in> streams S \<longleftrightarrow> (\<forall>n. X n \<in> S)"
+  by (simp add: to_stream_def streams_iff_snth)
+
 definition stream_space :: "'a measure \<Rightarrow> 'a stream measure" where
   "stream_space M =
     distr (\<Pi>\<^sub>M i\<in>UNIV. M) (vimage_algebra (streams (space M)) snth (\<Pi>\<^sub>M i\<in>UNIV. M)) to_stream"
@@ -98,6 +102,61 @@
   "stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))"
   by (induct i) auto
 
+lemma measurable_shift[measurable]: 
+  assumes f: "f \<in> measurable N (stream_space M)"
+  assumes [measurable]: "g \<in> measurable N (stream_space M)"
+  shows "(\<lambda>x. stake n (f x) @- g x) \<in> measurable N (stream_space M)"
+  using f by (induction n arbitrary: f) simp_all
+
+lemma measurable_ev_at[measurable]:
+  assumes [measurable]: "Measurable.pred (stream_space M) P"
+  shows "Measurable.pred (stream_space M) (ev_at P n)"
+  by (induction n) auto
+
+lemma measurable_alw[measurable]:
+  "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (alw P)"
+  unfolding alw_def
+  by (coinduction rule: measurable_gfp_coinduct) (auto simp: Order_Continuity.down_continuous_def)
+
+lemma measurable_ev[measurable]:
+  "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (ev P)"
+  unfolding ev_def
+  by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
+
+lemma measurable_until:
+  assumes [measurable]: "Measurable.pred (stream_space M) \<phi>" "Measurable.pred (stream_space M) \<psi>"
+  shows "Measurable.pred (stream_space M) (\<phi> until \<psi>)"
+  unfolding UNTIL_def
+  by (coinduction rule: measurable_gfp_coinduct) (simp_all add: down_continuous_def fun_eq_iff)
+
+lemma measurable_holds [measurable]: "Measurable.pred M P \<Longrightarrow> Measurable.pred (stream_space M) (holds P)"
+  unfolding holds.simps[abs_def]
+  by (rule measurable_compose[OF measurable_shd]) simp
+
+lemma measurable_hld[measurable]: assumes [measurable]: "t \<in> sets M" shows "Measurable.pred (stream_space M) (HLD t)"
+  unfolding HLD_def by measurable
+
+lemma measurable_nxt[measurable (raw)]:
+  "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (nxt P)"
+  unfolding nxt.simps[abs_def] by simp
+
+lemma measurable_suntil[measurable]:
+  assumes [measurable]: "Measurable.pred (stream_space M) Q" "Measurable.pred (stream_space M) P"
+  shows "Measurable.pred (stream_space M) (Q suntil P)"
+  unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
+
+lemma measurable_szip:
+  "(\<lambda>(\<omega>1, \<omega>2). szip \<omega>1 \<omega>2) \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (stream_space (M \<Otimes>\<^sub>M N))"
+proof (rule measurable_stream_space2)
+  fix n
+  have "(\<lambda>x. (case x of (\<omega>1, \<omega>2) \<Rightarrow> szip \<omega>1 \<omega>2) !! n) = (\<lambda>(\<omega>1, \<omega>2). (\<omega>1 !! n, \<omega>2 !! n))"
+    by auto
+  also have "\<dots> \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (M \<Otimes>\<^sub>M N)"
+    by measurable
+  finally show "(\<lambda>x. (case x of (\<omega>1, \<omega>2) \<Rightarrow> szip \<omega>1 \<omega>2) !! n) \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (M \<Otimes>\<^sub>M N)"
+    .
+qed
+
 lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
 proof -
   interpret product_prob_space "\<lambda>_. M" UNIV by default
@@ -189,4 +248,185 @@
     unfolding stream_all_def by (simp add: AE_all_countable)
 qed
 
+lemma streams_sets:
+  assumes X[measurable]: "X \<in> sets M" shows "streams X \<in> sets (stream_space M)"
+proof -
+  have "streams X = {x\<in>space (stream_space M). x \<in> streams X}"
+    using streams_mono[OF _ sets.sets_into_space[OF X]] by (auto simp: space_stream_space)
+  also have "\<dots> = {x\<in>space (stream_space M). gfp (\<lambda>p x. shd x \<in> X \<and> p (stl x)) x}"
+    apply (simp add: set_eq_iff streams_def streamsp_def)
+    apply (intro allI conj_cong refl arg_cong2[where f=gfp] ext)
+    apply (case_tac xa)
+    apply auto
+    done
+  also have "\<dots> \<in> sets (stream_space M)"
+    apply (intro predE)
+    apply (coinduction rule: measurable_gfp_coinduct)
+    apply (auto simp: down_continuous_def)
+    done
+  finally show ?thesis .
+qed
+
+lemma sets_stream_space_in_sets:
+  assumes space: "space N = streams (space M)"
+  assumes sets: "\<And>i. (\<lambda>x. x !! i) \<in> measurable N M"
+  shows "sets (stream_space M) \<subseteq> sets N"
+  unfolding stream_space_def sets_distr
+  by (auto intro!: sets_image_in_sets measurable_Sup_sigma2 measurable_vimage_algebra2 del: subsetI equalityI 
+           simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
+
+lemma sets_stream_space_eq: "sets (stream_space M) =
+    sets (\<Squnion>\<^sub>\<sigma> i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
+  by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
+                   measurable_Sup_sigma1  snth_in measurable_vimage_algebra1 del: subsetI
+           simp: space_Sup_sigma space_stream_space)
+
+lemma sets_restrict_stream_space:
+  assumes S[measurable]: "S \<in> sets M"
+  shows "sets (restrict_space (stream_space M) (streams S)) = sets (stream_space (restrict_space M S))"
+  using  S[THEN sets.sets_into_space]
+  apply (subst restrict_space_eq_vimage_algebra)
+  apply (simp add: space_stream_space streams_mono2)
+  apply (subst vimage_algebra_cong[OF sets_stream_space_eq])
+  apply (subst sets_stream_space_eq)
+  apply (subst sets_vimage_Sup_eq)
+  apply simp
+  apply (auto intro: streams_mono) []
+  apply (simp add: image_image space_restrict_space)
+  apply (intro SUP_sigma_cong)
+  apply (simp add: vimage_algebra_cong[OF restrict_space_eq_vimage_algebra])
+  apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
+  apply (auto simp: streams_mono snth_in)
+  done
+
+
+primrec sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" where
+  "sstart S [] = streams S"
+| [simp del]: "sstart S (x # xs) = op ## x ` sstart S xs"
+
+lemma in_sstart[simp]: "s \<in> sstart S (x # xs) \<longleftrightarrow> shd s = x \<and> stl s \<in> sstart S xs"
+  by (cases s) (auto simp: sstart.simps(2))
+
+lemma sstart_in_streams: "xs \<in> lists S \<Longrightarrow> sstart S xs \<subseteq> streams S"
+  by (induction xs) (auto simp: sstart.simps(2))
+
+lemma sstart_eq: "x \<in> streams S \<Longrightarrow> x \<in> sstart S xs = (\<forall>i<length xs. x !! i = xs ! i)"
+  by (induction xs arbitrary: x) (auto simp: nth_Cons streams_stl split: nat.splits)
+
+lemma sstart_sets: "sstart S xs \<in> sets (stream_space (count_space UNIV))"
+proof (induction xs)
+  case (Cons x xs)
+  note Cons[measurable]
+  have "sstart S (x # xs) =
+    {s\<in>space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}"
+    by (simp add: set_eq_iff space_stream_space)
+  also have "\<dots> \<in> sets (stream_space (count_space UNIV))"
+    by measurable
+  finally show ?case .
+qed (simp add: streams_sets)
+
+lemma sets_stream_space_sstart:
+  assumes S[simp]: "countable S"
+  shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
+proof
+  have [simp]: "sstart S ` lists S \<subseteq> Pow (streams S)"
+    by (simp add: image_subset_iff sstart_in_streams)
+
+  let ?S = "sigma (streams S) (sstart S ` lists S \<union> {{}})"
+  { fix i a assume "a \<in> S"
+    { fix x have "(x !! i = a \<and> x \<in> streams S) \<longleftrightarrow> (\<exists>xs\<in>lists S. length xs = i \<and> x \<in> sstart S (xs @ [a]))"
+      proof (induction i arbitrary: x)
+        case (Suc i) from this[of "stl x"] show ?case
+          by (simp add: length_Suc_conv Bex_def ex_simps[symmetric] del: ex_simps)
+             (metis stream.collapse streams_Stream)
+      qed (insert `a \<in> S`, auto intro: streams_stl in_streams) }
+    then have "(\<lambda>x. x !! i) -` {a} \<inter> streams S = (\<Union>xs\<in>{xs\<in>lists S. length xs = i}. sstart S (xs @ [a]))"
+      by (auto simp add: set_eq_iff)
+    also have "\<dots> \<in> sets ?S"
+      using `a\<in>S` by (intro sets.countable_UN') (auto intro!: sigma_sets.Basic image_eqI)
+    finally have " (\<lambda>x. x !! i) -` {a} \<inter> streams S \<in> sets ?S" . }
+  then show "sets (stream_space (count_space S)) \<subseteq> sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
+    by (intro sets_stream_space_in_sets) (auto simp: measurable_count_space_eq_countable snth_in)
+
+  have "sigma_sets (space (stream_space (count_space S))) (sstart S`lists S \<union> {{}}) \<subseteq> sets (stream_space (count_space S))"
+  proof (safe intro!: sets.sigma_sets_subset)
+    fix xs assume "\<forall>x\<in>set xs. x \<in> S"
+    then have "sstart S xs = {x\<in>space (stream_space (count_space S)). \<forall>i<length xs. x !! i = xs ! i}"
+      by (induction xs)
+         (auto simp: space_stream_space nth_Cons split: nat.split intro: in_streams streams_stl)
+    also have "\<dots> \<in> sets (stream_space (count_space S))"
+      by measurable
+    finally show "sstart S xs \<in> sets (stream_space (count_space S))" .
+  qed
+  then show "sets (sigma (streams S) (sstart S`lists S \<union> {{}})) \<subseteq> sets (stream_space (count_space S))"
+    by (simp add: space_stream_space)
+qed
+
+lemma Int_stable_sstart: "Int_stable (sstart S`lists S \<union> {{}})"
+proof -
+  { fix xs ys assume "xs \<in> lists S" "ys \<in> lists S"
+    then have "sstart S xs \<inter> sstart S ys \<in> sstart S ` lists S \<union> {{}}"
+    proof (induction xs ys rule: list_induct2')
+      case (4 x xs y ys)
+      show ?case
+      proof cases
+        assume "x = y"
+        then have "sstart S (x # xs) \<inter> sstart S (y # ys) = op ## x ` (sstart S xs \<inter> sstart S ys)"
+          by (auto simp: image_iff intro!: stream.collapse[symmetric])
+        also have "\<dots> \<in> sstart S ` lists S \<union> {{}}"
+          using 4 by (auto simp: sstart.simps(2)[symmetric] del: in_listsD)
+        finally show ?case .
+      qed auto
+    qed (simp_all add: sstart_in_streams inf.absorb1 inf.absorb2 image_eqI[where x="[]"]) }
+  then show ?thesis
+    by (auto simp: Int_stable_def)
+qed
+
+lemma stream_space_eq_sstart:
+  assumes S[simp]: "countable S"
+  assumes P: "prob_space M" "prob_space N"
+  assumes ae: "AE x in M. x \<in> streams S" "AE x in N. x \<in> streams S"
+  assumes sets_M: "sets M = sets (stream_space (count_space UNIV))"
+  assumes sets_N: "sets N = sets (stream_space (count_space UNIV))"
+  assumes *: "\<And>xs. xs \<noteq> [] \<Longrightarrow> xs \<in> lists S \<Longrightarrow> emeasure M (sstart S xs) = emeasure N (sstart S xs)"
+  shows "M = N"
+proof (rule measure_eqI_restrict_generator[OF Int_stable_sstart])
+  have [simp]: "sstart S ` lists S \<subseteq> Pow (streams S)"
+    by (simp add: image_subset_iff sstart_in_streams)
+
+  interpret M: prob_space M by fact
+
+  show "sstart S ` lists S \<union> {{}} \<subseteq> Pow (streams S)"
+    by (auto dest: sstart_in_streams del: in_listsD)
+
+  { fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))"
+    have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
+      apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra
+        vimage_algebra_cong[OF M])
+      apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra[symmetric])
+      apply (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart)
+      done }
+  from this[OF sets_M] this[OF sets_N]
+  show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
+       "sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
+    by auto
+  show "{streams S} \<subseteq> sstart S ` lists S \<union> {{}}"
+    "\<Union>{streams S} = streams S" "\<And>s. s \<in> {streams S} \<Longrightarrow> emeasure M s \<noteq> \<infinity>"
+    using M.emeasure_space_1 space_stream_space[of "count_space S"] sets_eq_imp_space_eq[OF sets_M]
+    by (auto simp add: image_eqI[where x="[]"])
+  show "sets M = sets N"
+    by (simp add: sets_M sets_N)
+next
+  fix X assume "X \<in> sstart S ` lists S \<union> {{}}"
+  then obtain xs where "X = {} \<or> (xs \<in> lists S \<and> X = sstart S xs)"
+    by auto
+  moreover have "emeasure M (streams S) = 1"
+    using ae by (intro prob_space.emeasure_eq_1_AE[OF P(1)]) (auto simp: sets_M streams_sets)
+  moreover have "emeasure N (streams S) = 1"
+    using ae by (intro prob_space.emeasure_eq_1_AE[OF P(2)]) (auto simp: sets_N streams_sets)
+  ultimately show "emeasure M X = emeasure N X"
+    using P[THEN prob_space.emeasure_space_1]
+    by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
+qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
+
 end

--- a/src/HOL/Product_Type.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Product_Type.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1108,6 +1108,9 @@
 lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   by blast
 
+lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
+  by auto
+
 lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
   by blast
 

--- a/src/HOL/Rat.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Rat.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -680,6 +680,12 @@
 apply (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps)
 done
 
+lemma of_rat_setsum: "of_rat (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A. of_rat (f a))"
+  by (induct rule: infinite_finite_induct) (auto simp: of_rat_add)
+
+lemma of_rat_setprod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))"
+  by (induct rule: infinite_finite_induct) (auto simp: of_rat_mult)
+
 lemma nonzero_of_rat_inverse:
   "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)"
 apply (rule inverse_unique [symmetric])

--- a/src/HOL/Real.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Real.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1020,13 +1020,17 @@
 end
 
 declare [[coercion_enabled]]
-declare [[coercion "real::nat\<Rightarrow>real"]]
-declare [[coercion "real::int\<Rightarrow>real"]]
-declare [[coercion "int"]]
+
+declare [[coercion "of_nat :: nat \<Rightarrow> int"]]
+declare [[coercion "real   :: nat \<Rightarrow> real"]]
+declare [[coercion "real   :: int \<Rightarrow> real"]]
+
+(* We do not add rat to the coerced types, this has often unpleasant side effects when writing
+inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *)
 
 declare [[coercion_map map]]
-declare [[coercion_map "% f g h x. g (h (f x))"]]
-declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
+declare [[coercion_map "\<lambda>f g h x. g (h (f x))"]]
+declare [[coercion_map "\<lambda>f g (x,y). (f x, g y)"]]
 
 lemma real_eq_of_nat: "real = of_nat"
   unfolding real_of_nat_def ..

--- a/src/HOL/Rings.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Rings.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1021,6 +1021,12 @@
   using assms mult_strict_mono [of 1 m 1 n]
     by (simp add:  less_trans [OF zero_less_one]) 
 
+lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
+  using mult_left_mono[of c 1 a] by simp
+
+lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
+  using mult_mono[of a 1 b 1] by simp
+
 end
 
 class linordered_idom = comm_ring_1 +

--- a/src/HOL/Series.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Series.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -666,4 +666,14 @@
 lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   by (fold real_norm_def) (rule summable_norm)
 
+lemma summable_power_series:
+  fixes z :: real
+  assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
+  shows "summable (\<lambda>i. f i * z^i)"
+proof (rule summable_comparison_test[OF _ summable_geometric])
+  show "norm z < 1" using z by (auto simp: less_imp_le)
+  show "\<And>n. \<exists>N. \<forall>na\<ge>N. norm (f na * z ^ na) \<le> z ^ na"
+    using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
+qed
+
 end

--- a/src/HOL/Set.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Set.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -478,6 +478,8 @@
     (EX x:A. P x) = (EX x:B. Q x)"
   by (simp add: simp_implies_def Bex_def cong: conj_cong)
 
+lemma bex1_def: "(\<exists>!x\<in>X. P x) \<longleftrightarrow> (\<exists>x\<in>X. P x) \<and> (\<forall>x\<in>X. \<forall>y\<in>X. P x \<longrightarrow> P y \<longrightarrow> x = y)"
+  by auto
 
 subsection {* Basic operations *}
 

--- a/src/HOL/Set_Interval.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -666,16 +666,18 @@
 new elements get indices at the beginning. So it is used to transform
 @{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
 
+lemma zero_notin_Suc_image: "0 \<notin> Suc ` A"
+  by auto
+
 lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"
-proof safe
-  fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}"
-  then have "x \<noteq> Suc (x - 1)" by auto
-  with `x < Suc n` show "x = 0" by auto
-qed
+  by (auto simp: image_iff less_Suc_eq_0_disj)
 
 lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
 by (simp add: lessThan_def atMost_def less_Suc_eq_le)
 
+lemma Iic_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
+  unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] ..
+
 lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
 by blast