[STATEMENT]
lemma Zp_nth_root_lemma:
  assumes "a \<in> carrier Zp"
  assumes "a \<noteq> \<one>"
  assumes "n > 1"
  assumes "val_Zp (\<one> \<ominus> a) > 2*val_Zp ([(n::nat)]\<cdot> \<one>)"
  shows "\<exists> b \<in> carrier Zp. b[^]n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
obtain f where f_def: "f = monom Zp_x \<one> n \<oplus>\<^bsub>Zp_x\<^esub> monom Zp_x (\<ominus>a) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. f = monom (UP Zp) \<one> n \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> a) 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = monom (UP Zp) \<one> n \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> a) 0

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have "f \<in> carrier Zp_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
using f_def monom_closed assms
[PROOF STATE]
proof (prove)
using this:
f = monom (UP Zp) \<one> n \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> a) 0
?a \<in> carrier Zp \<Longrightarrow> monom (UP Zp) ?a ?n \<in> carrier (UP Zp)
a \<in> carrier Zp
a \<noteq> \<one>
1 < n
eint 2 * val_Zp ([n] \<cdot> \<one>) < val_Zp (\<one> \<ominus> a)

goal (1 subgoal):
 1. f \<in> carrier (UP Zp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<in> carrier (UP Zp)

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have 0: "pderiv f = monom Zp_x ([n]\<cdot> \<one>) (n-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f = monom (UP Zp) ([n] \<cdot> \<one>) (n - 1)
[PROOF STEP]
by (simp add: assms(1) f_def pderiv_add pderiv_monom)
[PROOF STATE]
proof (state)
this:
pderiv f = monom (UP Zp) ([n] \<cdot> \<one>) (n - 1)

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have 1: "f \<bullet> \<one> = \<one> \<ominus> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> \<one> = \<one> \<ominus> a
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
f = monom (UP Zp) \<one> n \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> a) 0

goal (1 subgoal):
 1. f \<bullet> \<one> = \<one> \<ominus> a
[PROOF STEP]
by (metis R.add.inv_closed R.minus_eq R.nat_pow_one R.one_closed assms(1) to_fun_const to_fun_monom to_fun_monom_plus monom_closed)
[PROOF STATE]
proof (state)
this:
f \<bullet> \<one> = \<one> \<ominus> a

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have 2: "(pderiv f) \<bullet> \<one> = ([n]\<cdot> \<one>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> \<one> = [n] \<cdot> \<one>
[PROOF STEP]
using 0 to_fun_monom assms
[PROOF STATE]
proof (prove)
using this:
pderiv f = monom (UP Zp) ([n] \<cdot> \<one>) (n - 1)
\<lbrakk>?c \<in> carrier Zp; ?x \<in> carrier Zp\<rbrakk> \<Longrightarrow> monom (UP Zp) ?c ?n \<bullet> ?x = ?c \<otimes> ?x [^] ?n
a \<in> carrier Zp
a \<noteq> \<one>
1 < n
eint 2 * val_Zp ([n] \<cdot> \<one>) < val_Zp (\<one> \<ominus> a)

goal (1 subgoal):
 1. pderiv f \<bullet> \<one> = [n] \<cdot> \<one>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> \<one> = [n] \<cdot> \<one>

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have 3: "val_Zp (f \<bullet> \<one>) > 2* val_Zp ((pderiv f) \<bullet> \<one>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)
[PROOF STEP]
using 1 2 assms
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<one> = \<one> \<ominus> a
pderiv f \<bullet> \<one> = [n] \<cdot> \<one>
a \<in> carrier Zp
a \<noteq> \<one>
1 < n
eint 2 * val_Zp ([n] \<cdot> \<one>) < val_Zp (\<one> \<ominus> a)

goal (1 subgoal):
 1. eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)
[PROOF STEP]
by (simp add: val_Zp_def)
[PROOF STATE]
proof (state)
this:
eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>)

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have 4: "f \<bullet> \<one> \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> \<one> \<noteq> \<zero>
[PROOF STEP]
using 1 assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
f \<bullet> \<one> = \<one> \<ominus> a
a \<in> carrier Zp
a \<noteq> \<one>

goal (1 subgoal):
 1. f \<bullet> \<one> \<noteq> \<zero>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<bullet> \<one> \<noteq> \<zero>

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
have 5: "(pderiv f) \<bullet> \<one> \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv f \<bullet> \<one> \<noteq> \<zero>
[PROOF STEP]
using "2" Zp_char_0' assms(3)
[PROOF STATE]
proof (prove)
using this:
pderiv f \<bullet> \<one> = [n] \<cdot> \<one>
0 < ?n \<Longrightarrow> [?n] \<cdot> \<one> \<noteq> \<zero>
1 < n

goal (1 subgoal):
 1. pderiv f \<bullet> \<one> \<noteq> \<zero>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pderiv f \<bullet> \<one> \<noteq> \<zero>

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
obtain \<beta> where beta_def: "\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<beta>. \<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hensels_lemma[of f \<one>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier (UP Zp); \<one> \<in> carrier Zp; pderiv f \<bullet> \<one> \<noteq> \<zero>; f \<bullet> \<one> \<noteq> \<zero>; eint 2 * val_Zp (pderiv f \<bullet> \<one>) < val_Zp (f \<bullet> \<one>); \<And>\<alpha>. \<lbrakk>f \<bullet> \<alpha> = \<zero>; \<alpha> \<in> carrier Zp; val_Zp (pderiv f \<bullet> \<one>) < val_Zp (\<one> \<ominus> \<alpha>); val_Zp (\<one> \<ominus> \<alpha>) = val_Zp (local.divide (f \<bullet> \<one>) (pderiv f \<bullet> \<one>)); val_Zp (pderiv f \<bullet> \<alpha>) = val_Zp (pderiv f \<bullet> \<one>)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<beta>. \<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis "3" "5" R.one_closed \<open>f \<in> carrier Zp_x\<close>)
[PROOF STATE]
proof (state)
this:
\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>
[PROOF STEP]
have "(\<beta> [^] n) \<ominus> a = \<zero>"
[PROOF STATE]
proof (prove)
using this:
\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>

goal (1 subgoal):
 1. \<beta> [^] n \<ominus> a = \<zero>
[PROOF STEP]
using f_def R.add.inv_closed  assms(1) to_fun_const[of "\<ominus> a"] to_fun_monic_monom[of \<beta> n] to_fun_plus monom_closed
[PROOF STATE]
proof (prove)
using this:
\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>
f = monom (UP Zp) \<one> n \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> a) 0
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
a \<in> carrier Zp
\<lbrakk>\<ominus> a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> monom (UP Zp) (\<ominus> a) 0 \<bullet> ?b = \<ominus> a
\<beta> \<in> carrier Zp \<Longrightarrow> monom (UP Zp) \<one> n \<bullet> \<beta> = \<beta> [^] n
\<lbrakk>?g \<in> carrier (UP Zp); ?f \<in> carrier (UP Zp); ?x \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?f \<oplus>\<^bsub>UP Zp\<^esub> ?g) \<bullet> ?x = ?f \<bullet> ?x \<oplus> ?g \<bullet> ?x
?a \<in> carrier Zp \<Longrightarrow> monom (UP Zp) ?a ?n \<in> carrier (UP Zp)

goal (1 subgoal):
 1. \<beta> [^] n \<ominus> a = \<zero>
[PROOF STEP]
unfolding a_minus_def
[PROOF STATE]
proof (prove)
using this:
\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>
f = monom (UP Zp) \<one> n \<oplus>\<^bsub>UP Zp\<^esub> monom (UP Zp) (\<ominus> a) 0
?x \<in> carrier Zp \<Longrightarrow> \<ominus> ?x \<in> carrier Zp
a \<in> carrier Zp
\<lbrakk>\<ominus> a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> monom (UP Zp) (\<ominus> a) 0 \<bullet> ?b = \<ominus> a
\<beta> \<in> carrier Zp \<Longrightarrow> monom (UP Zp) \<one> n \<bullet> \<beta> = \<beta> [^] n
\<lbrakk>?g \<in> carrier (UP Zp); ?f \<in> carrier (UP Zp); ?x \<in> carrier Zp\<rbrakk> \<Longrightarrow> (?f \<oplus>\<^bsub>UP Zp\<^esub> ?g) \<bullet> ?x = ?f \<bullet> ?x \<oplus> ?g \<bullet> ?x
?a \<in> carrier Zp \<Longrightarrow> monom (UP Zp) ?a ?n \<in> carrier (UP Zp)

