theory Prefix_Refinement

lemma prefix_refinement_interference:
  "env_stable AR R sr iosr Q
    \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) \<top>\<top> (\<lambda>t0 t. Q t) AR R interference interference" apply (simp add: interference_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind[where intsr=iosr]) apply (rule prefix_refinement_commit_step) apply (simp add: env_stable_def le_fun_def) apply (erule prefix_refinement_env_steps) apply (simp add: commit_step_def del: put_trace.simps) apply wp apply (simp add: commit_step_def del: put_trace.simps) apply wp apply (simp add: guar_cond_def) apply (clarsimp simp: guar_cond_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>t0. Q) AR R interference interference proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>t0. Q) AR R (do y <- commit_step;
env_steps
od) (do y <- commit_step;
env_steps
od) proof (prove)
goal (3 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) ?P' ?Q' AR R (do y <- commit_step;
env_steps
od) (do y <- commit_step;
env_steps
od)
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ?P' s0 s
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ?Q' t0 t proof (prove)
goal (6 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> prefix_refinement sr iosr iosr ?rvr4 ?P4 ?Q4 AR R commit_step commit_step
 2. \<And>x y. \<lbrakk>env_stable AR R sr iosr Q; ?rvr4 x y\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) AR R env_steps env_steps
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> commit_step -, \<lbrace>?P''4\<rbrace>
 4. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> commit_step -, \<lbrace>?Q''4\<rbrace>
 5. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> (?P4 and ?P'4) s0 s
 6. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (6 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t. iosr s t \<longrightarrow> sr s t \<and> iosr s t
 2. \<And>x y. \<lbrakk>env_stable AR R sr iosr Q; True\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) AR R env_steps env_steps
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> commit_step -, \<lbrace>?P''4\<rbrace>
 4. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> commit_step -, \<lbrace>?Q''4\<rbrace>
 5. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 6. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>env_stable AR R sr iosr Q; True\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) AR R env_steps env_steps
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> commit_step -, \<lbrace>?P''4\<rbrace>
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> commit_step -, \<lbrace>?Q''4\<rbrace>
 4. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> commit_step -, \<lbrace>\<lambda>x. (=)\<rbrace>
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> commit_step -, \<lbrace>\<lambda>y t0 t. t0 = t \<and> Q t0\<rbrace>
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 4. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?P'4\<rbrace>, \<lbrace>AR\<rbrace> do s <- get;
put_trace [(Me, s)]
od -, \<lbrace>\<lambda>x. (=)\<rbrace>
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> commit_step -, \<lbrace>\<lambda>y t0 t. t0 = t \<and> Q t0\<rbrace>
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 4. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (3 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> commit_step -, \<lbrace>\<lambda>y t0 t. t0 = t \<and> Q t0\<rbrace>
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. (\<forall>n. rely_cond AR s0 (drop n [(Me, s)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Me, s)])) \<and> (rely_cond AR s0 [(Me, s)] \<longrightarrow> last_st_tr [(Me, s)] s0 = s))) s0 s
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (3 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<lbrace>?Q'4\<rbrace>, \<lbrace>R\<rbrace> do s <- get;
put_trace [(Me, s)]
od -, \<lbrace>\<lambda>y t0 t. t0 = t \<and> Q t0\<rbrace>
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. (\<forall>n. rely_cond AR s0 (drop n [(Me, s)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Me, s)])) \<and> (rely_cond AR s0 [(Me, s)] \<longrightarrow> last_st_tr [(Me, s)] s0 = s))) s0 s
 3. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (2 subgoals):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. (\<forall>n. rely_cond AR s0 (drop n [(Me, s)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Me, s)])) \<and> (rely_cond AR s0 [(Me, s)] \<longrightarrow> last_st_tr [(Me, s)] s0 = s))) s0 s
 2. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. (\<forall>n. rely_cond R s0 (drop n [(Me, s)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Me, s)])) \<and> (rely_cond R s0 [(Me, s)] \<longrightarrow> last_st_tr [(Me, s)] s0 = s \<and> Q (last_st_tr [(Me, s)] s0)))) t0 t proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr Q \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> True \<longrightarrow> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. (\<forall>n. rely_cond R s0 (drop n [(Me, s)]) \<longrightarrow> guar_cond (\<lambda>_ _. True) s0 (drop n [(Me, s)])) \<and> (rely_cond R s0 [(Me, s)] \<longrightarrow> last_st_tr [(Me, s)] s0 = s \<and> Q (last_st_tr [(Me, s)] s0)))) t0 t proof (prove)
goal:
No subgoals!