author hoelzl Wed, 07 Dec 2011 15:10:29 +0100 changeset 45777 c36637603821 parent 45776 714100f5fda4 child 45778 df6e210fb44c
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -315,12 +315,9 @@

subsection {* Binary products of $\sigma$-finite measure spaces *}

-locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
+locale pair_sigma_finite = pair_sigma_algebra M1 M2 + M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"

-sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
-  by default
-
lemma (in pair_sigma_finite) measure_cut_measurable_fst:
assumes "Q \<in> sets P" shows "(\<lambda>x. measure M2 (Pair x - Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
proof -
@@ -919,10 +916,7 @@
show "a \<in> A" and "b \<in> B" by auto
qed

-locale pair_finite_sigma_algebra = M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2
-  for M1 :: "('a, 'c) measure_space_scheme" and M2 :: "('b, 'd) measure_space_scheme"
-
-sublocale pair_finite_sigma_algebra \<subseteq> pair_sigma_algebra by default
+locale pair_finite_sigma_algebra = pair_sigma_algebra M1 M2 + M1: finite_sigma_algebra M1 + M2: finite_sigma_algebra M2 for M1 M2

lemma (in pair_finite_sigma_algebra) finite_pair_sigma_algebra:
shows "P = \<lparr> space = space M1 \<times> space M2, sets = Pow (space M1 \<times> space M2), \<dots> = algebra.more P \<rparr>"
@@ -933,20 +927,16 @@
qed

sublocale pair_finite_sigma_algebra \<subseteq> finite_sigma_algebra P
-  apply default
-  using M1.finite_space M2.finite_space
-  apply (subst finite_pair_sigma_algebra) apply simp
-  apply (subst (1 2) finite_pair_sigma_algebra) apply simp
-  done
+proof
+  show "finite (space P)"
+    using M1.finite_space M2.finite_space
+    by (subst finite_pair_sigma_algebra) simp
+  show "sets P = Pow (space P)"
+    by (subst (1 2) finite_pair_sigma_algebra) simp
+qed

-locale pair_finite_space = M1: finite_measure_space M1 + M2: finite_measure_space M2
-  for M1 M2
-
-sublocale pair_finite_space \<subseteq> pair_finite_sigma_algebra
-  by default
-
-sublocale pair_finite_space \<subseteq> pair_sigma_finite
-  by default
+locale pair_finite_space = pair_sigma_finite M1 M2 + pair_finite_sigma_algebra M1 M2 +
+  M1: finite_measure_space M1 + M2: finite_measure_space M2 for M1 M2

lemma (in pair_finite_space) pair_measure_Pair[simp]:
assumes "a \<in> space M1" "b \<in> space M2"
@@ -964,6 +954,10 @@
using pair_measure_Pair assms by (cases x) auto

sublocale pair_finite_space \<subseteq> finite_measure_space P
-  by default (auto simp: space_pair_measure)
+proof unfold_locales
+  show "measure P (space P) \<noteq> \<infinity>"
+    by (subst (2) finite_pair_sigma_algebra)
+qed

end
\ No newline at end of file
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -240,7 +240,7 @@
locale finite_product_sigma_algebra = product_sigma_algebra M
for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
fixes I :: "'i set"
-  assumes finite_index: "finite I"
+  assumes finite_index[simp, intro]: "finite I"

definition
"product_algebra_generator I M = \<lparr> space = (\<Pi>\<^isub>E i \<in> I. space (M i)),
@@ -508,22 +508,15 @@
finally show "(\<lambda>x. \<lambda>i\<in>I. X i x) - E \<inter> space M \<in> sets M" .
qed

-locale product_sigma_finite =
-  fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
+locale product_sigma_finite = product_sigma_algebra M
+  for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"

-locale finite_product_sigma_finite = product_sigma_finite M
-  for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" +
-  fixes I :: "'i set" assumes finite_index'[intro]: "finite I"
-
sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
by (rule sigma_finite_measures)

-sublocale product_sigma_finite \<subseteq> product_sigma_algebra
-  by default
-
-sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
-  by default (fact finite_index')
+locale finite_product_sigma_finite = finite_product_sigma_algebra M I + product_sigma_finite M
+  for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set"

lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
assumes "Pi\<^isub>E I F \<in> sets G"
--- a/src/HOL/Probability/Independent_Family.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -845,8 +845,8 @@
moreover
have "D.prob A = P.prob A"
proof (rule prob_space_unique_Int_stable)
-      show "prob_space ?D'" by default
-      show "prob_space (Pi\<^isub>M I ?M)" by default
+      show "prob_space ?D'" by unfold_locales
+      show "prob_space (Pi\<^isub>M I ?M)" by unfold_locales
show "Int_stable P.G" using M'.Int
by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def)
show "space P.G \<in> sets P.G"
@@ -963,13 +963,13 @@
unfolding space_pair_measure[simplified pair_measure_def space_sigma]
using X.top Y.top by (auto intro!: pair_measure_generatorI)

-    show "prob_space ?J" by default
+    show "prob_space ?J" by unfold_locales
show "space ?J = space ?P"
show "sets ?J = sets (sigma ?P)"

-    show "prob_space XY.P" by default
+    show "prob_space XY.P" by unfold_locales
show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)"

--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -41,36 +41,11 @@
qed
qed

