src/HOL/Probability/SPMF.thy
changeset 63333 158ab2239496
parent 63308 d49580620ecb
child 63343 fb5d8a50c641
     1.1 --- a/src/HOL/Probability/SPMF.thy	Wed Jun 15 22:19:03 2016 +0200
     1.2 +++ b/src/HOL/Probability/SPMF.thy	Thu Jun 16 23:03:27 2016 +0200
     1.3 @@ -302,7 +302,7 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -lemma integral_measure_spmf: 
     1.8 +lemma integral_measure_spmf:
     1.9    assumes "integrable (measure_spmf p) f"
    1.10    shows "(\<integral> x. f x \<partial>measure_spmf p) = \<integral> x. spmf p x * f x \<partial>count_space UNIV"
    1.11  proof -
    1.12 @@ -340,7 +340,7 @@
    1.13  proof(rule neq_top_trans)
    1.14    show "(SUP i. ennreal (spmf (Y i) x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
    1.15  qed simp
    1.16 -                 
    1.17 +
    1.18  lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
    1.19  proof(rule neq_top_trans)
    1.20    show "(SUP p:Y. emeasure (measure_spmf p) A) \<le> 1"
    1.21 @@ -453,7 +453,7 @@
    1.22  
    1.23  lemma set_map_spmf [simp]: "set_spmf (map_spmf f p) = f ` set_spmf p"
    1.24  by(simp add: set_spmf_def image_bind bind_image o_def Option.option.set_map)
    1.25 -        
    1.26 +
    1.27  lemma map_spmf_cong:
    1.28    "\<lbrakk> p = q; \<And>x. x \<in> set_spmf q \<Longrightarrow> f x = g x \<rbrakk>
    1.29    \<Longrightarrow> map_spmf f p = map_spmf g q"
    1.30 @@ -576,7 +576,7 @@
    1.31      by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf)
    1.32  next
    1.33    fix A :: "'a set"
    1.34 -  have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_pmf p" 
    1.35 +  have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_pmf p"
    1.36      by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
    1.37    also have "\<dots> = emeasure ?rhs A"
    1.38      by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
    1.39 @@ -591,13 +591,13 @@
    1.40  next
    1.41    fix A :: "'a set"
    1.42    let ?A = "the -` A \<inter> range Some"
    1.43 -  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" 
    1.44 +  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"
    1.45      by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
    1.46    also have "\<dots> =  \<integral>\<^sup>+ x. emeasure (measure_pmf (f (the x))) ?A * indicator (range Some) x \<partial>measure_pmf p"
    1.47      by(rule nn_integral_cong)(auto split: option.split simp add: indicator_def)
    1.48    also have "\<dots> = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_spmf p"
    1.49      by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space emeasure_distr space_restrict_space emeasure_restrict_space)
    1.50 -  also have "\<dots> = emeasure ?rhs A" 
    1.51 +  also have "\<dots> = emeasure ?rhs A"
    1.52      by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
    1.53    finally show "emeasure ?lhs A = emeasure ?rhs A" .
    1.54  qed
    1.55 @@ -663,7 +663,7 @@
    1.56  
    1.57  lemma rel_spmf_mono:
    1.58    "\<lbrakk>rel_spmf A f g; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_spmf B f g"
    1.59 -apply(erule rel_pmf_mono) 
    1.60 +apply(erule rel_pmf_mono)
    1.61  using option.rel_mono[of A B] by(simp add: le_fun_def)
    1.62  
    1.63  lemma rel_spmf_mono_strong:
    1.64 @@ -684,7 +684,7 @@
    1.65  
    1.66  lemma rel_spmfE [elim?, consumes 1, case_names rel_spmf]:
    1.67    assumes "rel_spmf P p q"
    1.68 -  obtains pq where 
    1.69 +  obtains pq where
    1.70      "\<And>x y. (x, y) \<in> set_spmf pq \<Longrightarrow> P x y"
    1.71      "p = map_spmf fst pq"
    1.72      "q = map_spmf snd pq"
    1.73 @@ -847,7 +847,7 @@
    1.74  lemma weight_spmf_nonneg: "weight_spmf p \<ge> 0"
    1.75  by(fact measure_nonneg)
    1.76  
    1.77 -lemma (in finite_measure) integrable_weight_spmf [simp]: 
    1.78 +lemma (in finite_measure) integrable_weight_spmf [simp]:
    1.79    "(\<lambda>x. weight_spmf (f x)) \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. weight_spmf (f x))"
    1.80  by(rule integrable_const_bound[where B=1])(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
    1.81  
    1.82 @@ -1068,7 +1068,7 @@
    1.83    and refl: "\<And>x. x \<in> set_spmf p \<Longrightarrow> R x x"
    1.84    shows "ord_spmf R p q"
    1.85  proof(rule rel_pmf.intros)
    1.86 -  define pq where "pq = embed_pmf 
    1.87 +  define pq where "pq = embed_pmf
    1.88      (\<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)
    1.89        | None \<Rightarrow> (case y of None \<Rightarrow> pmf q None | Some y' \<Rightarrow> spmf q y' - spmf p y'))"
    1.90       (is "_ = embed_pmf ?f")
    1.91 @@ -1077,8 +1077,8 @@
    1.92    have integral: "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) = 1" (is "nn_integral ?M _ = _")
    1.93    proof -
    1.94      have "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) =
    1.95 -      \<integral>\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy + 
    1.96 -             ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy + 
    1.97 +      \<integral>\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy +
    1.98 +             ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy +
    1.99               ennreal (?f xy) * indicator (range (\<lambda>x. (Some x, Some x))) xy \<partial>?M"
   1.100        by(rule nn_integral_cong)(auto split: split_indicator option.splits if_split_asm)
   1.101      also have "\<dots> = (\<integral>\<^sup>+ xy. ?f xy * indicator {(None, None)} xy \<partial>?M) +
   1.102 @@ -1132,8 +1132,8 @@
   1.103        then show ?thesis using Some by simp
   1.104      next
   1.105        case None
   1.106 -      have "(\<integral>\<^sup>+ y. pmf pq (None, y) \<partial>count_space UNIV) = 
   1.107 -            (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y + 
   1.108 +      have "(\<integral>\<^sup>+ y. pmf pq (None, y) \<partial>count_space UNIV) =
   1.109 +            (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y +
   1.110                     ennreal (pmf pq (None, None)) * indicator {None} y \<partial>count_space UNIV)"
   1.111          by(rule nn_integral_cong)(auto split: split_indicator)
   1.112        also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) \<partial>count_space (range Some)) + pmf pq (None, None)"
   1.113 @@ -1170,8 +1170,8 @@
   1.114        then show ?thesis using None by simp
   1.115      next
   1.116        case (Some y)
   1.117 -      have "(\<integral>\<^sup>+ x. pmf pq (x, Some y) \<partial>count_space UNIV) = 
   1.118 -        (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x + 
   1.119 +      have "(\<integral>\<^sup>+ x. pmf pq (x, Some y) \<partial>count_space UNIV) =
   1.120 +        (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x +
   1.121                 ennreal (pmf pq (None, Some y)) * indicator {None} x \<partial>count_space UNIV)"
   1.122          by(rule nn_integral_cong)(auto split: split_indicator)
   1.123        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)"
   1.124 @@ -1215,8 +1215,7 @@
   1.125  by(auto intro!: nn_integral_mono split: split_indicator dest: ord_spmf_eq_leD simp add: nn_integral_measure_spmf nn_integral_indicator[symmetric])
   1.126  
   1.127  lemma ord_spmf_eqD_measure_spmf: "ord_spmf op = p q \<Longrightarrow> measure_spmf p \<le> measure_spmf q"
   1.128 -by(rule less_eq_measure.intros)(simp_all add: ord_spmf_eqD_emeasure)
   1.129 -
   1.130 +  by (subst le_measure) (auto simp: ord_spmf_eqD_emeasure)
   1.131  
   1.132  subsection \<open>CCPO structure for the flat ccpo @{term "ord_option op ="}\<close>
   1.133  
   1.134 @@ -1224,7 +1223,7 @@
   1.135  
   1.136  definition lub_spmf :: "'a spmf"
   1.137  where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
   1.138 -  \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close> 
   1.139 +  \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
   1.140  
   1.141  lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
   1.142  by(simp add: SPMF.lub_spmf_def bot_ereal_def)
   1.143 @@ -1259,18 +1258,18 @@
   1.144  proof(rule spmf_eqI)
   1.145    fix i
   1.146    from le have le': "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
   1.147 -  have "(\<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV) = 
   1.148 +  have "(\<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV) =
   1.149       (\<integral>\<^sup>+ x. spmf q x \<partial>count_space UNIV) - (\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV)"
   1.150      by(subst nn_integral_diff)(simp_all add: AE_count_space le' nn_integral_spmf_neq_top)
   1.151    also have "\<dots> = (1 - pmf q None) - (1 - pmf p None)" unfolding pmf_None_eq_weight_spmf
   1.152      by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus)
   1.153    also have "\<dots> = 0" using None by simp
   1.154 -  finally have "\<And>x. spmf q x \<le> spmf p x" 
   1.155 +  finally have "\<And>x. spmf q x \<le> spmf p x"
   1.156      by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff)
   1.157    with le' show "spmf p i = spmf q i" by(rule antisym)
   1.158  qed
   1.159  
   1.160 -lemma ord_spmf_eqD_pmf_None: 
   1.161 +lemma ord_spmf_eqD_pmf_None:
   1.162    assumes "ord_spmf op = x y"
   1.163    shows "pmf x None \<ge> pmf y None"
   1.164  using assms
   1.165 @@ -1283,7 +1282,7 @@
   1.166    Chains on @{typ "'a spmf"} maintain countable support.
   1.167    Thanks to Johannes Hölzl for the proof idea.
   1.168  \<close>
   1.169 -lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)" 
   1.170 +lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)"
   1.171  proof(cases "Y = {}")
   1.172    case Y: False
   1.173    show ?thesis
   1.174 @@ -1295,13 +1294,13 @@
   1.175    next
   1.176      case False
   1.177      define N :: "'a option pmf \<Rightarrow> real" where "N p = pmf p None" for p
   1.178 -  
   1.179 +
   1.180      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
   1.181        using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x]
   1.182        by (auto simp: N_def)
   1.183      have N_eq_imp_eq: "\<lbrakk> x \<in> Y; y \<in> Y; N y = N x \<rbrakk> \<Longrightarrow> x = y" for x y
   1.184        using chainD[OF chain, of x y] by(auto simp add: N_def dest: ord_spmf_eq_pmf_None_eq)
   1.185 -    
   1.186 +
   1.187      have NC: "N ` Y \<noteq> {}" "bdd_below (N ` Y)"
   1.188        using \<open>Y \<noteq> {}\<close> by(auto intro!: bdd_belowI[of _ 0] simp: N_def)
   1.189      have NC_less: "Inf (N ` Y) < N x" if "x \<in> Y" for x unfolding cInf_less_iff[OF NC]
   1.190 @@ -1314,12 +1313,12 @@
   1.191            by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) }
   1.192        with False \<open>x \<in> Y\<close> show False by blast
   1.193      qed
   1.194 -  
   1.195 +
   1.196      from NC have "Inf (N ` Y) \<in> closure (N ` Y)" by (intro closure_contains_Inf)
   1.197      then obtain X' where "\<And>n. X' n \<in> N ` Y" and X': "X' \<longlonglongrightarrow> Inf (N ` Y)"
   1.198        unfolding closure_sequential by auto
   1.199      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
   1.200 -  
   1.201 +
   1.202      with X' have seq: "(\<lambda>n. N (X n)) \<longlonglongrightarrow> Inf (N ` Y)" by simp
   1.203      have "(\<Union>x \<in> Y. set_spmf x) \<subseteq> (\<Union>n. set_spmf (X n))"
   1.204      proof(rule UN_least)
   1.205 @@ -1343,7 +1342,7 @@
   1.206    let ?B = "\<Union>p\<in>Y. set_spmf p"
   1.207    have countable: "countable ?B" by(rule spmf_chain_countable)
   1.208  
   1.209 -  have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) = 
   1.210 +  have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
   1.211          (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
   1.212      by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
   1.213    also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space ?B)"
   1.214 @@ -1481,8 +1480,10 @@
   1.215    from assms obtain p where p: "p \<in> Y" by auto
   1.216    from chain have chain': "Complete_Partial_Order.chain op \<le> (measure_spmf ` Y)"
   1.217      by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf)
   1.218 -  show "sets ?lhs = sets ?rhs" and "emeasure ?lhs A = emeasure ?rhs A" for A
   1.219 -    using chain' Y p by(simp_all add: sets_SUP emeasure_SUP emeasure_lub_spmf)
   1.220 +  show "sets ?lhs = sets ?rhs"
   1.221 +    using Y by (subst sets_SUP) auto
   1.222 +  show "emeasure ?lhs A = emeasure ?rhs A" for A
   1.223 +    using chain' Y p by (subst emeasure_SUP_chain) (auto simp:  emeasure_lub_spmf)
   1.224  qed
   1.225  
   1.226  end
   1.227 @@ -1552,11 +1553,11 @@
   1.228    ultimately show "ord_spmf op = (bind_spmf (B f) (\<lambda>y. C y f)) (bind_spmf (B g) (\<lambda>y'. C y' g))"
   1.229      by(rule bind_spmf_mono')
   1.230  qed
   1.231 -  
   1.232 +
   1.233  lemma monotone_bind_spmf1: "monotone (ord_spmf op =) (ord_spmf op =) (\<lambda>y. bind_spmf y g)"
   1.234  by(rule monotoneI)(simp add: bind_spmf_mono' ord_spmf_reflI)
   1.235  
   1.236 -lemma monotone_bind_spmf2: 
   1.237 +lemma monotone_bind_spmf2:
   1.238    assumes g: "\<And>x. monotone ord (ord_spmf op =) (\<lambda>y. g y x)"
   1.239    shows "monotone ord (ord_spmf op =) (\<lambda>y. bind_spmf p (g y))"
   1.240  by(rule monotoneI)(auto intro: bind_spmf_mono' monotoneD[OF g] ord_spmf_reflI)
   1.241 @@ -1611,7 +1612,7 @@
   1.242        using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono)
   1.243      have chain''': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
   1.244        using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
   1.245 -  
   1.246 +
   1.247      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)"
   1.248        by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
   1.249      also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
   1.250 @@ -1707,7 +1708,7 @@
   1.251  
   1.252  locale rel_spmf_characterisation =
   1.253    assumes rel_pmf_measureI:
   1.254 -    "\<And>(R :: 'a option \<Rightarrow> 'b option \<Rightarrow> bool) p q. 
   1.255 +    "\<And>(R :: 'a option \<Rightarrow> 'b option \<Rightarrow> bool) p q.
   1.256      (\<And>A. measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y})
   1.257      \<Longrightarrow> rel_pmf R p q"
   1.258    \<comment> \<open>This assumption is shown to hold in general in the AFP entry \<open>MFMC_Countable\<close>.\<close>
   1.259 @@ -1911,7 +1912,7 @@
   1.260  subsection \<open>Subprobability distributions of sets\<close>
   1.261  
   1.262  definition spmf_of_set :: "'a set \<Rightarrow> 'a spmf"
   1.263 -where 
   1.264 +where
   1.265    "spmf_of_set A = (if finite A \<and> A \<noteq> {} then spmf_of_pmf (pmf_of_set A) else return_pmf None)"
   1.266  
   1.267  lemma spmf_of_set: "spmf (spmf_of_set A) x = indicator A x / card A"
   1.268 @@ -1933,7 +1934,7 @@
   1.269    "inj_on f A \<Longrightarrow> map_spmf f (spmf_of_set A) = spmf_of_set (f ` A)"
   1.270  by(auto simp add: spmf_of_set_def map_pmf_of_set_inj dest: finite_imageD)
   1.271  
   1.272 -lemma spmf_of_pmf_pmf_of_set [simp]: 
   1.273 +lemma spmf_of_pmf_pmf_of_set [simp]:
   1.274    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> spmf_of_pmf (pmf_of_set A) = spmf_of_set A"
   1.275  by(simp add: spmf_of_set_def)
   1.276  
   1.277 @@ -2001,7 +2002,7 @@
   1.278  lemma rel_pmf_of_set_bij:
   1.279    assumes f: "bij_betw f A B"
   1.280    and A: "A \<noteq> {}" "finite A"
   1.281 -  and B: "B \<noteq> {}" "finite B" 
   1.282 +  and B: "B \<noteq> {}" "finite B"
   1.283    and R: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
   1.284    shows "rel_pmf R (pmf_of_set A) (pmf_of_set B)"
   1.285  proof(rule pmf.rel_mono_strong)
   1.286 @@ -2056,7 +2057,7 @@
   1.287      by(auto intro: arg_cong[where f=card])
   1.288    also have "\<dots> = (if i then card (B \<inter> A) / card B else (card B - card (B \<inter> A)) / card B)"
   1.289      by(auto simp add: card_Diff_subset_Int assms)
   1.290 -  also have "\<dots> = ennreal (spmf ?rhs i)"                               
   1.291 +  also have "\<dots> = ennreal (spmf ?rhs i)"
   1.292      by(simp add: assms card_gt_0_iff field_simps card_mono Int_commute of_nat_diff)
   1.293    finally show "spmf ?lhs i = spmf ?rhs i" by simp
   1.294  qed
   1.295 @@ -2233,7 +2234,7 @@
   1.296  apply(auto simp add: max_def min_def ennreal_mult[symmetric] not_le ennreal_lt_0)
   1.297  done
   1.298  
   1.299 -lemma measure_spmf_scale_spmf': 
   1.300 +lemma measure_spmf_scale_spmf':
   1.301    "r \<le> 1 \<Longrightarrow> measure_spmf (scale_spmf r p) = scale_measure r (measure_spmf p)"
   1.302  unfolding measure_spmf_scale_spmf
   1.303  apply(cases "weight_spmf p > 0")
   1.304 @@ -2250,7 +2251,7 @@
   1.305  lemma scale_spmf_0 [simp]: "scale_spmf 0 p = return_pmf None"
   1.306  by(rule spmf_eqI)(simp add: spmf_scale_spmf min_def max_def weight_spmf_le_0)
   1.307  
   1.308 -lemma bind_scale_spmf: 
   1.309 +lemma bind_scale_spmf:
   1.310    assumes r: "r \<le> 1"
   1.311    shows "bind_spmf (scale_spmf r p) f = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
   1.312    (is "?lhs = ?rhs")
   1.313 @@ -2262,7 +2263,7 @@
   1.314    thus "spmf ?lhs x = spmf ?rhs x" by simp
   1.315  qed
   1.316  
   1.317 -lemma scale_bind_spmf: 
   1.318 +lemma scale_bind_spmf:
   1.319    assumes "r \<le> 1"
   1.320    shows "scale_spmf r (bind_spmf p f) = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
   1.321    (is "?lhs = ?rhs")
   1.322 @@ -2298,7 +2299,7 @@
   1.323  lemma set_scale_spmf' [simp]: "0 < r \<Longrightarrow> set_spmf (scale_spmf r p) = set_spmf p"
   1.324  by(simp add: set_scale_spmf)
   1.325  
   1.326 -lemma rel_spmf_scaleI: 
   1.327 +lemma rel_spmf_scaleI:
   1.328    assumes "r > 0 \<Longrightarrow> rel_spmf A p q"
   1.329    shows "rel_spmf A (scale_spmf r p) (scale_spmf r q)"
   1.330  proof(cases "r > 0")
   1.331 @@ -2319,7 +2320,7 @@
   1.332    thus ?thesis by(auto simp add: min_def max_def ennreal_mult[symmetric] split: if_split_asm)
   1.333  qed
   1.334  
   1.335 -lemma weight_scale_spmf' [simp]: 
   1.336 +lemma weight_scale_spmf' [simp]:
   1.337    "\<lbrakk> 0 \<le> r; r \<le> 1 \<rbrakk> \<Longrightarrow> weight_spmf (scale_spmf r p) = r * weight_spmf p"
   1.338  by(simp add: weight_scale_spmf max_def min_def)(metis antisym_conv mult_left_le order_trans weight_spmf_le_1)
   1.339  
   1.340 @@ -2327,7 +2328,7 @@
   1.341    "pmf (scale_spmf k p) None = 1 - min 1 (max 0 k * (1 - pmf p None))"
   1.342  unfolding pmf_None_eq_weight_spmf by(simp add: weight_scale_spmf)
   1.343  
   1.344 -lemma scale_scale_spmf: 
   1.345 +lemma scale_scale_spmf:
   1.346    "scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
   1.347    (is "?lhs = ?rhs")
   1.348  proof(rule spmf_eqI)
   1.349 @@ -2432,7 +2433,7 @@
   1.350  
   1.351  lemma set_pair_spmf [simp]: "set_spmf (pair_spmf p q) = set_spmf p \<times> set_spmf q"
   1.352  by(auto 4 3 simp add: pair_spmf_def set_spmf_bind_pmf bind_UNION in_set_spmf intro: rev_bexI split: option.splits)
   1.353 -                                                 
   1.354 +
   1.355  lemma spmf_pair [simp]: "spmf (pair_spmf p q) (x, y) = spmf p x * spmf q y" (is "?lhs = ?rhs")
   1.356  proof -
   1.357    have "ennreal ?lhs = \<integral>\<^sup>+ a. \<integral>\<^sup>+ b. indicator {(x, y)} (a, b) \<partial>measure_spmf q \<partial>measure_spmf p"
   1.358 @@ -2483,8 +2484,8 @@
   1.359  by(simp add: pair_spmf_return_spmf1)
   1.360  
   1.361  lemma rel_pair_spmf_prod:
   1.362 -  "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \<longleftrightarrow> 
   1.363 -   rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \<and> 
   1.364 +  "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \<longleftrightarrow>
   1.365 +   rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \<and>
   1.366     rel_spmf B (scale_spmf (weight_spmf p) q) (scale_spmf (weight_spmf p') q')"
   1.367    (is "?lhs \<longleftrightarrow> ?rhs" is "_ \<longleftrightarrow> ?A \<and> ?B" is "_ \<longleftrightarrow> rel_spmf _ ?p ?p' \<and> rel_spmf _ ?q ?q'")
   1.368  proof(intro iffI conjI)
   1.369 @@ -2506,7 +2507,7 @@
   1.370      moreover have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) \<le> (1 * 1) * (1 * 1)"
   1.371        by(intro mult_mono)(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
   1.372      ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
   1.373 -    hence *: "weight_spmf p * weight_spmf q = 1" 
   1.374 +    hence *: "weight_spmf p * weight_spmf q = 1"
   1.375        by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
   1.376      hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
   1.377      moreover with * have "weight_spmf q = 1" by simp
   1.378 @@ -2526,7 +2527,7 @@
   1.379      have [simp]: "snd \<circ> ?f = map_prod snd snd" by(simp add: fun_eq_iff)
   1.380      from \<open>?rhs\<close> have eq: "weight_spmf p * weight_spmf q = weight_spmf p' * weight_spmf q'"
   1.381        by(auto dest!: rel_spmf_weightD simp add: weight_spmf_le_1 weight_spmf_nonneg)
   1.382 -    
   1.383 +
   1.384      have "map_spmf snd ?pq = scale_spmf ?r (pair_spmf ?p' ?q')"
   1.385        by(simp add: pair_map_spmf[symmetric] p' q' map_scale_spmf spmf.map_comp)
   1.386      also have "\<dots> = pair_spmf p' q'" using full[of p' q'] eq
   1.387 @@ -2546,24 +2547,24 @@
   1.388      let ?f = "(\<lambda>((x, y), (x', y')). (x, x'))"
   1.389      let ?pq = "map_spmf ?f pq"
   1.390      have [simp]: "fst \<circ> ?f = fst \<circ> fst" by(simp add: split_def o_def)
   1.391 -    show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq 
   1.392 +    show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq
   1.393        by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
   1.394  
   1.395      have [simp]: "snd \<circ> ?f = fst \<circ> snd" by(simp add: split_def o_def)
   1.396 -    show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq' 
   1.397 +    show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq'
   1.398        by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
   1.399    qed(auto dest: * )
   1.400 -    
   1.401 +
   1.402    show ?B
   1.403    proof
   1.404      let ?f = "(\<lambda>((x, y), (x', y')). (y, y'))"
   1.405      let ?pq = "map_spmf ?f pq"
   1.406      have [simp]: "fst \<circ> ?f = snd \<circ> fst" by(simp add: split_def o_def)
   1.407 -    show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq 
   1.408 +    show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq
   1.409        by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
   1.410  
   1.411      have [simp]: "snd \<circ> ?f = snd \<circ> snd" by(simp add: split_def o_def)
   1.412 -    show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq' 
   1.413 +    show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq'
   1.414        by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
   1.415    qed(auto dest: * )
   1.416  qed
   1.417 @@ -2650,7 +2651,7 @@
   1.418  lemma rel_spmf_try_spmf:
   1.419    "\<lbrakk> rel_spmf R p p'; \<not> lossless_spmf p' \<Longrightarrow> rel_spmf R q q' \<rbrakk>
   1.420    \<Longrightarrow> rel_spmf R (TRY p ELSE q) (TRY p' ELSE q')"
   1.421 -unfolding try_spmf_def 
   1.422 +unfolding try_spmf_def
   1.423  apply(rule rel_pmf_bindI[where R="\<lambda>x y. rel_option R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf p'"])
   1.424   apply(erule pmf.rel_mono_strong; simp)
   1.425  apply(auto split: option.split simp add: lossless_iff_set_pmf_None)