goal (1 subgoal):
 1. \<beta> [^] n \<oplus> \<ominus> a = \<zero>
[PROOF STEP]
by (simp add: beta_def)
[PROOF STATE]
proof (state)
this:
\<beta> [^] n \<ominus> a = \<zero>

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<beta> [^] n \<ominus> a = \<zero>
[PROOF STEP]
have "\<beta> \<in> carrier Zp \<and> \<beta> [^] n = a"
[PROOF STATE]
proof (prove)
using this:
\<beta> [^] n \<ominus> a = \<zero>

goal (1 subgoal):
 1. \<beta> \<in> carrier Zp \<and> \<beta> [^] n = a
[PROOF STEP]
using beta_def nonzero_memE  not_eq_diff_nonzero assms(1) pow_closed
[PROOF STATE]
proof (prove)
using this:
\<beta> [^] n \<ominus> a = \<zero>
\<beta> \<in> carrier Zp \<and> f \<bullet> \<beta> = \<zero>
?a \<in> nonzero Zp \<Longrightarrow> ?a \<in> carrier Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<noteq> \<zero>
\<lbrakk>?a \<noteq> ?b; ?a \<in> carrier Zp; ?b \<in> carrier Zp\<rbrakk> \<Longrightarrow> ?a \<ominus> ?b \<in> nonzero Zp
a \<in> carrier Zp
?a \<in> carrier Zp \<Longrightarrow> ?a [^] ?n \<in> carrier Zp

goal (1 subgoal):
 1. \<beta> \<in> carrier Zp \<and> \<beta> [^] n = a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<beta> \<in> carrier Zp \<and> \<beta> [^] n = a

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<beta> \<in> carrier Zp \<and> \<beta> [^] n = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<beta> \<in> carrier Zp \<and> \<beta> [^] n = a

goal (1 subgoal):
 1. \<exists>b\<in>carrier Zp. b [^] n = a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b\<in>carrier Zp. b [^] n = a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in prob_space) integral_stream_space:
  fixes f :: "'a stream \<Rightarrow> ('b :: {banach, second_countable_topology,real_normed_vector})"
  assumes int_f: "integrable (stream_space M) f"
  assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
  shows "(\<integral>X. f X \<partial>stream_space M) = (\<integral>x. (\<integral>X. f (x ## X) \<partial>stream_space M) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
interpret S: sequence_space M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sequence_space M
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair_sigma_finite M (Pi\<^sub>M UNIV (\<lambda>i. M))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
interpret P': pair_sigma_finite "\<Pi>\<^sub>M i::nat\<in>UNIV. M" M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair_sigma_finite (Pi\<^sub>M UNIV (\<lambda>i. M)) M
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
obtain i where "has_bochner_integral (stream_space M) f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. has_bochner_integral (stream_space M) f i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using int_f
[PROOF STATE]
proof (prove)
using this:
integrable (stream_space M) f

goal (1 subgoal):
 1. (\<And>i. has_bochner_integral (stream_space M) f i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using integrable.cases
[PROOF STATE]
proof (prove)
using this:
integrable (stream_space M) f
\<lbrakk>integrable ?M ?f; \<And>x. has_bochner_integral ?M ?f x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>i. has_bochner_integral (stream_space M) f i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
has_bochner_integral (stream_space M) f i

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "integrable S.S (\<lambda>X. f (to_stream X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream X))
[PROOF STEP]
using int_f
[PROOF STATE]
proof (prove)
using this:
integrable (stream_space M) f

goal (1 subgoal):
 1. integrable (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream X))
[PROOF STEP]
by (metis integrable_distr measurable_to_stream stream_space_eq_distr)
[PROOF STATE]
proof (state)
this:
integrable (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
hence "integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M))
    (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X))"
[PROOF STATE]
proof (prove)
using this:
integrable (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream X))

goal (1 subgoal):
 1. integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X))
[PROOF STEP]
by (auto simp: S.PiM_iter)
[PROOF STATE]
proof (state)
this:
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y))
    (\<lambda>X. f (to_stream X)) \<longleftrightarrow>
    integrable (M \<Otimes>\<^sub>M S.S) (\<lambda>X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X)) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))
[PROOF STEP]
by (auto simp: integrable_distr_eq)
[PROOF STATE]
proof (state)
this:
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X)) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X))
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X)) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))
[PROOF STEP]
have "integrable (M \<Otimes>\<^sub>M S.S) (\<lambda>X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)))"
[PROOF STATE]
proof (prove)
using this:
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X))
integrable (distr (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, y). case_nat x y)) (\<lambda>X. f (to_stream X)) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))

goal (1 subgoal):
 1. integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
hence "integrable (M \<Otimes>\<^sub>M (Pi\<^sub>M UNIV (\<lambda>i. M)))
    (\<lambda>X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)))"
[PROOF STATE]
proof (prove)
using this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))

goal (1 subgoal):
 1. integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "integrable (M \<Otimes>\<^sub>M (Pi\<^sub>M UNIV (\<lambda>i. M)))
    (\<lambda>X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X))) =
      integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))
[PROOF STEP]
by (fastforce intro!: Bochner_Integration.integrable_cong)
[PROOF STATE]
proof (state)
this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))
[PROOF STEP]
have *: "integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))"
[PROOF STATE]
proof (prove)
using this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>X. f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))) = integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))

goal (1 subgoal):
 1. integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "(\<integral>X. f X \<partial>stream_space M) = (\<integral>X. f (to_stream X) \<partial>S.S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = S.expectation (\<lambda>X. f (to_stream X))
[PROOF STEP]
by (subst stream_space_eq_distr) (simp add: integral_distr)
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (stream_space M) f = S.expectation (\<lambda>X. f (to_stream X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (stream_space M) f = S.expectation (\<lambda>X. f (to_stream X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "\<dots> = (\<integral>X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)) \<partial>(M \<Otimes>\<^sub>M S.S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S.expectation (\<lambda>X. f (to_stream X)) = LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))
[PROOF STEP]
by (subst S.PiM_iter[symmetric]) (simp add: integral_distr)
[PROOF STATE]
proof (state)
this:
S.expectation (\<lambda>X. f (to_stream X)) = LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
S.expectation (\<lambda>X. f (to_stream X)) = LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "\<dots> = (\<integral>x. \<integral>X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) (x, X)))\<partial>S.S  \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
integrable (M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)) (\<lambda>(x, X). f (to_stream (case_nat x X)))

goal (1 subgoal):
 1. LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))))
