# HG changeset patch
# User Andreas Lochbihler
# Date 1447234102 -3600
# Node ID 48e2de1b1df52b1a905a1a7db9fad628d2fa0a4e
# Parent  64e6d712af165cd5b8409dc7f1a39e767466b3dc
add various lemmas

diff -r 64e6d712af16 -r 48e2de1b1df5 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Wed Nov 11 10:13:40 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Wed Nov 11 10:28:22 2015 +0100
@@ -1567,4 +1567,8 @@
   by (rule measure_eqI) 
      (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
 
+lemma null_measure_in_space_subprob_algebra [simp]:
+  "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}"
+by(simp add: space_subprob_algebra subprob_space_null_measure_iff)
+
 end
diff -r 64e6d712af16 -r 48e2de1b1df5 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Nov 11 10:13:40 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Nov 11 10:28:22 2015 +0100
@@ -2106,6 +2106,56 @@
 lemma null_measure_idem [simp]: "null_measure (null_measure M) = null_measure M"
 by(rule measure_eqI) simp_all
 
+subsection \<open>Scaling a measure\<close>
+
+definition scale_measure :: "real \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+where "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. (max 0 r) * emeasure M A)"
+
+lemma space_scale_measure: "space (scale_measure r M) = space M"
+by(simp add: scale_measure_def)
+
+lemma sets_scale_measure [simp, measurable_cong]: "sets (scale_measure r M) = sets M"
+by(simp add: scale_measure_def)
+
+lemma emeasure_scale_measure [simp]:
+  "emeasure (scale_measure r M) A = max 0 r * emeasure M A"
+  (is "_ = ?\<mu> A")
+proof(cases "A \<in> sets M")
+  case True
+  show ?thesis unfolding scale_measure_def
+  proof(rule emeasure_measure_of_sigma)
+    show "sigma_algebra (space M) (sets M)" ..
+    show "positive (sets M) ?\<mu>" by(simp add: positive_def emeasure_nonneg)
+    show "countably_additive (sets M) ?\<mu>"
+    proof (rule countably_additiveI)
+      fix A :: "nat \<Rightarrow> _"  assume *: "range A \<subseteq> sets M" "disjoint_family A"
+      have "(\<Sum>i. ?\<mu> (A i)) = max 0 (ereal r) * (\<Sum>i. emeasure M (A i))"
+        by(rule suminf_cmult_ereal)(simp_all add: emeasure_nonneg)
+      also have "\<dots> = ?\<mu> (\<Union>i. A i)" using * by(simp add: suminf_emeasure)
+      finally show "(\<Sum>i. ?\<mu> (A i)) = ?\<mu> (\<Union>i. A i)" .
+    qed
+  qed(fact True)
+qed(simp add: emeasure_notin_sets)
+
+lemma measure_scale_measure [simp]: "measure (scale_measure r M) A = max 0 r * measure M A"
+by(simp add: measure_def max_def)
+
+lemma scale_measure_1 [simp]: "scale_measure 1 M = M"
+by(rule measure_eqI)(simp_all add: max_def)
+
+lemma scale_measure_le_0: "r \<le> 0 \<Longrightarrow> scale_measure r M = null_measure M"
+by(rule measure_eqI)(simp_all add: max_def)
+
+lemma scale_measure_0 [simp]: "scale_measure 0 M = null_measure M"
+by(simp add: scale_measure_le_0)
+
+lemma scale_scale_measure [simp]:
+  "scale_measure r (scale_measure r' M) = scale_measure (max 0 r * max 0 r') M"
+by(rule measure_eqI)(simp_all add: max_def mult.assoc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
+
+lemma scale_null_measure [simp]: "scale_measure r (null_measure M) = null_measure M"
+by(rule measure_eqI) simp_all
+
 subsection \<open>Measures form a chain-complete partial order\<close>
 
 instantiation measure :: (type) order_bot
diff -r 64e6d712af16 -r 48e2de1b1df5 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Nov 11 10:13:40 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Nov 11 10:28:22 2015 +0100
@@ -2719,4 +2719,32 @@
   "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True"
 by(simp_all add: sets_uniform_count_measure)
 
+subsubsection \<open>Scaled measure\<close>
+
+lemma nn_integral_scale_measure':
+  assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x"
+  shows "nn_integral (scale_measure r M) f = max 0 r * nn_integral M f"
+  using f
+proof induction
+  case (cong f g)
+  thus ?case
+    by(simp add: cong.hyps space_scale_measure cong: nn_integral_cong_simp)
+next
+  case (mult f c)
+  thus ?case
+    by(simp add: nn_integral_cmult max_def mult.assoc mult.left_commute)
+next
+  case (add f g)
+  thus ?case
+    by(simp add: nn_integral_add ereal_right_distrib nn_integral_nonneg)
+next
+  case (seq U)
+  thus ?case
+    by(simp add: nn_integral_monotone_convergence_SUP SUP_ereal_mult_left nn_integral_nonneg)
+qed simp
+
+lemma nn_integral_scale_measure:
+  "f \<in> borel_measurable M \<Longrightarrow> nn_integral (scale_measure r M) f = max 0 r * nn_integral M f"
+by(subst (1 2) nn_integral_max_0[symmetric])(rule nn_integral_scale_measure', simp_all)
+
 end
diff -r 64e6d712af16 -r 48e2de1b1df5 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Nov 11 10:13:40 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Nov 11 10:28:22 2015 +0100
@@ -144,6 +144,9 @@
 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
 
+lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1"
+using measure_pmf.prob_space[of p] by simp
+
 lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
   by (simp add: space_subprob_algebra subprob_space_measure_pmf)
 
@@ -198,6 +201,9 @@
   using AE_measure_singleton[of M] AE_measure_pmf[of M]
   by (auto simp: set_pmf.rep_eq)
 
+lemma AE_pmfI: "(\<And>y. y \<in> set_pmf M \<Longrightarrow> P y) \<Longrightarrow> almost_everywhere (measure_pmf M) P"
+by(simp add: AE_measure_pmf_iff)
+
 lemma countable_set_pmf [simp]: "countable (set_pmf p)"
   by transfer (metis prob_space.finite_measure finite_measure.countable_support)
 
@@ -487,6 +493,9 @@
 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 measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)"
+using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure)
+
 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
 
