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.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