Quellcode-Bibliothek Stream_Space.thy   Sprache: Isabelle

(x in stream_space M. P x) = (\\<^sup>+t. \

(x in stream_space M. P (t ## x)) \M)"
proof -
  interpret S: prob_space "stream_space M"
    by (rule prob_space_stream_space)
  show ?thesis
    unfolding S.emeasure_eq_measure[symmetric]
    by (subst emeasure_stream_space) (auto simp: stream_space_Stream intro!: nn_integral_cong)
qed

lemma (in prob_space) AE_stream_space:
  assumes [measurable]: "Measurable.pred (stream_space M) P"
  shows "(AE X in stream_space M. P X) = (AE x in M. AE X in stream_space M. P (x ## X))"
proof -
  interpret stream: prob_space "stream_space M"
    by (rule prob_space_stream_space)

  have eq: "\x X. indicator {x. \ P x} (x ## X) = indicator {X. \ P (x ## X)} X"
    by (auto split: split_indicator)
  show ?thesis
    apply (subst AE_iff_nn_integral, simp)
    apply (subst nn_integral_stream_space, simp)
    apply (subst eq)
    apply (subst nn_integral_0_iff_AE, simp)
    apply (simp add: AE_iff_nn_integral[symmetric])
    done
qed

lemma (in prob_space) AE_stream_all:
  assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x"
  shows "AE x in stream_space M. stream_all P x"
proof -
  { fix n have "AE x in stream_space M. P (x !! n)"
    proof (induct n)
      case 0 with P show ?case
        by (subst AE_stream_space) (auto elim!: eventually_mono)
    next
      case (Suc n) then show ?case
        by (subst AE_stream_space) auto
    qed }
  then show ?thesis
    unfolding stream_all_def by (simp add: AE_all_countable)
qed

lemma streams_sets:
  assumes X[measurable]: "X \ sets M" shows "streams X \ sets (stream_space M)"
proof -
  have "streams X = {x\space (stream_space M). x \ streams X}"
    using streams_mono[OF _ sets.sets_into_space[OF X]] by (auto simp: space_stream_space)
  also have "\ = {x\space (stream_space M). gfp (\p x. shd x \ X \ p (stl x)) x}"
    apply (simp add: set_eq_iff streams_def streamsp_def)
    apply (intro allI conj_cong refl arg_cong2[where f=gfp] ext)
    apply (case_tac xa)
    apply auto
    done
  also have "\ \ sets (stream_space M)"
    apply (intro predE)
    apply (coinduction rule: measurable_gfp_coinduct)
    apply (auto simp: inf_continuous_def)
    done
  finally show ?thesis .
qed

lemma sets_stream_space_in_sets:
  assumes space: "space N = streams (space M)"
  assumes sets: "\i. (\x. x !! i) \ measurable N M"
  shows "sets (stream_space M) \ sets N"
  unfolding stream_space_def sets_distr
  by (auto intro!: sets_image_in_sets measurable_Sup2 measurable_vimage_algebra2 del: subsetI equalityI
           simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)

lemma sets_stream_space_eq: "sets (stream_space M) =
    sets (SUP i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
  by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
                   measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI
           simp: space_Sup_eq_UN space_stream_space)

lemma sets_restrict_stream_space:
  assumes S[measurable]: "S \ sets M"
  shows "sets (restrict_space (stream_space M) (streams S)) = sets (stream_space (restrict_space M S))"
  using  S[THEN sets.sets_into_space]
  apply (subst restrict_space_eq_vimage_algebra)
  apply (simp add: space_stream_space streams_mono2)
  apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
  apply (subst sets_stream_space_eq)
  apply (subst sets_vimage_Sup_eq[where Y="streams (space M)"])
  apply simp
  apply auto []
  apply (auto intro: streams_mono) []
  apply auto []
  apply (simp add: image_image space_restrict_space)
  apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
  apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
  apply (auto simp: streams_mono snth_in )
  done

primrec sstart :: "'a set \ 'a list \ 'a stream set" where
  "sstart S [] = streams S"
| [simp del]: "sstart S (x # xs) = (##) x ` sstart S xs"

lemma in_sstart[simp]: "s \ sstart S (x # xs) \ shd s = x \ stl s \ sstart S xs"
  by (cases s) (auto simp: sstart.simps(2))

lemma sstart_in_streams: "xs \ lists S \ sstart S xs \ streams S"
  by (induction xs) (auto simp: sstart.simps(2))

lemma sstart_eq: "x \ streams S \ x \ sstart S xs = (\i
  by (induction xs arbitrary: x) (auto simp: nth_Cons streams_stl split: nat.splits)

lemma sstart_sets: "sstart S xs \ sets (stream_space (count_space UNIV))"
proof (induction xs)
  case (Cons x xs)
  note Cons[measurable]
  have "sstart S (x # xs) =
    {s\<in>space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}"
    by (simp add: set_eq_iff space_stream_space)
  also have "\ \ sets (stream_space (count_space UNIV))"
    by measurable
  finally show ?case .
qed (simp add: streams_sets)

lemma sigma_sets_singletons:
  assumes "countable S"
  shows "sigma_sets S ((\s. {s})`S) = Pow S"
proof safe
  interpret sigma_algebra S "sigma_sets S ((\s. {s})`S)"
    by (rule sigma_algebra_sigma_sets) auto
  fix A assume "A \ S"
  with assms have "(\a\A. {a}) \ sigma_sets S ((\s. {s})`S)"
    by (intro countable_UN') (auto dest: countable_subset)
  then show "A \ sigma_sets S ((\s. {s})`S)"
    by simp
qed (auto dest: sigma_sets_into_sp[rotated])

lemma sets_count_space_eq_sigma:
  "countable S \ sets (count_space S) = sets (sigma S ((\s. {s})`S))"
  by (subst sets_measure_of) (auto simp: sigma_sets_singletons)

lemma sets_stream_space_sstart:
  assumes S[simp]: "countable S"
  shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \ {{}}))"
proof
  have [simp]: "sstart S ` lists S \ Pow (streams S)"
    by (simp add: image_subset_iff sstart_in_streams)

  let ?S = "sigma (streams S) (sstart S ` lists S \ {{}})"
  { fix i a assume "a \ S"
    { fix x have "(x !! i = a \ x \ streams S) \ (\xs\lists S. length xs = i \ x \ sstart S (xs @ [a]))"
      proof (induction i arbitrary: x)
        case (Suc i) from this[of "stl x"] show ?case
          by (simp add: length_Suc_conv Bex_def ex_simps[symmetric] del: ex_simps)
             (metis stream.collapse streams_Stream)
      qed (insert \<open>a \<in> S\<close>, auto intro: streams_stl in_streams) }
    then have "(\x. x !! i) -` {a} \ streams S = (\xs\{xs\lists S. length xs = i}. sstart S (xs @ [a]))"
      by (auto simp add: set_eq_iff)
    also have "\ \ sets ?S"
      using \<open>a\<in>S\<close> by (intro sets.countable_UN') (auto intro!: sigma_sets.Basic image_eqI)
    finally have " (\x. x !! i) -` {a} \ streams S \ sets ?S" . }
  then show "sets (stream_space (count_space S)) \ sets (sigma (streams S) (sstart S`lists S \ {{}}))"
    by (intro sets_stream_space_in_sets) (auto simp: measurable_count_space_eq_countable snth_in)

  have "sigma_sets (space (stream_space (count_space S))) (sstart S`lists S \ {{}}) \ sets (stream_space (count_space S))"
  proof (safe intro!: sets.sigma_sets_subset)
    fix xs assume "\x\set xs. x \ S"
    then have "sstart S xs = {x\space (stream_space (count_space S)). \i
      by (induction xs)
         (auto simp: space_stream_space nth_Cons split: nat.split intro: in_streams streams_stl)
    also have "\ \ sets (stream_space (count_space S))"
      by measurable
    finally show "sstart S xs \ sets (stream_space (count_space S))" .
  qed
  then show "sets (sigma (streams S) (sstart S`lists S \ {{}})) \ sets (stream_space (count_space S))"
    by (simp add: space_stream_space)
qed

lemma Int_stable_sstart: "Int_stable (sstart S`lists S \ {{}})"
proof -
  { fix xs ys assume "xs \ lists S" "ys \ lists S"
    then have "sstart S xs \ sstart S ys \ sstart S ` lists S \ {{}}"
    proof (induction xs ys rule: list_induct2')
      case (4 x xs y ys)
      show ?case
      proof cases
        assume "x = y"
        then have "sstart S (x # xs) \ sstart S (y # ys) = (##) x ` (sstart S xs \ sstart S ys)"
          by (auto simp: image_iff intro!: stream.collapse[symmetric])
        also have "\ \ sstart S ` lists S \ {{}}"
          using 4 by (auto simp: sstart.simps(2)[symmetric] del: in_listsD)
        finally show ?case .
      qed auto
    qed (simp_all add: sstart_in_streams inf.absorb1 inf.absorb2 image_eqI[where x="[]"]) }
  then show ?thesis
    by (auto simp: Int_stable_def)
qed

lemma stream_space_eq_sstart:
  assumes S[simp]: "countable S"
  assumes P: "prob_space M" "prob_space N"
  assumes ae: "AE x in M. x \ streams S" "AE x in N. x \ streams S"
  assumes sets_M: "sets M = sets (stream_space (count_space UNIV))"
  assumes sets_N: "sets N = sets (stream_space (count_space UNIV))"
  assumes *: "\xs. xs \ [] \ xs \ lists S \ emeasure M (sstart S xs) = emeasure N (sstart S xs)"
  shows "M = N"
proof (rule measure_eqI_restrict_generator[OF Int_stable_sstart])
  have [simp]: "sstart S ` lists S \ Pow (streams S)"
    by (simp add: image_subset_iff sstart_in_streams)

  interpret M: prob_space M by fact

  show "sstart S ` lists S \ {{}} \ Pow (streams S)"
    by (auto dest: sstart_in_streams del: in_listsD)

  { fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))"
    have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \ {{}})"
      by (subst sets_restrict_space_cong[OF M])
         (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart) }
  from this[OF sets_M] this[OF sets_N]
  show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \ {{}})"
       "sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \ {{}})"
    by auto
  show "{streams S} \ sstart S ` lists S \ {{}}"
    "\{streams S} = streams S" "\s. s \ {streams S} \ emeasure M s \ \"
    using M.emeasure_space_1 space_stream_space[of "count_space S"] sets_eq_imp_space_eq[OF sets_M]
    by (auto simp add: image_eqI[where x="[]"])
  show "sets M = sets N"
    by (simp add: sets_M sets_N)
