theory Move_C

lemma asUser_mapM_x:
  "(\<And>x. empty_fail (f x)) \<Longrightarrow>
    asUser t (mapM_x f xs) = do stateAssert (tcb_at' t) []; mapM_x (\<lambda>x. asUser t (f x)) xs od" supply empty_fail_cond[simp] apply (simp add: mapM_x_mapM asUser_bind_distrib) apply (subst submonad_mapM [OF submonad_asUser submonad_asUser]) apply simp apply (simp add: asUser_return bind_assoc o_def) apply (rule ext) apply (rule bind_apply_cong [OF refl])+ apply (clarsimp simp: in_monad dest!: fst_stateAssertD) apply (drule use_valid, rule mapM_wp', rule asUser_typ_ats, assumption) apply (simp add: stateAssert_def get_def Nondet_Monad.bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> asUser t (mapM_x f xs) = do stateAssert (tcb_at' t) [];
mapM_x (\<lambda>x. asUser t (f x)) xs
od proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> asUser t (mapM_x f xs) = do stateAssert (tcb_at' t) [];
mapM_x (\<lambda>x. asUser t (f x)) xs
od proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> do rv <- asUser t (mapM f xs);
asUser t (return ())
od = do y <- stateAssert (tcb_at' t) [];
x <- mapM (\<lambda>x. asUser t (f x)) xs;
return ()
od proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<And>x. empty_fail (f x)) \<Longrightarrow> empty_fail (f x)
 2. (\<And>x. empty_fail (f x)) \<Longrightarrow> do rv <- do u <- stateAssert (tcb_at' t) [];
mapM (asUser t \<circ> f) xs
od;
asUser t (return ())
od = do y <- stateAssert (tcb_at' t) [];
x <- mapM (\<lambda>x. asUser t (f x)) xs;
return ()
od proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> do rv <- do u <- stateAssert (tcb_at' t) [];
mapM (asUser t \<circ> f) xs
od;
asUser t (return ())
od = do y <- stateAssert (tcb_at' t) [];
x <- mapM (\<lambda>x. asUser t (f x)) xs;
return ()
od proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> do x <- stateAssert (tcb_at' t) [];
rv <- mapM (\<lambda>x. asUser t (f x)) xs;
stateAssert (tcb_at' t) []
od = do y <- stateAssert (tcb_at' t) [];
x <- mapM (\<lambda>x. asUser t (f x)) xs;
return ()
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>x. empty_fail (f x)) \<Longrightarrow> (do x <- stateAssert (tcb_at' t) [];
rv <- mapM (\<lambda>x. asUser t (f x)) xs;
stateAssert (tcb_at' t) []
od) x = (do y <- stateAssert (tcb_at' t) [];
x <- mapM (\<lambda>x. asUser t (f x)) xs;
return ()
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta. \<lbrakk>\<And>x. empty_fail (f x); (rv, st) \<in> fst (stateAssert (tcb_at' t) [] x); (rva, sta) \<in> fst (mapM (\<lambda>x. asUser t (f x)) xs st)\<rbrakk> \<Longrightarrow> stateAssert (tcb_at' t) [] sta = return () sta proof (prove)
goal (1 subgoal):
 1. \<And>x rva sta. \<lbrakk>\<And>x. empty_fail (f x); (rva, sta) \<in> fst (mapM (\<lambda>x. asUser t (f x)) xs x); tcb_at' t x\<rbrakk> \<Longrightarrow> stateAssert (tcb_at' t) [] sta = return () sta proof (prove)
goal (1 subgoal):
 1. \<And>x rva sta. \<lbrakk>\<And>x. empty_fail (f x); tcb_at' t x; tcb_at' t sta\<rbrakk> \<Longrightarrow> stateAssert (tcb_at' t) [] sta = return () sta proof (prove)
goal:
No subgoals!