--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/ex/capDL/Abstract_Separation_D.thy Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,714 @@
+(* Author: Andrew Boyton, 2012
+ Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+ Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Instantiating capDL as a separation algebra."
+
+theory Abstract_Separation_D
+imports "../../Sep_Tactics" Types_D "../../Map_Extra"
+begin
+
+(**************************************
+ * Start of lemmas to move elsewhere. *
+ **************************************)
+
+lemma inter_empty_not_both:
+"\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B"
+ by fastforce
+
+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"
+ by fastforce+
+
+lemma union_intersection1: "A \<inter> (A \<union> B) = A"
+ by (rule inf_sup_absorb)
+lemma union_intersection2: "B \<inter> (A \<union> B) = B"
+ by fastforce
+
+(* This lemma is strictly weaker than restrict_map_disj. *)
+lemma restrict_map_disj':
+ "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T"
+ by (auto simp: map_disj_def restrict_map_def dom_def)
+
+lemma map_add_restrict_comm:
+ "S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S"
+ apply (drule restrict_map_disj')
+ apply (erule map_add_com)
+ done
+
+(************************************
+ * End of lemmas to move elsewhere. *
+ ************************************)
+
+
+
+(* The state for separation logic has:
+ * The memory heap.
+ * A function for which objects own which fields.
+ In capDL, we say that an object either owns all of its fields, or none of them.
+ These are both taken from the cdl_state.
+ *)
+
+datatype sep_state = SepState cdl_heap cdl_ghost_state
+
+(* Functions to get the heap and the ghost_state from the sep_state. *)
+primrec sep_heap :: "sep_state \<Rightarrow> cdl_heap"
+where "sep_heap (SepState h gs) = h"
+
+primrec sep_ghost_state :: "sep_state \<Rightarrow> cdl_ghost_state"
+where "sep_ghost_state (SepState h gs) = gs"
+
+definition
+ the_set :: "'a option set \<Rightarrow> 'a set"
+where
+ "the_set xs = {x. Some x \<in> xs}"
+
+lemma the_set_union [simp]:
+ "the_set (A \<union> B) = the_set A \<union> the_set B"
+ by (fastforce simp: the_set_def)
+
+lemma the_set_inter [simp]:
+ "the_set (A \<inter> B) = the_set A \<inter> the_set B"
+ by (fastforce simp: the_set_def)
+
+lemma the_set_inter_empty:
+ "A \<inter> B = {} \<Longrightarrow> the_set A \<inter> the_set B = {}"
+ by (fastforce simp: the_set_def)
+
+
+(* As the capDL operations mostly take the state (rather than the heap)
+ * we need to redefine some of them again to take just the heap.
+ *)
+definition
+ slots_of_heap :: "cdl_heap \<Rightarrow> cdl_object_id \<Rightarrow> cdl_cap_map"
+where
+ "slots_of_heap h \<equiv> \<lambda>obj_id.
+ case h obj_id of
+ None \<Rightarrow> empty
+ | Some obj \<Rightarrow> object_slots obj"
+
+(* Adds new caps to an object. It won't overwrite on a collision. *)
+definition
+ add_to_slots :: "cdl_cap_map \<Rightarrow> cdl_object \<Rightarrow> cdl_object"
+where
+ "add_to_slots new_val obj \<equiv> update_slots (new_val ++ (object_slots obj)) obj"
+
+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)"
+ apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def)
+ apply (fastforce simp: cdl_tcb.splits cdl_cnode.splits
+ split: cdl_object.splits)
+ done
+
+(* Lemmas about add_to_slots, update_slots and object_slots. *)
+lemma add_to_slots_twice [simp]:
+ "add_to_slots x (add_to_slots y a) = add_to_slots (x ++ y) a"
+ by (fastforce simp: add_to_slots_def update_slots_def object_slots_def
+ split: cdl_object.splits)
+
+lemma slots_of_heap_empty [simp]: "slots_of_heap empty object_id = empty"
+ by (simp add: slots_of_heap_def)
+
+lemma slots_of_heap_empty2 [simp]:
+ "h obj_id = None \<Longrightarrow> slots_of_heap h obj_id = empty"
+ by (simp add: slots_of_heap_def)
+
+lemma update_slots_add_to_slots_empty [simp]:
+ "update_slots empty (add_to_slots new obj) = update_slots empty obj"
+ by (clarsimp simp: update_slots_def add_to_slots_def split:cdl_object.splits)
+
+lemma update_object_slots_id [simp]: "update_slots (object_slots a) a = a"
+ by (clarsimp simp: update_slots_def object_slots_def
+ split: cdl_object.splits)
+
+lemma update_slots_of_heap_id [simp]:
+ "h obj_id = Some obj \<Longrightarrow> update_slots (slots_of_heap h obj_id) obj = obj"
+ by (clarsimp simp: update_slots_def slots_of_heap_def object_slots_def
+ split: cdl_object.splits)
+
+lemma add_to_slots_empty [simp]: "add_to_slots empty h = h"
+ by (simp add: add_to_slots_def)
+
+lemma update_slots_eq:
+ "update_slots a o1 = update_slots a o2 \<Longrightarrow> update_slots b o1 = update_slots b o2"
+ by (fastforce simp: update_slots_def cdl_tcb.splits cdl_cnode.splits
+ split: cdl_object.splits)
+
+
+
+(* If there are not two conflicting objects at a position in two states.
+ * Objects conflict if their types are different or their ghost_states collide.
+ *)
+definition
+ not_conflicting_objects :: "sep_state \<Rightarrow> sep_state \<Rightarrow> cdl_object_id \<Rightarrow> bool"
+where
+ "not_conflicting_objects state_a state_b = (\<lambda>obj_id.
+ let heap_a = sep_heap state_a;
+ heap_b = sep_heap state_b;
+ gs_a = sep_ghost_state state_a;
+ gs_b = sep_ghost_state state_b
+ in case (heap_a obj_id, heap_b obj_id) of
+ (Some o1, Some o2) \<Rightarrow> object_type o1 = object_type o2 \<and> gs_a obj_id \<inter> gs_b obj_id = {}
+ | _ \<Rightarrow> True)"
+
+
+(* "Cleans" slots to conform with the compontents. *)
+definition
+ clean_slots :: "cdl_cap_map \<Rightarrow> cdl_components \<Rightarrow> cdl_cap_map"
+where
+ "clean_slots slots cmp \<equiv> slots |` the_set cmp"
+
+(* Sets the fields of an object to a "clean" state.
+ Because a frame's size is part of it's type, we don't reset it. *)
+definition
+ object_clean_fields :: "cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_object"
+where
+ "object_clean_fields obj cmp \<equiv> if None \<in> cmp then obj else case obj of
+ Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_fault_endpoint := undefined\<rparr>)
+ | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_size_bits := undefined \<rparr>)
+ | _ \<Rightarrow> obj"
+
+(* Sets the slots of an object to a "clean" state. *)
+definition
+ object_clean_slots :: "cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_object"
+where
+ "object_clean_slots obj cmp \<equiv> update_slots (clean_slots (object_slots obj) cmp) obj"
+
+(* Sets an object to a "clean" state. *)
+definition
+ object_clean :: "cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_object"
+where
+ "object_clean obj gs \<equiv> object_clean_slots (object_clean_fields obj gs) gs"
+
+(* Overrides the left object with the attributes of the right, as specified by the ghost state.
+ If the components for an object are empty, then this object is treated as empty, and thus ignored.
+ *)
+definition
+ object_add :: "cdl_object \<Rightarrow> cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_components \<Rightarrow> cdl_object"
+where
+ "object_add obj_a obj_b cmps_a cmps_b \<equiv>
+ let clean_obj_a = object_clean obj_a cmps_a;
+ clean_obj_b = object_clean obj_b cmps_b
+ in if (cmps_a = {})
+ then clean_obj_b
+ else if (cmps_b = {})
+ then clean_obj_a
+ else if (None \<in> cmps_b)
+ then (update_slots (object_slots clean_obj_a ++ object_slots clean_obj_b) clean_obj_b)
+ else (update_slots (object_slots clean_obj_a ++ object_slots clean_obj_b) clean_obj_a)"
+
+(* Heaps are added by adding their repsective objects.
+ * The ghost state tells us which object's fields should be taken.
+ * Adding objects of the same type adds their caps
+ * (overwrites the left with the right).
+ *)
+definition
+ cdl_heap_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> cdl_heap"
+where
+ "cdl_heap_add state_a state_b \<equiv> \<lambda>obj_id.
+ let heap_a = sep_heap state_a;
+ heap_b = sep_heap state_b;
+ gs_a = sep_ghost_state state_a;
+ gs_b = sep_ghost_state state_b
+ in case heap_b obj_id of
+ None \<Rightarrow> heap_a obj_id
+ | Some obj_b \<Rightarrow> case heap_a obj_id of
+ None \<Rightarrow> heap_b obj_id
+ | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))"
+
+(* Heaps are added by adding their repsective objects.
+ * The ghost state tells us which object's fields should be taken.
+ * Adding objects of the same type adds their caps
+ * (overwrites the left with the right).
+ *)
+definition
+ cdl_ghost_state_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> cdl_ghost_state"
+where
+ "cdl_ghost_state_add state_a state_b \<equiv> \<lambda>obj_id.
+ let heap_a = sep_heap state_a;
+ heap_b = sep_heap state_b;
+ gs_a = sep_ghost_state state_a;
+ gs_b = sep_ghost_state state_b
+ in if heap_a obj_id = None \<and> heap_b obj_id \<noteq> None then gs_b obj_id
+ else if heap_b obj_id = None \<and> heap_a obj_id \<noteq> None then gs_a obj_id
+ else gs_a obj_id \<union> gs_b obj_id"
+
+
+(* Adding states adds their heaps,
+ * and each objects owns whichever fields it owned in either heap.
+ *)
+definition
+ sep_state_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> sep_state"
+where
+ "sep_state_add state_a state_b \<equiv>
+ let
+ heap_a = sep_heap state_a;
+ heap_b = sep_heap state_b;
+ gs_a = sep_ghost_state state_a;
+ gs_b = sep_ghost_state state_b
+ in
+ SepState (cdl_heap_add state_a state_b) (cdl_ghost_state_add state_a state_b)"
+
+
+(* Heaps are disjoint if for all of their objects:
+ * the caps of their respective objects are disjoint,
+ * their respective objects don't conflict,
+ * they don't both own any of the same fields.
+*)
+definition
+ sep_state_disj :: "sep_state \<Rightarrow> sep_state \<Rightarrow> bool"
+where
+ "sep_state_disj state_a state_b \<equiv>
+ let
+ heap_a = sep_heap state_a;
+ heap_b = sep_heap state_b;
+ gs_a = sep_ghost_state state_a;
+ gs_b = sep_ghost_state state_b
+ in
+ \<forall>obj_id. not_conflicting_objects state_a state_b obj_id"
+
+lemma not_conflicting_objects_comm:
+ "not_conflicting_objects h1 h2 obj = not_conflicting_objects h2 h1 obj"
+ apply (clarsimp simp: not_conflicting_objects_def split:option.splits)
+ apply (fastforce simp: update_slots_def cdl_tcb.splits cdl_cnode.splits
+ split: cdl_object.splits)
+ done
+
+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"
+ apply (clarsimp simp: object_type_def split: cdl_object.splits)
+ 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)+
+ done
+
+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
+
+lemma not_conflicting_objects_empty [simp]:
+ "not_conflicting_objects s (SepState empty (\<lambda>obj_id. {})) obj_id"
+ by (clarsimp simp: not_conflicting_objects_def split:option.splits)
+
+lemma empty_not_conflicting_objects [simp]:
+ "not_conflicting_objects (SepState empty (\<lambda>obj_id. {})) s obj_id"
+ by (clarsimp simp: not_conflicting_objects_def split:option.splits)
+
+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)
+
+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
+
+lemma cdl_heap_add_empty [simp]:
+ "cdl_heap_add (SepState h gs) (SepState empty (\<lambda>obj_id. {})) = h"
+ by (simp add: cdl_heap_add_def)
+
+lemma empty_cdl_heap_add [simp]:
+ "cdl_heap_add (SepState empty (\<lambda>obj_id. {})) (SepState h gs)= h"
+ apply (simp add: cdl_heap_add_def)
+ apply (rule ext)
+ apply (clarsimp split: option.splits)
+ done
+
+lemma map_add_result_empty1: "a ++ b = empty \<Longrightarrow> a = 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
+
+lemma map_add_result_empty2: "a ++ b = empty \<Longrightarrow> b = 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
+
+lemma map_add_emptyE [elim!]: "\<lbrakk>a ++ b = empty; \<lbrakk>a = empty; b = empty\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ apply (frule map_add_result_empty1)
+ apply (frule map_add_result_empty2)
+ apply clarsimp
+ done
+
+lemma clean_slots_empty [simp]:
+ "clean_slots empty cmp = empty"
+ by (clarsimp simp: clean_slots_def)
+
+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)
+
+lemma object_type_object_clean_slots [simp]:
+ "object_type (object_clean_slots x cmp) = object_type x"
+ by (clarsimp simp: object_clean_slots_def)
+
+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)
+
+lemma object_type_object_clean [simp]:
+ "object_type (object_clean x cmp) = object_type x"
+ by (clarsimp simp: object_clean_def)
+
+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)
+
+lemma object_slots_update_slots [simp]:
+ "has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = slots"
+ by (clarsimp simp: object_slots_def update_slots_def has_slots_def
+ split: cdl_object.splits)
+
+lemma object_slots_update_slots_empty [simp]:
+ "\<not>has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = empty"
+ by (clarsimp simp: object_slots_def update_slots_def has_slots_def
+ split: cdl_object.splits)
+
+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)
+
+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)
+
+lemma update_slots_same_object:
+ "a = b \<Longrightarrow> update_slots a obj = update_slots b obj"
+ by (erule arg_cong)
+
+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)
+
+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)
+
+lemma object_slots_object_clean_slots [simp]:
+ "object_slots (object_clean_slots obj cmp) = clean_slots (object_slots obj) cmp"
+ by (clarsimp simp: object_clean_slots_def object_slots_def update_slots_def split: cdl_object.splits)
+
+lemma object_slots_object_clean [simp]:
+ "object_slots (object_clean obj cmp) = clean_slots (object_slots obj) cmp"
+ by (clarsimp simp: object_clean_def)
+
+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)
+
+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)
+
+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)
+
+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
+
+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)
+
+lemma object_clean_idem [simp]:
+ "object_clean (object_clean obj cmp) cmp = object_clean obj cmp"
+ by (clarsimp simp: object_clean_def)
+
+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)
+
+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)
+
+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)
+
+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
+
+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)
+
+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)
+
+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)
+
+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)
+
+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
+
+lemma cdl_heap_add_assoc':
+ "\<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 \<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 (rule ext)
+ apply (rename_tac obj_id)
+ apply (erule_tac x=obj_id in allE)
+ apply (clarsimp simp: cdl_heap_add_def cdl_ghost_state_add_def not_conflicting_objects_def)
+ apply (simp add: Let_unfold split: option.splits)
+ apply (rename_tac obj_y obj_x obj_z)
+ apply (clarsimp simp: object_add_def clean_slots_def object_clean_def object_clean_slots_def Let_unfold)
+ apply (case_tac "has_slots obj_z")
+ apply (subgoal_tac "has_slots obj_y")
+ apply (subgoal_tac "has_slots obj_x")
+ apply ((clarsimp simp: has_slots_object_clean_fields has_slots_object_clean_slots has_slots_object_clean
+ map_add_restrict union_intersection |
+ drule inter_empty_not_both |
+ erule update_slots_object_clean_fields |
+ erule object_type_has_slots, simp |
+ simp | safe)+)[3]
+ apply (subgoal_tac "\<not> has_slots obj_y")
+ apply (subgoal_tac "\<not> has_slots obj_x")
+ apply ((clarsimp simp: has_slots_object_clean_fields has_slots_object_clean_slots has_slots_object_clean
+ map_add_restrict union_intersection |
+ drule inter_empty_not_both |
+ erule object_clean_fields_no_slots |
+ erule object_type_has_slots, simp |
+ simp | safe)+)
+ apply (fastforce simp: object_type_has_slots)+
+ done
+
+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
+
+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
+
+lemma clean_slots_map_add_comm:
+ "cmps_a \<inter> cmps_b = {}
+ \<Longrightarrow> clean_slots slots_a cmps_a ++ clean_slots slots_b cmps_b =
+ clean_slots slots_b cmps_b ++ clean_slots slots_a cmps_a"
+ apply (clarsimp simp: clean_slots_def)
+ apply (drule the_set_inter_empty)
+ apply (erule map_add_restrict_comm)
+ done
+
+lemma object_clean_all:
+ "object_type obj_a = object_type obj_b \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}"
+ apply (clarsimp simp: object_clean_def object_clean_slots_def clean_slots_def the_set_def)
+ apply (rule_tac cmps'1="{}" and obj'1="obj_a" in trans [OF update_slots_object_clean_fields], fastforce+)
+ done
+
+lemma object_add_comm:
+ "\<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk>
+ \<Longrightarrow> object_add obj_a obj_b cmps_a cmps_b = object_add obj_b obj_a cmps_b cmps_a"
+ apply (clarsimp simp: object_add_def Let_unfold)
+ apply (rule conjI | clarsimp)+
+ apply fastforce
+ apply (rule conjI | clarsimp)+
+ apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm)
+ apply fastforce
+ apply (rule conjI | clarsimp)+
+ apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm)
+ apply fastforce
+ apply (rule conjI | clarsimp)+
+ apply (erule object_clean_all)
+ apply (clarsimp)
+ apply (rule_tac cmps'1=cmps_b and obj'1=obj_b in trans [OF update_slots_object_clean], assumption+)
+ apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm)
+ apply fastforce
+ done
+
+lemma sep_state_add_comm:
+ "sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x"
+ apply (clarsimp simp: sep_state_add_def sep_state_disj_def)
+ apply (rule conjI)
+ apply (case_tac x, case_tac y, clarsimp)
+ apply (rename_tac heap_a gs_a heap_b gs_b)
+ apply (clarsimp simp: cdl_heap_add_def Let_unfold)
+ apply (rule ext)
+ apply (case_tac "heap_a obj_id")
+ apply (case_tac "heap_b obj_id", simp_all add: slots_of_heap_def)
+ apply (case_tac "heap_b obj_id", simp_all add: slots_of_heap_def)
+ apply (rename_tac obj_a obj_b)
+ apply (erule_tac x=obj_id in allE)
+ apply (rule object_add_comm)
+ apply (clarsimp simp: not_conflicting_objects_def)
+ apply (clarsimp simp: not_conflicting_objects_def)
+ apply (rule ext, fastforce simp: cdl_ghost_state_add_def Let_unfold Un_commute)
+ done
+
+lemma add_to_slots_comm:
+ "\<lbrakk>object_slots y_obj \<bottom> object_slots z_obj; update_slots empty y_obj = update_slots empty z_obj \<rbrakk>
+ \<Longrightarrow> add_to_slots (object_slots z_obj) y_obj = add_to_slots (object_slots y_obj) z_obj"
+ by (fastforce simp: add_to_slots_def update_slots_def object_slots_def
+ cdl_tcb.splits cdl_cnode.splits
+ dest!: map_add_com
+ split: cdl_object.splits)
+
+lemma cdl_heap_add_none1:
+ "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap x) obj_id = None"
+ by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits split_if_asm)
+
+lemma cdl_heap_add_none2:
+ "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap y) obj_id = None"
+ by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits split_if_asm)
+
+lemma object_type_object_addL:
+ "object_type obj = object_type obj'
+ \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj"
+ by (clarsimp simp: object_add_def Let_unfold)
+
+lemma object_type_object_addR:
+ "object_type obj = object_type obj'
+ \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj'"
+ by (clarsimp simp: object_add_def Let_unfold)
+
+lemma sep_state_add_disjL:
+ "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x y"
+ apply (clarsimp simp: sep_state_disj_def sep_state_add_def)
+ apply (rename_tac obj_id)
+ apply (clarsimp simp: not_conflicting_objects_def)
+ apply (erule_tac x=obj_id in allE)+
+ apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
+ split: option.splits)
+ done
+
+lemma sep_state_add_disjR:
+ "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x z"
+ apply (clarsimp simp: sep_state_disj_def sep_state_add_def)
+ apply (rename_tac obj_id)
+ apply (clarsimp simp: not_conflicting_objects_def)
+ apply (erule_tac x=obj_id in allE)+
+ apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
+ split: option.splits)
+ done
+
+lemma sep_state_add_disj:
+ "\<lbrakk>sep_state_disj y z; sep_state_disj x y; sep_state_disj x z\<rbrakk> \<Longrightarrow> sep_state_disj x (sep_state_add y z)"
+ apply (clarsimp simp: sep_state_disj_def sep_state_add_def)
+ apply (rename_tac obj_id)
+ apply (clarsimp simp: not_conflicting_objects_def)
+ apply (erule_tac x=obj_id in allE)+
+ apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR
+ split: option.splits)
+ done
+
+
+
+
+(*********************************************)
+(* Definition of separation logic for capDL. *)
+(*********************************************)
+
+instantiation "sep_state" :: zero
+begin
+ definition "0 \<equiv> SepState empty (\<lambda>obj_id. {})"
+ instance ..
+end
+
+instantiation "sep_state" :: stronger_sep_algebra
+begin
+
+definition "(op ##) \<equiv> sep_state_disj"
+definition "(op +) \<equiv> sep_state_add"
+
+
+
+(**********************************************
+ * The proof that this is a separation logic. *
+ **********************************************)
+
+instance
+ apply default
+(* x ## 0 *)
+ apply (simp add: sep_disj_sep_state_def sep_state_disj_def zero_sep_state_def)
+(* x ## y \<Longrightarrow> y ## x *)
+ apply (clarsimp simp: not_conflicting_objects_comm sep_disj_sep_state_def sep_state_disj_def Let_unfold
+ map_disj_com not_conflicting_objects_comm Int_commute)
+(* x + 0 = x *)
+ apply (simp add: plus_sep_state_def sep_state_add_def zero_sep_state_def)
+ apply (case_tac x)
+ apply (clarsimp simp: cdl_heap_add_def)
+ apply (rule ext)
+ apply (clarsimp simp: cdl_ghost_state_add_def split:split_if_asm)
+(* x ## y \<Longrightarrow> x + y = y + x *)
+ apply (clarsimp simp: plus_sep_state_def sep_disj_sep_state_def)
+ apply (erule sep_state_add_comm)
+(* (x + y) + z = x + (y + z) *)
+ apply (simp add: plus_sep_state_def sep_state_add_def)
+ apply (rule conjI)
+ apply (clarsimp simp: sep_disj_sep_state_def)
+ apply (erule (2) cdl_heap_add_assoc)
+ apply (rule cdl_ghost_state_add_assoc)
+(* x ## y + z = (x ## y \<and> x ## z) *)
+ apply (clarsimp simp: plus_sep_state_def sep_disj_sep_state_def)
+ apply (rule iffI)
+ (* x ## y + z \<Longrightarrow> (x ## y \<and> x ## z) *)
+ apply (rule conjI)
+ (* x ## y + z \<Longrightarrow> (x ## y) *)
+ apply (erule (1) sep_state_add_disjL)
+ (* x ## y + z \<Longrightarrow> (x ## z) *)
+ apply (erule (1) sep_state_add_disjR)
+ (* x ## y + z \<Longleftarrow> (x ## y \<and> x ## z) *)
+ apply clarsimp
+ apply (erule (2) sep_state_add_disj)
+ done
+
+end
+
+
+end