theory Tcb_R

lemma setP_invs':
  "\<lbrace>invs' and tcb_at' t and K (p \<le> maxPriority)\<rbrace> setPriority t p \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: setPriority_def) apply (wp rescheduleRequired_all_invs_but_ct_not_inQ) apply simp apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift') unfolding st_tcb_at'_def apply (strengthen not_obj_at'_strengthen, wp) apply (wp hoare_vcg_imp_lift') apply (rule_tac Q="\<lambda>rv s. invs' s" in hoare_post_imp) apply (clarsimp simp: invs_sch_act_wf' invs'_def invs_queues) apply (clarsimp simp: valid_state'_def) apply (wp hoare_drop_imps threadSet_invs_trivial,
             simp_all add: inQ_def cong: conj_cong)[1] apply (wp hoare_drop_imps threadSet_invs_trivial,
            simp_all add: inQ_def cong: conj_cong)[1] apply (wp hoare_drop_imps threadSet_invs_trivial,
           simp_all add: inQ_def cong: conj_cong)[1] apply (rule_tac Q="\<lambda>_. invs' and obj_at' (Not \<circ> tcbQueued) t
                                  and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d,p)))"
              in hoare_post_imp) apply (clarsimp simp: obj_at'_def inQ_def) apply (wp tcbSchedDequeue_not_queued)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and K (p \<le> maxPriority)\<rbrace> setPriority t p \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> setPriority t p \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<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. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. p \<le> maxPriority \<Longrightarrow> \<lbrace>?B3 y\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>ya s. (if st_tcb_at' runnable' t s then \<lambda>s. (t = ksCurThread s \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> (invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s) else invs') s\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> tcbSchedDequeue t \<lbrace>?B3\<rbrace>
 3. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?B3 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>ya s. (st_tcb_at' runnable' t s \<longrightarrow> (t = ksCurThread s \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> invs' s)) \<and> (\<not> st_tcb_at' runnable' t s \<longrightarrow> invs' s)\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> tcbSchedDequeue t \<lbrace>?B3\<rbrace>
 3. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'28 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' t s\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'27 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> invs' s)\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' t s \<longrightarrow> invs' s\<rbrace>
 4. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> ?P'28 a b \<longrightarrow> ?Q'27 a b) \<and> ?P'24 a b\<rbrace>
 5. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'28 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'27 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> invs' s)\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 4. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>a b. (\<not> ?P'28 a b \<longrightarrow> ?Q'27 a b) \<and> ?P'24 a b\<rbrace>
 5. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'27 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. (t = ksCurThread s \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> (t \<noteq> ksCurThread s \<longrightarrow> invs' s)\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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'27 a b) \<and> ?P'24 a b\<rbrace>
 4. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'42 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'39 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> invs' s\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 4. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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'42 a b) \<and> ?P'39 a b) \<and> ?P'24 a b\<rbrace>
 5. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>p \<le> maxPriority; invs' s\<rbrakk> \<Longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'42 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'39 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> invs' s\<rbrace>
 4. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 5. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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'42 a b) \<and> ?P'39 a b) \<and> ?P'24 a b\<rbrace>
 6. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>p \<le> maxPriority; valid_state' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_pspace' s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'42 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'39 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> invs' s\<rbrace>
 4. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 5. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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'42 a b) \<and> ?P'39 a b) \<and> ?P'24 a b\<rbrace>
 6. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q'42 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'39 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> invs' s\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 4. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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'42 a b) \<and> ?P'39 a b) \<and> ?P'24 a b\<rbrace>
 5. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'39 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. t \<noteq> ksCurThread s \<longrightarrow> invs' s\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 3. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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> invs' b \<and> tcb_at' t b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t b \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues b (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t b \<and> t \<noteq> ksCurThread b) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction b = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread b)) \<and> ?P'39 a b) \<and> ?P'24 a b\<rbrace>
 4. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?P'24 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. p)) t \<lbrace>\<lambda>rv s. \<not> obj_at' (runnable' \<circ> tcbState) t s \<longrightarrow> invs' s\<rbrace>
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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> invs' b \<and> tcb_at' t b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t b \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues b (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t b \<and> t \<noteq> ksCurThread b) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction b = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread b)) \<and> invs' b \<and> tcb_at' t b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t b \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues b (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t b \<and> t \<noteq> ksCurThread b) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction b = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread b)) \<and> ?P'24 a b\<rbrace>
 3. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<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> invs' b \<and> tcb_at' t b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t b \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues b (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t b \<and> t \<noteq> ksCurThread b) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction b = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread b)) \<and> invs' b \<and> tcb_at' t b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t b \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues b (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t b \<and> t \<noteq> ksCurThread b) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction b = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread b)) \<and> invs' b \<and> tcb_at' t b \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues b (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t b \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues b (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t b \<and> t \<noteq> ksCurThread b) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction b = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread b)\<rbrace>
 2. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>p \<le> maxPriority; (invs' and obj_at' (Not \<circ> tcbQueued) t and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))) s\<rbrakk> \<Longrightarrow> (\<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 s \<longrightarrow> (\<not> t \<noteq> ksCurThread s \<longrightarrow> invs' s \<and> tcb_at' t s \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t s \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues s (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t s \<and> t \<noteq> ksCurThread s) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread s)) \<and> invs' s \<and> tcb_at' t s \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t s \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues s (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t s \<and> t \<noteq> ksCurThread s) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread s)) \<and> invs' s \<and> tcb_at' t s \<and> (\<forall>d pa. (\<exists>tcb. inQ d pa tcb \<and> \<not> inQ d pa (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, pa))) \<and> (\<forall>ko d pa. ko_at' ko t s \<and> inQ d pa (tcbPriority_update (\<lambda>_. p) ko) \<and> \<not> inQ d pa ko \<longrightarrow> t \<in> set (ksReadyQueues s (d, pa))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbPriority_update (\<lambda>_. p) tcb)) \<longrightarrow> ex_nonz_cap_to' t s \<and> t \<noteq> ksCurThread s) \<and> (\<forall>tcb. tcbQueued (tcbPriority_update (\<lambda>_. p) tcb) \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> t \<noteq> ksCurThread s)
 2. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. invs' and obj_at' (Not \<circ> tcbQueued) t and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
 3. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. p \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. invs' and obj_at' (Not \<circ> tcbQueued) t and (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t) s \<and> True \<and> (Invariants_H.valid_queues and tcb_at' t and K (t = t)) s proof (prove)
goal:
No subgoals!