src/HOL/Probability/SPMF.thy
author wenzelm
Fri Jul 22 11:00:43 2016 +0200 (2016-07-22)
changeset 63540 f8652d0534fa
parent 63343 fb5d8a50c641
child 63566 e5abbdee461a
permissions -rw-r--r--
tuned proofs -- avoid unstructured calculation;
Andreas@63243
     1
(* Author: Andreas Lochbihler, ETH Zurich *)
Andreas@63243
     2
Andreas@63243
     3
section \<open>Discrete subprobability distribution\<close>
Andreas@63243
     4
Andreas@63243
     5
theory SPMF imports
Andreas@63243
     6
  Probability_Mass_Function
Andreas@63243
     7
  Embed_Measure
Andreas@63243
     8
  "~~/src/HOL/Library/Complete_Partial_Order2"
Andreas@63243
     9
  "~~/src/HOL/Library/Rewrite"
Andreas@63243
    10
begin
Andreas@63243
    11
Andreas@63243
    12
subsection \<open>Auxiliary material\<close>
Andreas@63243
    13
Andreas@63243
    14
lemma cSUP_singleton [simp]: "(SUP x:{x}. f x :: _ :: conditionally_complete_lattice) = f x"
Andreas@63243
    15
by (metis cSup_singleton image_empty image_insert)
Andreas@63243
    16
Andreas@63243
    17
subsubsection \<open>More about extended reals\<close>
Andreas@63243
    18
Andreas@63243
    19
lemma [simp]:
Andreas@63243
    20
  shows ennreal_max_0: "ennreal (max 0 x) = ennreal x"
Andreas@63243
    21
  and ennreal_max_0': "ennreal (max x 0) = ennreal x"
Andreas@63243
    22
by(simp_all add: max_def ennreal_eq_0_iff)
Andreas@63243
    23
Andreas@63243
    24
lemma ennreal_enn2real_if: "ennreal (enn2real r) = (if r = \<top> then 0 else r)"
Andreas@63243
    25
by(auto intro!: ennreal_enn2real simp add: less_top)
Andreas@63243
    26
Andreas@63243
    27
lemma e2ennreal_0 [simp]: "e2ennreal 0 = 0"
Andreas@63243
    28
by(simp add: zero_ennreal_def)
Andreas@63243
    29
Andreas@63243
    30
lemma enn2real_bot [simp]: "enn2real \<bottom> = 0"
Andreas@63243
    31
by(simp add: bot_ennreal_def)
Andreas@63243
    32
Andreas@63243
    33
lemma continuous_at_ennreal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ennreal (f x))"
Andreas@63243
    34
  unfolding continuous_def by auto
Andreas@63243
    35
Andreas@63243
    36
lemma ennreal_Sup:
Andreas@63243
    37
  assumes *: "(SUP a:A. ennreal a) \<noteq> \<top>"
Andreas@63243
    38
  and "A \<noteq> {}"
Andreas@63243
    39
  shows "ennreal (Sup A) = (SUP a:A. ennreal a)"
Andreas@63243
    40
proof (rule continuous_at_Sup_mono)
Andreas@63243
    41
  obtain r where r: "ennreal r = (SUP a:A. ennreal a)" "r \<ge> 0"
Andreas@63243
    42
    using * by(cases "(SUP a:A. ennreal a)") simp_all
Andreas@63243
    43
  then show "bdd_above A"
Andreas@63243
    44
    by(auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ennreal_le_iff[symmetric])
Andreas@63243
    45
qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ennreal ennreal_leI assms)
Andreas@63243
    46
Andreas@63243
    47
lemma ennreal_SUP:
Andreas@63243
    48
  "\<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))"
Andreas@63243
    49
using ennreal_Sup[of "f ` A"] by auto
Andreas@63243
    50
Andreas@63243
    51
lemma ennreal_lt_0: "x < 0 \<Longrightarrow> ennreal x = 0"
Andreas@63243
    52
by(simp add: ennreal_eq_0_iff)
Andreas@63243
    53
Andreas@63243
    54
subsubsection \<open>More about @{typ "'a option"}\<close>
Andreas@63243
    55
Andreas@63243
    56
lemma None_in_map_option_image [simp]: "None \<in> map_option f ` A \<longleftrightarrow> None \<in> A"
Andreas@63243
    57
by auto
Andreas@63243
    58
Andreas@63243
    59
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)"
Andreas@63243
    60
by(auto intro: rev_image_eqI dest: sym)
Andreas@63243
    61
Andreas@63243
    62
lemma case_option_collapse: "case_option x (\<lambda>_. x) = (\<lambda>_. x)"
Andreas@63243
    63
by(simp add: fun_eq_iff split: option.split)
Andreas@63243
    64
Andreas@63243
    65
lemma case_option_id: "case_option None Some = id"
Andreas@63243
    66
by(rule ext)(simp split: option.split)
Andreas@63243
    67
Andreas@63243
    68
inductive ord_option :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
Andreas@63243
    69
  for ord :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
Andreas@63243
    70
where
Andreas@63243
    71
  None: "ord_option ord None x"
Andreas@63243
    72
| Some: "ord x y \<Longrightarrow> ord_option ord (Some x) (Some y)"
Andreas@63243
    73
Andreas@63243
    74
inductive_simps ord_option_simps [simp]:
Andreas@63243
    75
  "ord_option ord None x"
Andreas@63243
    76
  "ord_option ord x None"
Andreas@63243
    77
  "ord_option ord (Some x) (Some y)"
Andreas@63243
    78
  "ord_option ord (Some x) None"
Andreas@63243
    79
Andreas@63243
    80
inductive_simps ord_option_eq_simps [simp]:
Andreas@63243
    81
  "ord_option op = None y"
Andreas@63243
    82
  "ord_option op = (Some x) y"
Andreas@63243
    83
Andreas@63243
    84
lemma ord_option_reflI: "(\<And>y. y \<in> set_option x \<Longrightarrow> ord y y) \<Longrightarrow> ord_option ord x x"
Andreas@63243
    85
by(cases x) simp_all
Andreas@63243
    86
Andreas@63243
    87
lemma reflp_ord_option: "reflp ord \<Longrightarrow> reflp (ord_option ord)"
Andreas@63243
    88
by(simp add: reflp_def ord_option_reflI)
Andreas@63243
    89
Andreas@63243
    90
lemma ord_option_trans:
Andreas@63243
    91
  "\<lbrakk> ord_option ord x y; ord_option ord y z;
Andreas@63243
    92
    \<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>
Andreas@63243
    93
  \<Longrightarrow> ord_option ord x z"
Andreas@63243
    94
by(auto elim!: ord_option.cases)
Andreas@63243
    95
Andreas@63243
    96
lemma transp_ord_option: "transp ord \<Longrightarrow> transp (ord_option ord)"
Andreas@63243
    97
unfolding transp_def by(blast intro: ord_option_trans)
Andreas@63243
    98
Andreas@63243
    99
lemma antisymP_ord_option: "antisymP ord \<Longrightarrow> antisymP (ord_option ord)"
Andreas@63243
   100
by(auto intro!: antisymI elim!: ord_option.cases dest: antisymD)
Andreas@63243
   101
Andreas@63243
   102
lemma ord_option_chainD:
Andreas@63243
   103
  "Complete_Partial_Order.chain (ord_option ord) Y
Andreas@63243
   104
  \<Longrightarrow> Complete_Partial_Order.chain ord {x. Some x \<in> Y}"
Andreas@63243
   105
by(rule chainI)(auto dest: chainD)
Andreas@63243
   106
Andreas@63243
   107
definition lub_option :: "('a set \<Rightarrow> 'b) \<Rightarrow> 'a option set \<Rightarrow> 'b option"
Andreas@63243
   108
where "lub_option lub Y = (if Y \<subseteq> {None} then None else Some (lub {x. Some x \<in> Y}))"
Andreas@63243
   109
Andreas@63243
   110
lemma map_lub_option: "map_option f (lub_option lub Y) = lub_option (f \<circ> lub) Y"
Andreas@63243
   111
by(simp add: lub_option_def)
Andreas@63243
   112
Andreas@63243
   113
lemma lub_option_upper:
Andreas@63243
   114
  assumes "Complete_Partial_Order.chain (ord_option ord) Y" "x \<in> Y"
Andreas@63243
   115
  and lub_upper: "\<And>Y x. \<lbrakk> Complete_Partial_Order.chain ord Y; x \<in> Y \<rbrakk> \<Longrightarrow> ord x (lub Y)"
Andreas@63243
   116
  shows "ord_option ord x (lub_option lub Y)"
Andreas@63243
   117
using assms(1-2)
Andreas@63243
   118
by(cases x)(auto simp add: lub_option_def intro: lub_upper[OF ord_option_chainD])
Andreas@63243
   119
Andreas@63243
   120
lemma lub_option_least:
Andreas@63243
   121
  assumes Y: "Complete_Partial_Order.chain (ord_option ord) Y"
Andreas@63243
   122
  and upper: "\<And>x. x \<in> Y \<Longrightarrow> ord_option ord x y"
Andreas@63243
   123
  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"
Andreas@63243
   124
  shows "ord_option ord (lub_option lub Y) y"
Andreas@63243
   125
using Y
Andreas@63243
   126
by(cases y)(auto 4 3 simp add: lub_option_def intro: lub_least[OF ord_option_chainD] dest: upper)
Andreas@63243
   127
Andreas@63243
   128
lemma lub_map_option: "lub_option lub (map_option f ` Y) = lub_option (lub \<circ> op ` f) Y"
Andreas@63243
   129
apply(auto simp add: lub_option_def)
Andreas@63243
   130
apply(erule notE)
Andreas@63243
   131
apply(rule arg_cong[where f=lub])
Andreas@63243
   132
apply(auto intro: rev_image_eqI dest: sym)
Andreas@63243
   133
done
Andreas@63243
   134
Andreas@63243
   135
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"
Andreas@63243
   136
by(auto elim: ord_option.cases)
Andreas@63243
   137
Andreas@63243
   138
lemma ord_option_mono' [mono]:
Andreas@63243
   139
  "(\<And>x y. A x y \<longrightarrow> B x y) \<Longrightarrow> ord_option A x y \<longrightarrow> ord_option B x y"
Andreas@63243
   140
by(blast intro: ord_option_mono)
Andreas@63243
   141
Andreas@63243
   142
lemma ord_option_compp: "ord_option (A OO B) = ord_option A OO ord_option B"
Andreas@63243
   143
by(auto simp add: fun_eq_iff elim!: ord_option.cases intro: ord_option.intros)
Andreas@63243
   144
Andreas@63243
   145
lemma ord_option_inf: "inf (ord_option A) (ord_option B) = ord_option (inf A B)" (is "?lhs = ?rhs")
Andreas@63243
   146
proof(rule antisym)
Andreas@63243
   147
  show "?lhs \<le> ?rhs" by(auto elim!: ord_option.cases)
Andreas@63243
   148
qed(auto elim: ord_option_mono)
Andreas@63243
   149
Andreas@63243
   150
lemma ord_option_map2: "ord_option ord x (map_option f y) = ord_option (\<lambda>x y. ord x (f y)) x y"
Andreas@63243
   151
by(auto elim: ord_option.cases)
Andreas@63243
   152
Andreas@63243
   153
lemma ord_option_map1: "ord_option ord (map_option f x) y = ord_option (\<lambda>x y. ord (f x) y) x y"
Andreas@63243
   154
by(auto elim: ord_option.cases)
Andreas@63243
   155
Andreas@63243
   156
lemma option_ord_Some1_iff: "option_ord (Some x) y \<longleftrightarrow> y = Some x"
Andreas@63243
   157
by(auto simp add: flat_ord_def)
Andreas@63243
   158
Andreas@63243
   159
subsubsection \<open>A relator for sets that treats sets like predicates\<close>
Andreas@63243
   160
wenzelm@63343
   161
context includes lifting_syntax
wenzelm@63343
   162
begin
wenzelm@63343
   163
Andreas@63243
   164
definition rel_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
Andreas@63243
   165
where "rel_pred R A B = (R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
Andreas@63243
   166
Andreas@63243
   167
lemma rel_predI: "(R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B) \<Longrightarrow> rel_pred R A B"
Andreas@63243
   168
by(simp add: rel_pred_def)
Andreas@63243
   169
Andreas@63243
   170
lemma rel_predD: "\<lbrakk> rel_pred R A B; R x y \<rbrakk> \<Longrightarrow> x \<in> A \<longleftrightarrow> y \<in> B"
Andreas@63243
   171
by(simp add: rel_pred_def rel_fun_def)
Andreas@63243
   172
Andreas@63243
   173
lemma Collect_parametric: "((A ===> op =) ===> rel_pred A) Collect Collect"
wenzelm@63308
   174
  \<comment> \<open>Declare this rule as @{attribute transfer_rule} only locally
Andreas@63243
   175
      because it blows up the search space for @{method transfer}
Andreas@63243
   176
      (in combination with @{thm [source] Collect_transfer})\<close>
Andreas@63243
   177
by(simp add: rel_funI rel_predI)
wenzelm@63343
   178
Andreas@63243
   179
end
Andreas@63243
   180
Andreas@63243
   181
subsubsection \<open>Monotonicity rules\<close>
Andreas@63243
   182
Andreas@63243
   183
lemma monotone_gfp_eadd1: "monotone op \<ge> op \<ge> (\<lambda>x. x + y :: enat)"
Andreas@63243
   184
by(auto intro!: monotoneI)
Andreas@63243
   185
Andreas@63243
   186
lemma monotone_gfp_eadd2: "monotone op \<ge> op \<ge> (\<lambda>y. x + y :: enat)"
Andreas@63243
   187
by(auto intro!: monotoneI)
Andreas@63243
   188
Andreas@63243
   189
lemma mono2mono_gfp_eadd[THEN gfp.mono2mono2, cont_intro, simp]:
Andreas@63243
   190
  shows monotone_eadd: "monotone (rel_prod op \<ge> op \<ge>) op \<ge> (\<lambda>(x, y). x + y :: enat)"
Andreas@63243
   191
by(simp add: monotone_gfp_eadd1 monotone_gfp_eadd2)
Andreas@63243
   192
Andreas@63243
   193
lemma eadd_gfp_partial_function_mono [partial_function_mono]:
Andreas@63243
   194
  "\<lbrakk> monotone (fun_ord op \<ge>) op \<ge> f; monotone (fun_ord op \<ge>) op \<ge> g \<rbrakk>
Andreas@63243
   195
  \<Longrightarrow> monotone (fun_ord op \<ge>) op \<ge> (\<lambda>x. f x + g x :: enat)"
Andreas@63243
   196
by(rule mono2mono_gfp_eadd)
Andreas@63243
   197
Andreas@63243
   198
lemma mono2mono_ereal[THEN lfp.mono2mono]:
Andreas@63243
   199
  shows monotone_ereal: "monotone op \<le> op \<le> ereal"
Andreas@63243
   200
by(rule monotoneI) simp
Andreas@63243
   201
Andreas@63243
   202
lemma mono2mono_ennreal[THEN lfp.mono2mono]:
Andreas@63243
   203
  shows monotone_ennreal: "monotone op \<le> op \<le> ennreal"
Andreas@63243
   204
by(rule monotoneI)(simp add: ennreal_leI)
Andreas@63243
   205
Andreas@63243
   206
subsubsection \<open>Bijections\<close>
Andreas@63243
   207
Andreas@63243
   208
lemma bi_unique_rel_set_bij_betw:
Andreas@63243
   209
  assumes unique: "bi_unique R"
Andreas@63243
   210
  and rel: "rel_set R A B"
Andreas@63243
   211
  shows "\<exists>f. bij_betw f A B \<and> (\<forall>x\<in>A. R x (f x))"
Andreas@63243
   212
proof -
Andreas@63243
   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"
Andreas@63243
   214
    apply(atomize_elim)
Andreas@63243
   215
    apply(fold all_conj_distrib)
Andreas@63243
   216
    apply(subst choice_iff[symmetric])
Andreas@63243
   217
    apply(auto dest: rel_setD1)
Andreas@63243
   218
    done
Andreas@63243
   219
  have "inj_on f A" by(rule inj_onI)(auto dest!: f dest: bi_uniqueDl[OF unique])
Andreas@63243
   220
  moreover have "f ` A = B" using rel
Andreas@63243
   221
    by(auto 4 3 intro: B dest: rel_setD2 f bi_uniqueDr[OF unique])
Andreas@63243
   222
  ultimately have "bij_betw f A B" unfolding bij_betw_def ..
Andreas@63243
   223
  thus ?thesis using f by blast
Andreas@63243
   224
qed
Andreas@63243
   225
Andreas@63243
   226
lemma bij_betw_rel_setD: "bij_betw f A B \<Longrightarrow> rel_set (\<lambda>x y. y = f x) A B"
Andreas@63243
   227
by(rule rel_setI)(auto dest: bij_betwE bij_betw_imp_surj_on[symmetric])
Andreas@63243
   228
wenzelm@63308
   229
subsection \<open>Subprobability mass function\<close>
Andreas@63243
   230
Andreas@63243
   231
type_synonym 'a spmf = "'a option pmf"
Andreas@63243
   232
translations (type) "'a spmf" \<leftharpoondown> (type) "'a option pmf"
Andreas@63243
   233
Andreas@63243
   234
definition measure_spmf :: "'a spmf \<Rightarrow> 'a measure"
Andreas@63243
   235
where "measure_spmf p = distr (restrict_space (measure_pmf p) (range Some)) (count_space UNIV) the"
Andreas@63243
   236
Andreas@63243
   237
abbreviation spmf :: "'a spmf \<Rightarrow> 'a \<Rightarrow> real"
Andreas@63243
   238
where "spmf p x \<equiv> pmf p (Some x)"
Andreas@63243
   239
Andreas@63243
   240
lemma space_measure_spmf: "space (measure_spmf p) = UNIV"
Andreas@63243
   241
by(simp add: measure_spmf_def)
Andreas@63243
   242
Andreas@63243
   243
lemma sets_measure_spmf [simp, measurable_cong]: "sets (measure_spmf p) = sets (count_space UNIV)"
Andreas@63243
   244
by(simp add: measure_spmf_def)
Andreas@63243
   245
Andreas@63243
   246
lemma measure_spmf_not_bot [simp]: "measure_spmf p \<noteq> \<bottom>"
Andreas@63243
   247
proof
Andreas@63243
   248
  assume "measure_spmf p = \<bottom>"
Andreas@63243
   249
  hence "space (measure_spmf p) = space \<bottom>" by simp
Andreas@63243
   250
  thus False by(simp add: space_measure_spmf)
Andreas@63243
   251
qed
Andreas@63243
   252
Andreas@63243
   253
lemma measurable_the_measure_pmf_Some [measurable, simp]:
Andreas@63243
   254
  "the \<in> measurable (restrict_space (measure_pmf p) (range Some)) (count_space UNIV)"
Andreas@63243
   255
by(auto simp add: measurable_def sets_restrict_space space_restrict_space integral_restrict_space)
Andreas@63243
   256
Andreas@63243
   257
lemma measurable_spmf_measure1[simp]: "measurable (measure_spmf M) N = UNIV \<rightarrow> space N"
Andreas@63243
   258
by(auto simp: measurable_def space_measure_spmf)
Andreas@63243
   259
Andreas@63243
   260
lemma measurable_spmf_measure2[simp]: "measurable N (measure_spmf M) = measurable N (count_space UNIV)"
Andreas@63243
   261
by(intro measurable_cong_sets) simp_all
Andreas@63243
   262
Andreas@63243
   263
lemma subprob_space_measure_spmf [simp, intro!]: "subprob_space (measure_spmf p)"
Andreas@63243
   264
proof
Andreas@63243
   265
  show "emeasure (measure_spmf p) (space (measure_spmf p)) \<le> 1"
Andreas@63243
   266
    by(simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space measure_pmf.measure_le_1)
Andreas@63243
   267
qed(simp add: space_measure_spmf)
Andreas@63243
   268
Andreas@63243
   269
interpretation measure_spmf: subprob_space "measure_spmf p" for p
Andreas@63243
   270
by(rule subprob_space_measure_spmf)
Andreas@63243
   271
Andreas@63243
   272
lemma finite_measure_spmf [simp]: "finite_measure (measure_spmf p)"
Andreas@63243
   273
by unfold_locales
Andreas@63243
   274
Andreas@63243
   275
lemma spmf_conv_measure_spmf: "spmf p x = measure (measure_spmf p) {x}"
Andreas@63243
   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])
Andreas@63243
   277
Andreas@63243
   278
lemma emeasure_measure_spmf_conv_measure_pmf:
Andreas@63243
   279
  "emeasure (measure_spmf p) A = emeasure (measure_pmf p) (Some ` A)"
Andreas@63243
   280
by(auto simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space intro: arg_cong2[where f=emeasure])
Andreas@63243
   281
Andreas@63243
   282
lemma measure_measure_spmf_conv_measure_pmf:
Andreas@63243
   283
  "measure (measure_spmf p) A = measure (measure_pmf p) (Some ` A)"
Andreas@63243
   284
using emeasure_measure_spmf_conv_measure_pmf[of p A]
Andreas@63243
   285
by(simp add: measure_spmf.emeasure_eq_measure measure_pmf.emeasure_eq_measure)
Andreas@63243
   286
Andreas@63243
   287
lemma emeasure_spmf_map_pmf_Some [simp]:
Andreas@63243
   288
  "emeasure (measure_spmf (map_pmf Some p)) A = emeasure (measure_pmf p) A"
Andreas@63243
   289
by(auto simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space intro: arg_cong2[where f=emeasure])
Andreas@63243
   290
Andreas@63243
   291
lemma measure_spmf_map_pmf_Some [simp]:
Andreas@63243
   292
  "measure (measure_spmf (map_pmf Some p)) A = measure (measure_pmf p) A"
Andreas@63243
   293
using emeasure_spmf_map_pmf_Some[of p A] by(simp add: measure_spmf.emeasure_eq_measure measure_pmf.emeasure_eq_measure)
Andreas@63243
   294
Andreas@63243
   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"
Andreas@63243
   296
  (is "?lhs = ?rhs")
Andreas@63243
   297
proof -
Andreas@63243
   298
  have "?lhs = \<integral>\<^sup>+ x. pmf p x * f (the x) \<partial>count_space (range Some)"
Andreas@63243
   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))
Andreas@63243
   300
  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (spmf p (the x)) * f (the x) \<partial>count_space (range Some)"
Andreas@63243
   301
    by(rule nn_integral_cong) auto
Andreas@63243
   302
  also have "\<dots> = \<integral>\<^sup>+ x. spmf p (the (Some x)) * f (the (Some x)) \<partial>count_space UNIV"
Andreas@63243
   303
    by(rule nn_integral_bij_count_space[symmetric])(simp add: bij_betw_def)
Andreas@63243
   304
  also have "\<dots> = ?rhs" by simp
Andreas@63243
   305
  finally show ?thesis .
Andreas@63243
   306
qed
Andreas@63243
   307
hoelzl@63333
   308
lemma integral_measure_spmf:
Andreas@63243
   309
  assumes "integrable (measure_spmf p) f"
Andreas@63243
   310
  shows "(\<integral> x. f x \<partial>measure_spmf p) = \<integral> x. spmf p x * f x \<partial>count_space UNIV"
Andreas@63243
   311
proof -
Andreas@63243
   312
  have "integrable (count_space UNIV) (\<lambda>x. spmf p x * f x)"
Andreas@63243
   313
    using assms by(simp add: integrable_iff_bounded nn_integral_measure_spmf abs_mult ennreal_mult'')
Andreas@63243
   314
  then show ?thesis using assms