@@ -810,6 +819,67 @@
 
 end
 
+lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y"
+by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
+
+lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\<lambda>x. (x, y)) x"
+by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
+
+lemma pair_pair_pmf: "pair_pmf (pair_pmf u v) w = map_pmf (\<lambda>(x, (y, z)). ((x, y), z)) (pair_pmf u (pair_pmf v w))"
+by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf)
+
+lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\<lambda>(x, y). (y, x)) (pair_pmf y x)"
+unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)
+
+lemma set_pmf_subset_singleton: "set_pmf p \<subseteq> {x} \<longleftrightarrow> p = return_pmf x"
+proof(intro iffI pmf_eqI)
+  fix i
+  assume x: "set_pmf p \<subseteq> {x}"
+  hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto
+  have "ereal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single)
+  also have "\<dots> = \<integral>\<^sup>+ i. 1 \<partial>p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
+  also have "\<dots> = 1" by simp
+  finally show "pmf p i = pmf (return_pmf x) i" using x
+    by(auto split: split_indicator simp add: pmf_eq_0_set_pmf)
+qed auto
+
+lemma bind_eq_return_pmf:
+  "bind_pmf p f = return_pmf x \<longleftrightarrow> (\<forall>y\<in>set_pmf p. f y = return_pmf x)"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof(intro iffI strip)
+  fix y
+  assume y: "y \<in> set_pmf p"
+  assume "?lhs"
+  hence "set_pmf (bind_pmf p f) = {x}" by simp
+  hence "(\<Union>y\<in>set_pmf p. set_pmf (f y)) = {x}" by simp
+  hence "set_pmf (f y) \<subseteq> {x}" using y by auto
+  thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton)
+next
+  assume *: ?rhs
+  show ?lhs
+  proof(rule pmf_eqI)
+    fix i
+    have "ereal (pmf (bind_pmf p f) i) = \<integral>\<^sup>+ y. ereal (pmf (f y) i) \<partial>p" by(simp add: ereal_pmf_bind)
+    also have "\<dots> = \<integral>\<^sup>+ y. ereal (pmf (return_pmf x) i) \<partial>p"
+      by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
+    also have "\<dots> = ereal (pmf (return_pmf x) i)" by simp
+    finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" by simp
+  qed
+qed
+
+lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True"
+proof -
+  have "pmf p False + pmf p True = measure p {False} + measure p {True}"
+    by(simp add: measure_pmf_single)
+  also have "\<dots> = measure p ({False} \<union> {True})"
+    by(subst measure_pmf.finite_measure_Union) simp_all
+  also have "{False} \<union> {True} = space p" by auto
+  finally show ?thesis by simp
+qed
+
+lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False"
+by(simp add: pmf_False_conv_True)
+
 subsection \<open> Conditional Probabilities \<close>
 
 lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
