theory HaskellLemmaBucket

lemma findM_is_mapME:
  "(findM f xs >>= g)
   = liftM (\<lambda>_. ())
      (doE ys \<leftarrow> mapME_x (\<lambda>x. do v \<leftarrow> f x;
                             if v then do g (Some x); throwError () od
                             else returnOk () od) xs;
              liftE (g None) odE)" apply (induct xs) apply (simp add: mapME_x_def sequenceE_x_def liftM_def returnOk_bind) apply (simp add: liftE_def) apply (simp add: mapME_x_Cons bindE_assoc liftE_bindE[symmetric]
                   liftM_def cong: if_cong) apply (simp add: liftE_bindE bind_assoc) apply (rule bind_cong[OF refl]) apply (simp add: bindE_assoc split: if_split) apply (simp add: liftE_bindE bind_assoc throwError_bind) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. findM f xs >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) xs;
liftE (g None)
odE) proof (prove)
goal (2 subgoals):
 1. findM f [] >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) [];
liftE (g None)
odE)
 2. \<And>a xs. findM f xs >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) xs;
liftE (g None)
odE) \<Longrightarrow> findM f (a # xs) >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) (a # xs);
liftE (g None)
odE) proof (prove)
goal (2 subgoals):
 1. g None = do x <- liftE (g None);
return ()
od
 2. \<And>a xs. findM f xs >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) xs;
liftE (g None)
odE) \<Longrightarrow> findM f (a # xs) >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) (a # xs);
liftE (g None)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. findM f xs >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) xs;
liftE (g None)
odE) \<Longrightarrow> findM f (a # xs) >>= g = liftM (\<lambda>_. ()) (doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then do g (Some x);
throwError ()
od else returnOk ()
od) (a # xs);
liftE (g None)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. findM f xs >>= g = do x <- doE ys <- mapME_x (\<lambda>x. doE v <- liftE (f x);
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
odE) xs;
liftE (g None)
odE;
return ()
od \<Longrightarrow> do r <- f a;
if r then return (Some a) else findM f xs
od >>= g = do x <- doE x <- liftE (f a);
x <- if x then liftE (g (Some a)) >>=E throwError else returnOk ();
ys <- mapME_x (\<lambda>x. doE v <- liftE (f x);
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
odE) xs;
liftE (g None)
odE;
return ()
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs. findM f xs >>= g = do x <- doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
od) xs;
liftE (g None)
odE;
return ()
od \<Longrightarrow> do x <- f a;
(if x then return (Some a) else findM f xs) >>= g
od = do x <- f a;
x <- doE x <- if x then liftE (g (Some a)) >>=E throwError else returnOk ();
ys <- mapME_x (\<lambda>x. do v <- f x;
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
od) xs;
liftE (g None)
odE;
return ()
od proof (prove)
goal (1 subgoal):
 1. \<And>a xs v s s'. \<lbrakk>findM f xs >>= g = do x <- doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
od) xs;
liftE (g None)
odE;
return ()
od; (v, s') \<in> fst (f a s)\<rbrakk> \<Longrightarrow> ((if v then return (Some a) else findM f xs) >>= g) s' = (do x <- doE x <- if v then liftE (g (Some a)) >>=E throwError else returnOk ();
ys <- mapME_x (\<lambda>x. do v <- f x;
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
od) xs;
liftE (g None)
odE;
return ()
od) s' proof (prove)
goal (1 subgoal):
 1. \<And>a xs v s s'. \<lbrakk>findM f xs >>= g = do x <- doE ys <- mapME_x (\<lambda>x. do v <- f x;
if v then liftE (g (Some x)) >>=E throwError else returnOk ()
od) xs;
liftE (g None)
odE;
return ()
od; (v, s') \<in> fst (f a s)\<rbrakk> \<Longrightarrow> v \<longrightarrow> g (Some a) s' = (do x <- liftE (g (Some a)) >>=E throwError;
return ()
od) s' proof (prove)
goal:
No subgoals!