theory Separation_SD

lemma sep_map_S'_decomp_helper:
  "\<lbrakk>distinct slots; slots \<noteq> []\<rbrakk>
  \<Longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots" apply (induct slots arbitrary: obj) apply clarsimp apply (atomize) apply (case_tac "slots = []") apply (clarsimp simp: sep_map_S'_def sep_map_s_def) apply clarsimp apply (erule_tac x=obj in allE) apply (subgoal_tac "(obj_id, insert a (set slots)) \<mapsto>S' obj =
                      ((obj_id, set slots) \<mapsto>S' obj \<and>* (obj_id, a) \<mapsto>s obj)") apply (clarsimp simp: sep_conj_ac) apply (erule sep_map_S'_decomp') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct slots; slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots proof (prove)
goal (2 subgoals):
 1. \<And>obj. \<lbrakk>distinct []; [] \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set []) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) []
 2. \<And>a slots obj. \<lbrakk>\<And>obj. \<lbrakk>distinct slots; slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; distinct (a # slots); a # slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set (a # slots)) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) (a # slots) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>\<And>obj. \<lbrakk>distinct slots; slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; distinct (a # slots); a # slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set (a # slots)) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) (a # slots) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>\<forall>obj. distinct slots \<longrightarrow> slots \<noteq> [] \<longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; distinct (a # slots); a # slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set (a # slots)) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) (a # slots) proof (prove)
goal (2 subgoals):
 1. \<And>a slots obj. \<lbrakk>\<forall>obj. distinct slots \<longrightarrow> slots \<noteq> [] \<longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; distinct (a # slots); a # slots \<noteq> []; slots = []\<rbrakk> \<Longrightarrow> (obj_id, set (a # slots)) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) (a # slots)
 2. \<And>a slots obj. \<lbrakk>\<forall>obj. distinct slots \<longrightarrow> slots \<noteq> [] \<longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; distinct (a # slots); a # slots \<noteq> []; slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set (a # slots)) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) (a # slots) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>\<forall>obj. distinct slots \<longrightarrow> slots \<noteq> [] \<longrightarrow> (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; distinct (a # slots); a # slots \<noteq> []; slots \<noteq> []\<rbrakk> \<Longrightarrow> (obj_id, set (a # slots)) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) (a # slots) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>\<forall>obj. (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; slots \<noteq> []; a \<notin> set slots; distinct slots\<rbrakk> \<Longrightarrow> (obj_id, insert a (set slots)) \<mapsto>S' obj = ((obj_id, a) \<mapsto>s obj \<and>* \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>slots \<noteq> []; a \<notin> set slots; distinct slots; (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots\<rbrakk> \<Longrightarrow> (obj_id, insert a (set slots)) \<mapsto>S' obj = ((obj_id, a) \<mapsto>s obj \<and>* \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots) proof (prove)
goal (2 subgoals):
 1. \<And>a slots obj. \<lbrakk>slots \<noteq> []; a \<notin> set slots; distinct slots; (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots; (obj_id, insert a (set slots)) \<mapsto>S' obj = ((obj_id, set slots) \<mapsto>S' obj \<and>* (obj_id, a) \<mapsto>s obj)\<rbrakk> \<Longrightarrow> (obj_id, insert a (set slots)) \<mapsto>S' obj = ((obj_id, a) \<mapsto>s obj \<and>* \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots)
 2. \<And>a slots obj. \<lbrakk>slots \<noteq> []; a \<notin> set slots; distinct slots; (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots\<rbrakk> \<Longrightarrow> (obj_id, insert a (set slots)) \<mapsto>S' obj = ((obj_id, set slots) \<mapsto>S' obj \<and>* (obj_id, a) \<mapsto>s obj) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>slots \<noteq> []; a \<notin> set slots; distinct slots; (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots\<rbrakk> \<Longrightarrow> (obj_id, insert a (set slots)) \<mapsto>S' obj = ((obj_id, set slots) \<mapsto>S' obj \<and>* (obj_id, a) \<mapsto>s obj) proof (prove)
goal (1 subgoal):
 1. \<And>a slots obj. \<lbrakk>slots \<noteq> []; distinct slots; (obj_id, set slots) \<mapsto>S' obj = \<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots\<rbrakk> \<Longrightarrow> set slots \<noteq> {} proof (prove)
goal:
No subgoals!