@@ -946,6 +1016,22 @@
   finally show "measure p {x. R x y} = measure q {y. R x y}" .
 qed
 
+lemma rel_pmf_measureD:
+  assumes "rel_pmf R p q"
+  shows "measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs")
+using assms
+proof cases
+  fix pq
+  assume R: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
+    and p[symmetric]: "map_pmf fst pq = p"
+    and q[symmetric]: "map_pmf snd pq = q"
+  have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p)
+  also have "\<dots> \<le> measure (measure_pmf pq) {y. \<exists>x\<in>A. R x (snd y)}"
+    by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R)
+  also have "\<dots> = ?rhs" by(simp add: q)
+  finally show ?thesis .
+qed
+
 lemma rel_pmf_iff_measure:
   assumes "symp R" "transp R"
   shows "rel_pmf R p q \<longleftrightarrow>
@@ -1092,6 +1178,9 @@
   qed
 qed (fact natLeq_card_order natLeq_cinfinite)+
 
+lemma map_pmf_idI: "(\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_pmf f p = p"
+by(simp cong: pmf.map_cong)
+
 lemma rel_pmf_conj[simp]:
   "rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
   "rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
@@ -1190,6 +1279,31 @@
   by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
      (auto simp add: pmf.map_comp o_def assms)
 
+lemma rel_pmf_bij_betw:
+  assumes f: "bij_betw f (set_pmf p) (set_pmf q)"
+  and eq: "\<And>x. x \<in> set_pmf p \<Longrightarrow> pmf p x = pmf q (f x)"
+  shows "rel_pmf (\<lambda>x y. f x = y) p q"
+proof(rule rel_pmf.intros)
+  let ?pq = "map_pmf (\<lambda>x. (x, f x)) p"
+  show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def)
+
+  have "map_pmf f p = q"
+  proof(rule pmf_eqI)
+    fix i
+    show "pmf (map_pmf f p) i = pmf q i"
+    proof(cases "i \<in> set_pmf q")
+      case True
+      with f obtain j where "i = f j" "j \<in> set_pmf p"
+        by(auto simp add: bij_betw_def image_iff)
+      thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq)
+    next
+      case False thus ?thesis
+        by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric])
+    qed
+  qed
+  then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def)
+qed auto
+
 context
 begin
 
@@ -1442,7 +1556,7 @@
 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"
+lemma emeasure_pmf_of_set_space[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':
@@ -1471,6 +1585,13 @@
 apply(rule setsum.cong; simp_all)
 done
 
+lemma emeasure_pmf_of_set:
+  "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
+apply(subst nn_integral_indicator[symmetric], simp)
+apply(subst nn_integral_pmf_of_set)
+apply(simp add: o_def max_def ereal_indicator[symmetric] S_not_empty S_finite real_of_nat_indicator[symmetric] of_nat_setsum[symmetric] setsum_indicator_eq_card del: of_nat_setsum)
+done
+
 end
 
 lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
@@ -1498,6 +1619,14 @@
 lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
 by(rule pmf_eqI) simp_all
 
+
+
+lemma measure_pmf_of_set:
+  assumes "S \<noteq> {}" "finite S"
+  shows "measure (measure_pmf (pmf_of_set S)) A = card (S \<inter> A) / card S"
+using emeasure_pmf_of_set[OF assms, of A]
+unfolding measure_pmf.emeasure_eq_measure by simp
+
 subsubsection \<open> Poisson Distribution \<close>
 
 context
@@ -1564,4 +1693,15 @@
 lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
   by (simp add: set_pmf_binomial_eq)
 
+context begin interpretation lifting_syntax .
+
+lemma bind_pmf_parametric [transfer_rule]:
+  "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"
+by(blast intro: rel_pmf_bindI dest: rel_funD)
+
+lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf"
+by(rule rel_funI) simp
+
 end
+
+end