# HG changeset patch
# User haftmann
# Date 1267808130 -3600
# Node ID d80f417269b4193dc14383c98da01e04f0481c14
# Parent  c0db094d0d803f63869e620221bcb27724b6aace# Parent  768f8d92b7675cef6a6b8c0c15c802ee6344f184
merged

diff -r c0db094d0d80 -r d80f417269b4 Admin/isatest/settings/at-poly-test
--- a/Admin/isatest/settings/at-poly-test	Fri Mar 05 17:55:14 2010 +0100
+++ b/Admin/isatest/settings/at-poly-test	Fri Mar 05 17:55:30 2010 +0100
@@ -1,6 +1,6 @@
 # -*- shell-script -*- :mode=shellscript:
 
-  POLYML_HOME="/home/polyml/polyml-5.3.0"
+  POLYML_HOME="/home/polyml/polyml-svn"
   ML_SYSTEM="polyml-5.3.0"
   ML_PLATFORM="x86-linux"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
diff -r c0db094d0d80 -r d80f417269b4 README_REPOSITORY
--- a/README_REPOSITORY	Fri Mar 05 17:55:14 2010 +0100
+++ b/README_REPOSITORY	Fri Mar 05 17:55:30 2010 +0100
@@ -83,6 +83,8 @@
 See also the fine documentation for further details, especially the
 book http://hgbook.red-bean.com/
 
+There is also a nice tutorial at http://hginit.com/
+
 
 Shared pull/push access
 -----------------------
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -236,7 +236,7 @@
 by blast
 
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
-by (metis equalityE parts_idem parts_increasing parts_mono subset_trans)
+by (metis parts_idem parts_increasing parts_mono subset_trans)
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
 by (drule parts_mono, blast)
@@ -611,7 +611,7 @@
 by blast
 
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
-by (metis equalityE subset_trans synth_idem synth_increasing synth_mono)
+by (metis subset_trans synth_idem synth_increasing synth_mono)
 
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
@@ -674,8 +674,7 @@
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
 by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)
 
-text{*More specifically for Fake.  Very occasionally we could do with a version
-  of the form  @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"} *}
+text{*More specifically for Fake. See also @{text Fake_parts_sing} below *}
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
@@ -884,17 +883,17 @@
 
 lemma Fake_analz_eq [simp]:
      "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
-by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute equalityI
+by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute 
           subset_insertI synth_analz_mono synth_increasing synth_subset_iff)
 
 text{*Two generalizations of @{text analz_insert_eq}*}
 lemma gen_analz_insert_eq [rule_format]:
-     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
+     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
 
 lemma synth_analz_insert_eq [rule_format]:
      "X \<in> synth (analz H) 
-      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
+      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
 apply (erule synth.induct) 
 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
 done
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Fields.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -1034,30 +1034,33 @@
   apply (simp add: order_less_imp_le)
 done
 
-
 lemma field_le_epsilon:
-  fixes x y :: "'a :: {division_by_zero,linordered_field}"
+  fixes x y :: "'a\<Colon>linordered_field"
   assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
   shows "x \<le> y"
-proof (rule ccontr)
-  obtain two :: 'a where two: "two = 1 + 1" by simp
-  assume "\<not> x \<le> y"
-  then have yx: "y < x" by simp
-  then have "y + - y < x + - y" by (rule add_strict_right_mono)
-  then have "x - y > 0" by (simp add: diff_minus)
-  then have "(x - y) / two > 0"
-    by (rule divide_pos_pos) (simp add: two)
-  then have "x \<le> y + (x - y) / two" by (rule e)
-  also have "... = (x - y + two * y) / two"
-    by (simp add: add_divide_distrib two)
-  also have "... = (x + y) / two" 
-    by (simp add: two algebra_simps)
-  also have "... < x" using yx
-    by (simp add: two pos_divide_less_eq algebra_simps)
-  finally have "x < x" .
-  then show False ..
+proof (rule dense_le)
+  fix t assume "t < x"
+  hence "0 < x - t" by (simp add: less_diff_eq)
+  from e[OF this]
+  show "t \<le> y" by (simp add: field_simps)
 qed
 
+lemma field_le_mult_one_interval:
+  fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
+  assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
+  shows "x \<le> y"
+proof (cases "0 < x")
+  assume "0 < x"
+  thus ?thesis
+    using dense_le_bounded[of 0 1 "y/x"] *
+    unfolding le_divide_eq if_P[OF `0 < x`] by simp
+next
+  assume "\<not>0 < x" hence "x \<le> 0" by simp
+  obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto
+  hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto
+  also note *[OF s]
+  finally show ?thesis .
+qed
 
 code_modulename SML
   Fields Arith
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -1278,14 +1278,15 @@
 
 lemma setsum_cases:
   assumes fA: "finite A"
-  shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
-         setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
+  shows "setsum (\<lambda>x. if P x then f x else g x) A =
+         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
 proof-
-  have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}" 
+  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
+          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
     by blast+
   from fA 
-  have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
-  let ?g = "\<lambda>x. if x \<in> B then f x else g x"
+  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
+  let ?g = "\<lambda>x. if P x then f x else g x"
   from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
   show ?thesis by simp
 qed
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Fun.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -378,6 +378,11 @@
 apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
 done
 
+lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
+  by (auto intro!: inj_onI)
+
+lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
+  by (auto intro!: inj_onI dest: strict_mono_eq)
 
 subsection{*Function Updating*}
 
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 05 17:55:30 2010 +0100
@@ -1086,13 +1086,15 @@
 
 HOL-Probability: HOL $(LOG)/HOL-Probability.gz
 
-$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \
-  Probability/Probability.thy \
-  Probability/Sigma_Algebra.thy \
-  Probability/SeriesPlus.thy \
-  Probability/Caratheodory.thy \
-  Probability/Measure.thy \
-  Probability/Borel.thy
+$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML	\
+  Probability/Probability.thy					\
+  Probability/Sigma_Algebra.thy					\
+  Probability/SeriesPlus.thy					\
+  Probability/Caratheodory.thy					\
+  Probability/Borel.thy						\
+  Probability/Measure.thy					\
+  Probability/Lebesgue.thy					\
+  Probability/Probability_Space.thy
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
 
 
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -342,8 +342,8 @@
     apply(rule_tac x="insert a f" in exI)
     apply(rule_tac x="\<lambda>x. if x=a then 1 - setsum (\<lambda>x. u (x - a)) f else u (x - a)" in exI)
     using assms and f unfolding setsum_clauses(2)[OF f(1)] and if_smult
-    unfolding setsum_cases[OF f(1), of "{a}", unfolded singleton_iff] and *
-    by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed
+    unfolding setsum_cases[OF f(1), of "\<lambda>x. x = a"]
+    by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps *) qed
 
 lemma affine_hull_span:
   fixes a :: "real ^ _"
@@ -492,7 +492,7 @@
   fix t u assume as:"\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s" " finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
   have *:"s \<inter> t = t" using as(3) by auto
   show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" using as(1)[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]]
-    unfolding if_smult and setsum_cases[OF assms] and * using as(2-) by auto
+    unfolding if_smult and setsum_cases[OF assms] using as(2-) * by auto
 qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
 
 subsection {* Cones. *}
@@ -890,7 +890,7 @@
   show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
     apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
     apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)
-    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def
+    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq
     unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] setsum_right_distrib[THEN sym] proof-
     fix i assume i:"i \<in> {1..k1+k2}"
     show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Orderings.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -1097,7 +1097,43 @@
   assumes gt_ex: "\<exists>y. x < y" 
   and lt_ex: "\<exists>y. y < x"
   and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+begin
 
+lemma dense_le:
+  fixes y z :: 'a
+  assumes "\<And>x. x < y \<Longrightarrow> x \<le> z"
+  shows "y \<le> z"
+proof (rule ccontr)
+  assume "\<not> ?thesis"
+  hence "z < y" by simp
+  from dense[OF this]
+  obtain x where "x < y" and "z < x" by safe
+  moreover have "x \<le> z" using assms[OF `x < y`] .
+  ultimately show False by auto
+qed
+
+lemma dense_le_bounded:
+  fixes x y z :: 'a
+  assumes "x < y"
+  assumes *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z"
+  shows "y \<le> z"
+proof (rule dense_le)
+  fix w assume "w < y"
+  from dense[OF `x < y`] obtain u where "x < u" "u < y" by safe
+  from linear[of u w]
+  show "w \<le> z"
+  proof (rule disjE)
+    assume "u \<le> w"
+    from less_le_trans[OF `x < u` `u \<le> w`] `w < y`
+    show "w \<le> z" by (rule *)
+  next
+    assume "w \<le> u"
+    from `w \<le> u` *[OF `x < u` `u < y`]
+    show "w \<le> z" by (rule order_trans)
+  qed
+qed
+
+end
 
 subsection {* Wellorders *}
 
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Probability/Borel.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -17,7 +17,7 @@
 
 definition mono_convergent where
   "mono_convergent u f s \<equiv>
-        (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+        (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
         (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
 
 lemma in_borel_measurable:
@@ -355,7 +355,7 @@
                     borel_measurable_add_borel_measurable f g) 
   have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = 
         (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
-    by (simp add: minus_divide_right) 
+    by (simp add: minus_divide_right)
   also have "... \<in> borel_measurable M" 
     by (fast intro: affine_borel_measurable borel_measurable_square 
                     borel_measurable_add_borel_measurable 
@@ -388,7 +388,7 @@
         assume w: "w \<in> space M" and f: "f w \<le> a"
         hence "u i w \<le> f w"
           by (auto intro: SEQ.incseq_le
-                   simp add: incseq_def mc [unfolded mono_convergent_def])
+                   simp add: mc [unfolded mono_convergent_def])
         thus "u i w \<le> a" using f
           by auto
       next
@@ -422,4 +422,143 @@
     by (auto simp add: borel_measurable_add_borel_measurable) 
 qed
 
+section "Monotone convergence"
+
+lemma mono_convergentD:
+  assumes "mono_convergent u f s" and "x \<in> s"
+  shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
+  using assms unfolding mono_convergent_def by auto
+
+
+lemma mono_convergentI:
+  assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
+  assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
+  shows "mono_convergent u f s"
+  using assms unfolding mono_convergent_def by auto
+
+lemma mono_convergent_le:
+  assumes "mono_convergent u f s" and "t \<in> s"
+  shows "u n t \<le> f t"
+using mono_convergentD[OF assms] by (auto intro!: incseq_le)
+
+definition "upclose f g x = max (f x) (g x)"
+
+primrec mon_upclose where
+"mon_upclose 0 u = u 0" |
+"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
+
+lemma mon_upclose_ex:
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
+  shows "\<exists>n \<le> m. mon_upclose m u x = u n x"
+proof (induct m)
+  case (Suc m)
+  then obtain n where "n \<le> m" and *: "mon_upclose m u x = u n x" by blast
+  thus ?case
+  proof (cases "u n x \<le> u (Suc m) x")
+    case True with min_max.sup_absorb1 show ?thesis
+      by (auto simp: * upclose_def intro!: exI[of _ "Suc m"])
+  next
+    case False
+     with min_max.sup_absorb2 `n \<le> m` show ?thesis
+       by (auto simp: * upclose_def intro!: exI[of _ n] min_max.sup_absorb2)
+  qed
+qed simp
+
+lemma mon_upclose_all:
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
+  assumes "m \<le> n"
+  shows "u m x \<le> mon_upclose n u x"
+using assms proof (induct n)
+  case 0 thus ?case by auto
+next
+  case (Suc n)
+  show ?case
+  proof (cases "m = Suc n")
+    case True thus ?thesis by (simp add: upclose_def)
+  next
+    case False
+    hence "m \<le> n" using `m \<le> Suc n` by simp
+    from Suc.hyps[OF this]
+    show ?thesis by (auto simp: upclose_def intro!: min_max.le_supI2)
+  qed
+qed
+
+lemma mono_convergent_limit:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "mono_convergent u f s" and "x \<in> s" and "0 < r"
+  shows "\<exists>N. \<forall>n\<ge>N. f x - u n x < r"
+proof -
+  from LIMSEQ_D[OF mono_convergentD(2)[OF assms(1,2)] `0 < r`]
+  obtain N where "\<And>n. N \<le> n \<Longrightarrow> \<bar> u n x - f x \<bar> < r" by auto
+  with mono_convergent_le[OF assms(1,2)] `0 < r`
+  show ?thesis by (auto intro!: exI[of _ N])
+qed
+
+lemma mon_upclose_le_mono_convergent:
+  assumes mc: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s" and "x \<in> s"
+  and "incseq (\<lambda>n. f n x)"
+  shows "mon_upclose n (u n) x <= f n x"
+proof -
+  obtain m where *: "mon_upclose n (u n) x = u n m x" and "m \<le> n"
+    using mon_upclose_ex[of n "u n" x] by auto
+  note this(1)
+  also have "u n m x \<le> f m x" using mono_convergent_le[OF assms(1,2)] .
+  also have "... \<le> f n x" using assms(3) `m \<le> n` unfolding incseq_def by auto
+  finally show ?thesis .
+qed
+
+lemma mon_upclose_mono_convergent:
+  assumes mc_u: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s"
+  and mc_f: "mono_convergent f h s"
+  shows "mono_convergent (\<lambda>n. mon_upclose n (u n)) h s"
+proof (rule mono_convergentI)
+  fix x assume "x \<in> s"
+  show "incseq (\<lambda>n. mon_upclose n (u n) x)" unfolding incseq_def
+  proof safe
+    fix m n :: nat assume "m \<le> n"
+    obtain i where mon: "mon_upclose m (u m) x = u m i x" and "i \<le> m"
+      using mon_upclose_ex[of m "u m" x] by auto
+    hence "i \<le> n" using `m \<le> n` by auto
+
+    note mon
+    also have "u m i x \<le> u n i x"
+      using mono_convergentD(1)[OF mc_u `x \<in> s`] `m \<le> n`
+      unfolding incseq_def by auto
+    also have "u n i x \<le> mon_upclose n (u n) x"
+      using mon_upclose_all[OF `i \<le> n`, of "u n" x] .
+    finally show "mon_upclose m (u m) x \<le> mon_upclose n (u n) x" .
+  qed
+
+  show "(\<lambda>i. mon_upclose i (u i) x) ----> h x"
+  proof (rule LIMSEQ_I)
+    fix r :: real assume "0 < r"
+    hence "0 < r / 2" by auto
+    from mono_convergent_limit[OF mc_f `x \<in> s` this]
+    obtain N where f_h: "\<And>n. N \<le> n \<Longrightarrow> h x - f n x < r / 2" by auto
+
+    from mono_convergent_limit[OF mc_u `x \<in> s` `0 < r / 2`]
+    obtain N' where u_f: "\<And>n. N' \<le> n \<Longrightarrow> f N x - u n N x < r / 2" by auto
+
+    show "\<exists>N. \<forall>n\<ge>N. norm (mon_upclose n (u n) x - h x) < r"
+    proof (rule exI[of _ "max N N'"], safe)
+      fix n assume "max N N' \<le> n"
+      hence "N \<le> n" and "N' \<le> n" by auto
+      hence "u n N x \<le> mon_upclose n (u n) x"
+        using mon_upclose_all[of N n "u n" x] by auto
+      moreover
+      from add_strict_mono[OF u_f[OF `N' \<le> n`] f_h[OF order_refl]]
+      have "h x - u n N x < r" by auto
+      ultimately have "h x - mon_upclose n (u n) x < r" by auto
+      moreover
+      obtain i where "mon_upclose n (u n) x = u n i x"
+        using mon_upclose_ex[of n "u n"] by blast
+      with mono_convergent_le[OF mc_u `x \<in> s`, of n i]
+           mono_convergent_le[OF mc_f `x \<in> s`, of i]
+      have "mon_upclose n (u n) x \<le> h x" by auto
+      ultimately
+      show "norm (mon_upclose n (u n) x - h x) < r" by auto
+     qed
+  qed
+qed
+
 end
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -15,8 +15,11 @@
   measure:: "'a set \<Rightarrow> real"
 
 definition
-  disjoint_family  where
-  "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
+  disjoint_family_on  where
+  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
+
+abbreviation
+  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
 
 definition
   positive  where
@@ -99,9 +102,9 @@
   by (auto simp add: additive_def)
 
 lemma countably_additiveD:
-  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A 
+  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
    \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
-  by (simp add: countably_additive_def) 
+  by (simp add: countably_additive_def)
 
 lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
   by blast
@@ -111,7 +114,7 @@
 
 lemma disjoint_family_subset:
      "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
-  by (force simp add: disjoint_family_def) 
+  by (force simp add: disjoint_family_on_def)
 
 subsection {* A Two-Element Series *}
 
@@ -119,28 +122,28 @@
   where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
 
 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
-  apply (simp add: binaryset_def) 
-  apply (rule set_ext) 
-  apply (auto simp add: image_iff) 
+  apply (simp add: binaryset_def)
+  apply (rule set_ext)
+  apply (auto simp add: image_iff)
   done
 
 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
-  by (simp add: UNION_eq_Union_image range_binaryset_eq) 
+  by (simp add: UNION_eq_Union_image range_binaryset_eq)
 
-lemma LIMSEQ_binaryset: 
+lemma LIMSEQ_binaryset:
   assumes f: "f {} = 0"
   shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
 proof -
   have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
-    proof 
+    proof
       fix n
       show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
-        by (induct n)  (auto simp add: binaryset_def f) 
+        by (induct n)  (auto simp add: binaryset_def f)
     qed
   moreover
-  have "... ----> f A + f B" by (rule LIMSEQ_const) 
+  have "... ----> f A + f B" by (rule LIMSEQ_const)
   ultimately
-  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" 
+  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
     by metis
   hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
     by simp
@@ -285,23 +288,23 @@
 lemma (in algebra) countably_subadditive_subadditive:
   assumes f: "positive M f" and cs: "countably_subadditive M f"
   shows  "subadditive M f"
-proof (auto simp add: subadditive_def) 
+proof (auto simp add: subadditive_def)
   fix x y
   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   hence "disjoint_family (binaryset x y)"
-    by (auto simp add: disjoint_family_def binaryset_def) 
-  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
-         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
+    by (auto simp add: disjoint_family_on_def binaryset_def)
+  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
+         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
          summable (f o (binaryset x y)) \<longrightarrow>
          f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
-    using cs by (simp add: countably_subadditive_def) 
-  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
+    using cs by (simp add: countably_subadditive_def)
+  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
          summable (f o (binaryset x y)) \<longrightarrow>
          f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
     by (simp add: range_binaryset_eq UN_binaryset_eq)
   thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
-    by (auto simp add: Un sums_iff positive_def o_def) 
-qed 
+    by (auto simp add: Un sums_iff positive_def o_def)
+qed
 
 
 definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
@@ -312,19 +315,19 @@
   case 0 show ?case by simp
 next
   case (Suc n)
-  thus ?case by (simp add: atLeastLessThanSuc disjointed_def) 
+  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
 qed
 
 lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
-  apply (rule UN_finite2_eq [where k=0]) 
-  apply (simp add: finite_UN_disjointed_eq) 
+  apply (rule UN_finite2_eq [where k=0])
+  apply (simp add: finite_UN_disjointed_eq)
   done
 
 lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   by (auto simp add: disjointed_def)
 
 lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
-  by (simp add: disjoint_family_def) 
+  by (simp add: disjoint_family_on_def)
      (metis neq_iff Int_commute less_disjoint_disjointed)
 
 lemma disjointed_subset: "disjointed A n \<subseteq> A n"
@@ -383,7 +386,7 @@
 next
   case (Suc n) 
   have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj 
-    by (auto simp add: disjoint_family_def neq_iff) blast
+    by (auto simp add: disjoint_family_on_def neq_iff) blast
   moreover 
   have "A n \<in> sets M" using A by blast 
   moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
@@ -440,7 +443,7 @@
 next
   case (Suc n) 
   have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
-    by (force simp add: disjoint_family_def neq_iff) 
+    by (force simp add: disjoint_family_on_def neq_iff) 
   have 3: "A n \<in> lambda_system M f" using A
     by blast
   have 4: "UNION {0..<n} A \<in> lambda_system M f"
@@ -505,7 +508,7 @@
           by blast
         moreover 
         have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
-          by (auto simp add: disjoint_family_def) 
+          by (auto simp add: disjoint_family_on_def) 
         moreover 
         have "a \<inter> (\<Union>i. A i) \<in> sets M"
           by (metis Int U_in a)
@@ -584,7 +587,7 @@
   finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
   thus ?thesis using a
     by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] 
-             simp add: measure_set_def disjoint_family_def b split_if_mem2) 
+             simp add: measure_set_def disjoint_family_on_def b split_if_mem2) 
 qed  
 
 lemma (in algebra) inf_measure_pos0:
