theory Tcb_R

lemma setP_vq[wp]:
  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority\<rbrace>
     setPriority t p
   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: setPriority_def) apply (wpsimp ) apply (wp hoare_vcg_imp_lift') unfolding st_tcb_at'_def apply (strengthen not_obj_at'_strengthen) apply (wp hoare_wp_combs) apply (wp hoare_vcg_imp_lift') apply (wp threadSet_valid_queues threadSet_valid_objs_tcbPriority_update) apply(wp threadSet_weak_sch_act_wf) apply clarsimp apply clarsimp apply (wp hoare_vcg_imp_lift') apply (wp threadSet_valid_queues threadSet_valid_objs_tcbPriority_update threadSet_sch_act, clarsimp) apply (wp add: threadSet_valid_queues comb:hoare_drop_imps ) apply (clarsimp simp: eq_commute[where a=t]) apply (wp add: threadSet_valid_queues threadSet_valid_objs_tcbPriority_update threadSet_weak_sch_act_wf
                  hoare_vcg_imp_lift'[where P="\<lambda>_ s. ksCurThread s \<noteq> _"] hoare_drop_imps hoare_vcg_all_lift
                  tcbSchedDequeue_not_in_queue tcbSchedEnqueue_valid_objs' tcbSchedDequeue_valid_queues
          | clarsimp simp: valid_objs'_maxDomain valid_objs'_maxPriority)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority\<rbrace> setPriority t p \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority\<rbrace> do y <- tcbSchedDequeue t;
y <- threadSet (tcbPriority_update (\<lambda>_. p)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B2 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>ya s. (st_tcb_at' runnable' t s \<longrightarrow> (t = ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (\<not> st_tcb_at' runnable' t s \<longrightarrow> Invariants_H.valid_queues s)\<rbrace>
 2. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>?B2\<rbrace>
 3. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'30 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' t s\<rbrace>
 2. \<lbrace>?Q'29 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 4. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> ?P'30 a b \<longrightarrow> ?Q'29 a b) \<and> ?P'26 a b\<rbrace>
 5. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'30 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s\<rbrace>
 2. \<lbrace>?Q'29 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 4. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> ?P'30 a b \<longrightarrow> ?Q'29 a b) \<and> ?P'26 a b\<rbrace>
 5. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'30 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>r. obj_at' (Not \<circ> (runnable' \<circ> tcbState)) t\<rbrace>
 2. \<lbrace>?Q'29 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 4. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> ?P'30 a b \<longrightarrow> ?Q'29 a b) \<and> ?P'26 a b\<rbrace>
 5. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q'29 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> ?Q'29 a b) \<and> ?P'26 a b\<rbrace>
 4. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'44 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?P'41 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 4. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> ?Q'44 a b) \<and> ?P'41 a b) \<and> ?P'26 a b\<rbrace>
 5. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'54 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?P'41 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 4. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> ?P'54 a b) \<and> ?P'41 a b) \<and> ?P'26 a b\<rbrace>
 5. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (6 subgoals):
 1. \<And>tcb. tcbState (tcbPriority_update (\<lambda>_. p) tcb) = tcbState tcb
 2. \<And>tcb. tcbDomain (tcbPriority_update (\<lambda>_. p) tcb) = tcbDomain tcb
 3. \<lbrace>?P'41 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 4. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 5. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> ?P'41 a b) \<and> ?P'26 a b\<rbrace>
 6. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>tcb. tcbDomain (tcbPriority_update (\<lambda>_. p) tcb) = tcbDomain tcb
 2. \<lbrace>?P'41 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 4. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> ?P'41 a b) \<and> ?P'26 a b\<rbrace>
 5. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'41 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> ?P'41 a b) \<and> ?P'26 a b\<rbrace>
 4. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q'63 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> (\<not> \<not> t \<noteq> ksCurThread b \<longrightarrow> ?Q'63 a b)) \<and> ?P'26 a b\<rbrace>
 4. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'26 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> Invariants_H.valid_queues s\<rbrace>
 2. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> (\<not> \<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> sch_act_wf (ksSchedulerAction b) b)) \<and> ?P'26 a b\<rbrace>
 3. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. if t = t then (Not \<circ> (runnable' \<circ> tcbState)) (tcbPriority_update (\<lambda>_. p) obj) else (Not \<circ> (runnable' \<circ> tcbState)) obj) t b \<longrightarrow> (\<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> (\<not> \<not> t \<noteq> ksCurThread b \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b \<and> (valid_objs' and (\<lambda>_. p \<le> maxPriority)) b \<and> sch_act_wf (ksSchedulerAction b) b)) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d pa. (\<exists>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d pa tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. p) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa)))) b\<rbrace>
 2. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> obj_at' (\<lambda>obj. \<not> runnable' (tcbState obj)) t b \<longrightarrow> (ksCurThread b = t \<longrightarrow> Invariants_H.valid_queues b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> runnable' (tcbState tcb) \<and> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d pa tcb \<and> runnable' (tcbState tcb) \<and> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) t b \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> valid_objs' b \<and> p \<le> maxPriority \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> (ksCurThread b \<noteq> t \<longrightarrow> Invariants_H.valid_queues b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> runnable' (tcbState tcb) \<and> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d pa tcb \<and> runnable' (tcbState tcb) \<and> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) t b \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> valid_objs' b \<and> p \<le> maxPriority \<and> sch_act_wf (ksSchedulerAction b) b)) \<and> Invariants_H.valid_queues b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> runnable' (tcbState tcb) \<and> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d pa tcb \<and> runnable' (tcbState tcb) \<and> (inQ d pa (tcbPriority_update (\<lambda>_. p) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) t b \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa)))\<rbrace>
 2. \<And>s. Invariants_H.valid_queues s \<and> tcb_at' t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> p \<le> maxPriority \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!