theory MonadSep

lemma sep_list_conj_submap_wp:
  "\<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys;
   \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* R>\<rbrace>" apply (subst sep_list_con_map_filter [where t="\<lambda>x. x \<in> set xs" and xs=ys, THEN sym]) apply (subst sep_list_con_map_filter [where t="\<lambda>x. x \<in> set xs" and xs=ys, THEN sym]) apply (subgoal_tac "set [x\<leftarrow>ys . x \<in> set xs] = set xs") apply (subst sep_list_conj_eq [where xs="[x\<leftarrow>ys . x \<in> set xs]" and ys=xs], clarsimp+) apply (subst sep_list_conj_eq [where xs="[x\<leftarrow>ys . x \<in> set xs]" and ys=xs], clarsimp+) apply (clarsimp simp: sep_conj_assoc) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* \<And>* map I ys \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* R>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* (\<And>* map I (filter (\<lambda>x. x \<in> set xs) ys) \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I ys \<and>* R>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* (\<And>* map I (filter (\<lambda>x. x \<in> set xs) ys) \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* map I (filter (\<lambda>x. x \<in> set xs) ys) \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>; set (filter (\<lambda>x. x \<in> set xs) ys) = set xs\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* (\<And>* map I (filter (\<lambda>x. x \<in> set xs) ys) \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* map I (filter (\<lambda>x. x \<in> set xs) ys) \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace>
 2. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> set (filter (\<lambda>x. x \<in> set xs) ys) = set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>; {x \<in> set ys. x \<in> set xs} = set xs\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* (\<And>* map I xs \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* map I (filter (\<lambda>x. x \<in> set xs) ys) \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace>
 2. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> set (filter (\<lambda>x. x \<in> set xs) ys) = set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>; {x \<in> set ys. x \<in> set xs} = set xs\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* (\<And>* map I xs \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* map I xs \<and>* \<And>* map I (filter (\<lambda>s. s \<notin> set xs) ys)) \<and>* R>\<rbrace>
 2. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> set (filter (\<lambda>x. x \<in> set xs) ys) = set xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> set ys; distinct xs; distinct ys; \<And>R. \<lbrace><P \<and>* \<And>* map I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* \<And>* map I xs \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> set (filter (\<lambda>x. x \<in> set xs) ys) = set xs proof (prove)
goal:
No subgoals!