# HG changeset patch
# User paulson
# Date 1256730151 0
# Node ID 7be66dee1a5ae6c9dfa8058060d6e02b13298498
# Parent  320a1d67b9ae62cc4fb8d4ad149339dc868def29
New theory Probability, which contains a development of measure theory

diff -r 320a1d67b9ae -r 7be66dee1a5a NEWS
--- a/NEWS	Tue Oct 27 14:46:03 2009 +0000
+++ b/NEWS	Wed Oct 28 11:42:31 2009 +0000
@@ -67,6 +67,8 @@
 
 * New theory SupInf of the supremum and infimum operators for sets of reals.
 
+* New theory Probability containing a development of measure theory, eventually leading to Lebesgue integration and probability.
+
 * Split off prime number ingredients from theory GCD
 to theory Number_Theory/Primes;
 
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/IsaMakefile	Wed Oct 28 11:42:31 2009 +0000
@@ -51,6 +51,7 @@
   HOL-Nominal-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
+  HOL-Probability \
   HOL-Prolog \
   HOL-SET_Protocol \
   HOL-SMT-Examples \
@@ -1060,6 +1061,18 @@
   Multivariate_Analysis/Convex_Euclidean_Space.thy
 	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
 
+## HOL-Probability
+
+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
+	$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
+
 ## HOL-Nominal
 
 HOL-Nominal: HOL $(OUT)/HOL-Nominal
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Library/FuncSet.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -101,6 +101,19 @@
 lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
 by auto
 
