[STATEMENT]
lemma absc_repcs_id:
  notes R_G.cfg_onD_state[simp del]
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg"
  shows "absc (repcs s cfg) = cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc (repcs s cfg) = cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. absc (repcs s cfg) = cfg
[PROOF STEP]
proof (subst eq_commute, coinduction arbitrary: cfg s)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> state cfg = state (absc (repcs s cfg))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg = action (absc (repcs s cfg))
 3. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
case state
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
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; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> state cfg = state (absc (repcs s cfg))
 2. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg = action (absc (repcs s cfg))
 3. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
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
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. state cfg = state (absc (repcs s cfg))
[PROOF STEP]
by (simp add: absc_def repc_def repcs_def)
[PROOF STATE]
proof (state)
this:
state cfg = state (absc (repcs s cfg))

goal (2 subgoals):
 1. \<And>cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg = action (absc (repcs s cfg))
 2. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[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; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg = action (absc (repcs s cfg))
 2. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
case prems: (action cfg)
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
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; cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg = action (absc (repcs s cfg))
 2. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
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
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. action cfg = action (absc (repcs s cfg))
[PROOF STEP]
by (auto simp: action_abst_repcs action_absc)
[PROOF STATE]
proof (state)
this:
action cfg = action (absc (repcs s cfg))

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
case prems: (cont s')
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
define cfg' where "cfg' \<equiv> repcs s cfg"
[PROOF STATE]
proof (state)
this:
cfg' \<equiv> repcs s cfg

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
define t    where "t    \<equiv> THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')"
[PROOF STATE]
proof (state)
this:
t \<equiv> THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
[PROOF STEP]
have "cfg \<in> R_G.cfg_on (state cfg)" "state cfg \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. cfg \<in> R_G.cfg_on (state cfg) &&& state cfg \<in> \<S>
[PROOF STEP]
by (auto dest: R_G_I)
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.cfg_on (state cfg)
state cfg \<in> \<S>

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.cfg_on (state cfg)
state cfg \<in> \<S>
[PROOF STEP]
have *: "cfg \<in> R_G.cfg_on (abss (reps (state cfg)))" "abss (reps (state cfg)) \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.cfg_on (state cfg)
state cfg \<in> \<S>

goal (1 subgoal):
 1. cfg \<in> R_G.cfg_on (abss (reps (state cfg))) &&& abss (reps (state cfg)) \<in> \<S>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.cfg_on (abss (reps (state cfg)))
abss (reps (state cfg)) \<in> \<S>

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
[PROOF STEP]
have "s' \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. s' \<in> \<S>
[PROOF STEP]
by (auto intro: R_G.valid_cfg_action)
[PROOF STATE]
proof (state)
this:
s' \<in> \<S>

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
[PROOF STEP]
have valid: "cfg' \<in> valid_cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)

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

goal (1 subgoal):
 1. repcs s cfg \<in> MDP.valid_cfg
[PROOF STEP]
by (intro repcs_valid)
[PROOF STATE]
proof (state)
this:
cfg' \<in> MDP.valid_cfg

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
[PROOF STEP]
have "s' \<in> abst (action cfg')"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)

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

goal (1 subgoal):
 1. s' \<in> set_pmf (abst (action (repcs s cfg)))
[PROOF STEP]
by (subst action_abst_repcs)
[PROOF STATE]
proof (state)
this:
s' \<in> set_pmf (abst (action cfg'))

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
from cont_cfg_defined[OF valid this]
[PROOF STATE]
proof (chain)
picking this:
(abss (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')) = s' \<and> (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')) \<in> set_pmf (action cfg')) \<and> (\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg') \<longrightarrow> y = (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')))
[PROOF STEP]
have t:
    "abss t = s'" "t \<in> action cfg'"
[PROOF STATE]
proof (prove)
using this:
(abss (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')) = s' \<and> (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')) \<in> set_pmf (action cfg')) \<and> (\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg') \<longrightarrow> y = (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg')))

goal (1 subgoal):
 1. abss t = s' &&& t \<in> set_pmf (action cfg')