Andreas@63243
   315
    by(simp add: real_lebesgue_integral_def nn_integral_measure_spmf ennreal_mult'[symmetric])
Andreas@63243
   316
qed
Andreas@63243
   317
Andreas@63243
   318
lemma emeasure_spmf_single: "emeasure (measure_spmf p) {x} = spmf p x"
Andreas@63243
   319
by(simp add: measure_spmf.emeasure_eq_measure spmf_conv_measure_spmf)
Andreas@63243
   320
Andreas@63243
   321
lemma measurable_measure_spmf[measurable]:
Andreas@63243
   322
  "(\<lambda>x. measure_spmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
Andreas@63243
   323
by (auto simp: space_subprob_algebra)
Andreas@63243
   324
Andreas@63243
   325
lemma nn_integral_measure_spmf_conv_measure_pmf:
Andreas@63243
   326
  assumes [measurable]: "f \<in> borel_measurable (count_space UNIV)"
Andreas@63243
   327
  shows "nn_integral (measure_spmf p) f = nn_integral (restrict_space (measure_pmf p) (range Some)) (f \<circ> the)"
Andreas@63243
   328
by(simp add: measure_spmf_def nn_integral_distr o_def)
Andreas@63243
   329
Andreas@63243
   330
lemma measure_spmf_in_space_subprob_algebra [simp]:
Andreas@63243
   331
  "measure_spmf p \<in> space (subprob_algebra (count_space UNIV))"
Andreas@63243
   332
by(simp add: space_subprob_algebra)
Andreas@63243
   333
Andreas@63243
   334
lemma nn_integral_spmf_neq_top: "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV) \<noteq> \<top>"
Andreas@63243
   335
using nn_integral_measure_spmf[where f="\<lambda>_. 1", of p, symmetric] by simp
Andreas@63243
   336
Andreas@63243
   337
lemma SUP_spmf_neq_top': "(SUP p:Y. ennreal (spmf p x)) \<noteq> \<top>"
Andreas@63243
   338
proof(rule neq_top_trans)
Andreas@63243
   339
  show "(SUP p:Y. ennreal (spmf p x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
Andreas@63243
   340
qed simp
Andreas@63243
   341
Andreas@63243
   342
lemma SUP_spmf_neq_top: "(SUP i. ennreal (spmf (Y i) x)) \<noteq> \<top>"
Andreas@63243
   343
proof(rule neq_top_trans)
Andreas@63243
   344
  show "(SUP i. ennreal (spmf (Y i) x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
Andreas@63243
   345
qed simp
hoelzl@63333
   346
Andreas@63243
   347
lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
Andreas@63243
   348
proof(rule neq_top_trans)
Andreas@63243
   349
  show "(SUP p:Y. emeasure (measure_spmf p) A) \<le> 1"
Andreas@63243
   350
    by(rule SUP_least)(simp add: measure_spmf.subprob_emeasure_le_1)
Andreas@63243
   351
qed simp
Andreas@63243
   352
wenzelm@63308
   353
subsection \<open>Support\<close>
Andreas@63243
   354
Andreas@63243
   355
definition set_spmf :: "'a spmf \<Rightarrow> 'a set"
Andreas@63243
   356
where "set_spmf p = set_pmf p \<bind> set_option"
Andreas@63243
   357
Andreas@63243
   358
lemma set_spmf_rep_eq: "set_spmf p = {x. measure (measure_spmf p) {x} \<noteq> 0}"
Andreas@63243
   359
proof -
Andreas@63243
   360
  have "\<And>x :: 'a. the -` {x} \<inter> range Some = {Some x}" by auto
Andreas@63243
   361
  then show ?thesis
Andreas@63243
   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)
Andreas@63243
   363
qed
Andreas@63243
   364
Andreas@63243
   365
lemma in_set_spmf: "x \<in> set_spmf p \<longleftrightarrow> Some x \<in> set_pmf p"
Andreas@63243
   366
by(simp add: set_spmf_def)
Andreas@63243
   367
Andreas@63243
   368
lemma AE_measure_spmf_iff [simp]: "(AE x in measure_spmf p. P x) \<longleftrightarrow> (\<forall>x\<in>set_spmf p. P x)"
Andreas@63243
   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)
Andreas@63243
   370
Andreas@63243
   371
lemma spmf_eq_0_set_spmf: "spmf p x = 0 \<longleftrightarrow> x \<notin> set_spmf p"
Andreas@63243
   372
by(auto simp add: pmf_eq_0_set_pmf set_spmf_def intro: rev_image_eqI)
Andreas@63243
   373
Andreas@63243
   374
lemma in_set_spmf_iff_spmf: "x \<in> set_spmf p \<longleftrightarrow> spmf p x \<noteq> 0"
Andreas@63243
   375
by(auto simp add: set_spmf_def set_pmf_iff intro: rev_image_eqI)
Andreas@63243
   376
Andreas@63243
   377
lemma set_spmf_return_pmf_None [simp]: "set_spmf (return_pmf None) = {}"
Andreas@63243
   378
by(auto simp add: set_spmf_def)
Andreas@63243
   379
Andreas@63243
   380
lemma countable_set_spmf [simp]: "countable (set_spmf p)"
Andreas@63243
   381
by(simp add: set_spmf_def bind_UNION)
Andreas@63243
   382
Andreas@63243
   383
lemma spmf_eqI:
Andreas@63243
   384
  assumes "\<And>i. spmf p i = spmf q i"
Andreas@63243
   385
  shows "p = q"
Andreas@63243
   386
proof(rule pmf_eqI)
Andreas@63243
   387
  fix i
Andreas@63243
   388
  show "pmf p i = pmf q i"
Andreas@63243
   389
  proof(cases i)
Andreas@63243
   390
    case (Some i')
Andreas@63243
   391
    thus ?thesis by(simp add: assms)
Andreas@63243
   392
  next
Andreas@63243
   393
    case None
Andreas@63243
   394
    have "ennreal (pmf p i) = measure (measure_pmf p) {i}" by(simp add: pmf_def)
Andreas@63243
   395
    also have "{i} = space (measure_pmf p) - range Some"
Andreas@63243
   396
      by(auto simp add: None intro: ccontr)
Andreas@63243
   397
    also have "measure (measure_pmf p) \<dots> = ennreal 1 - measure (measure_pmf p) (range Some)"
Andreas@63243
   398
      by(simp add: measure_pmf.prob_compl ennreal_minus[symmetric] del: space_measure_pmf)
Andreas@63243
   399
    also have "range Some = (\<Union>x\<in>set_spmf p. {Some x}) \<union> Some ` (- set_spmf p)"
Andreas@63243
   400
      by auto
Andreas@63243
   401
    also have "measure (measure_pmf p) \<dots> = measure (measure_pmf p) (\<Union>x\<in>set_spmf p. {Some x})"
Andreas@63243
   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)
Andreas@63243
   403
    also have "ennreal \<dots> = \<integral>\<^sup>+ x. measure (measure_pmf p) {Some x} \<partial>count_space (set_spmf p)"
Andreas@63243
   404
      unfolding measure_pmf.emeasure_eq_measure[symmetric]
Andreas@63243
   405
      by(simp_all add: emeasure_UN_countable disjoint_family_on_def)
Andreas@63243
   406
    also have "\<dots> = \<integral>\<^sup>+ x. spmf p x \<partial>count_space (set_spmf p)" by(simp add: pmf_def)
Andreas@63243
   407
    also have "\<dots> = \<integral>\<^sup>+ x. spmf q x \<partial>count_space (set_spmf p)" by(simp add: assms)
Andreas@63243
   408
    also have "set_spmf p = set_spmf q" by(auto simp add: in_set_spmf_iff_spmf assms)
Andreas@63243
   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)"
Andreas@63243
   410
      by(simp add: pmf_def)
Andreas@63243
   411
    also have "\<dots> = measure (measure_pmf q) (\<Union>x\<in>set_spmf q. {Some x})"
Andreas@63243
   412
      unfolding measure_pmf.emeasure_eq_measure[symmetric]
Andreas@63243
   413
      by(simp_all add: emeasure_UN_countable disjoint_family_on_def)
Andreas@63243
   414
    also have "\<dots> = measure (measure_pmf q) ((\<Union>x\<in>set_spmf q. {Some x}) \<union> Some ` (- set_spmf q))"
Andreas@63243
   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)
Andreas@63243
   416
    also have "((\<Union>x\<in>set_spmf q. {Some x}) \<union> Some ` (- set_spmf q)) = range Some" by auto
Andreas@63243
   417
    also have "ennreal 1 - measure (measure_pmf q) \<dots> = measure (measure_pmf q) (space (measure_pmf q) - range Some)"
Andreas@63243
   418
      by(simp add: one_ereal_def measure_pmf.prob_compl ennreal_minus[symmetric] del: space_measure_pmf)
Andreas@63243
   419
    also have "space (measure_pmf q) - range Some = {i}"
Andreas@63243
   420
      by(auto simp add: None intro: ccontr)
Andreas@63243
   421
    also have "measure (measure_pmf q) \<dots> = pmf q i" by(simp add: pmf_def)
Andreas@63243
   422
    finally show ?thesis by simp
Andreas@63243
   423
  qed
Andreas@63243
   424
qed
Andreas@63243
   425
Andreas@63243
   426
lemma integral_measure_spmf_restrict:
Andreas@63243
   427
  fixes f ::  "'a \<Rightarrow> 'b :: {banach, second_countable_topology}" shows
Andreas@63243
   428
  "(\<integral> x. f x \<partial>measure_spmf M) = (\<integral> x. f x \<partial>restrict_space (measure_spmf M) (set_spmf M))"
Andreas@63243
   429
by(auto intro!: integral_cong_AE simp add: integral_restrict_space)
Andreas@63243
   430
Andreas@63243
   431
lemma nn_integral_measure_spmf':
Andreas@63243
   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)"
Andreas@63243
   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)
Andreas@63243
   434
wenzelm@63308
   435
subsection \<open>Functorial structure\<close>
Andreas@63243
   436
Andreas@63243
   437
abbreviation map_spmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf"
Andreas@63243
   438
where "map_spmf f \<equiv> map_pmf (map_option f)"
Andreas@63243
   439
Andreas@63243
   440
context begin
wenzelm@63308
   441
local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "spmf")\<close>
Andreas@63243
   442
Andreas@63243
   443
lemma map_comp: "map_spmf f (map_spmf g p) = map_spmf (f \<circ> g) p"
Andreas@63243
   444
by(simp add: pmf.map_comp o_def option.map_comp)
Andreas@63243
   445
Andreas@63243
   446
lemma map_id0: "map_spmf id = id"
Andreas@63243
   447
by(simp add: pmf.map_id option.map_id0)
Andreas@63243
   448
Andreas@63243
   449
lemma map_id [simp]: "map_spmf id p = p"
Andreas@63243
   450
by(simp add: map_id0)
Andreas@63243
   451
Andreas@63243
   452
lemma map_ident [simp]: "map_spmf (\<lambda>x. x) p = p"
Andreas@63243
   453
by(simp add: id_def[symmetric])
Andreas@63243
   454
Andreas@63243
   455
end
Andreas@63243
   456
Andreas@63243
   457
lemma set_map_spmf [simp]: "set_spmf (map_spmf f p) = f ` set_spmf p"
Andreas@63243
   458
by(simp add: set_spmf_def image_bind bind_image o_def Option.option.set_map)
hoelzl@63333
   459
Andreas@63243
   460
lemma map_spmf_cong:
Andreas@63243
   461
  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q \<Longrightarrow> f x = g x \<rbrakk>
Andreas@63243
   462
  \<Longrightarrow> map_spmf f p = map_spmf g q"
Andreas@63243
   463
by(auto intro: pmf.map_cong option.map_cong simp add: in_set_spmf)
Andreas@63243
   464
Andreas@63243
   465
lemma map_spmf_cong_simp:
Andreas@63243
   466
  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q =simp=> f x = g x \<rbrakk>
Andreas@63243
   467
  \<Longrightarrow> map_spmf f p = map_spmf g q"
Andreas@63243
   468
unfolding simp_implies_def by(rule map_spmf_cong)
Andreas@63243
   469
Andreas@63243
   470
lemma map_spmf_idI: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_spmf f p = p"
Andreas@63243
   471
by(rule map_pmf_idI map_option_idI)+(simp add: in_set_spmf)
Andreas@63243
   472
Andreas@63243
   473
lemma emeasure_map_spmf:
Andreas@63243
   474
  "emeasure (measure_spmf (map_spmf f p)) A = emeasure (measure_spmf p) (f -` A)"
Andreas@63243
   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])
Andreas@63243
   476
Andreas@63243
   477
lemma measure_map_spmf: "measure (measure_spmf (map_spmf f p)) A = measure (measure_spmf p) (f -` A)"
Andreas@63243
   478
using emeasure_map_spmf[of f p A] by(simp add: measure_spmf.emeasure_eq_measure)
Andreas@63243
   479
Andreas@63243
   480
lemma measure_map_spmf_conv_distr:
Andreas@63243
   481
  "measure_spmf (map_spmf f p) = distr (measure_spmf p) (count_space UNIV) f"
Andreas@63243
   482
by(rule measure_eqI)(simp_all add: emeasure_map_spmf emeasure_distr)
Andreas@63243
   483
Andreas@63243
   484
lemma spmf_map_pmf_Some [simp]: "spmf (map_pmf Some p) i = pmf p i"
Andreas@63243
   485
by(simp add: pmf_map_inj')
Andreas@63243
   486
Andreas@63243
   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"
Andreas@63243
   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])
Andreas@63243
   489
Andreas@63243
   490
lemma spmf_map_inj': "inj f \<Longrightarrow> spmf (map_spmf f M) (f x) = spmf M x"
Andreas@63243
   491
by(subst option.map(2)[symmetric, where f=f])(rule pmf_map_inj'[OF option.inj_map])
Andreas@63243
   492
Andreas@63243
   493
lemma spmf_map_outside: "x \<notin> f ` set_spmf M \<Longrightarrow> spmf (map_spmf f M) x = 0"
Andreas@63243
   494
unfolding spmf_eq_0_set_spmf by simp
Andreas@63243
   495
Andreas@63243
   496
lemma ennreal_spmf_map: "ennreal (spmf (map_spmf f p) x) = emeasure (measure_spmf p) (f -` {x})"
Andreas@63243
   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])
Andreas@63243
   498
Andreas@63243
   499
lemma spmf_map: "spmf (map_spmf f p) x = measure (measure_spmf p) (f -` {x})"
Andreas@63243
   500
using ennreal_spmf_map[of f p x] by(simp add: measure_spmf.emeasure_eq_measure)
Andreas@63243
   501
Andreas@63243
   502
lemma ennreal_spmf_map_conv_nn_integral:
Andreas@63243
   503
  "ennreal (spmf (map_spmf f p) x) = integral\<^sup>N (measure_spmf p) (indicator (f -` {x}))"
Andreas@63243
   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])
Andreas@63243
   505
wenzelm@63308
   506
subsection \<open>Monad operations\<close>
wenzelm@63308
   507
wenzelm@63308
   508
subsubsection \<open>Return\<close>
Andreas@63243
   509
Andreas@63243
   510
abbreviation return_spmf :: "'a \<Rightarrow> 'a spmf"
Andreas@63243
   511
where "return_spmf x \<equiv> return_pmf (Some x)"
Andreas@63243
   512
Andreas@63243
   513
lemma pmf_return_spmf: "pmf (return_spmf x) y = indicator {y} (Some x)"
Andreas@63243
   514
by(fact pmf_return)
Andreas@63243
   515
Andreas@63243
   516
lemma measure_spmf_return_spmf: "measure_spmf (return_spmf x) = Giry_Monad.return (count_space UNIV) x"
Andreas@63243
   517
by(rule measure_eqI)(simp_all add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space indicator_def)
Andreas@63243
   518
Andreas@63243
   519
lemma measure_spmf_return_pmf_None [simp]: "measure_spmf (return_pmf None) = null_measure (count_space UNIV)"
Andreas@63243
   520
by(rule measure_eqI)(auto simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space indicator_eq_0_iff)
Andreas@63243
   521
Andreas@63243
   522
lemma set_return_spmf [simp]: "set_spmf (return_spmf x) = {x}"
Andreas@63243
   523
by(auto simp add: set_spmf_def)
Andreas@63243
   524
wenzelm@63308
   525
subsubsection \<open>Bind\<close>
Andreas@63243
   526
Andreas@63243
   527
definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
Andreas@63243
   528
where "bind_spmf x f = bind_pmf x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
Andreas@63243
   529
Andreas@63243
   530
adhoc_overloading Monad_Syntax.bind bind_spmf
Andreas@63243
   531
Andreas@63243
   532
lemma return_None_bind_spmf [simp]: "return_pmf None \<bind> (f :: 'a \<Rightarrow> _) = return_pmf None"
Andreas@63243
   533
by(simp add: bind_spmf_def bind_return_pmf)
Andreas@63243
   534
Andreas@63243
   535
lemma return_bind_spmf [simp]: "return_spmf x \<bind> f = f x"
Andreas@63243
   536
by(simp add: bind_spmf_def bind_return_pmf)
Andreas@63243
   537
Andreas@63243
   538
lemma bind_return_spmf [simp]: "x \<bind> return_spmf = x"
Andreas@63243
   539
proof -
Andreas@63243
   540
  have "\<And>a :: 'a option. (case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> return_spmf a') = return_pmf a"
Andreas@63243
   541
    by(simp split: option.split)
Andreas@63243
   542
  then show ?thesis
Andreas@63243
   543
    by(simp add: bind_spmf_def bind_return_pmf')
Andreas@63243
   544
qed
Andreas@63243
   545
Andreas@63243
   546
lemma bind_spmf_assoc [simp]:
Andreas@63243
   547
  fixes x :: "'a spmf" and f :: "'a \<Rightarrow> 'b spmf" and g :: "'b \<Rightarrow> 'c spmf"
Andreas@63243
   548
  shows "(x \<bind> f) \<bind> g = x \<bind> (\<lambda>y. f y \<bind> g)"
Andreas@63243
   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"])
Andreas@63243
   550
Andreas@63243
   551
lemma pmf_bind_spmf_None: "pmf (p \<bind> f) None = pmf p None + \<integral> x. pmf (f x) None \<partial>measure_spmf p"
Andreas@63243
   552
  (is "?lhs = ?rhs")
Andreas@63243
   553
proof -
Andreas@63243
   554
  let ?f = "\<lambda>x. pmf (case x of None \<Rightarrow> return_pmf None | Some x \<Rightarrow> f x) None"
Andreas@63243
   555
  have "?lhs = \<integral> x. ?f x \<partial>measure_pmf p"
Andreas@63243
   556
    by(simp add: bind_spmf_def pmf_bind)
Andreas@63243
   557
  also have "\<dots> = \<integral> x. ?f None * indicator {None} x + ?f x * indicator (range Some) x \<partial>measure_pmf p"
Andreas@63243
   558
    by(rule integral_cong)(auto simp add: indicator_def)
Andreas@63243
   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)"
Andreas@63243
   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)
Andreas@63243
   561
  also have "\<dots> = pmf p None + \<integral> x. indicator (range Some) x * pmf (f (the x)) None \<partial>measure_pmf p"
Andreas@63243
   562
    by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: integral_cong)
Andreas@63243
   563
  also have "\<dots> = ?rhs" unfolding measure_spmf_def
Andreas@63243
   564
    by(subst integral_distr)(auto simp add: integral_restrict_space)
Andreas@63243
   565
  finally show ?thesis .
Andreas@63243
   566
qed
Andreas@63243
   567
Andreas@63243
   568
lemma spmf_bind: "spmf (p \<bind> f) y = \<integral> x. spmf (f x) y \<partial>measure_spmf p"
Andreas@63243
   569
unfolding measure_spmf_def
Andreas@63243
   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)
Andreas@63243
   571
Andreas@63243
   572
lemma ennreal_spmf_bind: "ennreal (spmf (p \<bind> f) x) = \<integral>\<^sup>+ y. spmf (f y) x \<partial>measure_spmf p"
Andreas@63243
   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)
Andreas@63243
   574
Andreas@63243
   575
lemma measure_spmf_bind_pmf: "measure_spmf (p \<bind> f) = measure_pmf p \<bind> measure_spmf \<circ> f"
Andreas@63243
   576
  (is "?lhs = ?rhs")
Andreas@63243
   577
proof(rule measure_eqI)
Andreas@63243
   578
  show "sets ?lhs = sets ?rhs"
Andreas@63243
   579
    by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf)
Andreas@63243
   580
next
Andreas@63243
   581
  fix A :: "'a set"
hoelzl@63333
   582
  have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_pmf p"
Andreas@63243
   583
    by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
Andreas@63243
   584
  also have "\<dots> = emeasure ?rhs A"
Andreas@63243
   585
    by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
Andreas@63243
   586
  finally show "emeasure ?lhs A = emeasure ?rhs A" .
Andreas@63243
   587
qed
Andreas@63243
   588
Andreas@63243
   589
lemma measure_spmf_bind: "measure_spmf (p \<bind> f) = measure_spmf p \<bind> measure_spmf \<circ> f"
Andreas@63243
   590
  (is "?lhs = ?rhs")
Andreas@63243
   591
proof(rule measure_eqI)
Andreas@63243
   592
  show "sets ?lhs = sets ?rhs"
Andreas@63243
   593
    by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf)
Andreas@63243
   594
next
Andreas@63243
   595
  fix A :: "'a set"
Andreas@63243
   596
  let ?A = "the -` A \<inter> range Some"
hoelzl@63333
   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"
Andreas@63243
   598
    by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
Andreas@63243
   599
  also have "\<dots> =  \<integral>\<^sup>+ x. emeasure (measure_pmf (f (the x))) ?A * indicator (range Some) x \<partial>measure_pmf p"
Andreas@63243
   600
    by(rule nn_integral_cong)(auto split: option.split simp add: indicator_def)
Andreas@63243
   601
  also have "\<dots> = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_spmf p"
Andreas@63243
   602
    by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space emeasure_distr space_restrict_space emeasure_restrict_space)
hoelzl@63333
   603
  also have "\<dots> = emeasure ?rhs A"
Andreas@63243
   604
    by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
Andreas@63243
   605
  finally show "emeasure ?lhs A = emeasure ?rhs A" .
Andreas@63243
   606
qed
Andreas@63243
   607
Andreas@63243
   608
lemma map_spmf_bind_spmf: "map_spmf f (bind_spmf p g) = bind_spmf p (map_spmf f \<circ> g)"
Andreas@63243
   609
by(auto simp add: bind_spmf_def map_bind_pmf fun_eq_iff split: option.split intro: arg_cong2[where f=bind_pmf])
Andreas@63243
   610
Andreas@63243
   611
lemma bind_map_spmf: "map_spmf f p \<bind> g = p \<bind> g \<circ> f"
Andreas@63243
   612
by(simp add: bind_spmf_def bind_map_pmf o_def cong del: option.case_cong_weak)
Andreas@63243
   613
Andreas@63243
   614
lemma spmf_bind_leI:
Andreas@63243
   615
  assumes "\<And>y. y \<in> set_spmf p \<Longrightarrow> spmf (f y) x \<le> r"
Andreas@63243
   616
  and "0 \<le> r"
Andreas@63243
   617
  shows "spmf (bind_spmf p f) x \<le> r"
Andreas@63243
   618
proof -
Andreas@63243
   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)
Andreas@63243
   620
  also have "\<dots> \<le> \<integral>\<^sup>+ y. r \<partial>measure_spmf p" by(rule nn_integral_mono_AE)(simp add: assms)
Andreas@63243
   621
  also have "\<dots> \<le> r" using assms measure_spmf.emeasure_space_le_1
Andreas@63243
   622
    by(auto simp add: measure_spmf.emeasure_eq_measure intro!: mult_left_le)
Andreas@63243
   623
  finally show ?thesis using assms(2) by(simp)
Andreas@63243
   624
qed
Andreas@63243
   625
Andreas@63243
   626
lemma map_spmf_conv_bind_spmf: "map_spmf f p = (p \<bind> (\<lambda>x. return_spmf (f x)))"
Andreas@63243
   627
by(simp add: map_pmf_def bind_spmf_def)(rule bind_pmf_cong, simp_all split: option.split)
Andreas@63243
   628
Andreas@63243
   629
lemma bind_spmf_cong:
Andreas@63243
   630
  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q \<Longrightarrow> f x = g x \<rbrakk>
Andreas@63243
   631
  \<Longrightarrow> bind_spmf p f = bind_spmf q g"
Andreas@63243
   632
by(auto simp add: bind_spmf_def in_set_spmf intro: bind_pmf_cong option.case_cong)
Andreas@63243
   633
Andreas@63243
   634
lemma bind_spmf_cong_simp:
Andreas@63243
   635
  "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q =simp=> f x = g x \<rbrakk>
Andreas@63243
   636
  \<Longrightarrow> bind_spmf p f = bind_spmf q g"
Andreas@63243
   637
by(simp add: simp_implies_def cong: bind_spmf_cong)
Andreas@63243
   638
Andreas@63243
   639
lemma set_bind_spmf: "set_spmf (M \<bind> f) = set_spmf M \<bind> (set_spmf \<circ> f)"
Andreas@63243
   640
by(auto simp add: set_spmf_def bind_spmf_def bind_UNION split: option.splits)
Andreas@63243
   641
Andreas@63243
   642
lemma bind_spmf_const_return_None [simp]: "bind_spmf p (\<lambda>_. return_pmf None) = return_pmf None"
Andreas@63243
   643
