# HG changeset patch
# User paulson
# Date 1256730186 0
# Node ID 73a0c804840fbe5ebbbf12a35d4cc7e5fc005636
# Parent  02de0317f66fb7509c0e48b5c99f4175a3ed9df6# Parent  7be66dee1a5ae6c9dfa8058060d6e02b13298498
merged

diff -r 02de0317f66f -r 73a0c804840f NEWS
--- a/NEWS	Wed Oct 28 00:24:38 2009 +0100
+++ b/NEWS	Wed Oct 28 11:43:06 2009 +0000
@@ -65,6 +65,10 @@
 of finite and infinite sets. It is shown that they form a complete
 lattice.
 
+* 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 02de0317f66f -r 73a0c804840f src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Complex_Main.thy	Wed Oct 28 11:43:06 2009 +0000
@@ -4,6 +4,7 @@
 imports
   Main
   Real
+  SupInf
   Complex
   Log
   Ln
diff -r 02de0317f66f -r 73a0c804840f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/IsaMakefile	Wed Oct 28 11:43:06 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 \
@@ -345,6 +346,7 @@
   RealVector.thy \
   SEQ.thy \
   Series.thy \
+  SupInf.thy \
   Taylor.thy \
   Transcendental.thy \
   Tools/float_syntax.ML \
@@ -1067,6 +1069,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 02de0317f66f -r 73a0c804840f src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Library/FuncSet.thy	Wed Oct 28 11:43:06 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 02de0317f66f -r 73a0c804840f src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Oct 28 11:43:06 2009 +0000
@@ -1133,7 +1133,7 @@
     hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
       apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
       apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
-  thus ?thesis unfolding convex_def cone_def by blast
+  thus ?thesis unfolding convex_def cone_def by auto
 qed
 
 lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
@@ -1742,17 +1742,16 @@
     using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
     using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast)
   hence ab:"\<forall>x\<in>s. \<forall>y\<in>t. b + inner a y < inner a x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
-  def k \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
+  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
   show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI)
     apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
     from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
       apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
-    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
+    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
     fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
   next
     fix x assume "x\<in>s" 
-    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
-      unfolding setle_def
+    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
       using ab[THEN bspec[where x=x]] by auto
     thus "k + b / 2 < inner a x" using `0 < b` by auto
   qed
@@ -1794,11 +1793,20 @@
   assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
   shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
 proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
-  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"  using assms(3-5) by auto 
-  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
-  thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
-    apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def
-    prefer 4 using assms(3-5) by blast+ qed
+  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" 
+    using assms(3-5) by auto 
+  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
+    by (force simp add: inner_diff)
+  thus ?thesis
+    apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
+    apply auto
+    apply (rule Sup[THEN isLubD2]) 
+    prefer 4
+    apply (rule Sup_least) 
+     using assms(3-5) apply (auto simp add: setle_def)
+    apply (metis COMBC_def Collect_def Collect_mem_eq) 
+    done
+qed
 
 subsection {* More convexity generalities. *}
 
@@ -2571,12 +2579,17 @@
     thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm 
       by(auto simp add: vector_component_simps) qed
   hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
