summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Probability_Mass_Function.thy

changeset 63540 | f8652d0534fa |

parent 63343 | fb5d8a50c641 |

child 63680 | 6e1e8b5abbfa |

1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Jul 22 08:02:37 2016 +0200 1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Jul 22 11:00:43 2016 +0200 1.3 @@ -1104,17 +1104,17 @@ 1.4 assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}" 1.5 1.6 show "measure p C = measure q C" 1.7 - proof cases 1.8 - assume "p \<inter> C = {}" 1.9 - moreover then have "q \<inter> C = {}" 1.10 + proof (cases "p \<inter> C = {}") 1.11 + case True 1.12 + then have "q \<inter> C = {}" 1.13 using quotient_rel_set_disjoint[OF assms C R] by simp 1.14 - ultimately show ?thesis 1.15 + with True show ?thesis 1.16 unfolding measure_pmf_zero_iff[symmetric] by simp 1.17 next 1.18 - assume "p \<inter> C \<noteq> {}" 1.19 - moreover then have "q \<inter> C \<noteq> {}" 1.20 + case False 1.21 + then have "q \<inter> C \<noteq> {}" 1.22 using quotient_rel_set_disjoint[OF assms C R] by simp 1.23 - ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C" 1.24 + with False obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C" 1.25 by auto 1.26 then have "R x y" 1.27 using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms