# HG changeset patch
# User hoelzl
# Date 1291298942 -3600
# Node ID 9a9d33f6fb46bf842742194f3de40afaad2ebd51
# Parent  f5a74b17a69e35366ca66b403b64ceea66b3f49c
generalized simple_functionD

diff -r f5a74b17a69e -r 9a9d33f6fb46 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 02 14:57:50 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Dec 02 15:09:02 2010 +0100
@@ -43,19 +43,14 @@
 
 lemma (in sigma_algebra) simple_functionD:
   assumes "simple_function g"
-  shows "finite (g ` space M)" and "g -` {x} \<inter> space M \<in> sets M"
+  shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M"
 proof -
   show "finite (g ` space M)"
     using assms unfolding simple_function_def by auto
-  show "g -` {x} \<inter> space M \<in> sets M"
-  proof cases
-    assume "x \<in> g`space M" then show ?thesis
-      using assms unfolding simple_function_def by auto
-  next
-    assume "x \<notin> g`space M"
-    then have "g -` {x} \<inter> space M = {}" by auto
-    then show ?thesis by auto
-  qed
+  have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
+  also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
+  finally show "g -` X \<inter> space M \<in> sets M" using assms
+    by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def)
 qed
 
 lemma (in sigma_algebra) simple_function_indicator_representation:
@@ -2309,7 +2304,7 @@
 qed
 
 lemma (in finite_measure_space) simple_function_finite[simp, intro]: "simple_function f"
-  unfolding simple_function_def sets_eq_Pow using finite_space by auto
+  unfolding simple_function_def using finite_space by auto
 
 lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
   by (auto intro: borel_measurable_simple_function)
@@ -2320,7 +2315,7 @@
   have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
     by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
   show ?thesis unfolding * using borel_measurable_finite[of f]
-    by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
+    by (simp add: positive_integral_setsum positive_integral_cmult_indicator)
 qed
 
 lemma (in finite_measure_space) integral_finite_singleton:
@@ -2332,9 +2327,9 @@
     "positive_integral (\<lambda>x. Real (- f x)) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})"
     unfolding positive_integral_finite_eq_setsum by auto
   show "integrable f" using finite_space finite_measure
-    by (simp add: setsum_\<omega> integrable_def sets_eq_Pow)
+    by (simp add: setsum_\<omega> integrable_def)
   show ?I using finite_measure
-    apply (simp add: integral_def sets_eq_Pow real_of_pinfreal_setsum[symmetric]
+    apply (simp add: integral_def real_of_pinfreal_setsum[symmetric]
       real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric])
     by (rule setsum_cong) (simp_all split: split_if)
 qed