# HG changeset patch
# User hoelzl
# Date 1282653697 -7200
# Node ID aaee86c0e2373d97f239dd76429df00f2623576c
# Parent  d5d342611edb1723e36625e37971bb16ed72db54
moved generic lemmas in Probability to HOL

diff -r d5d342611edb -r aaee86c0e237 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy	Tue Aug 24 14:41:37 2010 +0200
@@ -88,6 +88,26 @@
 lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   by (auto intro: Inf_greatest dest: Inf_lower)
 
+lemma Sup_mono:
+  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
+  shows "Sup A \<le> Sup B"
+proof (rule Sup_least)
+  fix a assume "a \<in> A"
+  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
+  from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
+  with `a \<le> b` show "a \<le> Sup B" by auto
+qed
+
+lemma Inf_mono:
+  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
+  shows "Inf A \<le> Inf B"
+proof (rule Inf_greatest)
+  fix b assume "b \<in> B"
+  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
+  from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
+  with `a \<le> b` show "Inf A \<le> b" by auto
+qed
+
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f = \<Squnion> (f ` A)"
 
@@ -144,8 +164,25 @@
 lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
   by (auto intro: antisym INF_leI le_INFI)
 
+lemma SUP_mono:
+  "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+  by (force intro!: Sup_mono simp: SUPR_def)
+
+lemma INF_mono:
+  "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
+  by (force intro!: Inf_mono simp: INFI_def)
+
 end
 
+lemma less_Sup_iff:
+  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+  shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
+  unfolding not_le[symmetric] Sup_le_iff by auto
+
+lemma Inf_less_iff:
+  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
+  shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
+  unfolding not_le[symmetric] le_Inf_iff by auto
 
 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
@@ -204,6 +241,18 @@
 
 end
 
+lemma SUPR_fun_expand:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
+  shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
+  by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
+           simp: SUPR_def Sup_fun_def)
+
+lemma INFI_fun_expand:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
+  shows "(INF y:A. f y) x = (INF y:A. f y x)"
+  by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
+           simp: INFI_def Inf_fun_def)
+
 lemma Inf_empty_fun:
   "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   by (simp add: Inf_fun_def)
diff -r d5d342611edb -r aaee86c0e237 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Orderings.thy	Tue Aug 24 14:41:37 2010 +0200
@@ -1154,7 +1154,7 @@
       have "\<And>y. P y \<Longrightarrow> x \<le> y"
       proof (rule classical)
         fix y
-        assume "P y" and "\<not> x \<le> y" 
+        assume "P y" and "\<not> x \<le> y"
         with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
           by (auto simp add: not_le)
         with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
@@ -1181,13 +1181,25 @@
   "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
   by (blast intro: LeastI_ex)
 
+lemma LeastI2_wellorder:
+  assumes "P a"
+  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
+  shows "Q (Least P)"
+proof (rule LeastI2_order)
+  show "P (Least P)" using `P a` by (rule LeastI)
+next
+  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
+next
+  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
+qed
+
 lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
 apply (simp (no_asm_use) add: not_le [symmetric])
 apply (erule contrapos_nn)
 apply (erule Least_le)
 done
 
-end  
+end
 
 
 subsection {* Order on bool *}
diff -r d5d342611edb -r aaee86c0e237 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Tue Aug 24 14:41:37 2010 +0200
@@ -1238,7 +1238,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=pinfreal] SUPR_fun_expand[where 'b=pinfreal])
+    by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'c=pinfreal])
   then show "{x\<in>space M. a < ?sup x} \<in> sets M"
     using assms by auto
 qed
diff -r d5d342611edb -r aaee86c0e237 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Aug 24 14:41:37 2010 +0200
@@ -57,7 +57,7 @@
   shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
   (is "?l = ?r")
 proof -
-  have "?r = (\<Sum>y \<in> f ` space M. 
+  have "?r = (\<Sum>y \<in> f ` space M.
     (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
     by (auto intro!: setsum_cong2)
   also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
@@ -222,19 +222,6 @@
     by (simp add: if_distrib setsum_cases[OF `finite P`])
 qed
 
-lemma LeastI2_wellorder:
-  fixes a :: "_ :: wellorder"
-  assumes "P a"
-  and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
-  shows "Q (Least P)"
-proof (rule LeastI2_order)
-  show "P (Least P)" using `P a` by (rule LeastI)
-next
-  fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
-next
-  fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
-qed
-
 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
   fixes u :: "'a \<Rightarrow> pinfreal"
   assumes u: "u \<in> borel_measurable M"
@@ -399,7 +386,8 @@
           let ?N = "max n (natfloor r + 1)"
           have "u t < of_nat ?N" "n \<le> ?N"
             using ge_natfloor_plus_one_imp_gt[of r n] preal
-            by (auto simp: max_def real_Suc_natfloor)
+            using real_natfloor_add_one_gt
+            by (auto simp: max_def real_of_nat_Suc)
           from lower[OF this(1)]
           have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq
             using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm)
@@ -875,7 +863,7 @@
   moreover
   have "a * (SUP i. simple_integral (?uB i)) \<le> ?S"
     unfolding pinfreal_SUP_cmult[symmetric]
-  proof (safe intro!: SUP_mono)
+  proof (safe intro!: SUP_mono bexI)
     fix i
     have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)"
       using B `simple_function u`
