kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_Prefix_Closed

lemma prefix_closed_filterM[prefix_closed_cond]:
  "(\<And>m. m \<in> set ms \<Longrightarrow> prefix_closed (P m)) \<Longrightarrow> prefix_closed (filterM P ms)" by (induct ms; wpsimp wp: prefix_closed_terminal split_del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m \<in> set ms \<Longrightarrow> prefix_closed (P m)) \<Longrightarrow> prefix_closed (filterM P ms)
theory Trace_Prefix_Closed

lemma prefix_closed_zipWithM_x[prefix_closed_cond]:
  "(\<And>x y. prefix_closed (f x y)) \<Longrightarrow> prefix_closed (zipWithM_x f xs ys)" unfolding zipWithM_x_def zipWith_def by (fastforce intro: prefix_closed_sequence_x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (f x y)) \<Longrightarrow> prefix_closed (zipWithM_x f xs ys) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (f x y)) \<Longrightarrow> prefix_closed (sequence_x (map2 f xs ys))
theory Trace_Prefix_Closed

lemma prefix_closed_zipWithM[prefix_closed_cond]:
  "(\<And>x y. prefix_closed (f x y)) \<Longrightarrow> prefix_closed (zipWithM f xs ys)" unfolding zipWithM_def zipWith_def by (fastforce intro: prefix_closed_sequence)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (f x y)) \<Longrightarrow> prefix_closed (zipWithM f xs ys) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (f x y)) \<Longrightarrow> prefix_closed (sequence (map2 f xs ys))
theory Trace_Prefix_Closed

lemma prefix_closed_foldM[prefix_closed_cond]:
  "(\<And>x y. prefix_closed (m x y)) \<Longrightarrow> prefix_closed (foldM m xs a)" unfolding foldM_def by (induct xs; wpsimp wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (m x y)) \<Longrightarrow> prefix_closed (foldM m xs a) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (m x y)) \<Longrightarrow> prefix_closed (foldr (\<lambda>p q. q >>= m p) xs (return a))
theory Trace_Prefix_Closed

lemma prefix_closed_foldME[prefix_closed_cond]:
  "(\<And>x y. prefix_closed (m x y)) \<Longrightarrow> prefix_closed (foldME m a xs)" unfolding foldME_def by (induct xs; wpsimp wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (m x y)) \<Longrightarrow> prefix_closed (foldME m a xs) proof (prove)
goal (1 subgoal):
 1. (\<And>x y. prefix_closed (m x y)) \<Longrightarrow> prefix_closed (foldr (\<lambda>p q. q >>=E swp m p) xs (returnOk a))
theory Trace_Prefix_Closed

