src/HOL/Probability/Fin_Map.thy
 changeset 50244 de72bbe42190 parent 50124 4161c834c2fd child 50245 dea9363887a6
```     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Thu Nov 22 10:09:54 2012 +0100
1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
1.3 @@ -620,7 +620,7 @@
1.4
1.5  lemma PiF_gen_subset: "{(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} \<subseteq>
1.6      Pow (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
1.7 -  by (auto simp: Pi'_def) (blast dest: sets_into_space)
1.8 +  by (auto simp: Pi'_def) (blast dest: sets.sets_into_space)
1.9
1.10  lemma space_PiF: "space (PiF I M) = (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
1.11    unfolding PiF_def using PiF_gen_subset by (rule space_measure_of)
1.12 @@ -757,7 +757,7 @@
1.13        done
1.14    qed
1.15    also have "\<dots> \<in> sets (PiF I M)"
1.16 -    apply (intro Int countable_nat_UN subsetI, safe)
1.17 +    apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
1.18      apply (case_tac "set (from_nat i) \<in> I")
1.19      apply simp_all
1.20      apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]])
1.21 @@ -807,7 +807,7 @@
1.22    case (Union a)
1.23    have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
1.24      by simp
1.25 -  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro countable_nat_UN) auto
1.26 +  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto
1.27    finally show ?case .
1.28  next
1.29    case (Compl a)
1.30 @@ -838,10 +838,10 @@
1.31    show "(\<lambda>x. finmap_of (J x) (f x)) -` Pi' K S \<inter> space N \<in> sets N"
1.32      unfolding eq r
1.33      apply (simp del: INT_simps add: )
1.34 -    apply (intro conjI impI finite_INT JN Int[OF top])
1.35 +    apply (intro conjI impI sets.finite_INT JN sets.Int[OF sets.top])
1.36      apply simp apply assumption
1.37      apply (subst Int_assoc[symmetric])
1.38 -    apply (rule Int)
1.39 +    apply (rule sets.Int)
1.40      apply (intro measurable_sets[OF f] *) apply force apply assumption
1.41      apply (intro JN)
1.42      done
1.43 @@ -865,7 +865,7 @@
1.44    assume "i \<in> I"
1.45    hence "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space (PiF {I} M) =
1.46      Pi' I (\<lambda>x. if x = i then A else space (M x))"
1.47 -    using sets_into_space[OF ] `A \<in> sets (M i)` assms
1.48 +    using sets.sets_into_space[OF ] `A \<in> sets (M i)` assms
1.49      by (auto simp: space_PiF Pi'_def)
1.50    thus ?thesis  using assms `A \<in> sets (M i)`
1.51      by (intro in_sets_PiFI) auto
1.52 @@ -934,7 +934,7 @@
1.53    shows "A \<inter> B \<in> sets M" using assms
1.54  proof -
1.55    have "A \<inter> B = (A \<inter> space M) \<inter> B"
1.56 -    using assms sets_into_space by auto
1.57 +    using assms sets.sets_into_space by auto
1.58    thus ?thesis using assms by auto
1.59  qed
1.60
1.61 @@ -959,7 +959,7 @@
1.62    show "A \<in> sigma_sets ?\<Omega> ?R"
1.63    proof -
1.64      from `I \<noteq> {}` X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})"
1.65 -      using sets_into_space
1.66 +      using sets.sets_into_space
1.67        by (auto simp: space_PiF product_def) blast
1.68      also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
1.69        using X `I \<noteq> {}` assms by (intro R.finite_INT) (auto simp: space_PiF)
1.70 @@ -970,7 +970,7 @@
1.71    then obtain i B where A: "A = {f\<in>\<Pi>' i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)"
1.72      by auto
1.73    then have "A = (\<Pi>' j \<in> I. if j = i then B else space (M j))"
1.74 -    using sets_into_space[OF A(3)]
1.75 +    using sets.sets_into_space[OF A(3)]
1.76      apply (auto simp: Pi'_iff split: split_if_asm)
1.77      apply blast
1.78      done
1.79 @@ -1033,7 +1033,7 @@
1.80        sigma_sets (space ?P) {{f \<in> \<Pi>' i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
1.81      using sets_PiF_single[of I M] by (simp add: space_P)
1.82    also have "\<dots> \<subseteq> sets (sigma (space (PiF {I} M)) P)"
1.83 -  proof (safe intro!: sigma_sets_subset)
1.84 +  proof (safe intro!: sets.sigma_sets_subset)
1.85      fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
1.86      have "(\<lambda>x. (x)\<^isub>F i) \<in> measurable ?P (sigma (space (M i)) (E i))"
1.87      proof (subst measurable_iff_measure_of)
1.88 @@ -1051,7 +1051,7 @@
1.89            using S_mono
1.90            by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
1.91          also have "\<dots> \<in> sets ?P"
1.92 -        proof (safe intro!: countable_UN)
1.93 +        proof (safe intro!: sets.countable_UN)
1.94            fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
1.95              using A S_in_E
1.97 @@ -1072,7 +1072,7 @@
1.99    show "sigma_sets (space (PiF {I} M)) P \<subseteq> sets (PiF {I} M)"
1.100      using `finite I` `I \<noteq> {}`
1.101 -    by (auto intro!: sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
1.102 +    by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
1.103  qed
1.104
1.105  lemma enumerable_sigma_fprod_algebra_sigma_eq:
1.106 @@ -1176,7 +1176,7 @@
1.107      show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
1.108      proof
1.109        fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
1.110 -      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets_into_space)
1.111 +      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
1.112        let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
1.113        have "x = \<Union>{?x J |J. finite J}" by auto
1.114        also have "\<dots> \<in> sets borel"
1.115 @@ -1316,7 +1316,7 @@
1.116    have "mf (fm x) \<in> extensional J"
1.117      by (auto simp: mf_def extensional_def compose_def)
1.118    moreover
1.119 -  have "x \<in> extensional J" using assms sets_into_space
1.120 +  have "x \<in> extensional J" using assms sets.sets_into_space
1.121      by (force simp: space_PiM PiE_def)
1.122    moreover
1.123    { fix i assume "i \<in> J"
1.124 @@ -1344,7 +1344,7 @@
1.125    have "fm ` X = (mf) -` X \<inter> space (PiF {f ` J} (\<lambda>_. M))"
1.126    proof safe
1.127      fix x assume "x \<in> X"
1.128 -    with mf_fm[of x] sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
1.129 +    with mf_fm[of x] sets.sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
1.130      show "fm x \<in> space (PiF {f ` J} (\<lambda>_. M))" by (simp add: space_PiF assms)
1.131    next
1.132      fix y x
1.133 @@ -1396,7 +1396,7 @@
1.134    shows "emeasure M X = emeasure (mapmeasure M (\<lambda>_. N)) (fm ` X)"
1.135    unfolding mapmeasure_def
1.136  proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
1.137 -  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets_into_space)
1.138 +  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
1.139    from assms inj_on_fm[of "\<lambda>_. N"] set_mp[OF this] have "fm -` fm ` X \<inter> space (Pi\<^isub>M J (\<lambda>_. N)) = X"
1.140      by (auto simp: vimage_image_eq inj_on_def)
1.141    thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1
```