theory Atomicity_Lib

lemma rel_tr_refinement_comm_repeat_n[simplified K_bind_def]:
  "equivp sr
    \<Longrightarrow> rel_tr_refinement sr P R C (do f; g od) (do x \<leftarrow> g; f; return x 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 repeat_n n f; g od)
        (do x \<leftarrow> g; repeat_n n f; return x od)" apply (induct n) apply simp apply (rule rel_tr_refinement_refl) apply (metis equivpE) apply (simp add: bind_assoc repeat_n_plus[where m=1, simplified]) apply (rule rel_tr_refinement_trans) apply (metis equivpE) apply (rule rel_tr_refinement_bind_right_general[rule_format]) apply (metis equivpE) apply assumption apply (wpsimp wp: repeat_n_validI) apply (drule_tac h="\<lambda>x. do f; return x od"
      in rel_tr_refinement_bind_left_general[rotated 2]) apply (metis equivpE) apply (auto intro!: not_env_steps_first_all)[1] apply (simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n n f;
g
od) (do x <- g;
repeat_n n f;
return x
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n 0 f;
g
od) (do x <- g;
repeat_n 0 f;
return x
od)
 2. \<And>n. \<lbrakk>\<lbrakk>equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n n f;
g
od) (do x <- g;
repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n (Suc n) f;
g
od) (do x <- g;
repeat_n (Suc n) f;
return x
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 g g
 2. \<And>n. \<lbrakk>\<lbrakk>equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n n f;
g
od) (do x <- g;
repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n (Suc n) f;
g
od) (do x <- g;
repeat_n (Suc n) f;
return x
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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>n. \<lbrakk>\<lbrakk>equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n n f;
g
od) (do x <- g;
repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n (Suc n) f;
g
od) (do x <- g;
repeat_n (Suc n) f;
return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n n f;
g
od) (do x <- g;
repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do f;
g
od) (do x <- g;
f;
return x
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 repeat_n (Suc n) f;
g
od) (do x <- g;
repeat_n (Suc n) f;
return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 <- repeat_n n f;
y <- f;
g
od) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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> transp sr
 2. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 <- repeat_n n f;
y <- f;
g
od) (?g9 n)
 3. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 (?g9 n) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 <- repeat_n n f;
y <- f;
g
od) (?g9 n)
 2. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 (?g9 n) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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>n x. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 (?Q16 n) R (?C'16 n) (do y <- f;
g
od) (?h16 n x)
 3. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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> repeat_n n f -, \<lbrace>\<lambda>_ s0 s. (?C'16 n \<longrightarrow> s0 = s) \<and> ?Q16 n s\<rbrace>
 4. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 (repeat_n n f >>= ?h16 n) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (3 subgoals):
 1. \<And>n x. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 (?Q16 n) R (?C'16 n) (do y <- f;
g
od) (?h16 n x)
 2. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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> repeat_n n f -, \<lbrace>\<lambda>_ s0 s. (?C'16 n \<longrightarrow> s0 = s) \<and> ?Q16 n s\<rbrace>
 3. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 (repeat_n n f >>= ?h16 n) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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> repeat_n n f -, \<lbrace>\<lambda>_ s0 s. (C \<longrightarrow> s0 = s) \<and> P s\<rbrace>
 2. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 <- repeat_n n f;
x <- g;
y <- f;
return x
od) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>rel_tr_refinement sr P R C (do y <- repeat_n n f;
g
od) (do x <- g;
y <- repeat_n n f;
return x
od); equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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 <- repeat_n n f;
x <- g;
y <- f;
return x
od) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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>n. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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> (\<forall>x. not_env_steps_first (do f;
return x
od)) \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t)
 3. \<And>n. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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>; rel_tr_refinement sr P R C (do x <- do y <- repeat_n n f;
g
od;
f;
return x
od) (do x <- do x <- g;
y <- repeat_n n f;
return x
od;
f;
return x
od)\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- repeat_n n f;
x <- g;
y <- f;
return x
od) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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> (\<forall>x. not_env_steps_first (do f;
return x
od)) \<or> (\<forall>s s' t. sr s s' \<longrightarrow> R s t = R s' t)
 2. \<And>n. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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>; rel_tr_refinement sr P R C (do x <- do y <- repeat_n n f;
g
od;
f;
return x
od) (do x <- do x <- g;
y <- repeat_n n f;
return x
od;
f;
return x
od)\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- repeat_n n f;
x <- g;
y <- f;
return x
od) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>equivp sr; rel_tr_refinement sr P R C (do y <- f;
g
od) (do x <- g;
y <- f;
return x
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>; rel_tr_refinement sr P R C (do x <- do y <- repeat_n n f;
g
od;
f;
return x
od) (do x <- do x <- g;
y <- repeat_n n f;
return x
od;
f;
return x
od)\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C (do x <- repeat_n n f;
x <- g;
y <- f;
return x
od) (do x <- g;
xa <- repeat_n n f;
y <- f;
return x
od) proof (prove)
goal:
No subgoals!