theory SubMonadLib

lemma submonad_mapM_x:
  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_x m l)) = (stateAssert g [] >>= (\<lambda>u. mapM_x (sm' \<circ> m) l))" proof (induct l) case Nil thus ?case by (simp add: mapM_x_def sequence_x_def bind_def submonad.return [OF sm]) next case (Cons x xs) thus ?case using sm sm' efm apply (simp add: mapM_x_Cons) apply (simp add: bind_subst_lift [OF submonad.stateAssert_fn]) apply (simp add: bind_assoc submonad_bind submonad.return) apply (subst submonad.fn_stateAssert [OF sm']) apply (intro ext bind_apply_cong [OF refl]) apply (subgoal_tac "g st") apply (clarsimp simp: stateAssert_def bind_def get_def assert_def return_def) apply (frule(1) submonad.guard_preserved, simp) done qed

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


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

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

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

goal (1 subgoal):
 1. sm (mapM_x m (x # xs)) = do u <- stateAssert g [];
mapM_x (sm' \<circ> m) (x # xs)
od proof (prove)
using this:
sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (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_x m (x # xs)) = do u <- stateAssert g [];
mapM_x (sm' \<circ> m) (x # xs)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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;
mapM_x m xs
od) = do u <- stateAssert g [];
y <- sm' (m x);
mapM_x (\<lambda>a. sm' (m a)) xs
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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;
mapM_x m xs
od) = do y <- sm' (m x);
mapM_x (\<lambda>a. sm' (m a)) xs
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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);
u <- stateAssert g [];
mapM_x (\<lambda>a. sm' (m a)) xs
od = do y <- sm' (m x);
mapM_x (\<lambda>a. sm' (m a)) xs
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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);
mapM_x (\<lambda>a. sm' (m a)) xs
od = do y <- sm' (m x);
mapM_x (\<lambda>a. sm' (m a)) xs
od proof (prove)
goal (1 subgoal):
 1. \<And>xa rv st. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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)\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>a. sm' (m a)) xs st = mapM_x (\<lambda>a. sm' (m a)) xs st proof (prove)
goal (2 subgoals):
 1. \<And>xa rv st. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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); g st\<rbrakk> \<Longrightarrow> mapM_x (\<lambda>a. sm' (m a)) xs st = mapM_x (\<lambda>a. sm' (m a)) xs st
 2. \<And>xa rv st. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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)\<rbrakk> \<Longrightarrow> g st proof (prove)
goal (1 subgoal):
 1. \<And>xa rv st. \<lbrakk>sm (mapM_x m xs) = do u <- stateAssert g [];
mapM_x (\<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)\<rbrakk> \<Longrightarrow> g st proof (prove)
goal:
No subgoals! proof (state)
this:
sm (mapM_x m (x # xs)) = do u <- stateAssert g [];
mapM_x (sm' \<circ> m) (x # xs)
od

goal:
No subgoals!