theory SubMonadLib

lemma submonad_bind:
  "\<lbrakk> submonad f r g m; submonad f r g m'; submonad f r g m'';
     empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow>
   m (a >>= b) = (m' a) >>= (\<lambda>rv. m'' (b rv))" apply (subst submonad.fn_is_sm, assumption)+ apply (clarsimp simp: submonad_def bind_assoc split_def submonad_fn_def) apply (subst bind_subst_lift [OF modify_gets, unfolded bind_assoc]) apply (simp add: submonad_args.args submonad_args.replace_preserves_guard)+ apply (subst select_f_stateAssert, assumption) apply (subst gets_stateAssert) apply (subst bind_subst_lift [OF stateAssert_stateAssert]) apply (clarsimp simp: bind_assoc split_def select_f_walk empty_failD pred_conj_def
                        bind_subst_lift[OF modify_modify] submonad_args.args o_def
                        bind_subst_lift[OF bind_select_f_bind]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad f r g m; submonad f r g m'; submonad f r g m''; empty_fail a; \<And>x. empty_fail (b x)\<rbrakk> \<Longrightarrow> m (a >>= b) = do rv <- m' a;
m'' (b rv)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad f r g m; submonad f r g m'; submonad f r g m''; empty_fail a; \<And>x. empty_fail (b x)\<rbrakk> \<Longrightarrow> submonad_fn f r g (a >>= b) = do rv <- submonad_fn f r g a;
submonad_fn f r g (b rv)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> do y <- stateAssert g [];
substate <- gets f;
p <- select_f ((a >>= b) substate);
y <- modify (r (snd p));
return (fst p)
od = do x <- stateAssert g [];
x <- gets f;
x <- select_f (a x);
y <- modify (r (snd x));
y <- stateAssert g [];
substate <- gets f;
p <- select_f (b (fst x) substate);
y <- modify (r (snd p));
return (fst p)
od proof (prove)
goal (3 subgoals):
 1. \<And>xb xa x xc s. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> g (r xc s) = g s
 2. \<And>xb xa x xc s. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> g s \<longrightarrow> f (r xc s) = xc
 3. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> do y <- stateAssert g [];
substate <- gets f;
p <- select_f ((a >>= b) substate);
y <- modify (r (snd p));
return (fst p)
od = do x <- stateAssert g [];
x <- gets f;
x <- select_f (a x);
xa <- stateAssert g [];
xa <- modify (r (snd x));
a <- return (snd x);
p <- select_f (b (fst x) a);
y <- modify (r (snd p));
return (fst p)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> do y <- stateAssert g [];
substate <- gets f;
p <- select_f ((a >>= b) substate);
y <- modify (r (snd p));
return (fst p)
od = do x <- stateAssert g [];
x <- gets f;
x <- select_f (a x);
xa <- stateAssert g [];
xa <- modify (r (snd x));
p <- select_f (b (fst x) (snd x));
y <- modify (r (snd p));
return (fst p)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> do y <- stateAssert g [];
substate <- gets f;
p <- select_f ((a >>= b) substate);
y <- modify (r (snd p));
return (fst p)
od = do x <- stateAssert g [];
x <- gets f;
u <- stateAssert g [];
x <- select_f (a x);
xa <- modify (r (snd x));
p <- select_f (b (fst x) (snd x));
y <- modify (r (snd p));
return (fst p)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> do y <- stateAssert g [];
substate <- gets f;
p <- select_f ((a >>= b) substate);
y <- modify (r (snd p));
return (fst p)
od = do x <- stateAssert g [];
u <- stateAssert g [];
x <- gets f;
x <- select_f (a x);
xa <- modify (r (snd x));
p <- select_f (b (fst x) (snd x));
y <- modify (r (snd p));
return (fst p)
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>submonad_axioms f r g m'; submonad_axioms f r g m''; empty_fail a; \<And>x. empty_fail (b x); submonad_args f r g; submonad_axioms f r g m\<rbrakk> \<Longrightarrow> do y <- stateAssert g [];
substate <- gets f;
p <- select_f ((a >>= b) substate);
y <- modify (r (snd p));
return (fst p)
od = do u <- stateAssert (g and g) [];
x <- gets f;
x <- select_f (a x);
xa <- modify (r (snd x));
p <- select_f (b (fst x) (snd x));
y <- modify (r (snd p));
return (fst p)
od proof (prove)
goal:
No subgoals!