kings-crown/FVELER_Isabelle huggingface dataset:
theory Abstract_Separation_D

lemma add_to_slots_object_slots:
  "object_type y = object_type z
 \<Longrightarrow> add_to_slots (object_slots (add_to_slots (x) y)) z =
     add_to_slots (x ++ object_slots y) z" apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def) apply (fastforce simp: object_type_def cdl_tcb.splits cdl_cnode.splits
                 split: cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type y = object_type z \<Longrightarrow> Abstract_Separation_D.add_to_slots (object_slots (Abstract_Separation_D.add_to_slots x y)) z = Abstract_Separation_D.add_to_slots (x ++ object_slots y) z proof (prove)
goal (1 subgoal):
 1. object_type y = object_type z \<Longrightarrow> (case z of Endpoint \<Rightarrow> z | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := (case case y of Endpoint \<Rightarrow> y | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ (case y of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode xa \<Rightarrow> CNode (xa\<lparr>cdl_cnode_caps := x ++ (case y of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode xa \<Rightarrow> CNode (xa\<lparr>cdl_cnode_caps := (case case y of Endpoint \<Rightarrow> y | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ (case y of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode xa \<Rightarrow> CNode (xa\<lparr>cdl_cnode_caps := x ++ (case y of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>)) = (case z of Endpoint \<Rightarrow> z | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ (case y of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode xa \<Rightarrow> CNode (xa\<lparr>cdl_cnode_caps := x ++ (case y of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma not_conflicting_objects_empty [simp]:
  "not_conflicting_objects s (SepState Map.empty (\<lambda>obj_id. {})) obj_id" by (clarsimp simp: not_conflicting_objects_def split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects s (SepState (\<lambda>x. None) (\<lambda>obj_id. {})) obj_id
theory Abstract_Separation_D

lemma not_conflicting_objects_empty_object [elim!]:
  "(sep_heap x) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id" by (clarsimp simp: not_conflicting_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_heap x obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id
theory Abstract_Separation_D

lemma empty_object_not_conflicting_objects [elim!]:
  "(sep_heap y) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id" apply (drule not_conflicting_objects_empty_object [where y=x]) apply (clarsimp simp: not_conflicting_objects_comm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_heap y obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects y x obj_id \<Longrightarrow> not_conflicting_objects x y obj_id proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma cdl_heap_add_empty [simp]:
 "cdl_heap_add (SepState h gs) (SepState Map.empty (\<lambda>obj_id. {})) = h" by (simp add: cdl_heap_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add (SepState h gs) (SepState (\<lambda>x. None) (\<lambda>obj_id. {})) = h
theory Abstract_Separation_D

lemma empty_cdl_heap_add [simp]:
  "cdl_heap_add (SepState Map.empty (\<lambda>obj_id. {})) (SepState h gs)= h" apply (simp add: cdl_heap_add_def) apply (rule ext) apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add (SepState (\<lambda>x. None) (\<lambda>obj_id. {})) (SepState h gs) = h proof (prove)
goal (1 subgoal):
 1. (\<lambda>obj_id. case h obj_id of None \<Rightarrow> None | Some obj_b \<Rightarrow> case None of None \<Rightarrow> h obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b {} (gs obj_id))) = h proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. (case h obj_id of None \<Rightarrow> None | Some obj_b \<Rightarrow> case None of None \<Rightarrow> h obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b {} (gs obj_id))) = h obj_id proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma map_add_result_empty1: "a ++ b = Map.empty \<Longrightarrow> a = Map.empty" apply (subgoal_tac "dom (a++b) = {}") apply (subgoal_tac "dom (a) = {}") apply clarsimp apply (unfold dom_map_add)[1] apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ++ b = (\<lambda>x. None) \<Longrightarrow> a = (\<lambda>x. None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> a = (\<lambda>x. None)
 2. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}; dom a = {}\<rbrakk> \<Longrightarrow> a = (\<lambda>x. None)
 2. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 3. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom b \<union> dom a = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (1 subgoal):
 1. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma map_add_result_empty2: "a ++ b = Map.empty \<Longrightarrow> b = Map.empty" apply (subgoal_tac "dom (a++b) = {}") apply (subgoal_tac "dom (a) = {}") apply clarsimp apply (unfold dom_map_add)[1] apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ++ b = (\<lambda>x. None) \<Longrightarrow> b = (\<lambda>x. None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> b = (\<lambda>x. None)
 2. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}; dom a = {}\<rbrakk> \<Longrightarrow> b = (\<lambda>x. None)
 2. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 3. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); dom b \<union> dom a = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal (1 subgoal):
 1. a ++ b = (\<lambda>x. None) \<Longrightarrow> dom (a ++ b) = {} proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma map_add_emptyE [elim!]: "\<lbrakk>a ++ b = Map.empty; \<lbrakk>a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" apply (frule map_add_result_empty1) apply (frule map_add_result_empty2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); \<lbrakk>a = (\<lambda>x. None); b = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); \<lbrakk>a = (\<lambda>x. None); b = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> R; a = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); \<lbrakk>a = (\<lambda>x. None); b = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> R; a = (\<lambda>x. None); b = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma clean_slots_empty [simp]:
  "clean_slots Map.empty cmp = Map.empty" by (clarsimp simp: clean_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clean_slots (\<lambda>x. None) cmp = (\<lambda>x. None)
theory Abstract_Separation_D

lemma object_type_update_slots [simp]:
  "object_type (update_slots slots x) = object_type x" by (clarsimp simp: object_type_def update_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (update_slots slots x) = object_type x
theory Abstract_Separation_D

lemma object_type_object_clean_slots [simp]:
  "object_type (object_clean_slots x cmp) = object_type x" by (clarsimp simp: object_clean_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean_slots x cmp) = object_type x
theory Abstract_Separation_D

lemma object_type_object_clean_fields [simp]:
  "object_type (object_clean_fields x cmp) = object_type x" by (clarsimp simp: object_clean_fields_def object_type_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean_fields x cmp) = object_type x
theory Abstract_Separation_D

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean x cmp) = object_type x
theory Abstract_Separation_D

lemma object_type_add_to_slots [simp]:
  "object_type (add_to_slots slots x) = object_type x" by (clarsimp simp: object_type_def add_to_slots_def update_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type (Abstract_Separation_D.add_to_slots slots x) = object_type x
theory Abstract_Separation_D

lemma object_slots_update_slots_empty [simp]:
  "\<not>has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = Map.empty" by (clarsimp simp: object_slots_def update_slots_def has_slots_def
                 split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = (\<lambda>x. None)
theory Abstract_Separation_D

lemma update_slots_no_slots [simp]:
  "\<not>has_slots obj \<Longrightarrow> update_slots slots obj = obj" by (clarsimp simp: update_slots_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> has_slots obj \<Longrightarrow> update_slots slots obj = obj
theory Abstract_Separation_D

lemma update_slots_update_slots [simp]:
  "update_slots slots (update_slots slots' obj) = update_slots slots obj" by (clarsimp simp: update_slots_def split: cdl_object.splits)

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

lemma update_slots_same_object:
  "a = b \<Longrightarrow> update_slots a obj = update_slots b obj" by (erule arg_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a = b \<Longrightarrow> update_slots a obj = update_slots b obj
theory Abstract_Separation_D

lemma object_type_has_slots:
  "\<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y" by (clarsimp simp: object_type_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y
theory Abstract_Separation_D

lemma object_slots_object_clean_fields [simp]:
  "object_slots (object_clean_fields obj cmp) = object_slots obj" by (clarsimp simp: object_slots_def object_clean_fields_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots (object_clean_fields obj cmp) = object_slots obj
theory Abstract_Separation_D

lemma object_slots_object_clean [simp]:
  "object_slots (object_clean obj cmp) = clean_slots (object_slots obj) cmp" by (clarsimp simp: object_clean_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots (object_clean obj cmp) = clean_slots (object_slots obj) cmp
theory Abstract_Separation_D

lemma object_slots_add_to_slots [simp]:
  "object_type y = object_type z \<Longrightarrow> object_slots (add_to_slots (object_slots y) z) = object_slots y ++ object_slots z" by (clarsimp simp: object_slots_def add_to_slots_def update_slots_def object_type_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type y = object_type z \<Longrightarrow> object_slots (Abstract_Separation_D.add_to_slots (object_slots y) z) = object_slots y ++ object_slots z
theory Abstract_Separation_D

lemma update_slots_object_clean_slots [simp]:
  "update_slots slots (object_clean_slots obj cmp) = update_slots slots obj" by (clarsimp simp: object_clean_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_slots slots (object_clean_slots obj cmp) = update_slots slots obj
theory Abstract_Separation_D

lemma object_clean_fields_idem [simp]:
  "object_clean_fields (object_clean_fields obj cmp) cmp = object_clean_fields obj cmp" by (clarsimp simp: object_clean_fields_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (object_clean_fields obj cmp) cmp = object_clean_fields obj cmp
theory Abstract_Separation_D

lemma object_clean_slots_idem [simp]:
  "object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp" apply (case_tac  "has_slots obj") apply (clarsimp simp: object_clean_slots_def clean_slots_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp proof (prove)
goal (2 subgoals):
 1. has_slots obj \<Longrightarrow> object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp
 2. \<not> has_slots obj \<Longrightarrow> object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma object_clean_fields_object_clean_slots [simp]:
  "object_clean_fields (object_clean_slots obj gs) gs = object_clean_slots (object_clean_fields obj gs) gs" by (clarsimp simp: object_clean_fields_def object_clean_slots_def
                     clean_slots_def object_slots_def update_slots_def
              split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (object_clean_slots obj gs) gs = object_clean_slots (object_clean_fields obj gs) gs
theory Abstract_Separation_D

lemma object_clean_idem [simp]:
  "object_clean (object_clean obj cmp) cmp = object_clean obj cmp" by (clarsimp simp: object_clean_def)

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

lemma has_slots_object_clean_slots:
 "has_slots (object_clean_slots obj cmp) = has_slots obj" by (clarsimp simp: has_slots_def object_clean_slots_def update_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. has_slots (object_clean_slots obj cmp) = has_slots obj
theory Abstract_Separation_D

lemma has_slots_object_clean_fields:
 "has_slots (object_clean_fields obj cmp) = has_slots obj" by (clarsimp simp: has_slots_def object_clean_fields_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. has_slots (object_clean_fields obj cmp) = has_slots obj
theory Abstract_Separation_D

lemma has_slots_object_clean:
 "has_slots (object_clean obj cmp) = has_slots obj" by (clarsimp simp: object_clean_def has_slots_object_clean_slots has_slots_object_clean_fields)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. has_slots (object_clean obj cmp) = has_slots obj
theory Abstract_Separation_D

lemma object_slots_update_slots_object_clean_fields [simp]:
  "object_slots (update_slots slots (object_clean_fields obj cmp)) = object_slots (update_slots slots obj)" apply (case_tac "has_slots obj") apply (clarsimp simp: has_slots_object_clean_fields)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots (update_slots slots (object_clean_fields obj cmp)) = object_slots (update_slots slots obj) proof (prove)
goal (2 subgoals):
 1. has_slots obj \<Longrightarrow> object_slots (update_slots slots (object_clean_fields obj cmp)) = object_slots (update_slots slots obj)
 2. \<not> has_slots obj \<Longrightarrow> object_slots (update_slots slots (object_clean_fields obj cmp)) = object_slots (update_slots slots obj) proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma object_clean_fields_update_slots [simp]:
 "object_clean_fields (update_slots slots obj) cmp = update_slots slots (object_clean_fields obj cmp)" by (clarsimp simp: object_clean_fields_def update_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (update_slots slots obj) cmp = update_slots slots (object_clean_fields obj cmp)
theory Abstract_Separation_D

lemma object_clean_fields_twice [simp]:
  "(object_clean_fields (object_clean_fields obj cmp') cmp) = object_clean_fields obj (cmp \<inter> cmp')" by (clarsimp simp: object_clean_fields_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (object_clean_fields obj cmp') cmp = object_clean_fields obj (cmp \<inter> cmp')
theory Abstract_Separation_D

lemma update_slots_object_clean_fields:
  "\<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk>
    \<Longrightarrow> update_slots slots (object_clean_fields obj cmps) =
        update_slots slots (object_clean_fields obj' cmps')" by (fastforce simp: update_slots_def object_clean_fields_def object_type_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk> \<Longrightarrow> update_slots slots (object_clean_fields obj cmps) = update_slots slots (object_clean_fields obj' cmps')
theory Abstract_Separation_D

lemma object_clean_fields_no_slots:
  "\<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'; \<not> has_slots obj; \<not> has_slots obj'\<rbrakk>
    \<Longrightarrow> object_clean_fields obj cmps = object_clean_fields obj' cmps'" by (fastforce simp: object_clean_fields_def object_type_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'; \<not> has_slots obj; \<not> has_slots obj'\<rbrakk> \<Longrightarrow> object_clean_fields obj cmps = object_clean_fields obj' cmps'
theory Abstract_Separation_D

lemma update_slots_object_clean:
  "\<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk>
   \<Longrightarrow> update_slots slots (object_clean obj cmps) = update_slots slots (object_clean obj' cmps')" apply (clarsimp simp: object_clean_def object_clean_slots_def) apply (erule (2) update_slots_object_clean_fields) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk> \<Longrightarrow> update_slots slots (object_clean obj cmps) = update_slots slots (object_clean obj' cmps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk> \<Longrightarrow> update_slots slots (object_clean_fields obj cmps) = update_slots slots (object_clean_fields obj' cmps') proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma cdl_heap_add_assoc:
  "\<lbrakk>sep_state_disj x y; sep_state_disj y z; sep_state_disj x z\<rbrakk>
  \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z =
      cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))" apply (clarsimp simp: sep_state_disj_def) apply (cut_tac cdl_heap_add_assoc') apply fast apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_state_disj x y; sep_state_disj y z; sep_state_disj x z\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z); cdl_heap_add (SepState (cdl_heap_add ?x1 ?y1) (cdl_ghost_state_add ?x1 ?y1)) ?z1 = cdl_heap_add ?x1 (SepState (cdl_heap_add ?y1 ?z1) (cdl_ghost_state_add ?y1 ?z1))\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))
 2. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> \<forall>obj_id. not_conflicting_objects ?x1 ?z1 obj_id \<and> not_conflicting_objects ?y1 ?z1 obj_id \<and> not_conflicting_objects ?x1 ?z1 obj_id proof (prove)
goal (1 subgoal):
 1. \<lbrakk>All (not_conflicting_objects x y); All (not_conflicting_objects y z); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> \<forall>obj_id. not_conflicting_objects x z obj_id \<and> not_conflicting_objects y z obj_id \<and> not_conflicting_objects x z obj_id proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma cdl_ghost_state_add_assoc:
  "cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z =
   cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))" apply (rule ext) apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def Let_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) proof (prove)
goal (1 subgoal):
 1. \<And>xa. cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z xa = cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) xa proof (prove)
goal:
No subgoals!