# HG changeset patch
# User hoelzl
# Date 1291298270 -3600
# Node ID f5a74b17a69e35366ca66b403b64ceea66b3f49c
# Parent  1ef85f4e709767f2f0dd2b452688d7ac37e3afe9
Moved theorems to appropriate place.

diff -r 1ef85f4e7097 -r f5a74b17a69e src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 02 14:57:21 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Dec 02 14:57:50 2010 +0100
@@ -755,20 +755,6 @@
   qed
 qed
 
-lemma Real_mult_nonneg: assumes "x \<ge> 0" "y \<ge> 0"
-  shows "Real (x * y) = Real x * Real y" using assms by auto
-
-lemma Real_setprod: assumes "\<forall>x\<in>A. f x \<ge> 0" shows "Real (setprod f A) = setprod (\<lambda>x. Real (f x)) A"
-proof(cases "finite A")
-  case True thus ?thesis using assms
-  proof(induct A) case (insert x A)
-    have "0 \<le> setprod f A" apply(rule setprod_nonneg) using insert by auto
-    thus ?case unfolding setprod_insert[OF insert(1-2)] apply-
-      apply(subst Real_mult_nonneg) prefer 3 apply(subst insert(3)[THEN sym])
-      using insert by auto
-  qed auto
-qed auto
-
 lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
   apply(rule image_Int[THEN sym]) using bij_euclidean_component
   unfolding bij_betw_def by auto
diff -r 1ef85f4e7097 -r f5a74b17a69e src/HOL/Probability/Positive_Infinite_Real.thy
--- a/src/HOL/Probability/Positive_Infinite_Real.thy	Thu Dec 02 14:57:21 2010 +0100
+++ b/src/HOL/Probability/Positive_Infinite_Real.thy	Thu Dec 02 14:57:50 2010 +0100
@@ -360,6 +360,20 @@
 lemma real_of_pinfreal_mult: "real X * real Y = real (X * Y :: pinfreal)"
   by (cases X, cases Y) (auto simp: zero_le_mult_iff)
 
+lemma Real_mult_nonneg: assumes "x \<ge> 0" "y \<ge> 0"
+  shows "Real (x * y) = Real x * Real y" using assms by auto
+
+lemma Real_setprod: assumes "\<forall>x\<in>A. f x \<ge> 0" shows "Real (setprod f A) = setprod (\<lambda>x. Real (f x)) A"
+proof(cases "finite A")
+  case True thus ?thesis using assms
+  proof(induct A) case (insert x A)
+    have "0 \<le> setprod f A" apply(rule setprod_nonneg) using insert by auto
+    thus ?case unfolding setprod_insert[OF insert(1-2)] apply-
+      apply(subst Real_mult_nonneg) prefer 3 apply(subst insert(3)[THEN sym])
+      using insert by auto
+  qed auto
+qed auto
+
 subsection "@{typ pinfreal} is a linear order"
 
 instantiation pinfreal :: linorder