theory RWHelper_DP

lemma sep_map_dom_predicate:
  "\<lbrakk>sep_heap_dom P m; sep_irq_node_dom P m';
    <P \<and>* P'> b\<rbrakk>
  \<Longrightarrow> P (SepState (sep_heap (sep_state_projection b) |` m)
                  (sep_irq_node (sep_state_projection b) |` m'))" apply (clarsimp simp: sep_state_projection_def sep_conj_def
                        plus_sep_state_def sep_state_add_def) apply (drule(1) sep_heap_domD') apply (drule(1) sep_irq_node_domD') apply simp apply (case_tac x,case_tac y) apply (clarsimp simp: sep_state_projection_def sep_conj_def
                        sep_disj_sep_state_def sep_state_disj_def) apply (simp add: map_add_restrict_dom_left) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap_dom P m; sep_irq_node_dom P m'; cdl.lift (P \<and>* P') b\<rbrakk> \<Longrightarrow> P (SepState (cdl.lift sep_heap b |` m) (cdl.lift sep_irq_node b |` m')) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sep_heap_dom P m; sep_irq_node_dom P m'; x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects b obj_id)) = sep_heap x ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node b irq)) = sep_irq_node x ++ sep_irq_node y; P x; P' y\<rbrakk> \<Longrightarrow> P (SepState ((sep_heap x ++ sep_heap y) |` m) ((sep_irq_node x ++ sep_irq_node y) |` m')) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>sep_irq_node_dom P m'; x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects b obj_id)) = sep_heap x ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node b irq)) = sep_irq_node x ++ sep_irq_node y; P x; P' y; m = dom (sep_heap x)\<rbrakk> \<Longrightarrow> P (SepState ((sep_heap x ++ sep_heap y) |` m) ((sep_irq_node x ++ sep_irq_node y) |` m')) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects b obj_id)) = sep_heap x ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node b irq)) = sep_irq_node x ++ sep_irq_node y; P x; P' y; m = dom (sep_heap x); m' = dom (sep_irq_node x)\<rbrakk> \<Longrightarrow> P (SepState ((sep_heap x ++ sep_heap y) |` m) ((sep_irq_node x ++ sep_irq_node y) |` m')) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects b obj_id)) = sep_heap x ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node b irq)) = sep_irq_node x ++ sep_irq_node y; P x; P' y; m = dom (sep_heap x); m' = dom (sep_irq_node x)\<rbrakk> \<Longrightarrow> P (SepState ((sep_heap x ++ sep_heap y) |` dom (sep_heap x)) ((sep_irq_node x ++ sep_irq_node y) |` dom (sep_irq_node x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y x1 x2 x1a x2a. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects b obj_id)) = sep_heap x ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node b irq)) = sep_irq_node x ++ sep_irq_node y; P x; P' y; m = dom (sep_heap x); m' = dom (sep_irq_node x); x = SepState x1 x2; y = SepState x1a x2a\<rbrakk> \<Longrightarrow> P (SepState ((sep_heap x ++ sep_heap y) |` dom (sep_heap x)) ((sep_irq_node x ++ sep_irq_node y) |` dom (sep_irq_node x))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>(\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects b obj_id)) = x1 ++ x1a; (\<lambda>irq. Some (cdl_irq_node b irq)) = x2 ++ x2a; P (SepState x1 x2); P' (SepState x1a x2a); m = dom x1; m' = dom x2; x1 \<bottom> x1a; x2 \<bottom> x2a\<rbrakk> \<Longrightarrow> P (SepState ((x1 ++ x1a) |` dom x1) ((x2 ++ x2a) |` dom x2)) proof (prove)
goal:
No subgoals!