-locale product_prob_space =
-  fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set"
-  assumes prob_spaces: "\<And>i. prob_space (M i)"
-  and I_not_empty: "I \<noteq> {}"
-
-locale finite_product_prob_space = product_prob_space M I
-  for M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme" and I :: "'i set" +
-  assumes finite_index'[intro]: "finite I"
-
-sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
-  by (rule prob_spaces)
-
-sublocale product_prob_space \<subseteq> product_sigma_finite
-  by default
-
-sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite
-  by default (fact finite_index')
-
-sublocale finite_product_prob_space \<subseteq> prob_space "Pi\<^isub>M I M"
-proof
-  show "measure P (space P) = 1"
-    by (simp add: measure_times measure_space_1 setprod_1)
-qed
-
lemma (in product_prob_space) measure_preserving_restrict:
assumes "J \<noteq> {}" "J \<subseteq> K" "finite K"
shows "(\<lambda>f. restrict f J) \<in> measure_preserving (\<Pi>\<^isub>M i\<in>K. M i) (\<Pi>\<^isub>M i\<in>J. M i)" (is "?R \<in> _")
proof -
-  interpret K: finite_product_prob_space M K
-    by default (insert assms, auto)
+  interpret K: finite_product_prob_space M K by default fact
have J: "J \<noteq> {}" "finite J" using assms by (auto simp add: finite_subset)
interpret J: finite_product_prob_space M J
by default (insert J, auto)
@@ -297,7 +272,7 @@
definition (in product_prob_space) infprod_algebra :: "('i \<Rightarrow> 'a) measure_space" where
"infprod_algebra = sigma generator \<lparr> measure :=
(SOME \<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and>
-       measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>"
+       prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>)\<rparr>"

syntax
"_PiP"  :: "[pttrn, 'i set, ('b, 'd) measure_space_scheme] => ('i => 'b, 'd) measure_space_scheme"  ("(3PIP _:_./ _)" 10)
@@ -314,13 +289,13 @@
translations
"PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)"

-sublocale product_prob_space \<subseteq> G!: algebra generator
+lemma (in product_prob_space) algebra_generator:
+  assumes "I \<noteq> {}" shows "algebra generator"
proof
let ?G = generator
show "sets ?G \<subseteq> Pow (space ?G)"
by (auto simp: generator_def emb_def)
-  from I_not_empty
-  obtain i where "i \<in> I" by auto
+  from I \<noteq> {} obtain i where "i \<in> I" by auto
then show "{} \<in> sets ?G"
by (auto intro!: exI[of _ "{i}"] image_eqI[where x="\<lambda>i. {}"]
simp: product_algebra_def sigma_def sigma_sets.Empty generator_def emb_def)
@@ -343,42 +318,54 @@
using XA XB by (auto intro!: generatorI')
qed

-lemma (in product_prob_space) positive_\<mu>G: "positive generator \<mu>G"
-proof (intro positive_def[THEN iffD2] conjI ballI)
-  from generatorE[OF G.empty_sets] guess J X . note this[simp]
-  interpret J: finite_product_sigma_finite M J by default fact
-  have "X = {}"
-    by (rule emb_injective[of J I]) simp_all
-  then show "\<mu>G {} = 0" by simp
-next
-  fix A assume "A \<in> sets generator"
-  from generatorE[OF this] guess J X . note this[simp]
-  interpret J: finite_product_sigma_finite M J by default fact
-  show "0 \<le> \<mu>G A" by simp
+lemma (in product_prob_space) positive_\<mu>G:
+  assumes "I \<noteq> {}"
+  shows "positive generator \<mu>G"
+proof -
+  interpret G!: algebra generator by (rule algebra_generator) fact
+  show ?thesis
+  proof (intro positive_def[THEN iffD2] conjI ballI)
+    from generatorE[OF G.empty_sets] guess J X . note this[simp]
+    interpret J: finite_product_sigma_finite M J by default fact
+    have "X = {}"
+      by (rule emb_injective[of J I]) simp_all
+    then show "\<mu>G {} = 0" by simp
+  next
+    fix A assume "A \<in> sets generator"
+    from generatorE[OF this] guess J X . note this[simp]
+    interpret J: finite_product_sigma_finite M J by default fact
+    show "0 \<le> \<mu>G A" by simp
+  qed
qed

-proof (intro additive_def[THEN iffD2] ballI impI)
-  fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this
-  fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this
-  assume "A \<inter> B = {}"
-  have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
-    using J K by auto
-  interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
-  have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
-    apply (rule emb_injective[of "J \<union> K" I])
-    apply (insert A \<inter> B = {} JK J K)
-    apply (simp_all add: JK.Int emb_simps)
-    done
-  have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
-    using J K by simp_all
-  then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
-  also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
-    using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un)
-  also have "\<dots> = \<mu>G A + \<mu>G B"
-  finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
+  assumes "I \<noteq> {}"
+proof -
+  interpret G!: algebra generator by (rule algebra_generator) fact
+  show ?thesis
+  proof (intro additive_def[THEN iffD2] ballI impI)
+    fix A assume "A \<in> sets generator" with generatorE guess J X . note J = this
+    fix B assume "B \<in> sets generator" with generatorE guess K Y . note K = this
+    assume "A \<inter> B = {}"
+    have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
+      using J K by auto
+    interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
+    have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
+      apply (rule emb_injective[of "J \<union> K" I])
+      apply (insert A \<inter> B = {} JK J K)
+      apply (simp_all add: JK.Int emb_simps)
+      done
+    have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
+      using J K by simp_all
+    then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
+    also have "\<dots> = measure (Pi\<^isub>M (J \<union> K) M) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
+      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq JK.Un)
+    also have "\<dots> = \<mu>G A + \<mu>G B"
+    finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
+  qed
qed

lemma (in product_prob_space) finite_index_eq_finite_product:
@@ -386,7 +373,7 @@
shows "sets (sigma generator) = sets (Pi\<^isub>M I M)"
proof safe
interpret I: finite_product_sigma_algebra M I by default fact
-  have [simp]: "space generator = space (Pi\<^isub>M I M)"
+  have space_generator[simp]: "space generator = space (Pi\<^isub>M I M)"
{ fix A assume "A \<in> sets (sigma generator)"
then show "A \<in> sets I.P" unfolding sets_sigma
@@ -396,19 +383,32 @@
with finite I have "emb I J X \<in> sets I.P" by auto
with emb I J X = A show "A \<in> sets I.P" by simp
qed auto }
-  { fix A assume "A \<in> sets I.P"
-    moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto
-    ultimately show "A \<in> sets (sigma generator)"
-      using finite I I_not_empty unfolding sets_sigma
-      by (intro sigma_sets.Basic generatorI[of I A]) auto }
+  { fix A assume A: "A \<in> sets I.P"
+    show "A \<in> sets (sigma generator)"
+    proof cases
+      assume "I = {}"
+      with I.P_empty[OF this] A
+      have "A = space generator \<or> A = {}"
+        unfolding space_generator by auto
+      then show ?thesis
+        by (auto simp: sets_sigma simp del: space_generator
+                 intro: sigma_sets.Empty sigma_sets_top)
+    next
+      assume "I \<noteq> {}"
+      note A this
+      moreover with I.sets_into_space have "emb I I A = A" by (intro emb_id) auto
+      ultimately show "A \<in> sets (sigma generator)"
+        using finite I unfolding sets_sigma
+        by (intro sigma_sets.Basic generatorI[of I A]) auto
+  qed }
qed

