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