next
  fix X assume "X \ sstart S ` lists S \ {{}}"
  then obtain xs where "X = {} \ (xs \ lists S \ X = sstart S xs)"
    by auto
  moreover have "emeasure M (streams S) = 1"
    using ae by (intro prob_space.emeasure_eq_1_AE[OF P(1)]) (auto simp: sets_M streams_sets)
  moreover have "emeasure N (streams S) = 1"
    using ae by (intro prob_space.emeasure_eq_1_AE[OF P(2)]) (auto simp: sets_N streams_sets)
  ultimately show "emeasure M X = emeasure N X"
    using P[THEN prob_space.emeasure_space_1]
    by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)

lemma sets_sstart[measurable]: "sstart \ xs \ sets (stream_space (count_space UNIV))"
proof (induction xs)
  case (Cons x xs)
  note this[measurable]
  have "sstart \ (x # xs) = {\\space (stream_space (count_space UNIV)). \ \ sstart \ (x # xs)}"
    by (auto simp: space_stream_space)
  also have "\ \ sets (stream_space (count_space UNIV))"
    unfolding in_sstart by measurable
  finally show ?case .
qed (auto intro!: streams_sets)

primrec scylinder :: "'a set \ 'a set list \ 'a stream set"
where
  "scylinder S [] = streams S"