lemma (in product_prob_space) extend_\<mu>G:
"\<exists>\<mu>. (\<forall>s\<in>sets generator. \<mu> s = \<mu>G s) \<and>
-       measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
+       prob_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
proof cases
assume "finite I"
-  interpret I: finite_product_sigma_finite M I by default fact
+  interpret I: finite_product_prob_space M I by default fact
show ?thesis
proof (intro exI[of _ "measure (Pi\<^isub>M I M)"] ballI conjI)
fix A assume "A \<in> sets generator"
@@ -422,13 +422,20 @@
have "\<lparr>space = space generator, sets = sets (sigma generator), measure = measure I.P\<rparr>
= I.P" (is "?P = _")
by (auto intro!: measure_space.equality simp: finite_index_eq_finite_product[OF finite I])
-    then show "measure_space ?P" by simp default
+    show "prob_space ?P"
+    proof
+      show "measure_space ?P" using ?P = I.P by simp default
+      show "measure ?P (space ?P) = 1"
+        using I.measure_space_1 by simp
+    qed
qed
next
let ?G = generator
assume "\<not> finite I"
+  then have I_not_empty: "I \<noteq> {}" by auto
+  interpret G!: algebra generator by (rule algebra_generator) fact
note \<mu>G_mono =

{ fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> sets ?G"

@@ -488,7 +495,9 @@
note this fold le_1 merge_in_G(3) }
note fold = this

-  show ?thesis
+  have "\<exists>\<mu>. (\<forall>s\<in>sets ?G. \<mu> s = \<mu>G s) \<and>
+    measure_space \<lparr>space = space ?G, sets = sets (sigma ?G), measure = \<mu>\<rparr>"
+    (is "\<exists>\<mu>. _ \<and> measure_space (?ms \<mu>)")
fix A assume "A \<in> sets ?G"
with generatorE guess J X . note JX = this
@@ -503,7 +512,7 @@
proof (rule ccontr)
assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0")
moreover have "0 \<le> ?a"
-        using A positive_\<mu>G by (auto intro!: INF_greatest simp: positive_def)
+        using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
ultimately have "0 < ?a" by auto

have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = measure (Pi\<^isub>M J M) X"
@@ -659,7 +668,7 @@
moreover
from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
then have "?M (J k) (A k) (w k) \<noteq> {}"
-          using positive_\<mu>G[unfolded positive_def] 0 < ?a ?a \<le> 1
+          using positive_\<mu>G[OF I_not_empty, unfolded positive_def] 0 < ?a ?a \<le> 1
by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
then have "merge (J k) (w k) (I - J k) x \<in> A k" by auto
@@ -713,28 +722,42 @@
qed
ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
+  qed fact+
+  then guess \<mu> .. note \<mu> = this
+  show ?thesis
+  proof (intro exI[of _ \<mu>] conjI)
+    show "\<forall>S\<in>sets ?G. \<mu> S = \<mu>G S" using \<mu> by simp
+    show "prob_space (?ms \<mu>)"
+    proof
+      show "measure_space (?ms \<mu>)" using \<mu> by simp
+      obtain i where "i \<in> I" using I_not_empty by auto
+      interpret i: finite_product_sigma_finite M "{i}" by default auto
+      let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)"
+      have X: "?X \<in> sets (Pi\<^isub>M {i} M)"
+        by auto
+      with i \<in> I have "emb I {i} ?X \<in> sets generator"
+        by (intro generatorI') auto
+      with \<mu> have "\<mu> (emb I {i} ?X) = \<mu>G (emb I {i} ?X)" by auto
+      with \<mu>G_eq[OF _ _ _ X] i \<in> I
+      have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
+      also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
+        using i \<in> I by (auto simp: emb_def infprod_algebra_def generator_def)
+      finally show "measure (?ms \<mu>) (space (?ms \<mu>)) = 1"
+        using M.measure_space_1 by (simp add: infprod_algebra_def)
+    qed
qed
qed

lemma (in product_prob_space) infprod_spec:
-  shows "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> measure_space (Pi\<^isub>P I M)"
-proof -
-  let ?P = "\<lambda>\<mu>. (\<forall>A\<in>sets generator. \<mu> A = \<mu>G A) \<and>
-       measure_space \<lparr>space = space generator, sets = sets (sigma generator), measure = \<mu>\<rparr>"
-  have **: "measure infprod_algebra = (SOME \<mu>. ?P \<mu>)"
-    unfolding infprod_algebra_def by simp
-  have *: "Pi\<^isub>P I M = \<lparr>space = space generator, sets = sets (sigma generator), measure = measure (Pi\<^isub>P I M)\<rparr>"
-    unfolding infprod_algebra_def by auto
-  show ?thesis
-    apply (subst (2) *)
-    apply (unfold **)
-    apply (rule someI_ex[where P="?P"])
-    apply (rule extend_\<mu>G)
-    done
-qed
+  "(\<forall>s\<in>sets generator. measure (Pi\<^isub>P I M) s = \<mu>G s) \<and> prob_space (Pi\<^isub>P I M)"
+  (is "?Q infprod_algebra")
+  unfolding infprod_algebra_def
+  by (rule someI2_ex[OF extend_\<mu>G])
+     (auto simp: sigma_def generator_def)

-sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M"
-  using infprod_spec by auto
+sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
+  using infprod_spec by simp

lemma (in product_prob_space) measure_infprod_emb:
assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
@@ -745,22 +768,6 @@
with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
qed

-sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
-proof
-  obtain i where "i \<in> I" using I_not_empty by auto
-  interpret i: finite_product_sigma_finite M "{i}" by default auto
-  let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)"
-  have "?X \<in> sets (Pi\<^isub>M {i} M)"
-    by auto
-  from measure_infprod_emb[OF _ _ _ this] i \<in> I
-  have "\<mu> (emb I {i} ?X) = measure (M i) (space (M i))"
-  also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
-    using i \<in> I by (auto simp: emb_def infprod_algebra_def generator_def)
-  finally show "\<mu> (space (Pi\<^isub>P I M)) = 1"
-    using M.measure_space_1 by simp
-qed
-
lemma (in product_prob_space) measurable_component:
assumes "i \<in> I"
shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)"
@@ -821,7 +828,8 @@
assume "J = {}"
then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra"
by (auto simp: infprod_algebra_def generator_def sigma_def emb_def)
-  then show ?thesis using J = {} prob_space by simp
+  then show ?thesis using J = {} P.prob_space
+    by simp
next
assume "J \<noteq> {}"
interpret J: finite_product_prob_space M J by default fact+
--- a/src/HOL/Probability/Information.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Information.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -198,7 +198,7 @@
proof -
interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
-  have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by default
+  have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
note RN = RN_deriv[OF ms ac]

