theory KHeap_DP

lemma obj_exists_map_i:
  "<obj_id \<mapsto>o obj \<and>* R> s \<Longrightarrow> \<exists>obj'. (cdl_objects s obj_id = Some obj'
                                       \<and> object_clean obj = object_clean obj')" apply (clarsimp simp: sep_map_o_conj) apply (case_tac "cdl_objects s obj_id") apply (drule_tac x = "(obj_id,Fields)" in fun_cong) apply (clarsimp simp: lift_def object_to_sep_state_def object_project_def
      object_at_heap_def sep_state_projection_def
      sep_conj_def Let_unfold) apply (rule_tac x = a in exI,simp) apply (rule object_eqI) apply (drule_tac x = "(obj_id,Fields)" in fun_cong) apply (clarsimp simp: lift_def object_to_sep_state_def object_project_def
      object_at_heap_def sep_state_projection_def
      Let_unfold) apply (rule ext) apply (drule_tac x= "(obj_id,Slot x)" in fun_cong) apply (clarsimp simp: lift_def object_to_sep_state_def
      object_project_def sep_state_projection_def
      Let_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (obj_id \<mapsto>o obj \<and>* R) s \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = None\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj'
 2. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = None; (cdl.lift sep_heap s |` ({obj_id} \<times> UNIV)) (obj_id, Fields) = object_to_sep_state obj_id obj UNIV (obj_id, Fields)\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj'
 2. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_clean obj = object_clean obj' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_clean obj = object_clean a proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_wipe_slots (object_clean obj) = object_wipe_slots (object_clean a)
 2. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_slots (object_clean obj) = object_slots (object_clean a) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a; (cdl.lift sep_heap s |` ({obj_id} \<times> UNIV)) (obj_id, Fields) = object_to_sep_state obj_id obj UNIV (obj_id, Fields)\<rbrakk> \<Longrightarrow> object_wipe_slots (object_clean obj) = object_wipe_slots (object_clean a)
 2. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_slots (object_clean obj) = object_slots (object_clean a) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_slots (object_clean obj) = object_slots (object_clean a) proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>cdl.lift sep_heap s |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV; R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_slots (object_clean obj) x = object_slots (object_clean a) x proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>R (SepState (cdl.lift sep_heap s |` (UNIV - {obj_id} \<times> UNIV)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a; (cdl.lift sep_heap s |` ({obj_id} \<times> UNIV)) (obj_id, Slot x) = object_to_sep_state obj_id obj UNIV (obj_id, Slot x)\<rbrakk> \<Longrightarrow> object_slots (object_clean obj) x = object_slots (object_clean a) x proof (prove)
goal:
No subgoals!