theory Atomicity_Lib

lemma shuttle_modify_interferences[simplified K_bind_def]:
  "equivp sr \<Longrightarrow> \<forall>s. sr s (f s) \<Longrightarrow> \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t)
    \<Longrightarrow> not_env_steps_first g
    \<Longrightarrow> \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t
    \<Longrightarrow> rel_tr_refinement sr P R C
        (do x \<leftarrow> interferences; modify f; g od) (do x \<leftarrow> modify f; interferences; g od)" apply (simp only: bind_assoc[symmetric]) apply (rule rel_tr_refinement_bind_left_general) apply (metis equivpE) apply simp apply (rule rel_tr_refinement_drop_C) apply (rule rel_tr_refinement_comm_repeat[where g="modify f", simplified]) apply assumption apply (rule shuttle_modify_interference, (simp add: r_into_rtranclp)+) apply (simp add: not_env_steps_first_interference) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- interferences;
modify f;
g
od) (do x <- modify f;
interferences;
g
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do do x <- interferences;
modify f
od;
g
od) (do do x <- modify f;
interferences
od;
g
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> reflp sr
 2. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> (\<forall>x. not_env_steps_first (K_bind g x)) \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t)
 3. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- interferences;
modify f
od) (do x <- modify f;
interferences
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> (\<forall>x. not_env_steps_first (K_bind g x)) \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t)
 2. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- interferences;
modify f
od) (do x <- modify f;
interferences
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- interferences;
modify f
od) (do x <- modify f;
interferences
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R False (do x <- interferences;
modify f
od) (do x <- modify f;
interferences
od) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> equivp sr
 2. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R False (do x <- interference;
modify f
od) (do x <- modify f;
interference
od)
 3. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> not_env_steps_first interference \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t))
 4. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> interference -, \<lbrace>\<lambda>_ s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R False (do x <- interference;
modify f
od) (do x <- modify f;
interference
od)
 2. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> not_env_steps_first interference \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t))
 3. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> interference -, \<lbrace>\<lambda>_ s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s. P s \<longrightarrow> (\<forall>t. R s t \<longrightarrow> R (f s) (f t)); not_env_steps_first g; \<forall>s. P s \<longrightarrow> (\<forall>t. R\<^sup>*\<^sup>* s t \<longrightarrow> P t)\<rbrakk> \<Longrightarrow> not_env_steps_first interference \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t))
 2. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> interference -, \<lbrace>\<lambda>_ s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; \<forall>s. sr s (f s); \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> R (f s) (f t); not_env_steps_first g; \<forall>s t. P s \<longrightarrow> R\<^sup>*\<^sup>* s t \<longrightarrow> P t\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> interference -, \<lbrace>\<lambda>_ s0 s. (False \<longrightarrow> s0 = s) \<and> P s\<rbrace> proof (prove)
goal:
No subgoals!