theory KHeap_DR

lemma set_thread_state_corres:
  "dcorres dc \<top> (not_idle_thread y and K (cap = infer_tcb_pending_op y st) and valid_etcbs)
    (KHeap_D.set_cap (y, tcb_pending_op_slot) cap)
    (KHeap_A.set_thread_state y st)" apply (simp add:set_thread_state_def) apply (rule dcorres_absorb_gets_the) apply (rule dcorres_rhs_noop_below) apply (rule set_thread_state_ext_dcorres) apply (rule corres_guard_imp) apply (rule set_pending_cap_corres) apply simp apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def) apply (rule hoare_TrueI)+ done

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