from real_RN_deriv[OF fms ac] guess D . note D = this
@@ -460,7 +460,7 @@
proof -
interpret information_space M by default fact
interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
-  have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by default
+  have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis .
qed

@@ -558,7 +558,7 @@

have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A"
proof (rule XY.KL_eq_0_imp)
-    show "prob_space ?J" by default
+    show "prob_space ?J" by unfold_locales
show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
using ac by (simp add: P_def)
show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))"
@@ -624,7 +624,7 @@
have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
-      unfolding prob_space_def by simp
+      unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp
qed auto
qed

@@ -654,7 +654,7 @@
note rv = assms[THEN finite_random_variableD]
show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
proof (rule XY.absolutely_continuousI)
-    show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
+    show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0"
then obtain a b where "x = (a, b)"
and "distribution X {a} = 0 \<or> distribution Y {b} = 0"
@@ -684,8 +684,8 @@
interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>"
using assms by (auto intro!: joint_distribution_finite_prob_space)

-  have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
-  have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
+  have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
+  have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales

show ?sum
unfolding Let_def mutual_information_def
--- a/src/HOL/Probability/Measure.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -1175,13 +1175,21 @@
finally show ?thesis by simp
qed

-locale finite_measure = measure_space +
+locale finite_measure = sigma_finite_measure +
assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<infinity>"

-sublocale finite_measure < sigma_finite_measure
-proof
-  show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)"
-    using finite_measure_of_space by (auto intro!: exI[of _ "\<lambda>x. space M"])
+lemma finite_measureI[Pure.intro!]:
+  assumes "measure_space M"
+  assumes *: "measure M (space M) \<noteq> \<infinity>"
+  shows "finite_measure M"
+proof -
+  interpret measure_space M by fact
+  show "finite_measure M"
+  proof
+    show "measure M (space M) \<noteq> \<infinity>" by fact
+    show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<infinity>)"
+      using * by (auto intro!: exI[of _ "\<lambda>x. space M"])
+  qed
qed

lemma (in finite_measure) finite_measure[simp, intro]:
@@ -1222,22 +1230,19 @@
assumes "S \<in> sets M"
shows "finite_measure (restricted_space S)"
(is "finite_measure ?r")
-  unfolding finite_measure_def finite_measure_axioms_def
-proof (intro conjI)
+proof
show "measure_space ?r" using restricted_measure_space[OF assms] .
-next
show "measure ?r (space ?r) \<noteq> \<infinity>" using finite_measure[OF S \<in> sets M] by auto
qed

lemma (in measure_space) restricted_to_finite_measure:
assumes "S \<in> sets M" "\<mu> S \<noteq> \<infinity>"
shows "finite_measure (restricted_space S)"
-proof -
-  have "measure_space (restricted_space S)"
+proof
+  show "measure_space (restricted_space S)"
using S \<in> sets M by (rule restricted_measure_space)
-  then show ?thesis
-    unfolding finite_measure_def finite_measure_axioms_def
-    using assms by auto
+  show "measure (restricted_space S) (space (restricted_space S)) \<noteq> \<infinity>"
+    by simp fact
qed

lemma (in finite_measure) finite_measure_Diff:
@@ -1357,66 +1362,43 @@

section "Finite spaces"

-locale finite_measure_space = measure_space + finite_sigma_algebra +
-  assumes finite_single_measure[simp]: "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<infinity>"
+locale finite_measure_space = finite_measure + finite_sigma_algebra
+
+lemma finite_measure_spaceI[Pure.intro!]:
+  assumes "finite (space M)"
+  assumes sets_Pow: "sets M = Pow (space M)"
+    and space: "measure M (space M) \<noteq> \<infinity>"
+    and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}"
+    and add: "\<And>A. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})"
+  shows "finite_measure_space M"
+proof -
+  interpret finite_sigma_algebra M
+  proof
+    show "finite (space M)" by fact
+  qed (auto simp: sets_Pow)
+  interpret measure_space M
+    show "sigma_algebra M" by default
+    show "finite (space M)" by fact
+    show "positive M (measure M)"
+      by (auto simp: add positive_def intro!: setsum_nonneg pos)
+    show "additive M (measure M)"
+      using finite (space M)
+               intro!: setsum_Un_disjoint dest: finite_subset)
+  qed
+  interpret finite_measure M
+  proof
+    show "\<mu> (space M) \<noteq> \<infinity>" by fact
+  qed default
+  show "finite_measure_space M"
+    by default
+qed

lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
using measure_setsum[of "space M" "\<lambda>i. {i}"]
by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)

