theory Atomicity_Lib

lemma shuttle_modify_interference[simplified K_bind_def]:
  assumes sr: "\<forall>s. sr s (f s)" (*FIXME add P as in next lemma*)
    and P_stable: "\<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> P t"
    and R: "\<forall>s0 s. P s0 \<longrightarrow> R s0 s \<longrightarrow> R (f s0) (f s)"
  shows
  "rel_tr_refinement sr P R C
        (do interference; modify f od)
        (do modify f; interference od)" proof - have list_all2_map:
    "\<And>xs. list_all2 (rel_prod (=) sr) xs (map (apsnd f) xs)" by (clarsimp simp add: list_all2_map2 list_all2_same sr) have rely_cond:
    "\<And>xs. \<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xs)
                  \<longrightarrow> rely_cond R (f s) (map (apsnd f o Pair Env) xs)" apply (induct_tac xs rule: rev_induct; simp add: rely_cond_append) apply clarsimp apply (rule conjI[rotated]) apply (frule_tac t=x in P_stable[rule_format]) apply (clarsimp simp: rely_cond_def) apply (drule spec, drule(1) mp, drule(1) mp) apply (clarsimp simp: rely_cond_def) apply (clarsimp simp: rely_cond_def R) done show ?thesis apply (clarsimp simp: rel_tr_refinement_def) apply (clarsimp simp: bind_def commit_step_def get_def return_def
                          put_trace_elem_def modify_def put_def
                          interference_def env_steps_def select_def
                          ) apply (erule disjE; clarsimp) apply (simp add: put_trace_eq_drop) apply (clarsimp; split if_split_asm) apply (clarsimp simp: image_Union) apply (rule exI, strengthen list_all2_map) apply (clarsimp simp: rely_cond_append) apply (frule(1) rely_cond[rule_format]) apply simp apply (simp add: rely_cond_append rely_cond_Cons) apply (rule exI[where x="map f xs" for xs]) apply (simp add: o_def, strengthen refl) apply (simp add: last_st_tr_def hd_append hd_map) apply (clarsimp simp: Sigma_def image_Union) apply (rule exI, strengthen list_all2_map) apply (clarsimp simp: rely_cond_append drop_map) apply (frule(1) rely_cond[rule_format]) apply (simp add: rely_cond_append rely_cond_Cons) apply (rule exI[where x="map f xs" for xs]) apply (simp add: drop_map[symmetric] o_def) apply auto done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do interference;
modify f
od) (do modify f;
interference
od) proof (state)
goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do interference;
modify f
od) (do modify f;
interference
od) proof (prove)
goal (1 subgoal):
 1. \<And>xs. list_all2 (rel_prod (=) sr) xs (map (apsnd f) xs) proof (state)
this:
list_all2 (rel_prod (=) sr) ?xs (map (apsnd f) ?xs)

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do interference;
modify f
od) (do modify f;
interference
od) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xs) \<longrightarrow> rely_cond R (f s) (map (apsnd f \<circ> Pair Env) xs) proof (prove)
goal (1 subgoal):
 1. \<And>x xsa. \<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa) \<Longrightarrow> \<forall>s. P s \<longrightarrow> rely_cond R s [(Env, x)] \<and> rely_cond R x (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) [(Env, f x)] \<and> rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa) proof (prove)
goal (1 subgoal):
 1. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f s) [(Env, f x)] \<and> rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa) proof (prove)
goal (2 subgoals):
 1. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa)
 2. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f s) [(Env, f x)] proof (prove)
goal (3 subgoals):
 1. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> R s x
 2. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa); P x\<rbrakk> \<Longrightarrow> rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa)
 3. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f s) [(Env, f x)] proof (prove)
goal (2 subgoals):
 1. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa); P x\<rbrakk> \<Longrightarrow> rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa)
 2. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f s) [(Env, f x)] proof (prove)
goal (2 subgoals):
 1. \<And>x xsa s. \<lbrakk>P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa); P x; rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f x) (map (\<lambda>a. (Env, f a)) xsa)
 2. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f s) [(Env, f x)] proof (prove)
