theory Atomicity_Lib

lemma rshuttle_modify_interference[simplified K_bind_def]:
  assumes sr: "\<forall>s. P s \<longrightarrow> sr (f s) s"
    and P_stable: "\<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> P t"
    and R: "\<forall>s0 s. R (f s0) s \<longrightarrow> P s0 \<longrightarrow> (\<exists>s_pre. s = f s_pre \<and> R s0 s_pre)"
  shows
  "rel_tr_refinement sr P R C
        (do modify f; interference od)
        (do interference; modify f od)" proof - have last_st_tr: "\<And>s ss. last_st_tr (map (Pair Env \<circ> f) ss) (f s)
        = f (last_st_tr (map (Pair Env) ss) s)" by (simp add: last_st_tr_def hd_append hd_map) { fix s ss s' have rely_cond_P_stable[rule_format]:
    "P s \<longrightarrow> rely_cond R s (map (Pair Env) ss)
           \<longrightarrow> s' \<in> set (ss @ [s]) \<longrightarrow> P s'" apply (induct ss arbitrary: s' rule: list.induct) apply simp apply clarsimp apply (clarsimp simp: rely_cond_Cons_eq P_stable) apply (erule P_stable[rule_format, rotated]) apply (case_tac x2; simp add: last_st_tr_in_set) done } note rely_cond_P_stable = this have rely_cond_ex:
    "\<And>s ss. rely_cond R (f s) (map (Pair Env) ss) \<longrightarrow> P s
        \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> ss = map f ss')" apply (induct_tac ss) apply simp apply (clarsimp simp: rely_cond_Cons_eq last_st_tr) apply (frule R[rule_format], erule(1) rely_cond_P_stable, rule last_st_tr_in_set) apply (strengthen exI[where x="x # xs" for x xs]) apply (simp add: rely_cond_Cons_eq) apply blast 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 (clarsimp simp: put_trace_eq_drop) apply (split if_split_asm) apply (clarsimp simp: image_Union rely_cond_append rely_cond_Cons_eq) apply (drule(1) rely_cond_ex[rule_format], clarsimp) apply (strengthen exI[where x="map (Pair Env) ss @ [(Me, x)]" for ss x], simp) apply (simp add: rely_cond_append rely_cond_Cons) apply (strengthen list_all2_appendI, simp) apply (simp add: list_all2_map1 list_all2_map2) apply (intro exI, strengthen sr[rule_format] list_all2_same[THEN iffD2]) apply (simp add: sr last_st_tr rely_cond_P_stable) apply blast apply (clarsimp simp: image_Union rely_cond_append rely_cond_Cons_eq) apply (simp add: drop_map) apply (drule(1) rely_cond_ex[rule_format], clarsimp) apply (strengthen exI[where x="(map (Pair Env) ss @ [(Me, x)])" for n ss x], simp) apply (strengthen list_all2_appendI, simp) apply (simp add: list_all2_map1 list_all2_map2) apply (intro exI, strengthen sr[rule_format] list_all2_same[THEN iffD2]) apply (simp add: sr last_st_tr rely_cond_append rely_cond_Cons_eq rely_cond_P_stable) apply (strengthen bexI[where x=1], simp) apply (strengthen exI[where x="x # xs" for x xs], simp) apply blast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (state)
goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (prove)
goal (1 subgoal):
 1. \<And>s ss. last_st_tr (map (Pair Env \<circ> f) ss) (f s) = f (last_st_tr (map (Pair Env) ss) s) proof (state)
this:
last_st_tr (map (Pair Env \<circ> f) ?ss) (f ?s) = f (last_st_tr (map (Pair Env) ?ss) ?s)

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (state)
this:
last_st_tr (map (Pair Env \<circ> f) ?ss) (f ?s) = f (last_st_tr (map (Pair Env) ?ss) ?s)

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (state)
goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (prove)
goal (1 subgoal):
 1. P s \<longrightarrow> rely_cond R s (map (Pair Env) ss) \<longrightarrow> s' \<in> set (ss @ [s]) \<longrightarrow> P s' proof (prove)
