# HG changeset patch
# User Andreas Lochbihler
# Date 1429019815 -7200
# Node ID d76f9047121ce3fbb00b0c870d16f57a0e713ab5
# Parent  71c1b9b9e9377977e2b55c476114b81ddfb958c4# Parent  ef2123db900ca9689663511f2d17f337b1072b86
merged

diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -53,6 +53,20 @@
 lemma chain_empty: "chain ord {}"
 by(simp add: chain_def)
 
+lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
+by(auto simp add: chain_def)
+
+lemma chain_subset:
+  "\<lbrakk> chain ord A; B \<subseteq> A \<rbrakk>
+  \<Longrightarrow> chain ord B"
+by(rule chainI)(blast dest: chainD)
+
+lemma chain_imageI: 
+  assumes chain: "chain le_a Y"
+  and mono: "\<And>x y. \<lbrakk> x \<in> Y; y \<in> Y; le_a x y \<rbrakk> \<Longrightarrow> le_b (f x) (f y)"
+  shows "chain le_b (f ` Y)"
+by(blast intro: chainI dest: chainD[OF chain] mono)
+
 subsection {* Chain-complete partial orders *}
 
 text {*
@@ -65,6 +79,12 @@
   assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
 begin
 
+lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
+by(rule chainI) simp
+
+lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
+by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+
 subsection {* Transfinite iteration of a function *}
 
 inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -247,6 +247,13 @@
   shows "countable ((X ^^ i) `` Y)"
   using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
 
+lemma countable_funpow:
+  fixes f :: "'a set \<Rightarrow> 'a set"
+  assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
+  and "countable A"
+  shows "countable ((f ^^ n) A)"
+by(induction n)(simp_all add: assms)
+
 lemma countable_rtrancl:
   "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
   unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
@@ -276,6 +283,9 @@
   "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
   unfolding Collect_finite_subset_eq_lists by auto
 
+lemma countable_set_option [simp]: "countable (set_option x)"
+by(cases x) auto
+
 subsection {* Misc lemmas *}
 
 lemma countable_all:
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -341,7 +341,30 @@
 lemmas cin_mono = in_mono[Transfer.transferred]
 lemmas cLeast_mono = Least_mono[Transfer.transferred]
 lemmas cequalityI = equalityI[Transfer.transferred]
-
+lemmas cUnion_cimage_eq [simp] = Union_image_eq[Transfer.transferred]
+lemmas cUN_iff [simp] = UN_iff[Transfer.transferred]
+lemmas cUN_I [intro] = UN_I[Transfer.transferred]
+lemmas cUN_E [elim!] = UN_E[Transfer.transferred]
+lemmas cimage_eq_cUN = image_eq_UN[Transfer.transferred]
+lemmas cUN_upper = UN_upper[Transfer.transferred]
+lemmas cUN_least = UN_least[Transfer.transferred]
+lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred]
+lemmas cUN_empty [simp] = UN_empty[Transfer.transferred]
+lemmas cUN_empty2 [simp] = UN_empty2[Transfer.transferred]
+lemmas cUN_absorb = UN_absorb[Transfer.transferred]
+lemmas cUN_cinsert [simp] = UN_insert[Transfer.transferred]
+lemmas cUN_cUn [simp] = UN_Un[Transfer.transferred]
+lemmas cUN_cUN_flatten = UN_UN_flatten[Transfer.transferred]
+lemmas cUN_csubset_iff = UN_subset_iff[Transfer.transferred]
+lemmas cUN_constant [simp] = UN_constant[Transfer.transferred]
+lemmas cimage_cUnion = image_Union[Transfer.transferred]
+lemmas cUNION_cempty_conv [simp] = UNION_empty_conv[Transfer.transferred]
+lemmas cBall_cUN = ball_UN[Transfer.transferred]
+lemmas cBex_cUN = bex_UN[Transfer.transferred]
+lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred]
+lemmas cUN_mono = UN_mono[Transfer.transferred]
+lemmas cimage_cUN = image_UN[Transfer.transferred]
+lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred]
 
 subsection {* Additional lemmas*}
 
@@ -395,6 +418,11 @@
 apply (rule equal_intr_rule)
 by (transfer, simp)+
 
+subsubsection {* @{const cUnion} *}
+
+lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)"
+including cset.lifting by transfer auto
+
 
 subsection {* Setup for Lifting/Transfer *}
 
@@ -415,6 +443,14 @@
    (\<forall>t. cin t b \<longrightarrow> (\<exists>u. cin u a \<and> R u t))"
 by transfer(auto simp add: rel_set_def)
 
+lemma rel_cset_cUNION:
+  "\<lbrakk> rel_cset Q A B; rel_fun Q (rel_cset R) f g \<rbrakk>
+  \<Longrightarrow> rel_cset R (cUNION A f) (cUNION B g)"
+unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def)
+
+lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y"
+by transfer(auto simp add: rel_set_def)
+
 subsubsection {* Transfer rules for the Transfer package *}
 
 text {* Unconditional transfer rules *}
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -298,6 +298,10 @@
 
 end
 
+lemma ereal_0_plus [simp]: "ereal 0 + x = x"
+  and plus_ereal_0 [simp]: "x + ereal 0 = x"
+by(simp_all add: zero_ereal_def[symmetric])
+
 instance ereal :: numeral ..
 
 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