-lemma finite_measure_spaceI:
-  assumes "finite (space M)" "sets M = Pow(space M)" and space: "measure M (space M) \<noteq> \<infinity>"
-    and add: "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B"
-    and "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A"
-  shows "finite_measure_space M"
-    unfolding finite_measure_space_def finite_measure_space_axioms_def
-proof (intro allI impI conjI)
-  show "measure_space M"
-    have *: "\<lparr>space = space M, sets = Pow (space M), \<dots> = algebra.more M\<rparr> = M"
-      unfolding assms(2)[symmetric] by (auto intro!: algebra.equality)
-    show "sigma_algebra M"
-      using sigma_algebra_Pow[of "space M" "algebra.more M"]
-      unfolding * .
-    show "finite (space M)" by fact
-    show "positive M (measure M)" unfolding positive_def using assms by auto
-    show "additive M (measure M)" unfolding additive_def using assms by simp
-  qed
-  then interpret measure_space M .
-  show "finite_sigma_algebra M"
-  proof
-    show "finite (space M)" by fact
-    show "sets M = Pow (space M)" using assms by auto
-  qed
-  { fix x assume *: "x \<in> space M"
-    with add[of "{x}" "space M - {x}"] space
-    show "\<mu> {x} \<noteq> \<infinity>" by (auto simp: insert_absorb[OF *] Diff_subset) }
-qed
-
-sublocale finite_measure_space \<subseteq> finite_measure
-proof
-  show "\<mu> (space M) \<noteq> \<infinity>"
-    unfolding sum_over_space[symmetric] setsum_Pinfty
-    using finite_space finite_single_measure by auto
-qed
-
-lemma finite_measure_space_iff:
-  "finite_measure_space M \<longleftrightarrow>
-    finite (space M) \<and> sets M = Pow(space M) \<and> measure M (space M) \<noteq> \<infinity> \<and>
-    measure M {} = 0 \<and> (\<forall>A\<subseteq>space M. 0 \<le> measure M A) \<and>
-    (\<forall>A\<subseteq>space M. \<forall>B\<subseteq>space M. A \<inter> B = {} \<longrightarrow> measure M (A \<union> B) = measure M A + measure M B)"
-    (is "_ = ?rhs")
-proof (intro iffI)
-  assume "finite_measure_space M"
-  then interpret finite_measure_space M .
-  show ?rhs
-    using finite_space sets_eq_Pow measure_additive empty_measure finite_measure
-    by auto
-next
-  assume ?rhs then show "finite_measure_space M"
-    by (auto intro!: finite_measure_spaceI)
-qed
-
lemma (in finite_measure_space) finite_measure_singleton:
assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
using A finite_subset[OF A finite_space]
--- a/src/HOL/Probability/Probability_Measure.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -9,12 +9,20 @@
imports Lebesgue_Measure
begin

-locale prob_space = measure_space +
+locale prob_space = finite_measure +
assumes measure_space_1: "measure M (space M) = 1"

-sublocale prob_space < finite_measure
-proof
-  from measure_space_1 show "\<mu> (space M) \<noteq> \<infinity>" by simp
+lemma prob_spaceI[Pure.intro!]:
+  assumes "measure_space M"
+  assumes *: "measure M (space M) = 1"
+  shows "prob_space M"
+proof -
+  interpret finite_measure M
+  proof
+    show "measure_space M" by fact
+    show "measure M (space M) \<noteq> \<infinity>" using * by simp
+  qed
+  show "prob_space M" by default fact
qed

abbreviation (in prob_space) "events \<equiv> sets M"
@@ -31,9 +39,10 @@
lemma (in prob_space) prob_space_cong:
assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "space N = space M" "sets N = sets M"
shows "prob_space N"
-proof -
-  interpret N: measure_space N by (intro measure_space_cong assms)
-  show ?thesis by default (insert assms measure_space_1, simp)
+proof
+  show "measure_space N" by (intro measure_space_cong assms)
+  show "measure N (space N) = 1"
+    using measure_space_1 assms by simp
qed

lemma (in prob_space) distribution_cong:
@@ -201,18 +210,17 @@
assumes S: "sigma_algebra S"
assumes T: "T \<in> measure_preserving M S"
shows "prob_space S"
-proof -
+proof
interpret S: measure_space S
using S and T by (rule measure_space_vimage)
-  show ?thesis
-  proof
-    from T[THEN measure_preservingD2]
-    have "T - space S \<inter> space M = space M"
-      by (auto simp: measurable_def)
-    with T[THEN measure_preservingD, of "space S", symmetric]
-    show  "measure S (space S) = 1"
-      using measure_space_1 by simp
-  qed
+  show "measure_space S" ..
+
+  from T[THEN measure_preservingD2]
+  have "T - space S \<inter> space M = space M"
+    by (auto simp: measurable_def)
+  with T[THEN measure_preservingD, of "space S", symmetric]
+  show  "measure S (space S) = 1"
+    using measure_space_1 by simp
qed

lemma prob_space_unique_Int_stable:
@@ -539,12 +547,14 @@
joint_distribution (\<lambda>x. (X x, Y x)) Z {((x, y), z)}"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])

-locale pair_prob_space = M1: prob_space M1 + M2: prob_space M2 for M1 M2
-
-sublocale pair_prob_space \<subseteq> pair_sigma_finite M1 M2 by default
+locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2

sublocale pair_prob_space \<subseteq> P: prob_space P
-by default (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure)
+proof
+  show "measure_space P" ..
+  show "measure P (space P) = 1"
+    by (simp add: pair_measure_times M1.measure_space_1 M2.measure_space_1 space_pair_measure)
+qed

assumes "\<And>A. \<lbrakk> range A \<subseteq> sets M ; disjoint_family A ; (\<Union>i. A i) \<in> sets M\<rbrakk> \<Longrightarrow>
@@ -557,20 +567,21 @@
shows "prob_space ((MX \<Otimes>\<^isub>M MY) \<lparr> measure := ereal \<circ> joint_distribution X Y\<rparr>)"
using random_variable_pairI[OF assms] by (rule distribution_prob_space)

+locale product_prob_space = product_sigma_finite M for M :: "'i \<Rightarrow> ('a, 'b) measure_space_scheme" +
+  fixes I :: "'i set"
+  assumes prob_space: "\<And>i. prob_space (M i)"

