theory Monad_Lists

lemma no_fail_mapM_wp:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> no_fail (P x) (f x)"
  assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>"
  shows "no_fail (\<lambda>s. \<forall>x \<in> set xs. P x s) (mapM f xs)" using assms proof (induct xs) case Nil thus ?case by (simp add: mapM_empty) next case (Cons z zs) show ?case apply (clarsimp simp: mapM_Cons) apply (wp Cons.prems Cons.hyps hoare_vcg_const_Ball_lift|simp)+ done qed

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

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

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

goal (1 subgoal):
 1. no_fail (\<lambda>s. \<forall>x\<in>set []. P x s) (mapM f []) proof (state)
this:
no_fail (\<lambda>s. \<forall>x\<in>set []. P x s) (mapM f [])

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

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> no_fail (P x) (f x); \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs\<rbrakk> \<Longrightarrow> \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<forall>x\<in>set xs. P x s) (mapM f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> no_fail (P x) (f x); \<And>x y. \<lbrakk>x \<in> set (a # xs); y \<in> set (a # xs)\<rbrakk> \<Longrightarrow> \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<forall>x\<in>set (a # xs). P x s) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. \<forall>x\<in>set (z # zs). P x s) (mapM f (z # zs)) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. P z s \<and> (\<forall>x\<in>set zs. P x s)) (do y <- f z;
ys <- mapM f zs;
return (y # ys)
od) proof (prove)
goal:
No subgoals! proof (state)
this:
no_fail (\<lambda>s. \<forall>x\<in>set (z # zs). P x s) (mapM f (z # zs))

goal:
No subgoals!