kings-crown/FVELER_Isabelle huggingface dataset:
theory Separation_SD

lemma sep_map_general_inj:
  "cmps \<noteq> {} \<Longrightarrow> inj (\<lambda>obj_id. sep_map_general obj_id object cmps)" apply (clarsimp simp: inj_on_def fun_eq_iff sep_map_general_def) apply (erule_tac x="SepState (object_to_sep_state x object cmps) Map.empty" in allE) apply (fastforce simp: object_to_sep_state_def
                  split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmps \<noteq> {} \<Longrightarrow> inj (\<lambda>obj_id. sep_map_general obj_id object cmps) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>cmps \<noteq> {}; \<forall>xa. ((\<forall>a b. sep_heap xa (a, b) = object_to_sep_state x object cmps (a, b)) \<and> (\<forall>x. sep_irq_node xa x = None)) = ((\<forall>a b. sep_heap xa (a, b) = object_to_sep_state y object cmps (a, b)) \<and> (\<forall>x. sep_irq_node xa x = None))\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>cmps \<noteq> {}; ((\<forall>a b. sep_heap (SepState (object_to_sep_state x object cmps) (\<lambda>x. None)) (a, b) = object_to_sep_state x object cmps (a, b)) \<and> (\<forall>xa. sep_irq_node (SepState (object_to_sep_state x object cmps) (\<lambda>x. None)) xa = None)) = ((\<forall>a b. sep_heap (SepState (object_to_sep_state x object cmps) (\<lambda>x. None)) (a, b) = object_to_sep_state y object cmps (a, b)) \<and> (\<forall>xa. sep_irq_node (SepState (object_to_sep_state x object cmps) (\<lambda>x. None)) xa = None))\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_o_inj:
  "inj (\<lambda>obj_id. obj_id \<mapsto>o obj)" by (clarsimp simp: sep_map_o_def sep_map_general_inj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>obj_id. obj_id \<mapsto>o obj)
theory Separation_SD

lemma sep_map_f_inj:
  "inj (\<lambda>obj_id. obj_id \<mapsto>f obj)" by (clarsimp simp: sep_map_f_def sep_map_general_inj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>obj_id. obj_id \<mapsto>f obj)
theory Separation_SD

lemma sep_map_s_inj:
  "inj (\<lambda>obj_id. obj_id \<mapsto>s obj)" apply (clarsimp simp: inj_on_def fun_eq_iff sep_map_s_def sep_map_general_def) apply (erule_tac x="SepState (object_to_sep_state a obj {Slot b}) Map.empty" in allE) apply (fastforce simp: object_to_sep_state_def
                  split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>obj_id. obj_id \<mapsto>s obj) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<forall>x. ((\<forall>aa ba. sep_heap x (aa, ba) = object_to_sep_state a obj {Slot b} (aa, ba)) \<and> (\<forall>xa. sep_irq_node x xa = None)) = ((\<forall>a b. sep_heap x (a, b) = object_to_sep_state aa obj {Slot ba} (a, b)) \<and> (\<forall>xa. sep_irq_node x xa = None)) \<Longrightarrow> a = aa \<and> b = ba proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. ((\<forall>aa ba. sep_heap (SepState (object_to_sep_state a obj {Slot b}) (\<lambda>x. None)) (aa, ba) = object_to_sep_state a obj {Slot b} (aa, ba)) \<and> (\<forall>x. sep_irq_node (SepState (object_to_sep_state a obj {Slot b}) (\<lambda>x. None)) x = None)) = ((\<forall>ab bb. sep_heap (SepState (object_to_sep_state a obj {Slot b}) (\<lambda>x. None)) (ab, bb) = object_to_sep_state aa obj {Slot ba} (ab, bb)) \<and> (\<forall>x. sep_irq_node (SepState (object_to_sep_state a obj {Slot b}) (\<lambda>x. None)) x = None)) \<Longrightarrow> a = aa \<and> b = ba proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_c_inj:
  "inj (\<lambda>(obj_id,slot). (obj_id,slot) \<mapsto>c cap)" apply (clarsimp simp: inj_on_def fun_eq_iff sep_map_c_def sep_map_general_def) apply (erule_tac x="SepState (object_to_sep_state a
                                                 (CNode \<lparr> cdl_cnode_caps = [b \<mapsto> cap],
                                                          cdl_cnode_size_bits = 0 \<rparr>)
                                                 {Slot b})
                                Map.empty" in allE) apply (auto simp: object_to_sep_state_def object_project_def object_slots_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>(obj_id, slot). (obj_id, slot) \<mapsto>c cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<forall>x. (\<exists>obj. (\<forall>aa ba. sep_heap x (aa, ba) = object_to_sep_state a obj {Slot b} (aa, ba)) \<and> (\<forall>xa. sep_irq_node x xa = None) \<and> (\<forall>x. (x = b \<longrightarrow> object_slots obj b = Some cap) \<and> (x \<noteq> b \<longrightarrow> object_slots obj x = None))) = (\<exists>obj. (\<forall>a b. sep_heap x (a, b) = object_to_sep_state aa obj {Slot ba} (a, b)) \<and> (\<forall>xa. sep_irq_node x xa = None) \<and> (\<forall>x. (x = ba \<longrightarrow> object_slots obj ba = Some cap) \<and> (x \<noteq> ba \<longrightarrow> object_slots obj x = None))) \<Longrightarrow> a = aa \<and> b = ba proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. (\<exists>obj. (\<forall>aa ba. sep_heap (SepState (object_to_sep_state a (CNode \<lparr>cdl_cnode_caps = [b \<mapsto> cap], cdl_cnode_size_bits = 0\<rparr>) {Slot b}) (\<lambda>x. None)) (aa, ba) = object_to_sep_state a obj {Slot b} (aa, ba)) \<and> (\<forall>x. sep_irq_node (SepState (object_to_sep_state a (CNode \<lparr>cdl_cnode_caps = [b \<mapsto> cap], cdl_cnode_size_bits = 0\<rparr>) {Slot b}) (\<lambda>x. None)) x = None) \<and> (\<forall>x. (x = b \<longrightarrow> object_slots obj b = Some cap) \<and> (x \<noteq> b \<longrightarrow> object_slots obj x = None))) = (\<exists>obj. (\<forall>ab bb. sep_heap (SepState (object_to_sep_state a (CNode \<lparr>cdl_cnode_caps = [b \<mapsto> cap], cdl_cnode_size_bits = 0\<rparr>) {Slot b}) (\<lambda>x. None)) (ab, bb) = object_to_sep_state aa obj {Slot ba} (ab, bb)) \<and> (\<forall>x. sep_irq_node (SepState (object_to_sep_state a (CNode \<lparr>cdl_cnode_caps = [b \<mapsto> cap], cdl_cnode_size_bits = 0\<rparr>) {Slot b}) (\<lambda>x. None)) x = None) \<and> (\<forall>x. (x = ba \<longrightarrow> object_slots obj ba = Some cap) \<and> (x \<noteq> ba \<longrightarrow> object_slots obj x = None))) \<Longrightarrow> a = aa \<and> b = ba proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma range_Slot [simp]:
  "(range Slot) = (UNIV - {Fields})" apply (clarsimp simp: image_def) apply rule apply clarsimp+ apply (case_tac x) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range Slot = UNIV - {Fields} proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x. y = Slot x} = UNIV - {Fields} proof (prove)
