theory Tcb_C

lemma threadGet_context:
  "\<lbrakk> (uc, s') \<in> fst (threadGet (atcbContextGet o tcbArch) (ksCurThread s) s); ko_at' ko t s;
      t \<noteq> ksCurThread s \<rbrakk> \<Longrightarrow>
   (uc, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in>
  fst (threadGet (atcbContextGet o tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>))" apply (clarsimp simp: threadGet_def liftM_def in_monad) apply (drule (1) getObject_context [where st=st]) apply (rule exI) apply (erule conjI) apply (simp split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(uc, s') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); ko_at' ko t s; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> (uc, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; (x, s') \<in> fst (getObject (ksCurThread s) s); uc = atcbContextGet (tcbArch x)\<rbrakk> \<Longrightarrow> \<exists>xa. (xa, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; uc = atcbContextGet (tcbArch x); (if t = ksCurThread s then ?tcbContext_update4 x (\<lambda>_. st) x else x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update4 x (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update4 x (\<lambda>_. st) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>xa. (xa, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; uc = atcbContextGet (tcbArch x); (if t = ksCurThread s then ?tcbContext_update4 x (\<lambda>_. st) x else x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update4 x (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update4 x (\<lambda>_. st) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?x7 x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch (?x7 x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; t \<noteq> ksCurThread s; uc = atcbContextGet (tcbArch x)\<rbrakk> \<Longrightarrow> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch (if t = ksCurThread s then tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch x)) x else x)) proof (prove)
goal:
No subgoals!