diff r 843c40bbc379 r a1abfa4e2b44 src/HOL/Probability/Borel_Space.thy
 a/src/HOL/Probability/Borel_Space.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Wed Dec 08 19:32:11 2010 +0100
@@ 1395,7 +1395,7 @@
lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
fixes f :: "'d\countable \ 'a \ pextreal"
assumes "\i. i \ A \ f i \ borel_measurable M"
 shows "(SUP i : A. f i) \ borel_measurable M" (is "?sup \ borel_measurable M")
+ shows "(\x. SUP i : A. f i x) \ borel_measurable M" (is "?sup \ borel_measurable M")
unfolding borel_measurable_pextreal_iff_greater
proof safe
fix a
@@ 1408,7 +1408,7 @@
lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
fixes f :: "'d :: countable \ 'a \ pextreal"
assumes "\i. i \ A \ f i \ borel_measurable M"
 shows "(INF i : A. f i) \ borel_measurable M" (is "?inf \ borel_measurable M")
+ shows "(\x. INF i : A. f i x) \ borel_measurable M" (is "?inf \ borel_measurable M")
unfolding borel_measurable_pextreal_iff_less
proof safe
fix a
@@ 1432,20 +1432,10 @@
using assms by auto
qed
lemma INFI_fun_expand:
 "(INF y:A. f y) = (\x. (INF y:A. f y x))"
 by (simp add: fun_eq_iff INFI_apply)

lemma SUPR_fun_expand:
 "(SUP y:A. f y) = (\x. (SUP y:A. f y x))"
 by (simp add: fun_eq_iff SUPR_apply)

lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
assumes "\i. f i \ borel_measurable M"
shows "(\x. (\\<^isub>\ i. f i x)) \ borel_measurable M"
 using assms unfolding psuminf_def
 by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])

+ using assms unfolding psuminf_def by auto
section "LIMSEQ is borel measurable"
@@ 1468,13 +1458,12 @@
note eq = this
have *: "\x. real (Real (u' x))  real (Real ( u' x)) = u' x"
by auto
 have "(SUP n. INF m. (\x. Real (u (n + m) x))) \ borel_measurable M"
 "(SUP n. INF m. (\x. Real ( u (n + m) x))) \ borel_measurable M"
 using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
+ have "(\x. SUP n. INF m. Real (u (n + m) x)) \ borel_measurable M"
+ "(\x. SUP n. INF m. Real ( u (n + m) x)) \ borel_measurable M"
+ using u by auto
with eq[THEN measurable_cong, of M "\x. x" borel]
have "(\x. Real (u' x)) \ borel_measurable M"
 "(\x. Real ( u' x)) \ borel_measurable M"
 unfolding SUPR_fun_expand INFI_fun_expand by auto
+ "(\x. Real ( u' x)) \ borel_measurable M" by auto
note this[THEN borel_measurable_real]
from borel_measurable_diff[OF this]
show ?thesis unfolding * .