theory Abstract_Separation_D

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x proof (prove)
goal (1 subgoal):
 1. All (not_conflicting_objects x y) \<Longrightarrow> cdl_heap_add x y = cdl_heap_add y x \<and> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. All (not_conflicting_objects x y) \<Longrightarrow> cdl_heap_add x y = cdl_heap_add y x
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>All (not_conflicting_objects (SepState x1 x2) (SepState x1a x2a)); x = SepState x1 x2; y = SepState x1a x2a\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState x1 x2) (SepState x1a x2a) = cdl_heap_add (SepState x1a x2a) (SepState x1 x2)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b\<rbrakk> \<Longrightarrow> cdl_heap_add (SepState heap_a gs_a) (SepState heap_b gs_b) = cdl_heap_add (SepState heap_b gs_b) (SepState heap_a gs_a)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b\<rbrakk> \<Longrightarrow> (\<lambda>obj_id. 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))) = (\<lambda>obj_id. case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b\<rbrakk> \<Longrightarrow> (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))) = (case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (3 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = None\<rbrakk> \<Longrightarrow> (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))) = (case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 2. \<And>heap_a gs_a heap_b gs_b obj_id a. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some a\<rbrakk> \<Longrightarrow> (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))) = (case heap_a obj_id of None \<Rightarrow> heap_b obj_id | Some obj_b \<Rightarrow> case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_b obj_id) (gs_a obj_id)))
 3. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id a. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some a\<rbrakk> \<Longrightarrow> (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))) = (case heap_b obj_id of None \<Rightarrow> heap_a obj_id | Some obj_a \<Rightarrow> Some (object_add obj_a a (gs_b obj_id) (gs_a obj_id)))
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id a aa. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some a; heap_b obj_id = Some aa\<rbrakk> \<Longrightarrow> object_add a aa (gs_a obj_id) (gs_b obj_id) = object_add aa a (gs_b obj_id) (gs_a obj_id)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>All (not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b)); x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b\<rbrakk> \<Longrightarrow> object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id) = object_add obj_b obj_a (gs_b obj_id) (gs_a obj_id)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id) = object_add obj_b obj_a (gs_b obj_id) (gs_a obj_id)
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (3 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> object_type obj_a = object_type obj_b
 2. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> gs_a obj_id \<inter> gs_b obj_id = {}
 3. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (2 subgoals):
 1. \<And>heap_a gs_a heap_b gs_b obj_id obj_a obj_b. \<lbrakk>x = SepState heap_a gs_a; y = SepState heap_b gs_b; heap_a obj_id = Some obj_a; heap_b obj_id = Some obj_b; not_conflicting_objects (SepState heap_a gs_a) (SepState heap_b gs_b) obj_id\<rbrakk> \<Longrightarrow> gs_a obj_id \<inter> gs_b obj_id = {}
 2. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal (1 subgoal):
 1. All (not_conflicting_objects x y) \<Longrightarrow> cdl_ghost_state_add x y = cdl_ghost_state_add y x proof (prove)
goal:
No subgoals!