theory KHeap_DP

lemma obj_exists_map_f:
  "<obj_id \<mapsto>f obj \<and>* R> s \<Longrightarrow>
  \<exists>obj'. (cdl_objects s obj_id = Some obj' \<and> object_type obj = object_type obj')" apply (clarsimp simp: sep_map_f_conj Let_def) apply (case_tac "cdl_objects s obj_id") 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 (clarsimp simp: lift_def object_to_sep_state_def object_project_def
      object_at_heap_def sep_state_projection_def
      Let_unfold) apply (drule_tac f = object_type in arg_cong) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (obj_id \<mapsto>f obj \<and>* R) s \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_type obj = object_type obj' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift sep_heap s (obj_id, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((cdl.lift sep_heap s)((obj_id, Fields) := None)) (cdl.lift sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>obj'. cdl_objects s obj_id = Some obj' \<and> object_type obj = object_type obj' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cdl.lift sep_heap s (obj_id, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((cdl.lift sep_heap s)((obj_id, Fields) := None)) (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_type obj = object_type obj'
 2. \<And>a. \<lbrakk>cdl.lift sep_heap s (obj_id, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((cdl.lift sep_heap s)((obj_id, Fields) := None)) (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_type obj = object_type obj' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cdl.lift sep_heap s (obj_id, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((cdl.lift sep_heap s)((obj_id, Fields) := None)) (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_type obj = object_type obj' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cdl.lift sep_heap s (obj_id, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((cdl.lift sep_heap s)((obj_id, Fields) := None)) (cdl.lift sep_irq_node s)); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_type obj = object_type a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>object_wipe_slots (object_clean a) = object_wipe_slots (object_clean obj); R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); cdl_objects s obj_id = Some a\<rbrakk> \<Longrightarrow> object_type obj = object_type a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); cdl_objects s obj_id = Some a; object_type (object_wipe_slots (object_clean a)) = object_type (object_wipe_slots (object_clean obj))\<rbrakk> \<Longrightarrow> object_type obj = object_type a proof (prove)
goal:
No subgoals!