theory Intent_DR

lemma dcorres_set_object_tcb:
  "\<lbrakk> \<exists>etcb'. (transform_tcb (machine_state s') p' tcb' etcb' = Tcb tcb \<and> ekheap s' p' = Some etcb');
     p' \<noteq> idle_thread s'; kheap s' p' \<noteq> None; ekheap s' p' \<noteq> None \<rbrakk> \<Longrightarrow>
  dcorres dc ((=) (transform s')) ((=) s')
           (KHeap_D.set_object p' (Tcb tcb ))
           (KHeap_A.set_object p' (TCB tcb'))" apply (clarsimp simp: corres_underlying_def set_object_def get_object_def in_monad) apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def) apply (clarsimp simp: transform_def transform_current_thread_def) apply (clarsimp simp: transform_objects_def) apply (rule ext) apply clarsimp apply (clarsimp simp: option_map_def restrict_map_def map_add_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>etcb'. transform_tcb (machine_state s') p' tcb' etcb' = Tcb tcb \<and> ekheap s' p' = Some etcb'; p' \<noteq> idle_thread s'; kheap s' p' \<noteq> None; ekheap s' p' \<noteq> None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_object p' (Tcb tcb)) (KHeap_A.set_object p' (TCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>ya tcba. \<lbrakk>p' \<noteq> idle_thread s'; kheap s' p' = Some (TCB tcba); transform_tcb (machine_state s') p' tcb' ya = Tcb tcb; ekheap s' p' = Some ya\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_object p' (Tcb tcb) (transform s')). case x of (r, x) \<Rightarrow> transform (update_kheap ((kheap s')(p' \<mapsto> TCB tcb')) s') = x proof (prove)
goal (1 subgoal):
 1. \<And>ya tcba. \<lbrakk>p' \<noteq> idle_thread s'; kheap s' p' = Some (TCB tcba); transform_tcb (machine_state s') p' tcb' ya = Tcb tcb; ekheap s' p' = Some ya\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s')(p' \<mapsto> TCB tcb')) s') = dupdate_cdl_object p' (Tcb tcb) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>ya tcba. \<lbrakk>p' \<noteq> idle_thread s'; kheap s' p' = Some (TCB tcba); transform_tcb (machine_state s') p' tcb' ya = Tcb tcb; ekheap s' p' = Some ya\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(p' \<mapsto> TCB tcb')) s') = (transform_objects s')(p' \<mapsto> Tcb tcb) proof (prove)
goal (1 subgoal):
 1. \<And>ya tcba. \<lbrakk>p' \<noteq> idle_thread s'; kheap s' p' = Some (TCB tcba); transform_tcb (machine_state s') p' tcb' ya = Tcb tcb; ekheap s' p' = Some ya\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = p' then Some (TCB tcb') else (kheap s' |` (- {idle_thread s'} - {p'})) ptr)) = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr)))(p' \<mapsto> Tcb tcb) proof (prove)
goal (1 subgoal):
 1. \<And>ya tcba x. \<lbrakk>p' \<noteq> idle_thread s'; kheap s' p' = Some (TCB tcba); transform_tcb (machine_state s') p' tcb' ya = Tcb tcb; ekheap s' p' = Some ya\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = p' then Some (TCB tcb') else (kheap s' |` (- {idle_thread s'} - {p'})) ptr))) x = (((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr)))(p' \<mapsto> Tcb tcb)) x proof (prove)
goal (1 subgoal):
 1. \<And>ya tcba x. \<lbrakk>p' \<noteq> idle_thread s'; kheap s' p' = Some (TCB tcba); transform_tcb (machine_state s') p' tcb' ya = Tcb tcb; ekheap s' p' = Some ya; x \<noteq> p'\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) (if ptr = p' then Some (TCB tcb') else (kheap s' |` (- {idle_thread s'} - {p'})) ptr))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr))) x proof (prove)
goal:
No subgoals!