src/HOL/Probability/Radon_Nikodym.thy
changeset 53374 a14d2a854c02
parent 53015 a1119cf551e8
child 54776 db890d9fc5c2
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -412,14 +412,14 @@
     1.4  
     1.5    have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def
     1.6    proof
     1.7 -    fix A assume A: "A \<in> null_sets M"
     1.8 -    with `absolutely_continuous M N` have "A \<in> null_sets N"
     1.9 +    fix A assume A_M: "A \<in> null_sets M"
    1.10 +    with `absolutely_continuous M N` have A_N: "A \<in> null_sets N"
    1.11        unfolding absolutely_continuous_def by auto
    1.12 -    moreover with A have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
    1.13 +    moreover from A_M A_N have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
    1.14      ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
    1.15        using positive_integral_positive[of M] by (auto intro!: antisym)
    1.16      then show "A \<in> null_sets ?M"
    1.17 -      using A by (simp add: emeasure_M null_sets_def sets_eq)
    1.18 +      using A_M by (simp add: emeasure_M null_sets_def sets_eq)
    1.19    qed
    1.20    have upper_bound: "\<forall>A\<in>sets M. ?M A \<le> 0"
    1.21    proof (rule ccontr)
    1.22 @@ -431,7 +431,7 @@
    1.23        using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq])
    1.24      finally have pos_t: "0 < ?M (space M)" by simp
    1.25      moreover
    1.26 -    then have "emeasure M (space M) \<noteq> 0"
    1.27 +    from pos_t have "emeasure M (space M) \<noteq> 0"
    1.28        using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def)
    1.29      then have pos_M: "0 < emeasure M (space M)"
    1.30        using emeasure_nonneg[of M "space M"] by (simp add: le_less)
    1.31 @@ -594,12 +594,14 @@
    1.32        proof (rule disjCI, simp)
    1.33          assume *: "0 < emeasure M A \<longrightarrow> N A \<noteq> \<infinity>"
    1.34          show "emeasure M A = 0 \<and> N A = 0"
    1.35 -        proof cases
    1.36 -          assume "emeasure M A = 0" moreover with ac A have "N A = 0"
    1.37 +        proof (cases "emeasure M A = 0")
    1.38 +          case True
    1.39 +          with ac A have "N A = 0"
    1.40              unfolding absolutely_continuous_def by auto
    1.41 -          ultimately show ?thesis by simp
    1.42 +          with True show ?thesis by simp
    1.43          next
    1.44 -          assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
    1.45 +          case False
    1.46 +          with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
    1.47            with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
    1.48              using Q' by (auto intro!: plus_emeasure sets.countable_UN)
    1.49            also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"