theory Monad_Lists

lemma mapME_set:
  assumes  est: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>P\<rbrace>, -"
  and     invp: "\<And>x y. \<lbrace>R and P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>, -"
  and     invr: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>\<lambda>_. R\<rbrace>, -"
  shows "\<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. P x s\<rbrace>, -" proof (rule hoare_post_imp_R [where Q' = "\<lambda>rv s. R s \<and> (\<forall>x \<in> set rv. P x s)"], induct xs) case Nil thus ?case by (simp add: mapME_Nil | wp returnOKE_R_wp)+ next case (Cons y ys) have minvp: "\<And>x. \<lbrace>R and P x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P x\<rbrace>, -" apply (rule hoare_pre) apply (rule_tac Q' = "\<lambda>_ s. R s \<and> P x s" in hoare_post_imp_R) apply (wp mapME_wp' invr invp)+ apply simp apply simp apply simp done show ?case apply (simp add: mapME_Cons) apply (wp) apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P x s" in hoare_post_imp_R) apply (wp Cons.hyps minvp) apply simp apply (fold validE_R_def) apply simp apply (wp invr est) apply simp done qed clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. P x s\<rbrace>, - proof (state)
goal (3 subgoals):
 1. \<lbrace>R\<rbrace> mapME f [] \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 2. \<And>a xs. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - \<Longrightarrow> \<lbrace>R\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 3. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (state)
this:


goal (3 subgoals):
 1. \<lbrace>R\<rbrace> mapME f [] \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 2. \<And>a xs. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - \<Longrightarrow> \<lbrace>R\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 3. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (prove)
goal (1 subgoal):
 1. \<lbrace>R\<rbrace> mapME f [] \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - proof (state)
this:
\<lbrace>R\<rbrace> mapME f [] \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -

goal (2 subgoals):
 1. \<And>a xs. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - \<Longrightarrow> \<lbrace>R\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 2. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (state)
goal (2 subgoals):
 1. \<And>a xs. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - \<Longrightarrow> \<lbrace>R\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 2. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (state)
this:
\<lbrace>R\<rbrace> mapME f ys \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -

goal (2 subgoals):
 1. \<And>a xs. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - \<Longrightarrow> \<lbrace>R\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 2. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>R and P x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P x\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?P' x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P x\<rbrace>, -
 2. \<And>x s. (R and P x) s \<Longrightarrow> ?P' x s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P' x\<rbrace> mapME f ys \<lbrace>\<lambda>_ s. R s \<and> P x s\<rbrace>, -
 2. \<And>x rv s. R s \<and> P x s \<Longrightarrow> P x s
 3. \<And>x s. (R and P x) s \<Longrightarrow> ?P' x s proof (prove)
goal (3 subgoals):
 1. \<And>x xa s. \<lbrakk>xa \<in> set ys; R s \<and> P x s\<rbrakk> \<Longrightarrow> R s \<and> (R and P x) s
 2. \<And>x rv s. R s \<and> P x s \<Longrightarrow> P x s
 3. \<And>x s. (R and P x) s \<Longrightarrow> R s \<and> P x s proof (prove)
goal (2 subgoals):
 1. \<And>x rv s. R s \<and> P x s \<Longrightarrow> P x s
 2. \<And>x s. (R and P x) s \<Longrightarrow> R s \<and> P x s proof (prove)
goal (1 subgoal):
 1. \<And>x s. (R and P x) s \<Longrightarrow> R s \<and> P x s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>R and P ?x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P ?x\<rbrace>, -

goal (2 subgoals):
 1. \<And>a xs. \<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - \<Longrightarrow> \<lbrace>R\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -
 2. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s proof (prove)
goal (1 subgoal):
 1. \<lbrace>R\<rbrace> mapME f (y # ys) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>R\<rbrace> doE y <- f y;
ys <- mapME f ys;
returnOk (y # ys)
odE \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?P'5 x\<rbrace> mapME f ys \<lbrace>\<lambda>ys a. R a \<and> (\<forall>x\<in>set (x # ys). P x a)\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> f y \<lbrace>\<lambda>x s. True \<and> ?P'5 x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. R s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P'5 x\<rbrace> mapME f ys \<lbrace>\<lambda>xs s. (R s \<and> (\<forall>x\<in>set xs. P x s)) \<and> P x s\<rbrace>, -
 2. \<And>x rv s. (R s \<and> (\<forall>x\<in>set rv. P x s)) \<and> P x s \<Longrightarrow> R s \<and> (\<forall>x\<in>set (x # rv). P x s)
 3. \<lbrace>?P'\<rbrace> f y \<lbrace>\<lambda>x s. True \<and> ?P'5 x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. R s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. (R s \<and> (\<forall>x\<in>set rv. P x s)) \<and> P x s \<Longrightarrow> R s \<and> (\<forall>x\<in>set (x # rv). P x s)
 2. \<lbrace>?P'\<rbrace> f y \<lbrace>\<lambda>x s. True \<and> R s \<and> (R and P x) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. R s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> f y \<lbrace>\<lambda>x s. True \<and> R s \<and> (R and P x) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. R s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> f y \<lbrace>\<lambda>x s. True \<and> R s \<and> (R and P x) s\<rbrace>, -
 2. \<And>s. R s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> f y \<lbrace>\<lambda>x s. R s \<and> P x s\<rbrace>, -
 2. \<And>s. R s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. R s \<Longrightarrow> R s \<and> R s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>R\<rbrace> mapME f (y # ys) \<lbrace>\<lambda>rv s. R s \<and> (\<forall>x\<in>set rv. P x s)\<rbrace>, -

goal (1 subgoal):
 1. \<And>rv s. R s \<and> (\<forall>x\<in>set rv. P x s) \<Longrightarrow> \<forall>x\<in>set rv. P x s