@@ -622,7 +625,7 @@
   fix x y
   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   hence "disjoint_family (binaryset x y)"
-    by (auto simp add: disjoint_family_def binaryset_def) 
+    by (auto simp add: disjoint_family_on_def binaryset_def) 
   hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
          (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
          f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
@@ -655,7 +658,7 @@
       show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
         by blast
       show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
-        by (auto simp add: disjoint_family_def)
+        by (auto simp add: disjoint_family_on_def)
       show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
         by (metis UN_extend_simps(4) s seq)
     qed
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Probability/Lebesgue.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Lebesgue.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -0,0 +1,1790 @@
+header {*Lebesgue Integration*}
+
+theory Lebesgue
+imports Measure Borel
+begin
+
+text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*}
+
+definition
+  "pos_part f = (\<lambda>x. max 0 (f x))"
+
+definition
+  "neg_part f = (\<lambda>x. - min 0 (f x))"
+
+definition
+  "nonneg f = (\<forall>x. 0 \<le> f x)"
+
+lemma nonneg_pos_part[intro!]:
+  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,zero}"
+  shows "nonneg (pos_part f)"
+  unfolding nonneg_def pos_part_def by auto
+
+lemma nonneg_neg_part[intro!]:
+  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,ordered_ab_group_add}"
+  shows "nonneg (neg_part f)"
+  unfolding nonneg_def neg_part_def min_def by auto
+
+context measure_space
+begin
+
+definition
+ "pos_simple f =
+  { (s :: nat set, a, x).
+    finite s \<and> nonneg f \<and> nonneg x \<and> a ` s \<subseteq> sets M \<and>
+    (\<forall>t \<in> space M. (\<exists>!i\<in>s. t\<in>a i) \<and> (\<forall>i\<in>s. t \<in> a i \<longrightarrow> f t = x i)) }"
+
+definition
+  "pos_simple_integral \<equiv> \<lambda>(s, a, x). \<Sum> i \<in> s. x i * measure M (a i)"
+
+definition
+  "psfis f = pos_simple_integral ` (pos_simple f)"
+
+definition
+  "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
+                        (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
+
+definition
+  "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
+
+definition
+  "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
+
+definition
+  "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
+
+definition
+  "countable_space_integral f \<equiv>
+    let e = enumerate (f ` space M) in
+      suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
+
+definition
+  "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
+    f \<in> borel_measurable M \<and>
+    (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
+
+lemma pos_simpleE[consumes 1]:
+  assumes ps: "(s, a, x) \<in> pos_simple f"
+  obtains "finite s" and "nonneg f" and "nonneg x"
+    and "a ` s \<subseteq> sets M" and "(\<Union>i\<in>s. a i) = space M"
+    and "disjoint_family_on a s"
+    and "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
+    and "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
+proof
+  show "finite s" and "nonneg f" and "nonneg x"
+    and as_in_M: "a ` s \<subseteq> sets M"
+    and *: "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
+    and **: "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
+    using ps unfolding pos_simple_def by auto
+
+  thus t: "(\<Union>i\<in>s. a i) = space M"
+  proof safe
+    fix x assume "x \<in> space M"
+    from *[OF this] show "x \<in> (\<Union>i\<in>s. a i)" by auto
+  next
+    fix t i assume "i \<in> s"
+    hence "a i \<in> sets M" using as_in_M by auto
+    moreover assume "t \<in> a i"
+    ultimately show "t \<in> space M" using sets_into_space by blast
+  qed
+
+  show "disjoint_family_on a s" unfolding disjoint_family_on_def
+  proof safe
+    fix i j and t assume "i \<in> s" "t \<in> a i" and "j \<in> s" "t \<in> a j" and "i \<noteq> j"
+    with t * show "t \<in> {}" by auto
+  qed
+qed
+
+lemma pos_simple_cong:
+  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
+  shows "pos_simple f = pos_simple g"
+  unfolding pos_simple_def using assms by auto
+
+lemma psfis_cong:
+  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
+  shows "psfis f = psfis g"
+  unfolding psfis_def using pos_simple_cong[OF assms] by simp
+
+lemma pos_simple_setsum_indicator_fn:
+  assumes ps: "(s, a, x) \<in> pos_simple f"
+  and "t \<in> space M"
+  shows "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) = f t"
+proof -
+  from assms obtain i where *: "i \<in> s" "t \<in> a i"
+    and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE)
+
+  have **: "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) =
+    (\<Sum>j\<in>s. if j \<in> {i} then x i else 0)"
+    unfolding indicator_fn_def using assms *
+    by (auto intro!: setsum_cong elim!: pos_simpleE)
+  show ?thesis unfolding ** setsum_cases[OF `finite s`] xi
+    using `i \<in> s` by simp
+qed
+
+lemma (in measure_space) measure_setsum_split:
+  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
+  assumes "(\<Union>i \<in> r. b i) = space M"
+  assumes "disjoint_family_on b r"
+  shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
+proof -
+  have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
+    using assms by auto
+  show ?thesis unfolding *
+  proof (rule measure_finitely_additive''[symmetric])
+    show "finite r" using `finite r` by auto
+    { fix i assume "i \<in> r"
+      hence "b i \<in> sets M" using br_in_M by auto
+      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
+    }
+    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
+      using `disjoint_family_on b r`
+      unfolding disjoint_family_on_def by auto
+  qed
+qed
+
+lemma (in measure_space) pos_simple_common_partition:
+  assumes psf: "(s, a, x) \<in> pos_simple f"
+  assumes psg: "(s', b, y) \<in> pos_simple g"
+  obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
+proof -
+  (* definitions *)
+
+  def k == "{0 ..< card (s \<times> s')}"
+  have fs: "finite s" "finite s'" "finite k" unfolding k_def
+    using psf psg unfolding pos_simple_def by auto
+  hence "finite (s \<times> s')" by simp
+  then obtain p where p: "p ` k = s \<times> s'" "inj_on p k"
+    using ex_bij_betw_nat_finite[of "s \<times> s'"] unfolding bij_betw_def k_def by blast
+  def c == "\<lambda> i. a (fst (p i)) \<inter> b (snd (p i))"
+  def z == "\<lambda> i. x (fst (p i))"
+  def z' == "\<lambda> i. y (snd (p i))"
+
+  have "finite k" unfolding k_def by simp
+
+  have "nonneg z" and "nonneg z'"
+    using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto
+
+  have ck_subset_M: "c ` k \<subseteq> sets M"
+  proof
+    fix x assume "x \<in> c ` k"
+    then obtain j where "j \<in> k" and "x = c j" by auto
+    hence "p j \<in> s \<times> s'" using p(1) by auto
+    hence "a (fst (p j)) \<in> sets M" (is "?a \<in> _")
+      and "b (snd (p j)) \<in> sets M" (is "?b \<in> _")
+      using psf psg unfolding pos_simple_def by auto
+    thus "x \<in> sets M" unfolding `x = c j` c_def using Int by simp
+  qed
+
+  { fix t assume "t \<in> space M"
+    hence ex1s: "\<exists>!i\<in>s. t \<in> a i" and ex1s': "\<exists>!i\<in>s'. t \<in> b i"
+      using psf psg unfolding pos_simple_def by auto
+    then obtain j j' where j: "j \<in> s" "t \<in> a j" and j': "j' \<in> s'" "t \<in> b j'"
+      by auto
+    then obtain i :: nat where i: "(j,j') = p i" and "i \<in> k" using p by auto
+    have "\<exists>!i\<in>k. t \<in> c i"
+    proof (rule ex1I[of _ i])
+      show "\<And>x. x \<in> k \<Longrightarrow> t \<in> c x \<Longrightarrow> x = i"
+      proof -
+        fix l assume "l \<in> k" "t \<in> c l"
+        hence "p l \<in> s \<times> s'" and t_in: "t \<in> a (fst (p l))" "t \<in> b (snd (p l))"
+          using p unfolding c_def by auto
+        hence "fst (p l) \<in> s" and "snd (p l) \<in> s'" by auto
+        with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto)
+        thus "l = i"
+          using `(j, j') = p i` p(2)[THEN inj_onD] `l \<in> k` `i \<in> k` by auto
+      qed
+
+      show "i \<in> k \<and> t \<in> c i"
+        using `i \<in> k` `t \<in> a j` `t \<in> b j'` c_def i[symmetric] by auto
+    qed auto
+  } note ex1 = this
+
+  show thesis
+  proof (rule that)
+    { fix t i assume "t \<in> space M" and "i \<in> k"
+      hence "p i \<in> s \<times> s'" using p(1) by auto
+      hence "fst (p i) \<in> s" by auto
+      moreover
+      assume "t \<in> c i"
+      hence "t \<in> a (fst (p i))" unfolding c_def by auto
+      ultimately have "f t = z i" using psf `t \<in> space M`
+        unfolding z_def pos_simple_def by auto
+    }
+    thus "(k, c, z) \<in> pos_simple f"
+      using psf `finite k` `nonneg z` ck_subset_M ex1
+      unfolding pos_simple_def by auto
+
+    { fix t i assume "t \<in> space M" and "i \<in> k"
+      hence "p i \<in> s \<times> s'" using p(1) by auto
+      hence "snd (p i) \<in> s'" by auto
+      moreover
+      assume "t \<in> c i"
+      hence "t \<in> b (snd (p i))" unfolding c_def by auto
+      ultimately have "g t = z' i" using psg `t \<in> space M`
+        unfolding z'_def pos_simple_def by auto
+    }
+    thus "(k, c, z') \<in> pos_simple g"
+      using psg `finite k` `nonneg z'` ck_subset_M ex1
+      unfolding pos_simple_def by auto
+  qed
+qed
+
+lemma (in measure_space) pos_simple_integral_equal:
+  assumes psx: "(s, a, x) \<in> pos_simple f"
+  assumes psy: "(s', b, y) \<in> pos_simple f"
+  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
+  unfolding pos_simple_integral_def
+proof simp
+  have "(\<Sum>i\<in>s. x i * measure M (a i)) =
+    (\<Sum>i\<in>s. (\<Sum>j \<in> s'. x i * measure M (a i \<inter> b j)))" (is "?left = _")
+    using psy psx unfolding setsum_right_distrib[symmetric]
+    by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE)
+  also have "... = (\<Sum>i\<in>s. (\<Sum>j \<in> s'. y j * measure M (a i \<inter> b j)))"
+  proof (rule setsum_cong, simp, rule setsum_cong, simp_all)
+    fix i j assume i: "i \<in> s" and j: "j \<in> s'"
+    hence "a i \<in> sets M" using psx by (auto elim!: pos_simpleE)
+
+    show "measure M (a i \<inter> b j) = 0 \<or> x i = y j"
+    proof (cases "a i \<inter> b j = {}")
+      case True thus ?thesis using empty_measure by simp
+    next
+      case False then obtain t where t: "t \<in> a i" "t \<in> b j" by auto
+      hence "t \<in> space M" using `a i \<in> sets M` sets_into_space by auto
+      with psx psy t i j have "x i = f t" and "y j = f t"
+        unfolding pos_simple_def by auto
+      thus ?thesis by simp
+    qed
+  qed
+  also have "... = (\<Sum>j\<in>s'. (\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)))"
+    by (subst setsum_commute) simp
+  also have "... = (\<Sum>i\<in>s'. y i * measure M (b i))" (is "?sum_sum = ?right")
+  proof (rule setsum_cong)
+    fix j assume "j \<in> s'"
+    have "y j * measure M (b j) = (\<Sum>i\<in>s. y j * measure M (b j \<inter> a i))"
+      using psx psy `j \<in> s'` unfolding setsum_right_distrib[symmetric]
+      by (auto intro!: measure_setsum_split elim!: pos_simpleE)
+    thus "(\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)) = y j * measure M (b j)"
+      by (auto intro!: setsum_cong arg_cong[where f="measure M"])
+  qed simp
+  finally show "?left = ?right" .
+qed
+
+lemma (in measure_space)psfis_present:
+  assumes "A \<in> psfis f"
+  assumes "B \<in> psfis g"
+  obtains z z' c k where
+  "A = pos_simple_integral (k, c, z)"
+  "B = pos_simple_integral (k, c, z')"
+  "(k, c, z) \<in> pos_simple f"
+  "(k, c, z') \<in> pos_simple g"
+using assms
+proof -
+  from assms obtain s a x s' b y where
+    ps: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g" and
+    A: "A = pos_simple_integral (s, a, x)" and
+    B: "B = pos_simple_integral (s', b, y)"
+    unfolding psfis_def pos_simple_integral_def by auto
+
+  guess z z' c k using pos_simple_common_partition[OF ps] . note part = this
+  show thesis
+  proof (rule that[of k c z z', OF _ _ part])
+    show "A = pos_simple_integral (k, c, z)"
+      unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)])
+    show "B = pos_simple_integral (k, c, z')"
+      unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)])
+  qed
+qed
+
+lemma (in measure_space) pos_simple_integral_add:
+  assumes "(s, a, x) \<in> pos_simple f"
+  assumes "(s', b, y) \<in> pos_simple g"
+  obtains s'' c z where
+    "(s'', c, z) \<in> pos_simple (\<lambda>x. f x + g x)"
+    "(pos_simple_integral (s, a, x) +
+      pos_simple_integral (s', b, y) =
+      pos_simple_integral (s'', c, z))"
+using assms
+proof -
+  guess z z' c k
+    by (rule pos_simple_common_partition[OF `(s, a, x) \<in> pos_simple f ` `(s', b, y) \<in> pos_simple g`])
+  note kczz' = this
+  have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
+    by (rule pos_simple_integral_equal) (fact, fact)
+  have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')"
+    by (rule pos_simple_integral_equal) (fact, fact)
+
+  have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
+    = (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
+    unfolding pos_simple_integral_def by auto
+  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
+  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
+  also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
+  finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
+    pos_simple_integral (k, c, (\<lambda> x. z x + z' x))" using x y by auto
+  show ?thesis
+    apply (rule that[of k c "(\<lambda> x. z x + z' x)", OF _ ths])
+    using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg)
+qed
+
+lemma psfis_add:
+  assumes "a \<in> psfis f" "b \<in> psfis g"
+  shows "a + b \<in> psfis (\<lambda>x. f x + g x)"
+using assms pos_simple_integral_add
+unfolding psfis_def by auto blast
+
+lemma pos_simple_integral_mono_on_mspace:
+  assumes f: "(s, a, x) \<in> pos_simple f"
+  assumes g: "(s', b, y) \<in> pos_simple g"
+  assumes mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
+  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
+using assms
+proof -
+  guess z z' c k by (rule pos_simple_common_partition[OF f g])
+  note kczz' = this
+  (* w = z and w' = z'  except where c _ = {} or undef *)
+  def w == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z i"
+  def w' == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z' i"
+  { fix i
+    have "w i \<le> w' i"
+    proof (cases "i \<notin> k \<or> c i = {}")
+      case False hence "i \<in> k" "c i \<noteq> {}" by auto
+      then obtain v where v: "v \<in> c i" and "c i \<in> sets M"
+        using kczz'(1) unfolding pos_simple_def by blast
+      hence "v \<in> space M" using sets_into_space by blast
+      with mono[OF `v \<in> space M`] kczz' `i \<in> k` `v \<in> c i`
+      have "z i \<le> z' i" unfolding pos_simple_def by simp
+      thus ?thesis unfolding w_def w'_def using False by auto
+    next
+      case True thus ?thesis unfolding w_def w'_def by auto
+   qed
+  } note w_mn = this
+
+  (* some technical stuff for the calculation*)
+  have "\<And> i. i \<in> k \<Longrightarrow> c i \<in> sets M" using kczz' unfolding pos_simple_def by auto
+  hence "\<And> i. i \<in> k \<Longrightarrow> measure M (c i) \<ge> 0" using positive by auto
+  hence w_mono: "\<And> i. i \<in> k \<Longrightarrow> w i * measure M (c i) \<le> w' i * measure M (c i)"
+    using mult_right_mono w_mn by blast
+
+  { fix i have "\<lbrakk>i \<in> k ; z i \<noteq> w i\<rbrakk> \<Longrightarrow> measure M (c i) = 0"
+      unfolding w_def by (cases "c i = {}") auto }
+  hence zw: "\<And> i. i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)" by auto
+
+  { fix i have "i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)"
+      unfolding w_def by (cases "c i = {}") simp_all }
+  note zw = this
+
+  { fix i have "i \<in> k \<Longrightarrow> z' i * measure M (c i) = w' i * measure M (c i)"
+      unfolding w'_def by (cases "c i = {}") simp_all }
+  note z'w' = this
+
+  (* the calculation *)
+  have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
+    using f kczz'(1) by (rule pos_simple_integral_equal)
+  also have "\<dots> = (\<Sum> i \<in> k. z i * measure M (c i))"
+    unfolding pos_simple_integral_def by auto
+  also have "\<dots> = (\<Sum> i \<in> k. w i * measure M (c i))"
+    using setsum_cong2[of k, OF zw] by auto
+  also have "\<dots> \<le> (\<Sum> i \<in> k. w' i * measure M (c i))"
+    using setsum_mono[OF w_mono, of k] by auto
+  also have "\<dots> = (\<Sum> i \<in> k. z' i * measure M (c i))"
+    using setsum_cong2[of k, OF z'w'] by auto
+  also have "\<dots> = pos_simple_integral (k, c, z')"
+    unfolding pos_simple_integral_def by auto
+  also have "\<dots> = pos_simple_integral (s', b, y)"
+    using kczz'(2) g by (rule pos_simple_integral_equal)
+  finally show "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
+    by simp
+qed
+
+lemma pos_simple_integral_mono:
+  assumes a: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g"
+  assumes "\<And> z. f z \<le> g z"
+  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
+using assms pos_simple_integral_mono_on_mspace by auto
+
+lemma psfis_mono:
+  assumes "a \<in> psfis f" "b \<in> psfis g"
+  assumes "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
+  shows "a \<le> b"
+using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto
+
+lemma pos_simple_fn_integral_unique:
+  assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
+  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
+using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
+
+lemma psfis_unique:
+  assumes "a \<in> psfis f" "b \<in> psfis f"
+  shows "a = b"
+using assms real_le_antisym real_le_refl psfis_mono by metis
+
+lemma pos_simple_integral_indicator:
+  assumes "A \<in> sets M"
+  obtains s a x where
+  "(s, a, x) \<in> pos_simple (indicator_fn A)"
+  "measure M A = pos_simple_integral (s, a, x)"
+using assms
+proof -
+  def s == "{0, 1} :: nat set"
+  def a == "\<lambda> i :: nat. if i = 0 then A else space M - A"
+  def x == "\<lambda> i :: nat. if i = 0 then 1 else (0 :: real)"
+  have eq: "pos_simple_integral (s, a, x) = measure M A"
+    unfolding s_def a_def x_def pos_simple_integral_def by auto
+  have "(s, a, x) \<in> pos_simple (indicator_fn A)"
+    unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def
+    using assms sets_into_space by auto
+   from that[OF this] eq show thesis by auto
+qed
+
+lemma psfis_indicator:
+  assumes "A \<in> sets M"
+  shows "measure M A \<in> psfis (indicator_fn A)"
+using pos_simple_integral_indicator[OF assms]
+  unfolding psfis_def image_def by auto
+
+lemma pos_simple_integral_mult:
+  assumes f: "(s, a, x) \<in> pos_simple f"
+  assumes "0 \<le> z"
+  obtains s' b y where
+  "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
+  "pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)"
+  using assms that[of s a "\<lambda>i. z * x i"]
+  by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg)
+
+lemma psfis_mult:
+  assumes "r \<in> psfis f"
+  assumes "0 \<le> z"
+  shows "z * r \<in> psfis (\<lambda>x. z * f x)"
+using assms
+proof -
+  from assms obtain s a x
+    where sax: "(s, a, x) \<in> pos_simple f"
+    and r: "r = pos_simple_integral (s, a, x)"
+    unfolding psfis_def image_def by auto
+  obtain s' b y where
+    "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
+    "z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
+    using pos_simple_integral_mult[OF sax `0 \<le> z`, of thesis] by auto
+  thus ?thesis using r unfolding psfis_def image_def by auto
+qed
+
+lemma pos_simple_integral_setsum_image:
+  assumes "finite P"
+  assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
+  obtains s' a' x' where
+  "(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
+  "pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
+using assms that
+proof (induct P arbitrary:thesis rule:finite.induct)
+  case emptyI note asms = this
+  def s' == "{0 :: nat}"
+  def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
+  def x' == "\<lambda> x :: nat. (0 :: real)"
+  have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
+    unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
+  moreover have "pos_simple_integral (s', a', x') = 0"
+    unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
+  ultimately show ?case using asms by auto
+next
+
+  case (insertI P c) note asms = this
+  then obtain s' a' x' where
+    sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
+         "pos_simple_integral (s', a', x') =
+             (\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
+    by auto
+
+  { assume "c \<in> P"
+    hence "P = insert c P" by auto
+    hence thesis using asms sax by auto
+  }
+  moreover
+  { assume "c \<notin> P"
+    from asms obtain s'' a'' x'' where
+      sax': "s'' = s c" "a'' = a c" "x'' = x c"
+            "(s'', a'', x'') \<in> pos_simple (f c)" by auto
+    from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
+      tybbie:
+      "(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
+      "(pos_simple_integral (s', a', x') +
+      pos_simple_integral (s'', a'', x'') =
+      pos_simple_integral (k, b, z))"
+      using pos_simple_integral_add by blast
+
+    from tybbie have
+      "pos_simple_integral (k, b, z) =
+      pos_simple_integral (s', a', x') +
+      pos_simple_integral (s'', a'', x'')" by simp
+    also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
+                  + pos_simple_integral (s c, a c, x c)"
+      using sax sax' by auto
+    also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
+      using asms `c \<notin> P` by auto
+    finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
+      by simp
+
+    have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
+      using `c \<notin> P` `finite P` by auto
+    hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
+      using tybbie by simp
+
+    from A B have thesis using asms by auto
+    } ultimately show thesis by blast
+qed
+
+lemma psfis_setsum_image:
+  assumes "finite P"
+  assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
+  shows "(setsum a P) \<in> psfis (\<lambda>t. \<Sum>i \<in> P. f i t)"
+using assms
+proof (induct P)
+  case empty
+  let ?s = "{0 :: nat}"
+  let ?a = "\<lambda> i. if i = (0 :: nat) then space M else {}"
+  let ?x = "\<lambda> (i :: nat). (0 :: real)"
+  have "(?s, ?a, ?x) \<in> pos_simple (\<lambda> t. (0 :: real))"
+    unfolding pos_simple_def image_def nonneg_def by auto
+  moreover have "(\<Sum> i \<in> ?s. ?x i * measure M (?a i)) = 0" by auto
+  ultimately have "0 \<in> psfis (\<lambda> t. 0)"
+    unfolding psfis_def image_def pos_simple_integral_def nonneg_def
+    by (auto intro!:bexI[of _ "(?s, ?a, ?x)"])
+  thus ?case by auto
+next
+  case (insert x P) note asms = this
+  have "finite P" by fact
+  have "x \<notin> P" by fact
+  have "(\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)) \<Longrightarrow>
+    setsum a P \<in> psfis (\<lambda>t. \<Sum>i\<in>P. f i t)" by fact
+  have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \<notin> P` by auto
+  also have "\<dots> \<in> psfis (\<lambda> t. f x t + (\<Sum> i \<in> P. f i t))"
+    using asms psfis_add by auto
+  also have "\<dots> = psfis (\<lambda> t. \<Sum> i \<in> insert x P. f i t)"
+    using `x \<notin> P` `finite P` by auto
+  finally show ?case by simp
+qed
+
+lemma psfis_intro:
+  assumes "a ` P \<subseteq> sets M" and "nonneg x" and "finite P"
+  shows "(\<Sum>i\<in>P. x i * measure M (a i)) \<in> psfis (\<lambda>t. \<Sum>i\<in>P. x i * indicator_fn (a i) t)"
+using assms psfis_mult psfis_indicator
+unfolding image_def nonneg_def
+by (auto intro!:psfis_setsum_image)
+
+lemma psfis_nonneg: "a \<in> psfis f \<Longrightarrow> nonneg f"
+unfolding psfis_def pos_simple_def by auto
+
+lemma pos_psfis: "r \<in> psfis f \<Longrightarrow> 0 \<le> r"
+unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
+using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
+
+lemma pos_part_neg_part_borel_measurable:
+  assumes "f \<in> borel_measurable M"
+  shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
+using assms
+proof -
+  { fix a :: real
+    { assume asm: "0 \<le> a"
+      from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
+      have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
+        unfolding pos_part_def using assms borel_measurable_le_iff by auto
+      hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
+    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
+      unfolding pos_part_def using empty_sets by auto
+    ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
+      using le_less_linear by auto
+  } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+  { fix a :: real
+    { assume asm: "0 \<le> a"
+      from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
+      have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
+        unfolding neg_part_def using assms borel_measurable_ge_iff by auto
+      hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
+    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
+    moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
+    ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
+      using le_less_linear by auto
+  } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
+  from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
+qed
+
+lemma pos_part_neg_part_borel_measurable_iff:
+  "f \<in> borel_measurable M \<longleftrightarrow>
+  pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
+proof -
+  { fix x
+    have "f x = pos_part f x - neg_part f x"
+      unfolding pos_part_def neg_part_def unfolding max_def min_def
+      by auto }
+  hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
+  hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
+  from pos_part_neg_part_borel_measurable[of f]
+    borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
+    this
+  show ?thesis by auto
+qed
+
+lemma borel_measurable_cong:
+  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
+  shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
+using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
+
+lemma psfis_borel_measurable:
+  assumes "a \<in> psfis f"
+  shows "f \<in> borel_measurable M"
+using assms
+proof -
+  from assms obtain s a' x where sa'x: "(s, a', x) \<in> pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a"
+    and fs: "finite s"
+    unfolding psfis_def pos_simple_integral_def image_def
+    by (auto elim:pos_simpleE)
+  { fix w assume "w \<in> space M"
+    hence "(f w \<le> a) = ((\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
+      using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp
+  } hence "\<And> w. (w \<in> space M \<and> f w \<le> a) = (w \<in> space M \<and> (\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
+    by auto
+  { fix i assume "i \<in> s"
+    hence "indicator_fn (a' i) \<in> borel_measurable M"
+      using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
+    hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
+      using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
+        real_mult_commute by auto }
+  from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
+  have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
+  from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
+  show ?thesis by simp
+qed
+
+lemma mono_conv_outgrow:
+  assumes "incseq x" "x ----> y" "z < y"
+  shows "\<exists>b. \<forall> a \<ge> b. z < x a"
+using assms
+proof -
+  from assms have "y - z > 0" by simp
+  hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
+    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
+    by simp
+  have "\<forall>m. x m \<le> y" using incseq_le assms by auto
+  hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
+    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
+  from A B show ?thesis by auto
+qed
+
+lemma psfis_mono_conv_mono:
+  assumes mono: "mono_convergent u f (space M)"
+  and ps_u: "\<And>n. x n \<in> psfis (u n)"
+  and "x ----> y"
+  and "r \<in> psfis s"
+  and f_upper_bound: "\<And>t. t \<in> space M \<Longrightarrow> s t \<le> f t"
+  shows "r <= y"
+proof (rule field_le_mult_one_interval)
+  fix z :: real assume "0 < z" and "z < 1"
+  hence "0 \<le> z" by auto
+(*  def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
+  let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
+
+  have "incseq x" unfolding incseq_def
+  proof safe
+    fix m n :: nat assume "m \<le> n"
+    show "x m \<le> x n"
+    proof (rule psfis_mono[OF `x m \<in> psfis (u m)` `x n \<in> psfis (u n)`])
+      fix t assume "t \<in> space M"
+      with mono_convergentD[OF mono this] `m \<le> n` show "u m t \<le> u n t"
+        unfolding incseq_def by auto
+    qed
+  qed
+
+  from `r \<in> psfis s`
+  obtain s' a x' where r: "r = pos_simple_integral (s', a, x')"
+    and ps_s: "(s', a, x') \<in> pos_simple s"
+    unfolding psfis_def by auto
+
+  { fix t i assume "i \<in> s'" "t \<in> a i"
+    hence "t \<in> space M" using ps_s by (auto elim!: pos_simpleE) }
+  note t_in_space = this
+
+  { fix n
+    from psfis_borel_measurable[OF `r \<in> psfis s`]
+       psfis_borel_measurable[OF ps_u]
+    have "?B' n \<in> sets M"
+      by (auto intro!:
+        borel_measurable_leq_borel_measurable
+        borel_measurable_times_borel_measurable
+        borel_measurable_const) }
+  note B'_in_M = this
+
+  { fix n have "(\<lambda>i. a i \<inter> ?B' n) ` s' \<subseteq> sets M" using B'_in_M ps_s
+      by (auto intro!: Int elim!: pos_simpleE) }
+  note B'_inter_a_in_M = this
+
+  let "?sum n" = "(\<Sum>i\<in>s'. x' i * measure M (a i \<inter> ?B' n))"
+  { fix n
+    have "z * ?sum n \<le> x n"
+    proof (rule psfis_mono[OF _ ps_u])
+      have *: "\<And>i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) =
+        x' i * indicator_fn (a i \<inter> ?B' n) t" unfolding indicator_fn_def by auto
+      have ps': "?sum n \<in> psfis (\<lambda>t. indicator_fn (?B' n) t * (\<Sum>i\<in>s'. x' i * indicator_fn (a i) t))"
+        unfolding setsum_right_distrib * using B'_in_M ps_s
+        by (auto intro!: psfis_intro Int elim!: pos_simpleE)
+      also have "... = psfis (\<lambda>t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r")
+      proof (rule psfis_cong)
+        show "nonneg ?l" using psfis_nonneg[OF ps'] .
+        show "nonneg ?r" using psfis_nonneg[OF `r \<in> psfis s`] unfolding nonneg_def indicator_fn_def by auto
+        fix t assume "t \<in> space M"
+        show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \<in> space M`] ..
+      qed
+      finally show "z * ?sum n \<in> psfis (\<lambda>t. z * ?r t)" using psfis_mult[OF _ `0 \<le> z`] by simp
+    next
+      fix t assume "t \<in> space M"
+      show "z * (indicator_fn (?B' n) t * s t) \<le> u n t"
+         using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto
+    qed }
+  hence *: "\<exists>N. \<forall>n\<ge>N. z * ?sum n \<le> x n" by (auto intro!: exI[of _ 0])
+
+  show "z * r \<le> y" unfolding r pos_simple_integral_def
+  proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x ----> y` *],
+         simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ)
+    fix i assume "i \<in> s'"
+    from psfis_nonneg[OF `r \<in> psfis s`, unfolded nonneg_def]
+    have "\<And>t. 0 \<le> s t" by simp
+
+    have *: "(\<Union>j. a i \<inter> ?B' j) = a i"
+    proof (safe, simp, safe)
+      fix t assume "t \<in> a i"
+      thus "t \<in> space M" using t_in_space[OF `i \<in> s'`] by auto
+      show "\<exists>j. z * s t \<le> u j t"
+      proof (cases "s t = 0")
+        case True thus ?thesis
+          using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto
+      next
+        case False with `0 \<le> s t`
+        have "0 < s t" by auto
+        hence "z * s t < 1 * s t" using `0 < z` `z < 1`
+          by (auto intro!: mult_strict_right_mono simp del: mult_1_left)
+        also have "... \<le> f t" using f_upper_bound `t \<in> space M` by auto
+        finally obtain b where "\<And>j. b \<le> j \<Longrightarrow> z * s t < u j t" using `t \<in> space M`
+          using mono_conv_outgrow[of "\<lambda>n. u n t" "f t" "z * s t"]
+          using mono_convergentD[OF mono] by auto
+        from this[of b] show ?thesis by (auto intro!: exI[of _ b])
+      qed
+    qed
+
+    show "(\<lambda>n. measure M (a i \<inter> ?B' n)) ----> measure M (a i)"
+    proof (safe intro!:
+        monotone_convergence[of "\<lambda>n. a i \<inter> ?B' n", unfolded comp_def *])
+      fix n show "a i \<inter> ?B' n \<in> sets M"
+        using B'_inter_a_in_M[of n] `i \<in> s'` by auto
+    next
+      fix j t assume "t \<in> space M" and "z * s t \<le> u j t"
+      thus "z * s t \<le> u (Suc j) t"
+        using mono_convergentD(1)[OF mono, unfolded incseq_def,
+          rule_format, of t j "Suc j"]
+        by auto
+    qed
+  qed
+qed
+
+lemma psfis_nnfis:
+  "a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
+  unfolding nnfis_def mono_convergent_def incseq_def
+  by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
+
+lemma nnfis_times:
+  assumes "a \<in> nnfis f" and "0 \<le> z"
+  shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
+proof -
+  obtain u x where "mono_convergent u f (space M)" and
+    "\<And>n. x n \<in> psfis (u n)" "x ----> a"
+    using `a \<in> nnfis f` unfolding nnfis_def by auto
+  with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
+    by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
+      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
+qed
+
+lemma nnfis_add:
+  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
+  shows "a + b \<in> nnfis (\<lambda>t. f t + g t)"
+proof -
+  obtain u x w y
+    where "mono_convergent u f (space M)" and
+    "\<And>n. x n \<in> psfis (u n)" "x ----> a" and
+    "mono_convergent w g (space M)" and
+    "\<And>n. y n \<in> psfis (w n)" "y ----> b"
+    using `a \<in> nnfis f` `b \<in> nnfis g` unfolding nnfis_def by auto
+  thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def
+    by (auto intro!: exI[of _ "\<lambda>n a. u n a + w n a"] exI[of _ "\<lambda>n. x n + y n"]
+      LIMSEQ_add LIMSEQ_const psfis_add add_mono)
+qed
+
+lemma nnfis_mono:
+  assumes nnfis: "a \<in> nnfis f" "b \<in> nnfis g"
+  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+  shows "a \<le> b"
+proof -
+  obtain u x w y where
+    mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and
+    psfis: "\<And>n. x n \<in> psfis (u n)" "\<And>n. y n \<in> psfis (w n)" and
+    limseq: "x ----> a" "y ----> b" using nnfis unfolding nnfis_def by auto
+  show ?thesis
+  proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe)
+    fix n
+    show "x n \<le> b"
+    proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)])
+      fix t assume "t \<in> space M"
+      from mono_convergent_le[OF mc(1) this] mono[OF this]
+      show "u n t \<le> g t" by (rule order_trans)
+    qed
+  qed
+qed
+
+lemma nnfis_unique:
+  assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
+  shows "a = b"
+  using nnfis_mono[OF a b] nnfis_mono[OF b a]
+  by (auto intro!: real_le_antisym[of a b])
+
+lemma psfis_equiv:
+  assumes "a \<in> psfis f" and "nonneg g"
+  and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
+  shows "a \<in> psfis g"
+  using assms unfolding psfis_def pos_simple_def by auto
+
+lemma psfis_mon_upclose:
+  assumes "\<And>m. a m \<in> psfis (u m)"
+  shows "\<exists>c. c \<in> psfis (mon_upclose n u)"
+proof (induct n)
+  case 0 thus ?case unfolding mon_upclose.simps using assms ..
+next
+  case (Suc n)
+  then obtain sn an xn where ps: "(sn, an, xn) \<in> pos_simple (mon_upclose n u)"
+    unfolding psfis_def by auto
+  obtain ss as xs where ps': "(ss, as, xs) \<in> pos_simple (u (Suc n))"
+    using assms[of "Suc n"] unfolding psfis_def by auto
+  from pos_simple_common_partition[OF ps ps'] guess x x' a s .
+  hence "(s, a, upclose x x') \<in> pos_simple (mon_upclose (Suc n) u)"
+    by (simp add: upclose_def pos_simple_def nonneg_def max_def)
+  thus ?case unfolding psfis_def by auto
+qed
+
+text {* Beppo-Levi monotone convergence theorem *}
+lemma nnfis_mon_conv:
+  assumes mc: "mono_convergent f h (space M)"
+  and nnfis: "\<And>n. x n \<in> nnfis (f n)"
+  and "x ----> z"
+  shows "z \<in> nnfis h"
+proof -
+  have "\<forall>n. \<exists>u y. mono_convergent u (f n) (space M) \<and> (\<forall>m. y m \<in> psfis (u m)) \<and>
+    y ----> x n"
+    using nnfis unfolding nnfis_def by auto
+  from choice[OF this] guess u ..
+  from choice[OF this] guess y ..
+  hence mc_u: "\<And>n. mono_convergent (u n) (f n) (space M)"
+    and psfis: "\<And>n m. y n m \<in> psfis (u n m)" and "\<And>n. y n ----> x n"
+    by auto
+
+  let "?upclose n" = "mon_upclose n (\<lambda>m. u m n)"
+
+  have "\<exists>c. \<forall>n. c n \<in> psfis (?upclose n)"
+    by (safe intro!: choice psfis_mon_upclose) (rule psfis)
+  then guess c .. note c = this[rule_format]
+
+  show ?thesis unfolding nnfis_def
+  proof (safe intro!: exI)
+    show mc_upclose: "mono_convergent ?upclose h (space M)"
+      by (rule mon_upclose_mono_convergent[OF mc_u mc])
+    show psfis_upclose: "\<And>n. c n \<in> psfis (?upclose n)"
+      using c .
+
+    { fix n m :: nat assume "n \<le> m"
+      hence "c n \<le> c m"
+        using psfis_mono[OF c c]
+        using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def]
+        by auto }
+    hence "incseq c" unfolding incseq_def by auto
+
+    { fix n
+      have c_nnfis: "c n \<in> nnfis (?upclose n)" using c by (rule psfis_nnfis)
+      from nnfis_mono[OF c_nnfis nnfis]
+        mon_upclose_le_mono_convergent[OF mc_u]
+        mono_convergentD(1)[OF mc]
+      have "c n \<le> x n" by fast }
+    note c_less_x = this
+
+    { fix n
+      note c_less_x[of n]
+      also have "x n \<le> z"
+      proof (rule incseq_le)
+        show "x ----> z" by fact
+        from mono_convergentD(1)[OF mc]
+        show "incseq x" unfolding incseq_def
+          by (auto intro!: nnfis_mono[OF nnfis nnfis])
+      qed
+      finally have "c n \<le> z" . }
+    note c_less_z = this
+
+    have "convergent c"
+    proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]])
+      show "Bseq c"
+        using pos_psfis[OF c] c_less_z
+        by (auto intro!: BseqI'[of _ z])
+      show "incseq c" by fact
+    qed
+    then obtain l where l: "c ----> l" unfolding convergent_def by auto
+
+    have "l \<le> z" using c_less_x l
+      by (auto intro!: LIMSEQ_le[OF _ `x ----> z`])
+    moreover have "z \<le> l"
+    proof (rule LIMSEQ_le_const2[OF `x ----> z`], safe intro!: exI[of _ 0])
+      fix n
+      have "l \<in> nnfis h"
+        unfolding nnfis_def using l mc_upclose psfis_upclose by auto
+      from nnfis this mono_convergent_le[OF mc]
+      show "x n \<le> l" by (rule nnfis_mono)
+    qed
+    ultimately have "l = z" by (rule real_le_antisym)
+    thus "c ----> z" using `c ----> l` by simp
+  qed
+qed
+
+lemma nnfis_pos_on_mspace:
+  assumes "a \<in> nnfis f" and "x \<in>space M"
+  shows "0 \<le> f x"
+using assms
+proof -
+  from assms[unfolded nnfis_def] guess u y by auto note uy = this
+  hence "\<And> n. 0 \<le> u n x" 
+    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
+    by auto
+  thus "0 \<le> f x" using uy[rule_format]
+    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
+    using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
+    by fast
+qed
+
+lemma nnfis_borel_measurable:
+  assumes "a \<in> nnfis f"
+  shows "f \<in> borel_measurable M"
+using assms unfolding nnfis_def
+apply auto
+apply (rule mono_convergent_borel_measurable)
+using psfis_borel_measurable
+by auto
+
+lemma borel_measurable_mon_conv_psfis:
+  assumes f_borel: "f \<in> borel_measurable M"
+  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
+  shows"\<exists>u x. mono_convergent u f (space M) \<and> (\<forall>n. x n \<in> psfis (u n))"
+proof (safe intro!: exI)
+  let "?I n" = "{0<..<n * 2^n}"
+  let "?A n i" = "{w \<in> space M. real (i :: nat) / 2^(n::nat) \<le> f w \<and> f w < real (i + 1) / 2^n}"
+  let "?u n t" = "\<Sum>i\<in>?I n. real i / 2^n * indicator_fn (?A n i) t"
+  let "?x n" = "\<Sum>i\<in>?I n. real i / 2^n * measure M (?A n i)"
+
+  let "?w n t" = "if f t < real n then real (natfloor (f t * 2^n)) / 2^n else 0"
+
+  { fix t n assume t: "t \<in> space M"
+    have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)")
+    proof (cases "f t < real n")
+      case True
+      with nonneg t
+      have i: "?i < n * 2^n"
+        by (auto simp: real_of_nat_power[symmetric]
+                 intro!: less_natfloor mult_nonneg_nonneg)
+
+      hence t_in_A: "t \<in> ?A n ?i"
+        unfolding divide_le_eq less_divide_eq
+        using nonneg t True
+        by (auto intro!: real_natfloor_le
+          real_natfloor_gt_diff_one[unfolded diff_less_eq]
+          simp: real_of_nat_Suc zero_le_mult_iff)
+
+      hence *: "real ?i / 2^n \<le> f t"
+        "f t < real (?i + 1) / 2^n" by auto
+      { fix j assume "t \<in> ?A n j"
+        hence "real j / 2^n \<le> f t"
+          and "f t < real (j + 1) / 2^n" by auto
+        with * have "j \<in> {?i}" unfolding divide_le_eq less_divide_eq
+          by auto }
+      hence *: "\<And>j. t \<in> ?A n j \<longleftrightarrow> j \<in> {?i}" using t_in_A by auto
+
+      have "?u n t = real ?i / 2^n"
+        unfolding indicator_fn_def if_distrib *
+          setsum_cases[OF finite_greaterThanLessThan]
+        using i by (cases "?i = 0") simp_all
+      thus ?thesis using True by auto
+    next
+      case False
+      have "?u n t = (\<Sum>i \<in> {0 <..< n*2^n}. 0)"
+      proof (rule setsum_cong)
+        fix i assume "i \<in> {0 <..< n*2^n}"
+        hence "i + 1 \<le> n * 2^n" by simp
+        hence "real (i + 1) \<le> real n * 2^n"
+          unfolding real_of_nat_le_iff[symmetric]
+          by (auto simp: real_of_nat_power[symmetric])
+        also have "... \<le> f t * 2^n"
+          using False by (auto intro!: mult_nonneg_nonneg)
+        finally have "t \<notin> ?A n i"
+          by (auto simp: divide_le_eq less_divide_eq)
+        thus "real i / 2^n * indicator_fn (?A n i) t = 0"
+          unfolding indicator_fn_def by auto
+      qed simp
+      thus ?thesis using False by auto
+    qed }
+  note u_at_t = this
+
+  show "mono_convergent ?u f (space M)" unfolding mono_convergent_def
+  proof safe
+    fix t assume t: "t \<in> space M"
+    { fix m n :: nat assume "m \<le> n"
+      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
+      have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
+        apply (subst *)
+        apply (subst class_semiring.mul_a)
+        apply (subst real_of_nat_le_iff)
+        apply (rule le_mult_natfloor)
+        using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
+      hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
+        apply (subst *)
+        apply (subst (3) class_semiring.mul_c)
+        apply (subst class_semiring.mul_a)
+        by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
+    thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
+      by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)
+
+    show "(\<lambda>i. ?u i t) ----> f t" unfolding u_at_t[OF t]
+    proof (rule LIMSEQ_I, safe intro!: exI)
+      fix r :: real and n :: nat
+      let ?N = "natfloor (1/r) + 1"
+      assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \<le> n"
+      hence "?N \<le> n" by auto
+
+      have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt
+        by (simp add: real_of_nat_Suc)
+      also have "... < 2^?N" by (rule two_realpow_gt)
+      finally have less_r: "1 / 2^?N < r" using `0 < r`
+        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
+
+      have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto
+      also have "... \<le> real n" unfolding real_of_nat_le_iff using N by auto
+      finally have "f t < real n" .
+
+      have "real (natfloor (f t * 2^n)) \<le> f t * 2^n"
+        using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg)
+      hence less: "real (natfloor (f t * 2^n)) / 2^n \<le> f t" unfolding divide_le_eq by auto
+
+      have "f t * 2 ^ n - 1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one .
+      hence "f t - real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n"
+        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
+      also have "... \<le> 1 / 2^?N" using `?N \<le> n`
+        by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc)
+      also have "... < r" using less_r .
+      finally show "norm (?w n t - f t) < r" using `f t < real n` less by auto
+    qed
+  qed
+
+  fix n
+  show "?x n \<in> psfis (?u n)"
+  proof (rule psfis_intro)
+    show "?A n ` ?I n \<subseteq> sets M"
+    proof safe
+      fix i :: nat
+      from Int[OF
+        f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"]
+        f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]]
+      show "?A n i \<in> sets M"
+        by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute)
+    qed
+    show "nonneg (\<lambda>i :: nat. real i / 2 ^ n)"
+      unfolding nonneg_def by (auto intro!: divide_nonneg_pos)
+  qed auto
+qed
+
+lemma nnfis_dom_conv:
+  assumes borel: "f \<in> borel_measurable M"
+  and nnfis: "b \<in> nnfis g"
+  and ord: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
+  shows "\<exists>a. a \<in> nnfis f \<and> a \<le> b"
+proof -
+  obtain u x where mc_f: "mono_convergent u f (space M)" and
+    psfis: "\<And>n. x n \<in> psfis (u n)"
+    using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto
+
+  { fix n
+    { fix t assume t: "t \<in> space M"
+      note mono_convergent_le[OF mc_f this, of n]
+      also note ord[OF t]
+      finally have "u n t \<le> g t" . }
+    from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this]
+    have "x n \<le> b" by simp }
+  note x_less_b = this
+
+  have "convergent x"
+  proof (safe intro!: Bseq_mono_convergent)
+    from x_less_b pos_psfis[OF psfis]
+    show "Bseq x" by (auto intro!: BseqI'[of _ b])
+
+    fix n m :: nat assume *: "n \<le> m"
+    show "x n \<le> x m"
+    proof (rule psfis_mono[OF `x n \<in> psfis (u n)` `x m \<in> psfis (u m)`])
+      fix t assume "t \<in> space M"
+      from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this]
+      show "u n t \<le> u m t" using * by auto
+    qed
+  qed
+  then obtain a where "x ----> a" unfolding convergent_def by auto
+  with LIMSEQ_le_const2[OF `x ----> a`] x_less_b mc_f psfis
+  show ?thesis unfolding nnfis_def by auto
+qed
+
+lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
+  unfolding psfis_def pos_simple_def pos_simple_integral_def
+  by (auto simp: nonneg_def
+      intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
+
+lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
+  by (auto intro: the_equality nnfis_unique)
+
+lemma nnfis_cong:
+  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
+  shows "nnfis f = nnfis g"
+proof -
+  { fix f g :: "'a \<Rightarrow> real" assume cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
+    fix x assume "x \<in> nnfis f"
+    then guess u y unfolding nnfis_def by safe note x = this
+    hence "mono_convergent u g (space M)"
+      unfolding mono_convergent_def using cong by auto
+    with x(2,3) have "x \<in> nnfis g" unfolding nnfis_def by auto }
+  from this[OF cong] this[OF cong[symmetric]]
+  show ?thesis by safe
+qed
+
+lemma integral_cong:
+  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
+  shows "integral f = integral g"
+proof -
+  have "nnfis (pos_part f) = nnfis (pos_part g)"
+    using cong by (auto simp: pos_part_def intro!: nnfis_cong)
+  moreover
+  have "nnfis (neg_part f) = nnfis (neg_part g)"
+    using cong by (auto simp: neg_part_def intro!: nnfis_cong)
+  ultimately show ?thesis
+    unfolding integral_def by auto
+qed
+
+lemma nnfis_integral:
+  assumes "a \<in> nnfis f"
+  shows "integrable f" and "integral f = a"
+proof -
+  have a: "a \<in> nnfis (pos_part f)"
+    using assms nnfis_pos_on_mspace[OF assms]
+    by (auto intro!: nnfis_mon_conv[of "\<lambda>i. f" _ "\<lambda>i. a"]
+      LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def)
+
+  have "\<And>t. t \<in> space M \<Longrightarrow> neg_part f t = 0"
+    unfolding neg_part_def min_def
+    using nnfis_pos_on_mspace[OF assms] by auto
+  hence 0: "0 \<in> nnfis (neg_part f)"
+    by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def
+          intro!: LIMSEQ_const exI[of _ "\<lambda> x n. 0"] exI[of _ "\<lambda> n. 0"])
+
+  from 0 a show "integrable f" "integral f = a"
+    unfolding integrable_def integral_def by auto
+qed
+
+lemma nnfis_minus_nnfis_integral:
+  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
+  shows "integrable (\<lambda>t. f t - g t)" and "integral (\<lambda>t. f t - g t) = a - b"
+proof -
+  have borel: "(\<lambda>t. f t - g t) \<in> borel_measurable M" using assms
+    by (blast intro:
+      borel_measurable_diff_borel_measurable nnfis_borel_measurable)
+
+  have "\<exists>x. x \<in> nnfis (pos_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
+    (is "\<exists>x. x \<in> nnfis ?pp \<and> _")
+  proof (rule nnfis_dom_conv)
+    show "?pp \<in> borel_measurable M"
+      using borel by (rule pos_part_neg_part_borel_measurable)
+    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
+    fix t assume "t \<in> space M"
+    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
+    show "?pp t \<le> f t + g t" unfolding pos_part_def by auto
+    show "0 \<le> ?pp t" using nonneg_pos_part[of "\<lambda>t. f t - g t"]
+      unfolding nonneg_def by auto
+  qed
+  then obtain x where x: "x \<in> nnfis ?pp" by auto
+  moreover
+  have "\<exists>x. x \<in> nnfis (neg_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
+    (is "\<exists>x. x \<in> nnfis ?np \<and> _")
+  proof (rule nnfis_dom_conv)
+    show "?np \<in> borel_measurable M"
+      using borel by (rule pos_part_neg_part_borel_measurable)
+    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
+    fix t assume "t \<in> space M"
+    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
+    show "?np t \<le> f t + g t" unfolding neg_part_def by auto
+    show "0 \<le> ?np t" using nonneg_neg_part[of "\<lambda>t. f t - g t"]
+      unfolding nonneg_def by auto
+  qed
+  then obtain y where y: "y \<in> nnfis ?np" by auto
+  ultimately show "integrable (\<lambda>t. f t - g t)"
+    unfolding integrable_def by auto
+
+  from x and y
+  have "a + y \<in> nnfis (\<lambda>t. f t + ?np t)"
+    and "b + x \<in> nnfis (\<lambda>t. g t + ?pp t)" using assms by (auto intro: nnfis_add)
+  moreover
+  have "\<And>t. f t + ?np t = g t + ?pp t"
+    unfolding pos_part_def neg_part_def by auto
+  ultimately have "a - b = x - y"
+    using nnfis_unique by (auto simp: algebra_simps)
+  thus "integral (\<lambda>t. f t - g t) = a - b"
+    unfolding integral_def
+    using the_nnfis[OF x] the_nnfis[OF y] by simp
+qed
+
+lemma integral_borel_measurable:
+  "integrable f \<Longrightarrow> f \<in> borel_measurable M"
+  unfolding integrable_def
+  by (subst pos_part_neg_part_borel_measurable_iff)
+   (auto intro: nnfis_borel_measurable)
+
+lemma integral_indicator_fn:
+  assumes "a \<in> sets M"
+  shows "integral (indicator_fn a) = measure M a"
+  and "integrable (indicator_fn a)"
+  using psfis_indicator[OF assms, THEN psfis_nnfis]
+  by (auto intro!: nnfis_integral)
+
+lemma integral_add:
+  assumes "integrable f" and "integrable g"
+  shows "integrable (\<lambda>t. f t + g t)"
+  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
+proof -
+  { fix t
+    have "pos_part f t + pos_part g t - (neg_part f t + neg_part g t) =
+      f t + g t"
+      unfolding pos_part_def neg_part_def by auto }
+  note part_sum = this
+
+  from assms obtain a b c d where
+    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
+    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
+    unfolding integrable_def by auto
+  note sums = nnfis_add[OF a c] nnfis_add[OF b d]
+  note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum]
+
+  show "integrable (\<lambda>t. f t + g t)" using int(1) .
+
+  show "integral (\<lambda>t. f t + g t) = integral f + integral g"
+    using int(2) sums a b c d by (simp add: the_nnfis integral_def)
+qed
+
+lemma integral_mono:
+  assumes "integrable f" and "integrable g"
+  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+  shows "integral f \<le> integral g"
+proof -
+  from assms obtain a b c d where
+    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
+    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
+    unfolding integrable_def by auto
+
+  have "a \<le> c"
+  proof (rule nnfis_mono[OF a c])
+    fix t assume "t \<in> space M"
+    from mono[OF this] show "pos_part f t \<le> pos_part g t"
+      unfolding pos_part_def by auto
+  qed
+  moreover have "d \<le> b"
+  proof (rule nnfis_mono[OF d b])
+    fix t assume "t \<in> space M"
+    from mono[OF this] show "neg_part g t \<le> neg_part f t"
+      unfolding neg_part_def by auto
+  qed
+  ultimately have "a - b \<le> c - d" by auto
+  thus ?thesis unfolding integral_def
+    using a b c d by (simp add: the_nnfis)
+qed
+
+lemma integral_uminus:
+  assumes "integrable f"
+  shows "integrable (\<lambda>t. - f t)"
+  and "integral (\<lambda>t. - f t) = - integral f"
+proof -
+  have "pos_part f = neg_part (\<lambda>t.-f t)" and "neg_part f = pos_part (\<lambda>t.-f t)"
+    unfolding pos_part_def neg_part_def by (auto intro!: ext)
+  with assms show "integrable (\<lambda>t.-f t)" and "integral (\<lambda>t.-f t) = -integral f"
+    unfolding integrable_def integral_def by simp_all
+qed
+
+lemma integral_times_const:
+  assumes "integrable f"
+  shows "integrable (\<lambda>t. a * f t)" (is "?P a")
+  and "integral (\<lambda>t. a * f t) = a * integral f" (is "?I a")
+proof -
+  { fix a :: real assume "0 \<le> a"
+    hence "pos_part (\<lambda>t. a * f t) = (\<lambda>t. a * pos_part f t)"
+      and "neg_part (\<lambda>t. a * f t) = (\<lambda>t. a * neg_part f t)"
+      unfolding pos_part_def neg_part_def max_def min_def
+      by (auto intro!: ext simp: zero_le_mult_iff)
+    moreover
+    obtain x y where x: "x \<in> nnfis (pos_part f)" and y: "y \<in> nnfis (neg_part f)"
+      using assms unfolding integrable_def by auto
+    ultimately
+    have "a * x \<in> nnfis (pos_part (\<lambda>t. a * f t))" and
+      "a * y \<in> nnfis (neg_part (\<lambda>t. a * f t))"
+      using nnfis_times[OF _ `0 \<le> a`] by auto
+    with x y have "?P a \<and> ?I a"
+      unfolding integrable_def integral_def by (auto simp: algebra_simps) }
+  note int = this
+
+  have "?P a \<and> ?I a"
+  proof (cases "0 \<le> a")
+    case True from int[OF this] show ?thesis .
+  next
+    case False with int[of "- a"] integral_uminus[of "\<lambda>t. - a * f t"]
+    show ?thesis by auto
+  qed
+  thus "integrable (\<lambda>t. a * f t)"
+    and "integral (\<lambda>t. a * f t) = a * integral f" by simp_all
+qed
+
+lemma integral_cmul_indicator:
+  assumes "s \<in> sets M"
+  shows "integral (\<lambda>x. c * indicator_fn s x) = c * (measure M s)"
+  and "integrable (\<lambda>x. c * indicator_fn s x)"
+using assms integral_times_const integral_indicator_fn by auto
+
+lemma integral_zero:
+  shows "integral (\<lambda>x. 0) = 0"
+  and "integrable (\<lambda>x. 0)"
+  using integral_cmul_indicator[OF empty_sets, of 0]
+  unfolding indicator_fn_def by auto
+
+lemma integral_setsum:
+  assumes "finite S"
+  assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
+  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
+    and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I s")
+proof -
+  from assms have "?int S \<and> ?I S"
+  proof (induct S)
+    case empty thus ?case by (simp add: integral_zero)
+  next
+    case (insert i S)
+    thus ?case
+      apply simp
+      apply (subst integral_add)
+      using assms apply auto
+      apply (subst integral_add)
+      using assms by auto
+  qed
+  thus "?int S" and "?I S" by auto
+qed
+
+lemma markov_ineq:
+  assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"
+  shows "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
+using assms
+proof -
+  from assms have "0 < a ^ n" using real_root_pow_pos by auto
+  from assms have "f \<in> borel_measurable M"
+    using integral_borel_measurable[OF `integrable f`] by auto
+  hence w: "{w . w \<in> space M \<and> a \<le> f w} \<in> sets M"
+    using borel_measurable_ge_iff by auto
+  have i: "integrable (indicator_fn {w . w \<in> space M \<and> a \<le> f w})"
+    using integral_indicator_fn[OF w] by simp
+  have v1: "\<And> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t 
+            \<le> (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t"
+    unfolding indicator_fn_def
+    using `0 < a` power_mono[of a] assms by auto
+  have v2: "\<And> t. (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t \<le> \<bar>f t\<bar> ^ n"
+    unfolding indicator_fn_def 
+    using power_mono[of a _ n] abs_ge_self `a > 0` 
+    by auto
+  have "{w \<in> space M. a \<le> f w} \<inter> space M = {w . a \<le> f w} \<inter> space M"
+    using Collect_eq by auto
+  from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this
+  have "(a ^ n) * (measure M ((f -` {y . a \<le> y}) \<inter> space M)) =
+        (a ^ n) * measure M {w . w \<in> space M \<and> a \<le> f w}"
+    unfolding vimage_Collect_eq[of f] by simp
+  also have "\<dots> = integral (\<lambda> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t)"
+    using integral_cmul_indicator[OF w] i by auto
+  also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
+    apply (rule integral_mono)
+    using integral_cmul_indicator[OF w]
+      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
+  finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
+    unfolding atLeast_def
+    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
+qed
+
+lemma integral_finite_on_sets:
+  assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
+  shows "integral (\<lambda>x. f x * indicator_fn a x) =
+    (\<Sum> r \<in> f`a. r * measure M (f -` {r} \<inter> a))" (is "integral ?f = _")
+proof -
+  { fix x assume "x \<in> a"
+    with assms have "f -` {f x} \<inter> space M \<in> sets M"
+      by (subst Int_commute)
+         (auto simp: vimage_def Int_def
+               intro!: borel_measurable_const
+                      borel_measurable_eq_borel_measurable)
+    from Int[OF this assms(3)]
+         sets_into_space[OF assms(3), THEN Int_absorb1]
+    have "f -` {f x} \<inter> a \<in> sets M" by (simp add: Int_assoc) }
+  note vimage_f = this
+
+  have "finite a"
+    using assms(2,3) sets_into_space
+    by (auto intro: finite_subset)
+
+  have "integral (\<lambda>x. f x * indicator_fn a x) =
+    integral (\<lambda>x. \<Sum>i\<in>f ` a. i * indicator_fn (f -` {i} \<inter> a) x)"
+    (is "_ = integral (\<lambda>x. setsum (?f x) _)")
+    unfolding indicator_fn_def if_distrib
+    using `finite a` by (auto simp: setsum_cases intro!: integral_cong)
+  also have "\<dots> = (\<Sum>i\<in>f`a. integral (\<lambda>x. ?f x i))"
+  proof (rule integral_setsum, safe)
+    fix n x assume "x \<in> a"
+    thus "integrable (\<lambda>y. ?f y (f x))"
+      using integral_indicator_fn(2)[OF vimage_f]
+      by (auto intro!: integral_times_const)
+  qed (simp add: `finite a`)
+  also have "\<dots> = (\<Sum>i\<in>f`a. i * measure M (f -` {i} \<inter> a))"
+    using integral_cmul_indicator[OF vimage_f]
+    by (auto intro!: setsum_cong)
+  finally show ?thesis .
+qed
+
+lemma integral_finite:
+  assumes "f \<in> borel_measurable M" and "finite (space M)"
+  shows "integral f = (\<Sum> r \<in> f ` space M. r * measure M (f -` {r} \<inter> space M))"
+  using integral_finite_on_sets[OF assms top]
+    integral_cong[of "\<lambda>x. f x * indicator_fn (space M) x" f]
+  by (auto simp add: indicator_fn_def)
+
+lemma integral_finite_singleton:
+  assumes fin: "finite (space M)" and "Pow (space M) = sets M"
+  shows "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
+proof -
+  have "f \<in> borel_measurable M"
+    unfolding borel_measurable_le_iff
+    using assms by auto
+  { fix r let ?x = "f -` {r} \<inter> space M"
+    have "?x \<subseteq> space M" by auto
+    with assms have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
+      by (auto intro!: measure_real_sum_image) }
+  note measure_eq_setsum = this
+  show ?thesis
+    unfolding integral_finite[OF `f \<in> borel_measurable M` fin]
+      measure_eq_setsum setsum_right_distrib
+    apply (subst setsum_Sigma)
+    apply (simp add: assms)
+    apply (simp add: assms)
+  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 * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
+      by auto
+  qed (auto intro!: image_eqI inj_onI)
+qed
+
+lemma borel_measurable_inverse:
+  assumes "f \<in> borel_measurable M"
+  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
+  unfolding borel_measurable_ge_iff
+proof (safe, rule linorder_cases)
+  fix a :: real assume "0 < a"
+  { fix w
+    from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
+      by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
+                linorder_not_le real_le_refl real_le_trans real_less_def
+                xt1(7) zero_less_divide_1_iff) }
+  hence "{w \<in> space M. a \<le> inverse (f w)} =
+    {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
+  with Int assms[unfolded borel_measurable_gr_iff]
+    assms[unfolded borel_measurable_le_iff]
+  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+next
+  fix a :: real assume "0 = a"
+  { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
+      unfolding `0 = a`[symmetric] by auto }
+  thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
+    using assms[unfolded borel_measurable_ge_iff] by simp
+next
+  fix a :: real assume "a < 0"
+  { fix w
+    from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
+      apply (cases "0 \<le> f w")
+      apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
+                   zero_le_divide_1_iff)
+      apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
+                   linorder_not_le real_le_refl real_le_trans)
+      done }
+  hence "{w \<in> space M. a \<le> inverse (f w)} =
+    {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
+  with Un assms[unfolded borel_measurable_ge_iff]
+    assms[unfolded borel_measurable_le_iff]
+  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
+qed
+
+lemma borel_measurable_divide:
+  assumes "f \<in> borel_measurable M"
+  and "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
+  unfolding field_divide_inverse
+  by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
+
+lemma RN_deriv_finite_singleton:
+  fixes v :: "'a set \<Rightarrow> real"
+  assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M"
+  and ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
+  and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
+  and "x \<in> space M" and "measure M {x} \<noteq> 0"
+  shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
+  unfolding RN_deriv_def
+proof (rule someI2_ex[where Q = "\<lambda>f. f x = ?v x"], rule exI[where x = ?v], safe)
+  show "(\<lambda>a. v {a} / measure_space.measure M {a}) \<in> borel_measurable M"
+    unfolding borel_measurable_le_iff using Pow by auto
+next
+  fix a assume "a \<in> sets M"
+  hence "a \<subseteq> space M" and "finite a"
+    using sets_into_space finite by (auto intro: finite_subset)
+  have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
+    v {x} * indicator_fn a x" using eq_0 by auto
+
+  from measure_space.measure_real_sum_image[OF ms_v, of a]
+    Pow `a \<in> sets M` sets_into_space `finite a`
+  have "v a = (\<Sum>x\<in>a. v {x})" by auto
+  thus "integral (\<lambda>x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a"
+    apply (simp add: eq_0 integral_finite_singleton[OF finite Pow])
+    apply (unfold divide_1)
+    by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \<subseteq> space M` Int_absorb1)
+next
+  fix w assume "w \<in> borel_measurable M"
+  assume int_eq_v: "\<forall>a\<in>sets M. integral (\<lambda>x. w x * indicator_fn a x) = v a"
+  have "{x} \<in> sets M" using Pow `x \<in> space M` by auto
+
+  have "w x * measure M {x} =
+    (\<Sum>y\<in>space M. w y * indicator_fn {x} y * measure M {y})"
+    apply (subst (3) mult_commute)
+    unfolding indicator_fn_def if_distrib setsum_cases[OF finite]
+    using `x \<in> space M` by simp
+  also have "... = v {x}"
+    using int_eq_v[rule_format, OF `{x} \<in> sets M`]
+    by (simp add: integral_finite_singleton[OF finite Pow])
+  finally show "w x = v {x} / measure M {x}"
+    using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
+qed fact
+
+lemma countable_space_integral_reduce:
+  assumes "positive M (measure M)" and "f \<in> borel_measurable M"
+  and "countable (f ` space M)"
+  and "\<not> finite (pos_part f ` space M)"
+  and "\<not> finite (neg_part f ` space M)"
+  and "((\<lambda>r. r * measure m (neg_part f -` {r} \<inter> space m)) o enumerate (neg_part f ` space M)) sums n"
+  and "((\<lambda>r. r * measure m (pos_part f -` {r} \<inter> space m)) o enumerate (pos_part f ` space M)) sums p"
+  shows "integral f = p - n"
+oops
+
+(*
+val countable_space_integral_reduce = store_thm
+  ("countable_space_integral_reduce",
+   "\<forall>m f p n. measure_space m \<and>
+	     positive m \<and>
+	     f \<in> borel_measurable (space m, sets m) \<and>
+	     countable (IMAGE f (space m)) \<and>
+	     ~(FINITE (IMAGE (pos_part f) (space m))) \<and>
+	     ~(FINITE (IMAGE (neg_part f) (space m))) \<and>
+	     (\<lambda>r. r *
+		  measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
+		enumerate ((IMAGE (neg_part f) (space m))) sums n \<and>
+	     (\<lambda>r. r *
+		  measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
+		enumerate ((IMAGE (pos_part f) (space m))) sums p ==>
+	     (integral m f = p - n)",
+   RW_TAC std_ss [integral_def]
+   ++ Suff `((@i. i \<in> nnfis m (pos_part f)) = p) \<and> ((@i. i \<in> nnfis m (neg_part f)) = n)`
+   >> RW_TAC std_ss []
+   ++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss [])
+   >> (Suff `p \<in> nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique]
+       ++ MATCH_MP_TAC nnfis_mon_conv
+       ++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))`
+		by (`countable (IMAGE (pos_part f) (space m))`
+			by (MATCH_MP_TAC COUNTABLE_SUBSET
+			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))`
+			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT]
+			    ++ METIS_TAC [])
+		     ++ METIS_TAC [COUNTABLE_ALT])
+       ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
+       ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m)))
+			(pred_set$count n) then pos_part f t else 0)`
+       ++ Q.EXISTS_TAC `(\<lambda>n.
+         sum (0,n)
+           ((\<lambda>r.
+               r *
+               measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
+            enumerate (IMAGE (pos_part f) (space m))))`
+       ++ ASM_SIMP_TAC std_ss []
+       ++ CONJ_TAC
+       >> (RW_TAC std_ss [mono_convergent_def]
+	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS])
+	   ++ RW_TAC std_ss [SEQ]
+	   ++ `\<exists>N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t`
+		by METIS_TAC [IN_IMAGE]
+	   ++ Q.EXISTS_TAC `SUC N`
+	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
+	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
+	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def])
+       ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
+	   ++ `(\<lambda>t. (if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set$count n')
+      			then pos_part f t else  0)) =
+		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
+			indicator_fn ((\<lambda>i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i}
+					   \<inter> (space m)) i) t)
+		     (pred_set$count n'))`
+		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
+		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
+				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
+			++ POP_ORW
+			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
+			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
+				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
+			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
+			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
+				enumerate (IMAGE (pos_part f) (space m)) x' *
+				(if enumerate (IMAGE (pos_part f) (space m)) x =
+				enumerate (IMAGE (pos_part f) (space m)) x'
+				then 1 else 0) else 0)) = (\<lambda>x. 0)`
+				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
+			++ POP_ORW
+			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
+		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
+		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
+		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
+			REAL_SUM_IMAGE_IN_IF]
+		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
+			(\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i *
+           		(if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \<and>
+             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
+			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
+		    ++ POP_ORW
+		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
+	   ++ POP_ORW
+	   ++ `((\<lambda>r. r * measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
+		enumerate (IMAGE (pos_part f) (space m))) =
+		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
+			measure m ((\<lambda>i.
+                PREIMAGE (pos_part f)
+                  {enumerate (IMAGE (pos_part f) (space m)) i} \<inter>
+                space m) i))`
+		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
+	   ++ POP_ORW
+	   ++ MATCH_MP_TAC psfis_intro
+	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
+	   ++ REVERSE CONJ_TAC
+	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def]
+	       ++ METIS_TAC [REAL_LE_REFL])
+	   ++ `(pos_part f) \<in> borel_measurable (space m, sets m)`
+		by METIS_TAC [pos_part_neg_part_borel_measurable]
+	   ++ REPEAT STRIP_TAC
+	   ++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \<inter> space m =
+		{w | w \<in> space m \<and> ((pos_part f) w = (\<lambda>w. enumerate (IMAGE (pos_part f) (space m)) i) w)}`
+		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
+		    ++ DECIDE_TAC)
+	   ++ POP_ORW
+	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
+	   ++ METIS_TAC [borel_measurable_const, measure_space_def])
+   ++ Suff `n \<in> nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique]
+   ++ MATCH_MP_TAC nnfis_mon_conv
+   ++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))`
+		by (`countable (IMAGE (neg_part f) (space m))`
+			by (MATCH_MP_TAC COUNTABLE_SUBSET
+			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))`
+			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE]
+			    ++ METIS_TAC [])
+		     ++ METIS_TAC [COUNTABLE_ALT])
+   ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
+   ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m)))
+			(pred_set$count n) then neg_part f t else 0)`
+   ++ Q.EXISTS_TAC `(\<lambda>n.
+         sum (0,n)
+           ((\<lambda>r.
+               r *
+               measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
+            enumerate (IMAGE (neg_part f) (space m))))`
+   ++ ASM_SIMP_TAC std_ss []
+   ++ CONJ_TAC
+   >> (RW_TAC std_ss [mono_convergent_def]
+	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL])
+	   ++ RW_TAC std_ss [SEQ]
+	   ++ `\<exists>N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t`
+		by METIS_TAC [IN_IMAGE]
+	   ++ Q.EXISTS_TAC `SUC N`
+	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
+	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
+	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def])
+   ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
+	   ++ `(\<lambda>t. (if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set$count n')
+      			then neg_part f t else  0)) =
+		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
+			indicator_fn ((\<lambda>i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i}
+					   \<inter> (space m)) i) t)
+		     (pred_set$count n'))`
+		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
+		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
+				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
+			++ POP_ORW
+			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
+			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
+				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
+			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
+			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
+				enumerate (IMAGE (neg_part f) (space m)) x' *
+				(if enumerate (IMAGE (neg_part f) (space m)) x =
+				enumerate (IMAGE (neg_part f) (space m)) x'
+				then 1 else 0) else 0)) = (\<lambda>x. 0)`
+				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
+			++ POP_ORW
+			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
+		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
+		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
+		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
+			REAL_SUM_IMAGE_IN_IF]
+		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
+			(\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i *
+           		(if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \<and>
+             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
+			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
+		    ++ POP_ORW
+		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
+	   ++ POP_ORW
+	   ++ `((\<lambda>r. r * measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
+		enumerate (IMAGE (neg_part f) (space m))) =
+		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
+			measure m ((\<lambda>i.
+                PREIMAGE (neg_part f)
+                  {enumerate (IMAGE (neg_part f) (space m)) i} \<inter>
+                space m) i))`
+		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
+	   ++ POP_ORW
+	   ++ MATCH_MP_TAC psfis_intro
+	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
+	   ++ REVERSE CONJ_TAC
+	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def]
+	       ++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL])
+	   ++ `(neg_part f) \<in> borel_measurable (space m, sets m)`
+		by METIS_TAC [pos_part_neg_part_borel_measurable]
+	   ++ REPEAT STRIP_TAC
+	   ++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \<inter> space m =
+		{w | w \<in> space m \<and> ((neg_part f) w = (\<lambda>w. enumerate (IMAGE (neg_part f) (space m)) i) w)}`
+		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
+		    ++ DECIDE_TAC)
+	   ++ POP_ORW
+	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
+	   ++ METIS_TAC [borel_measurable_const, measure_space_def]);
+*)
+
+end
+
+end
\ No newline at end of file
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -104,7 +104,7 @@
   have ra: "range (binaryset A B) \<subseteq> sets M"
    by (simp add: range_binaryset_eq empty A B) 
  have di:  "disjoint_family (binaryset A B)" using disj