-    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
-  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed
-
-subsection {* Line segments, starlike sets etc.                                         *)
-(* Use the same overloading tricks as for intervals, so that                 *)
-(* segment[a,b] is closed and segment(a,b) is open relative to affine hull. *}
+    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
+    apply force
+    done
+  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball]
+    using `d>0` by auto 
+qed
+
+subsection {* Line segments, Starlike Sets, etc.*}
+
+(* Use the same overloading tricks as for intervals, so that 
+   segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
 
 definition
   midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
diff -r 02de0317f66f -r 73a0c804840f src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Oct 28 11:43:06 2009 +0000
@@ -2297,242 +2297,9 @@
   ultimately show ?thesis by metis
 qed
 
-(* Supremum and infimum of real sets *)
-
-
-definition rsup:: "real set \<Rightarrow> real" where
-  "rsup S = (SOME a. isLub UNIV S a)"
-
-lemma rsup_alt: "rsup S = (SOME a. (\<forall>x \<in> S. x \<le> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<le> b) \<longrightarrow> a \<le> b))"  by (auto simp  add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def)
-
-lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>b. S *<= b"
-  shows "isLub UNIV S (rsup S)"
-using Se b
-unfolding rsup_def
-apply clarify
-apply (rule someI_ex)
-apply (rule reals_complete)
-by (auto simp add: isUb_def setle_def)
-
-lemma rsup_le: assumes Se: "S \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> b"
-proof-
-  from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def)
-  from rsup[OF Se] Sb have "isLub UNIV S (rsup S)"  by blast
-  then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def)
-qed
-
-lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "rsup S = Max S"
-using fS Se
-proof-
-  let ?m = "Max S"
-  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
-  with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def)
-  from Max_in[OF fS Se] lub have mrS: "?m \<le> rsup S"
-    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
-  moreover
-  have "rsup S \<le> ?m" using Sm lub
-    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-  ultimately  show ?thesis by arith
-qed
-
-lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "rsup S \<in> S"
-  using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
-
-lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "isUb S S (rsup S)"
-  using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS]
-  unfolding isUb_def setle_def by metis
-
-lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_unique: assumes b: "S *<= b" and S: "\<forall>b' < b. \<exists>x \<in> S. b' < x"
-  shows "rsup S = b"
-using b S
-unfolding setle_def rsup_alt
-apply -
-apply (rule some_equality)
-apply (metis  linorder_not_le order_eq_iff[symmetric])+
-done
-
-lemma rsup_le_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> rsup T"
-  apply (rule rsup_le)
-  apply simp
-  using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def)
-
-lemma isUb_def': "isUb R S = (\<lambda>x. S *<= x \<and> x \<in> R)"
-  apply (rule ext)
-  by (metis isUb_def)
-
-lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def)
-lemma rsup_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
-  shows "a \<le> rsup S \<and> rsup S \<le> b"
-proof-
-  from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
-  hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
-  from Se obtain y where y: "y \<in> S" by blast
-  from lub l have "a \<le> rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
-    apply (erule ballE[where x=y])
-    apply (erule ballE[where x=y])
-    apply arith
-    using y apply auto
-    done
-  with b show ?thesis by blast
-qed
-
-lemma rsup_abs_le: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> a"
-  unfolding abs_le_interval_iff  using rsup_bounds[of S "-a" a]
-  by (auto simp add: setge_def setle_def)
-
-lemma rsup_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rsup S - l\<bar> \<le> e"
-proof-
-  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
-  show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th
-    by  (auto simp add: setge_def setle_def)
-qed
-
-definition rinf:: "real set \<Rightarrow> real" where
-  "rinf S = (SOME a. isGlb UNIV S a)"
-
-lemma rinf_alt: "rinf S = (SOME a. (\<forall>x \<in> S. x \<ge> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<ge> b) \<longrightarrow> a \<ge> b))"  by (auto simp  add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def)
-
-lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
-  shows "\<exists>(t::real). isGlb UNIV S t"
-proof-
-  let ?M = "uminus ` S"
-  from lb have th: "\<exists>y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def)
-    by (rule_tac x="-y" in exI, auto)
-  from Se have Me: "\<exists>x. x \<in> ?M" by blast
-  from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast
-  have "isGlb UNIV S (- t)" using t
-    apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def)
-    apply (erule_tac x="-y" in allE)
-    apply auto
-    done
-  then show ?thesis by metis
-qed
-
-lemma rinf: assumes Se: "S \<noteq> {}" and b: "\<exists>b. b <=* S"
-  shows "isGlb UNIV S (rinf S)"
-using Se b
-unfolding rinf_def
-apply clarify
-apply (rule someI_ex)
-apply (rule reals_complete_Glb)
-apply (auto simp add: isLb_def setle_def setge_def)
-done
-
-lemma rinf_ge: assumes Se: "S \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> b"
-proof-
-  from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def)
-  from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)"  by blast
-  then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def)
-qed
-
-lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "rinf S = Min S"
-using fS Se
-proof-
-  let ?m = "Min S"
-  from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?m" by metis
-  with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def)
-  from Min_in[OF fS Se] glb have mrS: "?m \<ge> rinf S"
-    by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
-  moreover
-  have "rinf S \<ge> ?m" using Sm glb
-    by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def)
-  ultimately  show ?thesis by arith
-qed
-
-lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "rinf S \<in> S"
-  using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
-
-lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "isLb S S (rinf S)"
-  using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS]
-  unfolding isLb_def setge_def by metis
-
-lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
-  shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_unique: assumes b: "b <=* S" and S: "\<forall>b' > b. \<exists>x \<in> S. b' > x"
-  shows "rinf S = b"
-using b S
-unfolding setge_def rinf_alt
-apply -
-apply (rule some_equality)
-apply (metis  linorder_not_le order_eq_iff[symmetric])+
-done
-
-lemma rinf_ge_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> rinf S >= rinf T"
-  apply (rule rinf_ge)
-  apply simp
-  using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def)
-
-lemma isLb_def': "isLb R S = (\<lambda>x. x <=* S \<and> x \<in> R)"
-  apply (rule ext)
-  by (metis isLb_def)
-
-lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
-  shows "a \<le> rinf S \<and> rinf S \<le> b"
-proof-
-  from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
-  hence b: "a \<le> rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
-  from Se obtain y where y: "y \<in> S" by blast
-  from lub u have "b \<ge> rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
-    apply (erule ballE[where x=y])
-    apply (erule ballE[where x=y])
-    apply arith
-    using y apply auto
-    done
-  with b show ?thesis by blast
-qed
-
-lemma rinf_abs_ge: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> a"
-  unfolding abs_le_interval_iff  using rinf_bounds[of S "-a" a]
-  by (auto simp add: setge_def setle_def)
-
-lemma rinf_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rinf S - l\<bar> \<le> e"
-proof-
-  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
-  show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th
-    by  (auto simp add: setge_def setle_def)
-qed
-
-
-
 subsection{* Operator norm. *}
 
