# HG changeset patch
# User immler@in.tum.de
# Date 1352466885 -3600
# Node ID afe886a04198f69d0719e28d2bd866312c196028
# Parent  5da32dc55cd806d84b18792ca952a82181762406
removed redundant/unnecessary assumptions from projective_family

diff -r 5da32dc55cd8 -r afe886a04198 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Nov 07 14:41:49 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 09 14:14:45 2012 +0100
@@ -276,6 +276,10 @@
   "B \<subseteq> (\<Pi>\<^isub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
   by (auto simp: prod_emb_def Pi_iff subset_eq extensional_restrict)
 
+lemma prod_emb_mono:
+  "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
+  by (auto simp: prod_emb_def)
+
 definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
   "PiM I M = extend_measure (\<Pi>\<^isub>E i\<in>I. space (M i))
     {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
diff -r 5da32dc55cd8 -r afe886a04198 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 07 14:41:49 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Nov 09 14:14:45 2012 +0100
@@ -102,7 +102,11 @@
   show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
     using sets[THEN sets_into_space] by (auto simp: space_PiM)
   have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
-      using M.not_empty by auto
+  proof
+    fix i assume "i \<in> L"
+    interpret prob_space "P {i}" using prob_space by simp
+    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 "(\<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))"
@@ -240,14 +244,12 @@
   show ?thesis
   proof (intro positive_def[THEN iffD2] conjI ballI)
     from generatorE[OF G.empty_sets] guess J X . note this[simp]
-    interpret J: finite_product_sigma_finite M J by default fact
     have "X = {}"
       by (rule prod_emb_injective[of J I]) simp_all
     then show "\<mu>G {} = 0" by simp
   next
     fix A assume "A \<in> generator"
     from generatorE[OF this] guess J X . note this[simp]
-    interpret J: finite_product_sigma_finite M J by default fact
     show "0 \<le> \<mu>G A" by (simp add: emeasure_nonneg)
   qed
 qed
@@ -264,7 +266,6 @@
     assume "A \<inter> B = {}"
     have JK: "J \<union> K \<noteq> {}" "J \<union> K \<subseteq> I" "finite (J \<union> K)"
       using J K by auto
-    interpret JK: finite_product_sigma_finite M "J \<union> K" by default fact
     have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
       apply (rule prod_emb_injective[of "J \<union> K" I])
       apply (insert `A \<inter> B = {}` JK J K)
diff -r 5da32dc55cd8 -r afe886a04198 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Wed Nov 07 14:41:49 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Fri Nov 09 14:14:45 2012 +0100
@@ -28,8 +28,6 @@
   assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
   assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
   assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
-  assumes proj_finite_measure: "\<And>J. finite J \<Longrightarrow> emeasure (P J) (space (PiM J M)) \<noteq> \<infinity>"
-  assumes measure_space: "\<And>i. prob_space (M i)"
 begin
 
 lemma emeasure_PiP:
@@ -79,8 +77,7 @@
   let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
   show "Int_stable ?J"
     by (rule Int_stable_PiE)
-  interpret finite_measure "P J" using proj_finite_measure `finite J`
-    by (intro finite_measureI) (simp add: proj_space)
+  interpret prob_space "P J" using prob_space `finite J` by simp
   show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP)
   show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
   show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
@@ -104,7 +101,4 @@
 
 end
 
-sublocale projective_family \<subseteq> M: prob_space "M i" for i
-  by (rule measure_space)
-
 end