lemma prefix_closed_maybeM[prefix_closed_cond]:
  "\<forall>x. prefix_closed (f x) \<Longrightarrow> prefix_closed (maybeM f t)" unfolding maybeM_def by (fastforce intro: prefix_closed_terminal split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. prefix_closed (f x) \<Longrightarrow> prefix_closed (maybeM f t) proof (prove)
goal (1 subgoal):
 1. \<forall>x. prefix_closed (f x) \<Longrightarrow> prefix_closed (case t of None \<Rightarrow> return () | Some x \<Rightarrow> f x)
theory Trace_Prefix_Closed

lemma prefix_closed_notM[prefix_closed_cond]:
  "prefix_closed A \<Longrightarrow> prefix_closed (notM A)" unfolding notM_def by (wpsimp wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed A \<Longrightarrow> prefix_closed (notM A) proof (prove)
goal (1 subgoal):
 1. prefix_closed A \<Longrightarrow> prefix_closed (do c <- A;
return (\<not> c)
od)
theory Trace_Prefix_Closed

lemma prefix_closed_ifM[prefix_closed_cond]:
  "\<lbrakk> prefix_closed P; prefix_closed a; prefix_closed b \<rbrakk> \<Longrightarrow> prefix_closed (ifM P a b)" unfolding ifM_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed P; prefix_closed a; prefix_closed b\<rbrakk> \<Longrightarrow> prefix_closed (ifM P a b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed P; prefix_closed a; prefix_closed b\<rbrakk> \<Longrightarrow> prefix_closed (do c <- P;
if c then a else b
od)
theory Trace_Prefix_Closed

lemma prefix_closed_ifME[prefix_closed_cond]:
  "\<lbrakk> prefix_closed P; prefix_closed a; prefix_closed b \<rbrakk> \<Longrightarrow> prefix_closed (ifME P a b)" unfolding ifME_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed P; prefix_closed a; prefix_closed b\<rbrakk> \<Longrightarrow> prefix_closed (ifME P a b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed P; prefix_closed a; prefix_closed b\<rbrakk> \<Longrightarrow> prefix_closed (doE c <- P;
if c then a else b
odE)
theory Trace_Prefix_Closed

lemma prefix_closed_whenM[prefix_closed_cond]:
  "\<lbrakk> prefix_closed P; prefix_closed f \<rbrakk> \<Longrightarrow> prefix_closed (whenM P f)" unfolding whenM_def by (wpsimp wp: prefix_closed_terminal prefix_closed_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed P; prefix_closed f\<rbrakk> \<Longrightarrow> prefix_closed (whenM P f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed P; prefix_closed f\<rbrakk> \<Longrightarrow> prefix_closed (ifM P f (return ()))
theory Trace_Prefix_Closed

lemma prefix_closed_orM[prefix_closed_cond]:
  "\<lbrakk> prefix_closed A; prefix_closed B \<rbrakk> \<Longrightarrow> prefix_closed (orM A B)" unfolding orM_def by (wpsimp wp: prefix_closed_terminal prefix_closed_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed A; prefix_closed B\<rbrakk> \<Longrightarrow> prefix_closed (orM A B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed A; prefix_closed B\<rbrakk> \<Longrightarrow> prefix_closed (ifM A (return True) B)
theory Trace_Prefix_Closed

lemma prefix_closed_andM[prefix_closed_cond]:
  "\<lbrakk> prefix_closed A; prefix_closed B \<rbrakk> \<Longrightarrow> prefix_closed (andM A B)" unfolding andM_def by (wpsimp wp: prefix_closed_terminal prefix_closed_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed A; prefix_closed B\<rbrakk> \<Longrightarrow> prefix_closed (andM A B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed A; prefix_closed B\<rbrakk> \<Longrightarrow> prefix_closed (ifM A B (return False))
theory Trace_Prefix_Closed

lemma prefix_closed_put_trace_elem[prefix_closed_terminal]:
  "prefix_closed (put_trace_elem x)" by (clarsimp simp: prefix_closed_def put_trace_elem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (put_trace_elem x)
theory Trace_Prefix_Closed

lemma prefix_closed_put_trace[prefix_closed_terminal]:
  "prefix_closed (put_trace tr)" by (induct tr; wpsimp wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (put_trace tr)
theory Trace_Prefix_Closed

lemma prefix_closed_env_steps[prefix_closed_terminal]:
  "prefix_closed env_steps" by (wpsimp simp: env_steps_def wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed env_steps
theory Trace_Prefix_Closed

lemma prefix_closed_interference[prefix_closed_terminal]:
  "prefix_closed interference" by (wpsimp simp: interference_def commit_step_def wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed interference
theory Trace_Prefix_Closed

lemma prefix_closed_await[prefix_closed_terminal]:
  "prefix_closed (Await c)" by (wpsimp simp: Await_def wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (Await c)
theory Trace_Prefix_Closed

lemma prefix_closed_repeat_n[prefix_closed_cond]:
  "prefix_closed f \<Longrightarrow> prefix_closed (repeat_n n f)" by (induct n; wpsimp wp: prefix_closed_terminal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> prefix_closed (repeat_n n f)
theory Trace_Prefix_Closed

lemma prefix_closed_repeat[prefix_closed_cond]:
  "prefix_closed f \<Longrightarrow> prefix_closed (repeat f)" apply (simp add: repeat_def) apply (wpsimp wp: prefix_closed_terminal prefix_closed_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> prefix_closed (repeat f) proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> prefix_closed (do n <- select UNIV;
repeat_n n f
od) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rg_empty_conds[simp]:
  "rely_cond R s0s []"
  "guar_cond G s0s []" by (simp_all add: rely_cond_def guar_cond_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond R s0s [] &&& guar_cond G s0s []
theory Trace_RG

lemma validIE_def2:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<equiv>
     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> (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 (unfold validI_def validIE_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> \<equiv> 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> (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 in_rely:
  "\<lbrakk>(tr, res) \<in> f s; rely_cond R s0s tr\<rbrakk> \<Longrightarrow> (tr, res) \<in> rely f R s0s s" by (simp add: rely_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> f s; rely_cond R s0s tr\<rbrakk> \<Longrightarrow> (tr, res) \<in> rely f R s0s s
theory Trace_RG

lemma rg_weaken_pre:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (simp add: validI_def, blast)

(* 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\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_weaken_preE:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: validIE_def rg_weaken_pre)

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

lemma rely_weaken:
  "\<lbrakk>\<forall>s0 s. R s0 s \<longrightarrow> R' s0 s; (tr, res) \<in> rely f R s s0\<rbrakk>
   \<Longrightarrow> (tr, res) \<in> rely f R' s s0" by (simp add: rely_def rely_cond_def, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s0 s. R s0 s \<longrightarrow> R' s0 s; (tr, res) \<in> rely f R s s0\<rbrakk> \<Longrightarrow> (tr, res) \<in> rely f R' s s0
theory Trace_RG

lemma rg_weaken_rely:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>s0 s. R s0 s \<Longrightarrow> R' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (simp add: validI_def) by (metis rely_weaken)

(* 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. R s0 s \<Longrightarrow> R' s0 s\<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. R s0 s \<Longrightarrow> R' s0 s\<rbrakk> \<Longrightarrow> \<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_weaken_relyE:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>s0 s. R s0 s \<Longrightarrow> R' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: validIE_def rg_weaken_rely)

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

lemma rg_weaken_pre_rely:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>s0 s. R s0 s \<Longrightarrow> R' s0 s; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (rule rg_weaken_pre, rule rg_weaken_rely; assumption)

(* 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. R s0 s \<Longrightarrow> R' s0 s; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_weaken_pre_relyE:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>s0 s. R s0 s \<Longrightarrow> R' s0 s; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: validIE_def rg_weaken_pre_rely)

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

lemma wpc_helper_validI:
  "\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (case_prod Q, Q', Q'') (\<lbrace>curry P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>)" by (clarsimp simp: wpc_helper_def elim!: rg_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (\<lambda>(x, y). Q x y, Q', Q'') \<lbrace>curry P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace>
theory Trace_RG

lemma wpc_helper_validIE:
  "\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (case_prod Q, Q', Q'') (\<lbrace>curry P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>)" by (clarsimp simp: wpc_helper_def elim!: rg_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (\<lambda>(x, y). Q x y, Q', Q'') \<lbrace>curry P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma trace_steps_append:
  "trace_steps (xs @ ys) s
   = trace_steps xs s \<union> trace_steps ys (last_st_tr (rev xs) s)" by (induct xs arbitrary: s, simp_all add: last_st_tr_def hd_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trace_steps (xs @ ys) s = trace_steps xs s \<union> trace_steps ys (last_st_tr (rev xs) s)
theory Trace_RG

lemma rely_cond_append:
  "rely_cond R s (xs @ ys) = (rely_cond R s ys \<and> rely_cond R (last_st_tr ys s) xs)" by (simp add: rely_cond_def trace_steps_append ball_Un conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond R s (xs @ ys) = (rely_cond R s ys \<and> rely_cond R (last_st_tr ys s) xs)
theory Trace_RG

lemma guar_cond_append:
  "guar_cond G s (xs @ ys) = (guar_cond G s ys \<and> guar_cond G (last_st_tr ys s) xs)" by (simp add: guar_cond_def trace_steps_append ball_Un conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guar_cond G s (xs @ ys) = (guar_cond G s ys \<and> guar_cond G (last_st_tr ys s) xs)
theory Trace_RG

lemma no_trace_last_st_tr:
  "\<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0" by (fastforce simp: no_trace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0
theory Trace_RG

lemma no_trace_rely_cond:
  "\<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> rely_cond R s0 tr" by (fastforce simp: no_trace_def rely_cond_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> rely_cond R s0 tr
theory Trace_RG

lemma validI_valid_no_trace_eq:
  "no_trace f \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> = (\<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>)" apply (rule iffI) apply (fastforce simp: rely_def validI_def valid_def mres_def
                    dest: no_trace_emp) apply (clarsimp simp: rely_def validI_def valid_def mres_def no_trace_prefix_closed) apply (fastforce simp: eq_snd_iff dest: no_trace_emp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace f \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> = (\<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_trace f; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>
 2. \<lbrakk>no_trace f; \<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_trace f; \<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>no_trace f; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>x\<in>Result -` snd ` f s. case x of (r, s') \<Rightarrow> Q r s0 s'); P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr\<rbrakk> \<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:
No subgoals!
theory Trace_RG

lemma validIE_validE_no_trace_eq:
  "no_trace f \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = (\<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>,\<lbrace>\<lambda>v. E v s0\<rbrace>)" unfolding validIE_def validE_def apply (clarsimp simp: validI_valid_no_trace_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace f \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> = (\<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0\<rbrace>, \<lbrace>\<lambda>v. E v s0\<rbrace>) proof (prove)
goal (1 subgoal):
 1. no_trace f \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace> = (\<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma validIE_split:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (auto simp: validIE_def validI_split)

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

lemma rg_TrueI:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>_ _. \<top>\<rbrace> = prefix_closed f" by (simp add: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ _ _. True\<rbrace> = prefix_closed f
theory Trace_RG

lemma rgE_TrueI:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>_ _. \<top>\<rbrace>,\<lbrace>\<lambda>_ _. \<top>\<rbrace> = prefix_closed f" by (simp add: validIE_def rg_TrueI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ _ _. True\<rbrace>, - = prefix_closed f
theory Trace_RG

lemma rg_post_conj[intro]:
  "\<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>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q and Q'\<rbrace>" by (fastforce 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>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q and Q'\<rbrace>
theory Trace_RG

lemma rg_pre_disj[intro]:
  "\<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>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (fastforce simp: validI_def pred_disj_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>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>