by(simp add: bind_spmf_def case_option_collapse)
Andreas@63243
   644
Andreas@63243
   645
lemma bind_commute_spmf:
Andreas@63243
   646
  "bind_spmf p (\<lambda>x. bind_spmf q (f x)) = bind_spmf q (\<lambda>y. bind_spmf p (\<lambda>x. f x y))"
Andreas@63243
   647
  (is "?lhs = ?rhs")
Andreas@63243
   648
proof -
Andreas@63243
   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)"
Andreas@63243
   650
  have "?lhs = p \<bind> (\<lambda>x. q \<bind> ?f x)"
Andreas@63243
   651
    unfolding bind_spmf_def by(rule bind_pmf_cong[OF refl])(simp split: option.split)
Andreas@63243
   652
  also have "\<dots> = q \<bind> (\<lambda>y. p \<bind> (\<lambda>x. ?f x y))" by(rule bind_commute_pmf)
Andreas@63243
   653
  also have "\<dots> = ?rhs" unfolding bind_spmf_def
Andreas@63243
   654
    by(rule bind_pmf_cong[OF refl])(auto split: option.split, metis bind_spmf_const_return_None bind_spmf_def)
Andreas@63243
   655
  finally show ?thesis .
Andreas@63243
   656
qed
Andreas@63243
   657
wenzelm@63308
   658
subsection \<open>Relator\<close>
Andreas@63243
   659
Andreas@63243
   660
abbreviation rel_spmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf \<Rightarrow> bool"
Andreas@63243
   661
where "rel_spmf R \<equiv> rel_pmf (rel_option R)"
Andreas@63243
   662
Andreas@63243
   663
lemma rel_pmf_mono:
Andreas@63243
   664
  "\<lbrakk>rel_pmf A f g; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_pmf B f g"
Andreas@63243
   665
using pmf.rel_mono[of A B] by(simp add: le_fun_def)
Andreas@63243
   666
Andreas@63243
   667
lemma rel_spmf_mono:
Andreas@63243
   668
  "\<lbrakk>rel_spmf A f g; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_spmf B f g"
hoelzl@63333
   669
apply(erule rel_pmf_mono)
Andreas@63243
   670
using option.rel_mono[of A B] by(simp add: le_fun_def)
Andreas@63243
   671
Andreas@63243
   672
lemma rel_spmf_mono_strong:
Andreas@63243
   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"
Andreas@63243
   674
apply(erule pmf.rel_mono_strong)
Andreas@63243
   675
apply(erule option.rel_mono_strong)
Andreas@63243
   676
apply(auto simp add: in_set_spmf)
Andreas@63243
   677
done
Andreas@63243
   678
Andreas@63243
   679
lemma rel_spmf_reflI: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> P x x) \<Longrightarrow> rel_spmf P p p"
Andreas@63243
   680
by(rule rel_pmf_reflI)(auto simp add: set_spmf_def intro: rel_option_reflI)
Andreas@63243
   681
Andreas@63243
   682
lemma rel_spmfI [intro?]:
Andreas@63243
   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>
Andreas@63243
   684
  \<Longrightarrow> rel_spmf P p q"
Andreas@63243
   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"])
Andreas@63243
   686
  (auto simp add: pmf.map_comp o_def in_set_spmf split: option.splits intro: pmf.map_cong)
Andreas@63243
   687
Andreas@63243
   688
lemma rel_spmfE [elim?, consumes 1, case_names rel_spmf]:
Andreas@63243
   689
  assumes "rel_spmf P p q"
hoelzl@63333
   690
  obtains pq where
Andreas@63243
   691
    "\<And>x y. (x, y) \<in> set_spmf pq \<Longrightarrow> P x y"
Andreas@63243
   692
    "p = map_spmf fst pq"
Andreas@63243
   693
    "q = map_spmf snd pq"
Andreas@63243
   694
using assms
Andreas@63243
   695
proof(cases rule: rel_pmf.cases[consumes 1, case_names rel_pmf])
Andreas@63243
   696
  case (rel_pmf pq)
Andreas@63243
   697
  let ?pq = "map_pmf (\<lambda>(a, b). case (a, b) of (Some x, Some y) \<Rightarrow> Some (x, y) | _ \<Rightarrow> None) pq"
Andreas@63243
   698
  have "\<And>x y. (x, y) \<in> set_spmf ?pq \<Longrightarrow> P x y"
Andreas@63243
   699
    by(auto simp add: in_set_spmf split: option.split_asm dest: rel_pmf(1))
Andreas@63243
   700
  moreover
Andreas@63243
   701
  have "\<And>x. (x, None) \<in> set_pmf pq \<Longrightarrow> x = None" by(auto dest!: rel_pmf(1))
Andreas@63243
   702
  then have "p = map_spmf fst ?pq" using rel_pmf(2)
Andreas@63243
   703
    by(auto simp add: pmf.map_comp split_beta intro!: pmf.map_cong split: option.split)
Andreas@63243
   704
  moreover
Andreas@63243
   705
  have "\<And>y. (None, y) \<in> set_pmf pq \<Longrightarrow> y = None" by(auto dest!: rel_pmf(1))
Andreas@63243
   706
  then have "q = map_spmf snd ?pq" using rel_pmf(3)
Andreas@63243
   707
    by(auto simp add: pmf.map_comp split_beta intro!: pmf.map_cong split: option.split)
Andreas@63243
   708
  ultimately show thesis ..
Andreas@63243
   709
qed
Andreas@63243
   710
Andreas@63243
   711
lemma rel_spmf_simps:
Andreas@63243
   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)"
Andreas@63243
   713
by(auto intro: rel_spmfI elim!: rel_spmfE)
Andreas@63243
   714
Andreas@63243
   715
lemma spmf_rel_map:
Andreas@63243
   716
  shows spmf_rel_map1: "\<And>R f x. rel_spmf R (map_spmf f x) = rel_spmf (\<lambda>x. R (f x)) x"
Andreas@63243
   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"
Andreas@63243
   718
by(simp_all add: fun_eq_iff pmf.rel_map option.rel_map[abs_def])
Andreas@63243
   719
Andreas@63243
   720
lemma spmf_rel_conversep: "rel_spmf R\<inverse>\<inverse> = (rel_spmf R)\<inverse>\<inverse>"
Andreas@63243
   721
by(simp add: option.rel_conversep pmf.rel_conversep)
Andreas@63243
   722
Andreas@63243
   723
lemma spmf_rel_eq: "rel_spmf op = = op ="
Andreas@63243
   724
by(simp add: pmf.rel_eq option.rel_eq)
Andreas@63243
   725
wenzelm@63343
   726
context includes lifting_syntax
wenzelm@63343
   727
begin
Andreas@63243
   728
Andreas@63243
   729
lemma bind_spmf_parametric [transfer_rule]:
Andreas@63243
   730
  "(rel_spmf A ===> (A ===> rel_spmf B) ===> rel_spmf B) bind_spmf bind_spmf"
Andreas@63243
   731
unfolding bind_spmf_def[abs_def] by transfer_prover
Andreas@63243
   732
Andreas@63243
   733
lemma return_spmf_parametric: "(A ===> rel_spmf A) return_spmf return_spmf"
Andreas@63243
   734
by transfer_prover
Andreas@63243
   735
Andreas@63243
   736
lemma map_spmf_parametric: "((A ===> B) ===> rel_spmf A ===> rel_spmf B) map_spmf map_spmf"
Andreas@63243
   737
by transfer_prover
Andreas@63243
   738
Andreas@63243
   739
lemma rel_spmf_parametric:
Andreas@63243
   740
  "((A ===> B ===> op =) ===> rel_spmf A ===> rel_spmf B ===> op =) rel_spmf rel_spmf"
Andreas@63243
   741
by transfer_prover
Andreas@63243
   742
Andreas@63243
   743
lemma set_spmf_parametric [transfer_rule]:
Andreas@63243
   744
  "(rel_spmf A ===> rel_set A) set_spmf set_spmf"
Andreas@63243
   745
unfolding set_spmf_def[abs_def] by transfer_prover
Andreas@63243
   746
Andreas@63243
   747
lemma return_spmf_None_parametric:
Andreas@63243
   748
  "(rel_spmf A) (return_pmf None) (return_pmf None)"
Andreas@63243
   749
by simp
Andreas@63243
   750
Andreas@63243
   751
end
Andreas@63243
   752
Andreas@63243
   753
lemma rel_spmf_bindI:
Andreas@63243
   754
  "\<lbrakk> rel_spmf R p q; \<And>x y. R x y \<Longrightarrow> rel_spmf P (f x) (g y) \<rbrakk>
Andreas@63243
   755
  \<Longrightarrow> rel_spmf P (p \<bind> f) (q \<bind> g)"
Andreas@63243
   756
by(fact bind_spmf_parametric[THEN rel_funD, THEN rel_funD, OF _ rel_funI])
Andreas@63243
   757
Andreas@63243
   758
lemma rel_spmf_bind_reflI:
Andreas@63243
   759
  "(\<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)"
Andreas@63243
   760
by(rule rel_spmf_bindI[where R="\<lambda>x y. x = y \<and> x \<in> set_spmf p"])(auto intro: rel_spmf_reflI)
Andreas@63243
   761
Andreas@63243
   762
lemma rel_pmf_return_pmfI: "P x y \<Longrightarrow> rel_pmf P (return_pmf x) (return_pmf y)"
Andreas@63243
   763
by(rule rel_pmf.intros[where pq="return_pmf (x, y)"])(simp_all)
Andreas@63243
   764
wenzelm@63343
   765
context includes lifting_syntax
wenzelm@63343
   766
begin
wenzelm@63343
   767
Andreas@63243
   768
text \<open>We do not yet have a relator for @{typ "'a measure"}, so we combine @{const measure} and @{const measure_pmf}\<close>
Andreas@63243
   769
lemma measure_pmf_parametric:
Andreas@63243
   770
  "(rel_pmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
Andreas@63243
   771
proof(rule rel_funI)+
Andreas@63243
   772
  fix p q X Y
Andreas@63243
   773
  assume "rel_pmf A p q" and "rel_pred A X Y"
Andreas@63243
   774
  from this(1) obtain pq where A: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> A x y"
Andreas@63243
   775
    and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
Andreas@63243
   776
  show "measure p X = measure q Y" unfolding p q measure_map_pmf
Andreas@63243
   777
    by(rule measure_pmf.finite_measure_eq_AE)(auto simp add: AE_measure_pmf_iff dest!: A rel_predD[OF \<open>rel_pred _ _ _\<close>])
Andreas@63243
   778
qed
Andreas@63243
   779
Andreas@63243
   780
lemma measure_spmf_parametric:
Andreas@63243
   781
  "(rel_spmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_spmf p)) (\<lambda>q. measure (measure_spmf q))"
Andreas@63243
   782
unfolding measure_measure_spmf_conv_measure_pmf[abs_def]
Andreas@63243
   783
apply(rule rel_funI)+
Andreas@63243
   784
apply(erule measure_pmf_parametric[THEN rel_funD, THEN rel_funD])
Andreas@63243
   785
apply(auto simp add: rel_pred_def rel_fun_def elim: option.rel_cases)
Andreas@63243
   786
done
wenzelm@63343
   787
Andreas@63243
   788
end
Andreas@63243
   789
wenzelm@63308
   790
subsection \<open>From @{typ "'a pmf"} to @{typ "'a spmf"}\<close>
Andreas@63243
   791
Andreas@63243
   792
definition spmf_of_pmf :: "'a pmf \<Rightarrow> 'a spmf"
Andreas@63243
   793
where "spmf_of_pmf = map_pmf Some"
Andreas@63243
   794
Andreas@63243
   795
lemma set_spmf_spmf_of_pmf [simp]: "set_spmf (spmf_of_pmf p) = set_pmf p"
Andreas@63243
   796
by(auto simp add: spmf_of_pmf_def set_spmf_def bind_image o_def)
Andreas@63243
   797
Andreas@63243
   798
lemma spmf_spmf_of_pmf [simp]: "spmf (spmf_of_pmf p) x = pmf p x"
Andreas@63243
   799
by(simp add: spmf_of_pmf_def)
Andreas@63243
   800
Andreas@63243
   801
lemma pmf_spmf_of_pmf_None [simp]: "pmf (spmf_of_pmf p) None = 0"
Andreas@63243
   802
using ennreal_pmf_map[of Some p None] by(simp add: spmf_of_pmf_def)
Andreas@63243
   803
Andreas@63243
   804
lemma emeasure_spmf_of_pmf [simp]: "emeasure (measure_spmf (spmf_of_pmf p)) A = emeasure (measure_pmf p) A"
Andreas@63243
   805
by(simp add: emeasure_measure_spmf_conv_measure_pmf spmf_of_pmf_def inj_vimage_image_eq)
Andreas@63243
   806
Andreas@63243
   807
lemma measure_spmf_spmf_of_pmf [simp]: "measure_spmf (spmf_of_pmf p) = measure_pmf p"
Andreas@63243
   808
by(rule measure_eqI) simp_all
Andreas@63243
   809
Andreas@63243
   810
lemma map_spmf_of_pmf [simp]: "map_spmf f (spmf_of_pmf p) = spmf_of_pmf (map_pmf f p)"
Andreas@63243
   811
by(simp add: spmf_of_pmf_def pmf.map_comp o_def)
Andreas@63243
   812
Andreas@63243
   813
lemma rel_spmf_spmf_of_pmf [simp]: "rel_spmf R (spmf_of_pmf p) (spmf_of_pmf q) = rel_pmf R p q"
Andreas@63243
   814
by(simp add: spmf_of_pmf_def pmf.rel_map)
Andreas@63243
   815
Andreas@63243
   816
lemma spmf_of_pmf_return_pmf [simp]: "spmf_of_pmf (return_pmf x) = return_spmf x"
Andreas@63243
   817
by(simp add: spmf_of_pmf_def)
Andreas@63243
   818
Andreas@63243
   819
lemma bind_spmf_of_pmf [simp]: "bind_spmf (spmf_of_pmf p) f = bind_pmf p f"
Andreas@63243
   820
by(simp add: spmf_of_pmf_def bind_spmf_def bind_map_pmf)
Andreas@63243
   821
Andreas@63243
   822
lemma set_spmf_bind_pmf: "set_spmf (bind_pmf p f) = Set.bind (set_pmf p) (set_spmf \<circ> f)"
Andreas@63243
   823
unfolding bind_spmf_of_pmf[symmetric] by(subst set_bind_spmf) simp
Andreas@63243
   824
Andreas@63243
   825
lemma spmf_of_pmf_bind: "spmf_of_pmf (bind_pmf p f) = bind_pmf p (\<lambda>x. spmf_of_pmf (f x))"
Andreas@63243
   826
by(simp add: spmf_of_pmf_def map_bind_pmf)
Andreas@63243
   827
Andreas@63243
   828
lemma bind_pmf_return_spmf: "p \<bind> (\<lambda>x. return_spmf (f x)) = spmf_of_pmf (map_pmf f p)"
Andreas@63243
   829
by(simp add: map_pmf_def spmf_of_pmf_bind)
Andreas@63243
   830
wenzelm@63308
   831
subsection \<open>Weight of a subprobability\<close>
Andreas@63243
   832
Andreas@63243
   833
abbreviation weight_spmf :: "'a spmf \<Rightarrow> real"
Andreas@63243
   834
where "weight_spmf p \<equiv> measure (measure_spmf p) (space (measure_spmf p))"
Andreas@63243
   835
Andreas@63243
   836
lemma weight_spmf_def: "weight_spmf p = measure (measure_spmf p) UNIV"
Andreas@63243
   837
by(simp add: space_measure_spmf)
Andreas@63243
   838
Andreas@63243
   839
lemma weight_spmf_le_1: "weight_spmf p \<le> 1"
Andreas@63243
   840
by(simp add: measure_spmf.subprob_measure_le_1)
Andreas@63243
   841
Andreas@63243
   842
lemma weight_return_spmf [simp]: "weight_spmf (return_spmf x) = 1"
Andreas@63243
   843
by(simp add: measure_spmf_return_spmf measure_return)
Andreas@63243
   844
Andreas@63243
   845
lemma weight_return_pmf_None [simp]: "weight_spmf (return_pmf None) = 0"
Andreas@63243
   846
by(simp)
Andreas@63243
   847
Andreas@63243
   848
lemma weight_map_spmf [simp]: "weight_spmf (map_spmf f p) = weight_spmf p"
Andreas@63243
   849
by(simp add: weight_spmf_def measure_map_spmf)
Andreas@63243
   850
Andreas@63243
   851
lemma weight_spmf_of_pmf [simp]: "weight_spmf (spmf_of_pmf p) = 1"
Andreas@63243
   852
using measure_pmf.prob_space[of p] by(simp add: spmf_of_pmf_def weight_spmf_def)
Andreas@63243
   853
Andreas@63243
   854
lemma weight_spmf_nonneg: "weight_spmf p \<ge> 0"
Andreas@63243
   855
by(fact measure_nonneg)
Andreas@63243
   856
hoelzl@63333
   857
lemma (in finite_measure) integrable_weight_spmf [simp]:
Andreas@63243
   858
  "(\<lambda>x. weight_spmf (f x)) \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. weight_spmf (f x))"
Andreas@63243
   859
by(rule integrable_const_bound[where B=1])(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
Andreas@63243
   860
Andreas@63243
   861
lemma weight_spmf_eq_nn_integral_spmf: "weight_spmf p = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
Andreas@63243
   862
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)
Andreas@63243
   863
Andreas@63243
   864
lemma weight_spmf_eq_nn_integral_support:
Andreas@63243
   865
  "weight_spmf p = \<integral>\<^sup>+ x. spmf p x \<partial>count_space (set_spmf p)"
Andreas@63243
   866
unfolding weight_spmf_eq_nn_integral_spmf
Andreas@63243
   867
by(auto simp add: nn_integral_count_space_indicator in_set_spmf_iff_spmf intro!: nn_integral_cong split: split_indicator)
Andreas@63243
   868
Andreas@63243
   869
lemma pmf_None_eq_weight_spmf: "pmf p None = 1 - weight_spmf p"
Andreas@63243
   870
proof -
Andreas@63243
   871
  have "weight_spmf p = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV" by(rule weight_spmf_eq_nn_integral_spmf)
Andreas@63243
   872
  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator (range Some) x \<partial>count_space UNIV"
Andreas@63243
   873
    by(simp add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] nn_integral_embed_measure measurable_embed_measure1)
Andreas@63243
   874
  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"
Andreas@63243
   875
    by(subst nn_integral_add)(simp_all add: max_def)
Andreas@63243
   876
  also have "\<dots> = \<integral>\<^sup>+ x. pmf p x \<partial>count_space UNIV"
Andreas@63243
   877
    by(rule nn_integral_cong)(auto split: split_indicator)
Andreas@63243
   878
  also have "\<dots> = 1" by (simp add: nn_integral_pmf)
Andreas@63243
   879
  finally show ?thesis by(simp add: ennreal_plus[symmetric] del: ennreal_plus)
Andreas@63243
   880
qed
Andreas@63243
   881
Andreas@63243
   882
lemma weight_spmf_conv_pmf_None: "weight_spmf p = 1 - pmf p None"
Andreas@63243
   883
by(simp add: pmf_None_eq_weight_spmf)
Andreas@63243
   884
Andreas@63243
   885
lemma weight_spmf_le_0: "weight_spmf p \<le> 0 \<longleftrightarrow> weight_spmf p = 0"
Andreas@63243
   886
by(rule measure_le_0_iff)
Andreas@63243
   887
Andreas@63243
   888
lemma weight_spmf_lt_0: "\<not> weight_spmf p < 0"
Andreas@63243
   889
by(simp add: not_less weight_spmf_nonneg)
Andreas@63243
   890
Andreas@63243
   891
lemma spmf_le_weight: "spmf p x \<le> weight_spmf p"
Andreas@63243
   892
proof -
Andreas@63243
   893
  have "ennreal (spmf p x) \<le> weight_spmf p"
Andreas@63243
   894
    unfolding weight_spmf_eq_nn_integral_spmf by(rule nn_integral_ge_point) simp
Andreas@63243
   895
  then show ?thesis by simp
Andreas@63243
   896
qed
Andreas@63243
   897
Andreas@63243
   898
lemma weight_spmf_eq_0: "weight_spmf p = 0 \<longleftrightarrow> p = return_pmf None"
Andreas@63243
   899
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)
Andreas@63243
   900
Andreas@63243
   901
lemma weight_bind_spmf: "weight_spmf (x \<bind> f) = lebesgue_integral (measure_spmf x) (weight_spmf \<circ> f)"
Andreas@63243
   902
unfolding weight_spmf_def
Andreas@63243
   903
by(simp add: measure_spmf_bind o_def measure_spmf.measure_bind[where N="count_space UNIV"])
Andreas@63243
   904
Andreas@63243
   905
lemma rel_spmf_weightD: "rel_spmf A p q \<Longrightarrow> weight_spmf p = weight_spmf q"
Andreas@63243
   906
by(erule rel_spmfE) simp
Andreas@63243
   907
Andreas@63243
   908
lemma rel_spmf_bij_betw:
Andreas@63243
   909
  assumes f: "bij_betw f (set_spmf p) (set_spmf q)"
Andreas@63243
   910
  and eq: "\<And>x. x \<in> set_spmf p \<Longrightarrow> spmf p x = spmf q (f x)"
Andreas@63243
   911
  shows "rel_spmf (\<lambda>x y. f x = y) p q"
Andreas@63243
   912
proof -
Andreas@63243
   913
  let ?f = "map_option f"
Andreas@63243
   914
Andreas@63243
   915
  have weq: "ennreal (weight_spmf p) = ennreal (weight_spmf q)"
Andreas@63243
   916
    unfolding weight_spmf_eq_nn_integral_support
Andreas@63243
   917
    by(subst nn_integral_bij_count_space[OF f, symmetric])(rule nn_integral_cong_AE, simp add: eq AE_count_space)
Andreas@63243
   918
  then have "None \<in> set_pmf p \<longleftrightarrow> None \<in> set_pmf q"
Andreas@63243
   919
    by(simp add: pmf_None_eq_weight_spmf set_pmf_iff)
Andreas@63243
   920
  with f have "bij_betw (map_option f) (set_pmf p) (set_pmf q)"
Andreas@63243
   921
    apply(auto simp add: bij_betw_def in_set_spmf inj_on_def intro: option.expand)
Andreas@63243
   922
    apply(rename_tac [!] x)
Andreas@63243
   923
    apply(case_tac [!] x)
Andreas@63243
   924
    apply(auto iff: in_set_spmf)
Andreas@63243
   925
    done
Andreas@63243
   926
  then have "rel_pmf (\<lambda>x y. ?f x = y) p q"
Andreas@63243
   927
    by(rule rel_pmf_bij_betw)(case_tac x, simp_all add: weq[simplified] eq in_set_spmf pmf_None_eq_weight_spmf)
Andreas@63243
   928
  thus ?thesis by(rule pmf.rel_mono_strong)(auto intro!: rel_optionI simp add: Option.is_none_def)
Andreas@63243
   929
qed
Andreas@63243
   930
wenzelm@63308
   931
subsection \<open>From density to spmfs\<close>
Andreas@63243
   932
Andreas@63243
   933
context fixes f :: "'a \<Rightarrow> real" begin
Andreas@63243
   934
Andreas@63243
   935
definition embed_spmf :: "'a spmf"
Andreas@63243
   936
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'))"
Andreas@63243
   937
Andreas@63243
   938
context
Andreas@63243
   939
  assumes prob: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV) \<le> 1"
Andreas@63243
   940
begin
Andreas@63243
   941
Andreas@63243
   942
lemma nn_integral_embed_spmf_eq_1:
Andreas@63243
   943
  "(\<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"
Andreas@63243
   944
  (is "?lhs = _" is "(\<integral>\<^sup>+ x. ?f x \<partial>?M) = _")
Andreas@63243
   945
proof -
Andreas@63243
   946
  have "?lhs = \<integral>\<^sup>+ x. ?f x * indicator {None} x + ?f x * indicator (range Some) x \<partial>?M"
Andreas@63243
   947
    by(rule nn_integral_cong)(auto split: split_indicator)
Andreas@63243
   948
  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"
Andreas@63243
   949
    (is "_ = ?None + ?Some")
Andreas@63243
   950
    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)
Andreas@63243
   951
  also have "?Some = \<integral>\<^sup>+ x. ?f x \<partial>count_space (range Some)"
Andreas@63243
   952
    by(simp add: nn_integral_count_space_indicator)
