theory Retype_DP

lemma mapME_x_wp:
  "\<forall>x \<in> set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>E\<rbrace>" proof (induct xs) case Nil show ?case apply (simp add: mapME_x_def sequenceE_x_def) by wp next case Cons show ?case using Cons.prems apply (simp add: mapME_x_def sequenceE_x_def) apply (fold mapME_x_def sequenceE_x_def) including no_pre apply wp apply (rule Cons.hyps) apply fastforce apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>set []. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; \<forall>x\<in>set (a # xs). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<forall>x\<in>set []. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>

goal (2 subgoals):
 1. \<forall>x\<in>set []. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; \<forall>x\<in>set (a # xs). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk () \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<lbrace>P\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; \<forall>x\<in>set (a # xs). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; \<forall>x\<in>set (a # xs). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (state)
this:
\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
\<forall>x\<in>set (a_ # xs_). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; \<forall>x\<in>set (a # xs). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapME_x f (a_ # xs_) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
using this:
\<forall>x\<in>set (a_ # xs_). \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapME_x f (a_ # xs_) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> doE _ <- f a_;
foldr (\<lambda>x y. doE _ <- x;
y
odE) (map f xs_) (returnOk ())
odE \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> doE _ <- f a_;
mapME_x f xs_
odE \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> doE _ <- f a_;
mapME_x f xs_
odE \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>?B9 x\<rbrace> mapME_x f xs_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f a_ \<lbrace>?B9\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<and> (\<forall>x\<in>set xs_. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f a_ \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P\<rbrace> mapME_x f (a_ # xs_) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>

goal:
No subgoals!