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