src/HOL/Probability/Projective_Family.thy
changeset 50123 69b35a75caf3
parent 50101 a3bede207a04
child 50124 4161c834c2fd
--- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 16:14:18 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 19 12:29:02 2012 +0100
@@ -44,7 +44,7 @@
   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))"
     using E by (simp add: K.measure_times)
   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))"
-    using `J \<subseteq> K` sets_into_space E by (force simp:  Pi_iff split: split_if_asm)
+    using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
   finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
     using X `J \<subseteq> K` apply (subst emeasure_distr)
     by (auto intro!: measurable_restrict_subset simp: space_PiM)
@@ -93,15 +93,10 @@
   shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
 proof -
   have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
-  proof safe
-    fix x j assume "x \<in> Pi J (restrict A J)" "j \<in> J"
-    hence "x j \<in> restrict A J j" by (auto simp: Pi_def)
-    also have "\<dots> \<subseteq> space (M j)" using sets_into_space A `j \<in> J` by auto
-    finally show "x j \<in> space (M j)" .
-  qed
+    using sets_into_space[OF A] by (auto simp: PiE_iff) blast
   hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
     emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
-    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id Pi_def)
+    using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
   also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
   proof (rule emeasure_extend_measure_Pair[OF limP_def])
     show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
@@ -169,7 +164,7 @@
     from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
   qed
   from bchoice[OF this]
-  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by auto
+  show "(\<Pi>\<^isub>E i\<in>L. space (M i)) \<noteq> {}" by (auto simp: PiE_def)
   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))"
     using `prod_emb L M J X = prod_emb L M J Y` by (simp add: prod_emb_def)
 qed fact
@@ -293,7 +288,7 @@
   have [simp]: "(K - J) \<inter> (K \<union> J) = K - J" by auto
   have [simp]: "(K - J) \<inter> K = K - J" by auto
   from y `K \<subseteq> I` `J \<subseteq> I` show ?thesis
-    by (simp split: split_merge add: prod_emb_def Pi_iff extensional_merge_sub set_eq_iff space_PiM)
+    by (simp split: split_merge add: prod_emb_def Pi_iff PiE_def extensional_merge_sub set_eq_iff space_PiM)
        auto
 qed