src/HOL/Probability/Stream_Space.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 59092 d469103c0737
child 60172 423273355b55
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58606
9c66f7c541fb add Giry monad
hoelzl
parents: 58588
diff changeset
     1
(*  Title:      HOL/Probability/Stream_Space.thy
9c66f7c541fb add Giry monad
hoelzl
parents: 58588
diff changeset
     2
    Author:     Johannes Hölzl, TU München *)
9c66f7c541fb add Giry monad
hoelzl
parents: 58588
diff changeset
     3
58588
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
     4
theory Stream_Space
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
     5
imports
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
     6
  Infinite_Product_Measure
58607
1f90ea1b4010 move Stream theory from Datatype_Examples to Library
hoelzl
parents: 58606
diff changeset
     7
  "~~/src/HOL/Library/Stream"
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
     8
  "~~/src/HOL/Library/Linear_Temporal_Logic_on_Streams"
58588
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
     9
begin
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    10
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    11
lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    12
  by (cases s) simp
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    13
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    14
lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    15
  by (cases n) simp_all
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    16
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    17
definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    18
  "to_stream X = smap X nats"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    19
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    20
lemma to_stream_nat_case: "to_stream (case_nat x X) = x ## to_stream X"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    21
  unfolding to_stream_def
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    22
  by (subst siterate.ctr) (simp add: smap_siterate[symmetric] stream.map_comp comp_def)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    23
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
    24
lemma to_stream_in_streams: "to_stream X \<in> streams S \<longleftrightarrow> (\<forall>n. X n \<in> S)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
    25
  by (simp add: to_stream_def streams_iff_snth)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
    26
58588
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    27
definition stream_space :: "'a measure \<Rightarrow> 'a stream measure" where
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    28
  "stream_space M =
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    29
    distr (\<Pi>\<^sub>M i\<in>UNIV. M) (vimage_algebra (streams (space M)) snth (\<Pi>\<^sub>M i\<in>UNIV. M)) to_stream"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    30
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    31
lemma space_stream_space: "space (stream_space M) = streams (space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    32
  by (simp add: stream_space_def)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    33
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    34
lemma streams_stream_space[intro]: "streams (space M) \<in> sets (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    35
  using sets.top[of "stream_space M"] by (simp add: space_stream_space)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    36
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    37
lemma stream_space_Stream:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    38
  "x ## \<omega> \<in> space (stream_space M) \<longleftrightarrow> x \<in> space M \<and> \<omega> \<in> space (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    39
  by (simp add: space_stream_space streams_Stream)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    40
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    41
lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    42
  unfolding stream_space_def by (rule distr_cong) auto
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    43
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59000
diff changeset
    44
lemma sets_stream_space_cong[measurable_cong]:
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59000
diff changeset
    45
  "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
