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)"