src/HOL/Probability/Projective_Family.thy
 changeset 50041 afe886a04198 parent 50040 5da32dc55cd8 child 50042 6fe18351e9dd
```     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Wed Nov 07 14:41:49 2012 +0100
1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Fri Nov 09 14:14:45 2012 +0100
1.3 @@ -28,8 +28,6 @@
1.4    assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
1.5    assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
1.6    assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
1.7 -  assumes proj_finite_measure: "\<And>J. finite J \<Longrightarrow> emeasure (P J) (space (PiM J M)) \<noteq> \<infinity>"
1.8 -  assumes measure_space: "\<And>i. prob_space (M i)"
1.9  begin
1.10
1.11  lemma emeasure_PiP:
1.12 @@ -79,8 +77,7 @@
1.13    let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
1.14    show "Int_stable ?J"
1.15      by (rule Int_stable_PiE)
1.16 -  interpret finite_measure "P J" using proj_finite_measure `finite J`
1.17 -    by (intro finite_measureI) (simp add: proj_space)
1.18 +  interpret prob_space "P J" using prob_space `finite J` by simp
1.19    show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_PiP)
1.20    show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
1.21    show "sets (PiP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
1.22 @@ -104,7 +101,4 @@
1.23
1.24  end
1.25
1.26 -sublocale projective_family \<subseteq> M: prob_space "M i" for i
1.27 -  by (rule measure_space)
1.28 -
1.29  end
```