[PROOF STEP]
by (auto simp: pair_sigma_finite.integral_fst P.pair_sigma_finite_axioms case_prod_unfold)
[PROOF STATE]
proof (state)
this:
LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT X|(M \<Otimes>\<^sub>M Pi\<^sub>M UNIV (\<lambda>i. M)). f (to_stream (case X of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>))))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "\<dots> = (\<integral>x. \<integral>X. f (x ## to_stream X) \<partial>S.S \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (x ## to_stream X)))
[PROOF STEP]
by (auto intro!: integral_cong simp: to_stream_nat_case)
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (x ## to_stream X)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. S.expectation (\<lambda>X. f (to_stream (case (x, X) of (s, \<omega>) \<Rightarrow> case_nat s \<omega>)))) = expectation (\<lambda>x. S.expectation (\<lambda>X. f (x ## to_stream X)))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "\<dots> = (\<integral>x. \<integral>X. f (x ## X) \<partial>distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. S.expectation (\<lambda>X. f (x ## to_stream X))) = expectation (\<lambda>x. LINT X|distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream. f (x ## X))
[PROOF STEP]
by (subst Bochner_Integration.integral_cong[OF refl]) (auto simp: integral_distr)
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. S.expectation (\<lambda>X. f (x ## to_stream X))) = expectation (\<lambda>x. LINT X|distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream. f (x ## X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. S.expectation (\<lambda>X. f (x ## to_stream X))) = expectation (\<lambda>x. LINT X|distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream. f (x ## X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
have "\<dots> = (\<integral>x. \<integral>X. f (x ## X) \<partial>stream_space M \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. LINT X|distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream. f (x ## X)) = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
using stream_space_eq_distr
[PROOF STATE]
proof (prove)
using this:
stream_space ?M = distr (Pi\<^sub>M UNIV (\<lambda>i. ?M)) (stream_space ?M) to_stream

goal (1 subgoal):
 1. expectation (\<lambda>x. LINT X|distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream. f (x ## X)) = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
expectation (\<lambda>x. LINT X|distr (Pi\<^sub>M UNIV (\<lambda>i. M)) (stream_space M) to_stream. f (x ## X)) = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))

goal (1 subgoal):
 1. integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (stream_space M) f = expectation (\<lambda>x. LINT X|stream_space M. f (x ## X))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prefix_cons:
  "Omega_Words_Fun.prefix (Suc n) seq = seq 0#Omega_Words_Fun.prefix n (\<lambda>n. seq (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Omega_Words_Fun.prefix (Suc n) seq = seq 0 # Omega_Words_Fun.prefix n (\<lambda>n. seq (Suc n))
[PROOF STEP]
by (metis map_upt_Suc subsequence_def)


[STATEMENT]
lemma restrict_Suc: "restrict y {0..<Suc i} (Suc n) = (restrict (\<lambda>n. y (Suc n)) {0..<i}) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict y {0..<Suc i} (Suc n) = (\<lambda>n\<in>{0..<i}. y (Suc n)) n
[PROOF STEP]
by auto


[STATEMENT]
lemma prefix_restrict: "Omega_Words_Fun.prefix i (restrict y {0..<i}) = Omega_Words_Fun.prefix i y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Omega_Words_Fun.prefix i (restrict y {0..<i}) = Omega_Words_Fun.prefix i y
[PROOF STEP]
proof (induction i arbitrary: y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. Omega_Words_Fun.prefix 0 (restrict y {0..<0}) = Omega_Words_Fun.prefix 0 y
 2. \<And>i y. (\<And>y. Omega_Words_Fun.prefix i (restrict y {0..<i}) = Omega_Words_Fun.prefix i y) \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) (restrict y {0..<Suc i}) = Omega_Words_Fun.prefix (Suc i) y
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
Omega_Words_Fun.prefix i (restrict ?y {0..<i}) = Omega_Words_Fun.prefix i ?y

goal (2 subgoals):
 1. \<And>y. Omega_Words_Fun.prefix 0 (restrict y {0..<0}) = Omega_Words_Fun.prefix 0 y
 2. \<And>i y. (\<And>y. Omega_Words_Fun.prefix i (restrict y {0..<i}) = Omega_Words_Fun.prefix i y) \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) (restrict y {0..<Suc i}) = Omega_Words_Fun.prefix (Suc i) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Omega_Words_Fun.prefix i (restrict ?y {0..<i}) = Omega_Words_Fun.prefix i ?y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Omega_Words_Fun.prefix i (restrict ?y {0..<i}) = Omega_Words_Fun.prefix i ?y

goal (1 subgoal):
 1. Omega_Words_Fun.prefix (Suc i) (restrict y {0..<Suc i}) = Omega_Words_Fun.prefix (Suc i) y
[PROOF STEP]
unfolding restrict_Suc prefix_cons
[PROOF STATE]
proof (prove)
using this:
Omega_Words_Fun.prefix i (restrict ?y {0..<i}) = Omega_Words_Fun.prefix i ?y

goal (1 subgoal):
 1. restrict y {0..<Suc i} 0 # Omega_Words_Fun.prefix i (\<lambda>n\<in>{0..<i}. y (Suc n)) = y 0 # Omega_Words_Fun.prefix i (\<lambda>n. y (Suc n))
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
Omega_Words_Fun.prefix (Suc i) (restrict y {0..<Suc i}) = Omega_Words_Fun.prefix (Suc i) y

goal (1 subgoal):
 1. \<And>y. Omega_Words_Fun.prefix 0 (restrict y {0..<0}) = Omega_Words_Fun.prefix 0 y
[PROOF STEP]
qed simp


[STATEMENT]
lemma prefix_measurable[measurable]:
  "Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i}
  (\<lambda>_. count_space (UNIV :: ('s ::countable \<times> 'a::countable) set)) \<rightarrow>\<^sub>M count_space UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
proof (induction i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Omega_Words_Fun.prefix 0 \<in> Pi\<^sub>M {0..<0} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 2. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Omega_Words_Fun.prefix 0 \<in> Pi\<^sub>M {0..<0} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 2. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Omega_Words_Fun.prefix 0 \<in> Pi\<^sub>M {0..<0} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Omega_Words_Fun.prefix 0 \<in> Pi\<^sub>M {0..<0} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
have aux: "(\<lambda>w. (restrict w {0..<i}, w i)) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M
    Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M (count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. (restrict w {0..<i}, w i)) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. (restrict w {0..<i}, w i)) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
have aux': "(\<lambda>(w,wi). Omega_Words_Fun.prefix i (restrict w {0..<i})@[wi]) \<in> Pi\<^sub>M {0..<i}
    (\<lambda>_. count_space (UNIV :: ('s \<times> 'a) set)) \<Otimes>\<^sub>M (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(w, wi). Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [wi]) \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. (\<lambda>(w, wi). Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [wi]) \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>(w, wi). Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [wi]) \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
have f_eq: "\<And>w. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i] =
    (\<lambda>(w,wi). Omega_Words_Fun.prefix i w @[wi]) ((restrict w {0..<i}), w i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i] = (case (restrict w {0..<i}, w i) of (w, wi) \<Rightarrow> Omega_Words_Fun.prefix i w @ [wi])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Omega_Words_Fun.prefix i (restrict ?w1 {0..<i}) @ [?w1 i] = (case (restrict ?w1 {0..<i}, ?w1 i) of (w, wi) \<Rightarrow> Omega_Words_Fun.prefix i w @ [wi])

goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
have "(\<lambda>w:: nat \<Rightarrow> 's \<times> 'a. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i]) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i]) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
using aux aux'[unfolded prefix_restrict]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>w. (restrict w {0..<i}, w i)) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV
(\<lambda>(w, wi). Omega_Words_Fun.prefix i w @ [wi]) \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<Otimes>\<^sub>M count_space UNIV \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. (\<lambda>w. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i]) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
by (subst f_eq) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>w. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i]) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. \<And>i. Omega_Words_Fun.prefix i \<in> Pi\<^sub>M {0..<i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV \<Longrightarrow> Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<lambda>w. Omega_Words_Fun.prefix i (restrict w {0..<i}) @ [w i]) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
unfolding prefix_restrict[of _ "i"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>w. Omega_Words_Fun.prefix i w @ [w i]) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Omega_Words_Fun.prefix (Suc i) \<in> Pi\<^sub>M {0..<Suc i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_decI[intro]:
  "(\<And>s. set_pmf (d s) \<subseteq> A s) \<Longrightarrow> is_dec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. set_pmf (d s) \<subseteq> A s) \<Longrightarrow> is_dec d
[PROOF STEP]
unfolding is_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. set_pmf (d s) \<subseteq> A s) \<Longrightarrow> \<forall>s. set_pmf (d s) \<subseteq> A s
[PROOF STEP]
by auto


[STATEMENT]
lemma is_dec_mk_dec_det_iff [simp]: "is_dec (mk_dec_det d) \<longleftrightarrow> is_dec_det d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dec (mk_dec_det d) = is_dec_det d
[PROOF STEP]
by (simp add: is_dec_def is_dec_det_def mk_dec_det_def)


[STATEMENT]
lemma D_det_to_MR[intro]: "is_dec_det d \<Longrightarrow> is_dec (mk_dec_det d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dec_det d \<Longrightarrow> is_dec (mk_dec_det d)
[PROOF STEP]
by simp


[STATEMENT]
lemma SOME_is_dec_det: "is_dec_det (\<lambda>s. SOME a. a \<in> A s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dec_det (\<lambda>s. SOME a. a \<in> A s)
[PROOF STEP]
using A_ne
[PROOF STATE]
proof (prove)
using this:
A ?s \<noteq> {}

goal (1 subgoal):
 1. is_dec_det (\<lambda>s. SOME a. a \<in> A s)
[PROOF STEP]
by (simp add: is_dec_det_def some_in_eq)


[STATEMENT]
lemma ex_dec_det [simp]: "\<exists>d. is_dec_det d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ex is_dec_det
[PROOF STEP]
using SOME_is_dec_det
[PROOF STATE]
proof (prove)
using this:
is_dec_det (\<lambda>s. SOME a. a \<in> A s)

goal (1 subgoal):
 1. Ex is_dec_det
[PROOF STEP]
by blast


[STATEMENT]
lemma D_det_ne [simp]: "D\<^sub>D \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D\<^sub>D \<noteq> {}
[PROOF STEP]
by simp


[STATEMENT]
lemma D\<^sub>R_ne [simp]: "D\<^sub>R \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D\<^sub>R \<noteq> {}
[PROOF STEP]
using D_det_ne D_det_to_MR
[PROOF STATE]
proof (prove)
using this:
D\<^sub>D \<noteq> {}
is_dec_det ?d \<Longrightarrow> is_dec (mk_dec_det ?d)

goal (1 subgoal):
 1. D\<^sub>R \<noteq> {}
[PROOF STEP]
by blast


[STATEMENT]
lemma ex_dec[intro, simp]: "\<exists>d. is_dec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ex is_dec
[PROOF STEP]
using ex_dec_det
[PROOF STATE]
proof (prove)
using this:
Ex is_dec_det

goal (1 subgoal):
 1. Ex is_dec
[PROOF STEP]
by blast


[STATEMENT]
lemma is_markovian_mk_iff[simp]: "is_markovian (mk_markovian p) \<longleftrightarrow> (\<forall>n. is_dec (p n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_markovian (mk_markovian p) = (\<forall>n. is_dec (p n))
[PROOF STEP]
unfolding is_markovian_def mk_markovian_def is_policy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>hs. is_dec (p (length hs))) \<and> (\<forall>h h'. length h = length h' \<longrightarrow> p (length h) = p (length h'))) = (\<forall>n. is_dec (p n))
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) Ex_list_of_length)


[STATEMENT]
lemma is_markovian_mk[intro]: "\<forall>n. is_dec (p n) \<Longrightarrow> is_markovian (mk_markovian p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. is_dec (p n) \<Longrightarrow> is_markovian (mk_markovian p)
[PROOF STEP]
unfolding is_markovian_def mk_markovian_def is_policy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. is_dec (p n) \<Longrightarrow> (\<forall>hs. is_dec (p (length hs))) \<and> (\<forall>h h'. length h = length h' \<longrightarrow> p (length h) = p (length h'))
[PROOF STEP]
by auto


[STATEMENT]
lemma mk_markovian_nil [simp]: "mk_markovian p [] = p 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_markovian p [] = p 0
[PROOF STEP]
unfolding mk_markovian_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p (length []) = p 0
[PROOF STEP]
by auto


[STATEMENT]
lemma \<Pi>\<^sub>M\<^sub>R_imp_policies[intro]: "p \<in> \<Pi>\<^sub>M\<^sub>R \<Longrightarrow> mk_markovian p \<in> \<Pi>\<^sub>H\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<Pi>\<^sub>M\<^sub>R \<Longrightarrow> mk_markovian p \<in> \<Pi>\<^sub>H\<^sub>R
[PROOF STEP]
unfolding is_policy_def mk_markovian_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<Pi>\<^sub>M\<^sub>R \<Longrightarrow> (\<lambda>h. p (length h)) \<in> {p. \<forall>hs. is_dec (p hs)}
[PROOF STEP]
by auto


[STATEMENT]
lemma \<Pi>\<^sub>M\<^sub>D_MR_iff[simp]: "(\<lambda>n. mk_dec_det (p n)) \<in> \<Pi>\<^sub>M\<^sub>R \<longleftrightarrow> p \<in> \<Pi>\<^sub>M\<^sub>D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>n. mk_dec_det (p n)) \<in> \<Pi>\<^sub>M\<^sub>R) = (p \<in> \<Pi>\<^sub>M\<^sub>D)
[PROOF STEP]
by auto


[STATEMENT]
lemma \<Pi>\<^sub>M\<^sub>D_to_MR[intro]: "p \<in> \<Pi>\<^sub>M\<^sub>D \<Longrightarrow> (\<lambda>n. mk_dec_det (p n)) \<in> \<Pi>\<^sub>M\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<Pi>\<^sub>M\<^sub>D \<Longrightarrow> (\<lambda>n. mk_dec_det (p n)) \<in> \<Pi>\<^sub>M\<^sub>R
[PROOF STEP]
by simp


[STATEMENT]
lemma \<Pi>\<^sub>M\<^sub>D_ne[simp]: "\<Pi>\<^sub>M\<^sub>D \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Pi>\<^sub>M\<^sub>D \<noteq> {}
[PROOF STEP]
by (auto simp: someI_ex[OF ex_dec_det] intro: exI[of _ "\<lambda>n. (SOME d. is_dec_det d)"])


[STATEMENT]
lemma \<Pi>\<^sub>M\<^sub>R_ne[simp]: "\<Pi>\<^sub>M\<^sub>R \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Pi>\<^sub>M\<^sub>R \<noteq> {}
[PROOF STEP]
using \<Pi>\<^sub>M\<^sub>D_ne
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>M\<^sub>D \<noteq> {}

goal (1 subgoal):
 1. \<Pi>\<^sub>M\<^sub>R \<noteq> {}
[PROOF STEP]
by fast


[STATEMENT]
lemma policies_ne[simp, intro]: "\<Pi>\<^sub>H\<^sub>R \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Pi>\<^sub>H\<^sub>R \<noteq> {}
[PROOF STEP]
using \<Pi>\<^sub>M\<^sub>R_ne is_policy_def
[PROOF STATE]
proof (prove)
using this:
\<Pi>\<^sub>M\<^sub>R \<noteq> {}
is_policy ?p \<equiv> \<forall>hs. is_dec (?p hs)

goal (1 subgoal):
 1. \<Pi>\<^sub>H\<^sub>R \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma is_stationary_const_iff[simp]: "is_stationary (\<lambda>_. d) = is_dec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_stationary (\<lambda>_. d) = is_dec d
[PROOF STEP]
unfolding is_stationary_def is_policy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>hs. is_dec d) \<and> (\<forall>h h'. d = d)) = is_dec d
[PROOF STEP]
by simp


[STATEMENT]
lemma is_stationary_const[intro]: "is_dec d \<Longrightarrow> is_stationary (\<lambda>_. d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dec d \<Longrightarrow> is_stationary (\<lambda>_. d)
[PROOF STEP]
by simp


[STATEMENT]
lemma is_policy_\<pi>_Suc [intro]: "is_policy p \<Longrightarrow> is_policy (\<pi>_Suc p sa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_policy p \<Longrightarrow> is_policy (\<pi>_Suc p sa)
[PROOF STEP]
unfolding is_policy_def \<pi>_Suc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>hs. is_dec (p hs) \<Longrightarrow> \<forall>hs. is_dec (p (sa # hs))
[PROOF STEP]
by force


[STATEMENT]
lemma Suc_mk_markovian[simp]: "\<pi>_Suc (mk_markovian p) x = mk_markovian (\<lambda>n. p (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>_Suc (mk_markovian p) x = mk_markovian (\<lambda>n. p (Suc n))
[PROOF STEP]
unfolding \<pi>_Suc_def mk_markovian_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>h. p (length (x # h))) = (\<lambda>h. p (Suc (length h)))
[PROOF STEP]
by auto


[STATEMENT]
lemma K0_iff: "K0 d S0 = S0 \<bind> (\<lambda>s. map_pmf (\<lambda>a. (s,a)) (d s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K\<^sub>0 d S0 = S0 \<bind> (\<lambda>s. map_pmf (Pair s) (d s))
[PROOF STEP]
by (simp add: K0_def map_pmf_def)


[STATEMENT]
lemma vimage_pair[simp]: "Pair x -` {p} = (if x = fst p then {snd p} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pair x -` {p} = (if x = fst p then {snd p} else {})
[PROOF STEP]
by auto


[STATEMENT]
lemma pmf_K0 [simp]: "pmf (K0 d S0) (s,a) = pmf S0 s * pmf (d s) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (K\<^sub>0 d S0) (s, a) = pmf S0 s * pmf (d s) a
[PROOF STEP]
unfolding K0_iff pmf_bind
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation S0 (\<lambda>x. pmf (map_pmf (Pair x) (d x)) (s, a)) = pmf S0 s * pmf (d s) a
[PROOF STEP]
by (subst integral_measure_pmf[where A = "{s}"]) (auto simp: pmf_map pmf.rep_eq split: if_splits)


[STATEMENT]
lemma set_pmf_K0: "set_pmf (K0 p S0) = {(s,a). s \<in> S0 \<and> a \<in> p s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (K\<^sub>0 p S0) = {(s, a). s \<in> set_pmf S0 \<and> a \<in> set_pmf (p s)}
[PROOF STEP]
by (auto simp add: K0_def)


[STATEMENT]
lemma fst_K0[simp]: "map_pmf fst (K0 p S0) = S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf fst (K\<^sub>0 p S0) = S0
[PROOF STEP]
unfolding K0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf fst (S0 \<bind> (\<lambda>s. p s \<bind> (\<lambda>a. return_pmf (s, a)))) = S0
[PROOF STEP]
by (simp add: map_bind_pmf map_pmf_comp bind_return_pmf')


[STATEMENT]
lemma count_space_M[simp]: "MDP_cont.M = count_space UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP_cont.M = count_space UNIV
[PROOF STEP]
by (auto simp: pair_measure_countable)


[STATEMENT]
lemma space_M[simp]: "space MDP_cont.M = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space MDP_cont.M = UNIV
[PROOF STEP]
by (auto simp: MDP_cont.space_lim_stream)


[STATEMENT]
lemma sets_T[measurable_cong]:
  "sets (T p x) = sets S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (T p x) = sets (stream_space (count_space UNIV))
[PROOF STEP]
by (auto simp: T_def MDP_cont.sets_lim_stream)


[STATEMENT]
lemma space_stream_space_ne[simp]: "space S \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space (stream_space (count_space UNIV)) \<noteq> {}
[PROOF STEP]
by (auto simp: space_stream_space)


[STATEMENT]
lemma space_T[simp]: "space (T p S0) = space S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space (T p S0) = space (stream_space (count_space UNIV))
[PROOF STEP]
by (simp add: MDP_cont.space_lim_stream T_def space_stream_space)


[STATEMENT]
lemma is_policy_MDP_cont[intro]:
  fixes p :: "('s \<times> 'a) list \<Rightarrow> 's \<Rightarrow> 'a pmf"
  shows "MDP_cont.is_policy (\<lambda>n (h,s). p (Omega_Words_Fun.prefix n h) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP_cont.is_policy (\<lambda>x xa. measure_pmf (case xa of (h, s) \<Rightarrow> p (Omega_Words_Fun.prefix x h) s))
[PROOF STEP]
unfolding MDP_cont.is_policy_def MDP_cont.is_dec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (\<lambda>x. measure_pmf (case x of (h, x) \<Rightarrow> p (Omega_Words_Fun.prefix i h) x)) \<in> Pi\<^sub>M {0..<i} (\<lambda>_. MDP_cont.M) \<Otimes>\<^sub>M count_space UNIV \<rightarrow>\<^sub>M prob_algebra (count_space UNIV)
[PROOF STEP]
using prefix_measurable measurable_pair_swap_iff
[PROOF STATE]
proof (prove)
using this:
Omega_Words_Fun.prefix ?i \<in> Pi\<^sub>M {0..<?i} (\<lambda>_. count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
(?f \<in> ?M2.0 \<Otimes>\<^sub>M ?M1.0 \<rightarrow>\<^sub>M ?M) = ((\<lambda>(x, y). ?f (y, x)) \<in> ?M1.0 \<Otimes>\<^sub>M ?M2.0 \<rightarrow>\<^sub>M ?M)

goal (1 subgoal):
 1. \<forall>i. (\<lambda>x. measure_pmf (case x of (h, x) \<Rightarrow> p (Omega_Words_Fun.prefix i h) x)) \<in> Pi\<^sub>M {0..<i} (\<lambda>_. MDP_cont.M) \<Otimes>\<^sub>M count_space UNIV \<rightarrow>\<^sub>M prob_algebra (count_space UNIV)
[PROOF STEP]
by (auto simp: prob_space_measure_pmf
      intro: measurable_pair_measure_countable1 measurable_prob_algebraI)


[STATEMENT]
lemma prob_space_T[intro, simp]: "prob_space (T p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (T p x)
[PROOF STEP]
by (auto simp add: T_def prob_space_measure_pmf space_prob_algebra)


[STATEMENT]
lemma T_subprob[simp]:
  "T p S0 \<in> space (subprob_algebra S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T p S0 \<in> space (subprob_algebra (stream_space (count_space UNIV)))
[PROOF STEP]
by (metis prob_space.M_in_subprob prob_space_T sets_T subprob_algebra_cong)


[STATEMENT]
lemma T_subprob_space [simp]: "subprob_space (T p S0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subprob_space (T p S0)
[PROOF STEP]
by (auto intro: prob_space_imp_subprob_space)


[STATEMENT]
lemma K0_MDP_cont_eq:
  "MDP_cont.K0 (\<lambda>x (h,s). measure_pmf (p (Omega_Words_Fun.prefix x h) s)) (measure_pmf S0) =
    K0 (p []) S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP_cont.K0 (\<lambda>x (h, s). measure_pmf (p (Omega_Words_Fun.prefix x h) s)) (measure_pmf S0) = measure_pmf (K\<^sub>0 (p []) S0)
[PROOF STEP]
unfolding MDP_cont.K0_def K0_def MDP_cont.K'_def map_pmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case 0 of 0 \<Rightarrow> measure_pmf S0 | Suc x \<Rightarrow> ((\<lambda>x. measure_pmf (K x)) \<circ> (\<lambda>_. undefined)) x) \<bind> (\<lambda>s. (case (\<lambda>_. undefined, s) of (h, s) \<Rightarrow> measure_pmf (p (Omega_Words_Fun.prefix 0 h) s)) \<bind> (\<lambda>a. return MDP_cont.M (s, a))) = measure_pmf (S0 \<bind> (\<lambda>s. p [] s \<bind> (\<lambda>a. return_pmf (s, a))))
[PROOF STEP]
by (simp add: measure_pmf_bind return_pmf.rep_eq)


[STATEMENT]
lemma T_eq:
  shows "T p S0 = do {
    sa \<leftarrow> measure_pmf (K0 (p []) S0);
    \<omega> \<leftarrow> T (\<pi>_Suc p sa) (K sa);
    return S (sa ## \<omega>)
  }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T p S0 = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP_cont.lim_stream (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa)) (measure_pmf S0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. MDP_cont.lim_stream (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> \<pi>_Suc p sa (Omega_Words_Fun.prefix x h) xa)) (measure_pmf (K sa)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
[PROOF STEP]
proof (subst MDP_cont.lim_stream_eq)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. MDP_cont.is_policy (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa))
 2. measure_pmf S0 \<in> space (prob_algebra (count_space UNIV))
 3. MDP_cont.K0 (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa)) (measure_pmf S0) \<bind> (\<lambda>y. MDP_cont.lim_stream (MDP_cont.Suc_policy (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa)) y) (measure_pmf (K y)) \<bind> (\<lambda>\<omega>. return (stream_space MDP_cont.M) (y ## \<omega>))) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. MDP_cont.lim_stream (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> \<pi>_Suc p sa (Omega_Words_Fun.prefix x h) xa)) (measure_pmf (K sa)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
[PROOF STEP]
show "MDP_cont.is_policy (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP_cont.is_policy (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MDP_cont.is_policy (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa))

goal (2 subgoals):
 1. measure_pmf S0 \<in> space (prob_algebra (count_space UNIV))
 2. MDP_cont.K0 (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa)) (measure_pmf S0) \<bind> (\<lambda>y. MDP_cont.lim_stream (MDP_cont.Suc_policy (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> p (Omega_Words_Fun.prefix x h) xa)) y) (measure_pmf (K y)) \<bind> (\<lambda>\<omega>. return (stream_space MDP_cont.M) (y ## \<omega>))) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. MDP_cont.lim_stream (\<lambda>x xa. measure_pmf (case xa of (h, xa) \<Rightarrow> \<pi>_Suc p sa (Omega_Words_Fun.prefix x h) xa)) (measure_pmf (K sa)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
[PROOF STEP]
qed (auto simp: space_prob_algebra prob_space_measure_pmf \<pi>_Suc_def MDP_cont.Suc_policy_def
    prefix_cons K0_MDP_cont_eq  prod.case_distrib)


[STATEMENT]
lemma T_eq_distr:
  shows "T p S0 = measure_pmf (K0 (p []) S0) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) S ((##) sa))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T p S0 = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))
[PROOF STEP]
by (simp add: T_eq[symmetric] bind_return_distr'[symmetric])


[STATEMENT]
lemma integral_T:
  fixes f :: "('s \<times> 'a) stream \<Rightarrow> real"
  assumes f_bounded: "\<And>x. \<bar>f x\<bar> \<le> B"
  assumes f: "f \<in> borel_measurable S"
  shows "(\<integral>t. f t \<partial>T p x) = \<integral>sa. \<integral>t'. f (sa##t') \<partial>T (\<pi>_Suc p sa) (K sa) \<partial>K0 (p []) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
note T_eq_distr
[PROOF STATE]
proof (state)
this:
T ?p ?S0.0 = measure_pmf (K\<^sub>0 (?p []) ?S0.0) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc ?p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))

goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
have "(\<integral>t. f t \<partial>T p x) = (\<integral>t. f t \<partial>measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = integral\<^sup>L (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f
[PROOF STEP]
using T_eq_distr
[PROOF STATE]
proof (prove)
using this:
T ?p ?S0.0 = measure_pmf (K\<^sub>0 (?p []) ?S0.0) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc ?p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))

goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = integral\<^sup>L (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (T p x) f = integral\<^sup>L (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f

goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (T p x) f = integral\<^sup>L (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f

goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
have "\<dots> = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
proof (subst integral_bind[OF f f_bounded, where B' = 1], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))
 2. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 3. AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1
 4. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))
 2. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 3. AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1
 4. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))
[PROOF STEP]
by (auto intro!: prob_space_imp_subprob_space prob_space.prob_space_distr
          simp: space_subprob_algebra)
[PROOF STATE]
proof (state)
this:
measure_pmf.random_variable (K\<^sub>0 (p []) x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))

goal (3 subgoals):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 2. AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1
 3. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 2. AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1
 3. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 2. AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1
 3. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1
[PROOF STEP]
by (auto intro!: prob_space.emeasure_le_1 prob_space.prob_space_distr)
[PROOF STATE]
proof (state)
this:
AE x in measure_pmf (K\<^sub>0 (p []) x). emeasure (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) (space (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x))) \<le> ennreal 1

goal (2 subgoals):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 2. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 2. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
 2. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
by (auto simp: f integral_distr intro: Bochner_Integration.integral_cong)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>x. integral\<^sup>L (distr (T (\<pi>_Suc p x) (K x)) (stream_space (count_space UNIV)) ((##) x)) f) = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))

goal (1 subgoal):
 1. finite_measure (measure_pmf (K\<^sub>0 (p []) x))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))

goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))

goal (1 subgoal):
 1. integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (T p x) f = measure_pmf.expectation (K\<^sub>0 (p []) x) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nn_integral_T:
  assumes f: "f \<in> borel_measurable S"
  shows "(\<integral>\<^sup>+t. f t \<partial>T p x) = (\<integral>\<^sup>+sa. \<integral>\<^sup>+ t'. f (sa##t') \<partial>T (\<pi>_Suc p sa) (K sa) \<partial>K0 (p []) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (T p x) f = \<integral>\<^sup>+ sa. \<integral>\<^sup>+ t'. f (sa ## t') \<partial>T (\<pi>_Suc p sa) (K sa) \<partial>measure_pmf (K\<^sub>0 (p []) x)
[PROOF STEP]
unfolding T_eq_distr[of p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_pmf (K\<^sub>0 (p []) x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) f = \<integral>\<^sup>+ sa. \<integral>\<^sup>+ t'. f (sa ## t') \<partial>T (\<pi>_Suc p sa) (K sa) \<partial>measure_pmf (K\<^sub>0 (p []) x)
[PROOF STEP]
by (subst nn_integral_bind[OF f])
    (auto intro!: prob_space_imp_subprob_space prob_space.prob_space_distr
      simp: f nn_integral_distr space_subprob_algebra)


[STATEMENT]
lemma Pn_eq_T:
  shows "measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)
[PROOF STEP]
proof (induction n arbitrary: p S0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p S0. measure_pmf (Pn p S0 0) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! 0)
 2. \<And>n p S0. (\<And>p S0. measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)) \<Longrightarrow> measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
case (0 p S0)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>p S0. measure_pmf (Pn p S0 0) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! 0)
 2. \<And>n p S0. (\<And>p S0. measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)) \<Longrightarrow> measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 0) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! 0)
[PROOF STEP]
unfolding T_eq[of p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 0) = distr (measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))) (count_space UNIV) (\<lambda>t. t !! 0)
[PROOF STEP]
proof (subst distr_bind[where K = S], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
 2. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 3. (\<lambda>t. t !! 0) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 4. measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
 2. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 3. (\<lambda>t. t !! 0) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 4. measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
[PROOF STEP]
by (auto intro!: prob_space_imp_subprob_space subprob_space.bind_in_space)
[PROOF STATE]
proof (state)
this:
measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))

