merged
authorAndreas Lochbihler
Wed Jun 08 09:05:32 2016 +0200 (2016-06-08)
changeset 63245ea13f44da888
parent 63242 9986559617ee
parent 63244 af43e35211c8
child 63246 c493859d4267
merged
     1.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Mon Jun 06 22:22:05 2016 +0200
     1.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Jun 08 09:05:32 2016 +0200
     1.3 @@ -1701,10 +1701,48 @@
     1.4    \<Longrightarrow> mcont lub ord lubb ordb (\<lambda>x. snd (t x))"
     1.5  by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
     1.6  
     1.7 +lemma monotone_Pair:
     1.8 +  "\<lbrakk> monotone ord orda f; monotone ord ordb g \<rbrakk>
     1.9 +  \<Longrightarrow> monotone ord (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
    1.10 +by(simp add: monotone_def)
    1.11 +
    1.12 +lemma cont_Pair:
    1.13 +  "\<lbrakk> cont lub ord luba orda f; cont lub ord lubb ordb g \<rbrakk>
    1.14 +  \<Longrightarrow> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
    1.15 +by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
    1.16 +
    1.17 +lemma mcont_Pair:
    1.18 +  "\<lbrakk> mcont lub ord luba orda f; mcont lub ord lubb ordb g \<rbrakk>
    1.19 +  \<Longrightarrow> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
    1.20 +by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
    1.21 +
    1.22  context partial_function_definitions begin
    1.23  text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
    1.24  lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
    1.25  lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
    1.26  end
    1.27  
    1.28 +lemma map_option_mono [partial_function_mono]:
    1.29 +  "mono_option B \<Longrightarrow> mono_option (\<lambda>f. map_option g (B f))"
    1.30 +unfolding map_conv_bind_option by(rule bind_mono) simp_all
    1.31 +
    1.32 +lemma compact_flat_lub [cont_intro]: "compact (flat_lub x) (flat_ord x) y"
    1.33 +using flat_interpretation[THEN ccpo]
    1.34 +proof(rule ccpo.compactI[OF _ ccpo.admissibleI])
    1.35 +  fix A
    1.36 +  assume chain: "Complete_Partial_Order.chain (flat_ord x) A"
    1.37 +    and A: "A \<noteq> {}"
    1.38 +    and *: "\<forall>z\<in>A. \<not> flat_ord x y z"
    1.39 +  from A obtain z where "z \<in> A" by blast
    1.40 +  with * have z: "\<not> flat_ord x y z" ..
    1.41 +  hence y: "x \<noteq> y" "y \<noteq> z" by(auto simp add: flat_ord_def)
    1.42 +  { assume "\<not> A \<subseteq> {x}"
    1.43 +    then obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
    1.44 +    then have "(THE z. z \<in> A - {x}) = z'"
    1.45 +      by(intro the_equality)(auto dest: chainD[OF chain] simp add: flat_ord_def)
    1.46 +    moreover have "z' \<noteq> y" using \<open>z' \<in> A\<close> * by(auto simp add: flat_ord_def)
    1.47 +    ultimately have "y \<noteq> (THE z. z \<in> A - {x})" by simp }
    1.48 +  with z show "\<not> flat_ord x y (flat_lub x A)" by(simp add: flat_ord_def flat_lub_def)
    1.49 +qed
    1.50 +
    1.51  end
     2.1 --- a/src/HOL/Probability/Probability.thy	Mon Jun 06 22:22:05 2016 +0200
     2.2 +++ b/src/HOL/Probability/Probability.thy	Wed Jun 08 09:05:32 2016 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4    Complete_Measure
     2.5    Projective_Limit
     2.6    Probability_Mass_Function
     2.7 +  SPMF
     2.8    PMF_Impl
     2.9    Stream_Space
    2.10    Random_Permutations
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Probability/SPMF.thy	Wed Jun 08 09:05:32 2016 +0200
     3.3 @@ -0,0 +1,2726 @@
     3.4 +(* Author: Andreas Lochbihler, ETH Zurich *)
     3.5 +
     3.6 +section \<open>Discrete subprobability distribution\<close>
     3.7 +
     3.8 +theory SPMF imports
     3.9 +  Probability_Mass_Function
    3.10 +  Embed_Measure
    3.11 +  "~~/src/HOL/Library/Complete_Partial_Order2"
    3.12 +  "~~/src/HOL/Library/Rewrite"
    3.13 +begin
    3.14 +
    3.15 +subsection \<open>Auxiliary material\<close>
    3.16 +
    3.17 +lemma cSUP_singleton [simp]: "(SUP x:{x}. f x :: _ :: conditionally_complete_lattice) = f x"
    3.18 +by (metis cSup_singleton image_empty image_insert)
    3.19 +
    3.20 +subsubsection \<open>More about extended reals\<close>
    3.21 +
    3.22 +lemma [simp]:
    3.23 +  shows ennreal_max_0: "ennreal (max 0 x) = ennreal x"
    3.24 +  and ennreal_max_0': "ennreal (max x 0) = ennreal x"
    3.25 +by(simp_all add: max_def ennreal_eq_0_iff)
    3.26 +
    3.27 +lemma ennreal_enn2real_if: "ennreal (enn2real r) = (if r = \<top> then 0 else r)"
    3.28 +by(auto intro!: ennreal_enn2real simp add: less_top)
    3.29 +
    3.30 +lemma e2ennreal_0 [simp]: "e2ennreal 0 = 0"
    3.31 +by(simp add: zero_ennreal_def)
    3.32 +
    3.33 +lemma enn2real_bot [simp]: "enn2real \<bottom> = 0"
    3.34 +by(simp add: bot_ennreal_def)
    3.35 +
    3.36 +lemma continuous_at_ennreal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ennreal (f x))"
    3.37 +  unfolding continuous_def by auto
    3.38 +
    3.39 +lemma ennreal_Sup:
    3.40 +  assumes *: "(SUP a:A. ennreal a) \<noteq> \<top>"
    3.41 +  and "A \<noteq> {}"
    3.42 +  shows "ennreal (Sup A) = (SUP a:A. ennreal a)"
    3.43 +proof (rule continuous_at_Sup_mono)
    3.44 +  obtain r where r: "ennreal r = (SUP a:A. ennreal a)" "r \<ge> 0"
    3.45 +    using * by(cases "(SUP a:A. ennreal a)") simp_all
    3.46 +  then show "bdd_above A"
    3.47 +    by(auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ennreal_le_iff[symmetric])
    3.48 +qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ennreal ennreal_leI assms)
    3.49 +
    3.50 +lemma ennreal_SUP:
    3.51 +  "\<lbrakk> (SUP a:A. ennreal (f a)) \<noteq> \<top>; A \<noteq> {} \<rbrakk> \<Longrightarrow> ennreal (SUP a:A. f a) = (SUP a:A. ennreal (f a))"
    3.52 +using ennreal_Sup[of "f ` A"] by auto
    3.53 +
    3.54 +lemma ennreal_lt_0: "x < 0 \<Longrightarrow> ennreal x = 0"
    3.55 +by(simp add: ennreal_eq_0_iff)
    3.56 +
    3.57 +subsubsection \<open>More about @{typ "'a option"}\<close>
    3.58 +
    3.59 +lemma None_in_map_option_image [simp]: "None \<in> map_option f ` A \<longleftrightarrow> None \<in> A"
    3.60 +by auto
    3.61 +
    3.62 +lemma Some_in_map_option_image [simp]: "Some x \<in> map_option f ` A \<longleftrightarrow> (\<exists>y. x = f y \<and> Some y \<in> A)"
    3.63 +by(auto intro: rev_image_eqI dest: sym)
    3.64 +
    3.65 +lemma case_option_collapse: "case_option x (\<lambda>_. x) = (\<lambda>_. x)"
    3.66 +by(simp add: fun_eq_iff split: option.split)
    3.67 +
    3.68 +lemma case_option_id: "case_option None Some = id"
    3.69 +by(rule ext)(simp split: option.split)
    3.70 +
    3.71 +inductive ord_option :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
    3.72 +  for ord :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
    3.73 +where
    3.74 +  None: "ord_option ord None x"
    3.75 +| Some: "ord x y \<Longrightarrow> ord_option ord (Some x) (Some y)"
    3.76 +
    3.77 +inductive_simps ord_option_simps [simp]:
    3.78 +  "ord_option ord None x"
    3.79 +  "ord_option ord x None"
    3.80 +  "ord_option ord (Some x) (Some y)"
    3.81 +  "ord_option ord (Some x) None"
    3.82 +
    3.83 +inductive_simps ord_option_eq_simps [simp]:
    3.84 +  "ord_option op = None y"
    3.85 +  "ord_option op = (Some x) y"
    3.86 +
    3.87 +lemma ord_option_reflI: "(\<And>y. y \<in> set_option x \<Longrightarrow> ord y y) \<Longrightarrow> ord_option ord x x"
    3.88 +by(cases x) simp_all
    3.89 +
    3.90 +lemma reflp_ord_option: "reflp ord \<Longrightarrow> reflp (ord_option ord)"
    3.91 +by(simp add: reflp_def ord_option_reflI)
    3.92 +
    3.93 +lemma ord_option_trans:
    3.94 +  "\<lbrakk> ord_option ord x y; ord_option ord y z;
    3.95 +    \<And>a b c. \<lbrakk> a \<in> set_option x; b \<in> set_option y; c \<in> set_option z; ord a b; ord b c \<rbrakk> \<Longrightarrow> ord a c \<rbrakk>
    3.96 +  \<Longrightarrow> ord_option ord x z"
    3.97 +by(auto elim!: ord_option.cases)
    3.98 +
    3.99 +lemma transp_ord_option: "transp ord \<Longrightarrow> transp (ord_option ord)"
   3.100 +unfolding transp_def by(blast intro: ord_option_trans)
   3.101 +
   3.102 +lemma antisymP_ord_option: "antisymP ord \<Longrightarrow> antisymP (ord_option ord)"
   3.103 +by(auto intro!: antisymI elim!: ord_option.cases dest: antisymD)
   3.104 +
   3.105 +lemma ord_option_chainD:
   3.106 +  "Complete_Partial_Order.chain (ord_option ord) Y
   3.107 +  \<Longrightarrow> Complete_Partial_Order.chain ord {x. Some x \<in> Y}"
   3.108 +by(rule chainI)(auto dest: chainD)
   3.109 +
   3.110 +definition lub_option :: "('a set \<Rightarrow> 'b) \<Rightarrow> 'a option set \<Rightarrow> 'b option"
   3.111 +where "lub_option lub Y = (if Y \<subseteq> {None} then None else Some (lub {x. Some x \<in> Y}))"
   3.112 +
   3.113 +lemma map_lub_option: "map_option f (lub_option lub Y) = lub_option (f \<circ> lub) Y"
   3.114 +by(simp add: lub_option_def)
   3.115 +
   3.116 +lemma lub_option_upper:
   3.117 +  assumes "Complete_Partial_Order.chain (ord_option ord) Y" "x \<in> Y"
   3.118 +  and lub_upper: "\<And>Y x. \<lbrakk> Complete_Partial_Order.chain ord Y; x \<in> Y \<rbrakk> \<Longrightarrow> ord x (lub Y)"
   3.119 +  shows "ord_option ord x (lub_option lub Y)"
   3.120 +using assms(1-2)
   3.121 +by(cases x)(auto simp add: lub_option_def intro: lub_upper[OF ord_option_chainD])
   3.122 +
   3.123 +lemma lub_option_least:
   3.124 +  assumes Y: "Complete_Partial_Order.chain (ord_option ord) Y"
   3.125 +  and upper: "\<And>x. x \<in> Y \<Longrightarrow> ord_option ord x y"
   3.126 +  assumes lub_least: "\<And>Y y. \<lbrakk> Complete_Partial_Order.chain ord Y; \<And>x. x \<in> Y \<Longrightarrow> ord x y \<rbrakk> \<Longrightarrow> ord (lub Y) y"
   3.127 +  shows "ord_option ord (lub_option lub Y) y"
   3.128 +using Y
   3.129 +by(cases y)(auto 4 3 simp add: lub_option_def intro: lub_least[OF ord_option_chainD] dest: upper)
   3.130 +
   3.131 +lemma lub_map_option: "lub_option lub (map_option f ` Y) = lub_option (lub \<circ> op ` f) Y"
   3.132 +apply(auto simp add: lub_option_def)
   3.133 +apply(erule notE)
   3.134 +apply(rule arg_cong[where f=lub])
   3.135 +apply(auto intro: rev_image_eqI dest: sym)
   3.136 +done
   3.137 +
   3.138 +lemma ord_option_mono: "\<lbrakk> ord_option A x y; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> ord_option B x y"
   3.139 +by(auto elim: ord_option.cases)
   3.140 +
   3.141 +lemma ord_option_mono' [mono]:
   3.142 +  "(\<And>x y. A x y \<longrightarrow> B x y) \<Longrightarrow> ord_option A x y \<longrightarrow> ord_option B x y"
   3.143 +by(blast intro: ord_option_mono)
   3.144 +
   3.145 +lemma ord_option_compp: "ord_option (A OO B) = ord_option A OO ord_option B"
   3.146 +by(auto simp add: fun_eq_iff elim!: ord_option.cases intro: ord_option.intros)
   3.147 +
   3.148 +lemma ord_option_inf: "inf (ord_option A) (ord_option B) = ord_option (inf A B)" (is "?lhs = ?rhs")
   3.149 +proof(rule antisym)
   3.150 +  show "?lhs \<le> ?rhs" by(auto elim!: ord_option.cases)
   3.151 +qed(auto elim: ord_option_mono)
   3.152 +
   3.153 +lemma ord_option_map2: "ord_option ord x (map_option f y) = ord_option (\<lambda>x y. ord x (f y)) x y"
   3.154 +by(auto elim: ord_option.cases)
   3.155 +
   3.156 +lemma ord_option_map1: "ord_option ord (map_option f x) y = ord_option (\<lambda>x y. ord (f x) y) x y"
   3.157 +by(auto elim: ord_option.cases)
   3.158 +
   3.159 +lemma option_ord_Some1_iff: "option_ord (Some x) y \<longleftrightarrow> y = Some x"
   3.160 +by(auto simp add: flat_ord_def)
   3.161 +
   3.162 +subsubsection \<open>A relator for sets that treats sets like predicates\<close>
   3.163 +
   3.164 +context begin interpretation lifting_syntax .
   3.165 +definition rel_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
   3.166 +where "rel_pred R A B = (R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
   3.167 +
   3.168 +lemma rel_predI: "(R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B) \<Longrightarrow> rel_pred R A B"
   3.169 +by(simp add: rel_pred_def)
   3.170 +
   3.171 +lemma rel_predD: "\<lbrakk> rel_pred R A B; R x y \<rbrakk> \<Longrightarrow> x \<in> A \<longleftrightarrow> y \<in> B"
   3.172 +by(simp add: rel_pred_def rel_fun_def)
   3.173 +
   3.174 +lemma Collect_parametric: "((A ===> op =) ===> rel_pred A) Collect Collect"
   3.175 +  -- \<open>Declare this rule as @{attribute transfer_rule} only locally
   3.176 +      because it blows up the search space for @{method transfer}
   3.177 +      (in combination with @{thm [source] Collect_transfer})\<close>
   3.178 +by(simp add: rel_funI rel_predI)
   3.179 +end
   3.180 +
   3.181 +subsubsection \<open>Monotonicity rules\<close>
   3.182 +
   3.183 +lemma monotone_gfp_eadd1: "monotone op \<ge> op \<ge> (\<lambda>x. x + y :: enat)"
   3.184 +by(auto intro!: monotoneI)
   3.185 +
   3.186 +lemma monotone_gfp_eadd2: "monotone op \<ge> op \<ge> (\<lambda>y. x + y :: enat)"
   3.187 +by(auto intro!: monotoneI)
   3.188 +
   3.189 +lemma mono2mono_gfp_eadd[THEN gfp.mono2mono2, cont_intro, simp]:
   3.190 +  shows monotone_eadd: "monotone (rel_prod op \<ge> op \<ge>) op \<ge> (\<lambda>(x, y). x + y :: enat)"
   3.191 +by(simp add: monotone_gfp_eadd1 monotone_gfp_eadd2)
   3.192 +
   3.193 +lemma eadd_gfp_partial_function_mono [partial_function_mono]:
   3.194 +  "\<lbrakk> monotone (fun_ord op \<ge>) op \<ge> f; monotone (fun_ord op \<ge>) op \<ge> g \<rbrakk>
   3.195 +  \<Longrightarrow> monotone (fun_ord op \<ge>) op \<ge> (\<lambda>x. f x + g x :: enat)"
   3.196 +by(rule mono2mono_gfp_eadd)
   3.197 +
   3.198 +lemma mono2mono_ereal[THEN lfp.mono2mono]:
   3.199 +  shows monotone_ereal: "monotone op \<le> op \<le> ereal"
   3.200 +by(rule monotoneI) simp
   3.201 +
   3.202 +lemma mono2mono_ennreal[THEN lfp.mono2mono]:
   3.203 +  shows monotone_ennreal: "monotone op \<le> op \<le> ennreal"
   3.204 +by(rule monotoneI)(simp add: ennreal_leI)
   3.205 +
   3.206 +subsubsection \<open>Bijections\<close>
   3.207 +
   3.208 +lemma bi_unique_rel_set_bij_betw:
   3.209 +  assumes unique: "bi_unique R"
   3.210 +  and rel: "rel_set R A B"
   3.211 +  shows "\<exists>f. bij_betw f A B \<and> (\<forall>x\<in>A. R x (f x))"
   3.212 +proof -
   3.213 +  from assms obtain f where f: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)" and B: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B"
   3.214 +    apply(atomize_elim)
   3.215 +    apply(fold all_conj_distrib)
   3.216 +    apply(subst choice_iff[symmetric])
   3.217 +    apply(auto dest: rel_setD1)
   3.218 +    done
   3.219 +  have "inj_on f A" by(rule inj_onI)(auto dest!: f dest: bi_uniqueDl[OF unique])
   3.220 +  moreover have "f ` A = B" using rel
   3.221 +    by(auto 4 3 intro: B dest: rel_setD2 f bi_uniqueDr[OF unique])
   3.222 +  ultimately have "bij_betw f A B" unfolding bij_betw_def ..
   3.223 +  thus ?thesis using f by blast
   3.224 +qed
   3.225 +
   3.226 +lemma bij_betw_rel_setD: "bij_betw f A B \<Longrightarrow> rel_set (\<lambda>x y. y = f x) A B"
   3.227 +by(rule rel_setI)(auto dest: bij_betwE bij_betw_imp_surj_on[symmetric])
   3.228 +
   3.229 +subsection {* Subprobability mass function *}
   3.230 +
   3.231 +type_synonym 'a spmf = "'a option pmf"
   3.232 +translations (type) "'a spmf" \<leftharpoondown> (type) "'a option pmf"
   3.233 +
   3.234 +definition measure_spmf :: "'a spmf \<Rightarrow> 'a measure"
   3.235 +where "measure_spmf p = distr (restrict_space (measure_pmf p) (range Some)) (count_space UNIV) the"
   3.236 +
   3.237 +abbreviation spmf :: "'a spmf \<Rightarrow> 'a \<Rightarrow> real"
   3.238 +where "spmf p x \<equiv> pmf p (Some x)"
   3.239 +
   3.240 +lemma space_measure_spmf: "space (measure_spmf p) = UNIV"
   3.241 +by(simp add: measure_spmf_def)
   3.242 +
   3.243 +lemma sets_measure_spmf [simp, measurable_cong]: "sets (measure_spmf p) = sets (count_space UNIV)"
   3.244 +by(simp add: measure_spmf_def)
   3.245 +
   3.246 +lemma measure_spmf_not_bot [simp]: "measure_spmf p \<noteq> \<bottom>"
   3.247 +proof
   3.248 +  assume "measure_spmf p = \<bottom>"
   3.249 +  hence "space (measure_spmf p) = space \<bottom>" by simp
   3.250 +  thus False by(simp add: space_measure_spmf)
   3.251 +qed
   3.252 +
   3.253 +lemma measurable_the_measure_pmf_Some [measurable, simp]:
   3.254 +  "the \<in> measurable (restrict_space (measure_pmf p) (range Some)) (count_space UNIV)"
   3.255 +by(auto simp add: measurable_def sets_restrict_space space_restrict_space integral_restrict_space)
   3.256 +
   3.257 +lemma measurable_spmf_measure1[simp]: "measurable (measure_spmf M) N = UNIV \<rightarrow> space N"
   3.258 +by(auto simp: measurable_def space_measure_spmf)
   3.259 +
   3.260 +lemma measurable_spmf_measure2[simp]: "measurable N (measure_spmf M) = measurable N (count_space UNIV)"
   3.261 +by(intro measurable_cong_sets) simp_all
   3.262 +
   3.263 +lemma subprob_space_measure_spmf [simp, intro!]: "subprob_space (measure_spmf p)"
   3.264 +proof
   3.265 +  show "emeasure (measure_spmf p) (space (measure_spmf p)) \<le> 1"
   3.266 +    by(simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space measure_pmf.measure_le_1)
   3.267 +qed(simp add: space_measure_spmf)
   3.268 +
   3.269 +interpretation measure_spmf: subprob_space "measure_spmf p" for p
   3.270 +by(rule subprob_space_measure_spmf)
   3.271 +
   3.272 +lemma finite_measure_spmf [simp]: "finite_measure (measure_spmf p)"
   3.273 +by unfold_locales
   3.274 +
   3.275 +lemma spmf_conv_measure_spmf: "spmf p x = measure (measure_spmf p) {x}"
   3.276 +by(auto simp add: measure_spmf_def measure_distr measure_restrict_space pmf.rep_eq space_restrict_space intro: arg_cong2[where f=measure])
   3.277 +
   3.278 +lemma emeasure_measure_spmf_conv_measure_pmf:
   3.279 +  "emeasure (measure_spmf p) A = emeasure (measure_pmf p) (Some ` A)"
   3.280 +by(auto simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space intro: arg_cong2[where f=emeasure])
   3.281 +
   3.282 +lemma measure_measure_spmf_conv_measure_pmf:
   3.283 +  "measure (measure_spmf p) A = measure (measure_pmf p) (Some ` A)"
   3.284 +using emeasure_measure_spmf_conv_measure_pmf[of p A]
   3.285 +by(simp add: measure_spmf.emeasure_eq_measure measure_pmf.emeasure_eq_measure)
   3.286 +
   3.287 +lemma emeasure_spmf_map_pmf_Some [simp]:
   3.288 +  "emeasure (measure_spmf (map_pmf Some p)) A = emeasure (measure_pmf p) A"
   3.289 +by(auto simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space intro: arg_cong2[where f=emeasure])
   3.290 +
   3.291 +lemma measure_spmf_map_pmf_Some [simp]:
   3.292 +  "measure (measure_spmf (map_pmf Some p)) A = measure (measure_pmf p) A"
   3.293 +using emeasure_spmf_map_pmf_Some[of p A] by(simp add: measure_spmf.emeasure_eq_measure measure_pmf.emeasure_eq_measure)
   3.294 +
   3.295 +lemma nn_integral_measure_spmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_spmf p) = \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>count_space UNIV"
   3.296 +  (is "?lhs = ?rhs")
   3.297 +proof -
   3.298 +  have "?lhs = \<integral>\<^sup>+ x. pmf p x * f (the x) \<partial>count_space (range Some)"
   3.299 +    by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space nn_integral_measure_pmf nn_integral_count_space_indicator ac_simps times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
   3.300 +  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (spmf p (the x)) * f (the x) \<partial>count_space (range Some)"
   3.301 +    by(rule nn_integral_cong) auto
   3.302 +  also have "\<dots> = \<integral>\<^sup>+ x. spmf p (the (Some x)) * f (the (Some x)) \<partial>count_space UNIV"
   3.303 +    by(rule nn_integral_bij_count_space[symmetric])(simp add: bij_betw_def)
   3.304 +  also have "\<dots> = ?rhs" by simp
   3.305 +  finally show ?thesis .
   3.306 +qed
   3.307 +
   3.308 +lemma integral_measure_spmf: 
   3.309 +  assumes "integrable (measure_spmf p) f"
   3.310 +  shows "(\<integral> x. f x \<partial>measure_spmf p) = \<integral> x. spmf p x * f x \<partial>count_space UNIV"
   3.311 +proof -
   3.312 +  have "integrable (count_space UNIV) (\<lambda>x. spmf p x * f x)"
   3.313 +    using assms by(simp add: integrable_iff_bounded nn_integral_measure_spmf abs_mult ennreal_mult'')
   3.314 +  then show ?thesis using assms
   3.315 +    by(simp add: real_lebesgue_integral_def nn_integral_measure_spmf ennreal_mult'[symmetric])
   3.316 +qed
   3.317 +
   3.318 +lemma emeasure_spmf_single: "emeasure (measure_spmf p) {x} = spmf p x"
   3.319 +by(simp add: measure_spmf.emeasure_eq_measure spmf_conv_measure_spmf)
   3.320 +
   3.321 +lemma measurable_measure_spmf[measurable]:
   3.322 +  "(\<lambda>x. measure_spmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
   3.323 +by (auto simp: space_subprob_algebra)
   3.324 +
   3.325 +lemma nn_integral_measure_spmf_conv_measure_pmf:
   3.326 +  assumes [measurable]: "f \<in> borel_measurable (count_space UNIV)"
   3.327 +  shows "nn_integral (measure_spmf p) f = nn_integral (restrict_space (measure_pmf p) (range Some)) (f \<circ> the)"
   3.328 +by(simp add: measure_spmf_def nn_integral_distr o_def)
   3.329 +
   3.330 +lemma measure_spmf_in_space_subprob_algebra [simp]:
   3.331 +  "measure_spmf p \<in> space (subprob_algebra (count_space UNIV))"
   3.332 +by(simp add: space_subprob_algebra)
   3.333 +
   3.334 +lemma nn_integral_spmf_neq_top: "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV) \<noteq> \<top>"
   3.335 +using nn_integral_measure_spmf[where f="\<lambda>_. 1", of p, symmetric] by simp
   3.336 +
   3.337 +lemma SUP_spmf_neq_top': "(SUP p:Y. ennreal (spmf p x)) \<noteq> \<top>"
   3.338 +proof(rule neq_top_trans)
   3.339 +  show "(SUP p:Y. ennreal (spmf p x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
   3.340 +qed simp
   3.341 +
   3.342 +lemma SUP_spmf_neq_top: "(SUP i. ennreal (spmf (Y i) x)) \<noteq> \<top>"
   3.343 +proof(rule neq_top_trans)
   3.344 +  show "(SUP i. ennreal (spmf (Y i) x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
   3.345 +qed simp
   3.346 +                 
   3.347 +lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
   3.348 +proof(rule neq_top_trans)
   3.349 +  show "(SUP p:Y. emeasure (measure_spmf p) A) \<le> 1"
   3.350 +    by(rule SUP_least)(simp add: measure_spmf.subprob_emeasure_le_1)
   3.351 +qed simp
   3.352 +
   3.353 +subsection {* Support *}
   3.354 +
   3.355 +definition set_spmf :: "'a spmf \<Rightarrow> 'a set"
   3.356 +where "set_spmf p = set_pmf p \<bind> set_option"
   3.357 +
   3.358 +lemma set_spmf_rep_eq: "set_spmf p = {x. measure (measure_spmf p) {x} \<noteq> 0}"
   3.359 +proof -
   3.360 +  have "\<And>x :: 'a. the -` {x} \<inter> range Some = {Some x}" by auto
   3.361 +  then show ?thesis
   3.362 +    by(auto simp add: set_spmf_def set_pmf.rep_eq measure_spmf_def measure_distr measure_restrict_space space_restrict_space intro: rev_image_eqI)
   3.363 +qed
   3.364 +
   3.365 +lemma in_set_spmf: "x \<in> set_spmf p \<longleftrightarrow> Some x \<in> set_pmf p"
   3.366 +by(simp add: set_spmf_def)
   3.367 +
   3.368 +lemma AE_measure_spmf_iff [simp]: "(AE x in measure_spmf p. P x) \<longleftrightarrow> (\<forall>x\<in>set_spmf p. P x)"
   3.369 +by(auto 4 3 simp add: measure_spmf_def AE_distr_iff AE_restrict_space_iff AE_measure_pmf_iff set_spmf_def cong del: AE_cong)
   3.370 +
   3.371 +lemma spmf_eq_0_set_spmf: "spmf p x = 0 \<longleftrightarrow> x \<notin> set_spmf p"
   3.372 +by(auto simp add: pmf_eq_0_set_pmf set_spmf_def intro: rev_image_eqI)
   3.373 +
   3.374 +lemma in_set_spmf_iff_spmf: "x \<in> set_spmf p \<longleftrightarrow> spmf p x \<noteq> 0"
   3.375 +by(auto simp add: set_spmf_def set_pmf_iff intro: rev_image_eqI)
   3.376 +
   3.377 +lemma set_spmf_return_pmf_None [simp]: "set_spmf (return_pmf None) = {}"
   3.378 +by(auto simp add: set_spmf_def)
   3.379 +
   3.380 +lemma countable_set_spmf [simp]: "countable (set_spmf p)"
   3.381 +by(simp add: set_spmf_def bind_UNION)
   3.382 +
   3.383 +lemma spmf_eqI:
   3.384 +  assumes "\<And>i. spmf p i = spmf q i"
   3.385 +  shows "p = q"
   3.386 +proof(rule pmf_eqI)
   3.387 +  fix i
   3.388 +  show "pmf p i = pmf q i"
   3.389 +  proof(cases i)
   3.390 +    case (Some i')
   3.391 +    thus ?thesis by(simp add: assms)
   3.392 +  next
   3.393 +    case None
   3.394 +    have "ennreal (pmf p i) = measure (measure_pmf p) {i}" by(simp add: pmf_def)
   3.395 +    also have "{i} = space (measure_pmf p) - range Some"
   3.396 +      by(auto simp add: None intro: ccontr)
   3.397 +    also have "measure (measure_pmf p) \<dots> = ennreal 1 - measure (measure_pmf p) (range Some)"
   3.398 +      by(simp add: measure_pmf.prob_compl ennreal_minus[symmetric] del: space_measure_pmf)
   3.399 +    also have "range Some = (\<Union>x\<in>set_spmf p. {Some x}) \<union> Some ` (- set_spmf p)"
   3.400 +      by auto
   3.401 +    also have "measure (measure_pmf p) \<dots> = measure (measure_pmf p) (\<Union>x\<in>set_spmf p. {Some x})"
   3.402 +      by(rule measure_pmf.measure_zero_union)(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff in_set_spmf_iff_spmf set_pmf_iff)
   3.403 +    also have "ennreal \<dots> = \<integral>\<^sup>+ x. measure (measure_pmf p) {Some x} \<partial>count_space (set_spmf p)"
   3.404 +      unfolding measure_pmf.emeasure_eq_measure[symmetric]
   3.405 +      by(simp_all add: emeasure_UN_countable disjoint_family_on_def)
   3.406 +    also have "\<dots> = \<integral>\<^sup>+ x. spmf p x \<partial>count_space (set_spmf p)" by(simp add: pmf_def)
   3.407 +    also have "\<dots> = \<integral>\<^sup>+ x. spmf q x \<partial>count_space (set_spmf p)" by(simp add: assms)
   3.408 +    also have "set_spmf p = set_spmf q" by(auto simp add: in_set_spmf_iff_spmf assms)
   3.409 +    also have "(\<integral>\<^sup>+ x. spmf q x \<partial>count_space (set_spmf q)) = \<integral>\<^sup>+ x. measure (measure_pmf q) {Some x} \<partial>count_space (set_spmf q)"
   3.410 +      by(simp add: pmf_def)
   3.411 +    also have "\<dots> = measure (measure_pmf q) (\<Union>x\<in>set_spmf q. {Some x})"
   3.412 +      unfolding measure_pmf.emeasure_eq_measure[symmetric]
   3.413 +      by(simp_all add: emeasure_UN_countable disjoint_family_on_def)
   3.414 +    also have "\<dots> = measure (measure_pmf q) ((\<Union>x\<in>set_spmf q. {Some x}) \<union> Some ` (- set_spmf q))"
   3.415 +      by(rule ennreal_cong measure_pmf.measure_zero_union[symmetric])+(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff in_set_spmf_iff_spmf set_pmf_iff)
   3.416 +    also have "((\<Union>x\<in>set_spmf q. {Some x}) \<union> Some ` (- set_spmf q)) = range Some" by auto
   3.417 +    also have "ennreal 1 - measure (measure_pmf q) \<dots> = measure (measure_pmf q) (space (measure_pmf q) - range Some)"
   3.418 +      by(simp add: one_ereal_def measure_pmf.prob_compl ennreal_minus[symmetric] del: space_measure_pmf)
   3.419 +    also have "space (measure_pmf q) - range Some = {i}"
   3.420 +      by(auto simp add: None intro: ccontr)
   3.421 +    also have "measure (measure_pmf q) \<dots> = pmf q i" by(simp add: pmf_def)
   3.422 +    finally show ?thesis by simp
   3.423 +  qed
   3.424 +qed
   3.425 +
   3.426 +lemma integral_measure_spmf_restrict:
   3.427 +  fixes f ::  "'a \<Rightarrow> 'b :: {banach, second_countable_topology}" shows
   3.428 +  "(\<integral> x. f x \<partial>measure_spmf M) = (\<integral> x. f x \<partial>restrict_space (measure_spmf M) (set_spmf M))"
   3.429 +by(auto intro!: integral_cong_AE simp add: integral_restrict_space)
   3.430 +
   3.431 +lemma nn_integral_measure_spmf':
   3.432 +  "(\<integral>\<^sup>+ x. f x \<partial>measure_spmf p) = \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>count_space (set_spmf p)"
   3.433 +by(auto simp add: nn_integral_measure_spmf nn_integral_count_space_indicator in_set_spmf_iff_spmf intro!: nn_integral_cong split: split_indicator)
   3.434 +
   3.435 +subsection {* Functorial structure *}
   3.436 +
   3.437 +abbreviation map_spmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf"
   3.438 +where "map_spmf f \<equiv> map_pmf (map_option f)"
   3.439 +
   3.440 +context begin
   3.441 +local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "spmf") *}
   3.442 +
   3.443 +lemma map_comp: "map_spmf f (map_spmf g p) = map_spmf (f \<circ> g) p"
   3.444 +by(simp add: pmf.map_comp o_def option.map_comp)
   3.445 +
   3.446 +lemma map_id0: "map_spmf id = id"
   3.447 +by(simp add: pmf.map_id option.map_id0)
   3.448 +
   3.449 +lemma map_id [simp]: "map_spmf id p = p"
   3.450 +by(simp add: map_id0)
   3.451 +
   3.452 +lemma map_ident [simp]: "map_spmf (\<lambda>x. x) p = p"
   3.453 +by(simp add: id_def[symmetric])
   3.454 +
   3.455 +end
   3.456 +
   3.457 +lemma set_map_spmf [simp]: "set_spmf (map_spmf f p) = f ` set_spmf p"
   3.458 +by(simp add: set_spmf_def image_bind bind_image o_def Option.option.set_map)
   3.459 +        
   3.460 +lemma map_spmf_cong:
   3.461 +  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q \<Longrightarrow> f x = g x \<rbrakk>
   3.462 +  \<Longrightarrow> map_spmf f p = map_spmf g q"
   3.463 +by(auto intro: pmf.map_cong option.map_cong simp add: in_set_spmf)
   3.464 +
   3.465 +lemma map_spmf_cong_simp:
   3.466 +  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q =simp=> f x = g x \<rbrakk>
   3.467 +  \<Longrightarrow> map_spmf f p = map_spmf g q"
   3.468 +unfolding simp_implies_def by(rule map_spmf_cong)
   3.469 +
   3.470 +lemma map_spmf_idI: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_spmf f p = p"
   3.471 +by(rule map_pmf_idI map_option_idI)+(simp add: in_set_spmf)
   3.472 +
   3.473 +lemma emeasure_map_spmf:
   3.474 +  "emeasure (measure_spmf (map_spmf f p)) A = emeasure (measure_spmf p) (f -` A)"
   3.475 +by(auto simp add: measure_spmf_def emeasure_distr measurable_restrict_space1 space_restrict_space emeasure_restrict_space intro: arg_cong2[where f=emeasure])
   3.476 +
   3.477 +lemma measure_map_spmf: "measure (measure_spmf (map_spmf f p)) A = measure (measure_spmf p) (f -` A)"
   3.478 +using emeasure_map_spmf[of f p A] by(simp add: measure_spmf.emeasure_eq_measure)
   3.479 +
   3.480 +lemma measure_map_spmf_conv_distr:
   3.481 +  "measure_spmf (map_spmf f p) = distr (measure_spmf p) (count_space UNIV) f"
   3.482 +by(rule measure_eqI)(simp_all add: emeasure_map_spmf emeasure_distr)
   3.483 +
   3.484 +lemma spmf_map_pmf_Some [simp]: "spmf (map_pmf Some p) i = pmf p i"
   3.485 +by(simp add: pmf_map_inj')
   3.486 +
   3.487 +lemma spmf_map_inj: "\<lbrakk> inj_on f (set_spmf M); x \<in> set_spmf M \<rbrakk> \<Longrightarrow> spmf (map_spmf f M) (f x) = spmf M x"
   3.488 +by(subst option.map(2)[symmetric, where f=f])(rule pmf_map_inj, auto simp add: in_set_spmf inj_on_def elim!: option.inj_map_strong[rotated])
   3.489 +
   3.490 +lemma spmf_map_inj': "inj f \<Longrightarrow> spmf (map_spmf f M) (f x) = spmf M x"
   3.491 +by(subst option.map(2)[symmetric, where f=f])(rule pmf_map_inj'[OF option.inj_map])
   3.492 +
   3.493 +lemma spmf_map_outside: "x \<notin> f ` set_spmf M \<Longrightarrow> spmf (map_spmf f M) x = 0"
   3.494 +unfolding spmf_eq_0_set_spmf by simp
   3.495 +
   3.496 +lemma ennreal_spmf_map: "ennreal (spmf (map_spmf f p) x) = emeasure (measure_spmf p) (f -` {x})"
   3.497 +by(auto simp add: ennreal_pmf_map measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space intro: arg_cong2[where f=emeasure])
   3.498 +
   3.499 +lemma spmf_map: "spmf (map_spmf f p) x = measure (measure_spmf p) (f -` {x})"
   3.500 +using ennreal_spmf_map[of f p x] by(simp add: measure_spmf.emeasure_eq_measure)
   3.501 +
   3.502 +lemma ennreal_spmf_map_conv_nn_integral:
   3.503 +  "ennreal (spmf (map_spmf f p) x) = integral\<^sup>N (measure_spmf p) (indicator (f -` {x}))"
   3.504 +by(auto simp add: ennreal_pmf_map measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space intro: arg_cong2[where f=emeasure])
   3.505 +
   3.506 +subsection {* Monad operations *}
   3.507 +
   3.508 +subsubsection {* Return *}
   3.509 +
   3.510 +abbreviation return_spmf :: "'a \<Rightarrow> 'a spmf"
   3.511 +where "return_spmf x \<equiv> return_pmf (Some x)"
   3.512 +
   3.513 +lemma pmf_return_spmf: "pmf (return_spmf x) y = indicator {y} (Some x)"
   3.514 +by(fact pmf_return)
   3.515 +
   3.516 +lemma measure_spmf_return_spmf: "measure_spmf (return_spmf x) = Giry_Monad.return (count_space UNIV) x"
   3.517 +by(rule measure_eqI)(simp_all add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space indicator_def)
   3.518 +
   3.519 +lemma measure_spmf_return_pmf_None [simp]: "measure_spmf (return_pmf None) = null_measure (count_space UNIV)"
   3.520 +by(rule measure_eqI)(auto simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space indicator_eq_0_iff)
   3.521 +
   3.522 +lemma set_return_spmf [simp]: "set_spmf (return_spmf x) = {x}"
   3.523 +by(auto simp add: set_spmf_def)
   3.524 +
   3.525 +subsubsection {* Bind *}
   3.526 +
   3.527 +definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
   3.528 +where "bind_spmf x f = bind_pmf x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
   3.529 +
   3.530 +adhoc_overloading Monad_Syntax.bind bind_spmf
   3.531 +
   3.532 +lemma return_None_bind_spmf [simp]: "return_pmf None \<bind> (f :: 'a \<Rightarrow> _) = return_pmf None"
   3.533 +by(simp add: bind_spmf_def bind_return_pmf)
   3.534 +
   3.535 +lemma return_bind_spmf [simp]: "return_spmf x \<bind> f = f x"
   3.536 +by(simp add: bind_spmf_def bind_return_pmf)
   3.537 +
   3.538 +lemma bind_return_spmf [simp]: "x \<bind> return_spmf = x"
   3.539 +proof -
   3.540 +  have "\<And>a :: 'a option. (case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> return_spmf a') = return_pmf a"
   3.541 +    by(simp split: option.split)
   3.542 +  then show ?thesis
   3.543 +    by(simp add: bind_spmf_def bind_return_pmf')
   3.544 +qed
   3.545 +
   3.546 +lemma bind_spmf_assoc [simp]:
   3.547 +  fixes x :: "'a spmf" and f :: "'a \<Rightarrow> 'b spmf" and g :: "'b \<Rightarrow> 'c spmf"
   3.548 +  shows "(x \<bind> f) \<bind> g = x \<bind> (\<lambda>y. f y \<bind> g)"
   3.549 +by(auto simp add: bind_spmf_def bind_assoc_pmf fun_eq_iff bind_return_pmf split: option.split intro: arg_cong[where f="bind_pmf x"])
   3.550 +
   3.551 +lemma pmf_bind_spmf_None: "pmf (p \<bind> f) None = pmf p None + \<integral> x. pmf (f x) None \<partial>measure_spmf p"
   3.552 +  (is "?lhs = ?rhs")
   3.553 +proof -
   3.554 +  let ?f = "\<lambda>x. pmf (case x of None \<Rightarrow> return_pmf None | Some x \<Rightarrow> f x) None"
   3.555 +  have "?lhs = \<integral> x. ?f x \<partial>measure_pmf p"
   3.556 +    by(simp add: bind_spmf_def pmf_bind)
   3.557 +  also have "\<dots> = \<integral> x. ?f None * indicator {None} x + ?f x * indicator (range Some) x \<partial>measure_pmf p"
   3.558 +    by(rule integral_cong)(auto simp add: indicator_def)
   3.559 +  also have "\<dots> = (\<integral> x. ?f None * indicator {None} x \<partial>measure_pmf p) + (\<integral> x. ?f x * indicator (range Some) x \<partial>measure_pmf p)"
   3.560 +    by(rule 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)
   3.561 +  also have "\<dots> = pmf p None + \<integral> x. indicator (range Some) x * pmf (f (the x)) None \<partial>measure_pmf p"
   3.562 +    by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: integral_cong)
   3.563 +  also have "\<dots> = ?rhs" unfolding measure_spmf_def
   3.564 +    by(subst integral_distr)(auto simp add: integral_restrict_space)
   3.565 +  finally show ?thesis .
   3.566 +qed
   3.567 +
   3.568 +lemma spmf_bind: "spmf (p \<bind> f) y = \<integral> x. spmf (f x) y \<partial>measure_spmf p"
   3.569 +unfolding measure_spmf_def
   3.570 +by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: integral_cong split: option.split)
   3.571 +
   3.572 +lemma ennreal_spmf_bind: "ennreal (spmf (p \<bind> f) x) = \<integral>\<^sup>+ y. spmf (f y) x \<partial>measure_spmf p"
   3.573 +by(auto simp add: bind_spmf_def ennreal_pmf_bind nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space intro: nn_integral_cong split: split_indicator option.split)
   3.574 +
   3.575 +lemma measure_spmf_bind_pmf: "measure_spmf (p \<bind> f) = measure_pmf p \<bind> measure_spmf \<circ> f"
   3.576 +  (is "?lhs = ?rhs")
   3.577 +proof(rule measure_eqI)
   3.578 +  show "sets ?lhs = sets ?rhs"
   3.579 +    by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf)
   3.580 +next
   3.581 +  fix A :: "'a set"
   3.582 +  have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_pmf p" 
   3.583 +    by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
   3.584 +  also have "\<dots> = emeasure ?rhs A"
   3.585 +    by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
   3.586 +  finally show "emeasure ?lhs A = emeasure ?rhs A" .
   3.587 +qed
   3.588 +
   3.589 +lemma measure_spmf_bind: "measure_spmf (p \<bind> f) = measure_spmf p \<bind> measure_spmf \<circ> f"
   3.590 +  (is "?lhs = ?rhs")
   3.591 +proof(rule measure_eqI)
   3.592 +  show "sets ?lhs = sets ?rhs"
   3.593 +    by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf)
   3.594 +next
   3.595 +  fix A :: "'a set"
   3.596 +  let ?A = "the -` A \<inter> range Some"
   3.597 +  have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_pmf (case x of None \<Rightarrow> return_pmf None | Some x \<Rightarrow> f x)) ?A \<partial>measure_pmf p" 
   3.598 +    by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
   3.599 +  also have "\<dots> =  \<integral>\<^sup>+ x. emeasure (measure_pmf (f (the x))) ?A * indicator (range Some) x \<partial>measure_pmf p"
   3.600 +    by(rule nn_integral_cong)(auto split: option.split simp add: indicator_def)
   3.601 +  also have "\<dots> = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_spmf p"
   3.602 +    by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space emeasure_distr space_restrict_space emeasure_restrict_space)
   3.603 +  also have "\<dots> = emeasure ?rhs A" 
   3.604 +    by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
   3.605 +  finally show "emeasure ?lhs A = emeasure ?rhs A" .
   3.606 +qed
   3.607 +
   3.608 +lemma map_spmf_bind_spmf: "map_spmf f (bind_spmf p g) = bind_spmf p (map_spmf f \<circ> g)"
   3.609 +by(auto simp add: bind_spmf_def map_bind_pmf fun_eq_iff split: option.split intro: arg_cong2[where f=bind_pmf])
   3.610 +
   3.611 +lemma bind_map_spmf: "map_spmf f p \<bind> g = p \<bind> g \<circ> f"
   3.612 +by(simp add: bind_spmf_def bind_map_pmf o_def cong del: option.case_cong_weak)
   3.613 +
   3.614 +lemma spmf_bind_leI:
   3.615 +  assumes "\<And>y. y \<in> set_spmf p \<Longrightarrow> spmf (f y) x \<le> r"
   3.616 +  and "0 \<le> r"
   3.617 +  shows "spmf (bind_spmf p f) x \<le> r"
   3.618 +proof -
   3.619 +  have "ennreal (spmf (bind_spmf p f) x) = \<integral>\<^sup>+ y. spmf (f y) x \<partial>measure_spmf p" by(rule ennreal_spmf_bind)
   3.620 +  also have "\<dots> \<le> \<integral>\<^sup>+ y. r \<partial>measure_spmf p" by(rule nn_integral_mono_AE)(simp add: assms)
   3.621 +  also have "\<dots> \<le> r" using assms measure_spmf.emeasure_space_le_1
   3.622 +    by(auto simp add: measure_spmf.emeasure_eq_measure intro!: mult_left_le)
   3.623 +  finally show ?thesis using assms(2) by(simp)
   3.624 +qed
   3.625 +
   3.626 +lemma map_spmf_conv_bind_spmf: "map_spmf f p = (p \<bind> (\<lambda>x. return_spmf (f x)))"
   3.627 +by(simp add: map_pmf_def bind_spmf_def)(rule bind_pmf_cong, simp_all split: option.split)
   3.628 +
   3.629 +lemma bind_spmf_cong:
   3.630 +  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q \<Longrightarrow> f x = g x \<rbrakk>
   3.631 +  \<Longrightarrow> bind_spmf p f = bind_spmf q g"
   3.632 +by(auto simp add: bind_spmf_def in_set_spmf intro: bind_pmf_cong option.case_cong)
   3.633 +
   3.634 +lemma bind_spmf_cong_simp:
   3.635 +  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q =simp=> f x = g x \<rbrakk>
   3.636 +  \<Longrightarrow> bind_spmf p f = bind_spmf q g"
   3.637 +by(simp add: simp_implies_def cong: bind_spmf_cong)
   3.638 +
   3.639 +lemma set_bind_spmf: "set_spmf (M \<bind> f) = set_spmf M \<bind> (set_spmf \<circ> f)"
   3.640 +by(auto simp add: set_spmf_def bind_spmf_def bind_UNION split: option.splits)
   3.641 +
   3.642 +lemma bind_spmf_const_return_None [simp]: "bind_spmf p (\<lambda>_. return_pmf None) = return_pmf None"
   3.643 +by(simp add: bind_spmf_def case_option_collapse)
   3.644 +
   3.645 +lemma bind_commute_spmf:
   3.646 +  "bind_spmf p (\<lambda>x. bind_spmf q (f x)) = bind_spmf q (\<lambda>y. bind_spmf p (\<lambda>x. f x y))"
   3.647 +  (is "?lhs = ?rhs")
   3.648 +proof -
   3.649 +  let ?f = "\<lambda>x y. case x of None \<Rightarrow> return_pmf None | Some a \<Rightarrow> (case y of None \<Rightarrow> return_pmf None | Some b \<Rightarrow> f a b)"
   3.650 +  have "?lhs = p \<bind> (\<lambda>x. q \<bind> ?f x)"
   3.651 +    unfolding bind_spmf_def by(rule bind_pmf_cong[OF refl])(simp split: option.split)
   3.652 +  also have "\<dots> = q \<bind> (\<lambda>y. p \<bind> (\<lambda>x. ?f x y))" by(rule bind_commute_pmf)
   3.653 +  also have "\<dots> = ?rhs" unfolding bind_spmf_def
   3.654 +    by(rule bind_pmf_cong[OF refl])(auto split: option.split, metis bind_spmf_const_return_None bind_spmf_def)
   3.655 +  finally show ?thesis .
   3.656 +qed
   3.657 +
   3.658 +subsection {* Relator *}
   3.659 +
   3.660 +abbreviation rel_spmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf \<Rightarrow> bool"
   3.661 +where "rel_spmf R \<equiv> rel_pmf (rel_option R)"
   3.662 +
   3.663 +lemma rel_pmf_mono:
   3.664 +  "\<lbrakk>rel_pmf A f g; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_pmf B f g"
   3.665 +using pmf.rel_mono[of A B] by(simp add: le_fun_def)
   3.666 +
   3.667 +lemma rel_spmf_mono:
   3.668 +  "\<lbrakk>rel_spmf A f g; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_spmf B f g"
   3.669 +apply(erule rel_pmf_mono) 
   3.670 +using option.rel_mono[of A B] by(simp add: le_fun_def)
   3.671 +
   3.672 +lemma rel_spmf_mono_strong:
   3.673 +  "\<lbrakk> rel_spmf A f g; \<And>x y. \<lbrakk> A x y; x \<in> set_spmf f; y \<in> set_spmf g \<rbrakk> \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_spmf B f g"
   3.674 +apply(erule pmf.rel_mono_strong)
   3.675 +apply(erule option.rel_mono_strong)
   3.676 +apply(auto simp add: in_set_spmf)
   3.677 +done
   3.678 +
   3.679 +lemma rel_spmf_reflI: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> P x x) \<Longrightarrow> rel_spmf P p p"
   3.680 +by(rule rel_pmf_reflI)(auto simp add: set_spmf_def intro: rel_option_reflI)
   3.681 +
   3.682 +lemma rel_spmfI [intro?]:
   3.683 +  "\<lbrakk> \<And>x y. (x, y) \<in> set_spmf pq \<Longrightarrow> P x y; map_spmf fst pq = p; map_spmf snd pq = q \<rbrakk>
   3.684 +  \<Longrightarrow> rel_spmf P p q"
   3.685 +by(rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. case x of None \<Rightarrow> (None, None) | Some (a, b) \<Rightarrow> (Some a, Some b)) pq"])
   3.686 +  (auto simp add: pmf.map_comp o_def in_set_spmf split: option.splits intro: pmf.map_cong)
   3.687 +
   3.688 +lemma rel_spmfE [elim?, consumes 1, case_names rel_spmf]:
   3.689 +  assumes "rel_spmf P p q"
   3.690 +  obtains pq where 
   3.691 +    "\<And>x y. (x, y) \<in> set_spmf pq \<Longrightarrow> P x y"
   3.692 +    "p = map_spmf fst pq"
   3.693 +    "q = map_spmf snd pq"
   3.694 +using assms
   3.695 +proof(cases rule: rel_pmf.cases[consumes 1, case_names rel_pmf])
   3.696 +  case (rel_pmf pq)
   3.697 +  let ?pq = "map_pmf (\<lambda>(a, b). case (a, b) of (Some x, Some y) \<Rightarrow> Some (x, y) | _ \<Rightarrow> None) pq"
   3.698 +  have "\<And>x y. (x, y) \<in> set_spmf ?pq \<Longrightarrow> P x y"
   3.699 +    by(auto simp add: in_set_spmf split: option.split_asm dest: rel_pmf(1))
   3.700 +  moreover
   3.701 +  have "\<And>x. (x, None) \<in> set_pmf pq \<Longrightarrow> x = None" by(auto dest!: rel_pmf(1))
   3.702 +  then have "p = map_spmf fst ?pq" using rel_pmf(2)
   3.703 +    by(auto simp add: pmf.map_comp split_beta intro!: pmf.map_cong split: option.split)
   3.704 +  moreover
   3.705 +  have "\<And>y. (None, y) \<in> set_pmf pq \<Longrightarrow> y = None" by(auto dest!: rel_pmf(1))
   3.706 +  then have "q = map_spmf snd ?pq" using rel_pmf(3)
   3.707 +    by(auto simp add: pmf.map_comp split_beta intro!: pmf.map_cong split: option.split)
   3.708 +  ultimately show thesis ..
   3.709 +qed
   3.710 +
   3.711 +lemma rel_spmf_simps:
   3.712 +  "rel_spmf R p q \<longleftrightarrow> (\<exists>pq. (\<forall>(x, y)\<in>set_spmf pq. R x y) \<and> map_spmf fst pq = p \<and> map_spmf snd pq = q)"
   3.713 +by(auto intro: rel_spmfI elim!: rel_spmfE)
   3.714 +
   3.715 +lemma spmf_rel_map:
   3.716 +  shows spmf_rel_map1: "\<And>R f x. rel_spmf R (map_spmf f x) = rel_spmf (\<lambda>x. R (f x)) x"
   3.717 +  and spmf_rel_map2: "\<And>R x g y. rel_spmf R x (map_spmf g y) = rel_spmf (\<lambda>x y. R x (g y)) x y"
   3.718 +by(simp_all add: fun_eq_iff pmf.rel_map option.rel_map[abs_def])
   3.719 +
   3.720 +lemma spmf_rel_conversep: "rel_spmf R\<inverse>\<inverse> = (rel_spmf R)\<inverse>\<inverse>"
   3.721 +by(simp add: option.rel_conversep pmf.rel_conversep)
   3.722 +
   3.723 +lemma spmf_rel_eq: "rel_spmf op = = op ="
   3.724 +by(simp add: pmf.rel_eq option.rel_eq)
   3.725 +
   3.726 +context begin interpretation lifting_syntax .
   3.727 +
   3.728 +lemma bind_spmf_parametric [transfer_rule]:
   3.729 +  "(rel_spmf A ===> (A ===> rel_spmf B) ===> rel_spmf B) bind_spmf bind_spmf"
   3.730 +unfolding bind_spmf_def[abs_def] by transfer_prover
   3.731 +
   3.732 +lemma return_spmf_parametric: "(A ===> rel_spmf A) return_spmf return_spmf"
   3.733 +by transfer_prover
   3.734 +
   3.735 +lemma map_spmf_parametric: "((A ===> B) ===> rel_spmf A ===> rel_spmf B) map_spmf map_spmf"
   3.736 +by transfer_prover
   3.737 +
   3.738 +lemma rel_spmf_parametric:
   3.739 +  "((A ===> B ===> op =) ===> rel_spmf A ===> rel_spmf B ===> op =) rel_spmf rel_spmf"
   3.740 +by transfer_prover
   3.741 +
   3.742 +lemma set_spmf_parametric [transfer_rule]:
   3.743 +  "(rel_spmf A ===> rel_set A) set_spmf set_spmf"
   3.744 +unfolding set_spmf_def[abs_def] by transfer_prover
   3.745 +
   3.746 +lemma return_spmf_None_parametric:
   3.747 +  "(rel_spmf A) (return_pmf None) (return_pmf None)"
   3.748 +by simp
   3.749 +
   3.750 +end
   3.751 +
   3.752 +lemma rel_spmf_bindI:
   3.753 +  "\<lbrakk> rel_spmf R p q; \<And>x y. R x y \<Longrightarrow> rel_spmf P (f x) (g y) \<rbrakk>
   3.754 +  \<Longrightarrow> rel_spmf P (p \<bind> f) (q \<bind> g)"
   3.755 +by(fact bind_spmf_parametric[THEN rel_funD, THEN rel_funD, OF _ rel_funI])
   3.756 +
   3.757 +lemma rel_spmf_bind_reflI:
   3.758 +  "(\<And>x. x \<in> set_spmf p \<Longrightarrow> rel_spmf P (f x) (g x)) \<Longrightarrow> rel_spmf P (p \<bind> f) (p \<bind> g)"
   3.759 +by(rule rel_spmf_bindI[where R="\<lambda>x y. x = y \<and> x \<in> set_spmf p"])(auto intro: rel_spmf_reflI)
   3.760 +
   3.761 +lemma rel_pmf_return_pmfI: "P x y \<Longrightarrow> rel_pmf P (return_pmf x) (return_pmf y)"
   3.762 +by(rule rel_pmf.intros[where pq="return_pmf (x, y)"])(simp_all)
   3.763 +
   3.764 +context begin interpretation lifting_syntax .
   3.765 +text \<open>We do not yet have a relator for @{typ "'a measure"}, so we combine @{const measure} and @{const measure_pmf}\<close>
   3.766 +lemma measure_pmf_parametric:
   3.767 +  "(rel_pmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
   3.768 +proof(rule rel_funI)+
   3.769 +  fix p q X Y
   3.770 +  assume "rel_pmf A p q" and "rel_pred A X Y"
   3.771 +  from this(1) obtain pq where A: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> A x y"
   3.772 +    and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
   3.773 +  show "measure p X = measure q Y" unfolding p q measure_map_pmf
   3.774 +    by(rule measure_pmf.finite_measure_eq_AE)(auto simp add: AE_measure_pmf_iff dest!: A rel_predD[OF \<open>rel_pred _ _ _\<close>])
   3.775 +qed
   3.776 +
   3.777 +lemma measure_spmf_parametric:
   3.778 +  "(rel_spmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_spmf p)) (\<lambda>q. measure (measure_spmf q))"
   3.779 +unfolding measure_measure_spmf_conv_measure_pmf[abs_def]
   3.780 +apply(rule rel_funI)+
   3.781 +apply(erule measure_pmf_parametric[THEN rel_funD, THEN rel_funD])
   3.782 +apply(auto simp add: rel_pred_def rel_fun_def elim: option.rel_cases)
   3.783 +done
   3.784 +end
   3.785 +
   3.786 +subsection {* From @{typ "'a pmf"} to @{typ "'a spmf"} *}
   3.787 +
   3.788 +definition spmf_of_pmf :: "'a pmf \<Rightarrow> 'a spmf"
   3.789 +where "spmf_of_pmf = map_pmf Some"
   3.790 +
   3.791 +lemma set_spmf_spmf_of_pmf [simp]: "set_spmf (spmf_of_pmf p) = set_pmf p"
   3.792 +by(auto simp add: spmf_of_pmf_def set_spmf_def bind_image o_def)
   3.793 +
   3.794 +lemma spmf_spmf_of_pmf [simp]: "spmf (spmf_of_pmf p) x = pmf p x"
   3.795 +by(simp add: spmf_of_pmf_def)
   3.796 +
   3.797 +lemma pmf_spmf_of_pmf_None [simp]: "pmf (spmf_of_pmf p) None = 0"
   3.798 +using ennreal_pmf_map[of Some p None] by(simp add: spmf_of_pmf_def)
   3.799 +
   3.800 +lemma emeasure_spmf_of_pmf [simp]: "emeasure (measure_spmf (spmf_of_pmf p)) A = emeasure (measure_pmf p) A"
   3.801 +by(simp add: emeasure_measure_spmf_conv_measure_pmf spmf_of_pmf_def inj_vimage_image_eq)
   3.802 +
   3.803 +lemma measure_spmf_spmf_of_pmf [simp]: "measure_spmf (spmf_of_pmf p) = measure_pmf p"
   3.804 +by(rule measure_eqI) simp_all
   3.805 +
   3.806 +lemma map_spmf_of_pmf [simp]: "map_spmf f (spmf_of_pmf p) = spmf_of_pmf (map_pmf f p)"
   3.807 +by(simp add: spmf_of_pmf_def pmf.map_comp o_def)
   3.808 +
   3.809 +lemma rel_spmf_spmf_of_pmf [simp]: "rel_spmf R (spmf_of_pmf p) (spmf_of_pmf q) = rel_pmf R p q"
   3.810 +by(simp add: spmf_of_pmf_def pmf.rel_map)
   3.811 +
   3.812 +lemma spmf_of_pmf_return_pmf [simp]: "spmf_of_pmf (return_pmf x) = return_spmf x"
   3.813 +by(simp add: spmf_of_pmf_def)
   3.814 +
   3.815 +lemma bind_spmf_of_pmf [simp]: "bind_spmf (spmf_of_pmf p) f = bind_pmf p f"
   3.816 +by(simp add: spmf_of_pmf_def bind_spmf_def bind_map_pmf)
   3.817 +
   3.818 +lemma set_spmf_bind_pmf: "set_spmf (bind_pmf p f) = Set.bind (set_pmf p) (set_spmf \<circ> f)"
   3.819 +unfolding bind_spmf_of_pmf[symmetric] by(subst set_bind_spmf) simp
   3.820 +
   3.821 +lemma spmf_of_pmf_bind: "spmf_of_pmf (bind_pmf p f) = bind_pmf p (\<lambda>x. spmf_of_pmf (f x))"
   3.822 +by(simp add: spmf_of_pmf_def map_bind_pmf)
   3.823 +
   3.824 +lemma bind_pmf_return_spmf: "p \<bind> (\<lambda>x. return_spmf (f x)) = spmf_of_pmf (map_pmf f p)"
   3.825 +by(simp add: map_pmf_def spmf_of_pmf_bind)
   3.826 +
   3.827 +subsection {* Weight of a subprobability *}
   3.828 +
   3.829 +abbreviation weight_spmf :: "'a spmf \<Rightarrow> real"
   3.830 +where "weight_spmf p \<equiv> measure (measure_spmf p) (space (measure_spmf p))"
   3.831 +
   3.832 +lemma weight_spmf_def: "weight_spmf p = measure (measure_spmf p) UNIV"
   3.833 +by(simp add: space_measure_spmf)
   3.834 +
   3.835 +lemma weight_spmf_le_1: "weight_spmf p \<le> 1"
   3.836 +by(simp add: measure_spmf.subprob_measure_le_1)
   3.837 +
   3.838 +lemma weight_return_spmf [simp]: "weight_spmf (return_spmf x) = 1"
   3.839 +by(simp add: measure_spmf_return_spmf measure_return)
   3.840 +
   3.841 +lemma weight_return_pmf_None [simp]: "weight_spmf (return_pmf None) = 0"
   3.842 +by(simp)
   3.843 +
   3.844 +lemma weight_map_spmf [simp]: "weight_spmf (map_spmf f p) = weight_spmf p"
   3.845 +by(simp add: weight_spmf_def measure_map_spmf)
   3.846 +
   3.847 +lemma weight_spmf_of_pmf [simp]: "weight_spmf (spmf_of_pmf p) = 1"
   3.848 +using measure_pmf.prob_space[of p] by(simp add: spmf_of_pmf_def weight_spmf_def)
   3.849 +
   3.850 +lemma weight_spmf_nonneg: "weight_spmf p \<ge> 0"
   3.851 +by(fact measure_nonneg)
   3.852 +
   3.853 +lemma (in finite_measure) integrable_weight_spmf [simp]: 
   3.854 +  "(\<lambda>x. weight_spmf (f x)) \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. weight_spmf (f x))"
   3.855 +by(rule integrable_const_bound[where B=1])(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
   3.856 +
   3.857 +lemma weight_spmf_eq_nn_integral_spmf: "weight_spmf p = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
   3.858 +by(simp add: measure_measure_spmf_conv_measure_pmf space_measure_spmf measure_pmf.emeasure_eq_measure[symmetric] nn_integral_pmf[symmetric] embed_measure_count_space[symmetric] inj_on_def nn_integral_embed_measure measurable_embed_measure1)
   3.859 +
   3.860 +lemma weight_spmf_eq_nn_integral_support:
   3.861 +  "weight_spmf p = \<integral>\<^sup>+ x. spmf p x \<partial>count_space (set_spmf p)"
   3.862 +unfolding weight_spmf_eq_nn_integral_spmf
   3.863 +by(auto simp add: nn_integral_count_space_indicator in_set_spmf_iff_spmf intro!: nn_integral_cong split: split_indicator)
   3.864 +
   3.865 +lemma pmf_None_eq_weight_spmf: "pmf p None = 1 - weight_spmf p"
   3.866 +proof -
   3.867 +  have "weight_spmf p = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV" by(rule weight_spmf_eq_nn_integral_spmf)
   3.868 +  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator (range Some) x \<partial>count_space UNIV"
   3.869 +    by(simp add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] nn_integral_embed_measure measurable_embed_measure1)
   3.870 +  also have "\<dots> + pmf p None = \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator (range Some) x + ennreal (pmf p None) * indicator {None} x \<partial>count_space UNIV"
   3.871 +    by(subst nn_integral_add)(simp_all add: max_def)
   3.872 +  also have "\<dots> = \<integral>\<^sup>+ x. pmf p x \<partial>count_space UNIV"
   3.873 +    by(rule nn_integral_cong)(auto split: split_indicator)
   3.874 +  also have "\<dots> = 1" by (simp add: nn_integral_pmf)
   3.875 +  finally show ?thesis by(simp add: ennreal_plus[symmetric] del: ennreal_plus)
   3.876 +qed
   3.877 +
   3.878 +lemma weight_spmf_conv_pmf_None: "weight_spmf p = 1 - pmf p None"
   3.879 +by(simp add: pmf_None_eq_weight_spmf)
   3.880 +
   3.881 +lemma weight_spmf_le_0: "weight_spmf p \<le> 0 \<longleftrightarrow> weight_spmf p = 0"
   3.882 +by(rule measure_le_0_iff)
   3.883 +
   3.884 +lemma weight_spmf_lt_0: "\<not> weight_spmf p < 0"
   3.885 +by(simp add: not_less weight_spmf_nonneg)
   3.886 +
   3.887 +lemma spmf_le_weight: "spmf p x \<le> weight_spmf p"
   3.888 +proof -
   3.889 +  have "ennreal (spmf p x) \<le> weight_spmf p"
   3.890 +    unfolding weight_spmf_eq_nn_integral_spmf by(rule nn_integral_ge_point) simp
   3.891 +  then show ?thesis by simp
   3.892 +qed
   3.893 +
   3.894 +lemma weight_spmf_eq_0: "weight_spmf p = 0 \<longleftrightarrow> p = return_pmf None"
   3.895 +by(auto intro!: pmf_eqI simp add: pmf_None_eq_weight_spmf split: split_indicator)(metis not_Some_eq pmf_le_0_iff spmf_le_weight)
   3.896 +
   3.897 +lemma weight_bind_spmf: "weight_spmf (x \<bind> f) = lebesgue_integral (measure_spmf x) (weight_spmf \<circ> f)"
   3.898 +unfolding weight_spmf_def
   3.899 +by(simp add: measure_spmf_bind o_def measure_spmf.measure_bind[where N="count_space UNIV"])
   3.900 +
   3.901 +lemma rel_spmf_weightD: "rel_spmf A p q \<Longrightarrow> weight_spmf p = weight_spmf q"
   3.902 +by(erule rel_spmfE) simp
   3.903 +
   3.904 +lemma rel_spmf_bij_betw:
   3.905 +  assumes f: "bij_betw f (set_spmf p) (set_spmf q)"
   3.906 +  and eq: "\<And>x. x \<in> set_spmf p \<Longrightarrow> spmf p x = spmf q (f x)"
   3.907 +  shows "rel_spmf (\<lambda>x y. f x = y) p q"
   3.908 +proof -
   3.909 +  let ?f = "map_option f"
   3.910 +
   3.911 +  have weq: "ennreal (weight_spmf p) = ennreal (weight_spmf q)"
   3.912 +    unfolding weight_spmf_eq_nn_integral_support
   3.913 +    by(subst nn_integral_bij_count_space[OF f, symmetric])(rule nn_integral_cong_AE, simp add: eq AE_count_space)
   3.914 +  then have "None \<in> set_pmf p \<longleftrightarrow> None \<in> set_pmf q"
   3.915 +    by(simp add: pmf_None_eq_weight_spmf set_pmf_iff)
   3.916 +  with f have "bij_betw (map_option f) (set_pmf p) (set_pmf q)"
   3.917 +    apply(auto simp add: bij_betw_def in_set_spmf inj_on_def intro: option.expand)
   3.918 +    apply(rename_tac [!] x)
   3.919 +    apply(case_tac [!] x)
   3.920 +    apply(auto iff: in_set_spmf)
   3.921 +    done
   3.922 +  then have "rel_pmf (\<lambda>x y. ?f x = y) p q"
   3.923 +    by(rule rel_pmf_bij_betw)(case_tac x, simp_all add: weq[simplified] eq in_set_spmf pmf_None_eq_weight_spmf)
   3.924 +  thus ?thesis by(rule pmf.rel_mono_strong)(auto intro!: rel_optionI simp add: Option.is_none_def)
   3.925 +qed
   3.926 +
   3.927 +subsection {* From density to spmfs *}
   3.928 +
   3.929 +context fixes f :: "'a \<Rightarrow> real" begin
   3.930 +
   3.931 +definition embed_spmf :: "'a spmf"
   3.932 +where "embed_spmf = embed_pmf (\<lambda>x. case x of None \<Rightarrow> 1 - enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV) | Some x' \<Rightarrow> max 0 (f x'))"
   3.933 +
   3.934 +context
   3.935 +  assumes prob: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV) \<le> 1"
   3.936 +begin
   3.937 +
   3.938 +lemma nn_integral_embed_spmf_eq_1:
   3.939 +  "(\<integral>\<^sup>+ x. ennreal (case x of None \<Rightarrow> 1 - enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV) | Some x' \<Rightarrow> max 0 (f x')) \<partial>count_space UNIV) = 1"
   3.940 +  (is "?lhs = _" is "(\<integral>\<^sup>+ x. ?f x \<partial>?M) = _")
   3.941 +proof -
   3.942 +  have "?lhs = \<integral>\<^sup>+ x. ?f x * indicator {None} x + ?f x * indicator (range Some) x \<partial>?M"
   3.943 +    by(rule nn_integral_cong)(auto split: split_indicator)
   3.944 +  also have "\<dots> = (1 - enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV)) + \<integral>\<^sup>+ x. ?f x * indicator (range Some) x \<partial>?M"
   3.945 +    (is "_ = ?None + ?Some")
   3.946 +    by(subst nn_integral_add)(simp_all add: AE_count_space max_def le_diff_eq real_le_ereal_iff one_ereal_def[symmetric] prob split: option.split)
   3.947 +  also have "?Some = \<integral>\<^sup>+ x. ?f x \<partial>count_space (range Some)"
   3.948 +    by(simp add: nn_integral_count_space_indicator)
   3.949 +  also have "count_space (range Some) = embed_measure (count_space UNIV) Some"
   3.950 +    by(simp add: embed_measure_count_space)
   3.951 +  also have "(\<integral>\<^sup>+ x. ?f x \<partial>\<dots>) = \<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV"
   3.952 +    by(subst nn_integral_embed_measure)(simp_all add: measurable_embed_measure1)
   3.953 +  also have "?None + \<dots> = 1" using prob
   3.954 +    by(auto simp add: ennreal_minus[symmetric] ennreal_1[symmetric] ennreal_enn2real_if top_unique simp del: ennreal_1)(simp add: diff_add_self_ennreal)
   3.955 +  finally show ?thesis .
   3.956 +qed
   3.957 +
   3.958 +lemma pmf_embed_spmf_None: "pmf embed_spmf None = 1 - enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV)"
   3.959 +unfolding embed_spmf_def
   3.960 +apply(subst pmf_embed_pmf)
   3.961 +  subgoal using prob by(simp add: field_simps enn2real_leI split: option.split)
   3.962 + apply(rule nn_integral_embed_spmf_eq_1)
   3.963 +apply simp
   3.964 +done
   3.965 +
   3.966 +lemma spmf_embed_spmf [simp]: "spmf embed_spmf x = max 0 (f x)"
   3.967 +unfolding embed_spmf_def
   3.968 +apply(subst pmf_embed_pmf)
   3.969 +  subgoal using prob by(simp add: field_simps enn2real_leI split: option.split)
   3.970 + apply(rule nn_integral_embed_spmf_eq_1)
   3.971 +apply simp
   3.972 +done
   3.973 +
   3.974 +end
   3.975 +
   3.976 +end
   3.977 +
   3.978 +lemma embed_spmf_K_0[simp]: "embed_spmf (\<lambda>_. 0) = return_pmf None" (is "?lhs = ?rhs")
   3.979 +by(rule spmf_eqI)(simp add: zero_ereal_def[symmetric])
   3.980 +
   3.981 +subsection {* Ordering on spmfs *}
   3.982 +
   3.983 +text {*
   3.984 +  @{const rel_pmf} does not preserve a ccpo structure. Counterexample by Saheb-Djahromi:
   3.985 +  Take prefix order over @{text "bool llist"} and
   3.986 +  the set @{text "range (\<lambda>n :: nat. uniform (llist_n n))"} where @{text "llist_n"} is the set
   3.987 +  of all @{text llist}s of length @{text n} and @{text uniform} returns a uniform distribution over
   3.988 +  the given set. The set forms a chain in @{text "ord_pmf lprefix"}, but it has not an upper bound.
   3.989 +  Any upper bound may contain only infinite lists in its support because otherwise it is not greater
   3.990 +  than the @{text "n+1"}-st element in the chain where @{text n} is the length of the finite list.
   3.991 +  Moreover its support must contain all infinite lists, because otherwise there is a finite list
   3.992 +  all of whose finite extensions are not in the support - a contradiction to the upper bound property.
   3.993 +  Hence, the support is uncountable, but pmf's only have countable support.
   3.994 +
   3.995 +  However, if all chains in the ccpo are finite, then it should preserve the ccpo structure.
   3.996 +*}
   3.997 +
   3.998 +abbreviation ord_spmf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf \<Rightarrow> bool"
   3.999 +where "ord_spmf ord \<equiv> rel_pmf (ord_option ord)"
  3.1000 +
  3.1001 +locale ord_spmf_syntax begin
  3.1002 +notation ord_spmf (infix "\<sqsubseteq>\<index>" 60)
  3.1003 +end
  3.1004 +
  3.1005 +lemma ord_spmf_map_spmf1: "ord_spmf R (map_spmf f p) = ord_spmf (\<lambda>x. R (f x)) p"
  3.1006 +by(simp add: pmf.rel_map[abs_def] ord_option_map1[abs_def])
  3.1007 +
  3.1008 +lemma ord_spmf_map_spmf2: "ord_spmf R p (map_spmf f q) = ord_spmf (\<lambda>x y. R x (f y)) p q"
  3.1009 +by(simp add: pmf.rel_map ord_option_map2)
  3.1010 +
  3.1011 +lemma ord_spmf_map_spmf12: "ord_spmf R (map_spmf f p) (map_spmf f q) = ord_spmf (\<lambda>x y. R (f x) (f y)) p q"
  3.1012 +by(simp add: pmf.rel_map ord_option_map1[abs_def] ord_option_map2)
  3.1013 +
  3.1014 +lemmas ord_spmf_map_spmf = ord_spmf_map_spmf1 ord_spmf_map_spmf2 ord_spmf_map_spmf12
  3.1015 +
  3.1016 +context fixes ord :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (structure) begin
  3.1017 +interpretation ord_spmf_syntax .
  3.1018 +
  3.1019 +lemma ord_spmfI:
  3.1020 +  "\<lbrakk> \<And>x y. (x, y) \<in> set_spmf pq \<Longrightarrow> ord x y; map_spmf fst pq = p; map_spmf snd pq = q \<rbrakk>
  3.1021 +  \<Longrightarrow> p \<sqsubseteq> q"
  3.1022 +by(rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. case x of None \<Rightarrow> (None, None) | Some (a, b) \<Rightarrow> (Some a, Some b)) pq"])
  3.1023 +  (auto simp add: pmf.map_comp o_def in_set_spmf split: option.splits intro: pmf.map_cong)
  3.1024 +
  3.1025 +lemma ord_spmf_None [simp]: "return_pmf None \<sqsubseteq> x"
  3.1026 +by(rule rel_pmf.intros[where pq="map_pmf (Pair None) x"])(auto simp add: pmf.map_comp o_def)
  3.1027 +
  3.1028 +lemma ord_spmf_reflI: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> ord x x) \<Longrightarrow> p \<sqsubseteq> p"
  3.1029 +by(rule rel_pmf_reflI ord_option_reflI)+(auto simp add: in_set_spmf)
  3.1030 +
  3.1031 +lemma rel_spmf_inf:
  3.1032 +  assumes "p \<sqsubseteq> q"
  3.1033 +  and "q \<sqsubseteq> p"
  3.1034 +  and refl: "reflp ord"
  3.1035 +  and trans: "transp ord"
  3.1036 +  shows "rel_spmf (inf ord ord\<inverse>\<inverse>) p q"
  3.1037 +proof -
  3.1038 +  from \<open>p \<sqsubseteq> q\<close> \<open>q \<sqsubseteq> p\<close>
  3.1039 +  have "rel_pmf (inf (ord_option ord) (ord_option ord)\<inverse>\<inverse>) p q"
  3.1040 +    by(rule rel_pmf_inf)(blast intro: reflp_ord_option transp_ord_option refl trans)+
  3.1041 +  also have "inf (ord_option ord) (ord_option ord)\<inverse>\<inverse> = rel_option (inf ord ord\<inverse>\<inverse>)"
  3.1042 +    by(auto simp add: fun_eq_iff elim: ord_option.cases option.rel_cases)
  3.1043 +  finally show ?thesis .
  3.1044 +qed
  3.1045 +
  3.1046 +end
  3.1047 +
  3.1048 +lemma ord_spmf_return_spmf2: "ord_spmf R p (return_spmf y) \<longleftrightarrow> (\<forall>x\<in>set_spmf p. R x y)"
  3.1049 +by(auto simp add: rel_pmf_return_pmf2 in_set_spmf ord_option.simps intro: ccontr)
  3.1050 +
  3.1051 +lemma ord_spmf_mono: "\<lbrakk> ord_spmf A p q; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> ord_spmf B p q"
  3.1052 +by(erule rel_pmf_mono)(erule ord_option_mono)
  3.1053 +
  3.1054 +lemma ord_spmf_compp: "ord_spmf (A OO B) = ord_spmf A OO ord_spmf B"
  3.1055 +by(simp add: ord_option_compp pmf.rel_compp)
  3.1056 +
  3.1057 +lemma ord_spmf_bindI:
  3.1058 +  assumes pq: "ord_spmf R p q"
  3.1059 +  and fg: "\<And>x y. R x y \<Longrightarrow> ord_spmf P (f x) (g y)"
  3.1060 +  shows "ord_spmf P (p \<bind> f) (q \<bind> g)"
  3.1061 +unfolding bind_spmf_def using pq
  3.1062 +by(rule rel_pmf_bindI)(auto split: option.split intro: fg)
  3.1063 +
  3.1064 +lemma ord_spmf_bind_reflI:
  3.1065 +  "(\<And>x. x \<in> set_spmf p \<Longrightarrow> ord_spmf R (f x) (g x))
  3.1066 +  \<Longrightarrow> ord_spmf R (p \<bind> f) (p \<bind> g)"
  3.1067 +by(rule ord_spmf_bindI[where R="\<lambda>x y. x = y \<and> x \<in> set_spmf p"])(auto intro: ord_spmf_reflI)
  3.1068 +
  3.1069 +lemma ord_pmf_increaseI:
  3.1070 +  assumes le: "\<And>x. spmf p x \<le> spmf q x"
  3.1071 +  and refl: "\<And>x. x \<in> set_spmf p \<Longrightarrow> R x x"
  3.1072 +  shows "ord_spmf R p q"
  3.1073 +proof(rule rel_pmf.intros)
  3.1074 +  define pq where "pq = embed_pmf 
  3.1075 +    (\<lambda>(x, y). case x of Some x' \<Rightarrow> (case y of Some y' \<Rightarrow> if x' = y' then spmf p x' else 0 | None \<Rightarrow> 0)
  3.1076 +      | None \<Rightarrow> (case y of None \<Rightarrow> pmf q None | Some y' \<Rightarrow> spmf q y' - spmf p y'))"
  3.1077 +     (is "_ = embed_pmf ?f")
  3.1078 +  have nonneg: "\<And>xy. ?f xy \<ge> 0"
  3.1079 +    by(clarsimp simp add: le field_simps split: option.split)
  3.1080 +  have integral: "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) = 1" (is "nn_integral ?M _ = _")
  3.1081 +  proof -
  3.1082 +    have "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) =
  3.1083 +      \<integral>\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy + 
  3.1084 +             ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy + 
  3.1085 +             ennreal (?f xy) * indicator (range (\<lambda>x. (Some x, Some x))) xy \<partial>?M"
  3.1086 +      by(rule nn_integral_cong)(auto split: split_indicator option.splits if_split_asm)
  3.1087 +    also have "\<dots> = (\<integral>\<^sup>+ xy. ?f xy * indicator {(None, None)} xy \<partial>?M) +
  3.1088 +        (\<integral>\<^sup>+ xy. ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy \<partial>?M) +
  3.1089 +        (\<integral>\<^sup>+ xy. ennreal (?f xy) * indicator (range (\<lambda>x. (Some x, Some x))) xy \<partial>?M)"
  3.1090 +      (is "_ = ?None + ?Some2 + ?Some")
  3.1091 +      by(subst nn_integral_add)(simp_all add: nn_integral_add AE_count_space le_diff_eq le split: option.split)
  3.1092 +    also have "?None = pmf q None" by simp
  3.1093 +    also have "?Some2 = \<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV"
  3.1094 +      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)
  3.1095 +    also have "\<dots> = (\<integral>\<^sup>+ x. spmf q x \<partial>count_space UNIV) - (\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV)"
  3.1096 +      (is "_ = ?Some2' - ?Some2''")
  3.1097 +      by(subst nn_integral_diff)(simp_all add: le nn_integral_spmf_neq_top)
  3.1098 +    also have "?Some = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
  3.1099 +      by(simp add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] inj_on_def nn_integral_embed_measure measurable_embed_measure1)
  3.1100 +    also have "pmf q None + (?Some2' - ?Some2'') + \<dots> = pmf q None + ?Some2'"
  3.1101 +      by(auto simp add: diff_add_self_ennreal le intro!: nn_integral_mono)
  3.1102 +    also have "\<dots> = \<integral>\<^sup>+ x. ennreal (pmf q x) * indicator {None} x + ennreal (pmf q x) * indicator (range Some) x \<partial>count_space UNIV"
  3.1103 +      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)
  3.1104 +    also have "\<dots> = \<integral>\<^sup>+ x. pmf q x \<partial>count_space UNIV"
  3.1105 +      by(rule nn_integral_cong)(auto split: split_indicator)
  3.1106 +    also have "\<dots> = 1" by(simp add: nn_integral_pmf)
  3.1107 +    finally show ?thesis .
  3.1108 +  qed
  3.1109 +  note f = nonneg integral
  3.1110 +
  3.1111 +  { fix x y
  3.1112 +    assume "(x, y) \<in> set_pmf pq"
  3.1113 +    hence "?f (x, y) \<noteq> 0" unfolding pq_def by(simp add: set_embed_pmf[OF f])
  3.1114 +    then show "ord_option R x y"
  3.1115 +      by(simp add: spmf_eq_0_set_spmf refl split: option.split_asm if_split_asm) }
  3.1116 +
  3.1117 +  have weight_le: "weight_spmf p \<le> weight_spmf q"
  3.1118 +    by(subst ennreal_le_iff[symmetric])(auto simp add: weight_spmf_eq_nn_integral_spmf intro!: nn_integral_mono le)
  3.1119 +
  3.1120 +  show "map_pmf fst pq = p"
  3.1121 +  proof(rule pmf_eqI)
  3.1122 +    fix i
  3.1123 +    have "ennreal (pmf (map_pmf fst pq) i) = (\<integral>\<^sup>+ y. pmf pq (i, y) \<partial>count_space UNIV)"
  3.1124 +      unfolding pq_def ennreal_pmf_map
  3.1125 +      apply(simp add: embed_pmf.rep_eq[OF f] o_def emeasure_density nn_integral_count_space_indicator[symmetric])
  3.1126 +      apply(subst pmf_embed_pmf[OF f])
  3.1127 +      apply(rule nn_integral_bij_count_space[symmetric])
  3.1128 +      apply(auto simp add: bij_betw_def inj_on_def)
  3.1129 +      done
  3.1130 +    also have "\<dots> = pmf p i"
  3.1131 +    proof(cases i)
  3.1132 +      case (Some x)
  3.1133 +      have "(\<integral>\<^sup>+ y. pmf pq (Some x, y) \<partial>count_space UNIV) = \<integral>\<^sup>+ y. pmf p (Some x) * indicator {Some x} y \<partial>count_space UNIV"
  3.1134 +        by(rule nn_integral_cong)(simp add: pq_def pmf_embed_pmf[OF f] split: option.split)
  3.1135 +      then show ?thesis using Some by simp
  3.1136 +    next
  3.1137 +      case None
  3.1138 +      have "(\<integral>\<^sup>+ y. pmf pq (None, y) \<partial>count_space UNIV) = 
  3.1139 +            (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y + 
  3.1140 +                   ennreal (pmf pq (None, None)) * indicator {None} y \<partial>count_space UNIV)"
  3.1141 +        by(rule nn_integral_cong)(auto split: split_indicator)
  3.1142 +      also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) \<partial>count_space (range Some)) + pmf pq (None, None)"
  3.1143 +        by(subst nn_integral_add)(simp_all add: nn_integral_count_space_indicator)
  3.1144 +      also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (spmf q y) - ennreal (spmf p y) \<partial>count_space UNIV) + pmf q None"
  3.1145 +        by(simp add: pq_def pmf_embed_pmf[OF f] embed_measure_count_space[symmetric] nn_integral_embed_measure measurable_embed_measure1 ennreal_minus)
  3.1146 +      also have "(\<integral>\<^sup>+ y. ennreal (spmf q y) - ennreal (spmf p y) \<partial>count_space UNIV) =
  3.1147 +                 (\<integral>\<^sup>+ y. spmf q y \<partial>count_space UNIV) - (\<integral>\<^sup>+ y. spmf p y \<partial>count_space UNIV)"
  3.1148 +        by(subst nn_integral_diff)(simp_all add: AE_count_space le nn_integral_spmf_neq_top split: split_indicator)
  3.1149 +      also have "\<dots> = pmf p None - pmf q None"
  3.1150 +        by(simp add: pmf_None_eq_weight_spmf weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus)
  3.1151 +      also have "\<dots> = ennreal (pmf p None) - ennreal (pmf q None)" by(simp add: ennreal_minus)
  3.1152 +      finally show ?thesis using None weight_le
  3.1153 +        by(auto simp add: diff_add_self_ennreal pmf_None_eq_weight_spmf intro: ennreal_leI)
  3.1154 +    qed
  3.1155 +    finally show "pmf (map_pmf fst pq) i = pmf p i" by simp
  3.1156 +  qed
  3.1157 +
  3.1158 +  show "map_pmf snd pq = q"
  3.1159 +  proof(rule pmf_eqI)
  3.1160 +    fix i
  3.1161 +    have "ennreal (pmf (map_pmf snd pq) i) = (\<integral>\<^sup>+ x. pmf pq (x, i) \<partial>count_space UNIV)"
  3.1162 +      unfolding pq_def ennreal_pmf_map
  3.1163 +      apply(simp add: embed_pmf.rep_eq[OF f] o_def emeasure_density nn_integral_count_space_indicator[symmetric])
  3.1164 +      apply(subst pmf_embed_pmf[OF f])
  3.1165 +      apply(rule nn_integral_bij_count_space[symmetric])
  3.1166 +      apply(auto simp add: bij_betw_def inj_on_def)
  3.1167 +      done
  3.1168 +    also have "\<dots> = ennreal (pmf q i)"
  3.1169 +    proof(cases i)
  3.1170 +      case None
  3.1171 +      have "(\<integral>\<^sup>+ x. pmf pq (x, None) \<partial>count_space UNIV) = \<integral>\<^sup>+ x. pmf q None * indicator {None :: 'a option} x \<partial>count_space UNIV"
  3.1172 +        by(rule nn_integral_cong)(simp add: pq_def pmf_embed_pmf[OF f] split: option.split)
  3.1173 +      then show ?thesis using None by simp
  3.1174 +    next
  3.1175 +      case (Some y)
  3.1176 +      have "(\<integral>\<^sup>+ x. pmf pq (x, Some y) \<partial>count_space UNIV) = 
  3.1177 +        (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x + 
  3.1178 +               ennreal (pmf pq (None, Some y)) * indicator {None} x \<partial>count_space UNIV)"
  3.1179 +        by(rule nn_integral_cong)(auto split: split_indicator)
  3.1180 +      also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x \<partial>count_space UNIV) + pmf pq (None, Some y)"
  3.1181 +        by(subst nn_integral_add)(simp_all)
  3.1182 +      also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (spmf p y) * indicator {Some y} x \<partial>count_space UNIV) + (spmf q y - spmf p y)"
  3.1183 +        by(auto simp add: pq_def pmf_embed_pmf[OF f] one_ereal_def[symmetric] simp del: nn_integral_indicator_singleton intro!: arg_cong2[where f="op +"] nn_integral_cong split: option.split)
  3.1184 +      also have "\<dots> = spmf q y" by(simp add: ennreal_minus[symmetric] le)
  3.1185 +      finally show ?thesis using Some by simp
  3.1186 +    qed
  3.1187 +    finally show "pmf (map_pmf snd pq) i = pmf q i" by simp
  3.1188 +  qed
  3.1189 +qed
  3.1190 +
  3.1191 +lemma ord_spmf_eq_leD:
  3.1192 +  assumes "ord_spmf op = p q"
  3.1193 +  shows "spmf p x \<le> spmf q x"
  3.1194 +proof(cases "x \<in> set_spmf p")
  3.1195 +  case False
  3.1196 +  thus ?thesis by(simp add: in_set_spmf_iff_spmf)
  3.1197 +next
  3.1198 +  case True
  3.1199 +  from assms obtain pq
  3.1200 +    where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> ord_option op = x y"
  3.1201 +    and p: "p = map_pmf fst pq"
  3.1202 +    and q: "q = map_pmf snd pq" by cases auto
  3.1203 +  have "ennreal (spmf p x) = integral\<^sup>N pq (indicator (fst -` {Some x}))"
  3.1204 +    using p by(simp add: ennreal_pmf_map)
  3.1205 +  also have "\<dots> = integral\<^sup>N pq (indicator {(Some x, Some x)})"
  3.1206 +    by(rule nn_integral_cong_AE)(auto simp add: AE_measure_pmf_iff split: split_indicator dest: pq)
  3.1207 +  also have "\<dots> \<le> integral\<^sup>N pq (indicator (snd -` {Some x}))"
  3.1208 +    by(rule nn_integral_mono) simp
  3.1209 +  also have "\<dots> = ennreal (spmf q x)" using q by(simp add: ennreal_pmf_map)
  3.1210 +  finally show ?thesis by simp
  3.1211 +qed
  3.1212 +
  3.1213 +lemma ord_spmf_eqD_set_spmf: "ord_spmf op = p q \<Longrightarrow> set_spmf p \<subseteq> set_spmf q"
  3.1214 +by(rule subsetI)(drule_tac x=x in ord_spmf_eq_leD, auto simp add: in_set_spmf_iff_spmf)
  3.1215 +
  3.1216 +lemma ord_spmf_eqD_emeasure:
  3.1217 +  "ord_spmf op = p q \<Longrightarrow> emeasure (measure_spmf p) A \<le> emeasure (measure_spmf q) A"
  3.1218 +by(auto intro!: nn_integral_mono split: split_indicator dest: ord_spmf_eq_leD simp add: nn_integral_measure_spmf nn_integral_indicator[symmetric])
  3.1219 +
  3.1220 +lemma ord_spmf_eqD_measure_spmf: "ord_spmf op = p q \<Longrightarrow> measure_spmf p \<le> measure_spmf q"
  3.1221 +by(rule less_eq_measure.intros)(simp_all add: ord_spmf_eqD_emeasure)
  3.1222 +
  3.1223 +
  3.1224 +subsection {* CCPO structure for the flat ccpo @{term "ord_option op ="} *}
  3.1225 +
  3.1226 +context fixes Y :: "'a spmf set" begin
  3.1227 +
  3.1228 +definition lub_spmf :: "'a spmf"
  3.1229 +where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
  3.1230 +  -- \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close> 
  3.1231 +
  3.1232 +lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
  3.1233 +by(simp add: SPMF.lub_spmf_def bot_ereal_def)
  3.1234 +
  3.1235 +context assumes chain: "Complete_Partial_Order.chain (ord_spmf op =) Y" begin
  3.1236 +
  3.1237 +lemma chain_ord_spmf_eqD: "Complete_Partial_Order.chain (op \<le>) ((\<lambda>p x. ennreal (spmf p x)) ` Y)"
  3.1238 +  (is "Complete_Partial_Order.chain _ (?f ` _)")
  3.1239 +proof(rule chainI)
  3.1240 +  fix f g
  3.1241 +  assume "f \<in> ?f ` Y" "g \<in> ?f ` Y"
  3.1242 +  then obtain p q where f: "f = ?f p" "p \<in> Y" and g: "g = ?f q" "q \<in> Y" by blast
  3.1243 +  from chain \<open>p \<in> Y\<close> \<open>q \<in> Y\<close> have "ord_spmf op = p q \<or> ord_spmf op = q p" by(rule chainD)
  3.1244 +  thus "f \<le> g \<or> g \<le> f"
  3.1245 +  proof
  3.1246 +    assume "ord_spmf op = p q"
  3.1247 +    hence "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
  3.1248 +    hence "f \<le> g" unfolding f g by(auto intro: le_funI)
  3.1249 +    thus ?thesis ..
  3.1250 +  next
  3.1251 +    assume "ord_spmf op = q p"
  3.1252 +    hence "\<And>x. spmf q x \<le> spmf p x" by(rule ord_spmf_eq_leD)
  3.1253 +    hence "g \<le> f" unfolding f g by(auto intro: le_funI)
  3.1254 +    thus ?thesis ..
  3.1255 +  qed
  3.1256 +qed
  3.1257 +
  3.1258 +lemma ord_spmf_eq_pmf_None_eq:
  3.1259 +  assumes le: "ord_spmf op = p q"
  3.1260 +  and None: "pmf p None = pmf q None"
  3.1261 +  shows "p = q"
  3.1262 +proof(rule spmf_eqI)
  3.1263 +  fix i
  3.1264 +  from le have le': "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
  3.1265 +  have "(\<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV) = 
  3.1266 +     (\<integral>\<^sup>+ x. spmf q x \<partial>count_space UNIV) - (\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV)"
  3.1267 +    by(subst nn_integral_diff)(simp_all add: AE_count_space le' nn_integral_spmf_neq_top)
  3.1268 +  also have "\<dots> = (1 - pmf q None) - (1 - pmf p None)" unfolding pmf_None_eq_weight_spmf
  3.1269 +    by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus)
  3.1270 +  also have "\<dots> = 0" using None by simp
  3.1271 +  finally have "\<And>x. spmf q x \<le> spmf p x" 
  3.1272 +    by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff)
  3.1273 +  with le' show "spmf p i = spmf q i" by(rule antisym)
  3.1274 +qed
  3.1275 +
  3.1276 +lemma ord_spmf_eqD_pmf_None: 
  3.1277 +  assumes "ord_spmf op = x y"
  3.1278 +  shows "pmf x None \<ge> pmf y None"
  3.1279 +using assms
  3.1280 +apply cases
  3.1281 +apply(clarsimp simp only: ennreal_le_iff[symmetric, OF pmf_nonneg] ennreal_pmf_map)
  3.1282 +apply(fastforce simp add: AE_measure_pmf_iff intro!: nn_integral_mono_AE)
  3.1283 +done
  3.1284 +
  3.1285 +text \<open>
  3.1286 +  Chains on @{typ "'a spmf"} maintain countable support.
  3.1287 +  Thanks to Johannes Hölzl for the proof idea.
  3.1288 +\<close>
  3.1289 +lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)" 
  3.1290 +proof(cases "Y = {}")
  3.1291 +  case Y: False
  3.1292 +  show ?thesis
  3.1293 +  proof(cases "\<exists>x\<in>Y. \<forall>y\<in>Y. ord_spmf op = y x")
  3.1294 +    case True
  3.1295 +    then obtain x where x: "x \<in> Y" and upper: "\<And>y. y \<in> Y \<Longrightarrow> ord_spmf op = y x" by blast
  3.1296 +    hence "(\<Union>x\<in>Y. set_spmf x) \<subseteq> set_spmf x" by(auto dest: ord_spmf_eqD_set_spmf)
  3.1297 +    thus ?thesis by(rule countable_subset) simp
  3.1298 +  next
  3.1299 +    case False
  3.1300 +    define N :: "'a option pmf \<Rightarrow> real" where "N p = pmf p None" for p
  3.1301 +  
  3.1302 +    have N_less_imp_le_spmf: "\<lbrakk> x \<in> Y; y \<in> Y; N y < N x \<rbrakk> \<Longrightarrow> ord_spmf op = x y" for x y
  3.1303 +      using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x]
  3.1304 +      by (auto simp: N_def)
  3.1305 +    have N_eq_imp_eq: "\<lbrakk> x \<in> Y; y \<in> Y; N y = N x \<rbrakk> \<Longrightarrow> x = y" for x y
  3.1306 +      using chainD[OF chain, of x y] by(auto simp add: N_def dest: ord_spmf_eq_pmf_None_eq)
  3.1307 +    
  3.1308 +    have NC: "N ` Y \<noteq> {}" "bdd_below (N ` Y)"
  3.1309 +      using \<open>Y \<noteq> {}\<close> by(auto intro!: bdd_belowI[of _ 0] simp: N_def)
  3.1310 +    have NC_less: "Inf (N ` Y) < N x" if "x \<in> Y" for x unfolding cInf_less_iff[OF NC]
  3.1311 +    proof(rule ccontr)
  3.1312 +      assume **: "\<not> (\<exists>y\<in>N ` Y. y < N x)"
  3.1313 +      { fix y
  3.1314 +        assume "y \<in> Y"
  3.1315 +        with ** consider "N x < N y" | "N x = N y" by(auto simp add: not_less le_less)
  3.1316 +        hence "ord_spmf op = y x" using \<open>y \<in> Y\<close> \<open>x \<in> Y\<close>
  3.1317 +          by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) }
  3.1318 +      with False \<open>x \<in> Y\<close> show False by blast
  3.1319 +    qed
  3.1320 +  
  3.1321 +    from NC have "Inf (N ` Y) \<in> closure (N ` Y)" by (intro closure_contains_Inf)
  3.1322 +    then obtain X' where "\<And>n. X' n \<in> N ` Y" and X': "X' \<longlonglongrightarrow> Inf (N ` Y)"
  3.1323 +      unfolding closure_sequential by auto
  3.1324 +    then obtain X where X: "\<And>n. X n \<in> Y" and "X' = (\<lambda>n. N (X n))" unfolding image_iff Bex_def by metis
  3.1325 +  
  3.1326 +    with X' have seq: "(\<lambda>n. N (X n)) \<longlonglongrightarrow> Inf (N ` Y)" by simp
  3.1327 +    have "(\<Union>x \<in> Y. set_spmf x) \<subseteq> (\<Union>n. set_spmf (X n))"
  3.1328 +    proof(rule UN_least)
  3.1329 +      fix x
  3.1330 +      assume "x \<in> Y"
  3.1331 +      from order_tendstoD(2)[OF seq NC_less[OF \<open>x \<in> Y\<close>]]
  3.1332 +      obtain i where "N (X i) < N x" by (auto simp: eventually_sequentially)
  3.1333 +      thus "set_spmf x \<subseteq> (\<Union>n. set_spmf (X n))" using X \<open>x \<in> Y\<close>
  3.1334 +        by(blast dest: N_less_imp_le_spmf ord_spmf_eqD_set_spmf)
  3.1335 +    qed
  3.1336 +    thus ?thesis by(rule countable_subset) simp
  3.1337 +  qed
  3.1338 +qed simp
  3.1339 +
  3.1340 +lemma lub_spmf_subprob: "(\<integral>\<^sup>+ x. (SUP p : Y. ennreal (spmf p x)) \<partial>count_space UNIV) \<le> 1"
  3.1341 +proof(cases "Y = {}")
  3.1342 +  case True
  3.1343 +  thus ?thesis by(simp add: bot_ennreal)
  3.1344 +next
  3.1345 +  case False
  3.1346 +  let ?B = "\<Union>p\<in>Y. set_spmf p"
  3.1347 +  have countable: "countable ?B" by(rule spmf_chain_countable)
  3.1348 +
  3.1349 +  have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) = 
  3.1350 +        (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
  3.1351 +    by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
  3.1352 +  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space ?B)"
  3.1353 +    unfolding ennreal_indicator[symmetric] using False
  3.1354 +    by(subst SUP_mult_right_ennreal[symmetric])(simp add: ennreal_indicator nn_integral_count_space_indicator)
  3.1355 +  also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B)" using False _ countable
  3.1356 +    by(rule nn_integral_monotone_convergence_SUP_countable)(rule chain_ord_spmf_eqD)
  3.1357 +  also have "\<dots> \<le> 1"
  3.1358 +  proof(rule SUP_least)
  3.1359 +    fix p
  3.1360 +    assume "p \<in> Y"
  3.1361 +    have "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B) = \<integral>\<^sup>+ x. ennreal (spmf p x) * indicator ?B x \<partial>count_space UNIV"
  3.1362 +      by(simp add: nn_integral_count_space_indicator)
  3.1363 +    also have "\<dots> = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
  3.1364 +      by(rule nn_integral_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf \<open>p \<in> Y\<close>)
  3.1365 +    also have "\<dots> \<le> 1"
  3.1366 +      by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] weight_spmf_le_1)
  3.1367 +    finally show "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B) \<le> 1" .
  3.1368 +  qed
  3.1369 +  finally show ?thesis .
  3.1370 +qed
  3.1371 +
  3.1372 +lemma spmf_lub_spmf:
  3.1373 +  assumes "Y \<noteq> {}"
  3.1374 +  shows "spmf lub_spmf x = (SUP p : Y. spmf p x)"
  3.1375 +proof -
  3.1376 +  from assms obtain p where "p \<in> Y" by auto
  3.1377 +  have "spmf lub_spmf x = max 0 (enn2real (SUP p:Y. ennreal (spmf p x)))" unfolding lub_spmf_def
  3.1378 +    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)
  3.1379 +  also have "\<dots> = enn2real (SUP p:Y. ennreal (spmf p x))"
  3.1380 +    by(rule max_absorb2)(simp)
  3.1381 +  also have "\<dots> = enn2real (ennreal (SUP p : Y. spmf p x))" using assms
  3.1382 +    by(subst ennreal_SUP[symmetric])(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
  3.1383 +  also have "0 \<le> (\<Squnion>p\<in>Y. spmf p x)" using assms
  3.1384 +    by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] simp add: pmf_le_1)
  3.1385 +  then have "enn2real (ennreal (SUP p : Y. spmf p x)) = (SUP p : Y. spmf p x)"
  3.1386 +    by(rule enn2real_ennreal)
  3.1387 +  finally show ?thesis .
  3.1388 +qed
  3.1389 +
  3.1390 +lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
  3.1391 +unfolding spmf_lub_spmf by(subst ennreal_SUP)(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
  3.1392 +
  3.1393 +lemma lub_spmf_upper:
  3.1394 +  assumes p: "p \<in> Y"
  3.1395 +  shows "ord_spmf op = p lub_spmf"
  3.1396 +proof(rule ord_pmf_increaseI)
  3.1397 +  fix x
  3.1398 +  from p have [simp]: "Y \<noteq> {}" by auto
  3.1399 +  from p have "ennreal (spmf p x) \<le> (SUP p:Y. ennreal (spmf p x))" by(rule SUP_upper)
  3.1400 +  also have "\<dots> = ennreal (spmf lub_spmf x)" using p
  3.1401 +    by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' simp del: SUP_eq_top_iff Sup_eq_top_iff)
  3.1402 +  finally show "spmf p x \<le> spmf lub_spmf x" by simp
  3.1403 +qed simp
  3.1404 +
  3.1405 +lemma lub_spmf_least:
  3.1406 +  assumes z: "\<And>x. x \<in> Y \<Longrightarrow> ord_spmf op = x z"
  3.1407 +  shows "ord_spmf op = lub_spmf z"
  3.1408 +proof(cases "Y = {}")
  3.1409 +  case nonempty: False
  3.1410 +  show ?thesis
  3.1411 +  proof(rule ord_pmf_increaseI)
  3.1412 +    fix x
  3.1413 +    from nonempty obtain p where p: "p \<in> Y" by auto
  3.1414 +    have "ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
  3.1415 +      by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' nonempty simp del: SUP_eq_top_iff Sup_eq_top_iff)
  3.1416 +    also have "\<dots> \<le> ennreal (spmf z x)" by(rule SUP_least)(simp add: ord_spmf_eq_leD z)
  3.1417 +    finally show "spmf lub_spmf x \<le> spmf z x" by simp
  3.1418 +  qed simp
  3.1419 +qed simp
  3.1420 +
  3.1421 +lemma set_lub_spmf: "set_spmf lub_spmf = (\<Union>p\<in>Y. set_spmf p)" (is "?lhs = ?rhs")
  3.1422 +proof(cases "Y = {}")
  3.1423 +  case [simp]: False
  3.1424 +  show ?thesis
  3.1425 +  proof(rule set_eqI)
  3.1426 +    fix x
  3.1427 +    have "x \<in> ?lhs \<longleftrightarrow> ennreal (spmf lub_spmf x) > 0"
  3.1428 +      by(simp_all add: in_set_spmf_iff_spmf less_le)
  3.1429 +    also have "\<dots> \<longleftrightarrow> (\<exists>p\<in>Y. ennreal (spmf p x) > 0)"
  3.1430 +      by(simp add: ennreal_spmf_lub_spmf less_SUP_iff)
  3.1431 +    also have "\<dots> \<longleftrightarrow> x \<in> ?rhs"
  3.1432 +      by(auto simp add: in_set_spmf_iff_spmf less_le)
  3.1433 +    finally show "x \<in> ?lhs \<longleftrightarrow> x \<in> ?rhs" .
  3.1434 +  qed
  3.1435 +qed simp
  3.1436 +
  3.1437 +lemma emeasure_lub_spmf:
  3.1438 +  assumes Y: "Y \<noteq> {}"
  3.1439 +  shows "emeasure (measure_spmf lub_spmf) A = (SUP y:Y. emeasure (measure_spmf y) A)"
  3.1440 +  (is "?lhs = ?rhs")
  3.1441 +proof -
  3.1442 +  let ?M = "count_space (set_spmf lub_spmf)"
  3.1443 +  have "?lhs = \<integral>\<^sup>+ x. ennreal (spmf lub_spmf x) * indicator A x \<partial>?M"
  3.1444 +    by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf')
  3.1445 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP y:Y. ennreal (spmf y x) * indicator A x) \<partial>?M"
  3.1446 +    unfolding ennreal_indicator[symmetric]
  3.1447 +    by(simp add: spmf_lub_spmf assms ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal)
  3.1448 +  also from assms have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
  3.1449 +  proof(rule nn_integral_monotone_convergence_SUP_countable)
  3.1450 +    have "(\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y = (\<lambda>f x. f x * indicator A x) ` (\<lambda>p x. ennreal (spmf p x)) ` Y"
  3.1451 +      by(simp add: image_image)
  3.1452 +    also have "Complete_Partial_Order.chain op \<le> \<dots>" using chain_ord_spmf_eqD
  3.1453 +      by(rule chain_imageI)(auto simp add: le_fun_def split: split_indicator)
  3.1454 +    finally show "Complete_Partial_Order.chain op \<le> ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
  3.1455 +  qed simp
  3.1456 +  also have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
  3.1457 +    by(auto simp add: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: SUP_cong nn_integral_cong)
  3.1458 +  also have "\<dots> = ?rhs"
  3.1459 +    by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf)
  3.1460 +  finally show ?thesis .
  3.1461 +qed
  3.1462 +
  3.1463 +lemma measure_lub_spmf:
  3.1464 +  assumes Y: "Y \<noteq> {}"
  3.1465 +  shows "measure (measure_spmf lub_spmf) A = (SUP y:Y. measure (measure_spmf y) A)" (is "?lhs = ?rhs")
  3.1466 +proof -
  3.1467 +  have "ennreal ?lhs = ennreal ?rhs"
  3.1468 +    using emeasure_lub_spmf[OF assms] SUP_emeasure_spmf_neq_top[of A Y] Y
  3.1469 +    unfolding measure_spmf.emeasure_eq_measure by(subst ennreal_SUP)
  3.1470 +  moreover have "0 \<le> ?rhs" using Y
  3.1471 +    by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] measure_spmf.subprob_measure_le_1)
  3.1472 +  ultimately show ?thesis by(simp)
  3.1473 +qed
  3.1474 +
  3.1475 +lemma weight_lub_spmf:
  3.1476 +  assumes Y: "Y \<noteq> {}"
  3.1477 +  shows "weight_spmf lub_spmf = (SUP y:Y. weight_spmf y)"
  3.1478 +unfolding weight_spmf_def by(rule measure_lub_spmf) fact
  3.1479 +
  3.1480 +lemma measure_spmf_lub_spmf:
  3.1481 +  assumes Y: "Y \<noteq> {}"
  3.1482 +  shows "measure_spmf lub_spmf = (SUP p:Y. measure_spmf p)" (is "?lhs = ?rhs")
  3.1483 +proof(rule measure_eqI)
  3.1484 +  from assms obtain p where p: "p \<in> Y" by auto
  3.1485 +  from chain have chain': "Complete_Partial_Order.chain op \<le> (measure_spmf ` Y)"
  3.1486 +    by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf)
  3.1487 +  show "sets ?lhs = sets ?rhs" and "emeasure ?lhs A = emeasure ?rhs A" for A
  3.1488 +    using chain' Y p by(simp_all add: sets_SUP emeasure_SUP emeasure_lub_spmf)
  3.1489 +qed
  3.1490 +
  3.1491 +end
  3.1492 +
  3.1493 +end
  3.1494 +
  3.1495 +lemma partial_function_definitions_spmf: "partial_function_definitions (ord_spmf op =) lub_spmf"
  3.1496 +  (is "partial_function_definitions ?R _")
  3.1497 +proof
  3.1498 +  fix x show "?R x x" by(simp add: ord_spmf_reflI)
  3.1499 +next
  3.1500 +  fix x y z
  3.1501 +  assume "?R x y" "?R y z"
  3.1502 +  with transp_ord_option[OF transp_equality] show "?R x z" by(rule transp_rel_pmf[THEN transpD])
  3.1503 +next
  3.1504 +  fix x y
  3.1505 +  assume "?R x y" "?R y x"
  3.1506 +  thus "x = y"
  3.1507 +    by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymP_ord_option)
  3.1508 +next
  3.1509 +  fix Y x
  3.1510 +  assume "Complete_Partial_Order.chain ?R Y" "x \<in> Y"
  3.1511 +  then show "?R x (lub_spmf Y)"
  3.1512 +    by(rule lub_spmf_upper)
  3.1513 +next
  3.1514 +  fix Y z
  3.1515 +  assume "Complete_Partial_Order.chain ?R Y" "\<And>x. x \<in> Y \<Longrightarrow> ?R x z"
  3.1516 +  then show "?R (lub_spmf Y) z"
  3.1517 +    by(cases "Y = {}")(simp_all add: lub_spmf_least)
  3.1518 +qed
  3.1519 +
  3.1520 +lemma ccpo_spmf: "class.ccpo lub_spmf (ord_spmf op =) (mk_less (ord_spmf op =))"
  3.1521 +by(rule ccpo partial_function_definitions_spmf)+
  3.1522 +
  3.1523 +interpretation spmf: partial_function_definitions "ord_spmf op =" "lub_spmf"
  3.1524 +  rewrites "lub_spmf {} \<equiv> return_pmf None"
  3.1525 +by(rule partial_function_definitions_spmf) simp
  3.1526 +
  3.1527 +declaration {* Partial_Function.init "spmf" @{term spmf.fixp_fun}
  3.1528 +  @{term spmf.mono_body} @{thm spmf.fixp_rule_uc} @{thm spmf.fixp_induct_uc}
  3.1529 +  NONE *}
  3.1530 +
  3.1531 +declare spmf.leq_refl[simp]
  3.1532 +declare admissible_leI[OF ccpo_spmf, cont_intro]
  3.1533 +
  3.1534 +abbreviation "mono_spmf \<equiv> monotone (fun_ord (ord_spmf op =)) (ord_spmf op =)"
  3.1535 +
  3.1536 +lemma lub_spmf_const [simp]: "lub_spmf {p} = p"
  3.1537 +by(rule spmf_eqI)(simp add: spmf_lub_spmf[OF ccpo.chain_singleton[OF ccpo_spmf]])
  3.1538 +
  3.1539 +lemma bind_spmf_mono':
  3.1540 +  assumes fg: "ord_spmf op = f g"
  3.1541 +  and hk: "\<And>x :: 'a. ord_spmf op = (h x) (k x)"
  3.1542 +  shows "ord_spmf op = (f \<bind> h) (g \<bind> k)"
  3.1543 +unfolding bind_spmf_def using assms(1)
  3.1544 +by(rule rel_pmf_bindI)(auto split: option.split simp add: hk)
  3.1545 +
  3.1546 +lemma bind_spmf_mono [partial_function_mono]:
  3.1547 +  assumes mf: "mono_spmf B" and mg: "\<And>y. mono_spmf (\<lambda>f. C y f)"
  3.1548 +  shows "mono_spmf (\<lambda>f. bind_spmf (B f) (\<lambda>y. C y f))"
  3.1549 +proof (rule monotoneI)
  3.1550 +  fix f g :: "'a \<Rightarrow> 'b spmf"
  3.1551 +  assume fg: "fun_ord (ord_spmf op =) f g"
  3.1552 +  with mf have "ord_spmf op = (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
  3.1553 +  moreover from mg have "\<And>y'. ord_spmf op = (C y' f) (C y' g)"
  3.1554 +    by (rule monotoneD) (rule fg)
  3.1555 +  ultimately show "ord_spmf op = (bind_spmf (B f) (\<lambda>y. C y f)) (bind_spmf (B g) (\<lambda>y'. C y' g))"
  3.1556 +    by(rule bind_spmf_mono')
  3.1557 +qed
  3.1558 +  
  3.1559 +lemma monotone_bind_spmf1: "monotone (ord_spmf op =) (ord_spmf op =) (\<lambda>y. bind_spmf y g)"
  3.1560 +by(rule monotoneI)(simp add: bind_spmf_mono' ord_spmf_reflI)
  3.1561 +
  3.1562 +lemma monotone_bind_spmf2: 
  3.1563 +  assumes g: "\<And>x. monotone ord (ord_spmf op =) (\<lambda>y. g y x)"
  3.1564 +  shows "monotone ord (ord_spmf op =) (\<lambda>y. bind_spmf p (g y))"
  3.1565 +by(rule monotoneI)(auto intro: bind_spmf_mono' monotoneD[OF g] ord_spmf_reflI)
  3.1566 +
  3.1567 +lemma bind_lub_spmf:
  3.1568 +  assumes chain: "Complete_Partial_Order.chain (ord_spmf op =) Y"
  3.1569 +  shows "bind_spmf (lub_spmf Y) f = lub_spmf ((\<lambda>p. bind_spmf p f) ` Y)" (is "?lhs = ?rhs")
  3.1570 +proof(cases "Y = {}")
  3.1571 +  case Y: False
  3.1572 +  show ?thesis
  3.1573 +  proof(rule spmf_eqI)
  3.1574 +    fix i
  3.1575 +    have chain': "Complete_Partial_Order.chain op \<le> ((\<lambda>p x. ennreal (spmf p x * spmf (f x) i)) ` Y)"
  3.1576 +      using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD intro: mult_right_mono)
  3.1577 +    have chain'': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. p \<bind> f) ` Y)"
  3.1578 +      using chain by(rule chain_imageI)(auto intro!: monotoneI bind_spmf_mono' ord_spmf_reflI)
  3.1579 +    let ?M = "count_space (set_spmf (lub_spmf Y))"
  3.1580 +    have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ x. ennreal (spmf (lub_spmf Y) x) * ennreal (spmf (f x) i) \<partial>?M"
  3.1581 +      by(auto simp add: ennreal_spmf_lub_spmf ennreal_spmf_bind nn_integral_measure_spmf')
  3.1582 +    also have "\<dots> = \<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"
  3.1583 +      by(subst ennreal_spmf_lub_spmf[OF chain Y])(subst SUP_mult_right_ennreal, simp_all add: ennreal_mult Y)
  3.1584 +    also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
  3.1585 +      using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
  3.1586 +    also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf p f) i))"
  3.1587 +      by(auto simp add: ennreal_spmf_bind nn_integral_measure_spmf nn_integral_count_space_indicator set_lub_spmf[OF chain] in_set_spmf_iff_spmf ennreal_mult intro!: SUP_cong nn_integral_cong split: split_indicator)
  3.1588 +    also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
  3.1589 +    finally show "spmf ?lhs i = spmf ?rhs i" by simp
  3.1590 +  qed
  3.1591 +qed simp
  3.1592 +
  3.1593 +lemma map_lub_spmf:
  3.1594 +  "Complete_Partial_Order.chain (ord_spmf op =) Y
  3.1595 +  \<Longrightarrow> map_spmf f (lub_spmf Y) = lub_spmf (map_spmf f ` Y)"
  3.1596 +unfolding map_spmf_conv_bind_spmf[abs_def] by(simp add: bind_lub_spmf o_def)
  3.1597 +
  3.1598 +lemma mcont_bind_spmf1: "mcont lub_spmf (ord_spmf op =) lub_spmf (ord_spmf op =) (\<lambda>y. bind_spmf y f)"
  3.1599 +using monotone_bind_spmf1 by(rule mcontI)(rule contI, simp add: bind_lub_spmf)
  3.1600 +
  3.1601 +lemma bind_lub_spmf2:
  3.1602 +  assumes chain: "Complete_Partial_Order.chain ord Y"
  3.1603 +  and g: "\<And>y. monotone ord (ord_spmf op =) (g y)"
  3.1604 +  shows "bind_spmf x (\<lambda>y. lub_spmf (g y ` Y)) = lub_spmf ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
  3.1605 +  (is "?lhs = ?rhs")
  3.1606 +proof(cases "Y = {}")
  3.1607 +  case Y: False
  3.1608 +  show ?thesis
  3.1609 +  proof(rule spmf_eqI)
  3.1610 +    fix i
  3.1611 +    have chain': "\<And>y. Complete_Partial_Order.chain (ord_spmf op =) (g y ` Y)"
  3.1612 +      using chain g[THEN monotoneD] by(rule chain_imageI)
  3.1613 +    have chain'': "Complete_Partial_Order.chain op \<le> ((\<lambda>p y. ennreal (spmf x y * spmf (g y p) i)) ` Y)"
  3.1614 +      using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono)
  3.1615 +    have chain''': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
  3.1616 +      using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
  3.1617 +  
  3.1618 +    have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p:Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
  3.1619 +      by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
  3.1620 +    also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
  3.1621 +      unfolding nn_integral_measure_spmf' using Y chain''
  3.1622 +      by(rule nn_integral_monotone_convergence_SUP_countable) simp
  3.1623 +    also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
  3.1624 +      by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult)
  3.1625 +    also have "\<dots> = ennreal (spmf ?rhs i)" using chain'''
  3.1626 +      by(auto simp add: ennreal_spmf_lub_spmf Y)
  3.1627 +    finally show "spmf ?lhs i = spmf ?rhs i" by simp
  3.1628 +  qed
  3.1629 +qed simp
  3.1630 +
  3.1631 +lemma mcont_bind_spmf [cont_intro]:
  3.1632 +  assumes f: "mcont luba orda lub_spmf (ord_spmf op =) f"
  3.1633 +  and g: "\<And>y. mcont luba orda lub_spmf (ord_spmf op =) (g y)"
  3.1634 +  shows "mcont luba orda lub_spmf (ord_spmf op =) (\<lambda>x. bind_spmf (f x) (\<lambda>y. g y x))"
  3.1635 +proof(rule spmf.mcont2mcont'[OF _ _ f])
  3.1636 +  fix z
  3.1637 +  show "mcont lub_spmf (ord_spmf op =) lub_spmf (ord_spmf op =) (\<lambda>x. bind_spmf x (\<lambda>y. g y z))"
  3.1638 +    by(rule mcont_bind_spmf1)
  3.1639 +next
  3.1640 +  fix x
  3.1641 +  let ?f = "\<lambda>z. bind_spmf x (\<lambda>y. g y z)"
  3.1642 +  have "monotone orda (ord_spmf op =) ?f" using mcont_mono[OF g] by(rule monotone_bind_spmf2)
  3.1643 +  moreover have "cont luba orda lub_spmf (ord_spmf op =) ?f"
  3.1644 +  proof(rule contI)
  3.1645 +    fix Y
  3.1646 +    assume chain: "Complete_Partial_Order.chain orda Y" and Y: "Y \<noteq> {}"
  3.1647 +    have "bind_spmf x (\<lambda>y. g y (luba Y)) = bind_spmf x (\<lambda>y. lub_spmf (g y ` Y))"
  3.1648 +      by(rule bind_spmf_cong)(simp_all add: mcont_contD[OF g chain Y])
  3.1649 +    also have "\<dots> = lub_spmf ((\<lambda>p. x \<bind> (\<lambda>y. g y p)) ` Y)" using chain
  3.1650 +      by(rule bind_lub_spmf2)(rule mcont_mono[OF g])
  3.1651 +    finally show "bind_spmf x (\<lambda>y. g y (luba Y)) = \<dots>" .
  3.1652 +  qed
  3.1653 +  ultimately show "mcont luba orda lub_spmf (ord_spmf op =) ?f" by(rule mcontI)
  3.1654 +qed
  3.1655 +
  3.1656 +lemma bind_pmf_mono [partial_function_mono]:
  3.1657 +  "(\<And>y. mono_spmf (\<lambda>f. C y f)) \<Longrightarrow> mono_spmf (\<lambda>f. bind_pmf p (\<lambda>x. C x f))"
  3.1658 +using bind_spmf_mono[of "\<lambda>_. spmf_of_pmf p" C] by simp
  3.1659 +
  3.1660 +lemma map_spmf_mono [partial_function_mono]: "mono_spmf B \<Longrightarrow> mono_spmf (\<lambda>g. map_spmf f (B g))"
  3.1661 +unfolding map_spmf_conv_bind_spmf by(rule bind_spmf_mono) simp_all
  3.1662 +
  3.1663 +lemma mcont_map_spmf [cont_intro]:
  3.1664 +  "mcont luba orda lub_spmf (ord_spmf op =) g
  3.1665 +  \<Longrightarrow> mcont luba orda lub_spmf (ord_spmf op =) (\<lambda>x. map_spmf f (g x))"
  3.1666 +unfolding map_spmf_conv_bind_spmf by(rule mcont_bind_spmf) simp_all
  3.1667 +
  3.1668 +lemma monotone_set_spmf: "monotone (ord_spmf op =) op \<subseteq> set_spmf"
  3.1669 +by(rule monotoneI)(rule ord_spmf_eqD_set_spmf)
  3.1670 +
  3.1671 +lemma cont_set_spmf: "cont lub_spmf (ord_spmf op =) Union op \<subseteq> set_spmf"
  3.1672 +by(rule contI)(subst set_lub_spmf; simp)
  3.1673 +
  3.1674 +lemma mcont2mcont_set_spmf[THEN mcont2mcont, cont_intro]:
  3.1675 +  shows mcont_set_spmf: "mcont lub_spmf (ord_spmf op =) Union op \<subseteq> set_spmf"
  3.1676 +by(rule mcontI monotone_set_spmf cont_set_spmf)+
  3.1677 +
  3.1678 +lemma monotone_spmf: "monotone (ord_spmf op =) op \<le> (\<lambda>p. spmf p x)"
  3.1679 +by(rule monotoneI)(simp add: ord_spmf_eq_leD)
  3.1680 +
  3.1681 +lemma cont_spmf: "cont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. spmf p x)"
  3.1682 +by(rule contI)(simp add: spmf_lub_spmf)
  3.1683 +
  3.1684 +lemma mcont_spmf: "mcont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. spmf p x)"
  3.1685 +by(rule mcontI monotone_spmf cont_spmf)+
  3.1686 +
  3.1687 +lemma cont_ennreal_spmf: "cont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. ennreal (spmf p x))"
  3.1688 +by(rule contI)(simp add: ennreal_spmf_lub_spmf)
  3.1689 +
  3.1690 +lemma mcont2mcont_ennreal_spmf [THEN mcont2mcont, cont_intro]:
  3.1691 +  shows mcont_ennreal_spmf: "mcont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. ennreal (spmf p x))"
  3.1692 +by(rule mcontI mono2mono_ennreal monotone_spmf cont_ennreal_spmf)+
  3.1693 +
  3.1694 +lemma nn_integral_map_spmf [simp]: "nn_integral (measure_spmf (map_spmf f p)) g = nn_integral (measure_spmf p) (g \<circ> f)"
  3.1695 +by(auto 4 3 simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space intro: nn_integral_cong split: split_indicator)
  3.1696 +
  3.1697 +subsubsection \<open>Admissibility of @{term rel_spmf}\<close>
  3.1698 +
  3.1699 +lemma rel_spmf_measureD:
  3.1700 +  assumes "rel_spmf R p q"
  3.1701 +  shows "measure (measure_spmf p) A \<le> measure (measure_spmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs")
  3.1702 +proof -
  3.1703 +  have "?lhs = measure (measure_pmf p) (Some ` A)" by(simp add: measure_measure_spmf_conv_measure_pmf)
  3.1704 +  also have "\<dots> \<le> measure (measure_pmf q) {y. \<exists>x\<in>Some ` A. rel_option R x y}"
  3.1705 +    using assms by(rule rel_pmf_measureD)
  3.1706 +  also have "\<dots> = ?rhs" unfolding measure_measure_spmf_conv_measure_pmf
  3.1707 +    by(rule arg_cong2[where f=measure])(auto simp add: option_rel_Some1)
  3.1708 +  finally show ?thesis .
  3.1709 +qed
  3.1710 +
  3.1711 +locale rel_spmf_characterisation =
  3.1712 +  assumes rel_pmf_measureI:
  3.1713 +    "\<And>(R :: 'a option \<Rightarrow> 'b option \<Rightarrow> bool) p q. 
  3.1714 +    (\<And>A. measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y})
  3.1715 +    \<Longrightarrow> rel_pmf R p q"
  3.1716 +  -- \<open>This assumption is shown to hold in general in the AFP entry @{text "MFMC_Countable"}.\<close>
  3.1717 +begin
  3.1718 +
  3.1719 +context fixes R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" begin
  3.1720 +
  3.1721 +lemma rel_spmf_measureI:
  3.1722 +  assumes eq1: "\<And>A. measure (measure_spmf p) A \<le> measure (measure_spmf q) {y. \<exists>x\<in>A. R x y}"
  3.1723 +  assumes eq2: "weight_spmf q \<le> weight_spmf p"
  3.1724 +  shows "rel_spmf R p q"
  3.1725 +proof(rule rel_pmf_measureI)
  3.1726 +  fix A :: "'a option set"
  3.1727 +  define A' where "A' = the ` (A \<inter> range Some)"
  3.1728 +  define A'' where "A'' = A \<inter> {None}"
  3.1729 +  have A: "A = Some ` A' \<union> A''" "Some ` A' \<inter> A'' = {}"
  3.1730 +    unfolding A'_def A''_def by(auto 4 3 intro: rev_image_eqI)
  3.1731 +  have "measure (measure_pmf p) A = measure (measure_pmf p) (Some ` A') + measure (measure_pmf p) A''"
  3.1732 +    by(simp add: A measure_pmf.finite_measure_Union)
  3.1733 +  also have "measure (measure_pmf p) (Some ` A') = measure (measure_spmf p) A'"
  3.1734 +    by(simp add: measure_measure_spmf_conv_measure_pmf)
  3.1735 +  also have "\<dots> \<le> measure (measure_spmf q) {y. \<exists>x\<in>A'. R x y}" by(rule eq1)
  3.1736 +  also (ord_eq_le_trans[OF _ add_right_mono])
  3.1737 +  have "\<dots> = measure (measure_pmf q) {y. \<exists>x\<in>A'. rel_option R (Some x) y}"
  3.1738 +    unfolding measure_measure_spmf_conv_measure_pmf
  3.1739 +    by(rule arg_cong2[where f=measure])(auto simp add: A'_def option_rel_Some1)
  3.1740 +  also
  3.1741 +  { have "weight_spmf p \<le> measure (measure_spmf q) {y. \<exists>x. R x y}"
  3.1742 +      using eq1[of UNIV] unfolding weight_spmf_def by simp
  3.1743 +    also have "\<dots> \<le> weight_spmf q" unfolding weight_spmf_def
  3.1744 +      by(rule measure_spmf.finite_measure_mono) simp_all
  3.1745 +    finally have "weight_spmf p = weight_spmf q" using eq2 by simp }
  3.1746 +  then have "measure (measure_pmf p) A'' = measure (measure_pmf q) (if None \<in> A then {None} else {})"
  3.1747 +    unfolding A''_def by(simp add: pmf_None_eq_weight_spmf measure_pmf_single)
  3.1748 +  also have "measure (measure_pmf q) {y. \<exists>x\<in>A'. rel_option R (Some x) y} + \<dots> = measure (measure_pmf q) {y. \<exists>x\<in>A. rel_option R x y}"
  3.1749 +    by(subst measure_pmf.finite_measure_Union[symmetric])
  3.1750 +      (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)
  3.1751 +  finally show "measure (measure_pmf p) A \<le> \<dots>" .
  3.1752 +qed
  3.1753 +
  3.1754 +lemma admissible_rel_spmf:
  3.1755 +  "ccpo.admissible (prod_lub lub_spmf lub_spmf) (rel_prod (ord_spmf op =) (ord_spmf op =)) (case_prod (rel_spmf R))"
  3.1756 +  (is "ccpo.admissible ?lub ?ord ?P")
  3.1757 +proof(rule ccpo.admissibleI)
  3.1758 +  fix Y
  3.1759 +  assume chain: "Complete_Partial_Order.chain ?ord Y"
  3.1760 +    and Y: "Y \<noteq> {}"
  3.1761 +    and R: "\<forall>(p, q) \<in> Y. rel_spmf R p q"
  3.1762 +  from R have R: "\<And>p q. (p, q) \<in> Y \<Longrightarrow> rel_spmf R p q" by auto
  3.1763 +  have chain1: "Complete_Partial_Order.chain (ord_spmf op =) (fst ` Y)"
  3.1764 +    and chain2: "Complete_Partial_Order.chain (ord_spmf op =) (snd ` Y)"
  3.1765 +    using chain by(rule chain_imageI; clarsimp)+
  3.1766 +  from Y have Y1: "fst ` Y \<noteq> {}" and Y2: "snd ` Y \<noteq> {}" by auto
  3.1767 +
  3.1768 +  have "rel_spmf R (lub_spmf (fst ` Y)) (lub_spmf (snd ` Y))"
  3.1769 +  proof(rule rel_spmf_measureI)
  3.1770 +    show "weight_spmf (lub_spmf (snd ` Y)) \<le> weight_spmf (lub_spmf (fst ` Y))"
  3.1771 +      by(auto simp add: weight_lub_spmf chain1 chain2 Y rel_spmf_weightD[OF R, symmetric] intro!: cSUP_least intro: cSUP_upper2[OF bdd_aboveI2[OF weight_spmf_le_1]])
  3.1772 +
  3.1773 +    fix A
  3.1774 +    have "measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y:fst ` Y. measure (measure_spmf y) A)"
  3.1775 +      using chain1 Y1 by(rule measure_lub_spmf)
  3.1776 +    also have "\<dots> \<le> (SUP y:snd ` Y. measure (measure_spmf y) {y. \<exists>x\<in>A. R x y})" using Y1
  3.1777 +      by(rule cSUP_least)(auto intro!: cSUP_upper2[OF bdd_aboveI2[OF measure_spmf.subprob_measure_le_1]] rel_spmf_measureD R)
  3.1778 +    also have "\<dots> = measure (measure_spmf (lub_spmf (snd ` Y))) {y. \<exists>x\<in>A. R x y}"
  3.1779 +      using chain2 Y2 by(rule measure_lub_spmf[symmetric])
  3.1780 +    finally show "measure (measure_spmf (lub_spmf (fst ` Y))) A \<le> \<dots>" .
  3.1781 +  qed
  3.1782 +  then show "?P (?lub Y)" by(simp add: prod_lub_def)
  3.1783 +qed
  3.1784 +
  3.1785 +lemma admissible_rel_spmf_mcont [cont_intro]:
  3.1786 +  "\<lbrakk> mcont lub ord lub_spmf (ord_spmf op =) f; mcont lub ord lub_spmf (ord_spmf op =) g \<rbrakk>
  3.1787 +  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. rel_spmf R (f x) (g x))"
  3.1788 +by(rule admissible_subst[OF admissible_rel_spmf, where f="\<lambda>x. (f x, g x)", simplified])(rule mcont_Pair)
  3.1789 +
  3.1790 +context begin interpretation lifting_syntax .
  3.1791 +
  3.1792 +lemma fixp_spmf_parametric':
  3.1793 +  assumes f: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) F"
  3.1794 +  and g: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) G"
  3.1795 +  and param: "(rel_spmf R ===> rel_spmf R) F G"
  3.1796 +  shows "(rel_spmf R) (ccpo.fixp lub_spmf (ord_spmf op =) F) (ccpo.fixp lub_spmf (ord_spmf op =) G)"
  3.1797 +by(rule parallel_fixp_induct[OF ccpo_spmf ccpo_spmf _ f g])(auto intro: param[THEN rel_funD])
  3.1798 +
  3.1799 +lemma fixp_spmf_parametric:
  3.1800 +  assumes f: "\<And>x. mono_spmf (\<lambda>f. F f x)"
  3.1801 +  and g: "\<And>x. mono_spmf (\<lambda>f. G f x)"
  3.1802 +  and param: "((A ===> rel_spmf R) ===> A ===> rel_spmf R) F G"
  3.1803 +  shows "(A ===> rel_spmf R) (spmf.fixp_fun F) (spmf.fixp_fun G)"
  3.1804 +using f g
  3.1805 +proof(rule parallel_fixp_induct_1_1[OF partial_function_definitions_spmf partial_function_definitions_spmf _ _ reflexive reflexive, where P="(A ===> rel_spmf R)"])
  3.1806 +  show "ccpo.admissible (prod_lub (fun_lub lub_spmf) (fun_lub lub_spmf)) (rel_prod (fun_ord (ord_spmf op =)) (fun_ord (ord_spmf op =))) (\<lambda>x. (A ===> rel_spmf R) (fst x) (snd x))"
  3.1807 +    unfolding rel_fun_def
  3.1808 +    apply(rule admissible_all admissible_imp admissible_rel_spmf_mcont)+
  3.1809 +    apply(rule spmf.mcont2mcont[OF mcont_call])
  3.1810 +     apply(rule mcont_fst)
  3.1811 +    apply(rule spmf.mcont2mcont[OF mcont_call])
  3.1812 +     apply(rule mcont_snd)
  3.1813 +    done
  3.1814 +  show "(A ===> rel_spmf R) (\<lambda>_. lub_spmf {}) (\<lambda>_. lub_spmf {})" by auto
  3.1815 +  show "(A ===> rel_spmf R) (F f) (G g)" if "(A ===> rel_spmf R) f g" for f g
  3.1816 +    using that by(rule rel_funD[OF param])
  3.1817 +qed
  3.1818 +
  3.1819 +end
  3.1820 +
  3.1821 +end
  3.1822 +
  3.1823 +end
  3.1824 +
  3.1825 +subsection {* Restrictions on spmfs *}
  3.1826 +
  3.1827 +definition restrict_spmf :: "'a spmf \<Rightarrow> 'a set \<Rightarrow> 'a spmf" (infixl "\<upharpoonleft>" 110)
  3.1828 +where "p \<upharpoonleft> A = map_pmf (\<lambda>x. x \<bind> (\<lambda>y. if y \<in> A then Some y else None)) p"
  3.1829 +
  3.1830 +lemma set_restrict_spmf [simp]: "set_spmf (p \<upharpoonleft> A) = set_spmf p \<inter> A"
  3.1831 +by(fastforce simp add: restrict_spmf_def set_spmf_def split: bind_splits if_split_asm)
  3.1832 +
  3.1833 +lemma restrict_map_spmf: "map_spmf f p \<upharpoonleft> A = map_spmf f (p \<upharpoonleft> (f -` A))"
  3.1834 +by(simp add: restrict_spmf_def pmf.map_comp o_def map_option_bind bind_map_option if_distrib cong del: if_weak_cong)
  3.1835 +
  3.1836 +lemma restrict_restrict_spmf [simp]: "p \<upharpoonleft> A \<upharpoonleft> B = p \<upharpoonleft> (A \<inter> B)"
  3.1837 +by(auto simp add: restrict_spmf_def pmf.map_comp o_def intro!: pmf.map_cong bind_option_cong)
  3.1838 +
  3.1839 +lemma restrict_spmf_empty [simp]: "p \<upharpoonleft> {} = return_pmf None"
  3.1840 +by(simp add: restrict_spmf_def)
  3.1841 +
  3.1842 +lemma restrict_spmf_UNIV [simp]: "p \<upharpoonleft> UNIV = p"
  3.1843 +by(simp add: restrict_spmf_def)
  3.1844 +
  3.1845 +lemma spmf_restrict_spmf_outside [simp]: "x \<notin> A \<Longrightarrow> spmf (p \<upharpoonleft> A) x = 0"
  3.1846 +by(simp add: spmf_eq_0_set_spmf)
  3.1847 +
  3.1848 +lemma emeasure_restrict_spmf [simp]:
  3.1849 +  "emeasure (measure_spmf (p \<upharpoonleft> A)) X = emeasure (measure_spmf p) (X \<inter> A)"
  3.1850 +by(auto simp add: restrict_spmf_def measure_spmf_def emeasure_distr measurable_restrict_space1 emeasure_restrict_space space_restrict_space intro: arg_cong2[where f=emeasure] split: bind_splits if_split_asm)
  3.1851 +
  3.1852 +lemma measure_restrict_spmf [simp]:
  3.1853 +  "measure (measure_spmf (p \<upharpoonleft> A)) X = measure (measure_spmf p) (X \<inter> A)"
  3.1854 +using emeasure_restrict_spmf[of p A X]
  3.1855 +by(simp only: measure_spmf.emeasure_eq_measure ennreal_inj measure_nonneg)
  3.1856 +
  3.1857 +lemma spmf_restrict_spmf: "spmf (p \<upharpoonleft> A) x = (if x \<in> A then spmf p x else 0)"
  3.1858 +by(simp add: spmf_conv_measure_spmf)
  3.1859 +
  3.1860 +lemma spmf_restrict_spmf_inside [simp]: "x \<in> A \<Longrightarrow> spmf (p \<upharpoonleft> A) x = spmf p x"
  3.1861 +by(simp add: spmf_restrict_spmf)
  3.1862 +
  3.1863 +lemma pmf_restrict_spmf_None: "pmf (p \<upharpoonleft> A) None = pmf p None + measure (measure_spmf p) (- A)"
  3.1864 +proof -
  3.1865 +  have [simp]: "None \<notin> Some ` (- A)" by auto
  3.1866 +  have "(\<lambda>x. x \<bind> (\<lambda>y. if y \<in> A then Some y else None)) -` {None} = {None} \<union> (Some ` (- A))"
  3.1867 +    by(auto split: bind_splits if_split_asm)
  3.1868 +  then show ?thesis unfolding ereal.inject[symmetric]
  3.1869 +    by(simp add: restrict_spmf_def ennreal_pmf_map emeasure_pmf_single del: ereal.inject)
  3.1870 +      (simp add: pmf.rep_eq measure_pmf.finite_measure_Union[symmetric] measure_measure_spmf_conv_measure_pmf measure_pmf.emeasure_eq_measure)
  3.1871 +qed
  3.1872 +
  3.1873 +lemma restrict_spmf_trivial: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> x \<in> A) \<Longrightarrow> p \<upharpoonleft> A = p"
  3.1874 +by(rule spmf_eqI)(auto simp add: spmf_restrict_spmf spmf_eq_0_set_spmf)
  3.1875 +
  3.1876 +lemma restrict_spmf_trivial': "set_spmf p \<subseteq> A \<Longrightarrow> p \<upharpoonleft> A = p"
  3.1877 +by(rule restrict_spmf_trivial) blast
  3.1878 +
  3.1879 +lemma restrict_return_spmf: "return_spmf x \<upharpoonleft> A = (if x \<in> A then return_spmf x else return_pmf None)"
  3.1880 +by(simp add: restrict_spmf_def)
  3.1881 +
  3.1882 +lemma restrict_return_spmf_inside [simp]: "x \<in> A \<Longrightarrow> return_spmf x \<upharpoonleft> A = return_spmf x"
  3.1883 +by(simp add: restrict_return_spmf)
  3.1884 +
  3.1885 +lemma restrict_return_spmf_outside [simp]: "x \<notin> A \<Longrightarrow> return_spmf x \<upharpoonleft> A = return_pmf None"
  3.1886 +by(simp add: restrict_return_spmf)
  3.1887 +
  3.1888 +lemma restrict_spmf_return_pmf_None [simp]: "return_pmf None \<upharpoonleft> A = return_pmf None"
  3.1889 +by(simp add: restrict_spmf_def)
  3.1890 +
  3.1891 +lemma restrict_bind_pmf: "bind_pmf p g \<upharpoonleft> A = p \<bind> (\<lambda>x. g x \<upharpoonleft> A)"
  3.1892 +by(simp add: restrict_spmf_def map_bind_pmf o_def)
  3.1893 +
  3.1894 +lemma restrict_bind_spmf: "bind_spmf p g \<upharpoonleft> A = p \<bind> (\<lambda>x. g x \<upharpoonleft> A)"
  3.1895 +by(auto simp add: bind_spmf_def restrict_bind_pmf cong del: option.case_cong_weak cong: option.case_cong intro!: bind_pmf_cong split: option.split)
  3.1896 +
  3.1897 +lemma bind_restrict_pmf: "bind_pmf (p \<upharpoonleft> A) g = p \<bind> (\<lambda>x. if x \<in> Some ` A then g x else g None)"
  3.1898 +by(auto simp add: restrict_spmf_def bind_map_pmf fun_eq_iff split: bind_split intro: arg_cong2[where f=bind_pmf])
  3.1899 +
  3.1900 +lemma bind_restrict_spmf: "bind_spmf (p \<upharpoonleft> A) g = p \<bind> (\<lambda>x. if x \<in> A then g x else return_pmf None)"
  3.1901 +by(auto simp add: bind_spmf_def bind_restrict_pmf fun_eq_iff intro: arg_cong2[where f=bind_pmf] split: option.split)
  3.1902 +
  3.1903 +lemma spmf_map_restrict: "spmf (map_spmf fst (p \<upharpoonleft> (snd -` {y}))) x = spmf p (x, y)"
  3.1904 +by(subst spmf_map)(auto intro: arg_cong2[where f=measure] simp add: spmf_conv_measure_spmf)
  3.1905 +
  3.1906 +lemma measure_eqI_restrict_spmf:
  3.1907 +  assumes "rel_spmf R (restrict_spmf p A) (restrict_spmf q B)"
  3.1908 +  shows "measure (measure_spmf p) A = measure (measure_spmf q) B"
  3.1909 +proof -
  3.1910 +  from assms have "weight_spmf (restrict_spmf p A) = weight_spmf (restrict_spmf q B)" by(rule rel_spmf_weightD)
  3.1911 +  thus ?thesis by(simp add: weight_spmf_def)
  3.1912 +qed
  3.1913 +
  3.1914 +subsection {* Subprobability distributions of sets *}
  3.1915 +
  3.1916 +definition spmf_of_set :: "'a set \<Rightarrow> 'a spmf"
  3.1917 +where 
  3.1918 +  "spmf_of_set A = (if finite A \<and> A \<noteq> {} then spmf_of_pmf (pmf_of_set A) else return_pmf None)"
  3.1919 +
  3.1920 +lemma spmf_of_set: "spmf (spmf_of_set A) x = indicator A x / card A"
  3.1921 +by(auto simp add: spmf_of_set_def)
  3.1922 +
  3.1923 +lemma pmf_spmf_of_set_None [simp]: "pmf (spmf_of_set A) None = indicator {A. infinite A \<or> A = {}} A"
  3.1924 +by(simp add: spmf_of_set_def)
  3.1925 +
  3.1926 +lemma set_spmf_of_set: "set_spmf (spmf_of_set A) = (if finite A then A else {})"
  3.1927 +by(simp add: spmf_of_set_def)
  3.1928 +
  3.1929 +lemma set_spmf_of_set_finite [simp]: "finite A \<Longrightarrow> set_spmf (spmf_of_set A) = A"
  3.1930 +by(simp add: set_spmf_of_set)
  3.1931 +
  3.1932 +lemma spmf_of_set_singleton: "spmf_of_set {x} = return_spmf x"
  3.1933 +by(simp add: spmf_of_set_def pmf_of_set_singleton)
  3.1934 +
  3.1935 +lemma map_spmf_of_set_inj_on [simp]:
  3.1936 +  "inj_on f A \<Longrightarrow> map_spmf f (spmf_of_set A) = spmf_of_set (f ` A)"
  3.1937 +by(auto simp add: spmf_of_set_def map_pmf_of_set_inj dest: finite_imageD)
  3.1938 +
  3.1939 +lemma spmf_of_pmf_pmf_of_set [simp]: 
  3.1940 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> spmf_of_pmf (pmf_of_set A) = spmf_of_set A"
  3.1941 +by(simp add: spmf_of_set_def)
  3.1942 +
  3.1943 +lemma weight_spmf_of_set:
  3.1944 +  "weight_spmf (spmf_of_set A) = (if finite A \<and> A \<noteq> {} then 1 else 0)"
  3.1945 +by(auto simp only: spmf_of_set_def weight_spmf_of_pmf weight_return_pmf_None split: if_split)
  3.1946 +
  3.1947 +lemma weight_spmf_of_set_finite [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> weight_spmf (spmf_of_set A) = 1"
  3.1948 +by(simp add: weight_spmf_of_set)
  3.1949 +
  3.1950 +lemma weight_spmf_of_set_infinite [simp]: "infinite A \<Longrightarrow> weight_spmf (spmf_of_set A) = 0"
  3.1951 +by(simp add: weight_spmf_of_set)
  3.1952 +
  3.1953 +lemma measure_spmf_spmf_of_set:
  3.1954 +  "measure_spmf (spmf_of_set A) = (if finite A \<and> A \<noteq> {} then measure_pmf (pmf_of_set A) else null_measure (count_space UNIV))"
  3.1955 +by(simp add: spmf_of_set_def del: spmf_of_pmf_pmf_of_set)
  3.1956 +
  3.1957 +lemma emeasure_spmf_of_set:
  3.1958 +  "emeasure (measure_spmf (spmf_of_set S)) A = card (S \<inter> A) / card S"
  3.1959 +by(auto simp add: measure_spmf_spmf_of_set emeasure_pmf_of_set)
  3.1960 +
  3.1961 +lemma measure_spmf_of_set:
  3.1962 +  "measure (measure_spmf (spmf_of_set S)) A = card (S \<inter> A) / card S"
  3.1963 +by(auto simp add: measure_spmf_spmf_of_set measure_pmf_of_set)
  3.1964 +
  3.1965 +lemma nn_integral_spmf_of_set: "nn_integral (measure_spmf (spmf_of_set A)) f = setsum f A / card A"
  3.1966 +by(cases "finite A")(auto simp add: spmf_of_set_def nn_integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set)
  3.1967 +
  3.1968 +lemma integral_spmf_of_set: "integral\<^sup>L (measure_spmf (spmf_of_set A)) f = setsum f A / card A"
  3.1969 +by(clarsimp simp add: spmf_of_set_def integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set)
  3.1970 +
  3.1971 +notepad begin -- \<open>@{const pmf_of_set} is not fully parametric.\<close>
  3.1972 +  define R :: "nat \<Rightarrow> nat \<Rightarrow> bool" where "R x y \<longleftrightarrow> (x \<noteq> 0 \<longrightarrow> y = 0)" for x y
  3.1973 +  define A :: "nat set" where "A = {0, 1}"
  3.1974 +  define B :: "nat set" where "B = {0, 1, 2}"
  3.1975 +  have "rel_set R A B" unfolding R_def[abs_def] A_def B_def rel_set_def by auto
  3.1976 +  have "\<not> rel_pmf R (pmf_of_set A) (pmf_of_set B)"
  3.1977 +  proof
  3.1978 +    assume "rel_pmf R (pmf_of_set A) (pmf_of_set B)"
  3.1979 +    then obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
  3.1980 +      and 1: "map_pmf fst pq = pmf_of_set A"
  3.1981 +      and 2: "map_pmf snd pq = pmf_of_set B"
  3.1982 +      by cases auto
  3.1983 +    have "pmf (pmf_of_set B) 1 = 1 / 3" by(simp add: B_def)
  3.1984 +    have "pmf (pmf_of_set B) 2 = 1 / 3" by(simp add: B_def)
  3.1985 +
  3.1986 +    have "2 / 3 = pmf (pmf_of_set B) 1 + pmf (pmf_of_set B) 2" by(simp add: B_def)
  3.1987 +    also have "\<dots> = measure (measure_pmf (pmf_of_set B)) ({1} \<union> {2})"
  3.1988 +      by(subst measure_pmf.finite_measure_Union)(simp_all add: measure_pmf_single)
  3.1989 +    also have "\<dots> = emeasure (measure_pmf pq) (snd -` {2, 1})"
  3.1990 +      unfolding 2[symmetric] measure_pmf.emeasure_eq_measure[symmetric] by(simp)
  3.1991 +    also have "\<dots> = emeasure (measure_pmf pq) {(0, 2), (0, 1)}"
  3.1992 +      by(rule emeasure_eq_AE)(auto simp add: AE_measure_pmf_iff R_def dest!: pq)
  3.1993 +    also have "\<dots> \<le> emeasure (measure_pmf pq) (fst -` {0})"
  3.1994 +      by(rule emeasure_mono) auto
  3.1995 +    also have "\<dots> = emeasure (measure_pmf (pmf_of_set A)) {0}"
  3.1996 +      unfolding 1[symmetric] by simp
  3.1997 +    also have "\<dots> = pmf (pmf_of_set A) 0"
  3.1998 +      by(simp add: measure_pmf_single measure_pmf.emeasure_eq_measure)
  3.1999 +    also have "pmf (pmf_of_set A) 0 = 1 / 2" by(simp add: A_def)
  3.2000 +    finally show False by(subst (asm) ennreal_le_iff; simp)
  3.2001 +  qed
  3.2002 +end
  3.2003 +
  3.2004 +lemma rel_pmf_of_set_bij:
  3.2005 +  assumes f: "bij_betw f A B"
  3.2006 +  and A: "A \<noteq> {}" "finite A"
  3.2007 +  and B: "B \<noteq> {}" "finite B" 
  3.2008 +  and R: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
  3.2009 +  shows "rel_pmf R (pmf_of_set A) (pmf_of_set B)"
  3.2010 +proof(rule pmf.rel_mono_strong)
  3.2011 +  define AB where "AB = (\<lambda>x. (x, f x)) ` A"
  3.2012 +  define R' where "R' x y \<longleftrightarrow> (x, y) \<in> AB" for x y
  3.2013 +  have "(x, y) \<in> AB" if "(x, y) \<in> set_pmf (pmf_of_set AB)" for x y
  3.2014 +    using that by(auto simp add: AB_def A)
  3.2015 +  moreover have "map_pmf fst (pmf_of_set AB) = pmf_of_set A"
  3.2016 +    by(simp add: AB_def map_pmf_of_set_inj[symmetric] inj_on_def A pmf.map_comp o_def)
  3.2017 +  moreover
  3.2018 +  from f have [simp]: "inj_on f A" by(rule bij_betw_imp_inj_on)
  3.2019 +  from f have [simp]: "f ` A = B" by(rule bij_betw_imp_surj_on)
  3.2020 +  have "map_pmf snd (pmf_of_set AB) = pmf_of_set B"
  3.2021 +    by(simp add: AB_def map_pmf_of_set_inj[symmetric] inj_on_def A pmf.map_comp o_def)
  3.2022 +      (simp add: map_pmf_of_set_inj A)
  3.2023 +  ultimately show "rel_pmf (\<lambda>x y. (x, y) \<in> AB) (pmf_of_set A) (pmf_of_set B)" ..
  3.2024 +qed(auto intro: R)
  3.2025 +
  3.2026 +lemma rel_spmf_of_set_bij:
  3.2027 +  assumes f: "bij_betw f A B"
  3.2028 +  and R: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
  3.2029 +  shows "rel_spmf R (spmf_of_set A) (spmf_of_set B)"
  3.2030 +proof -
  3.2031 +  have "finite A \<longleftrightarrow> finite B" using f by(rule bij_betw_finite)
  3.2032 +  moreover have "A = {} \<longleftrightarrow> B = {}" using f by(auto dest: bij_betw_empty2 bij_betw_empty1)
  3.2033 +  ultimately show ?thesis using assms
  3.2034 +    by(auto simp add: spmf_of_set_def simp del: spmf_of_pmf_pmf_of_set intro: rel_pmf_of_set_bij)
  3.2035 +qed
  3.2036 +
  3.2037 +context begin interpretation lifting_syntax .
  3.2038 +lemma rel_spmf_of_set:
  3.2039 +  assumes "bi_unique R"
  3.2040 +  shows "(rel_set R ===> rel_spmf R) spmf_of_set spmf_of_set"
  3.2041 +proof
  3.2042 +  fix A B
  3.2043 +  assume R: "rel_set R A B"
  3.2044 +  with assms obtain f where "bij_betw f A B" and f: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
  3.2045 +    by(auto dest: bi_unique_rel_set_bij_betw)
  3.2046 +  then show "rel_spmf R (spmf_of_set A) (spmf_of_set B)" by(rule rel_spmf_of_set_bij)
  3.2047 +qed
  3.2048 +end
  3.2049 +
  3.2050 +lemma map_mem_spmf_of_set:
  3.2051 +  assumes "finite B" "B \<noteq> {}"
  3.2052 +  shows "map_spmf (\<lambda>x. x \<in> A) (spmf_of_set B) = spmf_of_pmf (bernoulli_pmf (card (A \<inter> B) / card B))"
  3.2053 +  (is "?lhs = ?rhs")
  3.2054 +proof(rule spmf_eqI)
  3.2055 +  fix i
  3.2056 +  have "ennreal (spmf ?lhs i) = card (B \<inter> (\<lambda>x. x \<in> A) -` {i}) / (card B)"
  3.2057 +    by(subst ennreal_spmf_map)(simp add: measure_spmf_spmf_of_set assms emeasure_pmf_of_set)
  3.2058 +  also have "\<dots> = (if i then card (B \<inter> A) / card B else card (B - A) / card B)"
  3.2059 +    by(auto intro: arg_cong[where f=card])
  3.2060 +  also have "\<dots> = (if i then card (B \<inter> A) / card B else (card B - card (B \<inter> A)) / card B)"
  3.2061 +    by(auto simp add: card_Diff_subset_Int assms)
  3.2062 +  also have "\<dots> = ennreal (spmf ?rhs i)"                               
  3.2063 +    by(simp add: assms card_gt_0_iff field_simps card_mono Int_commute of_nat_diff)
  3.2064 +  finally show "spmf ?lhs i = spmf ?rhs i" by simp
  3.2065 +qed
  3.2066 +
  3.2067 +abbreviation coin_spmf :: "bool spmf"
  3.2068 +where "coin_spmf \<equiv> spmf_of_set UNIV"
  3.2069 +
  3.2070 +lemma map_eq_const_coin_spmf: "map_spmf (op = c) coin_spmf = coin_spmf"
  3.2071 +proof -
  3.2072 +  have "inj (op \<longleftrightarrow> c)" "range (op \<longleftrightarrow> c) = UNIV" by(auto intro: inj_onI)
  3.2073 +  then show ?thesis by simp
  3.2074 +qed
  3.2075 +
  3.2076 +lemma bind_coin_spmf_eq_const: "coin_spmf \<bind> (\<lambda>x :: bool. return_spmf (b = x)) = coin_spmf"
  3.2077 +using map_eq_const_coin_spmf unfolding map_spmf_conv_bind_spmf by simp
  3.2078 +
  3.2079 +lemma bind_coin_spmf_eq_const': "coin_spmf \<bind> (\<lambda>x :: bool. return_spmf (x = b)) = coin_spmf"
  3.2080 +by(rewrite in "_ = \<hole>" bind_coin_spmf_eq_const[symmetric, of b])(auto intro: bind_spmf_cong)
  3.2081 +
  3.2082 +subsection {* Losslessness *}
  3.2083 +
  3.2084 +definition lossless_spmf :: "'a spmf \<Rightarrow> bool"
  3.2085 +where "lossless_spmf p \<longleftrightarrow> weight_spmf p = 1"
  3.2086 +
  3.2087 +lemma lossless_iff_pmf_None: "lossless_spmf p \<longleftrightarrow> pmf p None = 0"
  3.2088 +by(simp add: lossless_spmf_def pmf_None_eq_weight_spmf)
  3.2089 +
  3.2090 +lemma lossless_return_spmf [iff]: "lossless_spmf (return_spmf x)"
  3.2091 +by(simp add: lossless_iff_pmf_None)
  3.2092 +
  3.2093 +lemma lossless_return_pmf_None [iff]: "\<not> lossless_spmf (return_pmf None)"
  3.2094 +by(simp add: lossless_iff_pmf_None)
  3.2095 +
  3.2096 +lemma lossless_map_spmf [simp]: "lossless_spmf (map_spmf f p) \<longleftrightarrow> lossless_spmf p"
  3.2097 +by(auto simp add: lossless_iff_pmf_None pmf_eq_0_set_pmf)
  3.2098 +
  3.2099 +lemma lossless_bind_spmf [simp]:
  3.2100 +  "lossless_spmf (p \<bind> f) \<longleftrightarrow> lossless_spmf p \<and> (\<forall>x\<in>set_spmf p. lossless_spmf (f x))"
  3.2101 +by(simp add: lossless_iff_pmf_None pmf_bind_spmf_None add_nonneg_eq_0_iff integral_nonneg_AE integral_nonneg_eq_0_iff_AE measure_spmf.integrable_const_bound[where B=1] pmf_le_1)
  3.2102 +
  3.2103 +lemma lossless_weight_spmfD: "lossless_spmf p \<Longrightarrow> weight_spmf p = 1"
  3.2104 +by(simp add: lossless_spmf_def)
  3.2105 +
  3.2106 +lemma lossless_iff_set_pmf_None:
  3.2107 +  "lossless_spmf p \<longleftrightarrow> None \<notin> set_pmf p"
  3.2108 +by (simp add: lossless_iff_pmf_None pmf_eq_0_set_pmf)
  3.2109 +
  3.2110 +lemma lossless_spmf_of_set [simp]: "lossless_spmf (spmf_of_set A) \<longleftrightarrow> finite A \<and> A \<noteq> {}"
  3.2111 +by(auto simp add: lossless_spmf_def weight_spmf_of_set)
  3.2112 +
  3.2113 +lemma lossless_spmf_spmf_of_spmf [simp]: "lossless_spmf (spmf_of_pmf p)"
  3.2114 +by(simp add: lossless_spmf_def)
  3.2115 +
  3.2116 +lemma lossless_spmf_bind_pmf [simp]:
  3.2117 +  "lossless_spmf (bind_pmf p f) \<longleftrightarrow> (\<forall>x\<in>set_pmf p. lossless_spmf (f x))"
  3.2118 +by(simp add: lossless_iff_pmf_None pmf_bind integral_nonneg_AE integral_nonneg_eq_0_iff_AE measure_pmf.integrable_const_bound[where B=1] AE_measure_pmf_iff pmf_le_1)
  3.2119 +
  3.2120 +lemma lossless_spmf_conv_spmf_of_pmf: "lossless_spmf p \<longleftrightarrow> (\<exists>p'. p = spmf_of_pmf p')"
  3.2121 +proof
  3.2122 +  assume "lossless_spmf p"
  3.2123 +  hence *: "\<And>y. y \<in> set_pmf p \<Longrightarrow> \<exists>x. y = Some x"
  3.2124 +    by(case_tac y)(simp_all add: lossless_iff_set_pmf_None)
  3.2125 +
  3.2126 +  let ?p = "map_pmf the p"
  3.2127 +  have "p = spmf_of_pmf ?p"
  3.2128 +  proof(rule spmf_eqI)
  3.2129 +    fix i
  3.2130 +    have "ennreal (pmf (map_pmf the p) i) = \<integral>\<^sup>+ x. indicator (the -` {i}) x \<partial>p" by(simp add: ennreal_pmf_map)
  3.2131 +    also have "\<dots> = \<integral>\<^sup>+ x. indicator {i} x \<partial>measure_spmf p" unfolding measure_spmf_def
  3.2132 +      by(subst nn_integral_distr)(auto simp add: nn_integral_restrict_space AE_measure_pmf_iff simp del: nn_integral_indicator intro!: nn_integral_cong_AE split: split_indicator dest!: * )
  3.2133 +    also have "\<dots> = spmf p i" by(simp add: emeasure_spmf_single)
  3.2134 +    finally show "spmf p i = spmf (spmf_of_pmf ?p) i" by simp
  3.2135 +  qed
  3.2136 +  thus "\<exists>p'. p = spmf_of_pmf p'" ..
  3.2137 +qed auto
  3.2138 +
  3.2139 +lemma spmf_False_conv_True: "lossless_spmf p \<Longrightarrow> spmf p False = 1 - spmf p True"
  3.2140 +by(clarsimp simp add: lossless_spmf_conv_spmf_of_pmf pmf_False_conv_True)
  3.2141 +
  3.2142 +lemma spmf_True_conv_False: "lossless_spmf p \<Longrightarrow> spmf p True = 1 - spmf p False"
  3.2143 +by(simp add: spmf_False_conv_True)
  3.2144 +
  3.2145 +lemma bind_eq_return_spmf:
  3.2146 +  "bind_spmf p f = return_spmf x \<longleftrightarrow> (\<forall>y\<in>set_spmf p. f y = return_spmf x) \<and> lossless_spmf p"
  3.2147 +by(auto simp add: bind_spmf_def bind_eq_return_pmf in_set_spmf lossless_iff_pmf_None pmf_eq_0_set_pmf iff del: not_None_eq split: option.split)
  3.2148 +
  3.2149 +lemma rel_spmf_return_spmf2:
  3.2150 +  "rel_spmf R p (return_spmf x) \<longleftrightarrow> lossless_spmf p \<and> (\<forall>a\<in>set_spmf p. R a x)"
  3.2151 +by(auto simp add: lossless_iff_set_pmf_None rel_pmf_return_pmf2 option_rel_Some2 in_set_spmf, metis in_set_spmf not_None_eq)
  3.2152 +
  3.2153 +lemma rel_spmf_return_spmf1:
  3.2154 +  "rel_spmf R (return_spmf x) p \<longleftrightarrow> lossless_spmf p \<and> (\<forall>a\<in>set_spmf p. R x a)"
  3.2155 +using rel_spmf_return_spmf2[of "R\<inverse>\<inverse>"] by(simp add: spmf_rel_conversep)
  3.2156 +
  3.2157 +lemma rel_spmf_bindI1:
  3.2158 +  assumes f: "\<And>x. x \<in> set_spmf p \<Longrightarrow> rel_spmf R (f x) q"
  3.2159 +  and p: "lossless_spmf p"
  3.2160 +  shows "rel_spmf R (bind_spmf p f) q"
  3.2161 +proof -
  3.2162 +  fix x :: 'a
  3.2163 +  have "rel_spmf R (bind_spmf p f) (bind_spmf (return_spmf x) (\<lambda>_. q))"
  3.2164 +    by(rule rel_spmf_bindI[where R="\<lambda>x _. x \<in> set_spmf p"])(simp_all add: rel_spmf_return_spmf2 p f)
  3.2165 +  then show ?thesis by simp
  3.2166 +qed
  3.2167 +
  3.2168 +lemma rel_spmf_bindI2:
  3.2169 +  "\<lbrakk> \<And>x. x \<in> set_spmf q \<Longrightarrow> rel_spmf R p (f x); lossless_spmf q \<rbrakk>
  3.2170 +  \<Longrightarrow> rel_spmf R p (bind_spmf q f)"
  3.2171 +using rel_spmf_bindI1[of q "conversep R" f p] by(simp add: spmf_rel_conversep)
  3.2172 +
  3.2173 +subsection {* Scaling *}
  3.2174 +
  3.2175 +definition scale_spmf :: "real \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf"
  3.2176 +where
  3.2177 +  "scale_spmf r p = embed_spmf (\<lambda>x. min (inverse (weight_spmf p)) (max 0 r) * spmf p x)"
  3.2178 +
  3.2179 +lemma scale_spmf_le_1:
  3.2180 +  "(\<integral>\<^sup>+ x. min (inverse (weight_spmf p)) (max 0 r) * spmf p x \<partial>count_space UNIV) \<le> 1" (is "?lhs \<le> _")
  3.2181 +proof -
  3.2182 +  have "?lhs = min (inverse (weight_spmf p)) (max 0 r) * \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
  3.2183 +    by(subst nn_integral_cmult[symmetric])(simp_all add: weight_spmf_nonneg max_def min_def ennreal_mult)
  3.2184 +  also have "\<dots> \<le> 1" unfolding weight_spmf_eq_nn_integral_spmf[symmetric]
  3.2185 +    by(simp add: min_def max_def weight_spmf_nonneg order.strict_iff_order field_simps ennreal_mult[symmetric])
  3.2186 +  finally show ?thesis .
  3.2187 +qed
  3.2188 +
  3.2189 +lemma spmf_scale_spmf: "spmf (scale_spmf r p) x = max 0 (min (inverse (weight_spmf p)) r) * spmf p x" (is "?lhs = ?rhs")
  3.2190 +unfolding scale_spmf_def
  3.2191 +apply(subst spmf_embed_spmf[OF scale_spmf_le_1])
  3.2192 +apply(simp add: max_def min_def weight_spmf_le_0 field_simps weight_spmf_nonneg not_le order.strict_iff_order)
  3.2193 +apply(metis antisym_conv order_trans weight_spmf_nonneg zero_le_mult_iff zero_le_one)
  3.2194 +done
  3.2195 +
  3.2196 +lemma real_inverse_le_1_iff: fixes x :: real
  3.2197 +  shows "\<lbrakk> 0 \<le> x; x \<le> 1 \<rbrakk> \<Longrightarrow> 1 / x \<le> 1 \<longleftrightarrow> x = 1 \<or> x = 0"
  3.2198 +by auto
  3.2199 +
  3.2200 +lemma spmf_scale_spmf': "r \<le> 1 \<Longrightarrow> spmf (scale_spmf r p) x = max 0 r * spmf p x"
  3.2201 +using real_inverse_le_1_iff[OF weight_spmf_nonneg weight_spmf_le_1, of p]
  3.2202 +by(auto simp add: spmf_scale_spmf max_def min_def field_simps)(metis pmf_le_0_iff spmf_le_weight)
  3.2203 +
  3.2204 +lemma scale_spmf_neg: "r \<le> 0 \<Longrightarrow> scale_spmf r p = return_pmf None"
  3.2205 +by(rule spmf_eqI)(simp add: spmf_scale_spmf' max_def)
  3.2206 +
  3.2207 +lemma scale_spmf_return_None [simp]: "scale_spmf r (return_pmf None) = return_pmf None"
  3.2208 +by(rule spmf_eqI)(simp add: spmf_scale_spmf)
  3.2209 +
  3.2210 +lemma scale_spmf_conv_bind_bernoulli:
  3.2211 +  assumes "r \<le> 1"
  3.2212 +  shows "scale_spmf r p = bind_pmf (bernoulli_pmf r) (\<lambda>b. if b then p else return_pmf None)" (is "?lhs = ?rhs")
  3.2213 +proof(rule spmf_eqI)
  3.2214 +  fix x
  3.2215 +  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using assms
  3.2216 +    unfolding spmf_scale_spmf ennreal_pmf_bind nn_integral_measure_pmf UNIV_bool bernoulli_pmf.rep_eq
  3.2217 +    apply(auto simp add: nn_integral_count_space_finite max_def min_def field_simps real_inverse_le_1_iff[OF weight_spmf_nonneg weight_spmf_le_1] weight_spmf_lt_0 not_le ennreal_mult[symmetric])
  3.2218 +    apply (metis pmf_le_0_iff spmf_le_weight)
  3.2219 +    apply (metis pmf_le_0_iff spmf_le_weight)
  3.2220 +    apply (meson le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 not_less order_trans weight_spmf_le_0)
  3.2221 +    by (meson divide_le_0_1_iff less_imp_le order_trans weight_spmf_le_0)
  3.2222 +  thus "spmf ?lhs x = spmf ?rhs x" by simp
  3.2223 +qed
  3.2224 +
  3.2225 +lemma nn_integral_spmf: "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space A) = emeasure (measure_spmf p) A"
  3.2226 +apply(simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space nn_integral_pmf[symmetric])
  3.2227 +apply(rule nn_integral_bij_count_space[where g=Some])
  3.2228 +apply(auto simp add: bij_betw_def)
  3.2229 +done
  3.2230 +
  3.2231 +lemma measure_spmf_scale_spmf: "measure_spmf (scale_spmf r p) = scale_measure (min (inverse (weight_spmf p)) r) (measure_spmf p)"
  3.2232 +apply(rule measure_eqI)
  3.2233 + apply simp
  3.2234 +apply(simp add: nn_integral_spmf[symmetric] spmf_scale_spmf)
  3.2235 +apply(subst nn_integral_cmult[symmetric])
  3.2236 +apply(auto simp add: max_def min_def ennreal_mult[symmetric] not_le ennreal_lt_0)
  3.2237 +done
  3.2238 +
  3.2239 +lemma measure_spmf_scale_spmf': 
  3.2240 +  "r \<le> 1 \<Longrightarrow> measure_spmf (scale_spmf r p) = scale_measure r (measure_spmf p)"
  3.2241 +unfolding measure_spmf_scale_spmf
  3.2242 +apply(cases "weight_spmf p > 0")
  3.2243 + apply(simp add: min.absorb2 field_simps weight_spmf_le_1 mult_le_one)
  3.2244 +apply(clarsimp simp add: weight_spmf_le_0 min_def scale_spmf_neg weight_spmf_eq_0 not_less)
  3.2245 +done
  3.2246 +
  3.2247 +lemma scale_spmf_1 [simp]: "scale_spmf 1 p = p"
  3.2248 +apply(rule spmf_eqI)
  3.2249 +apply(simp add: spmf_scale_spmf max_def min_def order.strict_iff_order field_simps weight_spmf_nonneg)
  3.2250 +apply(metis antisym_conv divide_le_eq_1 less_imp_le pmf_nonneg spmf_le_weight weight_spmf_nonneg weight_spmf_le_1)
  3.2251 +done
  3.2252 +
  3.2253 +lemma scale_spmf_0 [simp]: "scale_spmf 0 p = return_pmf None"
  3.2254 +by(rule spmf_eqI)(simp add: spmf_scale_spmf min_def max_def weight_spmf_le_0)
  3.2255 +
  3.2256 +lemma bind_scale_spmf: 
  3.2257 +  assumes r: "r \<le> 1"
  3.2258 +  shows "bind_spmf (scale_spmf r p) f = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
  3.2259 +  (is "?lhs = ?rhs")
  3.2260 +proof(rule spmf_eqI)
  3.2261 +  fix x
  3.2262 +  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using r
  3.2263 +    by(simp add: ennreal_spmf_bind measure_spmf_scale_spmf' nn_integral_scale_measure spmf_scale_spmf')
  3.2264 +      (simp add: ennreal_mult ennreal_lt_0 nn_integral_cmult max_def min_def)
  3.2265 +  thus "spmf ?lhs x = spmf ?rhs x" by simp
  3.2266 +qed
  3.2267 +
  3.2268 +lemma scale_bind_spmf: 
  3.2269 +  assumes "r \<le> 1"
  3.2270 +  shows "scale_spmf r (bind_spmf p f) = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
  3.2271 +  (is "?lhs = ?rhs")
  3.2272 +proof(rule spmf_eqI)
  3.2273 +  fix x
  3.2274 +  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using assms
  3.2275 +    unfolding spmf_scale_spmf'[OF assms]
  3.2276 +    by(simp add: ennreal_mult ennreal_spmf_bind spmf_scale_spmf' nn_integral_cmult max_def min_def)
  3.2277 +  thus "spmf ?lhs x = spmf ?rhs x" by simp
  3.2278 +qed
  3.2279 +
  3.2280 +lemma bind_spmf_const: "bind_spmf p (\<lambda>x. q) = scale_spmf (weight_spmf p) q" (is "?lhs = ?rhs")
  3.2281 +proof(rule spmf_eqI)
  3.2282 +  fix x
  3.2283 +  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)"
  3.2284 +    using measure_spmf.subprob_measure_le_1[of p "space (measure_spmf p)"]
  3.2285 +    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)
  3.2286 +  thus "spmf ?lhs x = spmf ?rhs x" by simp
  3.2287 +qed
  3.2288 +
  3.2289 +lemma map_scale_spmf: "map_spmf f (scale_spmf r p) = scale_spmf r (map_spmf f p)" (is "?lhs = ?rhs")
  3.2290 +proof(rule spmf_eqI)
  3.2291 +  fix i
  3.2292 +  show "spmf ?lhs i = spmf ?rhs i" unfolding spmf_scale_spmf
  3.2293 +    by(subst (1 2) spmf_map)(auto simp add: measure_spmf_scale_spmf max_def min_def ennreal_lt_0)
  3.2294 +qed
  3.2295 +
  3.2296 +lemma set_scale_spmf: "set_spmf (scale_spmf r p) = (if r > 0 then set_spmf p else {})"
  3.2297 +apply(auto simp add: in_set_spmf_iff_spmf spmf_scale_spmf)
  3.2298 +apply(simp add: max_def min_def not_le weight_spmf_lt_0 weight_spmf_eq_0 split: if_split_asm)
  3.2299 +done
  3.2300 +
  3.2301 +lemma set_scale_spmf' [simp]: "0 < r \<Longrightarrow> set_spmf (scale_spmf r p) = set_spmf p"
  3.2302 +by(simp add: set_scale_spmf)
  3.2303 +
  3.2304 +lemma rel_spmf_scaleI: 
  3.2305 +  assumes "r > 0 \<Longrightarrow> rel_spmf A p q"
  3.2306 +  shows "rel_spmf A (scale_spmf r p) (scale_spmf r q)"
  3.2307 +proof(cases "r > 0")
  3.2308 +  case True
  3.2309 +  from assms[OF this] show ?thesis
  3.2310 +    by(rule rel_spmfE)(auto simp add: map_scale_spmf[symmetric] spmf_rel_map True intro: rel_spmf_reflI)
  3.2311 +qed(simp add: not_less scale_spmf_neg)
  3.2312 +
  3.2313 +lemma weight_scale_spmf: "weight_spmf (scale_spmf r p) = min 1 (max 0 r * weight_spmf p)"
  3.2314 +proof -
  3.2315 +  have "ennreal (weight_spmf (scale_spmf r p)) = min 1 (max 0 r * ennreal (weight_spmf p))"
  3.2316 +    unfolding weight_spmf_eq_nn_integral_spmf
  3.2317 +    apply(simp add: spmf_scale_spmf ennreal_mult zero_ereal_def[symmetric] nn_integral_cmult)
  3.2318 +    apply(auto simp add: weight_spmf_eq_nn_integral_spmf[symmetric] field_simps min_def max_def not_le weight_spmf_lt_0 ennreal_mult[symmetric])
  3.2319 +    subgoal by(subst (asm) ennreal_mult[symmetric], meson divide_less_0_1_iff le_less_trans not_le weight_spmf_lt_0, simp+, meson not_le pos_divide_le_eq weight_spmf_le_0)
  3.2320 +    subgoal by(cases "r \<ge> 0")(simp_all add: ennreal_mult[symmetric] weight_spmf_nonneg ennreal_lt_0, meson le_less_trans not_le pos_divide_le_eq zero_less_divide_1_iff)
  3.2321 +    done
  3.2322 +  thus ?thesis by(auto simp add: min_def max_def ennreal_mult[symmetric] split: if_split_asm)
  3.2323 +qed
  3.2324 +
  3.2325 +lemma weight_scale_spmf' [simp]: 
  3.2326 +  "\<lbrakk> 0 \<le> r; r \<le> 1 \<rbrakk> \<Longrightarrow> weight_spmf (scale_spmf r p) = r * weight_spmf p"
  3.2327 +by(simp add: weight_scale_spmf max_def min_def)(metis antisym_conv mult_left_le order_trans weight_spmf_le_1)
  3.2328 +
  3.2329 +lemma pmf_scale_spmf_None:
  3.2330 +  "pmf (scale_spmf k p) None = 1 - min 1 (max 0 k * (1 - pmf p None))"
  3.2331 +unfolding pmf_None_eq_weight_spmf by(simp add: weight_scale_spmf)
  3.2332 +
  3.2333 +lemma scale_scale_spmf: 
  3.2334 +  "scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
  3.2335 +  (is "?lhs = ?rhs")
  3.2336 +proof(rule spmf_eqI)
  3.2337 +  fix i
  3.2338 +  have "max 0 (min (1 / weight_spmf p) r') *
  3.2339 +    max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
  3.2340 +    max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
  3.2341 +  proof(cases "weight_spmf p > 0")
  3.2342 +    case False
  3.2343 +    thus ?thesis by(simp add: not_less weight_spmf_le_0)
  3.2344 +  next
  3.2345 +    case True
  3.2346 +    thus ?thesis by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
  3.2347 +  qed
  3.2348 +  then show "spmf ?lhs i = spmf ?rhs i"
  3.2349 +    by(simp add: spmf_scale_spmf field_simps weight_scale_spmf)
  3.2350 +qed
  3.2351 +
  3.2352 +lemma scale_scale_spmf' [simp]:
  3.2353 +  "\<lbrakk> 0 \<le> r; r \<le> 1; 0 \<le> r'; r' \<le> 1 \<rbrakk>
  3.2354 +  \<Longrightarrow> scale_spmf r (scale_spmf r' p) = scale_spmf (r * r') p"
  3.2355 +apply(cases "weight_spmf p > 0")
  3.2356 +apply(auto simp add: scale_scale_spmf min_def max_def field_simps not_le weight_spmf_lt_0 weight_spmf_eq_0 not_less weight_spmf_le_0)
  3.2357 +apply(subgoal_tac "1 = r'")
  3.2358 + apply (metis (no_types) divide_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
  3.2359 +apply(meson eq_iff le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 mult_imp_div_pos_le order.trans)
  3.2360 +done
  3.2361 +
  3.2362 +lemma scale_spmf_eq_same: "scale_spmf r p = p \<longleftrightarrow> weight_spmf p = 0 \<or> r = 1 \<or> r \<ge> 1 \<and> weight_spmf p = 1"
  3.2363 +  (is "?lhs \<longleftrightarrow> ?rhs")
  3.2364 +proof
  3.2365 +  assume ?lhs
  3.2366 +  hence "weight_spmf (scale_spmf r p) = weight_spmf p" by simp
  3.2367 +  hence *: "min 1 (max 0 r * weight_spmf p) = weight_spmf p" by(simp add: weight_scale_spmf)
  3.2368 +  hence **: "weight_spmf p = 0 \<or> r \<ge> 1" by(auto simp add: min_def max_def split: if_split_asm)
  3.2369 +  show ?rhs
  3.2370 +  proof(cases "weight_spmf p = 0")
  3.2371 +    case False
  3.2372 +    with ** have "r \<ge> 1" by simp
  3.2373 +    with * False have "r = 1 \<or> weight_spmf p = 1" by(simp add: max_def min_def not_le split: if_split_asm)
  3.2374 +    with \<open>r \<ge> 1\<close> show ?thesis by simp
  3.2375 +  qed simp
  3.2376 +qed(auto intro!: spmf_eqI simp add: spmf_scale_spmf, metis pmf_le_0_iff spmf_le_weight)
  3.2377 +
  3.2378 +lemma map_const_spmf_of_set:
  3.2379 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> map_spmf (\<lambda>_. c) (spmf_of_set A) = return_spmf c"
  3.2380 +by(simp add: map_spmf_conv_bind_spmf bind_spmf_const)
  3.2381 +
  3.2382 +subsection {* Conditional spmfs *}
  3.2383 +
  3.2384 +lemma set_pmf_Int_Some: "set_pmf p \<inter> Some ` A = {} \<longleftrightarrow> set_spmf p \<inter> A = {}"
  3.2385 +by(auto simp add: in_set_spmf)
  3.2386 +
  3.2387 +lemma measure_spmf_zero_iff: "measure (measure_spmf p) A = 0 \<longleftrightarrow> set_spmf p \<inter> A = {}"
  3.2388 +unfolding measure_measure_spmf_conv_measure_pmf by(simp add: measure_pmf_zero_iff set_pmf_Int_Some)
  3.2389 +
  3.2390 +definition cond_spmf :: "'a spmf \<Rightarrow> 'a set \<Rightarrow> 'a spmf"
  3.2391 +where "cond_spmf p A = (if set_spmf p \<inter> A = {} then return_pmf None else cond_pmf p (Some ` A))"
  3.2392 +
  3.2393 +lemma set_cond_spmf [simp]: "set_spmf (cond_spmf p A) = set_spmf p \<inter> A"
  3.2394 +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])
  3.2395 +
  3.2396 +lemma cond_map_spmf [simp]: "cond_spmf (map_spmf f p) A = map_spmf f (cond_spmf p (f -` A))"
  3.2397 +proof -
  3.2398 +  have "map_option f -` Some ` A = Some ` f -` A" by auto
  3.2399 +  moreover have "set_pmf p \<inter> map_option f -` Some ` A \<noteq> {}" if "Some x \<in> set_pmf p" "f x \<in> A" for x
  3.2400 +    using that by auto
  3.2401 +  ultimately show ?thesis by(auto simp add: cond_spmf_def in_set_spmf cond_map_pmf)
  3.2402 +qed
  3.2403 +
  3.2404 +lemma spmf_cond_spmf [simp]:
  3.2405 +  "spmf (cond_spmf p A) x = (if x \<in> A then spmf p x / measure (measure_spmf p) A else 0)"
  3.2406 +by(auto simp add: cond_spmf_def pmf_cond set_pmf_Int_Some[symmetric] measure_measure_spmf_conv_measure_pmf measure_pmf_zero_iff)
  3.2407 +
  3.2408 +lemma bind_eq_return_pmf_None:
  3.2409 +  "bind_spmf p f = return_pmf None \<longleftrightarrow> (\<forall>x\<in>set_spmf p. f x = return_pmf None)"
  3.2410 +by(auto simp add: bind_spmf_def bind_eq_return_pmf in_set_spmf split: option.splits)
  3.2411 +
  3.2412 +lemma return_pmf_None_eq_bind:
  3.2413 +  "return_pmf None = bind_spmf p f \<longleftrightarrow> (\<forall>x\<in>set_spmf p. f x = return_pmf None)"
  3.2414 +using bind_eq_return_pmf_None[of p f] by auto
  3.2415 +
  3.2416 +(* Conditional probabilities do not seem to interact nicely with bind. *)
  3.2417 +
  3.2418 +subsection {* Product spmf *}
  3.2419 +
  3.2420 +definition pair_spmf :: "'a spmf \<Rightarrow> 'b spmf \<Rightarrow> ('a \<times> 'b) spmf"
  3.2421 +where "pair_spmf p q = bind_pmf (pair_pmf p q) (\<lambda>xy. case xy of (Some x, Some y) \<Rightarrow> return_spmf (x, y) | _ \<Rightarrow> return_pmf None)"
  3.2422 +
  3.2423 +lemma map_fst_pair_spmf [simp]: "map_spmf fst (pair_spmf p q) = scale_spmf (weight_spmf q) p"
  3.2424 +unfolding bind_spmf_const[symmetric]
  3.2425 +apply(simp add: pair_spmf_def map_bind_pmf pair_pmf_def bind_assoc_pmf option.case_distrib)
  3.2426 +apply(subst bind_commute_pmf)
  3.2427 +apply(auto intro!: bind_pmf_cong[OF refl] simp add: bind_return_pmf bind_spmf_def bind_return_pmf' case_option_collapse option.case_distrib[where h="map_spmf _"] option.case_distrib[symmetric] case_option_id split: option.split cong del: option.case_cong)
  3.2428 +done
  3.2429 +
  3.2430 +lemma map_snd_pair_spmf [simp]: "map_spmf snd (pair_spmf p q) = scale_spmf (weight_spmf p) q"
  3.2431 +unfolding bind_spmf_const[symmetric]
  3.2432 +apply(simp add: pair_spmf_def map_bind_pmf pair_pmf_def bind_assoc_pmf option.case_distrib cong del: option.case_cong)
  3.2433 +apply(auto intro!: bind_pmf_cong[OF refl] simp add: bind_return_pmf bind_spmf_def bind_return_pmf' case_option_collapse option.case_distrib[where h="map_spmf _"] option.case_distrib[symmetric] case_option_id split: option.split cong del: option.case_cong)
  3.2434 +done
  3.2435 +
  3.2436 +lemma set_pair_spmf [simp]: "set_spmf (pair_spmf p q) = set_spmf p \<times> set_spmf q"
  3.2437 +by(auto 4 3 simp add: pair_spmf_def set_spmf_bind_pmf bind_UNION in_set_spmf intro: rev_bexI split: option.splits)
  3.2438 +                                                 
  3.2439 +lemma spmf_pair [simp]: "spmf (pair_spmf p q) (x, y) = spmf p x * spmf q y" (is "?lhs = ?rhs")
  3.2440 +proof -
  3.2441 +  have "ennreal ?lhs = \<integral>\<^sup>+ a. \<integral>\<^sup>+ b. indicator {(x, y)} (a, b) \<partial>measure_spmf q \<partial>measure_spmf p"
  3.2442 +    unfolding measure_spmf_def pair_spmf_def ennreal_pmf_bind nn_integral_pair_pmf'
  3.2443 +    by(auto simp add: zero_ereal_def[symmetric] nn_integral_distr nn_integral_restrict_space nn_integral_multc[symmetric] intro!: nn_integral_cong split: option.split split_indicator)
  3.2444 +  also have "\<dots> = \<integral>\<^sup>+ a. (\<integral>\<^sup>+ b. indicator {y} b \<partial>measure_spmf q) * indicator {x} a \<partial>measure_spmf p"
  3.2445 +    by(subst nn_integral_multc[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
  3.2446 +  also have "\<dots> = ennreal ?rhs" by(simp add: emeasure_spmf_single max_def ennreal_mult mult.commute)
  3.2447 +  finally show ?thesis by simp
  3.2448 +qed
  3.2449 +
  3.2450 +lemma pair_map_spmf2: "pair_spmf p (map_spmf f q) = map_spmf (apsnd f) (pair_spmf p q)"
  3.2451 +by(auto simp add: pair_spmf_def pair_map_pmf2 bind_map_pmf map_bind_pmf intro: bind_pmf_cong split: option.split)
  3.2452 +
  3.2453 +lemma pair_map_spmf1: "pair_spmf (map_spmf f p) q = map_spmf (apfst f) (pair_spmf p q)"
  3.2454 +by(auto simp add: pair_spmf_def pair_map_pmf1 bind_map_pmf map_bind_pmf intro: bind_pmf_cong split: option.split)
  3.2455 +
  3.2456 +lemma pair_map_spmf: "pair_spmf (map_spmf f p) (map_spmf g q) = map_spmf (map_prod f g) (pair_spmf p q)"
  3.2457 +unfolding pair_map_spmf2 pair_map_spmf1 spmf.map_comp by(simp add: apfst_def apsnd_def o_def prod.map_comp)
  3.2458 +
  3.2459 +lemma pair_spmf_alt_def: "pair_spmf p q = bind_spmf p (\<lambda>x. bind_spmf q (\<lambda>y. return_spmf (x, y)))"
  3.2460 +by(auto simp add: pair_spmf_def pair_pmf_def bind_spmf_def bind_assoc_pmf bind_return_pmf split: option.split intro: bind_pmf_cong)
  3.2461 +
  3.2462 +lemma weight_pair_spmf [simp]: "weight_spmf (pair_spmf p q) = weight_spmf p * weight_spmf q"
  3.2463 +unfolding pair_spmf_alt_def by(simp add: weight_bind_spmf o_def)
  3.2464 +
  3.2465 +lemma pair_scale_spmf1: (* FIXME: generalise to arbitrary r *)
  3.2466 +  "r \<le> 1 \<Longrightarrow> pair_spmf (scale_spmf r p) q = scale_spmf r (pair_spmf p q)"
  3.2467 +by(simp add: pair_spmf_alt_def scale_bind_spmf bind_scale_spmf)
  3.2468 +
  3.2469 +lemma pair_scale_spmf2: (* FIXME: generalise to arbitrary r *)
  3.2470 +  "r \<le> 1 \<Longrightarrow> pair_spmf p (scale_spmf r q) = scale_spmf r (pair_spmf p q)"
  3.2471 +by(simp add: pair_spmf_alt_def scale_bind_spmf bind_scale_spmf)
  3.2472 +
  3.2473 +lemma pair_spmf_return_None1 [simp]: "pair_spmf (return_pmf None) p = return_pmf None"
  3.2474 +by(rule spmf_eqI)(clarsimp)
  3.2475 +
  3.2476 +lemma pair_spmf_return_None2 [simp]: "pair_spmf p (return_pmf None) = return_pmf None"
  3.2477 +by(rule spmf_eqI)(clarsimp)
  3.2478 +
  3.2479 +lemma pair_spmf_return_spmf1: "pair_spmf (return_spmf x) q = map_spmf (Pair x) q"
  3.2480 +by(rule spmf_eqI)(auto split: split_indicator simp add: spmf_map_inj' inj_on_def intro: spmf_map_outside)
  3.2481 +
  3.2482 +lemma pair_spmf_return_spmf2: "pair_spmf p (return_spmf y) = map_spmf (\<lambda>x. (x, y)) p"
  3.2483 +by(rule spmf_eqI)(auto split: split_indicator simp add: inj_on_def intro!: spmf_map_outside spmf_map_inj'[symmetric])
  3.2484 +
  3.2485 +lemma pair_spmf_return_spmf [simp]: "pair_spmf (return_spmf x) (return_spmf y) = return_spmf (x, y)"
  3.2486 +by(simp add: pair_spmf_return_spmf1)
  3.2487 +
  3.2488 +lemma rel_pair_spmf_prod:
  3.2489 +  "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \<longleftrightarrow> 
  3.2490 +   rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \<and> 
  3.2491 +   rel_spmf B (scale_spmf (weight_spmf p) q) (scale_spmf (weight_spmf p') q')"
  3.2492 +  (is "?lhs \<longleftrightarrow> ?rhs" is "_ \<longleftrightarrow> ?A \<and> ?B" is "_ \<longleftrightarrow> rel_spmf _ ?p ?p' \<and> rel_spmf _ ?q ?q'")
  3.2493 +proof(intro iffI conjI)
  3.2494 +  assume ?rhs
  3.2495 +  then obtain pq pq' where p: "map_spmf fst pq = ?p" and p': "map_spmf snd pq = ?p'"
  3.2496 +    and q: "map_spmf fst pq' = ?q" and q': "map_spmf snd pq' = ?q'"
  3.2497 +    and *: "\<And>x x'. (x, x') \<in> set_spmf pq \<Longrightarrow> A x x'"
  3.2498 +    and **: "\<And>y y'. (y, y') \<in> set_spmf pq' \<Longrightarrow> B y y'" by(auto elim!: rel_spmfE)
  3.2499 +  let ?f = "\<lambda>((x, x'), (y, y')). ((x, y), (x', y'))"
  3.2500 +  let ?r = "1 / (weight_spmf p * weight_spmf q)"
  3.2501 +  let ?pq = "scale_spmf ?r (map_spmf ?f (pair_spmf pq pq'))"
  3.2502 +
  3.2503 +  { fix p :: "'x spmf" and q :: "'y spmf"
  3.2504 +    assume "weight_spmf q \<noteq> 0"
  3.2505 +      and "weight_spmf p \<noteq> 0"
  3.2506 +      and "1 / (weight_spmf p * weight_spmf q) \<le> weight_spmf p * weight_spmf q"
  3.2507 +    hence "1 \<le> (weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q)"
  3.2508 +      by(simp add: pos_divide_le_eq order.strict_iff_order weight_spmf_nonneg)
  3.2509 +    moreover have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) \<le> (1 * 1) * (1 * 1)"
  3.2510 +      by(intro mult_mono)(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
  3.2511 +    ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
  3.2512 +    hence *: "weight_spmf p * weight_spmf q = 1" 
  3.2513 +      by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
  3.2514 +    hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
  3.2515 +    moreover with * have "weight_spmf q = 1" by simp
  3.2516 +    moreover note calculation }
  3.2517 +  note full = this
  3.2518 +
  3.2519 +  show ?lhs
  3.2520 +  proof
  3.2521 +    have [simp]: "fst \<circ> ?f = map_prod fst fst" by(simp add: fun_eq_iff)
  3.2522 +    have "map_spmf fst ?pq = scale_spmf ?r (pair_spmf ?p ?q)"
  3.2523 +      by(simp add: pair_map_spmf[symmetric] p q map_scale_spmf spmf.map_comp)
  3.2524 +    also have "\<dots> = pair_spmf p q" using full[of p q]
  3.2525 +      by(simp add: pair_scale_spmf1 pair_scale_spmf2 weight_spmf_le_1 weight_spmf_nonneg)
  3.2526 +        (auto simp add: scale_scale_spmf max_def min_def field_simps weight_spmf_nonneg weight_spmf_eq_0)
  3.2527 +    finally show "map_spmf fst ?pq = \<dots>" .
  3.2528 +
  3.2529 +    have [simp]: "snd \<circ> ?f = map_prod snd snd" by(simp add: fun_eq_iff)
  3.2530 +    from \<open>?rhs\<close> have eq: "weight_spmf p * weight_spmf q = weight_spmf p' * weight_spmf q'"
  3.2531 +      by(auto dest!: rel_spmf_weightD simp add: weight_spmf_le_1 weight_spmf_nonneg)
  3.2532 +    
  3.2533 +    have "map_spmf snd ?pq = scale_spmf ?r (pair_spmf ?p' ?q')"
  3.2534 +      by(simp add: pair_map_spmf[symmetric] p' q' map_scale_spmf spmf.map_comp)
  3.2535 +    also have "\<dots> = pair_spmf p' q'" using full[of p' q'] eq
  3.2536 +      by(simp add: pair_scale_spmf1 pair_scale_spmf2 weight_spmf_le_1 weight_spmf_nonneg)
  3.2537 +        (auto simp add: scale_scale_spmf max_def min_def field_simps weight_spmf_nonneg weight_spmf_eq_0)
  3.2538 +    finally show "map_spmf snd ?pq = \<dots>" .
  3.2539 +  qed(auto simp add: set_scale_spmf split: if_split_asm dest: * ** )
  3.2540 +next
  3.2541 +  assume ?lhs
  3.2542 +  then obtain pq where pq: "map_spmf fst pq = pair_spmf p q"
  3.2543 +    and pq': "map_spmf snd pq = pair_spmf p' q'"
  3.2544 +    and *: "\<And>x y x' y'. ((x, y), (x', y')) \<in> set_spmf pq \<Longrightarrow> A x x' \<and> B y y'"
  3.2545 +    by(auto elim: rel_spmfE)
  3.2546 +
  3.2547 +  show ?A
  3.2548 +  proof
  3.2549 +    let ?f = "(\<lambda>((x, y), (x', y')). (x, x'))"
  3.2550 +    let ?pq = "map_spmf ?f pq"
  3.2551 +    have [simp]: "fst \<circ> ?f = fst \<circ> fst" by(simp add: split_def o_def)
  3.2552 +    show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq 
  3.2553 +      by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
  3.2554 +
  3.2555 +    have [simp]: "snd \<circ> ?f = fst \<circ> snd" by(simp add: split_def o_def)
  3.2556 +    show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq' 
  3.2557 +      by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
  3.2558 +  qed(auto dest: * )
  3.2559 +    
  3.2560 +  show ?B
  3.2561 +  proof
  3.2562 +    let ?f = "(\<lambda>((x, y), (x', y')). (y, y'))"
  3.2563 +    let ?pq = "map_spmf ?f pq"
  3.2564 +    have [simp]: "fst \<circ> ?f = snd \<circ> fst" by(simp add: split_def o_def)
  3.2565 +    show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq 
  3.2566 +      by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
  3.2567 +
  3.2568 +    have [simp]: "snd \<circ> ?f = snd \<circ> snd" by(simp add: split_def o_def)
  3.2569 +    show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq' 
  3.2570 +      by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
  3.2571 +  qed(auto dest: * )
  3.2572 +qed
  3.2573 +
  3.2574 +lemma pair_pair_spmf:
  3.2575 +  "pair_spmf (pair_spmf p q) r = map_spmf (\<lambda>(x, (y, z)). ((x, y), z)) (pair_spmf p (pair_spmf q r))"
  3.2576 +by(simp add: pair_spmf_alt_def map_spmf_conv_bind_spmf)
  3.2577 +
  3.2578 +lemma pair_commute_spmf:
  3.2579 +  "pair_spmf p q = map_spmf (\<lambda>(y, x). (x, y)) (pair_spmf q p)"
  3.2580 +unfolding pair_spmf_alt_def by(subst bind_commute_spmf)(simp add: map_spmf_conv_bind_spmf)
  3.2581 +
  3.2582 +subsection {* Assertions *}
  3.2583 +
  3.2584 +definition assert_spmf :: "bool \<Rightarrow> unit spmf"
  3.2585 +where "assert_spmf b = (if b then return_spmf () else return_pmf None)"
  3.2586 +
  3.2587 +lemma assert_spmf_simps [simp]:
  3.2588 +  "assert_spmf True = return_spmf ()"
  3.2589 +  "assert_spmf False = return_pmf None"
  3.2590 +by(simp_all add: assert_spmf_def)
  3.2591 +
  3.2592 +lemma in_set_assert_spmf [simp]: "x \<in> set_spmf (assert_spmf p) \<longleftrightarrow> p"
  3.2593 +by(cases p) simp_all
  3.2594 +
  3.2595 +lemma set_spmf_assert_spmf_eq_empty [simp]: "set_spmf (assert_spmf b) = {} \<longleftrightarrow> \<not> b"
  3.2596 +by(cases b) simp_all
  3.2597 +
  3.2598 +lemma lossless_assert_spmf [iff]: "lossless_spmf (assert_spmf b) \<longleftrightarrow> b"
  3.2599 +by(cases b) simp_all
  3.2600 +
  3.2601 +subsection {* Try *}
  3.2602 +
  3.2603 +definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf" ("TRY _ ELSE _" [0,60] 59)
  3.2604 +where "try_spmf p q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
  3.2605 +
  3.2606 +lemma try_spmf_lossless [simp]:
  3.2607 +  assumes "lossless_spmf p"
  3.2608 +  shows "TRY p ELSE q = p"
  3.2609 +proof -
  3.2610 +  have "TRY p ELSE q = bind_pmf p return_pmf" unfolding try_spmf_def using assms
  3.2611 +    by(auto simp add: lossless_iff_set_pmf_None split: option.split intro: bind_pmf_cong)
  3.2612 +  thus ?thesis by(simp add: bind_return_pmf')
  3.2613 +qed
  3.2614 +
  3.2615 +lemma try_spmf_return_spmf1: "TRY return_spmf x ELSE q = return_spmf x"
  3.2616 +by(simp add: try_spmf_def bind_return_pmf)
  3.2617 +
  3.2618 +lemma try_spmf_return_None [simp]: "TRY return_pmf None ELSE q = q"
  3.2619 +by(simp add: try_spmf_def bind_return_pmf)
  3.2620 +
  3.2621 +lemma try_spmf_return_pmf_None2 [simp]: "TRY p ELSE return_pmf None = p"
  3.2622 +by(simp add: try_spmf_def option.case_distrib[symmetric] bind_return_pmf' case_option_id)
  3.2623 +
  3.2624 +lemma map_try_spmf: "map_spmf f (try_spmf p q) = try_spmf (map_spmf f p) (map_spmf f q)"
  3.2625 +by(simp add: try_spmf_def map_bind_pmf bind_map_pmf option.case_distrib[where h="map_spmf f"] o_def cong del: option.case_cong_weak)
  3.2626 +
  3.2627 +lemma try_spmf_bind_pmf: "TRY (bind_pmf p f) ELSE q = bind_pmf p (\<lambda>x. TRY (f x) ELSE q)"
  3.2628 +by(simp add: try_spmf_def bind_assoc_pmf)
  3.2629 +
  3.2630 +lemma try_spmf_bind_spmf_lossless:
  3.2631 +  "lossless_spmf p \<Longrightarrow> TRY (bind_spmf p f) ELSE q = bind_spmf p (\<lambda>x. TRY (f x) ELSE q)"
  3.2632 +by(auto simp add: try_spmf_def bind_spmf_def bind_assoc_pmf bind_return_pmf lossless_iff_set_pmf_None intro!: bind_pmf_cong split: option.split)
  3.2633 +
  3.2634 +lemma try_spmf_bind_out:
  3.2635 +  "lossless_spmf p \<Longrightarrow> bind_spmf p (\<lambda>x. TRY (f x) ELSE q) = TRY (bind_spmf p f) ELSE q"
  3.2636 +by(simp add: try_spmf_bind_spmf_lossless)
  3.2637 +
  3.2638 +lemma lossless_try_spmf [simp]:
  3.2639 +  "lossless_spmf (TRY p ELSE q) \<longleftrightarrow> lossless_spmf p \<or> lossless_spmf q"
  3.2640 +by(auto simp add: try_spmf_def in_set_spmf lossless_iff_set_pmf_None split: option.splits)
  3.2641 +
  3.2642 +context begin interpretation lifting_syntax .
  3.2643 +lemma try_spmf_parametric [transfer_rule]:
  3.2644 +  "(rel_spmf A ===> rel_spmf A ===> rel_spmf A) try_spmf try_spmf"
  3.2645 +unfolding try_spmf_def[abs_def] by transfer_prover
  3.2646 +end
  3.2647 +
  3.2648 +lemma try_spmf_cong:
  3.2649 +  "\<lbrakk> p = p'; \<not> lossless_spmf p' \<Longrightarrow> q = q' \<rbrakk> \<Longrightarrow> TRY p ELSE q = TRY p' ELSE q'"
  3.2650 +unfolding try_spmf_def
  3.2651 +by(rule bind_pmf_cong)(auto split: option.split simp add: lossless_iff_set_pmf_None)
  3.2652 +
  3.2653 +lemma rel_spmf_try_spmf:
  3.2654 +  "\<lbrakk> rel_spmf R p p'; \<not> lossless_spmf p' \<Longrightarrow> rel_spmf R q q' \<rbrakk>
  3.2655 +  \<Longrightarrow> rel_spmf R (TRY p ELSE q) (TRY p' ELSE q')"
  3.2656 +unfolding try_spmf_def 
  3.2657 +apply(rule rel_pmf_bindI[where R="\<lambda>x y. rel_option R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf p'"])
  3.2658 + apply(erule pmf.rel_mono_strong; simp)
  3.2659 +apply(auto split: option.split simp add: lossless_iff_set_pmf_None)
  3.2660 +done
  3.2661 +
  3.2662 +lemma spmf_try_spmf:
  3.2663 +  "spmf (TRY p ELSE q) x = spmf p x + pmf p None * spmf q x"
  3.2664 +proof -
  3.2665 +  have "ennreal (spmf (TRY p ELSE q) x) = \<integral>\<^sup>+ y. ennreal (spmf q x) * indicator {None} y + indicator {Some x} y \<partial>measure_pmf p"
  3.2666 +    unfolding try_spmf_def ennreal_pmf_bind by(rule nn_integral_cong)(simp split: option.split split_indicator)
  3.2667 +  also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (spmf q x) * indicator {None} y \<partial>measure_pmf p) + \<integral>\<^sup>+ y. indicator {Some x} y \<partial>measure_pmf p"
  3.2668 +    by(simp add: nn_integral_add)
  3.2669 +  also have "\<dots> = ennreal (spmf q x) * pmf p None + spmf p x" by(simp add: emeasure_pmf_single)
  3.2670 +  finally show ?thesis by(simp add: ennreal_mult[symmetric] ennreal_plus[symmetric] del: ennreal_plus)
  3.2671 +qed
  3.2672 +
  3.2673 +lemma try_scale_spmf_same [simp]: "lossless_spmf p \<Longrightarrow> TRY scale_spmf k p ELSE p = p"
  3.2674 +by(rule spmf_eqI)(auto simp add: 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)
  3.2675 +
  3.2676 +lemma pmf_try_spmf_None [simp]: "pmf (TRY p ELSE q) None = pmf p None * pmf q None" (is "?lhs = ?rhs")
  3.2677 +proof -
  3.2678 +  have "?lhs = \<integral> x. pmf q None * indicator {None} x \<partial>measure_pmf p"
  3.2679 +    unfolding try_spmf_def pmf_bind by(rule integral_cong)(simp_all split: option.split)
  3.2680 +  also have "\<dots> = ?rhs" by(simp add: measure_pmf_single)
  3.2681 +  finally show ?thesis .
  3.2682 +qed
  3.2683 +
  3.2684 +lemma try_bind_spmf_lossless2:
  3.2685 +  "lossless_spmf q \<Longrightarrow> TRY (bind_spmf p f) ELSE q = TRY (p \<bind> (\<lambda>x. TRY (f x) ELSE q)) ELSE q"
  3.2686 +by(rule spmf_eqI)(simp add: spmf_try_spmf pmf_bind_spmf_None spmf_bind field_simps measure_spmf.integrable_const_bound[where B=1] pmf_le_1 lossless_iff_pmf_None)
  3.2687 +
  3.2688 +lemma try_bind_spmf_lossless2':
  3.2689 +  fixes f :: "'a \<Rightarrow> 'b spmf" shows
  3.2690 +  "\<lbrakk> NO_MATCH (\<lambda>x :: 'a. try_spmf (g x :: 'b spmf) (h x)) f; lossless_spmf q \<rbrakk>
  3.2691 +  \<Longrightarrow> TRY (bind_spmf p f) ELSE q = TRY (p \<bind> (\<lambda>x :: 'a. TRY (f x) ELSE q)) ELSE q"
  3.2692 +by(rule try_bind_spmf_lossless2)
  3.2693 +
  3.2694 +lemma try_bind_assert_spmf:
  3.2695 +  "TRY (assert_spmf b \<bind> f) ELSE q = (if b then TRY (f ()) ELSE q else q)"
  3.2696 +by simp
  3.2697 +
  3.2698 +subsection \<open>Miscellaneous\<close>
  3.2699 +
  3.2700 +lemma assumes "rel_spmf (\<lambda>x y. bad1 x = bad2 y \<and> (\<not> bad2 y \<longrightarrow> A x \<longleftrightarrow> B y)) p q" (is "rel_spmf ?A _ _")
  3.2701 +  shows fundamental_lemma_bad: "measure (measure_spmf p) {x. bad1 x} = measure (measure_spmf q) {y. bad2 y}" (is "?bad")
  3.2702 +  and fundamental_lemma: "\<bar>measure (measure_spmf p) {x. A x} - measure (measure_spmf q) {y. B y}\<bar> \<le>
  3.2703 +    measure (measure_spmf p) {x. bad1 x}" (is ?fundamental)
  3.2704 +proof -
  3.2705 +  have good: "rel_fun ?A op = (\<lambda>x. A x \<and> \<not> bad1 x) (\<lambda>y. B y \<and> \<not> bad2 y)" by(auto simp add: rel_fun_def)
  3.2706 +  from assms have 1: "measure (measure_spmf p) {x. A x \<and> \<not> bad1 x} = measure (measure_spmf q) {y. B y \<and> \<not> bad2 y}"
  3.2707 +    by(rule measure_spmf_parametric[THEN rel_funD, THEN rel_funD])(rule Collect_parametric[THEN rel_funD, OF good])
  3.2708 +
  3.2709 +  have bad: "rel_fun ?A op = bad1 bad2" by(simp add: rel_fun_def)
  3.2710 +  show 2: ?bad using assms
  3.2711 +    by(rule measure_spmf_parametric[THEN rel_funD, THEN rel_funD])(rule Collect_parametric[THEN rel_funD, OF bad])
  3.2712 +
  3.2713 +  let ?\<mu>p = "measure (measure_spmf p)" and ?\<mu>q = "measure (measure_spmf q)"
  3.2714 +  have "{x. A x \<and> bad1 x} \<union> {x. A x \<and> \<not> bad1 x} = {x. A x}"
  3.2715 +    and "{y. B y \<and> bad2 y} \<union> {y. B y \<and> \<not> bad2 y} = {y. B y}" by auto
  3.2716 +  then have "\<bar>?\<mu>p {x. A x} - ?\<mu>q {x. B x}\<bar> = \<bar>?\<mu>p ({x. A x \<and> bad1 x} \<union> {x. A x \<and> \<not> bad1 x}) - ?\<mu>q ({y. B y \<and> bad2 y} \<union> {y. B y \<and> \<not> bad2 y})\<bar>"
  3.2717 +    by simp
  3.2718 +  also have "\<dots> = \<bar>?\<mu>p {x. A x \<and> bad1 x} + ?\<mu>p {x. A x \<and> \<not> bad1 x} - ?\<mu>q {y. B y \<and> bad2 y} - ?\<mu>q {y. B y \<and> \<not> bad2 y}\<bar>"
  3.2719 +    by(subst (1 2) measure_Union)(auto)
  3.2720 +  also have "\<dots> = \<bar>?\<mu>p {x. A x \<and> bad1 x} - ?\<mu>q {y. B y \<and> bad2 y}\<bar>" using 1 by simp
  3.2721 +  also have "\<dots> \<le> max (?\<mu>p {x. A x \<and> bad1 x}) (?\<mu>q {y. B y \<and> bad2 y})"
  3.2722 +    by(rule abs_leI)(auto simp add: max_def not_le, simp_all only: add_increasing measure_nonneg mult_2)
  3.2723 +  also have "\<dots> \<le> max (?\<mu>p {x. bad1 x}) (?\<mu>q {y. bad2 y})"
  3.2724 +    by(rule max.mono; rule measure_spmf.finite_measure_mono; auto)
  3.2725 +  also note 2[symmetric]
  3.2726 +  finally show ?fundamental by simp
  3.2727 +qed
  3.2728 +
  3.2729 +end
     4.1 --- a/src/HOL/Probability/document/root.tex	Mon Jun 06 22:22:05 2016 +0200
     4.2 +++ b/src/HOL/Probability/document/root.tex	Wed Jun 08 09:05:32 2016 +0200
     4.3 @@ -2,6 +2,7 @@
     4.4  \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
     4.5  \usepackage{amsmath}
     4.6  \usepackage{amssymb}
     4.7 +\usepackage{wasysym}
     4.8  \usepackage[only,bigsqcap]{stmaryrd}
     4.9  \usepackage[utf8]{inputenc}
    4.10  \usepackage{pdfsetup}