theory KHeap_DR

lemma corres_dummy_set_thread_state_Running:
  "dcorres dc \<top> (not_idle_thread thread and valid_etcbs)
  (KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap)
  (set_thread_state thread Structures_A.Running)" 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 simp: infer_tcb_pending_op_def
    tcb_at_def obj_at_def
    dest!: get_tcb_SomeD) apply (rule hoare_TrueI)+ 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) RunningCap) (set_thread_state thread Running) 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) RunningCap) (do tcb <- gets_the (get_tcb thread);
y <- KHeap_A.set_object thread (TCB (update_tcb_state Running 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) RunningCap) (do y <- KHeap_A.set_object thread (TCB (update_tcb_state Running obj'));
set_thread_state_ext thread
od) proof (prove)
goal (4 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') (return ()) (set_thread_state_ext thread)
 2. \<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) RunningCap) (KHeap_A.set_object thread (TCB (update_tcb_state Running obj')))
 3. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state Running obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> 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 ((=) (transform s')) ((=) s') (KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap) (KHeap_A.set_object thread (TCB (update_tcb_state Running obj')))
 2. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state Running obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (5 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 (?Q8 s' obj') (?Q'8 s' obj') (KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap) (KHeap_A.set_object thread (TCB (update_tcb_state Running 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> ?Q8 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'8 s' obj' s
 4. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 5. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state Running obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (4 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 (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs) s
 3. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 4. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state Running obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 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 (RunningCap = infer_tcb_pending_op thread Running) and valid_etcbs) s
 2. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state Running obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 2. \<And>s' obj'. \<lbrakk>(not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state Running obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal:
No subgoals!