equal
deleted
inserted
replaced
1095 also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq" |
1095 also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq" |
1096 by (metis Field_natLeq card_of_least natLeq_Well_order) |
1096 by (metis Field_natLeq card_of_least natLeq_Well_order) |
1097 finally show ?thesis . |
1097 finally show ?thesis . |
1098 qed |
1098 qed |
1099 |
1099 |
1100 show "\<And>R. rel_pmf R = |
1100 show "\<And>R. rel_pmf R = (\<lambda>x y. \<exists>z. set_pmf z \<subseteq> {(x, y). R x y} \<and> |
1101 (BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO |
1101 map_pmf fst z = x \<and> map_pmf snd z = y)" |
1102 BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)" |
1102 by (auto simp add: fun_eq_iff rel_pmf.simps) |
1103 by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps) |
|
1104 |
1103 |
1105 show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
1104 show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)" |
1106 for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" |
1105 for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" |
1107 proof - |
1106 proof - |
1108 { fix p q r |
1107 { fix p q r |