goal (3 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! 0) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 3. measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! 0) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 3. measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! 0) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 3. measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))
[PROOF STEP]
by (subst bind_cong[OF refl, where g = "return (count_space UNIV)"])
        (auto intro!: bind_const' simp: distr_bind[where K = S] distr_return bind_return'' space_stream_space subprob_space_return_ne)
[PROOF STATE]
proof (state)
this:
measure_pmf (Pn p S0 0) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! 0))

goal (2 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! 0) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
measure_pmf (Pn p S0 0) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! 0)

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)) \<Longrightarrow> measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)) \<Longrightarrow> measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
measure_pmf (Pn ?p3 ?S0.3 n) = distr (T ?p3 ?S0.3) (count_space UNIV) (\<lambda>t. t !! n)

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. measure_pmf (Pn p S0 n) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n)) \<Longrightarrow> measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
unfolding T_eq[of p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 (Suc n)) = distr (measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))) (count_space UNIV) (\<lambda>t. t !! Suc n)
[PROOF STEP]
proof (subst distr_bind[where K = S], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
 2. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 3. (\<lambda>t. t !! Suc n) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 4. measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
 2. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 3. (\<lambda>t. t !! Suc n) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 4. measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))
[PROOF STEP]
by (auto intro!: prob_space_imp_subprob_space subprob_space.bind_in_space)[1]
[PROOF STATE]
proof (state)
this:
measure_pmf.random_variable (K\<^sub>0 (p []) S0) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>sa. T (\<pi>_Suc p sa) (K sa) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (sa ## \<omega>)))

goal (3 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! Suc n) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 3. measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! Suc n) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 3. measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! Suc n) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
 3. measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))