-   by (simp add: disjoint_family_def binaryset_def Int_commute) 
+   by (simp add: disjoint_family_on_def binaryset_def Int_commute) 
  from closed_cdi_Disj [OF cdi ra di]
  show ?thesis
    by (simp add: UN_binaryset_eq) 
@@ -118,7 +118,7 @@
   have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
     by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
   have di:  "disjoint_family (binaryset A B)" using disj
-    by (simp add: disjoint_family_def binaryset_def Int_commute) 
+    by (simp add: disjoint_family_on_def binaryset_def Int_commute) 
   from Disj [OF ra di]
   show ?thesis
     by (simp add: UN_binaryset_eq) 
@@ -164,7 +164,7 @@
   have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
     by blast
   moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
-    by (auto simp add: disjoint_family_def) 
+    by (auto simp add: disjoint_family_on_def) 
   ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
     by (rule smallest_ccdi_sets.Disj) 
   show ?case
@@ -208,7 +208,7 @@
   have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
     by blast
   moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
-    by (auto simp add: disjoint_family_def) 
+    by (auto simp add: disjoint_family_on_def) 
   ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
     by (rule smallest_ccdi_sets.Disj) 
   show ?case
@@ -355,7 +355,7 @@
   hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
     by (metis add_commute le_add_diff_inverse nat_less_le)
   thus ?thesis
