theory Atomicity_Lib

lemma rel_tr_refinement_rev_comm_repeat[simplified K_bind_def]:
  "equivp sr
    \<Longrightarrow> rel_tr_refinement sr P R C (do x \<leftarrow> g; f; return x od) (do f; g od)
    \<Longrightarrow> not_env_steps_first f \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t)
    \<Longrightarrow> \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>,\<lbrace>R\<rbrace> f
        \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>
    \<Longrightarrow> rel_tr_refinement sr P R C
        (do x \<leftarrow> g; repeat f; return x od)
        (do repeat f; g od)" apply (simp add: repeat_def select_early bind_assoc) apply (rule rel_tr_refinement_bind_right_general[rule_format]) apply (metis equivpE) apply (erule(1) rel_tr_refinement_rev_comm_repeat_n, simp+) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
f;
return x
od) (do f;
g
od); not_env_steps_first f \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- g;
repeat f;
return x
od) (do repeat f;
g
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- select UNIV;
xa <- g;
y <- repeat_n x f;
return xa
od) (do x <- select UNIV;
y <- repeat_n x f;
g
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> reflp sr
 2. \<And>x. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> rel_tr_refinement sr ?Q3 R ?C'3 (do xa <- g;
y <- repeat_n x f;
return xa
od) (do y <- repeat_n x f;
g
od)
 3. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>\<lambda>_ s0 s. (?C'3 \<longrightarrow> s0 = s) \<and> ?Q3 s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> rel_tr_refinement sr ?Q3 R ?C'3 (do xa <- g;
y <- repeat_n x f;
return xa
od) (do y <- repeat_n x f;
g
od)
 2. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>\<lambda>_ s0 s. (?C'3 \<longrightarrow> s0 = s) \<and> ?Q3 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do x <- g;
y <- f;
return x
od) (do y <- f;
g
od); not_env_steps_first f \<or> (\<forall>s s'. sr s s' \<longrightarrow> (\<forall>t. R s t = R s' t)); \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>, \<lbrace>R\<rbrace> select UNIV -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace> proof (prove)
goal:
No subgoals!