[PROOF STEP]
by (auto simp: Pn.simps(2) measure_pmf_bind Suc bind_return_distr' distr_distr comp_def intro!: bind_cong)
[PROOF STATE]
proof (state)
this:
measure_pmf (Pn p S0 (Suc n)) = measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. distr (T (\<pi>_Suc p x) (K x) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) (x ## \<omega>))) (count_space UNIV) (\<lambda>t. t !! Suc n))

goal (2 subgoals):
 1. space (measure_pmf (K\<^sub>0 (p []) S0)) \<noteq> {}
 2. (\<lambda>t. t !! Suc n) \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
measure_pmf (Pn p S0 (Suc n)) = distr (T p S0) (count_space UNIV) (\<lambda>t. t !! Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Pn_in_A: "is_policy p \<Longrightarrow> (s, a) \<in> Pn p S0 n \<Longrightarrow> a \<in> A s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 n)\<rbrakk> \<Longrightarrow> a \<in> A s
[PROOF STEP]
proof (induction n arbitrary: S0 p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 0)\<rbrakk> \<Longrightarrow> a \<in> A s
 2. \<And>n S0 p. \<lbrakk>\<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 n)\<rbrakk> \<Longrightarrow> a \<in> A s; is_policy p; (s, a) \<in> set_pmf (Pn p S0 (Suc n))\<rbrakk> \<Longrightarrow> a \<in> A s
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
is_policy p
(s, a) \<in> set_pmf (Pn p S0 0)

goal (2 subgoals):
 1. \<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 0)\<rbrakk> \<Longrightarrow> a \<in> A s
 2. \<And>n S0 p. \<lbrakk>\<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 n)\<rbrakk> \<Longrightarrow> a \<in> A s; is_policy p; (s, a) \<in> set_pmf (Pn p S0 (Suc n))\<rbrakk> \<Longrightarrow> a \<in> A s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_policy p
