[STATEMENT]
lemma prob_Pn_X[simp]: "measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x
[PROOF STEP]
proof (induction n arbitrary: p S0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p S0. measure_pmf.prob (Pn p S0 0) {(s, a). s = x} = pmf (Xn p S0 0) x
 2. \<And>n p S0. (\<And>p S0. measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x) \<Longrightarrow> measure_pmf.prob (Pn p S0 (Suc n)) {(s, a). s = x} = pmf (Xn p S0 (Suc n)) x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>p S0. measure_pmf.prob (Pn p S0 0) {(s, a). s = x} = pmf (Xn p S0 0) x
 2. \<And>n p S0. (\<And>p S0. measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x) \<Longrightarrow> measure_pmf.prob (Pn p S0 (Suc n)) {(s, a). s = x} = pmf (Xn p S0 (Suc n)) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (Pn p S0 0) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (Xn p S0 0) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measure_pmf.prob (Pn p S0 0) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (Xn p S0 0) x

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x) \<Longrightarrow> measure_pmf.prob (Pn p S0 (Suc n)) {(s, a). s = x} = pmf (Xn p S0 (Suc n)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x) \<Longrightarrow> measure_pmf.prob (Pn p S0 (Suc n)) {(s, a). s = x} = pmf (Xn p S0 (Suc n)) x
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
measure_pmf.prob (Pn ?p3 ?S0.3 n) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (Xn ?p3 ?S0.3 n) x

goal (1 subgoal):
 1. \<And>n p S0. (\<And>p S0. measure_pmf.prob (Pn p S0 n) {(s, a). s = x} = pmf (Xn p S0 n) x) \<Longrightarrow> measure_pmf.prob (Pn p S0 (Suc n)) {(s, a). s = x} = pmf (Xn p S0 (Suc n)) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (Pn p S0 (Suc n)) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (Xn p S0 (Suc n)) x
[PROOF STEP]
unfolding Xn_Suc' Pn.simps(2) measure_pmf_bind
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. measure_pmf (Pn (\<pi>_Suc p x) (K x) n))) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (K\<^sub>0 (p []) S0 \<bind> (\<lambda>sa. Xn (\<pi>_Suc p sa) (K sa) n)) x
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
measure_pmf.prob (Pn ?p3 ?S0.3 n) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (Xn ?p3 ?S0.3 n) x

goal (1 subgoal):
 1. Sigma_Algebra.measure (measure_pmf (K\<^sub>0 (p []) S0) \<bind> (\<lambda>x. measure_pmf (Pn (\<pi>_Suc p x) (K x) n))) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (K\<^sub>0 (p []) S0 \<bind> (\<lambda>sa. Xn (\<pi>_Suc p sa) (K sa) n)) x
[PROOF STEP]
by (simp add: measure_pmf.measure_bind[of _ _ "count_space UNIV"] K0_def
        measure_pmf_in_subprob_algebra pmf_bind)
[PROOF STATE]
proof (state)
this:
measure_pmf.prob (Pn p S0 (Suc n)) {a. case a of (s, a) \<Rightarrow> s = x} = pmf (Xn p S0 (Suc n)) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_Pn_pair:
  assumes "sa \<in> set_pmf (Pn p S0 n)"
  shows "pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
have aux: "set_pmf (Pn p S0 n) \<inter> {(s, a). s = fst sa} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (Pn p S0 n) \<inter> {(s, a). s = fst sa} \<noteq> {}
[PROOF STEP]
using Xn_def assms
[PROOF STATE]
proof (prove)
using this:
Xn ?p ?S0.0 ?n = map_pmf fst (Pn ?p ?S0.0 ?n)
sa \<in> set_pmf (Pn p S0 n)

goal (1 subgoal):
 1. set_pmf (Pn p S0 n) \<inter> {(s, a). s = fst sa} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_pmf (Pn p S0 n) \<inter> {(s, a). s = fst sa} \<noteq> {}

goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
have aux': "({(s, a). s = fst sa} \<inter> snd -` {snd sa}) = {sa}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s, a). s = fst sa} \<inter> snd -` {snd sa} = {sa}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(s, a). s = fst sa} \<inter> snd -` {snd sa} = {sa}

goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sa \<in> set_pmf (Pn p S0 n)

goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
unfolding Y_cond_X_def pmf_map cond_pmf.rep_eq[OF aux]
[PROOF STATE]
proof (prove)
using this:
sa \<in> set_pmf (Pn p S0 n)

goal (1 subgoal):
 1. pmf (Pn p S0 n) sa = Sigma_Algebra.measure (uniform_measure (measure_pmf (Pn p S0 n)) {(s, a). s = fst sa}) (snd -` {snd sa}) * pmf (Xn p S0 n) (fst sa)
[PROOF STEP]
by (auto simp: Xn_def pmf_eq_0_set_pmf measure_pmf.emeasure_eq_measure aux' measure_pmf_single)
[PROOF STATE]
proof (state)
this:
pmf (Pn p S0 n) sa = pmf (Y_cond_X p S0 n (fst sa)) (snd sa) * pmf (Xn p S0 n) (fst sa)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_Pn:
  assumes "x \<in> set_pmf (Xn p S0 n)"
  shows "pmf (Pn p S0 n) (x,a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x
[PROOF STEP]
have aux: "set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}
[PROOF STEP]
using Xn_def assms
[PROOF STATE]
proof (prove)
using this:
Xn ?p ?S0.0 ?n = map_pmf fst (Pn ?p ?S0.0 ?n)
x \<in> set_pmf (Xn p S0 n)

goal (1 subgoal):
 1. set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}

goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x
[PROOF STEP]
have aux': "({(s, a). s = x} \<inter> snd -` {a}) = {(x, a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s, a). s = x} \<inter> snd -` {a} = {(x, a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(s, a). s = x} \<inter> snd -` {a} = {(x, a)}

goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf (Xn p S0 n)

goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x
[PROOF STEP]
unfolding Y_cond_X_def cond_pmf.rep_eq[OF aux] pmf_map
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf (Xn p S0 n)

goal (1 subgoal):
 1. pmf (Pn p S0 n) (x, a) = Sigma_Algebra.measure (uniform_measure (measure_pmf (Pn p S0 n)) {(s, a). s = x}) (snd -` {a}) * pmf (Xn p S0 n) x
[PROOF STEP]
by (auto simp: pmf_eq_0_set_pmf measure_pmf.emeasure_eq_measure aux' measure_pmf_single)
[PROOF STATE]
proof (state)
this:
pmf (Pn p S0 n) (x, a) = pmf (Y_cond_X p S0 n x) a * pmf (Xn p S0 n) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_Y_cond_X:
  assumes "x \<in> set_pmf (Xn p S0 n)"
  shows "pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x,a) / pmf (Xn p S0 n) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
have aux: "set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}
[PROOF STEP]
using Xn_def assms
[PROOF STATE]
proof (prove)
using this:
Xn ?p ?S0.0 ?n = map_pmf fst (Pn ?p ?S0.0 ?n)
x \<in> set_pmf (Xn p S0 n)

goal (1 subgoal):
 1. set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_pmf (Pn p S0 n) \<inter> {(s, a). s = x} \<noteq> {}

goal (1 subgoal):
 1. pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
have aux': "({(s, a). s = x} \<inter> snd -` {a}) = {(x, a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s, a). s = x} \<inter> snd -` {a} = {(x, a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(s, a). s = x} \<inter> snd -` {a} = {(x, a)}

goal (1 subgoal):
 1. pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
using assms aux'
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf (Xn p S0 n)
{(s, a). s = x} \<inter> snd -` {a} = {(x, a)}

goal (1 subgoal):
 1. pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
unfolding Y_cond_X_def
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf (Xn p S0 n)
{(s, a). s = x} \<inter> snd -` {a} = {(x, a)}

