theory MonadSep

lemma sep_list_conj_map_singleton_wp:
  "\<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>" apply (rule hoare_chain [where P="<P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R>" and
                                 Q="\<lambda>_. <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R>"]) apply fastforce apply (subst (asm) sep_list_conj_map_remove1, assumption) apply (sep_select_asm 3) apply (sep_solve) apply (subst sep_list_conj_map_remove1, sep_solve+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R>\<rbrace>
 2. \<And>s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <P \<and>* \<And>* map I xs \<and>* R> s\<rbrakk> \<Longrightarrow> <P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s
 3. \<And>rv s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* \<And>* map I xs \<and>* R> s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <P \<and>* \<And>* map I xs \<and>* R> s\<rbrakk> \<Longrightarrow> <P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s
 2. \<And>rv s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* \<And>* map I xs \<and>* R> s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <P \<and>* (I x \<and>* \<And>* map I (remove1 x xs)) \<and>* R> s\<rbrakk> \<Longrightarrow> <P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s
 2. \<And>rv s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* \<And>* map I xs \<and>* R> s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <R \<and>* P \<and>* I x \<and>* \<And>* map I (remove1 x xs)> s\<rbrakk> \<Longrightarrow> <P \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s
 2. \<And>rv s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* \<And>* map I xs \<and>* R> s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>x \<in> set xs; \<And>R. \<lbrace><P \<and>* I x \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* I x \<and>* R>\<rbrace>; <Q \<and>* I x \<and>* \<And>* map I (remove1 x xs) \<and>* R> s\<rbrakk> \<Longrightarrow> <Q \<and>* \<And>* map I xs \<and>* R> s proof (prove)
goal:
No subgoals!