| "scylinder S (A # As) = {\\streams S. shd \ \ A \ stl \ \ scylinder S As}"

lemma scylinder_streams: "scylinder S xs \ streams S"
  by (induction xs) auto

lemma sets_scylinder: "(\x\set xs. x \ sets S) \ scylinder (space S) xs \ sets (stream_space S)"
  by (induction xs) (auto simp: space_stream_space[symmetric])

lemma stream_space_eq_scylinder:
  assumes P: "prob_space M" "prob_space N"
  assumes "Int_stable G" and S: "sets S = sets (sigma (space S) G)"
    and C: "countable C" "C \ G" "\C = space S" and G: "G \ Pow (space S)"
  assumes sets_M: "sets M = sets (stream_space S)"
  assumes sets_N: "sets N = sets (stream_space S)"
  assumes *: "\xs. xs \ [] \ xs \ lists G \ emeasure M (scylinder (space S) xs) = emeasure N (scylinder (space S) xs)"
  shows "M = N"
proof (rule measure_eqI_generator_eq)
  interpret M: prob_space M by fact
  interpret N: prob_space N by fact

  let ?G = "scylinder (space S) ` lists G"
  show sc_Pow: "?G \ Pow (streams (space S))"
    using scylinder_streams by auto

  have "sets (stream_space S) = sets (sigma (streams (space S)) ?G)"
    (is "?S = sets ?R")
  proof (rule antisym)
    let ?V = "\i. vimage_algebra (streams (space S)) (\s. s !! i) S"
    show "?S \ sets ?R"
      unfolding sets_stream_space_eq
    proof (safe intro!: sets_Sup_in_sets del: subsetI equalityI)
      fix i :: nat
      show "space (?V i) = space ?R"
        using scylinder_streams by (subst space_measure_of) auto
      { fix A assume "A \ G"
        then have "scylinder (space S) (replicate i (space S) @ [A]) = (\s. s !! i) -` A \ streams (space S)"
          by (induction i) (auto simp add: streams_shd streams_stl cong: conj_cong)
        also have "scylinder (space S) (replicate i (space S) @ [A]) = (\xs\{xs\lists C. length xs = i}. scylinder (space S) (xs @ [A]))"
          apply (induction i)
          apply auto []
          apply (simp add: length_Suc_conv set_eq_iff ex_simps(1,2)[symmetric] cong: conj_cong del: ex_simps(1,2))
          apply rule
          subgoal for i x
            apply (cases x)
            apply (subst (2) C(3)[symmetric])
            apply (simp del: ex_simps(1,2) add: ex_simps(1,2)[symmetric] ac_simps Bex_def)
            apply auto
            done
          done
        finally have "(\s. s !! i) -` A \ streams (space S) = (\xs\{xs\lists C. length xs = i}. scylinder (space S) (xs @ [A]))"
          ..
        also have "\ \ ?R"
          using C(2) \<open>A\<in>G\<close>
          by (intro sets.countable_UN' countable_Collect countable_lists C)
             (auto intro!: in_measure_of[OF sc_Pow] imageI)
        finally have "(\s. s !! i) -` A \ streams (space S) \ ?R" . }
      then show "sets (?V i) \ ?R"
        apply (subst vimage_algebra_cong[OF refl refl S])
        apply (subst vimage_algebra_sigma[OF G])
        apply (simp add: streams_iff_snth) []
        apply (subst sigma_le_sets)
        apply auto
        done
    qed
    have "G \ sets S"
      unfolding S using G by auto
    with C(2) show "sets ?R \ ?S"
      unfolding sigma_le_sets[OF sc_Pow] by (auto intro!: sets_scylinder)
  qed
  then show "sets M = sigma_sets (streams (space S)) (scylinder (space S) ` lists G)"
    "sets N = sigma_sets (streams (space S)) (scylinder (space S) ` lists G)"
    unfolding sets_M sets_N by (simp_all add: sc_Pow)

  show "Int_stable ?G"
  proof (rule Int_stableI_image)
    fix xs ys assume "xs \ lists G" "ys \ lists G"
    then show "\zs\lists G. scylinder (space S) xs \ scylinder (space S) ys = scylinder (space S) zs"
    proof (induction xs arbitrary: ys)
      case Nil then show ?case
        by (auto simp add: Int_absorb1 scylinder_streams)
    next
      case xs: (Cons x xs)
      show ?case
      proof (cases ys)
        case Nil with xs.hyps show ?thesis
          by (auto simp add: Int_absorb2 scylinder_streams intro!: bexI[of _ "x#xs"])
      next
        case ys: (Cons y ys')
        with xs.IH[of ys'] xs.prems obtain zs where
          "zs \ lists G" and eq: "scylinder (space S) xs \ scylinder (space S) ys' = scylinder (space S) zs"
          by auto
        show ?thesis
        proof (intro bexI[of _ "(x \ y)#zs"])
          show "x \ y # zs \ lists G"
            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
          show "scylinder (space S) (x # xs) \ scylinder (space S) ys = scylinder (space S) (x \ y # zs)"
            by (auto simp add: eq[symmetric] ys)
        qed
      qed
    qed
  qed

  show "range (\_::nat. streams (space S)) \ scylinder (space S) ` lists G"
    "(\i. streams (space S)) = streams (space S)"
    "emeasure M (streams (space S)) \ \"
    by (auto intro!: image_eqI[of _ _ "[]"])

  fix X assume "X \ scylinder (space S) ` lists G"
  then obtain xs where xs: "xs \ lists G" and eq: "X = scylinder (space S) xs"
    by auto
  then show "emeasure M X = emeasure N X"
  proof (cases "xs = []")
    assume "xs = []" then show ?thesis
      unfolding eq
      using sets_M[THEN sets_eq_imp_space_eq] sets_N[THEN sets_eq_imp_space_eq]
         M.emeasure_space_1 N.emeasure_space_1
      by (simp add: space_stream_space[symmetric])
  next
    assume "xs \ []" with xs show ?thesis
      unfolding eq by (intro *)
  qed
qed

lemma stream_space_coinduct:
  fixes R :: "'a stream measure \ 'a stream measure \ bool"
  assumes "R A B"
  assumes R: "\A B. R A B \ \K\space (prob_algebra M).
    \<exists>A'\<in>M \<rightarrow>\<^sub>M prob_algebra (stream_space M). \<exists>B'\<in>M \<rightarrow>\<^sub>M prob_algebra (stream_space M).
    (AE y in K. R (A' y) (B' y) \<or> A' y = B' y) \<and>
    A = do { y \<leftarrow> K; \<omega> \<leftarrow> A' y; return (stream_space M) (y ## \<omega>) } \<and>
    B = do { y \<leftarrow> K; \<omega> \<leftarrow> B' y; return (stream_space M) (y ## \<omega>) }"
  shows "A = B"
proof (rule stream_space_eq_scylinder)
  let ?step = "\K L. do { y \ K; \ \ L y; return (stream_space M) (y ## \) }"
  { fix K A A' assume K: "K \ space (prob_algebra M)"
      and A'[measurable]: "A' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" and A_eq: "A = ?step K A'"
    have ps: "prob_space A"
      unfolding A_eq by (rule prob_space_bind'[OF K]) measurable
    have "sets A = sets (stream_space M)"
      unfolding A_eq by (rule sets_bind'[OF K]) measurable
    note ps this }
  note ** = this

  { fix A B assume "R A B"
    obtain K A' B' where K: "K \ space (prob_algebra M)"
      and A': "A' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" "A = ?step K A'"
      and B': "B' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" "B = ?step K B'"
      using R[OF \<open>R A B\<close>] by blast
    have "prob_space A" "prob_space B" "sets A = sets (stream_space M)" "sets B = sets (stream_space M)"
      using **[OF K A'] **[OF K B'] by auto }
  note R_D = this

  show "prob_space A" "prob_space B" "sets A = sets (stream_space M)" "sets B = sets (stream_space M)"
    using R_D[OF \<open>R A B\<close>] by auto

  show "Int_stable (sets M)" "sets M = sets (sigma (space M) (sets M))" "countable {space M}"
    "{space M} \ sets M" "\{space M} = space M" "sets M \ Pow (space M)"
    using sets.space_closed[of M] by (auto simp: Int_stable_def)

  { fix A As L K assume K[measurable]: "K \ space (prob_algebra M)" and A: "A \ sets M" "As \ lists (sets M)"
      and L[measurable]: "L \ M \\<^sub>M prob_algebra (stream_space M)"
    from A have [measurable]: "\x\set (A # As). x \ sets M" "\x\set As. x \ sets M"
      by auto
    have [simp]: "space K = space M" "sets K = sets M"
      using K by (auto simp: space_prob_algebra intro!: sets_eq_imp_space_eq)
    have [simp]: "x \ space M \ sets (L x) = sets (stream_space M)" for x
      using measurable_space[OF L] by (auto simp: space_prob_algebra)
    note sets_scylinder[measurable]
    have *: "indicator (scylinder (space M) (A # As)) (x ## \) =
        (indicator A x * indicator (scylinder (space M) As) \<omega> :: ennreal)" for \<omega> x
      using scylinder_streams[of "space M" As] \<open>A \<in> sets M\<close>[THEN sets.sets_into_space]
      by (auto split: split_indicator)
    have "emeasure (?step K L) (scylinder (space M) (A # As)) = (\\<^sup>+y. L y (scylinder (space M) As) * indicator A y \K)"
      apply (subst emeasure_bind_prob_algebra[OF K])
      apply measurable
      apply (rule nn_integral_cong)
      apply (subst emeasure_bind_prob_algebra[OF L[THEN measurable_space]])
      apply (simp_all add: ac_simps * nn_integral_cmult_indicator del: scylinder.simps)
      apply measurable
      done }
  note emeasure_step = this

  fix Xs assume "Xs \ lists (sets M)"
  from this \<open>R A B\<close> show "emeasure A (scylinder (space M) Xs) = emeasure B (scylinder (space M) Xs)"
  proof (induction Xs arbitrary: A B)
    case (Cons X Xs)
    obtain K A' B' where K: "K \ space (prob_algebra M)"
      and A'[measurable]: "A' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" and A: "A = ?step K A'"
      and B'[measurable]: "B' \<in> M \<rightarrow>\<^sub>M prob_algebra (stream_space M)" and B: "B = ?step K B'"
      and AE_R: "AE x in K. R (A' x) (B' x) \ A' x = B' x"
      using R[OF \<open>R A B\<close>] by blast

    show ?case
      unfolding A B emeasure_step[OF K Cons.hyps A'] emeasure_step[OF K Cons.hyps B']
      apply (rule nn_integral_cong_AE)
      using AE_R by eventually_elim (auto simp add: Cons.IH)
  next
    case Nil
    note R_D[OF this]
    from this(1,2)[THEN prob_space.emeasure_space_1] this(3,4)[THEN sets_eq_imp_space_eq]
    show ?case
      by (simp add: space_stream_space)
  qed
qed

end

quality100%