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.73              by (simp add: field_simps)
    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>])
   1.433         (simp add: integrable_distr_eq int_Y)
   1.434    then show ?int
   1.435      by (simp add: integrable_distr_eq Y_def)