kings-crown/FVELER_Isabelle huggingface dataset:
theory Monad_Lists

lemma mapME_x_sequenceE:
  "mapME_x f xs \<equiv> doE _ \<leftarrow> sequenceE (map f xs); returnOk () odE" apply (induct xs, simp_all add: mapME_x_def sequenceE_def sequenceE_x_def) apply (simp add: Let_def bindE_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f xs \<equiv> doE _ <- sequenceE (map f xs);
returnOk ()
odE proof (prove)
goal (1 subgoal):
 1. \<And>a xs. foldr (\<lambda>x y. doE _ <- x;
y
odE) (map f xs) (returnOk ()) = doE _ <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map f xs) (returnOk []);
returnOk ()
odE \<Longrightarrow> doE _ <- f a;
_ <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map f xs) (returnOk []);
returnOk ()
odE = doE _ <- doE x <- f a;
y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map f xs) (returnOk []);
returnOk (x # y)
odE;
returnOk ()
odE proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma sequenceE_Cons:
  "sequenceE (x # xs) = (doE v \<leftarrow> x; vs \<leftarrow> sequenceE xs; returnOk (v # vs) odE)" by (simp add: sequenceE_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sequenceE (x # xs) = doE v <- x;
vs <- sequenceE xs;
returnOk (v # vs)
odE
theory Monad_Lists

lemma zipWithM_Nil [simp]:
  "zipWithM f xs [] = return []" by (simp add: zipWithM_def zipWith_def sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM f xs [] = return []
theory Monad_Lists

lemma zipWithM_One:
  "zipWithM f (x#xs) [a] = (do z \<leftarrow> f x a; return [z] od)" by (simp add: zipWithM_def zipWith_def sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM f (x # xs) [a] = do z <- f x a;
return [z]
od
theory Monad_Lists

lemma zipWithM_x_Nil[simp]:
  "zipWithM_x f xs [] = return ()" by (simp add: zipWithM_x_def zipWith_def sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x f xs [] = return ()
theory Monad_Lists

lemma zipWithM_x_One:
  "zipWithM_x f (x#xs) [a] = f x a" by (simp add: zipWithM_x_def zipWith_def sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x f (x # xs) [a] = f x a
theory Monad_Lists

lemma mapM_last_Cons:
  "\<lbrakk> xs = [] \<Longrightarrow> g v = y;
     xs \<noteq> [] \<Longrightarrow> do x \<leftarrow> f (last xs); return (g x) od
             = do x \<leftarrow> f (last xs); return y od \<rbrakk> \<Longrightarrow>
   do ys \<leftarrow> mapM f xs; return (g (last (v # ys))) od = do mapM_x f xs; return y od" apply (cases "xs = []") apply (simp add: mapM_x_Nil mapM_Nil) apply (simp add: mapM_x_mapM) apply (subst append_butlast_last_id[symmetric], assumption,
         subst mapM_append)+ apply (simp add: bind_assoc mapM_Cons mapM_Nil) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = [] \<Longrightarrow> g v = y; xs \<noteq> [] \<Longrightarrow> do x <- f (last xs);
return (g x)
od = do x <- f (last xs);
return y
od\<rbrakk> \<Longrightarrow> do ys <- mapM f xs;
return (g (last (v # ys)))
od = do mapM_x f xs;
return y
od proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xs = [] \<Longrightarrow> g v = y; xs \<noteq> [] \<Longrightarrow> do x <- f (last xs);
return (g x)
od = do x <- f (last xs);
return y
od; xs = []\<rbrakk> \<Longrightarrow> do ys <- mapM f xs;
return (g (last (v # ys)))
od = do mapM_x f xs;
return y
od
 2. \<lbrakk>xs = [] \<Longrightarrow> g v = y; xs \<noteq> [] \<Longrightarrow> do x <- f (last xs);
return (g x)
od = do x <- f (last xs);
return y
od; xs \<noteq> []\<rbrakk> \<Longrightarrow> do ys <- mapM f xs;
return (g (last (v # ys)))
od = do mapM_x f xs;
return y
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = [] \<Longrightarrow> g v = y; xs \<noteq> [] \<Longrightarrow> do x <- f (last xs);
return (g x)
od = do x <- f (last xs);
return y
od; xs \<noteq> []\<rbrakk> \<Longrightarrow> do ys <- mapM f xs;
return (g (last (v # ys)))
od = do mapM_x f xs;
return y
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>do x <- f (last xs);
return (g x)
od = do x <- f (last xs);
return y
od; xs \<noteq> []\<rbrakk> \<Longrightarrow> do ys <- mapM f xs;
return (g (if ys = [] then v else last ys))
od = do x <- mapM f xs;
return y
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>do x <- f (last xs);
return (g x)
od = do x <- f (last xs);
return y
od; xs \<noteq> []\<rbrakk> \<Longrightarrow> do ys <- do x <- mapM f (butlast xs);
y <- mapM f [last xs];
return (x @ y)
od;
return (g (if ys = [] then v else last ys))
od = do x <- do x <- mapM f (butlast xs);
y <- mapM f [last xs];
return (x @ y)
od;
return y
od proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma map_length_cong:
  "\<lbrakk> length xs = length ys; \<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x = g y \<rbrakk>
     \<Longrightarrow> map f xs = map g ys" apply atomize apply (erule rev_mp, erule list_induct2) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; \<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x = g y\<rbrakk> \<Longrightarrow> map f xs = map g ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; \<forall>x y. (x, y) \<in> set (zip xs ys) \<longrightarrow> f x = g y\<rbrakk> \<Longrightarrow> map f xs = map g ys proof (prove)
goal (2 subgoals):
 1. (\<forall>x y. (x, y) \<in> set (zip [] []) \<longrightarrow> f x = g y) \<longrightarrow> map f [] = map g []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; (\<forall>x y. (x, y) \<in> set (zip xs ys) \<longrightarrow> f x = g y) \<longrightarrow> map f xs = map g ys\<rbrakk> \<Longrightarrow> (\<forall>xa ya. (xa, ya) \<in> set (zip (x # xs) (y # ys)) \<longrightarrow> f xa = g ya) \<longrightarrow> map f (x # xs) = map g (y # ys) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_length_cong:
  "\<lbrakk> length xs = length ys; \<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x = g y \<rbrakk>
   \<Longrightarrow> mapM f xs = mapM g ys" by (simp add: mapM_def map_length_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; \<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x = g y\<rbrakk> \<Longrightarrow> mapM f xs = mapM g ys
theory Monad_Lists

lemma zipWithM_mapM:
  "zipWithM f xs ys = mapM (case_prod f) (zip xs ys)" by (simp add: zipWithM_def zipWith_def mapM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM f xs ys = mapM (\<lambda>(x, y). f x y) (zip xs ys)
theory Monad_Lists

lemma zip_take_triv2:
  "length as \<le> n \<Longrightarrow> zip as (take n bs) = zip as bs" apply (induct as arbitrary: n bs; simp) apply (case_tac n; simp) apply (case_tac bs; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length as \<le> n \<Longrightarrow> zip as (take n bs) = zip as bs proof (prove)
goal (1 subgoal):
 1. \<And>a as n bs. \<lbrakk>\<And>n bs. length as \<le> n \<Longrightarrow> zip as (take n bs) = zip as bs; Suc (length as) \<le> n\<rbrakk> \<Longrightarrow> zip (a # as) (take n bs) = zip (a # as) bs proof (prove)
goal (1 subgoal):
 1. \<And>a as n bs nat. \<lbrakk>\<And>n bs. length as \<le> n \<Longrightarrow> zip as (take n bs) = zip as bs; length as \<le> nat; n = Suc nat\<rbrakk> \<Longrightarrow> zip (a # as) (take (Suc nat) bs) = zip (a # as) bs proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_discarded:
  "mapM f xs >>= (\<lambda>ys. g) = mapM_x f xs >>= (\<lambda>_. g)" by (simp add: mapM_x_mapM)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do ys <- mapM f xs;
g
od = do _ <- mapM_x f xs;
g
od
theory Monad_Lists

lemma mapM_x_map:
  "mapM_x f (map g xs) = mapM_x (\<lambda>x. f (g x)) xs" by (simp add: mapM_x_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f (map g xs) = mapM_x (\<lambda>x. f (g x)) xs
theory Monad_Lists

lemma filterM_append:
  "filterM f (xs @ ys) = do
     xs' \<leftarrow> filterM f xs;
     ys' \<leftarrow> filterM f ys;
     return (xs' @ ys')
   od" apply (induct xs) apply simp apply (simp add: bind_assoc) apply (rule ext bind_apply_cong [OF refl])+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. filterM f (xs @ ys) = do xs' <- filterM f xs;
ys' <- filterM f ys;
return (xs' @ ys')
od proof (prove)
goal (2 subgoals):
 1. filterM f ([] @ ys) = do xs' <- filterM f [];
ys' <- filterM f ys;
return (xs' @ ys')
od
 2. \<And>a xs. filterM f (xs @ ys) = do xs' <- filterM f xs;
ys' <- filterM f ys;
return (xs' @ ys')
od \<Longrightarrow> filterM f ((a # xs) @ ys) = do xs' <- filterM f (a # xs);
ys' <- filterM f ys;
return (xs' @ ys')
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. filterM f (xs @ ys) = do xs' <- filterM f xs;
ys' <- filterM f ys;
return (xs' @ ys')
od \<Longrightarrow> filterM f ((a # xs) @ ys) = do xs' <- filterM f (a # xs);
ys' <- filterM f ys;
return (xs' @ ys')
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. filterM f (xs @ ys) = do xs' <- filterM f xs;
ys' <- filterM f ys;
return (xs' @ ys')
od \<Longrightarrow> do b <- f a;
x <- filterM f xs;
ys' <- filterM f ys;
return (if b then a # x @ ys' else x @ ys')
od = do x <- f a;
ysa <- filterM f xs;
ys' <- filterM f ys;
return ((if x then a # ysa else ysa) @ ys')
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs x rv st rva sta rvb stb. \<lbrakk>filterM f (xs @ ys) = do xs' <- filterM f xs;
ys' <- filterM f ys;
return (xs' @ ys')
od; (rv, st) \<in> fst (f a x); (rva, sta) \<in> fst (filterM f xs st); (rvb, stb) \<in> fst (filterM f ys sta)\<rbrakk> \<Longrightarrow> return (if rv then a # rva @ rvb else rva @ rvb) stb = return ((if rv then a # rva else rva) @ rvb) stb proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma filterM_mapM:
  "filterM f xs = do
     ys \<leftarrow> mapM (\<lambda>x. do v \<leftarrow> f x; return (x, v) od) xs;
     return (map fst (filter snd ys))
   od" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons bind_assoc) apply (rule bind_cong [OF refl] bind_apply_cong[OF refl])+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. filterM f xs = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (map fst (filter snd ys))
od proof (prove)
goal (2 subgoals):
 1. filterM f [] = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) [];
return (map fst (filter snd ys))
od
 2. \<And>a xs. filterM f xs = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (map fst (filter snd ys))
od \<Longrightarrow> filterM f (a # xs) = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) (a # xs);
return (map fst (filter snd ys))
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. filterM f xs = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (map fst (filter snd ys))
od \<Longrightarrow> filterM f (a # xs) = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) (a # xs);
return (map fst (filter snd ys))
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. filterM f xs = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (map fst (filter snd ys))
od \<Longrightarrow> do b <- f a;
ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (if b then a # map fst (filter snd ys) else map fst (filter snd ys))
od = do x <- f a;
ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (map fst (if x then (a, x) # filter snd ys else filter snd ys))
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs v s s' rv st. \<lbrakk>filterM f xs = do ys <- mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs;
return (map fst (filter snd ys))
od; (v, s') \<in> fst (f a s); (rv, st) \<in> fst (mapM (\<lambda>x. do v <- f x;
return (x, v)
od) xs s')\<rbrakk> \<Longrightarrow> return (if v then a # map fst (filter snd rv) else map fst (filter snd rv)) st = return (map fst (if v then (a, v) # filter snd rv else filter snd rv)) st proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_gets:
  assumes P: "\<And>x. m x = gets (f x)"
  shows      "mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs)" proof (induct xs) case Nil show ?case by (simp add: mapM_def sequence_def gets_def get_def bind_def) next case (Cons y ys) thus ?case by (simp add: mapM_Cons P simpler_gets_def return_def bind_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs) proof (state)
goal (2 subgoals):
 1. mapM m [] = gets (\<lambda>s. map (\<lambda>x. f x s) [])
 2. \<And>a xs. mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs) \<Longrightarrow> mapM m (a # xs) = gets (\<lambda>s. map (\<lambda>x. f x s) (a # xs)) proof (state)
this:


goal (2 subgoals):
 1. mapM m [] = gets (\<lambda>s. map (\<lambda>x. f x s) [])
 2. \<And>a xs. mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs) \<Longrightarrow> mapM m (a # xs) = gets (\<lambda>s. map (\<lambda>x. f x s) (a # xs)) proof (prove)
goal (1 subgoal):
 1. mapM m [] = gets (\<lambda>s. map (\<lambda>x. f x s) []) proof (state)
this:
mapM m [] = gets (\<lambda>s. map (\<lambda>x. f x s) [])

goal (1 subgoal):
 1. \<And>a xs. mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs) \<Longrightarrow> mapM m (a # xs) = gets (\<lambda>s. map (\<lambda>x. f x s) (a # xs)) proof (state)
goal (1 subgoal):
 1. \<And>a xs. mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs) \<Longrightarrow> mapM m (a # xs) = gets (\<lambda>s. map (\<lambda>x. f x s) (a # xs)) proof (state)
this:
mapM m ys = gets (\<lambda>s. map (\<lambda>x. f x s) ys)

goal (1 subgoal):
 1. \<And>a xs. mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs) \<Longrightarrow> mapM m (a # xs) = gets (\<lambda>s. map (\<lambda>x. f x s) (a # xs)) proof (prove)
using this:
mapM m ys = gets (\<lambda>s. map (\<lambda>x. f x s) ys)

goal (1 subgoal):
 1. mapM m (y # ys) = gets (\<lambda>s. map (\<lambda>x. f x s) (y # ys)) proof (state)
this:
mapM m (y # ys) = gets (\<lambda>s. map (\<lambda>x. f x s) (y # ys))

goal:
No subgoals!
theory Monad_Lists

lemma mapM_map_simp:
  "mapM m (map f xs) = mapM (m \<circ> f) xs" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM m (map f xs) = mapM (m \<circ> f) xs proof (prove)
goal (2 subgoals):
 1. mapM m (map f []) = mapM (m \<circ> f) []
 2. \<And>a xs. mapM m (map f xs) = mapM (m \<circ> f) xs \<Longrightarrow> mapM m (map f (a # xs)) = mapM (m \<circ> f) (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. mapM m (map f xs) = mapM (m \<circ> f) xs \<Longrightarrow> mapM m (map f (a # xs)) = mapM (m \<circ> f) (a # xs) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma filterM_voodoo:
  "\<forall>ys. P ys (do zs \<leftarrow> filterM m xs; return (ys @ zs) od)
       \<Longrightarrow> P [] (filterM m xs)" by (drule spec[where x=Nil], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. P ys (do zs <- filterM m xs;
return (ys @ zs)
od) \<Longrightarrow> P [] (filterM m xs)
theory Monad_Lists

lemma mapME_x_Cons:
  "mapME_x f (x # xs) = (doE f x; mapME_x f xs odE)" by (simp add: mapME_x_def sequenceE_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f (x # xs) = doE f x;
mapME_x f xs
odE
theory Monad_Lists

lemma liftME_map_mapME:
  "liftME (map f) (mapME m xs)
      = mapME (liftME f o m) xs" apply (rule sym) apply (induct xs) apply (simp add: liftME_def mapME_Nil) apply (simp add: mapME_Cons liftME_def bindE_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftME (map f) (mapME m xs) = mapME (liftME f \<circ> m) xs proof (prove)
goal (1 subgoal):
 1. mapME (liftME f \<circ> m) xs = liftME (map f) (mapME m xs) proof (prove)
goal (2 subgoals):
 1. mapME (liftME f \<circ> m) [] = liftME (map f) (mapME m [])
 2. \<And>a xs. mapME (liftME f \<circ> m) xs = liftME (map f) (mapME m xs) \<Longrightarrow> mapME (liftME f \<circ> m) (a # xs) = liftME (map f) (mapME m (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. mapME (liftME f \<circ> m) xs = liftME (map f) (mapME m xs) \<Longrightarrow> mapME (liftME f \<circ> m) (a # xs) = liftME (map f) (mapME m (a # xs)) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapM_x_split_append:
  "mapM_x f xs = do _ \<leftarrow> mapM_x f (take n xs); mapM_x f (drop n xs) od" using mapM_x_append[where f=f and xs="take n xs" and ys="drop n xs"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f xs = do _ <- mapM_x f (take n xs);
mapM_x f (drop n xs)
od proof (prove)
using this:
mapM_x f (take n xs @ drop n xs) = do x <- mapM_x f (take n xs);
y <- mapM_x f (drop n xs);
return ()
od

goal (1 subgoal):
 1. mapM_x f xs = do _ <- mapM_x f (take n xs);
mapM_x f (drop n xs)
od
theory Monad_Lists

lemma mapME_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>"
  shows      "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>" apply (induct xs) apply (simp add: mapME_def sequenceE_def) apply wp apply simp apply (simp add: mapME_Cons) apply (wp x|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f [] \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> returnOk [] \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>; a \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>; a \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE y <- f a;
ys <- mapME f xs;
returnOk (y # ys)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma mapME_x_inv_wp:
  assumes x: "\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>E\<rbrace>"
  shows      "\<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>E\<rbrace>" apply (induct xs) apply (simp add: mapME_x_def sequenceE_x_def) apply wp apply (simp add: mapME_x_def sequenceE_x_def) apply (fold mapME_x_def sequenceE_x_def) apply wp apply (rule x) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> mapME_x f [] \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> returnOk () \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f (a # xs) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>P\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map f xs) (returnOk ()) \<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. \<And>a xs. \<lbrace>P\<rbrace> mapME_x f xs \<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>a xs. \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>?Q6 a xs\<rbrace> f a \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q6 a xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma no_fail_mapM:
  "\<forall>x. no_fail \<top> (f x) \<Longrightarrow> no_fail \<top> (mapM f xs)" apply (induct xs) apply (simp add: mapM_def sequence_def) apply (simp add: mapM_Cons) apply (wp|fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. no_fail (\<lambda>_. True) (f x) \<Longrightarrow> no_fail (\<lambda>_. True) (mapM f xs) proof (prove)
goal (2 subgoals):
 1. \<forall>x. no_fail (\<lambda>_. True) (f x) \<Longrightarrow> no_fail (\<lambda>_. True) (mapM f [])
 2. \<And>a xs. \<lbrakk>\<forall>x. no_fail (\<lambda>_. True) (f x) \<Longrightarrow> no_fail (\<lambda>_. True) (mapM f xs); \<forall>x. no_fail (\<lambda>_. True) (f x)\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x. no_fail (\<lambda>_. True) (f x) \<Longrightarrow> no_fail (\<lambda>_. True) (mapM f xs); \<forall>x. no_fail (\<lambda>_. True) (f x)\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>no_fail (\<lambda>_. True) (mapM f xs); \<forall>x. no_fail (\<lambda>_. True) (f x)\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (do y <- f a;
ys <- mapM f xs;
return (y # ys)
od) proof (prove)
goal:
No subgoals!
theory Monad_Lists

lemma filterM_subset:
  "\<lbrace>\<top>\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. set rv \<subseteq> set xs\<rbrace>" by (rule hoare_chain, rule filterM_distinct1[where P=False], simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. set rv \<subseteq> set xs\<rbrace>