1(* Title: HOL/Probability/Stream_Space.thy 2 Author: Johannes H��lzl, TU M��nchen *) 3 4theory Stream_Space 5imports 6 Infinite_Product_Measure 7 "HOL-Library.Stream" 8 "HOL-Library.Linear_Temporal_Logic_on_Streams" 9begin 10 11lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)" 12 by (cases s) simp 13 14lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)" 15 by (cases n) simp_all 16 17definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where 18 "to_stream X = smap X nats" 19 20lemma to_stream_nat_case: "to_stream (case_nat x X) = x ## to_stream X" 21 unfolding to_stream_def 22 by (subst siterate.ctr) (simp add: smap_siterate[symmetric] stream.map_comp comp_def) 23 24lemma to_stream_in_streams: "to_stream X \<in> streams S \<longleftrightarrow> (\<forall>n. X n \<in> S)" 25 by (simp add: to_stream_def streams_iff_snth) 26 27definition stream_space :: "'a measure \<Rightarrow> 'a stream measure" where 28 "stream_space M = 29 distr (\<Pi>\<^sub>M i\<in>UNIV. M) (vimage_algebra (streams (space M)) snth (\<Pi>\<^sub>M i\<in>UNIV. M)) to_stream" 30 31lemma space_stream_space: "space (stream_space M) = streams (space M)" 32 by (simp add: stream_space_def) 33 34lemma streams_stream_space[intro]: "streams (space M) \<in> sets (stream_space M)" 35 using sets.top[of "stream_space M"] by (simp add: space_stream_space) 36 37lemma stream_space_Stream: 38 "x ## \<omega> \<in> space (stream_space M) \<longleftrightarrow> x \<in> space M \<and> \<omega> \<in> space (stream_space M)" 39 by (simp add: space_stream_space streams_Stream) 40 41lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream" 42 unfolding stream_space_def by (rule distr_cong) auto 43 44lemma sets_stream_space_cong[measurable_cong]: 45 "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)" 46 using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong) 47 48lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)" 49 by (auto intro!: measurable_vimage_algebra1 50 simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def) 51 52lemma measurable_snth[measurable]: "(\<lambda>\<omega>. \<omega> !! n) \<in> measurable (stream_space M) M" 53 using measurable_snth_PiM measurable_component_singleton by (rule measurable_compose) simp 54 55lemma measurable_shd[measurable]: "shd \<in> measurable (stream_space M) M" 56 using measurable_snth[of 0] by simp 57 58lemma measurable_stream_space2: 59 assumes f_snth: "\<And>n. (\<lambda>x. f x !! n) \<in> measurable N M" 60 shows "f \<in> measurable N (stream_space M)" 61 unfolding stream_space_def measurable_distr_eq2 62proof (rule measurable_vimage_algebra2) 63 show "f \<in> space N \<rightarrow> streams (space M)" 64 using f_snth[THEN measurable_space] by (auto simp add: streams_iff_sset sset_range) 65 show "(\<lambda>x. (!!) (f x)) \<in> measurable N (Pi\<^sub>M UNIV (\<lambda>i. M))" 66 proof (rule measurable_PiM_single') 67 show "(\<lambda>x. (!!) (f x)) \<in> space N \<rightarrow> UNIV \<rightarrow>\<^sub>E space M" 68 using f_snth[THEN measurable_space] by auto 69 qed (rule f_snth) 70qed 71 72lemma measurable_stream_coinduct[consumes 1, case_names shd stl, coinduct set: measurable]: 73 assumes "F f" 74 assumes h: "\<And>f. F f \<Longrightarrow> (\<lambda>x. shd (f x)) \<in> measurable N M" 75 assumes t: "\<And>f. F f \<Longrightarrow> F (\<lambda>x. stl (f x))" 76 shows "f \<in> measurable N (stream_space M)" 77proof (rule measurable_stream_space2) 78 fix n show "(\<lambda>x. f x !! n) \<in> measurable N M" 79 using \<open>F f\<close> by (induction n arbitrary: f) (auto intro: h t) 80qed 81 82lemma measurable_sdrop[measurable]: "sdrop n \<in> measurable (stream_space M) (stream_space M)" 83 by (rule measurable_stream_space2) (simp add: sdrop_snth) 84 85lemma measurable_stl[measurable]: "(\<lambda>\<omega>. stl \<omega>) \<in> measurable (stream_space M) (stream_space M)" 86 by (rule measurable_stream_space2) (simp del: snth.simps add: snth.simps[symmetric]) 87 88lemma measurable_to_stream[measurable]: "to_stream \<in> measurable (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M)" 89 by (rule measurable_stream_space2) (simp add: to_stream_def) 90 91lemma measurable_Stream[measurable (raw)]: 92 assumes f[measurable]: "f \<in> measurable N M" 93 assumes g[measurable]: "g \<in> measurable N (stream_space M)" 94 shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)" 95 by (rule measurable_stream_space2) (simp add: Stream_snth) 96 97lemma measurable_smap[measurable]: 98 assumes X[measurable]: "X \<in> measurable N M" 99 shows "smap X \<in> measurable (stream_space N) (stream_space M)" 100 by (rule measurable_stream_space2) simp 101 102lemma measurable_stake[measurable]: 103 "stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))" 104 by (induct i) auto 105 106lemma measurable_shift[measurable]: 107 assumes f: "f \<in> measurable N (stream_space M)" 108 assumes [measurable]: "g \<in> measurable N (stream_space M)" 109 shows "(\<lambda>x. stake n (f x) @- g x) \<in> measurable N (stream_space M)" 110 using f by (induction n arbitrary: f) simp_all 111 112lemma measurable_case_stream_replace[measurable (raw)]: 113 "(\<lambda>x. f x (shd (g x)) (stl (g x))) \<in> measurable M N \<Longrightarrow> (\<lambda>x. case_stream (f x) (g x)) \<in> measurable M N" 114 unfolding stream.case_eq_if . 115 116lemma measurable_ev_at[measurable]: 117 assumes [measurable]: "Measurable.pred (stream_space M) P" 118 shows "Measurable.pred (stream_space M) (ev_at P n)" 119 by (induction n) auto 120 121lemma measurable_alw[measurable]: 122 "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (alw P)" 123 unfolding alw_def 124 by (coinduction rule: measurable_gfp_coinduct) (auto simp: inf_continuous_def) 125 126lemma measurable_ev[measurable]: 127 "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (ev P)" 128 unfolding ev_def 129 by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def) 130 131lemma measurable_until: 132 assumes [measurable]: "Measurable.pred (stream_space M) \<phi>" "Measurable.pred (stream_space M) \<psi>" 133 shows "Measurable.pred (stream_space M) (\<phi> until \<psi>)" 134 unfolding UNTIL_def 135 by (coinduction rule: measurable_gfp_coinduct) (simp_all add: inf_continuous_def fun_eq_iff) 136 137lemma measurable_holds [measurable]: "Measurable.pred M P \<Longrightarrow> Measurable.pred (stream_space M) (holds P)" 138 unfolding holds.simps[abs_def] 139 by (rule measurable_compose[OF measurable_shd]) simp 140 141lemma measurable_hld[measurable]: assumes [measurable]: "t \<in> sets M" shows "Measurable.pred (stream_space M) (HLD t)" 142 unfolding HLD_def by measurable 143 144lemma measurable_nxt[measurable (raw)]: 145 "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (nxt P)" 146 unfolding nxt.simps[abs_def] by simp 147 148lemma measurable_suntil[measurable]: 149 assumes [measurable]: "Measurable.pred (stream_space M) Q" "Measurable.pred (stream_space M) P" 150 shows "Measurable.pred (stream_space M) (Q suntil P)" 151 unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: sup_continuous_def) 152 153lemma measurable_szip: 154 "(\<lambda>(\<omega>1, \<omega>2). szip \<omega>1 \<omega>2) \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (stream_space (M \<Otimes>\<^sub>M N))" 155proof (rule measurable_stream_space2) 156 fix n 157 have "(\<lambda>x. (case x of (\<omega>1, \<omega>2) \<Rightarrow> szip \<omega>1 \<omega>2) !! n) = (\<lambda>(\<omega>1, \<omega>2). (\<omega>1 !! n, \<omega>2 !! n))" 158 by auto 159 also have "\<dots> \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (M \<Otimes>\<^sub>M N)" 160 by measurable 161 finally show "(\<lambda>x. (case x of (\<omega>1, \<omega>2) \<Rightarrow> szip \<omega>1 \<omega>2) !! n) \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (M \<Otimes>\<^sub>M N)" 162 . 163qed 164 165lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)" 166proof - 167 interpret product_prob_space "\<lambda>_. M" UNIV .. 168 show ?thesis 169 by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr) 170qed 171 172lemma (in prob_space) nn_integral_stream_space: 173 assumes [measurable]: "f \<in> borel_measurable (stream_space M)" 174 shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)" 175proof - 176 interpret S: sequence_space M .. 177 interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M" .. 178 179 have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)" 180 by (subst stream_space_eq_distr) (simp add: nn_integral_distr) 181 also have "\<dots> = (\<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)) \<partial>(M \<Otimes>\<^sub>M S.S))" 182 by (subst S.PiM_iter[symmetric]) (simp add: nn_integral_distr) 183 also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) (x, X))) \<partial>S.S \<partial>M)" 184 by (subst S.nn_integral_fst) simp_all 185 also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## to_stream X) \<partial>S.S \<partial>M)" 186 by (auto intro!: nn_integral_cong simp: to_stream_nat_case) 187 also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M \<partial>M)" 188 by (subst stream_space_eq_distr) 189 (simp add: nn_integral_distr cong: nn_integral_cong) 190 finally show ?thesis . 191qed 192 193lemma (in prob_space) emeasure_stream_space: 194 assumes X[measurable]: "X \<in> sets (stream_space M)" 195 shows "emeasure (stream_space M) X = (\<integral>\<^sup>+t. emeasure (stream_space M) {x\<in>space (stream_space M). t ## x \<in> X } \<partial>M)" 196proof - 197 have eq: "\<And>x xs. xs \<in> space (stream_space M) \<Longrightarrow> x \<in> space M \<Longrightarrow> 198 indicator X (x ## xs) = indicator {xs\<in>space (stream_space M). x ## xs \<in> X } xs" 199 by (auto split: split_indicator) 200 show ?thesis 201 using nn_integral_stream_space[of "indicator X"] 202 apply (auto intro!: nn_integral_cong) 203 apply (subst nn_integral_cong) 204 apply (rule eq) 205 apply simp_all 206 done 207qed 208 209lemma (in prob_space) prob_stream_space: 210 assumes P[measurable]: "{x\<in>space (stream_space M). P x} \<in> sets (stream_space M)" 211 shows "\<P>(x in stream_space M. P x) = (\<integral>\<^sup>+t. \<P>(x in stream_space M. P (t ## x)) \<partial>M)" 212proof - 213 interpret S: prob_space "stream_space M" 214 by (rule prob_space_stream_space) 215 show ?thesis 216 unfolding S.emeasure_eq_measure[symmetric] 217 by (subst emeasure_stream_space) (auto simp: stream_space_Stream intro!: nn_integral_cong) 218qed 219 220lemma (in prob_space) AE_stream_space: 221 assumes [measurable]: "Measurable.pred (stream_space M) P" 222 shows "(AE X in stream_space M. P X) = (AE x in M. AE X in stream_space M. P (x ## X))" 223proof - 224 interpret stream: prob_space "stream_space M" 225 by (rule prob_space_stream_space) 226 227 have eq: "\<And>x X. indicator {x. \<not> P x} (x ## X) = indicator {X. \<not> P (x ## X)} X" 228 by (auto split: split_indicator) 229 show ?thesis 230 apply (subst AE_iff_nn_integral, simp) 231 apply (subst nn_integral_stream_space, simp) 232 apply (subst eq) 233 apply (subst nn_integral_0_iff_AE, simp) 234 apply (simp add: AE_iff_nn_integral[symmetric]) 235 done 236qed 237 238lemma (in prob_space) AE_stream_all: 239 assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x" 240 shows "AE x in stream_space M. stream_all P x" 241proof - 242 { fix n have "AE x in stream_space M. P (x !! n)" 243 proof (induct n) 244 case 0 with P show ?case 245 by (subst AE_stream_space) (auto elim!: eventually_mono) 246 next 247 case (Suc n) then show ?case 248 by (subst AE_stream_space) auto 249 qed } 250 then show ?thesis 251 unfolding stream_all_def by (simp add: AE_all_countable) 252qed 253 254lemma streams_sets: 255 assumes X[measurable]: "X \<in> sets M" shows "streams X \<in> sets (stream_space M)" 256proof - 257 have "streams X = {x\<in>space (stream_space M). x \<in> streams X}" 258 using streams_mono[OF _ sets.sets_into_space[OF X]] by (auto simp: space_stream_space) 259 also have "\<dots> = {x\<in>space (stream_space M). gfp (\<lambda>p x. shd x \<in> X \<and> p (stl x)) x}" 260 apply (simp add: set_eq_iff streams_def streamsp_def) 261 apply (intro allI conj_cong refl arg_cong2[where f=gfp] ext) 262 apply (case_tac xa) 263 apply auto 264 done 265 also have "\<dots> \<in> sets (stream_space M)" 266 apply (intro predE) 267 apply (coinduction rule: measurable_gfp_coinduct) 268 apply (auto simp: inf_continuous_def) 269 done 270 finally show ?thesis . 271qed 272 273lemma sets_stream_space_in_sets: 274 assumes space: "space N = streams (space M)" 275 assumes sets: "\<And>i. (\<lambda>x. x !! i) \<in> measurable N M" 276 shows "sets (stream_space M) \<subseteq> sets N" 277 unfolding stream_space_def sets_distr 278 by (auto intro!: sets_image_in_sets measurable_Sup2 measurable_vimage_algebra2 del: subsetI equalityI 279 simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets) 280 281lemma sets_stream_space_eq: "sets (stream_space M) = 282 sets (SUP i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)" 283 by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets 284 measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI 285 simp: space_Sup_eq_UN space_stream_space) 286 287lemma sets_restrict_stream_space: 288 assumes S[measurable]: "S \<in> sets M" 289 shows "sets (restrict_space (stream_space M) (streams S)) = sets (stream_space (restrict_space M S))" 290 using S[THEN sets.sets_into_space] 291 apply (subst restrict_space_eq_vimage_algebra) 292 apply (simp add: space_stream_space streams_mono2) 293 apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq]) 294 apply (subst sets_stream_space_eq) 295 apply (subst sets_vimage_Sup_eq[where Y="streams (space M)"]) 296 apply simp 297 apply auto [] 298 apply (auto intro: streams_mono) [] 299 apply auto [] 300 apply (simp add: image_image space_restrict_space) 301 apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra]) 302 apply (subst (1 2) vimage_algebra_vimage_algebra_eq) 303 apply (auto simp: streams_mono snth_in ) 304 done 305 306primrec sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" where 307 "sstart S [] = streams S" 308| [simp del]: "sstart S (x # xs) = (##) x ` sstart S xs" 309 310lemma in_sstart[simp]: "s \<in> sstart S (x # xs) \<longleftrightarrow> shd s = x \<and> stl s \<in> sstart S xs" 311 by (cases s) (auto simp: sstart.simps(2)) 312 313lemma sstart_in_streams: "xs \<in> lists S \<Longrightarrow> sstart S xs \<subseteq> streams S" 314 by (induction xs) (auto simp: sstart.simps(2)) 315 316lemma sstart_eq: "x \<in> streams S \<Longrightarrow> x \<in> sstart S xs = (\<forall>i<length xs. x !! i = xs ! i)" 317 by (induction xs arbitrary: x) (auto simp: nth_Cons streams_stl split: nat.splits) 318 319lemma sstart_sets: "sstart S xs \<in> sets (stream_space (count_space UNIV))" 320proof (induction xs) 321 case (Cons x xs) 322 note Cons[measurable] 323 have "sstart S (x # xs) = 324 {s\<in>space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}" 325 by (simp add: set_eq_iff space_stream_space) 326 also have "\<dots> \<in> sets (stream_space (count_space UNIV))" 327 by measurable 328 finally show ?case . 329qed (simp add: streams_sets) 330 331lemma sigma_sets_singletons: 332 assumes "countable S" 333 shows "sigma_sets S ((\<lambda>s. {s})`S) = Pow S" 334proof safe 335 interpret sigma_algebra S "sigma_sets S ((\<lambda>s. {s})`S)" 336 by (rule sigma_algebra_sigma_sets) auto 337 fix A assume "A \<subseteq> S" 338 with assms have "(\<Union>a\<in>A. {a}) \<in> sigma_sets S ((\<lambda>s. {s})`S)" 339 by (intro countable_UN') (auto dest: countable_subset) 340 then show "A \<in> sigma_sets S ((\<lambda>s. {s})`S)" 341 by simp 342qed (auto dest: sigma_sets_into_sp[rotated]) 343 344lemma sets_count_space_eq_sigma: 345 "countable S \<Longrightarrow> sets (count_space S) = sets (sigma S ((\<lambda>s. {s})`S))" 346 by (subst sets_measure_of) (auto simp: sigma_sets_singletons) 347 348lemma sets_stream_space_sstart: 349 assumes S[simp]: "countable S" 350 shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \<union> {{}}))" 351proof 352 have [simp]: "sstart S ` lists S \<subseteq> Pow (streams S)" 353 by (simp add: image_subset_iff sstart_in_streams) 354 355 let ?S = "sigma (streams S) (sstart S ` lists S \<union> {{}})" 356 { fix i a assume "a \<in> S" 357 { fix x have "(x !! i = a \<and> x \<in> streams S) \<longleftrightarrow> (\<exists>xs\<in>lists S. length xs = i \<and> x \<in> sstart S (xs @ [a]))" 358 proof (induction i arbitrary: x) 359 case (Suc i) from this[of "stl x"] show ?case 360 by (simp add: length_Suc_conv Bex_def ex_simps[symmetric] del: ex_simps) 361 (metis stream.collapse streams_Stream) 362 qed (insert \<open>a \<in> S\<close>, auto intro: streams_stl in_streams) } 363 then have "(\<lambda>x. x !! i) -` {a} \<inter> streams S = (\<Union>xs\<in>{xs\<in>lists S. length xs = i}. sstart S (xs @ [a]))" 364 by (auto simp add: set_eq_iff) 365 also have "\<dots> \<in> sets ?S" 366 using \<open>a\<in>S\<close> by (intro sets.countable_UN') (auto intro!: sigma_sets.Basic image_eqI) 367 finally have " (\<lambda>x. x !! i) -` {a} \<inter> streams S \<in> sets ?S" . } 368 then show "sets (stream_space (count_space S)) \<subseteq> sets (sigma (streams S) (sstart S`lists S \<union> {{}}))" 369 by (intro sets_stream_space_in_sets) (auto simp: measurable_count_space_eq_countable snth_in) 370 371 have "sigma_sets (space (stream_space (count_space S))) (sstart S`lists S \<union> {{}}) \<subseteq> sets (stream_space (count_space S))" 372 proof (safe intro!: sets.sigma_sets_subset) 373 fix xs assume "\<forall>x\<in>set xs. x \<in> S" 374 then have "sstart S xs = {x\<in>space (stream_space (count_space S)). \<forall>i<length xs. x !! i = xs ! i}" 375 by (induction xs) 376 (auto simp: space_stream_space nth_Cons split: nat.split intro: in_streams streams_stl) 377 also have "\<dots> \<in> sets (stream_space (count_space S))" 378 by measurable 379 finally show "sstart S xs \<in> sets (stream_space (count_space S))" . 380 qed 381 then show "sets (sigma (streams S) (sstart S`lists S \<union> {{}})) \<subseteq> sets (stream_space (count_space S))" 382 by (simp add: space_stream_space) 383qed 384 385lemma Int_stable_sstart: "Int_stable (sstart S`lists S \<union> {{}})" 386proof - 387 { fix xs ys assume "xs \<in> lists S" "ys \<in> lists S" 388 then have "sstart S xs \<inter> sstart S ys \<in> sstart S ` lists S \<union> {{}}" 389 proof (induction xs ys rule: list_induct2') 390 case (4 x xs y ys) 391 show ?case 392 proof cases 393 assume "x = y" 394 then have "sstart S (x # xs) \<inter> sstart S (y # ys) = (##) x ` (sstart S xs \<inter> sstart S ys)" 395 by (auto simp: image_iff intro!: stream.collapse[symmetric]) 396 also have "\<dots> \<in> sstart S ` lists S \<union> {{}}" 397 using 4 by (auto simp: sstart.simps(2)[symmetric] del: in_listsD) 398 finally show ?case . 399 qed auto 400 qed (simp_all add: sstart_in_streams inf.absorb1 inf.absorb2 image_eqI[where x="[]"]) } 401 then show ?thesis 402 by (auto simp: Int_stable_def) 403qed 404 405lemma stream_space_eq_sstart: 406 assumes S[simp]: "countable S" 407 assumes P: "prob_space M" "prob_space N" 408 assumes ae: "AE x in M. x \<in> streams S" "AE x in N. x \<in> streams S" 409 assumes sets_M: "sets M = sets (stream_space (count_space UNIV))" 410 assumes sets_N: "sets N = sets (stream_space (count_space UNIV))" 411 assumes *: "\<And>xs. xs \<noteq> [] \<Longrightarrow> xs \<in> lists S \<Longrightarrow> emeasure M (sstart S xs) = emeasure N (sstart S xs)" 412 shows "M = N" 413proof (rule measure_eqI_restrict_generator[OF Int_stable_sstart]) 414 have [simp]: "sstart S ` lists S \<subseteq> Pow (streams S)" 415 by (simp add: image_subset_iff sstart_in_streams) 416 417 interpret M: prob_space M by fact 418 419 show "sstart S ` lists S \<union> {{}} \<subseteq> Pow (streams S)" 420 by (auto dest: sstart_in_streams del: in_listsD) 421 422 { fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))" 423 have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})" 424 by (subst sets_restrict_space_cong[OF M]) 425 (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart) } 426 from this[OF sets_M] this[OF sets_N] 427 show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})" 428 "sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})" 429 by auto 430 show "{streams S} \<subseteq> sstart S ` lists S \<union> {{}}" 431 "\<Union>{streams S} = streams S" "\<And>s. s \<in> {streams S} \<Longrightarrow> emeasure M s \<noteq> \<infinity>" 432 using M.emeasure_space_1 space_stream_space[of "count_space S"] sets_eq_imp_space_eq[OF sets_M] 433 by (auto simp add: image_eqI[where x="[]"]) 434 show "sets M = sets N" 435 by (simp add: sets_M sets_N) 436next 437 fix X assume "X \<in> sstart S ` lists S \<union> {{}}" 438 then obtain xs where "X = {} \<or> (xs \<in> lists S \<and> X = sstart S xs)" 439 by auto 440 moreover have "emeasure M (streams S) = 1" 441 using ae by (intro prob_space.emeasure_eq_1_AE[OF P(1)]) (auto simp: sets_M streams_sets) 442 moreover have "emeasure N (streams S) = 1" 443 using ae by (intro prob_space.emeasure_eq_1_AE[OF P(2)]) (auto simp: sets_N streams_sets) 444 ultimately show "emeasure M X = emeasure N X" 445 using P[THEN prob_space.emeasure_space_1] 446 by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD) 447qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets) 448 449lemma sets_sstart[measurable]: "sstart \<Omega> xs \<in> sets (stream_space (count_space UNIV))" 450proof (induction xs) 451 case (Cons x xs) 452 note this[measurable] 453 have "sstart \<Omega> (x # xs) = {\<omega>\<in>space (stream_space (count_space UNIV)). \<omega> \<in> sstart \<Omega> (x # xs)}" 454 by (auto simp: space_stream_space) 455 also have "\<dots> \<in> sets (stream_space (count_space UNIV))" 456 unfolding in_sstart by measurable 457 finally show ?case . 458qed (auto intro!: streams_sets) 459 460primrec scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set" 461where 462 "scylinder S [] = streams S" 463| "scylinder S (A # As) = {\<omega>\<in>streams S. shd \<omega> \<in> A \<and> stl \<omega> \<in> scylinder S As}" 464 465lemma scylinder_streams: "scylinder S xs \<subseteq> streams S" 466 by (induction xs) auto 467 468lemma sets_scylinder: "(\<forall>x\<in>set xs. x \<in> sets S) \<Longrightarrow> scylinder (space S) xs \<in> sets (stream_space S)" 469 by (induction xs) (auto simp: space_stream_space[symmetric]) 470 471lemma stream_space_eq_scylinder: 472 assumes P: "prob_space M" "prob_space N" 473 assumes "Int_stable G" and S: "sets S = sets (sigma (space S) G)" 474 and C: "countable C" "C \<subseteq> G" "\<Union>C = space S" and G: "G \<subseteq> Pow (space S)" 475 assumes sets_M: "sets M = sets (stream_space S)" 476 assumes sets_N: "sets N = sets (stream_space S)" 477 assumes *: "\<And>xs. xs \<noteq> [] \<Longrightarrow> xs \<in> lists G \<Longrightarrow> emeasure M (scylinder (space S) xs) = emeasure N (scylinder (space S) xs)" 478 shows "M = N" 479proof (rule measure_eqI_generator_eq) 480 interpret M: prob_space M by fact 481 interpret N: prob_space N by fact 482 483 let ?G = "scylinder (space S) ` lists G" 484 show sc_Pow: "?G \<subseteq> Pow (streams (space S))" 485 using scylinder_streams by auto 486 487 have "sets (stream_space S) = sets (sigma (streams (space S)) ?G)" 488 (is "?S = sets ?R") 489 proof (rule antisym) 490 let ?V = "\<lambda>i. vimage_algebra (streams (space S)) (\<lambda>s. s !! i) S" 491 show "?S \<subseteq> sets ?R" 492 unfolding sets_stream_space_eq 493 proof (safe intro!: sets_Sup_in_sets del: subsetI equalityI) 494 fix i :: nat 495 show "space (?V i) = space ?R" 496 using scylinder_streams by (subst space_measure_of) (auto simp: ) 497 { fix A assume "A \<in> G" 498 then have "scylinder (space S) (replicate i (space S) @ [A]) = (\<lambda>s. s !! i) -` A \<inter> streams (space S)" 499 by (induction i) (auto simp add: streams_shd streams_stl cong: conj_cong) 500 also have "scylinder (space S) (replicate i (space S) @ [A]) = (\<Union>xs\<in>{xs\<in>lists C. length xs = i}. scylinder (space S) (xs @ [A]))" 501 apply (induction i) 502 apply auto [] 503 apply (simp add: length_Suc_conv set_eq_iff ex_simps(1,2)[symmetric] cong: conj_cong del: ex_simps(1,2)) 504 apply rule 505 subgoal for i x 506 apply (cases x) 507 apply (subst (2) C(3)[symmetric]) 508 apply (simp del: ex_simps(1,2) add: ex_simps(1,2)[symmetric] ac_simps Bex_def) 509 apply auto 510 done 511 done 512 finally have "(\<lambda>s. s !! i) -` A \<inter> streams (space S) = (\<Union>xs\<in>{xs\<in>lists C. length xs = i}. scylinder (space S) (xs @ [A]))" 513 .. 514 also have "\<dots> \<in> ?R" 515 using C(2) \<open>A\<in>G\<close> 516 by (intro sets.countable_UN' countable_Collect countable_lists C) 517 (auto intro!: in_measure_of[OF sc_Pow] imageI) 518 finally have "(\<lambda>s. s !! i) -` A \<inter> streams (space S) \<in> ?R" . } 519 then show "sets (?V i) \<subseteq> ?R" 520 apply (subst vimage_algebra_cong[OF refl refl S]) 521 apply (subst vimage_algebra_sigma[OF G]) 522 apply (simp add: streams_iff_snth) [] 523 apply (subst sigma_le_sets) 524 apply auto 525 done 526 qed 527 have "G \<subseteq> sets S" 528 unfolding S using G by auto 529 with C(2) show "sets ?R \<subseteq> ?S" 530 unfolding sigma_le_sets[OF sc_Pow] by (auto intro!: sets_scylinder) 531 qed 532 then show "sets M = sigma_sets (streams (space S)) (scylinder (space S) ` lists G)" 533 "sets N = sigma_sets (streams (space S)) (scylinder (space S) ` lists G)" 534 unfolding sets_M sets_N by (simp_all add: sc_Pow) 535 536 show "Int_stable ?G" 537 proof (rule Int_stableI_image) 538 fix xs ys assume "xs \<in> lists G" "ys \<in> lists G" 539 then show "\<exists>zs\<in>lists G. scylinder (space S) xs \<inter> scylinder (space S) ys = scylinder (space S) zs" 540 proof (induction xs arbitrary: ys) 541 case Nil then show ?case 542 by (auto simp add: Int_absorb1 scylinder_streams) 543 next 544 case xs: (Cons x xs) 545 show ?case 546 proof (cases ys) 547 case Nil with xs.hyps show ?thesis 548 by (auto simp add: Int_absorb2 scylinder_streams intro!: bexI[of _ "x#xs"]) 549 next 550 case ys: (Cons y ys') 551 with xs.IH[of ys'] xs.prems obtain zs where 552 "zs \<in> lists G" and eq: "scylinder (space S) xs \<inter> scylinder (space S) ys' = scylinder (space S) zs" 553 by auto 554 show ?thesis 555 proof (intro bexI[of _ "(x \<inter> y)#zs"]) 556 show "x \<inter> y # zs \<in> lists G" 557 using \<open>zs\<in>lists G\<close> \<open>x\<in>G\<close> \<open>ys\<in>lists G\<close> ys \<open>Int_stable G\<close>[THEN Int_stableD, of x y] by auto 558 show "scylinder (space S) (x # xs) \<inter> scylinder (space S) ys = scylinder (space S) (x \<inter> y # zs)" 559 by (auto simp add: eq[symmetric] ys) 560 qed 561 qed 562 qed 563 qed 564 565 show "range (\<lambda>_::nat. streams (space S)) \<subseteq> scylinder (space S) ` lists G" 566 "(\<Union>i. streams (space S)) = streams (space S)" 567 "emeasure M (streams (space S)) \<noteq> \<infinity>" 568 by (auto intro!: image_eqI[of _ _ "[]"]) 569 570 fix X assume "X \<in> scylinder (space S) ` lists G" 571 then obtain xs where xs: "xs \<in> lists G" and eq: "X = scylinder (space S) xs" 572 by auto 573 then show "emeasure M X = emeasure N X" 574 proof (cases "xs = []") 575 assume "xs = []" then show ?thesis 576 unfolding eq 577 using sets_M[THEN sets_eq_imp_space_eq] sets_N[THEN sets_eq_imp_space_eq] 578 M.emeasure_space_1 N.emeasure_space_1 579 by (simp add: space_stream_space[symmetric]) 580 next 581 assume "xs \<noteq> []" with xs show ?thesis 582 unfolding eq by (intro *) 583 qed 584qed 585 586lemma stream_space_coinduct: 587 fixes R :: "'a stream measure \<Rightarrow> 'a stream measure \<Rightarrow> bool" 588 assumes "R A B" 589 assumes R: "\<And>A B. R A B \<Longrightarrow> \<exists>K\<in>space (prob_algebra M). 590 \<exists>A'\<in>M \<rightarrow>\<^sub>M prob_algebra (stream_space M). \<exists>B'\<in>M \<rightarrow>\<^sub>M prob_algebra (stream_space M). 591 (AE y in K. R (A' y) (B' y) \<or> A' y = B' y) \<and> 592 A = do { y \<leftarrow> K; \<omega> \<leftarrow> A' y; return (stream_space M) (y ## \<omega>) } \<and> 593 B = do { y \<leftarrow> K; \<omega> \<leftarrow> B' y; return (stream_space M) (y ## \<omega>) }" 594 shows "A = B" 595proof (rule stream_space_eq_scylinder) 596 let ?step = "\<lambda>K L. do { y \<leftarrow> K; \<omega> \<leftarrow> L y; return (stream_space M) (y ## \<omega>) }" 597 { fix K A A' assume K: "K \<in> space (prob_algebra M)" 598 and A'[measurable]: "A' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" and A_eq: "A = ?step K A'" 599 have ps: "prob_space A" 600 unfolding A_eq by (rule prob_space_bind'[OF K]) measurable 601 have "sets A = sets (stream_space M)" 602 unfolding A_eq by (rule sets_bind'[OF K]) measurable 603 note ps this } 604 note ** = this 605 606 { fix A B assume "R A B" 607 obtain K A' B' where K: "K \<in> space (prob_algebra M)" 608 and A': "A' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" "A = ?step K A'" 609 and B': "B' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" "B = ?step K B'" 610 using R[OF \<open>R A B\<close>] by blast 611 have "prob_space A" "prob_space B" "sets A = sets (stream_space M)" "sets B = sets (stream_space M)" 612 using **[OF K A'] **[OF K B'] by auto } 613 note R_D = this 614 615 show "prob_space A" "prob_space B" "sets A = sets (stream_space M)" "sets B = sets (stream_space M)" 616 using R_D[OF \<open>R A B\<close>] by auto 617 618 show "Int_stable (sets M)" "sets M = sets (sigma (space M) (sets M))" "countable {space M}" 619 "{space M} \<subseteq> sets M" "\<Union>{space M} = space M" "sets M \<subseteq> Pow (space M)" 620 using sets.space_closed[of M] by (auto simp: Int_stable_def) 621 622 { fix A As L K assume K[measurable]: "K \<in> space (prob_algebra M)" and A: "A \<in> sets M" "As \<in> lists (sets M)" 623 and L[measurable]: "L \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" 624 from A have [measurable]: "\<forall>x\<in>set (A # As). x \<in> sets M" "\<forall>x\<in>set As. x \<in> sets M" 625 by auto 626 have [simp]: "space K = space M" "sets K = sets M" 627 using K by (auto simp: space_prob_algebra intro!: sets_eq_imp_space_eq) 628 have [simp]: "x \<in> space M \<Longrightarrow> sets (L x) = sets (stream_space M)" for x 629 using measurable_space[OF L] by (auto simp: space_prob_algebra) 630 note sets_scylinder[measurable] 631 have *: "indicator (scylinder (space M) (A # As)) (x ## \<omega>) = 632 (indicator A x * indicator (scylinder (space M) As) \<omega> :: ennreal)" for \<omega> x 633 using scylinder_streams[of "space M" As] \<open>A \<in> sets M\<close>[THEN sets.sets_into_space] 634 by (auto split: split_indicator) 635 have "emeasure (?step K L) (scylinder (space M) (A # As)) = (\<integral>\<^sup>+y. L y (scylinder (space M) As) * indicator A y \<partial>K)" 636 apply (subst emeasure_bind_prob_algebra[OF K]) 637 apply measurable 638 apply (rule nn_integral_cong) 639 apply (subst emeasure_bind_prob_algebra[OF L[THEN measurable_space]]) 640 apply (simp_all add: ac_simps * nn_integral_cmult_indicator del: scylinder.simps) 641 apply measurable 642 done } 643 note emeasure_step = this 644 645 fix Xs assume "Xs \<in> lists (sets M)" 646 from this \<open>R A B\<close> show "emeasure A (scylinder (space M) Xs) = emeasure B (scylinder (space M) Xs)" 647 proof (induction Xs arbitrary: A B) 648 case (Cons X Xs) 649 obtain K A' B' where K: "K \<in> space (prob_algebra M)" 650 and A'[measurable]: "A' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" and A: "A = ?step K A'" 651 and B'[measurable]: "B' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" and B: "B = ?step K B'" 652 and AE_R: "AE x in K. R (A' x) (B' x) \<or> A' x = B' x" 653 using R[OF \<open>R A B\<close>] by blast 654 655 show ?case 656 unfolding A B emeasure_step[OF K Cons.hyps A'] emeasure_step[OF K Cons.hyps B'] 657 apply (rule nn_integral_cong_AE) 658 using AE_R by eventually_elim (auto simp add: Cons.IH) 659 next 660 case Nil 661 note R_D[OF this] 662 from this(1,2)[THEN prob_space.emeasure_space_1] this(3,4)[THEN sets_eq_imp_space_eq] 663 show ?case 664 by (simp add: space_stream_space) 665 qed 666qed 667 668end 669