# HG changeset patch
# User haftmann
# Date 1291823265 -3600
# Node ID c987429a1298cbb313ece7cb941eb151feb611da
# Parent  9ff94e7cc3b3c3c478e186849350c44416637d2a
work around problems with eta-expansion of equations

diff -r 9ff94e7cc3b3 -r c987429a1298 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 15:05:46 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:47:45 2010 +0100
@@ -1391,7 +1391,7 @@
 proof safe
   fix a
   have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
-    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_apply[where 'c=pextreal])
+    by (auto simp: less_SUP_iff SUPR_apply)
   then show "{x\<in>space M. a < ?sup x} \<in> sets M"
     using assms by auto
 qed
@@ -1404,7 +1404,7 @@
 proof safe
   fix a
   have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
-    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_apply)
+    by (auto simp: INF_less_iff INFI_apply)
   then show "{x\<in>space M. ?inf x < a} \<in> sets M"
     using assms by auto
 qed
@@ -1423,11 +1423,20 @@
     using assms by auto
 qed
 
+lemma INFI_fun_expand:
+  "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
+  by (simp add: fun_eq_iff INFI_apply)
+
+lemma SUPR_fun_expand:
+  "(SUP y:A. f y) = (\<lambda>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 "\<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
-  by (auto intro!: borel_measurable_SUP[unfolded SUPR_apply])
+  by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
+
 
 section "LIMSEQ is borel measurable"
 
@@ -1456,7 +1465,7 @@
   with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
   have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
        "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
-    unfolding SUPR_apply INFI_apply by auto
+    unfolding SUPR_fun_expand INFI_fun_expand by auto
   note this[THEN borel_measurable_real]
   from borel_measurable_diff[OF this]
   show ?thesis unfolding * .