theory Separation_SD

lemma sep_map_general_disjoint:
  "\<lbrakk>(sep_map_general obj_id obj cmps \<and>* sep_map_general obj_id obj' cmps') s\<rbrakk>
  \<Longrightarrow> cmps \<inter> cmps' = {}" apply (clarsimp simp:sep_map_general_def sep_conj_def) apply (case_tac x,case_tac y) apply (clarsimp simp:object_to_sep_state_def map_disj_def
    sep_disj_sep_state_def sep_state_disj_def) apply (drule_tac a1 = "{obj_id}\<times>cmps" in
    disjoint_subset[OF dom_map_restrict]) apply (drule_tac a1 = "{obj_id}\<times>cmps'" in
    disjoint_subset2[OF dom_map_restrict]) apply (rule ccontr) apply (clarsimp dest!:int_not_emptyD) apply (erule_tac x = "(obj_id,x)" in in_empty_interE) apply (clarsimp simp:object_project_def split:cdl_component_id.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sep_map_general obj_id obj cmps \<and>* sep_map_general obj_id obj' cmps') s \<Longrightarrow> cmps \<inter> cmps' = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; sep_heap x = object_to_sep_state obj_id obj cmps; sep_irq_node x = (\<lambda>x. None); sep_heap y = object_to_sep_state obj_id obj' cmps'; sep_irq_node y = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> cmps \<inter> cmps' = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y x1 x2 x1a x2a. \<lbrakk>x ## y; s = x + y; sep_heap x = object_to_sep_state obj_id obj cmps; sep_irq_node x = (\<lambda>x. None); sep_heap y = object_to_sep_state obj_id obj' cmps'; sep_irq_node y = (\<lambda>x. None); x = SepState x1 x2; y = SepState x1a x2a\<rbrakk> \<Longrightarrow> cmps \<inter> cmps' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) \<inter> dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) = {}; s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None)\<rbrakk> \<Longrightarrow> cmps \<inter> cmps' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None); dom ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) |` ({obj_id} \<times> cmps)) \<inter> dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) = {}\<rbrakk> \<Longrightarrow> cmps \<inter> cmps' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None); dom ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) |` ({obj_id} \<times> cmps)) \<inter> dom ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) |` ({obj_id} \<times> cmps')) = {}\<rbrakk> \<Longrightarrow> cmps \<inter> cmps' = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None); dom ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) |` ({obj_id} \<times> cmps)) \<inter> dom ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) |` ({obj_id} \<times> cmps')) = {}; cmps \<inter> cmps' \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None); dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) \<inter> {obj_id} \<times> cmps \<inter> (dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) \<inter> {obj_id} \<times> cmps') = {}; x \<in> cmps; x \<in> cmps'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None); x \<in> cmps; x \<in> cmps'\<rbrakk> \<Longrightarrow> (obj_id, x) \<in> dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) \<inter> {obj_id} \<times> cmps
 2. \<And>x. \<lbrakk>s = SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) (\<lambda>x. None) + SepState (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) (\<lambda>x. None); x \<in> cmps; x \<in> cmps'\<rbrakk> \<Longrightarrow> (obj_id, x) \<in> dom (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id \<in> cmps' then Some (object_project comp_id obj') else None) \<inter> {obj_id} \<times> cmps' proof (prove)
goal:
No subgoals!