theory SubMonadLib

lemma submonad_mapM:
  assumes sm: "submonad f r g sm" and sm': "submonad f r g sm'"
  assumes efm: "\<And>x. empty_fail (m x)"
  shows
  "(sm (mapM m l)) = (stateAssert g [] >>= (\<lambda>u. mapM (sm' \<circ> m) l))" proof (induct l) case Nil thus ?case by (simp add: mapM_def sequence_def bind_def submonad.return [OF sm]) next case (Cons x xs) thus ?case using sm sm' efm apply (simp add: mapM_Cons) apply (simp add: bind_subst_lift [OF submonad.stateAssert_fn]) apply (simp add: bind_assoc submonad_bind submonad.return empty_fail_cond) apply (subst submonad.fn_stateAssert [OF sm']) apply (intro ext bind_apply_cong [OF refl]) apply (subgoal_tac "g sta") apply (clarsimp simp: stateAssert_def bind_def get_def assert_def return_def) apply (frule(1) submonad.guard_preserved) apply (erule(1) submonad.mapM_guard_preserved, fastforce simp: o_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sm (mapM m l) = do u <- stateAssert g [];
mapM (sm' \<circ> m) l
od proof (state)
goal (2 subgoals):
 1. sm (mapM m []) = do u <- stateAssert g [];
mapM (sm' \<circ> m) []
od
 2. \<And>a l. sm (mapM m l) = do u <- stateAssert g [];
mapM (sm' \<circ> m) l
od \<Longrightarrow> sm (mapM m (a # l)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (a # l)
od proof (state)
this:


goal (2 subgoals):
 1. sm (mapM m []) = do u <- stateAssert g [];
mapM (sm' \<circ> m) []
od
 2. \<And>a l. sm (mapM m l) = do u <- stateAssert g [];
mapM (sm' \<circ> m) l
od \<Longrightarrow> sm (mapM m (a # l)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (a # l)
od proof (prove)
goal (1 subgoal):
 1. sm (mapM m []) = do u <- stateAssert g [];
mapM (sm' \<circ> m) []
od proof (state)
this:
sm (mapM m []) = do u <- stateAssert g [];
mapM (sm' \<circ> m) []
od

goal (1 subgoal):
 1. \<And>a l. sm (mapM m l) = do u <- stateAssert g [];
mapM (sm' \<circ> m) l
od \<Longrightarrow> sm (mapM m (a # l)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (a # l)
od proof (state)
goal (1 subgoal):
 1. \<And>a l. sm (mapM m l) = do u <- stateAssert g [];
mapM (sm' \<circ> m) l
od \<Longrightarrow> sm (mapM m (a # l)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (a # l)
od proof (state)
this:
sm (mapM m xs) = do u <- stateAssert g [];
mapM (sm' \<circ> m) xs
od

goal (1 subgoal):
 1. \<And>a l. sm (mapM m l) = do u <- stateAssert g [];
mapM (sm' \<circ> m) l
od \<Longrightarrow> sm (mapM m (a # l)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (a # l)
od proof (prove)
using this:
sm (mapM m xs) = do u <- stateAssert g [];
mapM (sm' \<circ> m) xs
od

goal (1 subgoal):
 1. sm (mapM m (x # xs)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (x # xs)
od proof (prove)
using this:
sm (mapM m xs) = do u <- stateAssert g [];
mapM (sm' \<circ> m) xs
od
submonad f r g sm
submonad f r g sm'
empty_fail (m ?x)

goal (1 subgoal):
 1. sm (mapM m (x # xs)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (x # xs)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x)\<rbrakk> \<Longrightarrow> sm (do y <- m x;
ys <- mapM m xs;
return (y # ys)
od) = do u <- stateAssert g [];
y <- sm' (m x);
ys <- mapM (\<lambda>a. sm' (m a)) xs;
return (y # ys)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x)\<rbrakk> \<Longrightarrow> sm (do y <- m x;
ys <- mapM m xs;
return (y # ys)
od) = do y <- sm' (m x);
ys <- mapM (\<lambda>a. sm' (m a)) xs;
return (y # ys)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x)\<rbrakk> \<Longrightarrow> do rv <- sm' (m x);
x <- stateAssert g [];
rva <- mapM (\<lambda>a. sm' (m a)) xs;
u <- stateAssert g [];
return (rv # rva)
od = do y <- sm' (m x);
ys <- mapM (\<lambda>a. sm' (m a)) xs;
return (y # ys)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x)\<rbrakk> \<Longrightarrow> do rv <- sm' (m x);
rva <- mapM (\<lambda>a. sm' (m a)) xs;
u <- stateAssert g [];
return (rv # rva)
od = do y <- sm' (m x);
ys <- mapM (\<lambda>a. sm' (m a)) xs;
return (y # ys)
od proof (prove)
goal (1 subgoal):
 1. \<And>xa rv st rva sta. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x); (rv, st) \<in> fst (sm' (m x) xa); (rva, sta) \<in> fst (mapM (\<lambda>a. sm' (m a)) xs st)\<rbrakk> \<Longrightarrow> (do u <- stateAssert g [];
return (rv # rva)
od) sta = return (rv # rva) sta proof (prove)
goal (2 subgoals):
 1. \<And>xa rv st rva sta. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x); (rv, st) \<in> fst (sm' (m x) xa); (rva, sta) \<in> fst (mapM (\<lambda>a. sm' (m a)) xs st); g sta\<rbrakk> \<Longrightarrow> (do u <- stateAssert g [];
return (rv # rva)
od) sta = return (rv # rva) sta
 2. \<And>xa rv st rva sta. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x); (rv, st) \<in> fst (sm' (m x) xa); (rva, sta) \<in> fst (mapM (\<lambda>a. sm' (m a)) xs st)\<rbrakk> \<Longrightarrow> g sta proof (prove)
goal (1 subgoal):
 1. \<And>xa rv st rva sta. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x); (rv, st) \<in> fst (sm' (m x) xa); (rva, sta) \<in> fst (mapM (\<lambda>a. sm' (m a)) xs st)\<rbrakk> \<Longrightarrow> g sta proof (prove)
goal (1 subgoal):
 1. \<And>xa rv st rva sta. \<lbrakk>sm (mapM m xs) = do u <- stateAssert g [];
mapM (\<lambda>a. sm' (m a)) xs
od; submonad f r g sm; submonad f r g sm'; \<And>x. empty_fail (m x); (rv, st) \<in> fst (sm' (m x) xa); (rva, sta) \<in> fst (mapM (\<lambda>a. sm' (m a)) xs st); g st\<rbrakk> \<Longrightarrow> g sta proof (prove)
goal:
No subgoals! proof (state)
this:
sm (mapM m (x # xs)) = do u <- stateAssert g [];
mapM (sm' \<circ> m) (x # xs)
od

goal:
No subgoals!