kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma last_st_tr_map_zip:
  "\<lbrakk>length flags = length tr; \<forall>fl tmid s. snd (f (fl, (tmid, s))) = s\<rbrakk>
   \<Longrightarrow> last_st_tr (map f (zip flags tr)) = last_st_tr tr" apply (erule last_st_tr_map_zip_hd) apply (clarsimp simp: neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length flags = length tr; \<forall>fl tmid s. snd (f (fl, tmid, s)) = s\<rbrakk> \<Longrightarrow> last_st_tr (map f (zip flags tr)) = last_st_tr tr proof (prove)
goal (1 subgoal):
 1. \<forall>fl tmid s. snd (f (fl, tmid, s)) = s \<Longrightarrow> tr \<noteq> [] \<longrightarrow> snd (f (hd flags, hd tr)) = snd (hd tr) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rg_validI:
  assumes validI: "\<lbrace>Pf\<rbrace>,\<lbrace>Rf\<rbrace> f \<lbrace>Gf\<rbrace>,\<lbrace>Qf\<rbrace>"
     "\<lbrace>Pg\<rbrace>,\<lbrace>Rg\<rbrace> g \<lbrace>Gg\<rbrace>,\<lbrace>Qg\<rbrace>"
  and compat: "R \<le> Rf" "R \<le> Rg" "Gf \<le> G" "Gg \<le> G" "Gf \<le> Rg" "Gg \<le> Rf"
  shows "\<lbrace>Pf and Pg\<rbrace>,\<lbrace>R\<rbrace> parallel f g \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Qf rv and Qg rv\<rbrace>" apply (clarsimp simp: validI_def rely_def pred_conj_def
                        prefix_closed_parallel validI[THEN validI_prefix_closed]) apply (drule(3) parallel_rely_induct0[OF _ _ _ validI order_refl order_refl compat]) apply clarsimp apply (drule(2) validI[THEN validI_rvD])+ apply (simp add: last_st_tr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Pf and Pg\<rbrace>, \<lbrace>R\<rbrace> parallel f g \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. Qf rv and Qg rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>Pf s0 s; Pg s0 s; (tr, res) \<in> parallel f g s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Qf rv (last_st_tr tr s0) s' \<and> Qg rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>Pf s0 s; Pg s0 s; rely_cond R s0 tr; \<exists>tr_f. (tr_f, res) \<in> f s \<and> (\<exists>tr_g. (tr_g, res) \<in> g s \<and> rely_cond Rf s0 tr_f \<and> rely_cond Rg s0 tr_g \<and> map snd tr_f = map snd tr \<and> map snd tr_g = map snd tr \<and> (\<forall>i\<le>length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0) \<and> guar_cond G s0 tr)\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Qf rv (last_st_tr tr s0) s' \<and> Qg rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr tr_f tr_g rv s'. \<lbrakk>Pf s0 s; Pg s0 s; rely_cond R s0 tr; (tr_f, Result (rv, s')) \<in> f s; (tr_g, Result (rv, s')) \<in> g s; rely_cond Rf s0 tr_f; rely_cond Rg s0 tr_g; map snd tr_f = map snd tr; map snd tr_g = map snd tr; \<forall>i\<le>length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0; guar_cond G s0 tr\<rbrakk> \<Longrightarrow> Qf rv (last_st_tr tr s0) s' \<and> Qg rv (last_st_tr tr s0) s' proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr tr_f tr_g rv s'. \<lbrakk>rely_cond R s0 tr; (tr_f, Result (rv, s')) \<in> f s; (tr_g, Result (rv, s')) \<in> g s; rely_cond Rf s0 tr_f; rely_cond Rg s0 tr_g; map snd tr_f = map snd tr; map snd tr_g = map snd tr; \<forall>i\<le>length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0; guar_cond G s0 tr; Qf rv (last_st_tr tr_f s0) s'; Qg rv (last_st_tr tr_g s0) s'\<rbrakk> \<Longrightarrow> Qf rv (last_st_tr tr s0) s' \<and> Qg rv (last_st_tr tr s0) s' proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rely_prim[simp]:
  "rely (\<lambda>s. insert (v s) (f s)) R s0 = (\<lambda>s. {x. x = v s \<and> rely_cond R s0 (fst x)} \<union> (rely f R s0 s))"
  "rely (\<lambda>s. {}) R s0 = (\<lambda>_. {})"
  "rely (\<lambda>s. (f s) \<union> (g s)) R s0 = (\<lambda>s. (rely f R s0 s) \<union> (rely g R s0 s))"
  "rely (\<lambda>s. if C s then f s else g s) R s0 = (\<lambda>s. if C s then rely f R s0 s else rely g R s0 s)" by (auto simp: rely_def prod_eq_iff split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rely (\<lambda>s. insert (v s) (f s)) R s0 = (\<lambda>s. {x. x = v s \<and> rely_cond R s0 (fst x)} \<union> rely f R s0 s) &&& rely (\<lambda>s. {}) R s0 = (\<lambda>_. {})) &&& rely (\<lambda>s. f s \<union> g s) R s0 = (\<lambda>s. rely f R s0 s \<union> rely g R s0 s) &&& rely (\<lambda>s. if C s then f s else g s) R s0 = (\<lambda>s. if C s then rely f R s0 s else rely g R s0 s)
theory Trace_RG

lemma put_trace_res:
  "(tr, res) \<in> put_trace xs s
   \<Longrightarrow> \<exists>n. tr = drop n xs \<and> n \<le> length xs
         \<and> res = (case n of 0 \<Rightarrow> Result ((), s) | _ \<Rightarrow> Incomplete)" apply (clarsimp simp: put_trace_eq_drop) apply (auto simp: gr0_conv_Suc intro: exI[where x=0]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tr, res) \<in> put_trace xs s \<Longrightarrow> \<exists>n. tr = drop n xs \<and> n \<le> length xs \<and> res = (case n of 0 \<Rightarrow> Result ((), s) | Suc nat \<Rightarrow> Incomplete) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n \<le> length xs; res = (if n = 0 then Result ((), s) else Incomplete); tr = drop n xs\<rbrakk> \<Longrightarrow> (n = 0 \<longrightarrow> (\<exists>n. xs = drop n xs \<and> n \<le> length xs \<and> Result ((), s) = (case n of 0 \<Rightarrow> Result ((), s) | Suc nat \<Rightarrow> Incomplete))) \<and> (0 < n \<longrightarrow> (\<exists>na. drop n xs = drop na xs \<and> na \<le> length xs \<and> Incomplete = (case na of 0 \<Rightarrow> Result ((), s) | Suc nat \<Rightarrow> Incomplete))) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma put_trace_twp[wp]:
  "\<lbrace>\<lambda>s0 s. (\<forall>n. rely_cond R s0 (drop n xs) \<longrightarrow> guar_cond G s0 (drop n xs))
     \<and> (rely_cond R s0 xs \<longrightarrow> Q () (last_st_tr xs s0) s)\<rbrace>,\<lbrace>R\<rbrace>
   put_trace xs
   \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (clarsimp simp: validI_def rely_def) apply (drule put_trace_res) apply (clarsimp; clarsimp split: nat.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. (\<forall>n. rely_cond R s0 (drop n xs) \<longrightarrow> guar_cond G s0 (drop n xs)) \<and> (rely_cond R s0 xs \<longrightarrow> Q () (last_st_tr xs s0) s)\<rbrace>, \<lbrace>R\<rbrace> put_trace xs \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>\<forall>n. rely_cond R s0 (drop n xs) \<longrightarrow> guar_cond G s0 (drop n xs); rely_cond R s0 xs \<longrightarrow> Q () (last_st_tr xs s0) s; (tr, res) \<in> put_trace xs s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>s'. res = Result ((), s') \<longrightarrow> Q () (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>\<forall>n. rely_cond R s0 (drop n xs) \<longrightarrow> guar_cond G s0 (drop n xs); rely_cond R s0 xs \<longrightarrow> Q () (last_st_tr xs s0) s; rely_cond R s0 tr; \<exists>n. tr = drop n xs \<and> n \<le> length xs \<and> res = (case n of 0 \<Rightarrow> Result ((), s) | Suc nat \<Rightarrow> Incomplete)\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>s'. res = Result ((), s') \<longrightarrow> Q () (last_st_tr tr s0) s') proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rely_cond_rtranclp:
  "rely_cond R s (map (Pair Env) xs) \<Longrightarrow> rtranclp R s (last_st_tr (map (Pair Env) xs) s)" apply (induct xs arbitrary: s rule: rev_induct) apply simp apply (clarsimp simp add: rely_cond_def) apply (erule converse_rtranclp_into_rtranclp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond R s (map (Pair Env) xs) \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) xs) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. rely_cond R s (map (Pair Env) []) \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) []) s)
 2. \<And>x xs s. \<lbrakk>\<And>s. rely_cond R s (map (Pair Env) xs) \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) xs) s); rely_cond R s (map (Pair Env) (xs @ [x]))\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) (xs @ [x])) s) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. rely_cond R s (map (Pair Env) xs) \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) xs) s); rely_cond R s (map (Pair Env) (xs @ [x]))\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) (xs @ [x])) s) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. \<forall>x\<in>trace_steps (rev (map (Pair Env) xs)) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) xs) s); R s x; \<forall>x\<in>trace_steps (rev (map (Pair Env) xs)) x. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) xs) x) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. \<forall>x\<in>trace_steps (rev (map (Pair Env) xs)) s. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s \<Longrightarrow> R\<^sup>*\<^sup>* s (last_st_tr (map (Pair Env) xs) s); \<forall>x\<in>trace_steps (rev (map (Pair Env) xs)) x. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* x (last_st_tr (map (Pair Env) xs) x) proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rg_gen_asm:
  "\<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<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>" by (auto simp: validI_def)