@@ -890,7 +878,7 @@
     qed
     finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)"
       by auto
-  qed
+  qed simp
   ultimately show "a * simple_integral u \<le> ?S" by simp
 qed
 
@@ -1056,16 +1044,17 @@
     by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
 
   have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
-  proof (unfold isoton_def, safe)
-    fix i show "(INF m. u (m + i)) \<le> (INF m. u (m + Suc i))"
-      by (rule INF_mono[where N=Suc]) simp
-  qed
+  proof (unfold isoton_def, safe intro!: INF_mono bexI)
+    fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
+  qed simp
   from positive_integral_isoton[OF this] assms
   have "positive_integral (SUP n. INF m. u (m + n)) =
     (SUP n. positive_integral (INF m. u (m + n)))"
     unfolding isoton_def by (simp add: borel_measurable_INF)
   also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
-    by (auto intro!: SUP_mono[where N="\<lambda>x. x"] INFI_bound positive_integral_mono INF_leI simp: INFI_fun_expand)
+    apply (rule SUP_mono)
+    apply (rule_tac x=n in bexI)
+    by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
   finally show ?thesis .
 qed
 
@@ -1123,10 +1112,10 @@
   have "?I = (SUP i. positive_integral (\<lambda>x. min (of_nat i) (u x) * indicator N x))"
     unfolding isoton_def using borel `N \<in> sets M` by (simp add: borel_measurable_indicator)
   also have "\<dots> \<le> (SUP i. positive_integral (\<lambda>x. of_nat i * indicator N x))"
-  proof (rule SUP_mono, rule positive_integral_mono)
+  proof (rule SUP_mono, rule bexI, rule positive_integral_mono)
     fix x i show "min (of_nat i) (u x) * indicator N x \<le> of_nat i * indicator N x"
       by (cases "x \<in> N") auto
-  qed
+  qed simp
   also have "\<dots> = 0"
     using `N \<in> null_sets` by (simp add: positive_integral_cmult_indicator)
   finally show ?thesis by simp
@@ -1967,46 +1956,37 @@
   unfolding finite_measure_space_def finite_measure_space_axioms_def
   using assms by simp
 
-lemma (in finite_measure_space) borel_measurable_finite[intro, simp]:
-  fixes f :: "'a \<Rightarrow> real"
-  shows "f \<in> borel_measurable M"
+lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
   unfolding measurable_def sets_eq_Pow by auto
 
+lemma (in finite_measure_space) simple_function_finite: "simple_function f"
+  unfolding simple_function_def sets_eq_Pow using finite_space by auto
+
+lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
+  "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
+proof -
+  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)
+qed
+
 lemma (in finite_measure_space) integral_finite_singleton:
   shows "integrable f"
   and "integral f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
 proof -
-  have 1: "f \<in> borel_measurable M"
-    unfolding measurable_def sets_eq_Pow by auto
-
-  have 2: "finite (f`space M)" using finite_space by simp
-
-  have 3: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>"
-    using finite_measure[unfolded sets_eq_Pow] by simp
-
-  show "integrable f"
-    by (rule integral_on_finite(1)[OF 1 2 3]) simp
+  have [simp]:
+    "positive_integral (\<lambda>x. Real (f x)) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})"
+    "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
 
-  { fix r let ?x = "f -` {r} \<inter> space M"
-    have "?x \<subseteq> space M" by auto
-    with finite_space sets_eq_Pow finite_single_measure
-    have "real (\<mu> ?x) = (\<Sum>i \<in> ?x. real (\<mu> {i}))"
-      using real_measure_setsum_singleton[of ?x] by auto }
-  note measure_eq_setsum = this
+  show "integrable f" using finite_space finite_measure
+    by (simp add: setsum_\<omega> integrable_def sets_eq_Pow)
 