-locale finite_product_prob_space =
-  fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
-    and I :: "'i set"
-  assumes prob_space: "\<And>i. prob_space (M i)" and finite_index: "finite I"
-
-sublocale finite_product_prob_space \<subseteq> M: prob_space "M i" for i
+sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
by (rule prob_space)

-sublocale finite_product_prob_space \<subseteq> finite_product_sigma_finite M I
-  by default (rule finite_index)
+locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I

sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^isub>M i\<in>I. M i"
-  proof qed (simp add: measure_times M.measure_space_1 setprod_1)
+proof
+  show "measure_space P" ..
+  show "measure P (space P) = 1"
+    by (simp add: measure_times M.measure_space_1 setprod_1)
+qed

lemma (in finite_product_prob_space) prob_times:
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets (M i)"
@@ -667,7 +678,7 @@
interpret MX: finite_sigma_algebra MX using assms by simp
interpret MY: finite_sigma_algebra MY using assms by simp
interpret P: pair_finite_sigma_algebra MX MY by default
-  show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" by default
+  show "finite_sigma_algebra (MX \<Otimes>\<^isub>M MY)" ..
have sa: "sigma_algebra M" by default
show "(\<lambda>x. (X x, Y x)) \<in> measurable M (MX \<Otimes>\<^isub>M MY)"
unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
@@ -754,25 +765,9 @@
using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp

-locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
-
-sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default
-sublocale pair_finite_prob_space \<subseteq> pair_finite_space M1 M2  by default
-sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default
+locale pair_finite_prob_space = pair_prob_space M1 M2 + pair_finite_space M1 M2 + M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2

-locale product_finite_prob_space =
-  fixes M :: "'i \<Rightarrow> ('a,'b) measure_space_scheme"
-    and I :: "'i set"
-  assumes finite_space: "\<And>i. finite_prob_space (M i)" and finite_index: "finite I"
-
-sublocale product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space .
-sublocale product_finite_prob_space \<subseteq> finite_product_sigma_finite M I by default (rule finite_index)
-sublocale product_finite_prob_space \<subseteq> prob_space "Pi\<^isub>M I M"
-proof
-  show "\<mu> (space P) = 1"
-    using measure_times[OF M.top] M.measure_space_1
-    by (simp add: setprod_1 space_product_algebra)
-qed
+sublocale pair_finite_prob_space \<subseteq> finite_prob_space P by default

lemma funset_eq_UN_fun_upd_I:
assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
@@ -815,7 +810,12 @@
using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
qed

-lemma (in product_finite_prob_space) singleton_eq_product:
+locale finite_product_finite_prob_space = finite_product_prob_space M I for M I +
+  assumes finite_space: "\<And>i. finite_prob_space (M i)"
+
+sublocale finite_product_finite_prob_space \<subseteq> M!: finite_prob_space "M i" using finite_space .
+
+lemma (in finite_product_finite_prob_space) singleton_eq_product:
assumes x: "x \<in> space P" shows "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
proof (safe intro!: ext[of _ x])
fix y i assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
@@ -823,7 +823,7 @@
by (cases "i \<in> I") (auto simp: extensional_def)
qed (insert x, auto)

-sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
+sublocale finite_product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
proof
show "finite (space P)"
using finite_index M.finite_space by auto
@@ -844,23 +844,18 @@
then show "X \<in> sets P" by simp
qed
with space_closed show [simp]: "sets P = Pow (space P)" ..
-
-  { fix x assume "x \<in> space P"
-    from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto
-    then show "\<mu> {x} \<noteq> \<infinity>"
-      using measure_space_1 by auto }
qed

-lemma (in product_finite_prob_space) measure_finite_times:
+lemma (in finite_product_finite_prob_space) measure_finite_times:
"(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))"
by (rule measure_times) simp

-lemma (in product_finite_prob_space) measure_singleton_times:
+lemma (in finite_product_finite_prob_space) measure_singleton_times:
assumes x: "x \<in> space P" shows "\<mu> {x} = (\<Prod>i\<in>I. M.\<mu> i {x i})"
unfolding singleton_eq_product[OF x] using x
by (intro measure_finite_times) auto

-lemma (in product_finite_prob_space) prob_finite_times:
+lemma (in finite_product_finite_prob_space) prob_finite_times:
assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)"
shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
proof -
@@ -873,13 +868,13 @@
finally show ?thesis by simp
qed

-lemma (in product_finite_prob_space) prob_singleton_times:
+lemma (in finite_product_finite_prob_space) prob_singleton_times:
assumes x: "x \<in> space P"
shows "prob {x} = (\<Prod>i\<in>I. M.prob i {x i})"
unfolding singleton_eq_product[OF x] using x
by (intro prob_finite_times) auto

