real is better supported than real_of_nat, use it in the nat => ereal coercion
authorhoelzl
Mon Dec 05 17:33:57 2011 +0100 (2011-12-05)
changeset 457692d5b1af2426a
parent 45768 97be233b32ed
child 45770 5d35cb2c0f02
real is better supported than real_of_nat, use it in the nat => ereal coercion
src/HOL/Library/Extended_Real.thy
src/HOL/Probability/Radon_Nikodym.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Dec 05 14:47:01 2011 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Dec 05 17:33:57 2011 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  
     1.5  declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
     1.6  declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
     1.7 -declare [[coercion "(\<lambda>n. ereal (of_nat n)) :: nat \<Rightarrow> ereal"]]
     1.8 +declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
     1.9  
    1.10  lemma ereal_uminus_uminus[simp]:
    1.11    fixes a :: ereal shows "- (- a) = a"
     2.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 14:47:01 2011 +0100
     2.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 17:33:57 2011 +0100
     2.3 @@ -1097,7 +1097,7 @@
     2.4        next
     2.5          case (real r)
     2.6          with less_PInf_Ex_of_nat[of "f x"] obtain n :: nat where "f x < n" by (auto simp: real_eq_of_nat)
     2.7 -        then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"])
     2.8 +        then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"] simp: real_eq_of_nat)
     2.9        next
    2.10          case MInf with x show ?thesis
    2.11            unfolding A_def by (auto intro!: exI[of _ "Suc 0"])
    2.12 @@ -1117,7 +1117,7 @@
    2.13        case (Suc n)
    2.14        then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
    2.15          (\<integral>\<^isup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
    2.16 -        by (auto intro!: positive_integral_mono simp: indicator_def A_def)
    2.17 +        by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat)
    2.18        also have "\<dots> = Suc n * \<mu> (Q j)"
    2.19          using Q by (auto intro!: positive_integral_cmult_indicator)
    2.20        also have "\<dots> < \<infinity>"