-  have "integral f = (\<Sum>r\<in>f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))"
-    by (rule integral_on_finite(2)[OF 1 2 3]) simp
-  also have "\<dots> = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))"
-    unfolding measure_eq_setsum setsum_right_distrib
-    apply (subst setsum_Sigma)
-    apply (simp add: finite_space)
-    apply (simp add: finite_space)
-  proof (rule setsum_reindex_cong[symmetric])
-    fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
-    thus "(\<lambda>(x, y). x * real (\<mu> {y})) a = f (snd a) * real (\<mu> {snd a})"
-      by auto
-  qed (auto intro!: image_eqI inj_onI)
-  finally show ?I .
+  show ?I using finite_measure
+    apply (simp add: integral_def sets_eq_Pow real_of_pinfreal_setsum[symmetric]
+      real_of_pinfreal_mult[symmetric] setsum_subtractf[symmetric])
+    by (rule setsum_cong) (simp_all split: split_if)
 qed
 
 end
diff -r d5d342611edb -r aaee86c0e237 src/HOL/Probability/Positive_Infinite_Real.thy
--- a/src/HOL/Probability/Positive_Infinite_Real.thy	Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Positive_Infinite_Real.thy	Tue Aug 24 14:41:37 2010 +0200
@@ -6,53 +6,20 @@
   imports Complex_Main Nat_Bijection Multivariate_Analysis
 begin
 
-lemma less_Sup_iff:
-  fixes a :: "'x\<Colon>{complete_lattice,linorder}"
-  shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
-  unfolding not_le[symmetric] Sup_le_iff by auto
-
-lemma Inf_less_iff:
-  fixes a :: "'x\<Colon>{complete_lattice,linorder}"
-  shows "Inf S < a \<longleftrightarrow> (\<exists> x \<in> S. x < a)"
-  unfolding not_le[symmetric] le_Inf_iff by auto
-
-lemma SUPR_fun_expand: "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
-  unfolding SUPR_def expand_fun_eq Sup_fun_def
-  by (auto intro!: arg_cong[where f=Sup])
-
-lemma real_Suc_natfloor: "r < real (Suc (natfloor r))"
-proof cases
-  assume "0 \<le> r"
-  from floor_correct[of r]
-  have "r < real (\<lfloor>r\<rfloor> + 1)" by auto
-  also have "\<dots> = real (Suc (natfloor r))"
-    using `0 \<le> r` by (auto simp: real_of_nat_Suc natfloor_def)
-  finally show ?thesis .
-next
-  assume "\<not> 0 \<le> r"
-  hence "r < 0" by auto
-  also have "0 < real (Suc (natfloor r))" by auto
-  finally show ?thesis .
+lemma (in complete_lattice) Sup_start:
+  assumes *: "\<And>x. f x \<le> f 0"
+  shows "(SUP n. f n) = f 0"
+proof (rule antisym)
+  show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
+  show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
 qed
 
-lemma (in complete_lattice) Sup_mono:
-  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
-  shows "Sup A \<le> Sup B"
-proof (rule Sup_least)
-  fix a assume "a \<in> A"
-  with assms obtain b where "b \<in> B" and "a \<le> b" by auto
-  hence "b \<le> Sup B" by (auto intro: Sup_upper)
-  with `a \<le> b` show "a \<le> Sup B" by auto
-qed
-
-lemma (in complete_lattice) Inf_mono:
-  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
-  shows "Inf A \<le> Inf B"
-proof (rule Inf_greatest)
-  fix b assume "b \<in> B"
-  with assms obtain a where "a \<in> A" and "a \<le> b" by auto
-  hence "Inf A \<le> a" by (auto intro: Inf_lower)
-  with `a \<le> b` show "Inf A \<le> b" by auto
+lemma (in complete_lattice) Inf_start:
+  assumes *: "\<And>x. f 0 \<le> f x"
+  shows "(INF n. f n) = f 0"
+proof (rule antisym)
+  show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
+  show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
 qed
 
 lemma (in complete_lattice) Sup_mono_offset:
@@ -77,12 +44,18 @@
   apply (rule Sup_mono_offset)
   by (auto intro!: order.lift_Suc_mono_le[of "op \<le>" "op <" f, OF _ *]) default
 
-lemma (in complete_lattice) Inf_start:
-  assumes *: "\<And>x. f 0 \<le> f x"
-  shows "(INF n. f n) = f 0"
+lemma (in complete_lattice) Inf_mono_offset:
+  fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
+  assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
+  shows "(INF n . f (k + n)) = (INF n. f n)"
 proof (rule antisym)
-  show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
-  show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
+  show "(INF n. f n) \<le> (INF n. f (k + n))"
+    by (auto intro!: Inf_mono simp: INFI_def)
+  { fix n :: 'b
+    have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
+    with * have "f (k + n) \<le> f n" by simp }
+  thus "(INF n. f (k + n)) \<le> (INF n. f n)"
+    by (auto intro!: Inf_mono exI simp: INFI_def)
 qed
 
 lemma (in complete_lattice) isotone_converge:
