theory TcbAcc_R

lemma threadSet_tcbBoundNotification_update_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> threadSet (tcbBoundNotification_update f) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: ct_not_inQ_def) apply (rule hoare_convert_imp [OF threadSet_nosch]) apply (simp add: threadSet_def) apply (wp) apply (wps setObject_ct_inv) apply (rule setObject_tcb_strongest) prefer 2 apply assumption apply (clarsimp) apply (rule hoare_conjI) apply (rule hoare_weaken_pre) apply wps apply (wp hoare_weak_lift_imp) apply (wp OMG_getObject_tcb) apply (clarsimp simp: comp_def) apply (wp hoare_drop_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> threadSet (tcbBoundNotification_update f) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> threadSet (tcbBoundNotification_update f) t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> threadSet (tcbBoundNotification_update f) t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> do tcb <- getObject t;
setObject t (tcbBoundNotification_update f tcb)
od \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B5 x\<rbrace> setObject t (tcbBoundNotification_update f x) \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<lbrace>?Q4\<rbrace> getObject t \<lbrace>?B5\<rbrace>
 3. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>x prev_s. \<lbrace>?P6 x prev_s\<rbrace> setObject t (tcbBoundNotification_update f x) \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<lbrace>?Q4\<rbrace> getObject t \<lbrace>\<lambda>x s. ?P6 x s s\<rbrace>
 3. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> getObject t \<lbrace>\<lambda>x s. if t = ksCurThread s then (Not \<circ> tcbQueued) (tcbBoundNotification_update f x) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q4 s
 2. \<lbrace>?Q4\<rbrace> getObject t \<lbrace>\<lambda>x s. if t = ksCurThread s then (Not \<circ> tcbQueued) (tcbBoundNotification_update f x) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>x s. if t = ksCurThread s then (Not \<circ> tcbQueued) (tcbBoundNotification_update f x) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>x s. (t = ksCurThread s \<longrightarrow> \<not> tcbQueued x) \<and> (t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t = ksCurThread s \<longrightarrow> \<not> tcbQueued r\<rbrace>
 2. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q26\<rbrace> getObject t \<lbrace>\<lambda>r s. t = ksCurThread s \<longrightarrow> \<not> tcbQueued r\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q26 s
 3. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>prev_s. \<lbrace>?P29 prev_s\<rbrace> getObject t \<lbrace>\<lambda>rv s'. t = ksCurThread prev_s \<longrightarrow> \<not> tcbQueued rv\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P29 s s
 3. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>prev_s. \<lbrace>?P'36 prev_s\<rbrace> getObject t \<lbrace>\<lambda>rv s. \<not> tcbQueued rv\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> t = ksCurThread s \<longrightarrow> ?P'36 s s
 3. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> t = ksCurThread s \<longrightarrow> obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) t s
 2. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> getObject t \<lbrace>\<lambda>r s. t \<noteq> ksCurThread s \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal:
No subgoals!