(s, a) \<in> set_pmf (Pn p S0 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_policy p
(s, a) \<in> set_pmf (Pn p S0 0)

goal (1 subgoal):
 1. a \<in> A s
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
is_policy p
(s, a) \<in> set_pmf (Pn p S0 0)
is_policy p
(s, a) \<in> set_pmf (Pn p S0 0)

goal (1 subgoal):
 1. a \<in> A s
[PROOF STEP]
unfolding is_policy_def is_dec_def
[PROOF STATE]
proof (prove)
using this:
\<forall>hs s. set_pmf (p hs s) \<subseteq> A s
(s, a) \<in> set_pmf (Pn p S0 0)
\<forall>hs s. set_pmf (p hs s) \<subseteq> A s
(s, a) \<in> set_pmf (Pn p S0 0)

goal (1 subgoal):
 1. a \<in> A s
[PROOF STEP]
by (auto simp: K0_def)
[PROOF STATE]
proof (state)
this:
a \<in> A s

goal (1 subgoal):
 1. \<And>n S0 p. \<lbrakk>\<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 n)\<rbrakk> \<Longrightarrow> a \<in> A s; is_policy p; (s, a) \<in> set_pmf (Pn p S0 (Suc n))\<rbrakk> \<Longrightarrow> a \<in> A s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n S0 p. \<lbrakk>\<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 n)\<rbrakk> \<Longrightarrow> a \<in> A s; is_policy p; (s, a) \<in> set_pmf (Pn p S0 (Suc n))\<rbrakk> \<Longrightarrow> a \<in> A s
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_policy ?p3; (s, a) \<in> set_pmf (Pn ?p3 ?S0.3 n)\<rbrakk> \<Longrightarrow> a \<in> A s
is_policy p
(s, a) \<in> set_pmf (Pn p S0 (Suc n))

