theory Finalise_DR

lemma set_cap_set_thread_state_inactive:
  "dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
   (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap)
   (set_thread_state thread Structures_A.thread_state.Inactive)" apply (clarsimp simp:set_thread_state_def) apply (rule dcorres_absorb_gets_the) apply (rule corres_guard_imp) apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres]) apply (rule set_pending_cap_corres) apply simp apply (clarsimp dest!:get_tcb_SomeD
    simp:obj_at_def infer_tcb_pending_op_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (set_thread_state thread Inactive) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (do tcb <- gets_the (get_tcb thread);
y <- KHeap_A.set_object thread (TCB (update_tcb_state Inactive tcb));
set_thread_state_ext thread
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- KHeap_A.set_object thread (TCB (update_tcb_state Inactive obj'));
set_thread_state_ext thread
od) proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc (?Q2 s' obj') (?Q'2 s' obj') (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (do y <- KHeap_A.set_object thread (TCB (update_tcb_state Inactive obj'));
set_thread_state_ext thread
od)
 2. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ?Q2 s' obj' s
 3. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ?Q'2 s' obj' s proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc (?Q2 s' obj') (?Q'2 s' obj') (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (KHeap_A.set_object thread (TCB (update_tcb_state Inactive obj')))
 2. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> ?Q2 s' obj' s
 3. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> ?Q'2 s' obj' s proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and ko_at (TCB obj') thread and K (cdl_cap.NullCap = infer_tcb_pending_op thread Inactive) and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s' obj' s. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and ko_at (TCB obj') thread and K (cdl_cap.NullCap = infer_tcb_pending_op thread Inactive) and valid_etcbs) s proof (prove)
goal:
No subgoals!