renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
authorhoelzl
Fri Nov 16 14:46:23 2012 +0100 (2012-11-16)
changeset 50101a3bede207a04
parent 50100 9af8721ecd20
child 50103 3d89c38408cd
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Projective_Limit.thy
     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]
     2.1 --- a/src/HOL/Probability/Projective_Limit.thy	Fri Nov 16 14:46:23 2012 +0100
     2.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Fri Nov 16 14:46:23 2012 +0100
     2.3 @@ -207,7 +207,7 @@
     2.4        OF `I \<noteq> {}`, OF `I \<noteq> {}`])
     2.5      fix A assume "A \<in> ?G"
     2.6      with generatorE guess J X . note JX = this
     2.7 -    interpret prob_space "P J" using prob_space[OF `finite J`] .
     2.8 +    interpret prob_space "P J" using proj_prob_space[OF `finite J`] .
     2.9      show "\<mu>G A \<noteq> \<infinity>" using JX by (simp add: limP_finite)
    2.10    next
    2.11      fix Z assume Z: "range Z \<subseteq> ?G" "decseq Z" "(\<Inter>i. Z i) = {}"
    2.12 @@ -241,7 +241,7 @@
    2.13        note [simp] = `\<And>n. finite (J n)`
    2.14        from J  Z_emb have Z_eq: "\<And>n. Z n = emb I (J n) (B n)" "\<And>n. Z n \<in> ?G"
    2.15          unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto)
    2.16 -      interpret prob_space "P (J i)" for i using prob_space by simp
    2.17 +      interpret prob_space "P (J i)" for i using proj_prob_space by simp
    2.18        have "?a \<le> \<mu>G (Z 0)" by (auto intro: INF_lower)
    2.19        also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq \<mu>G_eq limP_finite proj_sets)
    2.20        finally have "?a \<noteq> \<infinity>" by simp
    2.21 @@ -636,13 +636,13 @@
    2.22    show "emeasure (lim\<^isub>B I P) (space (lim\<^isub>B I P)) = 1"
    2.23    proof cases
    2.24      assume "I = {}"
    2.25 -    interpret prob_space "P {}" using prob_space by simp
    2.26 +    interpret prob_space "P {}" using proj_prob_space by simp
    2.27      show ?thesis
    2.28        by (simp add: space_PiM_empty limP_finite emeasure_space_1 `I = {}`)
    2.29    next
    2.30      assume "I \<noteq> {}"
    2.31      then obtain i where "i \<in> I" by auto
    2.32 -    interpret prob_space "P {i}" using prob_space by simp
    2.33 +    interpret prob_space "P {i}" using proj_prob_space by simp
    2.34      have R: "(space (lim\<^isub>B I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"
    2.35        by (auto simp: prod_emb_def space_PiM)
    2.36      moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)
    2.37 @@ -660,7 +660,7 @@
    2.38    assumes X: "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
    2.39    shows "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (P J) (Pi\<^isub>E J B)"
    2.40  proof cases
    2.41 -  interpret prob_space "P {}" using prob_space by simp
    2.42 +  interpret prob_space "P {}" using proj_prob_space by simp
    2.43    assume "J = {}"
    2.44    moreover have "emb I {} {\<lambda>x. undefined} = space (lim\<^isub>B I P)"
    2.45      by (auto simp: space_PiM prod_emb_def)
    2.46 @@ -677,7 +677,7 @@
    2.47    assumes "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
    2.48    shows "measure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = measure (P J) (Pi\<^isub>E J B)"
    2.49  proof -
    2.50 -  interpret prob_space "P J" using prob_space assms by simp
    2.51 +  interpret prob_space "P J" using proj_prob_space assms by simp
    2.52    show ?thesis
    2.53      using emeasure_limB_emb[OF assms]
    2.54      unfolding emeasure_eq_measure limP_finite[OF `finite J` `J \<subseteq> I`] P.emeasure_eq_measure