theory TcbAcc_R

lemma tcbSchedEnqueue_ct_not_inQ:
  "\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
    tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") proof - have ts: "\<lbrace>?PRE\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: ct_not_inQ_def) apply (rule_tac Q="\<lambda>s. ksSchedulerAction s = ResumeCurrentThread
                  \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ksCurThread s \<noteq> t"
                  in hoare_pre_imp, clarsimp) apply (rule hoare_convert_imp [OF threadSet_nosch]) apply (rule hoare_weaken_pre) apply (wps setObject_ct_inv) apply (rule threadSet_obj_at'_strongish) apply (clarsimp simp: comp_def) done have sq: "\<And>d p q. \<lbrace>ct_not_inQ\<rbrace> setQueue d p q \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: ct_not_inQ_def setQueue_def) apply (wp) apply (clarsimp) done show ?thesis apply (simp add: tcbSchedEnqueue_def unless_def null_def) apply (wp ts sq hoare_convert_imp [OF addToBitmap_nosch addToBitmap_ct'])+ apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_post_imp, clarsimp) apply (wp sq hoare_convert_imp [OF setQueue_nosch setQueue_ct])+ apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_post_imp, clarsimp) apply wp apply assumption done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) 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) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) 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. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ksCurThread s \<noteq> t\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) 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 \<and> ksCurThread s \<noteq> t\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ksCurThread s \<noteq> t \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P11 prev_s\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ksCurThread s \<noteq> t \<Longrightarrow> ?P11 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ksCurThread s \<noteq> t \<Longrightarrow> obj_at' (\<lambda>obj. if t = ksCurThread s then (Not \<circ> tcbQueued) (tcbQueued_update (\<lambda>_. True) obj) else (Not \<circ> tcbQueued) obj) (ksCurThread s) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>

goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p q. \<lbrace>ct_not_inQ\<rbrace> setQueue d p q \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p q. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((d, p) := q)\<rparr>) \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p q s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ksSchedulerAction (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := q)\<rparr>) = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := q)\<rparr>)) (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := q)\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_not_inQ\<rbrace> setQueue ?d ?p ?q \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>

goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> do queued <- threadGet tcbQueued t;
when (\<not> queued) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (queue = []) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (t # queue) \<lbrace>\<lambda>y. if queue = [] then \<lambda>s. ct_not_inQ s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t) else (\<lambda>s. ct_not_inQ s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t))\<rbrace>
 2. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q2 queued else ct_not_inQ\<rbrace>
 6. \<And>s. (ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio queue\<rbrace> setQueue tdom prio (t # queue) \<lbrace>\<lambda>_. ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B4 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B5 queued tdom prio\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B3 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B4 queued tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q2 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B3 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q2 queued else ct_not_inQ\<rbrace>
 6. \<And>s. (ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then \<lambda>s. ct_not_inQ s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t) else ct_not_inQ\<rbrace>
 2. \<And>s. (ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>_. ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>s. (ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> (ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_not_inQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>

goal:
No subgoals!