--- a/src/HOL/Probability/Stream_Space.thy Thu Dec 04 21:28:35 2014 +0100
+++ b/src/HOL/Probability/Stream_Space.thy Fri Dec 05 12:06:18 2014 +0100
@@ -288,14 +288,14 @@
using S[THEN sets.sets_into_space]
apply (subst restrict_space_eq_vimage_algebra)
apply (simp add: space_stream_space streams_mono2)
- apply (subst vimage_algebra_cong[OF sets_stream_space_eq])
+ apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
apply (subst sets_stream_space_eq)
apply (subst sets_vimage_Sup_eq)
apply simp
apply (auto intro: streams_mono) []
apply (simp add: image_image space_restrict_space)
apply (intro SUP_sigma_cong)
- apply (simp add: vimage_algebra_cong[OF restrict_space_eq_vimage_algebra])
+ apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
apply (auto simp: streams_mono snth_in)
done
@@ -326,6 +326,23 @@
finally show ?case .
qed (simp add: streams_sets)
+lemma sigma_sets_singletons:
+ assumes "countable S"
+ shows "sigma_sets S ((\<lambda>s. {s})`S) = Pow S"
+proof safe
+ interpret sigma_algebra S "sigma_sets S ((\<lambda>s. {s})`S)"
+ by (rule sigma_algebra_sigma_sets) auto
+ fix A assume "A \<subseteq> S"
+ with assms have "(\<Union>a\<in>A. {a}) \<in> sigma_sets S ((\<lambda>s. {s})`S)"
+ by (intro countable_UN') (auto dest: countable_subset)
+ then show "A \<in> sigma_sets S ((\<lambda>s. {s})`S)"
+ by simp
+qed (auto dest: sigma_sets_into_sp[rotated])
+
+lemma sets_count_space_eq_sigma:
+ "countable S \<Longrightarrow> sets (count_space S) = sets (sigma S ((\<lambda>s. {s})`S))"
+ by (subst sets_measure_of) (auto simp: sigma_sets_singletons)
+
lemma sets_stream_space_sstart:
assumes S[simp]: "countable S"
shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
@@ -402,11 +419,8 @@
{ fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))"
have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
- apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra
- vimage_algebra_cong[OF M])
- apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra[symmetric])
- apply (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart)
- done }
+ by (subst sets_restrict_space_cong[OF M])
+ (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart) }
from this[OF sets_M] this[OF sets_N]
show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
"sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"