theory MonadSep

lemma sep_set_conj_subset_wp:
  "\<lbrakk>xs \<subseteq> ys; finite xs; finite ys;
   \<And>R. \<lbrace><P \<and>* (\<And>* x \<in> xs. I x) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> xs. I x) \<and>* R>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace><P \<and>* (\<And>* x \<in> ys. I x) \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> ys. I x) \<and>* R>\<rbrace>" apply (subst sep_map_set_conj_restrict [where t="\<lambda>x. x \<in> xs" and xs=ys], assumption) apply (subst sep_map_set_conj_restrict [where t="\<lambda>x. x \<in> xs" and xs=ys], assumption) apply (subgoal_tac "{x \<in> ys. x \<in> xs} = xs") apply (clarsimp simp: sep_conj_assoc) apply auto done

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