[STATEMENT]
lemma R_G_trace_space_distr_eq:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg"
  shows "MDP.MC.T cfg = distr (MDP.MC.T (repcs s cfg)) MDP.MC.S (smap absc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP.MC.T cfg = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. MDP.MC.T cfg = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
proof (coinduction arbitrary: cfg s rule: MDP.MC.T_coinduct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> prob_space (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 3. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case prob
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (3 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> prob_space (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 3. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc))
[PROOF STEP]
by (rule MDP.MC.T.prob_space_distr, simp)
[PROOF STATE]
proof (state)
this:
prob_space (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc))

goal (2 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case sets
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (2 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sets (distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))

goal (1 subgoal):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case prems: (cont cfg s)
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
let ?\<mu> = "rept s (action cfg)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
define repc' where "repc' \<equiv> \<lambda> cfg'. repcs (THE s. s \<in> ?\<mu> \<and> abss s = state cfg') cfg'"
[PROOF STATE]
proof (state)
this:
repc' \<equiv> \<lambda>cfg'. repcs (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') cfg'

goal (1 subgoal):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
define M' where "M' \<equiv> \<lambda> cfg. distr (MDP.MC.T (repc' cfg)) MDP.MC.S (smap absc)"
[PROOF STATE]
proof (state)
this:
M' \<equiv> \<lambda>cfg. distr (MDP.MC.T (repc' cfg)) (stream_space (count_space UNIV)) (smap absc)

goal (1 subgoal):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
proof (intro exI[where x = M'], safe, goal_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg cfg) \<Longrightarrow> \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
 2. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 3. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 4. \<And>y. prob_space (M' y)
 5. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case A: (1 cfg')
[PROOF STATE]
proof (state)
this:
cfg' \<in> set_pmf (K_cfg cfg)

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg cfg) \<Longrightarrow> \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
 2. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 3. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 4. \<And>y. prob_space (M' y)
 5. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
with K_cfg_rept_action[OF prems]
[PROOF STATE]
proof (chain)
picking this:
?cfg' \<in> set_pmf (K_cfg cfg) \<Longrightarrow> abss (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state ?cfg') = state ?cfg'
cfg' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
have
      "abss (THE s. s \<in> ?\<mu> \<and> abss s = state cfg') = state cfg'"
[PROOF STATE]
proof (prove)
using this:
?cfg' \<in> set_pmf (K_cfg cfg) \<Longrightarrow> abss (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state ?cfg') = state ?cfg'
cfg' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg cfg) \<Longrightarrow> \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
 2. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 3. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 4. \<And>y. prob_space (M' y)
 5. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg cfg) \<Longrightarrow> \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
 2. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 3. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 4. \<And>y. prob_space (M' y)
 5. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
from A prems
[PROOF STATE]
proof (chain)
picking this:
cfg' \<in> set_pmf (K_cfg cfg)
cfg \<in> R_G.valid_cfg
abss s = state cfg
[PROOF STEP]
have "cfg' \<in> R_G.valid_cfg"
[PROOF STATE]
proof (prove)
using this:
cfg' \<in> set_pmf (K_cfg cfg)
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. cfg' \<in> R_G.valid_cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg' \<in> R_G.valid_cfg

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg cfg) \<Longrightarrow> \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
 2. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 3. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 4. \<And>y. prob_space (M' y)
 5. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'
cfg' \<in> R_G.valid_cfg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'
cfg' \<in> R_G.valid_cfg

goal (1 subgoal):
 1. \<exists>cfg s. cfg' = cfg \<and> M' cfg' = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
[PROOF STEP]
unfolding M'_def repc'_def
[PROOF STATE]
proof (prove)
using this:
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'
cfg' \<in> R_G.valid_cfg

goal (1 subgoal):
 1. \<exists>cfg s. cfg' = cfg \<and> distr (MDP.MC.T (repcs (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') cfg')) (stream_space (count_space UNIV)) (smap absc) = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
[PROOF STEP]
by best
[PROOF STATE]
proof (state)
this:
\<exists>cfg s. cfg' = cfg \<and> M' cfg' = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg

goal (4 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. \<And>y. prob_space (M' y)
 4. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. \<And>y. prob_space (M' y)
 4. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. \<And>y. prob_space (M' y)
 4. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (M' y_)
[PROOF STEP]
unfolding M'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (distr (MDP.MC.T (repc' y_)) (stream_space (count_space UNIV)) (smap absc))
[PROOF STEP]
by (rule MDP.MC.T.prob_space_distr, simp)
[PROOF STATE]
proof (state)
this:
prob_space (M' y_)

goal (3 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case 5
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
have *: "smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc"
    if "cfg' \<in> set_pmf (K_cfg cfg)" for cfg'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc
[PROOF STEP]
from K_cfg_rept_action[OF prems that]
[PROOF STATE]
proof (chain)
picking this:
abss (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') = state cfg'
[PROOF STEP]
have
        "abss (THE s. s \<in> ?\<mu> \<and> abss s = state cfg') = state cfg'"
[PROOF STATE]
proof (prove)
using this:
abss (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') = state cfg'

goal (1 subgoal):
 1. abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'

goal (1 subgoal):
 1. smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc
[PROOF STEP]
with prems that
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'
[PROOF STEP]
have *:
        "absc (repc' cfg') = cfg'"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'

goal (1 subgoal):
 1. absc (repc' cfg') = cfg'
[PROOF STEP]
unfolding repc'_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)
abss (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') = state cfg'

goal (1 subgoal):
 1. absc (repcs (THE s. s \<in> set_pmf (rept s (action cfg)) \<and> abss s = state cfg') cfg') = cfg'
[PROOF STEP]
by (subst absc_repcs_id, auto)
[PROOF STATE]
proof (state)
this:
absc (repc' cfg') = cfg'

goal (1 subgoal):
 1. smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
absc (repc' cfg') = cfg'
[PROOF STEP]
show "(smap absc \<circ> (##) (repc' cfg')) = ((##) cfg' \<circ> smap absc)"
[PROOF STATE]
proof (prove)
using this:
absc (repc' cfg') = cfg'

goal (1 subgoal):
 1. smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
smap absc \<circ> (##) (repc' cfg') = (##) cfg' \<circ> smap absc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?cfg'5 \<in> set_pmf (K_cfg cfg) \<Longrightarrow> smap absc \<circ> (##) (repc' ?cfg'5) = (##) ?cfg'5 \<circ> smap absc

goal (3 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
 3. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
unfolding M'_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) (smap absc)) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
apply (subst distr_distr)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. \<And>y. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> MDP.MC.T.random_variable (repc' y) (stream_space (count_space UNIV)) (smap absc)
 3. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (subst MDP.MC.T_eq_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> distr (measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (subst distr_bind)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf.random_variable (K_cfg (repcs s cfg)) (subprob_algebra ?K2) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> space (measure_pmf (K_cfg (repcs s cfg))) \<noteq> {}
 3. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> smap absc \<in> ?K2 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 4. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (distr (MDP.MC.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap absc)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> space (measure_pmf (K_cfg (repcs s cfg))) \<noteq> {}
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf.random_variable (K_cfg (repcs s cfg)) (subprob_algebra ?K2) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 3. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> smap absc \<in> ?K2 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 4. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (distr (MDP.MC.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap absc)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf.random_variable (K_cfg (repcs s cfg)) (subprob_algebra ?K2) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> smap absc \<in> ?K2 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 3. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (distr (MDP.MC.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap absc)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (rule MDP.MC.distr_Stream_subprob)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (distr (MDP.MC.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap absc)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (distr (MDP.MC.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap absc)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (subst distr_distr)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. \<And>x. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 3. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg (repcs s cfg)) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (subst K_cfg_map_repcs[OF prems])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (map_pmf (\<lambda>cfg'. repcs (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') cfg') (K_cfg cfg)) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (subst map_pmf_rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> distr (measure_pmf (K_cfg cfg)) (count_space UNIV) (\<lambda>cfg'. repcs (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') cfg') \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
apply (subst bind_distr)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf.random_variable (K_cfg cfg) (count_space UNIV) (\<lambda>cfg'. repcs (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') cfg')
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra ?K4
 3. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> space (measure_pmf (K_cfg cfg)) \<noteq> {}
 4. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> measure_pmf (K_cfg cfg) \<bind> (\<lambda>x. distr (MDP.MC.T (repcs (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state x) x)) (stream_space (count_space UNIV)) (smap absc \<circ> (##) (repcs (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state x) x))) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (MDP.MC.T (repc' y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
by (fastforce simp: *[unfolded repc'_def] repc'_def space_subprob_algebra MC_syntax.in_S
                  intro: bind_measure_pmf_cong MDP.MC.T.subprob_space_distr)+
[PROOF STATE]
proof (state)
this:
distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))

goal (2 subgoals):
 1. \<And>y x. x \<in> sets (M' y) \<Longrightarrow> x \<in> sets (stream_space (count_space UNIV))
 2. \<And>y x. x \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> x \<in> sets (M' y)
[PROOF STEP]
qed (simp add: M'_def)+
[PROOF STATE]
proof (state)
this:
\<exists>M'. (\<forall>y\<in>set_pmf (K_cfg cfg). \<exists>cfg s. y = cfg \<and> M' y = distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T (repcs s cfg)) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg cfg) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma repc_inj_on_K_cfg:
  assumes "cfg \<in> R_G.cfg_on s" "s \<in> \<S>"
  shows "inj_on repc (set_pmf (K_cfg cfg))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on repc (set_pmf (K_cfg cfg))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.cfg_on s
s \<in> \<S>

goal (1 subgoal):
 1. inj_on repc (set_pmf (K_cfg cfg))
[PROOF STEP]
by (intro inj_on_inverseI[where g = absc], subst absc_repc_id)
     (auto intro: R_G.valid_cfgD R_G.valid_cfgI R_G.valid_cfg_state_in_S)


[STATEMENT]
lemma smap_absc_iff:
  assumes "\<And> x y. x \<in> X \<Longrightarrow> smap abss x = smap abss y \<Longrightarrow> y \<in> X"
  shows "(smap state xs \<in> X) = (smap (\<lambda>z. abss (state z)) xs \<in> smap abss ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (smap state xs \<in> X) = (smap (\<lambda>z. abss (state z)) xs \<in> smap abss ` X)
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. smap state xs \<in> X \<Longrightarrow> smap (\<lambda>z. abss (state z)) xs \<in> smap abss ` X
 2. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
smap state xs \<in> X

goal (2 subgoals):
 1. smap state xs \<in> X \<Longrightarrow> smap (\<lambda>z. abss (state z)) xs \<in> smap abss ` X
 2. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
smap state xs \<in> X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
smap state xs \<in> X

goal (1 subgoal):
 1. smap (\<lambda>z. abss (state z)) xs \<in> smap abss ` X
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
using this:
smap state xs \<in> X

goal (1 subgoal):
 1. smap (\<lambda>z. abss (state z)) xs \<in> {y. \<exists>x\<in>X. y = smap abss x}
[PROOF STEP]
by clarify (inst_existentials "smap state xs", auto simp: stream.map_comp)
[PROOF STATE]
proof (state)
this:
smap (\<lambda>z. abss (state z)) xs \<in> smap abss ` X

goal (1 subgoal):
 1. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
case prems: (2 xs')
[PROOF STATE]
proof (state)
this:
smap (\<lambda>z. abss (state z)) xs = smap abss xs'
xs' \<in> X

goal (1 subgoal):
 1. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
have
    "smap (\<lambda>z. abss (state z)) xs = smap abss (smap state xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap (\<lambda>z. abss (state z)) xs = smap abss (smap state xs)
[PROOF STEP]
by (auto simp: comp_def stream.map_comp)
[PROOF STATE]
proof (state)
this:
smap (\<lambda>z. abss (state z)) xs = smap abss (smap state xs)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
smap (\<lambda>z. abss (state z)) xs = smap abss xs'
xs' \<in> X
smap (\<lambda>z. abss (state z)) xs = smap abss (smap state xs)
[PROOF STEP]
have "smap abss (smap state xs) = smap abss xs'"
[PROOF STATE]
proof (prove)
using this:
smap (\<lambda>z. abss (state z)) xs = smap abss xs'
xs' \<in> X
smap (\<lambda>z. abss (state z)) xs = smap abss (smap state xs)

goal (1 subgoal):
 1. smap abss (smap state xs) = smap abss xs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
smap abss (smap state xs) = smap abss xs'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>smap (\<lambda>z. abss (state z)) xs = smap abss x; x \<in> X\<rbrakk> \<Longrightarrow> smap state xs \<in> X
[PROOF STEP]
with prems(2) assms
[PROOF STATE]
proof (chain)
picking this:
xs' \<in> X
\<lbrakk>?x5 \<in> X; smap abss ?x5 = smap abss ?y5\<rbrakk> \<Longrightarrow> ?y5 \<in> X
smap abss (smap state xs) = smap abss xs'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xs' \<in> X
\<lbrakk>?x5 \<in> X; smap abss ?x5 = smap abss ?y5\<rbrakk> \<Longrightarrow> ?y5 \<in> X
smap abss (smap state xs) = smap abss xs'

goal (1 subgoal):
 1. smap state xs \<in> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
smap state xs \<in> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_abss_reps[simp]:
  assumes "cfg \<in> R_G.valid_cfg"
  shows "abss (reps (state cfg)) = state cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss (reps (state cfg)) = state cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. abss (reps (state cfg)) = state cfg
[PROOF STEP]
by (subst \<S>_abss_reps) (auto intro: R_G.valid_cfg_state_in_S)


[STATEMENT]
lemma in_space_UNIV: "x \<in> space (count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> space (count_space UNIV)
[PROOF STEP]
by simp


[STATEMENT]
lemma S_reps_\<S>_aux:
  "reps (l, R) \<in> S \<Longrightarrow> (l, R) \<in> \<S>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reps (l, R) \<in> S \<Longrightarrow> (l, R) \<in> \<S>
[PROOF STEP]
using ccompatible_inv
[PROOF STATE]
proof (prove)
using this:
ccompatible \<R> (PTA.inv_of A ?l)

goal (1 subgoal):
 1. reps (l, R) \<in> S \<Longrightarrow> (l, R) \<in> \<S>
[PROOF STEP]
unfolding reps_def ccompatible_def \<S>_def S_def
[PROOF STATE]
proof (prove)
using this:
\<forall>R\<in>\<R>. R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l} \<or> {v. v \<turnstile> PTA.inv_of A ?l} \<inter> R = {}

goal (1 subgoal):
 1. (case (l, R) of (l, R) \<Rightarrow> if R \<in> \<R> then (l, SOME u. u \<in> R) else (l, \<lambda>_. - 1)) \<in> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l} \<Longrightarrow> (l, R) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by (cases "R \<in> \<R>"; auto simp: non_empty)


[STATEMENT]
lemma S_reps_\<S>[intro]:
  "reps s \<in> S \<Longrightarrow> s \<in> \<S>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reps s \<in> S \<Longrightarrow> s \<in> \<S>
[PROOF STEP]
using S_reps_\<S>_aux
[PROOF STATE]
proof (prove)
using this:
reps (?l, ?R) \<in> S \<Longrightarrow> (?l, ?R) \<in> \<S>

goal (1 subgoal):
 1. reps s \<in> S \<Longrightarrow> s \<in> \<S>
[PROOF STEP]
by (metis surj_pair)


[STATEMENT]
lemma absc_valid_cfg_eq:
  "absc ` valid_cfg = R_G.valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc ` MDP.valid_cfg = R_G.valid_cfg
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> MDP.valid_cfg \<Longrightarrow> absc xa \<in> R_G.valid_cfg
 2. \<And>x. x \<in> R_G.valid_cfg \<Longrightarrow> x \<in> absc ` MDP.valid_cfg
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> MDP.valid_cfg \<Longrightarrow> absc xa_ \<in> R_G.valid_cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> R_G.valid_cfg \<Longrightarrow> x \<in> absc ` MDP.valid_cfg
[PROOF STEP]
subgoal for cfg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> R_G.valid_cfg \<Longrightarrow> cfg \<in> absc ` MDP.valid_cfg
[PROOF STEP]
using absc_repcs_id[where s = "reps (state cfg)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?cfg \<in> R_G.valid_cfg; abss (reps (state cfg)) = state ?cfg\<rbrakk> \<Longrightarrow> absc (repcs (reps (state cfg)) ?cfg) = ?cfg

goal (1 subgoal):
 1. cfg \<in> R_G.valid_cfg \<Longrightarrow> cfg \<in> absc ` MDP.valid_cfg
[PROOF STEP]
by - (frule repcs_valid[where s = "reps (state cfg)"]; force intro: imageI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma action_repcs:
  "action (repcs (l, u) cfg) = rept (l, u) (action cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (repcs (l, u) cfg) = rept (l, u) (action cfg)
[PROOF STEP]
by (simp add: repcs_def)


[STATEMENT]
lemma path_measure_eq_absc1_new:
  fixes cfg s
  defines "cfg' \<equiv> absc cfg"
  assumes valid: "cfg \<in> valid_cfg"
  assumes X[measurable]: "X \<in> R_G.St" and Y[measurable]: "Y \<in> MDP.St"
  assumes P: "AE x in (R_G.T cfg'). P x" and Q: "AE x in (MDP.T cfg). Q x"
  assumes P'[measurable]: "Measurable.pred R_G.St P"
      and Q'[measurable]: "Measurable.pred MDP.St Q"
  assumes X_Y_closed: "\<And> x y. P x \<Longrightarrow> smap abss y = x \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<and> Q y"
  assumes Y_X_closed: "\<And> x y. Q y \<Longrightarrow> smap abss y = x \<Longrightarrow> y \<in> Y \<Longrightarrow> x \<in> X \<and> P x"
  shows
    "emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
have *: "stream_all2 (\<lambda>s. (=) (absc s)) x y = stream_all2 (=) (smap absc x) y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>s. (=) (absc s)) x y = stream_all2 (=) (smap absc x) y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>s. (=) (absc s)) ?x5 ?y5 = stream_all2 (=) (smap absc ?x5) ?y5

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
have *: "stream_all2 (\<lambda>s t. t = absc s) x y = stream_all2 (=) y (smap absc x)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y = stream_all2 (=) y (smap absc x)
[PROOF STEP]
using stream.rel_conversep[of "\<lambda>s t. t = absc s"]
[PROOF STATE]
proof (prove)
using this:
stream_all2 (\<lambda>s t. t = absc s)\<inverse>\<inverse> = (stream_all2 (\<lambda>s t. t = absc s))\<inverse>\<inverse>

goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y = stream_all2 (=) y (smap absc x)
[PROOF STEP]
by (simp add: conversep_iff[abs_def])
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>s t. t = absc s) ?x5 ?y5 = stream_all2 (=) ?y5 (smap absc ?x5)

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (R_G.T cfg') P
[PROOF STEP]
have "emeasure (R_G.T cfg') X = emeasure (R_G.T cfg') {x \<in> X. P x}"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (R_G.T cfg') P

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (R_G.T cfg') {x \<in> X. P x}
[PROOF STEP]
by (auto intro: emeasure_eq_AE)
[PROOF STATE]
proof (state)
this:
emeasure (R_G.T cfg') X = emeasure (R_G.T cfg') {x \<in> X. P x}

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
emeasure (R_G.T cfg') X = emeasure (R_G.T cfg') {x \<in> X. P x}

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
from Q
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (MDP.T cfg) Q
[PROOF STEP]
have "emeasure (MDP.T cfg) Y = emeasure (MDP.T cfg) {y \<in> Y. Q y}"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (MDP.T cfg) Q

goal (1 subgoal):
 1. emeasure (MDP.T cfg) Y = emeasure (MDP.T cfg) {y \<in> Y. Q y}
[PROOF STEP]
by (auto intro: emeasure_eq_AE)
[PROOF STATE]
proof (state)
this:
emeasure (MDP.T cfg) Y = emeasure (MDP.T cfg) {y \<in> Y. Q y}

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
emeasure (MDP.T cfg) Y = emeasure (MDP.T cfg) {y \<in> Y. Q y}

goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y
[PROOF STEP]
apply (simp only: calculation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg') {x \<in> X. P x} = emeasure (MDP.T cfg) {y \<in> Y. Q y}
[PROOF STEP]
unfolding R_G.T_def MDP.T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (MDP.MC.T cfg') R_G.St (smap state)) {x \<in> X. P x} = emeasure (distr (MDP.MC.T cfg) MDP.St (smap state)) {y \<in> Y. Q y}
[PROOF STEP]
apply (simp add: emeasure_distr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (MDP.MC.T cfg') ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV))) = emeasure (MDP.MC.T cfg) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV)))
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (MDP.MC.T cfg) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) = emeasure (MDP.MC.T cfg') ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
[PROOF STEP]
apply (rule T_eq_rel_half[where f = absc and S = valid_cfg])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s t. ?R5 s t = (s \<in> MDP.valid_cfg \<and> absc s = t)
 2. {y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 3. {y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 4. PTA.rel_set_strong (stream_all2 ?R5) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
 5. rel_fun ?R5 (rel_pmf ?R5) K_cfg K_cfg
 6. ?R5 cfg cfg'
[PROOF STEP]
apply (rule HOL.refl)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 2. {y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 3. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
 4. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 5. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
 2. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 3. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
apply (simp add: space_stream_space)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) {y. smap state y \<in> Y \<and> Q (smap state y)} {y. smap state y \<in> X \<and> P (smap state y)}
 2. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 3. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) {y. smap state y \<in> Y \<and> Q (smap state y)} {y. smap state y \<in> X \<and> P (smap state y)}
[PROOF STEP]
unfolding rel_set_strong_def stream.rel_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) x y \<longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
apply (drule stream.rel_mono_strong[where Ra = "\<lambda>s t. t = absc s"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z yb. \<lbrakk>z \<in> sset x; yb \<in> sset y; z \<in> MDP.valid_cfg \<and> absc z = yb\<rbrakk> \<Longrightarrow> yb = absc z
 2. \<And>x y. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
apply (simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
using Y_X_closed[of "smap state x" "smap state (smap absc x)" for x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q (smap state ?xa7); smap abss (smap state ?xa7) = smap state (smap absc ?xa7); smap state ?xa7 \<in> Y\<rbrakk> \<Longrightarrow> smap state (smap absc ?xa7) \<in> X \<and> P (smap state (smap absc ?xa7))

goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
using X_Y_closed[of "smap state (smap absc x)" "smap state x" for x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q (smap state ?xa7); smap abss (smap state ?xa7) = smap state (smap absc ?xa7); smap state ?xa7 \<in> Y\<rbrakk> \<Longrightarrow> smap state (smap absc ?xa7) \<in> X \<and> P (smap state (smap absc ?xa7))
\<lbrakk>P (smap state (smap absc ?xa7)); smap abss (smap state ?xa7) = smap state (smap absc ?xa7); smap state (smap absc ?xa7) \<in> X\<rbrakk> \<Longrightarrow> smap state ?xa7 \<in> Y \<and> Q (smap state ?xa7)

goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
by (auto simp: * stream.rel_eq stream.map_comp state_absc)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 2. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
[PROOF STEP]
apply (auto intro!: rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (K_cfg x) (K_cfg (absc x))
[PROOF STEP]
apply (subst K_cfg_map_absc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (K_cfg x) (map_pmf absc (K_cfg x))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (K_cfg x) (map_pmf absc (K_cfg x))
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
[PROOF STEP]
apply (subst pmf.rel_map(2))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>x y. x \<in> MDP.valid_cfg \<and> absc x = absc y) (K_cfg x) (K_cfg x)
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
[PROOF STEP]
apply (rule rel_pmf_reflI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> MDP.valid_cfg; xa \<in> set_pmf (K_cfg x)\<rbrakk> \<Longrightarrow> xa \<in> MDP.valid_cfg \<and> absc xa = absc xa
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg \<and> absc cfg = cfg'
[PROOF STEP]
unfolding cfg'_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg \<and> absc cfg = absc cfg
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
emeasure (R_G.T cfg') X = emeasure (MDP.T cfg) Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_measure_eq_repcs1_new:
  fixes cfg s
  defines "cfg' \<equiv> repcs s cfg"
  assumes s: "abss s = state cfg"
  assumes valid: "cfg \<in> R_G.valid_cfg"
  assumes X[measurable]: "X \<in> R_G.St" and Y[measurable]: "Y \<in> MDP.St"
  assumes P: "AE x in (R_G.T cfg). P x" and Q: "AE x in (MDP.T cfg'). Q x"
  assumes P'[measurable]: "Measurable.pred R_G.St P"
      and Q'[measurable]: "Measurable.pred MDP.St Q"
  assumes X_Y_closed: "\<And> x y. P x \<Longrightarrow> smap abss y = x \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<and> Q y"
  assumes Y_X_closed: "\<And> x y. Q y \<Longrightarrow> smap abss y = x \<Longrightarrow> y \<in> Y \<Longrightarrow> x \<in> X \<and> P x"
  shows
    "emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
have *: "stream_all2 (\<lambda>s t. t = absc s) x y = stream_all2 (=) y (smap absc x)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y = stream_all2 (=) y (smap absc x)
[PROOF STEP]
using stream.rel_conversep[of "\<lambda>s t. t = absc s"]
[PROOF STATE]
proof (prove)
using this:
stream_all2 (\<lambda>s t. t = absc s)\<inverse>\<inverse> = (stream_all2 (\<lambda>s t. t = absc s))\<inverse>\<inverse>

goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y = stream_all2 (=) y (smap absc x)
[PROOF STEP]
by (simp add: conversep_iff[abs_def])
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>s t. t = absc s) ?x5 ?y5 = stream_all2 (=) ?y5 (smap absc ?x5)

goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
from P X
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (R_G.T cfg) P
X \<in> sets R_G.St
[PROOF STEP]
have
    "emeasure (R_G.T cfg) X = emeasure (R_G.T cfg) {x \<in> X. P x}"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (R_G.T cfg) P
X \<in> sets R_G.St

goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (R_G.T cfg) {x \<in> X. P x}
[PROOF STEP]
by (auto intro: emeasure_eq_AE)
[PROOF STATE]
proof (state)
this:
emeasure (R_G.T cfg) X = emeasure (R_G.T cfg) {x \<in> X. P x}

goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
emeasure (R_G.T cfg) X = emeasure (R_G.T cfg) {x \<in> X. P x}

goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
from Q Y
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (MDP.T cfg') Q
Y \<in> sets MDP.St
[PROOF STEP]
have
    "emeasure (MDP.T cfg') Y = emeasure (MDP.T cfg') {y \<in> Y. Q y}"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (MDP.T cfg') Q
Y \<in> sets MDP.St

goal (1 subgoal):
 1. emeasure (MDP.T cfg') Y = emeasure (MDP.T cfg') {y \<in> Y. Q y}
[PROOF STEP]
by (auto intro: emeasure_eq_AE)
[PROOF STATE]
proof (state)
this:
emeasure (MDP.T cfg') Y = emeasure (MDP.T cfg') {y \<in> Y. Q y}

goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
emeasure (MDP.T cfg') Y = emeasure (MDP.T cfg') {y \<in> Y. Q y}

goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y
[PROOF STEP]
apply (simp only: calculation)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg) {x \<in> X. P x} = emeasure (MDP.T cfg') {y \<in> Y. Q y}
[PROOF STEP]
unfolding R_G.T_def MDP.T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (MDP.MC.T cfg) R_G.St (smap state)) {x \<in> X. P x} = emeasure (distr (MDP.MC.T cfg') MDP.St (smap state)) {y \<in> Y. Q y}
[PROOF STEP]
apply (simp add: emeasure_distr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (MDP.MC.T cfg) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV))) = emeasure (MDP.MC.T cfg') ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV)))
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (MDP.MC.T cfg') ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) = emeasure (MDP.MC.T cfg) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
[PROOF STEP]
apply (rule T_eq_rel_half[where f = absc and S = valid_cfg])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s t. ?R5 s t = (s \<in> MDP.valid_cfg \<and> absc s = t)
 2. {y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 3. {y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 4. PTA.rel_set_strong (stream_all2 ?R5) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
 5. rel_fun ?R5 (rel_pmf ?R5) K_cfg K_cfg
 6. ?R5 cfg' cfg
[PROOF STEP]
apply (rule HOL.refl)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 2. {y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 3. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
 4. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 5. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) ({y. smap state y \<in> Y \<and> Q (smap state y)} \<inter> space (stream_space (count_space UNIV))) ({y. smap state y \<in> X \<and> P (smap state y)} \<inter> space (stream_space (count_space UNIV)))
 2. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 3. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
apply (simp add: space_stream_space)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) {y. smap state y \<in> Y \<and> Q (smap state y)} {y. smap state y \<in> X \<and> P (smap state y)}
 2. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 3. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PTA.rel_set_strong (stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) {y. smap state y \<in> Y \<and> Q (smap state y)} {y. smap state y \<in> X \<and> P (smap state y)}
[PROOF STEP]
unfolding rel_set_strong_def stream.rel_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) x y \<longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. stream_all2 (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
apply (drule stream.rel_mono_strong[where Ra = "\<lambda>s t. t = absc s"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z yb. \<lbrakk>z \<in> sset x; yb \<in> sset y; z \<in> MDP.valid_cfg \<and> absc z = yb\<rbrakk> \<Longrightarrow> yb = absc z
 2. \<And>x y. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
apply (simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
using Y_X_closed[of "smap state x" "smap state (smap absc x)" for x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q (smap state ?xa7); smap abss (smap state ?xa7) = smap state (smap absc ?xa7); smap state ?xa7 \<in> Y\<rbrakk> \<Longrightarrow> smap state (smap absc ?xa7) \<in> X \<and> P (smap state (smap absc ?xa7))

goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
using X_Y_closed[of "smap state (smap absc x)" "smap state x" for x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q (smap state ?xa7); smap abss (smap state ?xa7) = smap state (smap absc ?xa7); smap state ?xa7 \<in> Y\<rbrakk> \<Longrightarrow> smap state (smap absc ?xa7) \<in> X \<and> P (smap state (smap absc ?xa7))
\<lbrakk>P (smap state (smap absc ?xa7)); smap abss (smap state ?xa7) = smap state (smap absc ?xa7); smap state (smap absc ?xa7) \<in> X\<rbrakk> \<Longrightarrow> smap state ?xa7 \<in> Y \<and> Q (smap state ?xa7)

goal (1 subgoal):
 1. stream_all2 (\<lambda>s t. t = absc s) x y \<Longrightarrow> (x \<in> {y. smap state y \<in> Y \<and> Q (smap state y)}) = (y \<in> {y. smap state y \<in> X \<and> P (smap state y)})
[PROOF STEP]
by (auto simp: * stream.rel_eq stream.map_comp state_absc)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
 2. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t)) K_cfg K_cfg
[PROOF STEP]
apply (auto intro!: rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (K_cfg x) (K_cfg (absc x))
[PROOF STEP]
apply (subst K_cfg_map_absc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (K_cfg x) (map_pmf absc (K_cfg x))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>s t. s \<in> MDP.valid_cfg \<and> absc s = t) (K_cfg x) (map_pmf absc (K_cfg x))
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
[PROOF STEP]
apply (subst pmf.rel_map(2))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> rel_pmf (\<lambda>x y. x \<in> MDP.valid_cfg \<and> absc x = absc y) (K_cfg x) (K_cfg x)
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
[PROOF STEP]
apply (rule rel_pmf_reflI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> MDP.valid_cfg; xa \<in> set_pmf (K_cfg x)\<rbrakk> \<Longrightarrow> xa \<in> MDP.valid_cfg \<and> absc xa = absc xa
 2. \<And>x. x \<in> MDP.valid_cfg \<Longrightarrow> x \<in> MDP.valid_cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. cfg' \<in> MDP.valid_cfg \<and> absc cfg' = cfg
[PROOF STEP]
unfolding cfg'_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. repcs s cfg \<in> MDP.valid_cfg \<and> absc (repcs s cfg) = cfg
[PROOF STEP]
by (auto simp: s absc_repcs_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
emeasure (R_G.T cfg) X = emeasure (MDP.T cfg') Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma region_compatible_suntil1:
  assumes "(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)"
      and "pred_stream (\<lambda> s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x"
      and "pred_stream (\<lambda> s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x"
  shows "(holds \<phi> suntil holds \<psi>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x

goal (1 subgoal):
 1. (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
proof (induction "smap abss x" arbitrary: x rule: suntil.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<psi> (reps x)) (smap abss x); pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
 2. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
holds (\<lambda>x. \<psi> (reps x)) (smap abss x)
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x

goal (2 subgoals):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<psi> (reps x)) (smap abss x); pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
 2. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
holds (\<lambda>x. \<psi> (reps x)) (smap abss x)
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
holds (\<lambda>x. \<psi> (reps x)) (smap abss x)
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x

goal (1 subgoal):
 1. (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
by (auto intro: suntil.base simp: stream.pred_set)
[PROOF STATE]
proof (state)
this:
(holds \<phi> suntil holds \<psi>) x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
holds (\<lambda>x. \<phi> (reps x)) (smap abss x)
(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x))
\<lbrakk>stl (smap abss x) = smap abss ?x5; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) ?x5; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) ?x5\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) ?x5
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
have
    "pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x)"
    "pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x) &&& pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x) &&& pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)
[PROOF STEP]
apply (cases x; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)
[PROOF STEP]
apply (cases x; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x)
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
with step.hyps(3)[of "stl x"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>stl (smap abss x) = smap abss (stl x); pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x); pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) (stl x)
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x)
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)
[PROOF STEP]
have "(holds \<phi> suntil holds \<psi>) (stl x)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stl (smap abss x) = smap abss (stl x); pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x); pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) (stl x)
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) (stl x)
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) (stl x)

goal (1 subgoal):
 1. (holds \<phi> suntil holds \<psi>) (stl x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(holds \<phi> suntil holds \<psi>) (stl x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>holds (\<lambda>x. \<phi> (reps x)) (smap abss x); (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x)); \<And>xa. \<lbrakk>stl (smap abss x) = smap abss xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) xa; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) xa\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) xa; pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x; pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x\<rbrakk> \<Longrightarrow> (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
with step.prems step.hyps(1-2)
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x
holds (\<lambda>x. \<phi> (reps x)) (smap abss x)
(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x))
(holds \<phi> suntil holds \<psi>) (stl x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) \<longrightarrow> \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) \<longrightarrow> \<psi> s) x
holds (\<lambda>x. \<phi> (reps x)) (smap abss x)
(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (stl (smap abss x))
(holds \<phi> suntil holds \<psi>) (stl x)

goal (1 subgoal):
 1. (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
by (auto intro: suntil.step simp: stream.pred_set)
[PROOF STATE]
proof (state)
this:
(holds \<phi> suntil holds \<psi>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma region_compatible_suntil2:
  assumes "(holds \<phi> suntil holds \<psi>) x"
      and "pred_stream (\<lambda> s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x"
      and "pred_stream (\<lambda> s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x"
  shows "(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(holds \<phi> suntil holds \<psi>) x
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x

goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)
[PROOF STEP]
proof (induction x rule: suntil.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>holds \<psi> \<omega>; pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
 2. \<And>\<omega>. \<lbrakk>holds \<phi> \<omega>; (holds \<phi> suntil holds \<psi>) (stl \<omega>); \<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl \<omega>); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl \<omega>)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl \<omega>)); pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
[PROOF STEP]
case (base x)
[PROOF STATE]
proof (state)
this:
holds \<psi> x
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x

goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>holds \<psi> \<omega>; pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
 2. \<And>\<omega>. \<lbrakk>holds \<phi> \<omega>; (holds \<phi> suntil holds \<psi>) (stl \<omega>); \<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl \<omega>); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl \<omega>)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl \<omega>)); pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
holds \<psi> x
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
holds \<psi> x
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x

goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)
[PROOF STEP]
by (auto intro: suntil.base simp: stream.pred_set)
[PROOF STATE]
proof (state)
this:
(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)

goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>holds \<phi> \<omega>; (holds \<phi> suntil holds \<psi>) (stl \<omega>); \<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl \<omega>); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl \<omega>)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl \<omega>)); pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>holds \<phi> \<omega>; (holds \<phi> suntil holds \<psi>) (stl \<omega>); \<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl \<omega>); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl \<omega>)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl \<omega>)); pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
holds \<phi> x
(holds \<phi> suntil holds \<psi>) (stl x)
\<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl x))
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x

goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>holds \<phi> \<omega>; (holds \<phi> suntil holds \<psi>) (stl \<omega>); \<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl \<omega>); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl \<omega>)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl \<omega>)); pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
[PROOF STEP]
have
    "pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x)"
    "pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x) &&& pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x) &&& pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)
[PROOF STEP]
apply (cases x; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)
[PROOF STEP]
apply (cases x; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x)
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)

goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>holds \<phi> \<omega>; (holds \<phi> suntil holds \<psi>) (stl \<omega>); \<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl \<omega>); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl \<omega>)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl \<omega>)); pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) \<omega>; pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) \<omega>\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss \<omega>)
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
holds \<phi> x
(holds \<phi> suntil holds \<psi>) (stl x)
\<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl x))
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x)
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
holds \<phi> x
(holds \<phi> suntil holds \<psi>) (stl x)
\<lbrakk>pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x); pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (stl x))
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) x
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) x
pred_stream (\<lambda>s. \<phi> s \<longrightarrow> \<phi> (reps (abss s))) (stl x)
pred_stream (\<lambda>s. \<psi> s \<longrightarrow> \<psi> (reps (abss s))) (stl x)

goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)
[PROOF STEP]
by (auto intro: suntil.step simp: stream.pred_set)
[PROOF STATE]
proof (state)
this:
(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma region_compatible_suntil:
  assumes "pred_stream (\<lambda> s. \<phi> (reps (abss s)) \<longleftrightarrow> \<phi> s) x"
      and "pred_stream (\<lambda> s. \<psi> (reps (abss s)) \<longleftrightarrow> \<psi> s) x"
  shows "(holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x)
     \<longleftrightarrow> (holds \<phi> suntil holds \<psi>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x) = (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) x

goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x) = (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
using assms region_compatible_suntil1 region_compatible_suntil2
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) x
pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) x
pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) x
\<lbrakk>(holds (\<lambda>x. ?\<phi> (reps x)) suntil holds (\<lambda>x. ?\<psi> (reps x))) (smap abss ?x); pred_stream (\<lambda>s. ?\<phi> (reps (abss s)) \<longrightarrow> ?\<phi> s) ?x; pred_stream (\<lambda>s. ?\<psi> (reps (abss s)) \<longrightarrow> ?\<psi> s) ?x\<rbrakk> \<Longrightarrow> (holds ?\<phi> suntil holds ?\<psi>) ?x
\<lbrakk>(holds ?\<phi> suntil holds ?\<psi>) ?x; pred_stream (\<lambda>s. ?\<phi> s \<longrightarrow> ?\<phi> (reps (abss s))) ?x; pred_stream (\<lambda>s. ?\<psi> s \<longrightarrow> ?\<psi> (reps (abss s))) ?x\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. ?\<phi> (reps x)) suntil holds (\<lambda>x. ?\<psi> (reps x))) (smap abss ?x)

goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x) = (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
unfolding stream.pred_set
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>sset x. \<phi> (reps (abss s)) = \<phi> s
\<forall>s\<in>sset x. \<psi> (reps (abss s)) = \<psi> s
\<forall>s\<in>sset x. \<phi> (reps (abss s)) = \<phi> s
\<forall>s\<in>sset x. \<psi> (reps (abss s)) = \<psi> s
\<lbrakk>(holds (\<lambda>x. ?\<phi> (reps x)) suntil holds (\<lambda>x. ?\<psi> (reps x))) (smap abss ?x); \<forall>s\<in>sset ?x. ?\<phi> (reps (abss s)) \<longrightarrow> ?\<phi> s; \<forall>s\<in>sset ?x. ?\<psi> (reps (abss s)) \<longrightarrow> ?\<psi> s\<rbrakk> \<Longrightarrow> (holds ?\<phi> suntil holds ?\<psi>) ?x
\<lbrakk>(holds ?\<phi> suntil holds ?\<psi>) ?x; \<forall>s\<in>sset ?x. ?\<phi> s \<longrightarrow> ?\<phi> (reps (abss s)); \<forall>s\<in>sset ?x. ?\<psi> s \<longrightarrow> ?\<psi> (reps (abss s))\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. ?\<phi> (reps x)) suntil holds (\<lambda>x. ?\<psi> (reps x))) (smap abss ?x)

