# HG changeset patch
# User hoelzl
# Date 1291230773 -3600
# Node ID 94427db32392a2cc2027168e8079c4c5808559aa
# Parent  251df82c0088d4195f12398c5bc9eb288cdfdbfd
Tuned setup for borel_measurable with min, max and psuminf.

diff -r 251df82c0088 -r 94427db32392 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 20:09:41 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 20:12:53 2010 +0100
@@ -1016,7 +1016,6 @@
   then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B - {\<omega>}" and
     x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B"
     unfolding open_pinfreal_def by blast
-
   have "Real -` B = Real -` (B - {\<omega>})" by auto
   also have "\<dots> = Real -` (Real ` (T \<inter> {0..}))" using T by simp
   also have "\<dots> = (if 0 \<in> T then T \<union> {.. 0} else T \<inter> {0..})"
@@ -1222,12 +1221,10 @@
   hence **: "\<forall>a. {x\<in>space M. f x < a} \<in> sets M"
     unfolding less_eq_le_pinfreal_measurable
     unfolding greater_eq_le_measurable .
-
   show "f \<in> borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater
   proof safe
     have "f -` {\<omega>} \<inter> space M = space M - {x\<in>space M. f x < \<omega>}" by auto
     then show \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" using ** by auto
-
     fix a
     have "{w \<in> space M. a < real (f w)} =
       (if 0 \<le> a then {w\<in>space M. Real a < f w} - (f -` {\<omega>} \<inter> space M) else space M)"
@@ -1358,14 +1355,14 @@
     by induct auto
 qed (simp add: borel_measurable_const)
 
-lemma (in sigma_algebra) borel_measurable_pinfreal_min[intro, simp]:
+lemma (in sigma_algebra) borel_measurable_pinfreal_min[simp, intro]:
   fixes f g :: "'a \<Rightarrow> pinfreal"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
   using assms unfolding min_def by (auto intro!: measurable_If)
 
-lemma (in sigma_algebra) borel_measurable_pinfreal_max[intro]:
+lemma (in sigma_algebra) borel_measurable_pinfreal_max[simp, intro]:
   fixes f g :: "'a \<Rightarrow> pinfreal"
   assumes "f \<in> borel_measurable M"
   and "g \<in> borel_measurable M"
@@ -1412,7 +1409,7 @@
     using assms by auto
 qed
 
-lemma (in sigma_algebra) borel_measurable_psuminf:
+lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
   assumes "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
   using assms unfolding psuminf_def
@@ -1428,7 +1425,6 @@
 proof -
   let "?pu x i" = "max (u i x) 0"
   let "?nu x i" = "max (- u i x) 0"
-
   { fix x assume x: "x \<in> space M"
     have "(?pu x) ----> max (u' x) 0"
       "(?nu x) ----> max (- u' x) 0"
@@ -1438,10 +1434,8 @@
       "(SUP n. INF m. Real (- u (n + m) x)) = Real (- u' x)"
       by (simp_all add: Real_max'[symmetric]) }
   note eq = this
-
   have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
     by auto
-
   have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
        "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
     using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)