@@ -1286,6 +1290,9 @@
   shows "real (a - b) = (if \<bar>a\<bar> = \<infinity> \<or> \<bar>b\<bar> = \<infinity> then 0 else real a - real b)"
   by (cases rule: ereal2_cases[of a b]) auto
 
+lemma real_of_ereal_minus': "\<bar>x\<bar> = \<infinity> \<longleftrightarrow> \<bar>y\<bar> = \<infinity> \<Longrightarrow> real x - real y = real (x - y :: ereal)"
+by(subst real_of_ereal_minus) auto
+
 lemma ereal_diff_positive:
   fixes a b :: ereal shows "a \<le> b \<Longrightarrow> 0 \<le> b - a"
   by (cases rule: ereal2_cases[of a b]) auto
@@ -1428,6 +1435,14 @@
   shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
   by (cases x) auto
 
+lemma ereal_inverse_le_0_iff:
+  fixes x :: ereal
+  shows "inverse x \<le> 0 \<longleftrightarrow> x < 0 \<or> x = \<infinity>"
+  by(cases x) auto
+
+lemma ereal_divide_eq_0_iff: "x / y = 0 \<longleftrightarrow> x = 0 \<or> \<bar>y :: ereal\<bar> = \<infinity>"
+by(cases x y rule: ereal2_cases) simp_all
+
 lemma ereal_mult_less_right:
   fixes a b c :: ereal
   assumes "b * a < c * a"
@@ -1971,7 +1986,7 @@
   assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
   shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
 proof cases
-  assume "(SUP i:I. f i) = 0"
+  assume "(SUP i: I. f i) = 0"
   moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
     by (metis SUP_upper f antisym)
   ultimately show ?thesis
@@ -2646,6 +2661,38 @@
   finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
 qed
 
+lemma Sup_ereal_mult_right':
+  assumes nonempty: "Y \<noteq> {}"
+  and x: "x \<ge> 0"
+  shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs")
+proof(cases "x = 0")
+  case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
+next
+  case False
+  show ?thesis
+  proof(rule antisym)
+    show "?rhs \<le> ?lhs"
+      by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x)
+  next
+    have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
+    also have "\<dots> = (SUP i:Y. f i)" using False by simp
+    also have "\<dots> \<le> ?rhs / x"
+    proof(rule SUP_least)
+      fix i
+      assume "i \<in> Y"
+      have "f i = f i * (ereal x / ereal x)" using False by simp
+      also have "\<dots> = f i * x / x" by(simp only: ereal_times_divide_eq)
+      also from \<open>i \<in> Y\<close> have "f i * x \<le> ?rhs" by(rule SUP_upper)
+      hence "f i * x / x \<le> ?rhs / x" using x False by simp
+      finally show "f i \<le> ?rhs / x" .
+    qed
+    finally have "(?lhs / x) * x \<le> (?rhs / x) * x"
+      by(rule ereal_mult_right_mono)(simp add: x)
+    also have "\<dots> = ?rhs" using False ereal_divide_eq mult.commute by force
+    also have "(?lhs / x) * x = ?lhs" using False ereal_divide_eq mult.commute by force
+    finally show "?lhs \<le> ?rhs" .
+  qed
+qed
 
 subsubsection {* Tests for code generator *}
 
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Lifting_Set.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -281,4 +281,9 @@
 lemmas setsum_parametric = setsum.F_parametric
 lemmas setprod_parametric = setprod.F_parametric
 
+lemma rel_set_UNION:
+  assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
+  shows "rel_set R (UNION A f) (UNION B g)"
+by transfer_prover
+
 end
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Map.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -641,6 +641,8 @@
   ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
 qed
 
+lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
+by(auto simp add: ran_def)
 
 subsection {* @{text "map_le"} *}
 
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Partial_Function.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -12,6 +12,40 @@
 named_theorems partial_function_mono "monotonicity rules for partial function definitions"
 ML_file "Tools/Function/partial_function.ML"
 
+lemma (in ccpo) in_chain_finite:
+  assumes "Complete_Partial_Order.chain op \<le> A" "finite A" "A \<noteq> {}"
+  shows "\<Squnion>A \<in> A"
+using assms(2,1,3)
+proof induction
+  case empty thus ?case by simp
+next
+  case (insert x A)
+  note chain = `Complete_Partial_Order.chain op \<le> (insert x A)`
+  show ?case
+  proof(cases "A = {}")
+    case True thus ?thesis by simp
+  next
+    case False
+    from chain have chain': "Complete_Partial_Order.chain op \<le> A"
+      by(rule chain_subset) blast
+    hence "\<Squnion>A \<in> A" using False by(rule insert.IH)
+    show ?thesis
+    proof(cases "x \<le> \<Squnion>A")
+      case True
+      have "\<Squnion>insert x A \<le> \<Squnion>A" using chain
+        by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
+      hence "\<Squnion>insert x A = \<Squnion>A"
+        by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
+      with `\<Squnion>A \<in> A` show ?thesis by simp
+    next
+      case False
+      with chainD[OF chain, of x "\<Squnion>A"] `\<Squnion>A \<in> A`
+      have "\<Squnion>insert x A = x"
+        by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
+      thus ?thesis by simp
+    qed
+  qed
+qed
 
 subsection {* Axiomatic setup *}
 
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -1056,6 +1056,13 @@
   finally show ?thesis .
 qed
 
