inductive ord_option :: "('a ==> 'b ==> bool) ==> 'a option ==> 'b option ==> bool" for ord :: "'a ==> 'b ==> bool" where
None: "ord_option ord None x"
| Some: "ord x y ==> ord_option ord (Some x) (Some y)"
inductive_simps ord_option_simps [simp]: "ord_option ord None x" "ord_option ord x None" "ord_option ord (Some x) (Some y)" "ord_option ord (Some x) None"
lemma ord_option_trans: "[ ord_option ord x y; ord_option ord y z; ∧a b c. [ a ∈ set_option x; b ∈ set_option y; c ∈ set_option z; ord a b; ord b c]==> ord a c ] ==> ord_option ord x z" by(auto elim!: ord_option.cases)
lemma ord_option_chainD: "Complete_Partial_Order.chain (ord_option ord) Y ==> Complete_Partial_Order.chain ord {x. Some x ∈ Y}" by(rule chainI)(auto dest: chainD)
definition lub_option :: "('a set ==> 'b) ==> 'a option set ==> 'b option" where"lub_option lub Y = (if Y ⊆ {None} then None else Some (lub {x. Some x ∈ Y}))"
lemma map_lub_option: "map_option f (lub_option lub Y) = lub_option (f ∘ lub) Y" by(simp add: lub_option_def)
lemma lub_option_upper: assumes"Complete_Partial_Order.chain (ord_option ord) Y""x ∈ Y" and lub_upper: "∧Y x. [ Complete_Partial_Order.chain ord Y; x ∈ Y ]==> ord x (lub Y)" shows"ord_option ord x (lub_option lub Y)" using assms(1-2) by(cases x)(auto simp: lub_option_def intro: lub_upper[OF ord_option_chainD])
lemma lub_option_least: assumes Y: "Complete_Partial_Order.chain (ord_option ord) Y" and upper: "∧x. x ∈ Y ==> ord_option ord x y" assumes lub_least: "∧Y y. [ Complete_Partial_Order.chain ord Y; ∧x. x ∈ Y ==> ord x y ]==> ord (lub Y) y" shows"ord_option ord (lub_option lub Y) y" using Y by(cases y)(auto 4 3 simp add: lub_option_def intro: lub_least[OF ord_option_chainD] dest: upper)
lemma lub_map_option: "lub_option lub (map_option f ` Y) = lub_option (lub ∘ (`) f) Y" proof - have"∧u y. [Some u ∈ Y; y ∈ Y]==> {f y |y. Some y ∈ Y} = f ` {x. Some x ∈ Y}" by blast thenshow ?thesis by (auto simp: lub_option_def) qed
lemma ord_option_mono: "[ ord_option A x y; ∧x y. A x y ==> B x y ]==> ord_option B x y" by(auto elim: ord_option.cases)
lemma ord_option_mono' [mono]: "(∧x y. A x y ⟶ B x y) ==> ord_option A x y ⟶ ord_option B x y" by(blast intro: ord_option_mono)
lemma ord_option_compp: "ord_option (A OO B) = ord_option A OO ord_option B" by(auto simp: fun_eq_iff elim!: ord_option.cases intro: ord_option.intros)
lemma ord_option_inf: "inf (ord_option A) (ord_option B) = ord_option (inf A B)" (is"?lhs = ?rhs") proof(rule antisym) show"?lhs ≤ ?rhs"by(auto elim!: ord_option.cases) qed(auto elim: ord_option_mono)
lemma ord_option_map2: "ord_option ord x (map_option f y) = ord_option (λx y. ord x (f y)) x y" by(auto elim: ord_option.cases)
lemma ord_option_map1: "ord_option ord (map_option f x) y = ord_option (λx y. ord (f x) y) x y" by(auto elim: ord_option.cases)
lemma option_ord_Some1_iff: "option_ord (Some x) y ⟷ y = Some x" by(auto simp: flat_ord_def)
subsubsection ‹A relator for sets that treats sets like predicates›
contextincludes lifting_syntax begin
definition rel_pred :: "('a ==> 'b ==> bool) ==> 'a set ==> 'b set ==> bool" where"rel_pred R A B = (R ===> (=)) (λx. x ∈ A) (λy. y ∈ B)"
lemma rel_predI: "(R ===> (=)) (λx. x ∈ A) (λy. y ∈ B) ==> rel_pred R A B" by(simp add: rel_pred_def)
lemma rel_predD: "[ rel_pred R A B; R x y ]==> x ∈ A ⟷ y ∈ B" by(simp add: rel_pred_def rel_fun_def)
lemma Collect_parametric: "((A ===> (=)) ===> rel_pred A) Collect Collect" 🍋‹Declare this rule as @{attribute transfer_rule} only locally because it blows up the search space for @{method transfer} (in combination with @{thm [source] Collect_transfer})› by(simp add: rel_funI rel_predI)
end
subsubsection ‹Monotonicity rules›
lemma monotone_gfp_eadd1: "monotone (≥) (≥) (λx. x + y :: enat)" by(auto intro!: monotoneI)
lemma monotone_gfp_eadd2: "monotone (≥) (≥) (λy. x + y :: enat)" by(auto intro!: monotoneI)
lemma bi_unique_rel_set_bij_betw: assumes unique: "bi_unique R" and rel: "rel_set R A B" shows"∃f. bij_betw f A B ∧ (∀x∈A. R x (f x))" proof - from assms obtain f where f: "∧x. x ∈ A ==> R x (f x)"and B: "∧x. x ∈ A ==> f x ∈ B" by (metis bi_unique_rel_set_lemma image_eqI) have"inj_on f A" by (metis (no_types, lifting) bi_unique_def f inj_on_def unique) moreoverhave"f ` A = B"using rel by (smt (verit) bi_unique_def bi_unique_rel_set_lemma f image_cong unique) ultimatelyhave"bij_betw f A B"unfolding bij_betw_def .. thus ?thesis using f by blast qed
lemma bij_betw_rel_setD: "bij_betw f A B ==> rel_set (λx y. y = f x) A B" by(rule rel_setI)(auto dest: bij_betwE bij_betw_imp_surj_on[symmetric])
lemma measure_spmf_map_pmf_Some [simp]: "measure (measure_spmf (map_pmf Some p)) A = measure (measure_pmf p) A" using emeasure_spmf_map_pmf_Some[of p A] by(simp add: measure_spmf.emeasure_eq_measure measure_pmf.emeasure_eq_measure)
lemma nn_integral_measure_spmf: "(∫🪙+ x. f x ∂measure_spmf p) = ∫🪙+ x. ennreal (spmf p x) * f x ∂count_space UNIV"
(is"?lhs = ?rhs") proof - have"?lhs = ∫🪙+ x. pmf p x * f (the x) ∂count_space (range Some)" by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space nn_integral_measure_pmf nn_integral_count_space_indicator ac_simps
flip: times_ereal.simps [symmetric]) alsohave"… = ∫🪙+ x. ennreal (spmf p (the x)) * f (the x) ∂count_space (range Some)" by(rule nn_integral_cong) auto alsohave"… = ∫🪙+ x. spmf p (the (Some x)) * f (the (Some x)) ∂count_space UNIV" by(rule nn_integral_bij_count_space[symmetric])(simp add: bij_betw_def) alsohave"… = ?rhs"by simp finallyshow ?thesis . qed
lemma integral_measure_spmf: assumes"integrable (measure_spmf p) f" shows"(∫ x. f x ∂measure_spmf p) = ∫ x. spmf p x * f x ∂count_space UNIV" proof - have"integrable (count_space UNIV) (λx. spmf p x * f x)" using assms by(simp add: integrable_iff_bounded nn_integral_measure_spmf abs_mult ennreal_mult'') thenshow ?thesis using assms by(simp add: real_lebesgue_integral_def nn_integral_measure_spmf ennreal_mult'[symmetric]) qed
lemma measure_spmf_in_space_subprob_algebra [simp]: "measure_spmf p ∈ space (subprob_algebra (count_space UNIV))" by(simp add: space_subprob_algebra)
lemma nn_integral_spmf_neq_top: "(∫🪙+ x. spmf p x ∂count_space UNIV) ≠⊤" using nn_integral_measure_spmf[where f="λ_. 1", of p, symmetric] by simp
lemma SUP_spmf_neq_top': "(SUP p∈Y. ennreal (spmf p x)) ≠⊤" by (metis SUP_least ennreal_le_1 ennreal_one_neq_top neq_top_trans pmf_le_1)
lemma SUP_spmf_neq_top: "(SUP i. ennreal (spmf (Y i) x)) ≠⊤" by (meson SUP_eq_top_iff ennreal_le_1 ennreal_one_less_top linorder_not_le pmf_le_1)
lemma SUP_emeasure_spmf_neq_top: "(SUP p∈Y. emeasure (measure_spmf p) A) ≠⊤" by (metis ennreal_one_less_top less_SUP_iff linorder_not_le measure_spmf.subprob_emeasure_le_1)
subsection‹Support›
definition set_spmf :: "'a spmf ==> 'a set" where"set_spmf p = set_pmf p 🍋 set_option"
lemma set_spmf_rep_eq: "set_spmf p = {x. measure (measure_spmf p) {x} ≠ 0}" proof - have"∧x :: 'a. the -` {x} ∩ range Some = {Some x}"by auto thenshow ?thesis unfolding set_spmf_def measure_spmf_def by(auto simp: set_pmf.rep_eq measure_distr measure_restrict_space space_restrict_space) qed
lemma in_set_spmf: "x ∈ set_spmf p ⟷ Some x ∈ set_pmf p" by(simp add: set_spmf_def)
lemma AE_measure_spmf_iff [simp]: "(AE x in measure_spmf p. P x) ⟷ (∀x∈set_spmf p. P x)" unfolding set_spmf_def measure_spmf_def by(force simp: AE_distr_iff AE_restrict_space_iff AE_measure_pmf_iff cong del: AE_cong)
lemma spmf_eq_0_set_spmf: "spmf p x = 0 ⟷ x ∉ set_spmf p" by(auto simp: pmf_eq_0_set_pmf set_spmf_def)
lemma in_set_spmf_iff_spmf: "x ∈ set_spmf p ⟷ spmf p x ≠ 0" by(auto simp: set_spmf_def set_pmf_iff)
lemma spmf_eqI: assumes"∧i. spmf p i = spmf q i" shows"p = q" proof(rule pmf_eqI) fix i show"pmf p i = pmf q i" proof(cases i) case (Some i') thus ?thesis by(simp add: assms) next case None have"ennreal (pmf p i) = measure (measure_pmf p) {i}"by(simp add: pmf_def) alsohave"{i} = space (measure_pmf p) - range Some" by(auto simp: None intro: ccontr) alsohave"measure (measure_pmf p) … = ennreal 1 - measure (measure_pmf p) (range Some)" by(simp add: measure_pmf.prob_compl ennreal_minus[symmetric] del: space_measure_pmf) alsohave"range Some = (∪x∈set_spmf p. {Some x}) ∪ Some ` (- set_spmf p)" by auto alsohave"measure (measure_pmf p) … = measure (measure_pmf p) (∪x∈set_spmf p. {Some x})" by(rule measure_pmf.measure_zero_union)(auto simp: measure_pmf.prob_eq_0 AE_measure_pmf_iff in_set_spmf_iff_spmf set_pmf_iff) alsohave"ennreal … = ∫🪙+ x. measure (measure_pmf p) {Some x} ∂count_space (set_spmf p)" unfolding measure_pmf.emeasure_eq_measure[symmetric] by(simp_all add: emeasure_UN_countable disjoint_family_on_def) alsohave"… = ∫🪙+ x. spmf p x ∂count_space (set_spmf p)"by(simp add: pmf_def) alsohave"… = ∫🪙+ x. spmf q x ∂count_space (set_spmf p)"by(simp add: assms) alsohave"set_spmf p = set_spmf q"by(auto simp: in_set_spmf_iff_spmf assms) alsohave"(∫🪙+ x. spmf q x ∂count_space (set_spmf q)) = ∫🪙+ x. measure (measure_pmf q) {Some x} ∂count_space (set_spmf q)" by(simp add: pmf_def) alsohave"… = measure (measure_pmf q) (∪x∈set_spmf q. {Some x})" unfolding measure_pmf.emeasure_eq_measure[symmetric] by(simp_all add: emeasure_UN_countable disjoint_family_on_def) alsohave"… = measure (measure_pmf q) ((∪x∈set_spmf q. {Some x}) ∪ Some ` (- set_spmf q))" by(rule ennreal_cong measure_pmf.measure_zero_union[symmetric])+(auto simp: measure_pmf.prob_eq_0 AE_measure_pmf_iff in_set_spmf_iff_spmf set_pmf_iff) alsohave"((∪x∈set_spmf q. {Some x}) ∪ Some ` (- set_spmf q)) = range Some"by auto alsohave"ennreal 1 - measure (measure_pmf q) … = measure (measure_pmf q) (space (measure_pmf q) - range Some)" by(simp add: one_ereal_def measure_pmf.prob_compl ennreal_minus[symmetric] del: space_measure_pmf) alsohave"space (measure_pmf q) - range Some = {i}" by(auto simp: None intro: ccontr) alsohave"measure (measure_pmf q) … = pmf q i"by(simp add: pmf_def) finallyshow ?thesis by simp qed qed
lemma integral_measure_spmf_restrict: fixes f :: "'a ==> 'b :: {banach, second_countable_topology}" shows"(∫ x. f x ∂measure_spmf M) = (∫ x. f x ∂restrict_space (measure_spmf M) (set_spmf M))" by(auto intro!: integral_cong_AE simp add: integral_restrict_space)
lemma nn_integral_measure_spmf': "(∫🪙+ x. f x ∂measure_spmf p) = ∫🪙+ x. ennreal (spmf p x) * f x ∂count_space (set_spmf p)" by(auto simp: nn_integral_measure_spmf nn_integral_count_space_indicator in_set_spmf_iff_spmf intro!: nn_integral_cong split: split_indicator)
subsection‹Functorial structure›
abbreviation map_spmf :: "('a ==> 'b) ==> 'a spmf ==> 'b spmf" where"map_spmf f ≡ map_pmf (map_option f)"
lemma set_map_spmf [simp]: "set_spmf (map_spmf f p) = f ` set_spmf p" by(simp add: set_spmf_def image_bind bind_image o_def Option.option.set_map)
lemma map_spmf_cong: "[ p = q; ∧x. x ∈ set_spmf q ==> f x = g x ]==> map_spmf f p = map_spmf g q" by(auto intro: pmf.map_cong option.map_cong simp add: in_set_spmf)
lemma map_spmf_cong_simp: "[ p = q; ∧x. x ∈ set_spmf q =simp=> f x = g x ] ==> map_spmf f p = map_spmf g q" unfolding simp_implies_def by(rule map_spmf_cong)
lemma map_spmf_idI: "(∧x. x ∈ set_spmf p ==> f x = x) ==> map_spmf f p = p" by(rule map_pmf_idI map_option_idI)+(simp add: in_set_spmf)
lemma measure_map_spmf: "measure (measure_spmf (map_spmf f p)) A = measure (measure_spmf p) (f -` A)" using emeasure_map_spmf[of f p A] by(simp add: measure_spmf.emeasure_eq_measure)
lemma spmf_map_pmf_Some [simp]: "spmf (map_pmf Some p) i = pmf p i" by(simp add: pmf_map_inj')
lemma spmf_map_inj: "[ inj_on f (set_spmf M); x ∈ set_spmf M ]==> spmf (map_spmf f M) (f x) = spmf M x" by (smt (verit) elem_set in_set_spmf inj_on_def option.inj_map_strong option.map(2) pmf_map_inj)
lemma spmf_map_inj': "inj f ==> spmf (map_spmf f M) (f x) = spmf M x" by(subst option.map(2)[symmetric, where f=f])(rule pmf_map_inj'[OF option.inj_map])
lemma spmf_map_outside: "x ∉ f ` set_spmf M ==> spmf (map_spmf f M) x = 0" unfolding spmf_eq_0_set_spmf by simp
lemma ennreal_spmf_map: "ennreal (spmf (map_spmf f p) x) = emeasure (measure_spmf p) (f -` {x})" by (metis emeasure_map_spmf emeasure_spmf_single)
lemma spmf_map: "spmf (map_spmf f p) x = measure (measure_spmf p) (f -` {x})" using ennreal_spmf_map[of f p x] by(simp add: measure_spmf.emeasure_eq_measure)
lemma ennreal_spmf_map_conv_nn_integral: "ennreal (spmf (map_spmf f p) x) = integral🪙N (measure_spmf p) (indicator (f -` {x}))" by (simp add: ennreal_spmf_map)
subsection‹Monad operations›
subsubsection ‹Return›
abbreviation return_spmf :: "'a ==> 'a spmf" where"return_spmf x ≡ return_pmf (Some x)"
definition bind_spmf :: "'a spmf ==> ('a ==> 'b spmf) ==> 'b spmf" where"bind_spmf x f = bind_pmf x (λa. case a of None ==> return_pmf None | Some a' ==> f a')"
lemma return_bind_spmf [simp]: "return_spmf x 🍋 f = f x" by(simp add: bind_spmf_def bind_return_pmf)
lemma bind_return_spmf [simp]: "x 🍋 return_spmf = x" proof - have"∧a :: 'a option. (case a of None ==> return_pmf None | Some a' ==> return_spmf a') = return_pmf a" by(simp split: option.split) thenshow ?thesis by(simp add: bind_spmf_def bind_return_pmf') qed
lemma bind_spmf_assoc [simp]: fixes x :: "'a spmf"and f :: "'a ==> 'b spmf"and g :: "'b ==> 'c spmf" shows"(x 🍋 f) 🍋 g = x 🍋 (λy. f y 🍋 g)" unfolding bind_spmf_def by (smt (verit, best) bind_assoc_pmf bind_pmf_cong bind_return_pmf option.case_eq_if)
lemma pmf_bind_spmf_None: "pmf (p 🍋 f) None = pmf p None + ∫ x. pmf (f x) None ∂measure_spmf p"
(is"?lhs = ?rhs") proof - let ?f = "λx. pmf (case x of None ==> return_pmf None | Some x ==> f x) None" have"?lhs = ∫ x. ?f x ∂measure_pmf p" by(simp add: bind_spmf_def pmf_bind) alsohave"… = ∫ x. ?f None * indicator {None} x + ?f x * indicator (range Some) x ∂measure_pmf p" by(rule Bochner_Integration.integral_cong)(auto simp: indicator_def) alsohave"… = (∫ x. ?f None * indicator {None} x ∂measure_pmf p) + (∫ x. ?f x * indicator (range Some) x ∂measure_pmf p)" by(rule Bochner_Integration.integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1) alsohave"… = pmf p None + ∫ x. indicator (range Some) x * pmf (f (the x)) None ∂measure_pmf p" by(auto simp: measure_measure_pmf_finite indicator_eq_0_iff intro!: Bochner_Integration.integral_cong) alsohave"… = ?rhs" unfolding measure_spmf_def by(subst integral_distr)(auto simp: integral_restrict_space) finallyshow ?thesis . qed
lemma spmf_bind: "spmf (p 🍋 f) y = ∫ x. spmf (f x) y ∂measure_spmf p" proof - have"∧x. spmf (case x of None ==> return_pmf None | Some x ==> f x) y = indicat_real (range Some) x * spmf (f (the x)) y" by (simp add: split: option.split) thenshow ?thesis by (simp add: measure_spmf_def integral_distr bind_spmf_def pmf_bind integral_restrict_space) qed
lemma ennreal_spmf_bind: "ennreal (spmf (p 🍋 f) x) = ∫🪙+ y. spmf (f y) x ∂measure_spmf p" proof - have"∧y. ennreal (spmf (case y of None ==> return_pmf None | Some x ==> f x) x) = ennreal (spmf (f (the y)) x) * indicator (range Some) y" by (simp add: split: option.split) thenshow ?thesis by (simp add: bind_spmf_def ennreal_pmf_bind nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space) qed
lemma measure_spmf_bind_pmf: "measure_spmf (p 🍋 f) = measure_pmf p 🍋 measure_spmf ∘ f"
(is"?lhs = ?rhs") proof(rule measure_eqI) show"sets ?lhs = sets ?rhs" by (simp add: Giry_Monad.bind_def) next fix A :: "'a set" have"emeasure ?lhs A = ∫🪙+ x. emeasure (measure_spmf (f x)) A ∂measure_pmf p" by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def) alsohave"… = emeasure ?rhs A" by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra) finallyshow"emeasure ?lhs A = emeasure ?rhs A" . qed
lemma measure_spmf_bind: "measure_spmf (p 🍋 f) = measure_spmf p 🍋 measure_spmf ∘ f"
(is"?lhs = ?rhs") proof(rule measure_eqI) show"sets ?lhs = sets ?rhs" by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf) next fix A :: "'a set" let ?A = "the -` A ∩ range Some" have"emeasure ?lhs A = ∫🪙+ x. emeasure (measure_pmf (case x of None ==> return_pmf None | Some x ==> f x)) ?A ∂measure_pmf p" by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def) alsohave"… = ∫🪙+ x. emeasure (measure_pmf (f (the x))) ?A * indicator (range Some) x ∂measure_pmf p" by(rule nn_integral_cong)(auto split: option.split simp add: indicator_def) alsohave"… = ∫🪙+ x. emeasure (measure_spmf (f x)) A ∂measure_spmf p" by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space emeasure_distr space_restrict_space emeasure_restrict_space) alsohave"… = emeasure ?rhs A" by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra) finallyshow"emeasure ?lhs A = emeasure ?rhs A" . qed
lemma map_spmf_bind_spmf: "map_spmf f (bind_spmf p g) = bind_spmf p (map_spmf f ∘g)" by(auto simp: bind_spmf_def map_bind_pmf fun_eq_iff split: option.split intro: arg_cong2[where f=bind_pmf])
lemma bind_map_spmf: "map_spmf f p 🍋 g = p 🍋 g ∘ f" by(simp add: bind_spmf_def bind_map_pmf o_def cong del: option.case_cong_weak)
lemma spmf_bind_leI: assumes"∧y. y ∈ set_spmf p ==> spmf (f y) x ≤ r" and"0 ≤ r" shows"spmf (bind_spmf p f) x ≤ r" proof - have"ennreal (spmf (bind_spmf p f) x) = ∫🪙+ y. spmf (f y) x ∂measure_spmf p" by(rule ennreal_spmf_bind) alsohave"…≤∫🪙+ y. r ∂measure_spmf p" by(rule nn_integral_mono_AE)(simp add: assms) alsohave"…≤ r" using assms measure_spmf.emeasure_space_le_1 by(auto simp: measure_spmf.emeasure_eq_measure intro!: mult_left_le) finallyshow ?thesis using assms(2) by(simp) qed
lemma map_spmf_conv_bind_spmf: "map_spmf f p = (p 🍋 (λx. return_spmf (f x)))" by(simp add: map_pmf_def bind_spmf_def)(rule bind_pmf_cong, simp_all split: option.split)
lemma bind_spmf_cong: "[ p = q; ∧x. x ∈ set_spmf q ==> f x = g x ]==> bind_spmf p f = bind_spmf q g" by(auto simp: bind_spmf_def in_set_spmf intro: bind_pmf_cong option.case_cong)
lemma bind_spmf_cong_simp: "[ p = q; ∧x. x ∈ set_spmf q =simp=> f x = g x ] ==> bind_spmf p f = bind_spmf q g" by(simp add: simp_implies_def cong: bind_spmf_cong)
lemma bind_commute_spmf: "bind_spmf p (λx. bind_spmf q (f x)) = bind_spmf q (λy. bind_spmf p (λx. f x y))"
(is"?lhs = ?rhs") proof - let ?f = "λx y. case x of None ==> return_pmf None | Some a ==> (case y of None ==>return_pmf None | Some b ==> f a b)" have"?lhs = p 🍋 (λx. q 🍋 ?f x)" unfolding bind_spmf_def by(rule bind_pmf_cong[OF refl])(simp split: option.split) alsohave"… = q 🍋 (λy. p 🍋 (λx. ?f x y))"by(rule bind_commute_pmf) alsohave"… = ?rhs"unfolding bind_spmf_def by(rule bind_pmf_cong[OF refl])(auto split: option.split, metis bind_spmf_const_return_None bind_spmf_def) finallyshow ?thesis . qed
lemma rel_spmf_mono: "[rel_spmf A f g; ∧x y. A x y ==> B x y ]==> rel_spmf B f g" by (metis option.rel_sel pmf.rel_mono_strong)
lemma rel_spmf_mono_strong: "[ rel_spmf A f g; ∧x y. [ A x y; x ∈ set_spmf f; y ∈ set_spmf g ]==> B x y ]==> rel_spmf B f g" by (metis elem_set in_set_spmf option.rel_mono_strong pmf.rel_mono_strong)
lemma rel_spmf_reflI: "(∧x. x ∈ set_spmf p ==> P x x) ==> rel_spmf P p p" by (metis (mono_tags, lifting) option.rel_eq pmf.rel_eq rel_spmf_mono_strong)
lemma rel_spmfI [intro?]: "[∧x y. (x, y) ∈ set_spmf pq ==> P x y; map_spmf fst pq = p; map_spmf snd pq = q ] ==> rel_spmf P p q" by(rule rel_pmf.intros[where pq="map_pmf (λx. case x of None ==> (None, None) | Some (a, b) ==> (Some a, Some b)) pq"])
(auto simp: pmf.map_comp o_def in_set_spmf split: option.splits intro: pmf.map_cong)
lemma rel_spmfE [elim?, consumes 1, case_names rel_spmf]: assumes"rel_spmf P p q" obtains pq where "∧x y. (x, y) ∈ set_spmf pq ==> P x y" "p = map_spmf fst pq" "q = map_spmf snd pq" using assms proof(cases rule: rel_pmf.cases[consumes 1, case_names rel_pmf]) case (rel_pmf pq) let ?pq = "map_pmf (λ(a, b). case (a, b) of (Some x, Some y) ==> Some (x, y) | _ ==> None) pq" have"∧x y. (x, y) ∈ set_spmf ?pq ==> P x y" by(auto simp: in_set_spmf split: option.split_asm dest: rel_pmf(1)) moreover have"∧x. (x, None) ∈ set_pmf pq ==> x = None"by(auto dest!: rel_pmf(1)) thenhave"p = map_spmf fst ?pq"using rel_pmf(2) by(auto simp: pmf.map_comp split_beta intro!: pmf.map_cong split: option.split) moreover have"∧y. (None, y) ∈ set_pmf pq ==> y = None"by(auto dest!: rel_pmf(1)) thenhave"q = map_spmf snd ?pq"using rel_pmf(3) by(auto simp: pmf.map_comp split_beta intro!: pmf.map_cong split: option.split) ultimatelyshow thesis .. qed
lemma rel_spmf_simps: "rel_spmf R p q ⟷ (∃pq. (∀(x, y)∈set_spmf pq. R x y) ∧ map_spmf fst pq = p ∧ map_spmf snd pq = q)" by(auto intro: rel_spmfI elim!: rel_spmfE)
lemma spmf_rel_map: shows spmf_rel_map1: "∧R f x. rel_spmf R (map_spmf f x) = rel_spmf (λx. R (f x)) x" and spmf_rel_map2: "∧R x g y. rel_spmf R x (map_spmf g y) = rel_spmf (λx y. R x (g y)) x y" by(simp_all add: fun_eq_iff pmf.rel_map option.rel_map[abs_def])
lemma bind_spmf_parametric [transfer_rule]: "(rel_spmf A ===> (A ===> rel_spmf B) ===> rel_spmf B) bind_spmf bind_spmf" unfolding bind_spmf_def[abs_def] by transfer_prover
lemma return_spmf_parametric: "(A ===> rel_spmf A) return_spmf return_spmf" by transfer_prover
lemma map_spmf_parametric: "((A ===> B) ===> rel_spmf A ===> rel_spmf B) map_spmf map_spmf" by transfer_prover
lemma rel_spmf_parametric: "((A ===> B ===> (=)) ===> rel_spmf A ===> rel_spmf B ===> (=)) rel_spmf rel_spmf" by transfer_prover
lemma set_spmf_parametric [transfer_rule]: "(rel_spmf A ===> rel_set A) set_spmf set_spmf" unfolding set_spmf_def[abs_def] by transfer_prover
lemma return_spmf_None_parametric: "(rel_spmf A) (return_pmf None) (return_pmf None)" by simp
end
lemma rel_spmf_bindI: "[ rel_spmf R p q; ∧x y. R x y ==> rel_spmf P (f x) (g y) ] ==> rel_spmf P (p 🍋 f) (q 🍋 g)" by(fact bind_spmf_parametric[THEN rel_funD, THEN rel_funD, OF _ rel_funI])
lemma rel_spmf_bind_reflI: "(∧x. x ∈ set_spmf p ==> rel_spmf P (f x) (g x)) ==> rel_spmf P (p 🍋 f) (p 🍋 g)" by(rule rel_spmf_bindI[where R="λx y. x = y ∧ x ∈ set_spmf p"])(auto intro: rel_spmf_reflI)
lemma rel_pmf_return_pmfI: "P x y ==> rel_pmf P (return_pmf x) (return_pmf y)" by simp
contextincludes lifting_syntax begin
text‹We do not yet have a relator for 🍋‹'a measure›, so we combine 🍋‹measure›and 🍋‹measure_pmf›\› lemma measure_pmf_parametric: "(rel_pmf A ===> rel_pred A ===> (=)) (λp. measure (measure_pmf p)) (λq. measure (measure_pmf q))" proof(rule rel_funI)+ fix p q X Y assume"rel_pmf A p q"and"rel_pred A X Y" from this(1) obtain pq where A: "∧x y. (x, y) ∈ set_pmf pq ==> A x y" and p: "p = map_pmf fst pq"and q: "q = map_pmf snd pq"by cases auto show"measure p X = measure q Y"unfolding p q measure_map_pmf by(rule measure_pmf.finite_measure_eq_AE)(auto simp: AE_measure_pmf_iff dest!: A rel_predD[OF ‹rel_pred _ _ _›]) qed
lemma measure_spmf_parametric: "(rel_spmf A ===> rel_pred A ===> (=)) (λp. measure (measure_spmf p)) (λq. measure (measure_spmf q))" proof - have"∧x y xa ya. rel_pred A xa ya ==> rel_pred (rel_option A) (Some ` xa) (Some ` ya)" by(auto simp: rel_pred_def rel_fun_def elim: option.rel_cases) thenshow ?thesis unfolding measure_measure_spmf_conv_measure_pmf[abs_def] by (intro rel_funI) (force elim!: measure_pmf_parametric[THEN rel_funD, THEN rel_funD]) qed
lemma rel_spmf_weightD: "rel_spmf A p q ==> weight_spmf p = weight_spmf q" by(erule rel_spmfE) simp
lemma rel_spmf_bij_betw: assumes f: "bij_betw f (set_spmf p) (set_spmf q)" and eq: "∧x. x ∈ set_spmf p ==> spmf p x = spmf q (f x)" shows"rel_spmf (λx y. f x = y) p q" proof - let ?f = "map_option f"
have weq: "ennreal (weight_spmf p) = ennreal (weight_spmf q)" unfolding weight_spmf_eq_nn_integral_support by(subst nn_integral_bij_count_space[OF f, symmetric])(rule nn_integral_cong_AE, simp add: eq AE_count_space) thenhave"None ∈ set_pmf p ⟷ None ∈ set_pmf q" by(simp add: pmf_None_eq_weight_spmf set_pmf_iff) with f have"bij_betw (map_option f) (set_pmf p) (set_pmf q)" apply(auto simp: bij_betw_def in_set_spmf inj_on_def intro: option.expand split: option.split) apply(rename_tac [!] x) apply(case_tac [!] x) apply(auto iff: in_set_spmf) done thenhave"rel_pmf (λx y. ?f x = y) p q" proof (rule rel_pmf_bij_betw) show"pmf p x = pmf q (map_option f x)"if"x ∈ set_pmf p"for x proof (cases x) case None thenshow ?thesis by (metis ennreal_inj measure_nonneg option.map_disc_iff pmf_None_eq_weight_spmf weq) qed (use eq in_set_spmf that in force) qed thus ?thesis by (smt (verit, ccfv_SIG) None_eq_map_option_iff option.map_sel option.rel_sel pmf.rel_mono_strong) qed
subsection‹From density to spmfs›
contextfixes f :: "'a ==> real"begin
definition embed_spmf :: "'a spmf" where"embed_spmf = embed_pmf (λx. case x of None ==> 1 - enn2real (∫🪙+ x. ennreal (f x) ∂count_space UNIV) | Some x' ==> max 0 (f x'))"
text‹ 🍋‹rel_pmf›does not preserve a ccpo structure. Counterexample by Saheb-Djahromi: Take prefix order over ‹bool llist›and the set ‹range (λn :: nat. uniform (llist_n n))›where ‹llist_n› is the set of all ‹llist›s of length ‹n› and ‹uniform› returns a uniform distribution over the given set. The set forms a chain in ‹ord_pmf lprefix›, but it has not an upper bound. Any upper bound may contain only infinite lists in its support because otherwise it is not greater than the ‹n+1›-st element in the chain where ‹n› is the length of the finite list. Moreover its support must contain all infinite lists, because otherwise there is a finite list all of whose finite extensions are not in the support - a contradiction to the upper bound property. Hence, the support is uncountable, but pmf's only have countable support. However, if all chains in the ccpo are finite, then it should preserve the ccpo structure. ›
abbreviation ord_spmf :: "('a ==> 'a ==> bool) ==> 'a spmf ==> 'a spmf ==> bool" where"ord_spmf ord ≡ rel_pmf (ord_option ord)"
locale ord_spmf_syntax begin notation ord_spmf (infix‹⊑🍋› 60) end
lemma ord_spmf_map_spmf1: "ord_spmf R (map_spmf f p) = ord_spmf (λx. R (f x)) p" by(simp add: pmf.rel_map[abs_def] ord_option_map1[abs_def])
lemma ord_spmf_map_spmf2: "ord_spmf R p (map_spmf f q) = ord_spmf (λx y. R x (f y)) p q" by(simp add: pmf.rel_map ord_option_map2)
lemma ord_spmf_map_spmf12: "ord_spmf R (map_spmf f p) (map_spmf f q) = ord_spmf (λx y. R (f x) (f y)) p q" by(simp add: pmf.rel_map ord_option_map1[abs_def] ord_option_map2)
lemma ord_spmf_reflI: "(∧x. x ∈ set_spmf p ==> ord x x) ==> p ⊑ p" by (metis elem_set in_set_spmf ord_option_reflI pmf.rel_refl_strong)
lemma rel_spmf_inf: assumes"p ⊑ q" and"q ⊑ p" and refl: "reflp ord" and trans: "transp ord" shows"rel_spmf (inf ord ord-1-1) p q" proof - from‹p ⊑ q›‹q ⊑ p› have"rel_pmf (inf (ord_option ord) (ord_option ord)-1-1) p q" usinglocal.refl local.trans reflp_ord_option rel_pmf_inf transp_ord_option by blast alsohave"inf (ord_option ord) (ord_option ord)-1-1 = rel_option (inf ord ord-1-1)" by(auto simp: fun_eq_iff elim: ord_option.cases option.rel_cases) finallyshow ?thesis . qed
end
lemma ord_spmf_return_spmf2: "ord_spmf R p (return_spmf y) ⟷ (∀x∈set_spmf p. R x y)" by(auto simp: rel_pmf_return_pmf2 in_set_spmf ord_option.simps intro: ccontr)
lemma ord_spmf_mono: "[ ord_spmf A p q; ∧x y. A x y ==> B x y ]==> ord_spmf B p q" by(erule pmf.rel_mono_strong)(erule ord_option_mono)
lemma ord_spmf_compp: "ord_spmf (A OO B) = ord_spmf A OO ord_spmf B" by(simp add: ord_option_compp pmf.rel_compp)
lemma ord_spmf_bindI: assumes pq: "ord_spmf R p q" and fg: "∧x y. R x y ==> ord_spmf P (f x) (g y)" shows"ord_spmf P (p 🍋 f) (q 🍋 g)" unfolding bind_spmf_def using pq by(rule rel_pmf_bindI)(auto split: option.split intro: fg)
lemma ord_spmf_bind_reflI: "(∧x. x ∈ set_spmf p ==> ord_spmf R (f x) (g x)) ==> ord_spmf R (p 🍋 f) (p 🍋 g)" by(rule ord_spmf_bindI[where R="λx y. x = y ∧ x ∈ set_spmf p"])(auto intro: ord_spmf_reflI)
lemma ord_pmf_increaseI: assumes le: "∧x. spmf p x ≤ spmf q x" and refl: "∧x. x ∈ set_spmf p ==> R x x" shows"ord_spmf R p q" proof(rule rel_pmf.intros)
define pq where"pq = embed_pmf (λ(x, y). case x of Some x' ==> (case y of Some y' ==> if x' = y' then spmf p x' else 0 | None ==> 0) | None ==> (case y of None ==> pmf q None | Some y' ==> spmf q y' - spmf p y'))"
(is"_ = embed_pmf ?f") have nonneg: "∧xy. ?f xy ≥ 0" by(clarsimp simp add: le field_simps split: option.split) have integral: "(∫🪙+ xy. ?f xy ∂count_space UNIV) = 1" (is"nn_integral ?M _ = _") proof - have"(∫🪙+ xy. ?f xy ∂count_space UNIV) = ∫🪙+ xy. ennreal (?f xy) * indicator {(None, None)} xy + ennreal (?f xy) * indicator (range (λx. (None, Some x))) xy + ennreal (?f xy) * indicator (range (λx. (Some x, Some x))) xy ∂?M" by(rule nn_integral_cong)(auto split: split_indicator option.splits if_split_asm) alsohave"… = (∫🪙+ xy. ?f xy * indicator {(None, None)} xy ∂?M) + (∫🪙+ xy. ennreal (?f xy) * indicator (range (λx. (None, Some x))) xy ∂?M) + (∫🪙+ xy. ennreal (?f xy) * indicator (range (λx. (Some x, Some x))) xy ∂?M)"
(is"_ = ?None + ?Some2 + ?Some") by(subst nn_integral_add)(simp_all add: nn_integral_add AE_count_space le_diff_eq le split: option.split) alsohave"?None = pmf q None"by simp alsohave"?Some2 = ∫🪙+ x. ennreal (spmf q x) - spmf p x ∂count_space UNIV" by(simp add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] inj_on_def nn_integral_embed_measure measurable_embed_measure1 ennreal_minus) alsohave"… = (∫🪙+ x. spmf q x ∂count_space UNIV) - (∫🪙+ x. spmf p x ∂count_space UNIV)"
(is"_ = ?Some2' - ?Some2''") by(subst nn_integral_diff)(simp_all add: le nn_integral_spmf_neq_top) alsohave"?Some = ∫🪙+ x. spmf p x ∂count_space UNIV" by(simp add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] inj_on_def nn_integral_embed_measure measurable_embed_measure1) alsohave"pmf q None + (?Some2' - ?Some2'') + … = pmf q None + ?Some2'" by(auto simp: diff_add_self_ennreal le intro!: nn_integral_mono) alsohave"… = ∫🪙+ x. ennreal (pmf q x) * indicator {None} x + ennreal (pmf q x) * indicator (range Some) x ∂count_space UNIV" by(subst nn_integral_add)(simp_all add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] nn_integral_embed_measure measurable_embed_measure1) alsohave"… = ∫🪙+ x. pmf q x ∂count_space UNIV" by(rule nn_integral_cong)(auto split: split_indicator) alsohave"… = 1" by(simp add: nn_integral_pmf) finallyshow ?thesis . qed note f = nonneg integral
{ fix x y assume"(x, y) ∈ set_pmf pq" hence"?f (x, y) ≠ 0"unfolding pq_def by(simp add: set_embed_pmf[OF f]) thenshow"ord_option R x y" by(simp add: spmf_eq_0_set_spmf refl split: option.split_asm if_split_asm) }
have weight_le: "weight_spmf p ≤ weight_spmf q" by(subst ennreal_le_iff[symmetric])(auto simp: weight_spmf_eq_nn_integral_spmf intro!: nn_integral_mono le)
show"map_pmf fst pq = p" proof(rule pmf_eqI) fix i :: "'a option" have bi: "bij_betw (Pair i) UNIV (fst -` {i})" by(auto simp: bij_betw_def inj_on_def) have"ennreal (pmf (map_pmf fst pq) i) = (∫🪙+ y. pmf pq (i, y) ∂count_space UNIV)" unfolding pq_def ennreal_pmf_map apply (simp add: embed_pmf.rep_eq[OF f] o_def emeasure_density flip: nn_integral_count_space_indicator) by (smt (verit, best) nn_integral_bij_count_space [OF bi] integral nn_integral_cong nonneg pmf_embed_pmf) alsohave"… = pmf p i" proof(cases i) case (Some x) have"(∫🪙+ y. pmf pq (Some x, y) ∂count_space UNIV) = ∫🪙+ y. pmf p (Some x) * indicator {Some x} y ∂count_space UNIV" by(rule nn_integral_cong)(simp add: pq_def pmf_embed_pmf[OF f] split: option.split) thenshow ?thesis using Some by simp next case None have"(∫🪙+ y. pmf pq (None, y) ∂count_space UNIV) = (∫🪙+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y + ennreal (pmf pq (None, None)) * indicator {None} y ∂count_space UNIV)" by(rule nn_integral_cong)(auto split: split_indicator) alsohave"… = (∫🪙+ y. ennreal (pmf pq (None, Some (the y))) ∂count_space (range Some)) + pmf pq (None, None)" by(subst nn_integral_add)(simp_all add: nn_integral_count_space_indicator) alsohave"… = (∫🪙+ y. ennreal (spmf q y) - ennreal (spmf p y) ∂count_space UNIV) + pmf q None" by(simp add: pq_def pmf_embed_pmf[OF f] embed_measure_count_space[symmetric] nn_integral_embed_measure measurable_embed_measure1 ennreal_minus) alsohave"(∫🪙+ y. ennreal (spmf q y) - ennreal (spmf p y) ∂count_space UNIV) = (∫🪙+ y. spmf q y ∂count_space UNIV) - (∫🪙+ y. spmf p y ∂count_space UNIV)" by(subst nn_integral_diff)(simp_all add: AE_count_space le nn_integral_spmf_neq_top split: split_indicator) alsohave"… = pmf p None - pmf q None" by(simp add: pmf_None_eq_weight_spmf weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus) alsohave"… = ennreal (pmf p None) - ennreal (pmf q None)"by(simp add: ennreal_minus) finallyshow ?thesis using None weight_le by(auto simp: diff_add_self_ennreal pmf_None_eq_weight_spmf intro: ennreal_leI) qed finallyshow"pmf (map_pmf fst pq) i = pmf p i"by simp qed
show"map_pmf snd pq = q" proof(rule pmf_eqI) fix i :: "'a option" have bi: "bij_betw (λx. (x, i)) UNIV (snd -` {i})" by (auto simp: bij_betw_def inj_on_def) have"ennreal (pmf (map_pmf snd pq) i) = (∫🪙+ x. pmf pq (x, i) ∂count_space UNIV)" unfolding pq_def ennreal_pmf_map apply(simp add: embed_pmf.rep_eq[OF f] o_def emeasure_density nn_integral_count_space_indicator[symmetric]) by (smt (verit, best) nn_integral_bij_count_space [OF bi] integral nn_integral_cong nonneg pmf_embed_pmf) alsohave"… = ennreal (pmf q i)" proof(cases i) case None have"(∫🪙+ x. pmf pq (x, None) ∂count_space UNIV) = ∫🪙+ x. pmf q None * indicator {None :: 'a option} x ∂count_space UNIV" by(rule nn_integral_cong)(simp add: pq_def pmf_embed_pmf[OF f] split: option.split) thenshow ?thesis using None by simp next case (Some y) have"(∫🪙+ x. pmf pq (x, Some y) ∂count_space UNIV) = (∫🪙+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x + ennreal (pmf pq (None, Some y)) * indicator {None} x ∂count_space UNIV)" by(rule nn_integral_cong)(auto split: split_indicator) alsohave"… = (∫🪙+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x ∂count_space UNIV) + pmf pq (None, Some y)" by(subst nn_integral_add)(simp_all) alsohave"… = (∫🪙+ x. ennreal (spmf p y) * indicator {Some y} x ∂count_space UNIV) + (spmf q y - spmf p y)" by(auto simp: pq_def pmf_embed_pmf[OF f] one_ereal_def[symmetric] simp del: nn_integral_indicator_singleton intro!: arg_cong2[where f="(+)"] nn_integral_cong split: option.split) alsohave"… = spmf q y"by(simp add: ennreal_minus[symmetric] le) finallyshow ?thesis using Some by simp qed finallyshow"pmf (map_pmf snd pq) i = pmf q i"by simp qed qed
lemma ord_spmf_eq_leD: assumes"ord_spmf (=) p q" shows"spmf p x ≤ spmf q x" proof(cases "x ∈ set_spmf p") case False thus ?thesis by(simp add: in_set_spmf_iff_spmf) next case True from assms obtain pq where pq: "∧x y. (x, y) ∈ set_pmf pq ==> ord_option (=) x y" and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq"by cases auto have"ennreal (spmf p x) = integral🪙N pq (indicator (fst -` {Some x}))" using p by(simp add: ennreal_pmf_map) alsohave"… = integral🪙N pq (indicator {(Some x, Some x)})" by(rule nn_integral_cong_AE)(auto simp: AE_measure_pmf_iff split: split_indicator dest: pq) alsohave"…≤ integral🪙N pq (indicator (snd -` {Some x}))" by(rule nn_integral_mono) simp alsohave"… = ennreal (spmf q x)"using q by(simp add: ennreal_pmf_map) finallyshow ?thesis by simp qed
lemma ord_spmf_eqD_set_spmf: "ord_spmf (=) p q ==> set_spmf p ⊆ set_spmf q" by (metis ord_spmf_eq_leD pmf_le_0_iff spmf_eq_0_set_spmf subsetI)
lemma ord_spmf_eqD_measure_spmf: "ord_spmf (=) p q ==> measure_spmf p ≤ measure_spmf q" by (subst le_measure) (auto simp: ord_spmf_eqD_emeasure)
subsection‹CCPO structure for the flat ccpo 🍋‹ord_option (=)›\›
contextfixes Y :: "'a spmf set"begin
definition lub_spmf :: "'a spmf" where"lub_spmf = embed_spmf (λx. enn2real (SUP p ∈ Y. ennreal (spmf p x)))" 🍋‹We go through 🍋‹ennreal›to have a sensible definition even if 🍋‹Y› is empty.›
contextassumes chain: "Complete_Partial_Order.chain (ord_spmf (=)) Y" begin
lemma chain_ord_spmf_eqD: "Complete_Partial_Order.chain (≤) ((λp x. ennreal (spmf p x)) ` Y)"
(is"Complete_Partial_Order.chain _ (?f ` _)") proof(rule chainI) fix f g assume"f ∈ ?f ` Y""g ∈ ?f ` Y" thenobtain p q where f: "f = ?f p""p ∈ Y"and g: "g = ?f q""q ∈ Y"by blast from chain ‹p ∈ Y›‹q ∈ Y›have"ord_spmf (=) p q ∨ ord_spmf (=) q p"by(rule chainD) thus"f ≤ g ∨ g ≤ f" by (metis ennreal_leI f(1) g(1) le_funI ord_spmf_eq_leD) qed
lemma ord_spmf_eq_pmf_None_eq: assumes le: "ord_spmf (=) p q" and None: "pmf p None = pmf q None" shows"p = q" proof(rule spmf_eqI) fix i from le have le': "∧x. spmf p x ≤ spmf q x"by(rule ord_spmf_eq_leD) have"(∫🪙+ x. ennreal (spmf q x) - spmf p x ∂count_space UNIV) = (∫🪙+ x. spmf q x ∂count_space UNIV) - (∫🪙+ x. spmf p x ∂count_space UNIV)" by(subst nn_integral_diff)(simp_all add: AE_count_space le' nn_integral_spmf_neq_top) alsohave"… = (1 - pmf q None) - (1 - pmf p None)"unfolding pmf_None_eq_weight_spmf by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus) alsohave"… = 0"using None by simp finallyhave"∧x. spmf q x ≤ spmf p x" by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff) with le' show"spmf p i = spmf q i"by(rule antisym) qed
lemma ord_spmf_eqD_pmf_None: assumes"ord_spmf (=) x y" shows"pmf x None ≥ pmf y None" using assms apply cases apply(clarsimp simp only: ennreal_le_iff[symmetric, OF pmf_nonneg] ennreal_pmf_map) apply(fastforce simp: AE_measure_pmf_iff intro!: nn_integral_mono_AE) done
text‹ Chains on 🍋‹'a spmf›maintain countable support. Thanks to Johannes Hölzl for the proof idea. › lemma spmf_chain_countable: "countable (∪p∈Y. set_spmf p)" proof(cases "Y = {}") case Y: False show ?thesis proof(cases "∃x∈Y. ∀y∈Y. ord_spmf (=) y x") case True thenobtain x where x: "x ∈ Y"and upper: "∧y. y ∈ Y ==> ord_spmf (=) y x"by blast hence"(∪x∈Y. set_spmf x) ⊆ set_spmf x"by(auto dest: ord_spmf_eqD_set_spmf) thus ?thesis by(rule countable_subset) simp next case False
define N :: "'a option pmf ==> real"where"N p = pmf p None"for p
have N_less_imp_le_spmf: "[ x ∈ Y; y ∈ Y; N y < N x ]==> ord_spmf (=) x y"for x y using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x] by (auto simp: N_def) have N_eq_imp_eq: "[ x ∈ Y; y ∈ Y; N y = N x ]==> x = y"for x y using chainD[OF chain, of x y] by(auto simp: N_def dest: ord_spmf_eq_pmf_None_eq)
have NC: "N ` Y ≠ {}""bdd_below (N ` Y)" using‹Y ≠ {}›by(auto intro!: bdd_belowI[of _ 0] simp: N_def) have NC_less: "Inf (N ` Y) < N x"if"x ∈ Y"for x unfolding cInf_less_iff[OF NC] proof(rule ccontr) assume **: "¬ (∃y∈N ` Y. y < N x)"
{ fix y assume"y ∈ Y" with ** consider "N x < N y" | "N x = N y"by(auto simp: not_less le_less) hence"ord_spmf (=) y x"using‹y ∈ Y›‹x ∈ Y› by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) } with False ‹x ∈ Y›show False by blast qed
from NC have"Inf (N ` Y) ∈ closure (N ` Y)"by (intro closure_contains_Inf) thenobtain X' where"∧n. X' n ∈ N ` Y"and X': "X' <---- Inf (N ` Y)" unfolding closure_sequential by auto thenobtain X where X: "∧n. X n ∈ Y"and"X' = (λn. N (X n))"unfolding image_iff Bex_def bymetis
with X' have seq: "(λn. N (X n)) <---- Inf (N ` Y)"by simp have"(∪x ∈ Y. set_spmf x) ⊆ (∪n. set_spmf (X n))" proof(rule UN_least) fix x assume"x ∈ Y" from order_tendstoD(2)[OF seq NC_less[OF ‹x ∈ Y›]] obtain i where"N (X i) < N x"by (auto simp: eventually_sequentially) thus"set_spmf x ⊆ (∪n. set_spmf (X n))"using X ‹x ∈ Y› by(blast dest: N_less_imp_le_spmf ord_spmf_eqD_set_spmf) qed thus ?thesis by(rule countable_subset) simp qed qed simp
lemma lub_spmf_subprob: "(∫🪙+ x. (SUP p ∈ Y. ennreal (spmf p x)) ∂count_space UNIV) ≤ 1" proof(cases "Y = {}") case True thus ?thesis by(simp add: bot_ennreal) next case False let ?B = "∪p∈Y. set_spmf p" have countable: "countable ?B"by(rule spmf_chain_countable)
have"(∫🪙+ x. (SUP p∈Y. ennreal (spmf p x)) ∂count_space UNIV) = (∫🪙+ x. (SUP p∈Y. ennreal (spmf p x) * indicator ?B x) ∂count_space UNIV)" by (intro nn_integral_cong arg_cong [of _ _ Sup]) (auto split: split_indicator simp add: spmf_eq_0_set_spmf) alsohave"… = (∫🪙+ x. (SUP p∈Y. ennreal (spmf p x)) ∂count_space ?B)" unfolding ennreal_indicator[symmetric] using False by(subst SUP_mult_right_ennreal[symmetric])(simp add: ennreal_indicator nn_integral_count_space_indicator) alsohave"… = (SUP p∈Y. ∫🪙+ x. spmf p x ∂count_space ?B)"using False _ countable by(rule nn_integral_monotone_convergence_SUP_countable)(rule chain_ord_spmf_eqD) alsohave"…≤ 1" proof(rule SUP_least) fix p assume"p ∈ Y" have"(∫🪙+ x. spmf p x ∂count_space ?B) = ∫🪙+ x. ennreal (spmf p x) * indicator ?B x ∂count_space UNIV" by(simp add: nn_integral_count_space_indicator) alsohave"… = ∫🪙+ x. spmf p x ∂count_space UNIV" by(rule nn_integral_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf ‹p ∈ Y›) alsohave"…≤ 1" by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] weight_spmf_le_1) finallyshow"(∫🪙+ x. spmf p x ∂count_space ?B) ≤ 1" . qed finallyshow ?thesis . qed
lemma spmf_lub_spmf: assumes"Y ≠ {}" shows"spmf lub_spmf x = (SUP p ∈ Y. spmf p x)" proof - from assms obtain p where"p ∈ Y"by auto have"spmf lub_spmf x = max 0 (enn2real (SUP p∈Y. ennreal (spmf p x)))"unfolding lub_spmf_def by(rule spmf_embed_spmf)(simp del: SUP_eq_top_iff Sup_eq_top_iff add: ennreal_enn2real_if SUP_spmf_neq_top' lub_spmf_subprob) alsohave"… = enn2real (SUP p∈Y. ennreal (spmf p x))" by(rule max_absorb2)(simp) alsohave"… = enn2real (ennreal (SUP p ∈ Y. spmf p x))"using assms by(subst ennreal_SUP[symmetric])(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff) alsohave"0 ≤ (⊔p∈Y. spmf p x)"using assms by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] simp add: pmf_le_1) thenhave"enn2real (ennreal (SUP p ∈ Y. spmf p x)) = (SUP p ∈ Y. spmf p x)" by(rule enn2real_ennreal) finallyshow ?thesis . qed
lemma ennreal_spmf_lub_spmf: "Y ≠ {} ==> ennreal (spmf lub_spmf x) = (SUP p∈Y. ennreal (spmf p x))" by (metis SUP_spmf_neq_top' ennreal_SUP spmf_lub_spmf)
lemma lub_spmf_upper: assumes p: "p ∈ Y" shows"ord_spmf (=) p lub_spmf" proof(rule ord_pmf_increaseI) fix x from p have [simp]: "Y ≠ {}"by auto from p have"ennreal (spmf p x) ≤ (SUP p∈Y. ennreal (spmf p x))"by(rule SUP_upper) alsohave"… = ennreal (spmf lub_spmf x)"using p by(subst spmf_lub_spmf)(auto simp: ennreal_SUP SUP_spmf_neq_top' simp del: SUP_eq_top_iff Sup_eq_top_iff) finallyshow"spmf p x ≤ spmf lub_spmf x"by simp qed simp
lemma lub_spmf_least: assumes z: "∧x. x ∈ Y ==> ord_spmf (=) x z" shows"ord_spmf (=) lub_spmf z" proof(cases "Y = {}") case nonempty: False show ?thesis proof(rule ord_pmf_increaseI) fix x from nonempty obtain p where p: "p ∈ Y"by auto have"ennreal (spmf lub_spmf x) = (SUP p∈Y. ennreal (spmf p x))" by(subst spmf_lub_spmf)(auto simp: ennreal_SUP SUP_spmf_neq_top' nonempty simp del: SUP_eq_top_iff Sup_eq_top_iff) alsohave"…≤ ennreal (spmf z x)"by(rule SUP_least)(simp add: ord_spmf_eq_leD z) finallyshow"spmf lub_spmf x ≤ spmf z x"by simp qed simp qed simp
lemma set_lub_spmf: "set_spmf lub_spmf = (∪p∈Y. set_spmf p)" (is"?lhs = ?rhs") proof(cases "Y = {}") case [simp]: False show ?thesis proof(rule set_eqI) fix x have"x ∈ ?lhs ⟷ ennreal (spmf lub_spmf x) > 0" by(simp_all add: in_set_spmf_iff_spmf less_le) alsohave"…⟷ (∃p∈Y. ennreal (spmf p x) > 0)" by(simp add: ennreal_spmf_lub_spmf less_SUP_iff) alsohave"…⟷ x ∈ ?rhs" by(auto simp: in_set_spmf_iff_spmf less_le) finallyshow"x ∈ ?lhs ⟷ x ∈ ?rhs" . qed qed simp
lemma emeasure_lub_spmf: assumes Y: "Y ≠ {}" shows"emeasure (measure_spmf lub_spmf) A = (SUP y∈Y. emeasure (measure_spmf y) A)"
(is"?lhs = ?rhs") proof - let ?M = "count_space (set_spmf lub_spmf)" have"?lhs = ∫🪙+ x. ennreal (spmf lub_spmf x) * indicator A x ∂?M" by(auto simp: nn_integral_indicator[symmetric] nn_integral_measure_spmf') alsohave"… = ∫🪙+ x. (SUP y∈Y. ennreal (spmf y x) * indicator A x) ∂?M" unfolding ennreal_indicator[symmetric] by(simp add: spmf_lub_spmf assms ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal) alsofrom assms have"… = (SUP y∈Y. ∫🪙+ x. ennreal (spmf y x) * indicator A x ∂?M)" proof(rule nn_integral_monotone_convergence_SUP_countable) have"(λi x. ennreal (spmf i x) * indicator A x) ` Y = (λf x. f x * indicator A x) ` (λp x. ennreal (spmf p x)) ` Y" by(simp add: image_image) alsohave"Complete_Partial_Order.chain (≤) …"using chain_ord_spmf_eqD by(rule chain_imageI)(auto simp: le_fun_def split: split_indicator) finallyshow"Complete_Partial_Order.chain (≤) ((λi x. ennreal (spmf i x) * indicator A x) ` Y)" . qed simp alsohave"… = (SUP y∈Y. ∫🪙+ x. ennreal (spmf y x) * indicator A x ∂count_space UNIV)" by(auto simp: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: arg_cong [of _ _ Sup] image_cong nn_integral_cong) alsohave"… = ?rhs" by(auto simp: nn_integral_indicator[symmetric] nn_integral_measure_spmf) finallyshow ?thesis . qed
lemma measure_lub_spmf: assumes Y: "Y ≠ {}" shows"measure (measure_spmf lub_spmf) A = (SUP y∈Y. measure (measure_spmf y) A)"(is"?lhs = ?rhs") proof - have"ennreal ?lhs = ennreal ?rhs" using emeasure_lub_spmf[OF assms] SUP_emeasure_spmf_neq_top[of A Y] Y unfolding measure_spmf.emeasure_eq_measure by(subst ennreal_SUP) moreoverhave"0 ≤ ?rhs"using Y by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] measure_spmf.subprob_measure_le_1) ultimatelyshow ?thesis by(simp) qed
lemma measure_spmf_lub_spmf: assumes Y: "Y ≠ {}" shows"measure_spmf lub_spmf = (SUP p∈Y. measure_spmf p)" (is"?lhs = ?rhs") proof(rule measure_eqI) from assms obtain p where p: "p ∈ Y"by auto from chain have chain': "Complete_Partial_Order.chain (≤) (measure_spmf ` Y)" by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf) show"sets ?lhs = sets ?rhs" using Y by (subst sets_SUP) auto show"emeasure ?lhs A = emeasure ?rhs A"for A using chain' Y p by (subst emeasure_SUP_chain) (auto simp: emeasure_lub_spmf) qed
end
end
lemma partial_function_definitions_spmf: "partial_function_definitions (ord_spmf (=)) lub_spmf"
(is"partial_function_definitions ?R _") proof fix x show"?R x x"by(simp add: ord_spmf_reflI) next fix x y z assume"?R x y""?R y z" with transp_ord_option[OF transp_on_equality] show"?R x z"by(rule transp_rel_pmf[THEN transpD]) next fix x y assume"?R x y""?R y x" thus"x = y" by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymp_ord_option) next fix Y x assume"Complete_Partial_Order.chain ?R Y""x ∈ Y" thenshow"?R x (lub_spmf Y)" by(rule lub_spmf_upper) next fix Y z assume"Complete_Partial_Order.chain ?R Y""∧x. x ∈ Y ==> ?R x z" thenshow"?R (lub_spmf Y) z" by(cases "Y = {}")(simp_all add: lub_spmf_least) qed
lemma bind_lub_spmf2: assumes chain: "Complete_Partial_Order.chain ord Y" and g: "∧y. monotone ord (ord_spmf (=)) (g y)" shows"bind_spmf x (λy. lub_spmf (g y ` Y)) = lub_spmf ((λp. bind_spmf x (λy. g y p)) ` Y)"
(is"?lhs = ?rhs") proof(cases "Y = {}") case Y: False show ?thesis proof(rule spmf_eqI) fix i have chain': "∧y. Complete_Partial_Order.chain (ord_spmf (=)) (g y ` Y)" using chain g[THEN monotoneD] by(rule chain_imageI) have chain'': "Complete_Partial_Order.chain (≤) ((λp y. ennreal (spmf x y * spmf (g y p) i)) ` Y)" using chain by(rule chain_imageI)(auto simp: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono) have chain''': "Complete_Partial_Order.chain (ord_spmf (=)) ((λp. bind_spmf x (λy. g y p)) ` Y)" using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
have"ennreal (spmf ?lhs i) = ∫🪙+ y. (SUP p∈Y. ennreal (spmf x y * spmf (g y p) i)) ∂count_space (set_spmf x)" by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult image_comp) alsohave"… = (SUP p∈Y. ∫🪙+ y. ennreal (spmf x y * spmf (g y p) i) ∂count_space (set_spmf x))" unfolding nn_integral_measure_spmf' using Y chain'' by(rule nn_integral_monotone_convergence_SUP_countable) simp alsohave"… = (SUP p∈Y. ennreal (spmf (bind_spmf x (λy. g y p)) i))" by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult) alsohave"… = ennreal (spmf ?rhs i)"using chain''' by(auto simp: ennreal_spmf_lub_spmf Y image_comp) finallyshow"spmf ?lhs i = spmf ?rhs i"by simp qed qed simp
lemma mcont_bind_spmf [cont_intro]: assumes f: "mcont luba orda lub_spmf (ord_spmf (=)) f" and g: "∧y. mcont luba orda lub_spmf (ord_spmf (=)) (g y)" shows"mcont luba orda lub_spmf (ord_spmf (=)) (λx. bind_spmf (f x) (λy. g y x))" proof(rule spmf.mcont2mcont'[OF _ _ f]) fix z show"mcont lub_spmf (ord_spmf (=)) lub_spmf (ord_spmf (=)) (λx. bind_spmf x (λy. g y z))" by(rule mcont_bind_spmf1) next fix x let ?f = "λz. bind_spmf x (λy. g y z)" have"monotone orda (ord_spmf (=)) ?f"using mcont_mono[OF g] by(rule monotone_bind_spmf2) moreoverhave"cont luba orda lub_spmf (ord_spmf (=)) ?f" proof(rule contI) fix Y assume chain: "Complete_Partial_Order.chain orda Y"and Y: "Y ≠ {}" have"bind_spmf x (λy. g y (luba Y)) = bind_spmf x (λy. lub_spmf (g y ` Y))" by(rule bind_spmf_cong)(simp_all add: mcont_contD[OF g chain Y]) alsohave"… = lub_spmf ((λp. x 🍋 (λy. g y p)) ` Y)"using chain by(rule bind_lub_spmf2)(rule mcont_mono[OF g]) finallyshow"bind_spmf x (λy. g y (luba Y)) = …" . qed ultimatelyshow"mcont luba orda lub_spmf (ord_spmf (=)) ?f"by(rule mcontI) qed
lemma bind_pmf_mono [partial_function_mono]: "(∧y. mono_spmf (λf. C y f)) ==> mono_spmf (λf. bind_pmf p (λx. C x f))" using bind_spmf_mono[of "λ_. spmf_of_pmf p" C] by simp
lemma map_spmf_mono [partial_function_mono]: "mono_spmf B ==> mono_spmf (λg. map_spmf f (B g))" unfolding map_spmf_conv_bind_spmf by(rule bind_spmf_mono) simp_all
lemma mcont_map_spmf [cont_intro]: "mcont luba orda lub_spmf (ord_spmf (=)) g ==> mcont luba orda lub_spmf (ord_spmf (=)) (λx. map_spmf f (g x))" unfolding map_spmf_conv_bind_spmf by(rule mcont_bind_spmf) simp_all
lemma rel_spmf_measureD: assumes"rel_spmf R p q" shows"measure (measure_spmf p) A ≤ measure (measure_spmf q) {y. ∃x∈A. R x y}" (is"?lhs ≤ ?rhs") proof - have"?lhs = measure (measure_pmf p) (Some ` A)"by(simp add: measure_measure_spmf_conv_measure_pmf) alsohave"…≤ measure (measure_pmf q) {y. ∃x∈Some ` A. rel_option R x y}" using assms by(rule rel_pmf_measureD) alsohave"… = ?rhs"unfolding measure_measure_spmf_conv_measure_pmf by(rule arg_cong2[where f=measure])(auto simp: option_rel_Some1) finallyshow ?thesis . qed
locale rel_spmf_characterisation = assumes rel_pmf_measureI: "∧(R :: 'a option ==> 'b option ==> bool) p q. (∧A. measure (measure_pmf p) A ≤ measure (measure_pmf q) {y. ∃x∈A. R x y}) ==> rel_pmf R p q" 🍋‹This assumption is shown to hold in general in the AFP entry ‹MFMC_Countable›.› begin
contextfixes R :: "'a ==> 'b ==> bool"begin
lemma rel_spmf_measureI: assumes eq1: "∧A. measure (measure_spmf p) A ≤ measure (measure_spmf q) {y. ∃x∈A. R x y}" assumes eq2: "weight_spmf q ≤ weight_spmf p" shows"rel_spmf R p q" proof(rule rel_pmf_measureI) fix A :: "'a option set"
define A' where"A' = the ` (A ∩ range Some)"
define A'' where"A'' = A ∩ {None}" have A: "A = Some ` A' ∪ A''""Some ` A' ∩ A'' = {}" unfolding A'_def A''_defby(auto simp: image_iff) have"measure (measure_pmf p) A = measure (measure_pmf p) (Some ` A') + measure (measure_pmf p) A''" by(simp add: A measure_pmf.finite_measure_Union) alsohave"measure (measure_pmf p) (Some ` A') = measure (measure_spmf p) A'" by(simp add: measure_measure_spmf_conv_measure_pmf) alsohave"…≤ measure (measure_spmf q) {y. ∃x∈A'. R x y}"by(rule eq1) also (ord_eq_le_trans[OF _ add_right_mono]) have"… = measure (measure_pmf q) {y. ∃x∈A'. rel_option R (Some x) y}" unfolding measure_measure_spmf_conv_measure_pmf by(rule arg_cong2[where f=measure])(auto simp: A'_def option_rel_Some1) also
{ have"weight_spmf p ≤ measure (measure_spmf q) {y. ∃x. R x y}" using eq1[of UNIV] unfolding weight_spmf_def by simp alsohave"…≤ weight_spmf q"unfolding weight_spmf_def by(rule measure_spmf.finite_measure_mono) simp_all finallyhave"weight_spmf p = weight_spmf q"using eq2 by simp } thenhave"measure (measure_pmf p) A'' = measure (measure_pmf q) (if None ∈ A then {None} else {})" unfolding A''_defby(simp add: pmf_None_eq_weight_spmf measure_pmf_single) alsohave"measure (measure_pmf q) {y. ∃x∈A'. rel_option R (Some x) y} + … = measure (measure_pmf q) {y. ∃x∈A. rel_option R x y}" by(subst measure_pmf.finite_measure_Union[symmetric])
(auto 4 3 intro!: arg_cong2[where f=measure] simp add: option_rel_Some1 option_rel_Some2 A'_def intro: rev_bexI elim: option.rel_cases) finallyshow"measure (measure_pmf p) A ≤…" . qed
lemma admissible_rel_spmf: "ccpo.admissible (prod_lub lub_spmf lub_spmf) (rel_prod (ord_spmf (=)) (ord_spmf (=))) (case_prod (rel_spmf R))"
(is"ccpo.admissible ?lub ?ord ?P") proof(rule ccpo.admissibleI) fix Y assume chain: "Complete_Partial_Order.chain ?ord Y" and Y: "Y ≠ {}" and R: "∀(p, q) ∈ Y. rel_spmf R p q" from R have R: "∧p q. (p, q) ∈ Y ==> rel_spmf R p q"by auto have chain1: "Complete_Partial_Order.chain (ord_spmf (=)) (fst ` Y)" and chain2: "Complete_Partial_Order.chain (ord_spmf (=)) (snd ` Y)" using chain by(rule chain_imageI; clarsimp)+ from Y have Y1: "fst ` Y ≠ {}"and Y2: "snd ` Y ≠ {}"by auto
fix A have"measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y∈fst ` Y. measure (measure_spmf y) A)" using chain1 Y1 by(rule measure_lub_spmf) alsohave"…≤ (SUP y∈snd ` Y. measure (measure_spmf y) {y. ∃x∈A. R x y})"using Y1 by(rule cSUP_least)(auto intro!: cSUP_upper2[OF bdd_aboveI2[OF measure_spmf.subprob_measure_le_1]] rel_spmf_measureD R) alsohave"… = measure (measure_spmf (lub_spmf (snd ` Y))) {y. ∃x∈A. R x y}" using chain2 Y2 by(rule measure_lub_spmf[symmetric]) finallyshow"measure (measure_spmf (lub_spmf (fst ` Y))) A ≤…" . qed thenshow"?P (?lub Y)"by(simp add: prod_lub_def) qed
lemma admissible_rel_spmf_mcont [cont_intro]: "[ mcont lub ord lub_spmf (ord_spmf (=)) f; mcont lub ord lub_spmf (ord_spmf (=)) g ] ==> ccpo.admissible lub ord (λx. rel_spmf R (f x) (g x))" by(rule admissible_subst[OF admissible_rel_spmf, where f="λx. (f x, g x)", simplified])(rule mcont_Pair)
lemma spmf_restrict_spmf_outside [simp]: "x ∉ A ==> spmf (p ↿ A) x = 0" by(simp add: spmf_eq_0_set_spmf)
lemma emeasure_restrict_spmf [simp]: "emeasure (measure_spmf (p ↿ A)) X = emeasure (measure_spmf p) (X ∩ A)" proof - have"(λx. x 🍋 (λy. if y ∈ A then Some y else None)) -` the -` X ∩ (λx. x 🍋 (λy. if y ∈ A then Some y else None)) -` range Some = the -` X ∩ the -` A ∩ range Some" by(auto split: bind_splits if_split_asm) thenshow ?thesis by (simp add: restrict_spmf_def measure_spmf_def emeasure_distr emeasure_restrict_space) qed
lemma measure_restrict_spmf [simp]: "measure (measure_spmf (p ↿ A)) X = measure (measure_spmf p) (X ∩ A)" using emeasure_restrict_spmf[of p A X] by(simp only: measure_spmf.emeasure_eq_measure ennreal_inj measure_nonneg)
lemma spmf_restrict_spmf: "spmf (p ↿ A) x = (if x ∈ A then spmf p x else 0)" by(simp add: spmf_conv_measure_spmf)
lemma spmf_restrict_spmf_inside [simp]: "x ∈ A ==> spmf (p ↿ A) x = spmf p x" by(simp add: spmf_restrict_spmf)
lemma pmf_restrict_spmf_None: "pmf (p ↿ A) None = pmf p None + measure (measure_spmf p) (- A)" proof - have [simp]: "None ∉ Some ` (- A)"by auto have"(λx. x 🍋 (λy. if y ∈ A then Some y else None)) -` {None} = {None} ∪ (Some ` (- A))" by(auto split: bind_splits if_split_asm) thenshow ?thesis unfolding ereal.inject[symmetric] by(simp add: restrict_spmf_def ennreal_pmf_map emeasure_pmf_single del: ereal.inject)
(simp add: pmf.rep_eq measure_pmf.finite_measure_Union[symmetric] measure_measure_spmf_conv_measure_pmf measure_pmf.emeasure_eq_measure) qed
lemma restrict_spmf_trivial: "(∧x. x ∈ set_spmf p ==> x ∈ A) ==> p ↿ A = p" by(rule spmf_eqI)(auto simp: spmf_restrict_spmf spmf_eq_0_set_spmf)
lemma restrict_spmf_trivial': "set_spmf p ⊆ A ==> p ↿ A = p" by(rule restrict_spmf_trivial) blast
lemma restrict_return_spmf: "return_spmf x ↿ A = (if x ∈ A then return_spmf x else return_pmf None)" by(simp add: restrict_spmf_def)
lemma restrict_return_spmf_inside [simp]: "x ∈ A ==> return_spmf x ↿ A = return_spmf x" by(simp add: restrict_return_spmf)
lemma restrict_return_spmf_outside [simp]: "x ∉ A ==> return_spmf x ↿ A = return_pmf None" by(simp add: restrict_return_spmf)
lemma restrict_bind_pmf: "bind_pmf p g ↿ A = p 🍋 (λx. g x ↿ A)" by(simp add: restrict_spmf_def map_bind_pmf o_def)
lemma restrict_bind_spmf: "bind_spmf p g ↿ A = p 🍋 (λx. g x ↿ A)" by(auto simp: bind_spmf_def restrict_bind_pmf cong del: option.case_cong_weak cong: option.case_cong intro!: bind_pmf_cong split: option.split)
lemma bind_restrict_pmf: "bind_pmf (p ↿ A) g = p 🍋 (λx. if x ∈ Some ` A then g x else g None)" by(auto simp: restrict_spmf_def bind_map_pmf fun_eq_iff split: bind_split intro: arg_cong2[where f=bind_pmf])
lemma bind_restrict_spmf: "bind_spmf (p ↿ A) g = p 🍋 (λx. if x ∈ A then g x else return_pmf None)" by(auto simp: bind_spmf_def bind_restrict_pmf fun_eq_iff intro: arg_cong2[where f=bind_pmf] split: option.split)
lemma measure_eqI_restrict_spmf: assumes"rel_spmf R (restrict_spmf p A) (restrict_spmf q B)" shows"measure (measure_spmf p) A = measure (measure_spmf q) B" proof - from assms have"weight_spmf (restrict_spmf p A) = weight_spmf (restrict_spmf q B)"by(rule rel_spmf_weightD) thus ?thesis by(simp add: weight_spmf_def) qed
subsection‹Subprobability distributions of sets›
definition spmf_of_set :: "'a set ==> 'a spmf" where "spmf_of_set A = (if finite A ∧ A ≠ {} then spmf_of_pmf (pmf_of_set A) else return_pmf None)"
lemma spmf_of_set: "spmf (spmf_of_set A) x = indicator A x / card A" by(auto simp: spmf_of_set_def)
lemma pmf_spmf_of_set_None [simp]: "pmf (spmf_of_set A) None = indicator {A. infinite A ∨ A = {}} A" by(simp add: spmf_of_set_def)
lemma set_spmf_of_set: "set_spmf (spmf_of_set A) = (if finite A then A else {})" by(simp add: spmf_of_set_def)
lemma set_spmf_of_set_finite [simp]: "finite A ==> set_spmf (spmf_of_set A) = A" by(simp add: set_spmf_of_set)
lemma map_spmf_of_set_inj_on [simp]: "inj_on f A ==> map_spmf f (spmf_of_set A) = spmf_of_set (f ` A)" by(auto simp: spmf_of_set_def map_pmf_of_set_inj dest: finite_imageD)
lemma spmf_of_pmf_pmf_of_set [simp]: "[ finite A; A ≠ {} ]==> spmf_of_pmf (pmf_of_set A) = spmf_of_set A" by(simp add: spmf_of_set_def)
lemma weight_spmf_of_set: "weight_spmf (spmf_of_set A) = (if finite A ∧ A ≠ {} then 1 else 0)" by(auto simp only: spmf_of_set_def weight_spmf_of_pmf weight_return_pmf_None split: if_split)
lemma weight_spmf_of_set_finite [simp]: "[ finite A; A ≠ {} ]==> weight_spmf (spmf_of_set A) = 1" by(simp add: weight_spmf_of_set)
lemma weight_spmf_of_set_infinite [simp]: "infinite A ==> weight_spmf (spmf_of_set A) = 0" by(simp add: weight_spmf_of_set)
lemma measure_spmf_spmf_of_set: "measure_spmf (spmf_of_set A) = (if finite A ∧ A ≠ {} then measure_pmf (pmf_of_set A) else null_measure (count_space UNIV))" by(simp add: spmf_of_set_def del: spmf_of_pmf_pmf_of_set)
lemma emeasure_spmf_of_set: "emeasure (measure_spmf (spmf_of_set S)) A = card (S ∩ A) / card S" by(auto simp: measure_spmf_spmf_of_set emeasure_pmf_of_set)
lemma measure_spmf_of_set: "measure (measure_spmf (spmf_of_set S)) A = card (S ∩ A) / card S" by(auto simp: measure_spmf_spmf_of_set measure_pmf_of_set)
lemma nn_integral_spmf_of_set: "nn_integral (measure_spmf (spmf_of_set A)) f = sum f A / card A" by(cases "finite A")(auto simp: spmf_of_set_def nn_integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set)
lemma integral_spmf_of_set: "integral🪙L (measure_spmf (spmf_of_set A)) f = sum f A / card A" by (metis card.infinite div_0 division_ring_divide_zero integral_null_measure integral_pmf_of_set measure_spmf_spmf_of_set of_nat_0 sum.empty)
notepad begin🍋‹🍋‹pmf_of_set›is not fully parametric.›
define R :: "nat ==> nat ==> bool"where"R x y ⟷ (x ≠ 0 ⟶ y = 0)"for x y
define A :: "nat set"where"A = {0, 1}"
define B :: "nat set"where"B = {0, 1, 2}" have"rel_set R A B"unfolding R_def[abs_def] A_def B_def rel_set_def by auto have"¬ rel_pmf R (pmf_of_set A) (pmf_of_set B)" proof assume"rel_pmf R (pmf_of_set A) (pmf_of_set B)" thenobtain pq where pq: "∧x y. (x, y) ∈ set_pmf pq ==> R x y" and 1: "map_pmf fst pq = pmf_of_set A" and 2: "map_pmf snd pq = pmf_of_set B" by cases auto have"pmf (pmf_of_set B) 1 = 1 / 3"by(simp add: B_def) have"pmf (pmf_of_set B) 2 = 1 / 3"by(simp add: B_def)
lemma rel_pmf_of_set_bij: assumes f: "bij_betw f A B" and A: "A ≠ {}""finite A" and B: "B ≠ {}""finite B" and R: "∧x. x ∈ A ==> R x (f x)" shows"rel_pmf R (pmf_of_set A) (pmf_of_set B)" proof(rule pmf.rel_mono_strong)
define AB where"AB = (λx. (x, f x)) ` A"
define R' where"R' x y ⟷ (x, y) ∈ AB"for x y have"(x, y) ∈ AB"if"(x, y) ∈ set_pmf (pmf_of_set AB)"for x y using that by(auto simp: AB_def A) moreoverhave"map_pmf fst (pmf_of_set AB) = pmf_of_set A" by(simp add: AB_def map_pmf_of_set_inj[symmetric] inj_on_def A pmf.map_comp o_def) moreover from f have [simp]: "inj_on f A"by(rule bij_betw_imp_inj_on) from f have [simp]: "f ` A = B"by(rule bij_betw_imp_surj_on) have"map_pmf snd (pmf_of_set AB) = pmf_of_set B" by(simp add: AB_def map_pmf_of_set_inj[symmetric] inj_on_def A pmf.map_comp o_def)
(simp add: map_pmf_of_set_inj A) ultimatelyshow"rel_pmf (λx y. (x, y) ∈ AB) (pmf_of_set A) (pmf_of_set B)" .. qed(auto intro: R)
lemma rel_spmf_of_set_bij: assumes f: "bij_betw f A B" and R: "∧x. x ∈ A ==> R x (f x)" shows"rel_spmf R (spmf_of_set A) (spmf_of_set B)" proof - obtain"finite A ⟷ finite B""A = {} ⟷ B = {}" using bij_betw_empty1 bij_betw_empty2 bij_betw_finite f by blast thenshow ?thesis using assms by (metis rel_pmf_of_set_bij rel_spmf_spmf_of_pmf return_spmf_None_parametric spmf_of_set_def) qed
contextincludes lifting_syntax begin
lemma rel_spmf_of_set: assumes"bi_unique R" shows"(rel_set R ===> rel_spmf R) spmf_of_set spmf_of_set" proof fix A B assume R: "rel_set R A B" with assms obtain f where"bij_betw f A B"and f: "∧x. x ∈ A ==> R x (f x)" by(auto dest: bi_unique_rel_set_bij_betw) thenshow"rel_spmf R (spmf_of_set A) (spmf_of_set B)" by(rule rel_spmf_of_set_bij) qed
end
lemma map_mem_spmf_of_set: assumes"finite B""B ≠ {}" shows"map_spmf (λx. x ∈ A) (spmf_of_set B) = spmf_of_pmf (bernoulli_pmf (card (A ∩ B) / card B))"
(is"?lhs = ?rhs") proof(rule spmf_eqI) fix i have"ennreal (spmf ?lhs i) = card (B ∩ (λx. x ∈ A) -` {i}) / (card B)" by(subst ennreal_spmf_map)(simp add: measure_spmf_spmf_of_set assms emeasure_pmf_of_set) alsohave"… = (if i then card (B ∩ A) / card B else card (B - A) / card B)" by(auto intro: arg_cong[where f=card]) alsohave"… = (if i then card (B ∩ A) / card B else (card B - card (B ∩ A)) / card B)" by(auto simp: card_Diff_subset_Int assms) alsohave"… = ennreal (spmf ?rhs i)" by(simp add: assms card_gt_0_iff field_simps card_mono Int_commute of_nat_diff) finallyshow"spmf ?lhs i = spmf ?rhs i"by simp qed
lemma lossless_spmf_conv_spmf_of_pmf: "lossless_spmf p ⟷ (∃p'. p = spmf_of_pmf p')" proof assume"lossless_spmf p" hence *: "∧y. y ∈ set_pmf p ==>∃x. y = Some x" by(case_tac y)(simp_all add: lossless_iff_set_pmf_None)
let ?p = "map_pmf the p" have"p = spmf_of_pmf ?p" proof(rule spmf_eqI) fix i have"ennreal (pmf (map_pmf the p) i) = ∫🪙+ x. indicator (the -` {i}) x ∂p"by(simp add: ennreal_pmf_map) alsohave"… = ∫🪙+ x. indicator {i} x ∂measure_spmf p"unfolding measure_spmf_def by(subst nn_integral_distr)(auto simp: nn_integral_restrict_space AE_measure_pmf_iff simp del: nn_integral_indicator intro!: nn_integral_cong_AE split: split_indicator dest!: * ) alsohave"… = spmf p i"by(simp add: emeasure_spmf_single) finallyshow"spmf p i = spmf (spmf_of_pmf ?p) i"by simp qed thus"∃p'. p = spmf_of_pmf p'" .. qed auto
lemma spmf_False_conv_True: "lossless_spmf p ==> spmf p False = 1 - spmf p True" by(clarsimp simp add: lossless_spmf_conv_spmf_of_pmf pmf_False_conv_True)
lemma spmf_True_conv_False: "lossless_spmf p ==> spmf p True = 1 - spmf p False" by(simp add: spmf_False_conv_True)
lemma bind_eq_return_spmf: "bind_spmf p f = return_spmf x ⟷ (∀y∈set_spmf p. f y = return_spmf x) ∧ lossless_spmf p" apply (simp add: bind_spmf_def bind_eq_return_pmf split: option.split) by (metis in_set_spmf lossless_iff_set_pmf_None not_None_eq)
lemma rel_spmf_return_spmf2: "rel_spmf R p (return_spmf x) ⟷ lossless_spmf p ∧ (∀a∈set_spmf p. R a x)" apply (simp add: lossless_iff_set_pmf_None rel_pmf_return_pmf2 option_rel_Some2 in_set_spmf) by (metis in_set_spmf not_None_eq option.sel)
lemma rel_spmf_return_spmf1: "rel_spmf R (return_spmf x) p ⟷ lossless_spmf p ∧ (∀a∈set_spmf p. R x a)" using rel_spmf_return_spmf2[of "R-1-1"] by(simp add: spmf_rel_conversep)
lemma rel_spmf_bindI1: assumes f: "∧x. x ∈ set_spmf p ==> rel_spmf R (f x) q" and p: "lossless_spmf p" shows"rel_spmf R (bind_spmf p f) q" proof - fix x :: 'a have"rel_spmf R (bind_spmf p f) (bind_spmf (return_spmf x) (λ_. q))" by(rule rel_spmf_bindI[where R="λx _. x ∈ set_spmf p"])(simp_all add: rel_spmf_return_spmf2 p f) thenshow ?thesis by simp qed
lemma rel_spmf_bindI2: "[∧x. x ∈ set_spmf q ==> rel_spmf R p (f x); lossless_spmf q ] ==> rel_spmf R p (bind_spmf q f)" using rel_spmf_bindI1[of q "conversep R" f p] by(simp add: spmf_rel_conversep)
subsection‹Scaling›
definition scale_spmf :: "real ==> 'a spmf ==> 'a spmf" where "scale_spmf r p = embed_spmf (λx. min (inverse (weight_spmf p)) (max 0 r) * spmf p x)"
lemma scale_spmf_le_1: "(∫🪙+ x. min (inverse (weight_spmf p)) (max 0 r) * spmf p x ∂count_space UNIV) ≤ 1" (is"?lhs ≤ _") proof - have"?lhs = min (inverse (weight_spmf p)) (max 0 r) * ∫🪙+ x. spmf p x ∂count_space UNIV" by(subst nn_integral_cmult[symmetric])(simp_all add: weight_spmf_nonneg max_def min_def ennreal_mult) alsohave"…≤ 1"unfolding weight_spmf_eq_nn_integral_spmf[symmetric] by(simp add: min_def max_def weight_spmf_nonneg order.strict_iff_order field_simps ennreal_mult[symmetric]) finallyshow ?thesis . qed
lemma real_inverse_le_1_iff: fixes x :: real shows"[ 0 ≤ x; x ≤ 1 ]==> 1 / x ≤ 1 ⟷ x = 1 ∨ x = 0" by auto
lemma spmf_scale_spmf': "r ≤ 1 ==> spmf (scale_spmf r p) x = max 0 r * spmf p x" using real_inverse_le_1_iff[OF weight_spmf_nonneg weight_spmf_le_1, of p] by(auto simp: spmf_scale_spmf max_def min_def field_simps)(metis pmf_le_0_iff spmf_le_weight)
lemma scale_spmf_neg: "r ≤ 0 ==> scale_spmf r p = return_pmf None" by(rule spmf_eqI)(simp add: spmf_scale_spmf' max_def)
lemma scale_spmf_conv_bind_bernoulli: assumes"r ≤ 1" shows"scale_spmf r p = bind_pmf (bernoulli_pmf r) (λb. if b then p else return_pmf None)" (is"?lhs = ?rhs") proof(rule spmf_eqI) fix x have"[weight_spmf p = 0]==> spmf p x = 0" by (metis pmf_le_0_iff spmf_le_weight) moreoverhave"[weight_spmf p ≠ 0; 1 / weight_spmf p < 1]==> weight_spmf p = 1" by (smt (verit) divide_less_eq_1 measure_spmf.subprob_measure_le_1 weight_spmf_lt_0) ultimatelyhave"ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using assms unfolding spmf_scale_spmf ennreal_pmf_bind nn_integral_measure_pmf UNIV_bool bernoulli_pmf.rep_eq by(auto simp: nn_integral_count_space_finite max_def min_def field_simps
real_inverse_le_1_iff[OF weight_spmf_nonneg weight_spmf_le_1] ennreal_mult[symmetric]) thus"spmf ?lhs x = spmf ?rhs x"by simp qed
lemma nn_integral_spmf: "(∫🪙+ x. spmf p x ∂count_space A) = emeasure (measure_spmf p) A" proof - have"bij_betw Some A (the -` A ∩ range Some)" by(auto simp: bij_betw_def) thenshow ?thesis by (metis bij_betw_def emeasure_measure_spmf_conv_measure_pmf nn_integral_pmf') qed
lemma measure_spmf_scale_spmf': assumes"r ≤ 1" shows"measure_spmf (scale_spmf r p) = scale_measure r (measure_spmf p)" proof(cases "weight_spmf p > 0") case True with assms show ?thesis by(simp add: measure_spmf_scale_spmf field_simps weight_spmf_le_1 mult_le_one) next case False thenshow ?thesis by (simp add: order_less_le weight_spmf_eq_0) qed
lemma scale_spmf_1 [simp]: "scale_spmf 1 p = p" by (simp add: spmf_eqI spmf_scale_spmf')
lemma scale_spmf_0 [simp]: "scale_spmf 0 p = return_pmf None" by (simp add: scale_spmf_neg)
lemma bind_scale_spmf: assumes r: "r ≤ 1" shows"bind_spmf (scale_spmf r p) f = bind_spmf p (λx. scale_spmf r (f x))"
(is"?lhs = ?rhs") proof(rule spmf_eqI) fix x have"ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using r by(simp add: ennreal_spmf_bind measure_spmf_scale_spmf' nn_integral_scale_measure spmf_scale_spmf'
ennreal_mult nn_integral_cmult) thus"spmf ?lhs x = spmf ?rhs x"by simp qed
lemma scale_bind_spmf: assumes"r ≤ 1" shows"scale_spmf r (bind_spmf p f) = bind_spmf p (λx. scale_spmf r (f x))"
(is"?lhs = ?rhs") proof(rule spmf_eqI) fix x have"ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)"using assms unfolding spmf_scale_spmf'[OF assms] by(simp add: ennreal_mult ennreal_spmf_bind spmf_scale_spmf' nn_integral_cmult max_def min_def) thus"spmf ?lhs x = spmf ?rhs x"by simp qed
lemma bind_spmf_const: "bind_spmf p (λx. q) = scale_spmf (weight_spmf p) q" (is"?lhs = ?rhs") proof(rule spmf_eqI) fix x have"ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using measure_spmf.subprob_measure_le_1[of p "space (measure_spmf p)"] by(subst ennreal_spmf_bind)(simp add: spmf_scale_spmf' weight_spmf_le_1 ennreal_mult mult.commute max_def min_def measure_spmf.emeasure_eq_measure) thus"spmf ?lhs x = spmf ?rhs x"by simp qed
lemma map_scale_spmf: "map_spmf f (scale_spmf r p) = scale_spmf r (map_spmf f p)" (is"?lhs = ?rhs") proof(rule spmf_eqI) fix i show"spmf ?lhs i = spmf ?rhs i"unfolding spmf_scale_spmf by(subst (1 2) spmf_map)(auto simp: measure_spmf_scale_spmf max_def min_def ennreal_lt_0) qed
lemma set_scale_spmf: "set_spmf (scale_spmf r p) = (if r > 0 then set_spmf p else {})" apply(auto simp: in_set_spmf_iff_spmf spmf_scale_spmf) apply(simp add: min_def weight_spmf_eq_0 split: if_split_asm) done
lemma set_scale_spmf' [simp]: "0 < r ==> set_spmf (scale_spmf r p) = set_spmf p" by(simp add: set_scale_spmf)
lemma rel_spmf_scaleI: assumes"r > 0 ==> rel_spmf A p q" shows"rel_spmf A (scale_spmf r p) (scale_spmf r q)" proof(cases "r > 0") case True from assms[OF True] show ?thesis by(rule rel_spmfE)(auto simp: map_scale_spmf[symmetric] spmf_rel_map True intro: rel_spmf_reflI) qed(simp add: not_less scale_spmf_neg)
lemma weight_scale_spmf: "weight_spmf (scale_spmf r p) = min 1 (max 0 r * weight_spmf p)" proof - have"[1 / weight_spmf p ≤ r; ennreal r * ennreal (weight_spmf p) < 1]==> weight_spmf p = 0" by (smt (verit) ennreal_less_one_iff ennreal_mult'' measure_le_0_iff mult_imp_less_div_pos) moreover have"[r < 1 / weight_spmf p; 1 ≤ ennreal r * ennreal (weight_spmf p)]==> weight_spmf p = 0" by (smt (verit, ccfv_threshold) ennreal_ge_1 ennreal_mult'' mult_imp_div_pos_le weight_spmf_lt_0) ultimately have"ennreal (weight_spmf (scale_spmf r p)) = min 1 (max 0 r * ennreal (weight_spmf p))" unfolding weight_spmf_eq_nn_integral_spmf apply(simp add: spmf_scale_spmf ennreal_mult zero_ereal_def[symmetric] nn_integral_cmult) apply(auto simp: weight_spmf_eq_nn_integral_spmf[symmetric] field_simps min_def max_def not_le weight_spmf_lt_0 ennreal_mult[symmetric]) done thus ?thesis by(auto simp: min_def max_def ennreal_mult[symmetric] split: if_split_asm) qed
lemma weight_scale_spmf' [simp]: "[ 0 ≤ r; r ≤ 1 ]==> weight_spmf (scale_spmf r p) = r * weight_spmf p" by(simp add: weight_scale_spmf max_def min_def)(metis antisym_conv mult_left_le order_trans weight_spmf_le_1)
lemma pmf_scale_spmf_None: "pmf (scale_spmf k p) None = 1 - min 1 (max 0 k * (1 - pmf p None))" unfolding pmf_None_eq_weight_spmf by(simp add: weight_scale_spmf)
lemma scale_scale_spmf: "scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
(is"?lhs = ?rhs") proof(cases "weight_spmf p > 0") case False thus ?thesis by (simp add: weight_spmf_eq_0 zero_less_measure_iff) next case True show ?thesis proof(rule spmf_eqI) fix i have *: "max 0 (min (1 / weight_spmf p) r') * max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) = max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))" using True by (simp add: max_def) (auto simp: min_def field_simps zero_le_mult_iff) show"spmf ?lhs i = spmf ?rhs i" by (simp add: spmf_scale_spmf) (metis * inverse_eq_divide mult.commute weight_scale_spmf) qed qed
lemma scale_scale_spmf' [simp]: assumes"0 ≤ r""r ≤ 1""0 ≤ r'""r' ≤ 1" shows"scale_spmf r (scale_spmf r' p) = scale_spmf (r * r') p" proof(cases "weight_spmf p > 0") case True with assms have"r' = 1"if"1 ≤ r' * weight_spmf p" by (smt (verit, best) measure_spmf.subprob_measure_le_1 mult_eq_1 mult_le_one that) with assms True show ?thesis by (smt (verit, best) eq_divide_imp measure_le_0_iff mult.assoc mult_nonneg_nonneg scale_scale_spmf weight_scale_spmf') next case False with assms show ?thesis by (simp add: weight_spmf_eq_0 zero_less_measure_iff) qed
lemma scale_spmf_eq_same: "scale_spmf r p = p ⟷ weight_spmf p = 0 ∨ r = 1 ∨ r ≥ 1 ∧ weight_spmf p = 1"
(is"?lhs ⟷ ?rhs") proof assume ?lhs hence"weight_spmf (scale_spmf r p) = weight_spmf p"by simp hence *: "min 1 (max 0 r * weight_spmf p) = weight_spmf p"by(simp add: weight_scale_spmf) hence **: "weight_spmf p = 0 ∨ r ≥ 1"by(auto simp: min_def max_def split: if_split_asm) show ?rhs proof(cases "weight_spmf p = 0") case False with ** have"r ≥ 1" by simp with * False have"r = 1 ∨ weight_spmf p = 1" by(simp add: max_def min_def not_le split: if_split_asm) with‹r ≥ 1›show ?thesis by simp qed simp next show"weight_spmf p = 0 ∨ r = 1 ∨ 1 ≤ r ∧ weight_spmf p = 1 ==> scale_spmf r p = p" by (smt (verit) div_by_1 inverse_eq_divide inverse_positive_iff_positive scale_scale_spmf scale_spmf_1) qed
lemma map_const_spmf_of_set: "[ finite A; A ≠ {} ]==> map_spmf (λ_. c) (spmf_of_set A) = return_spmf c" by(simp add: map_spmf_conv_bind_spmf bind_spmf_const)
subsection‹Conditional spmfs›
lemma set_pmf_Int_Some: "set_pmf p ∩ Some ` A = {} ⟷ set_spmf p ∩ A = {}" by(auto simp: in_set_spmf)
lemma measure_spmf_zero_iff: "measure (measure_spmf p) A = 0 ⟷ set_spmf p ∩ A = {}" unfolding measure_measure_spmf_conv_measure_pmf by(simp add: measure_pmf_zero_iff set_pmf_Int_Some)
definition cond_spmf :: "'a spmf ==> 'a set ==> 'a spmf" where"cond_spmf p A = (if set_spmf p ∩ A = {} then return_pmf None else cond_pmf p (Some ` A))"
lemma set_cond_spmf [simp]: "set_spmf (cond_spmf p A) = set_spmf p ∩ A" by(auto 4 4 simp add: cond_spmf_def in_set_spmf iff: set_cond_pmf[THEN set_eq_iff[THEN iffD1], THEN spec, rotated])
lemma cond_map_spmf [simp]: "cond_spmf (map_spmf f p) A = map_spmf f (cond_spmf p (f -` A))" proof - have"map_option f -` Some ` A = Some ` f -` A"by auto moreoverhave"set_pmf p ∩ map_option f -` Some ` A ≠ {}"if"Some x ∈ set_pmf p""f x ∈ A"for x using that by auto ultimatelyshow ?thesis by(auto simp: cond_spmf_def in_set_spmf cond_map_pmf) qed
lemma spmf_cond_spmf [simp]: "spmf (cond_spmf p A) x = (if x ∈ A then spmf p x / measure (measure_spmf p) A else 0)" by(auto simp: cond_spmf_def pmf_cond set_pmf_Int_Some[symmetric] measure_measure_spmf_conv_measure_pmf measure_pmf_zero_iff)
lemma bind_eq_return_pmf_None: "bind_spmf p f = return_pmf None ⟷ (∀x∈set_spmf p. f x = return_pmf None)" by(auto simp: bind_spmf_def bind_eq_return_pmf in_set_spmf split: option.splits)
lemma return_pmf_None_eq_bind: "return_pmf None = bind_spmf p f ⟷ (∀x∈set_spmf p. f x = return_pmf None)" using bind_eq_return_pmf_None[of p f] by auto
(* Conditional probabilities do not seem to interact nicely with bind. *)
subsection‹Product spmf›
definition pair_spmf :: "'a spmf ==> 'b spmf ==> ('a × 'b) spmf" where"pair_spmf p q = bind_pmf (pair_pmf p q) (λxy. case xy of (Some x, Some y) ==> return_spmf (x, y) | _ ==> return_pmf None)"
lemma spmf_pair [simp]: "spmf (pair_spmf p q) (x, y) = spmf p x * spmf q y" (is"?lhs = ?rhs") proof - have"ennreal ?lhs = ∫🪙+ a. ∫🪙+ b. indicator {(x, y)} (a, b) ∂measure_spmf q ∂measure_spmf p" unfolding measure_spmf_def pair_spmf_def ennreal_pmf_bind nn_integral_pair_pmf' by(auto simp: zero_ereal_def[symmetric] nn_integral_distr nn_integral_restrict_space nn_integral_multc[symmetric] intro!: nn_integral_cong split: option.split split_indicator) alsohave"… = ∫🪙+ a. (∫🪙+ b. indicator {y} b ∂measure_spmf q) * indicator {x} a ∂measure_spmf p" by(subst nn_integral_multc[symmetric])(auto intro!: nn_integral_cong split: split_indicator) alsohave"… = ennreal ?rhs"by(simp add: emeasure_spmf_single max_def ennreal_mult mult.commute) finallyshow ?thesis by simp qed
lemma pair_map_spmf2: "pair_spmf p (map_spmf f q) = map_spmf (apsnd f) (pair_spmf p q)" unfolding pair_spmf_def pair_map_pmf2 bind_map_pmf map_bind_pmf by (intro bind_pmf_cong refl) (auto split: option.split)
lemma pair_map_spmf1: "pair_spmf (map_spmf f p) q = map_spmf (apfst f) (pair_spmf p q)" unfolding pair_spmf_def pair_map_pmf1 bind_map_pmf map_bind_pmf by (intro bind_pmf_cong refl) (auto split: option.split)
lemma pair_map_spmf: "pair_spmf (map_spmf f p) (map_spmf g q) = map_spmf (map_prod f g) (pair_spmf p q)" unfolding pair_map_spmf2 pair_map_spmf1 spmf.map_comp by(simp add: apfst_def apsnd_def o_def prod.map_comp)
lemma pair_spmf_alt_def: "pair_spmf p q = bind_spmf p (λx. bind_spmf q (λy. return_spmf (x, y)))" unfolding pair_spmf_def pair_pmf_def bind_spmf_def bind_assoc_pmf bind_return_pmf by (intro bind_pmf_cong refl) (auto split: option.split)
lemma weight_pair_spmf [simp]: "weight_spmf (pair_spmf p q) = weight_spmf p * weight_spmf q" unfolding pair_spmf_alt_def by(simp add: weight_bind_spmf o_def)
lemma pair_scale_spmf1: (* FIXME: generalise to arbitrary r *) "r ≤ 1 ==> pair_spmf (scale_spmf r p) q = scale_spmf r (pair_spmf p q)" by(simp add: pair_spmf_alt_def scale_bind_spmf bind_scale_spmf)
lemma pair_scale_spmf2: (* FIXME: generalise to arbitrary r *) "r ≤ 1 ==> pair_spmf p (scale_spmf r q) = scale_spmf r (pair_spmf p q)" by(simp add: pair_spmf_alt_def scale_bind_spmf bind_scale_spmf)
lemma set_spmf_assert_spmf_eq_empty [simp]: "set_spmf (assert_spmf b) = {} ⟷¬ b" by auto
lemma lossless_assert_spmf [iff]: "lossless_spmf (assert_spmf b) ⟷ b" by(cases b) simp_all
subsection‹Try›
definition try_spmf :: "'a spmf ==> 'a spmf ==> 'a spmf"
(‹(‹open_block notation=‹mixfix try_spmf›\› [0,60] 59) where"TRY p ELSE q = bind_pmf p (λx. case x of None ==> q | Some y ==> return_spmf y)"
lemma try_spmf_lossless [simp]: assumes"lossless_spmf p" shows"TRY p ELSE q = p" proof - have"TRY p ELSE q = bind_pmf p return_pmf"unfolding try_spmf_def using assms by(auto simp: lossless_iff_set_pmf_None split: option.split intro: bind_pmf_cong) thus ?thesis by(simp add: bind_return_pmf') qed
lemma try_spmf_return_spmf1: "TRY return_spmf x ELSE q = return_spmf x" by simp
lemma try_spmf_parametric [transfer_rule]: "(rel_spmf A ===> rel_spmf A ===> rel_spmf A) try_spmf try_spmf" unfolding try_spmf_def[abs_def] by transfer_prover
end
lemma try_spmf_cong: "[ p = p'; ¬ lossless_spmf p' ==> q = q' ]==> TRY p ELSE q = TRY p' ELSE q'" unfolding try_spmf_def by(rule bind_pmf_cong)(auto split: option.split simp add: lossless_iff_set_pmf_None)
lemma rel_spmf_try_spmf: "[ rel_spmf R p p'; ¬ lossless_spmf p' ==> rel_spmf R q q' ] ==> rel_spmf R (TRY p ELSE q) (TRY p' ELSE q')" unfolding try_spmf_def apply(rule rel_pmf_bindI[where R="λx y. rel_option R x y ∧ x ∈ set_pmf p ∧ y ∈ set_pmf p'"]) apply (simp add: pmf.rel_mono_strong) apply(auto split: option.split simp add: lossless_iff_set_pmf_None) done
lemma spmf_try_spmf: "spmf (TRY p ELSE q) x = spmf p x + pmf p None * spmf q x" proof - have"ennreal (spmf (TRY p ELSE q) x) = ∫🪙+ y. ennreal (spmf q x) * indicator {None} y + indicator {Some x} y ∂measure_pmf p" unfolding try_spmf_def ennreal_pmf_bind by(rule nn_integral_cong)(simp split: option.split split_indicator) alsohave"… = (∫🪙+ y. ennreal (spmf q x) * indicator {None} y ∂measure_pmf p) + ∫??+ y. indicator {Some x} y ∂measure_pmf p" by(simp add: nn_integral_add) alsohave"… = ennreal (spmf q x) * pmf p None + spmf p x"by(simp add: emeasure_pmf_single) finallyshow ?thesis by(simp flip: ennreal_plus ennreal_mult) qed
lemma try_scale_spmf_same [simp]: "lossless_spmf p ==> TRY scale_spmf k p ELSE p = p" by(rule spmf_eqI)(auto simp: spmf_try_spmf spmf_scale_spmf pmf_scale_spmf_None lossless_iff_pmf_None weight_spmf_conv_pmf_None min_def max_def field_simps)
lemma try_bind_assert_spmf: "TRY (assert_spmf b 🍋 f) ELSE q = (if b then TRY (f ()) ELSE q else q)" by simp
subsection‹Miscellaneous›
lemmaassumes"rel_spmf (λx y. bad1 x = bad2 y ∧ (¬ bad2 y ⟶ A x ⟷ B y)) p q" (is"rel_spmf ?A _ _") shows fundamental_lemma_bad: "measure (measure_spmf p) {x. bad1 x} = measure (measure_spmf q) {y. bad2 y}" (is"?bad") and fundamental_lemma: "∣measure (measure_spmf p) {x. A x} - measure (measure_spmf q) {y. B y}∣≤ measure (measure_spmf p) {x. bad1 x}" (is ?fundamental) proof - have good: "rel_fun ?A (=) (λx. A x ∧¬ bad1 x) (λy. B y ∧¬ bad2 y)"by(auto simp: rel_fun_def) from assms have 1: "measure (measure_spmf p) {x. A x ∧¬ bad1 x} = measure (measure_spmf q) {y. B y ∧¬ bad2 y}" by(rule measure_spmf_parametric[THEN rel_funD, THEN rel_funD])(rule Collect_parametric[THEN rel_funD, OF good])
have bad: "rel_fun ?A (=) bad1 bad2"by(simp add: rel_fun_def) show 2: ?bad using assms by(rule measure_spmf_parametric[THEN rel_funD, THEN rel_funD])(rule Collect_parametric[THEN rel_funD, OF bad])
let ?μp = "measure (measure_spmf p)"and ?μq = "measure (measure_spmf q)" have"{x. A x ∧ bad1 x} ∪ {x. A x ∧¬ bad1 x} = {x. A x}" and"{y. B y ∧ bad2 y} ∪ {y. B y ∧¬ bad2 y} = {y. B y}"by auto thenhave"∣?μp {x. A x} - ?μq {x. B x}∣ = ∣?μp ({x. A x ∧ bad1 x} ∪ {x. A x ∧¬ bad1 x}) - ?μq ({y. B y ∧ bad2 y} ∪ {y. B y ∧¬ bad2 y})∣" by simp alsohave"… = ∣?μp {x. A x ∧ bad1 x} + ?μp {x. A x ∧¬ bad1 x} - ?μq {y. B y ∧ bad2 y} - ?μq {y. B y ∧¬ bad2 y}∣" by(subst (1 2) measure_Union)(auto) alsohave"… = ∣?μp {x. A x ∧ bad1 x} - ?μq {y. B y ∧ bad2 y}∣"using 1 by simp alsohave"…≤ max (?μp {x. A x ∧ bad1 x}) (?μq {y. B y ∧ bad2 y})" by(rule abs_leI)(auto simp: max_def not_le, simp_all only: add_increasing measure_nonneg mult_2) alsohave"…≤ max (?μp {x. bad1 x}) (?μq {y. bad2 y})" by(rule max.mono; rule measure_spmf.finite_measure_mono; auto) alsonote 2[symmetric] finallyshow ?fundamental by simp qed
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.103 Sekunden
(vorverarbeitet am 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
