src/HOL/Probability/Projective_Family.thy
changeset 50101 a3bede207a04
parent 50095 94d7dfa9f404
child 50123 69b35a75caf3
     1.1 --- a/src/HOL/Probability/Projective_Family.thy	Fri Nov 16 14:46:23 2012 +0100
     1.2 +++ b/src/HOL/Probability/Projective_Family.thy	Fri Nov 16 14:46:23 2012 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4    fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
     1.5    assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow>
     1.6       (P H) (prod_emb H M J X) = (P J) X"
     1.7 -  assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
     1.8 +  assumes proj_prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
     1.9    assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
    1.10    assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
    1.11  begin
    1.12 @@ -133,7 +133,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 prob_space "P J" using prob_space `finite J` by simp
    1.17 +  interpret prob_space "P J" using proj_prob_space `finite J` by simp
    1.18    show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
    1.19    show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
    1.20    show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
    1.21 @@ -165,7 +165,7 @@
    1.22    have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
    1.23    proof
    1.24      fix i assume "i \<in> L"
    1.25 -    interpret prob_space "P {i}" using prob_space by simp
    1.26 +    interpret prob_space "P {i}" using proj_prob_space by simp
    1.27      from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
    1.28    qed
    1.29    from bchoice[OF this]