theory TcbAcc_R

lemma threadSet_state_refs_of'T_P:
  assumes x: "\<forall>tcb. (P' \<longrightarrow> Q (tcbState tcb)) \<longrightarrow>
                     tcb_st_refs_of' (tcbState (F tcb))
                       = f' (tcb_st_refs_of' (tcbState tcb))"
  assumes y: "\<forall>tcb. (P' \<longrightarrow> Q' (tcbBoundNotification tcb)) \<longrightarrow>
                     tcb_bound_refs' (tcbBoundNotification (F tcb))
                       = g' (tcb_bound_refs' (tcbBoundNotification tcb))"
  shows
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (t := f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound}
                                  \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound}))
              \<and> (P' \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)\<rbrace>
     threadSet F t
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (simp add: threadSet_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs pred_tcb_at'_def
                 elim!: rsubst[where P=P] intro!: ext) apply (cut_tac s=s and p=t and 'a=tcb in ko_at_state_refs_ofD') apply (simp add: obj_at'_def projectKOs) apply (clarsimp simp: x y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(t := f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound})) \<and> (P' \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(t := f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound})) \<and> (P' \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((state_refs_of' s)(t := f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound})) \<and> (P' \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> P ((state_refs_of' s)(t := tcb_st_refs_of' (tcbState (F ta)) \<union> tcb_bound_refs' (tcbBoundNotification (F ta))))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>P' \<longrightarrow> Q (tcbState obj) \<and> Q' (tcbBoundNotification obj); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound} = tcb_st_refs_of' (tcbState (F obj)) \<union> tcb_bound_refs' (tcbBoundNotification (F obj)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>P' \<longrightarrow> Q (tcbState obj) \<and> Q' (tcbBoundNotification obj); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> ko_at' (?ko21 s obj) t s
 2. \<And>s obj. \<lbrakk>P' \<longrightarrow> Q (tcbState obj) \<and> Q' (tcbBoundNotification obj); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; state_refs_of' s t = refs_of' (injectKO (?ko21 s obj))\<rbrakk> \<Longrightarrow> f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound} = tcb_st_refs_of' (tcbState (F obj)) \<union> tcb_bound_refs' (tcbBoundNotification (F obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>P' \<longrightarrow> Q (tcbState obj) \<and> Q' (tcbBoundNotification obj); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; state_refs_of' s t = refs_of' (injectKO obj)\<rbrakk> \<Longrightarrow> f' {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> g' {r \<in> state_refs_of' s t. snd r = TCBBound} = tcb_st_refs_of' (tcbState (F obj)) \<union> tcb_bound_refs' (tcbBoundNotification (F obj)) proof (prove)
goal:
No subgoals!