-    by (auto simp add: disjoint_family_def)
+    by (auto simp add: disjoint_family_on_def)
       (metis insert_absorb insert_subset le_SucE le_antisym not_leE) 
 qed
 
@@ -642,7 +642,7 @@
                   show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
                     using f12 rA2 by (auto simp add: measurable_def)
                   show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
-                    by (auto simp add: disjoint_family_def) 
+                    by (auto simp add: disjoint_family_on_def) 
                   show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
                     proof (rule sigma_algebra.countable_UN [OF sa1])
                       show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
@@ -820,7 +820,98 @@
   thus ?thesis
     by (metis subset_refl s)
 qed
-  
+
+lemma (in measure_space) measure_finitely_additive':
+  assumes "f \<in> ({0 :: nat ..< n} \<rightarrow> sets M)"
+  assumes "\<And> a b. \<lbrakk>a < n ; b < n ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
+  assumes "s = \<Union> (f ` {0 ..< n})"
+  shows "(\<Sum> i \<in> {0 ..< n}. (measure M \<circ> f) i) = measure M s"
+proof -
+  def f' == "\<lambda> i. (if i < n then f i else {})"
+  have rf: "range f' \<subseteq> sets M" unfolding f'_def 
+    using assms empty_sets by auto
+  have df: "disjoint_family f'" unfolding f'_def disjoint_family_on_def 
+    using assms by simp
+  have "\<Union> range f' = (\<Union> i \<in> {0 ..< n}. f i)" 
+    unfolding f'_def by auto
+  then have "measure M s = measure M (\<Union> range f')" 
+    using assms by simp
+  then have part1: "(\<lambda> i. measure M (f' i)) sums measure M s" 
+    using df rf ca[unfolded countably_additive_def, rule_format, of f']
+    by auto
+
+  have "(\<lambda> i. measure M (f' i)) sums (\<Sum> i \<in> {0 ..< n}. measure M (f' i))" 
+    using series_zero[of "n" "\<lambda> i. measure M (f' i)", rule_format] 
+    unfolding f'_def by simp
+  also have "\<dots> = (\<Sum> i \<in> {0 ..< n}. measure M (f i))" 
+    unfolding f'_def by auto
+  finally have part2: "(\<lambda> i. measure M (f' i)) sums (\<Sum> i \<in> {0 ..< n}. measure M (f i))" by simp
+  show ?thesis 
+    using sums_unique[OF part1] 
+          sums_unique[OF part2] by auto
+qed
+
+
+lemma (in measure_space) measure_finitely_additive:
+  assumes "finite r"
+  assumes "r \<subseteq> sets M"
+  assumes d: "\<And> a b. \<lbrakk>a \<in> r ; b \<in> r ; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
+  shows "(\<Sum> i \<in> r. measure M i) = measure M (\<Union> r)"
+using assms
+proof -
+  (* counting the elements in r is enough *)
+  let ?R = "{0 ..< card r}"
+  obtain f where f: "f ` ?R = r" "inj_on f ?R"
+    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite r`]
+    by auto
+  hence f_into_sets: "f \<in> ?R \<rightarrow> sets M" using assms by auto
+  have disj: "\<And> a b. \<lbrakk>a \<in> ?R ; b \<in> ?R ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
+  proof -
+    fix a b assume asm: "a \<in> ?R" "b \<in> ?R" "a \<noteq> b"
+    hence neq: "f a \<noteq> f b" using f[unfolded inj_on_def, rule_format] by blast
+    from asm have "f a \<in> r" "f b \<in> r" using f by auto
+    thus "f a \<inter> f b = {}" using d[of "f a" "f b"] f using neq by auto
+  qed
+  have "(\<Union> r) = (\<Union> i \<in> ?R. f i)"
+    using f by auto
+  hence "measure M (\<Union> r)= measure M (\<Union> i \<in> ?R. f i)" by simp
+  also have "\<dots> = (\<Sum> i \<in> ?R. measure M (f i))"
+    using measure_finitely_additive'[OF f_into_sets disj] by simp
+  also have "\<dots> = (\<Sum> a \<in> r. measure M a)" 
+    using f[rule_format] setsum_reindex[of f ?R "\<lambda> a. measure M a"] by auto
+  finally show ?thesis by simp
+qed
+
+lemma (in measure_space) measure_finitely_additive'':
+  assumes "finite s"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<in> sets M"
+  assumes d: "disjoint_family_on a s"
+  shows "(\<Sum> i \<in> s. measure M (a i)) = measure M (\<Union> i \<in> s. a i)"
+using assms
+proof -
+  (* counting the elements in s is enough *)
+  let ?R = "{0 ..< card s}"
+  obtain f where f: "f ` ?R = s" "inj_on f ?R"
+    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite s`]
+    by auto
+  hence f_into_sets: "a \<circ> f \<in> ?R \<rightarrow> sets M" using assms unfolding o_def by auto
+  have disj: "\<And> i j. \<lbrakk>i \<in> ?R ; j \<in> ?R ; i \<noteq> j\<rbrakk> \<Longrightarrow> (a \<circ> f) i \<inter> (a \<circ> f) j = {}"
+  proof -
+    fix i j assume asm: "i \<in> ?R" "j \<in> ?R" "i \<noteq> j"
+    hence neq: "f i \<noteq> f j" using f[unfolded inj_on_def, rule_format] by blast
+    from asm have "f i \<in> s" "f j \<in> s" using f by auto
+    thus "(a \<circ> f) i \<inter> (a \<circ> f) j = {}"
+      using d f neq unfolding disjoint_family_on_def by auto
+  qed
+  have "(\<Union> i \<in> s. a i) = (\<Union> i \<in> f ` ?R. a i)" using f by auto
+  hence "(\<Union> i \<in> s. a i) = (\<Union> i \<in> ?R. a (f i))" by auto
+  hence "measure M (\<Union> i \<in> s. a i) = (\<Sum> i \<in> ?R. measure M (a (f i)))"
+    using measure_finitely_additive'[OF f_into_sets disj] by simp
+  also have "\<dots> = (\<Sum> i \<in> s. measure M (a i))"
+    using f[rule_format] setsum_reindex[of f ?R "\<lambda> i. measure M (a i)"] by auto
+  finally show ?thesis by simp
+qed
+
 lemma (in sigma_algebra) sigma_algebra_extend:
      "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
    by unfold_locales (auto intro!: space_closed)
