src/HOL/Probability/Projective_Family.thy
 changeset 50123 69b35a75caf3 parent 50101 a3bede207a04 child 50124 4161c834c2fd
```     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:14:18 2012 +0100
1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
1.3 @@ -44,7 +44,7 @@
1.4    also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
1.5      using E by (simp add: K.measure_times)
1.6    also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
1.7 -    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
1.8 +    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
1.9    finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
1.10      using X `J \<subseteq> K` apply (subst emeasure_distr)
1.11      by (auto intro!: measurable_restrict_subset simp: space_PiM)
1.12 @@ -93,15 +93,10 @@
1.13    shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
1.14  proof -
1.15    have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
1.16 -  proof safe
1.17 -    fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J"
1.18 -    hence "x j \<in> restrict A J j" by (auto simp: Pi_def)
1.19 -    also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
1.20 -    finally show "x j \<in> space (M j)" .
1.21 -  qed
1.22 +    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
1.23    hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
1.24      emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
1.25 -    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
1.26 +    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
1.27    also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
1.28    proof (rule emeasure_extend_measure_Pair[OF limP_def])
1.29      show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
1.30 @@ -169,7 +164,7 @@
1.31      from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
1.32    qed
1.33    from bchoice[OF this]
1.34 -  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
1.35 +  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
1.36    show "(\<lambda>x. restrict x J) -` X \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i)) = (\<lambda>x. restrict x J) -` Y \<inter> (\<Pi>\<^isub>E i\<in>L. space (M i))"
1.37      using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
1.38  qed fact
1.39 @@ -293,7 +288,7 @@
1.40    have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
1.41    have [simp]: "(K - J) \<inter> K = K - J" by auto
1.42    from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
1.43 -    by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
1.44 +    by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
1.45         auto
1.46  qed
1.47
```