theory Abstract_Separation_D

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x y); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) xa proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>All (not_conflicting_objects y z); All (not_conflicting_objects x y); All (not_conflicting_objects x z)\<rbrakk> \<Longrightarrow> not_conflicting_objects x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z)) obj_id proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>\<forall>obj_id. case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {}; \<forall>obj_id. case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {} proof (prove)
goal (1 subgoal):
 1. \<And>obj_id. \<lbrakk>case sep_heap y obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state y obj_id \<inter> sep_ghost_state z obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap y obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state y obj_id = {}; case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case sep_heap z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> sep_ghost_state z obj_id = {}\<rbrakk> \<Longrightarrow> case sep_heap x obj_id of None \<Rightarrow> True | Some o1 \<Rightarrow> case cdl_heap_add y z obj_id of None \<Rightarrow> True | Some o2 \<Rightarrow> object_type o1 = object_type o2 \<and> sep_ghost_state x obj_id \<inter> cdl_ghost_state_add y z obj_id = {} proof (prove)
goal:
No subgoals!