-definition "onorm f = rsup {norm (f x)| x. norm x = 1}"
+definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
 
 lemma norm_bound_generalize:
   fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
@@ -2578,7 +2345,7 @@
     have Se: "?S \<noteq> {}" using  norm_basis by auto
     from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
       unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
-    {from rsup[OF Se b, unfolded onorm_def[symmetric]]
+    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
       show "norm (f x) <= onorm f * norm x"
         apply -
         apply (rule spec[where x = x])
@@ -2586,7 +2353,7 @@
         by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
     {
       show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
-        using rsup[OF Se b, unfolded onorm_def[symmetric]]
+        using Sup[OF Se b, unfolded onorm_def[symmetric]]
         unfolding norm_bound_generalize[OF lf, symmetric]
         by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   }
@@ -2612,7 +2379,7 @@
     by(auto intro: vector_choose_size set_ext)
   show ?thesis
     unfolding onorm_def th
-    apply (rule rsup_unique) by (simp_all  add: setle_def)
+    apply (rule Sup_unique) by (simp_all  add: setle_def)
 qed
 
 lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
@@ -3055,31 +2822,6 @@
 qed
 
 (* ------------------------------------------------------------------------- *)
-(* Relate max and min to sup and inf.                                        *)
-(* ------------------------------------------------------------------------- *)
-
-lemma real_max_rsup: "max x y = rsup {x,y}"
-proof-
-  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
-  from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
-  moreover
-  have "max x y \<le> rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"]
-    by (simp add: linorder_linear)
-  ultimately show ?thesis by arith
-qed
-
-lemma real_min_rinf: "min x y = rinf {x,y}"
-proof-
-  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
-  from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
-    by (simp add: linorder_linear)
-  moreover
-  have "min x y \<le> rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"]
-    by simp
-  ultimately show ?thesis by arith
-qed
-
-(* ------------------------------------------------------------------------- *)
 (* Geometric progression.                                                    *)
 (* ------------------------------------------------------------------------- *)
 
@@ -5048,7 +4790,7 @@
 
 (* Infinity norm.                                                            *)
 
-definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
+definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
 
 lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
   by auto
@@ -5065,7 +4807,7 @@
 
 lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
   unfolding infnorm_def
-  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
+  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   unfolding infnorm_set_image
   by auto
 
@@ -5076,13 +4818,13 @@
   have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
   show ?thesis
   unfolding infnorm_def
-  unfolding rsup_finite_le_iff[ OF infnorm_set_lemma]
+  unfolding Sup_finite_le_iff[ OF infnorm_set_lemma]
   apply (subst diff_le_eq[symmetric])
-  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
+  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   unfolding infnorm_set_image bex_simps
   apply (subst th)
   unfolding th1
-  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
+  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
 
   unfolding infnorm_set_image ball_simps bex_simps
   apply simp
@@ -5094,7 +4836,7 @@
 proof-
   have "infnorm x <= 0 \<longleftrightarrow> x = 0"
     unfolding infnorm_def
-    unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
+    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
     unfolding infnorm_set_image ball_simps
     by vector
   then show ?thesis using infnorm_pos_le[of x] by simp
