theory Atomicity_Lib

lemma prefix_refinement_i_modify_split:
  "adjust_tr_relation tr_r sr
    \<Longrightarrow> \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t)
    \<Longrightarrow> \<forall>s. tr_r s (g s)
    \<Longrightarrow> \<forall>s t. R s t \<longrightarrow> R (g s) (g t)
    \<Longrightarrow> not_env_steps_first b
    \<Longrightarrow> prefix_refinement sr intsr osr rvr' P' Q' AR R
        d (do x \<leftarrow> interferences; b od)
    \<Longrightarrow> prefix_refinement sr isr osr rvr' (\<lambda>s0 s. P s \<and> P' s0 (f s)) (\<lambda>s0 s. Q s \<and> Q' s0 (g s)) AR R
        (do z \<leftarrow> modify f; d od)
        (do x \<leftarrow> interferences; y \<leftarrow> modify g; b od)" apply (clarsimp simp: adjust_tr_relation_def) apply (rule prefix_refinement_weaken_pre) apply (rule pfx_refinement_use_rel_tr_refinement[where tr_r=tr_r and Q=\<top>]) apply (rule shuttle_modify_interferences, simp+) apply (rule prefix_refinement_bind[where intsr=intsr]) apply (rule prefix_refinement_modify, assumption) apply assumption apply wp+ apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>adjust_tr_relation tr_r sr; \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od)\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr' (\<lambda>s0 s. P s \<and> P' s0 (f s)) (\<lambda>s0 s. Q s \<and> Q' s0 (g s)) AR R (do z <- modify f;
d
od) (do x <- interferences;
y <- modify g;
b
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr' (\<lambda>s0 s. P s \<and> P' s0 (f s)) (\<lambda>s0 s. Q s \<and> Q' s0 (g s)) AR R (do z <- modify f;
d
od) (do x <- interferences;
y <- modify g;
b
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr' ?P'1 ?Q'1 AR R (do z <- modify f;
d
od) (do x <- interferences;
y <- modify g;
b
od)
 2. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> ?P'1 s0 s
 3. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ?Q'1 t0 t proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> rel_tr_refinement tr_r (\<lambda>_. True) R False (do x <- interferences;
y <- modify g;
b
od) ?g'5
 2. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'
 3. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr' ?P'1 ?Q'5 AR R (do z <- modify f;
d
od) ?g'5
 4. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> ?P'1 s0 s
 5. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and ?Q'5 t0) t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr' ?P'1 ?Q'5 AR R (do z <- modify f;
d
od) (do x <- modify g;
y <- interferences;
b
od)
 2. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> ?P'1 s0 s
 3. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and ?Q'5 t0) t proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr intsr ?rvr15 ?P15 ?Q15 AR R (modify f) (modify g)
 2. \<And>x y. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; ?rvr15 x y\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr osr rvr' (?P''15 x) (?Q''15 y) AR R d (do y <- interferences;
b
od)
 3. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<lbrace>?P'15\<rbrace>, \<lbrace>AR\<rbrace> modify f -, \<lbrace>?P''15\<rbrace>
 4. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15\<rbrace>, \<lbrace>R\<rbrace> modify g -, \<lbrace>?Q''15\<rbrace>
 5. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> (?P15 and ?P'15) s0 s
 6. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and (?Q15 and ?Q'15) t0) t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; True\<rbrakk> \<Longrightarrow> prefix_refinement sr intsr osr rvr' (?P''15 x) (?Q''15 y) AR R d (do y <- interferences;
b
od)
 2. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<lbrace>?P'15\<rbrace>, \<lbrace>AR\<rbrace> modify f -, \<lbrace>?P''15\<rbrace>
 3. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15\<rbrace>, \<lbrace>R\<rbrace> modify g -, \<lbrace>?Q''15\<rbrace>
 4. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> ((\<lambda>_. P) and ?P'15) s0 s
 5. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. Q) and ?Q'15) t0) t proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<lbrace>?P'15\<rbrace>, \<lbrace>AR\<rbrace> modify f -, \<lbrace>\<lambda>x. P'\<rbrace>
 2. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15\<rbrace>, \<lbrace>R\<rbrace> modify g -, \<lbrace>\<lambda>y. Q'\<rbrace>
 3. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> ((\<lambda>_. P) and ?P'15) s0 s
 4. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. Q) and ?Q'15) t0) t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s s0. P s \<and> P' s0 (f s) \<longrightarrow> ((\<lambda>_. P) and (\<lambda>s0 s. P' s0 (f s))) s0 s
 2. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. Q) and (\<lambda>s0 s. Q' s0 (g s))) t0) t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t); \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b; prefix_refinement sr intsr osr rvr' P' Q' AR R d (do x <- interferences;
b
od); equivp tr_r; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s \<and> P' s0 (f s) \<longrightarrow> Q t \<and> Q' t0 (g t) \<longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. Q) and (\<lambda>s0 s. Q' s0 (g s))) t0) t proof (prove)
goal:
No subgoals!