@@ -845,7 +936,7 @@
       hence "finite (A ` I)"
         by (metis finite_UnionD finite_subset fin) 
       moreover have "inj_on A I" using disj
-        by (auto simp add: I_def disjoint_family_def inj_on_def) 
+        by (auto simp add: I_def disjoint_family_on_def inj_on_def) 
       ultimately have finI: "finite I"
         by (metis finite_imageD)
       hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
@@ -873,7 +964,7 @@
           have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
             proof (rule Caratheodory.additiveD [OF addf])
               show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
-                by (auto simp add: disjoint_family_def nat_less_le) blast
+                by (auto simp add: disjoint_family_on_def nat_less_le) blast
               show "A n \<in> sets M" using A 
                 by (force simp add: Mf_def) 
               show "(\<Union>i<n. A i) \<in> sets M"
@@ -906,5 +997,4 @@
       \<Longrightarrow> measure_space M"
   by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
 
-end
-
+end
\ No newline at end of file
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Probability/Probability.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -1,5 +1,5 @@
 theory Probability
-imports Measure Borel
+imports Probability_Space
 begin
 
 end
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Probability/Probability_Space.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -0,0 +1,458 @@
+theory Probability_Space
+imports Lebesgue
+begin
+
+locale prob_space = measure_space +
+  assumes prob_space: "measure M (space M) = 1"
+begin
+
+abbreviation "events \<equiv> sets M"
+abbreviation "prob \<equiv> measure M"
+abbreviation "prob_preserving \<equiv> measure_preserving"
+abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s"
+abbreviation "expectation \<equiv> integral"
+
+definition
+  "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B"
+
+definition
+  "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)"
+
+definition
+  "distribution X = (\<lambda>s. prob ((X -` s) \<inter> (space M)))"
+
+definition
+  "probably e \<longleftrightarrow> e \<in> events \<and> prob e = 1"
+
+definition
+  "possibly e \<longleftrightarrow> e \<in> events \<and> prob e \<noteq> 0"
+
+definition
+  "joint_distribution X Y \<equiv> (\<lambda>a. prob ((\<lambda>x. (X x, Y x)) -` a \<inter> space M))"
+
+definition
+  "conditional_expectation X s \<equiv> THE f. random_variable borel_space f \<and>
+    (\<forall> g \<in> s. integral (\<lambda>x. f x * indicator_fn g x) =
+              integral (\<lambda>x. X x * indicator_fn g x))"
+
+definition
+  "conditional_prob e1 e2 \<equiv> conditional_expectation (indicator_fn e1) e2"
+
+lemma positive: "positive M prob"
+  unfolding positive_def using positive empty_measure by blast
+
+lemma prob_compl:
+  assumes "s \<in> events"
+  shows "prob (space M - s) = 1 - prob s"
+using assms
+proof -
+  have "prob ((space M - s) \<union> s) = prob (space M - s) + prob s"
+    using assms additive[unfolded additive_def] by blast
+  thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space)
+qed
+
+lemma indep_space:
+  assumes "s \<in> events"
+  shows "indep (space M) s"
+using assms prob_space
+unfolding indep_def by auto
+
+
+lemma prob_space_increasing:
+  "increasing M prob"
+by (rule additive_increasing[OF positive additive])
+
+lemma prob_subadditive:
+  assumes "s \<in> events" "t \<in> events"
+  shows "prob (s \<union> t) \<le> prob s + prob t"
+using assms
+proof -
+  have "prob (s \<union> t) = prob ((s - t) \<union> t)" by simp
+  also have "\<dots> = prob (s - t) + prob t"
+    using additive[unfolded additive_def, rule_format, of "s-t" "t"] 
+      assms by blast
+  also have "\<dots> \<le> prob s + prob t"
+    using prob_space_increasing[unfolded increasing_def, rule_format] assms
+    by auto
+  finally show ?thesis by simp
+qed
+
+lemma prob_zero_union:
+  assumes "s \<in> events" "t \<in> events" "prob t = 0"
+  shows "prob (s \<union> t) = prob s"
+using assms 
+proof -
+  have "prob (s \<union> t) \<le> prob s"
+    using prob_subadditive[of s t] assms by auto
+  moreover have "prob (s \<union> t) \<ge> prob s"
+    using prob_space_increasing[unfolded increasing_def, rule_format] 
+      assms by auto
+  ultimately show ?thesis by simp
+qed
+
+lemma prob_eq_compl:
+  assumes "s \<in> events" "t \<in> events"
+  assumes "prob (space M - s) = prob (space M - t)"
+  shows "prob s = prob t"
+using assms prob_compl by auto
+
+lemma prob_one_inter:
+  assumes events:"s \<in> events" "t \<in> events"
+  assumes "prob t = 1"
+  shows "prob (s \<inter> t) = prob s"
+using assms
+proof -
+  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" 
+    using prob_compl[of "t"] prob_zero_union assms by auto
+  then show "prob (s \<inter> t) = prob s" 
+    using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto
+qed
+
+lemma prob_eq_bigunion_image:
+  assumes "range f \<subseteq> events" "range g \<subseteq> events"
+  assumes "disjoint_family f" "disjoint_family g"
+  assumes "\<And> n :: nat. prob (f n) = prob (g n)"
+  shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"
+using assms 
+proof -
+  have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" 
+    using ca[unfolded countably_additive_def] assms by blast
+  have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"
+    using ca[unfolded countably_additive_def] assms by blast
+  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
+qed
+
+lemma prob_countably_subadditive: 
+  assumes "range f \<subseteq> events" 
+  assumes "summable (prob \<circ> f)"
+  shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))"
+using assms
+proof -
+  def f' == "\<lambda> i. f i - (\<Union> j \<in> {0 ..< i}. f j)"
+  have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto
+  moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)"
+  proof (rule subsetI)
+    fix x assume "x \<in> (\<Union> i. f i)"
+    then obtain k where "x \<in> f k" by blast
+    hence k: "k \<in> {m. x \<in> f m}" by simp
+    have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')"
+      using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}", 
+        OF wf_less k] by auto
+    thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto
+  qed
+  ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI)
+
+  have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}"
+    unfolding f'_def by auto
+  have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}"
+    apply (drule iffD1[OF nat_neq_iff])
+    using df' by auto
+  hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp
+
+  have rf': "\<And> i. f' i \<in> events"
+  proof -
+    fix i :: nat
+    have "(\<Union> {f j | j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast
+    hence "(\<Union> {f j | j. j \<in> {0 ..< i}}) \<in> events 
+      \<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto
+    thus "f' i \<in> events" 
+      unfolding f'_def 
+      using assms finite_union[of "{f j | j. j \<in> {0 ..< i}}"]
+        Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto
+  qed
+  hence uf': "(\<Union> range f') \<in> events" by auto
+  
+  have "\<And> i. prob (f' i) \<le> prob (f i)"
+    using prob_space_increasing[unfolded increasing_def, rule_format, OF rf']
+      assms rf' unfolding f'_def by blast
+
+  hence absinc: "\<And> i. \<bar> prob (f' i) \<bar> \<le> prob (f i)"
+    using abs_of_nonneg positive[unfolded positive_def]
+      assms rf' by auto
+
+  have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp
+
+  also have "\<dots> = (\<Sum> i. prob (f' i))"
+    using ca[unfolded countably_additive_def, rule_format]
+    sums_unique rf' uf' df
+    by auto
+  
+  also have "\<dots> \<le> (\<Sum> i. prob (f i))"
+    using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)", 
+      rule_format, OF absinc]
+      assms[unfolded o_def] by auto
+
+  finally show ?thesis by auto
+qed
+
+lemma prob_countably_zero:
+  assumes "range c \<subseteq> events"
+  assumes "\<And> i. prob (c i) = 0"
+  shows "(prob (\<Union> i :: nat. c i) = 0)"
+  using assms
+proof -
+  have leq0: "0 \<le> prob (\<Union> i. c i)"
+    using assms positive[unfolded positive_def, rule_format] 
+    by auto
+
+  have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))"
+    using prob_countably_subadditive[of c, unfolded o_def]
+      assms sums_zero sums_summable by auto
+
+  also have "\<dots> = 0"
+    using assms sums_zero 
+      sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto
+
+  finally show "prob (\<Union> i. c i) = 0"
+    using leq0 by auto
+qed
+
+lemma indep_sym:
+   "indep a b \<Longrightarrow> indep b a"
+unfolding indep_def using Int_commute[of a b] by auto
+
+lemma indep_refl:
+  assumes "a \<in> events"
+  shows "indep a a = (prob a = 0) \<or> (prob a = 1)"
+using assms unfolding indep_def by auto
+
+lemma prob_equiprobable_finite_unions:
+  assumes "s \<in> events" 
+  assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
+  assumes "finite s"
+  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
+  shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}"
+using assms
+proof (cases "s = {}")
+  case True thus ?thesis by simp
+next
+  case False hence " \<exists> x. x \<in> s" by blast
+  from someI_ex[OF this] assms
+  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
+  have "prob s = (\<Sum> x \<in> s. prob {x})"
+    using assms measure_real_sum_image by blast
+  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
+  also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}"
+    using setsum_constant assms by auto
+  finally show ?thesis by simp
+qed
+
+lemma prob_real_sum_image_fn:
+  assumes "e \<in> events"
+  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
+  assumes "finite s"
+  assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
+  assumes "space M \<subseteq> (\<Union> i \<in> s. f i)"
+  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
+using assms
+proof -
+  let ?S = "{0 ..< card s}"
+  obtain g where "g ` ?S = s \<and> inj_on g ?S"
+    using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto
+  moreover hence gs: "g ` ?S = s" by simp
+  ultimately have ginj: "inj_on g ?S" by simp
+  let ?f' = "\<lambda> i. e \<inter> f (g i)"
+  have f': "?f' \<in> ?S \<rightarrow> events"
+    using gs assms by blast
+  hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk> 
+    \<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast
+  hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk> 
+    \<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp
+
+  have "e = e \<inter> space M" using assms sets_into_space by simp
+  also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast
+  also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp
+  also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp
+  finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp
+  also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))"
+    apply (subst measure_finitely_additive'')
+    using f' df' assms by (auto simp: disjoint_family_on_def)
+  also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))" 
+    using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"]
+      ginj by simp
+  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp
+  finally show ?thesis by simp
+qed
+
+lemma distribution_prob_space:
+  assumes "random_variable s X"
+  shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"
+using assms
+proof -
+  let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"
+  interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto
+  hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto
+
+  have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0"
+    unfolding distribution_def
+    using positive[unfolded positive_def]
+    assms[unfolded measurable_def] by auto
+
+  have cas: "countably_additive ?N (distribution X)"
+  proof -
+    {
+      fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool"
+      let ?g = "\<lambda> n. X -` f n \<inter> space M"
+      assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f"
+      hence "range ?g \<subseteq> events" 
+        using assms unfolding measurable_def by blast
+      from ca[unfolded countably_additive_def, 
+        rule_format, of ?g, OF this] countable_UN[OF this] asm
+      have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)"
+        unfolding disjoint_family_on_def by blast
+      moreover have "(X -` (\<Union> n. f n)) = (\<Union> n. X -` f n)" by blast
+      ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)"
+        unfolding distribution_def by simp
+    } thus ?thesis unfolding countably_additive_def by simp
+  qed
+
+  have ds0: "distribution X {} = 0"
+    unfolding distribution_def by simp
+
+  have "X -` space s \<inter> space M = space M"
+    using assms[unfolded measurable_def] by auto
+  hence ds1: "distribution X (space s) = 1"
+    unfolding measurable_def distribution_def using prob_space by simp
+
+  from ds0 ds1 cas pos sigN
+  show "prob_space ?N"
+    unfolding prob_space_def prob_space_axioms_def
+    measure_space_def measure_space_axioms_def by simp
+qed
+
+lemma distribution_lebesgue_thm1:
+  assumes "random_variable s X"
+  assumes "A \<in> sets s"
+  shows "distribution X A = expectation (indicator_fn (X -` A \<inter> space M))"
+unfolding distribution_def
+using assms unfolding measurable_def
+using integral_indicator_fn by auto
+
+lemma distribution_lebesgue_thm2:
+  assumes "random_variable s X" "A \<in> sets s"
+  shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)"
+  (is "_ = measure_space.integral ?M _")
+proof -
+  interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space)
+
+  show ?thesis
+    using S.integral_indicator_fn(1)
+    using assms unfolding distribution_def by auto
+qed
+
+lemma finite_expectation1:
+  assumes "finite (space M)" "random_variable borel_space X"
+  shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))"
+  using assms integral_finite measurable_def
+  unfolding borel_measurable_def by auto
+
+lemma finite_expectation:
+  assumes "finite (space M) \<and> random_variable borel_space X"
+  shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})"
+using assms unfolding distribution_def using finite_expectation1 by auto
+
+lemma finite_marginal_product_space_POW:
+  assumes "Pow (space M) = events"
+  assumes "random_variable \<lparr> space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
+  assumes "random_variable \<lparr> space = Y ` (space M), sets = Pow (Y ` (space M))\<rparr> Y"
+  assumes "finite (space M)"
+  shows "measure_space \<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),
+  sets = Pow ((X ` (space M)) \<times> (Y ` (space M))),
+  measure = (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))\<rparr>"
+  using assms
+proof -
+  let "?S" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))), 
+    sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
+  let "?M" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))), 
+    sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
+  have pos: "positive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
+    unfolding positive_def using positive[unfolded positive_def] assms by auto
+  { fix x y
+    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
+    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
+    assume "x \<inter> y = {}"
+    from additive[unfolded additive_def, rule_format, OF A B] this
+    have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
+      (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
+      prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
+      prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)" 
+      apply (subst Int_Un_distrib2)
+      by auto }
+  hence add: "additive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
+    unfolding additive_def by auto
+  interpret S: sigma_algebra "?S" 
+    unfolding sigma_algebra_def algebra_def
+      sigma_algebra_axioms_def by auto
+  show ?thesis
+     using add pos S.finite_additivity_sufficient assms by auto
+qed
+
+lemma finite_marginal_product_space_POW2:
+  assumes "Pow (space M) = events"
+  assumes "random_variable \<lparr>space = s1, sets = Pow s1\<rparr> X"
+  assumes "random_variable \<lparr>space = s2, sets = Pow s2\<rparr> Y"
+  assumes "finite (space M)"
+  assumes "finite s1" "finite s2"
+  shows "measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
+proof -
+  let "?S" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2) \<rparr>"
+  let "?M" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y \<rparr>"
+  have pos: "positive ?S (joint_distribution X Y)" using positive
+    unfolding positive_def joint_distribution_def using assms by auto
+  { fix x y
+    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
+    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
+    assume "x \<inter> y = {}"
+    from additive[unfolded additive_def, rule_format, OF A B] this
+    have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
+      (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
+      prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
+      prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)" 
+      apply (subst Int_Un_distrib2)
+      by auto }
+  hence add: "additive ?S (joint_distribution X Y)"
+    unfolding additive_def joint_distribution_def by auto
+  interpret S: sigma_algebra "?S" 
+    unfolding sigma_algebra_def algebra_def
+      sigma_algebra_axioms_def by auto
+  show ?thesis
+     using add pos S.finite_additivity_sufficient assms by auto
+qed
+
+lemma prob_x_eq_1_imp_prob_y_eq_0:
+  assumes "{x} \<in> events"
+  assumes "(prob {x} = 1)"
+  assumes "{y} \<in> events"
+  assumes "y \<noteq> x"
+  shows "prob {y} = 0"
+  using prob_one_inter[of "{y}" "{x}"] assms by auto
+
+lemma distribution_x_eq_1_imp_distribution_y_eq_0:
+  assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
+  assumes "(distribution X {x} = 1)"
+  assumes "y \<noteq> x"
+  shows "distribution X {y} = 0"
+proof -
+  let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>"
+  let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>"
+  interpret S: prob_space ?M
+    using distribution_prob_space[OF X] by auto
+  { assume "{x} \<notin> sets ?M"
+    hence "x \<notin> X ` space M" by auto
+    hence "X -` {x} \<inter> space M = {}" by auto
+    hence "distribution X {x} = 0" unfolding distribution_def by auto
+    hence "False" using assms by auto }
+  hence x: "{x} \<in> sets ?M" by auto
+  { assume "{y} \<notin> sets ?M"
+    hence "y \<notin> X ` space M" by auto
+    hence "X -` {y} \<inter> space M = {}" by auto
+    hence "distribution X {y} = 0" unfolding distribution_def by auto }
+  moreover
+  { assume "{y} \<in> sets ?M"
+    hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto }
+  ultimately show ?thesis by auto
+qed
+
+end
+
+end
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/RComplete.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -653,6 +653,18 @@
 lemma floor_subtract_one: "floor (x - 1) = floor x - 1"
   by (rule floor_diff_one) (* already declared [simp] *)
 
