[STATEMENT]
lemma exec_execl [dest!]:
 "P \<turnstile> cf \<rightarrow>* cf' \<Longrightarrow> \<exists>cfs. P \<Turnstile> cfs \<and> cfs \<noteq> [] \<and> hd cfs = cf \<and> last cfs = cf'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> cf \<rightarrow>* cf' \<Longrightarrow> \<exists>cfs. P \<Turnstile> cfs \<and> cfs \<noteq> [] \<and> hd cfs = cf \<and> last cfs = cf'
[PROOF STEP]
by (erule star.induct, force, erule exE, rule list.exhaust, blast,
 simp del: last.simps, rule exI, subst execl.simps(1), simp)


[STATEMENT]
theorem ccomp_exec:
 "ccomp c \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c), s', stk') \<Longrightarrow> (c, s) \<Rightarrow> s' \<and> stk' = stk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp c \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c), s', stk') \<Longrightarrow> (c, s) \<Rightarrow> s' \<and> stk' = stk
[PROOF STEP]
by (insert ccomp_correct, force simp: hd_conv_nth last_conv_nth execl_all_def cpred_def)


[STATEMENT]
lemma inter_empty_not_both:
"\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B
[PROOF STEP]
by fastforce


[STATEMENT]
lemma union_intersection:
  "A \<inter> (A \<union> B) = A"
  "B \<inter> (A \<union> B) = B"
  "(A \<union> B) \<inter> A = A"
  "(A \<union> B) \<inter> B = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<inter> (A \<union> B) = A &&& B \<inter> (A \<union> B) = B) &&& (A \<union> B) \<inter> A = A &&& (A \<union> B) \<inter> B = B
[PROOF STEP]
by fastforce+


[STATEMENT]
lemma union_intersection1: "A \<inter> (A \<union> B) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> (A \<union> B) = A
[PROOF STEP]
by (rule inf_sup_absorb)


[STATEMENT]
lemma union_intersection2: "B \<inter> (A \<union> B) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<inter> (A \<union> B) = B
[PROOF STEP]
by fastforce


[STATEMENT]
lemma restrict_map_disj':
  "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T
[PROOF STEP]
by (auto simp: map_disj_def restrict_map_def dom_def)


[STATEMENT]
lemma map_add_restrict_comm:
  "S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S