@@ -99,28 +72,6 @@
   ultimately show ?thesis by simp
 qed
 
-lemma (in complete_lattice) Inf_mono_offset:
-  fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
-  assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
-  shows "(INF n . f (k + n)) = (INF n. f n)"
-proof (rule antisym)
-  show "(INF n. f n) \<le> (INF n. f (k + n))"
-    by (auto intro!: Inf_mono simp: INFI_def)
-  { fix n :: 'b
-    have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
-    with * have "f (k + n) \<le> f n" by simp }
-  thus "(INF n. f (k + n)) \<le> (INF n. f n)"
-    by (auto intro!: Inf_mono exI simp: INFI_def)
-qed
-
-lemma (in complete_lattice) Sup_start:
-  assumes *: "\<And>x. f x \<le> f 0"
-  shows "(SUP n. f n) = f 0"
-proof (rule antisym)
-  show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
-  show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
-qed
-
 lemma (in complete_lattice) antitone_converges:
   fixes f :: "nat \<Rightarrow> 'a" assumes "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x"
   shows "(INF n. SUP m. f (n + m)) = (SUP n. INF m. f (n + m))"
@@ -1657,15 +1608,6 @@
   "1 \<le> Real p \<longleftrightarrow> 1 \<le> p"
   by (simp_all add: one_pinfreal_def del: Real_1)
 
-lemma SUP_mono:
-  assumes "\<And>n. f n \<le> g (N n)"
-  shows "(SUP n. f n) \<le> (SUP n. g n)"
-proof (safe intro!: SUPR_bound)
-  fix n note assms[of n]
-  also have "g (N n) \<le> (SUP n. g n)" by (auto intro!: le_SUPI)
-  finally show "f n \<le> (SUP n. g n)" .
-qed
-
 lemma isoton_Sup:
   assumes "f \<up> u"
   shows "f i \<le> u"
@@ -2563,20 +2505,6 @@
   shows "x \<le> (INF n. f n)"
   using assms by (simp add: INFI_def le_Inf_iff)
 
-lemma INF_mono:
-  assumes "\<And>n. f (N n) \<le> g n"
-  shows "(INF n. f n) \<le> (INF n. g n)"
-proof (safe intro!: INFI_bound)
-  fix n
-  have "(INF n. f n) \<le> f (N n)" by (auto intro!: INF_leI)
-  also note assms[of n]
-  finally show "(INF n. f n) \<le> g n" .
-qed
-
-lemma INFI_fun_expand: "(INF y:A. f y) = (\<lambda>x. INF y:A. f y x)"
-  unfolding INFI_def expand_fun_eq Inf_fun_def
-  by (auto intro!: arg_cong[where f=Inf])
-
 lemma LIMSEQ_imp_lim_INF:
   assumes pos: "\<And>i. 0 \<le> X i" and lim: "X ----> x"
   shows "(SUP n. INF m. Real (X (n + m))) = Real x"
@@ -2596,11 +2524,11 @@
     proof safe
       fix x y :: nat assume "x \<le> y"
       have "Real (r x) \<le> Real (r y)" unfolding r(1)[symmetric] using pos
-      proof (safe intro!: INF_mono)
+      proof (safe intro!: INF_mono bexI)
         fix m have "x + (m + y - x) = y + m"
           using `x \<le> y` by auto
         thus "Real (X (x + (m + y - x))) \<le> Real (X (y + m))" by simp
-      qed
+      qed simp
       thus "r x \<le> r y" using r by auto
     qed
     show "\<And>n. 0 \<le> r n" by fact
@@ -2646,7 +2574,6 @@
   qed
 qed
 
-
 lemma real_of_pinfreal_strict_mono_iff:
   "real a < real b \<longleftrightarrow> (b \<noteq> \<omega> \<and> ((a = \<omega> \<and> 0 < b) \<or> (a < b)))"
 proof (cases a)
diff -r d5d342611edb -r aaee86c0e237 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy	Tue Aug 24 14:41:37 2010 +0200
@@ -87,22 +87,6 @@
   shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
   oops
 
-lemma (in finite_measure_space) simple_function_finite:
-  "simple_function f"
-  unfolding simple_function_def sets_eq_Pow using finite_space by auto
-
-lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
-  unfolding measurable_def sets_eq_Pow by auto
-
-lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
-  "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
-proof -
-  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)
-qed
-
 lemma (in finite_measure_space) finite_prod_measure_times:
   assumes "finite_measure_space N \<nu>"
   and "A1 \<in> sets M" "A2 \<in> sets N"