theory Atomicity_Lib

lemma rel_tr_refinement_bind_right_general:
  "reflp sr
    \<Longrightarrow> \<forall>x. rel_tr_refinement sr Q R C' (g x) (h x)
    \<Longrightarrow> \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>,\<lbrace>R\<rbrace> f
        \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>
    \<Longrightarrow> rel_tr_refinement sr P R C (f >>= (\<lambda>x. g x)) (f >>= h)" apply (subst rel_tr_refinement_def, clarsimp) apply (erule elem_bindE) apply (clarsimp simp: bind_def) apply (strengthen bexI[mk_strg I _ E], simp) apply (auto simp: list_all2_same reflpD[where R=sr])[1] apply (clarsimp simp: rely_cond_append) apply (drule validI_D, erule(1) conjI, assumption+, clarsimp) apply (drule spec, drule(3) rel_tr_refinementD,
    simp add: hd_append hd_map split: if_split_asm) apply (clarsimp simp: bind_def) apply (simp add: image_def) apply (strengthen bexI[mk_strg I _ E] | simp)+ apply (simp add: list_all2_append list_all2_lengthD) apply (simp add: rely_cond_append list_all2_same reflpD[where R=sr] rel_prod_sel
        split del: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflp sr; \<forall>x. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (f >>= g) (f >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0. \<lbrakk>reflp sr; \<forall>x. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; P s; (tr, res) \<in> (f >>= g) s; rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; 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> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; 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'. (\<exists>x\<in>f 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; 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>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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C' \<longrightarrow> s0 = s) \<and> Q s\<rbrace>; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g 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> (f >>= 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. rel_tr_refinement sr Q R C' (g x) (h x); P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; C' \<longrightarrow> last_st_tr tr' s0 = s'; Q s'\<rbrakk> \<Longrightarrow> \<exists>tr'a. (tr'a, res) \<in> (f >>= 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; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; C' \<longrightarrow> last_st_tr tr' s0 = s'; Q s'; \<exists>tr'a. (tr'a, res) \<in> h x s' \<and> rely_cond R (last_st_tr tr' s0) tr'a \<and> list_all2 (rel_prod (=) sr) tr'' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'a. (tr'a, res) \<in> (f >>= 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; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; C' \<longrightarrow> last_st_tr tr' s0 = s'; Q s'; (tr'a, res) \<in> h x s'; rely_cond R (last_st_tr tr' s0) tr'a; list_all2 (rel_prod (=) sr) tr'' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'a. (\<exists>x\<in>f 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; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; C' \<longrightarrow> last_st_tr tr' s0 = s'; Q s'; (tr'a, res) \<in> h x s'; rely_cond R (last_st_tr tr' s0) tr'a; list_all2 (rel_prod (=) sr) tr'' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'a. (\<exists>x\<in>f 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; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; C' \<longrightarrow> last_st_tr tr' s0 = s'; Q s'; (tr'a, res) \<in> h x s'; rely_cond R (last_st_tr tr' s0) tr'a; list_all2 (rel_prod (=) sr) tr'' tr'a\<rbrakk> \<Longrightarrow> rely_cond R s0 (tr'a @ tr') \<and> list_all2 (rel_prod (=) sr) (tr'' @ tr') (tr'a @ tr') proof (prove)
goal (1 subgoal):
 1. \<And>res s s0 tr' tr'' x s' tr'a. \<lbrakk>reflp sr; P s; C \<longrightarrow> s0 = s; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; rely_cond R s0 tr'; rely_cond R (last_st_tr tr' s0) tr''; C' \<longrightarrow> last_st_tr tr' s0 = s'; Q s'; (tr'a, res) \<in> h x s'; rely_cond R (last_st_tr tr' s0) tr'a; list_all2 (rel_prod (=) sr) tr'' tr'a\<rbrakk> \<Longrightarrow> rely_cond R s0 (tr'a @ tr') \<and> list_all2 (rel_prod (=) sr) tr' tr' proof (prove)
goal:
No subgoals!