goal (1 subgoal):
 1. pmf (map_pmf snd (cond_pmf (Pn p S0 n) {(s, a). s = x})) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x
[PROOF STEP]
by (auto simp: cond_pmf.rep_eq[OF aux] pmf_map pmf_eq_0_set_pmf measure_pmf.emeasure_eq_measure
        measure_pmf_single)
[PROOF STATE]
proof (state)
this:
pmf (Y_cond_X p S0 n x) a = pmf (Pn p S0 n) (x, a) / pmf (Xn p S0 n) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Y_cond_X_0[simp]:
  assumes "x \<in> set_pmf S0"
  shows "Y_cond_X p S0 0 x = p [] x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y_cond_X p S0 0 x = p [] x
[PROOF STEP]
by (auto intro: pmf_eqI simp: assms pmf_Y_cond_X pmf_eq_0_set_pmf)


[STATEMENT]
lemma Y_cond_X_markovian[simp]:
  assumes h: "x \<in> Xn (mk_markovian p) S0 n"
  shows "Y_cond_X (mk_markovian p) S0 n x = p n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y_cond_X (mk_markovian p) S0 n x = p n x
[PROOF STEP]
by (auto intro!: pmf_eqI simp: pmf_Y_cond_X h Pn_markovian_eq_Xn_bind pmf_eq_0_set_pmf)


[STATEMENT]
lemma Pn_eq_Xn_Y_cond: "Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (\<lambda>a. (x, a)) (Y_cond_X p S0 n x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x))
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Pn p S0 0 = Xn p S0 0 \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 0 x))
 2. \<And>n. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x)) \<Longrightarrow> Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Pn p S0 0 = Xn p S0 0 \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 0 x))
 2. \<And>n. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x)) \<Longrightarrow> Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn p S0 0 = Xn p S0 0 \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 0 x))
[PROOF STEP]
by (auto simp: K0_iff intro: bind_pmf_cong)
[PROOF STATE]
proof (state)
this:
Pn p S0 0 = Xn p S0 0 \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 0 x))

goal (1 subgoal):
 1. \<And>n. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x)) \<Longrightarrow> Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x)) \<Longrightarrow> Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x))

goal (1 subgoal):
 1. \<And>n. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 n x)) \<Longrightarrow> Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))
[PROOF STEP]
proof (intro pmf_eqI; safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
fix a :: 's
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
fix b :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
have aux': "pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a,b)
      = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x.
          if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b) = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)
[PROOF STEP]
by (auto intro!: Bochner_Integration.integral_cong[OF refl]
          simp: Xn_def bind_map_pmf pmf_map pmf_bind measure_pmf_single)
[PROOF STATE]
proof (state)
this:
pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b) = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b) = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
have "\<dots> = measure_pmf.expectation (Pn p S0 (Suc n))
     (\<lambda>x. indicator {(s',a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))
[PROOF STEP]
proof (intro Bochner_Integration.integral_cong_AE AE_pmfI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)
 2. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))
 3. \<And>y. y \<in> set_pmf (Pn p S0 (Suc n)) \<Longrightarrow> (if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = indicat_real {(s', a'). s' = a} y * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)
 2. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))
 3. \<And>y. y \<in> set_pmf (Pn p S0 (Suc n)) \<Longrightarrow> (if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = indicat_real {(s', a'). s' = a} y * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)
[PROOF STEP]
assume h: "y \<in> set_pmf (Pn p S0 (Suc n))"
[PROOF STATE]
proof (state)
this:
y \<in> set_pmf (Pn p S0 (Suc n))

goal (3 subgoals):
 1. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)
 2. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))
 3. \<And>y. y \<in> set_pmf (Pn p S0 (Suc n)) \<Longrightarrow> (if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = indicat_real {(s', a'). s' = a} y * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)
[PROOF STEP]
hence h': "fst y \<in> set_pmf (Xn p S0 (Suc n))"
[PROOF STATE]
proof (prove)
using this:
y \<in> set_pmf (Pn p S0 (Suc n))

goal (1 subgoal):
 1. fst y \<in> set_pmf (Xn p S0 (Suc n))
[PROOF STEP]
by (metis mult_eq_0_iff pmf_Pn_pair pmf_eq_0_set_pmf)
[PROOF STATE]
proof (state)
this:
fst y \<in> set_pmf (Xn p S0 (Suc n))

goal (3 subgoals):
 1. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)
 2. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))
 3. \<And>y. y \<in> set_pmf (Pn p S0 (Suc n)) \<Longrightarrow> (if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = indicat_real {(s', a'). s' = a} y * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)
[PROOF STEP]
show "(if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) =
        indicat_real {(s', a'). s' = a} y *
        (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = indicat_real {(s', a'). s' = a} y * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)
[PROOF STEP]
by (auto simp: case_prod_beta' pmf_Y_cond_X[of "fst y" p S0 "(Suc n)" b, OF h'])
[PROOF STATE]
proof (state)
this:
(if fst y = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = indicat_real {(s', a'). s' = a} y * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)

goal (2 subgoals):
 1. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0)
 2. measure_pmf.random_variable (Pn p S0 (Suc n)) borel (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. if fst x = a then pmf (Y_cond_X p S0 (Suc n) a) b else 0) = measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a))

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
have "\<dots> = measure_pmf.prob (Pn p S0 (Suc n)) {(s',a'). s' = a} *
      pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)) = measure_pmf.prob (Pn p S0 (Suc n)) {(s', a'). s' = a} * pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)) = measure_pmf.prob (Pn p S0 (Suc n)) {(s', a'). s' = a} * pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (Pn p S0 (Suc n)) (\<lambda>x. indicat_real {(s', a'). s' = a} x * (pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a)) = measure_pmf.prob (Pn p S0 (Suc n)) {(s', a'). s' = a} * pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
have "\<dots> = pmf (Pn p S0 (Suc n)) (a,b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.prob (Pn p S0 (Suc n)) {(s', a'). s' = a} * pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a = pmf (Pn p S0 (Suc n)) (a, b)
[PROOF STEP]
using prob_Pn_X Xn_def pmf_Pn_pair pmf_eq_0_set_pmf
[PROOF STATE]
proof (prove)
using this:
measure_pmf.prob (Pn ?p ?S0.0 ?n) {(s, a). s = ?x} = pmf (Xn ?p ?S0.0 ?n) ?x
Xn ?p ?S0.0 ?n = map_pmf fst (Pn ?p ?S0.0 ?n)
?sa \<in> set_pmf (Pn ?p ?S0.0 ?n) \<Longrightarrow> pmf (Pn ?p ?S0.0 ?n) ?sa = pmf (Y_cond_X ?p ?S0.0 ?n (fst ?sa)) (snd ?sa) * pmf (Xn ?p ?S0.0 ?n) (fst ?sa)
(pmf ?M ?p = 0) = (?p \<notin> set_pmf ?M)

goal (1 subgoal):
 1. measure_pmf.prob (Pn p S0 (Suc n)) {(s', a'). s' = a} * pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a = pmf (Pn p S0 (Suc n)) (a, b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
measure_pmf.prob (Pn p S0 (Suc n)) {(s', a'). s' = a} * pmf (Pn p S0 (Suc n)) (a, b) / pmf (Xn p S0 (Suc n)) a = pmf (Pn p S0 (Suc n)) (a, b)

goal (1 subgoal):
 1. \<And>a b. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b) = pmf (Pn p S0 (Suc n)) (a, b)
[PROOF STEP]
show "pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind>
      (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)"
[PROOF STATE]
proof (prove)
using this:
pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b) = pmf (Pn p S0 (Suc n)) (a, b)

goal (1 subgoal):
 1. pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (Pn p S0 (Suc n)) (a, b) = pmf (Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))) (a, b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Pn p S0 (Suc n) = Xn p S0 (Suc n) \<bind> (\<lambda>x. map_pmf (Pair x) (Y_cond_X p S0 (Suc n) x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Pn_eq_Xn_Y_cond':
  "Pn p S0 n = Xn p S0 n \<bind> (\<lambda>s. Y_cond_X p S0 n s \<bind> (\<lambda>a. return_pmf (s,a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn p S0 n = Xn p S0 n \<bind> (\<lambda>s. Y_cond_X p S0 n s \<bind> (\<lambda>a. return_pmf (s, a)))
[PROOF STEP]
by (metis K0_def K0_iff Pn_eq_Xn_Y_cond)


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

goal (2 subgoals):
 1. \<And>S0 p. Pn (mk_markovian p) S0 (Suc 0) = Pn (mk_markovian p) S0 0 \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc 0)) (K sa))
 2. \<And>n S0 p. (\<And>S0 p. Pn (mk_markovian p) S0 (Suc n) = Pn (mk_markovian p) S0 n \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc n)) (K sa))) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc (Suc n)) = Pn (mk_markovian p) S0 (Suc n) \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc (Suc n))) (K sa))
