kings-crown/FVELER_Isabelle huggingface dataset:
theory Sep_Eq

lemma sep_disj_addD1':
  "disjoint x (sep_add' y z) \<Longrightarrow> disjoint y z \<Longrightarrow> disjoint x y" proof (clarsimp simp: disjoint_def sep_add'_def) fix a assume a: "y \<oplus> z = Some a" fix b assume b: "x \<oplus> a = Some b" with a have "Some x ++ (Some y ++ Some z) = Some b" by (simp add: lift2_def) hence "(Some x ++ Some y) ++ Some z = Some b" by (simp add: add_assoc) thus "\<exists>b. x \<oplus> y = Some b" by (simp add: lift2_def split: option.splits) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x ## sep_add' y z; y ## z\<rbrakk> \<Longrightarrow> x ## y proof (state)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (state)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (state)
this:
y \<oplus> z = Some a

goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (state)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (state)
this:
x \<oplus> a = Some b

goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (chain)
picking this:
y \<oplus> z = Some a
x \<oplus> a = Some b proof (prove)
using this:
y \<oplus> z = Some a
x \<oplus> a = Some b

goal (1 subgoal):
 1. Some x ++ Some y ++ Some z = Some b proof (state)
this:
Some x ++ Some y ++ Some z = Some b

goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (prove)
using this:
Some x ++ Some y ++ Some z = Some b

goal (1 subgoal):
 1. (Some x ++ Some y) ++ Some z = Some b proof (state)
this:
(Some x ++ Some y) ++ Some z = Some b

goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>x \<oplus> yaa = Some ya; y \<oplus> z = Some yaa\<rbrakk> \<Longrightarrow> \<exists>ya. x \<oplus> y = Some ya proof (prove)
using this:
(Some x ++ Some y) ++ Some z = Some b

goal (1 subgoal):
 1. \<exists>b. x \<oplus> y = Some b proof (state)
this:
\<exists>b. x \<oplus> y = Some b

goal:
No subgoals!
theory Sep_Heap_Instance

lemma domain_conv: "domain = dom" by (rule ext) (simp add: domain_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domain = dom
theory Sep_Heap_Instance

lemma plus_fun_conv: "a + b = a ++ b" by (auto simp: plus_fun_def map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + b = a ++ b
theory Sep_Heap_Instance

lemma unit_disj_sep_unit [simp]: "(a :: unit) ## b" by (clarsimp simp: sep_disj_unit_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ## b
theory Sep_Heap_Instance

lemma disj_sep_None [simp]:
  "a ## None"
  "None ## a" by (auto simp: sep_disj_option_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ## None &&& None ## a
theory Sep_Heap_Instance

lemma disj_sep_Some_Some [simp]:
  "\<not> (Some a ## Some b)" by (auto simp: sep_disj_option_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> Some a ## Some b
theory Sep_Heap_Instance

lemma None_plus [simp]:
  "a + None = a"
  "None + a = a" by (auto simp: plus_option_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + None = a &&& None + a = a
theory Sep_Heap_Instance

lemma None_plus_distrib:
  "(a :: 'a option) + (b + c) = (a + b) + c" by (clarsimp simp: plus_option_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + (b + c) = a + b + c
theory Sep_MP_Example

lemma "((P \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* P \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s" 
  (* sep_mp attempts to solve goals that could be solved by careful use of the sep_mp theorem *)
   apply (sep_mp) apply (clarsimp simp: sep_conj_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* P \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. ((P \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* P \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. (B \<and>* A) s \<Longrightarrow> (A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Sep_MP_Example

lemma "((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s" apply (sep_mp) apply (clarsimp simp: sep_conj_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. (B \<and>* A) s \<Longrightarrow> (A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Sep_Provers_Example

lemma "(A \<and>* B \<and>* C \<and>* Bar) s" apply (sep_rule Moo_Bar) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* Bar) s proof (prove)
goal (1 subgoal):
 1. (Moo \<and>* A \<and>* B \<and>* C) s
theory Sep_Provers_Example

lemma "(A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> R" apply (sep_drule Moo_Bar) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. (Bar \<and>* A \<and>* B \<and>* C) s \<Longrightarrow> R
theory Sep_Provers_Example

lemma "(A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* Bar) s" 
   (* In this case we need to rotate both, so we use sep_erule_full *)
   apply (sep_erule_full Moo_Bar) apply (assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* Bar) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* Bar) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (A \<and>* B \<and>* C) s \<Longrightarrow> (A \<and>* B \<and>* C) s proof (prove)
goal:
No subgoals!
theory Sep_Select_Example

lemma sep_select: "(A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* D) s" apply (sep_select 2)        (* moves the 2nd conjunct in the conclusions to the front *)
   apply (sep_select 2 3 4 1)  (* we can reorder multiple conjuncts at once *)
   apply (sep_select 2 3 4)    (* the list can be partial *)
   apply (sep_select_asm 3 4)  (* sep_select_asm works for the assumptions *)
   oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* D) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (B \<and>* A \<and>* C \<and>* D) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (B \<and>* A \<and>* C \<and>* D) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (A \<and>* C \<and>* D \<and>* B) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (A \<and>* C \<and>* D \<and>* B) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (C \<and>* D \<and>* B \<and>* A) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (C \<and>* D \<and>* B \<and>* A) s proof (prove)
goal (1 subgoal):
 1. (C \<and>* D \<and>* A \<and>* B) s \<Longrightarrow> (C \<and>* D \<and>* B \<and>* A) s proof (prove)
goal (1 subgoal):
 1. (C \<and>* D \<and>* A \<and>* B) s \<Longrightarrow> (C \<and>* D \<and>* B \<and>* A) s
theory Sep_Solve_Example

lemma "((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s" apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Sep_Tactics_Test

lemma "(A ** B ** Q ** P) s" apply (sep_select 1) apply (sep_select 3) apply (sep_select 4) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* Q \<and>* P) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* Q \<and>* P) s proof (prove)
goal (1 subgoal):
 1. (Q \<and>* A \<and>* B \<and>* P) s proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q \<and>* A \<and>* B) s
theory Sep_Tactics_Test

lemma "\<lbrakk> also unrelated; (A ** B ** Q ** P) s \<rbrakk> \<Longrightarrow> unrelated" apply (sep_select_asm 2) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>also unrelated; (A \<and>* B \<and>* Q \<and>* P) s\<rbrakk> \<Longrightarrow> unrelated proof (prove)
goal (1 subgoal):
 1. \<lbrakk>also unrelated; (B \<and>* A \<and>* Q \<and>* P) s\<rbrakk> \<Longrightarrow> unrelated
theory Sep_Tactics_Test

lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (A ** X) s" apply (sep_cancel) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(A \<and>* B) sa; (A \<and>* Y) s\<rbrakk> \<Longrightarrow> (A \<and>* X) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(A \<and>* B) sa; Y s\<rbrakk> \<Longrightarrow> X s
theory Sep_Tactics_Test

lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** X) s) s" apply (sep_cancel) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(A \<and>* B) sa; (A \<and>* Y) s\<rbrakk> \<Longrightarrow> (A \<and>* X) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(A \<and>* B) sa; Y s\<rbrakk> \<Longrightarrow> X s
theory Sep_Tactics_Test

lemma boxo: "P s \<Longrightarrow> (P \<and>* \<box>) s" by (erule sep_conj_sep_emptyI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> (P \<and>* \<box>) s
theory Sep_Tactics_Test

lemma f2:
  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
  assumes forward2: "\<And>s. instance s \<Longrightarrow> instance2 s"
  shows "generic s \<Longrightarrow> (instance2 ** \<box>) s" apply (drule forward forward2)+ apply (sep_erule_concl (direct) boxo) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. generic s \<Longrightarrow> (instance2 \<and>* \<box>) s proof (prove)
goal (1 subgoal):
 1. instance2 s \<Longrightarrow> (instance2 \<and>* \<box>) s proof (prove)
goal:
No subgoals!
theory Simple_Separation_Example

lemma maps_to_write:
  "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))" apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits) apply (rule_tac x=y in exI) apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<mapsto> - \<and>* P) H \<Longrightarrow> (p \<mapsto> v \<and>* P) (H(p \<mapsto> v)) proof (prove)
goal (1 subgoal):
 1. \<And>y xa. \<lbrakk>[p \<mapsto> xa] ## y; H = [p \<mapsto> xa] + y; P y\<rbrakk> \<Longrightarrow> \<exists>ya. [p \<mapsto> v] ## ya \<and> ([p \<mapsto> xa] + y)(p \<mapsto> v) = [p \<mapsto> v] + ya \<and> P ya proof (prove)
goal (1 subgoal):
 1. \<And>y xa. \<lbrakk>[p \<mapsto> xa] ## y; H = [p \<mapsto> xa] + y; P y\<rbrakk> \<Longrightarrow> [p \<mapsto> v] ## y \<and> ([p \<mapsto> xa] + y)(p \<mapsto> v) = [p \<mapsto> v] + y \<and> P y proof (prove)
goal:
No subgoals!
theory Simple_Separation_Example

lemma points_to:
  "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v" by (auto elim!: sep_conjE
           simp: sep_disj_fun_def maps_to_def map_convs map_add_def
           split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<mapsto> v \<and>* P) H \<Longrightarrow> the (H p) = v
theory Simple_Separation_Example

lemma list_empty [simp]:
  shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)" by (cases xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)
theory Simple_Separation_Example

lemma "VARS x y z w h
 {(x \<mapsto> y ** z \<mapsto> w) h}
 SKIP
 {x \<noteq> z}" apply vcg apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {(x \<mapsto> y \<and>* z \<mapsto> w) h}
SKIP
{x \<noteq> z} proof (prove)
goal (1 subgoal):
 1. \<And>x y z w h. (x \<mapsto> y \<and>* z \<mapsto> w) h \<Longrightarrow> x \<noteq> z proof (prove)
goal:
No subgoals!
theory Simple_Separation_Example

lemma "VARS H x y z w
 {(P ** Q) H}
 SKIP
 {(Q ** P) H}" apply vcg apply(simp add: sep_conj_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {(P \<and>* Q) H}
SKIP
{(Q \<and>* P) H} proof (prove)
goal (1 subgoal):
 1. \<And>H x y z w. (P \<and>* Q) H \<Longrightarrow> (Q \<and>* P) H proof (prove)
goal:
No subgoals!
theory Simple_Separation_Example

lemma "VARS H
 {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H}
 H := H(p \<mapsto> q)
 {list p (p#qs) H}" apply vcg apply (auto intro: maps_to_write) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {p \<noteq> 0 \<and> (p \<mapsto> - \<and>* list q qs) H}
H := H(p \<mapsto> q)
{list p (p # qs) H} proof (prove)
goal (1 subgoal):
 1. \<And>H. p \<noteq> 0 \<and> (p \<mapsto> - \<and>* list q qs) H \<Longrightarrow> list p (p # qs) (H(p \<mapsto> q)) proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma inter_empty_not_both:
"\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B
theory Abstract_Separation_D

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+

(* Proof state trace *)
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
theory Abstract_Separation_D

lemma union_intersection1: "A \<inter> (A \<union> B) = A" by (rule inf_sup_absorb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<inter> (A \<union> B) = A
theory Abstract_Separation_D

lemma union_intersection2: "B \<inter> (A \<union> B) = B" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. B \<inter> (A \<union> B) = B
theory Abstract_Separation_D

lemma restrict_map_disj':
  "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T" by (auto simp: map_disj_def restrict_map_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T
theory Abstract_Separation_D

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S proof (prove)
goal (1 subgoal):
 1. ?h |` S \<bottom> ?h' |` T \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S proof (prove)
goal:
No subgoals!
theory Abstract_Separation_D

lemma the_set_union [simp]:
  "the_set (A \<union> B) = the_set A \<union> the_set B" by (fastforce simp: the_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_set (A \<union> B) = the_set A \<union> the_set B
theory Abstract_Separation_D

lemma the_set_inter [simp]:
  "the_set (A \<inter> B) = the_set A \<inter> the_set B" by (fastforce simp: the_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_set (A \<inter> B) = the_set A \<inter> the_set B
theory Abstract_Separation_D

lemma the_set_inter_empty:
  "A \<inter> B = {} \<Longrightarrow> the_set A \<inter> the_set B = {}" by (fastforce simp: the_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<inter> B = {} \<Longrightarrow> the_set A \<inter> the_set B = {}
theory Abstract_Separation_D

lemma slots_of_heap_empty [simp]: "slots_of_heap Map.empty object_id = Map.empty" by (simp add: slots_of_heap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_of_heap (\<lambda>x. None) object_id = (\<lambda>x. None)
theory Abstract_Separation_D

lemma slots_of_heap_empty2 [simp]:
  "h obj_id = None \<Longrightarrow> slots_of_heap h obj_id = Map.empty" by (simp add: slots_of_heap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h obj_id = None \<Longrightarrow> slots_of_heap h obj_id = (\<lambda>x. None)
theory Abstract_Separation_D

lemma update_slots_add_to_slots_empty [simp]:
  "update_slots Map.empty (add_to_slots new obj) = update_slots Map.empty obj" by (clarsimp simp: update_slots_def add_to_slots_def split:cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_slots (\<lambda>x. None) (Abstract_Separation_D.add_to_slots new obj) = update_slots (\<lambda>x. None) obj
theory Abstract_Separation_D

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_slots (object_slots a) a = a
theory Abstract_Separation_D

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h obj_id = Some obj \<Longrightarrow> update_slots (slots_of_heap h obj_id) obj = obj
theory Abstract_Separation_D

lemma add_to_slots_empty [simp]: "add_to_slots Map.empty h = h" by (simp add: add_to_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Abstract_Separation_D.add_to_slots (\<lambda>x. None) h = h
theory Abstract_Separation_D

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_slots a o1 = update_slots a o2 \<Longrightarrow> update_slots b o1 = update_slots b o2
theory Abstract_Separation_D

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_conflicting_objects h1 h2 obj = not_conflicting_objects h2 h1 obj 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 (prove)
goal:
No subgoals!
theory Abstract_Separation_D

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

(* Proof state trace *)
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 (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 (prove)
goal:
No subgoals!