-lemma (in product_finite_prob_space) prob_finite_product:
+lemma (in finite_product_finite_prob_space) prob_finite_product:
"A \<subseteq> space P \<Longrightarrow> prob A = (\<Sum>x\<in>A. \<Prod>i\<in>I. M.prob i {x i})"
by (auto simp add: finite_measure_singleton prob_singleton_times
simp del: space_product_algebra
@@ -1010,11 +1005,12 @@
assumes "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M"
and "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A"
shows "prob_space N"
-proof -
+proof
interpret N: measure_space N
by (rule measure_space_subalgebra[OF assms])
-  show ?thesis
-  proof qed (insert assms(4)[OF N.top], simp add: assms measure_space_1)
+  show "measure_space N" ..
+  show "measure N (space N) = 1"
+    using assms(4)[OF N.top] by (simp add: assms measure_space_1)
qed

lemma (in prob_space) prob_space_of_restricted_space:
@@ -1028,44 +1024,76 @@
by (rule A.sigma_algebra_cong) auto
show "prob_space ?P"
proof
+    show "measure_space ?P"
+    proof
+      show "positive ?P (measure ?P)"
+      proof (simp add: positive_def, safe)
+        show "0 / \<mu> A = 0" using \<mu> A \<noteq> 0 by (cases "\<mu> A") (auto simp: zero_ereal_def)
+        fix B assume "B \<in> events"
+        with real_measure[of "A \<inter> B"] real_measure[OF A \<in> events] A \<in> sets M
+        show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)
+      qed
+      show "countably_additive ?P (measure ?P)"
+        fix B and F :: "nat \<Rightarrow> 'a set"
+        assume F: "range F \<subseteq> op \<inter> A  events" "disjoint_family F"
+        { fix i
+          from F have "F i \<in> op \<inter> A  events" by auto
+          with A \<in> events have "F i \<in> events" by auto }
+        moreover then have "range F \<subseteq> events" by auto
+        moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S"
+          by (simp add: mult_commute divide_ereal_def)
+        moreover have "0 \<le> inverse (\<mu> A)"
+          using real_measure[OF A \<in> events] by auto
+        ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A"
+          by (auto simp: suminf_cmult_ereal)
+      qed
+    qed
show "measure ?P (space ?P) = 1"
using real_measure[OF A \<in> events] \<mu> A \<noteq> 0 by auto
-    show "positive ?P (measure ?P)"
-    proof (simp add: positive_def, safe)
-      show "0 / \<mu> A = 0" using \<mu> A \<noteq> 0 by (cases "\<mu> A") (auto simp: zero_ereal_def)
-      fix B assume "B \<in> events"
-      with real_measure[of "A \<inter> B"] real_measure[OF A \<in> events] A \<in> sets M
-      show "0 \<le> \<mu> (A \<inter> B) / \<mu> A" by (auto simp: Int)
-    qed
-    show "countably_additive ?P (measure ?P)"
-      fix B and F :: "nat \<Rightarrow> 'a set"
-      assume F: "range F \<subseteq> op \<inter> A  events" "disjoint_family F"
-      { fix i
-        from F have "F i \<in> op \<inter> A  events" by auto
-        with A \<in> events have "F i \<in> events" by auto }
-      moreover then have "range F \<subseteq> events" by auto
-      moreover have "\<And>S. \<mu> S / \<mu> A = inverse (\<mu> A) * \<mu> S"
-        by (simp add: mult_commute divide_ereal_def)
-      moreover have "0 \<le> inverse (\<mu> A)"
-        using real_measure[OF A \<in> events] by auto
-      ultimately show "(\<Sum>i. \<mu> (F i) / \<mu> A) = \<mu> (\<Union>i. F i) / \<mu> A"
-        by (auto simp: suminf_cmult_ereal)
-    qed
qed
qed

lemma finite_prob_spaceI:
assumes "finite (space M)" "sets M = Pow(space M)"
-    and "measure M (space M) = 1" "measure M {} = 0" "\<And>A. A \<subseteq> space M \<Longrightarrow> 0 \<le> measure M A"
-    and "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M B"
+    and 1: "measure M (space M) = 1" and "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> measure M {x}"
+    and add: "\<And>A B. A \<subseteq> space M \<Longrightarrow> measure M A = (\<Sum>x\<in>A. measure M {x})"
shows "finite_prob_space M"
-  unfolding finite_prob_space_eq
-proof
-  show "finite_measure_space M" using assms
-    by (auto intro!: finite_measure_spaceI)
-  show "measure M (space M) = 1" by fact
+proof -
+  interpret finite_measure_space M
+  proof
+    show "measure M (space M) \<noteq> \<infinity>" using 1 by simp
+  qed fact+
+  show ?thesis by default fact
+qed
+
+lemma (in finite_prob_space) distribution_eq_setsum:
+  "distribution X A = (\<Sum>x\<in>A \<inter> X  space M. distribution X {x})"
+proof -
+  have *: "X - A \<inter> space M = (\<Union>x\<in>A \<inter> X  space M. X - {x} \<inter> space M)"
+    by auto
+  then show "distribution X A = (\<Sum>x\<in>A \<inter> X  space M. distribution X {x})"
+    using finite_space unfolding distribution_def *
+    by (intro finite_measure_finite_Union)
+       (auto simp: disjoint_family_on_def)
+qed
+
+lemma (in finite_prob_space) distribution_eq_setsum_finite:
+  assumes "finite A"
+  shows "distribution X A = (\<Sum>x\<in>A. distribution X {x})"
+proof -
+  note distribution_eq_setsum[of X A]
+  also have "(\<Sum>x\<in>A \<inter> X  space M. distribution X {x}) = (\<Sum>x\<in>A. distribution X {x})"
+  proof (intro setsum_mono_zero_cong_left ballI)
+    fix i assume "i\<in>A - A \<inter> X  space M"
+    then have "X - {i} \<inter> space M = {}" by auto
+    then show "distribution X {i} = 0"
+  next
+    show "finite A" by fact
+  qed simp_all
+  finally show ?thesis .
qed

lemma (in finite_prob_space) finite_measure_space:
@@ -1075,11 +1103,9 @@
proof (rule finite_measure_spaceI, simp_all)
show "finite (X  space M)" using finite_space by simp
next
-  fix A B :: "'x set" assume "A \<inter> B = {}"
-  then show "distribution X (A \<union> B) = distribution X A + distribution X B"
-    unfolding distribution_def
-    by (subst finite_measure_Union[symmetric])
-       (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow)
+  fix A assume "A \<subseteq> X  space M"
+  then show "distribution X A = (\<Sum>x\<in>A. distribution X {x})"
+    by (subst distribution_eq_setsum) (simp add: Int_absorb2)
qed

