1.1 --- a/src/HOL/Probability/Measure.thy	Fri May 20 16:22:24 2011 +0200
     1.2 +++ b/src/HOL/Probability/Measure.thy	Fri May 20 16:23:03 2011 +0200
     1.3 @@ -1379,6 +1379,11 @@
     1.4      by (auto intro!: finite_measure_spaceI)
     1.5  qed
     1.6  
     1.7 +lemma (in finite_measure_space) finite_measure_singleton:
     1.8 +  assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
     1.9 +  using A finite_subset[OF A finite_space]
    1.10 +  by (intro finite_measure_finite_singleton) auto
    1.11 +
    1.12  lemma suminf_cmult_indicator:
    1.13    fixes f :: "nat \<Rightarrow> extreal"
    1.14    assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"

     2.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri May 20 16:22:24 2011 +0200
     2.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri May 20 16:23:03 2011 +0200
     2.3 @@ -598,22 +598,22 @@
     2.4      using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
     2.5  qed
     2.6  
     2.7 +lemma (in product_finite_prob_space) singleton_eq_product:
     2.8 +  assumes x: "x \<in> space P" shows "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
     2.9 +proof (safe intro!: ext[of _ x])
    2.10 +  fix y i assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
    2.11 +  with x show "y i = x i"
    2.12 +    by (cases "i \<in> I") (auto simp: extensional_def)
    2.13 +qed (insert x, auto)
    2.14 +
    2.15  sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
    2.16  proof
    2.17    show "finite (space P)"
    2.18      using finite_index M.finite_space by auto
    2.19  
    2.20    { fix x assume "x \<in> space P"
    2.21 -    then have x: "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
    2.22 -    proof safe
    2.23 -      fix y assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
    2.24 -      show "y = x"
    2.25 -      proof
    2.26 -        fix i show "y i = x i"
    2.27 -          using * `x \<in> space P` by (cases "i \<in> I") (auto simp: extensional_def)
    2.28 -      qed
    2.29 -    qed auto
    2.30 -    with `x \<in> space P` have "{x} \<in> sets P"
    2.31 +    with this[THEN singleton_eq_product]
    2.32 +    have "{x} \<in> sets P"
    2.33        by (auto intro!: in_P) }
    2.34    note x_in_P = this
    2.35  
    2.36 @@ -628,7 +628,6 @@
    2.37    qed
    2.38    with space_closed show [simp]: "sets P = Pow (space P)" ..
    2.39  
    2.40 -
    2.41    { fix x assume "x \<in> space P"
    2.42      from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto
    2.43      then show "\<mu> {x} \<noteq> \<infinity>"
    2.44 @@ -639,7 +638,12 @@
    2.45    "(\<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))"
    2.46    by (rule measure_times) simp
    2.47  
    2.48 -lemma (in product_finite_prob_space) prob_times:
    2.49 +lemma (in product_finite_prob_space) measure_singleton_times:
    2.50 +  assumes x: "x \<in> space P" shows "\<mu> {x} = (\<Prod>i\<in>I. M.\<mu> i {x i})"
    2.51 +  unfolding singleton_eq_product[OF x] using x
    2.52 +  by (intro measure_finite_times) auto
    2.53 +
    2.54 +lemma (in product_finite_prob_space) prob_finite_times:
    2.55    assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)"
    2.56    shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
    2.57  proof -
    2.58 @@ -652,6 +656,18 @@
    2.59    finally show ?thesis by simp
    2.60  qed
    2.61  
    2.62 +lemma (in product_finite_prob_space) prob_singleton_times:
    2.63 +  assumes x: "x \<in> space P"
    2.64 +  shows "prob {x} = (\<Prod>i\<in>I. M.prob i {x i})"
    2.65 +  unfolding singleton_eq_product[OF x] using x
    2.66 +  by (intro prob_finite_times) auto
    2.67 +
    2.68 +lemma (in product_finite_prob_space) prob_finite_product:
    2.69 +  "A \<subseteq> space P \<Longrightarrow> prob A = (\<Sum>x\<in>A. \<Prod>i\<in>I. M.prob i {x i})"
    2.70 +  by (auto simp add: finite_measure_singleton prob_singleton_times
    2.71 +           simp del: space_product_algebra
    2.72 +           intro!: setsum_cong prob_singleton_times)
    2.73 +
    2.74  lemma (in prob_space) joint_distribution_finite_prob_space:
    2.75    assumes X: "finite_random_variable MX X"
    2.76    assumes Y: "finite_random_variable MY Y"