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