theory SubMonad_R

lemma threadSet_modify_asUser:
  "tcb_at' t st \<Longrightarrow>
   threadSet (\<lambda>tcb. tcb\<lparr> tcbArch := atcbContextSet uc (tcbArch tcb)\<rparr>) t st = modify (asUser_replace t uc) st" apply (rule is_modify [OF _ empty_fail_threadSet no_fail_threadSet]) apply (clarsimp simp: threadSet_def setObject_def split_def
                         updateObject_default_def) apply wp apply (rule_tac Q="\<lambda>rv. obj_at' ((=) rv) t and ((=) st)" in hoare_post_imp) apply (clarsimp simp: asUser_replace_def Let_def obj_at'_def
                          projectKOs fun_upd_def
                   split: option.split kernel_object.split) apply (wp getObject_obj_at' | clarsimp simp: objBits_simps' atcbContextSet_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t st \<Longrightarrow> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb) t st = modify (asUser_replace t uc) st proof (prove)
goal (2 subgoals):
 1. tcb_at' t st \<Longrightarrow> \<lbrace>(=) st\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. (=) (asUser_replace t uc st)\<rbrace>
 2. tcb_at' t st \<Longrightarrow> tcb_at' t st proof (prove)
goal (2 subgoals):
 1. tcb_at' t st \<Longrightarrow> \<lbrace>(=) st\<rbrace> do tcb <- getObject t;
ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- do y <- assert (t = fst p);
_ <- projectKO (snd p);
y <- alignCheck t (objBits (tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb));
y <- magnitudeCheck t (snd (lookupAround2 t ps)) (objBits (tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb));
return (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_. (=) (asUser_replace t uc st)\<rbrace>
 2. tcb_at' t st \<Longrightarrow> tcb_at' t st proof (prove)
goal (3 subgoals):
 1. tcb_at' t st \<Longrightarrow> \<lbrace>?Q9\<rbrace> getObject t \<lbrace>\<lambda>tcb s. fst (lookupAround2 t (ksPSpace s)) \<noteq> None \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> asUser_replace t uc st = s\<lparr>ksPSpace := (ksPSpace s)(fst (the (fst (lookupAround2 t (ksPSpace s)))) \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch tcb)) tcb))\<rparr>\<rbrace>
 2. \<And>s. \<lbrakk>tcb_at' t st; st = s\<rbrakk> \<Longrightarrow> ?Q9 s
 3. tcb_at' t st \<Longrightarrow> tcb_at' t st proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>tcb_at' t st; (obj_at' ((=) rv) t and (=) st) s\<rbrakk> \<Longrightarrow> fst (lookupAround2 t (ksPSpace s)) \<noteq> None \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> asUser_replace t uc st = s\<lparr>ksPSpace := (ksPSpace s)(fst (the (fst (lookupAround2 t (ksPSpace s)))) \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet uc (tcbArch rv)) rv))\<rparr>
 2. tcb_at' t st \<Longrightarrow> \<lbrace>?Q9\<rbrace> getObject t \<lbrace>\<lambda>rv. obj_at' ((=) rv) t and (=) st\<rbrace>
 3. \<And>s. \<lbrakk>tcb_at' t st; st = s\<rbrakk> \<Longrightarrow> ?Q9 s
 4. tcb_at' t st \<Longrightarrow> tcb_at' t st proof (prove)
goal (3 subgoals):
 1. tcb_at' t st \<Longrightarrow> \<lbrace>?Q9\<rbrace> getObject t \<lbrace>\<lambda>rv. obj_at' ((=) rv) t and (=) st\<rbrace>
 2. \<And>s. \<lbrakk>tcb_at' t st; st = s\<rbrakk> \<Longrightarrow> ?Q9 s
 3. tcb_at' t st \<Longrightarrow> tcb_at' t st proof (prove)
goal:
No subgoals!