theory Trace_More_RG

lemma rg_list_all_lift:
  "\<lbrakk>\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. list_all (\<lambda>r. Q r s0 s) xs \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. list_all (\<lambda>r. Q r s0 s) xs\<rbrace>" apply (rule validI_split[rotated, simplified pred_conj_def]) apply assumption apply (induct xs; simp) apply wpsimp apply (rule rg_vcg_conj_lift; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. list_all (\<lambda>r. Q r s0 s) xs \<and> P s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. list_all (\<lambda>r. Q r s0 s) xs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<lbrakk>\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x xa. list_all (\<lambda>r. Q r x xa) xs\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. list_all (\<lambda>r. Q r s0 s) xs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x xa. list_all (\<lambda>r. Q r x xa) xs\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. list_all (\<lambda>r. Q r s0 s) xs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>x xa. True\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. True\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>x xa. list_all (\<lambda>r. Q r x xa) xs\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. list_all (\<lambda>r. Q r s0 s) xs\<rbrace>; \<And>r. r = a \<or> r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x xa. Q a x xa \<and> list_all (\<lambda>r. Q r x xa) xs\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. Q a s0 s \<and> list_all (\<lambda>r. Q r s0 s) xs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>x xa. list_all (\<lambda>r. Q r x xa) xs\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. list_all (\<lambda>r. Q r s0 s) xs\<rbrace>; \<And>r. r = a \<or> r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q r\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x xa. Q a x xa \<and> list_all (\<lambda>r. Q r x xa) xs\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. Q a s0 s \<and> list_all (\<lambda>r. Q r s0 s) xs\<rbrace> proof (prove)
goal:
No subgoals!