goal (1 subgoal):
 1. \<And>n S0 p. \<lbrakk>\<And>S0 p. \<lbrakk>is_policy p; (s, a) \<in> set_pmf (Pn p S0 n)\<rbrakk> \<Longrightarrow> a \<in> A s; is_policy p; (s, a) \<in> set_pmf (Pn p S0 (Suc n))\<rbrakk> \<Longrightarrow> a \<in> A s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_policy ?p3; (s, a) \<in> set_pmf (Pn ?p3 ?S0.3 n)\<rbrakk> \<Longrightarrow> a \<in> A s
is_policy p
(s, a) \<in> set_pmf (Pn p S0 (Suc n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_policy ?p3; (s, a) \<in> set_pmf (Pn ?p3 ?S0.3 n)\<rbrakk> \<Longrightarrow> a \<in> A s
is_policy p
(s, a) \<in> set_pmf (Pn p S0 (Suc n))

goal (1 subgoal):
 1. a \<in> A s
[PROOF STEP]
by (auto simp: Pn.simps(2) K0_def)
[PROOF STATE]
proof (state)
this:
a \<in> A s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T_in_A:
  assumes "is_policy p"
  shows "AE t in T p S0. snd (t !! n) \<in> A (fst (t !! n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE t in T p S0. snd (t !! n) \<in> A (fst (t !! n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE t in T p S0. snd (t !! n) \<in> A (fst (t !! n))
[PROOF STEP]
have aux: "AE t in distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n). snd t \<in> A (fst t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE t in distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n). snd t \<in> A (fst t)
[PROOF STEP]
using assms Pn_eq_T[symmetric]
[PROOF STATE]
proof (prove)
using this:
is_policy p
distr (T ?p ?S0.0) (count_space UNIV) (\<lambda>t. t !! ?n) = measure_pmf (Pn ?p ?S0.0 ?n)

goal (1 subgoal):
 1. AE t in distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n). snd t \<in> A (fst t)
[PROOF STEP]
by (auto simp: Pn_in_A intro!: AE_pmfI cong: AE_cong_simp)
[PROOF STATE]
proof (state)
this:
AE t in distr (T p S0) (count_space UNIV) (\<lambda>t. t !! n). snd t \<in> A (fst t)

goal (1 subgoal):
 1. AE t in T p S0. snd (t !! n) \<in> A (fst (t !! n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE t in T p S0. snd (t !! n) \<in> A (fst (t !! n))
[PROOF STEP]
by (auto intro!: AE_distrD[OF _ aux])
[PROOF STATE]
proof (state)
this:
AE t in T p S0. snd (t !! n) \<in> A (fst (t !! n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma X0 [simp]: "Xn p S0 0 = S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn p S0 0 = S0
[PROOF STEP]
using fst_K0 Xn_def
[PROOF STATE]
proof (prove)
using this:
map_pmf fst (K\<^sub>0 ?p ?S0.0) = ?S0.0
Xn ?p ?S0.0 ?n = map_pmf fst (Pn ?p ?S0.0 ?n)

goal (1 subgoal):
 1. Xn p S0 0 = S0
[PROOF STEP]
by auto


[STATEMENT]
lemma Xn_Suc: "Xn p S0 (Suc n) = Pn p S0 n \<bind> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn p S0 (Suc n) = Pn p S0 n \<bind> K
[PROOF STEP]
proof (induction n arbitrary: p S0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p S0. Xn p S0 (Suc 0) = Pn p S0 0 \<bind> K
 2. \<And>n p S0. (\<And>p S0. Xn p S0 (Suc n) = Pn p S0 n \<bind> K) \<Longrightarrow> Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>p S0. Xn p S0 (Suc 0) = Pn p S0 0 \<bind> K
 2. \<And>n p S0. (\<And>p S0. Xn p S0 (Suc n) = Pn p S0 n \<bind> K) \<Longrightarrow> Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn p S0 (Suc 0) = Pn p S0 0 \<bind> K
[PROOF STEP]
by (simp add: Pn.simps(2) Xn_def map_bind_pmf)
[PROOF STATE]
proof (state)
this:
Xn p S0 (Suc 0) = Pn p S0 0 \<bind> K

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. Xn p S0 (Suc n) = Pn p S0 n \<bind> K) \<Longrightarrow> Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. Xn p S0 (Suc n) = Pn p S0 n \<bind> K) \<Longrightarrow> Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
Xn ?p3 ?S0.3 (Suc n) = Pn ?p3 ?S0.3 n \<bind> K

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. Xn p S0 (Suc n) = Pn p S0 n \<bind> K) \<Longrightarrow> Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Xn ?p3 ?S0.3 (Suc n) = Pn ?p3 ?S0.3 n \<bind> K
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Xn ?p3 ?S0.3 (Suc n) = Pn ?p3 ?S0.3 n \<bind> K

goal (1 subgoal):
 1. Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K
[PROOF STEP]
by (simp add: Pn.simps(2) Xn_def map_bind_pmf bind_assoc_pmf)
[PROOF STATE]
proof (state)
this:
Xn p S0 (Suc (Suc n)) = Pn p S0 (Suc n) \<bind> K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Pn_markovian_eq_Xn_bind: "Pn (mk_markovian p) S0 n = K0 (p n) (Xn (mk_markovian p) S0 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian p) S0 n = K\<^sub>0 (p n) (Xn (mk_markovian p) S0 n)
[PROOF STEP]
proof (induction n arbitrary: p S0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p S0. Pn (mk_markovian p) S0 0 = K\<^sub>0 (p 0) (Xn (mk_markovian p) S0 0)
 2. \<And>n p S0. (\<And>p S0. Pn (mk_markovian p) S0 n = K\<^sub>0 (p n) (Xn (mk_markovian p) S0 n)) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>p S0. Pn (mk_markovian p) S0 0 = K\<^sub>0 (p 0) (Xn (mk_markovian p) S0 0)
 2. \<And>n p S0. (\<And>p S0. Pn (mk_markovian p) S0 n = K\<^sub>0 (p n) (Xn (mk_markovian p) S0 n)) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian p) S0 0 = K\<^sub>0 (p 0) (Xn (mk_markovian p) S0 0)
[PROOF STEP]
unfolding Xn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian p) S0 0 = K\<^sub>0 (p 0) (map_pmf fst (Pn (mk_markovian p) S0 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian p) S0 0 = K\<^sub>0 (p 0) (Xn (mk_markovian p) S0 0)

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. Pn (mk_markovian p) S0 n = K\<^sub>0 (p n) (Xn (mk_markovian p) S0 n)) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. Pn (mk_markovian p) S0 n = K\<^sub>0 (p n) (Xn (mk_markovian p) S0 n)) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian ?p3) ?S0.3 n = K\<^sub>0 (?p3 n) (Xn (mk_markovian ?p3) ?S0.3 n)

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. Pn (mk_markovian p) S0 n = K\<^sub>0 (p n) (Xn (mk_markovian p) S0 n)) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pn (mk_markovian ?p3) ?S0.3 n = K\<^sub>0 (?p3 n) (Xn (mk_markovian ?p3) ?S0.3 n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Pn (mk_markovian ?p3) ?S0.3 n = K\<^sub>0 (?p3 n) (Xn (mk_markovian ?p3) ?S0.3 n)

goal (1 subgoal):
 1. Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))
