kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma rg_fun_app_twp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f' x \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f' $ x \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>"
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f $ x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f' x \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f' $ x \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>) &&& (\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f $ x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>)
theory Trace_RG

lemma case_option_twpE:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> m x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> m' \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. (x = None \<longrightarrow> P' s0 s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s0 s)\<rbrace>,\<lbrace>R\<rbrace> case_option m' m x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (cases x; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> m x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> m' \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (x = None \<longrightarrow> P' s0 s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s0 s)\<rbrace>, \<lbrace>R\<rbrace> case x of None \<Rightarrow> m' | Some x \<Rightarrow> m x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma whenE_throwError_twp:
  "\<lbrace>\<lambda>s0 s. \<not>P \<longrightarrow> Q s0 s\<rbrace>,\<lbrace>R\<rbrace> whenE P (throwError e) \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,-" by (simp add: whenE_def returnOk_def throwError_def return_def validIE_def validI_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. \<not> P \<longrightarrow> Q s0 s\<rbrace>, \<lbrace>R\<rbrace> whenE P (throwError e) \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, -
theory Trace_RG

lemma env_steps_twp[wp]:
  "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s') \<and> Q () s0 s\<rbrace>,\<lbrace>R\<rbrace> env_steps \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (simp add: env_steps_def) apply wp apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) apply (drule rely_cond_rtranclp) apply (clarsimp simp add: last_st_tr_def hd_append) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s') \<and> Q () s0 s\<rbrace>, \<lbrace>R\<rbrace> env_steps \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s') \<and> Q () s0 s\<rbrace>, \<lbrace>R\<rbrace> do s <- get;
xs <- select UNIV;
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s') \<and> Q () s0 s \<Longrightarrow> \<forall>x\<in>UNIV. (\<forall>n. rely_cond R s0 (drop n (map (Pair Env) x)) \<longrightarrow> guar_cond G s0 (drop n (map (Pair Env) x))) \<and> (rely_cond R s0 (map (Pair Env) x) \<longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s x. \<lbrakk>\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s'; Q () s0 s; rely_cond R s0 (map (Pair Env) x)\<rbrakk> \<Longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s x. \<lbrakk>\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s'; Q () s0 s; R\<^sup>*\<^sup>* s0 (last_st_tr (map (Pair Env) x) s0)\<rbrakk> \<Longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma interference_twp[wp]:
  "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrace>,\<lbrace>R\<rbrace> interference \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (simp add: interference_def commit_step_def del: put_trace.simps) apply wp apply clarsimp apply (simp add: drop_Cons nat.split rely_cond_def guar_cond_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrace>, \<lbrace>R\<rbrace> interference \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrace>, \<lbrace>R\<rbrace> do y <- do s <- get;
put_trace [(Me, s)]
od;
env_steps
od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<Longrightarrow> (\<forall>n. rely_cond R s0 (drop n [(Me, s)]) \<longrightarrow> guar_cond G s0 (drop n [(Me, s)])) \<and> (rely_cond R s0 [(Me, s)] \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* (last_st_tr [(Me, s)] s0) s' \<longrightarrow> Q () s' s') \<and> Q () (last_st_tr [(Me, s)] s0) s) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s n. \<lbrakk>\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s'; G s0 s; rely_cond R s0 (drop n [(Me, s)])\<rbrakk> \<Longrightarrow> guar_cond G s0 (drop n [(Me, s)]) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma Await_sync_twp:
  "\<lbrace>\<lambda>s0 s. s = s0 \<and> (\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x)\<rbrace>,\<lbrace>R\<rbrace> Await c \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (simp add: Await_def split_def) apply wp apply clarsimp apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) apply (drule rely_cond_rtranclp) apply (simp add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. s = s0 \<and> (\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x)\<rbrace>, \<lbrace>R\<rbrace> Await c \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. s = s0 \<and> (\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x)\<rbrace>, \<lbrace>R\<rbrace> do s <- get;
xs <- select {xs. c (last_st_tr (map (Pair Env) xs) s)};
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. s = s0 \<and> (\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x) \<Longrightarrow> \<forall>x\<in>{xs. c (last_st_tr (map (Pair Env) xs) s)}. (\<forall>n. rely_cond R s0 (drop n (map (Pair Env) x)) \<longrightarrow> guar_cond G s0 (drop n (map (Pair Env) x))) \<and> (rely_cond R s0 (map (Pair Env) x) \<longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 x. \<lbrakk>\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x; c (last_st_tr (map (Pair Env) x) s0)\<rbrakk> \<Longrightarrow> (\<forall>n. rely_cond R s0 (drop n (map (Pair Env) x)) \<longrightarrow> guar_cond G s0 (drop n (map (Pair Env) x))) \<and> (rely_cond R s0 (map (Pair Env) x) \<longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s0)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 x. \<lbrakk>\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x; c (last_st_tr (map (Pair Env) x) s0); rely_cond R s0 (map (Pair Env) x)\<rbrakk> \<Longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s0) proof (prove)
goal (1 subgoal):
 1. \<And>s0 x. \<lbrakk>\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x; c (last_st_tr (map (Pair Env) x) s0); R\<^sup>*\<^sup>* s0 (last_st_tr (map (Pair Env) x) s0)\<rbrakk> \<Longrightarrow> Q () (last_st_tr (map (Pair Env) x) s0) (last_st_tr (map (Pair Env) x) s0) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma validI_is_triple:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>
   = triple_judgement (\<lambda>(s0,s). prefix_closed f \<longrightarrow> P s0 s) f
                      (\<lambda>(s0,s) f. prefix_closed f \<and> (\<forall>tr res. (tr, res) \<in> rely f R s0 s
                          \<longrightarrow> guar_cond G s0 tr
                              \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')))" apply (simp add: triple_judgement_def validI_def ) apply (cases "prefix_closed f"; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> = triple_judgement (\<lambda>(s0, s). prefix_closed f \<longrightarrow> P s0 s) f (\<lambda>(s0, s) f. prefix_closed f \<and> (\<forall>tr res. (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))) proof (prove)
goal (1 subgoal):
 1. (prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))) = (\<forall>a b. (prefix_closed f \<longrightarrow> P a b) \<longrightarrow> prefix_closed f \<and> (\<forall>tr res. (tr, res) \<in> rely f R a b \<longrightarrow> guar_cond G a tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr a) s'))) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma validIE_is_triple:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>
   = triple_judgement (\<lambda>(s0,s). prefix_closed f \<longrightarrow> P s0 s) f
                      (\<lambda>(s0,s) f. prefix_closed f \<and> (\<forall>tr res. (tr, res) \<in> rely f R s0 s
                          \<longrightarrow> guar_cond G s0 tr
                              \<and> (\<forall>rv s'. res = Result (rv, s')
                                   \<longrightarrow> (case rv of Inr b \<Rightarrow> Q b (last_st_tr tr s0) s'
                                                 | Inl a \<Rightarrow> E a (last_st_tr tr s0) s'))))" by (fastforce simp: validIE_def2 triple_judgement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> = triple_judgement (\<lambda>(s0, s). prefix_closed f \<longrightarrow> P s0 s) f (\<lambda>(s0, s) f. prefix_closed f \<and> (\<forall>tr res. (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl a \<Rightarrow> E a (last_st_tr tr s0) s' | Inr b \<Rightarrow> Q b (last_st_tr tr s0) s'))))
theory Trace_RG

lemma rg_post_eq:
  "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q = Q'; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_post_eqE1:
  "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q = Q'; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_post_eqE2:
  "\<lbrakk> E = E'; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E = E'; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma pred_conj_apply_elim':
  "(\<lambda>rv. Q rv and Q' rv) = (\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s)" by (simp add: pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv. Q rv and Q' rv) = (\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s)
theory Trace_RG

lemma pred_conj_conj_elim':
  "(\<lambda>rv s0 s. (Q rv and Q' rv) s0 s \<and> Q'' rv s0 s) = (\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s \<and> Q'' rv s0 s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s0 s. (Q rv and Q' rv) s0 s \<and> Q'' rv s0 s) = (\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s \<and> Q'' rv s0 s)
theory Trace_RG

lemma conj_assoc_apply':
  "(\<lambda>rv s0 s. (Q rv s0 s \<and> Q' rv s0 s) \<and> Q'' rv s0 s) = (\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s \<and> Q'' rv s0 s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s0 s. (Q rv s0 s \<and> Q' rv s0 s) \<and> Q'' rv s0 s) = (\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s \<and> Q'' rv s0 s)
theory Trace_RG

lemma all_elim':
  "(\<lambda>rv s0 s. \<forall>x. P rv s0 s) = P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s0 s. \<forall>x. P rv s0 s) = P
theory Trace_RG

lemma all_conj_elim':
  "(\<lambda>rv s0 s. (\<forall>x. P rv s0 s) \<and> Q rv s0 s) = (\<lambda>rv s0 s. P rv s0 s \<and> Q rv s0 s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s0 s. (\<forall>x. P rv s0 s) \<and> Q rv s0 s) = (\<lambda>rv s0 s. P rv s0 s \<and> Q rv s0 s)
theory Trace_RG

lemma if_apply_reductI:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> If P' (f x) (g x) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> If P' f g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (cases P'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> if P' then f x else g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> (if P' then f else g) x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma if_apply_reductIE:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> If P' (f x) (g x) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> If P' f g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (cases P'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> if P' then f x else g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> (if P' then f else g) x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_elim_pred_conj:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q rv and Q' rv\<rbrace>" by (unfold pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. Q rv and Q' rv\<rbrace>
theory Trace_RG

lemma rg_elim_pred_conjE2:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. E rv s0 s \<and> E' rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. E rv and E' rv\<rbrace>" by (unfold pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s0 s. E rv s0 s \<and> E' rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. E rv and E' rv\<rbrace>
theory Trace_RG

lemma rg_pre_cases:
  "\<lbrakk> \<lbrace>\<lambda>s0 s. C s0 s \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s0 s. \<not>C s0 s \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding validI_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s0 s. C s0 s \<and> P s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s0 s. \<not> C s0 s \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f \<and> (\<forall>s0 s tr res. (C s0 s \<and> P s0 s) \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')); prefix_closed f \<and> (\<forall>s0 s tr res. (\<not> C s0 s \<and> P' s0 s) \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. (P and P') s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_vcg_mp:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r s0 s. Q r s0 s \<longrightarrow> Q' r s0 s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>" by (auto simp: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r s0 s. Q r s0 s \<longrightarrow> Q' r s0 s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>
theory Trace_RG

lemma rg_add_post:
  "\<lbrakk> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q' rv s0 s \<longrightarrow> Q rv s0 s\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding validI_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q' rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f \<and> (\<forall>s0 s tr res. P' s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr tr s0) s')); \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s; prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q' rv (last_st_tr tr s0) s' \<longrightarrow> Q rv (last_st_tr tr s0) s'))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_gen_asmE:
  "\<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<not> P \<Longrightarrow> prefix_closed f\<rbrakk>
   \<Longrightarrow> \<lbrace>P' and (\<lambda>_ _. P)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: validIE_def validI_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<not> P \<Longrightarrow> prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>P' and (\<lambda>_ _. P)\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_list_case:
  "\<lbrakk> \<lbrace>P1\<rbrace>,\<lbrace>R\<rbrace> f f1 \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>y ys. xs = y#ys \<Longrightarrow> \<lbrace>P2 y ys\<rbrace>,\<lbrace>R\<rbrace> f (f2 y ys) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>case xs of [] \<Rightarrow> P1 | y#ys \<Rightarrow> P2 y ys\<rbrace>,\<lbrace>R\<rbrace> f (case xs of [] \<Rightarrow> f1 | y#ys \<Rightarrow> f2 y ys) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (cases xs; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P1\<rbrace>, \<lbrace>R\<rbrace> f f1 \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P2 y ys\<rbrace>, \<lbrace>R\<rbrace> f (f2 y ys) \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>case xs of [] \<Rightarrow> P1 | y # ys \<Rightarrow> P2 y ys\<rbrace>, \<lbrace>R\<rbrace> f (case xs of [] \<Rightarrow> f1 | y # ys \<Rightarrow> f2 y ys) \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>