goal (1 subgoal):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss x) = (holds \<phi> suntil holds \<psi>) x
[PROOF STEP]
by blast


[STATEMENT]
lemma reps_abss_S:
  assumes "reps (abss s) \<in> S"
  shows "s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
by (simp add: S_reps_\<S> \<S>_abss_S assms)


[STATEMENT]
lemma measurable_sset[measurable (raw)]:
  assumes f[measurable]: "f \<in> N \<rightarrow>\<^sub>M stream_space M" and P[measurable]: "Measurable.pred M P"
  shows "Measurable.pred N (\<lambda>x. \<forall>s\<in>sset (f x). P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Measurable.pred N (\<lambda>x. \<forall>s\<in>sset (f x). P s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Measurable.pred N (\<lambda>x. \<forall>s\<in>sset (f x). P s)
[PROOF STEP]
have *: "(\<lambda>x. \<forall>s\<in>sset (f x). P s) = (\<lambda>x. \<forall>i. P (f x !! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<forall>s\<in>sset (f x). P s) = (\<lambda>x. \<forall>i. P (f x !! i))
[PROOF STEP]
by (simp add: sset_range)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<forall>s\<in>sset (f x). P s) = (\<lambda>x. \<forall>i. P (f x !! i))

goal (1 subgoal):
 1. Measurable.pred N (\<lambda>x. \<forall>s\<in>sset (f x). P s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Measurable.pred N (\<lambda>x. \<forall>s\<in>sset (f x). P s)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Measurable.pred N (\<lambda>x. \<forall>i. P (f x !! i))
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
Measurable.pred N (\<lambda>x. \<forall>s\<in>sset (f x). P s)

goal:
No subgoals!
[PROOF STEP]
qed