theory Tcb_DR

lemma suspend_corres:
  "dcorres dc \<top> (tcb_at obj_id and not_idle_thread obj_id and invs and valid_etcbs)
     (Tcb_D.suspend obj_id) (IpcCancel_A.suspend obj_id)" apply (rule corres_guard_imp) apply (clarsimp simp: IpcCancel_A.suspend_def Tcb_D.suspend_def) apply (rule corres_split[OF finalise_cancel_ipc]) apply (rule dcorres_symb_exec_r[OF _ gts_inv gts_inv]) apply (rule dcorres_rhs_noop_above) apply (case_tac "rv = Running"; simp) apply (rule update_restart_pc_dcorres) apply simp apply (rule dcorres_rhs_noop_below_True[OF tcb_sched_action_dcorres]) apply (rule set_thread_state_corres) apply wp apply (case_tac "rv = Running"; simp) apply wp+ apply (wpsimp simp: not_idle_thread_def conj_comms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (normal_tcb_at obj_id and invs and valid_etcbs) (Tcb_D.suspend obj_id) (IpcCancel_A.suspend obj_id) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (Tcb_D.suspend obj_id) (IpcCancel_A.suspend obj_id)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do y <- CSpace_D.cancel_ipc obj_id;
KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap
od) (do y <- IpcCancel_A.cancel_ipc obj_id;
state <- get_thread_state obj_id;
y <- if state = Running then update_restart_pc obj_id else return ();
y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> dcorres dc (?R6 y) (?R'6 ya) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (do state <- get_thread_state obj_id;
y <- if state = Running then update_restart_pc obj_id else return ();
y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 2. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres dc (?R6 y) (?R'6 ya) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- if rv = Running then update_restart_pc obj_id else return ();
y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 2. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres (?anyrel17 y ya rv) (?R6 y) (?R'6 ya) (return ()) (if rv = Running then update_restart_pc obj_id else return ())
 2. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres dc (?Q17 y ya rv) (?Q'17 y ya rv) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 3. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R6 y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q17 y ya rv\<rbrace>
 4. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>yb. ?Q'17 y ya rv\<rbrace>
 5. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. dcorres (?anyrel17 () () Running) (?R6 ()) (?R'6 ()) (return ()) (update_restart_pc obj_id)
 2. \<And>rv. rv \<noteq> Running \<Longrightarrow> (\<exists>s. ?R6 () s \<and> (\<exists>s'. ?R'6 () s' \<and> transform s' = s)) \<longrightarrow> ?anyrel17 () () rv () ()
 3. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres dc (?Q17 y ya rv) (?Q'17 y ya rv) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 4. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R6 y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q17 y ya rv\<rbrace>
 5. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>yb. ?Q'17 y ya rv\<rbrace>
 6. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>rv. rv \<noteq> Running \<Longrightarrow> (\<exists>s. ?R6 () s \<and> (\<exists>s'. ?R'6 () s' \<and> transform s' = s)) \<longrightarrow> dc () ()
 2. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres dc (?Q17 y ya rv) (?Q'17 y ya rv) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 3. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R6 y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q17 y ya rv\<rbrace>
 4. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>yb. ?Q'17 y ya rv\<rbrace>
 5. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres dc (?Q17 y ya rv) (?Q'17 y ya rv) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- set_thread_state obj_id Inactive;
tcb_sched_action tcb_sched_dequeue obj_id
od)
 2. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R6 y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q17 y ya rv\<rbrace>
 3. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>yb. ?Q'17 y ya rv\<rbrace>
 4. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya rv. dc y ya \<Longrightarrow> dcorres dc (?Q17 y ya rv) (?Q'17 y ya rv) (KHeap_D.set_cap (obj_id, tcb_pending_op_slot) cdl_cap.NullCap) (set_thread_state obj_id Inactive)
 2. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R6 y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q17 y ya rv\<rbrace>
 3. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>yb. ?Q'17 y ya rv\<rbrace>
 4. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R6 y\<rbrace> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>y. not_idle_thread obj_id and K (cdl_cap.NullCap = infer_tcb_pending_op obj_id Inactive) and valid_etcbs\<rbrace>
 3. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>y ya rv. dc y ya \<Longrightarrow> \<lbrace>?R'6 ya\<rbrace> if rv = Running then update_restart_pc obj_id else return () \<lbrace>\<lambda>y. not_idle_thread obj_id and K (cdl_cap.NullCap = infer_tcb_pending_op obj_id Inactive) and valid_etcbs\<rbrace>
 2. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?R'6 ()\<rbrace> update_restart_pc obj_id \<lbrace>\<lambda>y. not_idle_thread obj_id and valid_etcbs\<rbrace>
 2. \<And>rv. rv \<noteq> Running \<Longrightarrow> \<lbrace>?R'6 ()\<rbrace> return () \<lbrace>\<lambda>y. not_idle_thread obj_id and valid_etcbs\<rbrace>
 3. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?R'6 ()\<rbrace> update_restart_pc obj_id \<lbrace>\<lambda>y s. not_idle_thread obj_id s \<and> valid_etcbs s\<rbrace>
 2. \<And>rv. rv \<noteq> Running \<Longrightarrow> \<lbrace>?R'6 ()\<rbrace> return () \<lbrace>\<lambda>y. not_idle_thread obj_id and valid_etcbs\<rbrace>
 3. \<lbrace>?Q6\<rbrace> CSpace_D.cancel_ipc obj_id \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> IpcCancel_A.cancel_ipc obj_id \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (normal_tcb_at obj_id and invs and valid_etcbs) s \<Longrightarrow> (not_idle_thread obj_id and invs and valid_etcbs and ?Q'6) s proof (prove)
goal:
No subgoals!