src/HOL/Probability/Probability_Mass_Function.thy
changeset 62324 ae44f16dcea5
parent 62083 7582b39f51ed
child 62390 842917225d56
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 16 17:01:40 2016 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 16 22:28:19 2016 +0100
     1.3 @@ -1097,10 +1097,9 @@
     1.4      finally show ?thesis .
     1.5    qed
     1.6  
     1.7 -  show "\<And>R. rel_pmf R =
     1.8 -         (BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
     1.9 -         BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
    1.10 -     by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps)
    1.11 +  show "\<And>R. rel_pmf R = (\<lambda>x y. \<exists>z. set_pmf z \<subseteq> {(x, y). R x y} \<and>
    1.12 +    map_pmf fst z = x \<and> map_pmf snd z = y)"
    1.13 +     by (auto simp add: fun_eq_iff rel_pmf.simps)
    1.14  
    1.15    show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    1.16      for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"