kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma liftE_validIE[simp]:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> liftE f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (simp add: liftE_liftM validIE_def rg_liftM_subst o_def)

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

lemma rg_vcg_if_split:
  "\<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>P''\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> (\<not>P \<longrightarrow> P'' s0 s)\<rbrace>,\<lbrace>R\<rbrace> if P then f else g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by simp

(* 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> \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> (\<not> P \<longrightarrow> P'' s0 s)\<rbrace>, \<lbrace>R\<rbrace> if P then f else g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_vcg_if_splitE:
  "\<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>P''\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> (\<not>P \<longrightarrow> P'' s0 s)\<rbrace>,\<lbrace>R\<rbrace> if P then f else g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* 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> \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> (\<not> P \<longrightarrow> P'' s0 s)\<rbrace>, \<lbrace>R\<rbrace> if P then f else g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_vcg_split_case_option:
  "\<lbrakk>\<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f x \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>P' x y\<rbrace>,\<lbrace>R\<rbrace> g x y \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (x = None \<longrightarrow> P x s0 s) \<and> (\<forall>y. x = Some y \<longrightarrow> P' x y s0 s)\<rbrace>,\<lbrace>R\<rbrace>
       case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
       \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>" by (cases x; simp)

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

lemma rg_vcg_split_case_optionE:
  "\<lbrakk>\<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f x \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>,\<lbrace>E x\<rbrace>; \<And>x y. x = Some y \<Longrightarrow> \<lbrace>P' x y\<rbrace>,\<lbrace>R\<rbrace> g x y \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>,\<lbrace>E x\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (x = None \<longrightarrow> P x s0 s) \<and> (\<forall>y. x = Some y \<longrightarrow> P' x y s0 s)\<rbrace>,\<lbrace>R\<rbrace>
       case x of None \<Rightarrow> f x | Some y \<Rightarrow> g x y
       \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>,\<lbrace>E x\<rbrace>" by (cases x; simp)

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

lemma rg_vcg_split_case_sum:
  "\<lbrakk>\<And>x a. x = Inl a \<Longrightarrow> \<lbrace>P x a\<rbrace>,\<lbrace>R\<rbrace> f x a \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>; \<And>x b. x = Inr b \<Longrightarrow> \<lbrace>P' x b\<rbrace>,\<lbrace>R\<rbrace> g x b \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>a. x = Inl a \<longrightarrow> P x a s0 s) \<and> (\<forall>b. x = Inr b \<longrightarrow> P' x b s0 s)\<rbrace>,\<lbrace>R\<rbrace>
       case x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b
       \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>" by (cases x; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x a. x = Inl a \<Longrightarrow> \<lbrace>P x a\<rbrace>, \<lbrace>R\<rbrace> f x a \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>; \<And>x b. x = Inr b \<Longrightarrow> \<lbrace>P' x b\<rbrace>, \<lbrace>R\<rbrace> g x b \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>a. x = Inl a \<longrightarrow> P x a s0 s) \<and> (\<forall>b. x = Inr b \<longrightarrow> P' x b s0 s)\<rbrace>, \<lbrace>R\<rbrace> case x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>
theory Trace_RG

lemma bind_twp_nobind:
  "\<lbrakk>\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> do f; g od \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>" by (erule bind_twp_fwd) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>B\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>C\<rbrace>; \<lbrace>A\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>, \<lbrace>R\<rbrace> do f;
g
od \<lbrace>G\<rbrace>, \<lbrace>C\<rbrace>
theory Trace_RG

lemma bindE_twp_nobind:
  "\<lbrakk>\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> doE f; g odE \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>" by (erule bindE_twp_fwd) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>B\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>, \<lbrace>R\<rbrace> doE f;
g
odE \<lbrace>G\<rbrace>, \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_chain:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>s0 s. P' s0 s \<Longrightarrow> P s0 s; \<And>rv s0 s. Q rv s0 s \<Longrightarrow> S rv s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>" by (wp_pre, rule rg_post_imp)

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

lemma validIE_weaken: (* FIXME lib: eliminate in favour of rg_chainE *)
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s; \<And>rv s0 s. Q' rv s0 s \<Longrightarrow> Q rv s0 s;
    \<And>rv s0 s. E' rv s0 s \<Longrightarrow> E rv s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by wp_pre (rule rg_post_impE)

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

lemma rg_vcg_conj_lift:
  "\<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>\<lambda>s0 s. P s0 s \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>" unfolding validI_def by fastforce

\<comment> \<open>A variant which works nicely with subgoals that do not contain schematics\<close>

(* 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>\<lambda>s0 s. P s0 s \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<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')); 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'))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. (P 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' \<and> Q' rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma rg_vcg_conj_liftE1:
  "\<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>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>,\<lbrace>E\<rbrace>" unfolding validI_def validIE_def by (fastforce simp: split_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>Q\<rbrace>, -; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>, \<lbrace>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> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r (last_st_tr tr 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> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q' r (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> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s' \<and> Q' r (last_st_tr tr s0) s')))
