theory Trace_More_RG

lemma rg_weak_lift_imp_conj:
  "\<lbrakk> \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> m -,\<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> m -,\<lbrace>R'\<rbrace>; \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> Q s0 s) \<and> R s0 s \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (P \<longrightarrow> Q' rv s0 s) \<and> R' rv s0 s\<rbrace>" apply wp_pre apply (rule rg_vcg_conj_lift) apply (rule rg_weak_lift_imp; assumption) apply (rule validI_split; assumption) apply clarsimp done

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