@@ -5105,7 +4847,7 @@
 
 lemma infnorm_neg: "infnorm (- x) = infnorm x"
   unfolding infnorm_def
-  apply (rule cong[of "rsup" "rsup"])
+  apply (rule cong[of "Sup" "Sup"])
   apply blast
   apply (rule set_ext)
   apply auto
@@ -5140,14 +4882,15 @@
     apply (rule finite_imageI) unfolding Collect_def mem_def by simp
   have S0: "?S \<noteq> {}" by blast
   have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
-  from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]
-  show ?thesis unfolding infnorm_def isUb_def setle_def
-    unfolding infnorm_set_image ball_simps by auto
+  from Sup_finite_in[OF fS S0] 
+  show ?thesis unfolding infnorm_def infnorm_set_image 
+    by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty 
+              rangeI real_le_refl)
 qed
 
 lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
   apply (subst infnorm_def)
-  unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
+  unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   unfolding infnorm_set_image ball_simps
   apply (simp add: abs_mult)
   apply (rule allI)
@@ -5180,7 +4923,7 @@
 (* Prove that it differs only up to a bound from Euclidean norm.             *)
 
 lemma infnorm_le_norm: "infnorm x \<le> norm x"
-  unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]
+  unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
   unfolding infnorm_set_image  ball_simps
   by (metis component_le_norm)
 lemma card_enum: "card {1 .. n} = n" by auto
@@ -5200,7 +4943,7 @@
     apply (rule setsum_bounded)
     apply (rule power_mono)
     unfolding abs_of_nonneg[OF infnorm_pos_le]
-    unfolding infnorm_def  rsup_finite_ge_iff[OF infnorm_set_lemma]
+    unfolding infnorm_def  Sup_finite_ge_iff[OF infnorm_set_lemma]
     unfolding infnorm_set_image bex_simps
     apply blast
     by (rule abs_ge_zero)
diff -r 02de0317f66f -r 73a0c804840f src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Oct 28 11:43:06 2009 +0000
@@ -2100,59 +2100,54 @@
   shows "bounded S \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
   by (simp add: bounded_iff)
 
-lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
-  shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
+lemma bounded_has_Sup:
+  fixes S :: "real set"
+  assumes "bounded S" "S \<noteq> {}"
+  shows "\<forall>x\<in>S. x <= Sup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> Sup S <= b"
+proof
+  fix x assume "x\<in>S"
+  thus "x \<le> Sup S"
+    by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
+next
+  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
+    by (metis SupInf.Sup_least)
+qed
+
+lemma Sup_insert:
+  fixes S :: "real set"
+  shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" 
+by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal) 
+
+lemma Sup_insert_finite:
+  fixes S :: "real set"
+  shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
+  apply (rule Sup_insert)
+  apply (rule finite_imp_bounded)
+  by simp
+
+lemma bounded_has_Inf:
+  fixes S :: "real set"
+  assumes "bounded S"  "S \<noteq> {}"
+  shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
 proof
   fix x assume "x\<in>S"
   from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
-  hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
-  thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
-next
-  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> b" using assms
-  using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def]
-  apply (auto simp add: bounded_real)
-  by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def)
-qed
-
-lemma rsup_insert: assumes "bounded S"
-  shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))"
-proof(cases "S={}")
-  case True thus ?thesis using rsup_finite_in[of "{x}"] by auto
+  thus "x \<ge> Inf S" using `x\<in>S`
+    by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
 next