+lemma le_mult_floor:
+  assumes "0 \<le> (a :: real)" and "0 \<le> b"
+  shows "floor a * floor b \<le> floor (a * b)"
+proof -
+  have "real (floor a) \<le> a"
+    and "real (floor b) \<le> b" by auto
+  hence "real (floor a * floor b) \<le> a * b"
+    using assms by (auto intro!: mult_mono)
+  also have "a * b < real (floor (a * b) + 1)" by auto
+  finally show ?thesis unfolding real_of_int_less_iff by simp
+qed
+
 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   unfolding real_of_nat_def by simp
 
@@ -821,6 +833,19 @@
   apply simp
 done
 
+lemma less_natfloor:
+  assumes "0 \<le> x" and "x < real (n :: nat)"
+  shows "natfloor x < n"
+proof (rule ccontr)
+  assume "\<not> ?thesis" hence *: "n \<le> natfloor x" by simp
+  note assms(2)
+  also have "real n \<le> real (natfloor x)"
+    using * unfolding real_of_nat_le_iff .
+  finally have "x < real (natfloor x)" .
+  with real_natfloor_le[OF assms(1)]
+  show False by auto
+qed
+
 lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
   apply (rule iffI)
   apply (rule order_trans)
@@ -851,7 +876,7 @@
 
 lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n"
   apply (unfold natfloor_def)
