src/HOL/Probability/Measure_Space.thy
changeset 56212 3253aaf73a01
parent 56193 c726ecfb22b6
child 56994 8d5e5ec1cac3
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4      from this[of "Suc i"] show "f i \<le> y" by auto
     1.5    qed (insert assms, simp)
     1.6    ultimately show ?thesis using assms
     1.7 -    by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def)
     1.8 +    by (subst suminf_ereal_eq_SUP) (auto simp: indicator_def)
     1.9  qed
    1.10  
    1.11  lemma suminf_indicator:
    1.12 @@ -375,7 +375,7 @@
    1.13      by auto
    1.14    ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
    1.15      using A(4) f_fin f_Int_fin
    1.16 -    by (subst INFI_ereal_add) (auto simp: decseq_f)
    1.17 +    by (subst INF_ereal_add) (auto simp: decseq_f)
    1.18    moreover {
    1.19      fix n
    1.20      have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
    1.21 @@ -543,10 +543,10 @@
    1.22    have A0: "0 \<le> emeasure M (A 0)" using A by auto
    1.23  
    1.24    have "emeasure M (A 0) - (INF n. emeasure M (A n)) = emeasure M (A 0) + (SUP n. - emeasure M (A n))"
    1.25 -    by (simp add: ereal_SUPR_uminus minus_ereal_def)
    1.26 +    by (simp add: ereal_SUP_uminus minus_ereal_def)
    1.27    also have "\<dots> = (SUP n. emeasure M (A 0) - emeasure M (A n))"
    1.28      unfolding minus_ereal_def using A0 assms
    1.29 -    by (subst SUPR_ereal_add) (auto simp add: decseq_emeasure)
    1.30 +    by (subst SUP_ereal_add) (auto simp add: decseq_emeasure)
    1.31    also have "\<dots> = (SUP n. emeasure M (A 0 - A n))"
    1.32      using A finite `decseq A`[unfolded decseq_def] by (subst emeasure_Diff) auto
    1.33    also have "\<dots> = emeasure M (\<Union>i. A 0 - A i)"