Andreas@63243
   953
  also have "count_space (range Some) = embed_measure (count_space UNIV) Some"
Andreas@63243
   954
    by(simp add: embed_measure_count_space)
Andreas@63243
   955
  also have "(\<integral>\<^sup>+ x. ?f x \<partial>\<dots>) = \<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV"
Andreas@63243
   956
    by(subst nn_integral_embed_measure)(simp_all add: measurable_embed_measure1)
Andreas@63243
   957
  also have "?None + \<dots> = 1" using prob
Andreas@63243
   958
    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)
Andreas@63243
   959
  finally show ?thesis .
Andreas@63243
   960
qed
Andreas@63243
   961
Andreas@63243
   962
lemma pmf_embed_spmf_None: "pmf embed_spmf None = 1 - enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>count_space UNIV)"
Andreas@63243
   963
unfolding embed_spmf_def
Andreas@63243
   964
apply(subst pmf_embed_pmf)
Andreas@63243
   965
  subgoal using prob by(simp add: field_simps enn2real_leI split: option.split)
Andreas@63243
   966
 apply(rule nn_integral_embed_spmf_eq_1)
Andreas@63243
   967
apply simp
Andreas@63243
   968
done
Andreas@63243
   969
Andreas@63243
   970
lemma spmf_embed_spmf [simp]: "spmf embed_spmf x = max 0 (f x)"
Andreas@63243
   971
unfolding embed_spmf_def
Andreas@63243
   972
apply(subst pmf_embed_pmf)
Andreas@63243
   973
  subgoal using prob by(simp add: field_simps enn2real_leI split: option.split)
Andreas@63243
   974
 apply(rule nn_integral_embed_spmf_eq_1)
Andreas@63243
   975
apply simp
Andreas@63243
   976
done
Andreas@63243
   977
Andreas@63243
   978
end
Andreas@63243
   979
Andreas@63243
   980
end
Andreas@63243
   981
Andreas@63243
   982
lemma embed_spmf_K_0[simp]: "embed_spmf (\<lambda>_. 0) = return_pmf None" (is "?lhs = ?rhs")
Andreas@63243
   983
by(rule spmf_eqI)(simp add: zero_ereal_def[symmetric])
Andreas@63243
   984
wenzelm@63308
   985
subsection \<open>Ordering on spmfs\<close>
wenzelm@63308
   986
wenzelm@63308
   987
text \<open>
Andreas@63243
   988
  @{const rel_pmf} does not preserve a ccpo structure. Counterexample by Saheb-Djahromi:
wenzelm@63308
   989
  Take prefix order over \<open>bool llist\<close> and
wenzelm@63308
   990
  the set \<open>range (\<lambda>n :: nat. uniform (llist_n n))\<close> where \<open>llist_n\<close> is the set
wenzelm@63308
   991
  of all \<open>llist\<close>s of length \<open>n\<close> and \<open>uniform\<close> returns a uniform distribution over
wenzelm@63308
   992
  the given set. The set forms a chain in \<open>ord_pmf lprefix\<close>, but it has not an upper bound.
Andreas@63243
   993
  Any upper bound may contain only infinite lists in its support because otherwise it is not greater
wenzelm@63308
   994
  than the \<open>n+1\<close>-st element in the chain where \<open>n\<close> is the length of the finite list.
Andreas@63243
   995
  Moreover its support must contain all infinite lists, because otherwise there is a finite list
Andreas@63243
   996
  all of whose finite extensions are not in the support - a contradiction to the upper bound property.
Andreas@63243
   997
  Hence, the support is uncountable, but pmf's only have countable support.
Andreas@63243
   998
Andreas@63243
   999
  However, if all chains in the ccpo are finite, then it should preserve the ccpo structure.
wenzelm@63308
  1000
\<close>
Andreas@63243
  1001
Andreas@63243
  1002
abbreviation ord_spmf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf \<Rightarrow> bool"
Andreas@63243
  1003
where "ord_spmf ord \<equiv> rel_pmf (ord_option ord)"
Andreas@63243
  1004
Andreas@63243
  1005
locale ord_spmf_syntax begin
Andreas@63243
  1006
notation ord_spmf (infix "\<sqsubseteq>\<index>" 60)
Andreas@63243
  1007
end
Andreas@63243
  1008
Andreas@63243
  1009
lemma ord_spmf_map_spmf1: "ord_spmf R (map_spmf f p) = ord_spmf (\<lambda>x. R (f x)) p"
Andreas@63243
  1010
by(simp add: pmf.rel_map[abs_def] ord_option_map1[abs_def])
Andreas@63243
  1011
Andreas@63243
  1012
lemma ord_spmf_map_spmf2: "ord_spmf R p (map_spmf f q) = ord_spmf (\<lambda>x y. R x (f y)) p q"
Andreas@63243
  1013
by(simp add: pmf.rel_map ord_option_map2)
Andreas@63243
  1014
Andreas@63243
  1015
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"
Andreas@63243
  1016
by(simp add: pmf.rel_map ord_option_map1[abs_def] ord_option_map2)
Andreas@63243
  1017
Andreas@63243
  1018
lemmas ord_spmf_map_spmf = ord_spmf_map_spmf1 ord_spmf_map_spmf2 ord_spmf_map_spmf12
Andreas@63243
  1019
Andreas@63243
  1020
context fixes ord :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (structure) begin
Andreas@63243
  1021
interpretation ord_spmf_syntax .
Andreas@63243
  1022
Andreas@63243
  1023
lemma ord_spmfI:
Andreas@63243
  1024
  "\<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>
Andreas@63243
  1025
  \<Longrightarrow> p \<sqsubseteq> q"
Andreas@63243
  1026
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"])
Andreas@63243
  1027
  (auto simp add: pmf.map_comp o_def in_set_spmf split: option.splits intro: pmf.map_cong)
Andreas@63243
  1028
Andreas@63243
  1029
lemma ord_spmf_None [simp]: "return_pmf None \<sqsubseteq> x"
Andreas@63243
  1030
by(rule rel_pmf.intros[where pq="map_pmf (Pair None) x"])(auto simp add: pmf.map_comp o_def)
Andreas@63243
  1031
Andreas@63243
  1032
lemma ord_spmf_reflI: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> ord x x) \<Longrightarrow> p \<sqsubseteq> p"
Andreas@63243
  1033
by(rule rel_pmf_reflI ord_option_reflI)+(auto simp add: in_set_spmf)
Andreas@63243
  1034
Andreas@63243
  1035
lemma rel_spmf_inf:
Andreas@63243
  1036
  assumes "p \<sqsubseteq> q"
Andreas@63243
  1037
  and "q \<sqsubseteq> p"
Andreas@63243
  1038
  and refl: "reflp ord"
Andreas@63243
  1039
  and trans: "transp ord"
Andreas@63243
  1040
  shows "rel_spmf (inf ord ord\<inverse>\<inverse>) p q"
Andreas@63243
  1041
proof -
Andreas@63243
  1042
  from \<open>p \<sqsubseteq> q\<close> \<open>q \<sqsubseteq> p\<close>
Andreas@63243
  1043
  have "rel_pmf (inf (ord_option ord) (ord_option ord)\<inverse>\<inverse>) p q"
Andreas@63243
  1044
    by(rule rel_pmf_inf)(blast intro: reflp_ord_option transp_ord_option refl trans)+
Andreas@63243
  1045
  also have "inf (ord_option ord) (ord_option ord)\<inverse>\<inverse> = rel_option (inf ord ord\<inverse>\<inverse>)"
Andreas@63243
  1046
    by(auto simp add: fun_eq_iff elim: ord_option.cases option.rel_cases)
Andreas@63243
  1047
  finally show ?thesis .
Andreas@63243
  1048
qed
Andreas@63243
  1049
Andreas@63243
  1050
end
Andreas@63243
  1051
Andreas@63243
  1052
lemma ord_spmf_return_spmf2: "ord_spmf R p (return_spmf y) \<longleftrightarrow> (\<forall>x\<in>set_spmf p. R x y)"
Andreas@63243
  1053
by(auto simp add: rel_pmf_return_pmf2 in_set_spmf ord_option.simps intro: ccontr)
Andreas@63243
  1054
Andreas@63243
  1055
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"
Andreas@63243
  1056
by(erule rel_pmf_mono)(erule ord_option_mono)
Andreas@63243
  1057
Andreas@63243
  1058
lemma ord_spmf_compp: "ord_spmf (A OO B) = ord_spmf A OO ord_spmf B"
Andreas@63243
  1059
by(simp add: ord_option_compp pmf.rel_compp)
Andreas@63243
  1060
Andreas@63243
  1061
lemma ord_spmf_bindI:
Andreas@63243
  1062
  assumes pq: "ord_spmf R p q"
Andreas@63243
  1063
  and fg: "\<And>x y. R x y \<Longrightarrow> ord_spmf P (f x) (g y)"
Andreas@63243
  1064
  shows "ord_spmf P (p \<bind> f) (q \<bind> g)"
Andreas@63243
  1065
unfolding bind_spmf_def using pq
Andreas@63243
  1066
by(rule rel_pmf_bindI)(auto split: option.split intro: fg)
Andreas@63243
  1067
Andreas@63243
  1068
lemma ord_spmf_bind_reflI:
Andreas@63243
  1069
  "(\<And>x. x \<in> set_spmf p \<Longrightarrow> ord_spmf R (f x) (g x))
Andreas@63243
  1070
  \<Longrightarrow> ord_spmf R (p \<bind> f) (p \<bind> g)"
Andreas@63243
  1071
by(rule ord_spmf_bindI[where R="\<lambda>x y. x = y \<and> x \<in> set_spmf p"])(auto intro: ord_spmf_reflI)
Andreas@63243
  1072
Andreas@63243
  1073
lemma ord_pmf_increaseI:
Andreas@63243
  1074
  assumes le: "\<And>x. spmf p x \<le> spmf q x"
Andreas@63243
  1075
  and refl: "\<And>x. x \<in> set_spmf p \<Longrightarrow> R x x"
Andreas@63243
  1076
  shows "ord_spmf R p q"
Andreas@63243
  1077
proof(rule rel_pmf.intros)
hoelzl@63333
  1078
  define pq where "pq = embed_pmf
Andreas@63243
  1079
    (\<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)
Andreas@63243
  1080
      | None \<Rightarrow> (case y of None \<Rightarrow> pmf q None | Some y' \<Rightarrow> spmf q y' - spmf p y'))"
Andreas@63243
  1081
     (is "_ = embed_pmf ?f")
Andreas@63243
  1082
  have nonneg: "\<And>xy. ?f xy \<ge> 0"
Andreas@63243
  1083
    by(clarsimp simp add: le field_simps split: option.split)
Andreas@63243
  1084
  have integral: "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) = 1" (is "nn_integral ?M _ = _")
Andreas@63243
  1085
  proof -
Andreas@63243
  1086
    have "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) =
hoelzl@63333
  1087
      \<integral>\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy +
hoelzl@63333
  1088
             ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy +
Andreas@63243
  1089
             ennreal (?f xy) * indicator (range (\<lambda>x. (Some x, Some x))) xy \<partial>?M"
Andreas@63243
  1090
      by(rule nn_integral_cong)(auto split: split_indicator option.splits if_split_asm)
Andreas@63243
  1091
    also have "\<dots> = (\<integral>\<^sup>+ xy. ?f xy * indicator {(None, None)} xy \<partial>?M) +
Andreas@63243
  1092
        (\<integral>\<^sup>+ xy. ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy \<partial>?M) +
Andreas@63243
  1093
        (\<integral>\<^sup>+ xy. ennreal (?f xy) * indicator (range (\<lambda>x. (Some x, Some x))) xy \<partial>?M)"
Andreas@63243
  1094
      (is "_ = ?None + ?Some2 + ?Some")
Andreas@63243
  1095
      by(subst nn_integral_add)(simp_all add: nn_integral_add AE_count_space le_diff_eq le split: option.split)
Andreas@63243
  1096
    also have "?None = pmf q None" by simp
Andreas@63243
  1097
    also have "?Some2 = \<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV"
Andreas@63243
  1098
      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)
Andreas@63243
  1099
    also have "\<dots> = (\<integral>\<^sup>+ x. spmf q x \<partial>count_space UNIV) - (\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV)"
Andreas@63243
  1100
      (is "_ = ?Some2' - ?Some2''")
Andreas@63243
  1101
      by(subst nn_integral_diff)(simp_all add: le nn_integral_spmf_neq_top)
Andreas@63243
  1102
    also have "?Some = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
Andreas@63243
  1103
      by(simp add: nn_integral_count_space_indicator[symmetric] embed_measure_count_space[symmetric] inj_on_def nn_integral_embed_measure measurable_embed_measure1)
Andreas@63243
  1104
    also have "pmf q None + (?Some2' - ?Some2'') + \<dots> = pmf q None + ?Some2'"
Andreas@63243
  1105
      by(auto simp add: diff_add_self_ennreal le intro!: nn_integral_mono)
Andreas@63243
  1106
    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"
Andreas@63243
  1107
      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)
Andreas@63243
  1108
    also have "\<dots> = \<integral>\<^sup>+ x. pmf q x \<partial>count_space UNIV"
Andreas@63243
  1109
      by(rule nn_integral_cong)(auto split: split_indicator)
Andreas@63243
  1110
    also have "\<dots> = 1" by(simp add: nn_integral_pmf)
Andreas@63243
  1111
    finally show ?thesis .
Andreas@63243
  1112
  qed
Andreas@63243
  1113
  note f = nonneg integral
Andreas@63243
  1114
Andreas@63243
  1115
  { fix x y
Andreas@63243
  1116
    assume "(x, y) \<in> set_pmf pq"
Andreas@63243
  1117
    hence "?f (x, y) \<noteq> 0" unfolding pq_def by(simp add: set_embed_pmf[OF f])
Andreas@63243
  1118
    then show "ord_option R x y"
Andreas@63243
  1119
      by(simp add: spmf_eq_0_set_spmf refl split: option.split_asm if_split_asm) }
Andreas@63243
  1120
Andreas@63243
  1121
  have weight_le: "weight_spmf p \<le> weight_spmf q"
Andreas@63243
  1122
    by(subst ennreal_le_iff[symmetric])(auto simp add: weight_spmf_eq_nn_integral_spmf intro!: nn_integral_mono le)
Andreas@63243
  1123
Andreas@63243
  1124
  show "map_pmf fst pq = p"
Andreas@63243
  1125
  proof(rule pmf_eqI)
Andreas@63243
  1126
    fix i
Andreas@63243
  1127
    have "ennreal (pmf (map_pmf fst pq) i) = (\<integral>\<^sup>+ y. pmf pq (i, y) \<partial>count_space UNIV)"
Andreas@63243
  1128
      unfolding pq_def ennreal_pmf_map
Andreas@63243
  1129
      apply(simp add: embed_pmf.rep_eq[OF f] o_def emeasure_density nn_integral_count_space_indicator[symmetric])
Andreas@63243
  1130
      apply(subst pmf_embed_pmf[OF f])
Andreas@63243
  1131
      apply(rule nn_integral_bij_count_space[symmetric])
Andreas@63243
  1132
      apply(auto simp add: bij_betw_def inj_on_def)
Andreas@63243
  1133
      done
Andreas@63243
  1134
    also have "\<dots> = pmf p i"
Andreas@63243
  1135
    proof(cases i)
Andreas@63243
  1136
      case (Some x)
Andreas@63243
  1137
      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"
Andreas@63243
  1138
        by(rule nn_integral_cong)(simp add: pq_def pmf_embed_pmf[OF f] split: option.split)
Andreas@63243
  1139
      then show ?thesis using Some by simp
Andreas@63243
  1140
    next
Andreas@63243
  1141
      case None
hoelzl@63333
  1142
      have "(\<integral>\<^sup>+ y. pmf pq (None, y) \<partial>count_space UNIV) =
hoelzl@63333
  1143
            (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y +
Andreas@63243
  1144
                   ennreal (pmf pq (None, None)) * indicator {None} y \<partial>count_space UNIV)"
Andreas@63243
  1145
        by(rule nn_integral_cong)(auto split: split_indicator)
Andreas@63243
  1146
      also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) \<partial>count_space (range Some)) + pmf pq (None, None)"
Andreas@63243
  1147
        by(subst nn_integral_add)(simp_all add: nn_integral_count_space_indicator)
Andreas@63243
  1148
      also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (spmf q y) - ennreal (spmf p y) \<partial>count_space UNIV) + pmf q None"
Andreas@63243
  1149
        by(simp add: pq_def pmf_embed_pmf[OF f] embed_measure_count_space[symmetric] nn_integral_embed_measure measurable_embed_measure1 ennreal_minus)
Andreas@63243
  1150
      also have "(\<integral>\<^sup>+ y. ennreal (spmf q y) - ennreal (spmf p y) \<partial>count_space UNIV) =
Andreas@63243
  1151
                 (\<integral>\<^sup>+ y. spmf q y \<partial>count_space UNIV) - (\<integral>\<^sup>+ y. spmf p y \<partial>count_space UNIV)"
Andreas@63243
  1152
        by(subst nn_integral_diff)(simp_all add: AE_count_space le nn_integral_spmf_neq_top split: split_indicator)
Andreas@63243
  1153
      also have "\<dots> = pmf p None - pmf q None"
Andreas@63243
  1154
        by(simp add: pmf_None_eq_weight_spmf weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus)
Andreas@63243
  1155
      also have "\<dots> = ennreal (pmf p None) - ennreal (pmf q None)" by(simp add: ennreal_minus)
Andreas@63243
  1156
      finally show ?thesis using None weight_le
Andreas@63243
  1157
        by(auto simp add: diff_add_self_ennreal pmf_None_eq_weight_spmf intro: ennreal_leI)
Andreas@63243
  1158
    qed
Andreas@63243
  1159
    finally show "pmf (map_pmf fst pq) i = pmf p i" by simp
Andreas@63243
  1160
  qed
Andreas@63243
  1161
Andreas@63243
  1162
  show "map_pmf snd pq = q"
Andreas@63243
  1163
  proof(rule pmf_eqI)
Andreas@63243
  1164
    fix i
Andreas@63243
  1165
    have "ennreal (pmf (map_pmf snd pq) i) = (\<integral>\<^sup>+ x. pmf pq (x, i) \<partial>count_space UNIV)"
Andreas@63243
  1166
      unfolding pq_def ennreal_pmf_map
Andreas@63243
  1167
      apply(simp add: embed_pmf.rep_eq[OF f] o_def emeasure_density nn_integral_count_space_indicator[symmetric])
Andreas@63243
  1168
      apply(subst pmf_embed_pmf[OF f])
Andreas@63243
  1169
      apply(rule nn_integral_bij_count_space[symmetric])
Andreas@63243
  1170
      apply(auto simp add: bij_betw_def inj_on_def)
Andreas@63243
  1171
      done
Andreas@63243
  1172
    also have "\<dots> = ennreal (pmf q i)"
Andreas@63243
  1173
    proof(cases i)
Andreas@63243
  1174
      case None
Andreas@63243
  1175
      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"
Andreas@63243
  1176
        by(rule nn_integral_cong)(simp add: pq_def pmf_embed_pmf[OF f] split: option.split)
Andreas@63243
  1177
      then show ?thesis using None by simp
Andreas@63243
  1178
    next
Andreas@63243
  1179
      case (Some y)
hoelzl@63333
  1180
      have "(\<integral>\<^sup>+ x. pmf pq (x, Some y) \<partial>count_space UNIV) =
hoelzl@63333
  1181
        (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x +
Andreas@63243
  1182
               ennreal (pmf pq (None, Some y)) * indicator {None} x \<partial>count_space UNIV)"
Andreas@63243
  1183
        by(rule nn_integral_cong)(auto split: split_indicator)
Andreas@63243
  1184
      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)"
Andreas@63243
  1185
        by(subst nn_integral_add)(simp_all)
Andreas@63243
  1186
      also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (spmf p y) * indicator {Some y} x \<partial>count_space UNIV) + (spmf q y - spmf p y)"
Andreas@63243
  1187
        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)
Andreas@63243
  1188
      also have "\<dots> = spmf q y" by(simp add: ennreal_minus[symmetric] le)
Andreas@63243
  1189
      finally show ?thesis using Some by simp
Andreas@63243
  1190
    qed
Andreas@63243
  1191
    finally show "pmf (map_pmf snd pq) i = pmf q i" by simp
Andreas@63243
  1192
  qed
Andreas@63243
  1193
qed
Andreas@63243
  1194
Andreas@63243
  1195
lemma ord_spmf_eq_leD:
Andreas@63243
  1196
  assumes "ord_spmf op = p q"
Andreas@63243
  1197
  shows "spmf p x \<le> spmf q x"
Andreas@63243
  1198
proof(cases "x \<in> set_spmf p")
Andreas@63243
  1199
  case False
Andreas@63243
  1200
  thus ?thesis by(simp add: in_set_spmf_iff_spmf)
Andreas@63243
  1201
next
Andreas@63243
  1202
  case True
Andreas@63243
  1203
  from assms obtain pq
Andreas@63243
  1204
    where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> ord_option op = x y"
Andreas@63243
  1205
    and p: "p = map_pmf fst pq"
Andreas@63243
  1206
    and q: "q = map_pmf snd pq" by cases auto
Andreas@63243
  1207
  have "ennreal (spmf p x) = integral\<^sup>N pq (indicator (fst -` {Some x}))"
Andreas@63243
  1208
    using p by(simp add: ennreal_pmf_map)
Andreas@63243
  1209
  also have "\<dots> = integral\<^sup>N pq (indicator {(Some x, Some x)})"
Andreas@63243
  1210
    by(rule nn_integral_cong_AE)(auto simp add: AE_measure_pmf_iff split: split_indicator dest: pq)
Andreas@63243
  1211
  also have "\<dots> \<le> integral\<^sup>N pq (indicator (snd -` {Some x}))"
Andreas@63243
  1212
    by(rule nn_integral_mono) simp
Andreas@63243
  1213
  also have "\<dots> = ennreal (spmf q x)" using q by(simp add: ennreal_pmf_map)
Andreas@63243
  1214
  finally show ?thesis by simp
Andreas@63243
  1215
qed
Andreas@63243
  1216
Andreas@63243
  1217
lemma ord_spmf_eqD_set_spmf: "ord_spmf op = p q \<Longrightarrow> set_spmf p \<subseteq> set_spmf q"
Andreas@63243
  1218
by(rule subsetI)(drule_tac x=x in ord_spmf_eq_leD, auto simp add: in_set_spmf_iff_spmf)
Andreas@63243
  1219
Andreas@63243
  1220
lemma ord_spmf_eqD_emeasure:
Andreas@63243
  1221
  "ord_spmf op = p q \<Longrightarrow> emeasure (measure_spmf p) A \<le> emeasure (measure_spmf q) A"
Andreas@63243
  1222
by(auto intro!: nn_integral_mono split: split_indicator dest: ord_spmf_eq_leD simp add: nn_integral_measure_spmf nn_integral_indicator[symmetric])
Andreas@63243
  1223
Andreas@63243
  1224
lemma ord_spmf_eqD_measure_spmf: "ord_spmf op = p q \<Longrightarrow> measure_spmf p \<le> measure_spmf q"
hoelzl@63333
  1225
  by (subst le_measure) (auto simp: ord_spmf_eqD_emeasure)
Andreas@63243
  1226
wenzelm@63308
  1227
subsection \<open>CCPO structure for the flat ccpo @{term "ord_option op ="}\<close>
Andreas@63243
  1228
Andreas@63243
  1229
context fixes Y :: "'a spmf set" begin
Andreas@63243
  1230
Andreas@63243
  1231
definition lub_spmf :: "'a spmf"
Andreas@63243
  1232
where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
hoelzl@63333
  1233
  \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
Andreas@63243
  1234
Andreas@63243
  1235
lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
Andreas@63243
  1236
by(simp add: SPMF.lub_spmf_def bot_ereal_def)
Andreas@63243
  1237
Andreas@63243
  1238
context assumes chain: "Complete_Partial_Order.chain (ord_spmf op =) Y" begin
Andreas@63243
  1239
Andreas@63243
  1240
lemma chain_ord_spmf_eqD: "Complete_Partial_Order.chain (op \<le>) ((\<lambda>p x. ennreal (spmf p x)) ` Y)"
Andreas@63243
  1241
  (is "Complete_Partial_Order.chain _ (?f ` _)")
Andreas@63243
  1242
proof(rule chainI)
Andreas@63243
  1243
  fix f g
Andreas@63243
  1244
  assume "f \<in> ?f ` Y" "g \<in> ?f ` Y"
