src/HOL/Probability/Stream_Space.thy
author hoelzl
Thu Oct 20 18:41:59 2016 +0200 (2016-10-20)
changeset 64320 ba194424b895
parent 64008 17a20ca86d62
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
HOL-Probability: move stopping time from AFP/Markov_Models
     1 (*  Title:      HOL/Probability/Stream_Space.thy
     2     Author:     Johannes Hölzl, TU München *)
     3 
     4 theory Stream_Space
     5 imports
     6   Infinite_Product_Measure
     7   "~~/src/HOL/Library/Stream"
     8   "~~/src/HOL/Library/Linear_Temporal_Logic_on_Streams"
     9 begin
    10 
    11 lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
    12   by (cases s) simp
    13 
    14 lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)"
    15   by (cases n) simp_all
    16 
    17 definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where
    18   "to_stream X = smap X nats"
    19 
    20 lemma 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 
    24 lemma 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 
    27 definition 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 
    31 lemma space_stream_space: "space (stream_space M) = streams (space M)"
    32   by (simp add: stream_space_def)
    33 
    34 lemma 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 
    37 lemma 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 
    41 lemma 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 
    44 lemma 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 
    48 lemma 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 
    52 lemma 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 
    55 lemma measurable_shd[measurable]: "shd \<in> measurable (stream_space M) M"
    56   using measurable_snth[of 0] by simp
    57 
    58 lemma 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
    62 proof (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. op !! (f x)) \<in> measurable N (Pi\<^sub>M UNIV (\<lambda>i. M))"
    66   proof (rule measurable_PiM_single')
    67     show "(\<lambda>x. op !! (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)
    70 qed
    71 
    72 lemma 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)"
    77 proof (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)
    80 qed
    81 
    82 lemma measurable_sdrop[measurable]: "sdrop n \<in> measurable (stream_space M) (stream_space M)"
    83   by (rule measurable_stream_space2) (simp add: sdrop_snth)
    84 
    85 lemma 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 
    88 lemma 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 
    91 lemma 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 
    97 lemma 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 
   102 lemma 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 
   106 lemma 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 
   112 lemma 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 
   116 lemma 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 
   121 lemma 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 
   126 lemma 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 
   131 lemma 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 
   137 lemma 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 
   141 lemma measurable_hld[measurable]: assumes [measurable]: "t \<in> sets M" shows "Measurable.pred (stream_space M) (HLD t)"
   142   unfolding HLD_def by measurable
   143 
   144 lemma 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 
   148 lemma 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 
   153 lemma 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))"
   155 proof (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     .
   163 qed
   164 
   165 lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
   166 proof -
   167   interpret product_prob_space "\<lambda>_. M" UNIV ..
   168   show ?thesis
   169     by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr)
   170 qed
   171 
   172 lemma (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)"
   175 proof -
   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 .
   191 qed
   192 
   193 lemma (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)"
   196 proof -
   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
   207 qed
   208 
   209 lemma (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)"
   212 proof -
   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)
   218 qed
   219 
   220 lemma (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))"
   223 proof -
   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
   236 qed
   237 
   238 lemma (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"
   241 proof -
   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)
   252 qed
   253 
   254 lemma streams_sets:
   255   assumes X[measurable]: "X \<in> sets M" shows "streams X \<in> sets (stream_space M)"
   256 proof -
   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 .
   271 qed
   272 
   273 lemma 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 
   281 lemma sets_stream_space_eq: "sets (stream_space M) =
   282     sets (SUP i: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 
   287 lemma 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 
   306 primrec sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" where
   307   "sstart S [] = streams S"
   308 | [simp del]: "sstart S (x # xs) = op ## x ` sstart S xs"
   309 
   310 lemma 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 
   313 lemma sstart_in_streams: "xs \<in> lists S \<Longrightarrow> sstart S xs \<subseteq> streams S"
   314   by (induction xs) (auto simp: sstart.simps(2))
   315 
   316 lemma 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 
   319 lemma sstart_sets: "sstart S xs \<in> sets (stream_space (count_space UNIV))"
   320 proof (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 .
   329 qed (simp add: streams_sets)
   330 
   331 lemma sigma_sets_singletons:
   332   assumes "countable S"
   333   shows "sigma_sets S ((\<lambda>s. {s})`S) = Pow S"
   334 proof 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
   342 qed (auto dest: sigma_sets_into_sp[rotated])
   343 
   344 lemma 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 
   348 lemma 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> {{}}))"
   351 proof
   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)
   383 qed
   384 
   385 lemma Int_stable_sstart: "Int_stable (sstart S`lists S \<union> {{}})"
   386 proof -
   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) = op ## 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)
   403 qed
   404 
   405 lemma 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"
   413 proof (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)
   436 next
   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)
   447 qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
   448 
   449 lemma sets_sstart[measurable]: "sstart \<Omega> xs \<in> sets (stream_space (count_space UNIV))"
   450 proof (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 .
   458 qed (auto intro!: streams_sets)
   459 
   460 primrec scylinder :: "'a set \<Rightarrow> 'a set list \<Rightarrow> 'a stream set"
   461 where
   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 
   465 lemma scylinder_streams: "scylinder S xs \<subseteq> streams S"
   466   by (induction xs) auto
   467 
   468 lemma 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 
   471 lemma 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"
   479 proof (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
   584 qed
   585 
   586 lemma 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"
   595 proof (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
   666 qed
   667 
   668 end