theory Frame_SD

lemma sep_map_f_conj:
  "(ptr \<mapsto>f obj \<and>* R) s =
  (let slot = (ptr,Fields)
  in (sep_heap s) slot  = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and>
     R (SepState ((sep_heap s)(slot:= None)) (sep_irq_node s)))" apply (clarsimp simp:sep_conj_def Let_def plus_sep_state_def sep_state_add_def) apply (rule iffI) apply (clarsimp simp:sep_map_f_def sep_disj_sep_state_def
     sep_map_general_def sep_state_disj_def map_disj_def) apply (subst object_to_sep_state_add) apply (simp add:dom_object_to_sep_state singleton_iff)+ apply (simp add:object_project_def) apply (erule arg_cong[where f = R,THEN iffD1,rotated]) apply (case_tac y) apply simp apply (rule ext) apply (clarsimp simp:dom_def map_add_def
     object_to_sep_state_def split:if_splits option.splits) apply (clarsimp simp:sep_map_c_def) apply (rule_tac x = "SepState [(ptr,Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))]
                                Map.empty" in exI) apply (rule_tac x = "SepState ((sep_heap s)((ptr,Fields):= None))
                                (sep_irq_node s)" in exI) apply (clarsimp simp:sep_map_f_def sep_disj_sep_state_def
     sep_map_general_def sep_state_disj_def map_disj_def) apply (intro conjI) apply (case_tac s,simp) apply (rule ext) apply (clarsimp simp:map_add_def split:option.splits) apply (clarsimp simp:object_to_sep_state_def split:if_splits) apply (rule ext) apply (clarsimp simp:object_project_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>f obj \<and>* R) s = (let slot = (ptr, Fields) in sep_heap s slot = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)(slot := None)) (sep_irq_node s))) proof (prove)
goal (1 subgoal):
 1. (\<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y) = (sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))) proof (prove)
goal (2 subgoals):
 1. \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y \<Longrightarrow> sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj {Fields}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((object_to_sep_state ptr obj {Fields} ++ sep_heap y)((ptr, Fields) := None)) (sep_irq_node y))
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj {Fields}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> {ptr} \<times> {Fields} \<inter> dom (sep_heap y) = {}
 2. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj {Fields}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> Fields \<in> {Fields}
 3. \<And>x y. \<lbrakk>dom (object_to_sep_state ptr obj {Fields}) \<inter> dom (sep_heap y) = {}; s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> Some (object_project Fields obj) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((object_to_sep_state ptr obj {Fields} ++ sep_heap y)((ptr, Fields) := None)) (sep_irq_node y))
 4. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>(ptr, Fields) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> object_project Fields obj = CDL_Object (object_wipe_slots (object_clean obj)) \<and> R (SepState ((object_to_sep_state ptr obj {Fields} ++ sep_heap y)((ptr, Fields) := None)) (sep_irq_node y))
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>(ptr, Fields) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); R y\<rbrakk> \<Longrightarrow> R (SepState ((object_to_sep_state ptr obj {Fields} ++ sep_heap y)((ptr, Fields) := None)) (sep_irq_node y))
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>(ptr, Fields) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> y = SepState ((object_to_sep_state ptr obj {Fields} ++ sep_heap y)((ptr, Fields) := None)) (sep_irq_node y)
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y x1 x2. \<lbrakk>(ptr, Fields) \<notin> dom (sep_heap y); s = SepState (object_to_sep_state ptr obj {Fields} ++ sep_heap y) (sep_irq_node y); sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); y = SepState x1 x2\<rbrakk> \<Longrightarrow> y = SepState ((object_to_sep_state ptr obj {Fields} ++ sep_heap y)((ptr, Fields) := None)) (sep_irq_node y)
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y x1 x2. \<lbrakk>(ptr, Fields) \<notin> dom x1; s = SepState (object_to_sep_state ptr obj {Fields} ++ x1) x2; sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); y = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 = (object_to_sep_state ptr obj {Fields} ++ x1)((ptr, Fields) := None)
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (2 subgoals):
 1. \<And>x y x1 x2 xa. \<lbrakk>(ptr, Fields) \<notin> dom x1; s = SepState (object_to_sep_state ptr obj {Fields} ++ x1) x2; sep_heap x = object_to_sep_state ptr obj {Fields}; sep_irq_node x = (\<lambda>x. None); y = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 xa = ((object_to_sep_state ptr obj {Fields} ++ x1)((ptr, Fields) := None)) xa
 2. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (1 subgoal):
 1. sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>x y. x ## y \<and> s = SepState (sep_heap x ++ sep_heap y) (sep_irq_node x ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) x \<and> R y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> \<exists>y. SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None) ## y \<and> s = SepState (sep_heap (SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None)) ++ sep_heap y) (sep_irq_node (SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None)) ++ sep_irq_node y) \<and> (ptr \<mapsto>f obj) (SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None)) \<and> R y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None) ## SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s) \<and> s = SepState (sep_heap (SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None)) ++ sep_heap (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))) (sep_irq_node (SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None)) ++ sep_irq_node (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))) \<and> (ptr \<mapsto>f obj) (SepState [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] (\<lambda>x. None)) \<and> R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> s = SepState ([(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] ++ (sep_heap s)((ptr, Fields) := None)) (sep_irq_node s) \<and> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] = object_to_sep_state ptr obj {Fields} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> s = SepState ([(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] ++ (sep_heap s)((ptr, Fields) := None)) (sep_irq_node s)
 2. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] = object_to_sep_state ptr obj {Fields} proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>x1 (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState (x1((ptr, Fields) := None)) x2); s = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 = [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] ++ x1((ptr, Fields) := None)
 2. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] = object_to_sep_state ptr obj {Fields} proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x. \<lbrakk>x1 (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState (x1((ptr, Fields) := None)) x2); s = SepState x1 x2\<rbrakk> \<Longrightarrow> x1 x = ([(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] ++ x1((ptr, Fields) := None)) x
 2. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] = object_to_sep_state ptr obj {Fields} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] = object_to_sep_state ptr obj {Fields} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] = (\<lambda>(obj_id', comp_id). if obj_id' = ptr \<and> comp_id = Fields then Some (object_project comp_id obj) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sep_heap s (ptr, Fields) = Some (CDL_Object (object_wipe_slots (object_clean obj))); R (SepState ((sep_heap s)((ptr, Fields) := None)) (sep_irq_node s))\<rbrakk> \<Longrightarrow> [(ptr, Fields) \<mapsto> CDL_Object (object_wipe_slots (object_clean obj))] x = (case x of (obj_id', comp_id) \<Rightarrow> if obj_id' = ptr \<and> comp_id = Fields then Some (object_project comp_id obj) else None) proof (prove)
goal:
No subgoals!