goal (2 subgoals):
 1. {y. \<exists>x. y = Slot x} \<subseteq> UNIV - {Fields}
 2. UNIV - {Fields} \<subseteq> {y. \<exists>x. y = Slot x} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<noteq> Fields \<Longrightarrow> \<exists>xa. x = Slot xa proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> Fields; x = Fields\<rbrakk> \<Longrightarrow> \<exists>xa. x = Slot xa
 2. \<And>x x2. \<lbrakk>x \<noteq> Fields; x = Slot x2\<rbrakk> \<Longrightarrow> \<exists>xa. x = Slot xa proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma Slot_slot_union:
  "insert (Slot slot) (Slot ` (UNIV - {slot})) = UNIV - {Fields}" apply rule apply clarsimp+ apply (case_tac x) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. insert (Slot slot) (Slot ` (UNIV - {slot})) = UNIV - {Fields} proof (prove)
goal (2 subgoals):
 1. insert (Slot slot) (Slot ` (UNIV - {slot})) \<subseteq> UNIV - {Fields}
 2. UNIV - {Fields} \<subseteq> insert (Slot slot) (Slot ` (UNIV - {slot})) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> Slot ` (UNIV - {slot}); x \<noteq> Slot slot\<rbrakk> \<Longrightarrow> x = Fields proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<notin> Slot ` (UNIV - {slot}); x \<noteq> Slot slot; x = Fields\<rbrakk> \<Longrightarrow> x = Fields
 2. \<And>x x2. \<lbrakk>x \<notin> Slot ` (UNIV - {slot}); x \<noteq> Slot slot; x = Slot x2\<rbrakk> \<Longrightarrow> x = Fields proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma object_type_intent_reset [simp]:
  "object_type (intent_reset obj) = object_type obj" by (clarsimp simp: intent_reset_def object_type_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (intent_reset obj) = object_type obj
theory Separation_SD

lemma object_type_asid_reset [simp]:
  "object_type (asid_reset obj) = object_type obj" by (clarsimp simp: asid_reset_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (asid_reset obj) = object_type obj
theory Separation_SD

lemma object_type_object_clean [simp]:
  "object_type (object_clean obj) = object_type obj" by (clarsimp simp: object_clean_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean obj) = object_type obj
theory Separation_SD

lemma dom_map_restrict:
  "dom (f |` a) \<subseteq> dom f" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (f |` a) \<subseteq> dom f
theory Separation_SD

lemma object_type_object_wipe_slots[simp]:
  "object_type (object_wipe_slots obj) = object_type obj" by (clarsimp simp: object_wipe_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (object_wipe_slots obj) = object_type obj
theory Separation_SD

lemma object_slots_intent_reset [simp]:
  "object_slots (intent_reset obj) = object_slots obj" by (clarsimp simp: intent_reset_def object_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots (intent_reset obj) = object_slots obj
theory Separation_SD

lemma update_slots_intent_reset [simp]:
  "intent_reset (update_slots slots obj) = update_slots slots (intent_reset obj)" by (clarsimp simp: intent_reset_def update_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intent_reset (update_slots slots obj) = update_slots slots (intent_reset obj)
theory Separation_SD

lemma object_wipe_slots_intent_reset [simp]:
  "intent_reset (object_wipe_slots obj)
  = object_wipe_slots (intent_reset obj)" by (clarsimp simp: object_wipe_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intent_reset (object_wipe_slots obj) = object_wipe_slots (intent_reset obj)
theory Separation_SD

lemma object_wipe_slots_asid_reset [simp]:
  "object_wipe_slots (asid_reset obj) = asid_reset (object_wipe_slots obj)" apply (clarsimp simp: object_wipe_slots_def asid_reset_def) apply (case_tac "has_slots obj", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_wipe_slots (asid_reset obj) = asid_reset (object_wipe_slots obj) proof (prove)
goal (1 subgoal):
 1. update_slots (\<lambda>x. None) obj = update_slots (reset_cap_asid o_M object_slots (update_slots (\<lambda>x. None) obj)) obj proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma object_filds_update_slots[simp]:
  "object_wipe_slots (update_slots slots obj) = object_wipe_slots obj" apply (simp add:update_slots_def split:cdl_object.splits) apply (simp add:object_wipe_slots_def update_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_wipe_slots (update_slots slots obj) = object_wipe_slots obj proof (prove)
goal (1 subgoal):
 1. (\<forall>x3. obj = Tcb x3 \<longrightarrow> object_wipe_slots (Tcb (x3\<lparr>cdl_tcb_caps := slots\<rparr>)) = object_wipe_slots (Tcb x3)) \<and> (\<forall>x4. obj = CNode x4 \<longrightarrow> object_wipe_slots (CNode (x4\<lparr>cdl_cnode_caps := slots\<rparr>)) = object_wipe_slots (CNode x4)) \<and> (\<forall>x5. obj = AsidPool x5 \<longrightarrow> object_wipe_slots (AsidPool (x5\<lparr>cdl_asid_pool_caps := slots\<rparr>)) = object_wipe_slots (AsidPool x5)) \<and> (\<forall>x6. obj = PageTable x6 \<longrightarrow> object_wipe_slots (PageTable (x6\<lparr>cdl_page_table_caps := slots\<rparr>)) = object_wipe_slots (PageTable x6)) \<and> (\<forall>x7. obj = PageDirectory x7 \<longrightarrow> object_wipe_slots (PageDirectory (x7\<lparr>cdl_page_directory_caps := slots\<rparr>)) = object_wipe_slots (PageDirectory x7)) \<and> (\<forall>x10. obj = IRQNode x10 \<longrightarrow> object_wipe_slots (IRQNode (x10\<lparr>cdl_irq_node_caps := slots\<rparr>)) = object_wipe_slots (IRQNode x10)) proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma object_wipe_slots_idem[simp]:
  "object_wipe_slots (object_wipe_slots obj) = object_wipe_slots obj" by (case_tac obj,simp_all add: object_wipe_slots_def object_slots_def
     update_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_wipe_slots (object_wipe_slots obj) = object_wipe_slots obj
theory Separation_SD

lemma object_slots_update_slots[simp]:
  "\<lbrakk>has_slots obj'; object_type obj = object_type obj'\<rbrakk>
  \<Longrightarrow> object_slots (update_slots slots obj) slot = slots slot" by (clarsimp simp:has_slots_def object_type_def split:cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_slots obj'; object_type obj = object_type obj'\<rbrakk> \<Longrightarrow> object_slots (update_slots slots obj) slot = slots slot
theory Separation_SD

lemma product_union:
  "{p} \<times> (cmps \<union> cmps') = ({p} \<times> cmps) \<union> ({p} \<times> cmps')" by (rule Sigma_Un_distrib2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {p} \<times> (cmps \<union> cmps') = {p} \<times> cmps \<union> {p} \<times> cmps'
theory Separation_SD

lemma object_to_sep_state_add:
  "object_to_sep_state p obj cmps ++ object_to_sep_state p obj cmps' =
  object_to_sep_state p obj (cmps \<union> cmps')" apply (rule ext) apply (clarsimp simp:object_to_sep_state_def split_def
    map_add_def split:if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_to_sep_state p obj cmps ++ object_to_sep_state p obj cmps' = object_to_sep_state p obj (cmps \<union> cmps') proof (prove)
goal (1 subgoal):
 1. \<And>x. (object_to_sep_state p obj cmps ++ object_to_sep_state p obj cmps') x = object_to_sep_state p obj (cmps \<union> cmps') x proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_o_decomp:
  "p \<mapsto>o obj = (p \<mapsto>f obj \<and>* p \<mapsto>S obj)" apply (rule ext, rename_tac s) apply (clarsimp simp: sep_map_o_def sep_map_f_def sep_map_S_def) apply (subgoal_tac "{Fields} \<inter> (UNIV - {Fields}) = {}") apply (drule sep_map_decomp, fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<mapsto>o obj = (p \<mapsto>f obj \<and>* p \<mapsto>S obj) proof (prove)
goal (1 subgoal):
 1. \<And>s. (p \<mapsto>o obj) s = (p \<mapsto>f obj \<and>* p \<mapsto>S obj) s proof (prove)
goal (1 subgoal):
 1. \<And>s. sep_map_general p obj UNIV s = (sep_map_general p obj {Fields} \<and>* sep_map_general p obj (UNIV - {Fields})) s proof (prove)
goal (2 subgoals):
 1. \<And>s. {Fields} \<inter> (UNIV - {Fields}) = {} \<Longrightarrow> sep_map_general p obj UNIV s = (sep_map_general p obj {Fields} \<and>* sep_map_general p obj (UNIV - {Fields})) s
 2. \<And>s. {Fields} \<inter> (UNIV - {Fields}) = {} proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma intent_reset_has_slots[simp]:
  "has_slots (intent_reset obj) = has_slots obj" apply (simp add:intent_reset_def
    split:cdl_object.splits) apply (simp add:has_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. has_slots (intent_reset obj) = has_slots obj proof (prove)
goal (1 subgoal):
 1. \<forall>x3. obj = Tcb x3 \<longrightarrow> has_slots (Tcb (x3\<lparr>cdl_tcb_intent := undefined\<rparr>)) = has_slots (Tcb x3) proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma object_slots_some_has_slots:
  "object_slots obj slot = Some cap \<Longrightarrow> has_slots obj" by (metis object_slots_has_slots option.distinct(1))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots obj slot = Some cap \<Longrightarrow> has_slots obj
theory Separation_SD

lemma object_project_cap_project:
  "object_slots obj slot = Some cap \<Longrightarrow>
  object_project (Slot slot) obj = cap_project cap" apply (frule object_slots_some_has_slots) apply (clarsimp simp: object_project_def cap_project_def object_clean_def asid_reset_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots obj slot = Some cap \<Longrightarrow> object_project (Slot slot) obj = cap_project cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots obj slot = Some cap; has_slots obj\<rbrakk> \<Longrightarrow> object_project (Slot slot) obj = cap_project cap proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_s_sep_map_c_eq:
  "\<lbrakk>object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow>
  (obj_id, slot) \<mapsto>s obj = (obj_id, slot) \<mapsto>c cap" by (fastforce simp: sep_map_c_def_alt sep_map_s_def sep_map_S_def sep_map_general_def
                      object_to_sep_state_def cap_to_sep_state_def
                      object_project_cap_project)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots obj slot = Some cap \<Longrightarrow> (obj_id, slot) \<mapsto>s obj = (obj_id, slot) \<mapsto>c cap
theory Separation_SD

lemma sep_map_c_sep_map_s:
  "\<lbrakk>((obj_id,slot) \<mapsto>s obj) s; (object_slots obj) slot = Some cap\<rbrakk> \<Longrightarrow>
   ((obj_id,slot) \<mapsto>c cap) s" by (fastforce simp: sep_map_s_sep_map_c_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((obj_id, slot) \<mapsto>s obj) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> ((obj_id, slot) \<mapsto>c cap) s
theory Separation_SD

lemma sep_map_s_sep_map_c:
  "\<lbrakk>((obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow>
    ((obj_id, slot) \<mapsto>s obj) s" by (fastforce simp: sep_map_s_sep_map_c_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj) s
theory Separation_SD

lemma sep_map_s_object_slots_equal:
  "\<lbrakk>object_slots obj slot = object_slots obj' slot; object_type obj = object_type obj'\<rbrakk>
  \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj) = ((obj_id, slot) \<mapsto>s obj')" apply (clarsimp simp: sep_map_s_def sep_map_general_def split: sep_state.splits) apply (intro iffI ext conjI |
         clarsimp simp: object_to_sep_state_def object_project_def
                        object_slots_object_clean)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots obj slot = object_slots obj' slot; object_type obj = object_type obj'\<rbrakk> \<Longrightarrow> (obj_id, slot) \<mapsto>s obj = (obj_id, slot) \<mapsto>s obj' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots obj slot = object_slots obj' slot; object_type obj = object_type obj'\<rbrakk> \<Longrightarrow> (\<lambda>s. sep_heap s = object_to_sep_state obj_id obj {Slot slot} \<and> sep_irq_node s = (\<lambda>x. None)) = (\<lambda>s. sep_heap s = object_to_sep_state obj_id obj' {Slot slot} \<and> sep_irq_node s = (\<lambda>x. None)) proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_S_def2:
  "(obj_id \<mapsto>S obj) = ((obj_id,UNIV) \<mapsto>S' obj)" by (clarsimp simp: sep_map_S_def sep_map_S'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_id \<mapsto>S obj = (obj_id, UNIV) \<mapsto>S' obj
theory Separation_SD

lemma sep_map_S'_def_singleton:
  "(obj_id, {slot}) \<mapsto>S' obj = (obj_id, slot) \<mapsto>s obj" by (rule ext)(clarsimp simp: sep_map_S'_def sep_map_s_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (obj_id, {slot}) \<mapsto>S' obj = (obj_id, slot) \<mapsto>s obj
theory Separation_SD

lemma sep_map_S'_decomp':
  "\<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk>
  \<Longrightarrow> (obj_id, insert slot slots) \<mapsto>S' obj =
      ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, slot) \<mapsto>s obj)" apply (rule ext, rename_tac s) apply (clarsimp simp: sep_map_S'_def sep_map_s_def) apply (subgoal_tac "Slot ` slots \<inter> {Slot slot} = {}") apply (drule_tac p=obj_id and obj=obj and s=s in sep_map_decomp) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> (obj_id, insert slot slots) \<mapsto>S' obj = ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, slot) \<mapsto>s obj) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> ((obj_id, insert slot slots) \<mapsto>S' obj) s = ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, slot) \<mapsto>s obj) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (insert (Slot slot) (Slot ` slots)) s = (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj {Slot slot}) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}; Slot ` slots \<inter> {Slot slot} = {}\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (insert (Slot slot) (Slot ` slots)) s = (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj {Slot slot}) s
 2. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> {Slot slot} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}; (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj {Slot slot}) s = sep_map_general obj_id obj (Slot ` slots \<union> {Slot slot}) s\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (insert (Slot slot) (Slot ` slots)) s = (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj {Slot slot}) s
 2. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> {Slot slot} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot \<notin> slots; slots \<noteq> {}\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> {Slot slot} = {} proof (prove)
goal:
No subgoals!