(* 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>; \<not> P \<Longrightarrow> prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>P' and (\<lambda>_ _. P)\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

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

\<comment> \<open>Useful for forward reasoning, when P is known.
    The first version allows weakening the precondition.\<close>

(* 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>; \<not> P \<Longrightarrow> prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_ _. P) and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_gen_asm_spec':
  "\<lbrakk>\<And>s0 s. P s0 s \<Longrightarrow> S \<and> P' s0 s; S \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> S \<Longrightarrow> prefix_closed f\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (auto 6 2 simp: validI_def)

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

lemma rg_gen_asm_spec:
  "\<lbrakk>\<And>s0 s. P s0 s \<Longrightarrow> S; S \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> S \<Longrightarrow> prefix_closed f\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (rule rg_gen_asm_spec'[where S=S and P'=P]) simp

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

lemma rg_disjI1:
  "\<lbrakk>\<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>\<lambda>rv s0 s. Q rv s0 s \<or> Q' rv s0 s\<rbrace>" unfolding validI_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<or> Q' rv s0 s\<rbrace> 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')) \<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' \<or> Q' rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_disjI2:
  "\<lbrakk>\<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>\<lambda>rv s0 s. Q rv s0 s \<or> Q' rv s0 s\<rbrace>" unfolding validI_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<or> Q' rv s0 s\<rbrace> 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')) \<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' \<or> Q' rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_assume_preE:
  "\<lbrakk>\<And>s0 s. P s0 s \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (auto simp: validI_def validIE_def)

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

