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