src/HOL/Probability/Projective_Family.thy
 changeset 50124 4161c834c2fd parent 50123 69b35a75caf3 child 50244 de72bbe42190
```     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:09:11 2012 +0100
1.3 @@ -124,13 +124,9 @@
1.4    shows "limP J M P = P J" (is "?P = _")
1.5  proof (rule measure_eqI_generator_eq)
1.6    let ?J = "{Pi\<^isub>E J E | E. \<forall>i\<in>J. E i \<in> sets (M i)}"
1.7 -  let ?F = "\<lambda>i. \<Pi>\<^isub>E k\<in>J. space (M k)"
1.8    let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
1.9 -  show "Int_stable ?J"
1.10 -    by (rule Int_stable_PiE)
1.11    interpret prob_space "P J" using proj_prob_space `finite J` by simp
1.12 -  show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
1.13 -  show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
1.14 +  show "emeasure ?P (\<Pi>\<^isub>E k\<in>J. space (M k)) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
1.15    show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
1.16      using `finite J` proj_sets by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
1.17    fix X assume "X \<in> ?J"
1.18 @@ -142,7 +138,7 @@
1.19    show "emeasure (limP J M P) X = emeasure (P J) X"
1.20      unfolding X using E
1.21      by (intro emeasure_limP assms) simp
1.22 -qed (insert `finite J`, auto intro!: prod_algebraI_finite)
1.23 +qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
1.24
1.25  lemma emeasure_fun_emb[simp]:
1.26    assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
1.27 @@ -150,9 +146,12 @@
1.28    using assms
1.29    by (subst limP_finite) (auto simp: limP_finite finite_subset projective)
1.30
1.31 +abbreviation
1.32 +  "emb L K X \<equiv> prod_emb L M K X"
1.33 +
1.34  lemma prod_emb_injective:
1.35 -  assumes "J \<noteq> {}" "J \<subseteq> L" "finite J" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
1.36 -  assumes "prod_emb L M J X = prod_emb L M J Y"
1.37 +  assumes "J \<subseteq> L" and sets: "X \<in> sets (Pi\<^isub>M J M)" "Y \<in> sets (Pi\<^isub>M J M)"
1.38 +  assumes "emb L J X = emb L J Y"
1.39    shows "X = Y"
1.40  proof (rule injective_vimage_restrict)
1.41    show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
1.42 @@ -169,9 +168,6 @@
1.43      using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
1.44  qed fact
1.45
1.46 -abbreviation
1.47 -  "emb L K X \<equiv> prod_emb L M K X"
1.48 -
1.49  definition generator :: "('i \<Rightarrow> 'a) set set" where
1.50    "generator = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` sets (Pi\<^isub>M J M))"
1.51
1.52 @@ -265,11 +261,7 @@
1.53  lemma generatorE:
1.54    assumes A: "A \<in> generator"
1.55    obtains J X where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A" "\<mu>G A = emeasure (limP J M P) X"
1.56 -proof -
1.57 -  from generator_Ex[OF A] obtain X J where "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)" "emb I J X = A"
1.58 -    "\<mu>G A = emeasure (limP J M P) X" by auto
1.59 -  then show thesis by (intro that) auto
1.60 -qed
1.61 +  using generator_Ex[OF A] by atomize_elim auto
1.62
1.63  lemma merge_sets:
1.64    "J \<inter> K = {} \<Longrightarrow> A \<in> sets (Pi\<^isub>M (J \<union> K) M) \<Longrightarrow> x \<in> space (Pi\<^isub>M J M) \<Longrightarrow> (\<lambda>y. merge J K (x,y)) -` A \<inter> space (Pi\<^isub>M K M) \<in> sets (Pi\<^isub>M K M)"
```