-  let ?S = "insert x S"
-  case False
-  hence *:"\<forall>x\<in>S. x \<le> rsup S" using bounded_has_rsup(1)[of S] using assms by auto
-  hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto
-  hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto
-  moreover
-  have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto
-  { fix y assume as:"isUb UNIV (insert x S) y"
-    hence "max x (rsup S) \<le> y" unfolding isUb_def using rsup_le[OF `S\<noteq>{}`]
-      unfolding setle_def by auto  }
-  hence "max x (rsup S) <=* isUb UNIV (insert x S)" unfolding setge_def Ball_def mem_def by auto
-  hence "isLub UNIV ?S (max x (rsup S))" using ** isLubI2[of UNIV ?S "max x (rsup S)"] unfolding Collect_def by auto
-  ultimately show ?thesis using real_isLub_unique[of UNIV ?S] using `S\<noteq>{}` by auto
-qed
-
-lemma sup_insert_finite: "finite S \<Longrightarrow> rsup(insert x S) = (if S = {} then x else max x (rsup S))"
-  apply (rule rsup_insert)
-  apply (rule finite_imp_bounded)
-  by simp
-
-lemma bounded_has_rinf:
-  assumes "bounded S"  "S \<noteq> {}"
-  shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
-proof
-  fix x assume "x\<in>S"
-  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
-  hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
-  thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
-next
-  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> b" using assms
-  using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def]
-  apply (auto simp add: bounded_real)
-  by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def)
-qed
+  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
+    by (metis SupInf.Inf_greatest)
+qed
+
+lemma Inf_insert:
+  fixes S :: "real set"
+  shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" 
+by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) 
+lemma Inf_insert_finite:
+  fixes S :: "real set"
+  shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
+  by (rule Inf_insert, rule finite_imp_bounded, simp)
+
 
 (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
 lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
@@ -2161,29 +2156,6 @@
   apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   done
 
-lemma rinf_insert: assumes "bounded S"
-  shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs")
-proof(cases "S={}")
-  case True thus ?thesis using rinf_finite_in[of "{x}"] by auto
-next
-  let ?S = "insert x S"
-  case False
-  hence *:"\<forall>x\<in>S. x \<ge> rinf S" using bounded_has_rinf(1)[of S] using assms by auto
-  hence "min x (rinf S) <=* insert x S" unfolding setge_def by auto
-  hence "isGlb UNIV ?S (rinf ?S)" using rinf[of ?S] by auto
-  moreover
-  have **:"isLb UNIV ?S (min x (rinf S))" unfolding isLb_def setge_def using * by auto
-  { fix y assume as:"isLb UNIV (insert x S) y"
-    hence "min x (rinf S) \<ge> y" unfolding isLb_def using rinf_ge[OF `S\<noteq>{}`]
-      unfolding setge_def by auto  }
-  hence "isLb UNIV (insert x S) *<= min x (rinf S)" unfolding setle_def Ball_def mem_def by auto
-  hence "isGlb UNIV ?S (min x (rinf S))" using ** isGlbI2[of UNIV ?S "min x (rinf S)"] unfolding Collect_def by auto
-  ultimately show ?thesis using real_isGlb_unique[of UNIV ?S] using `S\<noteq>{}` by auto
-qed
-
-lemma inf_insert_finite: "finite S ==> rinf(insert x S) = (if S = {} then x else min x (rinf S))"
-  by (rule rinf_insert, rule finite_imp_bounded, simp)
-
 subsection{* Compactness (the definition is the one based on convegent subsequences). *}
 
 definition
@@ -4120,30 +4092,35 @@
   shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
 proof-
   from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
-  { fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> rsup s - x' < e"
-    have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto
-    moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
-    ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto  }
-  thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]]
-    apply(rule_tac x="rsup s" in bexI) by auto
-qed
+  { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e"
+    have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
+    moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
+    ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto  }
+  thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
+    apply(rule_tac x="Sup s" in bexI) by auto
+qed
+
+lemma Inf:
+  fixes S :: "real set"
+  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
+by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
 
 lemma compact_attains_inf:
   fixes s :: "real set"
   assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
 proof-
   from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
-  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s"  "rinf s \<notin> s"  "0 < e"
-      "\<forall>x'\<in>s. x' = rinf s \<or> \<not> abs (x' - rinf s) < e"
-    have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto
+  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s"  "Inf s \<notin> s"  "0 < e"
+      "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
+    have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
     moreover
     { fix x assume "x \<in> s"
-      hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto
-      have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
-    hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto
-    ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto  }
-  thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]]
-    apply(rule_tac x="rinf s" in bexI) by auto
+      hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
+      have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
+    hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
+    ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto  }
+  thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
+    apply(rule_tac x="Inf s" in bexI) by auto
 qed
 
 lemma continuous_attains_sup:
@@ -4413,7 +4390,7 @@
 
 text{* We can state this in terms of diameter of a set.                          *}
 
-definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
+definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
   (* TODO: generalize to class metric_space *)
 
 lemma diameter_bounded:
