theory Monad_Lists

lemma mapM_set:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>"
  assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>"
  shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x \<in> set xs. Q x s\<rbrace>" using assms proof (induct xs) case Nil show ?case by (simp add: mapM_def sequence_def) wp next case (Cons y ys) have PQ_inv: "\<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. P and Q y\<rbrace>" by (wpsimp wp: Cons) show ?case apply (simp add: mapM_Cons) apply wp apply (rule hoare_vcg_conj_lift) apply (rule hoare_strengthen_post) apply (rule mapM_wp') apply (erule PQ_inv) apply simp apply (wp Cons|simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace> proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>_. P\<rbrace>
?x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>_. Q ?x\<rbrace>
\<lbrakk>?x \<in> set xs; ?y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q ?y\<rbrace> f ?x \<lbrace>\<lambda>_. Q ?y\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace> proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set []\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f [] \<lbrace>\<lambda>_ s. \<forall>x\<in>set []. Q x s\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (a # xs). Q x s\<rbrace> proof (state)
this:
?x \<in> set [] \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>_. P\<rbrace>
?x \<in> set [] \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>_. Q ?x\<rbrace>
\<lbrakk>?x \<in> set []; ?y \<in> set []\<rbrakk> \<Longrightarrow> \<lbrace>P and Q ?y\<rbrace> f ?x \<lbrace>\<lambda>_. Q ?y\<rbrace>

goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set [] \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set []\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f [] \<lbrace>\<lambda>_ s. \<forall>x\<in>set []. Q x s\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (a # xs). Q x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM f [] \<lbrace>\<lambda>_ s. \<forall>x\<in>set []. Q x s\<rbrace> proof (state)
this:
\<lbrace>P\<rbrace> mapM f [] \<lbrace>\<lambda>_ s. \<forall>x\<in>set []. Q x s\<rbrace>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (a # xs). Q x s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (a # xs). Q x s\<rbrace> proof (state)
this:
\<lbrakk>\<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f ys \<lbrace>\<lambda>_ s. \<forall>x\<in>set ys. Q x s\<rbrace>
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>_. P\<rbrace>
?x \<in> set (y # ys) \<Longrightarrow> \<lbrace>P\<rbrace> f ?x \<lbrace>\<lambda>_. Q ?x\<rbrace>
\<lbrakk>?x \<in> set (y # ys); ?y \<in> set (y # ys)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q ?y\<rbrace> f ?x \<lbrace>\<lambda>_. Q ?y\<rbrace>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (a # xs). Q x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. P and Q y\<rbrace> proof (state)
this:
?x \<in> set ys \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f ?x \<lbrace>\<lambda>_. P and Q y\<rbrace>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x\<in>set xs. Q x s\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>; \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f (a # xs) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (a # xs). Q x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM f (y # ys) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (y # ys). Q x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do y <- f y;
ys <- mapM f ys;
return (y # ys)
od \<lbrace>\<lambda>_ s. Q y s \<and> (\<forall>x\<in>set ys. Q x s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B10 x\<rbrace> mapM f ys \<lbrace>\<lambda>ysa a. Q y a \<and> (\<forall>x\<in>set ys. Q x a)\<rbrace>
 2. \<lbrace>?Q9\<rbrace> f y \<lbrace>?B10\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P13 x\<rbrace> mapM f ys \<lbrace>\<lambda>rv. Q y\<rbrace>
 2. \<And>x. \<lbrace>?P'13 x\<rbrace> mapM f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. Q x s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. ?P13 x s \<and> ?P'13 x s\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ?Q9 s proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrace>?P13 x\<rbrace> mapM f ys \<lbrace>?Q16 x\<rbrace>
 2. \<And>x rv s. ?Q16 x rv s \<Longrightarrow> Q y s
 3. \<And>x. \<lbrace>?P'13 x\<rbrace> mapM f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. Q x s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. ?P13 x s \<and> ?P'13 x s\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?Q9 s proof (prove)
goal (5 subgoals):
 1. \<And>x xa. xa \<in> set ys \<Longrightarrow> \<lbrace>?P13 x\<rbrace> f xa \<lbrace>\<lambda>rv. ?P13 x\<rbrace>
 2. \<And>x rv s. ?P13 x s \<Longrightarrow> Q y s
 3. \<And>x. \<lbrace>?P'13 x\<rbrace> mapM f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. Q x s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. ?P13 x s \<and> ?P'13 x s\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?Q9 s proof (prove)
goal (4 subgoals):
 1. \<And>x rv s. (P and Q y) s \<Longrightarrow> Q y s
 2. \<And>x. \<lbrace>?P'13 x\<rbrace> mapM f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. Q x s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. (P and Q y) s \<and> ?P'13 x s\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ?Q9 s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P'13 x\<rbrace> mapM f ys \<lbrace>\<lambda>rv s. \<forall>x\<in>set ys. Q x s\<rbrace>
 2. \<lbrace>?Q9\<rbrace> f y \<lbrace>\<lambda>x s. (P and Q y) s \<and> ?P'13 x s\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q9 s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P\<rbrace> mapM f (y # ys) \<lbrace>\<lambda>_ s. \<forall>x\<in>set (y # ys). Q x s\<rbrace>

goal:
No subgoals!