lemma (in finite_prob_space) finite_prob_space_of_images:
@@ -1095,11 +1121,9 @@
show "finite (s1 \<times> s2)"
using assms by auto
next
-  fix A B :: "('x*'y) set" assume "A \<inter> B = {}"
-  then show "joint_distribution X Y (A \<union> B) = joint_distribution X Y A + joint_distribution X Y B"
-    unfolding distribution_def
-    by (subst finite_measure_Union[symmetric])
-       (auto intro!: arg_cong[where f=\<mu>'] simp: sets_eq_Pow)
+  fix A assume "A \<subseteq> (s1 \<times> s2)"
+  with assms show "joint_distribution X Y A = (\<Sum>x\<in>A. joint_distribution X Y {x})"
+    by (intro distribution_eq_setsum_finite) (auto dest: finite_subset)
qed

lemma (in finite_prob_space) finite_product_measure_space_of_images:
@@ -1140,7 +1164,10 @@

interpretation pborel: prob_space pborel
-  by default (simp add: one_ereal_def pborel_def)
+proof
+  show "measure pborel (space pborel) = 1"
+    by (simp add: one_ereal_def pborel_def)
+qed default

lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 ..< 1} then real (lborel.\<mu> A) else 0)"
unfolding pborel.\<mu>'_def by (auto simp: pborel_def)
--- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -427,35 +427,38 @@
have f_le_\<nu>: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. ?F A x \<partial>M) \<le> \<nu> A"
using f \<in> G unfolding G_def by auto
have fmM: "finite_measure ?M"
-    fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
-    have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)"
-      using range A \<subseteq> sets M \<And>x. 0 \<le> f x
-      by (intro positive_integral_suminf[symmetric]) auto
-    also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)"
-      using \<And>x. 0 \<le> f x
-      by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF disjoint_family A])
-    finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" .
-    moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
-    moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN)
-    moreover {
-      have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)"
-        using A f \<in> G unfolding G_def by (auto simp: countable_UN)
-      also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp
-      finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp }
-    moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)"
-      using A by (intro f_le_\<nu>) auto
-    ultimately
-    show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)"
-      by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive)
+  proof
+    show "measure_space ?M"
+      fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
+      have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)"
+        using range A \<subseteq> sets M \<And>x. 0 \<le> f x
+        by (intro positive_integral_suminf[symmetric]) auto
+      also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)"
+        using \<And>x. 0 \<le> f x
+        by (intro positive_integral_cong) (simp add: suminf_cmult_ereal suminf_indicator[OF disjoint_family A])
+      finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" .
+      moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
+      moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN)
+      moreover {
+        have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)"
+          using A f \<in> G unfolding G_def by (auto simp: countable_UN)
+        also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp
+        finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp }
+      moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)"
+        using A by (intro f_le_\<nu>) auto
+      ultimately
+      show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)"
+        by (subst suminf_ereal_minus) (simp_all add: positive_integral_positive)
+    next
+      fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A - \<integral>\<^isup>+ x. ?F A x \<partial>M"
+        using f_le_\<nu>[OF A] f \<in> G M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff)
+    qed
next
-    fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A - \<integral>\<^isup>+ x. ?F A x \<partial>M"
-      using f_le_\<nu>[OF A] f \<in> G M'.finite_measure[OF A] by (auto simp: G_def ereal_le_minus_iff)
-  next
-    show "\<nu> (space M) - (\<integral>\<^isup>+ x. ?F (space M) x \<partial>M) \<noteq> \<infinity>" (is "?a - ?b \<noteq> _")
+    show "measure ?M (space ?M) \<noteq> \<infinity>"
using positive_integral_positive[of "?F (space M)"]
-      by (cases rule: ereal2_cases[of ?a ?b]) auto
+      by (cases rule: ereal2_cases[of "\<nu> (space M)" "\<integral>\<^isup>+ x. ?F (space M) x \<partial>M"]) auto
qed
then interpret M: finite_measure ?M
where "space ?M = space M" and "sets ?M = sets M" and "measure ?M = ?t"
@@ -498,11 +501,14 @@
interpret b: sigma_algebra ?Mb by (intro sigma_algebra_cong) auto
have Mb: "finite_measure ?Mb"
proof
-      show "positive ?Mb (measure ?Mb)"
-        using 0 \<le> b by (auto simp: positive_def)
-      show "countably_additive ?Mb (measure ?Mb)"
-        using 0 \<le> b measure_countably_additive
-        by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq)
+      show "measure_space ?Mb"
+      proof
+        show "positive ?Mb (measure ?Mb)"
+          using 0 \<le> b by (auto simp: positive_def)
+        show "countably_additive ?Mb (measure ?Mb)"
+          using 0 \<le> b measure_countably_additive
+          by (auto simp: countably_additive_def suminf_cmult_ereal subset_eq)
+      qed
show "measure ?Mb (space ?Mb) \<noteq> \<infinity>"
using b by auto
qed
@@ -772,7 +778,6 @@
(is "finite_measure ?R") by (rule restricted_finite_measure[OF Q_sets[of i]])
then interpret R: finite_measure ?R .
have fmv: "finite_measure (restricted_space (Q i) \<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?Q")
-      unfolding finite_measure_def finite_measure_axioms_def
proof
show "measure_space ?Q"
using v.restricted_measure_space Q_sets[of i] by auto
@@ -849,8 +854,8 @@
let ?MT = "M\<lparr> measure := ?T \<rparr>"
interpret T: finite_measure ?MT
where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T"
-    unfolding finite_measure_def finite_measure_axioms_def using borel finite nn
-    by (auto intro!: measure_space_density cong: positive_integral_cong)
+    using borel finite nn
+    by (auto intro!: measure_space_density finite_measureI cong: positive_integral_cong)
have "T.absolutely_continuous \<nu>"
proof (unfold T.absolutely_continuous_def, safe)
fix N assume "N \<in> sets M" "(\<integral>\<^isup>+x. h x * indicator N x \<partial>M) = 0"
@@ -1000,7 +1005,7 @@
using h_borel h_nn by (rule measure_space_density) simp
then interpret h: measure_space ?H .
interpret h: finite_measure "M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M) \<rparr>"
-    by default (simp cong: positive_integral_cong add: fin)
+    by (intro H finite_measureI) (simp cong: positive_integral_cong add: fin)
let ?fM = "M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)\<rparr>"
interpret f: measure_space ?fM
using f by (rule measure_space_density) simp
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Mon Dec 05 15:10:15 2011 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Wed Dec 07 15:10:29 2011 +0100
@@ -22,11 +22,8 @@
by default (simp_all add: M_def one_ereal_def)