goal (1 subgoal):
 1. \<And>x xsa s. \<lbrakk>\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) xsa) \<longrightarrow> rely_cond R (f s) (map (\<lambda>a. (Env, f a)) xsa); P s; rely_cond R s [(Env, x)]; rely_cond R x (map (Pair Env) xsa)\<rbrakk> \<Longrightarrow> rely_cond R (f s) [(Env, f x)] proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>s. P s \<longrightarrow> rely_cond R s (map (Pair Env) ?xs1) \<longrightarrow> rely_cond R (f s) (map (apsnd f \<circ> Pair Env) ?xs1)

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do interference;
modify f
od) (do modify f;
interference
od) proof (prove)
goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do interference;
modify f
od) (do modify f;
interference
od) proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0. \<lbrakk>P s; (tr, res) \<in> (do y <- interference;
modify f
od) s; rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> (do y <- modify f;
interference
od) 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. \<lbrakk>P s; tr = [] \<and> res = Incomplete \<or> (\<exists>x. \<exists>y\<in>put_trace (map (Pair Env) x) s. \<exists>x\<in>case y of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, sa)) \<Rightarrow> {(xs, Result ((), last_st_tr (map (Pair Env) x) s))}. (tr, res) \<in> (case case x of (a, x) \<Rightarrow> (a @ [(Me, s)], x) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result ((), f s))})); rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<in>put_trace (map (Pair Env) rv) sa. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rva, sa)) \<Rightarrow> {(xs, Result ((), last_st_tr (map (Pair Env) rv) (f 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 x a b aa ba. \<lbrakk>P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (a, b) \<in> put_trace (map (Pair Env) x) s; (aa, ba) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, sa) \<Rightarrow> {(a, Result ((), last_st_tr (map (Pair Env) x) s))}); (tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<in>put_trace (map (Pair Env) rv) sa. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rva, sa)) \<Rightarrow> {(xs, Result ((), last_st_tr (map (Pair Env) rv) (f 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 x a b aa ba. \<lbrakk>P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (a, b) \<in> (\<lambda>xa. (drop xa (map (Pair Env) x), if xa = 0 then Result ((), s) else Incomplete)) ` {..length x}; (aa, ba) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, sa) \<Rightarrow> {(a, Result ((), last_st_tr (map (Pair Env) x) s))}); (tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f 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 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa = 0; (aa, ba) \<in> (case Result ((), s) of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr'
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; rely_cond R s0 (map (Pair Env) x @ [(Me, s)]); C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (\<exists>xa. tr' = map (Pair Env) xa @ [(Me, f s)] \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) xa) (f s)) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) (map (Pair Env) x @ [(Me, s)]) tr'
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; rely_cond R s0 (map (Pair Env) x @ [(Me, s)]); C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> (\<exists>xa. map (apsnd f) (map (Pair Env) x @ [(Me, s)]) = map (Pair Env) xa @ [(Me, f s)] \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) xa) (f s)) \<and> rely_cond R s0 (map (apsnd f) (map (Pair Env) x @ [(Me, s)])) \<and> True
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; C \<longrightarrow> s0 = s; rely_cond R s0 [(Me, s)]; rely_cond R s (map (Pair Env) x)\<rbrakk> \<Longrightarrow> (\<exists>xa. map (apsnd f \<circ> Pair Env) x = map (Pair Env) xa \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) xa) (f s)) \<and> rely_cond R s0 [(Me, f s)] \<and> rely_cond R (f s) (map (apsnd f \<circ> Pair Env) x)
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; C \<longrightarrow> s0 = s; rely_cond R s0 [(Me, s)]; rely_cond R s (map (Pair Env) x); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) x)\<rbrakk> \<Longrightarrow> (\<exists>xa. map (apsnd f \<circ> Pair Env) x = map (Pair Env) xa \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) xa) (f s)) \<and> rely_cond R s0 [(Me, f s)] \<and> rely_cond R (f s) (map (apsnd f \<circ> Pair Env) x)
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; C \<longrightarrow> s0 = s; rely_cond R s0 [(Me, s)]; rely_cond R s (map (Pair Env) x); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) x)\<rbrakk> \<Longrightarrow> (\<exists>xa. map (apsnd f \<circ> Pair Env) x = map (Pair Env) xa \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) xa) (f s)) \<and> rely_cond R s0 [(Me, f s)]
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; C \<longrightarrow> s0 = s; rely_cond R s (map (Pair Env) x); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) x)\<rbrakk> \<Longrightarrow> \<exists>xa. map (apsnd f \<circ> Pair Env) x = map (Pair Env) xa \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) xa) (f s)
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; C \<longrightarrow> s0 = s; rely_cond R s (map (Pair Env) x); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) x)\<rbrakk> \<Longrightarrow> map (apsnd f \<circ> Pair Env) x = map (Pair Env) (map f (?xs164 s s0 x)) \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (Pair Env) (map f (?xs164 s s0 x))) (f s)
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>s s0 x. \<lbrakk>P s; C \<longrightarrow> s0 = s; rely_cond R s (map (Pair Env) x); rely_cond R (f s) (map (\<lambda>x. (Env, f x)) x)\<rbrakk> \<Longrightarrow> True \<and> f (last_st_tr (map (Pair Env) x) s) = last_st_tr (map (\<lambda>x. (Env, f x)) x) (f s)
 2. \<And>tr res s s0 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f 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 x aa ba xa. \<lbrakk>(tr, res) \<in> (case ba of Failed \<Rightarrow> {(aa @ [(Me, s)], Failed)} | Incomplete \<Rightarrow> {(aa @ [(Me, s)], Incomplete)} | Result (rv, sa) \<Rightarrow> {(aa @ [(Me, s)], Result ((), f sa))}); xa \<le> length x; P s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; xa \<noteq> 0; (aa, ba) \<in> (case Incomplete of Failed \<Rightarrow> {(drop xa (map (Pair Env) x), Failed)} | Incomplete \<Rightarrow> {(drop xa (map (Pair Env) x), Incomplete)} | Result (rv, sa) \<Rightarrow> {(drop xa (map (Pair Env) x), Result ((), last_st_tr (map (Pair Env) x) s))})\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<and> res = Incomplete \<or> (tr', res) \<in> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ [(Me, f s)], x)) ` (\<Union>x\<in>UNIV \<times> {f s}. case x of (rv, sa) \<Rightarrow> \<Union>x\<le>length rv. case if x = 0 then Result ((), sa) else Incomplete of Failed \<Rightarrow> {(drop x (map (Pair Env) rv), Failed)} | Incomplete \<Rightarrow> {(drop x (map (Pair Env) rv), Incomplete)} | Result (rva, sa) \<Rightarrow> {(drop x (map (Pair Env) rv), Result ((), last_st_tr (map (Pair Env) rv) (f s)))})) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; rely_cond R s0 (drop xa (map (Pair Env) x) @ [(Me, s)]); C \<longrightarrow> s0 = s; 0 < xa\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr' = [] \<or> (\<exists>y. \<exists>x\<in>{..length y}. 0 < x \<and> (0 < x \<longrightarrow> tr' = drop x (map (Pair Env) y) @ [(Me, f s)]))) \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) (drop xa (map (Pair Env) x) @ [(Me, s)]) tr' proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; rely_cond R s0 (drop xa (map (Pair Env) x) @ [(Me, s)]); C \<longrightarrow> s0 = s; 0 < xa\<rbrakk> \<Longrightarrow> (map (apsnd f) (drop xa (map (Pair Env) x) @ [(Me, s)]) = [] \<or> (\<exists>y. \<exists>xb\<in>{..length y}. 0 < xb \<and> (0 < xb \<longrightarrow> map (apsnd f) (drop xa (map (Pair Env) x) @ [(Me, s)]) = drop xb (map (Pair Env) y) @ [(Me, f s)]))) \<and> rely_cond R s0 (map (apsnd f) (drop xa (map (Pair Env) x) @ [(Me, s)])) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; C \<longrightarrow> s0 = s; 0 < xa; rely_cond R s0 [(Me, s)]; rely_cond R s (map (Pair Env) (drop xa x))\<rbrakk> \<Longrightarrow> (\<exists>y. \<exists>xb\<in>{..length y}. 0 < xb \<and> (0 < xb \<longrightarrow> map (apsnd f \<circ> Pair Env) (drop xa x) = map (Pair Env) (drop xb y))) \<and> rely_cond R s0 [(Me, f s)] \<and> rely_cond R (f s) (map (apsnd f \<circ> Pair Env) (drop xa x)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; C \<longrightarrow> s0 = s; 0 < xa; rely_cond R s0 [(Me, s)]; rely_cond R s (map (Pair Env) (drop xa x)); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) (drop xa x))\<rbrakk> \<Longrightarrow> (\<exists>y. \<exists>xb\<in>{..length y}. 0 < xb \<and> (0 < xb \<longrightarrow> map (apsnd f \<circ> Pair Env) (drop xa x) = map (Pair Env) (drop xb y))) \<and> rely_cond R s0 [(Me, f s)] \<and> rely_cond R (f s) (map (apsnd f \<circ> Pair Env) (drop xa x)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; C \<longrightarrow> s0 = s; 0 < xa; rely_cond R s (map (Pair Env) (drop xa x)); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) (drop xa x))\<rbrakk> \<Longrightarrow> \<exists>y. \<exists>xb\<in>{..length y}. 0 < xb \<and> (0 < xb \<longrightarrow> map (apsnd f \<circ> Pair Env) (drop xa x) = map (Pair Env) (drop xb y)) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; C \<longrightarrow> s0 = s; 0 < xa; rely_cond R s (map (Pair Env) (drop xa x)); rely_cond R (f s) (map (apsnd f \<circ> Pair Env) (drop xa x))\<rbrakk> \<Longrightarrow> \<exists>xb\<in>{..length (map f (?xs207 s s0 x xa))}. 0 < xb \<and> (0 < xb \<longrightarrow> map (apsnd f \<circ> Pair Env) (drop xa x) = map (Pair Env) (drop xb (map f (?xs207 s s0 x xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 x xa. \<lbrakk>xa \<le> length x; P s; C \<longrightarrow> s0 = s; 0 < xa; rely_cond R s (drop xa (map (Pair Env) x)); rely_cond R (f s) (drop xa (map (\<lambda>x. (Env, f x)) x))\<rbrakk> \<Longrightarrow> \<exists>xb\<in>{..length (?xs207 s s0 x xa)}. 0 < xb \<and> (0 < xb \<longrightarrow> drop xa (map (\<lambda>x. (Env, f x)) x) = drop xb (map (\<lambda>x. (Env, f x)) (?xs207 s s0 x xa))) proof (prove)
goal:
No subgoals! proof (state)
this:
rel_tr_refinement sr P R C (do interference;
modify f
od) (do modify f;
interference
od)

goal:
No subgoals!