@@ -4427,12 +4404,22 @@
     hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
   note * = this
   { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
-    have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
+    have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
+      apply auto    (*FIXME: something horrible has happened here!*)
+      apply atomize
+      apply safe
+      apply metis +
+      done
     have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s` isLubD1[OF lub] unfolding setle_def by auto  }
   moreover
   { fix d::real assume "d>0" "d < diameter s"
     hence "s\<noteq>{}" unfolding diameter_def by auto
-    hence lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] unfolding setle_def by auto
+    hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def 
+      apply auto    (*FIXME: something horrible has happened here!*)
+      apply atomize
+      apply safe
+      apply metis +
+      done
     have "\<exists>d' \<in> ?D. d' > d"
     proof(rule ccontr)
       assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
@@ -4456,8 +4443,8 @@
 proof-
   have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
   then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
-  hence "diameter s \<le> norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}" "norm (x - y)"]
-    unfolding setle_def and diameter_def by auto
+  hence "diameter s \<le> norm (x - y)" 
+    by (force simp add: diameter_def intro!: Sup_least) 
   thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto
 qed
 
diff -r 02de0317f66f -r 73a0c804840f 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:43:06 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 02de0317f66f -r 73a0c804840f 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:43:06 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 02de0317f66f -r 73a0c804840f 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:43:06 2009 +0000
@@ -0,0 +1,5 @@
+theory Probability imports
+	Measure
+begin
+
+end
diff -r 02de0317f66f -r 73a0c804840f 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:43:06 2009 +0000
@@ -0,0 +1,6 @@
+(*
+  no_document use_thy "ThisTheory";
+  use_thy "ThatTheory";
+*)
+
+use_thy "Probability";
diff -r 02de0317f66f -r 73a0c804840f 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:43:06 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 02de0317f66f -r 73a0c804840f 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:43:06 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 02de0317f66f -r 73a0c804840f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Product_Type.thy	Wed Oct 28 11:43:06 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 02de0317f66f -r 73a0c804840f src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/SEQ.thy	Wed Oct 28 11:43:06 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 02de0317f66f -r 73a0c804840f src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed Oct 28 00:24:38 2009 +0100
+++ b/src/HOL/Series.thy	Wed Oct 28 11:43:06 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 02de0317f66f -r 73a0c804840f src/HOL/SupInf.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SupInf.thy	Wed Oct 28 11:43:06 2009 +0000
@@ -0,0 +1,462 @@
+(*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
+
+header {*Sup and Inf Operators on Sets of Reals.*}
+
+theory SupInf
+imports RComplete
+begin
+
+lemma minus_max_eq_min:
+  fixes x :: "'a::{lordered_ab_group_add, linorder}"
+  shows "- (max x y) = min (-x) (-y)"
+by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
+
+lemma minus_min_eq_max:
+  fixes x :: "'a::{lordered_ab_group_add, linorder}"
+  shows "- (min x y) = max (-x) (-y)"
+by (metis minus_max_eq_min minus_minus)
+
+lemma minus_Max_eq_Min [simp]:
+  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
+proof (induct S rule: finite_ne_induct)
+  case (singleton x)
+  thus ?case by simp
+next
+  case (insert x S)
+  thus ?case by (simp add: minus_max_eq_min) 
+qed
+
+lemma minus_Min_eq_Max [simp]:
+  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
+proof (induct S rule: finite_ne_induct)
+  case (singleton x)
+  thus ?case by simp
+next
+  case (insert x S)
+  thus ?case by (simp add: minus_min_eq_max) 
+qed
+
+instantiation real :: Sup 
+begin
+definition
+  Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
+
+instance ..
+end
+
+instantiation real :: Inf 
+begin
+definition
+  Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
+
+instance ..
+end
+
+subsection{*Supremum of a set of reals*}
+
+lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
+  fixes x :: real
+  assumes x: "x \<in> X"
+      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+  shows "x \<le> Sup X"
+proof (auto simp add: Sup_real_def) 
+  from reals_complete2
+  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+    by (blast intro: x z)
+  hence "x \<le> s"
+    by (blast intro: x z)
+  also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
+    by (fast intro: Least_equality [symmetric])  
+  finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
+qed
+
+lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
+  fixes z :: real
+  assumes x: "X \<noteq> {}"
+      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+  shows "Sup X \<le> z"
+proof (auto simp add: Sup_real_def) 
+  from reals_complete2 x
+  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+    by (blast intro: z)
+  hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
+    by (best intro: Least_equality)  
+  also with s z have "... \<le> z"
+    by blast
+  finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
+qed
+
+lemma Sup_singleton [simp]: "Sup {x::real} = x"
+  by (force intro: Least_equality simp add: Sup_real_def)
+ 
+lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
+  fixes z :: real
+  assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+  shows  "Sup X = z"
+  by (force intro: Least_equality X z simp add: Sup_real_def)
+ 
+lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
+  fixes x :: real
+  shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
+  by (metis Sup_upper real_le_trans)
+
+lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
+  fixes z :: real
+  shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
+  by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
+
+lemma Sup_eq:
+  fixes a :: real
+  shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
+        \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
+  by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
+        insert_not_empty real_le_anti_sym)
+
+lemma Sup_le:
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+by (metis SupInf.Sup_least setle_def)
+
+lemma Sup_upper_EX: 
+  fixes x :: real
+  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
+  by blast
+
+lemma Sup_insert_nonempty: 
+  fixes x :: real
+  assumes x: "x \<in> X"
+      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+  shows "Sup (insert a X) = max a (Sup X)"
+proof (cases "Sup X \<le> a")
+  case True
+  thus ?thesis
+    apply (simp add: max_def) 
+    apply (rule Sup_eq_maximum)
+    apply (metis insertCI)
+    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
+    done
+next
+  case False
+  hence 1:"a < Sup X" by simp
+  have "Sup X \<le> Sup (insert a X)"
+    apply (rule Sup_least)
+    apply (metis empty_psubset_nonempty psubset_eq x)
+    apply (rule Sup_upper_EX) 
+    apply blast
+    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+    done
+  moreover 
+  have "Sup (insert a X) \<le> Sup X"
+    apply (rule Sup_least)
+    apply blast
+    apply (metis False Sup_upper insertE real_le_linear z) 
+    done
+  ultimately have "Sup (insert a X) = Sup X"
+    by (blast intro:  antisym )
+  thus ?thesis
+    by (metis 1 min_max.le_iff_sup real_less_def)
+qed
+
+lemma Sup_insert_if: 
+  fixes X :: "real set"
+  assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+  shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
+by auto (metis Sup_insert_nonempty z) 
+
+lemma Sup: 
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
+by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) 
+
+lemma Sup_finite_Max: 
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "Sup S = Max S"
+using fS Se
+proof-
+  let ?m = "Max S"
+  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
+  with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
+  from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
+    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+  moreover
+  have "Sup S \<le> ?m" using Sm lub
+    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
+  ultimately  show ?thesis by arith
+qed
+
+lemma Sup_finite_in:
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "Sup S \<in> S"
+  using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
+
+lemma Sup_finite_ge_iff: 
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
+
+lemma Sup_finite_le_iff: 
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
+
+lemma Sup_finite_gt_iff: 
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
+by (metis Se Sup_finite_le_iff fS linorder_not_less)
+
+lemma Sup_finite_lt_iff: 
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
+by (metis Se Sup_finite_ge_iff fS linorder_not_less)
+
+lemma Sup_unique:
+  fixes S :: "real set"
+  shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
+unfolding setle_def
+apply (rule Sup_eq, auto) 
+apply (metis linorder_not_less) 
+done
+
+lemma Sup_abs_le:
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) 
+
+lemma Sup_bounds:
+  fixes S :: "real set"
+  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
+  shows "a \<le> Sup S \<and> Sup S \<le> b"
+proof-
+  from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
+  hence b: "Sup S \<le> b" using u 
+    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
+  from Se obtain y where y: "y \<in> S" by blast
+  from lub l have "a \<le> Sup S"
+    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+       (metis le_iff_sup le_sup_iff y)
+  with b show ?thesis by blast
+qed
+
+lemma Sup_asclose: 
+  fixes S :: "real set"
+  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
+proof-
+  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
+  thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
+    by  (auto simp add: setge_def setle_def)
+qed
+
+
+subsection{*Infimum of a set of reals*}
+
+lemma Inf_lower [intro]: 
+  fixes z :: real
+  assumes x: "x \<in> X"
+      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+  shows "Inf X \<le> x"
+proof -
+  have "-x \<le> Sup (uminus ` X)"
+    by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
+  thus ?thesis 
+    by (auto simp add: Inf_real_def)
+qed
+
+lemma Inf_greatest [intro]: 
+  fixes z :: real
+  assumes x: "X \<noteq> {}"
+      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+  shows "z \<le> Inf X"
+proof -
+  have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
+  hence "z \<le> - Sup (uminus ` X)"
+    by simp
+  thus ?thesis 
+    by (auto simp add: Inf_real_def)
+qed
+
+lemma Inf_singleton [simp]: "Inf {x::real} = x"
+  by (simp add: Inf_real_def) 
+ 
+lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
+  fixes z :: real
+  assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+  shows  "Inf X = z"
+proof -
+  have "Sup (uminus ` X) = -z" using x z
+    by (force intro: Sup_eq_maximum x z)
+  thus ?thesis
+    by (simp add: Inf_real_def) 
+qed
+ 
+lemma Inf_lower2:
+  fixes x :: real
+  shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
+  by (metis Inf_lower real_le_trans)
+
+lemma Inf_real_iff:
+  fixes z :: real
+  shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
+  by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
+            order_less_le_trans)
+
+lemma Inf_eq:
+  fixes a :: real
+  shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
+  by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
+        insert_absorb insert_not_empty real_le_anti_sym)
+
+lemma Inf_ge: 
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+by (metis SupInf.Inf_greatest setge_def)
+
+lemma Inf_lower_EX: 
+  fixes x :: real
+  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
+  by blast
+
+lemma Inf_insert_nonempty: 
+  fixes x :: real
+  assumes x: "x \<in> X"
+      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+  shows "Inf (insert a X) = min a (Inf X)"
+proof (cases "a \<le> Inf X")
+  case True
+  thus ?thesis
+    by (simp add: min_def)
+       (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) 
+next
+  case False
+  hence 1:"Inf X < a" by simp
+  have "Inf (insert a X) \<le> Inf X"
+    apply (rule Inf_greatest)
+    apply (metis empty_psubset_nonempty psubset_eq x)
+    apply (rule Inf_lower_EX) 
+    apply (blast intro: elim:) 
+    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+    done
+  moreover 
+  have "Inf X \<le> Inf (insert a X)"
+    apply (rule Inf_greatest)
+    apply blast
+    apply (metis False Inf_lower insertE real_le_linear z) 
+    done
+  ultimately have "Inf (insert a X) = Inf X"
+    by (blast intro:  antisym )
+  thus ?thesis
+    by (metis False min_max.inf_absorb2 real_le_linear)
+qed
+
+lemma Inf_insert_if: 
+  fixes X :: "real set"
+  assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+  shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
+by auto (metis Inf_insert_nonempty z) 
+
+lemma Inf_greater:
+  fixes z :: real
+  shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
+  by (metis Inf_real_iff mem_def not_leE)
+
+lemma Inf_close:
+  fixes e :: real
+  shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
+  by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
+
+lemma Inf_finite_Min:
+  fixes S :: "real set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
+by (simp add: Inf_real_def Sup_finite_Max image_image) 
+
+lemma Inf_finite_in: 
+  fixes S :: "real set"
+  assumes fS: "finite S" and Se: "S \<noteq> {}"
+  shows "Inf S \<in> S"
+  using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
+
+lemma Inf_finite_ge_iff: 
+  fixes S :: "real set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
+by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
+
+lemma Inf_finite_le_iff:
+  fixes S :: "real set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
+by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
+          real_le_anti_sym real_le_linear)
+
+lemma Inf_finite_gt_iff: 
+  fixes S :: "real set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
+by (metis Inf_finite_le_iff linorder_not_less)
+
+lemma Inf_finite_lt_iff: 
+  fixes S :: "real set"
+  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
+by (metis Inf_finite_ge_iff linorder_not_less)
+
+lemma Inf_unique:
+  fixes S :: "real set"
+  shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
+unfolding setge_def
+apply (rule Inf_eq, auto) 
+apply (metis less_le_not_le linorder_not_less) 
+done
+
+lemma Inf_abs_ge:
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
+by (simp add: Inf_real_def) (rule Sup_abs_le, auto) 
+
+lemma Inf_asclose:
+  fixes S :: "real set"
+  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
+    by auto
+  also have "... \<le> e" 
+    apply (rule Sup_asclose) 
+    apply (auto simp add: S)
+    apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
+    done
+  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
+  thus ?thesis
+    by (simp add: Inf_real_def)
+qed
+
+subsection{*Relate max and min to Sup and Inf.*}
+
+lemma real_max_Sup:
+  fixes x :: real
+  shows "max x y = Sup {x,y}"
+proof-
+  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
+  from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
+  moreover
+  have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
+    by (simp add: linorder_linear)
+  ultimately show ?thesis by arith
+qed
+
+lemma real_min_Inf: 
+  fixes x :: real
+  shows "min x y = Inf {x,y}"
+proof-
+  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
+  from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
+    by (simp add: linorder_linear)
+  moreover
+  have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
+    by simp
+  ultimately show ?thesis by arith
+qed
+
+end