kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma rg_vcg_all_liftE_R:
  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>,\<lbrace>E\<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>,\<lbrace>E\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

(* 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>, \<lbrace>E\<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>, \<lbrace>E\<rbrace>
theory Trace_RG

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

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

lemma rg_vcg_imp_lift:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' s0 s \<or> Q' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>" by (simp only: imp_conv_disj) (rule rg_vcg_disj_lift)

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

lemma rg_vcg_imp_lift':
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<not> P' s0 s \<longrightarrow> Q' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>" by (wpsimp wp: rg_vcg_imp_lift)

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

lemma rg_vcg_imp_liftE:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' s0 s \<or> Q' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P rv s0 s \<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>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' s0 s \<or> Q' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_vcg_imp_liftE':
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<not> P' s0 s \<longrightarrow> Q' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>,\<lbrace>E\<rbrace>" by (wpsimp wp: rg_vcg_imp_liftE)

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

lemma rg_vcg_imp_liftE_E:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' s0 s \<or> Q' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> E rv s0 s\<rbrace>" by (auto simp add: validI_def validIE_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>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' s0 s \<or> Q' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> E rv s0 s\<rbrace>
theory Trace_RG

lemma rg_vcg_imp_liftE_E':
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<not> P' s0 s \<longrightarrow> Q' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. P rv s0 s \<longrightarrow> E rv s0 s\<rbrace>" by (wpsimp wp: rg_vcg_imp_liftE_E)

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

lemma rg_vcg_imp_conj_lift[wp_comb]:
  "\<lbrakk>\<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>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q' rv s0 s \<and> Q'' rv s0 s) \<and> Q''' rv s0 s\<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>\<lambda>rv s0 s. Q rv s0 s \<longrightarrow> Q' rv s0 s\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q' rv s0 s \<and> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace>
theory Trace_RG

lemma rg_absorb_imp:
  "\<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 s0 s. Q rv s0 s \<longrightarrow> Q' rv s0 s\<rbrace>" by (erule rg_post_imp[rotated], blast)

(* 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 s0 s. Q rv s0 s \<longrightarrow> Q' rv s0 s\<rbrace>
theory Trace_RG

lemma rg_vcg_const_imp_lift:
  "\<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> P'' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P \<longrightarrow> Q rv s0 s\<rbrace>" apply (cases P; simp) apply wp_pre apply (rule validI_split; assumption) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> P'' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. P \<longrightarrow> Q rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' s0 s \<and> P'' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P\<rbrakk> \<Longrightarrow> \<lbrace>?P'7\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>s0 s. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P; P' s0 s \<and> P'' s0 s\<rbrakk> \<Longrightarrow> ?P'7 s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; P; P' s0 s \<and> P'' s0 s\<rbrakk> \<Longrightarrow> (P' and P'') s0 s proof (prove)
goal:
No subgoals!
theory Trace_RG

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

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

lemma rg_vcg_const_imp_liftE_R:
  "\<lbrakk>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>,-; \<lbrace>P''\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> P'' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P \<longrightarrow> Q rv s0 s\<rbrace>,-" unfolding validIE_def by (rule rg_strengthen_post)
     (fastforce intro!: rg_vcg_const_imp_lift split: sum.splits)+

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

lemma rg_weak_lift_imp:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P''\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> P'' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P \<longrightarrow> Q rv s0 s\<rbrace>" by (auto simp: validI_def split_def)

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

lemma rg_weak_lift_impE:
  "\<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>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> P'' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P \<longrightarrow> Q rv s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. P \<longrightarrow> E rv s0 s\<rbrace>" unfolding validIE_def by (rule rg_strengthen_post)
     (fastforce intro!: rg_weak_lift_imp split: sum.splits)+

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

lemma rg_weak_lift_impE_R:
  "\<lbrakk>\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>,-; \<lbrace>P''\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> P' s0 s) \<and> P'' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P \<longrightarrow> Q rv s0 s\<rbrace>,-" unfolding validIE_def by (rule rg_strengthen_post)
     (fastforce intro!: rg_weak_lift_imp split: sum.splits)+

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

lemma rg_vcg_ex_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. \<exists>x. P x s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<exists>x. Q x rv s0 s\<rbrace>" by (clarsimp simp: validI_def, blast)

(* 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. \<exists>x. P x s0 s\<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 rg_vcg_ex_liftE:
  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<exists>x. 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. (\<And>x. \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<exists>x. Q x rv s0 s\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_vcg_ex_liftE_E:
  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-,\<lbrace>E x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-,\<lbrace>\<lambda>rv s0 s. \<exists>x. E x rv s0 s\<rbrace>" by (fastforce simp: validIE_def validI_def split: sum.splits)

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

lemma rg_vcg_ex_lift_R1:
  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,-\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,-" by (fastforce simp: validI_def validIE_def split: sum.splits)

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

lemma rg_triv:    "\<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>Q\<rbrace>" .

(* 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>Q\<rbrace>
theory Trace_RG

lemma rg_trivE:   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" .

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

lemma rg_trivE_R: "\<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>Q\<rbrace>,-" .

(* 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>Q\<rbrace>, -