58588
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    46
  using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    47
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    48
lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    49
  by (auto intro!: measurable_vimage_algebra1
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    50
           simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    51
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    52
lemma measurable_snth[measurable]: "(\<lambda>\<omega>. \<omega> !! n) \<in> measurable (stream_space M) M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    53
  using measurable_snth_PiM measurable_component_singleton by (rule measurable_compose) simp
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    54
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    55
lemma measurable_shd[measurable]: "shd \<in> measurable (stream_space M) M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    56
  using measurable_snth[of 0] by simp
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    57
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    58
lemma measurable_stream_space2:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    59
  assumes f_snth: "\<And>n. (\<lambda>x. f x !! n) \<in> measurable N M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    60
  shows "f \<in> measurable N (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    61
  unfolding stream_space_def measurable_distr_eq2
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    62
proof (rule measurable_vimage_algebra2)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    63
  show "f \<in> space N \<rightarrow> streams (space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    64
    using f_snth[THEN measurable_space] by (auto simp add: streams_iff_sset sset_range)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    65
  show "(\<lambda>x. op !! (f x)) \<in> measurable N (Pi\<^sub>M UNIV (\<lambda>i. M))"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    66
  proof (rule measurable_PiM_single')
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    67
    show "(\<lambda>x. op !! (f x)) \<in> space N \<rightarrow> UNIV \<rightarrow>\<^sub>E space M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    68
      using f_snth[THEN measurable_space] by auto
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    69
  qed (rule f_snth)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    70
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    71
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    72
lemma measurable_stream_coinduct[consumes 1, case_names shd stl, coinduct set: measurable]:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    73
  assumes "F f"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    74
  assumes h: "\<And>f. F f \<Longrightarrow> (\<lambda>x. shd (f x)) \<in> measurable N M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    75
  assumes t: "\<And>f. F f \<Longrightarrow> F (\<lambda>x. stl (f x))"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    76
  shows "f \<in> measurable N (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    77
proof (rule measurable_stream_space2)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    78
  fix n show "(\<lambda>x. f x !! n) \<in> measurable N M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    79
    using `F f` by (induction n arbitrary: f) (auto intro: h t)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    80
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    81
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    82
lemma measurable_sdrop[measurable]: "sdrop n \<in> measurable (stream_space M) (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    83
  by (rule measurable_stream_space2) (simp add: sdrop_snth)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    84
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    85
lemma measurable_stl[measurable]: "(\<lambda>\<omega>. stl \<omega>) \<in> measurable (stream_space M) (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    86
  by (rule measurable_stream_space2) (simp del: snth.simps add: snth.simps[symmetric])
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    87
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    88
lemma measurable_to_stream[measurable]: "to_stream \<in> measurable (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    89
  by (rule measurable_stream_space2) (simp add: to_stream_def)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    90
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    91
lemma measurable_Stream[measurable (raw)]:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    92
  assumes f[measurable]: "f \<in> measurable N M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    93
  assumes g[measurable]: "g \<in> measurable N (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    94
  shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    95
  by (rule measurable_stream_space2) (simp add: Stream_snth)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    96
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    97
lemma measurable_smap[measurable]: 
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    98
  assumes X[measurable]: "X \<in> measurable N M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
    99
  shows "smap X \<in> measurable (stream_space N) (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   100
  by (rule measurable_stream_space2) simp
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   101
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   102
lemma measurable_stake[measurable]: 
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   103
  "stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   104
  by (induct i) auto
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   105
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   106
lemma measurable_shift[measurable]: 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   107
  assumes f: "f \<in> measurable N (stream_space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   108
  assumes [measurable]: "g \<in> measurable N (stream_space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   109
  shows "(\<lambda>x. stake n (f x) @- g x) \<in> measurable N (stream_space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   110
  using f by (induction n arbitrary: f) simp_all
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   111
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   112
lemma measurable_ev_at[measurable]:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   113
  assumes [measurable]: "Measurable.pred (stream_space M) P"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   114
  shows "Measurable.pred (stream_space M) (ev_at P n)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   115
  by (induction n) auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   116
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   117
lemma measurable_alw[measurable]:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   118
  "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (alw P)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   119
  unfolding alw_def
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   120
  by (coinduction rule: measurable_gfp_coinduct) (auto simp: Order_Continuity.down_continuous_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   121
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   122
lemma measurable_ev[measurable]:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   123
  "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (ev P)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   124
  unfolding ev_def
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   125
  by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   126
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   127
lemma measurable_until:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   128
  assumes [measurable]: "Measurable.pred (stream_space M) \<phi>" "Measurable.pred (stream_space M) \<psi>"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   129
  shows "Measurable.pred (stream_space M) (\<phi> until \<psi>)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   130
  unfolding UNTIL_def
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   131
  by (coinduction rule: measurable_gfp_coinduct) (simp_all add: down_continuous_def fun_eq_iff)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   132
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   133
lemma measurable_holds [measurable]: "Measurable.pred M P \<Longrightarrow> Measurable.pred (stream_space M) (holds P)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   134
  unfolding holds.simps[abs_def]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   135
  by (rule measurable_compose[OF measurable_shd]) simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   136
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   137
lemma measurable_hld[measurable]: assumes [measurable]: "t \<in> sets M" shows "Measurable.pred (stream_space M) (HLD t)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   138
  unfolding HLD_def by measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   139
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   140
lemma measurable_nxt[measurable (raw)]:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   141
  "Measurable.pred (stream_space M) P \<Longrightarrow> Measurable.pred (stream_space M) (nxt P)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   142
  unfolding nxt.simps[abs_def] by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   143
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   144
lemma measurable_suntil[measurable]:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   145
  assumes [measurable]: "Measurable.pred (stream_space M) Q" "Measurable.pred (stream_space M) P"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   146
  shows "Measurable.pred (stream_space M) (Q suntil P)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   147
  unfolding suntil_def by (coinduction rule: measurable_lfp_coinduct) (auto simp: Order_Continuity.continuous_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   148
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   149
lemma measurable_szip:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   150
  "(\<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))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   151
proof (rule measurable_stream_space2)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   152
  fix n
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   153
  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))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   154
    by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   155
  also have "\<dots> \<in> measurable (stream_space M \<Otimes>\<^sub>M stream_space N) (M \<Otimes>\<^sub>M N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   156
    by measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   157
  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)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   158
    .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   159
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   160
58588
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   161
lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   162
proof -
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   163
  interpret product_prob_space "\<lambda>_. M" UNIV by default
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   164
  show ?thesis
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   165
    by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   166
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   167
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   168
lemma (in prob_space) nn_integral_stream_space:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   169
  assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   170
  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)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   171