theory Trace_RG

lemma rg_vcg_conj_liftE2:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P' s0 s\<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>" unfolding validIE_def by (rule rg_post_imp[OF _ rg_vcg_conj_lift]; simp 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>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P' s0 s\<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> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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> True\<rbrace>; \<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>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s \<and> E' e s0 s | Inr r \<Rightarrow> Q' r s0 s\<rbrace>
theory Trace_RG

lemma rg_vcg_conj_liftE_weaker:
  assumes "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. P s0 s \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>,\<lbrace>E\<rbrace>" apply (rule rg_pre) apply (fastforce intro: assms rg_vcg_conj_liftE1 validE_validE_R rg_post_impE) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P s0 s \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 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>, \<lbrace>E\<rbrace>
 2. \<And>s0 s. P s0 s \<and> P' s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. P s0 s \<and> P' s0 s \<Longrightarrow> (P and P') s0 s proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rg_vcg_disj_lift:
  "\<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>\<lambda>s0 s. P s0 s \<or> P' s0 s\<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 fastforce

(* 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>\<lambda>s0 s. P s0 s \<or> P' s0 s\<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. \<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')); 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'))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. (P s0 s \<or> 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_vcg_disj_lift_R:
  assumes x: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,-"
  assumes y: "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,-"
  shows      "\<lbrace>\<lambda>s0 s. P s0 s \<or> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<or> Q' rv s0 s\<rbrace>,-" using assms by (fastforce simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P s0 s \<or> P' s0 s\<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)
using this:
\<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>, -

goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P s0 s \<or> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<or> Q' rv s0 s\<rbrace>, -
theory Trace_RG

lemma rg_vcg_const_Ball_lift:
  "\<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q x\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x\<in>S. P x s0 s) \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>x\<in>S. Q x rv s0 s\<rbrace>" by (fastforce simp: validI_def)

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

lemma rg_vcg_const_Ball_liftE:
  "\<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-, \<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x\<in>S. P x s0 s) \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>x\<in>S. Q x 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>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>Q x\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, -, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x\<in>S. P x s0 s) \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>x\<in>S. Q x rv s0 s\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_vcg_const_Ball_liftE_E:
 "\<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f -,-,\<lbrace>E x\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace>\<lambda>s0 s.(\<forall>x\<in>S. P x s0 s) \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-,\<lbrace>\<lambda>rv s0 s. \<forall>x \<in> S. E x rv s0 s\<rbrace>" unfolding validIE_def by (rule rg_strengthen_post)
     (fastforce intro!: rg_vcg_const_Ball_lift split: sum.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f -, -, \<lbrace>E x\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x\<in>S. P x s0 s) \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, -, \<lbrace>\<lambda>rv s0 s. \<forall>x\<in>S. E x rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E x e s0 s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x\<in>S. P x s0 s) \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> \<forall>x\<in>S. E x e s0 s | Inr r \<Rightarrow> True\<rbrace>
theory Trace_RG

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

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