src/HOL/Probability/Fin_Map.thy
 changeset 50244 de72bbe42190 parent 50124 4161c834c2fd child 50245 dea9363887a6
```--- a/src/HOL/Probability/Fin_Map.thy	Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
@@ -620,7 +620,7 @@

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>
Pow (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
-  by (auto simp: Pi'_def) (blast dest: sets_into_space)
+  by (auto simp: Pi'_def) (blast dest: sets.sets_into_space)

lemma space_PiF: "space (PiF I M) = (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
unfolding PiF_def using PiF_gen_subset by (rule space_measure_of)
@@ -757,7 +757,7 @@
done
qed
also have "\<dots> \<in> sets (PiF I M)"
-    apply (intro Int countable_nat_UN subsetI, safe)
+    apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
apply (case_tac "set (from_nat i) \<in> I")
apply simp_all
apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]])
@@ -807,7 +807,7 @@
case (Union a)
have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
by simp
-  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro countable_nat_UN) auto
+  also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto
finally show ?case .
next
case (Compl a)
@@ -838,10 +838,10 @@
show "(\<lambda>x. finmap_of (J x) (f x)) -` Pi' K S \<inter> space N \<in> sets N"
unfolding eq r
apply (simp del: INT_simps add: )
-    apply (intro conjI impI finite_INT JN Int[OF top])
+    apply (intro conjI impI sets.finite_INT JN sets.Int[OF sets.top])
apply simp apply assumption
apply (subst Int_assoc[symmetric])
-    apply (rule Int)
+    apply (rule sets.Int)
apply (intro measurable_sets[OF f] *) apply force apply assumption
apply (intro JN)
done
@@ -865,7 +865,7 @@
assume "i \<in> I"
hence "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space (PiF {I} M) =
Pi' I (\<lambda>x. if x = i then A else space (M x))"
-    using sets_into_space[OF ] `A \<in> sets (M i)` assms
+    using sets.sets_into_space[OF ] `A \<in> sets (M i)` assms
by (auto simp: space_PiF Pi'_def)
thus ?thesis  using assms `A \<in> sets (M i)`
by (intro in_sets_PiFI) auto
@@ -934,7 +934,7 @@
shows "A \<inter> B \<in> sets M" using assms
proof -
have "A \<inter> B = (A \<inter> space M) \<inter> B"
-    using assms sets_into_space by auto
+    using assms sets.sets_into_space by auto
thus ?thesis using assms by auto
qed

@@ -959,7 +959,7 @@
show "A \<in> sigma_sets ?\<Omega> ?R"
proof -
from `I \<noteq> {}` X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})"
-      using sets_into_space
+      using sets.sets_into_space
by (auto simp: space_PiF product_def) blast
also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
using X `I \<noteq> {}` assms by (intro R.finite_INT) (auto simp: space_PiF)
@@ -970,7 +970,7 @@
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)"
by auto
then have "A = (\<Pi>' j \<in> I. if j = i then B else space (M j))"
-    using sets_into_space[OF A(3)]
+    using sets.sets_into_space[OF A(3)]
apply (auto simp: Pi'_iff split: split_if_asm)
apply blast
done
@@ -1033,7 +1033,7 @@
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)}"
using sets_PiF_single[of I M] by (simp add: space_P)
also have "\<dots> \<subseteq> sets (sigma (space (PiF {I} M)) P)"
-  proof (safe intro!: sigma_sets_subset)
+  proof (safe intro!: sets.sigma_sets_subset)
fix i A assume "i \<in> I" and A: "A \<in> sets (M i)"
have "(\<lambda>x. (x)\<^isub>F i) \<in> measurable ?P (sigma (space (M i)) (E i))"
proof (subst measurable_iff_measure_of)
@@ -1051,7 +1051,7 @@
using S_mono
by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
also have "\<dots> \<in> sets ?P"
-        proof (safe intro!: countable_UN)
+        proof (safe intro!: sets.countable_UN)
fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
using A S_in_E
by (simp add: P_closed)
@@ -1072,7 +1072,7 @@
by (simp add: P_closed)
show "sigma_sets (space (PiF {I} M)) P \<subseteq> sets (PiF {I} M)"
using `finite I` `I \<noteq> {}`
-    by (auto intro!: sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
+    by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
qed

lemma enumerable_sigma_fprod_algebra_sigma_eq:
@@ -1176,7 +1176,7 @@
show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
proof
fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
-      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets_into_space)
+      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
have "x = \<Union>{?x J |J. finite J}" by auto
also have "\<dots> \<in> sets borel"
@@ -1316,7 +1316,7 @@
have "mf (fm x) \<in> extensional J"
by (auto simp: mf_def extensional_def compose_def)
moreover
-  have "x \<in> extensional J" using assms sets_into_space
+  have "x \<in> extensional J" using assms sets.sets_into_space
by (force simp: space_PiM PiE_def)
moreover
{ fix i assume "i \<in> J"
@@ -1344,7 +1344,7 @@
have "fm ` X = (mf) -` X \<inter> space (PiF {f ` J} (\<lambda>_. M))"
proof safe
fix x assume "x \<in> X"
-    with mf_fm[of x] sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
+    with mf_fm[of x] sets.sets_into_space[OF assms(2)] show "fm x \<in> mf -` X" by auto
show "fm x \<in> space (PiF {f ` J} (\<lambda>_. M))" by (simp add: space_PiF assms)
next
fix y x
@@ -1396,7 +1396,7 @@
shows "emeasure M X = emeasure (mapmeasure M (\<lambda>_. N)) (fm ` X)"
unfolding mapmeasure_def
proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
-  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets_into_space)
+  have "X \<subseteq> space (Pi\<^isub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
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"
by (auto simp: vimage_image_eq inj_on_def)
thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1```