theory Fastpath_Equiv

lemma sym_refs_upd_tcb_sD:
  "\<lbrakk> sym_refs ((state_refs_of' s) (p := {r \<in> state_refs_of' s p. snd r = TCBBound})); valid_pspace' s;
            ko_at' (tcb :: tcb) p s \<rbrakk>
      \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s')
               \<and> (\<forall>p' (ko' :: endpoint).
                          ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s')
               \<and> (\<forall>p' (ko' :: Structures_H.notification).
                          ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s')
               \<and> (st_tcb_at' ((=) Running) p s')" apply (drule(2) sym_refs_upd_sD[where koEx="makeObject\<lparr>tcbState := Running, tcbBoundNotification := tcbBoundNotification tcb\<rparr>"]) apply (clarsimp dest!: ko_at_state_refs_ofD') apply (simp add: objBits_simps) apply (erule exEI) apply clarsimp apply (auto simp: st_tcb_at'_def elim!: obj_at'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := {r \<in> state_refs_of' s p. snd r = TCBBound})); valid_pspace' s; ko_at' tcb p s\<rbrakk> \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> st_tcb_at' ((=) Structures_H.thread_state.Running) p s' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' s; ko_at' tcb p s\<rbrakk> \<Longrightarrow> refs_of' (injectKOS (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject))) = {r \<in> state_refs_of' s p. snd r = TCBBound}
 2. \<lbrakk>valid_pspace' s; ko_at' tcb p s\<rbrakk> \<Longrightarrow> objBits (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) = objBits tcb
 3. \<lbrakk>valid_pspace' s; ko_at' tcb p s; \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' s') \<and> ko_at' (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) p s'\<rbrakk> \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> st_tcb_at' ((=) Structures_H.thread_state.Running) p s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; ko_at' tcb p s\<rbrakk> \<Longrightarrow> objBits (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) = objBits tcb
 2. \<lbrakk>valid_pspace' s; ko_at' tcb p s; \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' s') \<and> ko_at' (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) p s'\<rbrakk> \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> st_tcb_at' ((=) Structures_H.thread_state.Running) p s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; ko_at' tcb p s; \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' s') \<and> ko_at' (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) p s'\<rbrakk> \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' s') \<and> st_tcb_at' ((=) Structures_H.thread_state.Running) p s' proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_pspace' s; ko_at' tcb p s; sym_refs (state_refs_of' x) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' x) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS tcb \<longrightarrow> ko_at' ko' p' x) \<and> ko_at' (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) p x\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of' x) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' x) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' x) \<and> st_tcb_at' ((=) Structures_H.thread_state.Running) p x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_pspace' s; ko_at' tcb p s; sym_refs (state_refs_of' x); \<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' x; \<forall>p' ko'. ko_at' ko' p' s \<longrightarrow> ko_at' ko' p' x; ko_at' (tcbBoundNotification_update (\<lambda>_. tcbBoundNotification tcb) (tcbState_update (\<lambda>_. Structures_H.thread_state.Running) makeObject)) p x\<rbrakk> \<Longrightarrow> st_tcb_at' ((=) Structures_H.thread_state.Running) p x proof (prove)
goal:
No subgoals!