Andreas@63243
  1245
  then obtain p q where f: "f = ?f p" "p \<in> Y" and g: "g = ?f q" "q \<in> Y" by blast
Andreas@63243
  1246
  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)
Andreas@63243
  1247
  thus "f \<le> g \<or> g \<le> f"
Andreas@63243
  1248
  proof
Andreas@63243
  1249
    assume "ord_spmf op = p q"
Andreas@63243
  1250
    hence "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
Andreas@63243
  1251
    hence "f \<le> g" unfolding f g by(auto intro: le_funI)
Andreas@63243
  1252
    thus ?thesis ..
Andreas@63243
  1253
  next
Andreas@63243
  1254
    assume "ord_spmf op = q p"
Andreas@63243
  1255
    hence "\<And>x. spmf q x \<le> spmf p x" by(rule ord_spmf_eq_leD)
Andreas@63243
  1256
    hence "g \<le> f" unfolding f g by(auto intro: le_funI)
Andreas@63243
  1257
    thus ?thesis ..
Andreas@63243
  1258
  qed
Andreas@63243
  1259
qed
Andreas@63243
  1260
Andreas@63243
  1261
lemma ord_spmf_eq_pmf_None_eq:
Andreas@63243
  1262
  assumes le: "ord_spmf op = p q"
Andreas@63243
  1263
  and None: "pmf p None = pmf q None"
Andreas@63243
  1264
  shows "p = q"
Andreas@63243
  1265
proof(rule spmf_eqI)
Andreas@63243
  1266
  fix i
Andreas@63243
  1267
  from le have le': "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
hoelzl@63333
  1268
  have "(\<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV) =
Andreas@63243
  1269
     (\<integral>\<^sup>+ x. spmf q x \<partial>count_space UNIV) - (\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV)"
Andreas@63243
  1270
    by(subst nn_integral_diff)(simp_all add: AE_count_space le' nn_integral_spmf_neq_top)
Andreas@63243
  1271
  also have "\<dots> = (1 - pmf q None) - (1 - pmf p None)" unfolding pmf_None_eq_weight_spmf
Andreas@63243
  1272
    by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus)
Andreas@63243
  1273
  also have "\<dots> = 0" using None by simp
hoelzl@63333
  1274
  finally have "\<And>x. spmf q x \<le> spmf p x"
Andreas@63243
  1275
    by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff)
Andreas@63243
  1276
  with le' show "spmf p i = spmf q i" by(rule antisym)
Andreas@63243
  1277
qed
Andreas@63243
  1278
hoelzl@63333
  1279
lemma ord_spmf_eqD_pmf_None:
Andreas@63243
  1280
  assumes "ord_spmf op = x y"
Andreas@63243
  1281
  shows "pmf x None \<ge> pmf y None"
Andreas@63243
  1282
using assms
Andreas@63243
  1283
apply cases
Andreas@63243
  1284
apply(clarsimp simp only: ennreal_le_iff[symmetric, OF pmf_nonneg] ennreal_pmf_map)
Andreas@63243
  1285
apply(fastforce simp add: AE_measure_pmf_iff intro!: nn_integral_mono_AE)
Andreas@63243
  1286
done
Andreas@63243
  1287
Andreas@63243
  1288
text \<open>
Andreas@63243
  1289
  Chains on @{typ "'a spmf"} maintain countable support.
Andreas@63243
  1290
  Thanks to Johannes Hölzl for the proof idea.
Andreas@63243
  1291
\<close>
hoelzl@63333
  1292
lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)"
Andreas@63243
  1293
proof(cases "Y = {}")
Andreas@63243
  1294
  case Y: False
Andreas@63243
  1295
  show ?thesis
Andreas@63243
  1296
  proof(cases "\<exists>x\<in>Y. \<forall>y\<in>Y. ord_spmf op = y x")
Andreas@63243
  1297
    case True
Andreas@63243
  1298
    then obtain x where x: "x \<in> Y" and upper: "\<And>y. y \<in> Y \<Longrightarrow> ord_spmf op = y x" by blast
Andreas@63243
  1299
    hence "(\<Union>x\<in>Y. set_spmf x) \<subseteq> set_spmf x" by(auto dest: ord_spmf_eqD_set_spmf)
Andreas@63243
  1300
    thus ?thesis by(rule countable_subset) simp
Andreas@63243
  1301
  next
Andreas@63243
  1302
    case False
Andreas@63243
  1303
    define N :: "'a option pmf \<Rightarrow> real" where "N p = pmf p None" for p
hoelzl@63333
  1304
Andreas@63243
  1305
    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
Andreas@63243
  1306
      using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x]
Andreas@63243
  1307
      by (auto simp: N_def)
Andreas@63243
  1308
    have N_eq_imp_eq: "\<lbrakk> x \<in> Y; y \<in> Y; N y = N x \<rbrakk> \<Longrightarrow> x = y" for x y
Andreas@63243
  1309
      using chainD[OF chain, of x y] by(auto simp add: N_def dest: ord_spmf_eq_pmf_None_eq)
hoelzl@63333
  1310
Andreas@63243
  1311
    have NC: "N ` Y \<noteq> {}" "bdd_below (N ` Y)"
Andreas@63243
  1312
      using \<open>Y \<noteq> {}\<close> by(auto intro!: bdd_belowI[of _ 0] simp: N_def)
Andreas@63243
  1313
    have NC_less: "Inf (N ` Y) < N x" if "x \<in> Y" for x unfolding cInf_less_iff[OF NC]
Andreas@63243
  1314
    proof(rule ccontr)
Andreas@63243
  1315
      assume **: "\<not> (\<exists>y\<in>N ` Y. y < N x)"
Andreas@63243
  1316
      { fix y
Andreas@63243
  1317
        assume "y \<in> Y"
Andreas@63243
  1318
        with ** consider "N x < N y" | "N x = N y" by(auto simp add: not_less le_less)
Andreas@63243
  1319
        hence "ord_spmf op = y x" using \<open>y \<in> Y\<close> \<open>x \<in> Y\<close>
Andreas@63243
  1320
          by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) }
Andreas@63243
  1321
      with False \<open>x \<in> Y\<close> show False by blast
Andreas@63243
  1322
    qed
hoelzl@63333
  1323
Andreas@63243
  1324
    from NC have "Inf (N ` Y) \<in> closure (N ` Y)" by (intro closure_contains_Inf)
Andreas@63243
  1325
    then obtain X' where "\<And>n. X' n \<in> N ` Y" and X': "X' \<longlonglongrightarrow> Inf (N ` Y)"
Andreas@63243
  1326
      unfolding closure_sequential by auto
Andreas@63243
  1327
    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
hoelzl@63333
  1328
Andreas@63243
  1329
    with X' have seq: "(\<lambda>n. N (X n)) \<longlonglongrightarrow> Inf (N ` Y)" by simp
Andreas@63243
  1330
    have "(\<Union>x \<in> Y. set_spmf x) \<subseteq> (\<Union>n. set_spmf (X n))"
Andreas@63243
  1331
    proof(rule UN_least)
Andreas@63243
  1332
      fix x
Andreas@63243
  1333
      assume "x \<in> Y"
Andreas@63243
  1334
      from order_tendstoD(2)[OF seq NC_less[OF \<open>x \<in> Y\<close>]]
Andreas@63243
  1335
      obtain i where "N (X i) < N x" by (auto simp: eventually_sequentially)
Andreas@63243
  1336
      thus "set_spmf x \<subseteq> (\<Union>n. set_spmf (X n))" using X \<open>x \<in> Y\<close>
Andreas@63243
  1337
        by(blast dest: N_less_imp_le_spmf ord_spmf_eqD_set_spmf)
Andreas@63243
  1338
    qed
Andreas@63243
  1339
    thus ?thesis by(rule countable_subset) simp
Andreas@63243
  1340
  qed
Andreas@63243
  1341
qed simp
Andreas@63243
  1342
Andreas@63243
  1343
lemma lub_spmf_subprob: "(\<integral>\<^sup>+ x. (SUP p : Y. ennreal (spmf p x)) \<partial>count_space UNIV) \<le> 1"
Andreas@63243
  1344
proof(cases "Y = {}")
Andreas@63243
  1345
  case True
Andreas@63243
  1346
  thus ?thesis by(simp add: bot_ennreal)
Andreas@63243
  1347
next
Andreas@63243
  1348
  case False
Andreas@63243
  1349
  let ?B = "\<Union>p\<in>Y. set_spmf p"
Andreas@63243
  1350
  have countable: "countable ?B" by(rule spmf_chain_countable)
Andreas@63243
  1351
hoelzl@63333
  1352
  have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
Andreas@63243
  1353
        (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
Andreas@63243
  1354
    by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
Andreas@63243
  1355
  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space ?B)"
Andreas@63243
  1356
    unfolding ennreal_indicator[symmetric] using False
Andreas@63243
  1357
    by(subst SUP_mult_right_ennreal[symmetric])(simp add: ennreal_indicator nn_integral_count_space_indicator)
Andreas@63243
  1358
  also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B)" using False _ countable
Andreas@63243
  1359
    by(rule nn_integral_monotone_convergence_SUP_countable)(rule chain_ord_spmf_eqD)
Andreas@63243
  1360
  also have "\<dots> \<le> 1"
Andreas@63243
  1361
  proof(rule SUP_least)
Andreas@63243
  1362
    fix p
Andreas@63243
  1363
    assume "p \<in> Y"
Andreas@63243
  1364
    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"
Andreas@63243
  1365
      by(simp add: nn_integral_count_space_indicator)
Andreas@63243
  1366
    also have "\<dots> = \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
Andreas@63243
  1367
      by(rule nn_integral_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf \<open>p \<in> Y\<close>)
Andreas@63243
  1368
    also have "\<dots> \<le> 1"
Andreas@63243
  1369
      by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] weight_spmf_le_1)
Andreas@63243
  1370
    finally show "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B) \<le> 1" .
Andreas@63243
  1371
  qed
Andreas@63243
  1372
  finally show ?thesis .
Andreas@63243
  1373
qed
Andreas@63243
  1374
Andreas@63243
  1375
lemma spmf_lub_spmf:
Andreas@63243
  1376
  assumes "Y \<noteq> {}"
Andreas@63243
  1377
  shows "spmf lub_spmf x = (SUP p : Y. spmf p x)"
Andreas@63243
  1378
proof -
Andreas@63243
  1379
  from assms obtain p where "p \<in> Y" by auto
Andreas@63243
  1380
  have "spmf lub_spmf x = max 0 (enn2real (SUP p:Y. ennreal (spmf p x)))" unfolding lub_spmf_def
Andreas@63243
  1381
    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)
Andreas@63243
  1382
  also have "\<dots> = enn2real (SUP p:Y. ennreal (spmf p x))"
Andreas@63243
  1383
    by(rule max_absorb2)(simp)
Andreas@63243
  1384
  also have "\<dots> = enn2real (ennreal (SUP p : Y. spmf p x))" using assms
Andreas@63243
  1385
    by(subst ennreal_SUP[symmetric])(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
Andreas@63243
  1386
  also have "0 \<le> (\<Squnion>p\<in>Y. spmf p x)" using assms
Andreas@63243
  1387
    by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] simp add: pmf_le_1)
Andreas@63243
  1388
  then have "enn2real (ennreal (SUP p : Y. spmf p x)) = (SUP p : Y. spmf p x)"
Andreas@63243
  1389
    by(rule enn2real_ennreal)
Andreas@63243
  1390
  finally show ?thesis .
Andreas@63243
  1391
qed
Andreas@63243
  1392
Andreas@63243
  1393
lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
Andreas@63243
  1394
unfolding spmf_lub_spmf by(subst ennreal_SUP)(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
Andreas@63243
  1395
Andreas@63243
  1396
lemma lub_spmf_upper:
Andreas@63243
  1397
  assumes p: "p \<in> Y"
Andreas@63243
  1398
  shows "ord_spmf op = p lub_spmf"
Andreas@63243
  1399
proof(rule ord_pmf_increaseI)
Andreas@63243
  1400
  fix x
Andreas@63243
  1401
  from p have [simp]: "Y \<noteq> {}" by auto
Andreas@63243
  1402
  from p have "ennreal (spmf p x) \<le> (SUP p:Y. ennreal (spmf p x))" by(rule SUP_upper)
Andreas@63243
  1403
  also have "\<dots> = ennreal (spmf lub_spmf x)" using p
Andreas@63243
  1404
    by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' simp del: SUP_eq_top_iff Sup_eq_top_iff)
Andreas@63243
  1405
  finally show "spmf p x \<le> spmf lub_spmf x" by simp
Andreas@63243
  1406
qed simp
Andreas@63243
  1407
Andreas@63243
  1408
lemma lub_spmf_least:
Andreas@63243
  1409
  assumes z: "\<And>x. x \<in> Y \<Longrightarrow> ord_spmf op = x z"
Andreas@63243
  1410
  shows "ord_spmf op = lub_spmf z"
Andreas@63243
  1411
proof(cases "Y = {}")
Andreas@63243
  1412
  case nonempty: False
Andreas@63243
  1413
  show ?thesis
Andreas@63243
  1414
  proof(rule ord_pmf_increaseI)
Andreas@63243
  1415
    fix x
Andreas@63243
  1416
    from nonempty obtain p where p: "p \<in> Y" by auto
Andreas@63243
  1417
    have "ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
Andreas@63243
  1418
      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)
Andreas@63243
  1419
    also have "\<dots> \<le> ennreal (spmf z x)" by(rule SUP_least)(simp add: ord_spmf_eq_leD z)
Andreas@63243
  1420
    finally show "spmf lub_spmf x \<le> spmf z x" by simp
Andreas@63243
  1421
  qed simp
Andreas@63243
  1422
qed simp
Andreas@63243
  1423
Andreas@63243
  1424
lemma set_lub_spmf: "set_spmf lub_spmf = (\<Union>p\<in>Y. set_spmf p)" (is "?lhs = ?rhs")
Andreas@63243
  1425
proof(cases "Y = {}")
Andreas@63243
  1426
  case [simp]: False
Andreas@63243
  1427
  show ?thesis
Andreas@63243
  1428
  proof(rule set_eqI)
Andreas@63243
  1429
    fix x
Andreas@63243
  1430
    have "x \<in> ?lhs \<longleftrightarrow> ennreal (spmf lub_spmf x) > 0"
Andreas@63243
  1431
      by(simp_all add: in_set_spmf_iff_spmf less_le)
Andreas@63243
  1432
    also have "\<dots> \<longleftrightarrow> (\<exists>p\<in>Y. ennreal (spmf p x) > 0)"
Andreas@63243
  1433
      by(simp add: ennreal_spmf_lub_spmf less_SUP_iff)
Andreas@63243
  1434
    also have "\<dots> \<longleftrightarrow> x \<in> ?rhs"
Andreas@63243
  1435
      by(auto simp add: in_set_spmf_iff_spmf less_le)
Andreas@63243
  1436
    finally show "x \<in> ?lhs \<longleftrightarrow> x \<in> ?rhs" .
Andreas@63243
  1437
  qed
Andreas@63243
  1438
qed simp
Andreas@63243
  1439
Andreas@63243
  1440
lemma emeasure_lub_spmf:
Andreas@63243
  1441
  assumes Y: "Y \<noteq> {}"
Andreas@63243
  1442
  shows "emeasure (measure_spmf lub_spmf) A = (SUP y:Y. emeasure (measure_spmf y) A)"
Andreas@63243
  1443
  (is "?lhs = ?rhs")
Andreas@63243
  1444
proof -
Andreas@63243
  1445
  let ?M = "count_space (set_spmf lub_spmf)"
Andreas@63243
  1446
  have "?lhs = \<integral>\<^sup>+ x. ennreal (spmf lub_spmf x) * indicator A x \<partial>?M"
Andreas@63243
  1447
    by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf')
Andreas@63243
  1448
  also have "\<dots> = \<integral>\<^sup>+ x. (SUP y:Y. ennreal (spmf y x) * indicator A x) \<partial>?M"
Andreas@63243
  1449
    unfolding ennreal_indicator[symmetric]
Andreas@63243
  1450
    by(simp add: spmf_lub_spmf assms ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal)
Andreas@63243
  1451
  also from assms have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
Andreas@63243
  1452
  proof(rule nn_integral_monotone_convergence_SUP_countable)
Andreas@63243
  1453
    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"
Andreas@63243
  1454
      by(simp add: image_image)
Andreas@63243
  1455
    also have "Complete_Partial_Order.chain op \<le> \<dots>" using chain_ord_spmf_eqD
Andreas@63243
  1456
      by(rule chain_imageI)(auto simp add: le_fun_def split: split_indicator)
Andreas@63243
  1457
    finally show "Complete_Partial_Order.chain op \<le> ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
Andreas@63243
  1458
  qed simp
Andreas@63243
  1459
  also have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
Andreas@63243
  1460
    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)
Andreas@63243
  1461
  also have "\<dots> = ?rhs"
Andreas@63243
  1462
    by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf)
Andreas@63243
  1463
  finally show ?thesis .
Andreas@63243
  1464
qed
Andreas@63243
  1465
Andreas@63243
  1466
lemma measure_lub_spmf:
Andreas@63243
  1467
  assumes Y: "Y \<noteq> {}"
Andreas@63243
  1468
  shows "measure (measure_spmf lub_spmf) A = (SUP y:Y. measure (measure_spmf y) A)" (is "?lhs = ?rhs")
Andreas@63243
  1469
proof -
Andreas@63243
  1470
  have "ennreal ?lhs = ennreal ?rhs"
Andreas@63243
  1471
    using emeasure_lub_spmf[OF assms] SUP_emeasure_spmf_neq_top[of A Y] Y
Andreas@63243
  1472
    unfolding measure_spmf.emeasure_eq_measure by(subst ennreal_SUP)
Andreas@63243
  1473
  moreover have "0 \<le> ?rhs" using Y
Andreas@63243
  1474
    by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] measure_spmf.subprob_measure_le_1)
Andreas@63243
  1475
  ultimately show ?thesis by(simp)
Andreas@63243
  1476
qed
Andreas@63243
  1477
Andreas@63243
  1478
lemma weight_lub_spmf:
Andreas@63243
  1479
  assumes Y: "Y \<noteq> {}"
Andreas@63243
  1480
  shows "weight_spmf lub_spmf = (SUP y:Y. weight_spmf y)"
Andreas@63243
  1481
unfolding weight_spmf_def by(rule measure_lub_spmf) fact
Andreas@63243
  1482
Andreas@63243
  1483
lemma measure_spmf_lub_spmf:
Andreas@63243
  1484
  assumes Y: "Y \<noteq> {}"
Andreas@63243
  1485
  shows "measure_spmf lub_spmf = (SUP p:Y. measure_spmf p)" (is "?lhs = ?rhs")
Andreas@63243
  1486
proof(rule measure_eqI)
Andreas@63243
  1487
  from assms obtain p where p: "p \<in> Y" by auto
Andreas@63243
  1488
  from chain have chain': "Complete_Partial_Order.chain op \<le> (measure_spmf ` Y)"
Andreas@63243
  1489
    by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf)
hoelzl@63333
  1490
  show "sets ?lhs = sets ?rhs"
hoelzl@63333
  1491
    using Y by (subst sets_SUP) auto
hoelzl@63333
  1492
  show "emeasure ?lhs A = emeasure ?rhs A" for A
hoelzl@63333
  1493
    using chain' Y p by (subst emeasure_SUP_chain) (auto simp:  emeasure_lub_spmf)
Andreas@63243
  1494
qed
Andreas@63243
  1495
Andreas@63243
  1496
end
Andreas@63243
  1497
Andreas@63243
  1498
end
Andreas@63243
  1499
Andreas@63243
  1500
lemma partial_function_definitions_spmf: "partial_function_definitions (ord_spmf op =) lub_spmf"
Andreas@63243
  1501
  (is "partial_function_definitions ?R _")
Andreas@63243
  1502
proof
Andreas@63243
  1503
  fix x show "?R x x" by(simp add: ord_spmf_reflI)
Andreas@63243
  1504
next
Andreas@63243
  1505
  fix x y z
Andreas@63243
  1506
  assume "?R x y" "?R y z"
Andreas@63243
  1507
  with transp_ord_option[OF transp_equality] show "?R x z" by(rule transp_rel_pmf[THEN transpD])
Andreas@63243
  1508
next
Andreas@63243
  1509
  fix x y
Andreas@63243
  1510
  assume "?R x y" "?R y x"
Andreas@63243
  1511
  thus "x = y"
Andreas@63243
  1512
    by(rule rel_pmf_antisym)(simp_all add: reflp_ord_option transp_ord_option antisymP_ord_option)
Andreas@63243
  1513
next
Andreas@63243
  1514
  fix Y x
Andreas@63243
  1515
  assume "Complete_Partial_Order.chain ?R Y" "x \<in> Y"
Andreas@63243
  1516
  then show "?R x (lub_spmf Y)"
Andreas@63243
  1517
    by(rule lub_spmf_upper)
Andreas@63243
  1518
next
Andreas@63243
  1519
  fix Y z
Andreas@63243
  1520
  assume "Complete_Partial_Order.chain ?R Y" "\<And>x. x \<in> Y \<Longrightarrow> ?R x z"
Andreas@63243
  1521
  then show "?R (lub_spmf Y) z"
Andreas@63243
  1522
    by(cases "Y = {}")(simp_all add: lub_spmf_least)
Andreas@63243
  1523
qed
Andreas@63243
  1524
Andreas@63243
  1525
lemma ccpo_spmf: "class.ccpo lub_spmf (ord_spmf op =) (mk_less (ord_spmf op =))"
Andreas@63243
  1526
by(rule ccpo partial_function_definitions_spmf)+
Andreas@63243
  1527
Andreas@63243
  1528
interpretation spmf: partial_function_definitions "ord_spmf op =" "lub_spmf"
Andreas@63243
  1529
  rewrites "lub_spmf {} \<equiv> return_pmf None"
Andreas@63243
  1530
by(rule partial_function_definitions_spmf) simp
Andreas@63243
  1531
wenzelm@63308
  1532
declaration \<open>Partial_Function.init "spmf" @{term spmf.fixp_fun}
Andreas@63243
  1533
  @{term spmf.mono_body} @{thm spmf.fixp_rule_uc} @{thm spmf.fixp_induct_uc}
wenzelm@63308
  1534
  NONE\<close>
Andreas@63243
  1535
Andreas@63243
  1536
declare spmf.leq_refl[simp]
Andreas@63243
  1537
declare admissible_leI[OF ccpo_spmf, cont_intro]
Andreas@63243
  1538
Andreas@63243
  1539
abbreviation "mono_spmf \<equiv> monotone (fun_ord (ord_spmf op =)) (ord_spmf op =)"
Andreas@63243
  1540
Andreas@63243
  1541
lemma lub_spmf_const [simp]: "lub_spmf {p} = p"
Andreas@63243
  1542
by(rule spmf_eqI)(simp add: spmf_lub_spmf[OF ccpo.chain_singleton[OF ccpo_spmf]])
Andreas@63243
  1543
Andreas@63243
  1544
lemma bind_spmf_mono':
Andreas@63243
  1545
  assumes fg: "ord_spmf op = f g"
Andreas@63243
  1546
  and hk: "\<And>x :: 'a. ord_spmf op = (h x) (k x)"
Andreas@63243
  1547
  shows "ord_spmf op = (f \<bind> h) (g \<bind> k)"
Andreas@63243
  1548
unfolding bind_spmf_def using assms(1)
Andreas@63243
  1549
by(rule rel_pmf_bindI)(auto split: option.split simp add: hk)
Andreas@63243
  1550
Andreas@63243
  1551
lemma bind_spmf_mono [partial_function_mono]:
Andreas@63243
  1552
  assumes mf: "mono_spmf B" and mg: "\<And>y. mono_spmf (\<lambda>f. C y f)"
Andreas@63243
  1553
  shows "mono_spmf (\<lambda>f. bind_spmf (B f) (\<lambda>y. C y f))"
Andreas@63243
  1554
proof (rule monotoneI)
Andreas@63243
  1555
  fix f g :: "'a \<Rightarrow> 'b spmf"
Andreas@63243
  1556
  assume fg: "fun_ord (ord_spmf op =) f g"
Andreas@63243
  1557
  with mf have "ord_spmf op = (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
Andreas@63243
  1558
  moreover from mg have "\<And>y'. ord_spmf op = (C y' f) (C y' g)"
Andreas@63243
  1559
    by (rule monotoneD) (rule fg)
Andreas@63243
  1560
  ultimately show "ord_spmf op = (bind_spmf (B f) (\<lambda>y. C y f)) (bind_spmf (B g) (\<lambda>y'. C y' g))"
