src/HOL/Probability/Independent_Family.thy
 changeset 61808 fc1556774cfe parent 61359 e985b52c3eb3 child 62343 24106dc44def
```     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Mon Dec 07 16:48:10 2015 +0000
1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Mon Dec 07 20:19:59 2015 +0100
1.3 @@ -3,7 +3,7 @@
1.4      Author:     Sudeep Kanav, TU München
1.5  *)
1.6
1.7 -section {* Independent families of events, event sets, and random variables *}
1.8 +section \<open>Independent families of events, event sets, and random variables\<close>
1.9
1.10  theory Independent_Family
1.11    imports Probability_Measure Infinite_Product_Measure
1.12 @@ -101,7 +101,7 @@
1.13    fix F J assume "J \<noteq> {}" "J \<subseteq> UNIV"
1.14      and F: "\<forall>j\<in>J. F j \<in> (case j of True \<Rightarrow> A | False \<Rightarrow> B)"
1.15    have "J \<in> Pow UNIV" by auto
1.16 -  with F `J \<noteq> {}` indep[of "F True" "F False"]
1.17 +  with F \<open>J \<noteq> {}\<close> indep[of "F True" "F False"]
1.18    show "prob (\<Inter>j\<in>J. F j) = (\<Prod>j\<in>J. prob (F j))"
1.19      unfolding UNIV_bool Pow_insert by (auto simp: ac_simps)
1.20  qed (auto split: bool.split simp: ev)
1.21 @@ -155,19 +155,19 @@
1.22              next
1.23                assume "J \<noteq> {j}"
1.24                have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)"
1.25 -                using `j \<in> J` `A j = X` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.26 +                using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.27                also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))"
1.28                proof (rule indep)
1.29                  show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}"
1.30 -                  using J `J \<noteq> {j}` `j \<in> J` by auto
1.31 +                  using J \<open>J \<noteq> {j}\<close> \<open>j \<in> J\<close> by auto
1.32                  show "\<forall>i\<in>J - {j}. A i \<in> G i"
1.33                    using J by auto
1.34                qed
1.35                also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))"
1.36 -                using `A j = X` by simp
1.37 +                using \<open>A j = X\<close> by simp
1.38                also have "\<dots> = (\<Prod>i\<in>J. prob (A i))"
1.39 -                unfolding setprod.insert_remove[OF `finite J`, symmetric, of "\<lambda>i. prob  (A i)"]
1.40 -                using `j \<in> J` by (simp add: insert_absorb)
1.41 +                unfolding setprod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob  (A i)"]
1.42 +                using \<open>j \<in> J\<close> by (simp add: insert_absorb)
1.43                finally show ?thesis .
1.44              qed
1.45            next
1.46 @@ -191,23 +191,23 @@
1.47              using G by auto
1.48            have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
1.49                prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
1.50 -            using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}`
1.51 +            using A_sets sets.sets_into_space[of _ M] X \<open>J \<noteq> {}\<close>
1.52              by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.53            also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
1.54 -            using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space
1.55 +            using J \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> A_sets X sets.sets_into_space
1.56              by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
1.57            finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
1.58                prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
1.59            moreover {
1.60              have "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))"
1.61 -              using J A `finite J` by (intro indep_setsD[OF G(1)]) auto
1.62 +              using J A \<open>finite J\<close> by (intro indep_setsD[OF G(1)]) auto
1.63              then have "prob (\<Inter>j\<in>J. A j) = prob (space M) * (\<Prod>i\<in>J. prob (A i))"
1.64                using prob_space by simp }
1.65            moreover {
1.66              have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))"
1.67 -              using J A `j \<in> K` by (intro indep_setsD[OF G']) auto
1.68 +              using J A \<open>j \<in> K\<close> by (intro indep_setsD[OF G']) auto
1.69              then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))"
1.70 -              using `finite J` `j \<notin> J` by (auto intro!: setprod.cong) }
1.71 +              using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: setprod.cong) }
1.72            ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = (prob (space M) - prob X) * (\<Prod>i\<in>J. prob (A i))"
1.74            also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))"
1.75 @@ -223,19 +223,19 @@
1.76            then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
1.77              using G by auto
1.78            have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
1.79 -            using `J \<noteq> {}` `j \<notin> J` `j \<in> K` by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.80 +            using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
1.81            moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
1.82            proof (rule finite_measure_UNION)
1.83              show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
1.84                using disj by (rule disjoint_family_on_bisimulation) auto
1.85              show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
1.86 -              using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: sets.Int)
1.87 +              using A_sets F \<open>finite J\<close> \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> by (auto intro!: sets.Int)
1.88            qed
1.89            moreover { fix k
1.90 -            from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
1.91 +            from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
1.92                by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: split_if_asm)
1.93              also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
1.94 -              using J A `j \<in> K` by (subst indep_setsD[OF G(1)]) auto
1.95 +              using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto
1.96              finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
1.97            ultimately have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)))"
1.98              by simp
1.99 @@ -243,7 +243,7 @@
1.100            have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * prob (\<Inter>i\<in>J. A i))"
1.101              using disj F(1) by (intro finite_measure_UNION sums_mult2) auto
1.102            then have "(\<lambda>k. prob (F k) * prob (\<Inter>i\<in>J. A i)) sums (prob (\<Union>k. F k) * (\<Prod>i\<in>J. prob (A i)))"
1.103 -            using J A `j \<in> K` by (subst indep_setsD[OF G(1), symmetric]) auto
1.104 +            using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1), symmetric]) auto
1.105            ultimately
1.106            show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
1.107              by (auto dest!: sums_unique)
1.108 @@ -252,10 +252,10 @@
1.109        then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
1.110        proof (rule dynkin_system.dynkin_subset, safe)
1.111          fix X assume "X \<in> G j"
1.112 -        then show "X \<in> events" using G `j \<in> K` by auto
1.113 -        from `indep_sets G K`
1.114 +        then show "X \<in> events" using G \<open>j \<in> K\<close> by auto
1.115 +        from \<open>indep_sets G K\<close>
1.116          show "indep_sets (G(j := {X})) K"
1.117 -          by (rule indep_sets_mono_sets) (insert `X \<in> G j`, auto)
1.118 +          by (rule indep_sets_mono_sets) (insert \<open>X \<in> G j\<close>, auto)
1.119        qed
1.120        have "indep_sets (G(j:=?D)) K"
1.121        proof (rule indep_setsI)
1.122 @@ -279,9 +279,9 @@
1.123        then have "indep_sets (G(j := dynkin (space M) (G j))) K"
1.124          by (rule indep_sets_mono_sets) (insert mono, auto)
1.125        then show ?case
1.126 -        by (rule indep_sets_mono_sets) (insert `j \<in> K` `j \<notin> J`, auto simp: G_def)
1.127 -    qed (insert `indep_sets F K`, simp) }
1.128 -  from this[OF `indep_sets F J` `finite J` subset_refl]
1.129 +        by (rule indep_sets_mono_sets) (insert \<open>j \<in> K\<close> \<open>j \<notin> J\<close>, auto simp: G_def)
1.130 +    qed (insert \<open>indep_sets F K\<close>, simp) }
1.131 +  from this[OF \<open>indep_sets F J\<close> \<open>finite J\<close> subset_refl]
1.132    show "indep_sets ?F J"
1.133      by (rule indep_sets_mono_sets) auto
1.134  qed
1.135 @@ -375,7 +375,7 @@
1.136    have "indep_sets (\<lambda>i. sigma_sets (space M) (case i of True \<Rightarrow> A | False \<Rightarrow> B)) UNIV"
1.137    proof (rule indep_sets_sigma)
1.138      show "indep_sets (case_bool A B) UNIV"
1.139 -      by (rule `indep_set A B`[unfolded indep_set_def])
1.140 +      by (rule \<open>indep_set A B\<close>[unfolded indep_set_def])
1.141      fix i show "Int_stable (case i of True \<Rightarrow> A | False \<Rightarrow> B)"
1.142        using A B by (cases i) auto
1.143    qed
1.144 @@ -398,7 +398,7 @@
1.145      then have "{{x \<in> space M. P i (X i x)}} = {X i -` {x\<in>space (N i). P i x} \<inter> space M}"
1.146        using indep by (auto simp: indep_vars_def dest: measurable_space)
1.147      also have "\<dots> \<subseteq> {X i -` A \<inter> space M |A. A \<in> sets (N i)}"
1.148 -      using P[OF `i \<in> I`] by blast
1.149 +      using P[OF \<open>i \<in> I\<close>] by blast
1.150      finally show "{{x \<in> space M. P i (X i x)}} \<subseteq> {X i -` A \<inter> space M |A. A \<in> sets (N i)}" .
1.151    qed
1.152  qed
1.153 @@ -457,10 +457,10 @@
1.154          have "k = j"
1.155          proof (rule ccontr)
1.156            assume "k \<noteq> j"
1.157 -          with disjoint `K \<subseteq> J` `k \<in> K` `j \<in> K` have "I k \<inter> I j = {}"
1.158 +          with disjoint \<open>K \<subseteq> J\<close> \<open>k \<in> K\<close> \<open>j \<in> K\<close> have "I k \<inter> I j = {}"
1.159              unfolding disjoint_family_on_def by auto
1.160 -          with L(2,3)[OF `j \<in> K`] L(2,3)[OF `k \<in> K`]
1.161 -          show False using `l \<in> L k` `l \<in> L j` by auto
1.162 +          with L(2,3)[OF \<open>j \<in> K\<close>] L(2,3)[OF \<open>k \<in> K\<close>]
1.163 +          show False using \<open>l \<in> L k\<close> \<open>l \<in> L j\<close> by auto
1.164          qed }
1.165        note L_inj = this
1.166
1.167 @@ -494,7 +494,7 @@
1.168        let ?A = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
1.169        have "a \<inter> b = INTER (Ka \<union> Kb) ?A"
1.170          by (simp add: a b set_eq_iff) auto
1.171 -      with a b `j \<in> J` Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j"
1.172 +      with a b \<open>j \<in> J\<close> Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j"
1.173          by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?A]) auto
1.174      qed
1.175    qed
1.176 @@ -536,10 +536,10 @@
1.177          { interpret sigma_algebra "space M" "?UN j"
1.178              by (rule sigma_algebra_sigma_sets) auto
1.179            have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> INTER J A \<in> ?UN j"
1.180 -            using `finite J` `J \<noteq> {}` by (rule finite_INT) blast }
1.181 +            using \<open>finite J\<close> \<open>J \<noteq> {}\<close> by (rule finite_INT) blast }
1.182          note INT = this
1.183
1.184 -        from `J \<noteq> {}` J K E[rule_format, THEN sets.sets_into_space] j
1.185 +        from \<open>J \<noteq> {}\<close> J K E[rule_format, THEN sets.sets_into_space] j
1.186          have "(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \<inter> space M
1.187            = (\<Inter>i\<in>J. X i -` E i \<inter> space M)"
1.188            apply (subst prod_emb_PiE[OF _ ])
1.189 @@ -552,7 +552,7 @@
1.190          also have "\<dots> \<in> ?UN j"
1.191            apply (rule INT)
1.192            apply (rule sigma_sets.Basic)
1.193 -          using `J \<subseteq> K j` E
1.194 +          using \<open>J \<subseteq> K j\<close> E
1.195            apply auto
1.196            done
1.197          finally show ?thesis .
1.198 @@ -630,7 +630,7 @@
1.199      from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
1.200      then have "X \<subseteq> space M"
1.201        by induct (insert A.sets_into_space, auto)
1.202 -    with `x \<in> X` show "x \<in> space M" by auto }
1.203 +    with \<open>x \<in> X\<close> show "x \<in> space M" by auto }
1.204    { fix F :: "nat \<Rightarrow> 'a set" and n assume "range F \<subseteq> ?A"
1.205      then show "(UNION UNIV F) \<in> sigma_sets (space M) (UNION {n..} A)"
1.206        by (intro sigma_sets.Union) auto }
1.207 @@ -661,11 +661,11 @@
1.208        using sets.sets_into_space by auto
1.209    next
1.210      show "space M \<in> ?D"
1.211 -      using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2)
1.212 +      using prob_space \<open>X \<subseteq> space M\<close> by (simp add: Int_absorb2)
1.213    next
1.214      fix A assume A: "A \<in> ?D"
1.215      have "prob (X \<inter> (space M - A)) = prob (X - (X \<inter> A))"
1.216 -      using `X \<subseteq> space M` by (auto intro!: arg_cong[where f=prob])
1.217 +      using \<open>X \<subseteq> space M\<close> by (auto intro!: arg_cong[where f=prob])
1.218      also have "\<dots> = prob X - prob (X \<inter> A)"
1.219        using X_in A by (intro finite_measure_Diff) auto
1.220      also have "\<dots> = prob X * prob (space M) - prob X * prob A"
1.221 @@ -674,7 +674,7 @@
1.222        using X_in A sets.sets_into_space
1.223        by (subst finite_measure_Diff) (auto simp: field_simps)
1.224      finally show "space M - A \<in> ?D"
1.225 -      using A `X \<subseteq> space M` by auto
1.226 +      using A \<open>X \<subseteq> space M\<close> by auto
1.227    next
1.228      fix F :: "nat \<Rightarrow> 'a set" assume dis: "disjoint_family F" and "range F \<subseteq> ?D"
1.229      then have F: "range F \<subseteq> events" "\<And>i. prob (X \<inter> F i) = prob X * prob (F i)"
1.230 @@ -726,7 +726,7 @@
1.231    then have "(\<Union>n. sigma_sets (space M) (\<Union>m\<in>{..n}. A m)) \<subseteq> ?D" (is "?A \<subseteq> _")
1.232      by auto
1.233
1.234 -  note `X \<in> tail_events A`
1.235 +  note \<open>X \<in> tail_events A\<close>
1.236    also {
1.237      have "\<And>n. sigma_sets (space M) (\<Union>i\<in>{n..}. A i) \<subseteq> sigma_sets (space M) ?A"
1.238        by (intro sigma_sets_subseteq UN_mono) auto
1.239 @@ -757,7 +757,7 @@
1.240      qed
1.241    qed
1.242    also have "dynkin (space M) ?A \<subseteq> ?D"
1.243 -    using `?A \<subseteq> ?D` by (auto intro!: D.dynkin_subset)
1.244 +    using \<open>?A \<subseteq> ?D\<close> by (auto intro!: D.dynkin_subset)
1.245    finally show ?thesis by auto
1.246  qed
1.247
1.248 @@ -838,8 +838,8 @@
1.249      with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))"
1.250        by auto
1.251      also have "\<dots> = (\<Prod>j\<in>J. prob (A j))"
1.252 -      unfolding if_distrib setprod.If_cases[OF `finite I`]
1.253 -      using prob_space `J \<subseteq> I` by (simp add: Int_absorb1 setprod.neutral_const)
1.254 +      unfolding if_distrib setprod.If_cases[OF \<open>finite I\<close>]
1.255 +      using prob_space \<open>J \<subseteq> I\<close> by (simp add: Int_absorb1 setprod.neutral_const)
1.256      finally show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" ..
1.257    qed
1.258  qed
1.259 @@ -858,10 +858,10 @@
1.260      unfolding measurable_def by simp
1.261
1.262    { fix i assume "i\<in>I"
1.263 -    from closed[OF `i \<in> I`]
1.264 +    from closed[OF \<open>i \<in> I\<close>]
1.265      have "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}
1.266        = sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> E i}"
1.267 -      unfolding sigma_sets_vimage_commute[OF X, OF `i \<in> I`, symmetric] M'[OF `i \<in> I`]
1.268 +      unfolding sigma_sets_vimage_commute[OF X, OF \<open>i \<in> I\<close>, symmetric] M'[OF \<open>i \<in> I\<close>]
1.269        by (subst sigma_sets_sigma_sets_eq) auto }
1.270    note sigma_sets_X = this
1.271
1.272 @@ -875,7 +875,7 @@
1.273        then obtain B where "b = X i -` B \<inter> space M" "B \<in> E i" by auto
1.274        moreover
1.275        have "(X i -` A \<inter> space M) \<inter> (X i -` B \<inter> space M) = X i -` (A \<inter> B) \<inter> space M" by auto
1.276 -      moreover note Int_stable[OF `i \<in> I`]
1.277 +      moreover note Int_stable[OF \<open>i \<in> I\<close>]
1.278        ultimately
1.279        show "a \<inter> b \<in> {X i -` A \<inter> space M |A. A \<in> E i}"
1.280          by (auto simp del: vimage_Int intro!: exI[of _ "A \<inter> B"] dest: Int_stableD)
1.281 @@ -884,12 +884,12 @@
1.282
1.283    { fix i assume "i \<in> I"
1.284      { fix A assume "A \<in> E i"
1.285 -      with M'[OF `i \<in> I`] have "A \<in> sets (M' i)" by auto
1.286 +      with M'[OF \<open>i \<in> I\<close>] have "A \<in> sets (M' i)" by auto
1.287        moreover
1.288 -      from rv[OF `i\<in>I`] have "X i \<in> measurable M (M' i)" by auto
1.289 +      from rv[OF \<open>i\<in>I\<close>] have "X i \<in> measurable M (M' i)" by auto
1.290        ultimately
1.291        have "X i -` A \<inter> space M \<in> sets M" by (auto intro: measurable_sets) }
1.292 -    with X[OF `i\<in>I`] space[OF `i\<in>I`]
1.293 +    with X[OF \<open>i\<in>I\<close>] space[OF \<open>i\<in>I\<close>]
1.294      have "{X i -` A \<inter> space M |A. A \<in> E i} \<subseteq> events"
1.295        "space M \<in> {X i -` A \<inter> space M |A. A \<in> E i}"
1.296        by (auto intro!: exI[of _ "space (M' i)"]) }
1.297 @@ -900,7 +900,7 @@
1.298      (is "?L = ?R")
1.299    proof safe
1.300      fix A assume ?L and A: "A \<in> (\<Pi> i\<in>I. E i)"
1.301 -    from `?L`[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A `I \<noteq> {}`
1.302 +    from \<open>?L\<close>[THEN bspec, of "\<lambda>i. X i -` A i \<inter> space M"] A \<open>I \<noteq> {}\<close>
1.303      show "prob ((\<Inter>j\<in>I. X j -` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x -` A x \<inter> space M))"
1.304        by (auto simp add: Pi_iff)
1.305    next
1.306 @@ -908,11 +908,11 @@
1.307      from A have "\<forall>i\<in>I. \<exists>B. A i = X i -` B \<inter> space M \<and> B \<in> E i" by auto
1.308      from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M"
1.309        "B \<in> (\<Pi> i\<in>I. E i)" by auto
1.310 -    from `?R`[THEN bspec, OF B(2)] B(1) `I \<noteq> {}`
1.311 +    from \<open>?R\<close>[THEN bspec, OF B(2)] B(1) \<open>I \<noteq> {}\<close>
1.312      show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))"
1.313        by simp
1.314    qed
1.315 -  then show ?thesis using `I \<noteq> {}`
1.316 +  then show ?thesis using \<open>I \<noteq> {}\<close>
1.317      by (simp add: rv indep_vars_def indep_sets_X sigma_sets_X indep_sets_finite_X cong: indep_sets_cong)
1.318  qed
1.319
1.320 @@ -922,21 +922,21 @@
1.321    shows "indep_vars N (\<lambda>i. Y i \<circ> X i) I"
1.322    unfolding indep_vars_def
1.323  proof
1.324 -  from rv `indep_vars M' X I`
1.325 +  from rv \<open>indep_vars M' X I\<close>
1.326    show "\<forall>i\<in>I. random_variable (N i) (Y i \<circ> X i)"
1.327      by (auto simp: indep_vars_def)
1.328
1.329    have "indep_sets (\<lambda>i. sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
1.330 -    using `indep_vars M' X I` by (simp add: indep_vars_def)
1.331 +    using \<open>indep_vars M' X I\<close> by (simp add: indep_vars_def)
1.332    then show "indep_sets (\<lambda>i. sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)}) I"
1.333    proof (rule indep_sets_mono_sets)
1.334      fix i assume "i \<in> I"
1.335 -    with `indep_vars M' X I` have X: "X i \<in> space M \<rightarrow> space (M' i)"
1.336 +    with \<open>indep_vars M' X I\<close> have X: "X i \<in> space M \<rightarrow> space (M' i)"
1.337        unfolding indep_vars_def measurable_def by auto
1.338      { fix A assume "A \<in> sets (N i)"
1.339        then have "\<exists>B. (Y i \<circ> X i) -` A \<inter> space M = X i -` B \<inter> space M \<and> B \<in> sets (M' i)"
1.340          by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
1.341 -           (auto simp: vimage_comp intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
1.342 +           (auto simp: vimage_comp intro!: measurable_sets rv \<open>i \<in> I\<close> funcset_mem[OF X]) }
1.343      then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
1.344        sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
1.345        by (intro sigma_sets_subseteq) (auto simp: vimage_comp)
1.346 @@ -1078,9 +1078,9 @@
1.347        then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
1.348          by (simp add: emeasure_distr X)
1.349        also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
1.350 -        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
1.351 +        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
1.352        also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
1.353 -        using `indep_vars M' X I` J `I \<noteq> {}` using indep_varsD[of M' X I J]
1.354 +        using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J]
1.355          by (auto simp: emeasure_eq_measure setprod_ereal)
1.356        also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))"
1.357          using rv J by (simp add: emeasure_distr)
1.358 @@ -1109,13 +1109,13 @@
1.359          Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
1.360        let ?E = "prod_emb I M' J (Pi\<^sub>E J Y)"
1.361        from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
1.362 -        using J `I \<noteq> {}` measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
1.363 +        using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
1.364        then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
1.365          by simp
1.366        also have "\<dots> = emeasure ?D ?E"
1.367          using Y  J by (intro emeasure_distr[symmetric] X sets_PiM_I) auto
1.368        also have "\<dots> = emeasure ?P' ?E"
1.369 -        using `?D = ?P'` by simp
1.370 +        using \<open>?D = ?P'\<close> by simp
1.371        also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))"
1.372          using P.emeasure_PiM_emb[of J Y] J Y by (simp add: prod_emb_def)
1.373        also have "\<dots> = (\<Prod> i\<in>J. emeasure M (Y' i))"
1.374 @@ -1191,7 +1191,7 @@
1.375      have "emeasure ?J (A \<times> B) = emeasure M ((\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M)"
1.376        using A B by (intro emeasure_distr[OF XY]) auto
1.377      also have "\<dots> = emeasure M (X -` A \<inter> space M) * emeasure M (Y -` B \<inter> space M)"
1.378 -      using indep_varD[OF `indep_var S X T Y`, of A B] A B by (simp add: emeasure_eq_measure)
1.379 +      using indep_varD[OF \<open>indep_var S X T Y\<close>, of A B] A B by (simp add: emeasure_eq_measure)
1.380      also have "\<dots> = emeasure ?S A * emeasure ?T B"
1.381        using rvs A B by (simp add: emeasure_distr)
1.382      finally show "emeasure ?S A * emeasure ?T B = emeasure ?J (A \<times> B)" by simp
1.383 @@ -1222,15 +1222,15 @@
1.384      show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}"
1.385      proof (safe intro!: indep_setI)
1.386        { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M"
1.387 -        using `X \<in> measurable M S` by (auto intro: measurable_sets) }
1.388 +        using \<open>X \<in> measurable M S\<close> by (auto intro: measurable_sets) }
1.389        { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M"
1.390 -        using `Y \<in> measurable M T` by (auto intro: measurable_sets) }
1.391 +        using \<open>Y \<in> measurable M T\<close> by (auto intro: measurable_sets) }
1.392      next
1.393        fix A B assume ab: "A \<in> sets S" "B \<in> sets T"
1.394        then have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) = emeasure ?J (A \<times> B)"
1.395          using XY by (auto simp add: emeasure_distr emeasure_eq_measure intro!: arg_cong[where f="prob"])
1.396        also have "\<dots> = emeasure (?S \<Otimes>\<^sub>M ?T) (A \<times> B)"
1.397 -        unfolding `?S \<Otimes>\<^sub>M ?T = ?J` ..
1.398 +        unfolding \<open>?S \<Otimes>\<^sub>M ?T = ?J\<close> ..
1.399        also have "\<dots> = emeasure ?S A * emeasure ?T B"
1.400          using ab by (simp add: Y.emeasure_pair_measure_Times)
1.401        finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =
1.402 @@ -1275,9 +1275,9 @@
1.403    also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
1.404      by (subst nn_integral_distr) auto
1.405    also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
1.406 -    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
1.407 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] ..
1.408    also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. max 0 \<omega> \<partial>distr M borel (Y i)))"
1.409 -    by (rule product_nn_integral_setprod) (auto intro: `finite I`)
1.410 +    by (rule product_nn_integral_setprod) (auto intro: \<open>finite I\<close>)
1.411    also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
1.412      by (intro setprod.cong nn_integral_cong)
1.413         (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X)
1.414 @@ -1317,17 +1317,17 @@
1.415    also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
1.416      by (subst integral_distr) auto
1.417    also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
1.418 -    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
1.419 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] ..
1.420    also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))"
1.421 -    by (rule product_integral_setprod) (auto intro: `finite I` simp: integrable_distr_eq int_Y)
1.422 +    by (rule product_integral_setprod) (auto intro: \<open>finite I\<close> simp: integrable_distr_eq int_Y)
1.423    also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)"
1.424      by (intro setprod.cong integral_cong)
1.425         (auto simp: integral_distr Y_def rv_X)
1.426    finally show ?eq .
1.427
1.428    have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))"
1.429 -    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y]
1.430 -    by (intro product_integrable_setprod[OF `finite I`])
1.431 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y]
1.432 +    by (intro product_integrable_setprod[OF \<open>finite I\<close>])