# HG changeset patch
# User nipkow
# Date 1397229101 -7200
# Node ID 01caba82e1d266870bc5a4ad8ca5882d97590716
# Parent  aefb4a8da31fb91b75d80c0ddf5ff6db3a22623b
made ereal_add_nonneg_nonneg a simp rule

diff -r aefb4a8da31f -r 01caba82e1d2 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Apr 11 13:36:57 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Apr 11 17:11:41 2014 +0200
@@ -536,7 +536,7 @@
 lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))"
   unfolding incseq_def by auto
 
-lemma ereal_add_nonneg_nonneg:
+lemma ereal_add_nonneg_nonneg[simp]:
   fixes a b :: ereal
   shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   using add_mono[of 0 a 0 b] by simp
diff -r aefb4a8da31f -r 01caba82e1d2 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 13:36:57 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 17:11:41 2014 +0200
@@ -1114,7 +1114,7 @@
   proof (rule SUP_simple_integral_sequences[OF l(3,6,2)])
     show "incseq ?L'" "\<And>i x. 0 \<le> ?L' i x" "\<And>i. simple_function M (?L' i)"
       using u v  `0 \<le> a` unfolding incseq_Suc_iff le_fun_def
-      by (auto intro!: add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg)
+      by (auto intro!: add_mono ereal_mult_left_mono)
     { fix x
       { fix i have "a * u i x \<noteq> -\<infinity>" "v i x \<noteq> -\<infinity>" "u i x \<noteq> -\<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x]
           by auto }
@@ -1122,10 +1122,10 @@
         using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
         by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
            (auto intro!: SUP_ereal_add
-                 simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) }
+                 simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) }
     then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
       unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
-      by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg)
+      by (intro AE_I2) (auto split: split_max)
   qed
   also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))"
     using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext)
@@ -1182,7 +1182,7 @@
   shows "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = integral\<^sup>P M f + integral\<^sup>P M g"
 proof -
   have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
-    using assms by (auto split: split_max simp: ereal_add_nonneg_nonneg)
+    using assms by (auto split: split_max)
   have "(\<integral>\<^sup>+ x. f x + g x \<partial>M) = (\<integral>\<^sup>+ x. max 0 (f x + g x) \<partial>M)"
     by (simp add: positive_integral_max_0)
   also have "\<dots> = (\<integral>\<^sup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"
diff -r aefb4a8da31f -r 01caba82e1d2 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Apr 11 13:36:57 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Apr 11 17:11:41 2014 +0200
@@ -483,8 +483,7 @@
         using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"]
         by (cases "\<integral>\<^sup>+x. ?F A x \<partial>M", cases "N A") auto
       finally have "(\<integral>\<^sup>+x. ?f0 x * indicator A x \<partial>M) \<le> N A" . }
-    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G`
-      by (auto intro!: ereal_add_nonneg_nonneg simp: G_def)
+    hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` by (auto simp: G_def)
     have int_f_finite: "integral\<^sup>P M f \<noteq> \<infinity>"
       by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le)
     have  "0 < ?M (space M) - emeasure ?Mb (space M)"