diff -r 4c1f119fadb9 -r f96aa31b739d src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Sat May 01 16:13:24 2010 -0700
+++ b/src/HOL/Probability/Measure.thy	Mon May 03 10:28:19 2010 -0700
@@ -365,6 +365,18 @@
     by arith
 qed
 
+lemma (in measure_space) measure_mono:
+  assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
+  shows "measure M a \<le> measure M b"
+proof -
+  have "b = a \<union> (b - a)" using assms by auto
+  moreover have "{} = a \<inter> (b - a)" by auto
+  ultimately have "measure M b = measure M a + measure M (b - a)"
+    using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
+  moreover have "measure M (b - a) \<ge> 0" using positive assms by auto
+  ultimately show "measure M a \<le> measure M b" by auto
+qed
+
 lemma disjoint_family_Suc:
   assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
   shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
@@ -1045,4 +1057,12 @@
   qed
 qed
 
+locale finite_measure_space = measure_space +
+  assumes finite_space: "finite (space M)"
+  and sets_eq_Pow: "sets M = Pow (space M)"
+
+lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. measure M {x}) = measure M (space M)"
+  using measure_finitely_additive''[of "space M" "\<lambda>i. {i}"]
+  by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
+
 end
\ No newline at end of file