-  apply (subst nat_int [THEN sym]);back;
+  apply (subst (2) nat_int [THEN sym])
   apply (subst eq_nat_nat_iff)
   apply simp
   apply simp
@@ -905,6 +930,83 @@
   apply simp
 done
 
+lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
+  natfloor (x / real y) = natfloor x div y"
+proof -
+  assume "1 <= (x::real)" and "(y::nat) > 0"
+  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
+    by simp
+  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
+    real((natfloor x) mod y)"
+    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
+  have "x = real(natfloor x) + (x - real(natfloor x))"
+    by simp
+  then have "x = real ((natfloor x) div y) * real y +
+      real((natfloor x) mod y) + (x - real(natfloor x))"
+    by (simp add: a)
+  then have "x / real y = ... / real y"
+    by simp
+  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y"
+    by (auto simp add: algebra_simps add_divide_distrib
+      diff_divide_distrib prems)
+  finally have "natfloor (x / real y) = natfloor(...)" by simp
+  also have "... = natfloor(real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
+    by (simp add: add_ac)
+  also have "... = natfloor(real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
+    apply (rule natfloor_add)
+    apply (rule add_nonneg_nonneg)
+    apply (rule divide_nonneg_pos)
+    apply simp
+    apply (simp add: prems)
+    apply (rule divide_nonneg_pos)
+    apply (simp add: algebra_simps)
+    apply (rule real_natfloor_le)
+    apply (insert prems, auto)
+    done
+  also have "natfloor(real((natfloor x) mod y) /
+    real y + (x - real(natfloor x)) / real y) = 0"
+    apply (rule natfloor_eq)
+    apply simp
+    apply (rule add_nonneg_nonneg)
+    apply (rule divide_nonneg_pos)
+    apply force
+    apply (force simp add: prems)
+    apply (rule divide_nonneg_pos)
+    apply (simp add: algebra_simps)
+    apply (rule real_natfloor_le)
+    apply (auto simp add: prems)
+    apply (insert prems, arith)
+    apply (simp add: add_divide_distrib [THEN sym])
+    apply (subgoal_tac "real y = real y - 1 + 1")
+    apply (erule ssubst)
+    apply (rule add_le_less_mono)
+    apply (simp add: algebra_simps)
+    apply (subgoal_tac "1 + real(natfloor x mod y) =
+      real(natfloor x mod y + 1)")
+    apply (erule ssubst)
+    apply (subst real_of_nat_le_iff)
+    apply (subgoal_tac "natfloor x mod y < y")
+    apply arith
+    apply (rule mod_less_divisor)
+    apply auto
+    using real_natfloor_add_one_gt
+    apply (simp add: algebra_simps)
+    done
+  finally show ?thesis by simp
+qed
+
+lemma le_mult_natfloor:
+  assumes "0 \<le> (a :: real)" and "0 \<le> b"
+  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
+  unfolding natfloor_def
+  apply (subst nat_mult_distrib[symmetric])
+  using assms apply simp
+  apply (subst nat_le_eq_zle)
+  using assms le_mult_floor by (auto intro!: mult_nonneg_nonneg)
+
 lemma natceiling_zero [simp]: "natceiling 0 = 0"
   by (unfold natceiling_def, simp)
 
@@ -957,7 +1059,7 @@
   apply (unfold natceiling_def)
   apply (case_tac "x < 0")
   apply simp
-  apply (subst nat_int [THEN sym]);back;
+  apply (subst (2) nat_int [THEN sym])
   apply (subst nat_le_eq_zle)
   apply simp
   apply (rule ceiling_le)
@@ -1042,72 +1144,5 @@
   apply simp
 done
 
-lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
-  natfloor (x / real y) = natfloor x div y"
-proof -
-  assume "1 <= (x::real)" and "(y::nat) > 0"
-  have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
-    by simp
-  then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
-    real((natfloor x) mod y)"
-    by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym])
-  have "x = real(natfloor x) + (x - real(natfloor x))"
-    by simp
-  then have "x = real ((natfloor x) div y) * real y +
-      real((natfloor x) mod y) + (x - real(natfloor x))"
-    by (simp add: a)
-  then have "x / real y = ... / real y"
-    by simp
-  also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y"
-    by (auto simp add: algebra_simps add_divide_distrib
-      diff_divide_distrib prems)
-  finally have "natfloor (x / real y) = natfloor(...)" by simp
-  also have "... = natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
-    by (simp add: add_ac)
-  also have "... = natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y) + (natfloor x) div y"
-    apply (rule natfloor_add)
-    apply (rule add_nonneg_nonneg)
-    apply (rule divide_nonneg_pos)
-    apply simp
-    apply (simp add: prems)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    apply (insert prems, auto)
-    done
-  also have "natfloor(real((natfloor x) mod y) /
-    real y + (x - real(natfloor x)) / real y) = 0"
-    apply (rule natfloor_eq)
-    apply simp
-    apply (rule add_nonneg_nonneg)
-    apply (rule divide_nonneg_pos)
-    apply force
-    apply (force simp add: prems)
-    apply (rule divide_nonneg_pos)
-    apply (simp add: algebra_simps)
-    apply (rule real_natfloor_le)
-    apply (auto simp add: prems)
-    apply (insert prems, arith)
-    apply (simp add: add_divide_distrib [THEN sym])
-    apply (subgoal_tac "real y = real y - 1 + 1")
-    apply (erule ssubst)
-    apply (rule add_le_less_mono)
-    apply (simp add: algebra_simps)
-    apply (subgoal_tac "1 + real(natfloor x mod y) =
-      real(natfloor x mod y + 1)")
-    apply (erule ssubst)
-    apply (subst real_of_nat_le_iff)
-    apply (subgoal_tac "natfloor x mod y < y")
-    apply arith
-    apply (rule mod_less_divisor)
-    apply auto
-    using real_natfloor_add_one_gt
-    apply (simp add: algebra_simps)
-    done
-  finally show ?thesis by simp
-qed
 
 end
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/RealPow.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -6,7 +6,7 @@
 header {* Natural powers theory *}
 
 theory RealPow
-imports RealDef
+imports RealDef RComplete
 begin
 
 (* FIXME: declare this in Rings.thy or not at all *)
@@ -107,6 +107,28 @@
     by (rule power_le_imp_le_base)
 qed
 
+subsection {*Floor*}
+
+lemma floor_power:
+  assumes "x = real (floor x)"
+  shows "floor (x ^ n) = floor x ^ n"
+proof -
+  have *: "x ^ n = real (floor x ^ n)"
+    using assms by (induct n arbitrary: x) simp_all
+  show ?thesis unfolding real_of_int_inject[symmetric]
+    unfolding * floor_real_of_int ..
+qed
+
+lemma natfloor_power:
+  assumes "x = real (natfloor x)"
+  shows "natfloor (x ^ n) = natfloor x ^ n"
+proof -
+  from assms have "0 \<le> floor x" by auto
+  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
+  from floor_power[OF this]
+  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
+    by simp
+qed
 
 subsection {*Various Other Theorems*}
 
@@ -131,4 +153,5 @@
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)
 