proof -                  
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   172
  interpret S: sequence_space M
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   173
    by default
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   174
  interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   175
    by default
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   176
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   177
  have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   178
    by (subst stream_space_eq_distr) (simp add: nn_integral_distr)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   179
  also have "\<dots> = (\<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)) \<partial>(M \<Otimes>\<^sub>M S.S))"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   180
    by (subst S.PiM_iter[symmetric]) (simp add: nn_integral_distr)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   181
  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)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   182
    by (subst S.nn_integral_fst) simp_all
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   183
  also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## to_stream X) \<partial>S.S \<partial>M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   184
    by (auto intro!: nn_integral_cong simp: to_stream_nat_case)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   185
  also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M \<partial>M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   186
    by (subst stream_space_eq_distr)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   187
       (simp add: nn_integral_distr cong: nn_integral_cong)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   188
  finally show ?thesis .
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   189
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   190
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   191
lemma (in prob_space) emeasure_stream_space:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   192
  assumes X[measurable]: "X \<in> sets (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   193
  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)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   194
proof -
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   195
  have eq: "\<And>x xs. xs \<in> space (stream_space M) \<Longrightarrow> x \<in> space M \<Longrightarrow>
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   196
      indicator X (x ## xs) = indicator {xs\<in>space (stream_space M). x ## xs \<in> X } xs"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   197
    by (auto split: split_indicator)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   198
  show ?thesis
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   199
    using nn_integral_stream_space[of "indicator X"]
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   200
    apply (auto intro!: nn_integral_cong)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   201
    apply (subst nn_integral_cong)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   202
    apply (rule eq)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   203
    apply simp_all
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   204
    done
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   205
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   206
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   207
lemma (in prob_space) prob_stream_space:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   208
  assumes P[measurable]: "{x\<in>space (stream_space M). P x} \<in> sets (stream_space M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   209
  shows "\<P>(x in stream_space M. P x) = (\<integral>\<^sup>+t. \<P>(x in stream_space M. P (t ## x)) \<partial>M)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   210
proof -
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   211
  interpret S: prob_space "stream_space M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   212
    by (rule prob_space_stream_space)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   213
  show ?thesis
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   214
    unfolding S.emeasure_eq_measure[symmetric]
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   215
    by (subst emeasure_stream_space) (auto simp: stream_space_Stream intro!: nn_integral_cong)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   216
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   217
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   218
lemma (in prob_space) AE_stream_space:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   219
  assumes [measurable]: "Measurable.pred (stream_space M) P"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   220
  shows "(AE X in stream_space M. P X) = (AE x in M. AE X in stream_space M. P (x ## X))"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   221
proof -
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   222
  interpret stream: prob_space "stream_space M"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   223
    by (rule prob_space_stream_space)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   224
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   225
  have eq: "\<And>x X. indicator {x. \<not> P x} (x ## X) = indicator {X. \<not> P (x ## X)} X"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   226
    by (auto split: split_indicator)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   227
  show ?thesis
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   228
    apply (subst AE_iff_nn_integral, simp)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   229
    apply (subst nn_integral_stream_space, simp)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   230
    apply (subst eq)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   231
    apply (subst nn_integral_0_iff_AE, simp)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   232
    apply (simp add: AE_iff_nn_integral[symmetric])
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   233
    done
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   234
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   235
  
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   236
lemma (in prob_space) AE_stream_all:
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   237
  assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   238
  shows "AE x in stream_space M. stream_all P x"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   239
proof -
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   240
  { fix n have "AE x in stream_space M. P (x !! n)"
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   241
    proof (induct n)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   242
      case 0 with P show ?case
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   243
        by (subst AE_stream_space) (auto elim!: eventually_elim1)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   244
    next
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   245
      case (Suc n) then show ?case
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   246
        by (subst AE_stream_space) auto
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   247
    qed }
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   248
  then show ?thesis
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   249
    unfolding stream_all_def by (simp add: AE_all_countable)
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   250
qed
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   251
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   252
lemma streams_sets:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   253
  assumes X[measurable]: "X \<in> sets M" shows "streams X \<in> sets (stream_space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   254
proof -
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   255
  have "streams X = {x\<in>space (stream_space M). x \<in> streams X}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   256
    using streams_mono[OF _ sets.sets_into_space[OF X]] by (auto simp: space_stream_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   257
  also have "\<dots> = {x\<in>space (stream_space M). gfp (\<lambda>p x. shd x \<in> X \<and> p (stl x)) x}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   258
    apply (simp add: set_eq_iff streams_def streamsp_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   259
    apply (intro allI conj_cong refl arg_cong2[where f=gfp] ext)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   260
    apply (case_tac xa)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   261
    apply auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   262
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   263
  also have "\<dots> \<in> sets (stream_space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   264
    apply (intro predE)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   265
    apply (coinduction rule: measurable_gfp_coinduct)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   266
    apply (auto simp: down_continuous_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   267
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   268
  finally show ?thesis .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   269
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   270
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   271
lemma sets_stream_space_in_sets:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   272
  assumes space: "space N = streams (space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   273
  assumes sets: "\<And>i. (\<lambda>x. x !! i) \<in> measurable N M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   274
  shows "sets (stream_space M) \<subseteq> sets N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   275
  unfolding stream_space_def sets_distr
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   276
  by (auto intro!: sets_image_in_sets measurable_Sup_sigma2 measurable_vimage_algebra2 del: subsetI equalityI 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   277
           simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   278
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   279
lemma sets_stream_space_eq: "sets (stream_space M) =
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   280
    sets (\<Squnion>\<^sub>\<sigma> i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   281
  by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   282
                   measurable_Sup_sigma1  snth_in measurable_vimage_algebra1 del: subsetI
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   283
           simp: space_Sup_sigma space_stream_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   284
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   285
lemma sets_restrict_stream_space:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   286
  assumes S[measurable]: "S \<in> sets M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   287
  shows "sets (restrict_space (stream_space M) (streams S)) = sets (stream_space (restrict_space M S))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   288
  using  S[THEN sets.sets_into_space]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   289
  apply (subst restrict_space_eq_vimage_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   290
  apply (simp add: space_stream_space streams_mono2)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   291
  apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   292
  apply (subst sets_stream_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   293
  apply (subst sets_vimage_Sup_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   294
  apply simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   295
  apply (auto intro: streams_mono) []
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   296
  apply (simp add: image_image space_restrict_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   297
  apply (intro SUP_sigma_cong)
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   298
  apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   299
  apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   300
  apply (auto simp: streams_mono snth_in)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   301
  done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   302
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   303
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   304
primrec sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" where
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   305
  "sstart S [] = streams S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   306
| [simp del]: "sstart S (x # xs) = op ## x ` sstart S xs"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   307
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   308
lemma in_sstart[simp]: "s \<in> sstart S (x # xs) \<longleftrightarrow> shd s = x \<and> stl s \<in> sstart S xs"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   309
  by (cases s) (auto simp: sstart.simps(2))
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   310
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   311
lemma sstart_in_streams: "xs \<in> lists S \<Longrightarrow> sstart S xs \<subseteq> streams S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   312
  by (induction xs) (auto simp: sstart.simps(2))
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   313
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   314
lemma sstart_eq: "x \<in> streams S \<Longrightarrow> x \<in> sstart S xs = (\<forall>i<length xs. x !! i = xs ! i)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   315
  by (induction xs arbitrary: x) (auto simp: nth_Cons streams_stl split: nat.splits)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   316
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   317
lemma sstart_sets: "sstart S xs \<in> sets (stream_space (count_space UNIV))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   318
proof (induction xs)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   319
  case (Cons x xs)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   320
  note Cons[measurable]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   321
  have "sstart S (x # xs) =
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   322
    {s\<in>space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   323
    by (simp add: set_eq_iff space_stream_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   324
  also have "\<dots> \<in> sets (stream_space (count_space UNIV))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   325
    by measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   326
  finally show ?case .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   327
qed (simp add: streams_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   328
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   329
lemma sigma_sets_singletons:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   330
  assumes "countable S"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   331
  shows "sigma_sets S ((\<lambda>s. {s})`S) = Pow S"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   332
proof safe
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   333
  interpret sigma_algebra S "sigma_sets S ((\<lambda>s. {s})`S)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   334
    by (rule sigma_algebra_sigma_sets) auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   335
  fix A assume "A \<subseteq> S"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   336
  with assms have "(\<Union>a\<in>A. {a}) \<in> sigma_sets S ((\<lambda>s. {s})`S)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   337
    by (intro countable_UN') (auto dest: countable_subset)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   338
  then show "A \<in> sigma_sets S ((\<lambda>s. {s})`S)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   339
    by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   340
qed (auto dest: sigma_sets_into_sp[rotated])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   341
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   342
lemma sets_count_space_eq_sigma:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   343
  "countable S \<Longrightarrow> sets (count_space S) = sets (sigma S ((\<lambda>s. {s})`S))"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   344
  by (subst sets_measure_of) (auto simp: sigma_sets_singletons)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   345
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   346
lemma sets_stream_space_sstart:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   347
  assumes S[simp]: "countable S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   348
  shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   349
proof
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   350
  have [simp]: "sstart S ` lists S \<subseteq> Pow (streams S)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   351
    by (simp add: image_subset_iff sstart_in_streams)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   352
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   353
  let ?S = "sigma (streams S) (sstart S ` lists S \<union> {{}})"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   354
  { fix i a assume "a \<in> S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   355
    { 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]))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   356
      proof (induction i arbitrary: x)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   357
        case (Suc i) from this[of "stl x"] show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   358
          by (simp add: length_Suc_conv Bex_def ex_simps[symmetric] del: ex_simps)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   359
             (metis stream.collapse streams_Stream)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   360
      qed (insert `a \<in> S`, auto intro: streams_stl in_streams) }
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   361
    then have "(\<lambda>x. x !! i) -` {a} \<inter> streams S = (\<Union>xs\<in>{xs\<in>lists S. length xs = i}. sstart S (xs @ [a]))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   362
      by (auto simp add: set_eq_iff)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   363
    also have "\<dots> \<in> sets ?S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   364
      using `a\<in>S` by (intro sets.countable_UN') (auto intro!: sigma_sets.Basic image_eqI)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   365
    finally have " (\<lambda>x. x !! i) -` {a} \<inter> streams S \<in> sets ?S" . }
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   366
  then show "sets (stream_space (count_space S)) \<subseteq> sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   367
    by (intro sets_stream_space_in_sets) (auto simp: measurable_count_space_eq_countable snth_in)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   368
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   369
  have "sigma_sets (space (stream_space (count_space S))) (sstart S`lists S \<union> {{}}) \<subseteq> sets (stream_space (count_space S))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   370
  proof (safe intro!: sets.sigma_sets_subset)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   371
    fix xs assume "\<forall>x\<in>set xs. x \<in> S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   372
    then have "sstart S xs = {x\<in>space (stream_space (count_space S)). \<forall>i<length xs. x !! i = xs ! i}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   373
      by (induction xs)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   374
         (auto simp: space_stream_space nth_Cons split: nat.split intro: in_streams streams_stl)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   375
    also have "\<dots> \<in> sets (stream_space (count_space S))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   376
      by measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   377
    finally show "sstart S xs \<in> sets (stream_space (count_space S))" .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   378
  qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   379
  then show "sets (sigma (streams S) (sstart S`lists S \<union> {{}})) \<subseteq> sets (stream_space (count_space S))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   380
    by (simp add: space_stream_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   381
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   382
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   383
lemma Int_stable_sstart: "Int_stable (sstart S`lists S \<union> {{}})"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   384
proof -
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   385
  { fix xs ys assume "xs \<in> lists S" "ys \<in> lists S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   386
    then have "sstart S xs \<inter> sstart S ys \<in> sstart S ` lists S \<union> {{}}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   387
    proof (induction xs ys rule: list_induct2')
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   388
      case (4 x xs y ys)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   389
      show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   390
      proof cases
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   391
        assume "x = y"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   392
        then have "sstart S (x # xs) \<inter> sstart S (y # ys) = op ## x ` (sstart S xs \<inter> sstart S ys)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   393
          by (auto simp: image_iff intro!: stream.collapse[symmetric])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   394
        also have "\<dots> \<in> sstart S ` lists S \<union> {{}}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   395
          using 4 by (auto simp: sstart.simps(2)[symmetric] del: in_listsD)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   396
        finally show ?case .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   397
      qed auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   398
    qed (simp_all add: sstart_in_streams inf.absorb1 inf.absorb2 image_eqI[where x="[]"]) }
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   399
  then show ?thesis
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   400
    by (auto simp: Int_stable_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   401
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   402
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   403
lemma stream_space_eq_sstart:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   404
  assumes S[simp]: "countable S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   405
  assumes P: "prob_space M" "prob_space N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   406
  assumes ae: "AE x in M. x \<in> streams S" "AE x in N. x \<in> streams S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   407
  assumes sets_M: "sets M = sets (stream_space (count_space UNIV))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   408
  assumes sets_N: "sets N = sets (stream_space (count_space UNIV))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   409
  assumes *: "\<And>xs. xs \<noteq> [] \<Longrightarrow> xs \<in> lists S \<Longrightarrow> emeasure M (sstart S xs) = emeasure N (sstart S xs)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   410
  shows "M = N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   411
proof (rule measure_eqI_restrict_generator[OF Int_stable_sstart])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   412
  have [simp]: "sstart S ` lists S \<subseteq> Pow (streams S)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   413
    by (simp add: image_subset_iff sstart_in_streams)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   414
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   415
  interpret M: prob_space M by fact
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   416
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   417
  show "sstart S ` lists S \<union> {{}} \<subseteq> Pow (streams S)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   418
    by (auto dest: sstart_in_streams del: in_listsD)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   419
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   420
  { fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   421
    have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   422
      by (subst sets_restrict_space_cong[OF M])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   423
         (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart) }
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   424
  from this[OF sets_M] this[OF sets_N]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   425
  show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   426
       "sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   427
    by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   428
  show "{streams S} \<subseteq> sstart S ` lists S \<union> {{}}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   429
    "\<Union>{streams S} = streams S" "\<And>s. s \<in> {streams S} \<Longrightarrow> emeasure M s \<noteq> \<infinity>"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   430
    using M.emeasure_space_1 space_stream_space[of "count_space S"] sets_eq_imp_space_eq[OF sets_M]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   431
    by (auto simp add: image_eqI[where x="[]"])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   432
  show "sets M = sets N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   433
    by (simp add: sets_M sets_N)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   434
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   435
  fix X assume "X \<in> sstart S ` lists S \<union> {{}}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   436
  then obtain xs where "X = {} \<or> (xs \<in> lists S \<and> X = sstart S xs)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   437
    by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   438
  moreover have "emeasure M (streams S) = 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   439
    using ae by (intro prob_space.emeasure_eq_1_AE[OF P(1)]) (auto simp: sets_M streams_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   440
  moreover have "emeasure N (streams S) = 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   441
    using ae by (intro prob_space.emeasure_eq_1_AE[OF P(2)]) (auto simp: sets_N streams_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   442
  ultimately show "emeasure M X = emeasure N X"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   443
    using P[THEN prob_space.emeasure_space_1]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   444
    by (cases "xs = []") (auto simp: * space_stream_space del: in_listsD)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   445
qed (auto simp: * ae sets_M del: in_listsD intro!: streams_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58607
diff changeset
   446
58588
93d87fd1583d add measure space for (coinductive) streams
hoelzl
parents:
diff changeset
   447
end