+lemma prod_final:
+  assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
+  shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
+proof (rule Pi_I) 
+  fix z
+  assume z: "z \<in> A" 
+  have "f z = (fst (f z), snd (f z))" 
+    by simp
+  also have "...  \<in> B z \<times> C z"
+    by (metis SigmaI PiE o_apply 1 2 z) 
+  finally show "f z \<in> B z \<times> C z" .
+qed
+
 
 subsection{*Composition With a Restricted Domain: @{term compose}*}
 
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Probability/Caratheodory.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Caratheodory.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,993 @@
+header {*Caratheodory Extension Theorem*}
+
+theory Caratheodory
+  imports Sigma_Algebra SupInf SeriesPlus
+
+begin
+
+text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
+
+subsection {* Measure Spaces *}
+
+text {*A measure assigns a nonnegative real to every measurable set. 
+       It is countably additive for disjoint sets.*}
+
+record 'a measure_space = "'a algebra" +
+  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 = {})"
+
+definition
+  positive  where
+  "positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)"
+
+definition
+  additive  where
+  "additive M f \<longleftrightarrow> 
+    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 
+    \<longrightarrow> f (x \<union> y) = f x + f y)"
+
+definition
+  countably_additive  where
+  "countably_additive M f \<longleftrightarrow> 
+    (\<forall>A. 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))"
+
+definition
+  increasing  where
+  "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
+
+definition
+  subadditive  where
+  "subadditive M f \<longleftrightarrow> 
+    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 
+    \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
+
+definition
+  countably_subadditive  where
+  "countably_subadditive M f \<longleftrightarrow> 
+    (\<forall>A. range A \<subseteq> sets M \<longrightarrow> 
+         disjoint_family A \<longrightarrow>
+         (\<Union>i. A i) \<in> sets M \<longrightarrow> 
+         summable (f o A) \<longrightarrow>
+         f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))"
+
+definition
+  lambda_system where
+  "lambda_system M f = 
+    {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
+
+definition
+  outer_measure_space where
+  "outer_measure_space M f  \<longleftrightarrow> 
+     positive M f & increasing M f & countably_subadditive M f"
+
+definition
+  measure_set where
+  "measure_set M f X =
+     {r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
+
+
+locale measure_space = sigma_algebra +
+  assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> measure M a"
+      and empty_measure [simp]: "measure M {} = (0::real)"
+      and ca: "countably_additive M (measure M)"
+
+subsection {* Basic Lemmas *}
+
+lemma positive_imp_0: "positive M f \<Longrightarrow> f {} = 0"
+  by (simp add: positive_def) 
+
+lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x"
+  by (simp add: positive_def) 
+
+lemma increasingD:
+     "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
+  by (auto simp add: increasing_def)
+
+lemma subadditiveD:
+     "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
+      \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
+  by (auto simp add: subadditive_def)
+
+lemma additiveD:
+     "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
+      \<Longrightarrow> f (x \<union> y) = f x + f y"
+  by (auto simp add: additive_def)
+
+lemma countably_additiveD:
+  "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) 
+
+lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
+  by blast
+
+lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A"
+  by blast
+
+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) 
+
+subsection {* A Two-Element Series *}
+
+definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
+  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) 
+  done
+
+lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
+  by (simp add: UNION_eq_Union_image range_binaryset_eq) 
+
+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 
+      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) 
+    qed
+  moreover
+  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" 
+    by metis
+  hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
+    by simp
+  thus ?thesis by (rule LIMSEQ_offset [where k=2])
+qed
+
+lemma binaryset_sums:
+  assumes f: "f {} = 0"
+  shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
+    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) 
+
+lemma suminf_binaryset_eq:
+     "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
+  by (metis binaryset_sums sums_unique)
+
+
+subsection {* Lambda Systems *}
+
+lemma (in algebra) lambda_system_eq:
+    "lambda_system M f = 
+        {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
+proof -
+  have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
+    by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space)
+  show ?thesis
+    by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+
+qed
+
+lemma (in algebra) lambda_system_empty:
+    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
+  by (auto simp add: positive_def lambda_system_eq) 
+
+lemma lambda_system_sets:
+    "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
+  by (simp add:  lambda_system_def)
+
+lemma (in algebra) lambda_system_Compl:
+  fixes f:: "'a set \<Rightarrow> real"
+  assumes x: "x \<in> lambda_system M f"
+  shows "space M - x \<in> lambda_system M f"
+  proof -
+    have "x \<subseteq> space M"
+      by (metis sets_into_space lambda_system_sets x)
+    hence "space M - (space M - x) = x"
+      by (metis double_diff equalityE) 
+    with x show ?thesis
+      by (force simp add: lambda_system_def)
+  qed
+
+lemma (in algebra) lambda_system_Int:
+  fixes f:: "'a set \<Rightarrow> real"
+  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+  shows "x \<inter> y \<in> lambda_system M f"
+  proof -
+    from xl yl show ?thesis
+      proof (auto simp add: positive_def lambda_system_eq Int)
+	fix u
+	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
+           and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
+           and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
+	have "u - x \<inter> y \<in> sets M"
+	  by (metis Diff Diff_Int Un u x y)
+	moreover
+	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
+	moreover
+	have "u - x \<inter> y - y = u - y" by blast
+	ultimately
+	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
+	  by force
+	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
+              = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
+	  by (simp add: ey) 
+	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
+	  by (simp add: Int_ac) 
+	also have "... = f (u \<inter> y) + f (u - y)"
+	  using fx [THEN bspec, of "u \<inter> y"] Int y u
+	  by force
+	also have "... = f u"
+	  by (metis fy u) 
+	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
+      qed
+  qed
+
+
+lemma (in algebra) lambda_system_Un:
+  fixes f:: "'a set \<Rightarrow> real"
+  assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+  shows "x \<union> y \<in> lambda_system M f"
+proof -
+  have "(space M - x) \<inter> (space M - y) \<in> sets M"
+    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) 
+  moreover
+  have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
+    by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
+  ultimately show ?thesis
+    by (metis lambda_system_Compl lambda_system_Int xl yl) 
+qed
+
+lemma (in algebra) lambda_system_algebra:
+    "positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
+  apply (auto simp add: algebra_def) 
+  apply (metis lambda_system_sets set_mp sets_into_space)
+  apply (metis lambda_system_empty)
+  apply (metis lambda_system_Compl)
+  apply (metis lambda_system_Un) 
+  done
+
+lemma (in algebra) lambda_system_strong_additive:
+  assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}"
+      and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+  shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
+  proof -
+    have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
+    moreover
+    have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
+    moreover 
+    have "(z \<inter> (x \<union> y)) \<in> sets M"
+      by (metis Int Un lambda_system_sets xl yl z) 
+    ultimately show ?thesis using xl yl
+      by (simp add: lambda_system_eq)
+  qed
+
+lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x"
+  by (metis Int_absorb1 sets_into_space)
+
+lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x"
+  by (metis Int_absorb2 sets_into_space)
+
+lemma (in algebra) lambda_system_additive:
+     "additive (M (|sets := lambda_system M f|)) f"
+  proof (auto simp add: additive_def)
+    fix x and y
+    assume disj: "x \<inter> y = {}"
+       and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
+    hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
+    thus "f (x \<union> y) = f x + f y" 
+      using lambda_system_strong_additive [OF top disj xl yl]
+      by (simp add: Un)
+  qed
+
+
+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) 
+  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> 
+         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> 
+         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 
+
+
+definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
+  where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)"
+
+lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  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) 
+  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) 
+     (metis neq_iff Int_commute less_disjoint_disjointed)
+
+lemma disjointed_subset: "disjointed A n \<subseteq> A n"
+  by (auto simp add: disjointed_def)
+
+
+lemma (in algebra) UNION_in_sets:
+  fixes A:: "nat \<Rightarrow> 'a set"
+  assumes A: "range A \<subseteq> sets M "
+  shows  "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n) 
+  thus ?case
+    by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff)
+qed
+
+lemma (in algebra) range_disjointed_sets:
+  assumes A: "range A \<subseteq> sets M "
+  shows  "range (disjointed A) \<subseteq> sets M"
+proof (auto simp add: disjointed_def) 
+  fix n
+  show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
+    by (metis A Diff UNIV_I disjointed_def image_subset_iff)
+qed
+
+lemma sigma_algebra_disjoint_iff: 
+     "sigma_algebra M \<longleftrightarrow> 
+      algebra M &
+      (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> 
+           (\<Union>i::nat. A i) \<in> sets M)"
+proof (auto simp add: sigma_algebra_iff)
+  fix A :: "nat \<Rightarrow> 'a set"
+  assume M: "algebra M"
+     and A: "range A \<subseteq> sets M"
+     and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow>
+               disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+  hence "range (disjointed A) \<subseteq> sets M \<longrightarrow>
+         disjoint_family (disjointed A) \<longrightarrow>
+         (\<Union>i. disjointed A i) \<in> sets M" by blast
+  hence "(\<Union>i. disjointed A i) \<in> sets M"
+    by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) 
+  thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq)
+qed
+
+
+lemma (in algebra) additive_sum:
+  fixes A:: "nat \<Rightarrow> 'a set"
+  assumes f: "positive M f" and ad: "additive M f"
+      and A: "range A \<subseteq> sets M"
+      and disj: "disjoint_family A"
+  shows  "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
+proof (induct n)
+  case 0 show ?case using f by (simp add: positive_def) 
+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
+  moreover 
+  have "A n \<in> sets M" using A by blast 
+  moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+    by (metis A UNION_in_sets atLeast0LessThan)
+  moreover 
+  ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
+    using ad UNION_in_sets A by (auto simp add: additive_def) 
+  with Suc.hyps show ?case using ad
+    by (auto simp add: atLeastLessThanSuc additive_def) 
+qed
+
+
+lemma countably_subadditiveD:
+  "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
+   (\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)" 
+  by (auto simp add: countably_subadditive_def o_def)
+
+lemma (in algebra) increasing_additive_summable:
+  fixes A:: "nat \<Rightarrow> 'a set"
+  assumes f: "positive M f" and ad: "additive M f"
+      and inc: "increasing M f"
+      and A: "range A \<subseteq> sets M"
+      and disj: "disjoint_family A"
+  shows  "summable (f o A)"
+proof (rule pos_summable) 
+  fix n
+  show "0 \<le> (f \<circ> A) n" using f A
+    by (force simp add: positive_def)
+  next
+  fix n
+  have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
+    by (rule additive_sum [OF f ad A disj]) 
+  also have "... \<le> f (space M)" using space_closed A
+    by (blast intro: increasingD [OF inc] UNION_in_sets top) 
+  finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" .
+qed
+
+lemma lambda_system_positive:
+     "positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f"
+  by (simp add: positive_def lambda_system_def) 
+
+lemma lambda_system_increasing:
+   "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
+  by (simp add: increasing_def lambda_system_def) 
+
+lemma (in algebra) lambda_system_strong_sum:
+  fixes A:: "nat \<Rightarrow> 'a set"
+  assumes f: "positive M f" and a: "a \<in> sets M"
+      and A: "range A \<subseteq> lambda_system M f"
+      and disj: "disjoint_family A"
+  shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
+proof (induct n)
+  case 0 show ?case using f by (simp add: positive_def) 
+next
+  case (Suc n) 
+  have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
+    by (force simp add: disjoint_family_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"
+    using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] 
+    by simp
+  from Suc.hyps show ?case
+    by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
+qed
+
+
+lemma (in sigma_algebra) lambda_system_caratheodory:
+  assumes oms: "outer_measure_space M f"
+      and A: "range A \<subseteq> lambda_system M f"
+      and disj: "disjoint_family A"
+  shows  "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A)  sums  f (\<Union>i. A i)"
+proof -
+  have pos: "positive M f" and inc: "increasing M f" 
+   and csa: "countably_subadditive M f" 
+    by (metis oms outer_measure_space_def)+
+  have sa: "subadditive M f"
+    by (metis countably_subadditive_subadditive csa pos) 
+  have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A 
+    by simp
+  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
+    by (rule lambda_system_algebra [OF pos]) 
+  have A'': "range A \<subseteq> sets M"
+     by (metis A image_subset_iff lambda_system_sets)
+  have sumfA: "summable (f \<circ> A)" 
+    by (metis algebra.increasing_additive_summable [OF alg_ls]
+          lambda_system_positive lambda_system_additive lambda_system_increasing
+          A' oms outer_measure_space_def disj)
+  have U_in: "(\<Union>i. A i) \<in> sets M"
+    by (metis A countable_UN image_subset_iff lambda_system_sets)
+  have U_eq: "f (\<Union>i. A i) = suminf (f o A)" 
+    proof (rule antisym)
+      show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
+	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
+      show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
+	by (rule suminf_le [OF sumfA]) 
+           (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
+	          lambda_system_positive lambda_system_additive 
+                  subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) 
+    qed
+  {
+    fix a 
+    assume a [iff]: "a \<in> sets M" 
+    have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
+    proof -
+      have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' 
+	apply -
+	apply (rule summable_comparison_test [OF _ sumfA]) 
+	apply (rule_tac x="0" in exI) 
+	apply (simp add: positive_def) 
+	apply (auto simp add: )
+	apply (subst abs_of_nonneg)
+	apply (metis A'' Int UNIV_I a image_subset_iff)
+	apply (blast intro:  increasingD [OF inc] a)   
+	done
+      show ?thesis
+      proof (rule antisym)
+	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
+	  by blast
+	moreover 
+	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
+	  by (auto simp add: disjoint_family_def) 
+	moreover 
+	have "a \<inter> (\<Union>i. A i) \<in> sets M"
+	  by (metis Int U_in a)
+	ultimately 
+	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
+	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
+	  by (simp add: o_def) 
+	moreover 
+	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
+	  proof (rule suminf_le [OF summ])
+	    fix n
+	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+	      by (metis A'' UNION_in_sets) 
+	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
+	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
+	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
+	      by (simp add: A) 
+	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
+	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
+	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
+	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
+                               UNION_in U_in a) 
+	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
+	      using eq_fa
+	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
+                            a A disj)
+	  qed
+	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
+	  by arith
+      next
+	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
+	  by (blast intro:  increasingD [OF inc] a U_in)
+	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
+	  by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
+	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
+        qed
+     qed
+  }
+  thus  ?thesis
+    by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA)
+qed
+
+lemma (in sigma_algebra) caratheodory_lemma:
+  assumes oms: "outer_measure_space M f"
+  shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)"
+proof -
+  have pos: "positive M f" 
+    by (metis oms outer_measure_space_def)
+  have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)"
+    using lambda_system_algebra [OF pos]
+    by (simp add: algebra_def) 
+  then moreover 
+  have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)"
+    using lambda_system_caratheodory [OF oms]
+    by (simp add: sigma_algebra_disjoint_iff) 
+  moreover 
+  have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" 
+    using pos lambda_system_caratheodory [OF oms]
+    by (simp add: measure_space_axioms_def positive_def lambda_system_sets 
+                  countably_additive_def o_def) 
+  ultimately 
+  show ?thesis
+    by intro_locales (auto simp add: sigma_algebra_def) 
+qed
+
+
+lemma (in algebra) inf_measure_nonempty:
+  assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
+  shows "f b \<in> measure_set M f a"
+proof -
+  have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}"
+    by (rule series_zero)  (simp add: positive_imp_0 [OF f]) 
+  also have "... = f b" 
+    by simp
+  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) 
+qed  
+
+lemma (in algebra) inf_measure_pos0:
+     "positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x"
+apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero)
+apply blast
+done
+
+lemma (in algebra) inf_measure_pos:
+  shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)"
+apply (rule Inf_greatest)
+apply (metis emptyE inf_measure_nonempty top)
+apply (metis inf_measure_pos0) 
+done
+
+lemma (in algebra) additive_increasing:
+  assumes posf: "positive M f" and addf: "additive M f" 
+  shows "increasing M f"
+proof (auto simp add: increasing_def) 
+  fix x y
+  assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
+  have "f x \<le> f x + f (y-x)" using posf
+    by (simp add: positive_def) (metis Diff xy)
+  also have "... = f (x \<union> (y-x))" using addf
+    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy) 
+  also have "... = f y"
+    by (metis Un_Diff_cancel Un_absorb1 xy)
+  finally show "f x \<le> f y" .
+qed
+
+lemma (in algebra) countably_additive_additive:
+  assumes posf: "positive M f" and ca: "countably_additive M f" 
+  shows "additive M f"
+proof (auto simp add: additive_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> 
+         f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
+    using ca
+    by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) 
+  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
+         f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))"
+    by (simp add: range_binaryset_eq UN_binaryset_eq)
+  thus "f (x \<union> y) = f x + f y" using posf x y
+    by (simp add: Un suminf_binaryset_eq positive_def)
+qed 
+ 
+lemma (in algebra) inf_measure_agrees:
+  assumes posf: "positive M f" and ca: "countably_additive M f" 
+      and s: "s \<in> sets M"  
+  shows "Inf (measure_set M f s) = f s"
+proof (rule Inf_eq) 
+  fix z
+  assume z: "z \<in> measure_set M f s"
+  from this obtain A where 
+    A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
+    and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)"
+    and si: "suminf (f \<circ> A) = z"
+    by (auto simp add: measure_set_def sums_iff) 
+  hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
+  have inc: "increasing M f"
+    by (metis additive_increasing ca countably_additive_additive posf)
+  have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
+    proof (rule countably_additiveD [OF ca]) 
+      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)
+      show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
+	by (metis UN_extend_simps(4) s seq)
+    qed
+  hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
+    by (metis Int_commute UN_simps(4) seq sums_iff) 
+  also have "... \<le> suminf (f \<circ> A)" 
+    proof (rule summable_le [OF _ _ sm]) 
+      show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
+	by (force intro: increasingD [OF inc]) 
+      show "summable (\<lambda>i. f (A i \<inter> s))" using sums
+	by (simp add: sums_iff) 
+    qed
+  also have "... = z" by (rule si) 
+  finally show "f s \<le> z" .
+next
+  fix y
+  assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u"
+  thus "y \<le> f s"
+    by (blast intro: inf_measure_nonempty [OF posf s subset_refl])
+qed
+
+lemma (in algebra) inf_measure_empty:
+  assumes posf: "positive M f"
+  shows "Inf (measure_set M f {}) = 0"
+proof (rule antisym)
+  show "0 \<le> Inf (measure_set M f {})"
+    by (metis empty_subsetI inf_measure_pos posf) 
+  show "Inf (measure_set M f {}) \<le> 0"
+    by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf
+              positive_imp_0 subset_refl) 
+qed
+
+lemma (in algebra) inf_measure_positive:
+  "positive M f \<Longrightarrow> 
+   positive (| space = space M, sets = Pow (space M) |)
+                  (\<lambda>x. Inf (measure_set M f x))"
+  by (simp add: positive_def inf_measure_empty inf_measure_pos) 
+
+lemma (in algebra) inf_measure_increasing:
+  assumes posf: "positive M f"
+  shows "increasing (| space = space M, sets = Pow (space M) |)
+                    (\<lambda>x. Inf (measure_set M f x))"
+apply (auto simp add: increasing_def) 
+apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf)
+apply (rule Inf_lower) 
+apply (clarsimp simp add: measure_set_def, blast) 
+apply (blast intro: inf_measure_pos0 posf)
+done
+
+
+lemma (in algebra) inf_measure_le:
+  assumes posf: "positive M f" and inc: "increasing M f" 
+      and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}"
+  shows "Inf (measure_set M f s) \<le> x"
+proof -
+  from x
+  obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" 
+             and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x"
+    by (auto simp add: sums_iff)
+  have dA: "range (disjointed A) \<subseteq> sets M"
+    by (metis A range_disjointed_sets)
+  have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n"
+    proof (auto)
+      fix n
+      have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
+	by (auto simp add: positive_def image_subset_iff)
+      also have "... \<le> f (A n)" 
+	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
+      finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
+    qed
+  from Series.summable_le2 [OF this sm]
+  have sda:  "summable (f o disjointed A)"  
+             "suminf (f o disjointed A) \<le> suminf (f \<circ> A)"
+    by blast+
+  hence ley: "suminf (f o disjointed A) \<le> x"
+    by (metis xeq) 
+  from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)"
+    by (simp add: sums_iff) 
+  hence y: "suminf (f o disjointed A) \<in> measure_set M f s"
+    apply (auto simp add: measure_set_def)
+    apply (rule_tac x="disjointed A" in exI) 
+    apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA)
+    done
+  show ?thesis
+    by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf)
+qed
+
+lemma (in algebra) inf_measure_close:
+  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
+  shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) & 
+               (f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e"
+proof -
+  have " measure_set M f s \<noteq> {}" 
+    by (metis emptyE ss inf_measure_nonempty [OF posf top])
+  hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e" 
+    by (rule Inf_close [OF _ e])
+  thus ?thesis 
+    by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto)
+qed
+
+lemma (in algebra) inf_measure_countably_subadditive:
+  assumes posf: "positive M f" and inc: "increasing M f" 
+  shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
+                  (\<lambda>x. Inf (measure_set M f x))"
+proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon)
+  fix A :: "nat \<Rightarrow> 'a set" and e :: real
+    assume A: "range A \<subseteq> Pow (space M)"
+       and disj: "disjoint_family A"
+       and sb: "(\<Union>i. A i) \<subseteq> space M"
+       and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))"
+       and e: "0 < e"
+    have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and>
+                    (f o B) sums l \<and>
+                    l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
+      apply (rule inf_measure_close [OF posf])
+      apply (metis e half mult_pos_pos zero_less_power) 
+      apply (metis UNIV_I UN_subset_iff sb)
+      done
+    hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
+                       A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and>
+                       ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
+      by (rule choice2)
+    then obtain BB ll
+      where BB: "!!n. (range (BB n) \<subseteq> sets M)"
+        and disjBB: "!!n. disjoint_family (BB n)" 
+        and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)"
+        and BBsums: "!!n. (f o BB n) sums ll n"
+        and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
+      by auto blast
+    have llpos: "!!n. 0 \<le> ll n"
+	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
+              range_subsetD BB) 
+    have sll: "summable ll &
+               suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
+      proof -
+	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
+	  by (rule sums_mult [OF power_half_series]) 
+	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
+	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
+	  by (auto simp add: sums_iff) 
+	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
+                 suminf (\<lambda>n. e * (1/2)^(Suc n)) =
+                 suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
+	  by (rule suminf_add [OF sum1 sum0]) 
+	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
+	  by (metis ll llpos abs_of_nonneg)
+	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
+	  by (rule summable_add [OF sum1 sum0]) 
+	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
+	  using Series.summable_le2 [OF 1 2] by auto
+	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
+                         (\<Sum>n. e * (1 / 2) ^ Suc n)"
+	  by (metis 0) 
+	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
+	  by (simp add: eqe) 
+	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
+      qed
+    def C \<equiv> "(split BB) o nat_to_nat2"
+    have C: "!!n. C n \<in> sets M"
+      apply (rule_tac p="nat_to_nat2 n" in PairE)
+      apply (simp add: C_def)
+      apply (metis BB subsetD rangeI)  
+      done
+    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
+      proof (auto simp add: C_def)
+	fix x i
+	assume x: "x \<in> A i"
+	with sbBB [of i] obtain j where "x \<in> BB i j"
+	  by blast	  
+	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
+	  by (metis nat_to_nat2_surj internal_split_def prod.cases 
+                prod_case_split surj_f_inv_f)
+      qed 
+    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
+      by (rule ext)  (auto simp add: C_def) 
+    also have "... sums suminf ll" 
+      proof (rule suminf_2dimen)
+	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
+	  by (force simp add: positive_def)
+	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
+	  by (force simp add: o_def)
+	show "summable ll" using sll
+	  by auto
+      qed
+    finally have Csums: "(f \<circ> C) sums suminf ll" .
+    have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
+      apply (rule inf_measure_le [OF posf inc], auto)
+      apply (rule_tac x="C" in exI)
+      apply (auto simp add: C sbC Csums) 
+      done
+    also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
+      by blast
+    finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> 
+          (\<Sum>n. Inf (measure_set M f (A n))) + e" .
+qed
+
+lemma (in algebra) inf_measure_outer:
+  "positive M f \<Longrightarrow> increasing M f 
+   \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
+                          (\<lambda>x. Inf (measure_set M f x))"
+  by (simp add: outer_measure_space_def inf_measure_positive
+                inf_measure_increasing inf_measure_countably_subadditive) 
+
+(*MOVE UP*)
+
+lemma (in algebra) algebra_subset_lambda_system:
+  assumes posf: "positive M f" and inc: "increasing M f" 
+      and add: "additive M f"
+  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
+                                (\<lambda>x. Inf (measure_set M f x))"
+proof (auto dest: sets_into_space 
+            simp add: algebra.lambda_system_eq [OF algebra_Pow]) 
+  fix x s
+  assume x: "x \<in> sets M"
+     and s: "s \<subseteq> space M"
+  have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s 
+    by blast
+  have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+        \<le> Inf (measure_set M f s)"
+    proof (rule field_le_epsilon) 
+      fix e :: real
+      assume e: "0 < e"
+      from inf_measure_close [OF posf e s]
+      obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
+                   and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
+	           and l: "l \<le> Inf (measure_set M f s) + e"
+	by auto
+      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
+                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
+	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
+      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
+	by (subst additiveD [OF add, symmetric])
+ 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
+      have fsumb: "summable (f \<circ> A)"
+	by (metis fsums sums_iff) 
+      { fix u
+	assume u: "u \<in> sets M"
+	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
+	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
+                        u Int  range_subsetD [OF A]) 
+	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
+          by (rule summable_comparison_test [OF _ fsumb]) simp
+	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
+          proof (rule Inf_lower) 
+            show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
+              apply (simp add: measure_set_def) 
+              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) 
+              apply (auto simp add: disjoint_family_subset [OF disj])
+              apply (blast intro: u range_subsetD [OF A]) 
+              apply (blast dest: subsetD [OF sUN])
+              apply (metis 1 o_assoc sums_iff) 
+              done
+          next
+            show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x"
+              by (blast intro: inf_measure_pos0 [OF posf]) 
+            qed
+          note 1 2
+      } note lesum = this
+      have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)"
+        and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)"
+        and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
+        and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) 
+                   \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
+	by (metis Diff lesum top x)+
+      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+           \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
+	by (simp add: x)
+      also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] 
+	by (simp add: x) (simp add: o_def) 
+      also have "... \<le> Inf (measure_set M f s) + e"
+	by (metis fsums l sums_unique) 
+      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+        \<le> Inf (measure_set M f s) + e" .
+    qed
+  moreover 
+  have "Inf (measure_set M f s)
+       \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
+    proof -
+    have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
+      by (metis Un_Diff_Int Un_commute)
+    also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" 
+      apply (rule subadditiveD) 
+      apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 
+	       inf_measure_positive inf_measure_countably_subadditive posf inc)
+      apply (auto simp add: subsetD [OF s])  
+      done
+    finally show ?thesis .
+    qed
+  ultimately 
+  show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
+        = Inf (measure_set M f s)"
+    by (rule order_antisym)
+qed
+
+lemma measure_down:
+     "measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
+      (measure M = measure N) \<Longrightarrow> measure_space M"
+  by (simp add: measure_space_def measure_space_axioms_def positive_def 
+                countably_additive_def) 
+     blast
+
+theorem (in algebra) caratheodory:
+  assumes posf: "positive M f" and ca: "countably_additive M f" 
+  shows "\<exists>MS :: 'a measure_space. 
+             (\<forall>s \<in> sets M. measure MS s = f s) \<and>
+             ((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and>
+             measure_space MS" 
+  proof -
+    have inc: "increasing M f"
+      by (metis additive_increasing ca countably_additive_additive posf) 
+    let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
+    def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
+    have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)"
+      using sigma_algebra.caratheodory_lemma
+              [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
+      by (simp add: ls_def)
+    hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)"
+      by (simp add: measure_space_def) 
+    have "sets M \<subseteq> ls" 
+      by (simp add: ls_def)
+         (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
+    hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" 
+      using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
+      by simp
+    have "measure_space (|space = space M, 
+                          sets = sigma_sets (space M) (sets M),
+                          measure = ?infm|)"
+      by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) 
+         (simp_all add: sgs_sb space_closed)
+    thus ?thesis
+      by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) 
+qed
+
+end
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Probability/Measure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Measure.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,916 @@
+header {*Measures*}
+
+theory Measure
+  imports Caratheodory FuncSet
+begin
+
+text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
+
+definition prod_sets where
+  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
+
+lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
+  by (auto simp add: prod_sets_def) 
+
+definition
+  closed_cdi  where
+  "closed_cdi M \<longleftrightarrow>
+   sets M \<subseteq> Pow (space M) &
+   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
+   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
+        (\<Union>i. A i) \<in> sets M) &
+   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+
+
+inductive_set
+  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
+  for M
+  where
+    Basic [intro]: 
+      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
+  | Compl [intro]:
+      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
+  | Inc:
+      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
+       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
+  | Disj:
+      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
+       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
+  monos Pow_mono
+
+
+definition
+  smallest_closed_cdi  where
+  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
+
+definition
+  measurable  where
+  "measurable a b = {f . sigma_algebra a & sigma_algebra b &
+			 f \<in> (space a -> space b) &
+			 (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
+
+definition
+  measure_preserving  where
+  "measure_preserving m1 m2 =
+     measurable m1 m2 \<inter> 
+     {f . measure_space m1 & measure_space m2 &
+          (\<forall>y \<in> sets m2. measure m1 ((f -` y) \<inter> (space m1)) = measure m2 y)}"
+
+lemma space_smallest_closed_cdi [simp]:
+     "space (smallest_closed_cdi M) = space M"
+  by (simp add: smallest_closed_cdi_def)
+
+
+lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
+  by (auto simp add: smallest_closed_cdi_def) 
+
+lemma (in algebra) smallest_ccdi_sets:
+     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
+  apply (rule subsetI) 
+  apply (erule smallest_ccdi_sets.induct) 
+  apply (auto intro: range_subsetD dest: sets_into_space)
+  done
+
+lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
+  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
+  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
+  done
+
+lemma (in algebra) smallest_closed_cdi3:
+     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
+  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) 
+
+lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
+  by (simp add: closed_cdi_def) 
+
+lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
+  by (simp add: closed_cdi_def) 
+
+lemma closed_cdi_Inc:
+     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
+        (\<Union>i. A i) \<in> sets M"
+  by (simp add: closed_cdi_def) 
+
+lemma closed_cdi_Disj:
+     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+  by (simp add: closed_cdi_def) 
+
+lemma closed_cdi_Un:
+  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
+      and A: "A \<in> sets M" and B: "B \<in> sets M"
+      and disj: "A \<inter> B = {}"
+    shows "A \<union> B \<in> sets M"
+proof -
+  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) 
+ from closed_cdi_Disj [OF cdi ra di]
+ show ?thesis
+   by (simp add: UN_binaryset_eq) 
+qed
+
+lemma (in algebra) smallest_ccdi_sets_Un:
+  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
+      and disj: "A \<inter> B = {}"
+    shows "A \<union> B \<in> smallest_ccdi_sets M"
+proof -
+  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) 
+  from Disj [OF ra di]
+  show ?thesis
+    by (simp add: UN_binaryset_eq) 
+qed
+
+
+
+lemma (in algebra) smallest_ccdi_sets_Int1:
+  assumes a: "a \<in> sets M"
+  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
+proof (induct rule: smallest_ccdi_sets.induct)
+  case (Basic x)
+  thus ?case
+    by (metis a Int smallest_ccdi_sets.Basic)
+next
+  case (Compl x)
+  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
+    by blast
+  also have "... \<in> smallest_ccdi_sets M" 
+    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
+           Diff_disjoint Int_Diff Int_empty_right Un_commute
+           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
+           smallest_ccdi_sets_Un) 
+  finally show ?case .
+next
+  case (Inc A)
+  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
+    by blast
+  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
+    by blast
+  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
+    by (simp add: Inc) 
+  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
+    by blast
+  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
+    by (rule smallest_ccdi_sets.Inc) 
+  show ?case
+    by (metis 1 2)
+next
+  case (Disj A)
+  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
+    by blast
+  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) 
+  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
+    by (metis 1 2)
+qed
+
+
+lemma (in algebra) smallest_ccdi_sets_Int:
+  assumes b: "b \<in> smallest_ccdi_sets M"
+  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
+proof (induct rule: smallest_ccdi_sets.induct)
+  case (Basic x)
+  thus ?case
+    by (metis b smallest_ccdi_sets_Int1)
+next
+  case (Compl x)
+  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
+    by blast
+  also have "... \<in> smallest_ccdi_sets M"
+    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b 
+           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) 
+  finally show ?case .
+next
+  case (Inc A)
+  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
+    by blast
+  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
+    by blast
+  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
+    by (simp add: Inc) 
+  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
+    by blast
+  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
+    by (rule smallest_ccdi_sets.Inc) 
+  show ?case
+    by (metis 1 2)
+next
+  case (Disj A)
+  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
+    by blast
+  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) 
+  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
+    by (metis 1 2)
+qed
+
+lemma (in algebra) sets_smallest_closed_cdi_Int:
+   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
+    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
+  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) 
+
+lemma algebra_iff_Int:
+     "algebra M \<longleftrightarrow> 
+       sets M \<subseteq> Pow (space M) & {} \<in> sets M & 
+       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
+       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
+proof (auto simp add: algebra.Int, auto simp add: algebra_def)
+  fix a b
+  assume ab: "sets M \<subseteq> Pow (space M)"
+             "\<forall>a\<in>sets M. space M - a \<in> sets M" 
+             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
+             "a \<in> sets M" "b \<in> sets M"
+  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
+    by blast
+  also have "... \<in> sets M"
+    by (metis ab)
+  finally show "a \<union> b \<in> sets M" .
+qed
+
+lemma (in algebra) sigma_property_disjoint_lemma:
+  assumes sbC: "sets M \<subseteq> C"
+      and ccdi: "closed_cdi (|space = space M, sets = C|)"
+  shows "sigma_sets (space M) (sets M) \<subseteq> C"
+proof -
+  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
+    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int 
+            smallest_ccdi_sets_Int)
+    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) 
+    apply (blast intro: smallest_ccdi_sets.Disj) 
+    done
+  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
+    by auto 
+       (metis sigma_algebra.sigma_sets_subset algebra.simps(1) 
+          algebra.simps(2) subsetD) 
+  also have "...  \<subseteq> C"
+    proof
+      fix x
+      assume x: "x \<in> smallest_ccdi_sets M"
+      thus "x \<in> C"
+	proof (induct rule: smallest_ccdi_sets.induct)
+	  case (Basic x)
+	  thus ?case
+	    by (metis Basic subsetD sbC)
+	next
+	  case (Compl x)
+	  thus ?case
+	    by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
+ 	next
+	  case (Inc A)
+	  thus ?case
+	       by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 
+	next
+	  case (Disj A)
+	  thus ?case
+	       by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 
+	qed
+    qed
+  finally show ?thesis .
+qed
+
+lemma (in algebra) sigma_property_disjoint:
+  assumes sbC: "sets M \<subseteq> C"
+      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
+      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
+                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) 
+                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
+      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
+                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
+  shows "sigma_sets (space M) (sets M) \<subseteq> C"
+proof -
+  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 
+    proof (rule sigma_property_disjoint_lemma) 
+      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
+	by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
+    next
+      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
+	by (simp add: closed_cdi_def compl inc disj)
+           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
+	     IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
+    qed
+  thus ?thesis
+    by blast
+qed
+
+
+(* or just countably_additiveD [OF measure_space.ca] *)
+lemma (in measure_space) measure_countably_additive:
+    "range A \<subseteq> sets M
+     \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M
+     \<Longrightarrow> (measure M o A)  sums  measure M (\<Union>i. A i)"
+  by (insert ca) (simp add: countably_additive_def o_def) 
+
+lemma (in measure_space) additive:
+     "additive M (measure M)"
+proof (rule algebra.countably_additive_additive [OF _ _ ca]) 
+  show "algebra M"
+    by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms)
+  show "positive M (measure M)"
+    by (simp add: positive_def empty_measure positive) 
+qed
+ 
+lemma (in measure_space) measure_additive:
+     "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} 
+      \<Longrightarrow> measure M a + measure M b = measure M (a \<union> b)"
+  by (metis additiveD additive)
+
+lemma (in measure_space) measure_compl:
+  assumes s: "s \<in> sets M"
+  shows "measure M (space M - s) = measure M (space M) - measure M s"
+proof -
+  have "measure M (space M) = measure M (s \<union> (space M - s))" using s
+    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
+  also have "... = measure M s + measure M (space M - s)"
+    by (rule additiveD [OF additive]) (auto simp add: s) 
+  finally have "measure M (space M) = measure M s + measure M (space M - s)" .
+  thus ?thesis
+    by arith
+qed
+
+lemma disjoint_family_Suc:
+  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
+  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
+proof -
+  {
+    fix m
+    have "!!n. A n \<subseteq> A (m+n)" 
+    proof (induct m)
+      case 0 show ?case by simp
+    next
+      case (Suc m) thus ?case
+	by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
+    qed
+  }
+  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)
+      (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) 
+qed
+
+
+lemma (in measure_space) measure_countable_increasing:
+  assumes A: "range A \<subseteq> sets M"
+      and A0: "A 0 = {}"
+      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
+  shows "(measure M o A) ----> measure M (\<Union>i. A i)"
+proof -
+  {
+    fix n
+    have "(measure M \<circ> A) n =
+          setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
+      proof (induct n)
+	case 0 thus ?case by (auto simp add: A0 empty_measure)
+      next
+	case (Suc m) 
+	have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
+	  by (metis ASuc Un_Diff_cancel Un_absorb1)
+	hence "measure M (A (Suc m)) =
+               measure M (A m) + measure M (A (Suc m) - A m)" 
+	  by (subst measure_additive) 
+             (auto simp add: measure_additive range_subsetD [OF A]) 
+	with Suc show ?case
+	  by simp
+      qed
+  }
+  hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
+    by (blast intro: ext) 
+  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
+    proof (rule UN_finite2_eq [where k=1], simp) 
+      fix i
+      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
+	proof (induct i)
+	  case 0 thus ?case by (simp add: A0)
+	next
+	  case (Suc i) 
+	  thus ?case
+	    by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
+	qed
+    qed
+  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
+    by (metis A Diff range_subsetD)
+  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
+    by (blast intro: countable_UN range_subsetD [OF A])  
+  have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
+    by (rule measure_countably_additive) 
+       (auto simp add: disjoint_family_Suc ASuc A1 A2)
+  also have "... =  measure M (\<Union>i. A i)"
+    by (simp add: Aeq) 
+  finally have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A i)" .
+  thus ?thesis
+    by (auto simp add: sums_iff Meq dest: summable_sumr_LIMSEQ_suminf) 
+qed
+
+lemma (in measure_space) monotone_convergence:
+  assumes A: "range A \<subseteq> sets M"
+      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
+  shows "(measure M \<circ> A) ----> measure M (\<Union>i. A i)"
+proof -
+  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)" 
+    by (auto simp add: split: nat.splits) 
+  have meq: "measure M \<circ> A = (\<lambda>n. (measure M \<circ> nat_case {} A) (Suc n))"
+    by (rule ext) simp
+  have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)" 
+    by (rule measure_countable_increasing) 
+       (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) 
+  also have "... = measure M (\<Union>i. A i)" 
+    by (simp add: ueq) 
+  finally have "(measure M \<circ> nat_case {} A) ---->  measure M (\<Union>i. A i)" .
+  thus ?thesis using meq
+    by (metis LIMSEQ_Suc)
+qed
+
+lemma measurable_sigma_preimages:
+  assumes a: "sigma_algebra a" and b: "sigma_algebra b"
+      and f: "f \<in> space a -> space b"
+      and ba: "!!y. y \<in> sets b ==> f -` y \<in> sets a"
+  shows "sigma_algebra (|space = space a, sets = (vimage f) ` (sets b) |)"
+proof (simp add: sigma_algebra_iff2, intro conjI) 
+  show "op -` f ` sets b \<subseteq> Pow (space a)"
+    by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI) 
+next
+  show "{} \<in> op -` f ` sets b"
+    by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty)
+next
+  { fix y
+    assume y: "y \<in> sets b"
+    with a b f
+    have "space a - f -` y = f -` (space b - y)"
+      by (auto simp add: sigma_algebra_iff2) (blast intro: ba) 
+    hence "space a - (f -` y) \<in> (vimage f) ` sets b"
+      by auto
+         (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
+                sigma_sets.Compl) 
+  } 
+  thus "\<forall>s\<in>sets b. space a - f -` s \<in> (vimage f) ` sets b"
+    by blast
+next
+  {
+    fix A:: "nat \<Rightarrow> 'a set"
+    assume A: "range A \<subseteq> (vimage f) ` (sets b)"
+    have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
+      proof -
+	def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
+	{ 
+	  fix i
+	  have "A i \<in> (vimage f) ` (sets b)" using A
+	    by blast
+	  hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
+	    by blast
+	  hence "B i \<in> sets b \<and> f -` B i = A i" 
+	    by (simp add: B_def) (erule someI_ex)
+	} note B = this
+	show ?thesis
+	  proof
+	    show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
+	      by (simp add: vimage_UN B) 
+	   show "(\<Union>i. B i) \<in> sets b" using B
+	     by (auto intro: sigma_algebra.countable_UN [OF b]) 
+	  qed
+      qed
+  }
+  thus "\<forall>A::nat \<Rightarrow> 'a set.
+           range A \<subseteq> (vimage f) ` sets b \<longrightarrow> (\<Union>i. A i) \<in> (vimage f) ` sets b"
+    by blast
+qed
+
+lemma (in sigma_algebra) measurable_sigma:
+  assumes B: "B \<subseteq> Pow X" 
+      and f: "f \<in> space M -> X"
+      and ba: "!!y. y \<in> B ==> (f -` y) \<inter> space M \<in> sets M"
+  shows "f \<in> measurable M (sigma X B)"
+proof -
+  have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
+    proof clarify
+      fix x
+      assume "x \<in> sigma_sets X B"
+      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
+	proof induct
+	  case (Basic a)
+	  thus ?case
+	    by (auto simp add: ba) (metis B subsetD PowD) 
+        next
+	  case Empty
+	  thus ?case
+	    by auto
+        next
+	  case (Compl a)
+	  have [simp]: "f -` X \<inter> space M = space M"
+	    by (auto simp add: funcset_mem [OF f]) 
+	  thus ?case
+	    by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+	next
+	  case (Union a)
+	  thus ?case
+	    by (simp add: vimage_UN, simp only: UN_extend_simps(4))
+	       (blast intro: countable_UN)
+	qed
+    qed
+  thus ?thesis
+    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 
+       (auto simp add: sigma_def) 
+qed
+
+lemma measurable_subset:
+     "measurable a b \<subseteq> measurable a (sigma (space b) (sets b))"
+  apply clarify
+  apply (rule sigma_algebra.measurable_sigma) 
+  apply (auto simp add: measurable_def)
+  apply (metis algebra.sets_into_space subsetD sigma_algebra_iff) 
+  done
+
+lemma measurable_eqI: 
+     "space m1 = space m1' \<Longrightarrow> space m2 = space m2'
+      \<Longrightarrow> sets m1 = sets m1' \<Longrightarrow> sets m2 = sets m2'
+      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
+  by (simp add: measurable_def sigma_algebra_iff2) 
+
+lemma measure_preserving_lift:
+  fixes f :: "'a1 \<Rightarrow> 'a2" 
+    and m1 :: "('a1, 'b1) measure_space_scheme"
+    and m2 :: "('a2, 'b2) measure_space_scheme"
+  assumes m1: "measure_space m1" and m2: "measure_space m2" 
+  defines "m x \<equiv> (|space = space m2, sets = x, measure = measure m2, ... = more m2|)"
+  assumes setsm2: "sets m2 = sigma_sets (space m2) a"
+      and fmp: "f \<in> measure_preserving m1 (m a)"
+  shows "f \<in> measure_preserving m1 m2"
+proof -
+  have [simp]: "!!x. space (m x) = space m2 & sets (m x) = x & measure (m x) = measure m2"
+    by (simp add: m_def) 
+  have sa1: "sigma_algebra m1" using m1 
+    by (simp add: measure_space_def) 
+  show ?thesis using fmp
+    proof (clarsimp simp add: measure_preserving_def m1 m2) 
+      assume fm: "f \<in> measurable m1 (m a)" 
+	 and mam: "measure_space (m a)"
+	 and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
+      have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
+	by (rule subsetD [OF measurable_subset fm]) 
+      also have "... = measurable m1 m2"
+	by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) 
+      finally have f12: "f \<in> measurable m1 m2" .
+      hence ffn: "f \<in> space m1 \<rightarrow> space m2"
+	by (simp add: measurable_def) 
+      have "space m1 \<subseteq> f -` (space m2)"
+	by auto (metis PiE ffn)
+      hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
+	by blast
+      {
+	fix y
+	assume y: "y \<in> sets m2" 
+	have ama: "algebra (m a)"  using mam
+	  by (simp add: measure_space_def sigma_algebra_iff) 
+	have spa: "space m2 \<in> a" using algebra.top [OF ama]
+	  by (simp add: m_def) 
+	have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
+	  by (simp add: m_def) 
+	also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
+	  proof (rule algebra.sigma_property_disjoint, auto simp add: ama) 
+	    fix x
+	    assume x: "x \<in> a"
+	    thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
+	      by (simp add: meq)
+	  next
+	    fix s
+	    assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
+	       and s: "s \<in> sigma_sets (space m2) a"
+	    hence s2: "s \<in> sets m2"
+	      by (simp add: setsm2) 
+	    thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
+                  measure m2 (space m2 - s)" using f12
+	      by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
+		    measure_space.measure_compl measurable_def)  
+	         (metis fveq meq spa) 
+	  next
+	    fix A
+	      assume A0: "A 0 = {}"
+	 	 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
+		 and rA1: "range A \<subseteq> 
+		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+		 and "range A \<subseteq> sigma_sets (space m2) a"
+	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+	      have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+		using rA1 by blast
+	      have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))" 
+		by (simp add: o_def eq1) 
+	      also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+		proof (rule measure_space.measure_countable_increasing [OF m1])
+		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+		    using f12 rA2 by (auto simp add: measurable_def)
+		  show "f -` A 0 \<inter> space m1 = {}" using A0
+		    by blast
+		  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
+		    using ASuc by auto
+		qed
+	      also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+		by (simp add: vimage_UN)
+	      finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
+	      moreover
+	      have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
+		by (rule measure_space.measure_countable_increasing 
+		          [OF m2 rA2, OF A0 ASuc])
+	      ultimately 
+	      show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+                    measure m2 (\<Union>i. A i)"
+		by (rule LIMSEQ_unique) 
+	  next
+	    fix A :: "nat => 'a2 set"
+	      assume dA: "disjoint_family A"
+		 and rA1: "range A \<subseteq> 
+		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+		 and "range A \<subseteq> sigma_sets (space m2) a"
+	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+	      hence Um2: "(\<Union>i. A i) \<in> sets m2"
+		by (metis range_subsetD setsm2 sigma_sets.Union)
+	      have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+		using rA1 by blast
+	      hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
+		by (simp add: o_def) 
+	      also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" 
+		proof (rule measure_space.measure_countably_additive [OF m1] )
+		  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) 
+		  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
+			by (auto simp add: measurable_def) 
+		    qed
+ 		qed
+	      finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
+	      with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] 
+	      have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
+		by (metis sums_unique) 
+
+	      moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+		by (simp add: vimage_UN)
+	      ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+                    measure m2 (\<Union>i. A i)" 
+		by metis
+	  qed
+	finally have "sigma_sets (space m2) a 
+              \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
+	hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
+	  by (force simp add: setsm2) 
+      }
+      thus "f \<in> measurable m1 m2 \<and>
+       (\<forall>y\<in>sets m2.
+           measure m1 (f -` y \<inter> space m1) = measure m2 y)"
+	by (blast intro: f12) 
+    qed
+qed
+
+lemma measurable_ident:
+     "sigma_algebra M ==> id \<in> measurable M M"
+  apply (simp add: measurable_def)
+  apply (auto simp add: sigma_algebra_def algebra.Int algebra.top)
+  done
+
+lemma measurable_comp:
+  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
+  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
+  apply (auto simp add: measurable_def vimage_compose) 
+  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
+  apply force+
+  done
+
+ lemma measurable_strong:
+  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
+  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
+      and c: "sigma_algebra c"
+      and t: "f ` (space a) \<subseteq> t"
+      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
+  shows "(g o f) \<in> measurable a c"
+proof -
+  have a: "sigma_algebra a" and b: "sigma_algebra b"
+   and fab: "f \<in> (space a -> space b)"
+   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
+     by (auto simp add: measurable_def)
+  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
+    by force
+  show ?thesis
+    apply (auto simp add: measurable_def vimage_compose a c) 
+    apply (metis funcset_mem fab g) 
+    apply (subst eq, metis ba cb) 
+    done
+qed
+ 
+lemma measurable_mono1:
+     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
+      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
+  by (auto simp add: measurable_def) 
+
+lemma measurable_up_sigma:
+   "measurable a b \<subseteq> measurable (sigma (space a) (sets a)) b"
+  apply (auto simp add: measurable_def) 
+  apply (metis sigma_algebra_iff2 sigma_algebra_sigma)
+  apply (metis algebra.simps(2) sigma_algebra.sigma_sets_eq sigma_def) 
+  done
+
+lemma measure_preserving_up:
+   "f \<in> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 \<Longrightarrow>
+    measure_space m1 \<Longrightarrow> sigma_algebra m1 \<Longrightarrow> a \<subseteq> sets m1 
+    \<Longrightarrow> f \<in> measure_preserving m1 m2"
+  by (auto simp add: measure_preserving_def measurable_def) 
+
+lemma measure_preserving_up_sigma:
+   "measure_space m1 \<Longrightarrow> (sets m1 = sets (sigma (space m1) a))
+    \<Longrightarrow> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 
+        \<subseteq> measure_preserving m1 m2"
+  apply (rule subsetI) 
+  apply (rule measure_preserving_up) 
+  apply (simp_all add: measure_space_def sigma_def) 
+  apply (metis sigma_algebra.sigma_sets_eq subsetI sigma_sets.Basic) 
+  done
+
+lemma (in sigma_algebra) measurable_prod_sigma:
+  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
+  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2)) 
+                          (prod_sets (sets a1) (sets a2)))"
+proof -
+  from 1 have sa1: "sigma_algebra a1" and fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
+     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
+    by (auto simp add: measurable_def) 
+  from 2 have sa2: "sigma_algebra a2" and fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
+     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
+    by (auto simp add: measurable_def) 
+  show ?thesis
+    proof (rule measurable_sigma) 
+      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
+        by (force simp add: prod_sets_def sigma_algebra_iff algebra_def) 
+    next
+      show "f \<in> space M \<rightarrow> space a1 \<times> space a2" 
+        by (rule prod_final [OF fn1 fn2])
+    next
+      fix z
+      assume z: "z \<in> prod_sets (sets a1) (sets a2)" 
+      thus "f -` z \<inter> space M \<in> sets M"
+        proof (auto simp add: prod_sets_def vimage_Times) 
+          fix x y
+          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
+          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M = 
+                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
+            by blast
+          also have "...  \<in> sets M" using x y q1 q2
+            by blast
+          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
+        qed
+    qed
+qed
+
+
+lemma (in measure_space) measurable_range_reduce:
+   "f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> \<Longrightarrow>
+    s \<noteq> {} 
+    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
+  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
+
+lemma (in measure_space) measurable_Pow_to_Pow:
+   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
+  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
+
+lemma (in measure_space) measurable_Pow_to_Pow_image:
+   "sets M = Pow (space M)
+    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
+  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
+
+lemma (in measure_space) measure_real_sum_image:
+  assumes s: "s \<in> sets M"
+      and ssets: "\<And>x. x \<in> s ==> {x} \<in> sets M"
+      and fin: "finite s"
+  shows "measure M s = (\<Sum>x\<in>s. measure M {x})"
+proof -
+  {
+    fix u
+    assume u: "u \<subseteq> s & u \<in> sets M"
+    hence "finite u"
+      by (metis fin finite_subset) 
+    hence "measure M u = (\<Sum>x\<in>u. measure M {x})" using u
+      proof (induct u)
+        case empty
+        thus ?case by simp
+      next
+        case (insert x t)
+        hence x: "x \<in> s" and t: "t \<subseteq> s" 
+          by (simp_all add: insert_subset) 
+        hence ts: "t \<in> sets M"  using insert
+          by (metis Diff_insert_absorb Diff ssets)
+        have "measure M (insert x t) = measure M ({x} \<union> t)"
+          by simp
+        also have "... = measure M {x} + measure M t" 
+          by (simp add: measure_additive insert insert_disjoint ssets x ts 
+                  del: Un_insert_left)
+        also have "... = (\<Sum>x\<in>insert x t. measure M {x})" 
+          by (simp add: x t ts insert) 
+        finally show ?case .
+      qed
+    }
+  thus ?thesis
+    by (metis subset_refl s)
+qed
+  
+lemma (in sigma_algebra) sigma_algebra_extend:
+     "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
+proof -
+  have 1: "sigma_algebra M \<Longrightarrow> ?thesis"
+    by (simp add: sigma_algebra_def algebra_def sigma_algebra_axioms_def) 
+  show ?thesis
+    by (rule 1) intro_locales
+qed
+
+
+lemma (in sigma_algebra) finite_additivity_sufficient:
+  assumes fin: "finite (space M)"
+      and posf: "positive M f" and addf: "additive M f" 
+  defines "Mf \<equiv> \<lparr>space = space M, sets = sets M, measure = f\<rparr>"
+  shows "measure_space Mf" 
+proof -
+  have [simp]: "f {} = 0" using posf
+    by (simp add: positive_def) 
+  have "countably_additive Mf f"
+    proof (auto simp add: countably_additive_def positive_def) 
+      fix A :: "nat \<Rightarrow> 'a set"
+      assume A: "range A \<subseteq> sets Mf"
+         and disj: "disjoint_family A"
+         and UnA: "(\<Union>i. A i) \<in> sets Mf"
+      def I \<equiv> "{i. A i \<noteq> {}}"
+      have "Union (A ` I) \<subseteq> space M" using A
+        by (auto simp add: Mf_def) (metis range_subsetD subsetD sets_into_space) 
+      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) 
+      ultimately have finI: "finite I"
+        by (metis finite_imageD)
+      hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
+        proof (cases "I = {}")
+          case True thus ?thesis by (simp add: I_def) 
+        next
+          case False
+          hence "\<forall>i\<in>I. i < Suc(Max I)"
+            by (simp add: Max_less_iff [symmetric] finI) 
+          hence "\<forall>m \<ge> Suc(Max I). A m = {}"
+            by (simp add: I_def) (metis less_le_not_le) 
+          thus ?thesis
+            by blast
+        qed
+      then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
+      hence "\<forall>m\<ge>N. (f o A) m = 0"
+        by simp 
+      hence "(\<lambda>n. f (A n)) sums setsum (f o A) {0..<N}" 
+        by (simp add: series_zero o_def) 
+      also have "... = f (\<Union>i<N. A i)"
+        proof (induct N)
+          case 0 thus ?case by simp
+        next
+          case (Suc n) 
+          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
+              show "A n \<in> sets M" using A 
+                by (force simp add: Mf_def) 
+              show "(\<Union>i<n. A i) \<in> sets M"
+                proof (induct n)
+                  case 0 thus ?case by simp
+                next
+                  case (Suc n) thus ?case using A
+                    by (simp add: lessThan_Suc Mf_def Un range_subsetD) 
+                qed
+            qed
+          thus ?case using Suc
+            by (simp add: lessThan_Suc) 
+        qed
+      also have "... = f (\<Union>i. A i)" 
+        proof -
+          have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
+            by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
+          thus ?thesis by simp
+        qed
+      finally show "(\<lambda>n. f (A n)) sums f (\<Union>i. A i)" .
+    qed
+  thus ?thesis using posf 
+    by (simp add: Mf_def measure_space_def measure_space_axioms_def sigma_algebra_extend positive_def) 
+qed
+
+lemma finite_additivity_sufficient:
+     "sigma_algebra M 
+      \<Longrightarrow> finite (space M) 
+      \<Longrightarrow> positive M (measure M) \<Longrightarrow> additive M (measure M) 
+      \<Longrightarrow> measure_space M"
+  by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
+
+end
+
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Probability/Probability.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Probability.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,5 @@
+theory Probability imports
+	Measure
+begin
+
+end
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Probability/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/ROOT.ML	Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,6 @@
+(*
+  no_document use_thy "ThisTheory";
+  use_thy "ThatTheory";
+*)
+
+use_thy "Probability";
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Probability/SeriesPlus.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/SeriesPlus.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,127 @@
+theory SeriesPlus
+  imports Complex_Main Nat_Int_Bij 
+
+begin
+
+text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
+
+lemma choice2: "(!!x. \<exists>y z. Q x y z) ==> \<exists>f g. \<forall>x. Q x (f x) (g x)"
+  by metis
+
+lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
+  by blast
+
+
+lemma suminf_2dimen:
+  fixes f:: "nat * nat \<Rightarrow> real"
+  assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
+      and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
+      and sumg: "summable g"
+  shows "(f o nat_to_nat2) sums suminf g"
+proof (simp add: sums_def)
+  {
+    fix x
+    have "0 \<le> f x"
+      by (cases x) (simp add: f_nneg) 
+  } note [iff]  = this
+  have g_nneg: "!!m. 0 \<le> g m"
+    proof -
+      fix m
+      have "0 \<le> suminf (\<lambda>n. f (m,n))"
+	by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
+      thus "0 \<le> g m" using fsums [of m] 
+	by (auto simp add: sums_iff) 
+    qed
+  show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
+  proof (rule increasing_LIMSEQ, simp add: f_nneg)
+    fix n
+    def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
+    def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
+    have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})" 
+      by (force simp add: i_def j_def 
+                intro: finite_imageI Max_ge finite_Domain finite_Range)  
+    have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})" 
+      using setsum_reindex [of nat_to_nat2 "{0..<n}" f] 
+      by (simp add: o_def)
+         (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj) 
+    also have "... \<le> setsum f ({0..i} \<times> {0..j})"
+      by (rule setsum_mono2) (auto simp add: ij) 
+    also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
+      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
+	        setsum_cartesian_product split_eta) 
+    also have "... \<le> setsum g {0..<Suc i}" 
+      proof (rule setsum_mono, simp add: less_Suc_eq_le) 
+	fix m
+	assume m: "m \<le> i"
+	thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
+	  by (auto simp add: sums_iff) 
+	   (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) 
+      qed
+    finally have  "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
+    also have "... \<le> suminf g" 
+      by (rule series_pos_le [OF sumg]) (simp add: g_nneg) 
+    finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
+  next
+    fix e :: real
+    assume e: "0 < e"
+    with summable_sums [OF sumg]
+    obtain N where "\<bar>setsum g {0..<N} - suminf g\<bar> < e/2" and nz: "N>0"
+      by (simp add: sums_def LIMSEQ_iff_nz dist_real_def)
+         (metis e half_gt_zero le_refl that)
+    hence gless: "suminf g < setsum g {0..<N} + e/2" using series_pos_le [OF sumg]
+      by (simp add: g_nneg)
+    { fix m
+      assume m: "m<N"
+      hence enneg: "0 < e / (2 * real N)" using e
+	by (simp add: zero_less_divide_iff) 
+      hence  "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
+	using fsums [of m] m
+        by (force simp add: sums_def LIMSEQ_def dist_real_def)
+      hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)" 
+	using fsums [of m]
+	by (auto simp add: sums_iff) 
+           (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq') 
+    }
+    hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
+      by (force intro: choice) 
+    then obtain jj where jj:
+          "!!m. m<N \<Longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
+      by auto
+    def IJ \<equiv> "SIGMA i : {0..<N}. {0..<jj i}"
+    have "setsum g {0..<N} <
+             (\<Sum>m = 0..<N. (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N))"
+      by (auto simp add: nz jj intro: setsum_strict_mono) 
+    also have "... = (\<Sum>m = 0..<N. \<Sum>n = 0..<jj m. f (m, n)) + e/2" using nz
+      by (auto simp add: setsum_addf real_of_nat_def) 
+    also have "... = setsum f IJ + e/2" 
+      by (simp add: IJ_def setsum_Sigma) 
+    finally have "setsum g {0..<N} < setsum f IJ + e/2" .
+    hence glessf: "suminf g < setsum f IJ + e" using gless 
+      by auto
+    have finite_IJ: "finite IJ"
+      by (simp add: IJ_def) 
+    def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
+    have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
+      proof (auto simp add: NIJ_def)
+	fix i j
+	assume ij:"(i,j) \<in> IJ"
+	hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
+	  by (metis nat_to_nat2_surj surj_f_inv_f) 
+	thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+	  by (rule image_eqI) 
+	     (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
+                    nat_to_nat2_surj surj_f_inv_f) 
+      qed
+    have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
+      by (rule setsum_mono2) (auto simp add: IJsb) 
+    also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
+      by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV]) 
+    also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
+      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
+    finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
+    thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
+      by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
+  qed
+qed
+
+end
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Probability/Sigma_Algebra.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -0,0 +1,229 @@
+(*  Title:      Sigma_Algebra.thy
+    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
+    Plus material from the Hurd/Coble measure theory development, 
+    translated by Lawrence Paulson.
+*)
+
+header {* Sigma Algebras *}
+
+theory Sigma_Algebra imports Complex_Main begin
+
+text {* Sigma algebras are an elementary concept in measure
+  theory. To measure --- that is to integrate --- functions, we first have
+  to measure sets. Unfortunately, when dealing with a large universe,
+  it is often not possible to consistently assign a measure to every
+  subset. Therefore it is necessary to define the set of measurable
+  subsets of the universe. A sigma algebra is such a set that has
+  three very natural and desirable properties. *}
+
+subsection {* Algebras *}
+
+record 'a algebra = 
+  space :: "'a set" 
+  sets :: "'a set set"
+
+locale algebra =
+  fixes M
+  assumes space_closed: "sets M \<subseteq> Pow (space M)"
+     and  empty_sets [iff]: "{} \<in> sets M"
+     and  compl_sets [intro]: "!!a. a \<in> sets M \<Longrightarrow> space M - a \<in> sets M"
+     and  Un [intro]: "!!a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M"
+
+lemma (in algebra) top [iff]: "space M \<in> sets M"
+  by (metis Diff_empty compl_sets empty_sets)
+
+lemma (in algebra) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M"
+  by (metis PowD contra_subsetD space_closed)
+
+lemma (in algebra) Int [intro]: 
+  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M"
+proof -
+  have "((space M - a) \<union> (space M - b)) \<in> sets M" 
+    by (metis a b compl_sets Un)
+  moreover
+  have "a \<inter> b = space M - ((space M - a) \<union> (space M - b))" 
+    using space_closed a b
+    by blast
+  ultimately show ?thesis
+    by (metis compl_sets)
+qed
+
+lemma (in algebra) Diff [intro]: 
+  assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a - b \<in> sets M"
+proof -
+  have "(a \<inter> (space M - b)) \<in> sets M"
+    by (metis a b compl_sets Int)
+  moreover
+  have "a - b = (a \<inter> (space M - b))"
+    by (metis Int_Diff Int_absorb1 Int_commute a sets_into_space)
+  ultimately show ?thesis
+    by metis
+qed
+
+lemma (in algebra) finite_union [intro]: 
+  "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
+  by (induct set: finite) (auto simp add: Un) 
+
+
+subsection {* Sigma Algebras *}
+
+locale sigma_algebra = algebra +
+  assumes countable_UN [intro]:
+         "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
+
+lemma (in sigma_algebra) countable_INT:
+  assumes a: "range a \<subseteq> sets M"
+  shows "(\<Inter>i::nat. a i) \<in> sets M"
+proof -
+  have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
+    by (blast intro: countable_UN compl_sets a) 
+  moreover
+  have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a 
+    by blast
+  ultimately show ?thesis by metis
+qed
+
+
+lemma algebra_Pow:
+     "algebra (| space = sp, sets = Pow sp |)"
+  by (auto simp add: algebra_def) 
+
+lemma sigma_algebra_Pow:
+     "sigma_algebra (| space = sp, sets = Pow sp |)"
+  by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow) 
+
+subsection {* Binary Unions *}
+
+definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
+  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
+
+lemma range_binary_eq: "range(binary a b) = {a,b}" 
+  by (auto simp add: binary_def)  
+
+lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" 
+  by (simp add: UNION_eq_Union_image range_binary_eq) 
+
+lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" 
+  by (simp add: INTER_eq_Inter_image range_binary_eq) 
+
+lemma sigma_algebra_iff: 
+     "sigma_algebra M \<longleftrightarrow> 
+      algebra M & (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+  by (simp add: sigma_algebra_def sigma_algebra_axioms_def) 
+
+lemma sigma_algebra_iff2:
+     "sigma_algebra M \<longleftrightarrow>
+       sets M \<subseteq> Pow (space M) &
+       {} \<in> sets M & (\<forall>s \<in> sets M. space M - s \<in> sets M) &
+       (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
+  by (force simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
+         algebra_def Un_range_binary) 
+
+
+subsection {* Initial Sigma Algebra *}
+
+text {*Sigma algebras can naturally be created as the closure of any set of
+  sets with regard to the properties just postulated.  *}
+
+inductive_set
+  sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+  for sp :: "'a set" and A :: "'a set set"
+  where
+    Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
+  | Empty: "{} \<in> sigma_sets sp A"
+  | Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp - a \<in> sigma_sets sp A"
+  | Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A"
+
+
+definition
+  sigma  where
+  "sigma sp A = (| space = sp, sets = sigma_sets sp A |)"
+
+
+lemma space_sigma [simp]: "space (sigma X B) = X"
+  by (simp add: sigma_def) 
+
+lemma sigma_sets_top: "sp \<in> sigma_sets sp A"
+  by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty)
+
+lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp"
+  by (erule sigma_sets.induct, auto) 
+
+lemma sigma_sets_Un: 
+  "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
+apply (simp add: Un_range_binary range_binary_eq) 
+apply (metis Union COMBK_def binary_def fun_upd_apply) 
+done
+
+lemma sigma_sets_Inter:
+  assumes Asb: "A \<subseteq> Pow sp"
+  shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A"
+proof -
+  assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A"
+  hence "\<And>i::nat. sp-(a i) \<in> sigma_sets sp A" 
+    by (rule sigma_sets.Compl)
+  hence "(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" 
+    by (rule sigma_sets.Union)
+  hence "sp-(\<Union>i. sp-(a i)) \<in> sigma_sets sp A" 
+    by (rule sigma_sets.Compl)
+  also have "sp-(\<Union>i. sp-(a i)) = sp Int (\<Inter>i. a i)" 
+    by auto
+  also have "... = (\<Inter>i. a i)" using ai
+    by (blast dest: sigma_sets_into_sp [OF Asb]) 
+  finally show ?thesis . 
+qed
+
+lemma sigma_sets_INTER:
+  assumes Asb: "A \<subseteq> Pow sp" 
+      and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}"
+  shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A"
+proof -
+  from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A"
+    by (simp add: sigma_sets.intros sigma_sets_top)
+  hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A"
+    by (rule sigma_sets_Inter [OF Asb])
+  also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)"
+    by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+
+  finally show ?thesis .
+qed
+
+lemma (in sigma_algebra) sigma_sets_subset:
+  assumes a: "a \<subseteq> sets M" 
+  shows "sigma_sets (space M) a \<subseteq> sets M"
+proof
+  fix x
+  assume "x \<in> sigma_sets (space M) a"
+  from this show "x \<in> sets M"
+    by (induct rule: sigma_sets.induct, auto) (metis a subsetD) 
+qed
+
+lemma (in sigma_algebra) sigma_sets_eq:
+     "sigma_sets (space M) (sets M) = sets M"
+proof
+  show "sets M \<subseteq> sigma_sets (space M) (sets M)"
+    by (metis Set.subsetI sigma_sets.Basic space_closed)
+  next
+  show "sigma_sets (space M) (sets M) \<subseteq> sets M"
+    by (metis sigma_sets_subset subset_refl)
+qed
+
+lemma sigma_algebra_sigma_sets:
+     "a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M"
+  apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
+      algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) 
+  apply (blast dest: sigma_sets_into_sp)
+  apply (blast intro: sigma_sets.intros) 
+  done
+
+lemma sigma_algebra_sigma:
+     "a \<subseteq> Pow X \<Longrightarrow> sigma_algebra (sigma X a)"
+  apply (rule sigma_algebra_sigma_sets) 
+  apply (auto simp add: sigma_def) 
+  done
+
+lemma (in sigma_algebra) sigma_subset:
+     "a \<subseteq> sets M ==> sets (sigma (space M) a) \<subseteq> (sets M)"
+  by (simp add: sigma_def sigma_sets_subset)
+
+end
+
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Product_Type.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -927,6 +927,9 @@
    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
 by blast
 
+lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
+  by (auto, rule_tac p = "f x" in PairE, auto)
+
 subsubsection {* Code generator setup *}
 
 instance * :: (eq, eq) eq ..
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/SEQ.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -205,6 +205,9 @@
   shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
 unfolding LIMSEQ_def dist_norm ..
 
+lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
+  by (auto simp add: LIMSEQ_def) (metis Suc_leD zero_less_Suc)  
+
 lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
 by (simp only: LIMSEQ_iff Zseq_def)
 
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/Series.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -10,7 +10,7 @@
 header{*Finite Summation and Infinite Series*}
 
 theory Series
-imports SEQ
+imports SEQ Deriv
 begin
 
 definition
@@ -285,6 +285,26 @@
 text{*A summable series of positive terms has limit that is at least as
 great as any partial sum.*}
 
+lemma pos_summable:
+  fixes f:: "nat \<Rightarrow> real"
+  assumes pos: "!!n. 0 \<le> f n" and le: "!!n. setsum f {0..<n} \<le> x"
+  shows "summable f"
+proof -
+  have "convergent (\<lambda>n. setsum f {0..<n})" 
+    proof (rule Bseq_mono_convergent)
+      show "Bseq (\<lambda>n. setsum f {0..<n})"
+	by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
+           (auto simp add: le pos)  
+    next 
+      show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
+	by (auto intro: setsum_mono2 pos) 
+    qed
+  then obtain L where "(%n. setsum f {0..<n}) ----> L"
+    by (blast dest: convergentD)
+  thus ?thesis
+    by (force simp add: summable_def sums_def) 
+qed
+
 lemma series_pos_le:
   fixes f :: "nat \<Rightarrow> real"
   shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 \<le> f m\<rbrakk> \<Longrightarrow> setsum f {0..<n} \<le> suminf f"
@@ -361,6 +381,19 @@
   shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
 by (rule geometric_sums [THEN sums_summable])
 
+lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,ordered_field})"
+  by arith 
+
+lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
+proof -
+  have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
+    by auto
+  have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
+    by simp
+  thus ?thesis using divide.sums [OF 2, of 2]
+    by simp
+qed
+
 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
 
 lemma summable_convergent_sumr_iff:
diff -r 320a1d67b9ae -r 7be66dee1a5a src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Tue Oct 27 14:46:03 2009 +0000
+++ b/src/HOL/SupInf.thy	Wed Oct 28 11:42:31 2009 +0000
@@ -361,11 +361,6 @@
   shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
 by auto (metis Inf_insert_nonempty z) 
 
-text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
-lemma Inf_binary:
-  "Inf{a, b::real} = min a b"
-  by (subst Inf_insert_nonempty, auto)
-
 lemma Inf_greater:
   fixes z :: real
   shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
@@ -437,7 +432,7 @@
     by (simp add: Inf_real_def)
 qed
 
-subsection{*Relate max and min to sup and inf.*}
+subsection{*Relate max and min to Sup and Inf.*}
 
 lemma real_max_Sup:
   fixes x :: real