+
 end
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Set.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -1656,6 +1656,10 @@
     else if d \<in> A then -B else {})"  
   by (auto simp add: vimage_def) 
 
+lemma vimage_inter_cong:
+  "(\<And> w. w \<in> S \<Longrightarrow> f w = g w) \<Longrightarrow> f -` y \<inter> S = g -` y \<inter> S"
+  by auto
+
 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
 by blast
 
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/SetInterval.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -445,6 +445,47 @@
   apply auto
   done
 
+context ordered_ab_group_add
+begin
+
+lemma
+  fixes x :: 'a
+  shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}"
+  and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}"
+proof safe
+  fix y assume "y < -x"
+  hence *:  "x < -y" using neg_less_iff_less[of "-y" x] by simp
+  have "- (-y) \<in> uminus ` {x<..}"
+    by (rule imageI) (simp add: *)
+  thus "y \<in> uminus ` {x<..}" by simp
+next
+  fix y assume "y \<le> -x"
+  have "- (-y) \<in> uminus ` {x..}"
+    by (rule imageI) (insert `y \<le> -x`[THEN le_imp_neg_le], simp)
+  thus "y \<in> uminus ` {x..}" by simp
+qed simp_all
+
+lemma
+  fixes x :: 'a
+  shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {-x<..}"
+  and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}"
+proof -
+  have "uminus ` {..<x} = uminus ` uminus ` {-x<..}"
+    and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all
+  thus "uminus ` {..<x} = {-x<..}" and "uminus ` {..x} = {-x..}"
+    by (simp_all add: image_image
+        del: image_uminus_greaterThan image_uminus_atLeast)
+qed
+
+lemma
+  fixes x :: 'a
+  shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}"
+  and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}"
+  and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {-y<..-x}"
+  and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
+  by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
+      greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
+end
 
 subsubsection {* Finiteness *}
 
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/SupInf.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -228,6 +228,24 @@
     by  (auto simp add: setge_def setle_def)
 qed
 
+lemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)"
+  by (auto intro!: Sup_eq intro: dense_le)
+
+lemma Sup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x} = (x::real)"
+  by (auto intro!: Sup_eq intro: dense_le_bounded)
+
+lemma Sup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x} = (x::real)"
+  by (auto intro!: Sup_eq intro: dense_le_bounded)
+
+lemma Sup_atMost[simp]: "Sup {..x} = (x::real)"
+  by (auto intro!: Sup_eq_maximum)
+
+lemma Sup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = (x::real)"
+  by (auto intro!: Sup_eq_maximum)
+
+lemma Sup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = (x::real)"
+  by (auto intro!: Sup_eq_maximum)
+
 
 subsection{*Infimum of a set of reals*}
 
@@ -406,6 +424,21 @@
     by (simp add: Inf_real_def)
 qed
 
+lemma Inf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x} = (y::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = (y::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x} = (y::real)"
+  by (simp add: Inf_real_def)
+
+lemma Inf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = (y::real)"
+  by (simp add: Inf_real_def)
+
 subsection{*Relate max and min to Sup and Inf.*}
 
 lemma real_max_Sup:
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 05 17:55:30 2010 +0100
@@ -89,7 +89,7 @@
 fun unregister message thread = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
-      SOME (birth_time, _, description) =>
+      SOME (_, _, description) =>
         let
           val active' = delete_thread thread active;
           val cancelling' = (thread, (Time.now (), description)) :: cancelling;
@@ -267,7 +267,7 @@
                   "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
                 | ERROR msg => ("Error: " ^ msg);
             val _ = unregister message (Thread.self ());
-          in () end)
+          in () end);
       in () end);
 
 
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 05 17:55:30 2010 +0100
@@ -111,14 +111,14 @@
   |> Exn.release
   |> tap (after path);
 
-fun external_prover relevance_filter prepare write cmd args find_failure produce_answer
-    axiom_clauses filtered_clauses name subgoalno goal =
+fun external_prover relevance_filter prepare write cmd args produce_answer name
+    ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
   let
     (* get clauses and prepare them for writing *)
     val (ctxt, (chain_ths, th)) = goal;
     val thy = ProofContext.theory_of ctxt;
     val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths;
-    val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoalno);
+    val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoal);
     val the_filtered_clauses =
       (case filtered_clauses of
         NONE => relevance_filter goal goal_cls
@@ -138,8 +138,8 @@
         Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr)
       in
         if destdir' = "" then File.tmp_path probfile
-        else if File.exists (Path.explode (destdir'))
-        then Path.append  (Path.explode (destdir')) probfile
+        else if File.exists (Path.explode destdir')
+        then Path.append  (Path.explode destdir') probfile
         else error ("No such directory: " ^ destdir')
       end;
 
@@ -167,7 +167,7 @@
       if Config.get ctxt measure_runtime then split_time s else (s, 0)
     fun run_on probfile =
       if File.exists cmd then
-        write probfile clauses
+        write with_full_types probfile clauses
         |> pair (apfst split_time' (bash_output (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd);
 
@@ -178,16 +178,16 @@
       else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
 
     val (((proof, time), rc), conj_pos) =
-      with_path cleanup export run_on (prob_pathname subgoalno);
+      with_path cleanup export run_on (prob_pathname subgoal);
 
     (* check for success and print out some information on failure *)
-    val failure = find_failure proof;
+    val failure = Res_Reconstruct.find_failure proof;
     val success = rc = 0 andalso is_none failure;
     val (message, real_thm_names) =
       if is_some failure then ("External prover failed.", [])
       else if rc <> 0 then ("External prover failed: " ^ proof, [])
       else apfst (fn s => "Try this command: " ^ s)
-        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno));
+        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal));
   in
     {success = success, message = message,
       theorem_names = real_thm_names, runtime = time, proof = proof,
@@ -201,22 +201,17 @@
   let
     val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
       prover_config;
-    val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem;
   in
     external_prover
       (Res_ATP.get_relevant max_new_clauses insert_theory_const)
       (Res_ATP.prepare_clauses false)
-      (Res_HOL_Clause.tptp_write_file with_full_types)
+      Res_HOL_Clause.tptp_write_file
       command
       (arguments timeout)
-      Res_Reconstruct.find_failure
       (if emit_structured_proof then Res_Reconstruct.structured_proof
        else Res_Reconstruct.lemma_list false)
-      axiom_clauses
-      filtered_clauses
       name
-      subgoal
-      goal
+      problem
   end;
 
 fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
@@ -276,22 +271,17 @@
 
 fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
   let
-    val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config
-    val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
+    val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
   in
     external_prover
       (Res_ATP.get_relevant max_new_clauses insert_theory_const)
       (Res_ATP.prepare_clauses true)
-      (Res_HOL_Clause.dfg_write_file with_full_types)
+      Res_HOL_Clause.dfg_write_file
       command
       (arguments timeout)
-      Res_Reconstruct.find_failure
       (Res_Reconstruct.lemma_list true)
-      axiom_clauses
-      filtered_clauses
       name
-      subgoal
-      goal
+      problem
   end;
 
 fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Fri Mar 05 17:55:30 2010 +0100
@@ -714,12 +714,12 @@
   let val _ = trace_msg (fn () =>
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   in
-     if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
-     then (error "metis: Proof state contains the empty sort"; Seq.empty)
-     else
-       (Meson.MESON Res_Axioms.neg_clausify
-         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
-        THEN Res_Axioms.expand_defs_tac st0) st0
+    if exists_type Res_Axioms.type_has_topsort (prop_of st0)
+    then raise METIS "Metis: Proof state contains the universal sort {}"
+    else
+      (Meson.MESON Res_Axioms.neg_clausify
+        (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
+          THEN Res_Axioms.expand_defs_tac st0) st0
   end
   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
 
@@ -734,7 +734,7 @@
   type_lits_setup #>
   method @{binding metis} HO "METIS for FOL & HOL problems" #>
   method @{binding metisF} FO "METIS for FOL problems" #>
-  method @{binding metisFT} FT "METIS With-fully typed translation" #>
+  method @{binding metisFT} FT "METIS with fully-typed translation" #>
   Method.setup @{binding finish_clausify}
     (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
     "cleanup after conversion to clauses";
diff -r c0db094d0d80 -r d80f417269b4 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Mar 05 17:55:30 2010 +0100
@@ -12,7 +12,7 @@
   val pairname: thm -> string * thm
   val multi_base_blacklist: string list
   val bad_for_atp: thm -> bool
-  val type_has_empty_sort: typ -> bool
+  val type_has_topsort: typ -> bool
   val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
   val neg_clausify: thm list -> thm list
   val expand_defs_tac: thm -> tactic
@@ -31,10 +31,10 @@
 
 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
 
-fun type_has_empty_sort (TFree (_, [])) = true
-  | type_has_empty_sort (TVar (_, [])) = true
-  | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
-  | type_has_empty_sort _ = false;
+val type_has_topsort = Term.exists_subtype
+  (fn TFree (_, []) => true
+    | TVar (_, []) => true
+    | _ => false);
 
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -321,7 +321,7 @@
 
 fun bad_for_atp th =
   too_complex (prop_of th)
-  orelse exists_type type_has_empty_sort (prop_of th)
+  orelse exists_type type_has_topsort (prop_of th)
   orelse is_strange_thm th;
 
 val multi_base_blacklist =
diff -r c0db094d0d80 -r d80f417269b4 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Fri Mar 05 17:55:30 2010 +0100
@@ -240,7 +240,6 @@
      ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & (LUB i. X i) = s)"
 apply (auto simp add: fstreams_lub_lemma1)
 apply (rule_tac x="%n. stream_take n$s" in exI, auto)
-apply (simp add: chain_stream_take)
 apply (induct_tac i, auto)
 apply (drule fstreams_lub_lemma1, auto)
 apply (rule_tac x="j" in exI, auto)
@@ -293,7 +292,6 @@
       ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & (LUB i. X i) = ms)"
 apply (auto simp add: fstreams_lub_lemma2)
 apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
-apply (simp add: chain_stream_take)
 apply (induct_tac i, auto)
 apply (drule fstreams_lub_lemma2, auto)
 apply (rule_tac x="j" in exI, auto)
diff -r c0db094d0d80 -r d80f417269b4 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Mar 05 17:55:30 2010 +0100
@@ -188,6 +188,13 @@
         (Thm.no_attributes (Binding.name name, thm))
     ||> Sign.parent_path;
 
+fun add_qualified_simp_thm name (path, thm) thy =
+    thy
+    |> Sign.add_path path
+    |> yield_singleton PureThy.add_thms
+        ((Binding.name name, thm), [Simplifier.simp_add])
+    ||> Sign.parent_path;
+
 (******************************************************************************)
 (************************** defining take functions ***************************)
 (******************************************************************************)
@@ -262,9 +269,9 @@
         val goal = mk_trp (mk_chain take_const);
         val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
         val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
-        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
+        val thm = Goal.prove_global thy [] [] goal (K tac);
       in
-        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
+        add_qualified_simp_thm "chain_take" (dname, thm) thy
       end;
     val (chain_take_thms, thy) =
       fold_map prove_chain_take (take_consts ~~ dnames) thy;
@@ -342,17 +349,17 @@
           (conjuncts dnames deflation_take_thm)) thy;
 
     (* prove strictness of take functions *)
-    fun prove_take_strict (take_const, dname) thy =
+    fun prove_take_strict (deflation_take, dname) thy =
       let
-        val goal = mk_trp (mk_strict (take_const $ Free ("n", natT)));
-        val tac = rtac @{thm deflation_strict} 1
-                  THEN resolve_tac deflation_take_thms 1;
-        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
+        val take_strict_thm =
+            Drule.export_without_context
+            (@{thm deflation_strict} OF [deflation_take]);
       in
         add_qualified_thm "take_strict" (dname, take_strict_thm) thy
       end;
     val (take_strict_thms, thy) =
-      fold_map prove_take_strict (take_consts ~~ dnames) thy;
+      fold_map prove_take_strict
+        (deflation_take_thms ~~ dnames) thy;
 
     (* prove take/take rules *)
     fun prove_take_take ((chain_take, deflation_take), dname) thy =
@@ -367,6 +374,19 @@
       fold_map prove_take_take
         (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
 
+    (* prove take_below rules *)
+    fun prove_take_below (deflation_take, dname) thy =
+      let
+        val take_below_thm =
+            Drule.export_without_context
+            (@{thm deflation.below} OF [deflation_take]);
+      in
+        add_qualified_thm "take_below" (dname, take_below_thm) thy
+      end;
+    val (take_below_thms, thy) =
+      fold_map prove_take_below
+        (deflation_take_thms ~~ dnames) thy;
+
     (* define finiteness predicates *)
     fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
       let
diff -r c0db094d0d80 -r d80f417269b4 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 17:55:14 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 17:55:30 2010 +0100
@@ -196,15 +196,20 @@
         pat_rews @ dist_les @ dist_eqs)
 end; (* let *)
 
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
+fun prove_coinduction
+    (comp_dnam, eqs : eq list)
+    (take_lemmas : thm list)
+    (thy : theory) : thm * theory =
 let
-val map_tab = Domain_Take_Proofs.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
-val conss  = map  snd        eqs;
 val comp_dname = Sign.full_bname thy comp_dnam;
+fun dc_take dn = %%:(dn^"_take");
+val x_name = idx_name dnames "x"; 
+val n_eqs = length eqs;
 
-val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+val take_rews =
+    maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
 
 (* ----- define bisimulation predicate -------------------------------------- *)
 
@@ -280,6 +285,74 @@
         ||> Sign.parent_path;
 end; (* local *)
 
+(* ----- theorem concerning coinduction ------------------------------------- *)
+
+local
+  val pg = pg' thy;
+  val xs = mapn (fn n => K (x_name n)) 1 dnames;
+  fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
+  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+  val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+  val _ = trace " Proving coind_lemma...";
+  val coind_lemma =
+    let
+      fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
+      fun mk_eqn n dn =
+        (dc_take dn $ %:"n" ` bnd_arg n 0) ===
+        (dc_take dn $ %:"n" ` bnd_arg n 1);
+      fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
+      val goal =
+        mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
+          Library.foldr mk_all2 (xs,
+            Library.foldr mk_imp (mapn mk_prj 0 dnames,
+              foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
+      fun x_tacs ctxt n x = [
+        rotate_tac (n+1) 1,
+        etac all2E 1,
+        eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+        TRY (safe_tac HOL_cs),
+        REPEAT (CHANGED (asm_simp_tac take_ss 1))];
+      fun tacs ctxt = [
+        rtac impI 1,
+        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
+        simp_tac take_ss 1,
+        safe_tac HOL_cs] @
+        flat (mapn (x_tacs ctxt) 0 xs);
+    in pg [ax_bisim_def] goal tacs end;
+in
+  val _ = trace " Proving coind...";
+  val coind = 
+    let
+      fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
+      fun mk_eqn x = %:x === %:(x^"'");
+      val goal =
+        mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
+          Logic.list_implies (mapn mk_prj 0 xs,
+            mk_trp (foldr1 mk_conj (map mk_eqn xs)));
+      val tacs =
+        TRY (safe_tac HOL_cs) ::
+        maps (fn take_lemma => [
+          rtac take_lemma 1,
+          cut_facts_tac [coind_lemma] 1,
+          fast_tac HOL_cs 1])
+        take_lemmas;
+    in pg [] goal (K tacs) end;
+end; (* local *)
+
+in
+  (coind, thy)
+end;
+
+fun comp_theorems (comp_dnam, eqs: eq list) thy =
+let
+val map_tab = Domain_Take_Proofs.get_map_tab thy;
+
+val dnames = map (fst o fst) eqs;
+val conss  = map  snd        eqs;
+val comp_dname = Sign.full_bname thy comp_dnam;
+
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
@@ -556,58 +629,7 @@
 
 end; (* local *)
 
-(* ----- theorem concerning coinduction ------------------------------------- *)
-
-local
-  val xs = mapn (fn n => K (x_name n)) 1 dnames;
-  fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
-  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
-  val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
-  val _ = trace " Proving coind_lemma...";
-  val coind_lemma =
-    let
-      fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
-      fun mk_eqn n dn =
-        (dc_take dn $ %:"n" ` bnd_arg n 0) ===
-        (dc_take dn $ %:"n" ` bnd_arg n 1);
-      fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
-      val goal =
-        mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
-          Library.foldr mk_all2 (xs,
-            Library.foldr mk_imp (mapn mk_prj 0 dnames,
-              foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
-      fun x_tacs ctxt n x = [
-        rotate_tac (n+1) 1,
-        etac all2E 1,
-        eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
-        TRY (safe_tac HOL_cs),
-        REPEAT (CHANGED (asm_simp_tac take_ss 1))];
-      fun tacs ctxt = [
-        rtac impI 1,
-        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
-        simp_tac take_ss 1,
-        safe_tac HOL_cs] @
-        flat (mapn (x_tacs ctxt) 0 xs);
-    in pg [ax_bisim_def] goal tacs end;
-in
-  val _ = trace " Proving coind...";
-  val coind = 
-    let
-      fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
-      fun mk_eqn x = %:x === %:(x^"'");
-      val goal =
-        mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
-          Logic.list_implies (mapn mk_prj 0 xs,
-            mk_trp (foldr1 mk_conj (map mk_eqn xs)));
-      val tacs =
-        TRY (safe_tac HOL_cs) ::
-        maps (fn take_lemma => [
-          rtac take_lemma 1,
-          cut_facts_tac [coind_lemma] 1,
-          fast_tac HOL_cs 1])
-        take_lemmas;
-    in pg [] goal (K tacs) end;
-end; (* local *)
+val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy;
 
 val inducts = Project_Rule.projections (ProofContext.init thy) ind;
 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);