[PROOF STEP]
unfolding Xn_def K0_def
[PROOF STATE]
proof (prove)
using this:
Pn (mk_markovian ?p3) ?S0.3 n = map_pmf fst (Pn (mk_markovian ?p3) ?S0.3 n) \<bind> (\<lambda>s. ?p3 n s \<bind> (\<lambda>a. return_pmf (s, a)))

goal (1 subgoal):
 1. Pn (mk_markovian p) S0 (Suc n) = map_pmf fst (Pn (mk_markovian p) S0 (Suc n)) \<bind> (\<lambda>s. p (Suc n) s \<bind> (\<lambda>a. return_pmf (s, a)))
[PROOF STEP]
by (auto intro!: bind_pmf_cong simp: Pn.simps(2) map_bind_pmf Suc bind_assoc_pmf)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian p) S0 (Suc n) = K\<^sub>0 (p (Suc n)) (Xn (mk_markovian p) S0 (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Xn_Suc': "Xn p S0 (Suc n) = K0 (p []) S0 \<bind> (\<lambda>sa. Xn (\<pi>_Suc p sa) (K sa) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn p S0 (Suc n) = K\<^sub>0 (p []) S0 \<bind> (\<lambda>sa. Xn (\<pi>_Suc p sa) (K sa) n)
[PROOF STEP]
unfolding Xn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf fst (Pn p S0 (Suc n)) = K\<^sub>0 (p []) S0 \<bind> (\<lambda>sa. map_pmf fst (Pn (\<pi>_Suc p sa) (K sa) n))
[PROOF STEP]
by (auto simp: Pn.simps(2) map_bind_pmf)


[STATEMENT]
lemma set_pmf_X0 [simp]: "set_pmf (Xn p S0 0) = S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (Xn p S0 0) = set_pmf S0
[PROOF STEP]
using X0
[PROOF STATE]
proof (prove)
using this:
Xn ?p ?S0.0 0 = ?S0.0

goal (1 subgoal):
 1. set_pmf (Xn p S0 0) = set_pmf S0
[PROOF STEP]
by auto


[STATEMENT]
lemma set_pmf_PSuc: "set_pmf (Pn (mk_markovian p) S0 n) =
  {(s, a). s \<in> set_pmf (Xn (mk_markovian p) S0 n) \<and> a \<in> p n s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (Pn (mk_markovian p) S0 n) = {(s, a). s \<in> set_pmf (Xn (mk_markovian p) S0 n) \<and> a \<in> set_pmf (p n s)}
[PROOF STEP]
using set_pmf_K0 Pn_markovian_eq_Xn_bind
[PROOF STATE]
proof (prove)
using this:
set_pmf (K\<^sub>0 ?p ?S0.0) = {(s, a). s \<in> set_pmf ?S0.0 \<and> a \<in> set_pmf (?p s)}
Pn (mk_markovian ?p) ?S0.0 ?n = K\<^sub>0 (?p ?n) (Xn (mk_markovian ?p) ?S0.0 ?n)

goal (1 subgoal):
 1. set_pmf (Pn (mk_markovian p) S0 n) = {(s, a). s \<in> set_pmf (Xn (mk_markovian p) S0 n) \<and> a \<in> set_pmf (p n s)}
[PROOF STEP]
by auto


[STATEMENT]
lemma prob_K0_X [simp]: "measure_pmf.prob (K0 p S0) {(s, a). s = x} = pmf S0 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (K\<^sub>0 p S0) {(s, a). s = x} = pmf S0 x
[PROOF STEP]
unfolding K0_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (S0 \<bind> (\<lambda>s. map_pmf (Pair s) (p s))) {(s, a). s = x} = pmf S0 x
[PROOF STEP]
proof (subst measure_pmf_bind, subst measure_pmf.measure_bind[of _ _ "count_space UNIV"], goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. measure_pmf.random_variable S0 (subprob_algebra (count_space UNIV)) (\<lambda>x. measure_pmf (map_pmf (Pair x) (p x)))
 2. {(s, a). s = x} \<in> sets (count_space UNIV)
 3. measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. measure_pmf.random_variable S0 (subprob_algebra (count_space UNIV)) (\<lambda>x. measure_pmf (map_pmf (Pair x) (p x)))
 2. {(s, a). s = x} \<in> sets (count_space UNIV)
 3. measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.random_variable S0 (subprob_algebra (count_space UNIV)) (\<lambda>x. measure_pmf (map_pmf (Pair x) (p x)))
[PROOF STEP]
by (simp add: measure_pmf_in_subprob_algebra)
[PROOF STATE]
proof (state)
this:
measure_pmf.random_variable S0 (subprob_algebra (count_space UNIV)) (\<lambda>x. measure_pmf (map_pmf (Pair x) (p x)))

goal (2 subgoals):
 1. {(s, a). s = x} \<in> sets (count_space UNIV)
 2. measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {(s, a). s = x} \<in> sets (count_space UNIV)
 2. measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. {(s, a). s = x} \<in> sets (count_space UNIV)
 2. measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x
[PROOF STEP]
by (subst integral_measure_pmf_real[of "{x}"]) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation S0 (\<lambda>xa. measure_pmf.prob (map_pmf (Pair xa) (p xa)) {(s, a). s = x}) = pmf S0 x

goal (1 subgoal):
 1. {(s, a). s = x} \<in> sets (count_space UNIV)
[PROOF STEP]
qed simp