theory Abstract_Separation_D

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> (None \<in> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))) \<and> (None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b; None \<in> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
 3. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<in> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; None \<in> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}; clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b = clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> \<Longrightarrow> None \<notin> cmps_b \<longrightarrow> (None \<in> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a))) \<and> (None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<in> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; None \<notin> cmps_b; None \<in> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}; clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b = clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_a cmps_a)
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b\<rbrakk> \<Longrightarrow> None \<notin> cmps_a \<longrightarrow> (cmps_a = {} \<longrightarrow> cmps_b = {} \<longrightarrow> object_clean obj_b {} = object_clean obj_a {}) \<and> (cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a = {}; cmps_b = {}\<rbrakk> \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}
 2. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a\<rbrakk> \<Longrightarrow> cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a\<rbrakk> \<Longrightarrow> cmps_a \<noteq> {} \<longrightarrow> cmps_b \<noteq> {} \<longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_a cmps_a) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}; None \<notin> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_type obj_a = object_type obj_b; None \<notin> cmps_b; None \<notin> cmps_a; cmps_a \<noteq> {}; cmps_b \<noteq> {}; clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b = clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a\<rbrakk> \<Longrightarrow> update_slots (clean_slots (object_slots obj_a) cmps_a ++ clean_slots (object_slots obj_b) cmps_b) (object_clean obj_b cmps_b) = update_slots (clean_slots (object_slots obj_b) cmps_b ++ clean_slots (object_slots obj_a) cmps_a) (object_clean obj_b cmps_b) proof (prove)
goal:
No subgoals!