theory MonadSep

lemma mapM_x_sep_inv':
  includes no_pre
  assumes f:
   "\<And>R x. x \<in> S \<Longrightarrow>
     \<lbrace>\<lambda>s.<P x \<and>* I \<and>* R> s \<and> I' s\<rbrace>
      f x
     \<lbrace>\<lambda>_ s.<Q x \<and>* I \<and>* R> s \<and> I' s\<rbrace>"
  shows
   "set xs \<subseteq> S \<Longrightarrow>
     \<lbrace>\<lambda>s.<\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>
      mapM_x f xs
     \<lbrace>\<lambda>_ s.<\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>" proof (induct xs arbitrary: R) case Nil thus ?case by (simp add: mapM_x_Nil) next case (Cons x xs) thus ?case apply (simp add: sep_conj_assoc mapM_x_Cons) apply (wp) apply (insert Cons.hyps [where R1="Q x ** R"])[1] apply (simp add: sep_conj_ac) apply (insert f [where R1="R ** \<And>* map P xs" and x1=x ])[1] apply (simp add: sep_conj_ac) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (state)
goal (2 subgoals):
 1. \<And>R. set [] \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P [] \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f [] \<lbrace>\<lambda>_ s. <\<And>* map Q [] \<and>* I \<and>* R> s \<and> I' s\<rbrace>
 2. \<And>a xs R. \<lbrakk>\<And>R. set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (state)
this:
set [] \<subseteq> S

goal (2 subgoals):
 1. \<And>R. set [] \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P [] \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f [] \<lbrace>\<lambda>_ s. <\<And>* map Q [] \<and>* I \<and>* R> s \<and> I' s\<rbrace>
 2. \<And>a xs R. \<lbrakk>\<And>R. set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (prove)
using this:
set [] \<subseteq> S

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. <\<And>* map P [] \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f [] \<lbrace>\<lambda>_ s. <\<And>* map Q [] \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. <\<And>* map P [] \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f [] \<lbrace>\<lambda>_ s. <\<And>* map Q [] \<and>* I \<and>* R> s \<and> I' s\<rbrace>

goal (1 subgoal):
 1. \<And>a xs R. \<lbrakk>\<And>R. set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a xs R. \<lbrakk>\<And>R. set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (state)
this:
set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* ?R1> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* ?R1> s \<and> I' s\<rbrace>
set (x # xs) \<subseteq> S

goal (1 subgoal):
 1. \<And>a xs R. \<lbrakk>\<And>R. set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (a # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (a # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (prove)
using this:
set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* ?R1> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* ?R1> s \<and> I' s\<rbrace>
set (x # xs) \<subseteq> S

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. <\<And>* map P (x # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (x # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (x # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <P x \<and>* \<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> do y <- f x;
mapM_x f xs
od \<lbrace>\<lambda>_ s. <Q x \<and>* \<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>?B4 xa\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <Q x \<and>* \<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>
 2. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <P x \<and>* \<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> f x \<lbrace>?B4\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S; set xs \<subseteq> S \<Longrightarrow> \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* Q x \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* Q x \<and>* R> s \<and> I' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B4 xa\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <Q x \<and>* \<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>
 2. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <P x \<and>* \<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> f x \<lbrace>?B4\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <P x \<and>* \<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> f x \<lbrace>\<lambda>xa s. <I \<and>* R \<and>* Q x \<and>* \<And>* map P xs> s \<and> I' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. <\<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f xs \<lbrace>\<lambda>_ s. <\<And>* map Q xs \<and>* I \<and>* R> s \<and> I' s\<rbrace>; x \<in> S \<and> set xs \<subseteq> S; x \<in> S \<Longrightarrow> \<lbrace>\<lambda>s. <P x \<and>* I \<and>* R \<and>* \<And>* map P xs> s \<and> I' s\<rbrace> f x \<lbrace>\<lambda>_ s. <Q x \<and>* I \<and>* R \<and>* \<And>* map P xs> s \<and> I' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. <P x \<and>* \<And>* map P xs \<and>* I \<and>* R> s \<and> I' s\<rbrace> f x \<lbrace>\<lambda>xa s. <I \<and>* R \<and>* Q x \<and>* \<And>* map P xs> s \<and> I' s\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. <\<And>* map P (x # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace> mapM_x f (x # xs) \<lbrace>\<lambda>_ s. <\<And>* map Q (x # xs) \<and>* I \<and>* R> s \<and> I' s\<rbrace>

goal:
No subgoals!