Andreas@63243
  1561
    by(rule bind_spmf_mono')
Andreas@63243
  1562
qed
hoelzl@63333
  1563
Andreas@63243
  1564
lemma monotone_bind_spmf1: "monotone (ord_spmf op =) (ord_spmf op =) (\<lambda>y. bind_spmf y g)"
Andreas@63243
  1565
by(rule monotoneI)(simp add: bind_spmf_mono' ord_spmf_reflI)
Andreas@63243
  1566
hoelzl@63333
  1567
lemma monotone_bind_spmf2:
Andreas@63243
  1568
  assumes g: "\<And>x. monotone ord (ord_spmf op =) (\<lambda>y. g y x)"
Andreas@63243
  1569
  shows "monotone ord (ord_spmf op =) (\<lambda>y. bind_spmf p (g y))"
Andreas@63243
  1570
by(rule monotoneI)(auto intro: bind_spmf_mono' monotoneD[OF g] ord_spmf_reflI)
Andreas@63243
  1571
Andreas@63243
  1572
lemma bind_lub_spmf:
Andreas@63243
  1573
  assumes chain: "Complete_Partial_Order.chain (ord_spmf op =) Y"
Andreas@63243
  1574
  shows "bind_spmf (lub_spmf Y) f = lub_spmf ((\<lambda>p. bind_spmf p f) ` Y)" (is "?lhs = ?rhs")
Andreas@63243
  1575
proof(cases "Y = {}")
Andreas@63243
  1576
  case Y: False
Andreas@63243
  1577
  show ?thesis
Andreas@63243
  1578
  proof(rule spmf_eqI)
Andreas@63243
  1579
    fix i
Andreas@63243
  1580
    have chain': "Complete_Partial_Order.chain op \<le> ((\<lambda>p x. ennreal (spmf p x * spmf (f x) i)) ` Y)"
Andreas@63243
  1581
      using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD intro: mult_right_mono)
Andreas@63243
  1582
    have chain'': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. p \<bind> f) ` Y)"
Andreas@63243
  1583
      using chain by(rule chain_imageI)(auto intro!: monotoneI bind_spmf_mono' ord_spmf_reflI)
Andreas@63243
  1584
    let ?M = "count_space (set_spmf (lub_spmf Y))"
Andreas@63243
  1585
    have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ x. ennreal (spmf (lub_spmf Y) x) * ennreal (spmf (f x) i) \<partial>?M"
Andreas@63243
  1586
      by(auto simp add: ennreal_spmf_lub_spmf ennreal_spmf_bind nn_integral_measure_spmf')
Andreas@63243
  1587
    also have "\<dots> = \<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"
Andreas@63243
  1588
      by(subst ennreal_spmf_lub_spmf[OF chain Y])(subst SUP_mult_right_ennreal, simp_all add: ennreal_mult Y)
Andreas@63243
  1589
    also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
Andreas@63243
  1590
      using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
Andreas@63243
  1591
    also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf p f) i))"
Andreas@63243
  1592
      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)
Andreas@63243
  1593
    also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
Andreas@63243
  1594
    finally show "spmf ?lhs i = spmf ?rhs i" by simp
Andreas@63243
  1595
  qed
Andreas@63243
  1596
qed simp
Andreas@63243
  1597
Andreas@63243
  1598
lemma map_lub_spmf:
Andreas@63243
  1599
  "Complete_Partial_Order.chain (ord_spmf op =) Y
Andreas@63243
  1600
  \<Longrightarrow> map_spmf f (lub_spmf Y) = lub_spmf (map_spmf f ` Y)"
Andreas@63243
  1601
unfolding map_spmf_conv_bind_spmf[abs_def] by(simp add: bind_lub_spmf o_def)
Andreas@63243
  1602
Andreas@63243
  1603
lemma mcont_bind_spmf1: "mcont lub_spmf (ord_spmf op =) lub_spmf (ord_spmf op =) (\<lambda>y. bind_spmf y f)"
Andreas@63243
  1604
using monotone_bind_spmf1 by(rule mcontI)(rule contI, simp add: bind_lub_spmf)
Andreas@63243
  1605
Andreas@63243
  1606
lemma bind_lub_spmf2:
Andreas@63243
  1607
  assumes chain: "Complete_Partial_Order.chain ord Y"
Andreas@63243
  1608
  and g: "\<And>y. monotone ord (ord_spmf op =) (g y)"
Andreas@63243
  1609
  shows "bind_spmf x (\<lambda>y. lub_spmf (g y ` Y)) = lub_spmf ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
Andreas@63243
  1610
  (is "?lhs = ?rhs")
Andreas@63243
  1611
proof(cases "Y = {}")
Andreas@63243
  1612
  case Y: False
Andreas@63243
  1613
  show ?thesis
Andreas@63243
  1614
  proof(rule spmf_eqI)
Andreas@63243
  1615
    fix i
Andreas@63243
  1616
    have chain': "\<And>y. Complete_Partial_Order.chain (ord_spmf op =) (g y ` Y)"
Andreas@63243
  1617
      using chain g[THEN monotoneD] by(rule chain_imageI)
Andreas@63243
  1618
    have chain'': "Complete_Partial_Order.chain op \<le> ((\<lambda>p y. ennreal (spmf x y * spmf (g y p) i)) ` Y)"
Andreas@63243
  1619
      using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono)
Andreas@63243
  1620
    have chain''': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
Andreas@63243
  1621
      using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
hoelzl@63333
  1622
Andreas@63243
  1623
    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)"
Andreas@63243
  1624
      by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
Andreas@63243
  1625
    also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
Andreas@63243
  1626
      unfolding nn_integral_measure_spmf' using Y chain''
Andreas@63243
  1627
      by(rule nn_integral_monotone_convergence_SUP_countable) simp
Andreas@63243
  1628
    also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
Andreas@63243
  1629
      by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult)
Andreas@63243
  1630
    also have "\<dots> = ennreal (spmf ?rhs i)" using chain'''
Andreas@63243
  1631
      by(auto simp add: ennreal_spmf_lub_spmf Y)
Andreas@63243
  1632
    finally show "spmf ?lhs i = spmf ?rhs i" by simp
Andreas@63243
  1633
  qed
Andreas@63243
  1634
qed simp
Andreas@63243
  1635
Andreas@63243
  1636
lemma mcont_bind_spmf [cont_intro]:
Andreas@63243
  1637
  assumes f: "mcont luba orda lub_spmf (ord_spmf op =) f"
Andreas@63243
  1638
  and g: "\<And>y. mcont luba orda lub_spmf (ord_spmf op =) (g y)"
Andreas@63243
  1639
  shows "mcont luba orda lub_spmf (ord_spmf op =) (\<lambda>x. bind_spmf (f x) (\<lambda>y. g y x))"
Andreas@63243
  1640
proof(rule spmf.mcont2mcont'[OF _ _ f])
Andreas@63243
  1641
  fix z
Andreas@63243
  1642
  show "mcont lub_spmf (ord_spmf op =) lub_spmf (ord_spmf op =) (\<lambda>x. bind_spmf x (\<lambda>y. g y z))"
Andreas@63243
  1643
    by(rule mcont_bind_spmf1)
Andreas@63243
  1644
next
Andreas@63243
  1645
  fix x
Andreas@63243
  1646
  let ?f = "\<lambda>z. bind_spmf x (\<lambda>y. g y z)"
Andreas@63243
  1647
  have "monotone orda (ord_spmf op =) ?f" using mcont_mono[OF g] by(rule monotone_bind_spmf2)
Andreas@63243
  1648
  moreover have "cont luba orda lub_spmf (ord_spmf op =) ?f"
Andreas@63243
  1649
  proof(rule contI)
Andreas@63243
  1650
    fix Y
Andreas@63243
  1651
    assume chain: "Complete_Partial_Order.chain orda Y" and Y: "Y \<noteq> {}"
Andreas@63243
  1652
    have "bind_spmf x (\<lambda>y. g y (luba Y)) = bind_spmf x (\<lambda>y. lub_spmf (g y ` Y))"
Andreas@63243
  1653
      by(rule bind_spmf_cong)(simp_all add: mcont_contD[OF g chain Y])
Andreas@63243
  1654
    also have "\<dots> = lub_spmf ((\<lambda>p. x \<bind> (\<lambda>y. g y p)) ` Y)" using chain
Andreas@63243
  1655
      by(rule bind_lub_spmf2)(rule mcont_mono[OF g])
Andreas@63243
  1656
    finally show "bind_spmf x (\<lambda>y. g y (luba Y)) = \<dots>" .
Andreas@63243
  1657
  qed
Andreas@63243
  1658
  ultimately show "mcont luba orda lub_spmf (ord_spmf op =) ?f" by(rule mcontI)
Andreas@63243
  1659
qed
Andreas@63243
  1660
Andreas@63243
  1661
lemma bind_pmf_mono [partial_function_mono]:
Andreas@63243
  1662
  "(\<And>y. mono_spmf (\<lambda>f. C y f)) \<Longrightarrow> mono_spmf (\<lambda>f. bind_pmf p (\<lambda>x. C x f))"
Andreas@63243
  1663
using bind_spmf_mono[of "\<lambda>_. spmf_of_pmf p" C] by simp
Andreas@63243
  1664
Andreas@63243
  1665
lemma map_spmf_mono [partial_function_mono]: "mono_spmf B \<Longrightarrow> mono_spmf (\<lambda>g. map_spmf f (B g))"
Andreas@63243
  1666
unfolding map_spmf_conv_bind_spmf by(rule bind_spmf_mono) simp_all
Andreas@63243
  1667
Andreas@63243
  1668
lemma mcont_map_spmf [cont_intro]:
Andreas@63243
  1669
  "mcont luba orda lub_spmf (ord_spmf op =) g
Andreas@63243
  1670
  \<Longrightarrow> mcont luba orda lub_spmf (ord_spmf op =) (\<lambda>x. map_spmf f (g x))"
Andreas@63243
  1671
unfolding map_spmf_conv_bind_spmf by(rule mcont_bind_spmf) simp_all
Andreas@63243
  1672
Andreas@63243
  1673
lemma monotone_set_spmf: "monotone (ord_spmf op =) op \<subseteq> set_spmf"
Andreas@63243
  1674
by(rule monotoneI)(rule ord_spmf_eqD_set_spmf)
Andreas@63243
  1675
Andreas@63243
  1676
lemma cont_set_spmf: "cont lub_spmf (ord_spmf op =) Union op \<subseteq> set_spmf"
Andreas@63243
  1677
by(rule contI)(subst set_lub_spmf; simp)
Andreas@63243
  1678
Andreas@63243
  1679
lemma mcont2mcont_set_spmf[THEN mcont2mcont, cont_intro]:
Andreas@63243
  1680
  shows mcont_set_spmf: "mcont lub_spmf (ord_spmf op =) Union op \<subseteq> set_spmf"
Andreas@63243
  1681
by(rule mcontI monotone_set_spmf cont_set_spmf)+
Andreas@63243
  1682
Andreas@63243
  1683
lemma monotone_spmf: "monotone (ord_spmf op =) op \<le> (\<lambda>p. spmf p x)"
Andreas@63243
  1684
by(rule monotoneI)(simp add: ord_spmf_eq_leD)
Andreas@63243
  1685
Andreas@63243
  1686
lemma cont_spmf: "cont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. spmf p x)"
Andreas@63243
  1687
by(rule contI)(simp add: spmf_lub_spmf)
Andreas@63243
  1688
Andreas@63243
  1689
lemma mcont_spmf: "mcont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. spmf p x)"
Andreas@63243
  1690
by(rule mcontI monotone_spmf cont_spmf)+
Andreas@63243
  1691
Andreas@63243
  1692
lemma cont_ennreal_spmf: "cont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. ennreal (spmf p x))"
Andreas@63243
  1693
by(rule contI)(simp add: ennreal_spmf_lub_spmf)
Andreas@63243
  1694
Andreas@63243
  1695
lemma mcont2mcont_ennreal_spmf [THEN mcont2mcont, cont_intro]:
Andreas@63243
  1696
  shows mcont_ennreal_spmf: "mcont lub_spmf (ord_spmf op =) Sup op \<le> (\<lambda>p. ennreal (spmf p x))"
Andreas@63243
  1697
by(rule mcontI mono2mono_ennreal monotone_spmf cont_ennreal_spmf)+
Andreas@63243
  1698
Andreas@63243
  1699
lemma nn_integral_map_spmf [simp]: "nn_integral (measure_spmf (map_spmf f p)) g = nn_integral (measure_spmf p) (g \<circ> f)"
Andreas@63243
  1700
by(auto 4 3 simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space intro: nn_integral_cong split: split_indicator)
Andreas@63243
  1701
Andreas@63243
  1702
subsubsection \<open>Admissibility of @{term rel_spmf}\<close>
Andreas@63243
  1703
Andreas@63243
  1704
lemma rel_spmf_measureD:
Andreas@63243
  1705
  assumes "rel_spmf R p q"
Andreas@63243
  1706
  shows "measure (measure_spmf p) A \<le> measure (measure_spmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs")
Andreas@63243
  1707
proof -
Andreas@63243
  1708
  have "?lhs = measure (measure_pmf p) (Some ` A)" by(simp add: measure_measure_spmf_conv_measure_pmf)
Andreas@63243
  1709
  also have "\<dots> \<le> measure (measure_pmf q) {y. \<exists>x\<in>Some ` A. rel_option R x y}"
Andreas@63243
  1710
    using assms by(rule rel_pmf_measureD)
Andreas@63243
  1711
  also have "\<dots> = ?rhs" unfolding measure_measure_spmf_conv_measure_pmf
Andreas@63243
  1712
    by(rule arg_cong2[where f=measure])(auto simp add: option_rel_Some1)
Andreas@63243
  1713
  finally show ?thesis .
Andreas@63243
  1714
qed
Andreas@63243
  1715
Andreas@63243
  1716
locale rel_spmf_characterisation =
Andreas@63243
  1717
  assumes rel_pmf_measureI:
hoelzl@63333
  1718
    "\<And>(R :: 'a option \<Rightarrow> 'b option \<Rightarrow> bool) p q.
Andreas@63243
  1719
    (\<And>A. measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y})
Andreas@63243
  1720
    \<Longrightarrow> rel_pmf R p q"
wenzelm@63308
  1721
  \<comment> \<open>This assumption is shown to hold in general in the AFP entry \<open>MFMC_Countable\<close>.\<close>
Andreas@63243
  1722
begin
Andreas@63243
  1723
Andreas@63243
  1724
context fixes R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" begin
Andreas@63243
  1725
Andreas@63243
  1726
lemma rel_spmf_measureI:
Andreas@63243
  1727
  assumes eq1: "\<And>A. measure (measure_spmf p) A \<le> measure (measure_spmf q) {y. \<exists>x\<in>A. R x y}"
Andreas@63243
  1728
  assumes eq2: "weight_spmf q \<le> weight_spmf p"
Andreas@63243
  1729
  shows "rel_spmf R p q"
Andreas@63243
  1730
proof(rule rel_pmf_measureI)
Andreas@63243
  1731
  fix A :: "'a option set"
Andreas@63243
  1732
  define A' where "A' = the ` (A \<inter> range Some)"
Andreas@63243
  1733
  define A'' where "A'' = A \<inter> {None}"
Andreas@63243
  1734
  have A: "A = Some ` A' \<union> A''" "Some ` A' \<inter> A'' = {}"
Andreas@63243
  1735
    unfolding A'_def A''_def by(auto 4 3 intro: rev_image_eqI)
Andreas@63243
  1736
  have "measure (measure_pmf p) A = measure (measure_pmf p) (Some ` A') + measure (measure_pmf p) A''"
Andreas@63243
  1737
    by(simp add: A measure_pmf.finite_measure_Union)
Andreas@63243
  1738
  also have "measure (measure_pmf p) (Some ` A') = measure (measure_spmf p) A'"
Andreas@63243
  1739
    by(simp add: measure_measure_spmf_conv_measure_pmf)
Andreas@63243
  1740
  also have "\<dots> \<le> measure (measure_spmf q) {y. \<exists>x\<in>A'. R x y}" by(rule eq1)
Andreas@63243
  1741
  also (ord_eq_le_trans[OF _ add_right_mono])
Andreas@63243
  1742
  have "\<dots> = measure (measure_pmf q) {y. \<exists>x\<in>A'. rel_option R (Some x) y}"
Andreas@63243
  1743
    unfolding measure_measure_spmf_conv_measure_pmf
Andreas@63243
  1744
    by(rule arg_cong2[where f=measure])(auto simp add: A'_def option_rel_Some1)
Andreas@63243
  1745
  also
Andreas@63243
  1746
  { have "weight_spmf p \<le> measure (measure_spmf q) {y. \<exists>x. R x y}"
Andreas@63243
  1747
      using eq1[of UNIV] unfolding weight_spmf_def by simp
Andreas@63243
  1748
    also have "\<dots> \<le> weight_spmf q" unfolding weight_spmf_def
Andreas@63243
  1749
      by(rule measure_spmf.finite_measure_mono) simp_all
Andreas@63243
  1750
    finally have "weight_spmf p = weight_spmf q" using eq2 by simp }
Andreas@63243
  1751
  then have "measure (measure_pmf p) A'' = measure (measure_pmf q) (if None \<in> A then {None} else {})"
Andreas@63243
  1752
    unfolding A''_def by(simp add: pmf_None_eq_weight_spmf measure_pmf_single)
Andreas@63243
  1753
  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}"
Andreas@63243
  1754
    by(subst measure_pmf.finite_measure_Union[symmetric])
Andreas@63243
  1755
      (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)
Andreas@63243
  1756
  finally show "measure (measure_pmf p) A \<le> \<dots>" .
Andreas@63243
  1757
qed
Andreas@63243
  1758
Andreas@63243
  1759
lemma admissible_rel_spmf:
Andreas@63243
  1760
  "ccpo.admissible (prod_lub lub_spmf lub_spmf) (rel_prod (ord_spmf op =) (ord_spmf op =)) (case_prod (rel_spmf R))"
Andreas@63243
  1761
  (is "ccpo.admissible ?lub ?ord ?P")
Andreas@63243
  1762
proof(rule ccpo.admissibleI)
Andreas@63243
  1763
  fix Y
Andreas@63243
  1764
  assume chain: "Complete_Partial_Order.chain ?ord Y"
Andreas@63243
  1765
    and Y: "Y \<noteq> {}"
Andreas@63243
  1766
    and R: "\<forall>(p, q) \<in> Y. rel_spmf R p q"
Andreas@63243
  1767
  from R have R: "\<And>p q. (p, q) \<in> Y \<Longrightarrow> rel_spmf R p q" by auto
Andreas@63243
  1768
  have chain1: "Complete_Partial_Order.chain (ord_spmf op =) (fst ` Y)"
Andreas@63243
  1769
    and chain2: "Complete_Partial_Order.chain (ord_spmf op =) (snd ` Y)"
Andreas@63243
  1770
    using chain by(rule chain_imageI; clarsimp)+
Andreas@63243
  1771
  from Y have Y1: "fst ` Y \<noteq> {}" and Y2: "snd ` Y \<noteq> {}" by auto
Andreas@63243
  1772
Andreas@63243
  1773
  have "rel_spmf R (lub_spmf (fst ` Y)) (lub_spmf (snd ` Y))"
Andreas@63243
  1774
  proof(rule rel_spmf_measureI)
Andreas@63243
  1775
    show "weight_spmf (lub_spmf (snd ` Y)) \<le> weight_spmf (lub_spmf (fst ` Y))"
Andreas@63243
  1776
      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]])
Andreas@63243
  1777
Andreas@63243
  1778
    fix A
Andreas@63243
  1779
    have "measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y:fst ` Y. measure (measure_spmf y) A)"
Andreas@63243
  1780
      using chain1 Y1 by(rule measure_lub_spmf)
Andreas@63243
  1781
    also have "\<dots> \<le> (SUP y:snd ` Y. measure (measure_spmf y) {y. \<exists>x\<in>A. R x y})" using Y1
Andreas@63243
  1782
      by(rule cSUP_least)(auto intro!: cSUP_upper2[OF bdd_aboveI2[OF measure_spmf.subprob_measure_le_1]] rel_spmf_measureD R)
Andreas@63243
  1783
    also have "\<dots> = measure (measure_spmf (lub_spmf (snd ` Y))) {y. \<exists>x\<in>A. R x y}"
Andreas@63243
  1784
      using chain2 Y2 by(rule measure_lub_spmf[symmetric])
Andreas@63243
  1785
    finally show "measure (measure_spmf (lub_spmf (fst ` Y))) A \<le> \<dots>" .
Andreas@63243
  1786
  qed
Andreas@63243
  1787
  then show "?P (?lub Y)" by(simp add: prod_lub_def)
Andreas@63243
  1788
qed
Andreas@63243
  1789
Andreas@63243
  1790
lemma admissible_rel_spmf_mcont [cont_intro]:
Andreas@63243
  1791
  "\<lbrakk> mcont lub ord lub_spmf (ord_spmf op =) f; mcont lub ord lub_spmf (ord_spmf op =) g \<rbrakk>
Andreas@63243
  1792
  \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. rel_spmf R (f x) (g x))"
Andreas@63243
  1793
by(rule admissible_subst[OF admissible_rel_spmf, where f="\<lambda>x. (f x, g x)", simplified])(rule mcont_Pair)
Andreas@63243
  1794
wenzelm@63343
  1795
context includes lifting_syntax
wenzelm@63343
  1796
begin
Andreas@63243
  1797
Andreas@63243
  1798
lemma fixp_spmf_parametric':
Andreas@63243
  1799
  assumes f: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) F"
Andreas@63243
  1800
  and g: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) G"
Andreas@63243
  1801
  and param: "(rel_spmf R ===> rel_spmf R) F G"
Andreas@63243
  1802
  shows "(rel_spmf R) (ccpo.fixp lub_spmf (ord_spmf op =) F) (ccpo.fixp lub_spmf (ord_spmf op =) G)"
Andreas@63243
  1803
by(rule parallel_fixp_induct[OF ccpo_spmf ccpo_spmf _ f g])(auto intro: param[THEN rel_funD])
Andreas@63243
  1804
Andreas@63243
  1805
lemma fixp_spmf_parametric:
Andreas@63243
  1806
  assumes f: "\<And>x. mono_spmf (\<lambda>f. F f x)"
Andreas@63243
  1807
  and g: "\<And>x. mono_spmf (\<lambda>f. G f x)"
Andreas@63243
  1808
  and param: "((A ===> rel_spmf R) ===> A ===> rel_spmf R) F G"
Andreas@63243
  1809
  shows "(A ===> rel_spmf R) (spmf.fixp_fun F) (spmf.fixp_fun G)"
Andreas@63243
  1810
using f g
Andreas@63243
  1811
proof(rule parallel_fixp_induct_1_1[OF partial_function_definitions_spmf partial_function_definitions_spmf _ _ reflexive reflexive, where P="(A ===> rel_spmf R)"])
Andreas@63243
  1812
  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))"
Andreas@63243
  1813
    unfolding rel_fun_def
Andreas@63243
  1814
    apply(rule admissible_all admissible_imp admissible_rel_spmf_mcont)+
Andreas@63243
  1815
    apply(rule spmf.mcont2mcont[OF mcont_call])
Andreas@63243
  1816
     apply(rule mcont_fst)
Andreas@63243
  1817
    apply(rule spmf.mcont2mcont[OF mcont_call])
Andreas@63243
  1818
     apply(rule mcont_snd)
Andreas@63243
  1819
    done
Andreas@63243
  1820
  show "(A ===> rel_spmf R) (\<lambda>_. lub_spmf {}) (\<lambda>_. lub_spmf {})" by auto
Andreas@63243
  1821
  show "(A ===> rel_spmf R) (F f) (G g)" if "(A ===> rel_spmf R) f g" for f g
Andreas@63243
  1822
    using that by(rule rel_funD[OF param])
Andreas@63243
  1823
qed
Andreas@63243
  1824
Andreas@63243
  1825
end
Andreas@63243
  1826
Andreas@63243
  1827
end
Andreas@63243
  1828
Andreas@63243
  1829
end
Andreas@63243
  1830
wenzelm@63308
  1831
subsection \<open>Restrictions on spmfs\<close>
Andreas@63243
  1832
Andreas@63243
  1833
definition restrict_spmf :: "'a spmf \<Rightarrow> 'a set \<Rightarrow> 'a spmf" (infixl "\<upharpoonleft>" 110)
Andreas@63243
  1834