[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 (Suc 0) = Pn (mk_markovian p) S0 0 \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc 0)) (K sa))
[PROOF STEP]
by (auto intro: bind_pmf_cong simp: Pn.simps(2) \<pi>_Suc_def)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian p) S0 (Suc 0) = Pn (mk_markovian p) S0 0 \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc 0)) (K sa))

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

goal (1 subgoal):
 1. \<And>n S0 p. (\<And>S0 p. Pn (mk_markovian p) S0 (Suc n) = Pn (mk_markovian p) S0 n \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc n)) (K sa))) \<Longrightarrow> Pn (mk_markovian p) S0 (Suc (Suc n)) = Pn (mk_markovian p) S0 (Suc n) \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc (Suc n))) (K sa))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian p) S0 (Suc (Suc n)) = Pn (mk_markovian p) S0 (Suc n) \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc (Suc n))) (K sa))
[PROOF STEP]
by (auto simp add: Suc bind_assoc_pmf Pn.simps(2)[of _ S0] intro: bind_pmf_cong)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian p) S0 (Suc (Suc n)) = Pn (mk_markovian p) S0 (Suc n) \<bind> (\<lambda>sa. K\<^sub>0 (p (Suc (Suc n))) (K sa))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Y0: "Yn p S0 0 = S0 \<bind> p []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Yn p S0 0 = S0 \<bind> p []
[PROOF STEP]
by (simp add: Yn_def K0_iff map_bind_pmf map_pmf_comp)


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

goal (2 subgoals):
 1. \<And>p S0. Yn (mk_markovian p) S0 0 = Xn (mk_markovian p) S0 0 \<bind> p 0
 2. \<And>n p S0. (\<And>p S0. Yn (mk_markovian p) S0 n = Xn (mk_markovian p) S0 n \<bind> p n) \<Longrightarrow> Yn (mk_markovian p) S0 (Suc n) = Xn (mk_markovian p) S0 (Suc n) \<bind> p (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Yn (mk_markovian p) S0 0 = Xn (mk_markovian p) S0 0 \<bind> p 0
[PROOF STEP]
by (auto simp: Y0)
[PROOF STATE]
proof (state)
this:
Yn (mk_markovian p) S0 0 = Xn (mk_markovian p) S0 0 \<bind> p 0

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_\<Pi>\<^sub>M\<^sub>R_as_markovian:
  assumes p: "is_policy p"
  shows "as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R
[PROOF STEP]
have aux: "\<And>hs s. s \<in> set_pmf (Xn p S0 hs) \<Longrightarrow> set_pmf ((Pn p S0 hs)) \<inter> {(s', a). s' = s} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hs s. s \<in> set_pmf (Xn p S0 hs) \<Longrightarrow> set_pmf (Pn p S0 hs) \<inter> {(s', a). s' = s} \<noteq> {}
[PROOF STEP]
by (simp add: measure_pmf_zero_iff[symmetric] pmf_eq_0_set_pmf)
[PROOF STATE]
proof (state)
this:
?s3 \<in> set_pmf (Xn p S0 ?hs3) \<Longrightarrow> set_pmf (Pn p S0 ?hs3) \<inter> {(s', a). s' = ?s3} \<noteq> {}

goal (1 subgoal):
 1. as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?s3 \<in> set_pmf (Xn p S0 ?hs3) \<Longrightarrow> set_pmf (Pn p S0 ?hs3) \<inter> {(s', a). s' = ?s3} \<noteq> {}

goal (1 subgoal):
 1. as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R
[PROOF STEP]
using assms A_ne Pn_in_A
[PROOF STATE]
proof (prove)
using this:
?s3 \<in> set_pmf (Xn p S0 ?hs3) \<Longrightarrow> set_pmf (Pn p S0 ?hs3) \<inter> {(s', a). s' = ?s3} \<noteq> {}
is_policy p
A ?s \<noteq> {}
\<lbrakk>is_policy ?p; (?s, ?a) \<in> set_pmf (Pn ?p ?S0.0 ?n)\<rbrakk> \<Longrightarrow> ?a \<in> A ?s

goal (1 subgoal):
 1. as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R
[PROOF STEP]
unfolding is_dec_def Y_cond_X_def
[PROOF STATE]
proof (prove)
using this:
?s3 \<in> set_pmf (Xn p S0 ?hs3) \<Longrightarrow> set_pmf (Pn p S0 ?hs3) \<inter> {(s', a). s' = ?s3} \<noteq> {}
is_policy p
A ?s \<noteq> {}
\<lbrakk>is_policy ?p; (?s, ?a) \<in> set_pmf (Pn ?p ?S0.0 ?n)\<rbrakk> \<Longrightarrow> ?a \<in> A ?s

goal (1 subgoal):
 1. (\<lambda>n x. if x \<in> set_pmf (Xn p S0 n) then map_pmf snd (cond_pmf (Pn p S0 n) {(s, a). s = x}) else return_pmf (SOME a. a \<in> A x)) \<in> {p. \<forall>n. p n \<in> {d. \<forall>s. set_pmf (d s) \<subseteq> A s}}
[PROOF STEP]
by (auto simp: some_in_eq)
[PROOF STATE]
proof (state)
this:
as_markovian p S0 \<in> \<Pi>\<^sub>M\<^sub>R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_policy_as_markovian: "is_policy p \<Longrightarrow> is_policy (mk_markovian (as_markovian p S0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_policy p \<Longrightarrow> is_policy (mk_markovian (as_markovian p S0))
[PROOF STEP]
using is_\<Pi>\<^sub>M\<^sub>R_as_markovian \<Pi>\<^sub>M\<^sub>R_imp_policies
[PROOF STATE]
proof (prove)
using this:
is_policy ?p \<Longrightarrow> as_markovian ?p ?S0.0 \<in> \<Pi>\<^sub>M\<^sub>R
?p \<in> \<Pi>\<^sub>M\<^sub>R \<Longrightarrow> mk_markovian ?p \<in> \<Pi>\<^sub>H\<^sub>R

goal (1 subgoal):
 1. is_policy p \<Longrightarrow> is_policy (mk_markovian (as_markovian p S0))
[PROOF STEP]
by auto


[STATEMENT]
theorem Pn_as_markovian_eq: "Pn (mk_markovian (as_markovian p S0)) S0 = Pn p S0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian (as_markovian p S0)) S0 = Pn p S0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. Pn (mk_markovian (as_markovian p S0)) S0 x = Pn p S0 x
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. Pn (mk_markovian (as_markovian p S0)) S0 x = Pn p S0 x
[PROOF STEP]
show "Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Pn (mk_markovian (as_markovian p S0)) S0 0 = Pn p S0 0
 2. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Pn (mk_markovian (as_markovian p S0)) S0 0 = Pn p S0 0
 2. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn (mk_markovian (as_markovian p S0)) S0 0 = Pn p S0 0
[PROOF STEP]
by (auto intro!: map_pmf_cong bind_pmf_cong simp: K0_def)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian (as_markovian p S0)) S0 0 = Pn p S0 0

goal (1 subgoal):
 1. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n

goal (1 subgoal):
 1. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
have "\<And>x. x \<in> Xn p S0 (Suc n) \<Longrightarrow>
      Y_cond_X (mk_markovian (as_markovian p S0)) S0 (Suc n) x = Y_cond_X p S0 (Suc n) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf (Xn p S0 (Suc n)) \<Longrightarrow> Y_cond_X (mk_markovian (as_markovian p S0)) S0 (Suc n) x = Y_cond_X p S0 (Suc n) x
[PROOF STEP]
by (auto simp: Suc.IH Xn_Suc)
[PROOF STATE]
proof (state)
this:
?x3 \<in> set_pmf (Xn p S0 (Suc n)) \<Longrightarrow> Y_cond_X (mk_markovian (as_markovian p S0)) S0 (Suc n) ?x3 = Y_cond_X p S0 (Suc n) ?x3

goal (1 subgoal):
 1. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x3 \<in> set_pmf (Xn p S0 (Suc n)) \<Longrightarrow> Y_cond_X (mk_markovian (as_markovian p S0)) S0 (Suc n) ?x3 = Y_cond_X p S0 (Suc n) ?x3

goal (1 subgoal):
 1. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
have "Xn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Xn p S0 (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Xn p S0 (Suc n)
[PROOF STEP]
by (simp add: Xn_Suc Suc.IH)
[PROOF STATE]
proof (state)
this:
Xn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Xn p S0 (Suc n)

goal (1 subgoal):
 1. \<And>n. Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n \<Longrightarrow> Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x3 \<in> set_pmf (Xn p S0 (Suc n)) \<Longrightarrow> Y_cond_X (mk_markovian (as_markovian p S0)) S0 (Suc n) ?x3 = Y_cond_X p S0 (Suc n) ?x3
Xn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Xn p S0 (Suc n)
[PROOF STEP]
show "Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)"
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> set_pmf (Xn p S0 (Suc n)) \<Longrightarrow> Y_cond_X (mk_markovian (as_markovian p S0)) S0 (Suc n) ?x3 = Y_cond_X p S0 (Suc n) ?x3
Xn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Xn p S0 (Suc n)

goal (1 subgoal):
 1. Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)
[PROOF STEP]
by (auto intro: bind_pmf_cong simp: Pn_eq_Xn_Y_cond)
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian (as_markovian p S0)) S0 (Suc n) = Pn p S0 (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Pn (mk_markovian (as_markovian p S0)) S0 n = Pn p S0 n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<T>_eq_return_distr: "\<T> p s =
  measure_pmf (p [] s) \<bind> (\<lambda>a. distr (T (\<pi>_Suc p (s,a)) (K (s,a))) S ((##) (s,a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. distr (T (\<pi>_Suc p (s, a)) (K (s, a))) (stream_space (count_space UNIV)) ((##) (s, a)))
[PROOF STEP]
unfolding \<T>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T p (return_pmf s) = measure_pmf (p [] s) \<bind> (\<lambda>a. distr (T (\<pi>_Suc p (s, a)) (K (s, a))) (stream_space (count_space UNIV)) ((##) (s, a)))
[PROOF STEP]
by (subst T_eq_distr) (fastforce intro!: bind_distr subprob_space.subprob_space_distr
      simp: K0_iff map_pmf_rep_eq space_subprob_algebra bind_return_pmf)+


[STATEMENT]
lemma \<T>_eq_return:
  shows "\<T> p s = do {
    y \<leftarrow> measure_pmf (p [] s);
    \<omega> \<leftarrow> T (\<pi>_Suc p (s,y)) (K (s,y));
    return S ((s,y) ## \<omega>)
  }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>y. T (\<pi>_Suc p (s, y)) (K (s, y)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, y) ## \<omega>)))
[PROOF STEP]
by (auto simp: \<T>_eq_return_distr bind_return_distr' prob_space.not_empty intro!: bind_cong)


[STATEMENT]
lemma \<T>_return:
  shows "T p S0 = measure_pmf S0 \<bind> \<T> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
have "T p S0 = measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (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. T p S0 = measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))
[PROOF STEP]
unfolding T_eq_distr[of p] K0_iff measure_pmf_bind
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)) = measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T p S0 = measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))

goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T p S0 = measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))

goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
have "\<dots> = measure_pmf S0 \<bind>
    (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair 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. measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)) = measure_pmf S0 \<bind> (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)))
[PROOF STEP]
using measurable_measure_pmf
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. measure_pmf (?M x)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra (count_space UNIV)

goal (1 subgoal):
 1. measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)) = measure_pmf S0 \<bind> (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)))