[PROOF STEP]
apply (drule restrict_map_disj')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?h |` S \<bottom> ?h' |` T \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S
[PROOF STEP]
apply (erule map_add_com)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma the_set_union [simp]:
  "the_set (A \<union> B) = the_set A \<union> the_set B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_set (A \<union> B) = the_set A \<union> the_set B
[PROOF STEP]
by (fastforce simp: the_set_def)


[STATEMENT]
lemma the_set_inter [simp]:
  "the_set (A \<inter> B) = the_set A \<inter> the_set B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_set (A \<inter> B) = the_set A \<inter> the_set B
[PROOF STEP]
by (fastforce simp: the_set_def)


[STATEMENT]
lemma the_set_inter_empty:
  "A \<inter> B = {} \<Longrightarrow> the_set A \<inter> the_set B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B = {} \<Longrightarrow> the_set A \<inter> the_set B = {}
[PROOF STEP]
by (fastforce simp: the_set_def)


[STATEMENT]
lemma add_to_slots_assoc:
  "add_to_slots x (add_to_slots (y ++ z) obj) =
   add_to_slots (x ++ y) (add_to_slots z obj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abstract_Separation_D.add_to_slots x (Abstract_Separation_D.add_to_slots (y ++ z) obj) = Abstract_Separation_D.add_to_slots (x ++ y) (Abstract_Separation_D.add_to_slots z obj)
[PROOF STEP]
apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> Map.empty | 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 case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>)) = (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ y ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> Map.empty | 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 ++ y ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>))
[PROOF STEP]
apply (fastforce simp: cdl_tcb.splits cdl_cnode.splits
                 split: cdl_object.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_to_slots_twice [simp]:
  "add_to_slots x (add_to_slots y a) = add_to_slots (x ++ y) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abstract_Separation_D.add_to_slots x (Abstract_Separation_D.add_to_slots y a) = Abstract_Separation_D.add_to_slots (x ++ y) a
[PROOF STEP]
by (fastforce simp: add_to_slots_def update_slots_def object_slots_def
              split: cdl_object.splits)


[STATEMENT]
lemma slots_of_heap_empty [simp]: "slots_of_heap Map.empty object_id = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slots_of_heap Map.empty object_id = Map.empty
[PROOF STEP]
by (simp add: slots_of_heap_def)


[STATEMENT]
lemma slots_of_heap_empty2 [simp]:
  "h obj_id = None \<Longrightarrow> slots_of_heap h obj_id = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h obj_id = None \<Longrightarrow> slots_of_heap h obj_id = Map.empty
[PROOF STEP]
by (simp add: slots_of_heap_def)


[STATEMENT]
lemma update_slots_add_to_slots_empty [simp]:
  "update_slots Map.empty (add_to_slots new obj) = update_slots Map.empty obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_slots Map.empty (Abstract_Separation_D.add_to_slots new obj) = update_slots Map.empty obj
[PROOF STEP]
by (clarsimp simp: update_slots_def add_to_slots_def split:cdl_object.splits)


[STATEMENT]
lemma update_object_slots_id [simp]: "update_slots (object_slots a) a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_slots (object_slots a) a = a
[PROOF STEP]
by (clarsimp simp: update_slots_def object_slots_def
              split: cdl_object.splits)


[STATEMENT]
lemma update_slots_of_heap_id [simp]:
  "h obj_id = Some obj \<Longrightarrow> update_slots (slots_of_heap h obj_id) obj = obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h obj_id = Some obj \<Longrightarrow> update_slots (slots_of_heap h obj_id) obj = obj
[PROOF STEP]
by (clarsimp simp: update_slots_def slots_of_heap_def object_slots_def
              split: cdl_object.splits)


[STATEMENT]
lemma add_to_slots_empty [simp]: "add_to_slots Map.empty h = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abstract_Separation_D.add_to_slots Map.empty h = h
[PROOF STEP]
by (simp add: add_to_slots_def)


[STATEMENT]
lemma update_slots_eq:
  "update_slots a o1 = update_slots a o2 \<Longrightarrow> update_slots b o1 = update_slots b o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_slots a o1 = update_slots a o2 \<Longrightarrow> update_slots b o1 = update_slots b o2
[PROOF STEP]
by (fastforce simp: update_slots_def cdl_tcb.splits cdl_cnode.splits
              split: cdl_object.splits)


[STATEMENT]
lemma not_conflicting_objects_comm:
  "not_conflicting_objects h1 h2 obj = not_conflicting_objects h2 h1 obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects h1 h2 obj = not_conflicting_objects h2 h1 obj
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_def split:option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>sep_heap h1 obj = Some x2; sep_heap h2 obj = Some x2a\<rbrakk> \<Longrightarrow> (object_type x2 = object_type x2a \<and> sep_ghost_state h1 obj \<inter> sep_ghost_state h2 obj = {}) = (object_type x2a = object_type x2 \<and> sep_ghost_state h2 obj \<inter> sep_ghost_state h1 obj = {})
[PROOF STEP]
apply (fastforce simp: update_slots_def cdl_tcb.splits cdl_cnode.splits
              split: cdl_object.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma object_clean_comm:
  "\<lbrakk>object_type obj_a = object_type obj_b;
    object_slots obj_a ++ object_slots obj_b = object_slots obj_b ++ object_slots obj_a; None \<notin> cmp\<rbrakk>
  \<Longrightarrow> object_clean (add_to_slots (object_slots obj_a) obj_b) cmp =
      object_clean (add_to_slots (object_slots obj_b) obj_a) cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; object_slots obj_a ++ object_slots obj_b = object_slots obj_b ++ object_slots obj_a; None \<notin> cmp\<rbrakk> \<Longrightarrow> object_clean (Abstract_Separation_D.add_to_slots (object_slots obj_a) obj_b) cmp = object_clean (Abstract_Separation_D.add_to_slots (object_slots obj_b) obj_a) cmp
[PROOF STEP]
apply (clarsimp simp: object_type_def split: cdl_object.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x2 x2a. \<lbrakk>object_slots (Tcb x2a) ++ object_slots (Tcb x2) = object_slots (Tcb x2) ++ object_slots (Tcb x2a); None \<notin> cmp; obj_b = Tcb x2; obj_a = Tcb x2a\<rbrakk> \<Longrightarrow> object_clean (Abstract_Separation_D.add_to_slots (object_slots (Tcb x2a)) (Tcb x2)) cmp = object_clean (Abstract_Separation_D.add_to_slots (object_slots (Tcb x2)) (Tcb x2a)) cmp
 2. \<And>x3 x3a. \<lbrakk>object_slots (CNode x3a) ++ object_slots (CNode x3) = object_slots (CNode x3) ++ object_slots (CNode x3a); None \<notin> cmp; obj_b = CNode x3; obj_a = CNode x3a\<rbrakk> \<Longrightarrow> object_clean (Abstract_Separation_D.add_to_slots (object_slots (CNode x3a)) (CNode x3)) cmp = object_clean (Abstract_Separation_D.add_to_slots (object_slots (CNode x3)) (CNode x3a)) cmp
[PROOF STEP]
apply (clarsimp simp: object_clean_def object_clean_slots_def object_clean_fields_def
                        add_to_slots_def object_slots_def update_slots_def
                        cdl_tcb.splits cdl_cnode.splits
                 split: cdl_object.splits)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
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"
[PROOF STATE]
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 STEP]
apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def)
[PROOF STATE]
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> Map.empty | 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> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> Map.empty | 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> Map.empty | 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> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> Map.empty | 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> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> Map.empty | 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> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x) ++ (case z of Endpoint \<Rightarrow> Map.empty | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>))
[PROOF STEP]
apply (fastforce simp: object_type_def cdl_tcb.splits cdl_cnode.splits
                 split: cdl_object.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_conflicting_objects_empty [simp]:
  "not_conflicting_objects s (SepState Map.empty (\<lambda>obj_id. {})) obj_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects s (SepState Map.empty (\<lambda>obj_id. {})) obj_id
[PROOF STEP]
by (clarsimp simp: not_conflicting_objects_def split:option.splits)


[STATEMENT]
lemma empty_not_conflicting_objects [simp]:
  "not_conflicting_objects (SepState Map.empty (\<lambda>obj_id. {})) s obj_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects (SepState Map.empty (\<lambda>obj_id. {})) s obj_id
[PROOF STEP]
by (clarsimp simp: not_conflicting_objects_def split:option.splits)


[STATEMENT]
lemma empty_object_not_conflicting_objects [elim!]:
  "(sep_heap y) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sep_heap y obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id
[PROOF STEP]
apply (drule not_conflicting_objects_empty_object [where y=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects y x obj_id \<Longrightarrow> not_conflicting_objects x y obj_id
[PROOF STEP]
apply (clarsimp simp: not_conflicting_objects_comm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cdl_heap_add_empty [simp]:
 "cdl_heap_add (SepState h gs) (SepState Map.empty (\<lambda>obj_id. {})) = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add (SepState h gs) (SepState Map.empty (\<lambda>obj_id. {})) = h
[PROOF STEP]
by (simp add: cdl_heap_add_def)


[STATEMENT]
lemma empty_cdl_heap_add [simp]:
  "cdl_heap_add (SepState Map.empty (\<lambda>obj_id. {})) (SepState h gs)= h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdl_heap_add (SepState Map.empty (\<lambda>obj_id. {})) (SepState h gs) = h
[PROOF STEP]
apply (simp add: cdl_heap_add_def)
[PROOF STATE]
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 STEP]
apply (rule ext)
[PROOF STATE]
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 STEP]
apply (clarsimp split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_add_result_empty1: "a ++ b = Map.empty \<Longrightarrow> a = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ++ b = Map.empty \<Longrightarrow> a = Map.empty
[PROOF STEP]
apply (subgoal_tac "dom (a++b) = {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> a = Map.empty
 2. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply (subgoal_tac "dom (a) = {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}; dom a = {}\<rbrakk> \<Longrightarrow> a = Map.empty
 2. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 3. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply (unfold dom_map_add)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom b \<union> dom a = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_add_result_empty2: "a ++ b = Map.empty \<Longrightarrow> b = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ++ b = Map.empty \<Longrightarrow> b = Map.empty
[PROOF STEP]
apply (subgoal_tac "dom (a++b) = {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> b = Map.empty
 2. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply (subgoal_tac "dom (a) = {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}; dom a = {}\<rbrakk> \<Longrightarrow> b = Map.empty
 2. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 3. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom (a ++ b) = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply (unfold dom_map_add)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a ++ b = Map.empty; dom b \<union> dom a = {}\<rbrakk> \<Longrightarrow> dom a = {}
 2. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ++ b = Map.empty \<Longrightarrow> dom (a ++ b) = {}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_add_emptyE [elim!]: "\<lbrakk>a ++ b = Map.empty; \<lbrakk>a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = Map.empty; \<lbrakk>a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
apply (frule map_add_result_empty1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = Map.empty; \<lbrakk>a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R; a = Map.empty\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
apply (frule map_add_result_empty2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = Map.empty; \<lbrakk>a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R; a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clean_slots_empty [simp]:
  "clean_slots Map.empty cmp = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clean_slots Map.empty cmp = Map.empty
[PROOF STEP]
by (clarsimp simp: clean_slots_def)


[STATEMENT]
lemma object_type_update_slots [simp]:
  "object_type (update_slots slots x) = object_type x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type (update_slots slots x) = object_type x
[PROOF STEP]
by (clarsimp simp: object_type_def update_slots_def split: cdl_object.splits)


[STATEMENT]
lemma object_type_object_clean_slots [simp]:
  "object_type (object_clean_slots x cmp) = object_type x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean_slots x cmp) = object_type x
[PROOF STEP]
by (clarsimp simp: object_clean_slots_def)


[STATEMENT]
lemma object_type_object_clean_fields [simp]:
  "object_type (object_clean_fields x cmp) = object_type x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean_fields x cmp) = object_type x
[PROOF STEP]
by (clarsimp simp: object_clean_fields_def object_type_def split: cdl_object.splits)


[STATEMENT]
lemma object_type_object_clean [simp]:
  "object_type (object_clean x cmp) = object_type x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type (object_clean x cmp) = object_type x
[PROOF STEP]
by (clarsimp simp: object_clean_def)


[STATEMENT]
lemma object_type_add_to_slots [simp]:
  "object_type (add_to_slots slots x) = object_type x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_type (Abstract_Separation_D.add_to_slots slots x) = object_type x
[PROOF STEP]
by (clarsimp simp: object_type_def add_to_slots_def update_slots_def split: cdl_object.splits)


[STATEMENT]
lemma object_slots_update_slots [simp]:
  "has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = slots"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = slots
[PROOF STEP]
by (clarsimp simp: object_slots_def update_slots_def has_slots_def
              split: cdl_object.splits)


[STATEMENT]
lemma object_slots_update_slots_empty [simp]:
  "\<not>has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = Map.empty
[PROOF STEP]
by (clarsimp simp: object_slots_def update_slots_def has_slots_def
                 split: cdl_object.splits)


[STATEMENT]
lemma update_slots_no_slots [simp]:
  "\<not>has_slots obj \<Longrightarrow> update_slots slots obj = obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_slots obj \<Longrightarrow> update_slots slots obj = obj
[PROOF STEP]
by (clarsimp simp: update_slots_def has_slots_def split: cdl_object.splits)


[STATEMENT]
lemma update_slots_update_slots [simp]:
  "update_slots slots (update_slots slots' obj) = update_slots slots obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_slots slots (update_slots slots' obj) = update_slots slots obj
[PROOF STEP]
by (clarsimp simp: update_slots_def split: cdl_object.splits)


[STATEMENT]
lemma update_slots_same_object:
  "a = b \<Longrightarrow> update_slots a obj = update_slots b obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b \<Longrightarrow> update_slots a obj = update_slots b obj
[PROOF STEP]
by (erule arg_cong)


[STATEMENT]
lemma object_type_has_slots:
  "\<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y
[PROOF STEP]
by (clarsimp simp: object_type_def has_slots_def split: cdl_object.splits)


[STATEMENT]
lemma object_slots_object_clean_fields [simp]:
  "object_slots (object_clean_fields obj cmp) = object_slots obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_slots (object_clean_fields obj cmp) = object_slots obj
[PROOF STEP]
by (clarsimp simp: object_slots_def object_clean_fields_def split: cdl_object.splits)


[STATEMENT]
lemma object_slots_object_clean_slots [simp]:
  "object_slots (object_clean_slots obj cmp) = clean_slots (object_slots obj) cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_slots (object_clean_slots obj cmp) = clean_slots (object_slots obj) cmp
[PROOF STEP]
by (clarsimp simp: object_clean_slots_def object_slots_def update_slots_def split: cdl_object.splits)


[STATEMENT]
lemma object_slots_object_clean [simp]:
  "object_slots (object_clean obj cmp) = clean_slots (object_slots obj) cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_slots (object_clean obj cmp) = clean_slots (object_slots obj) cmp
[PROOF STEP]
by (clarsimp simp: object_clean_def)


[STATEMENT]
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"
[PROOF STATE]
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
[PROOF STEP]
by (clarsimp simp: object_slots_def add_to_slots_def update_slots_def object_type_def split: cdl_object.splits)


[STATEMENT]
lemma update_slots_object_clean_slots [simp]:
  "update_slots slots (object_clean_slots obj cmp) = update_slots slots obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_slots slots (object_clean_slots obj cmp) = update_slots slots obj
[PROOF STEP]
by (clarsimp simp: object_clean_slots_def)


[STATEMENT]
lemma object_clean_fields_idem [simp]:
  "object_clean_fields (object_clean_fields obj cmp) cmp = object_clean_fields obj cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (object_clean_fields obj cmp) cmp = object_clean_fields obj cmp
[PROOF STEP]
by (clarsimp simp: object_clean_fields_def split: cdl_object.splits)


[STATEMENT]
lemma object_clean_slots_idem [simp]:
  "object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp
[PROOF STEP]
apply (case_tac  "has_slots obj")
[PROOF STATE]
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 STEP]
apply (clarsimp simp: object_clean_slots_def clean_slots_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (object_clean_slots obj gs) gs = object_clean_slots (object_clean_fields obj gs) gs
[PROOF STEP]
by (clarsimp simp: object_clean_fields_def object_clean_slots_def
                     clean_slots_def object_slots_def update_slots_def
              split: cdl_object.splits)


[STATEMENT]
lemma object_clean_idem [simp]:
  "object_clean (object_clean obj cmp) cmp = object_clean obj cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_clean (object_clean obj cmp) cmp = object_clean obj cmp
[PROOF STEP]
by (clarsimp simp: object_clean_def)


[STATEMENT]
lemma has_slots_object_clean_slots:
 "has_slots (object_clean_slots obj cmp) = has_slots obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_slots (object_clean_slots obj cmp) = has_slots obj
[PROOF STEP]
by (clarsimp simp: has_slots_def object_clean_slots_def update_slots_def split: cdl_object.splits)


[STATEMENT]
lemma has_slots_object_clean_fields:
 "has_slots (object_clean_fields obj cmp) = has_slots obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_slots (object_clean_fields obj cmp) = has_slots obj
[PROOF STEP]
by (clarsimp simp: has_slots_def object_clean_fields_def split: cdl_object.splits)


[STATEMENT]
lemma has_slots_object_clean:
 "has_slots (object_clean obj cmp) = has_slots obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_slots (object_clean obj cmp) = has_slots obj
[PROOF STEP]
by (clarsimp simp: object_clean_def has_slots_object_clean_slots has_slots_object_clean_fields)


[STATEMENT]
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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_slots (update_slots slots (object_clean_fields obj cmp)) = object_slots (update_slots slots obj)
[PROOF STEP]
apply (case_tac "has_slots obj")
[PROOF STATE]
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 STEP]
apply (clarsimp simp: has_slots_object_clean_fields)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma object_clean_fields_update_slots [simp]:
 "object_clean_fields (update_slots slots obj) cmp = update_slots slots (object_clean_fields obj cmp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (update_slots slots obj) cmp = update_slots slots (object_clean_fields obj cmp)
[PROOF STEP]
by (clarsimp simp: object_clean_fields_def update_slots_def split: cdl_object.splits)


[STATEMENT]
lemma object_clean_fields_twice [simp]:
  "(object_clean_fields (object_clean_fields obj cmp') cmp) = object_clean_fields obj (cmp \<inter> cmp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_clean_fields (object_clean_fields obj cmp') cmp = object_clean_fields obj (cmp \<inter> cmp')
[PROOF STEP]
by (clarsimp simp: object_clean_fields_def split: cdl_object.splits)


[STATEMENT]
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')"
[PROOF STATE]
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 STEP]
by (fastforce simp: update_slots_def object_clean_fields_def object_type_def split: cdl_object.splits)


[STATEMENT]
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'"
[PROOF STATE]
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'
[PROOF STEP]
by (fastforce simp: object_clean_fields_def object_type_def has_slots_def split: cdl_object.splits)


[STATEMENT]
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')"
[PROOF STATE]
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 STEP]
apply (clarsimp simp: object_clean_def object_clean_slots_def)
[PROOF STATE]
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 STEP]
apply (erule (2) update_slots_object_clean_fields)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done