where "p \<upharpoonleft> A = map_pmf (\<lambda>x. x \<bind> (\<lambda>y. if y \<in> A then Some y else None)) p"
Andreas@63243
  1835
Andreas@63243
  1836
lemma set_restrict_spmf [simp]: "set_spmf (p \<upharpoonleft> A) = set_spmf p \<inter> A"
Andreas@63243
  1837
by(fastforce simp add: restrict_spmf_def set_spmf_def split: bind_splits if_split_asm)
Andreas@63243
  1838
Andreas@63243
  1839
lemma restrict_map_spmf: "map_spmf f p \<upharpoonleft> A = map_spmf f (p \<upharpoonleft> (f -` A))"
Andreas@63243
  1840
by(simp add: restrict_spmf_def pmf.map_comp o_def map_option_bind bind_map_option if_distrib cong del: if_weak_cong)
Andreas@63243
  1841
Andreas@63243
  1842
lemma restrict_restrict_spmf [simp]: "p \<upharpoonleft> A \<upharpoonleft> B = p \<upharpoonleft> (A \<inter> B)"
Andreas@63243
  1843
by(auto simp add: restrict_spmf_def pmf.map_comp o_def intro!: pmf.map_cong bind_option_cong)
Andreas@63243
  1844
Andreas@63243
  1845
lemma restrict_spmf_empty [simp]: "p \<upharpoonleft> {} = return_pmf None"
Andreas@63243
  1846
by(simp add: restrict_spmf_def)
Andreas@63243
  1847
Andreas@63243
  1848
lemma restrict_spmf_UNIV [simp]: "p \<upharpoonleft> UNIV = p"
Andreas@63243
  1849
by(simp add: restrict_spmf_def)
Andreas@63243
  1850
Andreas@63243
  1851
lemma spmf_restrict_spmf_outside [simp]: "x \<notin> A \<Longrightarrow> spmf (p \<upharpoonleft> A) x = 0"
Andreas@63243
  1852
by(simp add: spmf_eq_0_set_spmf)
Andreas@63243
  1853
Andreas@63243
  1854
lemma emeasure_restrict_spmf [simp]:
Andreas@63243
  1855
  "emeasure (measure_spmf (p \<upharpoonleft> A)) X = emeasure (measure_spmf p) (X \<inter> A)"
Andreas@63243
  1856
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)
Andreas@63243
  1857
Andreas@63243
  1858
lemma measure_restrict_spmf [simp]:
Andreas@63243
  1859
  "measure (measure_spmf (p \<upharpoonleft> A)) X = measure (measure_spmf p) (X \<inter> A)"
Andreas@63243
  1860
using emeasure_restrict_spmf[of p A X]
Andreas@63243
  1861
by(simp only: measure_spmf.emeasure_eq_measure ennreal_inj measure_nonneg)
Andreas@63243
  1862
Andreas@63243
  1863
lemma spmf_restrict_spmf: "spmf (p \<upharpoonleft> A) x = (if x \<in> A then spmf p x else 0)"
Andreas@63243
  1864
by(simp add: spmf_conv_measure_spmf)
Andreas@63243
  1865
Andreas@63243
  1866
lemma spmf_restrict_spmf_inside [simp]: "x \<in> A \<Longrightarrow> spmf (p \<upharpoonleft> A) x = spmf p x"
Andreas@63243
  1867
by(simp add: spmf_restrict_spmf)
Andreas@63243
  1868
Andreas@63243
  1869
lemma pmf_restrict_spmf_None: "pmf (p \<upharpoonleft> A) None = pmf p None + measure (measure_spmf p) (- A)"
Andreas@63243
  1870
proof -
Andreas@63243
  1871
  have [simp]: "None \<notin> Some ` (- A)" by auto
Andreas@63243
  1872
  have "(\<lambda>x. x \<bind> (\<lambda>y. if y \<in> A then Some y else None)) -` {None} = {None} \<union> (Some ` (- A))"
Andreas@63243
  1873
    by(auto split: bind_splits if_split_asm)
Andreas@63243
  1874
  then show ?thesis unfolding ereal.inject[symmetric]
Andreas@63243
  1875
    by(simp add: restrict_spmf_def ennreal_pmf_map emeasure_pmf_single del: ereal.inject)
Andreas@63243
  1876
      (simp add: pmf.rep_eq measure_pmf.finite_measure_Union[symmetric] measure_measure_spmf_conv_measure_pmf measure_pmf.emeasure_eq_measure)
Andreas@63243
  1877
qed
Andreas@63243
  1878
Andreas@63243
  1879
lemma restrict_spmf_trivial: "(\<And>x. x \<in> set_spmf p \<Longrightarrow> x \<in> A) \<Longrightarrow> p \<upharpoonleft> A = p"
Andreas@63243
  1880
by(rule spmf_eqI)(auto simp add: spmf_restrict_spmf spmf_eq_0_set_spmf)
Andreas@63243
  1881
Andreas@63243
  1882
lemma restrict_spmf_trivial': "set_spmf p \<subseteq> A \<Longrightarrow> p \<upharpoonleft> A = p"
Andreas@63243
  1883
by(rule restrict_spmf_trivial) blast
Andreas@63243
  1884
Andreas@63243
  1885
lemma restrict_return_spmf: "return_spmf x \<upharpoonleft> A = (if x \<in> A then return_spmf x else return_pmf None)"
Andreas@63243
  1886
by(simp add: restrict_spmf_def)
Andreas@63243
  1887
Andreas@63243
  1888
lemma restrict_return_spmf_inside [simp]: "x \<in> A \<Longrightarrow> return_spmf x \<upharpoonleft> A = return_spmf x"
Andreas@63243
  1889
by(simp add: restrict_return_spmf)
Andreas@63243
  1890
Andreas@63243
  1891
lemma restrict_return_spmf_outside [simp]: "x \<notin> A \<Longrightarrow> return_spmf x \<upharpoonleft> A = return_pmf None"
Andreas@63243
  1892
by(simp add: restrict_return_spmf)
Andreas@63243
  1893
Andreas@63243
  1894
lemma restrict_spmf_return_pmf_None [simp]: "return_pmf None \<upharpoonleft> A = return_pmf None"
Andreas@63243
  1895
by(simp add: restrict_spmf_def)
Andreas@63243
  1896
Andreas@63243
  1897
lemma restrict_bind_pmf: "bind_pmf p g \<upharpoonleft> A = p \<bind> (\<lambda>x. g x \<upharpoonleft> A)"
Andreas@63243
  1898
by(simp add: restrict_spmf_def map_bind_pmf o_def)
Andreas@63243
  1899
Andreas@63243
  1900
lemma restrict_bind_spmf: "bind_spmf p g \<upharpoonleft> A = p \<bind> (\<lambda>x. g x \<upharpoonleft> A)"
Andreas@63243
  1901
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)
Andreas@63243
  1902
Andreas@63243
  1903
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)"
Andreas@63243
  1904
by(auto simp add: restrict_spmf_def bind_map_pmf fun_eq_iff split: bind_split intro: arg_cong2[where f=bind_pmf])
Andreas@63243
  1905
Andreas@63243
  1906
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)"
Andreas@63243
  1907
by(auto simp add: bind_spmf_def bind_restrict_pmf fun_eq_iff intro: arg_cong2[where f=bind_pmf] split: option.split)
Andreas@63243
  1908
Andreas@63243
  1909
lemma spmf_map_restrict: "spmf (map_spmf fst (p \<upharpoonleft> (snd -` {y}))) x = spmf p (x, y)"
Andreas@63243
  1910
by(subst spmf_map)(auto intro: arg_cong2[where f=measure] simp add: spmf_conv_measure_spmf)
Andreas@63243
  1911
Andreas@63243
  1912
lemma measure_eqI_restrict_spmf:
Andreas@63243
  1913
  assumes "rel_spmf R (restrict_spmf p A) (restrict_spmf q B)"
Andreas@63243
  1914
  shows "measure (measure_spmf p) A = measure (measure_spmf q) B"
Andreas@63243
  1915
proof -
Andreas@63243
  1916
  from assms have "weight_spmf (restrict_spmf p A) = weight_spmf (restrict_spmf q B)" by(rule rel_spmf_weightD)
Andreas@63243
  1917
  thus ?thesis by(simp add: weight_spmf_def)
Andreas@63243
  1918
qed
Andreas@63243
  1919
wenzelm@63308
  1920
subsection \<open>Subprobability distributions of sets\<close>
Andreas@63243
  1921
Andreas@63243
  1922
definition spmf_of_set :: "'a set \<Rightarrow> 'a spmf"
hoelzl@63333
  1923
where
Andreas@63243
  1924
  "spmf_of_set A = (if finite A \<and> A \<noteq> {} then spmf_of_pmf (pmf_of_set A) else return_pmf None)"
Andreas@63243
  1925
Andreas@63243
  1926
lemma spmf_of_set: "spmf (spmf_of_set A) x = indicator A x / card A"
Andreas@63243
  1927
by(auto simp add: spmf_of_set_def)
Andreas@63243
  1928
Andreas@63243
  1929
lemma pmf_spmf_of_set_None [simp]: "pmf (spmf_of_set A) None = indicator {A. infinite A \<or> A = {}} A"
Andreas@63243
  1930
by(simp add: spmf_of_set_def)
Andreas@63243
  1931
Andreas@63243
  1932
lemma set_spmf_of_set: "set_spmf (spmf_of_set A) = (if finite A then A else {})"
Andreas@63243
  1933
by(simp add: spmf_of_set_def)
Andreas@63243
  1934
Andreas@63243
  1935
lemma set_spmf_of_set_finite [simp]: "finite A \<Longrightarrow> set_spmf (spmf_of_set A) = A"
Andreas@63243
  1936
by(simp add: set_spmf_of_set)
Andreas@63243
  1937
Andreas@63243
  1938
lemma spmf_of_set_singleton: "spmf_of_set {x} = return_spmf x"
Andreas@63243
  1939
by(simp add: spmf_of_set_def pmf_of_set_singleton)
Andreas@63243
  1940
Andreas@63243
  1941
lemma map_spmf_of_set_inj_on [simp]:
Andreas@63243
  1942
  "inj_on f A \<Longrightarrow> map_spmf f (spmf_of_set A) = spmf_of_set (f ` A)"
Andreas@63243
  1943
by(auto simp add: spmf_of_set_def map_pmf_of_set_inj dest: finite_imageD)
Andreas@63243
  1944
hoelzl@63333
  1945
lemma spmf_of_pmf_pmf_of_set [simp]:
Andreas@63243
  1946
  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> spmf_of_pmf (pmf_of_set A) = spmf_of_set A"
Andreas@63243
  1947
by(simp add: spmf_of_set_def)
Andreas@63243
  1948
Andreas@63243
  1949
lemma weight_spmf_of_set:
Andreas@63243
  1950
  "weight_spmf (spmf_of_set A) = (if finite A \<and> A \<noteq> {} then 1 else 0)"
Andreas@63243
  1951
by(auto simp only: spmf_of_set_def weight_spmf_of_pmf weight_return_pmf_None split: if_split)
Andreas@63243
  1952
Andreas@63243
  1953
lemma weight_spmf_of_set_finite [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> weight_spmf (spmf_of_set A) = 1"
Andreas@63243
  1954
by(simp add: weight_spmf_of_set)
Andreas@63243
  1955
Andreas@63243
  1956
lemma weight_spmf_of_set_infinite [simp]: "infinite A \<Longrightarrow> weight_spmf (spmf_of_set A) = 0"
Andreas@63243
  1957
by(simp add: weight_spmf_of_set)
Andreas@63243
  1958
Andreas@63243
  1959
lemma measure_spmf_spmf_of_set:
Andreas@63243
  1960
  "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))"
Andreas@63243
  1961
by(simp add: spmf_of_set_def del: spmf_of_pmf_pmf_of_set)
Andreas@63243
  1962
Andreas@63243
  1963
lemma emeasure_spmf_of_set:
Andreas@63243
  1964
  "emeasure (measure_spmf (spmf_of_set S)) A = card (S \<inter> A) / card S"
Andreas@63243
  1965
by(auto simp add: measure_spmf_spmf_of_set emeasure_pmf_of_set)
Andreas@63243
  1966
Andreas@63243
  1967
lemma measure_spmf_of_set:
Andreas@63243
  1968
  "measure (measure_spmf (spmf_of_set S)) A = card (S \<inter> A) / card S"
Andreas@63243
  1969
by(auto simp add: measure_spmf_spmf_of_set measure_pmf_of_set)
Andreas@63243
  1970
Andreas@63243
  1971
lemma nn_integral_spmf_of_set: "nn_integral (measure_spmf (spmf_of_set A)) f = setsum f A / card A"
Andreas@63243
  1972
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)
Andreas@63243
  1973
Andreas@63243
  1974
lemma integral_spmf_of_set: "integral\<^sup>L (measure_spmf (spmf_of_set A)) f = setsum f A / card A"
Andreas@63243
  1975
by(clarsimp simp add: spmf_of_set_def integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set)
Andreas@63243
  1976
wenzelm@63308
  1977
notepad begin \<comment> \<open>@{const pmf_of_set} is not fully parametric.\<close>
Andreas@63243
  1978
  define R :: "nat \<Rightarrow> nat \<Rightarrow> bool" where "R x y \<longleftrightarrow> (x \<noteq> 0 \<longrightarrow> y = 0)" for x y
Andreas@63243
  1979
  define A :: "nat set" where "A = {0, 1}"
Andreas@63243
  1980
  define B :: "nat set" where "B = {0, 1, 2}"
Andreas@63243
  1981
  have "rel_set R A B" unfolding R_def[abs_def] A_def B_def rel_set_def by auto
Andreas@63243
  1982
  have "\<not> rel_pmf R (pmf_of_set A) (pmf_of_set B)"
Andreas@63243
  1983
  proof
Andreas@63243
  1984
    assume "rel_pmf R (pmf_of_set A) (pmf_of_set B)"
Andreas@63243
  1985
    then obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
Andreas@63243
  1986
      and 1: "map_pmf fst pq = pmf_of_set A"
Andreas@63243
  1987
      and 2: "map_pmf snd pq = pmf_of_set B"
Andreas@63243
  1988
      by cases auto
Andreas@63243
  1989
    have "pmf (pmf_of_set B) 1 = 1 / 3" by(simp add: B_def)
Andreas@63243
  1990
    have "pmf (pmf_of_set B) 2 = 1 / 3" by(simp add: B_def)
Andreas@63243
  1991
Andreas@63243
  1992
    have "2 / 3 = pmf (pmf_of_set B) 1 + pmf (pmf_of_set B) 2" by(simp add: B_def)
Andreas@63243
  1993
    also have "\<dots> = measure (measure_pmf (pmf_of_set B)) ({1} \<union> {2})"
Andreas@63243
  1994
      by(subst measure_pmf.finite_measure_Union)(simp_all add: measure_pmf_single)
Andreas@63243
  1995
    also have "\<dots> = emeasure (measure_pmf pq) (snd -` {2, 1})"
Andreas@63243
  1996
      unfolding 2[symmetric] measure_pmf.emeasure_eq_measure[symmetric] by(simp)
Andreas@63243
  1997
    also have "\<dots> = emeasure (measure_pmf pq) {(0, 2), (0, 1)}"
Andreas@63243
  1998
      by(rule emeasure_eq_AE)(auto simp add: AE_measure_pmf_iff R_def dest!: pq)
Andreas@63243
  1999
    also have "\<dots> \<le> emeasure (measure_pmf pq) (fst -` {0})"
Andreas@63243
  2000
      by(rule emeasure_mono) auto
Andreas@63243
  2001
    also have "\<dots> = emeasure (measure_pmf (pmf_of_set A)) {0}"
Andreas@63243
  2002
      unfolding 1[symmetric] by simp
Andreas@63243
  2003
    also have "\<dots> = pmf (pmf_of_set A) 0"
Andreas@63243
  2004
      by(simp add: measure_pmf_single measure_pmf.emeasure_eq_measure)
Andreas@63243
  2005
    also have "pmf (pmf_of_set A) 0 = 1 / 2" by(simp add: A_def)
Andreas@63243
  2006
    finally show False by(subst (asm) ennreal_le_iff; simp)
Andreas@63243
  2007
  qed
Andreas@63243
  2008
end
Andreas@63243
  2009
Andreas@63243
  2010
lemma rel_pmf_of_set_bij:
Andreas@63243
  2011
  assumes f: "bij_betw f A B"
Andreas@63243
  2012
  and A: "A \<noteq> {}" "finite A"
hoelzl@63333
  2013
  and B: "B \<noteq> {}" "finite B"
Andreas@63243
  2014
  and R: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
Andreas@63243
  2015
  shows "rel_pmf R (pmf_of_set A) (pmf_of_set B)"
Andreas@63243
  2016
proof(rule pmf.rel_mono_strong)
Andreas@63243
  2017
  define AB where "AB = (\<lambda>x. (x, f x)) ` A"
Andreas@63243
  2018
  define R' where "R' x y \<longleftrightarrow> (x, y) \<in> AB" for x y
Andreas@63243
  2019
  have "(x, y) \<in> AB" if "(x, y) \<in> set_pmf (pmf_of_set AB)" for x y
Andreas@63243
  2020
    using that by(auto simp add: AB_def A)
Andreas@63243
  2021
  moreover have "map_pmf fst (pmf_of_set AB) = pmf_of_set A"
Andreas@63243
  2022
    by(simp add: AB_def map_pmf_of_set_inj[symmetric] inj_on_def A pmf.map_comp o_def)
Andreas@63243
  2023
  moreover
Andreas@63243
  2024
  from f have [simp]: "inj_on f A" by(rule bij_betw_imp_inj_on)
Andreas@63243
  2025
  from f have [simp]: "f ` A = B" by(rule bij_betw_imp_surj_on)
Andreas@63243
  2026
  have "map_pmf snd (pmf_of_set AB) = pmf_of_set B"
Andreas@63243
  2027
    by(simp add: AB_def map_pmf_of_set_inj[symmetric] inj_on_def A pmf.map_comp o_def)
Andreas@63243
  2028
      (simp add: map_pmf_of_set_inj A)
Andreas@63243
  2029
  ultimately show "rel_pmf (\<lambda>x y. (x, y) \<in> AB) (pmf_of_set A) (pmf_of_set B)" ..
Andreas@63243
  2030
qed(auto intro: R)
Andreas@63243
  2031
Andreas@63243
  2032
lemma rel_spmf_of_set_bij:
Andreas@63243
  2033
  assumes f: "bij_betw f A B"
Andreas@63243
  2034
  and R: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
Andreas@63243
  2035
  shows "rel_spmf R (spmf_of_set A) (spmf_of_set B)"
Andreas@63243
  2036
proof -
Andreas@63243
  2037
  have "finite A \<longleftrightarrow> finite B" using f by(rule bij_betw_finite)
Andreas@63243
  2038
  moreover have "A = {} \<longleftrightarrow> B = {}" using f by(auto dest: bij_betw_empty2 bij_betw_empty1)
Andreas@63243
  2039
  ultimately show ?thesis using assms
Andreas@63243
  2040
    by(auto simp add: spmf_of_set_def simp del: spmf_of_pmf_pmf_of_set intro: rel_pmf_of_set_bij)
Andreas@63243
  2041
qed
Andreas@63243
  2042
wenzelm@63343
  2043
context includes lifting_syntax
wenzelm@63343
  2044
begin
wenzelm@63343
  2045
Andreas@63243
  2046
lemma rel_spmf_of_set:
Andreas@63243
  2047
  assumes "bi_unique R"
Andreas@63243
  2048
  shows "(rel_set R ===> rel_spmf R) spmf_of_set spmf_of_set"
Andreas@63243
  2049
proof
Andreas@63243
  2050
  fix A B
Andreas@63243
  2051
  assume R: "rel_set R A B"
Andreas@63243
  2052
  with assms obtain f where "bij_betw f A B" and f: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
Andreas@63243
  2053
    by(auto dest: bi_unique_rel_set_bij_betw)
Andreas@63243
  2054
  then show "rel_spmf R (spmf_of_set A) (spmf_of_set B)" by(rule rel_spmf_of_set_bij)
Andreas@63243
  2055
qed
wenzelm@63343
  2056
Andreas@63243
  2057
end
Andreas@63243
  2058
Andreas@63243
  2059
lemma map_mem_spmf_of_set:
Andreas@63243
  2060
  assumes "finite B" "B \<noteq> {}"
Andreas@63243
  2061
  shows "map_spmf (\<lambda>x. x \<in> A) (spmf_of_set B) = spmf_of_pmf (bernoulli_pmf (card (A \<inter> B) / card B))"
Andreas@63243
  2062
  (is "?lhs = ?rhs")
Andreas@63243
  2063
proof(rule spmf_eqI)
Andreas@63243
  2064
  fix i
Andreas@63243
  2065
  have "ennreal (spmf ?lhs i) = card (B \<inter> (\<lambda>x. x \<in> A) -` {i}) / (card B)"
Andreas@63243
  2066
    by(subst ennreal_spmf_map)(simp add: measure_spmf_spmf_of_set assms emeasure_pmf_of_set)
Andreas@63243
  2067
  also have "\<dots> = (if i then card (B \<inter> A) / card B else card (B - A) / card B)"
Andreas@63243
  2068
    by(auto intro: arg_cong[where f=card])
Andreas@63243
  2069
  also have "\<dots> = (if i then card (B \<inter> A) / card B else (card B - card (B \<inter> A)) / card B)"
Andreas@63243
  2070
    by(auto simp add: card_Diff_subset_Int assms)
hoelzl@63333
  2071
  also have "\<dots> = ennreal (spmf ?rhs i)"
Andreas@63243
  2072
    by(simp add: assms card_gt_0_iff field_simps card_mono Int_commute of_nat_diff)
Andreas@63243
  2073
  finally show "spmf ?lhs i = spmf ?rhs i" by simp
Andreas@63243
  2074
qed
Andreas@63243
  2075
Andreas@63243
  2076
abbreviation coin_spmf :: "bool spmf"
Andreas@63243
  2077
where "coin_spmf \<equiv> spmf_of_set UNIV"
Andreas@63243
  2078
Andreas@63243
  2079
lemma map_eq_const_coin_spmf: "map_spmf (op = c) coin_spmf = coin_spmf"
Andreas@63243
  2080
proof -
Andreas@63243
  2081
  have "inj (op \<longleftrightarrow> c)" "range (op \<longleftrightarrow> c) = UNIV" by(auto intro: inj_onI)
Andreas@63243
  2082
  then show ?thesis by simp
Andreas@63243
  2083
qed
Andreas@63243
  2084
Andreas@63243
  2085
lemma bind_coin_spmf_eq_const: "coin_spmf \<bind> (\<lambda>x :: bool. return_spmf (b = x)) = coin_spmf"
Andreas@63243
  2086
using map_eq_const_coin_spmf unfolding map_spmf_conv_bind_spmf by simp
Andreas@63243
  2087
Andreas@63243
  2088
lemma bind_coin_spmf_eq_const': "coin_spmf \<bind> (\<lambda>x :: bool. return_spmf (x = b)) = coin_spmf"
Andreas@63243
  2089
by(rewrite in "_ = \<hole>" bind_coin_spmf_eq_const[symmetric, of b])(auto intro: bind_spmf_cong)
Andreas@63243
  2090
wenzelm@63308
  2091
subsection \<open>Losslessness\<close>
Andreas@63243
  2092
Andreas@63243
  2093
definition lossless_spmf :: "'a spmf \<Rightarrow> bool"
Andreas@63243
  2094
where "lossless_spmf p \<longleftrightarrow> weight_spmf p = 1"
Andreas@63243
  2095
Andreas@63243
  2096
lemma lossless_iff_pmf_None: "lossless_spmf p \<longleftrightarrow> pmf p None = 0"
Andreas@63243
  2097
by(simp add: lossless_spmf_def pmf_None_eq_weight_spmf)
Andreas@63243
  2098
Andreas@63243
  2099
lemma lossless_return_spmf [iff]: "lossless_spmf (return_spmf x)"
Andreas@63243
  2100
by(simp add: lossless_iff_pmf_None)
Andreas@63243
  2101
Andreas@63243
  2102
lemma lossless_return_pmf_None [iff]: "\<not> lossless_spmf (return_pmf None)"
Andreas@63243
  2103
by(simp add: lossless_iff_pmf_None)
Andreas@63243
  2104
Andreas@63243
  2105
lemma lossless_map_spmf [simp]: "lossless_spmf (map_spmf f p) \<longleftrightarrow> lossless_spmf p"
Andreas@63243
  2106
