theory Tcb_R

lemma sp_corres2:
  "corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb)
             (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t
              and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority))
                     (set_priority t x) (setPriority t x)" apply (simp add: setPriority_def set_priority_def thread_set_priority_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF tcbSchedDequeue_corres]) apply (rule corres_split[OF ethread_set_corres], simp_all)[1] apply (simp add: etcb_relation_def) apply (rule corres_split[OF isRunnable_corres]) apply (erule corres_when) apply(rule corres_split[OF getCurThread_corres]) apply (wp corres_if; clarsimp) apply (rule rescheduleRequired_corres) apply (rule possibleSwitchTo_corres) apply ((clarsimp
                   | wp hoare_weak_lift_imp hoare_vcg_if_lift hoare_wp_combs gts_wp
                        isRunnable_wp)+)[4] apply (wp hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift) apply clarsimp apply ((wp hoare_drop_imps hoare_vcg_if_lift hoare_vcg_all_lift
                 isRunnable_wp threadSet_pred_tcb_no_state threadSet_valid_queues_no_state
                 threadSet_valid_queues'_no_state threadSet_cur threadSet_valid_objs_tcbPriority_update
                 threadSet_weak_sch_act_wf threadSet_ct_in_state'[simplified ct_in_state'_def]
              | simp add: etcb_relation_def)+)[1] apply ((wp hoare_vcg_imp_lift' hoare_vcg_if_lift hoare_vcg_all_lift hoare_vcg_disj_lift
                tcbSchedDequeue_not_in_queue tcbSchedDequeue_valid_queues
                tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def]
             | simp add: etcb_relation_def)+)[2] apply (force simp: valid_etcbs_def tcb_at_st_tcb_at[symmetric] state_relation_def
                dest: pspace_relation_tcb_at intro: st_tcb_at_opeqI) apply (force simp: state_relation_def elim: valid_objs'_maxDomain valid_objs'_maxPriority) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb) (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) (set_priority t x) (setPriority t x) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb) (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) (do y <- tcb_sched_action tcb_sched_dequeue t;
y <- ethread_set (tcb_priority_update (\<lambda>_. x)) t;
ts <- get_thread_state t;
when (runnable ts) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od)
od) (do y <- tcbSchedDequeue t;
y <- threadSet (tcbPriority_update (\<lambda>_. x)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do y <- tcb_sched_action tcb_sched_dequeue t;
y <- ethread_set (tcb_priority_update (\<lambda>_. x)) t;
ts <- get_thread_state t;
when (runnable ts) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od)
od) (do y <- tcbSchedDequeue t;
y <- threadSet (tcbPriority_update (\<lambda>_. x)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od)
 2. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (5 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> corres dc (?R4 y) (?R'4 ya) (do y <- ethread_set (tcb_priority_update (\<lambda>_. x)) t;
ts <- get_thread_state t;
when (runnable ts) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od)
od) (do y <- threadSet (tcbPriority_update (\<lambda>_. x)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od)
 2. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>?R'4\<rbrace>
 4. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 5. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> etcb_relation (etcb\<lparr>tcb_priority := x\<rparr>) (tcbPriority_update (\<lambda>_. x) tcb')
 2. corres dc (?R10 () () ()) (?R'10 () () ()) (do ts <- get_thread_state t;
when (runnable ts) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od)
od) (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od)
 3. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>?R10 () ()\<rbrace>
 4. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>?R'10 () ()\<rbrace>
 5. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 7. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 8. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. corres dc (?R10 () () ()) (?R'10 () () ()) (do ts <- get_thread_state t;
when (runnable ts) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od)
od) (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od)
 2. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>?R10 () ()\<rbrace>
 3. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>?R'10 () ()\<rbrace>
 4. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 6. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 7. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. \<And>ts runnablea. runnable ts = runnablea \<Longrightarrow> corres dc (?R27 ts) (?R'27 runnablea) (when (runnable ts) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od)) (when runnablea (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od))
 2. \<lbrace>?Q32 () () ()\<rbrace> get_thread_state t \<lbrace>?R27\<rbrace>
 3. \<lbrace>?Q'31 () () ()\<rbrace> isRunnable t \<lbrace>?R'27\<rbrace>
 4. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and ?Q32 () () a\<rbrace>
 5. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'31 () () a\<rbrace>
 6. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 8. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 9. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. \<And>ts runnable. corres dc (?P37 ts) (?P'38 runnable) (do cur <- gets cur_thread;
if t = cur then reschedule_required else possible_switch_to t
od) (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
 2. \<lbrace>?Q32 () () ()\<rbrace> get_thread_state t \<lbrace>\<lambda>ts x. runnable ts \<longrightarrow> ?P37 ts x\<rbrace>
 3. \<lbrace>?Q'31 () () ()\<rbrace> isRunnable t \<lbrace>\<lambda>runnable x. runnable \<longrightarrow> ?P'38 runnable x\<rbrace>
 4. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and ?Q32 () () a\<rbrace>
 5. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'31 () () a\<rbrace>
 6. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 8. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 9. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (11 subgoals):
 1. \<And>ts runnable rv rv'. rv = rv' \<Longrightarrow> corres dc (?R40 ts runnable rv) (?R'40 ts runnable rv') (if t = rv then reschedule_required else possible_switch_to t) (if t = rv' then rescheduleRequired else possibleSwitchTo t)
 2. \<And>ts runnable. \<lbrace>?Q41 ts\<rbrace> gets cur_thread \<lbrace>?R40 ts runnable\<rbrace>
 3. \<And>ts runnable. \<lbrace>?Q'42 runnable\<rbrace> getCurThread \<lbrace>?R'40 ts runnable\<rbrace>
 4. \<lbrace>?Q32 () () ()\<rbrace> get_thread_state t \<lbrace>\<lambda>ts x. runnable ts \<longrightarrow> ((\<lambda>_. True) and ?Q41 ts) x\<rbrace>
 5. \<lbrace>?Q'31 () () ()\<rbrace> isRunnable t \<lbrace>\<lambda>runnable x. runnable \<longrightarrow> ((\<lambda>_. True) and ?Q'42 runnable) x\<rbrace>
 6. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and ?Q32 () () a\<rbrace>
 7. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'31 () () a\<rbrace>
 8. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 10. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ts runnable rv. corres dc (?P49 ts runnable rv) (?P'52 ts runnable rv) reschedule_required rescheduleRequired
 2. \<And>ts runnable rv. corres dc (?Q50 ts runnable rv) (?Q'53 ts runnable rv) (possible_switch_to t) (possibleSwitchTo t)
 3. \<And>ts runnable. \<lbrace>?Q41 ts\<rbrace> gets cur_thread \<lbrace>\<lambda>rv. if t = rv then ?P49 ts runnable rv else ?Q50 ts runnable rv\<rbrace>
 4. \<And>ts runnable. \<lbrace>?Q'42 runnable\<rbrace> getCurThread \<lbrace>\<lambda>rv'. if t = rv' then ?P'52 ts runnable rv' else ?Q'53 ts runnable rv'\<rbrace>
 5. \<lbrace>?Q32 () () ()\<rbrace> get_thread_state t \<lbrace>\<lambda>ts x. runnable ts \<longrightarrow> ((\<lambda>_. True) and ?Q41 ts) x\<rbrace>
 6. \<lbrace>?Q'31 () () ()\<rbrace> isRunnable t \<lbrace>\<lambda>runnable x. runnable \<longrightarrow> ((\<lambda>_. True) and ?Q'42 runnable) x\<rbrace>
 7. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and ?Q32 () () a\<rbrace>
 8. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'31 () () a\<rbrace>
 9. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ts runnable rv. corres dc (?Q50 ts runnable rv) (?Q'53 ts runnable rv) (possible_switch_to t) (possibleSwitchTo t)
 2. \<And>ts runnable. \<lbrace>?Q41 ts\<rbrace> gets cur_thread \<lbrace>\<lambda>rv. if t = rv then weak_valid_sched_action and valid_etcbs else ?Q50 ts runnable rv\<rbrace>
 3. \<And>ts runnable. \<lbrace>?Q'42 runnable\<rbrace> getCurThread \<lbrace>\<lambda>rv'. if t = rv' then Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) else ?Q'53 ts runnable rv'\<rbrace>
 4. \<lbrace>?Q32 () () ()\<rbrace> get_thread_state t \<lbrace>\<lambda>ts x. runnable ts \<longrightarrow> ((\<lambda>_. True) and ?Q41 ts) x\<rbrace>
 5. \<lbrace>?Q'31 () () ()\<rbrace> isRunnable t \<lbrace>\<lambda>runnable x. runnable \<longrightarrow> ((\<lambda>_. True) and ?Q'42 runnable) x\<rbrace>
 6. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and ?Q32 () () a\<rbrace>
 7. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'31 () () a\<rbrace>
 8. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 10. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>ts runnablea. \<lbrace>?Q41 ts\<rbrace> gets cur_thread \<lbrace>\<lambda>rv. if t = rv then weak_valid_sched_action and valid_etcbs else valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t\<rbrace>
 2. \<And>ts runnable. \<lbrace>?Q'42 runnable\<rbrace> getCurThread \<lbrace>\<lambda>rv'. if t = rv' then Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) else Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs'\<rbrace>
 3. \<lbrace>?Q32 () () ()\<rbrace> get_thread_state t \<lbrace>\<lambda>ts x. runnable ts \<longrightarrow> ((\<lambda>_. True) and ?Q41 ts) x\<rbrace>
 4. \<lbrace>?Q'31 () () ()\<rbrace> isRunnable t \<lbrace>\<lambda>runnable x. runnable \<longrightarrow> ((\<lambda>_. True) and ?Q'42 runnable) x\<rbrace>
 5. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and ?Q32 () () a\<rbrace>
 6. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and ?Q'31 () () a\<rbrace>
 7. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 9. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 10. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q13 ()\<rbrace> ethread_set (tcb_priority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at t and (\<lambda>a. (\<forall>st. st_tcb_at ((=) st) t a \<longrightarrow> t = cur_thread a \<longrightarrow> runnable st \<longrightarrow> weak_valid_sched_action a \<and> valid_etcbs a) \<and> (\<forall>st. st_tcb_at ((=) st) t a \<longrightarrow> t \<noteq> cur_thread a \<longrightarrow> runnable st \<longrightarrow> valid_etcbs a \<and> weak_valid_sched_action a \<and> cur_tcb a \<and> st_tcb_at runnable t a))\<rbrace>
 2. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and (\<lambda>a. (t = ksCurThread a \<longrightarrow> st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a) \<and> (t \<noteq> ksCurThread a \<longrightarrow> st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> cur_tcb' a \<and> tcb_at' t a \<and> st_tcb_at' runnable' t a \<and> valid_objs' a))\<rbrace>
 3. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and ?Q13 y\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 5. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 6. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a. tcb_at' t and (\<lambda>a. (t = ksCurThread a \<longrightarrow> st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a) \<and> (t \<noteq> ksCurThread a \<longrightarrow> st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> cur_tcb' a \<and> tcb_at' t a \<and> st_tcb_at' runnable' t a \<and> valid_objs' a))\<rbrace>
 2. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and (\<lambda>a. tcb_at t a \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t a \<longrightarrow> \<not> t \<noteq> cur_thread a \<longrightarrow> \<not> \<not> runnable x \<longrightarrow> weak_valid_sched_action a \<and> valid_etcbs a) \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t a \<longrightarrow> \<not> \<not> t \<noteq> cur_thread a \<longrightarrow> \<not> \<not> runnable x \<longrightarrow> valid_etcbs a \<and> weak_valid_sched_action a \<and> cur_tcb a \<and> st_tcb_at runnable t a))\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 4. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 5. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'15 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>a b. tcb_at' t b \<and> (t = ksCurThread b \<longrightarrow> st_tcb_at' runnable' (ksCurThread b) b \<longrightarrow> Invariants_H.valid_queues b \<and> valid_queues' b \<and> weak_sch_act_wf (ksSchedulerAction b) b) \<and> (t \<noteq> ksCurThread b \<longrightarrow> st_tcb_at' runnable' t b \<longrightarrow> Invariants_H.valid_queues b \<and> valid_queues' b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> cur_tcb' b \<and> tcb_at' t b \<and> valid_objs' b)\<rbrace>
 2. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and (\<lambda>a. tcb_at t a \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t a \<longrightarrow> \<not> t \<noteq> cur_thread a \<longrightarrow> \<not> \<not> runnable x \<longrightarrow> weak_valid_sched_action a \<and> valid_etcbs a) \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t a \<longrightarrow> \<not> \<not> t \<noteq> cur_thread a \<longrightarrow> \<not> \<not> runnable x \<longrightarrow> valid_etcbs a \<and> weak_valid_sched_action a \<and> cur_tcb a \<and> st_tcb_at runnable t a))\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and ?Q'15 ya\<rbrace>
 4. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 5. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y. tcb_at t and valid_etcbs and (\<lambda>a. tcb_at t a \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t a \<longrightarrow> \<not> t \<noteq> cur_thread a \<longrightarrow> \<not> \<not> runnable x \<longrightarrow> weak_valid_sched_action a \<and> valid_etcbs a) \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t a \<longrightarrow> \<not> \<not> t \<noteq> cur_thread a \<longrightarrow> \<not> \<not> runnable x \<longrightarrow> valid_etcbs a \<and> weak_valid_sched_action a \<and> cur_tcb a \<and> st_tcb_at runnable t a))\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>ya. tcb_at' t and (\<lambda>a. obj_at' (\<lambda>obj. if t = t then True else True) t a \<and> ((Invariants_H.valid_queues and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) a \<and> (valid_queues' and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) a \<and> weak_sch_act_wf (ksSchedulerAction a) a) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) a \<and> (valid_queues' and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> cur_tcb' a \<and> obj_at' (\<lambda>obj. if t = t then True else True) t a \<and> (valid_objs' and (\<lambda>_. x \<le> maxPriority)) a)\<rbrace>
 3. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and ?Q4) s
 4. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and ?Q'4) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (is_etcb_at t and (\<lambda>s. tcb_at t s \<and> valid_etcbs s \<and> tcb_at t s \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t s \<longrightarrow> \<not> \<not> \<not> t \<noteq> cur_thread s \<longrightarrow> \<not> \<not> \<not> \<not> runnable x \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<forall>x. \<not> \<not> st_tcb_at ((=) x) t s \<longrightarrow> \<not> \<not> \<not> \<not> t \<noteq> cur_thread s \<longrightarrow> \<not> \<not> \<not> \<not> runnable x \<longrightarrow> valid_etcbs s \<and> weak_valid_sched_action s \<and> cur_tcb s \<and> st_tcb_at runnable t s))) s
 2. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and (\<lambda>s. tcb_at' t s \<and> obj_at' (\<lambda>tcb. if t = t then True else True) t s \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> (valid_queues' and tcb_at' t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> (valid_queues' and tcb_at' t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> obj_at' (\<lambda>tcb. if t = t then True else True) t s \<and> valid_objs' s \<and> x \<le> maxPriority)) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(valid_etcbs and weak_valid_sched_action and cur_tcb) s; (Invariants_H.valid_queues and valid_queues' and cur_tcb' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>_. x \<le> maxPriority)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (tcb_at' t and Invariants_H.valid_queues and (\<lambda>s. tcb_at' t s \<and> obj_at' (\<lambda>tcb. if t = t then True else True) t s \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> (valid_queues' and tcb_at' t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> (valid_queues' and tcb_at' t) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> obj_at' (\<lambda>tcb. if t = t then True else True) t s \<and> valid_objs' s \<and> x \<le> maxPriority)) s' proof (prove)
goal:
No subgoals!