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.96              by (simp add: P_closed)
    1.97 @@ -1072,7 +1072,7 @@
    1.98      by (simp add: P_closed)
    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