diff -r f9ff311992b6 -r 3e39b0e730d6 src/HOL/Probability/Complete_Measure.thy
--- a/src/HOL/Probability/Complete_Measure.thy	Wed Feb 02 10:35:41 2011 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy	Wed Feb 02 12:34:45 2011 +0100
@@ -7,9 +7,24 @@
 
 locale completeable_measure_space = measure_space
 
-definition (in completeable_measure_space) completion :: "'a algebra" where
+definition (in completeable_measure_space)
+  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
+    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
+
+definition (in completeable_measure_space)
+  "main_part A = fst (Eps (split_completion A))"
+
+definition (in completeable_measure_space)
+  "null_part A = snd (Eps (split_completion A))"
+
+abbreviation (in completeable_measure_space) "\<mu>' A \<equiv> \<mu> (main_part A)"
+
+definition (in completeable_measure_space) completion :: "('a, 'b) measure_space_scheme" where
   "completion = \<lparr> space = space M,
-    sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"
+                  sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' },
+                  measure = \<mu>',
+                  \<dots> = more M \<rparr>"
+
 
 lemma (in completeable_measure_space) space_completion[simp]:
   "space completion = space M" unfolding completion_def by simp
@@ -58,16 +73,6 @@
        auto
 qed auto
 
-definition (in completeable_measure_space)
-  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
-    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
-
-definition (in completeable_measure_space)
-  "main_part A = fst (Eps (split_completion A))"
-
-definition (in completeable_measure_space)
-  "null_part A = snd (Eps (split_completion A))"
-
 lemma (in completeable_measure_space) split_completion:
   assumes "A \<in> sets completion"
   shows "split_completion A (main_part A, null_part A)"
@@ -108,17 +113,15 @@
   show "\<mu> (null_part S) = 0" by auto
 qed
 
-definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"
-
 lemma (in completeable_measure_space) \<mu>'_set[simp]:
   assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
 proof -
   have S: "S \<in> sets completion" using assms by auto
   then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
-  also have "\<dots> = \<mu> (main_part S)"
+  also have "\<dots> = \<mu>' S"
     using S assms measure_additive[of "main_part S" "null_part S"]
     by (auto simp: measure_additive)
-  finally show ?thesis unfolding \<mu>'_def by simp
+  finally show ?thesis by simp
 qed
 
 lemma (in completeable_measure_space) sets_completionI_sub:
@@ -154,7 +157,7 @@
     unfolding * ..
   also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
     using null_set S by (intro measure_Un_null_set) auto
-  finally show ?thesis unfolding \<mu>'_def .
+  finally show ?thesis .
 qed
 
 lemma (in completeable_measure_space) \<mu>_main_part_Un:
@@ -168,30 +171,35 @@
     unfolding range_binary_eq Un_range_binary UN by auto
 qed
 
-sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'
-proof
-  show "\<mu>' {} = 0" by auto
-next
-  show "countably_additive completion \<mu>'"
-  proof (unfold countably_additive_def, intro allI conjI impI)
-    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
-    have "disjoint_family (\<lambda>i. main_part (A i))"
-    proof (intro disjoint_family_on_bisimulation[OF A(2)])
-      fix n m assume "A n \<inter> A m = {}"
-      then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
-        using A by (subst (1 2) main_part_null_part_Un) auto
-      then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
+sublocale completeable_measure_space \<subseteq> completion!: measure_space completion
+  where "measure completion = \<mu>'"
+proof -
+  show "measure_space completion"
+  proof
+    show "measure completion {} = 0" by (auto simp: completion_def)
+  next
+    show "countably_additive completion (measure completion)"
+    proof (intro countably_additiveI)
+      fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
+      have "disjoint_family (\<lambda>i. main_part (A i))"
+      proof (intro disjoint_family_on_bisimulation[OF A(2)])
+        fix n m assume "A n \<inter> A m = {}"
+        then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
+          using A by (subst (1 2) main_part_null_part_Un) auto
+        then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
+      qed
+      then have "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
+        unfolding completion_def using A by (auto intro!: measure_countably_additive)
+      then show "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = measure completion (UNION UNIV A)"
+        by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])
     qed
-    then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"
-      unfolding \<mu>'_def using A by (intro measure_countably_additive) auto
-    then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"
-      unfolding \<mu>_main_part_UN[OF A(1)] .
   qed
+  show "measure completion = \<mu>'" unfolding completion_def by simp
 qed
 
 lemma (in completeable_measure_space) completion_ex_simple_function:
-  assumes f: "completion.simple_function f"
-  shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
+  assumes f: "simple_function completion f"
+  shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
 proof -
   let "?F x" = "f -` {x} \<inter> space M"
   have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
@@ -248,11 +256,11 @@
   shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
 proof -
   from g[THEN completion.borel_measurable_implies_simple_function_sequence]
-  obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
-  then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
+  obtain f where "\<And>i. simple_function completion (f i)" "f \<up> g" by auto
+  then have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)"
     using completion_ex_simple_function by auto
   from this[THEN choice] obtain f' where
-    sf: "\<And>i. simple_function (f' i)" and
+    sf: "\<And>i. simple_function M (f' i)" and
     AE: "\<forall>i. AE x. f i x = f' i x" by auto
   show ?thesis
   proof (intro bexI)