by(auto simp add: lossless_iff_pmf_None pmf_eq_0_set_pmf)
Andreas@63243
  2107
Andreas@63243
  2108
lemma lossless_bind_spmf [simp]:
Andreas@63243
  2109
  "lossless_spmf (p \<bind> f) \<longleftrightarrow> lossless_spmf p \<and> (\<forall>x\<in>set_spmf p. lossless_spmf (f x))"
Andreas@63243
  2110
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)
Andreas@63243
  2111
Andreas@63243
  2112
lemma lossless_weight_spmfD: "lossless_spmf p \<Longrightarrow> weight_spmf p = 1"
Andreas@63243
  2113
by(simp add: lossless_spmf_def)
Andreas@63243
  2114
Andreas@63243
  2115
lemma lossless_iff_set_pmf_None:
Andreas@63243
  2116
  "lossless_spmf p \<longleftrightarrow> None \<notin> set_pmf p"
Andreas@63243
  2117
by (simp add: lossless_iff_pmf_None pmf_eq_0_set_pmf)
Andreas@63243
  2118
Andreas@63243
  2119
lemma lossless_spmf_of_set [simp]: "lossless_spmf (spmf_of_set A) \<longleftrightarrow> finite A \<and> A \<noteq> {}"
Andreas@63243
  2120
by(auto simp add: lossless_spmf_def weight_spmf_of_set)
Andreas@63243
  2121
Andreas@63243
  2122
lemma lossless_spmf_spmf_of_spmf [simp]: "lossless_spmf (spmf_of_pmf p)"
Andreas@63243
  2123
by(simp add: lossless_spmf_def)
Andreas@63243
  2124
Andreas@63243
  2125
lemma lossless_spmf_bind_pmf [simp]:
Andreas@63243
  2126
  "lossless_spmf (bind_pmf p f) \<longleftrightarrow> (\<forall>x\<in>set_pmf p. lossless_spmf (f x))"
Andreas@63243
  2127
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)
Andreas@63243
  2128
Andreas@63243
  2129
lemma lossless_spmf_conv_spmf_of_pmf: "lossless_spmf p \<longleftrightarrow> (\<exists>p'. p = spmf_of_pmf p')"
Andreas@63243
  2130
proof
Andreas@63243
  2131
  assume "lossless_spmf p"
Andreas@63243
  2132
  hence *: "\<And>y. y \<in> set_pmf p \<Longrightarrow> \<exists>x. y = Some x"
Andreas@63243
  2133
    by(case_tac y)(simp_all add: lossless_iff_set_pmf_None)
Andreas@63243
  2134
Andreas@63243
  2135
  let ?p = "map_pmf the p"
Andreas@63243
  2136
  have "p = spmf_of_pmf ?p"
Andreas@63243
  2137
  proof(rule spmf_eqI)
Andreas@63243
  2138
    fix i
Andreas@63243
  2139
    have "ennreal (pmf (map_pmf the p) i) = \<integral>\<^sup>+ x. indicator (the -` {i}) x \<partial>p" by(simp add: ennreal_pmf_map)
Andreas@63243
  2140
    also have "\<dots> = \<integral>\<^sup>+ x. indicator {i} x \<partial>measure_spmf p" unfolding measure_spmf_def
Andreas@63243
  2141
      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!: * )
Andreas@63243
  2142
    also have "\<dots> = spmf p i" by(simp add: emeasure_spmf_single)
Andreas@63243
  2143
    finally show "spmf p i = spmf (spmf_of_pmf ?p) i" by simp
Andreas@63243
  2144
  qed
Andreas@63243
  2145
  thus "\<exists>p'. p = spmf_of_pmf p'" ..
Andreas@63243
  2146
qed auto
Andreas@63243
  2147
Andreas@63243
  2148
lemma spmf_False_conv_True: "lossless_spmf p \<Longrightarrow> spmf p False = 1 - spmf p True"
Andreas@63243
  2149
by(clarsimp simp add: lossless_spmf_conv_spmf_of_pmf pmf_False_conv_True)
Andreas@63243
  2150
Andreas@63243
  2151
lemma spmf_True_conv_False: "lossless_spmf p \<Longrightarrow> spmf p True = 1 - spmf p False"
Andreas@63243
  2152
by(simp add: spmf_False_conv_True)
Andreas@63243
  2153
Andreas@63243
  2154
lemma bind_eq_return_spmf:
Andreas@63243
  2155
  "bind_spmf p f = return_spmf x \<longleftrightarrow> (\<forall>y\<in>set_spmf p. f y = return_spmf x) \<and> lossless_spmf p"
Andreas@63243
  2156
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)
Andreas@63243
  2157
Andreas@63243
  2158
lemma rel_spmf_return_spmf2:
Andreas@63243
  2159
  "rel_spmf R p (return_spmf x) \<longleftrightarrow> lossless_spmf p \<and> (\<forall>a\<in>set_spmf p. R a x)"
Andreas@63243
  2160
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)
Andreas@63243
  2161
Andreas@63243
  2162
lemma rel_spmf_return_spmf1:
Andreas@63243
  2163
  "rel_spmf R (return_spmf x) p \<longleftrightarrow> lossless_spmf p \<and> (\<forall>a\<in>set_spmf p. R x a)"
Andreas@63243
  2164
using rel_spmf_return_spmf2[of "R\<inverse>\<inverse>"] by(simp add: spmf_rel_conversep)
Andreas@63243
  2165
Andreas@63243
  2166
lemma rel_spmf_bindI1:
Andreas@63243
  2167
  assumes f: "\<And>x. x \<in> set_spmf p \<Longrightarrow> rel_spmf R (f x) q"
Andreas@63243
  2168
  and p: "lossless_spmf p"
Andreas@63243
  2169
  shows "rel_spmf R (bind_spmf p f) q"
Andreas@63243
  2170
proof -
Andreas@63243
  2171
  fix x :: 'a
Andreas@63243
  2172
  have "rel_spmf R (bind_spmf p f) (bind_spmf (return_spmf x) (\<lambda>_. q))"
Andreas@63243
  2173
    by(rule rel_spmf_bindI[where R="\<lambda>x _. x \<in> set_spmf p"])(simp_all add: rel_spmf_return_spmf2 p f)
Andreas@63243
  2174
  then show ?thesis by simp
Andreas@63243
  2175
qed
Andreas@63243
  2176
Andreas@63243
  2177
lemma rel_spmf_bindI2:
Andreas@63243
  2178
  "\<lbrakk> \<And>x. x \<in> set_spmf q \<Longrightarrow> rel_spmf R p (f x); lossless_spmf q \<rbrakk>
Andreas@63243
  2179
  \<Longrightarrow> rel_spmf R p (bind_spmf q f)"
Andreas@63243
  2180
using rel_spmf_bindI1[of q "conversep R" f p] by(simp add: spmf_rel_conversep)
Andreas@63243
  2181
wenzelm@63308
  2182
subsection \<open>Scaling\<close>
Andreas@63243
  2183
Andreas@63243
  2184
definition scale_spmf :: "real \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf"
Andreas@63243
  2185
where
Andreas@63243
  2186
  "scale_spmf r p = embed_spmf (\<lambda>x. min (inverse (weight_spmf p)) (max 0 r) * spmf p x)"
Andreas@63243
  2187
Andreas@63243
  2188
lemma scale_spmf_le_1:
Andreas@63243
  2189
  "(\<integral>\<^sup>+ x. min (inverse (weight_spmf p)) (max 0 r) * spmf p x \<partial>count_space UNIV) \<le> 1" (is "?lhs \<le> _")
Andreas@63243
  2190
proof -
Andreas@63243
  2191
  have "?lhs = min (inverse (weight_spmf p)) (max 0 r) * \<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV"
Andreas@63243
  2192
    by(subst nn_integral_cmult[symmetric])(simp_all add: weight_spmf_nonneg max_def min_def ennreal_mult)
Andreas@63243
  2193
  also have "\<dots> \<le> 1" unfolding weight_spmf_eq_nn_integral_spmf[symmetric]
Andreas@63243
  2194
    by(simp add: min_def max_def weight_spmf_nonneg order.strict_iff_order field_simps ennreal_mult[symmetric])
Andreas@63243
  2195
  finally show ?thesis .
Andreas@63243
  2196
qed
Andreas@63243
  2197
Andreas@63243
  2198
lemma spmf_scale_spmf: "spmf (scale_spmf r p) x = max 0 (min (inverse (weight_spmf p)) r) * spmf p x" (is "?lhs = ?rhs")
Andreas@63243
  2199
unfolding scale_spmf_def
Andreas@63243
  2200
apply(subst spmf_embed_spmf[OF scale_spmf_le_1])
Andreas@63243
  2201
apply(simp add: max_def min_def weight_spmf_le_0 field_simps weight_spmf_nonneg not_le order.strict_iff_order)
Andreas@63243
  2202
apply(metis antisym_conv order_trans weight_spmf_nonneg zero_le_mult_iff zero_le_one)
Andreas@63243
  2203
done
Andreas@63243
  2204
Andreas@63243
  2205
lemma real_inverse_le_1_iff: fixes x :: real
Andreas@63243
  2206
  shows "\<lbrakk> 0 \<le> x; x \<le> 1 \<rbrakk> \<Longrightarrow> 1 / x \<le> 1 \<longleftrightarrow> x = 1 \<or> x = 0"
Andreas@63243
  2207
by auto
Andreas@63243
  2208
Andreas@63243
  2209
lemma spmf_scale_spmf': "r \<le> 1 \<Longrightarrow> spmf (scale_spmf r p) x = max 0 r * spmf p x"
Andreas@63243
  2210
using real_inverse_le_1_iff[OF weight_spmf_nonneg weight_spmf_le_1, of p]
Andreas@63243
  2211
by(auto simp add: spmf_scale_spmf max_def min_def field_simps)(metis pmf_le_0_iff spmf_le_weight)
Andreas@63243
  2212
Andreas@63243
  2213
lemma scale_spmf_neg: "r \<le> 0 \<Longrightarrow> scale_spmf r p = return_pmf None"
Andreas@63243
  2214
by(rule spmf_eqI)(simp add: spmf_scale_spmf' max_def)
Andreas@63243
  2215
Andreas@63243
  2216
lemma scale_spmf_return_None [simp]: "scale_spmf r (return_pmf None) = return_pmf None"
Andreas@63243
  2217
by(rule spmf_eqI)(simp add: spmf_scale_spmf)
Andreas@63243
  2218
Andreas@63243
  2219
lemma scale_spmf_conv_bind_bernoulli:
Andreas@63243
  2220
  assumes "r \<le> 1"
Andreas@63243
  2221
  shows "scale_spmf r p = bind_pmf (bernoulli_pmf r) (\<lambda>b. if b then p else return_pmf None)" (is "?lhs = ?rhs")
Andreas@63243
  2222
proof(rule spmf_eqI)
Andreas@63243
  2223
  fix x
Andreas@63243
  2224
  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using assms
Andreas@63243
  2225
    unfolding spmf_scale_spmf ennreal_pmf_bind nn_integral_measure_pmf UNIV_bool bernoulli_pmf.rep_eq
Andreas@63243
  2226
    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])
Andreas@63243
  2227
    apply (metis pmf_le_0_iff spmf_le_weight)
Andreas@63243
  2228
    apply (metis pmf_le_0_iff spmf_le_weight)
Andreas@63243
  2229
    apply (meson le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 not_less order_trans weight_spmf_le_0)
Andreas@63243
  2230
    by (meson divide_le_0_1_iff less_imp_le order_trans weight_spmf_le_0)
Andreas@63243
  2231
  thus "spmf ?lhs x = spmf ?rhs x" by simp
Andreas@63243
  2232
qed
Andreas@63243
  2233
Andreas@63243
  2234
lemma nn_integral_spmf: "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space A) = emeasure (measure_spmf p) A"
Andreas@63243
  2235
apply(simp add: measure_spmf_def emeasure_distr emeasure_restrict_space space_restrict_space nn_integral_pmf[symmetric])
Andreas@63243
  2236
apply(rule nn_integral_bij_count_space[where g=Some])
Andreas@63243
  2237
apply(auto simp add: bij_betw_def)
Andreas@63243
  2238
done
Andreas@63243
  2239
Andreas@63243
  2240
lemma measure_spmf_scale_spmf: "measure_spmf (scale_spmf r p) = scale_measure (min (inverse (weight_spmf p)) r) (measure_spmf p)"
Andreas@63243
  2241
apply(rule measure_eqI)
Andreas@63243
  2242
 apply simp
Andreas@63243
  2243
apply(simp add: nn_integral_spmf[symmetric] spmf_scale_spmf)
Andreas@63243
  2244
apply(subst nn_integral_cmult[symmetric])
Andreas@63243
  2245
apply(auto simp add: max_def min_def ennreal_mult[symmetric] not_le ennreal_lt_0)
Andreas@63243
  2246
done
Andreas@63243
  2247
hoelzl@63333
  2248
lemma measure_spmf_scale_spmf':
Andreas@63243
  2249
  "r \<le> 1 \<Longrightarrow> measure_spmf (scale_spmf r p) = scale_measure r (measure_spmf p)"
Andreas@63243
  2250
unfolding measure_spmf_scale_spmf
Andreas@63243
  2251
apply(cases "weight_spmf p > 0")
Andreas@63243
  2252
 apply(simp add: min.absorb2 field_simps weight_spmf_le_1 mult_le_one)
Andreas@63243
  2253
apply(clarsimp simp add: weight_spmf_le_0 min_def scale_spmf_neg weight_spmf_eq_0 not_less)
Andreas@63243
  2254
done
Andreas@63243
  2255
Andreas@63243
  2256
lemma scale_spmf_1 [simp]: "scale_spmf 1 p = p"
Andreas@63243
  2257
apply(rule spmf_eqI)
Andreas@63243
  2258
apply(simp add: spmf_scale_spmf max_def min_def order.strict_iff_order field_simps weight_spmf_nonneg)
Andreas@63243
  2259
apply(metis antisym_conv divide_le_eq_1 less_imp_le pmf_nonneg spmf_le_weight weight_spmf_nonneg weight_spmf_le_1)
Andreas@63243
  2260
done
Andreas@63243
  2261
Andreas@63243
  2262
lemma scale_spmf_0 [simp]: "scale_spmf 0 p = return_pmf None"
Andreas@63243
  2263
by(rule spmf_eqI)(simp add: spmf_scale_spmf min_def max_def weight_spmf_le_0)
Andreas@63243
  2264
hoelzl@63333
  2265
lemma bind_scale_spmf:
Andreas@63243
  2266
  assumes r: "r \<le> 1"
Andreas@63243
  2267
  shows "bind_spmf (scale_spmf r p) f = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
Andreas@63243
  2268
  (is "?lhs = ?rhs")
Andreas@63243
  2269
proof(rule spmf_eqI)
Andreas@63243
  2270
  fix x
Andreas@63243
  2271
  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using r
Andreas@63243
  2272
    by(simp add: ennreal_spmf_bind measure_spmf_scale_spmf' nn_integral_scale_measure spmf_scale_spmf')
Andreas@63243
  2273
      (simp add: ennreal_mult ennreal_lt_0 nn_integral_cmult max_def min_def)
Andreas@63243
  2274
  thus "spmf ?lhs x = spmf ?rhs x" by simp
Andreas@63243
  2275
qed
Andreas@63243
  2276
hoelzl@63333
  2277
lemma scale_bind_spmf:
Andreas@63243
  2278
  assumes "r \<le> 1"
Andreas@63243
  2279
  shows "scale_spmf r (bind_spmf p f) = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
Andreas@63243
  2280
  (is "?lhs = ?rhs")
Andreas@63243
  2281
proof(rule spmf_eqI)
Andreas@63243
  2282
  fix x
Andreas@63243
  2283
  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)" using assms
Andreas@63243
  2284
    unfolding spmf_scale_spmf'[OF assms]
Andreas@63243
  2285
    by(simp add: ennreal_mult ennreal_spmf_bind spmf_scale_spmf' nn_integral_cmult max_def min_def)
Andreas@63243
  2286
  thus "spmf ?lhs x = spmf ?rhs x" by simp
Andreas@63243
  2287
qed
Andreas@63243
  2288
Andreas@63243
  2289
lemma bind_spmf_const: "bind_spmf p (\<lambda>x. q) = scale_spmf (weight_spmf p) q" (is "?lhs = ?rhs")
Andreas@63243
  2290
proof(rule spmf_eqI)
Andreas@63243
  2291
  fix x
Andreas@63243
  2292
  have "ennreal (spmf ?lhs x) = ennreal (spmf ?rhs x)"
Andreas@63243
  2293
    using measure_spmf.subprob_measure_le_1[of p "space (measure_spmf p)"]
Andreas@63243
  2294
    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)
Andreas@63243
  2295
  thus "spmf ?lhs x = spmf ?rhs x" by simp
Andreas@63243
  2296
qed
Andreas@63243
  2297
Andreas@63243
  2298
lemma map_scale_spmf: "map_spmf f (scale_spmf r p) = scale_spmf r (map_spmf f p)" (is "?lhs = ?rhs")
Andreas@63243
  2299
proof(rule spmf_eqI)
Andreas@63243
  2300
  fix i
Andreas@63243
  2301
  show "spmf ?lhs i = spmf ?rhs i" unfolding spmf_scale_spmf
Andreas@63243
  2302
    by(subst (1 2) spmf_map)(auto simp add: measure_spmf_scale_spmf max_def min_def ennreal_lt_0)
Andreas@63243
  2303
qed
Andreas@63243
  2304
Andreas@63243
  2305
lemma set_scale_spmf: "set_spmf (scale_spmf r p) = (if r > 0 then set_spmf p else {})"
Andreas@63243
  2306
apply(auto simp add: in_set_spmf_iff_spmf spmf_scale_spmf)
Andreas@63243
  2307
apply(simp add: max_def min_def not_le weight_spmf_lt_0 weight_spmf_eq_0 split: if_split_asm)
Andreas@63243
  2308
done
Andreas@63243
  2309
Andreas@63243
  2310
lemma set_scale_spmf' [simp]: "0 < r \<Longrightarrow> set_spmf (scale_spmf r p) = set_spmf p"
Andreas@63243
  2311
by(simp add: set_scale_spmf)
Andreas@63243
  2312
hoelzl@63333
  2313
lemma rel_spmf_scaleI:
Andreas@63243
  2314
  assumes "r > 0 \<Longrightarrow> rel_spmf A p q"
Andreas@63243
  2315
  shows "rel_spmf A (scale_spmf r p) (scale_spmf r q)"
Andreas@63243
  2316
proof(cases "r > 0")
Andreas@63243
  2317
  case True
Andreas@63243
  2318
  from assms[OF this] show ?thesis
Andreas@63243
  2319
    by(rule rel_spmfE)(auto simp add: map_scale_spmf[symmetric] spmf_rel_map True intro: rel_spmf_reflI)
Andreas@63243
  2320
qed(simp add: not_less scale_spmf_neg)
Andreas@63243
  2321
Andreas@63243
  2322
lemma weight_scale_spmf: "weight_spmf (scale_spmf r p) = min 1 (max 0 r * weight_spmf p)"
Andreas@63243
  2323
proof -
Andreas@63243
  2324
  have "ennreal (weight_spmf (scale_spmf r p)) = min 1 (max 0 r * ennreal (weight_spmf p))"
Andreas@63243
  2325
    unfolding weight_spmf_eq_nn_integral_spmf
Andreas@63243
  2326
    apply(simp add: spmf_scale_spmf ennreal_mult zero_ereal_def[symmetric] nn_integral_cmult)
Andreas@63243
  2327
    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])
Andreas@63243
  2328
    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)
Andreas@63243
  2329
    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)
Andreas@63243
  2330
    done
Andreas@63243
  2331
  thus ?thesis by(auto simp add: min_def max_def ennreal_mult[symmetric] split: if_split_asm)
Andreas@63243
  2332
qed
Andreas@63243
  2333
hoelzl@63333
  2334
lemma weight_scale_spmf' [simp]:
Andreas@63243
  2335
  "\<lbrakk> 0 \<le> r; r \<le> 1 \<rbrakk> \<Longrightarrow> weight_spmf (scale_spmf r p) = r * weight_spmf p"
Andreas@63243
  2336
by(simp add: weight_scale_spmf max_def min_def)(metis antisym_conv mult_left_le order_trans weight_spmf_le_1)
Andreas@63243
  2337
Andreas@63243
  2338
lemma pmf_scale_spmf_None:
Andreas@63243
  2339
  "pmf (scale_spmf k p) None = 1 - min 1 (max 0 k * (1 - pmf p None))"
Andreas@63243
  2340
unfolding pmf_None_eq_weight_spmf by(simp add: weight_scale_spmf)
Andreas@63243
  2341
hoelzl@63333
  2342
lemma scale_scale_spmf:
Andreas@63243
  2343
  "scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
Andreas@63243
  2344
  (is "?lhs = ?rhs")
Andreas@63243
  2345
proof(rule spmf_eqI)
Andreas@63243
  2346
  fix i
Andreas@63243
  2347
  have "max 0 (min (1 / weight_spmf p) r') *
Andreas@63243
  2348
    max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
Andreas@63243
  2349
    max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
Andreas@63243
  2350
  proof(cases "weight_spmf p > 0")
Andreas@63243
  2351
    case False
Andreas@63243
  2352
    thus ?thesis by(simp add: not_less weight_spmf_le_0)
Andreas@63243
  2353
  next
Andreas@63243
  2354
    case True
Andreas@63243
  2355
    thus ?thesis by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
Andreas@63243
  2356
  qed
Andreas@63243
  2357
  then show "spmf ?lhs i = spmf ?rhs i"
Andreas@63243
  2358
    by(simp add: spmf_scale_spmf field_simps weight_scale_spmf)
Andreas@63243
  2359
qed
Andreas@63243
  2360
Andreas@63243
  2361
lemma scale_scale_spmf' [simp]:
Andreas@63243
  2362
  "\<lbrakk> 0 \<le> r; r \<le> 1; 0 \<le> r'; r' \<le> 1 \<rbrakk>
Andreas@63243
  2363
  \<Longrightarrow> scale_spmf r (scale_spmf r' p) = scale_spmf (r * r') p"
Andreas@63243
  2364
apply(cases "weight_spmf p > 0")
Andreas@63243
  2365
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)
Andreas@63243
  2366
apply(subgoal_tac "1 = r'")
Andreas@63243
  2367
 apply (metis (no_types) divide_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
Andreas@63243
  2368
apply(meson eq_iff le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 mult_imp_div_pos_le order.trans)
Andreas@63243
  2369
done
Andreas@63243
  2370
Andreas@63243
  2371
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"
Andreas@63243
  2372
  (is "?lhs \<longleftrightarrow> ?rhs")
Andreas@63243
  2373
proof
Andreas@63243
  2374
  assume ?lhs
Andreas@63243
  2375
  hence "weight_spmf (scale_spmf r p) = weight_spmf p" by simp
Andreas@63243
  2376
  hence *: "min 1 (max 0 r * weight_spmf p) = weight_spmf p" by(simp add: weight_scale_spmf)
Andreas@63243
  2377
  hence **: "weight_spmf p = 0 \<or> r \<ge> 1" by(auto simp add: min_def max_def split: if_split_asm)
Andreas@63243
  2378
  show ?rhs
Andreas@63243
  2379
  proof(cases "weight_spmf p = 0")
Andreas@63243
  2380
    case False
Andreas@63243
  2381
    with ** have "r \<ge> 1" by simp
Andreas@63243
  2382
    with * False have "r = 1 \<or> weight_spmf p = 1" by(simp add: max_def min_def not_le split: if_split_asm)
Andreas@63243
  2383
    with \<open>r \<ge> 1\<close> show ?thesis by simp
Andreas@63243
  2384
  qed simp
Andreas@63243
  2385
qed(auto intro!: spmf_eqI simp add: spmf_scale_spmf, metis pmf_le_0_iff spmf_le_weight)
Andreas@63243
  2386
Andreas@63243
  2387
lemma map_const_spmf_of_set:
Andreas@63243
  2388
  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> map_spmf (\<lambda>_. c) (spmf_of_set A) = return_spmf c"
Andreas@63243
  2389
by(simp add: map_spmf_conv_bind_spmf bind_spmf_const)
Andreas@63243
  2390
wenzelm@63308
  2391
subsection \<open>Conditional spmfs\<close>
Andreas@63243
  2392
Andreas@63243
  2393
lemma set_pmf_Int_Some: "set_pmf p \<inter> Some ` A = {} \<longleftrightarrow> set_spmf p \<inter> A = {}"