--- a/src/HOL/Probability/Binary_Product_Measure.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Nov 27 11:29:47 2012 +0100
@@ -22,7 +22,7 @@
(\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)"
- using space_closed[of A] space_closed[of B] by auto
+ using sets.space_closed[of A] sets.space_closed[of B] by auto
lemma space_pair_measure:
"space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
@@ -47,7 +47,7 @@
assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M"
shows "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2)"
unfolding pair_measure_def using 1 2
- by (intro measurable_measure_of) (auto dest: sets_into_space)
+ by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
lemma measurable_split_replace[measurable (raw)]:
"(\<lambda>x. f x (fst (g x)) (snd (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. split (f x) (g x)) \<in> measurable M N"
@@ -63,7 +63,7 @@
have "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
by auto
also have "\<dots> \<in> sets M"
- by (rule Int) (auto intro!: measurable_sets * f g)
+ by (rule sets.Int) (auto intro!: measurable_sets * f g)
finally show "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
qed
@@ -79,10 +79,12 @@
using measurable_Pair[OF assms] by simp
lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^isub>M M2) M1"
- by (auto simp: fst_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
+ by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+ measurable_def)
lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^isub>M M2) M2"
- by (auto simp: snd_vimage_eq_Times space_pair_measure sets_into_space times_Int_times measurable_def)
+ by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+ measurable_def)
lemma
assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^isub>M P)"
@@ -122,7 +124,7 @@
assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "Pair x -` A \<in> sets M2"
proof -
have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
- using A[THEN sets_into_space] by (auto simp: space_pair_measure)
+ using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
also have "\<dots> \<in> sets M2"
using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: split_if_asm)
finally show ?thesis .
@@ -134,7 +136,7 @@
lemma sets_Pair2: assumes A: "A \<in> sets (M1 \<Otimes>\<^isub>M M2)" shows "(\<lambda>x. (x, y)) -` A \<in> sets M1"
proof -
have "(\<lambda>x. (x, y)) -` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) -` A \<inter> space M1 else {})"
- using A[THEN sets_into_space] by (auto simp: space_pair_measure)
+ using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
also have "\<dots> \<in> sets M1"
using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: split_if_asm)
finally show ?thesis .
@@ -167,11 +169,11 @@
unfolding sets_pair_measure
proof (induct rule: sigma_sets_induct_disjoint)
case (compl A)
- with sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
+ with sets.sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
(if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
unfolding sets_pair_measure[symmetric]
by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
- with compl top show ?case
+ with compl sets.top show ?case
by (auto intro!: measurable_If simp: space_pair_measure)
next
case (union F)
@@ -189,7 +191,7 @@
let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
{ fix i
have [simp]: "space N \<times> F i \<inter> space N \<times> space M = space N \<times> F i"
- using F sets_into_space by auto
+ using F sets.sets_into_space by auto
let ?R = "density M (indicator (F i))"
have "finite_measure ?R"
using F by (intro finite_measureI) (auto simp: emeasure_restricted subset_eq)
@@ -199,7 +201,7 @@
= emeasure M (F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q))"
using Q F_sets by (intro emeasure_restricted) (auto intro: sets_Pair1)
moreover have "\<And>x. F i \<inter> Pair x -` (space N \<times> space ?R \<inter> Q) = ?C x i"
- using sets_into_space[OF Q] by (auto simp: space_pair_measure)
+ using sets.sets_into_space[OF Q] by (auto simp: space_pair_measure)
ultimately have "(\<lambda>x. emeasure M (?C x i)) \<in> borel_measurable N"
by simp }
moreover
@@ -213,7 +215,7 @@
by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
qed
also have "(\<Union>i. ?C x i) = Pair x -` Q"
- using F sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
+ using F sets.sets_into_space[OF `Q \<in> sets (N \<Otimes>\<^isub>M M)`]
by (auto simp: space_pair_measure)
finally have "emeasure M (Pair x -` Q) = (\<Sum>i. emeasure M (?C x i))"
by simp }
@@ -255,7 +257,7 @@
intro!: positive_integral_cong positive_integral_indicator[symmetric])
qed
show "{a \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"
- using space_closed[of N] space_closed[of M] by auto
+ using sets.space_closed[of N] sets.space_closed[of M] by auto
qed fact
lemma (in sigma_finite_measure) emeasure_pair_measure_alt:
@@ -296,7 +298,7 @@
using Q measurable_pair_swap' by (auto intro: measurable_sets)
note M1.measurable_emeasure_Pair[OF this]
moreover have "\<And>y. Pair y -` ((\<lambda>(x, y). (y, x)) -` Q \<inter> space (M2 \<Otimes>\<^isub>M M1)) = (\<lambda>x. (x, y)) -` Q"
- using Q[THEN sets_into_space] by (auto simp: space_pair_measure)
+ using Q[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
ultimately show ?thesis by simp
qed
@@ -374,7 +376,7 @@
show ?thesis
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
show "?E \<subseteq> Pow (space ?P)"
- using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
+ using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)
show "sets ?P = sigma_sets (space ?P) ?E"
by (simp add: sets_pair_measure space_pair_measure)
then show "sets ?D = sigma_sets (space ?P) ?E"
@@ -386,7 +388,7 @@
fix X assume "X \<in> ?E"
then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
have "(\<lambda>(y, x). (x, y)) -` X \<inter> space (M2 \<Otimes>\<^isub>M M1) = B \<times> A"
- using sets_into_space[OF A] sets_into_space[OF B] by (auto simp: space_pair_measure)
+ using sets.sets_into_space[OF A] sets.sets_into_space[OF B] by (auto simp: space_pair_measure)
with A B show "emeasure (M1 \<Otimes>\<^isub>M M2) X = emeasure ?D X"
by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_pair_measure_Times emeasure_distr
measurable_pair_swap' ac_simps)
@@ -399,7 +401,7 @@
(is "_ = ?\<nu> A")
proof -
have [simp]: "\<And>y. (Pair y -` ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))) = (\<lambda>x. (x, y)) -` A"
- using sets_into_space[OF A] by (auto simp: space_pair_measure)
+ using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
show ?thesis using A
by (subst distr_pair_swap)
(simp_all del: vimage_Int add: measurable_sets[OF measurable_pair_swap']
@@ -438,7 +440,7 @@
shows "AE x in M1 \<Otimes>\<^isub>M M2. P x"
proof (subst AE_iff_measurable[OF _ refl])
show "{x\<in>space (M1 \<Otimes>\<^isub>M M2). \<not> P x} \<in> sets (M1 \<Otimes>\<^isub>M M2)"
- by (rule sets_Collect) fact
+ by (rule sets.sets_Collect) fact
then have "emeasure (M1 \<Otimes>\<^isub>M M2) {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} =
(\<integral>\<^isup>+ x. \<integral>\<^isup>+ y. indicator {x \<in> space (M1 \<Otimes>\<^isub>M M2). \<not> P x} (x, y) \<partial>M2 \<partial>M1)"
by (simp add: M2.emeasure_pair_measure)
@@ -790,7 +792,7 @@
show ?thesis
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
show "?E \<subseteq> Pow (space ?P)"
- using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
+ using sets.space_closed[of M1] sets.space_closed[of M2] by (auto simp: space_pair_measure)
show "sets ?P = sigma_sets (space ?P) ?E"
by (simp add: sets_pair_measure space_pair_measure)
then show "sets M = sigma_sets (space ?P) ?E"
--- a/src/HOL/Probability/Borel_Space.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Nov 27 11:29:47 2012 +0100
@@ -53,7 +53,7 @@
lemma borel_singleton[measurable]:
"A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
- unfolding insert_def by (rule Un) auto
+ unfolding insert_def by (rule sets.Un) auto
lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
unfolding Compl_eq_Diff_UNIV by simp
@@ -180,7 +180,7 @@
lemma borel_sigma_sets_subset:
"A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
- using sigma_sets_subset[of A borel] by simp
+ using sets.sigma_sets_subset[of A borel] by simp
lemma borel_eq_sigmaI1:
fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
@@ -276,7 +276,8 @@
by blast
show "S \<in> ?SIGMA"
unfolding *
- by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace)
+ by (safe intro!: sets.countable_UN sets.Int sets.countable_INT)
+ (auto intro!: halfspace_gt_in_halfspace)
qed auto
lemma borel_eq_halfspace_le:
@@ -299,7 +300,7 @@
finally show "x$$i < a" .
qed
show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
- by (safe intro!: countable_UN) auto
+ by (safe intro!: sets.countable_UN) auto
qed auto
lemma borel_eq_halfspace_ge:
@@ -308,7 +309,7 @@
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
- by (safe intro!: compl_sets) auto
+ by (safe intro!: sets.compl_sets) auto
qed auto
lemma borel_eq_halfspace_greater:
@@ -317,7 +318,7 @@
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
- by (safe intro!: compl_sets) auto
+ by (safe intro!: sets.compl_sets) auto
qed auto
lemma borel_eq_atMost:
@@ -337,7 +338,7 @@
by (auto intro!: exI[of _ k])
qed
show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
- by (safe intro!: countable_UN) auto
+ by (safe intro!: sets.countable_UN) auto
qed (auto intro: sigma_sets_top sigma_sets.Empty)
qed auto
@@ -363,7 +364,7 @@
qed
finally show "{x. x$$i \<le> a} \<in> ?SIGMA"
apply (simp only:)
- apply (safe intro!: countable_UN Diff)
+ apply (safe intro!: sets.countable_UN sets.Diff)
apply (auto intro: sigma_sets_top)
done
qed (auto intro: sigma_sets_top sigma_sets.Empty)
@@ -391,7 +392,7 @@
qed
finally show "{x. a \<le> x$$i} \<in> ?SIGMA"
apply (simp only:)
- apply (safe intro!: countable_UN Diff)
+ apply (safe intro!: sets.countable_UN sets.Diff)
apply (auto intro: sigma_sets_top)
done
qed (auto intro: sigma_sets_top sigma_sets.Empty)
@@ -415,7 +416,7 @@
by (auto intro!: exI[of _ k])
qed
show "{..a} \<in> ?SIGMA" unfolding *
- by (safe intro!: countable_UN)
+ by (safe intro!: sets.countable_UN)
(auto intro!: sigma_sets_top)
qed auto
@@ -427,7 +428,7 @@
then have "open M" by simp
show "M \<in> ?SIGMA"
apply (subst open_UNION[OF `open M`])
- apply (safe intro!: countable_UN)
+ apply (safe intro!: sets.countable_UN)
apply auto
done
qed auto
--- a/src/HOL/Probability/Complete_Measure.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Tue Nov 27 11:29:47 2012 +0100
@@ -22,7 +22,7 @@
lemma completion_into_space:
"{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
- using sets_into_space by auto
+ using sets.sets_into_space by auto
lemma space_completion[simp]: "space (completion M) = space M"
unfolding completion_def using space_measure_of[OF completion_into_space] by simp
@@ -43,7 +43,7 @@
unfolding sigma_algebra_iff2
proof (intro conjI ballI allI impI)
show "?A \<subseteq> Pow (space M)"
- using sets_into_space by auto
+ using sets.sets_into_space by auto
next
show "{} \<in> ?A" by auto
next
@@ -238,7 +238,7 @@
(if x \<in> ?N then ?F undefined \<union> ?N
else if f x = undefined then ?F (f x) \<union> ?N
else ?F (f x) - ?N)"
- using N(2) sets_into_space by (auto split: split_if_asm simp: null_sets_def)
+ using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def)
moreover { fix y have "?F y \<union> ?N \<in> sets M"
proof cases
assume y: "y \<in> f`space M"
--- 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
--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Nov 27 11:29:47 2012 +0100
@@ -140,7 +140,7 @@
lemma prod_emb_Pi:
assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
shows "prod_emb K M J (Pi\<^isub>E J X) = (\<Pi>\<^isub>E i\<in>K. if i \<in> J then X i else space (M i))"
- using assms space_closed
+ using assms sets.space_closed
by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
lemma prod_emb_id:
@@ -190,14 +190,14 @@
by (auto simp: prod_algebra_def)
let ?A = "\<Pi>\<^isub>E i\<in>I. if i \<in> J then E i else space (M i)"
have A: "A = ?A"
- unfolding A using J by (intro prod_emb_PiE sets_into_space) auto
- show "A \<in> ?R" unfolding A using J top
+ unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
+ show "A \<in> ?R" unfolding A using J sets.top
by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
next
fix A assume "A \<in> ?R"
then obtain X where A: "A = (\<Pi>\<^isub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
then have A: "A = prod_emb I M I (\<Pi>\<^isub>E i\<in>I. X i)"
- by (simp add: prod_emb_PiE_same_index[OF sets_into_space] Pi_iff)
+ by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
from X I show "A \<in> ?L" unfolding A
by (auto simp: prod_algebra_def)
qed
@@ -209,7 +209,7 @@
lemma prod_algebraI_finite:
"finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^isub>E I E) \<in> prod_algebra I M"
- using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets_into_space] by simp
+ using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
lemma Int_stable_PiE: "Int_stable {Pi\<^isub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
proof (safe intro!: Int_stableI)
@@ -232,11 +232,11 @@
and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
by (auto simp: prod_algebra_def)
from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
- using sets_into_space by auto
+ using sets.sets_into_space by auto
then have "A = (\<Pi>\<^isub>E i\<in>I. if i\<in>J then E i else space (M i))"
using A J by (auto simp: prod_emb_PiE)
moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
- using top E by auto
+ using sets.top E by auto
ultimately show ?thesis using that by auto
qed
@@ -248,7 +248,8 @@
from prod_algebraE[OF this] guess K F . note B = this
have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^isub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter>
(if i \<in> K then F i else space (M i)))"
- unfolding A B using A(2,3,4) A(5)[THEN sets_into_space] B(2,3,4) B(5)[THEN sets_into_space]
+ unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
+ B(5)[THEN sets.sets_into_space]
apply (subst (1 2 3) prod_emb_PiE)
apply (simp_all add: subset_eq PiE_Int)
apply blast
@@ -418,14 +419,14 @@
lemma sets_PiM_I_finite[measurable]:
assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
- using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
+ using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] `finite I` sets by auto
lemma measurable_component_singleton:
assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
proof (unfold measurable_def, intro CollectI conjI ballI)
fix A assume "A \<in> sets (M i)"
then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = prod_emb I M {i} (\<Pi>\<^isub>E j\<in>{i}. A)"
- using sets_into_space `i \<in> I`
+ using sets.sets_into_space `i \<in> I`
by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
@@ -460,7 +461,7 @@
fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
(if j = i then space (Pi\<^isub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
- using sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
+ using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
also have "\<dots> \<in> sets ?P"
using A j
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
@@ -560,7 +561,7 @@
fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
next
fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
- by (auto simp: PiE_def dest!: sets_into_space)
+ by (auto simp: PiE_def dest!: sets.sets_into_space)
next
fix f assume "f \<in> space (PiM I M)"
with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
@@ -584,7 +585,7 @@
show "positive (PiM {} M) ?\<mu>"
by (auto simp: positive_def)
show "countably_additive (PiM {} M) ?\<mu>"
- by (rule countably_additiveI_finite)
+ by (rule sets.countably_additiveI_finite)
(auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
qed (auto simp: prod_emb_def)
also have "(prod_emb {} M {} (\<Pi>\<^isub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
@@ -621,13 +622,13 @@
emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i))"
by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
also have "?h -` ?p \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
- using J E[rule_format, THEN sets_into_space]
+ using J E[rule_format, THEN sets.sets_into_space]
by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
also have "emeasure (Pi\<^isub>M I M \<Otimes>\<^isub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
emeasure (Pi\<^isub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
also have "?p' = (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
- using J E[rule_format, THEN sets_into_space]
+ using J E[rule_format, THEN sets.sets_into_space]
by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
also have "emeasure (Pi\<^isub>M I M) (\<Pi>\<^isub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
(\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
@@ -640,7 +641,7 @@
finally show "?\<mu> ?p = \<dots>" .
show "prod_emb (insert i I) M J (Pi\<^isub>E J E) \<in> Pow (\<Pi>\<^isub>E i\<in>insert i I. space (M i))"
- using J E[rule_format, THEN sets_into_space] by (auto simp: prod_emb_iff PiE_def)
+ using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
next
show "positive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^isub>M (insert i I) M)) ?\<mu>"
using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
@@ -650,7 +651,7 @@
using insert by auto
qed (auto intro!: setprod_cong)
with insert show ?case
- by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets_into_space)
+ by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
qed simp
lemma (in product_sigma_finite) sigma_finite:
@@ -750,7 +751,7 @@
let ?B = "Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M"
let ?X = "?g -` A \<inter> space ?B"
have "Pi\<^isub>E I F \<subseteq> space (Pi\<^isub>M I M)" "Pi\<^isub>E J F \<subseteq> space (Pi\<^isub>M J M)"
- using F[rule_format, THEN sets_into_space] by (force simp: space_PiM)+
+ using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+
then have X: "?X = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
have "emeasure ?D A = emeasure ?B ?X"
@@ -792,7 +793,7 @@
interpret I: finite_product_sigma_finite M "{i}" by default simp
fix A assume A: "A \<in> sets (M i)"
moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M {i} M) = (\<Pi>\<^isub>E i\<in>{i}. A)"
- using sets_into_space by (auto simp: space_PiM)
+ using sets.sets_into_space by (auto simp: space_PiM)
ultimately show "emeasure (M i) A = emeasure ?D A"
using A I.measure_times[of "\<lambda>_. A"]
by (simp add: emeasure_distr measurable_component_singleton)
@@ -846,7 +847,7 @@
have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
using insert by (auto intro!: setprod_cong)
have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^isub>M J M)"
- using sets_into_space insert
+ using sets.sets_into_space insert
by (intro borel_measurable_ereal_setprod
measurable_comp[OF measurable_component_singleton, unfolded comp_def])
auto
@@ -1036,7 +1037,7 @@
sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
using sets_PiM_single[of I M] by (simp add: space_P)
also have "\<dots> \<subseteq> sets (sigma (space (PiM 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)"
then have "(\<lambda>x. x i) \<in> measurable ?P (sigma (space (M i)) (E i))"
apply (subst measurable_iff_measure_of)
@@ -1059,7 +1060,7 @@
by (simp add: P_closed)
show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
unfolding P_def space_PiM[symmetric]
- by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
+ by (intro sets.sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
qed
lemma sigma_prod_algebra_sigma_eq:
@@ -1084,7 +1085,7 @@
sigma_sets (space ?P) {{f \<in> \<Pi>\<^isub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
using sets_PiM_single[of I M] by (simp add: space_P)
also have "\<dots> \<subseteq> sets (sigma (space (PiM 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 i) \<in> measurable ?P (sigma (space (M i)) (E i))"
proof (subst measurable_iff_measure_of)
@@ -1104,7 +1105,7 @@
apply (auto simp: bij_betw_def)
done
also have "\<dots> \<in> sets ?P"
- proof (safe intro!: countable_UN)
+ proof (safe intro!: sets.countable_UN)
fix xs show "(\<Pi>\<^isub>E j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
using A S_in_E
by (simp add: P_closed)
@@ -1125,7 +1126,7 @@
by (simp add: P_closed)
show "sigma_sets (space (PiM I M)) P \<subseteq> sets (PiM I M)"
using `finite I`
- by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
+ by (auto intro!: sets.sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
qed
lemma pair_measure_eq_distr_PiM:
@@ -1146,7 +1147,7 @@
also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
using A B by (subst B.emeasure_PiM) (auto split: bool.split)
also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
- using A[THEN sets_into_space] B[THEN sets_into_space]
+ using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
using A B
--- a/src/HOL/Probability/Independent_Family.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Tue Nov 27 11:29:47 2012 +0100
@@ -186,11 +186,11 @@
using G by auto
have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
- using A_sets sets_into_space[of _ M] X `J \<noteq> {}`
+ using A_sets sets.sets_into_space[of _ M] X `J \<noteq> {}`
by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
- using J `J \<noteq> {}` `j \<notin> J` A_sets X sets_into_space
- by (auto intro!: finite_measure_Diff finite_INT split: split_if_asm)
+ using J `J \<noteq> {}` `j \<notin> J` A_sets X sets.sets_into_space
+ by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
moreover {
@@ -224,7 +224,7 @@
show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
using disj by (rule disjoint_family_on_bisimulation) auto
show "range (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i) \<subseteq> events"
- using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: Int)
+ using A_sets F `finite J` `J \<noteq> {}` `j \<notin> J` by (auto intro!: sets.Int)
qed
moreover { fix k
from J A `j \<in> K` have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
@@ -243,7 +243,7 @@
show "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. F k) * (\<Prod>j\<in>J. prob (A j))"
by (auto dest!: sums_unique)
qed (insert F, auto)
- qed (insert sets_into_space, auto)
+ qed (insert sets.sets_into_space, auto)
then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
proof (rule dynkin_system.dynkin_subset, safe)
fix X assume "X \<in> G j"
@@ -291,7 +291,7 @@
proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
fix i assume "i \<in> I"
with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
- with sets_into_space show "F i \<subseteq> Pow (space M)" by auto
+ with sets.sets_into_space show "F i \<subseteq> Pow (space M)" by auto
qed
qed
@@ -394,7 +394,7 @@
let ?S = "sigma_sets (space M) (\<Union>i\<in>I j. E i)"
assume "j \<in> J"
from E[OF this] interpret S: sigma_algebra "space M" ?S
- using sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
+ using sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)"
proof (rule sigma_sets_eqI)
@@ -416,7 +416,7 @@
proof (rule indep_sets_sigma)
show "indep_sets ?E J"
proof (intro indep_setsI)
- fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force intro!: finite_INT)
+ fix j assume "j \<in> J" with E show "?E j \<subseteq> events" by (force intro!: sets.finite_INT)
next
fix K A assume K: "K \<noteq> {}" "K \<subseteq> J" "finite K"
and "\<forall>j\<in>K. A j \<in> ?E j"
@@ -533,7 +533,7 @@
interpret D: dynkin_system "space M" ?D
proof (rule dynkin_systemI)
fix D assume "D \<in> ?D" then show "D \<subseteq> space M"
- using sets_into_space by auto
+ using sets.sets_into_space by auto
next
show "space M \<in> ?D"
using prob_space `X \<subseteq> space M` by (simp add: Int_absorb2)
@@ -546,7 +546,7 @@
also have "\<dots> = prob X * prob (space M) - prob X * prob A"
using A prob_space by auto
also have "\<dots> = prob X * prob (space M - A)"
- using X_in A sets_into_space
+ using X_in A sets.sets_into_space
by (subst finite_measure_Diff) (auto simp: field_simps)
finally show "space M - A \<in> ?D"
using A `X \<subseteq> space M` by auto
@@ -611,14 +611,14 @@
proof (rule sigma_eq_dynkin)
{ fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
then have "B \<subseteq> space M"
- by induct (insert A sets_into_space[of _ M], auto) }
+ by induct (insert A sets.sets_into_space[of _ M], auto) }
then show "?A \<subseteq> Pow (space M)" by auto
show "Int_stable ?A"
proof (rule Int_stableI)
fix a assume "a \<in> ?A" then guess n .. note a = this
fix b assume "b \<in> ?A" then guess m .. note b = this
interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
- using A sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
+ using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
by (intro sigma_sets_subseteq UN_mono) auto
with a have "a \<in> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)" by auto
@@ -644,7 +644,7 @@
have F1: "range F \<subseteq> events"
using F2 by (simp add: indep_events_def subset_eq)
{ fix i show "sigma_algebra (space M) (sigma_sets (space M) {F i})"
- using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets_into_space
+ using sigma_algebra_sigma_sets[of "{F i}" "space M"] F1 sets.sets_into_space
by auto }
show "indep_sets (\<lambda>i. sigma_sets (space M) {F i}) UNIV"
proof (rule indep_sets_sigma)
@@ -659,12 +659,12 @@
proof
fix j
interpret S: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
- using order_trans[OF F1 space_closed]
+ using order_trans[OF F1 sets.space_closed]
by (intro sigma_algebra_sigma_sets) (simp add: sigma_sets_singleton subset_eq)
have "(\<Inter>n. ?Q n) = (\<Inter>n\<in>{j..}. ?Q n)"
by (intro decseq_SucI INT_decseq_offset UN_mono) auto
also have "\<dots> \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
- using order_trans[OF F1 space_closed]
+ using order_trans[OF F1 sets.space_closed]
by (safe intro!: S.countable_INT S.countable_UN)
(auto simp: sigma_sets_singleton intro!: sigma_sets.Basic bexI)
finally show "(\<Inter>n. ?Q n) \<in> sigma_sets (space M) (\<Union>i\<in>{j..}. sigma_sets (space M) {F i})"
@@ -688,7 +688,7 @@
assume A: "\<forall>j\<in>J. A j \<in> F j"
let ?A = "\<lambda>j. if j \<in> J then A j else space M"
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
- using subset_trans[OF F(1) space_closed] J A
+ using subset_trans[OF F(1) sets.space_closed] J A
by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
also
from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
@@ -882,7 +882,7 @@
show "indep_vars M' X I" unfolding indep_vars_def
proof (intro conjI indep_setsI ballI rv)
fix i show "sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)} \<subseteq> events"
- by (auto intro!: sigma_sets_subset measurable_sets rv)
+ by (auto intro!: sets.sigma_sets_subset measurable_sets rv)
next
fix J Y' assume J: "J \<noteq> {}" "J \<subseteq> I" "finite J"
assume Y': "\<forall>j\<in>J. Y' j \<in> sigma_sets (space M) {X j -` A \<inter> space M |A. A \<in> sets (M' j)}"
@@ -892,7 +892,7 @@
from Y'[rule_format, OF this] rv[of j]
show "\<exists>Y. Y' j = X j -` Y \<inter> space M \<and> Y \<in> sets (M' j)"
by (subst (asm) sigma_sets_vimage_commute[symmetric, of _ _ "space (M' j)"])
- (auto dest: measurable_space simp: sigma_sets_eq)
+ (auto dest: measurable_space simp: sets.sigma_sets_eq)
qed
from bchoice[OF this] obtain Y where
Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Nov 27 11:29:47 2012 +0100
@@ -311,7 +311,7 @@
next
fix J X assume J: "(J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))"
then show "emb I J (Pi\<^isub>E J X) \<in> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
- by (auto simp: Pi_iff prod_emb_def dest: sets_into_space)
+ by (auto simp: Pi_iff prod_emb_def dest: sets.sets_into_space)
have "emb I J (Pi\<^isub>E J X) \<in> generator"
using J `I \<noteq> {}` by (intro generatorI') (auto simp: Pi_iff)
then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
@@ -393,7 +393,7 @@
lemma (in finite_product_prob_space) finite_measure_PiM_emb:
"(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^isub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
- using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets_into_space, of I A M]
+ using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
by auto
lemma (in product_prob_space) PiM_component:
@@ -465,7 +465,7 @@
then have *: "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} =
(if j < i then {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> j \<in> A} \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M)
else space (\<Pi>\<^isub>M i\<in>UNIV. M) \<times> {\<omega> \<in> space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> (j - i) \<in> A})"
- by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets_into_space)
+ by (auto simp: space_PiM space_pair_measure comb_seq_def dest: sets.sets_into_space)
show "{\<omega> \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case (comb_seq i) \<omega> j \<in> A} \<in> sets ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
unfolding * by (auto simp: A intro!: sets_Collect_single)
qed
@@ -507,7 +507,7 @@
shows "Pi UNIV E \<in> sets S"
proof -
have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..i}. E j))"
- using E E[THEN sets_into_space]
+ using E E[THEN sets.sets_into_space]
by (auto simp: prod_emb_def Pi_iff extensional_def) blast
with E show ?thesis by auto
qed
@@ -520,7 +520,7 @@
have "\<And>n. (\<Prod>i\<le>n. measure M (E i)) = measure S (?E n)"
using E by (simp add: measure_PiM_emb)
moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
- using E E[THEN sets_into_space]
+ using E E[THEN sets.sets_into_space]
by (auto simp: prod_emb_def extensional_def Pi_iff) blast
moreover have "range ?E \<subseteq> sets S"
using E by auto
@@ -544,7 +544,7 @@
fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
let ?X = "prod_emb ?I ?M J (\<Pi>\<^isub>E j\<in>J. E j)"
have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
- using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
+ using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
with J have "?f -` ?X \<inter> space (S \<Otimes>\<^isub>M S) =
(prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
(prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
@@ -576,7 +576,7 @@
fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
- using J(3)[THEN sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
+ using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
with J have "?f -` ?X \<inter> space (M \<Otimes>\<^isub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
(prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
--- a/src/HOL/Probability/Information.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Information.thy Tue Nov 27 11:29:47 2012 +0100
@@ -183,7 +183,7 @@
proof
assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
then have disj: "AE x in M. D x = 1 \<or> D x = 0"
- using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
+ using D(1) by (auto intro!: AE_I[OF subset_refl] sets.sets_Collect)
have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
using D(1) by auto
@@ -198,7 +198,7 @@
finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
qed
show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
- using D(1) by (auto intro: sets_Collect_conj)
+ using D(1) by (auto intro: sets.sets_Collect_conj)
show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
@@ -383,7 +383,7 @@
interpret sigma_finite_measure T by fact
{ fix A assume "A \<in> sets S" "emeasure S A = 0"
moreover then have "fst -` A \<inter> space (S \<Otimes>\<^isub>M T) = A \<times> space T"
- by (auto simp: space_pair_measure dest!: sets_into_space)
+ by (auto simp: space_pair_measure dest!: sets.sets_into_space)
ultimately have "emeasure (S \<Otimes>\<^isub>M T) (fst -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
by (simp add: emeasure_pair_measure_Times) }
then show ?thesis
@@ -400,7 +400,7 @@
interpret sigma_finite_measure T by fact
{ fix A assume "A \<in> sets T" "emeasure T A = 0"
moreover then have "snd -` A \<inter> space (S \<Otimes>\<^isub>M T) = space S \<times> A"
- by (auto simp: space_pair_measure dest!: sets_into_space)
+ by (auto simp: space_pair_measure dest!: sets.sets_into_space)
ultimately have "emeasure (S \<Otimes>\<^isub>M T) (snd -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
by (simp add: emeasure_pair_measure_Times) }
then show ?thesis
@@ -1571,7 +1571,7 @@
unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
unfolding distributed_distr_eq_density[OF Py]
apply (rule ST.AE_pair_measure)
- apply (auto intro!: sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
+ apply (auto intro!: sets.sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
distributed_real_measurable[OF Pxy] distributed_real_AE[OF Py]
borel_measurable_real_of_ereal measurable_compose[OF _ borel_measurable_RN_deriv_density])
using distributed_RN_deriv[OF Py]
--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Nov 27 11:29:47 2012 +0100
@@ -117,7 +117,7 @@
using assms unfolding simple_function_def
using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
hence "?U \<in> sets M"
- apply (rule finite_UN)
+ apply (rule sets.finite_UN)
using assms unfolding simple_function_def by auto
thus "f -` S \<inter> space M \<in> sets M" unfolding * .
qed
@@ -152,7 +152,7 @@
(\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
using assms unfolding simple_function_def *
- by (rule_tac finite_UN) auto
+ by (rule_tac sets.finite_UN) auto
qed
lemma simple_function_indicator[intro, simp]:
@@ -447,7 +447,7 @@
then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
- using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
+ using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
@@ -637,7 +637,7 @@
using mono by (auto elim!: AE_E)
have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
moreover have "?S x \<in> sets M" using assms
- by (rule_tac Int) (auto intro!: simple_functionD)
+ by (rule_tac sets.Int) (auto intro!: simple_functionD)
ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N"
using `N \<in> sets M` by (auto intro!: emeasure_mono)
moreover have "0 \<le> (emeasure M) (?S x)"
@@ -683,13 +683,13 @@
ultimately show ?thesis by (simp add: simple_integral_def)
next
assume "A \<noteq> space M"
- then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
+ then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
proof safe
fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
next
fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
- using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
+ using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
next
show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
qed
@@ -700,7 +700,7 @@
show "finite (f ` space M \<union> {0})"
using assms(2) unfolding simple_function_def by auto
show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
- using sets_into_space[OF assms(1)] by auto
+ using sets.sets_into_space[OF assms(1)] by auto
have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
by (auto simp: image_iff)
thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
@@ -721,13 +721,13 @@
assumes "A \<in> sets M"
shows "integral\<^isup>S M (indicator A) = emeasure M A"
proof cases
- assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
+ assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto
thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
next
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto
thus ?thesis
using simple_integral_indicator[OF assms simple_function_const[of _ 1]]
- using sets_into_space[OF assms]
+ using sets.sets_into_space[OF assms]
by (auto intro!: arg_cong[where f="(emeasure M)"])
qed
@@ -916,7 +916,7 @@
qed }
note B_mono = this
- note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
+ note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B]
let ?B' = "\<lambda>i n. (u -` {i} \<inter> space M) \<inter> ?B n"
have measure_conv: "\<And>i. (emeasure M) (u -` {i} \<inter> space M) = (SUP n. (emeasure M) (?B' i n))"
@@ -1351,7 +1351,7 @@
also have "\<dots> = (emeasure M) (\<Union>n. ?M n \<inter> ?A)"
proof (safe intro!: SUP_emeasure_incseq)
fix n show "?M n \<inter> ?A \<in> sets M"
- using u by (auto intro!: Int)
+ using u by (auto intro!: sets.Int)
next
show "incseq (\<lambda>n. {x \<in> space M. 1 \<le> real n * u x} \<inter> {x \<in> space M. u x \<noteq> 0})"
proof (safe intro!: incseq_SucI)
@@ -1401,8 +1401,8 @@
lemma AE_iff_positive_integral:
"{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^isup>P M (indicator {x. \<not> P x}) = 0"
- by (subst positive_integral_0_iff_AE)
- (auto simp: one_ereal_def zero_ereal_def sets_Collect_neg indicator_def[abs_def] measurable_If)
+ by (subst positive_integral_0_iff_AE) (auto simp: one_ereal_def zero_ereal_def
+ sets.sets_Collect_neg indicator_def[abs_def] measurable_If)
lemma positive_integral_const_If:
"(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)"
@@ -2463,7 +2463,7 @@
lemma density_cong: "f \<in> borel_measurable M \<Longrightarrow> f' \<in> borel_measurable M \<Longrightarrow>
(AE x in M. f x = f' x) \<Longrightarrow> density M f = density M f'"
- unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE space_closed)
+ unfolding density_def by (auto intro!: measure_of_eq positive_integral_cong_AE sets.space_closed)
lemma density_max_0: "density M f = density M (\<lambda>x. max 0 (f x))"
proof -
@@ -2549,7 +2549,7 @@
by (auto simp: eventually_ae_filter)
then have *: "{x \<in> space (density M f). \<not> P x} \<subseteq> N \<union> {x\<in>space M. \<not> 0 < f x}"
"N \<union> {x\<in>space M. \<not> 0 < f x} \<in> sets M" and ae2: "AE x in M. x \<notin> N"
- using f by (auto simp: subset_eq intro!: sets_Collect_neg AE_not_in)
+ using f by (auto simp: subset_eq intro!: sets.sets_Collect_neg AE_not_in)
show "AE x in density M f. P x"
using ae2
unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f]
@@ -2618,7 +2618,7 @@
also have "\<dots> = (\<integral>\<^isup>+x. indicator (S \<inter> X) x \<partial>M)"
by (auto intro!: positive_integral_cong simp: indicator_def)
also have "\<dots> = emeasure M (S \<inter> X)"
- using S X by (simp add: Int)
+ using S X by (simp add: sets.Int)
finally show ?thesis .
qed
@@ -2651,7 +2651,7 @@
proof (rule measure_eqI)
fix A assume A: "A \<in> sets ?R"
{ fix x assume "x \<in> space M"
- with sets_into_space[OF A]
+ with sets.sets_into_space[OF A]
have "indicator (T' -` A \<inter> space M') (T x) = (indicator A x :: ereal)"
using T inv by (auto simp: indicator_def measurable_space) }
with A T T' f show "emeasure ?R A = emeasure ?L A"
@@ -2777,7 +2777,7 @@
intro!: positive_integral_cong)
also have "\<dots> = emeasure M (A \<inter> B) / emeasure M A"
using A B
- by (subst positive_integral_cmult_indicator) (simp_all add: Int emeasure_nonneg)
+ by (subst positive_integral_cmult_indicator) (simp_all add: sets.Int emeasure_nonneg)
finally show ?thesis .
qed
--- a/src/HOL/Probability/Lebesgue_Measure.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Nov 27 11:29:47 2012 +0100
@@ -217,7 +217,7 @@
have "s \<in> sigma_sets (space lebesgue) (range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)}))"
using assms by (simp add: borel_eq_atLeastAtMost)
also have "\<dots> \<subseteq> sets lebesgue"
- proof (safe intro!: sigma_sets_subset lebesgueI)
+ proof (safe intro!: sets.sigma_sets_subset lebesgueI)
fix n :: nat and a b :: 'a
let ?N = "\<chi>\<chi> i. max (- real n) (a $$ i)"
let ?P = "\<chi>\<chi> i. min (real n) (b $$ i)"
@@ -491,7 +491,7 @@
and sets_lborel[simp]: "sets lborel = sets borel"
and measurable_lborel1[simp]: "measurable lborel = measurable borel"
and measurable_lborel2[simp]: "measurable A lborel = measurable A borel"
- using sigma_sets_eq[of borel]
+ using sets.sigma_sets_eq[of borel]
by (auto simp add: lborel_def measurable_def[abs_def])
lemma emeasure_lborel[simp]: "A \<in> sets borel \<Longrightarrow> emeasure lborel A = emeasure lebesgue A"
--- a/src/HOL/Probability/Measure_Space.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Tue Nov 27 11:29:47 2012 +0100
@@ -449,11 +449,11 @@
lemma suminf_emeasure:
"range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
- using countable_UN[of A UNIV M] emeasure_countably_additive[of M]
+ using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
by (simp add: countably_additive_def)
lemma emeasure_additive: "additive (sets M) (emeasure M)"
- by (metis countably_additive_additive emeasure_positive emeasure_countably_additive)
+ by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)
lemma plus_emeasure:
"a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
@@ -462,16 +462,16 @@
lemma setsum_emeasure:
"F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
(\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
- by (metis additive_sum emeasure_positive emeasure_additive)
+ by (metis sets.additive_sum emeasure_positive emeasure_additive)
lemma emeasure_mono:
"a \<subseteq> b \<Longrightarrow> b \<in> sets M \<Longrightarrow> emeasure M a \<le> emeasure M b"
- by (metis additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
+ by (metis sets.additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets
emeasure_positive increasingD)
lemma emeasure_space:
"emeasure M A \<le> emeasure M (space M)"
- by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets_into_space top)
+ by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets.sets_into_space sets.top)
lemma emeasure_compl:
assumes s: "s \<in> sets M" and fin: "emeasure M s \<noteq> \<infinity>"
@@ -479,7 +479,7 @@
proof -
from s have "0 \<le> emeasure M s" by auto
have "emeasure M (space M) = emeasure M (s \<union> (space M - s))" using s
- by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
+ by (metis Un_Diff_cancel Un_absorb1 s sets.sets_into_space)
also have "... = emeasure M s + emeasure M (space M - s)"
by (rule plus_emeasure[symmetric]) (auto simp add: s)
finally have "emeasure M (space M) = emeasure M s + emeasure M (space M - s)" .
@@ -506,7 +506,8 @@
lemma Lim_emeasure_incseq:
"range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) ----> emeasure M (\<Union>i. A i)"
using emeasure_countably_additive
- by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive)
+ by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
+ emeasure_additive)
lemma incseq_emeasure:
assumes "range B \<subseteq> sets M" "incseq B"
@@ -595,10 +596,10 @@
have "emeasure M (\<Union>i. f i) = emeasure M (\<Union>i. disjointed f i)"
unfolding UN_disjointed_eq ..
also have "\<dots> = (\<Sum>i. emeasure M (disjointed f i))"
- using range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
+ using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
by (simp add: disjoint_family_disjointed comp_def)
also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))"
- using range_disjointed_sets[OF assms] assms
+ using sets.range_disjointed_sets[OF assms] assms
by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset)
finally show ?thesis .
qed
@@ -676,7 +677,8 @@
let ?\<mu> = "emeasure M" and ?\<nu> = "emeasure N"
interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
have "space M = \<Omega>"
- using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
+ using sets.top[of M] sets.space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E`
+ by blast
{ fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
@@ -724,9 +726,9 @@
fix F assume "F \<in> sets M"
let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
- using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
+ using `F \<in> sets M`[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
have [simp, intro]: "\<And>i. ?D i \<in> sets M"
- using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
+ using sets.range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
by (auto simp: subset_eq)
have "disjoint_family ?D"
by (auto simp: disjoint_family_disjointed)
@@ -770,7 +772,7 @@
interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
proof (rule ring_of_setsI)
show "null_sets M \<subseteq> Pow (space M)"
- using sets_into_space by auto
+ using sets.sets_into_space by auto
show "{} \<in> null_sets M"
by auto
fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
@@ -904,7 +906,7 @@
lemma AE_iff_null_sets:
"N \<in> sets M \<Longrightarrow> N \<in> null_sets M \<longleftrightarrow> (AE x in M. x \<notin> N)"
- using Int_absorb1[OF sets_into_space, of N M]
+ using Int_absorb1[OF sets.sets_into_space, of N M]
by (subst AE_iff_null) (auto simp: Int_def[symmetric])
lemma AE_not_in:
@@ -1033,7 +1035,7 @@
have "emeasure M A = emeasure M (A - N)"
using N A by (subst emeasure_Diff_null_set) auto
also have "emeasure M (A - N) \<le> emeasure M (B - N)"
- using N A B sets_into_space by (auto intro!: emeasure_mono)
+ using N A B sets.sets_into_space by (auto intro!: emeasure_mono)
also have "emeasure M (B - N) = emeasure M B"
using N B by (subst emeasure_Diff_null_set) auto
finally show ?thesis .
@@ -1062,7 +1064,7 @@
space: "(\<Union>i. A i) = space M" and
measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
using sigma_finite by auto
- note range' = range_disjointed_sets[OF range] range
+ note range' = sets.range_disjointed_sets[OF range] range
{ fix i
have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
@@ -1400,7 +1402,7 @@
lemma (in finite_measure) finite_measure_compl:
assumes S: "S \<in> sets M"
shows "measure M (space M - S) = measure M (space M) - measure M S"
- using measure_Diff[OF _ top S sets_into_space] S by simp
+ using measure_Diff[OF _ sets.top S sets.sets_into_space] S by simp
lemma (in finite_measure) finite_measure_mono_AE:
assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" and B: "B \<in> sets M"
@@ -1497,7 +1499,7 @@
shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
proof -
have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
- using `e \<in> sets M` sets_into_space upper by blast
+ using `e \<in> sets M` sets.sets_into_space upper by blast
hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
proof (rule finite_measure_finite_Union)
--- a/src/HOL/Probability/Probability_Measure.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Nov 27 11:29:47 2012 +0100
@@ -66,7 +66,7 @@
proof
assume ae: "AE x in M. x \<in> A"
have "{x \<in> space M. x \<in> A} = A" "{x \<in> space M. x \<notin> A} = space M - A"
- using `A \<in> events`[THEN sets_into_space] by auto
+ using `A \<in> events`[THEN sets.sets_into_space] by auto
with AE_E2[OF ae] `A \<in> events` have "1 - emeasure M A = 0"
by (simp add: emeasure_compl emeasure_space_1)
then show "prob A = 1"
@@ -273,7 +273,7 @@
assumes Q: "AE x in M. Q x \<longleftrightarrow> Q' x" "{x\<in>space M. Q x} \<in> events" "{x\<in>space M. Q' x} \<in> events"
shows "cond_prob M P Q = cond_prob M P' Q'"
using P Q
- by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets_Collect_conj)
+ by (auto simp: cond_prob_def intro!: arg_cong2[where f="op /"] prob_eq_AE sets.sets_Collect_conj)
lemma (in prob_space) joint_distribution_Times_le_fst:
@@ -476,7 +476,7 @@
show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
show "?E \<subseteq> Pow (space ?P)"
- using space_closed[of S] space_closed[of T] by (auto simp: space_pair_measure)
+ using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
show "sets ?L = sigma_sets (space ?P) ?E"
by (simp add: sets_pair_measure space_pair_measure)
then show "sets ?R = sigma_sets (space ?P) ?E"
@@ -529,7 +529,7 @@
using Pxy by auto
{ fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
- from sets_into_space[OF A]
+ from sets.sets_into_space[OF A]
have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
@@ -849,7 +849,7 @@
proof
show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
- using sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
+ using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
by (simp add: Int_absorb2 emeasure_nonneg)
qed
--- a/src/HOL/Probability/Projective_Family.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Tue Nov 27 11:29:47 2012 +0100
@@ -25,7 +25,7 @@
show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
using `finite J` by (auto intro!: prod_algebraI_finite)
{ fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
- show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
+ show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets.sets_into_space)
show "sets (\<Pi>\<^isub>M i\<in>J. M i) = sigma_sets ?\<Omega> ?J" "sets ?D = sigma_sets ?\<Omega> ?J"
using `finite J` by (simp_all add: sets_PiM prod_algebra_eq_finite Pi_iff)
@@ -44,7 +44,7 @@
also have "\<dots> = emeasure (Pi\<^isub>M K M) (\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i))"
using E by (simp add: K.measure_times)
also have "(\<Pi>\<^isub>E i\<in>K. if i \<in> J then E i else space (M i)) = (\<lambda>f. restrict f J) -` Pi\<^isub>E J E \<inter> (\<Pi>\<^isub>E i\<in>K. space (M i))"
- using `J \<subseteq> K` sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
+ using `J \<subseteq> K` sets.sets_into_space E by (force simp: Pi_iff PiE_def split: split_if_asm)
finally show "emeasure (Pi\<^isub>M J M) X = emeasure ?D X"
using X `J \<subseteq> K` apply (subst emeasure_distr)
by (auto intro!: measurable_restrict_subset simp: space_PiM)
@@ -93,10 +93,10 @@
shows "emeasure (limP J M P) (Pi\<^isub>E J A) = emeasure (P J) (Pi\<^isub>E J A)"
proof -
have "Pi\<^isub>E J (restrict A J) \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
- using sets_into_space[OF A] by (auto simp: PiE_iff) blast
+ using sets.sets_into_space[OF A] by (auto simp: PiE_iff) blast
hence "emeasure (limP J M P) (Pi\<^isub>E J A) =
emeasure (limP J M P) (prod_emb J M J (Pi\<^isub>E J A))"
- using assms(1-3) sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
+ using assms(1-3) sets.sets_into_space by (auto simp add: prod_emb_id PiE_def Pi_def)
also have "\<dots> = emeasure (P J) (Pi\<^isub>E J A)"
proof (rule emeasure_extend_measure_Pair[OF limP_def])
show "positive (sets (limP J M P)) (P J)" unfolding positive_def by auto
@@ -133,12 +133,12 @@
then obtain E where X: "X = Pi\<^isub>E J E" and E: "\<forall>i\<in>J. E i \<in> sets (M i)" by auto
with `finite J` have "X \<in> sets (limP J M P)" by simp
have emb_self: "prod_emb J M J (Pi\<^isub>E J E) = Pi\<^isub>E J E"
- using E sets_into_space
+ using E sets.sets_into_space
by (auto intro!: prod_emb_PiE_same_index)
show "emeasure (limP J M P) X = emeasure (P J) X"
unfolding X using E
by (intro emeasure_limP assms) simp
-qed (auto simp: Pi_iff dest: sets_into_space intro: Int_stable_PiE)
+qed (auto simp: Pi_iff dest: sets.sets_into_space intro: Int_stable_PiE)
lemma emeasure_fun_emb[simp]:
assumes L: "J \<noteq> {}" "J \<subseteq> L" "finite L" "L \<subseteq> I" and X: "X \<in> sets (PiM J M)"
@@ -155,7 +155,7 @@
shows "X = Y"
proof (rule injective_vimage_restrict)
show "X \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))" "Y \<subseteq> (\<Pi>\<^isub>E i\<in>J. space (M i))"
- using sets[THEN sets_into_space] by (auto simp: space_PiM)
+ using sets[THEN sets.sets_into_space] by (auto simp: space_PiM)
have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
proof
fix i assume "i \<in> L"
@@ -219,7 +219,7 @@
fix A assume "A \<in> prod_algebra I M" with `I \<noteq> {}` show "A \<in> generator"
by (auto intro!: generatorI' sets_PiM_I_finite elim!: prod_algebraE)
qed
- qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset)
+ qed (auto simp: generator_def space_PiM[symmetric] intro!: sets.sigma_sets_subset)
qed
lemma generatorI:
@@ -317,14 +317,14 @@
have JK_disj: "emb (J \<union> K) J X \<inter> emb (J \<union> K) K Y = {}"
apply (rule prod_emb_injective[of "J \<union> K" I])
apply (insert `A \<inter> B = {}` JK J K)
- apply (simp_all add: Int prod_emb_Int)
+ apply (simp_all add: sets.Int prod_emb_Int)
done
have AB: "A = emb I (J \<union> K) (emb (J \<union> K) J X)" "B = emb I (J \<union> K) (emb (J \<union> K) K Y)"
using J K by simp_all
then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
by simp
also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
- using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq Un del: prod_emb_Un)
+ using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq sets.Un del: prod_emb_Un)
also have "\<dots> = \<mu>G A + \<mu>G B"
using J K JK_disj by (simp add: plus_emeasure[symmetric])
finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
--- a/src/HOL/Probability/Projective_Limit.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Nov 27 11:29:47 2012 +0100
@@ -243,11 +243,8 @@
assume "x \<in> K n" hence fm_in: "fm n x \<in> fm n ` B n"
using K' by (force simp: K_def)
show "x \<in> B n"
- apply (rule inj_on_image_mem_iff[OF inj_on_fm _ fm_in])
- using `x \<in> K n` K_sets J[of n] sets_into_space
- apply (auto simp: proj_space)
- using J[of n] sets_into_space apply auto
- done
+ using `x \<in> K n` K_sets sets.sets_into_space J[of n]
+ by (intro inj_on_image_mem_iff[OF inj_on_fm _ fm_in, of "\<lambda>_. borel"]) auto
qed
def Z' \<equiv> "\<lambda>n. emb I (J n) (K n)"
have Z': "\<And>n. Z' n \<subseteq> Z n"
@@ -263,7 +260,7 @@
proof safe
fix y assume "y \<in> B n"
moreover
- hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets_into_space[of "B n" "P (J n)"]
+ hence "y \<in> space (Pi\<^isub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
by (auto simp add: proj_space proj_sets)
assume "fm n x = fm n y"
note inj_onD[OF inj_on_fm[OF space_borel],
@@ -314,7 +311,7 @@
moreover have "\<mu>G (Z n - Y n) = limP (J n) (\<lambda>_. borel) P
(B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"
unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`
- by (subst \<mu>G_eq) (auto intro!: Diff)
+ by (subst \<mu>G_eq) (auto intro!: sets.Diff)
ultimately
have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
using J J_mono K_sets `n \<ge> 1`
@@ -406,7 +403,7 @@
thus "K' (Suc n) \<noteq> {}" by auto
fix k
assume "k \<in> K' (Suc n)"
- with K'[of "Suc n"] sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
+ with K'[of "Suc n"] sets.sets_into_space have "k \<in> fm (Suc n) ` B (Suc n)" by auto
then obtain b where "k = fm (Suc n) b" by auto
thus "domain k = domain (fm (Suc n) (y (Suc n)))"
by (simp_all add: fm_def)
--- a/src/HOL/Probability/Radon_Nikodym.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Nov 27 11:29:47 2012 +0100
@@ -189,13 +189,13 @@
fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
from B[OF this] show "-e < ?d B" .
next
- show "space M - A n \<in> sets M" by (rule compl_sets) fact
+ show "space M - A n \<in> sets M" by (rule sets.compl_sets) fact
next
show "?d (space M) \<le> ?d (space M - A n)"
proof (induct n)
fix n assume "?d (space M) \<le> ?d (space M - A n)"
also have "\<dots> \<le> ?d (space M - A (Suc n))"
- using A_in_sets sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
+ using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq])
finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
qed simp
@@ -241,7 +241,7 @@
by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
with S have "?P (S \<inter> X) S n"
- by (simp add: measure_restricted sets_eq Int) (metis inf_absorb2)
+ by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
hence "\<exists>A. ?P A S n" .. }
note Ex_P = this
def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
@@ -309,7 +309,7 @@
hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
hence sets': "?A \<inter> A \<in> sets N" "(space M - ?A) \<inter> A \<in> sets N" by (auto simp: sets_eq)
have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
- using sets_into_space[OF `A \<in> sets M`] by auto
+ using sets.sets_into_space[OF `A \<in> sets M`] by auto
have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
by (auto simp: indicator_def max_def)
@@ -351,7 +351,7 @@
have y_le: "?y \<le> N (space M)" unfolding G_def
proof (safe intro!: SUP_least)
fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A"
- from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> N (space M)"
+ from this[THEN bspec, OF sets.top] show "integral\<^isup>P M g \<le> N (space M)"
by (simp cong: positive_integral_cong)
qed
from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^isup>P M"] guess ys .. note ys = this
@@ -507,7 +507,7 @@
with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * emeasure M A0" unfolding int_f_eq_y
using `f \<in> G`
by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
- also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
+ also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
by (simp cong: positive_integral_cong)
finally have "?y < integral\<^isup>P M ?f0" by simp
moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
@@ -536,7 +536,7 @@
let ?a = "SUP Q:?Q. emeasure M Q"
have "{} \<in> ?Q" by auto
then have Q_not_empty: "?Q \<noteq> {}" by blast
- have "?a \<le> emeasure M (space M)" using sets_into_space
+ have "?a \<le> emeasure M (space M)" using sets.sets_into_space
by (auto intro!: SUP_least emeasure_mono)
then have "?a \<noteq> \<infinity>" using finite_emeasure_space
by auto
@@ -601,7 +601,7 @@
next
assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
- using Q' by (auto intro!: plus_emeasure countable_UN)
+ using Q' by (auto intro!: plus_emeasure sets.countable_UN)
also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
proof (rule SUP_emeasure_incseq[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
@@ -712,7 +712,7 @@
also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
using borel Qi Q0(1) `A \<in> sets M`
by (subst positive_integral_add) (auto simp del: ereal_infty_mult
- simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le)
+ simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
finally have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
@@ -727,7 +727,7 @@
moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
using Q_sets `A \<in> sets M` Q0(1) by auto
moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
- using `A \<in> sets M` sets_into_space Q0 by auto
+ using `A \<in> sets M` sets.sets_into_space Q0 by auto
ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
@@ -755,7 +755,7 @@
fix A assume "A \<in> null_sets ?MT"
with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
by (auto simp add: null_sets_density_iff)
- with pos sets_into_space have "AE x in M. x \<notin> A"
+ with pos sets.sets_into_space have "AE x in M. x \<notin> A"
by (elim eventually_elim1) (auto simp: not_le[symmetric])
then have "A \<in> null_sets M"
using `A \<in> sets M` by (simp add: AE_iff_null_sets)
@@ -784,7 +784,7 @@
assume "density M f = density M g"
with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
by (simp add: emeasure_density[symmetric])
- from this[THEN bspec, OF top] fin
+ from this[THEN bspec, OF sets.top] fin
have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
{ fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
@@ -898,7 +898,7 @@
let ?f'M = "density M f'"
{ fix A assume "A \<in> sets M"
then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
- using pos(1) sets_into_space by (force simp: indicator_def)
+ using pos(1) sets.sets_into_space by (force simp: indicator_def)
then have "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
note h_null_sets = this
@@ -994,7 +994,7 @@
def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
{ fix i j have "A i \<inter> Q j \<in> sets M"
unfolding A_def using f Q
- apply (rule_tac Int)
+ apply (rule_tac sets.Int)
by (cases i) (auto intro: measurable_sets[OF f(1)]) }
note A_in_sets = this
let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
@@ -1133,12 +1133,12 @@
note sets_eq_imp_space_eq[OF N, simp]
have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
{ fix A assume "A \<in> sets M"
- with inv T T' sets_into_space[OF this]
+ with inv T T' sets.sets_into_space[OF this]
have "T -` T' -` A \<inter> T -` space M' \<inter> space M = A"
by (auto simp: measurable_def) }
note eq = this[simp]
{ fix A assume "A \<in> sets M"
- with inv T T' sets_into_space[OF this]
+ with inv T T' sets.sets_into_space[OF this]
have "(T' \<circ> T) -` A \<inter> space M = A"
by (auto simp: measurable_def) }
note eq2 = this[simp]
@@ -1168,7 +1168,7 @@
have "N = distr N M (T' \<circ> T)"
by (subst measure_of_of_measure[of N, symmetric])
- (auto simp add: distr_def sigma_sets_eq intro!: measure_of_eq space_closed)
+ (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed)
also have "\<dots> = distr (distr N M' T) M T'"
using T T' by (simp add: distr_distr)
also have "\<dots> = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'"
--- a/src/HOL/Probability/Regularity.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Regularity.thy Tue Nov 27 11:29:47 2012 +0100
@@ -428,9 +428,9 @@
have "M ?U - M (\<Union>i. D i) = M (?U - (\<Union>i. D i))" using U `(\<Union>i. D i) \<in> sets M`
by (subst emeasure_Diff) (auto simp: sb)
also have "\<dots> \<le> M (\<Union>i. U i - D i)" using U `range D \<subseteq> sets M`
- by (intro emeasure_mono) (auto simp: sb intro!: countable_nat_UN Diff)
+ by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)
also have "\<dots> \<le> (\<Sum>i. M (U i - D i))" using U `range D \<subseteq> sets M`
- by (intro emeasure_subadditive_countably) (auto intro!: Diff simp: sb)
+ by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)
also have "\<dots> \<le> (\<Sum>i. ereal e/(2 powr Suc i))" using U `range D \<subseteq> sets M`
by (intro suminf_le_pos, subst emeasure_Diff)
(auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
--- a/src/HOL/Probability/Sigma_Algebra.thy Thu Nov 22 10:09:54 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 27 11:29:47 2012 +0100
@@ -1026,7 +1026,7 @@
lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
-interpretation sigma_algebra "space M" "sets M" for M :: "'a measure"
+interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
using measure_space[of M] by (auto simp: measure_space_def)
definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
@@ -1146,7 +1146,7 @@
lemma sets_eq_imp_space_eq:
"sets M = sets M' \<Longrightarrow> space M = space M'"
- using top[of M] top[of M'] space_closed[of M] space_closed[of M']
+ using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
by blast
lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
@@ -1225,7 +1225,7 @@
shows "f \<in> measurable M N"
proof -
interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets)
- from B top[of N] A.top space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
+ from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
{ fix X assume "X \<in> sigma_sets \<Omega> A"
then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>"
@@ -1237,7 +1237,7 @@
have [simp]: "f -` \<Omega> \<inter> space M = space M"
by (auto simp add: funcset_mem [OF f])
then show ?case
- by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+ by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl)
next
case (Union a)
then show ?case
@@ -1316,7 +1316,7 @@
using measure unfolding measurable_def by (auto split: split_if_asm)
show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
using `A \<in> sets M'` measure P unfolding * measurable_def
- by (auto intro!: Un)
+ by (auto intro!: sets.Un)
qed
lemma measurable_If_set:
@@ -1348,7 +1348,7 @@
by (simp add: set_eq_iff, safe)
(insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
with meas show ?thesis
- by (auto intro!: Int)
+ by (auto intro!: sets.Int)
next
assume i: "(LEAST j. False) \<noteq> i"
then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
@@ -1363,7 +1363,7 @@
by auto
qed }
then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
- by (intro countable_UN) auto
+ by (intro sets.countable_UN) auto
moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
(\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
ultimately show ?thesis by auto
@@ -1417,7 +1417,7 @@
by (auto dest: finite_subset)
moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
ultimately have "f -` X \<inter> space M \<in> sets M"
- using `X \<subseteq> A` by (auto intro!: finite_UN simp del: UN_simps) }
+ using `X \<subseteq> A` by (auto intro!: sets.finite_UN simp del: UN_simps) }
then show ?thesis
unfolding measurable_def by auto
qed
@@ -1434,7 +1434,7 @@
have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
by auto
also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
- by (auto intro!: countable_UN measurable_sets)
+ by (auto intro!: sets.countable_UN measurable_sets)
finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
qed
@@ -1466,7 +1466,7 @@
then have "P -` X \<inter> space M = {x\<in>space M. ((X = {True} \<longrightarrow> P x) \<and> (X = {False} \<longrightarrow> \<not> P x) \<and> X \<noteq> {})}"
unfolding UNIV_bool Pow_insert Pow_empty by auto
then have "P -` X \<inter> space M \<in> sets M"
- by (auto intro!: sets_Collect_neg sets_Collect_imp sets_Collect_conj sets_Collect_const P) }
+ by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
then show "pred M P"
by (auto simp: measurable_def)
qed
@@ -1714,13 +1714,13 @@
measurable_compose_rev[measurable_dest]
pred_sets1[measurable_dest]
pred_sets2[measurable_dest]
- sets_into_space[measurable_dest]
+ sets.sets_into_space[measurable_dest]
declare
- top[measurable]
- empty_sets[measurable (raw)]
- Un[measurable (raw)]
- Diff[measurable (raw)]
+ sets.top[measurable]
+ sets.empty_sets[measurable (raw)]
+ sets.Un[measurable (raw)]
+ sets.Diff[measurable (raw)]
declare
measurable_count_space[measurable (raw)]
@@ -1777,7 +1777,7 @@
shows
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i. P x i)"
"(\<And>i. pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i. P x i)"
- by (auto intro!: sets_Collect_countable_All sets_Collect_countable_Ex simp: pred_def)
+ by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)
lemma pred_intros_countable_bounded[measurable (raw)]:
fixes X :: "'i :: countable set"
@@ -1793,7 +1793,7 @@
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>I. N x i))"
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>I. P x i)"
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>I. P x i)"
- by (auto intro!: sets_Collect_finite_Ex sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
+ by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)
lemma countable_Un_Int[measurable (raw)]:
"(\<And>i :: 'i :: countable. i \<in> I \<Longrightarrow> N i \<in> sets M) \<Longrightarrow> (\<Union>i\<in>I. N i) \<in> sets M"
@@ -1854,7 +1854,7 @@
by (auto simp: Int_def conj_commute eq_commute pred_def)
declare
- Int[measurable (raw)]
+ sets.Int[measurable (raw)]
lemma pred_in_If[measurable (raw)]:
"(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>