author hoelzl Mon, 05 Dec 2011 17:33:57 +0100 changeset 45769 2d5b1af2426a parent 45768 97be233b32ed child 45770 5d35cb2c0f02
real is better supported than real_of_nat, use it in the nat => ereal coercion
```--- a/src/HOL/Library/Extended_Real.thy	Mon Dec 05 14:47:01 2011 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Mon Dec 05 17:33:57 2011 +0100
@@ -59,7 +59,7 @@

declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
-declare [[coercion "(\<lambda>n. ereal (of_nat n)) :: nat \<Rightarrow> ereal"]]
+declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]

lemma ereal_uminus_uminus[simp]:
fixes a :: ereal shows "- (- a) = a"```
```--- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 14:47:01 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 17:33:57 2011 +0100
@@ -1097,7 +1097,7 @@
next
case (real r)
with less_PInf_Ex_of_nat[of "f x"] obtain n :: nat where "f x < n" by (auto simp: real_eq_of_nat)
-        then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"])
+        then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"] simp: real_eq_of_nat)
next
case MInf with x show ?thesis
unfolding A_def by (auto intro!: exI[of _ "Suc 0"])
@@ -1117,7 +1117,7 @@
case (Suc n)
then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
(\<integral>\<^isup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
-        by (auto intro!: positive_integral_mono simp: indicator_def A_def)
+        by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat)
also have "\<dots> = Suc n * \<mu> (Q j)"
using Q by (auto intro!: positive_integral_cmult_indicator)
also have "\<dots> < \<infinity>"```