[PROOF STEP]
by (subst bind_assoc[where N = "count_space UNIV", where R = S])
      (fastforce intro!: prob_space_imp_subprob_space prob_space.prob_space_distr
        simp: space_subprob_algebra prob_space_measure_pmf map_pmf_rep_eq)+
[PROOF STATE]
proof (state)
this:
measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)) = measure_pmf S0 \<bind> (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)))

goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf S0 \<bind> (\<lambda>x. measure_pmf (map_pmf (Pair x) (p [] x))) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)) = measure_pmf S0 \<bind> (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa)))

goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
have "\<dots> = measure_pmf S0 \<bind> \<T> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf S0 \<bind> (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
by (subst bind_distr[where K  = S])
      (auto intro!: prob_space_imp_subprob_space prob_space.prob_space_distr bind_cong
        simp: space_subprob_algebra \<T>_eq_return_distr)
[PROOF STATE]
proof (state)
this:
measure_pmf S0 \<bind> (\<lambda>x. distr (measure_pmf (p [] x)) (count_space UNIV) (Pair x) \<bind> (\<lambda>sa. distr (T (\<pi>_Suc p sa) (K sa)) (stream_space (count_space UNIV)) ((##) sa))) = measure_pmf S0 \<bind> \<T> p

goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
T p S0 = measure_pmf S0 \<bind> \<T> p

goal (1 subgoal):
 1. T p S0 = measure_pmf S0 \<bind> \<T> p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
T p S0 = measure_pmf S0 \<bind> \<T> p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<T>_eq:
  shows "\<T> p s = do {
  a \<leftarrow> measure_pmf (p [] s);
  s' \<leftarrow> measure_pmf (K (s,a));
  w \<leftarrow> \<T> (\<pi>_Suc p (s,a)) s';
  return S ((s,a)##w)
}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, a)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
by (subst \<T>_return_eq) (auto simp add: \<T>_def )


[STATEMENT]
lemma \<T>_prob_space[intro]: "prob_space (\<T> p s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (\<T> p s)
[PROOF STEP]
by (metis \<T>_def prob_space_T)


[STATEMENT]
lemma \<T>_sets[measurable_cong]:
  "sets (\<T> p s) = sets S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (\<T> p s) = sets (stream_space (count_space UNIV))
[PROOF STEP]
by (simp add: \<T>_def sets_T)


[STATEMENT]
lemma measurable_ident_Suc'[measurable]:
  "(\<lambda>x. x) \<in> \<T> (\<pi>_Suc p sa) s' \<rightarrow>\<^sub>M S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x) \<in> \<T> (\<pi>_Suc p sa) s' \<rightarrow>\<^sub>M stream_space (count_space UNIV)
[PROOF STEP]
by (simp add: \<T>_def)


[STATEMENT]
lemma nn_integral_\<T>:
  fixes f :: "('s \<times> 'a) stream \<Rightarrow> real"
  assumes f[measurable]: "f \<in> borel_measurable S"
  shows "(\<integral>\<^sup>+t. f t \<partial>\<T> p s)
    = \<integral>\<^sup>+a. \<integral>\<^sup>+s'. \<integral>\<^sup>+t'. f ((s,a)##t') \<partial>\<T> (\<pi>_Suc p (s,a)) s' \<partial>K (s,a) \<partial>p [] s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
have "(\<integral>\<^sup>+t. f t \<partial>\<T> p s) =
  \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (f y) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return S ((s, x) ## w))) \<partial>(p [] s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s)
[PROOF STEP]
unfolding \<T>_eq[of p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, a)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w)))) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s)
[PROOF STEP]
by (subst nn_integral_bind[of _ S])
      (auto intro!: measure_pmf.bind_in_space subprob_space.bind_in_space simp: \<T>_prob_space prob_space_imp_subprob_space)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ y. (f y) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return S ((s, x) ## w))
              \<partial>measure_pmf (K (s, x)) \<partial>(p [] s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
by (subst nn_integral_bind[of _ S])
      (auto intro!: subprob_space.bind_in_space simp: \<T>_prob_space prob_space_imp_subprob_space)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. \<integral>\<^sup>+ x. ennreal (f x) \<partial>measure_pmf (K (s, x)) \<bind> (\<lambda>s'. \<T> (\<pi>_Suc p (s, x)) s' \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w))) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ y. (f y) \<partial>distr (\<T> (\<pi>_Suc p (s, x)) xa) S ((##) (s, x)) \<partial>measure_pmf (K (s, x)) \<partial>(p [] s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>distr (\<T> (\<pi>_Suc p (s, x)) xa) (stream_space (count_space UNIV)) ((##) (s, x)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
by (auto simp add: bind_return_distr' \<T>_prob_space prob_space.not_empty)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>distr (\<T> (\<pi>_Suc p (s, x)) xa) (stream_space (count_space UNIV)) ((##) (s, x)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, x) ## w)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>distr (\<T> (\<pi>_Suc p (s, x)) xa) (stream_space (count_space UNIV)) ((##) (s, x)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ xa. (f ((s, x) ## xa)) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<partial>measure_pmf (K (s, x)) \<partial>(p [] s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>distr (\<T> (\<pi>_Suc p (s, x)) xa) (stream_space (count_space UNIV)) ((##) (s, x)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ xa. ennreal (f ((s, x) ## xa)) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
by (auto simp: nn_integral_distr)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ x. ennreal (f x) \<partial>distr (\<T> (\<pi>_Suc p (s, x)) xa) (stream_space (count_space UNIV)) ((##) (s, x)) \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s) = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ xa. ennreal (f ((s, x) ## xa)) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ xa. ennreal (f ((s, x) ## xa)) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ x. \<integral>\<^sup>+ xa. \<integral>\<^sup>+ xa. ennreal (f ((s, x) ## xa)) \<partial>\<T> (\<pi>_Suc p (s, x)) xa \<partial>measure_pmf (K (s, x)) \<partial>measure_pmf (p [] s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) \<partial>\<T> p s = \<integral>\<^sup>+ a. \<integral>\<^sup>+ s'. \<integral>\<^sup>+ x. ennreal (f ((s, a) ## x)) \<partial>\<T> (\<pi>_Suc p (s, a)) s' \<partial>measure_pmf (K (s, a)) \<partial>measure_pmf (p [] s)

goal:
No subgoals!
[PROOF STEP]
qed


[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[measurable]: "f \<in> borel_measurable S"
  shows "(\<integral>t. f t \<partial>\<T> p s)
    = \<integral>a. \<integral>s'. \<integral>t'. f ((s,a)##t') \<partial>\<T> (\<pi>_Suc p (s,a)) s' \<partial>K (s,a) \<partial>p [] s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (\<T> p s) f = measure_pmf.expectation (p [] s) (\<lambda>a. measure_pmf.expectation (K (s, a)) (\<lambda>s'. LINT t'|\<T> (\<pi>_Suc p (s, a)) s'. f ((s, a) ## t')))
[PROOF STEP]
unfolding \<T>_def integral_T[OF f_bounded f] K0_iff bind_return_pmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (map_pmf (Pair s) (p [] s)) (\<lambda>sa. LINT t'|T (\<pi>_Suc p sa) (K sa). f (sa ## t')) = measure_pmf.expectation (p [] s) (\<lambda>a. measure_pmf.expectation (K (s, a)) (\<lambda>s'. LINT t'|T (\<pi>_Suc p (s, a)) (return_pmf s'). f ((s, a) ## t')))
[PROOF STEP]
unfolding \<T>_return[of "\<pi>_Suc p _"] integral_map_pmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (p [] s) (\<lambda>x. LINT t'|(measure_pmf (K (s, x)) \<bind> \<T> (\<pi>_Suc p (s, x))). f ((s, x) ## t')) = measure_pmf.expectation (p [] s) (\<lambda>a. measure_pmf.expectation (K (s, a)) (\<lambda>s'. LINT t'|(measure_pmf (return_pmf s') \<bind> \<T> (\<pi>_Suc p (s, a))). f ((s, a) ## t')))
[PROOF STEP]
using \<T>_return[of "\<pi>_Suc p _", symmetric]
[PROOF STATE]
proof (prove)
using this:
measure_pmf ?S0.0 \<bind> \<T> (\<pi>_Suc p ?uu) = T (\<pi>_Suc p ?uu) ?S0.0

goal (1 subgoal):
 1. measure_pmf.expectation (p [] s) (\<lambda>x. LINT t'|(measure_pmf (K (s, x)) \<bind> \<T> (\<pi>_Suc p (s, x))). f ((s, x) ## t')) = measure_pmf.expectation (p [] s) (\<lambda>a. measure_pmf.expectation (K (s, a)) (\<lambda>s'. LINT t'|(measure_pmf (return_pmf s') \<bind> \<T> (\<pi>_Suc p (s, a))). f ((s, a) ## t')))
[PROOF STEP]
by (subst integral_bind[OF _ f_bounded, where B' = 1, where K = S])
    (auto simp: \<T>_def intro: prob_space.emeasure_le_1)


[STATEMENT]
lemma pmf_K_st: "pmf (K_st d s) t = \<integral>a. pmf (K(s, a)) t \<partial>d s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (K_st d s) t = measure_pmf.expectation (d s) (\<lambda>a. pmf (K (s, a)) t)
[PROOF STEP]
unfolding K_st_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (d s \<bind> (\<lambda>a. K (s, a))) t = measure_pmf.expectation (d s) (\<lambda>a. pmf (K (s, a)) t)
[PROOF STEP]
by (subst pmf_bind) auto


[STATEMENT]
lemma P0'[simp]: "Pn' p s 0 = K0' (p []) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn' p s 0 = K0' (p []) s
[PROOF STEP]
by (simp add: Pn'_def K0'_def K0_iff bind_return_pmf)


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

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


[STATEMENT]
lemma Pn_return_pmf: "S0 \<bind> (\<lambda>s'. Pn p (return_pmf s') n) = Pn p S0 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S0 \<bind> (\<lambda>s'. Pn p (return_pmf s') n) = Pn p S0 n
[PROOF STEP]
by (induction n arbitrary: p S0)
    (auto intro: bind_pmf_cong simp add: Pn.simps(2) K0_def bind_assoc_pmf bind_return_pmf)


[STATEMENT]
lemma PSuc': "Pn' p s (Suc n) = K0' (p []) s \<bind> (\<lambda>sa. K sa \<bind> (\<lambda>s'. Pn' (\<pi>_Suc p sa) s' n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn' p s (Suc n) = K0' (p []) s \<bind> (\<lambda>sa. K sa \<bind> (\<lambda>s'. Pn' (\<pi>_Suc p sa) s' n))
[PROOF STEP]
unfolding Pn'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn p (return_pmf s) (Suc n) = K0' (p []) s \<bind> (\<lambda>sa. K sa \<bind> (\<lambda>s'. Pn (\<pi>_Suc p sa) (return_pmf s') n))
[PROOF STEP]
by (auto intro!: bind_pmf_cong
      simp: Pn.simps(2) Pn_return_pmf K0_iff K0'_def bind_return_pmf map_bind_pmf bind_map_pmf)


[STATEMENT]
lemma PSuc'_markovian:
  "Pn' (mk_markovian p) s (Suc n) = K_st (p 0) s \<bind> (\<lambda>s'. Pn' (mk_markovian (p \<circ> Suc)) s' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn' (mk_markovian p) s (Suc n) = K_st (p 0) s \<bind> (\<lambda>s'. Pn' (mk_markovian (p \<circ> Suc)) s' n)
[PROOF STEP]
unfolding PSuc'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K0' (mk_markovian p []) s \<bind> (\<lambda>sa. K sa \<bind> (\<lambda>s'. Pn' (\<pi>_Suc (mk_markovian p) sa) s' n)) = K_st (p 0) s \<bind> (\<lambda>s'. Pn' (mk_markovian (p \<circ> Suc)) s' n)
[PROOF STEP]
by (auto simp: bind_map_pmf bind_assoc_pmf comp_def K0'_def K_st_def intro!: bind_pmf_cong)


[STATEMENT]
lemma Xn'_Suc: "Xn' p s (Suc n) = Pn' p s n \<bind> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn' p s (Suc n) = Pn' p s n \<bind> K
[PROOF STEP]
by (auto simp: Xn_Suc Xn'_def Pn'_def)


[STATEMENT]
lemma Xn'_Pn': "Xn' p s n = map_pmf fst (Pn' p s n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn' p s n = map_pmf fst (Pn' p s n)
[PROOF STEP]
by (simp add: Xn_def Xn'_def Pn'_def)


[STATEMENT]
lemma Suc_Xn': "Xn' p s (Suc n) = p [] s \<bind> (\<lambda>a. K (s,a) \<bind> (\<lambda>s'. Xn' (\<pi>_Suc p (s,a)) s' n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn' p s (Suc n) = p [] s \<bind> (\<lambda>a. K (s, a) \<bind> (\<lambda>s'. Xn' (\<pi>_Suc p (s, a)) s' n))
[PROOF STEP]
by (auto simp: Xn'_Pn' map_bind_pmf bind_map_pmf PSuc' K0'_def)


[STATEMENT]
lemma Suc_Xn'_markovian:
  "Xn' (mk_markovian p) s (Suc n) = K_st (p 0) s \<bind> (\<lambda>s'. Xn' (mk_markovian (\<lambda>n. p (Suc n))) s' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn' (mk_markovian p) s (Suc n) = K_st (p 0) s \<bind> (\<lambda>s'. Xn' (mk_markovian (\<lambda>n. p (Suc n))) s' n)
[PROOF STEP]
by (auto simp: K_st_def bind_assoc_pmf Suc_Xn')


[STATEMENT]
lemma Xn'_split: "Xn' (mk_markovian p) s (n + m) =
  Xn' (mk_markovian p) s n \<bind> (\<lambda>s. Xn' (mk_markovian (\<lambda>i. p (i + n))) s m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn' (mk_markovian p) s (n + m) = Xn' (mk_markovian p) s n \<bind> (\<lambda>s. Xn' (mk_markovian (\<lambda>i. p (i + n))) s m)
[PROOF STEP]
by (induction n arbitrary: p s) (auto intro!: bind_pmf_cong simp: bind_assoc_pmf bind_return_pmf Suc_Xn')


[STATEMENT]
lemma Yn'_markovian: "Yn' (mk_markovian p) s n = Xn' (mk_markovian p) s n \<bind> p n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Yn' (mk_markovian p) s n = Xn' (mk_markovian p) s n \<bind> p n
[PROOF STEP]
unfolding Yn'_def Xn'_def Yn_markovian
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn (mk_markovian p) (return_pmf s) n \<bind> p n = Xn (mk_markovian p) (return_pmf s) n \<bind> p n
[PROOF STEP]
by simp


[STATEMENT]
lemma Pn'_markovian_eq_Xn'_bind: "Pn' (mk_markovian p) s n = Xn' (mk_markovian p) s n \<bind> K0' (p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pn' (mk_markovian p) s n = Xn' (mk_markovian p) s n \<bind> K0' (p n)
[PROOF STEP]
unfolding Xn'_def Pn'_def K0'_def K0_iff Pn_markovian_eq_Xn_bind
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xn (mk_markovian p) (return_pmf s) n \<bind> (\<lambda>s. map_pmf (Pair s) (p n s)) = Xn (mk_markovian p) (return_pmf s) n \<bind> (\<lambda>s. map_pmf (Pair s) (p n s))
[PROOF STEP]
by simp


[STATEMENT]
lemma Pn'_eq_\<T>: "measure_pmf (Pn' p s n) = distr (\<T> p s) (count_space UNIV) (\<lambda>t. t !! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (Pn' p s n) = distr (\<T> p s) (count_space UNIV) (\<lambda>t. t !! n)
[PROOF STEP]
by (auto simp: \<T>_def Pn'_def Pn_eq_T)


[STATEMENT]
lemma App_mono:
  "(t, t') \<in> red\<^sup>* \<Longrightarrow> (u, u') \<in> red\<^sup>* \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
assume "(t, t') \<in> red\<^sup>*"
[PROOF STATE]
proof (state)
this:
(t, t') \<in> red\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
hence "(` t u, ` t' u) \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(t, t') \<in> red\<^sup>*

goal (1 subgoal):
 1. (` t u, ` t' u) \<in> red\<^sup>*
[PROOF STEP]
by (induct t' rule: rtrancl_induct) (auto intro: rtrancl_into_rtrancl red.intros)
[PROOF STATE]
proof (state)
this:
(` t u, ` t' u) \<in> red\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(` t u, ` t' u) \<in> red\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
assume "(u, u') \<in> red\<^sup>*"
[PROOF STATE]
proof (state)
this:
(u, u') \<in> red\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
hence "(` t' u, ` t' u') \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(u, u') \<in> red\<^sup>*

goal (1 subgoal):
 1. (` t' u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
by (induct u' rule: rtrancl_induct) (auto intro: rtrancl_into_rtrancl red.intros)
[PROOF STATE]
proof (state)
this:
(` t' u, ` t' u') \<in> red\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>(t, t') \<in> red\<^sup>*; (u, u') \<in> red\<^sup>*\<rbrakk> \<Longrightarrow> (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(` t u, ` t' u) \<in> red\<^sup>*
(` t' u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(` t u, ` t' u) \<in> red\<^sup>*
(` t' u, ` t' u') \<in> red\<^sup>*

goal (1 subgoal):
 1. (` t u, ` t' u') \<in> red\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(` t u, ` t' u') \<in> red\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bullet_app_red:
  "(` t u, bullet_app t u) \<in> red\<^sup>="
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (` t u, bullet_app t u) \<in> red\<^sup>=
[PROOF STEP]
by (induct t u rule: bullet_app.induct) (auto intro: red.intros)


[STATEMENT]
lemma bullet_app_redsI:
  "(s, ` t u) \<in> red\<^sup>* \<Longrightarrow> (s, bullet_app t u) \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, ` t u) \<in> red\<^sup>* \<Longrightarrow> (s, bullet_app t u) \<in> red\<^sup>*
[PROOF STEP]
using bullet_app_red[of t u]
[PROOF STATE]
proof (prove)
using this:
(` t u, bullet_app t u) \<in> red\<^sup>=

goal (1 subgoal):
 1. (s, ` t u) \<in> red\<^sup>* \<Longrightarrow> (s, bullet_app t u) \<in> red\<^sup>*
[PROOF STEP]
by auto


[STATEMENT]
lemma bullet_app_redL:
  "(t, t') \<in> red \<Longrightarrow> (bullet_app t u, bullet_app t' u) \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t, t') \<in> red \<Longrightarrow> (bullet_app t u, bullet_app t' u) \<in> red\<^sup>*
[PROOF STEP]
by (induct t u rule: bullet_app.induct)
   (auto 0 6 intro: App_mono bullet_app_redsI elim: red.cases simp only: bullet_app.simps)


[STATEMENT]
lemma bullet_app_redR:
  "(u, u') \<in> red \<Longrightarrow> (bullet_app t u, bullet_app t u') \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, u') \<in> red \<Longrightarrow> (bullet_app t u, bullet_app t u') \<in> red\<^sup>*
[PROOF STEP]
by (induct t u rule: bullet_app.induct) (auto intro: App_mono)


[STATEMENT]
lemma bullet_app_mono:
  assumes "(t, t') \<in> red\<^sup>*" "(u, u') \<in> red\<^sup>*" shows "(bullet_app t u, bullet_app t' u') \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
have "(bullet_app t u, bullet_app t' u) \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u) \<in> red\<^sup>*
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(t, t') \<in> red\<^sup>*

goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u) \<in> red\<^sup>*
[PROOF STEP]
by (induct t' rule: rtrancl_induct) (auto intro: rtrancl_trans bullet_app_redL)
[PROOF STATE]
proof (state)
this:
(bullet_app t u, bullet_app t' u) \<in> red\<^sup>*

goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(bullet_app t u, bullet_app t' u) \<in> red\<^sup>*

goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
have "(bullet_app t' u, bullet_app t' u') \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bullet_app t' u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(u, u') \<in> red\<^sup>*

goal (1 subgoal):
 1. (bullet_app t' u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
by (induct u' rule: rtrancl_induct) (auto intro: rtrancl_trans bullet_app_redR)
[PROOF STATE]
proof (state)
this:
(bullet_app t' u, bullet_app t' u') \<in> red\<^sup>*

goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(bullet_app t u, bullet_app t' u) \<in> red\<^sup>*
(bullet_app t' u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(bullet_app t u, bullet_app t' u) \<in> red\<^sup>*
(bullet_app t' u, bullet_app t' u') \<in> red\<^sup>*

goal (1 subgoal):
 1. (bullet_app t u, bullet_app t' u') \<in> red\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(bullet_app t u, bullet_app t' u') \<in> red\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bullet_incremental:
  "(t, bullet t) \<in> red\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t, bullet t) \<in> red\<^sup>*
[PROOF STEP]
by (induct t rule: bullet.induct) (auto intro: App_mono bullet_app_redsI)


[STATEMENT]
lemma guha_table_semantics_ex2res:
    assumes ta: "CARD('a) \<ge> 2" (* if there's only one action, the whole thing is moot. *)
	assumes ms: "\<exists>ff. \<gamma> ff p" (* if our matcher rejects the packet for any match condition, it is borked. *)
	shows "\<exists>ft (a1 :: 'a) (a2 :: 'a). a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
from ms
[PROOF STATE]
proof (chain)
picking this:
\<exists>ff. \<gamma> ff p
[PROOF STEP]
obtain ff  where m: "\<gamma> ff p"
[PROOF STATE]
proof (prove)
using this:
\<exists>ff. \<gamma> ff p

goal (1 subgoal):
 1. (\<And>ff. \<gamma> ff p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<gamma> ff p

goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
from ta
[PROOF STATE]
proof (chain)
picking this:
2 \<le> CARD('a)
[PROOF STEP]
obtain a1 a2 :: 'a where as: "a1 \<noteq> a2"
[PROOF STATE]
proof (prove)
using this:
2 \<le> CARD('a)

goal (1 subgoal):
 1. (\<And>a1 a2. a1 \<noteq> a2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using card2_eI
[PROOF STATE]
proof (prove)
using this:
2 \<le> CARD('a)
2 \<le> card ?S \<Longrightarrow> \<exists>x y. x \<noteq> y \<and> x \<in> ?S \<and> y \<in> ?S

goal (1 subgoal):
 1. (\<And>a1 a2. a1 \<noteq> a2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a1 \<noteq> a2

goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
let ?fe1 = "OFEntry 0 ff a1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
let ?fe2 = "OFEntry 0 ff a2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
let ?ft = "[?fe1, ?fe2]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
have "guha_table_semantics \<gamma> ?ft p (Some a1)" "guha_table_semantics \<gamma> ?ft p (Some a2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a1) &&& guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a2)
[PROOF STEP]
by(rule guha_table_semantics.intros(1)[of \<gamma> ?fe1 p "[]" "[?fe2]", unfolded append_Nil flow_entry_match.sel] |
	   rule guha_table_semantics.intros(1)[of \<gamma> ?fe2 p "[?fe1]" "[]", unfolded append_Nil2 flow_entry_match.sel append.simps] |
	   simp add: m)+
[PROOF STATE]
proof (state)
this:
guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a1)
guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a2)

goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a1)
guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a2)

goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a1)
guha_table_semantics \<gamma> [OFEntry 0 ff a1, OFEntry 0 ff a2] p (Some a2)
a1 \<noteq> a2

goal (1 subgoal):
 1. \<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)
[PROOF STEP]
by(intro exI conjI)
[PROOF STATE]
proof (state)
this:
\<exists>ft a1 a2. a1 \<noteq> a2 \<and> guha_table_semantics \<gamma> ft p (Some a1) \<and> guha_table_semantics \<gamma> ft p (Some a2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma guha_umstaendlich: (* or maybe it's Coq where the original formulation is more beneficial *)
	assumes ae: "a = ofe_action fe"
	assumes ele: "fe \<in> set ft"
	assumes rest: "\<gamma> (ofe_fields fe) p"
	              "\<forall>fe' \<in> set ft. ofe_prio fe' > ofe_prio fe \<longrightarrow> \<not>\<gamma> (ofe_fields fe') p"
 	shows "guha_table_semantics \<gamma> ft p (Some a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
from ele
[PROOF STATE]
proof (chain)
picking this:
fe \<in> set ft
[PROOF STEP]
obtain ft1 ft2 where ftspl: "ft = ft1 @ fe # ft2"
[PROOF STATE]
proof (prove)
using this:
fe \<in> set ft

goal (1 subgoal):
 1. (\<And>ft1 ft2. ft = ft1 @ fe # ft2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list
[PROOF STATE]
proof (prove)
using this:
fe \<in> set ft
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs

goal (1 subgoal):
 1. (\<And>ft1 ft2. ft = ft1 @ fe # ft2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ft = ft1 @ fe # ft2

goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
unfolding ae ftspl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> (ft1 @ fe # ft2) p (Some (ofe_action fe))
[PROOF STEP]
apply(rule guha_table_semantics.intros(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<gamma> (ofe_fields fe) p = True
 2. \<forall>fe'\<in>set (ft1 @ ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<gamma> (ofe_fields fe') p = False
[PROOF STEP]
using rest(1)
[PROOF STATE]
proof (prove)
using this:
\<gamma> (ofe_fields fe) p

goal (2 subgoals):
 1. \<gamma> (ofe_fields fe) p = True
 2. \<forall>fe'\<in>set (ft1 @ ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<gamma> (ofe_fields fe') p = False
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>fe'\<in>set (ft1 @ ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<gamma> (ofe_fields fe') p = False
[PROOF STEP]
using rest(2)[unfolded ftspl]
[PROOF STATE]
proof (prove)
using this:
\<forall>fe'\<in>set (ft1 @ fe # ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p

goal (1 subgoal):
 1. \<forall>fe'\<in>set (ft1 @ ft2). ofe_prio fe < ofe_prio fe' \<longrightarrow> \<gamma> (ofe_fields fe') p = False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
guha_table_semantics \<gamma> ft p (Some a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma guha_matched_rule_inversion:
	assumes "guha_table_semantics \<gamma> ft p (Some a)"
	shows "\<exists>fe \<in> set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe' \<in> set ft. ofe_prio fe' > ofe_prio fe \<longrightarrow> \<not>\<gamma> (ofe_fields fe') p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
assume "guha_table_semantics \<gamma> ft p d"
[PROOF STATE]
proof (state)
this:
guha_table_semantics \<gamma> ft p d

goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
hence "Some a = d \<Longrightarrow> (\<exists>fe \<in> set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe' \<in> set ft. ofe_prio fe' > ofe_prio fe \<longrightarrow> \<not>\<gamma> (ofe_fields fe') p))"
[PROOF STATE]
proof (prove)
using this:
guha_table_semantics \<gamma> ft p d

goal (1 subgoal):
 1. Some a = d \<Longrightarrow> \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
by(induction rule: guha_table_semantics.induct) simp_all
[PROOF STATE]
proof (state)
this:
Some a = d \<Longrightarrow> \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
(* strange to show this by induction, but I don't see an exhaust or cases I could use. *)
[PROOF STATE]
proof (state)
this:
Some a = d \<Longrightarrow> \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>guha_table_semantics \<gamma> ft p ?d2; Some a = ?d2\<rbrakk> \<Longrightarrow> \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
from this[OF assms refl]
[PROOF STATE]
proof (chain)
picking this:
\<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal (1 subgoal):
 1. \<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>fe\<in>set ft. a = ofe_action fe \<and> \<gamma> (ofe_fields fe) p \<and> (\<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma guha_equal_Action:
	assumes no: "no_overlaps \<gamma> ft"
	assumes spm: "OF_priority_match \<gamma> ft p = Action a"
	shows "guha_table_semantics \<gamma> ft p (Some a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
note spm[THEN OF_spm3_get_fe]
[PROOF STATE]
proof (state)
this:
\<exists>fe. ofe_action fe = a \<and> fe \<in> set ft \<and> OF_priority_match_ana \<gamma> ft p = Action fe

goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>fe. ofe_action fe = a \<and> fe \<in> set ft \<and> OF_priority_match_ana \<gamma> ft p = Action fe
[PROOF STEP]
obtain fe where a: "ofe_action fe = a" and fein: "fe \<in> set ft" and feana: "OF_priority_match_ana \<gamma> ft p = Action fe"
[PROOF STATE]
proof (prove)
using this:
\<exists>fe. ofe_action fe = a \<and> fe \<in> set ft \<and> OF_priority_match_ana \<gamma> ft p = Action fe

goal (1 subgoal):
 1. (\<And>fe. \<lbrakk>ofe_action fe = a; fe \<in> set ft; OF_priority_match_ana \<gamma> ft p = Action fe\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ofe_action fe = a
fe \<in> set ft
OF_priority_match_ana \<gamma> ft p = Action fe

goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some a)
[PROOF STEP]
apply(rule guha_umstaendlich)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a = ofe_action ?fe
 2. ?fe \<in> set ft
 3. \<gamma> (ofe_fields ?fe) p
 4. \<forall>fe'\<in>set ft. ofe_prio ?fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
[PROOF STEP]
apply(rule a[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. fe \<in> set ft
 2. \<gamma> (ofe_fields fe) p
 3. \<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
[PROOF STEP]
apply(rule fein)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<gamma> (ofe_fields fe) p
 2. \<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
[PROOF STEP]
using feana
[PROOF STATE]
proof (prove)
using this:
OF_priority_match_ana \<gamma> ft p = Action fe

goal (2 subgoals):
 1. \<gamma> (ofe_fields fe) p
 2. \<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
[PROOF STEP]
unfolding OF_priority_match_ana_def
[PROOF STATE]
proof (prove)
using this:
(let m = filter (\<lambda>f. \<gamma> (ofe_fields f) p) ft; m' = filter (\<lambda>f. \<forall>fo\<in>set m. ofe_prio fo \<le> ofe_prio f) m in case m' of [] \<Rightarrow> NoAction | [s] \<Rightarrow> Action s | s # aa # lista \<Rightarrow> Undefined) = Action fe

goal (2 subgoals):
 1. \<gamma> (ofe_fields fe) p
 2. \<forall>fe'\<in>set ft. ofe_prio fe < ofe_prio fe' \<longrightarrow> \<not> \<gamma> (ofe_fields fe') p
[PROOF STEP]
apply(auto dest!: filter_singleton split: list.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
guha_table_semantics \<gamma> ft p (Some a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma guha_equal_NoAction:
	assumes no: "no_overlaps \<gamma> ft"
	assumes spm: "OF_priority_match \<gamma> ft p = NoAction"
	shows "guha_table_semantics \<gamma> ft p None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p None
[PROOF STEP]
using spm
[PROOF STATE]
proof (prove)
using this:
OF_priority_match \<gamma> ft p = NoAction

goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p None
[PROOF STEP]
unfolding OF_priority_match_def
[PROOF STATE]
proof (prove)
using this:
(let m = filter (\<lambda>f. \<gamma> (ofe_fields f) p) ft; m' = filter (\<lambda>f. \<forall>fo\<in>set m. ofe_prio fo \<le> ofe_prio f) m in case m' of [] \<Rightarrow> NoAction | [s] \<Rightarrow> Action (ofe_action s) | s # aa # lista \<Rightarrow> Undefined) = NoAction

goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p None
[PROOF STEP]
by(auto simp add: filter_empty_conv OF_spm3_noa_none[OF no spm] intro: guha_table_semantics.intros(2) split: list.splits)


[STATEMENT]
lemma guha_equal_hlp:
	assumes no: "no_overlaps \<gamma> ft"
	shows "guha_table_semantics \<gamma> ft p (ftb_to_option (OF_priority_match \<gamma> ft p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (ftb_to_option (OF_priority_match \<gamma> ft p))
[PROOF STEP]
unfolding ftb_to_option_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
[PROOF STEP]
apply(cases "(OF_priority_match \<gamma> ft p)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1. OF_priority_match \<gamma> ft p = Action x1 \<Longrightarrow> guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
 2. OF_priority_match \<gamma> ft p = NoAction \<Longrightarrow> guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
 3. OF_priority_match \<gamma> ft p = Undefined \<Longrightarrow> guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
[PROOF STEP]
apply(simp add: guha_equal_Action[OF no])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. OF_priority_match \<gamma> ft p = NoAction \<Longrightarrow> guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
 2. OF_priority_match \<gamma> ft p = Undefined \<Longrightarrow> guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
[PROOF STEP]
apply(simp add: guha_equal_NoAction[OF no])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OF_priority_match \<gamma> ft p = Undefined \<Longrightarrow> guha_table_semantics \<gamma> ft p (case OF_priority_match \<gamma> ft p of Action a \<Rightarrow> Some a | NoAction \<Rightarrow> None)
[PROOF STEP]
apply(subgoal_tac False, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OF_priority_match \<gamma> ft p = Undefined \<Longrightarrow> False
[PROOF STEP]
apply(simp add: no no_overlaps_not_unefined)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma guha_deterministic1: "guha_table_semantics \<gamma> ft p (Some x1) \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. guha_table_semantics \<gamma> ft p (Some x1) \<Longrightarrow> \<not> guha_table_semantics \<gamma> ft p None
[PROOF STEP]
by(auto simp add: guha_table_semantics.simps)