theory Separation_SD

lemma sep_map_S_decomp:
  "\<lbrakk>dom (object_slots obj) = slots; finite slots\<rbrakk> \<Longrightarrow>
   (obj_id \<mapsto>S obj) = ((\<And>* slot \<in> slots. (obj_id,slot) \<mapsto>s obj)  \<and>* obj_id \<mapsto>E obj)" apply (case_tac "slots = {}") apply clarsimp apply (clarsimp simp: sep_map_E_def sep_map_S'_def sep_map_S_def) apply (subst sep_map_S_decomp' [where slots = slots]) apply clarsimp apply clarsimp apply (clarsimp simp: sep_map_E_def) apply (subst sep_map_S'_decomp, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom (object_slots obj) = slots; finite slots\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots = {}\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj)
 2. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_slots obj = (\<lambda>x. None); slots = {}\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = obj_id \<mapsto>E obj
 2. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> slots \<noteq> {}
 2. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> slots \<noteq> UNIV
 3. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, UNIV - slots) \<mapsto>S' obj) = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> slots \<noteq> UNIV
 2. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, UNIV - slots) \<mapsto>S' obj) = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom (object_slots obj) = slots; finite slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, UNIV - slots) \<mapsto>S' obj) = ((SETSEPCONJ slot:slots. (obj_id, slot) \<mapsto>s obj) \<and>* obj_id \<mapsto>E obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (dom (object_slots obj)); object_slots obj \<noteq> (\<lambda>x. None); slots = dom (object_slots obj)\<rbrakk> \<Longrightarrow> ((obj_id, dom (object_slots obj)) \<mapsto>S' obj \<and>* (obj_id, UNIV - dom (object_slots obj)) \<mapsto>S' obj) = ((SETSEPCONJ slot:dom (object_slots obj). (obj_id, slot) \<mapsto>s obj) \<and>* (obj_id, UNIV - dom (object_slots obj)) \<mapsto>S' obj) proof (prove)
goal:
No subgoals!