+lemma measurable_pair_measure_countable1:
+  assumes "countable A"
+  and [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N K"
+  shows "f \<in> measurable (count_space A \<Otimes>\<^sub>M N) K"
+using _ _ assms(1)
+by(rule measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A, simplified])simp_all
+
 subsection {* Product of Borel spaces *}
 
 lemma borel_Times:
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -1875,6 +1875,15 @@
   qed
 qed (simp add: integrable_restrict_space)
 
+lemma integral_empty:
+  assumes "space M = {}"
+  shows "integral\<^sup>L M f = 0"
+proof -
+  have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
+    by(rule integral_cong)(simp_all add: assms)
+  thus ?thesis by simp
+qed
+
 subsection {* Measure spaces with an associated density *}
 
 lemma integrable_density:
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Embed_Measure.thy
--- a/src/HOL/Probability/Embed_Measure.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -110,13 +110,18 @@
     "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
   by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
 
+lemma nn_integral_embed_measure':
+  "inj_on f (space M) \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
+  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
+  apply (subst embed_measure_eq_distr', simp)
+  apply (subst nn_integral_distr)
+  apply (simp_all add: measurable_embed_measure2')
+  done
+
 lemma nn_integral_embed_measure:
   "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
-  apply (subst embed_measure_eq_distr, simp)
-  apply (subst nn_integral_distr)
-  apply (simp_all add: measurable_embed_measure2)
-  done
+  by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
 
 lemma emeasure_embed_measure':
     assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
@@ -167,18 +172,21 @@
   qed
 qed
 
-lemma embed_measure_count_space: 
-    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
+lemma embed_measure_count_space':
+    "inj_on f A \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   apply (subst distr_bij_count_space[of f A "f`A", symmetric])
   apply (simp add: inj_on_def bij_betw_def)
-  apply (subst embed_measure_eq_distr)
+  apply (subst embed_measure_eq_distr')
   apply simp
-  apply (auto intro!: measure_eqI imageI simp: sets_embed_measure subset_image_iff)
-  apply blast
+  apply(auto 4 3 intro!: measure_eqI imageI simp add: sets_embed_measure' subset_image_iff)
   apply (subst (1 2) emeasure_distr)
-  apply (auto simp: space_embed_measure sets_embed_measure)
+  apply (auto simp: space_embed_measure sets_embed_measure')
   done
 
+lemma embed_measure_count_space: 
+    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
+  by(rule embed_measure_count_space')(erule subset_inj_on, simp)
+
 lemma sets_embed_measure_alt:
     "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
   by (auto simp: sets_embed_measure)
@@ -340,4 +348,33 @@
   shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
 
+lemma nn_integral_monotone_convergence_SUP_countable:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
+  assumes nonempty: "Y \<noteq> {}"
+  and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+  and countable: "countable B"
+  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
+  (is "?lhs = ?rhs")
+proof -
+  let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
+  have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
+    by(rule nn_integral_cong)(simp add: countable)
+  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
+    by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
+  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
+    by(simp add: nn_integral_count_space_indicator ereal_indicator[symmetric] Sup_ereal_mult_right' nonempty)
+  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)" using nonempty
+  proof(rule nn_integral_monotone_convergence_SUP_nat)
+    show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
+      by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
+  qed
+  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
+    by(simp add: nn_integral_count_space_indicator)
+  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
+    by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
+  also have "\<dots> = ?rhs" 
+    by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
+  finally show ?thesis .
+qed
+
 end
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -38,6 +38,12 @@
 sublocale prob_space \<subseteq> subprob_space
   by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
 
+lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)"
+by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv)
+
+lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)"
+by(simp add: null_measure_def)
+
 lemma (in subprob_space) subprob_space_distr:
   assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)"
 proof (rule subprob_spaceI)
@@ -324,6 +330,35 @@
   finally show ?thesis .
 qed
 
+lemma integral_measurable_subprob_algebra:
+  fixes f :: "_ \<Rightarrow> real"
+  assumes f_measurable [measurable]: "f \<in> borel_measurable N"
+  and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"
+  shows "(\<lambda>M. integral\<^sup>L M f) \<in> borel_measurable (subprob_algebra N)"
+proof -
+  note [measurable] = nn_integral_measurable_subprob_algebra
+  have "?thesis \<longleftrightarrow> (\<lambda>M. real (\<integral>\<^sup>+ x. f x \<partial>M) - real (\<integral>\<^sup>+ x. - f x \<partial>M)) \<in> borel_measurable (subprob_algebra N)"
+  proof(rule measurable_cong)
+    fix M
+    assume "M \<in> space (subprob_algebra N)"
+    hence "subprob_space M" and M [measurable_cong]: "sets M = sets N" 
+      by(simp_all add: space_subprob_algebra)
+    interpret subprob_space M by fact
+    have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M)"
+      by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded)
+    also have "\<dots> = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def)
+    also have "\<dots> \<le> ereal (max B 0) * 1"
+      by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def)
+    finally have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" by(auto simp add: max_def)
+    then have "integrable M f" using f_measurable
+      by(auto intro: integrableI_bounded)
+    thus "(\<integral> x. f x \<partial>M) = real (\<integral>\<^sup>+ x. f x \<partial>M) - real (\<integral>\<^sup>+ x. - f x \<partial>M)"
+      by(simp add: real_lebesgue_integral_def)
+  qed
+  also have "\<dots>" by measurable
+  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)"
@@ -796,6 +831,163 @@
   apply (auto simp: f)
   done
 
+lemma measurable_join1:
+  "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk>
+  \<Longrightarrow> f \<in> measurable (join M) K"
+by(simp add: measurable_def)
+
+lemma 
+  fixes f :: "_ \<Rightarrow> real"
+  assumes f_measurable [measurable]: "f \<in> borel_measurable N"
+  and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
+  and M [measurable_cong]: "sets M = sets (subprob_algebra N)"
+  and fin: "finite_measure M"
+  and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ereal B'"
+  shows integrable_join: "integrable (join M) f" (is ?integrable)
+  and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral)
+proof(case_tac [!] "space N = {}")
+  assume *: "space N = {}"
+  show ?integrable 
+    using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
+  have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
+  proof(rule integral_cong)
+    fix M'
+    assume "M' \<in> space M"
+    with sets_eq_imp_space_eq[OF M] have "space M' = space N"
+      by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
+  qed simp
+  then show ?integral
+    using M * by(simp add: integral_empty)
+next
+  assume *: "space N \<noteq> {}"
+
+  from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded)
+
+  have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M
+    by(rule measurable_join1)
+
+  { fix f M'
+    assume [measurable]: "f \<in> borel_measurable N"
+      and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
+      and "M' \<in> space M" "emeasure M' (space M') \<le> ereal B'"
+    have "AE x in M'. ereal (f x) \<le> ereal B"
+    proof(rule AE_I2)
+      fix x
+      assume "x \<in> space M'"
+      with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
+      have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+      from f_bounded[OF this] show "ereal (f x) \<le> ereal B" by simp
+    qed
+    then have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M')"
+      by(rule nn_integral_mono_AE)
+    also have "\<dots> = ereal B * emeasure M' (space M')" by(simp)
+    also have "\<dots> \<le> ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp)
+    also have "\<dots> \<le> ereal B * ereal \<bar>B'\<bar>" by(rule ereal_mult_left_mono)(simp_all)
+    finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" by simp }
+  note bounded1 = this
+
+  have bounded:
+    "\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk>
+    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
+  proof -
+    fix f
+    assume [measurable]: "f \<in> borel_measurable N"
+      and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
+    have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ereal (f x) \<partial>M' \<partial>M)"
+      by(rule nn_integral_join[OF _ M]) simp
+    also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M"
+      using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded]
+      by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format])
+    also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp
+    also have "\<dots> < \<infinity>" by(simp add: finite_measure.finite_emeasure_space[OF fin])
+    finally show "?thesis f" by simp
+  qed
+  have f_pos: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
+    and f_neg: "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>join M) \<noteq> \<infinity>"
+    using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff)
+  
+  show ?integrable using f_pos f_neg by(simp add: real_integrable_def)
+
+  note [measurable] = nn_integral_measurable_subprob_algebra
+
+  have "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>join M)"
+    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (f x) \<partial>M' \<partial>M"
+    by(simp add: nn_integral_join[OF _ M])
+  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M"
+    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+  finally have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" .
+
+  have "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (- f x) \<partial>join M)"
+    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (- f x) \<partial>M' \<partial>M"
+    by(simp add: nn_integral_join[OF _ M])
+  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M"
+    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
+  finally have int_mf: "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" .
+
+  have f_pos1:
+    "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
+    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
+    using f_measurable by(auto intro!: bounded1 dest: f_bounded)
+  have "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>"
+    using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1)
+  hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
+    by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
+  from f_pos have [simp]: "integrable M (\<lambda>M'. real (\<integral>\<^sup>+ x. f x \<partial>M'))"
+    by(simp add: int_f real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)
+
+  have f_neg1:
+    "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
+    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
+    using f_measurable by(auto intro!: bounded1 dest: f_bounded)
+  have "AE M' in M. (\<integral>\<^sup>+ x. - f x \<partial>M') \<noteq> \<infinity>"
+    using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1)
+  hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real (\<integral>\<^sup>+ x. - f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)"
+    by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
+  from f_neg have [simp]: "integrable M (\<lambda>M'. real (\<integral>\<^sup>+ x. - f x \<partial>M'))"
+    by(simp add: int_mf real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)
+
+  from \<open>?integrable\<close>
+  have "ereal (\<integral> x. f x \<partial>join M) = (\<integral>\<^sup>+ x. f x \<partial>join M) - (\<integral>\<^sup>+ x. - f x \<partial>join M)"
+    by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1))
+  also note int_f
+  also note int_mf
+  also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) = 
+    ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)) - 
+    ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M))"
+    by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg)
+  also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) = \<integral> M'. real (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M"
+    using f_pos
+    by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_f nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])
+  also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) = \<integral> M'. real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
+    using f_neg
+    by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_mf nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])
+  also note ereal_minus(1)
+  also have "(\<integral> M'. real (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M) - (\<integral> M'. real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M) = 
+    \<integral>M'. real (\<integral>\<^sup>+ x. f x \<partial>M') - real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
+    by simp
+  also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" using _ _ M_bounded
+  proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format])
+    show "(\<lambda>M'. integral\<^sup>L M' f) \<in> borel_measurable M"
+      by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded])
+      
+    fix M'
+    assume "M' \<in> space M" "emeasure M' (space M') \<le> B'"
+    then interpret finite_measure M' by(auto intro: finite_measureI)
+    
+    from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
+    have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra)
+    hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq)
+    have "integrable M' f"
+      by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded)
+    then show "real (\<integral>\<^sup>+ x. f x \<partial>M') - real (\<integral>\<^sup>+ x. - f x \<partial>M') = \<integral> x. f x \<partial>M'"
+      by(simp add: real_lebesgue_integral_def)
+  qed simp_all
+  finally show ?integral by simp
+qed
+
 lemma join_assoc:
   assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
   shows "join (distr M (subprob_algebra N) join) = join (join M)"
@@ -998,6 +1190,32 @@
     by (simp add: space_subprob_algebra)
 qed
 
+lemma 
+  fixes f :: "_ \<Rightarrow> real"
+  assumes f_measurable [measurable]: "f \<in> borel_measurable K"
+  and f_bounded: "\<And>x. x \<in> space K \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
+  and N [measurable]: "N \<in> measurable M (subprob_algebra K)"
+  and fin: "finite_measure M"
+  and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \<le> ereal B'"
+  shows integrable_bind: "integrable (bind M N) f" (is ?integrable)
+  and integral_bind: "integral\<^sup>L (bind M N) f = \<integral> x. integral\<^sup>L (N x) f \<partial>M" (is ?integral)
+proof(case_tac [!] "space M = {}")
+  assume [simp]: "space M \<noteq> {}"
+  interpret finite_measure M by(rule fin)
+
+  have "integrable (join (distr M (subprob_algebra K) N)) f"
+    using f_measurable f_bounded
+    by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
+  then show ?integrable by(simp add: bind_nonempty''[where N=K])
+
+  have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \<integral> M'. integral\<^sup>L M' f \<partial>distr M (subprob_algebra K) N"
+    using f_measurable f_bounded
+    by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
+  also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
+    by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _ f_bounded])
+  finally show ?integral by(simp add: bind_nonempty''[where N=K])
+qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
+
 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)"
@@ -1142,6 +1360,38 @@
     done
 qed
 
+lemma bind_restrict_space:
+  assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M"
+  and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)"
+  shows "restrict_space M A \<guillemotright>= f = M \<guillemotright>= (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
+  (is "?lhs = ?rhs" is "_ = M \<guillemotright>= ?f")
+proof -
+  let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M"
+  let ?x = "Eps ?P"
+  let ?c = "null_measure (f ?x)"
+  from A have "?P ?x" by-(rule someI_ex, blast)
+  hence "?x \<in> space (restrict_space M A)" by(simp add: space_restrict_space)
+  with f have "f ?x \<in> space (subprob_algebra N)" by(rule measurable_space)
+  hence sps: "subprob_space (f ?x)"
+    and sets: "sets (f ?x) = sets N" 
+    by(simp_all add: space_subprob_algebra)
+  have "space (f ?x) \<noteq> {}" using sps by(rule subprob_space.subprob_not_empty)
+  moreover have "sets ?c = sets N" by(simp add: null_measure_def)(simp add: sets)
+  ultimately have c: "?c \<in> space (subprob_algebra N)"
+    by(simp add: space_subprob_algebra subprob_space_null_measure)
+  from f A c have f': "?f \<in> measurable M (subprob_algebra N)"
+    by(simp add: measurable_restrict_space_iff)
+
+  from A have [simp]: "space M \<noteq> {}" by blast
+
+  have "?lhs = join (distr (restrict_space M A) (subprob_algebra N) f)"
+    using assms by(simp add: space_restrict_space bind_nonempty'')
+  also have "\<dots> = join (distr M (subprob_algebra N) ?f)"
+    by(rule measure_eqI)(auto simp add: emeasure_join nn_integral_distr nn_integral_restrict_space f f' A intro: nn_integral_cong)
+  also have "\<dots> = ?rhs" using f' by(simp add: bind_nonempty'')
+  finally show ?thesis .
+qed
+
 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)
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -1650,7 +1650,6 @@
   with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
 qed
 
-
 subsection {* Counting space *}
 
 lemma strict_monoI_Suc:
@@ -1882,6 +1881,40 @@
     by (cases "finite X") (auto simp add: emeasure_restrict_space)
 qed
 
+lemma sigma_finite_measure_restrict_space:
+  assumes "sigma_finite_measure M"
+  and A: "A \<in> sets M"
+  shows "sigma_finite_measure (restrict_space M A)"
+proof -
+  interpret sigma_finite_measure M by fact
+  from sigma_finite_countable obtain C
+    where C: "countable C" "C \<subseteq> sets M" "(\<Union>C) = space M" "\<forall>a\<in>C. emeasure M a \<noteq> \<infinity>"
+    by blast
+  let ?C = "op \<inter> A ` C"
+  from C have "countable ?C" "?C \<subseteq> sets (restrict_space M A)" "(\<Union>?C) = space (restrict_space M A)"
+    by(auto simp add: sets_restrict_space space_restrict_space)
+  moreover {
+    fix a
+    assume "a \<in> ?C"
+    then obtain a' where "a = A \<inter> a'" "a' \<in> C" ..
+    then have "emeasure (restrict_space M A) a \<le> emeasure M a'"
+      using A C by(auto simp add: emeasure_restrict_space intro: emeasure_mono)
+    also have "\<dots> < \<infinity>" using C(4)[rule_format, of a'] \<open>a' \<in> C\<close> by simp
+    finally have "emeasure (restrict_space M A) a \<noteq> \<infinity>" by simp }
+  ultimately show ?thesis
+    by unfold_locales (rule exI conjI|assumption|blast)+
+qed
+
+lemma finite_measure_restrict_space:
+  assumes "finite_measure M"
+  and A: "A \<in> sets M"
+  shows "finite_measure (restrict_space M A)"
+proof -
+  interpret finite_measure M by fact
+  show ?thesis
+    by(rule finite_measureI)(simp add: emeasure_restrict_space A space_restrict_space)
+qed
+
 lemma restrict_distr: 
   assumes [measurable]: "f \<in> measurable M N"
   assumes [simp]: "\<Omega> \<inter> space N \<in> sets N" and restrict: "f \<in> space M \<rightarrow> \<Omega>"
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -758,6 +758,9 @@
 lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
   using nn_integral_nonneg[of M f] by auto
 
+lemma nn_integral_not_less_0 [simp]: "\<not> nn_integral M f < 0"
+by(simp add: not_less nn_integral_nonneg)
+
 lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
   using nn_integral_nonneg[of M f] by auto
 
@@ -1648,6 +1651,15 @@
 
 subsection {* Integral under concrete measures *}
 
+lemma nn_integral_empty: 
+  assumes "space M = {}"
+  shows "nn_integral M f = 0"
+proof -
+  have "(\<integral>\<^sup>+ x. f x \<partial>M) = (\<integral>\<^sup>+ x. 0 \<partial>M)"
+    by(rule nn_integral_cong)(simp add: assms)
+  thus ?thesis by simp
+qed
+
 subsubsection {* Distributions *}
 
 lemma nn_integral_distr':
@@ -1854,6 +1866,143 @@
   finally show "emeasure M A = emeasure N A" ..
 qed simp
 
+lemma nn_integral_monotone_convergence_SUP_nat':
+  fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
+  assumes chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+  and nonempty: "Y \<noteq> {}"
+  and nonneg: "\<And>i n. i \<in> Y \<Longrightarrow> f i n \<ge> 0"
+  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
+  (is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _")
+proof (rule order_class.order.antisym)
+  show "?rhs \<le> ?lhs"
+    by (auto intro!: SUP_least SUP_upper nn_integral_mono)
+next
+  have "\<And>x. \<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)"
+    unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty)
+  then obtain g where incseq: "\<And>x. incseq (g x)"
+    and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
+    and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
+  from incseq have incseq': "incseq (\<lambda>i x. g x i)"
+    by(blast intro: incseq_SucI le_funI dest: incseq_SucD)
+
+  have "?lhs = \<integral>\<^sup>+ x. (SUP i. g x i) \<partial>?M" by(simp add: sup)
+  also have "\<dots> = (SUP i. \<integral>\<^sup>+ x. g x i \<partial>?M)" using incseq'
+    by(rule nn_integral_monotone_convergence_SUP) simp
+  also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+  proof(rule SUP_least)
+    fix n
+    have "\<And>x. \<exists>i. g x n = f i x \<and> i \<in> Y" using range by blast
+    then obtain I where I: "\<And>x. g x n = f (I x) x" "\<And>x. I x \<in> Y" by moura
+
+    { fix x
+      from range[of x] obtain i where "i \<in> Y" "g x n = f i x" by auto
+      hence "g x n \<ge> 0" using nonneg[of i x] by simp }
+    note nonneg_g = this
+    then have "(\<integral>\<^sup>+ x. g x n \<partial>count_space UNIV) = (\<Sum>x. g x n)"
+      by(rule nn_integral_count_space_nat)
+    also have "\<dots> = (SUP m. \<Sum>x<m. g x n)" using nonneg_g
+      by(rule suminf_ereal_eq_SUP)
+    also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+    proof(rule SUP_mono)
+      fix m
+      show "\<exists>m'\<in>Y. (\<Sum>x<m. g x n) \<le> (\<integral>\<^sup>+ x. f m' x \<partial>?M)"
+      proof(cases "m > 0")
+        case False
+        thus ?thesis using nonempty by(auto simp add: nn_integral_nonneg)
+      next
+        case True
+        let ?Y = "I ` {..<m}"
+        have "f ` ?Y \<subseteq> f ` Y" using I by auto
+        with chain have chain': "Complete_Partial_Order.chain op \<le> (f ` ?Y)" by(rule chain_subset)
+        hence "Sup (f ` ?Y) \<in> f ` ?Y"
+          by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff)
+        then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto
+        have "I m' \<in> Y" using I by blast
+        have "(\<Sum>x<m. g x n) \<le> (\<Sum>x<m. f (I m') x)"
+        proof(rule setsum_mono)
+          fix x
+          assume "x \<in> {..<m}"
+          hence "x < m" by simp
+          have "g x n = f (I x) x" by(simp add: I)
+          also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image
+            using \<open>x \<in> {..<m}\<close> by(rule Sup_upper[OF imageI])
+          also have "\<dots> = f (I m') x" unfolding m' by simp
+          finally show "g x n \<le> f (I m') x" .
+        qed
+        also have "\<dots> \<le> (SUP m. (\<Sum>x<m. f (I m') x))"
+          by(rule SUP_upper) simp
+        also have "\<dots> = (\<Sum>x. f (I m') x)"
+          by(rule suminf_ereal_eq_SUP[symmetric])(simp add: nonneg \<open>I m' \<in> Y\<close>)
+        also have "\<dots> = (\<integral>\<^sup>+ x. f (I m') x \<partial>?M)"
+          by(rule nn_integral_count_space_nat[symmetric])(simp add: nonneg \<open>I m' \<in> Y\<close>)
+        finally show ?thesis using \<open>I m' \<in> Y\<close> by blast
+      qed
+    qed
+    finally show "(\<integral>\<^sup>+ x. g x n \<partial>count_space UNIV) \<le> \<dots>" .
+  qed
+  finally show "?lhs \<le> ?rhs" .
+qed
+
+lemma nn_integral_monotone_convergence_SUP_nat:
+  fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
+  assumes nonempty: "Y \<noteq> {}"
+  and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
+  (is "?lhs = ?rhs")
+proof -
+  let ?f = "\<lambda>i x. max 0 (f i x)"
+  have chain': "Complete_Partial_Order.chain op \<le> (?f ` Y)"
+  proof(rule chainI)
+    fix g h
+    assume "g \<in> ?f ` Y" "h \<in> ?f ` Y"
+    then obtain g' h' where gh: "g' \<in> Y" "h' \<in> Y" "g = ?f g'" "h = ?f h'" by blast
+    hence "f g' \<in> f ` Y" "f h' \<in> f ` Y" by blast+
+    with chain have "f g' \<le> f h' \<or> f h' \<le> f g'" by(rule chainD)
+    thus "g \<le> h \<or> h \<le> g"
+    proof
+      assume "f g' \<le> f h'"
+      hence "g \<le> h" using gh order_trans by(auto simp add: le_fun_def max_def)
+      thus ?thesis ..
+    next
+      assume "f h' \<le> f g'"
+      hence "h \<le> g" using gh order_trans by(auto simp add: le_fun_def max_def)
+      thus ?thesis ..
+    qed
+  qed
+  have "?lhs = (\<integral>\<^sup>+ x. max 0 (SUP i:Y. f i x) \<partial>count_space UNIV)"
+    by(simp add: nn_integral_max_0)
+  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV)"
+  proof(rule nn_integral_cong)
+    fix x
+    have "max 0 (SUP i:Y. f i x) \<le> (SUP i:Y. ?f i x)"
+    proof(cases "0 \<le> (SUP i:Y. f i x)")
+      case True
+      have "(SUP i:Y. f i x) \<le> (SUP i:Y. ?f i x)" by(rule SUP_mono)(auto intro: rev_bexI)
+      with True show ?thesis by simp
+    next
+      case False
+      have "0 \<le> (SUP i:Y. ?f i x)" using nonempty by(auto intro: SUP_upper2)
+      thus ?thesis using False by simp
+    qed
+    moreover have "\<dots> \<le> max 0 (SUP i:Y. f i x)"
+    proof(cases "(SUP i:Y. f i x) \<ge> 0")
+      case True
+      show ?thesis
+        by(rule SUP_least)(auto simp add: True max_def intro: SUP_upper)
+    next
+      case False
+      hence "(SUP i:Y. f i x) \<le> 0" by simp
+      hence less: "\<forall>i\<in>Y. f i x \<le> 0" by(simp add: SUP_le_iff)
+      show ?thesis by(rule SUP_least)(auto simp add: max_def less intro: SUP_upper)
+    qed
+    ultimately show "\<dots> = (SUP i:Y. ?f i x)" by(rule order.antisym)
+  qed
+  also have "\<dots> = (SUP i:Y. (\<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV))"
+    using chain' nonempty by(rule nn_integral_monotone_convergence_SUP_nat') simp
+  also have "\<dots> = ?rhs" by(simp add: nn_integral_max_0)
+  finally show ?thesis .
+qed
+
 subsubsection {* Measures with Restricted Space *}
 
 lemma simple_function_iff_borel_measurable:
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -224,6 +224,9 @@
   shows "emeasure M {x} = pmf M x"
   by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
 
+lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x"
+using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure)
+
 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)
 
