theory Separation_SD

lemma sep_map_decomp:
  "\<lbrakk>cmps \<inter> cmps' = {}\<rbrakk>
  \<Longrightarrow> (sep_map_general p obj cmps \<and>* sep_map_general p obj cmps') s =
      sep_map_general p obj (cmps \<union> cmps') s" apply (clarsimp simp: sep_conj_def map_disj_def sep_disj_sep_state_def sep_state_disj_def) apply (rule iffI) 
  (* (p \<mapsto>L obj \<and>* p \<mapsto>R obj) \<Longrightarrow> p \<mapsto> obj *)
    apply (clarsimp simp: sep_map_general_def plus_sep_state_def
                         sep_state_add_def object_to_sep_state_add) 
  (* (p \<mapsto>L obj \<and>* p \<mapsto>R obj) \<Longleftarrow> p \<mapsto> obj *)
   apply (clarsimp simp:sep_map_general_def) apply (rule_tac x = "SepState (object_to_sep_state p obj cmps) Map.empty" in exI) apply (rule_tac x = "SepState (object_to_sep_state p obj cmps') Map.empty" in exI) apply (clarsimp simp: plus_sep_state_def sep_state_add_def object_to_sep_state_add) apply (intro conjI disjointI) apply (clarsimp simp: dom_def object_to_sep_state_def
                  split: if_splits) apply blast apply (case_tac s,simp) done

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