theory TcbAcc_R

lemma tcbSchedDequeue_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" proof - have TSNIQ: "\<And>F t.
      \<lbrace>ct_not_inQ and (\<lambda>_. \<forall>tcb. \<not>tcbQueued (F tcb))\<rbrace>
      threadSet F t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: ct_not_inQ_def) apply (wp hoare_convert_imp [OF threadSet_nosch]) apply (simp add: threadSet_def) apply (wp) apply (wps setObject_ct_inv) apply (wp setObject_tcb_strongest getObject_tcb_wp)+ apply (case_tac "t = ksCurThread s") apply (clarsimp simp: obj_at'_def)+ done show ?thesis apply (simp add: tcbSchedDequeue_def) apply (wp TSNIQ | simp cong: if_cong)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>F t. \<lbrace>ct_not_inQ and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))\<rbrace> threadSet F t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>F t. \<lbrace>(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>F t. \<lbrace>?R1 F t\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>F t s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R1 F t s proof (prove)
goal (2 subgoals):
 1. \<And>F t. \<lbrace>?R1 F t\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>F t s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R1 F t s proof (prove)
goal (3 subgoals):
 1. \<And>F t x. \<lbrace>?B6 F t x\<rbrace> setObject t (F x) \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>F t. \<lbrace>?R1 F t\<rbrace> getObject t \<lbrace>?B6 F t\<rbrace>
 3. \<And>F t s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R1 F t s proof (prove)
goal (3 subgoals):
 1. \<And>F t x prev_s. \<lbrace>?P8 F t x prev_s\<rbrace> setObject t (F x) \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>F t. \<lbrace>?R1 F t\<rbrace> getObject t \<lbrace>\<lambda>x s. ?P8 F t x s s\<rbrace>
 3. \<And>F t s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ?R1 F t s proof (prove)
goal (1 subgoal):
 1. \<And>F t s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (if t = ksCurThread s then (Not \<circ> tcbQueued) (F ta) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)) proof (prove)
goal (2 subgoals):
 1. \<And>F t s. \<lbrakk>((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s; t = ksCurThread s\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (if t = ksCurThread s then (Not \<circ> tcbQueued) (F ta) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s))
 2. \<And>F t s. \<lbrakk>((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (F tcb))) s; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (if t = ksCurThread s then (Not \<circ> tcbQueued) (F ta) else obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_not_inQ and (\<lambda>_. \<forall>tcb. \<not> tcbQueued (?F tcb))\<rbrace> threadSet ?F ?t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>

goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> do queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_not_inQ\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>

goal:
No subgoals!