@@ -510,13 +513,13 @@
   finally show ?thesis .
 qed
 
-lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
+lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
   by transfer (simp add: distr_return)
 
 lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c"
   by transfer (auto simp: prob_space.distr_const)
 
-lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
+lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x"
   by transfer (simp add: measure_return)
 
 lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
@@ -592,7 +595,7 @@
   then show "emeasure ?L X = emeasure ?R X"
     apply (simp add: emeasure_bind[OF _ M' X])
     apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
-                     nn_integral_measure_pmf_finite emeasure_nonneg pmf_return one_ereal_def[symmetric])
+                     nn_integral_measure_pmf_finite emeasure_nonneg one_ereal_def[symmetric])
     apply (subst emeasure_bind[OF _ _ X])
     apply measurable
     apply (subst emeasure_bind[OF _ _ X])
@@ -624,6 +627,16 @@
   by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD
            intro!: measure_pmf.finite_measure_eq_AE)
 
+lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x"
+apply(cases "x \<in> set_pmf M")
+ apply(simp add: pmf_map_inj[OF subset_inj_on])
+apply(simp add: pmf_eq_0_set_pmf[symmetric])
+apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
+done
+
+lemma pmf_map_outside: "x \<notin> f ` set_pmf M \<Longrightarrow> pmf (map_pmf f M) x = 0"
+unfolding pmf_eq_0_set_pmf by simp
+
 subsection \<open> PMFs as function \<close>
 
 context
