theory Atomicity_Lib

lemma rel_tr_refinement_bind_left_general:
  "reflp sr
    \<Longrightarrow> (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t)
    \<Longrightarrow> rel_tr_refinement sr P R C f g
    \<Longrightarrow> rel_tr_refinement sr P R C (f >>= (\<lambda>x. h x)) (g >>= h)" apply (subst rel_tr_refinement_def, clarsimp) apply (erule elem_bindE) apply (drule(3) rel_tr_refinementD, simp) apply (clarsimp simp: bind_def) apply (strengthen bexI[mk_strg I _ E], simp) apply auto[1] apply (clarsimp simp: rely_cond_append) apply (drule(3) rel_tr_refinementD, simp) apply (clarsimp simp: bind_def) apply (simp add: image_def) apply (strengthen bexI[mk_strg I _ E] | simp)+ apply (simp add: list_all2_append rely_cond_append
                   list_all2_same reflpD[where R=sr] rel_prod_sel
        split del: if_split) apply (erule rely_cond_equiv_s) apply (erule disjE) apply (drule spec, drule(2) not_env_steps_firstD) apply (clarsimp simp: neq_Nil_conv list_all2_Cons1 split: if_split_asm) apply (clarsimp simp: neq_Nil_conv list_all2_Cons1 last_st_tr_def hd_append
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t); rel_tr_refinement sr P R C f g\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (f >>= h) (g >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; (tr, res) \<in> (f >>= h) s; rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr res s s0. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr'
 2. \<And>tr res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr res s s0. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s; \<exists>tr'. (tr', map_tmres undefined undefined res) \<in> g s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr'
 2. \<And>tr res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr res s s0 tr'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s; (tr', map_tmres undefined undefined res) \<in> g s; rely_cond R s0 tr'; list_all2 (rel_prod (=) sr) tr tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (\<exists>x\<in>g s. (tr', res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` h rv s)) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr'
 2. \<And>tr res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>tr res s s0 tr'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s; (tr', map_tmres undefined undefined res) \<in> g s; rely_cond R s0 tr'; list_all2 (rel_prod (=) sr) tr tr'\<rbrakk> \<Longrightarrow> \<exists>x. (x, res) \<in> (case map_tmres undefined undefined res of Failed \<Rightarrow> {(tr', Failed)} | Incomplete \<Rightarrow> {(tr', Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ tr', x)) ` h rv s) \<and> rely_cond R s0 x \<and> list_all2 (rel_prod (=) sr) tr x
 2. \<And>tr res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (g >>= h) s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); rel_tr_refinement sr P R C f g; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''\<rbrakk> \<Longrightarrow> \<exists>tr'a. (tr'a, res) \<in> (g >>= h) s \<and> rely_cond R s0 tr'a \<and> list_all2 (rel_prod (=) sr) (tr'' @ tr') tr'a proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s'. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; \<exists>tr'a. (tr'a, Result (x, s')) \<in> g s \<and> rely_cond R s0 tr'a \<and> list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'a. (tr'a, res) \<in> (g >>= h) s \<and> rely_cond R s0 tr'a \<and> list_all2 (rel_prod (=) sr) (tr'' @ tr') tr'a proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'a. (\<exists>x\<in>g s. (tr'a, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` h rv s)) \<and> rely_cond R s0 tr'a \<and> list_all2 (rel_prod (=) sr) (tr'' @ tr') tr'a proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'a. (\<exists>x\<in>g s. (tr'a, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {y. \<exists>x\<in>h rv s. y = (case x of (a, x) \<Rightarrow> (a @ xs, x))})) \<and> rely_cond R s0 tr'a \<and> list_all2 (rel_prod (=) sr) (tr'' @ tr') tr'a proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> rely_cond R s0 (tr'' @ tr'a) \<and> list_all2 (rel_prod (=) sr) (tr'' @ tr') (tr'' @ tr'a) proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> rely_cond R (last_st_tr tr'a s0) tr'' proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a sa. \<lbrakk>reflp sr; (\<forall>x. not_env_steps_first (h x)) \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; tr'' \<noteq> []; last tr'' = (Env, sa); R (last_st_tr tr' s0) sa\<rbrakk> \<Longrightarrow> R (last_st_tr tr'a s0) sa proof (prove)
goal (2 subgoals):
 1. \<And>res s s0 tr' tr'' x s' tr'a sa. \<lbrakk>reflp sr; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; tr'' \<noteq> []; last tr'' = (Env, sa); R (last_st_tr tr' s0) sa; \<forall>x. not_env_steps_first (h x)\<rbrakk> \<Longrightarrow> R (last_st_tr tr'a s0) sa
 2. \<And>res s s0 tr' tr'' x s' tr'a sa. \<lbrakk>reflp sr; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; tr'' \<noteq> []; last tr'' = (Env, sa); R (last_st_tr tr' s0) sa; \<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)\<rbrakk> \<Longrightarrow> R (last_st_tr tr'a s0) sa proof (prove)
goal (2 subgoals):
 1. \<And>res s s0 tr' tr'' x s' tr'a sa. \<lbrakk>reflp sr; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; tr'' \<noteq> []; last tr'' = (Env, sa); R (last_st_tr tr' s0) sa; fst (last tr'') = Me\<rbrakk> \<Longrightarrow> R (last_st_tr tr'a s0) sa
 2. \<And>res s s0 tr' tr'' x s' tr'a sa. \<lbrakk>reflp sr; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; tr'' \<noteq> []; last tr'' = (Env, sa); R (last_st_tr tr' s0) sa; \<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)\<rbrakk> \<Longrightarrow> R (last_st_tr tr'a s0) sa proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a sa. \<lbrakk>reflp sr; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> h x s'; rely_cond R s0 tr'; (tr'a, Result (x, s')) \<in> g s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; tr'' \<noteq> []; last tr'' = (Env, sa); R (last_st_tr tr' s0) sa; \<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)\<rbrakk> \<Longrightarrow> R (last_st_tr tr'a s0) sa proof (prove)
goal:
No subgoals!