goal (2 subgoals):
 1. \<And>s'. P s \<longrightarrow> rely_cond R s (map (Pair Env) []) \<longrightarrow> s' \<in> set ([] @ [s]) \<longrightarrow> P s'
 2. \<And>x1 x2 s'. (\<And>s'. P s \<longrightarrow> rely_cond R s (map (Pair Env) x2) \<longrightarrow> s' \<in> set (x2 @ [s]) \<longrightarrow> P s') \<Longrightarrow> P s \<longrightarrow> rely_cond R s (map (Pair Env) (x1 # x2)) \<longrightarrow> s' \<in> set ((x1 # x2) @ [s]) \<longrightarrow> P s' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 s'. (\<And>s'. P s \<longrightarrow> rely_cond R s (map (Pair Env) x2) \<longrightarrow> s' \<in> set (x2 @ [s]) \<longrightarrow> P s') \<Longrightarrow> P s \<longrightarrow> rely_cond R s (map (Pair Env) (x1 # x2)) \<longrightarrow> s' \<in> set ((x1 # x2) @ [s]) \<longrightarrow> P s' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 s'. \<lbrakk>\<And>s'. rely_cond R s (map (Pair Env) x2) \<longrightarrow> s' \<in> set x2 \<longrightarrow> P s'; P s; rely_cond R s ((Env, x1) # map (Pair Env) x2)\<rbrakk> \<Longrightarrow> (s' = x1 \<longrightarrow> P x1) \<and> (s' \<in> set x2 \<longrightarrow> P s') proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>s'. s' \<in> set x2 \<longrightarrow> P s'; P s; rely_cond R s (map (Pair Env) x2); R (last_st_tr (map (Pair Env) x2) s) x1\<rbrakk> \<Longrightarrow> P x1 proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>s'. s' \<in> set x2 \<longrightarrow> P s'; P s; rely_cond R s (map (Pair Env) x2)\<rbrakk> \<Longrightarrow> P (last_st_tr (map (Pair Env) x2) s) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>P s; rely_cond R s (map (Pair Env) ss); s' \<in> set (ss @ [s])\<rbrakk> \<Longrightarrow> P s'

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (state)
this:
\<lbrakk>P ?s2; rely_cond R ?s2 (map (Pair Env) ?ss2); ?s'2 \<in> set (?ss2 @ [?s2])\<rbrakk> \<Longrightarrow> P ?s'2

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (state)
this:
\<lbrakk>P ?s2; rely_cond R ?s2 (map (Pair Env) ?ss2); ?s'2 \<in> set (?ss2 @ [?s2])\<rbrakk> \<Longrightarrow> P ?s'2

goal (1 subgoal):
 1. rel_tr_refinement sr P R C (do modify f;
interference
od) (do interference;
modify f
od) proof (prove)
goal (1 subgoal):
 1. \<And>s ss. rely_cond R (f s) (map (Pair Env) ss) \<longrightarrow> P s \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> ss = map f ss') proof (prove)
goal (2 subgoals):
 1. \<And>s ss. rely_cond R (f s) (map (Pair Env) []) \<longrightarrow> P s \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> [] = map f ss')
 2. \<And>s ss a list. rely_cond R (f s) (map (Pair Env) list) \<longrightarrow> P s \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> list = map f ss') \<Longrightarrow> rely_cond R (f s) (map (Pair Env) (a # list)) \<longrightarrow> P s \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> a # list = map f ss') proof (prove)
goal (1 subgoal):
 1. \<And>s ss a list. rely_cond R (f s) (map (Pair Env) list) \<longrightarrow> P s \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> list = map f ss') \<Longrightarrow> rely_cond R (f s) (map (Pair Env) (a # list)) \<longrightarrow> P s \<longrightarrow> (\<exists>ss'. rely_cond R s (map (Pair Env) ss') \<and> a # list = map f ss') proof (prove)
goal (1 subgoal):
 1. \<And>s a ss'. \<lbrakk>rely_cond R (f s) (map (Pair Env \<circ> f) ss'); R (f (last_st_tr (map (Pair Env) ss') s)) a; P s; rely_cond R s (map (Pair Env) ss')\<rbrakk> \<Longrightarrow> \<exists>ss'a. rely_cond R s (map (Pair Env) ss'a) \<and> a # map f ss' = map f ss'a proof (prove)
goal (1 subgoal):
 1. \<And>s a ss'. \<lbrakk>rely_cond R (f s) (map (Pair Env \<circ> f) ss'); R (f (last_st_tr (map (Pair Env) ss') s)) a; P s; rely_cond R s (map (Pair Env) ss'); \<exists>s_pre. a = f s_pre \<and> R (last_st_tr (map (Pair Env) ss') s) s_pre\<rbrakk> \<Longrightarrow> \<exists>ss'a. rely_cond R s (map (Pair Env) ss'a) \<and> a # map f ss' = map f ss'a proof (prove)
goal (1 subgoal):
 1. \<And>s a ss'. \<lbrakk>rely_cond R (f s) (map (Pair Env \<circ> f) ss'); R (f (last_st_tr (map (Pair Env) ss') s)) a; P s; rely_cond R s (map (Pair Env) ss'); \<exists>s_pre. a = f s_pre \<and> R (last_st_tr (map (Pair Env) ss') s) s_pre\<rbrakk> \<Longrightarrow> \<exists>xs x. rely_cond R s (map (Pair Env) (x # xs)) \<and> a # map f ss' = map f (x # xs) proof (prove)
goal (1 subgoal):
 1. \<And>s a ss'. \<lbrakk>rely_cond R (f s) (map (Pair Env \<circ> f) ss'); R (f (last_st_tr (map (Pair Env) ss') s)) a; P s; rely_cond R s (map (Pair Env) ss'); \<exists>s_pre. a = f s_pre \<and> R (last_st_tr (map (Pair Env) ss') s) s_pre\<rbrakk> \<Longrightarrow> \<exists>xs. rely_cond R s (map (Pair Env) xs) \<and> (\<exists>x. R (last_st_tr (map (Pair Env) xs) s) x \<and> a = f x \<and> map f ss' = map f xs) proof (prove)
goal:
No subgoals! proof (state)
this:
rely_cond R (f ?s) (map (Pair Env) ?ss) \<longrightarrow> P ?s \<longrightarrow> (\<exists>ss'. rely_cond R ?s (map (Pair Env) ss') \<and> ?ss = map f ss')

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

goal:
No subgoals!