@@ -651,6 +664,9 @@
     by transfer (simp add: measure_def emeasure_density nonneg max_def)
 qed
 
+lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
+by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
+
 end
 
 lemma embed_pmf_transfer:
@@ -700,6 +716,9 @@
 
 end
 
+lemma nn_integral_measure_pmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_pmf p) = \<integral>\<^sup>+ x. ereal (pmf p x) * f x \<partial>count_space UNIV"
+by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg)
+
 locale pmf_as_function
 begin
 
@@ -896,11 +915,11 @@
   then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
     by auto
   show "map_pmf fst ?pq = p"
-    by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
+    by (simp add: map_bind_pmf bind_return_pmf')
 
   show "map_pmf snd ?pq = q"
     using R eq
-    apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
+    apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf')
     apply (rule bind_cond_pmf_cancel)
     apply (auto simp: rel_set_def)
     done
@@ -1064,10 +1083,10 @@
         by blast
     next
       have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
-        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf map_pmf_comp)
+        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
       then show "map_pmf snd pr = r"
         unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
-    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
+    qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) }
   then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
     by(auto simp add: le_fun_def)
 qed (fact natLeq_card_order natLeq_cinfinite)+
@@ -1420,8 +1439,59 @@
 lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
   by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
 
+lemma nn_integral_pmf_of_set': 
+  "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
+apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite)
+apply(simp add: setsum_ereal_left_distrib[symmetric])
+apply(subst ereal_divide', simp add: S_not_empty S_finite)
+apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric])
+done
+
+lemma nn_integral_pmf_of_set: 
+  "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S"
+apply(subst nn_integral_max_0[symmetric])
+apply(subst nn_integral_pmf_of_set')
+apply simp_all
+done
+
+lemma integral_pmf_of_set:
+  "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"
+apply(simp add: real_lebesgue_integral_def integrable_measure_pmf_finite nn_integral_pmf_of_set S_finite)
+apply(subst real_of_ereal_minus')
+ apply(simp add: ereal_max_0 S_finite del: ereal_max)
+apply(simp add: ereal_max_0 S_finite S_not_empty del: ereal_max)
+apply(simp add: field_simps S_finite S_not_empty)
+apply(subst setsum.distrib[symmetric])
+apply(rule setsum.cong; simp_all)
+done
+
 end
 
+lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
+by(rule pmf_eqI)(simp add: indicator_def)
+
+lemma map_pmf_of_set_inj: 
+  assumes f: "inj_on f A"
+  and [simp]: "A \<noteq> {}" "finite A"
+  shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs")
+proof(rule pmf_eqI)
+  fix i
+  show "pmf ?lhs i = pmf ?rhs i"
+  proof(cases "i \<in> f ` A")
+    case True
+    then obtain i' where "i = f i'" "i' \<in> A" by auto
+    thus ?thesis using f by(simp add: card_image pmf_map_inj)
+  next
+    case False
+    hence "pmf ?lhs i = 0" by(simp add: pmf_eq_0_set_pmf set_map_pmf)
+    moreover have "pmf ?rhs i = 0" using False by simp
+    ultimately show ?thesis by simp
+  qed
+qed
+
+lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
+by(rule pmf_eqI) simp_all
+
 subsubsection \<open> Poisson Distribution \<close>
 
 context
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -2361,6 +2361,10 @@
     by simp
 qed
 
+lemma sets_restrict_space_count_space :
+  "sets (restrict_space (count_space A) B) = sets (count_space (A \<inter> B))"
+by(auto simp add: sets_restrict_space)
+
 lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M"
   by (auto simp add: sets_restrict_space)
 
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Product_Type.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -1224,6 +1224,18 @@
     using * eq[symmetric] by auto
 qed simp_all
 
+lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
+by(auto simp add: inj_on_def)
+
+lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
+using inj_on_apfst[of f UNIV] by simp
+
+lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
+by(auto simp add: inj_on_def)
+
+lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
+using inj_on_apsnd[of f UNIV] by simp
+
 definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
   [code_abbrev]: "product A B = A \<times> B"
 
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Relation.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -216,6 +216,8 @@
   "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
   by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
 
+lemma reflp_equality [simp]: "reflp op ="
+by(simp add: reflp_def)
 
 subsubsection {* Irreflexivity *}
 
@@ -357,6 +359,8 @@
 lemma antisym_empty [simp]: "antisym {}"
   by (unfold antisym_def) blast
 
+lemma antisymP_equality [simp]: "antisymP op ="
+by(auto intro: antisymI)
 
 subsubsection {* Transitivity *}
 
diff -r 71c1b9b9e937 -r d76f9047121c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Apr 14 15:54:17 2015 +0200
+++ b/src/HOL/Set.thy	Tue Apr 14 15:56:55 2015 +0200
@@ -647,7 +647,6 @@
 lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
 by blast
 
-
 subsubsection {* The Powerset operator -- Pow *}
 
 definition Pow :: "'a set => 'a set set" where
@@ -846,6 +845,9 @@
   assume ?R thus ?L by (auto split: if_splits)
 qed
 
+lemma insert_UNIV: "insert x UNIV = UNIV"
+by auto
+
 subsubsection {* Singletons, using insert *}
 
 lemma singletonI [intro!]: "a : {a}"
@@ -1884,6 +1886,8 @@
 lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
   by (auto simp add: bind_def)
 
+lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
+  by(auto simp add: bind_def)
 
 subsubsection {* Operations for execution *}