1285 and fg: "\<And>x y. R x y \<Longrightarrow> rel_pmf P (f x) (g y)" |
1285 and fg: "\<And>x y. R x y \<Longrightarrow> rel_pmf P (f x) (g y)" |
1286 shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)" |
1286 shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)" |
1287 unfolding bind_pmf_def |
1287 unfolding bind_pmf_def |
1288 by(rule rel_pmf_joinI)(auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg) |
1288 by(rule rel_pmf_joinI)(auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg) |
1289 |
1289 |
|
1290 text {* |
|
1291 Proof that @{const rel_pmf} preserves orders. |
|
1292 Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, |
|
1293 Theoretical Computer Science 12(1):19--37, 1980, |
|
1294 @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"} |
|
1295 *} |
|
1296 |
|
1297 lemma |
|
1298 assumes *: "rel_pmf R p q" |
|
1299 and refl: "reflp R" and trans: "transp R" |
|
1300 shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1) |
|
1301 and measure_Ioi: "measure p {y. R x y \<and> \<not> R y x} \<le> measure q {y. R x y \<and> \<not> R y x}" (is ?thesis2) |
|
1302 proof - |
|
1303 from * obtain pq |
|
1304 where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y" |
|
1305 and p: "p = map_pmf fst pq" |
|
1306 and q: "q = map_pmf snd pq" |
|
1307 by cases auto |
|
1308 show ?thesis1 ?thesis2 unfolding p q map_pmf.rep_eq using refl trans |
|
1309 by(auto 4 3 simp add: measure_distr reflpD AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE dest!: pq elim: transpE) |
|
1310 qed |
|
1311 |
|
1312 lemma rel_pmf_inf: |
|
1313 fixes p q :: "'a pmf" |
|
1314 assumes 1: "rel_pmf R p q" |
|
1315 assumes 2: "rel_pmf R q p" |
|
1316 and refl: "reflp R" and trans: "transp R" |
|
1317 shows "rel_pmf (inf R R\<inverse>\<inverse>) p q" |
|
1318 proof |
|
1319 let ?E = "\<lambda>x. {y. R x y \<and> R y x}" |
|
1320 let ?\<mu>E = "\<lambda>x. measure q (?E x)" |
|
1321 { fix x |
|
1322 have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})" |
|
1323 by(auto intro!: arg_cong[where f="measure p"]) |
|
1324 also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}" |
|
1325 by (rule measure_pmf.finite_measure_Diff) auto |
|
1326 also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}" |
|
1327 using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi) |
|
1328 also have "measure p {y. R x y} = measure q {y. R x y}" |
|
1329 using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici) |
|
1330 also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} = |
|
1331 measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})" |
|
1332 by(rule measure_pmf.finite_measure_Diff[symmetric]) auto |
|
1333 also have "\<dots> = ?\<mu>E x" |
|
1334 by(auto intro!: arg_cong[where f="measure q"]) |
|
1335 also note calculation } |
|
1336 note eq = this |
|
1337 |
|
1338 def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))" |
|
1339 |
|
1340 show "map_pmf fst pq = p" |
|
1341 by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf') |
|
1342 |
|
1343 show "map_pmf snd pq = q" |
|
1344 unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv |
|
1345 by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq intro: transpD[OF \<open>transp R\<close>]) |
|
1346 |
|
1347 fix x y |
|
1348 assume "(x, y) \<in> set_pmf pq" |
|
1349 moreover |
|
1350 { assume "x \<in> set_pmf p" |
|
1351 hence "measure (measure_pmf p) (?E x) \<noteq> 0" |
|
1352 by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>]) |
|
1353 hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp |
|
1354 hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}" |
|
1355 by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) } |
|
1356 ultimately show "inf R R\<inverse>\<inverse> x y" |
|
1357 by(auto simp add: pq_def set_bind_pmf set_return_pmf set_cond_pmf) |
|
1358 qed |
|
1359 |
|
1360 lemma rel_pmf_antisym: |
|
1361 fixes p q :: "'a pmf" |
|
1362 assumes 1: "rel_pmf R p q" |
|
1363 assumes 2: "rel_pmf R q p" |
|
1364 and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R" |
|
1365 shows "p = q" |
|
1366 proof - |
|
1367 from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf) |
|
1368 also have "inf R R\<inverse>\<inverse> = op =" |
|
1369 using refl antisym by(auto intro!: ext simp add: reflpD dest: antisymD) |
|
1370 finally show ?thesis unfolding pmf.rel_eq . |
|
1371 qed |
|
1372 |
|
1373 lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)" |
|
1374 by(blast intro: reflpI rel_pmf_reflI reflpD) |
|
1375 |
|
1376 lemma antisymP_rel_pmf: |
|
1377 "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk> |
|
1378 \<Longrightarrow> antisymP (rel_pmf R)" |
|
1379 by(rule antisymI)(blast intro: rel_pmf_antisym) |
|
1380 |
|
1381 lemma transp_rel_pmf: |
|
1382 assumes "transp R" |
|
1383 shows "transp (rel_pmf R)" |
|
1384 proof (rule transpI) |
|
1385 fix x y z |
|
1386 assume "rel_pmf R x y" and "rel_pmf R y z" |
|
1387 hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI) |
|
1388 thus "rel_pmf R x z" |
|
1389 using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq) |
|
1390 qed |
|
1391 |
1290 end |
1392 end |
1291 |
1393 |