diff -r 0d97ef1d6de9 -r de72bbe42190 src/HOL/Probability/Fin_Map.thy
--- 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: "{(\' j\J. X j) |X J. J \ I \ X \ (\ j\J. sets (M j))} \
Pow (\J \ I. (\' j\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) = (\J \ I. (\' j\J. space (M j)))"
unfolding PiF_def using PiF_gen_subset by (rule space_measure_of)
@@ -757,7 +757,7 @@
done
qed
also have "\ \ 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) \ 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 \ {m. domain m \ J} = (\i. (a i \ {m. domain m \ J}))"
by simp
- also have "\ \ sets (PiF J M)" using Union by (intro countable_nat_UN) auto
+ also have "\ \ 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 "(\x. finmap_of (J x) (f x)) -` Pi' K S \ space N \ 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 \ I"
hence "(\x. (x)\<^isub>F i) -` A \ space (PiF {I} M) =
Pi' I (\x. if x = i then A else space (M x))"
- using sets_into_space[OF ] `A \ sets (M i)` assms
+ using sets.sets_into_space[OF ] `A \ sets (M i)` assms
by (auto simp: space_PiF Pi'_def)
thus ?thesis using assms `A \ sets (M i)`
by (intro in_sets_PiFI) auto
@@ -934,7 +934,7 @@
shows "A \ B \ sets M" using assms
proof -
have "A \ B = (A \ space M) \ 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 \ sigma_sets ?\ ?R"
proof -
from `I \ {}` X have "A = (\j\I. {f\space (PiF {I} M). f j \ X j})"
- using sets_into_space
+ using sets.sets_into_space
by (auto simp: space_PiF product_def) blast
also have "\ \ sigma_sets ?\ ?R"
using X `I \ {}` assms by (intro R.finite_INT) (auto simp: space_PiF)
@@ -970,7 +970,7 @@
then obtain i B where A: "A = {f\\' i\I. space (M i). f i \ B}" "i \ I" "B \ sets (M i)"
by auto
then have "A = (\' j \ 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 \ \' i\I. space (M i). f i \ A} |i A. i \ I \ A \ sets (M i)}"
using sets_PiF_single[of I M] by (simp add: space_P)
also have "\ \ 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 \ I" and A: "A \ sets (M i)"
have "(\x. (x)\<^isub>F i) \ 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 "\ \ sets ?P"
- proof (safe intro!: countable_UN)
+ proof (safe intro!: sets.countable_UN)
fix n show "(\' j\I. if i = j then A else S j n) \ 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 \ sets (PiF {I} M)"
using `finite I` `I \ {}`
- 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) (\_. borel)) \ sets (borel::('i \\<^isub>F 'a) measure)"
proof
fix x assume x: "x \ sets (PiF (Collect finite::'i set set) (\_. borel::'a measure))"
- hence x_sp: "x \ space (PiF (Collect finite) (\_. borel))" by (rule sets_into_space)
+ hence x_sp: "x \ space (PiF (Collect finite) (\_. borel))" by (rule sets.sets_into_space)
let ?x = "\J. x \ {x. domain x = J}"
have "x = \{?x J |J. finite J}" by auto
also have "\ \ sets borel"
@@ -1316,7 +1316,7 @@
have "mf (fm x) \ extensional J"
by (auto simp: mf_def extensional_def compose_def)
moreover
- have "x \ extensional J" using assms sets_into_space
+ have "x \ extensional J" using assms sets.sets_into_space
by (force simp: space_PiM PiE_def)
moreover
{ fix i assume "i \ J"
@@ -1344,7 +1344,7 @@
have "fm ` X = (mf) -` X \ space (PiF {f ` J} (\_. M))"
proof safe
fix x assume "x \ X"
- with mf_fm[of x] sets_into_space[OF assms(2)] show "fm x \ mf -` X" by auto
+ with mf_fm[of x] sets.sets_into_space[OF assms(2)] show "fm x \ mf -` X" by auto
show "fm x \ space (PiF {f ` J} (\_. M))" by (simp add: space_PiF assms)
next
fix y x
@@ -1396,7 +1396,7 @@
shows "emeasure M X = emeasure (mapmeasure M (\_. N)) (fm ` X)"
unfolding mapmeasure_def
proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
- have "X \ space (Pi\<^isub>M J (\_. N))" using assms by (simp add: sets_into_space)
+ have "X \ space (Pi\<^isub>M J (\_. N))" using assms by (simp add: sets.sets_into_space)
from assms inj_on_fm[of "\_. N"] set_mp[OF this] have "fm -` fm ` X \ space (Pi\<^isub>M J (\_. N)) = X"
by (auto simp: vimage_image_eq inj_on_def)
thus "emeasure M X = emeasure M (fm -` fm ` X \ space M)" using s1