theory KHeap_DR

lemma get_object_corres:
  "ptr = ptr' \<Longrightarrow>
   dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv')
      \<top> (not_idle_thread ptr' and obj_at (Not o is_tcb) ptr')
      (KHeap_D.get_object ptr) (KHeap_A.get_object ptr')" apply (clarsimp simp: KHeap_A.get_object_def gets_the_def) apply (rule corres_underlying_split[OF _ _ gets_sp gets_sp, where r'=dc]) apply simp apply (clarsimp simp: assert_def corres_free_fail split: if_split) apply (rule_tac F="rv = Some (transform_object undefined 0 etcb' y)" in corres_req) apply (simp_all add: assert_opt_def) apply (clarsimp simp: transform_def transform_objects_def
                        not_idle_thread_def obj_at_def) apply (clarsimp simp: transform_object_def
                 split: Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr = ptr' \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv') (\<lambda>_. True) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr') (KHeap_D.get_object ptr) (KHeap_A.get_object ptr') proof (prove)
goal (1 subgoal):
 1. ptr = ptr' \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv') (\<lambda>_. True) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr') (gets (\<lambda>s. cdl_objects s ptr') >>= assert_opt) (do kh <- gets kheap;
y <- assert (\<exists>y. kh ptr' = Some y);
return (the (kh ptr'))
od) proof (prove)
goal (2 subgoals):
 1. ptr = ptr' \<Longrightarrow> dcorres dc (\<lambda>_. True) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr') (gets (\<lambda>s. cdl_objects s ptr')) (gets kheap)
 2. \<And>rv kh. \<lbrakk>ptr = ptr'; dc rv kh\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv') ((\<lambda>_. True) and (\<lambda>s. cdl_objects s ptr' = rv)) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr' and (\<lambda>s. kheap s = kh)) (assert_opt rv) (do y <- assert (\<exists>y. kh ptr' = Some y);
return (the (kh ptr'))
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv kh. \<lbrakk>ptr = ptr'; dc rv kh\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv') ((\<lambda>_. True) and (\<lambda>s. cdl_objects s ptr' = rv)) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr' and (\<lambda>s. kheap s = kh)) (assert_opt rv) (do y <- assert (\<exists>y. kh ptr' = Some y);
return (the (kh ptr'))
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv kh y. \<lbrakk>ptr = ptr'; kh ptr' = Some y\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv') (\<lambda>s. cdl_objects s ptr' = rv) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr' and (\<lambda>s. kheap s = kh)) (assert_opt rv) (return y) proof (prove)
goal (2 subgoals):
 1. \<And>rv kh y s s'. \<lbrakk>ptr = ptr'; kh ptr' = Some y; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; cdl_objects s ptr' = rv; (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr' and (\<lambda>s. kheap s = kh)) s'\<rbrakk> \<Longrightarrow> rv = Some (transform_object undefined 0 etcb' y)
 2. \<And>rv kh y. \<lbrakk>ptr = ptr'; kh ptr' = Some y; rv = Some (transform_object undefined 0 etcb' y)\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = transform_object undefined 0 etcb' rv') (\<lambda>s. cdl_objects s ptr' = rv) (not_idle_thread ptr' and obj_at (Not \<circ> is_tcb) ptr' and (\<lambda>s. kheap s = kh)) (assert_opt rv) (return y) proof (prove)
goal (1 subgoal):
 1. \<And>rv y s s'. \<lbrakk>ptr = ptr'; kheap s' ptr' = Some y; transform s' = s; cdl_objects s ptr' = rv; not_idle_thread ptr' s' \<and> obj_at (Not \<circ> is_tcb) ptr' s'\<rbrakk> \<Longrightarrow> rv = Some (transform_object undefined 0 etcb' y) proof (prove)
goal (1 subgoal):
 1. \<And>y s'. \<lbrakk>ptr = ptr'; kheap s' ptr' = Some y; ptr' \<noteq> idle_thread s'; \<not> is_tcb y\<rbrakk> \<Longrightarrow> transform_object (machine_state s') ptr' (ekheap s' ptr') y = transform_object undefined 0 etcb' y proof (prove)
goal:
No subgoals!