Theory MDP_Aux

theory MDP_Aux
  imports "Markov_Models.Markov_Decision_Process"
begin

lemma sets_stream_space_cylinder: 
  "sets (stream_space M) = sigma_sets (streams (space M)) (scylinder (space M) ` lists (sets M))"
proof (rule antisym)
  have closed[simp]: "scylinder (space M) ` lists (sets M) ⊆ Pow (streams (space M))"
    using scylinder_streams[of "space M" _] by auto
  have [simp]: "(λs. s !! i) ∈ streams (space M) → space M" for i
    by (auto simp: snth_in)

  interpret sigma_algebra "streams (space M)" "sigma_sets (streams (space M)) (scylinder (space M) ` lists (sets M))"
    by (intro sigma_algebra_sigma_sets) fact

  have *: "(λs. s !! i) -` A ∩ streams (space M) = scylinder (space M) (replicate i (space M) @ [A])"
    if "A ∈ sets M" for i A
  proof (induction i)
    case (Suc n) show ?case
      apply (intro set_eqI)
      subgoal for ω by (cases ω) (auto simp: streams_Stream Suc[symmetric])
      done
  qed (auto simp: streams_stl)

  have "sets (stream_space M) ≤ sets (sigma (streams (space M)) (scylinder (space M) ` lists (sets M)))"
    unfolding sets_stream_space_eq
    by (rule sets_Sup_in_sets)
       (auto simp: sets_vimage_algebra2 PiE_UNIV_domain space_PiM * intro!: sigma_sets.Basic imageI)
  also have "… = sigma_sets (streams (space M)) (scylinder (space M) ` lists (sets M))"
    by (rule sets_measure_of) fact
  finally show "sets (stream_space M) ≤ sigma_sets (streams (space M)) (scylinder (space M) ` lists (sets M))" .
next
  show "sigma_sets (streams (space M)) (scylinder (space M) ` lists (sets M)) ⊆ sets (stream_space M)"
    unfolding space_stream_space[symmetric]
    by (rule sets.sigma_sets_subset) (auto intro!: sets_scylinder)
qed

end