[PROOF STEP]
unfolding t_def cfg'_def
[PROOF STATE]
proof (prove)
using this:
(abss (THE x. abss x = s' \<and> x \<in> set_pmf (action (repcs s cfg))) = s' \<and> (THE x. abss x = s' \<and> x \<in> set_pmf (action (repcs s cfg))) \<in> set_pmf (action (repcs s cfg))) \<and> (\<forall>y. abss y = s' \<and> y \<in> set_pmf (action (repcs s cfg)) \<longrightarrow> y = (THE x. abss x = s' \<and> x \<in> set_pmf (action (repcs s cfg))))

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

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
abss t = s'
t \<in> set_pmf (action cfg')
[PROOF STEP]
have "t ~ reps (abss t)"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
abss t = s'
t \<in> set_pmf (action cfg')

goal (1 subgoal):
 1. t ~ reps (abss t)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; s' \<in> set_pmf (action cfg); abss t = s'; t \<in> set_pmf (action cfg')\<rbrakk> \<Longrightarrow> t ~ reps (abss t)
[PROOF STEP]
apply (subst \<S>_abss_reps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; s' \<in> set_pmf (action cfg); abss t = s'; t \<in> set_pmf (action cfg')\<rbrakk> \<Longrightarrow> abss t \<in> \<S>
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; s' \<in> set_pmf (action cfg); abss t = s'; t \<in> set_pmf (action cfg')\<rbrakk> \<Longrightarrow> t ~ t
[PROOF STEP]
by (auto intro: R_G.valid_cfg_action)
[PROOF STATE]
proof (state)
this:
t ~ reps (abss t)

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
have "cont (absc cfg') s' = cont (absc cfg') (abss t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc cfg') s' = cont (absc cfg') (abss t)
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
abss t = s'
t \<in> set_pmf (action cfg')

goal (1 subgoal):
 1. cont (absc cfg') s' = cont (absc cfg') (abss t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cont (absc cfg') s' = cont (absc cfg') (abss t)

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
have "cont (absc cfg') s' = absc (cont cfg' t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc cfg') s' = absc (cont cfg' t)
[PROOF STEP]
using t valid
[PROOF STATE]
proof (prove)
using this:
abss t = s'
t \<in> set_pmf (action cfg')
cfg' \<in> MDP.valid_cfg

goal (1 subgoal):
 1. cont (absc cfg') s' = absc (cont cfg' t)
[PROOF STEP]
by (auto simp: cont_absc_1)
[PROOF STATE]
proof (state)
this:
cont (absc cfg') s' = absc (cont cfg' t)

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cont (absc cfg') s' = absc (cont cfg' t)

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
have "\<dots> = absc (repcs t (cont cfg s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc (cont cfg' t) = absc (repcs t (cont cfg s'))
[PROOF STEP]
using prems t * \<open>t ~ _\<close> valid
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
abss t = s'
t \<in> set_pmf (action cfg')
cfg \<in> R_G.cfg_on (abss (reps (state cfg)))
abss (reps (state cfg)) \<in> \<S>
t ~ reps (abss t)
cfg' \<in> MDP.valid_cfg

goal (1 subgoal):
 1. absc (cont cfg' t) = absc (repcs t (cont cfg s'))
[PROOF STEP]
by (fastforce dest: R_G_I intro: repcs_bisim simp: cont_repcs1 cfg'_def)
[PROOF STATE]
proof (state)
this:
absc (cont cfg' t) = absc (repcs t (cont cfg s'))

goal (1 subgoal):
 1. \<And>t cfg s. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg; cfg \<in> R_G.valid_cfg; abss s = state cfg; t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> \<exists>cfga sa. cont cfg t = cfga \<and> cont (absc (repcs s cfg)) t = absc (repcs sa cfga) \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga \<and> cfga \<in> R_G.valid_cfg \<and> abss sa = state cfga
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cont (absc cfg') s' = absc (repcs t (cont cfg s'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cont (absc cfg') s' = absc (repcs t (cont cfg s'))

goal (1 subgoal):
 1. \<exists>cfg s. cont cfg s' = cfg \<and> cont (absc (repcs s cfg)) s' = absc (repcs s cfg) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc cfg') s' = absc (repcs t (cont cfg s')) \<Longrightarrow> \<exists>cfg s. cont cfg s' = cfg \<and> cont (absc (repcs s cfg)) s' = absc (repcs s cfg) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
[PROOF STEP]
apply (rule exI[where x = "cont cfg s'"], rule exI[where x = t])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc cfg') s' = absc (repcs t (cont cfg s')) \<Longrightarrow> cont cfg s' = cont cfg s' \<and> cont (absc (repcs s cfg)) s' = absc (repcs t (cont cfg s')) \<and> cont cfg s' \<in> R_G.valid_cfg \<and> abss t = state (cont cfg s') \<and> cont cfg s' \<in> R_G.valid_cfg \<and> abss t = state (cont cfg s')
[PROOF STEP]
unfolding cfg'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc (repcs s cfg)) s' = absc (repcs t (cont cfg s')) \<Longrightarrow> cont cfg s' = cont cfg s' \<and> cont (absc (repcs s cfg)) s' = absc (repcs t (cont cfg s')) \<and> cont cfg s' \<in> R_G.valid_cfg \<and> abss t = state (cont cfg s') \<and> cont cfg s' \<in> R_G.valid_cfg \<and> abss t = state (cont cfg s')
[PROOF STEP]
using prems t
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action cfg)
abss t = s'
t \<in> set_pmf (action cfg')

goal (1 subgoal):
 1. cont (absc (repcs s cfg)) s' = absc (repcs t (cont cfg s')) \<Longrightarrow> cont cfg s' = cont cfg s' \<and> cont (absc (repcs s cfg)) s' = absc (repcs t (cont cfg s')) \<and> cont cfg s' \<in> R_G.valid_cfg \<and> abss t = state (cont cfg s') \<and> cont cfg s' \<in> R_G.valid_cfg \<and> abss t = state (cont cfg s')
[PROOF STEP]
by (auto intro: R_G.valid_cfg_cont)
[PROOF STATE]
proof (state)
this:
\<exists>cfg s. cont cfg s' = cfg \<and> cont (absc (repcs s cfg)) s' = absc (repcs s cfg) \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absc_repc_id:
  notes R_G.cfg_onD_state[simp del]
  assumes "cfg \<in> R_G.valid_cfg"
  shows "absc (repc cfg) = cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc (repc cfg) = cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_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

goal (1 subgoal):
 1. absc (repcs (reps (state cfg)) cfg) = cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. absc (repcs (reps (state cfg)) cfg) = cfg
[PROOF STEP]
by (subst absc_repcs_id) (auto dest: R_G_I)


[STATEMENT]
lemma K_cfg_map_absc:
  "cfg \<in> valid_cfg \<Longrightarrow> K_cfg (absc cfg) = map_pmf absc (K_cfg cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg \<Longrightarrow> K_cfg (absc cfg) = map_pmf absc (K_cfg cfg)
[PROOF STEP]
by (auto simp: K_cfg_def map_pmf_comp action_absc abst_def cont_absc_1 intro: map_pmf_cong)


[STATEMENT]
lemma smap_comp:
  "(smap f o smap g) = smap (f o g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap f \<circ> smap g = smap (f \<circ> g)
[PROOF STEP]
by (auto simp: stream.map_comp)


[STATEMENT]
lemma state_abscD[simp]:
  assumes "cfg \<in> MDP.cfg_on s"
  shows "state (absc cfg) = abss s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (absc cfg) = abss s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.cfg_on s

goal (1 subgoal):
 1. state (absc cfg) = abss s
[PROOF STEP]
unfolding absc_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.cfg_on s

goal (1 subgoal):
 1. state (cfg_corec (abss (state cfg)) (abst \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) = abss s
[PROOF STEP]
by auto


[STATEMENT]
lemma R_G_valid_cfg_coinduct[coinduct set: valid_cfg]:
  assumes "P cfg"
  assumes "\<And>cfg. P cfg \<Longrightarrow> state cfg \<in> \<S>"
  assumes "\<And>cfg. P cfg \<Longrightarrow> action cfg \<in> \<K> (state cfg)"
  assumes "\<And>cfg t. P cfg \<Longrightarrow> t \<in> action cfg \<Longrightarrow> P (cont cfg t)"
  shows "cfg \<in> R_G.valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> R_G.valid_cfg
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cfg \<in> R_G.valid_cfg
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> \<S>
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> \<K> (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)
[PROOF STEP]
have "cfg \<in> R_G.cfg_on (state cfg)"
[PROOF STATE]
proof (prove)
using this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> \<S>
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> \<K> (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)

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

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

goal (1 subgoal):
 1. cfg \<in> R_G.valid_cfg
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> \<S>
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> \<K> (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)
[PROOF STEP]
have "state cfg \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> \<S>
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> \<K> (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)

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

goal (1 subgoal):
 1. cfg \<in> R_G.valid_cfg
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.cfg_on (state cfg)
state cfg \<in> \<S>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.cfg_on (state cfg)
state cfg \<in> \<S>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absc_valid[intro]:
  assumes "cfg \<in> valid_cfg"
  shows "absc cfg \<in> R_G.valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc cfg \<in> R_G.valid_cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. absc cfg \<in> R_G.valid_cfg
[PROOF STEP]
proof (coinduction arbitrary: cfg)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> state (absc cfga) \<in> \<S>
 2. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> action (absc cfga) \<in> \<K> (state (absc cfga))
 3. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
cfga \<in> MDP.valid_cfg

goal (3 subgoals):
 1. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> state (absc cfga) \<in> \<S>
 2. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> action (absc cfga) \<in> \<K> (state (absc cfga))
 3. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfga \<in> MDP.valid_cfg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfga \<in> MDP.valid_cfg

goal (1 subgoal):
 1. state (absc cfga) \<in> \<S>
[PROOF STEP]
by (auto simp: absc_def dest: MDP.valid_cfg_state_in_S)
[PROOF STATE]
proof (state)
this:
state (absc cfga) \<in> \<S>

goal (2 subgoals):
 1. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> action (absc cfga) \<in> \<K> (state (absc cfga))
 2. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> action (absc cfga) \<in> \<K> (state (absc cfga))
 2. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
case (2 cfg')
[PROOF STATE]
proof (state)
this:
cfg' \<in> MDP.valid_cfg

goal (2 subgoals):
 1. \<And>cfga. cfga \<in> MDP.valid_cfg \<Longrightarrow> action (absc cfga) \<in> \<K> (state (absc cfga))
 2. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg' \<in> MDP.valid_cfg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg' \<in> MDP.valid_cfg

goal (1 subgoal):
 1. action (absc cfg') \<in> \<K> (state (absc cfg'))
[PROOF STEP]
by (subst state_abscD) (auto intro: MDP.valid_cfgD action_abscD)
[PROOF STATE]
proof (state)
this:
action (absc cfg') \<in> \<K> (state (absc cfg'))

goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
case prems: (3 s' cfg)
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action (absc cfg))

goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
define t where "t \<equiv> THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)"
[PROOF STATE]
proof (state)
this:
t \<equiv> THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
let ?cfg = "cont cfg t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action (absc cfg))
[PROOF STEP]
obtain s where "s' = abss s" "s \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action (absc cfg))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s' = abss s; s \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: action_absc')
[PROOF STATE]
proof (state)
this:
s' = abss s
s \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
with cont_cfg_defined[OF prems(1), of s']
[PROOF STATE]
proof (chain)
picking this:
s' \<in> set_pmf (abst (action cfg)) \<Longrightarrow> (abss (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)) = s' \<and> (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)))
s' = abss s
s \<in> set_pmf (action cfg)
[PROOF STEP]
have
    "abss t = s'" "t \<in> set_pmf (action cfg)"
    "\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t"
[PROOF STATE]
proof (prove)
using this:
s' \<in> set_pmf (abst (action cfg)) \<Longrightarrow> (abss (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)) = s' \<and> (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)))
s' = abss s
s \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. abss t = s' &&& t \<in> set_pmf (action cfg) &&& \<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t
[PROOF STEP]
unfolding t_def abst_def
[PROOF STATE]
proof (prove)
using this:
s' \<in> set_pmf (map_pmf abss (action cfg)) \<Longrightarrow> (abss (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)) = s' \<and> (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. abss x = s' \<and> x \<in> set_pmf (action cfg)))
s' = abss s
s \<in> set_pmf (action cfg)

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

goal (1 subgoal):
 1. \<And>t cfga. \<lbrakk>cfga \<in> MDP.valid_cfg; t \<in> set_pmf (action (absc cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg. cont (absc cfga) t = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action (absc cfg))
abss t = s'
t \<in> set_pmf (action cfg)
\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action (absc cfg))
abss t = s'
t \<in> set_pmf (action cfg)
\<forall>y. abss y = s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t

goal (1 subgoal):
 1. \<exists>cfg. cont (absc cfg) s' = absc cfg \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
by (inst_existentials ?cfg)
       (auto intro: MDP.valid_cfg_cont simp: abst_def action_absc absc_def t_def)
[PROOF STATE]
proof (state)
this:
\<exists>cfg. cont (absc cfg) s' = absc cfg \<and> cfg \<in> MDP.valid_cfg

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_cfg_set_absc:
  assumes "cfg \<in> valid_cfg" "cfg' \<in> K_cfg cfg"
  shows "absc cfg' \<in> K_cfg (absc cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc cfg' \<in> set_pmf (K_cfg (absc cfg))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
cfg' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. absc cfg' \<in> set_pmf (K_cfg (absc cfg))
[PROOF STEP]
by (auto simp: K_cfg_map_absc)


[STATEMENT]
lemma abst_action_repcs:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg"
  shows "abst (action (repcs s cfg)) = action cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (action (repcs s cfg)) = action cfg
[PROOF STEP]
unfolding repc_def repcs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (action (cfg_corec s (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (s, cfg))) = action cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. abst (action (cfg_corec s (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (s, cfg))) = action cfg
[PROOF STEP]
by (simp, subst abst_rept_id) (auto intro: R_G_I)


[STATEMENT]
lemma abst_action_repc:
  assumes "cfg \<in> R_G.valid_cfg"
  shows "abst (action (repc cfg)) = action cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (action (repc cfg)) = action cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. abst (action (repc cfg)) = action cfg
[PROOF STEP]
unfolding repc_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. abst (action (repcs (reps (state cfg)) cfg)) = action cfg
[PROOF STEP]
by (auto intro: abst_action_repcs simp: R_G_I)


[STATEMENT]
lemma K_elem_abss_inj':
  assumes "\<mu> \<in> K s"
    and "s \<in> S"
  shows "inj_on abss (set_pmf \<mu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on abss (set_pmf \<mu>)
[PROOF STEP]
using assms K_elem_abss_inj
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K s
s \<in> S
\<lbrakk>?\<mu> \<in> K (?l, ?u); (?l, ?u) \<in> S\<rbrakk> \<Longrightarrow> inj_on abss (set_pmf ?\<mu>)

goal (1 subgoal):
 1. inj_on abss (set_pmf \<mu>)
[PROOF STEP]
by (simp add: K_bisim_unique inj_onI)


[STATEMENT]
lemma K_cfg_rept_aux:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg" "x \<in> rept s (action cfg)"
  defines "t \<equiv> \<lambda> cfg'. THE s'. s' \<in> rept s (action cfg) \<and> s' ~ x"
  shows "t cfg' = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t cfg' = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t cfg' = x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
x \<in> set_pmf (rept s (action cfg))
t \<equiv> \<lambda>cfg'. THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> s' ~ x
[PROOF STEP]
have "rept s (action cfg) \<in> K s" "s \<in> S"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
x \<in> set_pmf (rept s (action cfg))
t \<equiv> \<lambda>cfg'. THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> s' ~ x

goal (1 subgoal):
 1. rept s (action cfg) \<in> K s &&& s \<in> S
[PROOF STEP]
by (auto simp: R_G_I \<S>_abss_S)
[PROOF STATE]
proof (state)
this:
rept s (action cfg) \<in> K s
s \<in> S

goal (1 subgoal):
 1. t cfg' = x
[PROOF STEP]
from K_bisim_unique[OF this(2,1) _ assms(3)] assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> set_pmf (rept s (action cfg)); ?x ~ x\<rbrakk> \<Longrightarrow> ?x = x
x \<in> set_pmf (rept s (action cfg))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set_pmf (rept s (action cfg)); ?x ~ x\<rbrakk> \<Longrightarrow> ?x = x
x \<in> set_pmf (rept s (action cfg))

goal (1 subgoal):
 1. t cfg' = x
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set_pmf (rept s (action cfg)); ?x ~ x\<rbrakk> \<Longrightarrow> ?x = x
x \<in> set_pmf (rept s (action cfg))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_cfg_rept_action:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg" "cfg' \<in> set_pmf (K_cfg cfg)"
  shows "abss (THE s'. s' \<in> rept s (action cfg) \<and> abss s' = state cfg') = state cfg'"
[PROOF STATE]
proof (prove)
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 -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abss (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') = state cfg'
[PROOF STEP]
let ?\<mu> = "rept s (action cfg)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abss (THE s'. s' \<in> set_pmf (rept s (action cfg)) \<and> abss s' = state cfg') = state cfg'
[PROOF STEP]
from abst_rept_id assms
[PROOF STATE]
proof (chain)
picking this:
?\<mu> \<in> \<K> (abss ?s) \<Longrightarrow> abst (rept ?s ?\<mu>) = ?\<mu>
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
have "action cfg = abst ?\<mu>"
[PROOF STATE]
proof (prove)
using this:
?\<mu> \<in> \<K> (abss ?s) \<Longrightarrow> abst (rept ?s ?\<mu>) = ?\<mu>
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. action cfg = abst (rept s (action cfg))
[PROOF STEP]
by (auto simp: R_G_I)
[PROOF STATE]
proof (state)
this:
action cfg = abst (rept s (action 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]
moreover
[PROOF STATE]
proof (state)
this:
action cfg = abst (rept s (action 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]
from assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
have "state cfg' \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
cfg' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
by (auto simp: set_K_cfg)
[PROOF STATE]
proof (state)
this:
state cfg' \<in> set_pmf (action 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
action cfg = abst (rept s (action cfg))
state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
have "state cfg' \<in> abst ?\<mu>"
[PROOF STATE]
proof (prove)
using this:
action cfg = abst (rept s (action cfg))
state cfg' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. state cfg' \<in> set_pmf (abst (rept s (action cfg)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state cfg' \<in> set_pmf (abst (rept s (action 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]
then
[PROOF STATE]
proof (chain)
picking this:
state cfg' \<in> set_pmf (abst (rept s (action cfg)))
[PROOF STEP]
obtain s' where "s' \<in> ?\<mu>" "abss s' = state cfg'"
[PROOF STATE]
proof (prove)
using this:
state cfg' \<in> set_pmf (abst (rept s (action cfg)))

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>s' \<in> set_pmf (rept s (action cfg)); abss s' = state cfg'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: abst_def pmf.set_map)
[PROOF STATE]
proof (state)
this:
s' \<in> set_pmf (rept s (action cfg))
abss s' = 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]
with K_cfg_rept_aux[OF assms(1,2) this(1)]
[PROOF STATE]
proof (chain)
picking this:
(THE s'a. s'a \<in> set_pmf (rept s (action cfg)) \<and> s'a ~ s') = s'
s' \<in> set_pmf (rept s (action cfg))
abss s' = state cfg'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(THE s'a. s'a \<in> set_pmf (rept s (action cfg)) \<and> s'a ~ s') = s'
s' \<in> set_pmf (rept s (action cfg))
abss s' = 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]
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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_cfg_map_repcs:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg"
  defines "repc' \<equiv> (\<lambda> cfg'. repcs (THE s'. s' \<in> rept s (action cfg) \<and> abss s' = state cfg') cfg')"
  shows "K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
let ?\<mu> = "rept s (action cfg)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
define t where "t \<equiv> \<lambda> cfg'. THE s. s \<in> ?\<mu> \<and> abss s = state cfg'"
[PROOF STATE]
proof (state)
this:
t \<equiv> \<lambda>cfg'. THE sa. sa \<in> set_pmf (rept s (action cfg)) \<and> abss sa = state cfg'

goal (1 subgoal):
 1. K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
have t: "t (cont cfg (abss s')) = s'" if "s' \<in> ?\<mu>" for s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t (cont cfg (abss s')) = s'
[PROOF STEP]
using K_cfg_rept_aux[OF assms(1,2) that]
[PROOF STATE]
proof (prove)
using this:
(THE s'a. s'a \<in> set_pmf (rept s (action cfg)) \<and> s'a ~ s') = s'

goal (1 subgoal):
 1. t (cont cfg (abss s')) = s'
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
(THE s'a. s'a \<in> set_pmf (rept s (action cfg)) \<and> s'a ~ s') = s'

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

goal (1 subgoal):
 1. K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
unfolding K_cfg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (cont (repcs s cfg)) (action (repcs s cfg)) = map_pmf repc' (map_pmf (cont cfg) (action cfg))
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
?s'5 \<in> set_pmf (rept s (action cfg)) \<Longrightarrow> t (cont cfg (abss ?s'5)) = ?s'5

goal (1 subgoal):
 1. map_pmf (cont (repcs s cfg)) (action (repcs s cfg)) = map_pmf repc' (map_pmf (cont cfg) (action cfg))
[PROOF STEP]
by (subst abst_action_repcs[symmetric])
       (auto simp: repc_def repcs_def t_def map_pmf_comp abst_def assms intro: map_pmf_cong)
[PROOF STATE]
proof (state)
this:
K_cfg (repcs s cfg) = map_pmf repc' (K_cfg cfg)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_cfg_map_repc:
  assumes "cfg \<in> R_G.valid_cfg"
  defines
    "repc' cfg' \<equiv> repcs (THE s. s \<in> rept (reps (state cfg)) (action cfg) \<and> abss s = state cfg') cfg'"
  shows
    "K_cfg (repc cfg) = map_pmf repc' (K_cfg cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K_cfg (repc cfg) = map_pmf repc' (K_cfg cfg)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
repc' ?cfg'5 \<equiv> repcs (THE s. s \<in> set_pmf (rept (reps (state cfg)) (action cfg)) \<and> abss s = state ?cfg'5) ?cfg'5

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

goal (1 subgoal):
 1. K_cfg (repcs (reps (state cfg)) cfg) = map_pmf (\<lambda>cfg'. repcs (THE s. s \<in> set_pmf (rept (reps (state cfg)) (action cfg)) \<and> abss s = state cfg') cfg') (K_cfg cfg)
[PROOF STEP]
by (auto simp: R_G_I K_cfg_map_repcs)


[STATEMENT]
lemma K_cfg_valid_cfgD:
  assumes "cfg \<in> valid_cfg" "cfg' \<in> K_cfg cfg"
  shows "cfg' = cont cfg (state cfg')" "state cfg' \<in> action cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg' = cont cfg (state cfg') &&& state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cfg' = cont cfg (state cfg')
 2. state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
cfg' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
obtain s where "s \<in> action cfg" "cfg' = cont cfg s"
[PROOF STATE]
proof (prove)
using this:
cfg' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> set_pmf (action cfg); cfg' = cont cfg s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: set_K_cfg)
[PROOF STATE]
proof (state)
this:
s \<in> set_pmf (action cfg)
cfg' = cont cfg s

goal (2 subgoals):
 1. cfg' = cont cfg (state cfg')
 2. state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.valid_cfg
cfg' \<in> set_pmf (K_cfg cfg)
s \<in> set_pmf (action cfg)
cfg' = cont cfg s
[PROOF STEP]
show
    "cfg' = cont cfg (state cfg')" "state cfg' \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
cfg' \<in> set_pmf (K_cfg cfg)
s \<in> set_pmf (action cfg)
cfg' = cont cfg s

goal (1 subgoal):
 1. cfg' = cont cfg (state cfg') &&& state cfg' \<in> set_pmf (action cfg)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg' = cont cfg (state cfg')
state cfg' \<in> set_pmf (action cfg)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absc_bisim_abss:
  assumes "absc x = absc x'"
  shows "state x ~ state x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state x ~ state x'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state x ~ state x'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
absc x = absc x'
[PROOF STEP]
have "state (absc x) = state (absc x')"
[PROOF STATE]
proof (prove)
using this:
absc x = absc x'

goal (1 subgoal):
 1. state (absc x) = state (absc x')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state (absc x) = state (absc x')

goal (1 subgoal):
 1. state x ~ state x'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
state (absc x) = state (absc x')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state (absc x) = state (absc x')

goal (1 subgoal):
 1. state x ~ state x'
[PROOF STEP]
by (simp add: state_absc)
[PROOF STATE]
proof (state)
this:
state x ~ state x'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_cfg_bisim_unique:
  assumes "cfg \<in> valid_cfg" and "x \<in> K_cfg cfg" "x' \<in> K_cfg cfg" and "state x ~ state x'"
  shows "x = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = x'
[PROOF STEP]
define t where "t \<equiv> THE x'. x' ~ state x \<and> x' \<in> set_pmf (action cfg)"
[PROOF STATE]
proof (state)
this:
t \<equiv> THE x'. x' ~ state x \<and> x' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
from K_cfg_valid_cfgD assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?cfg \<in> MDP.valid_cfg; ?cfg' \<in> set_pmf (K_cfg ?cfg)\<rbrakk> \<Longrightarrow> ?cfg' = cont ?cfg (state ?cfg')
\<lbrakk>?cfg \<in> MDP.valid_cfg; ?cfg' \<in> set_pmf (K_cfg ?cfg)\<rbrakk> \<Longrightarrow> state ?cfg' \<in> set_pmf (action ?cfg)
cfg \<in> MDP.valid_cfg
x \<in> set_pmf (K_cfg cfg)
x' \<in> set_pmf (K_cfg cfg)
state x ~ state x'
[PROOF STEP]
have *:
    "x  = cont cfg (state x)"  "state x \<in> action cfg"
    "x' = cont cfg (state x')" "state x' \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?cfg \<in> MDP.valid_cfg; ?cfg' \<in> set_pmf (K_cfg ?cfg)\<rbrakk> \<Longrightarrow> ?cfg' = cont ?cfg (state ?cfg')
\<lbrakk>?cfg \<in> MDP.valid_cfg; ?cfg' \<in> set_pmf (K_cfg ?cfg)\<rbrakk> \<Longrightarrow> state ?cfg' \<in> set_pmf (action ?cfg)
cfg \<in> MDP.valid_cfg
x \<in> set_pmf (K_cfg cfg)
x' \<in> set_pmf (K_cfg cfg)
state x ~ state x'

goal (1 subgoal):
 1. (x = cont cfg (state x) &&& state x \<in> set_pmf (action cfg)) &&& x' = cont cfg (state x') &&& state x' \<in> set_pmf (action cfg)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.valid_cfg
x \<in> set_pmf (K_cfg cfg)
x' \<in> set_pmf (K_cfg cfg)
state x ~ state x'
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)
[PROOF STEP]
have
    "cfg \<in> valid_cfg" "abss (state x) \<in> set_pmf (abst (action cfg))"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
x \<in> set_pmf (K_cfg cfg)
x' \<in> set_pmf (K_cfg cfg)
state x ~ state x'
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg &&& abss (state x) \<in> set_pmf (abst (action cfg))
[PROOF STEP]
unfolding abst_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
x \<in> set_pmf (K_cfg cfg)
x' \<in> set_pmf (K_cfg cfg)
state x ~ state x'
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg &&& abss (state x) \<in> set_pmf (map_pmf abss (action cfg))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.valid_cfg
abss (state x) \<in> set_pmf (abst (action cfg))

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
with cont_cfg_defined[of cfg "abss (state x)"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>cfg \<in> MDP.valid_cfg; abss (state x) \<in> set_pmf (abst (action cfg))\<rbrakk> \<Longrightarrow> ((THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)) ~ state x \<and> (THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)))
cfg \<in> MDP.valid_cfg
abss (state x) \<in> set_pmf (abst (action cfg))
[PROOF STEP]
have
    "\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cfg \<in> MDP.valid_cfg; abss (state x) \<in> set_pmf (abst (action cfg))\<rbrakk> \<Longrightarrow> ((THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)) ~ state x \<and> (THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)))
cfg \<in> MDP.valid_cfg
abss (state x) \<in> set_pmf (abst (action cfg))

goal (1 subgoal):
 1. \<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cfg \<in> MDP.valid_cfg; abss (state x) \<in> set_pmf (abst (action cfg))\<rbrakk> \<Longrightarrow> ((THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)) ~ state x \<and> (THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE xa. xa ~ state x \<and> xa \<in> set_pmf (action cfg)))
cfg \<in> MDP.valid_cfg
abss (state x) \<in> set_pmf (abst (action cfg))

goal (1 subgoal):
 1. \<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x'. x' ~ state x \<and> x' \<in> set_pmf (action cfg))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
with * assms(4)
[PROOF STATE]
proof (chain)
picking this:
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)
state x ~ state x'
\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t
[PROOF STEP]
have "state x' = t" "state x = t"
[PROOF STATE]
proof (prove)
using this:
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)
state x ~ state x'
\<forall>y. y ~ state x \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = t

goal (1 subgoal):
 1. state x' = t &&& state x = t
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
state x' = t
state x = t

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)
state x' = t
state x = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = cont cfg (state x)
state x \<in> set_pmf (action cfg)
x' = cont cfg (state x')
state x' \<in> set_pmf (action cfg)
state x' = t
state x = t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absc_distr_self:
  "MDP.MC.T (absc cfg) = distr (MDP.MC.T cfg) MDP.MC.S (smap absc)" if "cfg \<in> valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MDP.MC.T (absc cfg) = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
using \<open>cfg \<in> _\<close>
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg

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

goal (3 subgoals):
 1. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> prob_space (distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc))
 2. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> sets (distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 3. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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 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 cfg) (stream_space (count_space UNIV)) (smap absc))

goal (2 subgoals):
 1. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> sets (distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 2. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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. cfg \<in> MDP.valid_cfg \<Longrightarrow> sets (distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 2. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case sets
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.valid_cfg

goal (2 subgoals):
 1. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> sets (distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))
 2. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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 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 cfg) (stream_space (count_space UNIV)) (smap absc)) = sets (stream_space (count_space UNIV))

goal (1 subgoal):
 1. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case prems: (cont cfg)
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.valid_cfg

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

goal (1 subgoal):
 1. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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 (t cfg)) MDP.MC.S (smap absc)"
[PROOF STATE]
proof (state)
this:
M' \<equiv> \<lambda>cfg. distr (MDP.MC.T (t cfg)) (stream_space (count_space UNIV)) (smap absc)

goal (1 subgoal):
 1. \<And>cfg. cfg \<in> MDP.valid_cfg \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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 (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
proof (rule exI[where x = M'], safe, goal_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg (absc cfg)) \<Longrightarrow> \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case A: (1 y)
[PROOF STATE]
proof (state)
this:
y \<in> set_pmf (K_cfg (absc cfg))

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg (absc cfg)) \<Longrightarrow> \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
from A prems
[PROOF STATE]
proof (chain)
picking this:
y \<in> set_pmf (K_cfg (absc cfg))
cfg \<in> MDP.valid_cfg
[PROOF STEP]
obtain x' where "y = absc x'" "x' \<in> K_cfg cfg"
[PROOF STATE]
proof (prove)
using this:
y \<in> set_pmf (K_cfg (absc cfg))
cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>y = absc x'; x' \<in> set_pmf (K_cfg cfg)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: K_cfg_map_absc)
[PROOF STATE]
proof (state)
this:
y = absc x'
x' \<in> set_pmf (K_cfg cfg)

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg (absc cfg)) \<Longrightarrow> \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
with K_cfg_bisim_unique[OF prems _ _ absc_bisim_abss]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> set_pmf (K_cfg cfg); ?x' \<in> set_pmf (K_cfg cfg); absc ?x = absc ?x'\<rbrakk> \<Longrightarrow> ?x = ?x'
y = absc x'
x' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
have
      "y = absc (t y)" "x' = t y"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set_pmf (K_cfg cfg); ?x' \<in> set_pmf (K_cfg cfg); absc ?x = absc ?x'\<rbrakk> \<Longrightarrow> ?x = ?x'
y = absc x'
x' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. y = absc (t y) &&& x' = t y
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set_pmf (K_cfg cfg); ?x' \<in> set_pmf (K_cfg cfg); absc ?x = absc ?x'\<rbrakk> \<Longrightarrow> ?x = ?x'
y = absc x'
x' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. y = absc (THE x. y = absc x \<and> x \<in> set_pmf (K_cfg cfg)) &&& x' = (THE x. y = absc x \<and> x \<in> set_pmf (K_cfg cfg))
[PROOF STEP]
by (auto intro: theI2)
[PROOF STATE]
proof (state)
this:
y = absc (t y)
x' = t y

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg (absc cfg)) \<Longrightarrow> \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = absc (t y)
x' = t y

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg (absc cfg)) \<Longrightarrow> \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
have "x' \<in> valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<in> MDP.valid_cfg
[PROOF STEP]
using \<open>x' \<in> _\<close> prems
[PROOF STATE]
proof (prove)
using this:
x' \<in> set_pmf (K_cfg cfg)
cfg \<in> MDP.valid_cfg

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

goal (5 subgoals):
 1. \<And>y. y \<in> set_pmf (K_cfg (absc cfg)) \<Longrightarrow> \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y = absc (t y)
x' = t y
x' \<in> MDP.valid_cfg
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
y = absc (t y)
x' = t y
x' \<in> MDP.valid_cfg

goal (1 subgoal):
 1. \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
unfolding M'_def
[PROOF STATE]
proof (prove)
using this:
y = absc (t y)
x' = t y
x' \<in> MDP.valid_cfg

goal (1 subgoal):
 1. \<exists>cfg. y = absc cfg \<and> distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) (smap absc) = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case 5
[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 cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc 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. distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
unfolding M'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (distr (MDP.MC.T (t 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. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
 3. distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 2. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 3. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (subst MDP.MC.T_eq_bind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. distr (measure_pmf (K_cfg 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 (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 2. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 3. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (subst distr_bind)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 2. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 3. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 4. measure_pmf (K_cfg 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 (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 5. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 6. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
prefer 4
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. measure_pmf (K_cfg 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 (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 2. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 3. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 4. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 5. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 6. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (subst distr_distr)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 3. measure_pmf (K_cfg cfg) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 4. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 5. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 6. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 7. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. measure_pmf (K_cfg cfg) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 2. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 3. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 4. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 5. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 6. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 7. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (subst K_cfg_map_absc)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. cfg \<in> MDP.valid_cfg
 2. measure_pmf (K_cfg cfg) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (map_pmf absc (K_cfg cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 3. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 4. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 5. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 6. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 7. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 9. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (rule prems)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. measure_pmf (K_cfg cfg) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = measure_pmf (map_pmf absc (K_cfg cfg)) \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 2. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 3. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 4. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 5. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 6. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 7. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (subst map_pmf_rep_eq)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. measure_pmf (K_cfg cfg) \<bind> (\<lambda>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x)) = distr (measure_pmf (K_cfg cfg)) (count_space UNIV) absc \<bind> (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc))
 2. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 3. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 4. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 5. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 6. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 7. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>y. MDP.MC.T.random_variable (t y) (stream_space (count_space UNIV)) (smap absc)
[PROOF STEP]
apply (subst bind_distr)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. measure_pmf.random_variable (K_cfg cfg) (count_space UNIV) absc
 2. (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra ?K12
 3. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 4. measure_pmf (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>x. distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc))
 5. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 6. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 7. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 8. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 9. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 10. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
A total of 11 subgoals...
[PROOF STEP]
prefer 4
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. measure_pmf (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>x. distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc))
 2. measure_pmf.random_variable (K_cfg cfg) (count_space UNIV) absc
 3. (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra ?K12
 4. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 5. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 6. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 7. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 8. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 9. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 10. \<And>y. (##) y \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
A total of 11 subgoals...
[PROOF STEP]
apply (rule bind_measure_pmf_cong)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) \<in> space (subprob_algebra ?N14)
 2. \<And>x. distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc) \<in> space (subprob_algebra ?N14)
 3. \<And>i. i \<in> set_pmf (K_cfg cfg) \<Longrightarrow> distr (MDP.MC.T i) (stream_space (count_space UNIV)) (smap absc \<circ> (##) i) = distr (MDP.MC.T (t (absc i))) (stream_space (count_space UNIV)) ((##) (absc i) \<circ> smap absc)
 4. measure_pmf.random_variable (K_cfg cfg) (count_space UNIV) absc
 5. (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra ?K12
 6. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 7. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 9. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 10. space (measure_pmf (K_cfg cfg)) \<noteq> {}
A total of 13 subgoals...
[PROOF STEP]
prefer 3
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>i. i \<in> set_pmf (K_cfg cfg) \<Longrightarrow> distr (MDP.MC.T i) (stream_space (count_space UNIV)) (smap absc \<circ> (##) i) = distr (MDP.MC.T (t (absc i))) (stream_space (count_space UNIV)) ((##) (absc i) \<circ> smap absc)
 2. \<And>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) \<in> space (subprob_algebra ?N14)
 3. \<And>x. distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc) \<in> space (subprob_algebra ?N14)
 4. measure_pmf.random_variable (K_cfg cfg) (count_space UNIV) absc
 5. (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra ?K12
 6. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 7. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 8. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 9. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 10. space (measure_pmf (K_cfg cfg)) \<noteq> {}
A total of 13 subgoals...
[PROOF STEP]
subgoal premises A for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) = distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) = distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc)
[PROOF STEP]
have "t (absc x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t (absc x) = x
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE xa. absc x = absc xa \<and> xa \<in> set_pmf (K_cfg cfg)) = x
[PROOF STEP]
proof (rule the_equality, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. absc x = absc x \<and> x \<in> set_pmf (K_cfg cfg)
 2. \<And>xa. absc x = absc xa \<and> xa \<in> set_pmf (K_cfg cfg) \<Longrightarrow> xa = x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. absc x = absc x \<and> x \<in> set_pmf (K_cfg cfg)
 2. \<And>xa. absc x = absc xa \<and> xa \<in> set_pmf (K_cfg cfg) \<Longrightarrow> xa = x
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
x \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. absc x = absc x \<and> x \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
absc x = absc x \<and> x \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. \<And>xa. absc x = absc xa \<and> xa \<in> set_pmf (K_cfg cfg) \<Longrightarrow> xa = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. absc x = absc xa \<and> xa \<in> set_pmf (K_cfg cfg) \<Longrightarrow> xa = x
[PROOF STEP]
case (2 x')
[PROOF STATE]
proof (state)
this:
absc x = absc x' \<and> x' \<in> set_pmf (K_cfg cfg)

goal (1 subgoal):
 1. \<And>xa. absc x = absc xa \<and> xa \<in> set_pmf (K_cfg cfg) \<Longrightarrow> xa = x
[PROOF STEP]
with K_cfg_bisim_unique[OF prems _ A absc_bisim_abss]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> set_pmf (K_cfg cfg); absc ?x = absc x\<rbrakk> \<Longrightarrow> ?x = x
absc x = absc x' \<and> x' \<in> set_pmf (K_cfg cfg)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set_pmf (K_cfg cfg); absc ?x = absc x\<rbrakk> \<Longrightarrow> ?x = x
absc x = absc x' \<and> x' \<in> set_pmf (K_cfg cfg)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t (absc x) = x

goal (1 subgoal):
 1. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) = distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t (absc x) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t (absc x) = x

goal (1 subgoal):
 1. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) = distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc)
[PROOF STEP]
by (auto simp: comp_def)
[PROOF STATE]
proof (state)
this:
distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) = distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>x. distr (MDP.MC.T x) (stream_space (count_space UNIV)) (smap absc \<circ> (##) x) \<in> space (subprob_algebra ?N14)
 2. \<And>x. distr (MDP.MC.T (t (absc x))) (stream_space (count_space UNIV)) ((##) (absc x) \<circ> smap absc) \<in> space (subprob_algebra ?N14)
 3. measure_pmf.random_variable (K_cfg cfg) (count_space UNIV) absc
 4. (\<lambda>y. distr (MDP.MC.T (t y)) (stream_space (count_space UNIV)) ((##) y \<circ> smap absc)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra ?K12
 5. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 6. \<And>x. smap absc \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 7. \<And>x. MDP.MC.T.random_variable x (stream_space (count_space UNIV)) ((##) x)
 8. measure_pmf.random_variable (K_cfg cfg) (subprob_algebra ?K3) (\<lambda>t. distr (MDP.MC.T t) (stream_space (count_space UNIV)) ((##) t))
 9. space (measure_pmf (K_cfg cfg)) \<noteq> {}
 10. smap absc \<in> ?K3 \<rightarrow>\<^sub>M stream_space (count_space UNIV)
A total of 12 subgoals...
[PROOF STEP]
by (fastforce
          simp:  space_subprob_algebra MC_syntax.in_S
          intro: bind_measure_pmf_cong MDP.MC.T.subprob_space_distr MDP.MC.T.prob_space_distr
          )+
[PROOF STATE]
proof (state)
this:
distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) 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. \<And>y. prob_space (M' y)
[PROOF STEP]
qed (auto simp: M'_def intro: MDP.MC.T.prob_space_distr)
[PROOF STATE]
proof (state)
this:
\<exists>M'. (\<forall>y\<in>set_pmf (K_cfg (absc cfg)). \<exists>cfg. y = absc cfg \<and> M' y = distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) \<and> cfg \<in> MDP.valid_cfg) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (MDP.MC.T cfg) (stream_space (count_space UNIV)) (smap absc) = measure_pmf (K_cfg (absc cfg)) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))

goal:
No subgoals!
[PROOF STEP]
qed