lemma rg_allI:
  "(\<And>x. \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>x. Q x rv s0 s\<rbrace>" by (simp add: validI_def)

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

lemma validE_allI:
  "(\<And>x. \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r s. Q x r s\<rbrace>,\<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>x. Q x rv s0 s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validI_def validIE_def split: sum.splits)

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

lemma rg_exI:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<exists>x. Q x rv s0 s\<rbrace>" by (simp add: validI_def) blast

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

lemma validIE_impI:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>,\<lbrace>E\<rbrace>; P' \<Longrightarrow> \<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>\<lambda>rv s0 s. P' \<longrightarrow> Q rv s0 s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, -, \<lbrace>E\<rbrace>; P' \<Longrightarrow> \<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>\<lambda>rv s0 s. P' \<longrightarrow> Q rv s0 s\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_when_cases:
  "\<lbrakk>\<And>s0 s. \<lbrakk>\<not>B; P s0 s\<rbrakk> \<Longrightarrow> Q s0 s; B \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> when B f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>" by (cases B; simp add: validI_def prefix_closed_def return_def)

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

lemma rg_vcg_prop:
  "prefix_closed f \<Longrightarrow> \<lbrace>\<lambda>s0 s. P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P\<rbrace>" by (simp add: validI_def)

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

lemma validI_validIE:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>" by (rule rg_post_imp_dc)

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

lemma validI_validIE2:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s; \<And>s0 s. Q' s0 s \<Longrightarrow> E s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>" unfolding validI_def validIE_def by (clarsimp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s; \<And>s0 s. Q' s0 s \<Longrightarrow> E s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>_. E\<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' (last_st_tr tr s0) s')); \<And>s0 s. Q' s0 s \<Longrightarrow> Q s0 s; \<And>s0 s. Q' s0 s \<Longrightarrow> E 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> (case rv of Inl e \<Rightarrow> E (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q (last_st_tr tr s0) s')))
theory Trace_RG

lemma validIE_validI:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>" unfolding validIE_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> Q s0 s | _ \<Rightarrow> Q s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
theory Trace_RG

lemma validI_validIE_R:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,-" by (rule rg_post_imp_dc2)

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

lemma validI_validIE_E:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-,\<lbrace>\<lambda>_. Q\<rbrace>" by (rule rg_post_imp_dc2E)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, -, \<lbrace>\<lambda>_. Q\<rbrace>