theory SubMonad_R

lemma submonad_asUser:
  "submonad (asUser_fetch t) (asUser_replace t) (tcb_at' t) (asUser t)" apply (unfold_locales) apply (clarsimp simp: asUser_fetch_def asUser_replace_def
                            Let_def obj_at'_def projectKOs
                     split: kernel_object.split option.split) apply (clarsimp simp: asUser_replace_def Let_def
                    split: kernel_object.split option.split) apply (rename_tac tcb) apply (case_tac tcb, simp) apply (clarsimp simp: asUser_fetch_def asUser_replace_def Let_def
                          fun_upd_idem
                   split: kernel_object.splits option.splits) apply (rename_tac tcb) apply (case_tac tcb, simp add: map_upd_triv atcbContextSet_def) apply (clarsimp simp: obj_at'_def asUser_replace_def
                         Let_def projectKOs atcbContextSet_def
                  split: kernel_object.splits option.splits) apply (rename_tac tcb) apply (case_tac tcb, simp add: objBitsKO_def ps_clear_def) apply (rule ext) apply (clarsimp simp: submonad_fn_def asUser_def bind_assoc split_def) apply (subst threadGet_stateAssert_gets_asUser, simp add: bind_assoc, rule ext) apply (rule bind_apply_cong [OF refl])+ apply (rule bind_apply_cong [OF threadSet_modify_asUser]) apply (clarsimp simp: in_monad stateAssert_def select_f_def) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad (asUser_fetch t) (asUser_replace t) (tcb_at' t) (asUser t) proof (prove)
goal (5 subgoals):
 1. \<forall>x s. tcb_at' t s \<longrightarrow> asUser_fetch t (asUser_replace t x s) = x
 2. \<forall>x y s. asUser_replace t x (asUser_replace t y s) = asUser_replace t x s
 3. \<forall>s. asUser_replace t (asUser_fetch t s) s = s
 4. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 5. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (4 subgoals):
 1. \<forall>x y s. asUser_replace t x (asUser_replace t y s) = asUser_replace t x s
 2. \<forall>s. asUser_replace t (asUser_fetch t s) s = s
 3. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 4. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (4 subgoals):
 1. \<And>x y s x6. ksPSpace s t = Some (KOTCB x6) \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x (tcbArch x6)) (tcbArch_update (\<lambda>_. atcbContextSet y (tcbArch x6)) x6)))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x (tcbArch x6)) x6))\<rparr>
 2. \<forall>s. asUser_replace t (asUser_fetch t s) s = s
 3. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 4. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (4 subgoals):
 1. \<And>x y s tcb. ksPSpace s t = Some (KOTCB tcb) \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x (tcbArch tcb)) (tcbArch_update (\<lambda>_. atcbContextSet y (tcbArch tcb)) tcb)))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet x (tcbArch tcb)) tcb))\<rparr>
 2. \<forall>s. asUser_replace t (asUser_fetch t s) s = s
 3. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 4. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (3 subgoals):
 1. \<forall>s. asUser_replace t (asUser_fetch t s) s = s
 2. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 3. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (3 subgoals):
 1. \<And>s x6. ksPSpace s t = Some (KOTCB x6) \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch x6) x6))\<rparr> = s
 2. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 3. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (3 subgoals):
 1. \<And>s tcb. ksPSpace s t = Some (KOTCB tcb) \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> = s
 2. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 3. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (2 subgoals):
 1. \<And>s x. tcb_at' t (asUser_replace t x s) = tcb_at' t s
 2. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (2 subgoals):
 1. \<And>s x x6. ksPSpace s t = Some (KOTCB x6) \<Longrightarrow> (is_aligned t (objBitsKO (KOTCB (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. x) (tcbArch x6)) x6))) \<and> ps_clear t (objBitsKO (KOTCB (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. x) (tcbArch x6)) x6))) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. x) (tcbArch x6)) x6))\<rparr>)) = (is_aligned t (objBitsKO (KOTCB x6)) \<and> ps_clear t (objBitsKO (KOTCB x6)) s)
 2. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (2 subgoals):
 1. \<And>s x tcb. ksPSpace s t = Some (KOTCB tcb) \<Longrightarrow> (is_aligned t (objBitsKO (KOTCB (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. x) (tcbArch tcb)) tcb))) \<and> ps_clear t (objBitsKO (KOTCB (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. x) (tcbArch tcb)) tcb))) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. x) (tcbArch tcb)) tcb))\<rparr>)) = (is_aligned t (objBitsKO (KOTCB tcb)) \<and> ps_clear t (objBitsKO (KOTCB tcb)) s)
 2. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (1 subgoal):
 1. asUser t = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) proof (prove)
goal (1 subgoal):
 1. \<And>x. asUser t x = submonad_fn (asUser_fetch t) (asUser_replace t) (tcb_at' t) x proof (prove)
goal (1 subgoal):
 1. \<And>x. do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (x uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od = do y <- stateAssert (tcb_at' t) [];
substate <- gets (asUser_fetch t);
p <- select_f (x substate);
y <- modify (asUser_replace t (snd p));
return (fst p)
od proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (do xa <- stateAssert (tcb_at' t) [];
uc <- gets (asUser_fetch t);
p <- select_f (x uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od) xa = (do y <- stateAssert (tcb_at' t) [];
substate <- gets (asUser_fetch t);
p <- select_f (x substate);
y <- modify (asUser_replace t (snd p));
return (fst p)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa rv st rva sta rvb stb. \<lbrakk>(rv, st) \<in> fst (stateAssert (tcb_at' t) [] xa); (rva, sta) \<in> fst (gets (asUser_fetch t) st); (rvb, stb) \<in> fst (select_f (x rva) sta)\<rbrakk> \<Longrightarrow> (do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd rvb) (tcbArch tcb)) tcb) t;
return (fst rvb)
od) stb = (do y <- modify (asUser_replace t (snd rvb));
return (fst rvb)
od) stb proof (prove)
goal (2 subgoals):
 1. \<And>x xa rv st rva sta rvb stb. \<lbrakk>(rv, st) \<in> fst (stateAssert (tcb_at' t) [] xa); (rva, sta) \<in> fst (gets (asUser_fetch t) st); (rvb, stb) \<in> fst (select_f (x rva) sta)\<rbrakk> \<Longrightarrow> tcb_at' t stb
 2. \<And>x xa rv st rva sta rvb stb rvc stc. \<lbrakk>(rv, st) \<in> fst (stateAssert (tcb_at' t) [] xa); (rva, sta) \<in> fst (gets (asUser_fetch t) st); (rvb, stb) \<in> fst (select_f (x rva) sta); (rvc, stc) \<in> fst (modify (asUser_replace t (snd rvb)) stb)\<rbrakk> \<Longrightarrow> return (fst rvb) stc = return (fst rvb) stc proof (prove)
goal (1 subgoal):
 1. \<And>x xa rv st rva sta rvb stb rvc stc. \<lbrakk>(rv, st) \<in> fst (stateAssert (tcb_at' t) [] xa); (rva, sta) \<in> fst (gets (asUser_fetch t) st); (rvb, stb) \<in> fst (select_f (x rva) sta); (rvc, stc) \<in> fst (modify (asUser_replace t (snd rvb)) stb)\<rbrakk> \<Longrightarrow> return (fst rvb) stc = return (fst rvb) stc proof (prove)
goal:
No subgoals!