theory KHeap_DR

lemma tcb_sched_action_dcorres: "dcorres dc P P' (return ()) (tcb_sched_action f t)" apply (clarsimp simp: tcb_sched_action_def) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (rule dcorres_symb_exec_r) apply (clarsimp simp: set_tcb_queue_def modify_def bind_def return_def get_def put_def corres_underlying_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (tcb_sched_action f t) proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (f t queue)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc P (?Q' rv) (return ()) (do prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue rv prio;
set_tcb_queue rv prio (f t queue)
od)
 2. \<lbrace>P'\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rva. dcorres dc P (?Q'4 rv rva) (return ()) (do queue <- get_tcb_queue rv rva;
set_tcb_queue rv rva (f t queue)
od)
 2. \<And>rv. \<lbrace>?Q' rv\<rbrace> ethread_get tcb_priority t \<lbrace>?Q'4 rv\<rbrace>
 3. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>P'\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rva rvb. dcorres dc P (?Q'8 rv rva rvb) (return ()) (set_tcb_queue rv rva (f t rvb))
 2. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> get_tcb_queue rv rva \<lbrace>?Q'8 rv rva\<rbrace>
 3. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_tcb_queue rv rva \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>rv. \<lbrace>?Q' rv\<rbrace> ethread_get tcb_priority t \<lbrace>?Q'4 rv\<rbrace>
 5. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>P'\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. \<lbrace>?Q'4 rv rva\<rbrace> get_tcb_queue rv rva \<lbrace>?Q'8 rv rva\<rbrace>
 2. \<And>rv rva cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_tcb_queue rv rva \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>rv. \<lbrace>?Q' rv\<rbrace> ethread_get tcb_priority t \<lbrace>?Q'4 rv\<rbrace>
 4. \<And>rv cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_priority t \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<lbrace>P'\<rbrace> ethread_get tcb_domain t \<lbrace>?Q'\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!