cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory

--- a/src/HOL/Library/Extended_Real.thy	Fri Nov 14 08:18:58 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Nov 14 13:18:33 2014 +0100
@@ -863,13 +863,13 @@
 
 lemma ereal_left_mult_cong:
   fixes a b c :: ereal
-  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
+  shows  "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d"
   by (cases "c = 0") simp_all
 
 lemma ereal_right_mult_cong: 
-  fixes a b c d :: ereal
+  fixes a b c :: ereal
   shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
-  by (cases "d = 0") simp_all
+  by (cases "c = 0") simp_all
 
 lemma ereal_distrib:
   fixes a b c :: ereal
@@ -891,6 +891,10 @@
   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 setsum_ereal_left_distrib:
+  "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
+  using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
+
 lemma ereal_le_epsilon:
   fixes x y :: ereal
   assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"

--- a/src/HOL/Library/Indicator_Function.thy	Fri Nov 14 08:18:58 2014 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Fri Nov 14 13:18:33 2014 +0100
@@ -57,6 +57,9 @@
 lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
   unfolding indicator_def by (cases x) auto
 
+lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
+  by (auto simp: indicator_def inj_on_def)
+
 lemma
   fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
   shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"

--- a/src/HOL/Probability/Giry_Monad.thy	Fri Nov 14 08:18:58 2014 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Nov 14 13:18:33 2014 +0100
@@ -785,7 +785,7 @@
       \<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 nn_integral_bind:
+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)"
@@ -795,6 +795,15 @@
     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 nn_integral_bind:
+  assumes [measurable]: "f \<in> borel_measurable B"
+  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)"
+  apply (subst (1 3) nn_integral_max_0[symmetric])
+  apply (rule nn_integral_bind'[OF _ _ N])
+  apply auto
+  done
+
 lemma AE_bind:
   assumes P[measurable]: "Measurable.pred B P"
   assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"

--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Nov 14 08:18:58 2014 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Nov 14 13:18:33 2014 +0100
@@ -552,7 +552,7 @@
     (\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M. 
       if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))"
     unfolding simple_integral_def
-  proof (safe intro!: setsum.cong ereal_left_mult_cong)
+  proof (safe intro!: setsum.cong ereal_right_mult_cong)
     fix y assume y: "y \<in> space M" "f y \<noteq> 0"
     have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 
         {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
@@ -1894,7 +1894,7 @@
   using simple_function_restrict_space_ereal[THEN iffD1, OF \<Omega>, THEN simple_functionD(1)]
   by (auto simp add: space_restrict_space emeasure_restrict_space[OF \<Omega>(1)] le_infI2 simple_integral_def
            split: split_indicator split_indicator_asm
-           intro!: setsum.mono_neutral_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure])
+           intro!: setsum.mono_neutral_cong_left ereal_right_mult_cong[OF refl] arg_cong2[where f=emeasure])
 
 lemma one_not_less_zero[simp]: "\<not> 1 < (0::ereal)"
   by (simp add: zero_ereal_def one_ereal_def) 

--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 08:18:58 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 13:18:33 2014 +0100
@@ -281,6 +281,12 @@
   unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] map_pmf.rep_eq
   by (auto simp add: emeasure_distr AE_measure_pmf_iff intro!: emeasure_eq_AE measure_eqI)
 
+lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
+  unfolding map_pmf.rep_eq by (subst emeasure_distr) auto
+
+lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)"
+  unfolding map_pmf.rep_eq by (intro nn_integral_distr) auto
+
 lemma pmf_set_map: 
   fixes f :: "'a \<Rightarrow> 'b"
   shows "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
@@ -433,6 +439,17 @@
 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)
 
+lemma nn_integral_bernoulli_pmf[simp]: 
+  assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
+  shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
+  by (subst nn_integral_measure_pmf_support[of UNIV])
+     (auto simp: UNIV_bool field_simps)
+
+lemma integral_bernoulli_pmf[simp]: 
+  assumes [simp]: "0 \<le> p" "p \<le> 1"
+  shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
+  by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
+
 lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
 proof
   note geometric_sums[of "1 / 2"]
@@ -445,7 +462,7 @@
 lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n"
   by transfer rule
 
-lemma set_pmf_geometric: "set_pmf geometric_pmf = UNIV"
+lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV"
   by (auto simp: set_pmf_iff)
 
 context
@@ -485,6 +502,9 @@
 lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
   using S_finite S_not_empty by (auto simp: set_pmf_iff)
 
+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)
+
 end
 
 end
@@ -558,12 +578,18 @@
 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}"
+lemma set_return_pmf: "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)
 
+lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
+  unfolding return_pmf.rep_eq by (intro nn_integral_return) auto
+
+lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
+  unfolding return_pmf.rep_eq by (intro emeasure_return) auto
+
 end
 
 definition "bind_pmf M f = join_pmf (map_pmf f M)"
@@ -584,6 +610,41 @@
 lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
   unfolding bind_pmf_def map_return_pmf join_return_pmf ..
 
+lemma set_bind_pmf: "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 measurable_pair_restrict_pmf2:
+  assumes "countable A"
+  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
+  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
+  apply (subst measurable_cong_sets)
+  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
+  apply (simp_all add: restrict_count_space)
+  apply (subst split_eta[symmetric])
+  unfolding measurable_split_conv
+  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
+  apply (rule measurable_compose[OF measurable_fst])
+  apply fact
+  done
+
+lemma measurable_pair_restrict_pmf1:
+  assumes "countable A"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
+  shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
+  apply (subst measurable_cong_sets)
+  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
+  apply (simp_all add: restrict_count_space)
+  apply (subst split_eta[symmetric])
+  unfolding measurable_split_conv
+  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
+  apply (rule measurable_compose[OF measurable_snd])
+  apply fact
+  done
+                                
 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
@@ -601,36 +662,15 @@
   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
+    by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
+              countable_set_pmf borel_measurable_count_space)
   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
+    by (rule AB.Fubini_integral[symmetric])
+       (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2
+             simp: pmf_nonneg pmf_le_1 countable_set_pmf measurable_restrict_space1)
   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
+    by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
+              countable_set_pmf borel_measurable_count_space)
   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)" .
@@ -642,6 +682,22 @@
 
 interpretation pmf_as_measure .
 
+lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
+  by transfer simp
+
+lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
+  using measurable_measure_pmf[of N]
+  unfolding measure_pmf_bind
+  apply (subst (1 3) nn_integral_max_0[symmetric])
+  apply (intro nn_integral_bind[where B="count_space UNIV"])
+  apply auto
+  done
+
+lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\<integral>\<^sup>+x. emeasure (N x) X \<partial>M)"
+  using measurable_measure_pmf[of N]
+  unfolding measure_pmf_bind
+  by (subst emeasure_bind[where N="count_space UNIV"]) auto
+
 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"
@@ -661,9 +717,6 @@
      (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)))"
@@ -676,6 +729,9 @@
   apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
   done
 
+lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
+  unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
+
 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))))"
@@ -700,18 +756,18 @@
   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 (subst nn_integral_bind)
     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 (subst nn_integral_bind)
     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 (simp add: nn_integral_measure_pmf_finite set_return_pmf 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"])
@@ -727,15 +783,6 @@
     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
 
 (*