equal
deleted
inserted
replaced
1136 from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
1136 from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
1137 and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
1137 and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto |
1138 from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
1138 from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z" |
1139 and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
1139 and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto |
1140 |
1140 |
1141 def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))" |
1141 define pr where "pr = |
|
1142 bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) |
|
1143 (\<lambda>yz. return_pmf (fst xy, snd yz)))" |
1142 have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}" |
1144 have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}" |
1143 by (force simp: q') |
1145 by (force simp: q') |
1144 |
1146 |
1145 have "rel_pmf (R OO S) p r" |
1147 have "rel_pmf (R OO S) p r" |
1146 proof (rule rel_pmf.intros) |
1148 proof (rule rel_pmf.intros) |