theory Tcb_C

lemma threadGet_state:
  "\<lbrakk> (uc, s') \<in> fst (threadGet (atcbContextGet o tcbArch) t' s); ko_at' ko t s \<rbrakk> \<Longrightarrow>
   (uc, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in>
  fst (threadGet (atcbContextGet o tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))" apply (clarsimp simp: threadGet_def liftM_def in_monad) apply (drule (1) getObject_state [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) t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> (uc, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; (x, s') \<in> fst (getObject t' s); uc = atcbContextGet (tcbArch x)\<rbrakk> \<Longrightarrow> \<exists>xa. (xa, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; uc = atcbContextGet (tcbArch x); (if t = t' then tcbState_update (\<lambda>_. st) x else x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>xa. (xa, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch xa) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; uc = atcbContextGet (tcbArch x); (if t = t' then tcbState_update (\<lambda>_. st) x else x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?x7 x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch (?x7 x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at' ko t s; uc = atcbContextGet (tcbArch x)\<rbrakk> \<Longrightarrow> atcbContextGet (tcbArch x) = atcbContextGet (tcbArch (if t = t' then tcbState_update (\<lambda>_. st) x else x)) proof (prove)
goal:
No subgoals!