[STATEMENT]
lemma (in mut_m) reachable_snapshot_inv_sweep_loop_free:
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes nmr: "white r s"
  assumes ngs: "no_grey_refs s"
  assumes rsi: "reachable_snapshot_inv s"
  shows "reachable_snapshot_inv (s(sys := (s sys)\<lparr>heap := (heap (s sys))(r := None)\<rparr>))" (is "reachable_snapshot_inv ?s'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_snapshot_inv (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> in_snapshot y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
fix y :: "'ref"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> in_snapshot y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
assume rx: "reachable y ?s'"
[PROOF STATE]
proof (state)
this:
reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. \<And>y. reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> in_snapshot y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
have "black y s \<and> y \<noteq> r"
[PROOF STATE]
proof (prove)
using this:
reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. black y s \<and> y \<noteq> r
[PROOF STEP]
proof(induct rule: reachable_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. x \<in> mut_roots (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x. x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 3. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 4. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
case (root x)
[PROOF STATE]
proof (state)
this:
x \<in> mut_roots (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (4 subgoals):
 1. \<And>x. x \<in> mut_roots (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x. x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 3. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 4. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
with ngs nmr rsi
[PROOF STATE]
proof (chain)
picking this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> mut_roots (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> mut_roots (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. black x s \<and> x \<noteq> r
[PROOF STEP]
by (auto simp: fun_upd_apply dest: reachable_blackD)
[PROOF STATE]
proof (state)
this:
black x s \<and> x \<noteq> r

goal (3 subgoals):
 1. \<And>x. x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 3. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 3. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
case (ghost_honorary_root x)
[PROOF STATE]
proof (state)
this:
x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (3 subgoals):
 1. \<And>x. x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 3. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
with ngs nmr rsi
[PROOF STATE]
proof (chain)
picking this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. black x s \<and> x \<noteq> r
[PROOF STEP]
unfolding reachable_def reaches_def
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. black x s \<and> x \<noteq> r
[PROOF STEP]
by (auto simp: fun_upd_apply dest: reachable_blackD)
[PROOF STATE]
proof (state)
this:
black x s \<and> x \<noteq> r

goal (2 subgoals):
 1. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
case (tso_root x)
[PROOF STATE]
proof (state)
this:
x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (2 subgoals):
 1. \<And>x. x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> black x s \<and> x \<noteq> r
 2. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
with ngs nmr rsi
[PROOF STATE]
proof (chain)
picking this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. black x s \<and> x \<noteq> r
[PROOF STEP]
unfolding reachable_def reaches_def
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
x \<in> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal (1 subgoal):
 1. black x s \<and> x \<noteq> r
[PROOF STEP]
by (auto simp: fun_upd_apply dest: reachable_blackD)
[PROOF STATE]
proof (state)
this:
black x s \<and> x \<noteq> r

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
case (reaches x y)
[PROOF STATE]
proof (state)
this:
reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
(x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
black x s \<and> x \<noteq> r

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)); black x s \<and> x \<noteq> r\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
with ngs nmr rsi
[PROOF STATE]
proof (chain)
picking this:
no_grey_refs s
white r s
reachable_snapshot_inv s
reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
(x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
black x s \<and> x \<noteq> r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
reachable x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
(x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
black x s \<and> x \<noteq> r

goal (1 subgoal):
 1. black y s \<and> y \<noteq> r
[PROOF STEP]
unfolding reachable_def reaches_def
[PROOF STATE]
proof (prove)
using this:
no_grey_refs s
white r s
reachable_snapshot_inv s
\<exists>xa. xa \<in> mut_roots (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<union> mut_ghost_honorary_root (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<union> tso_store_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<and> (\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)))\<^sup>*\<^sup>* xa x
(x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
black x s \<and> x \<noteq> r

goal (1 subgoal):
 1. black y s \<and> y \<noteq> r
[PROOF STEP]
apply (clarsimp simp: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s \<and> x \<noteq> r)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
apply (drule predicate2D[OF rtranclp_mono[where s="\<lambda>x y. (x points_to y) s", OF predicate2I], rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa y. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (xaa points_to y) s \<and> xaa \<noteq> r\<rbrakk> \<Longrightarrow> (xaa points_to y) s
 2. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
apply (clarsimp split: obj_at_splits if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> black y s \<and> y \<noteq> r
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> black y s
 2. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> y \<noteq> r
[PROOF STEP]
apply (rule reachable_blackD, assumption, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> reachable y s
 2. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> y \<noteq> r
[PROOF STEP]
apply (simp add: reachable_def reaches_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> x \<in> tso_store_refs s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> y \<noteq> r
[PROOF STEP]
apply (blast intro: rtranclp.intros(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to y) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x\<rbrakk> \<Longrightarrow> y \<noteq> r
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to r) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x; y = r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule (1) reachable_blackD[where r=r])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to r) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x; y = r\<rbrakk> \<Longrightarrow> reachable r s
 2. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to r) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x; y = r; black r s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: reachable_def reaches_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to r) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x; y = r\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> x \<in> tso_store_refs s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x r
 2. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to r) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x; y = r; black r s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (blast intro: rtranclp.intros(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>no_grey_refs s; white r s; reachable_snapshot_inv s; (x points_to r) s; black x s; x \<noteq> r; xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x; y = r; black r s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
black y s \<and> y \<noteq> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
black y s \<and> y \<noteq> r

goal (1 subgoal):
 1. \<And>y. reachable y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<Longrightarrow> in_snapshot y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
black y s \<and> y \<noteq> r
[PROOF STEP]
show "in_snapshot y ?s'"
[PROOF STATE]
proof (prove)
using this:
black y s \<and> y \<noteq> r

goal (1 subgoal):
 1. in_snapshot y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
unfolding in_snapshot_def
[PROOF STATE]
proof (prove)
using this:
black y s \<and> y \<noteq> r

goal (1 subgoal):
 1. black y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)) \<or> (\<exists>x. (x grey_protects_white y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
in_snapshot y (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_alloc[simp]:
  assumes rn: "sys_heap s r = None"
  shows "mut_m.reachable m r' (s(mutator m' := (s (mutator m'))\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := (s sys)\<lparr>heap := (sys_heap s)(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
     \<longleftrightarrow> mut_m.reachable m r' s \<or> (m' = m \<and> r' = r)" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) = (mut_m.reachable m r' s \<or> m' = m \<and> r' = r)
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<Longrightarrow> mut_m.reachable m r' s \<or> m' = m \<and> r' = r
 2. mut_m.reachable m r' s \<or> m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (2 subgoals):
 1. mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<Longrightarrow> mut_m.reachable m r' s \<or> m' = m \<and> r' = r
 2. mut_m.reachable m r' s \<or> m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
sys_heap s r = None
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
sys_heap s r = None

goal (1 subgoal):
 1. mut_m.reachable m r' s \<or> m' = m \<and> r' = r
[PROOF STEP]
proof(induct rule: reachable_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 2. \<And>x. \<lbrakk>x \<in> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 3. \<And>x. \<lbrakk>x \<in> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 4. \<And>x y. \<lbrakk>mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); (x points_to y) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); sys_heap s r = None \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r; sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m y s \<or> m' = m \<and> y = r
[PROOF STEP]
case (reaches x y)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
(x points_to y) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
sys_heap s r = None \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
sys_heap s r = None

goal (4 subgoals):
 1. \<And>x. \<lbrakk>x \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 2. \<And>x. \<lbrakk>x \<in> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 3. \<And>x. \<lbrakk>x \<in> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 4. \<And>x y. \<lbrakk>mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); (x points_to y) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); sys_heap s r = None \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r; sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m y s \<or> m' = m \<and> y = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
(x points_to y) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
sys_heap s r = None \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
sys_heap s r = None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
(x points_to y) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
sys_heap s r = None \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
sys_heap s r = None

goal (1 subgoal):
 1. mut_m.reachable m y s \<or> m' = m \<and> y = r
[PROOF STEP]
by clarsimp (fastforce simp: mut_m.reachable_def reaches_def elim: rtranclp.intros(2) split: obj_at_splits)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m y s \<or> m' = m \<and> y = r

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 2. \<And>x. \<lbrakk>x \<in> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
 3. \<And>x. \<lbrakk>x \<in> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)); sys_heap s r = None\<rbrakk> \<Longrightarrow> mut_m.reachable m x s \<or> m' = m \<and> x = r
[PROOF STEP]
qed (auto simp: fun_upd_apply split: if_splits)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' s \<or> m' = m \<and> r' = r

goal (1 subgoal):
 1. mut_m.reachable m r' s \<or> m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mut_m.reachable m r' s \<or> m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' s \<or> m' = m \<and> r' = r

goal (1 subgoal):
 1. mut_m.reachable m r' s \<or> m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mut_m.reachable m r' s \<or> m' = m \<and> r' = r
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
mut_m.reachable m r' s \<or> m' = m \<and> r' = r

goal (1 subgoal):
 1. mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
proof(rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mut_m.reachable m r' s \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
assume "mut_m.reachable m r' s"
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' s

goal (2 subgoals):
 1. mut_m.reachable m r' s \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mut_m.reachable m r' s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mut_m.reachable m r' s

goal (1 subgoal):
 1. mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
proof(induct rule: reachable_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. \<And>x. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 3. \<And>x. x \<in> mut_m.tso_store_refs m s \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 4. \<And>x y. \<lbrakk>mut_m.reachable m x s; (x points_to y) s; mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))\<rbrakk> \<Longrightarrow> mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
case (tso_root x)
[PROOF STATE]
proof (state)
this:
x \<in> mut_m.tso_store_refs m s

goal (4 subgoals):
 1. \<And>x. x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. \<And>x. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 3. \<And>x. x \<in> mut_m.tso_store_refs m s \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 4. \<And>x y. \<lbrakk>mut_m.reachable m x s; (x points_to y) s; mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))\<rbrakk> \<Longrightarrow> mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> mut_m.tso_store_refs m s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
unfolding mut_m.reachable_def
[PROOF STATE]
proof (prove)
using this:
x \<in> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. \<exists>xa. xa \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<and> (xa reaches x) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (3 subgoals):
 1. \<And>x. x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. \<And>x. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 3. \<And>x y. \<lbrakk>mut_m.reachable m x s; (x points_to y) s; mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))\<rbrakk> \<Longrightarrow> mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. \<And>x. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 3. \<And>x y. \<lbrakk>mut_m.reachable m x s; (x points_to y) s; mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))\<rbrakk> \<Longrightarrow> mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
case (reaches x y)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m x s
(x points_to y) s
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (3 subgoals):
 1. \<And>x. x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. \<And>x. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 3. \<And>x y. \<lbrakk>mut_m.reachable m x s; (x points_to y) s; mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))\<rbrakk> \<Longrightarrow> mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
with rn
[PROOF STATE]
proof (chain)
picking this:
sys_heap s r = None
mut_m.reachable m x s
(x points_to y) s
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sys_heap s r = None
mut_m.reachable m x s
(x points_to y) s
mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (1 subgoal):
 1. mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
unfolding mut_m.reachable_def
[PROOF STATE]
proof (prove)
using this:
sys_heap s r = None
\<exists>xa. xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<and> (xa reaches x) s
(x points_to y) s
\<exists>xa. xa \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<and> (xa reaches x) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (1 subgoal):
 1. \<exists>x. x \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<and> (x reaches y) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
mut_m.reachable m y (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (2 subgoals):
 1. \<And>x. x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
 2. \<And>x. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
qed (auto simp: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal (1 subgoal):
 1. m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
assume "m' = m \<and> r' = r"
[PROOF STATE]
proof (state)
this:
m' = m \<and> r' = r

goal (1 subgoal):
 1. m' = m \<and> r' = r \<Longrightarrow> mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
with rn
[PROOF STATE]
proof (chain)
picking this:
sys_heap s r = None
m' = m \<and> r' = r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sys_heap s r = None
m' = m \<and> r' = r

goal (1 subgoal):
 1. mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
unfolding mut_m.reachable_def
[PROOF STATE]
proof (prove)
using this:
sys_heap s r = None
m' = m \<and> r' = r

goal (1 subgoal):
 1. \<exists>x. x \<in> roots ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<and> (x reaches r') (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
by (fastforce simp: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mut_m.reachable m r' (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_snapshot_inv_alloc[simp, elim!]:
  fixes s :: "('field, 'mut, 'payload, 'ref) lsts"
  assumes rsi: "reachable_snapshot_inv s"
  assumes rn: "sys_heap s r = None"
  assumes fl: "fl = sys_fM s"
  assumes vri: "valid_refs_inv s"
  shows "reachable_snapshot_inv (s(mutator m' := (s (mutator m'))\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := (s sys)\<lparr>heap := (sys_heap s)(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))"
(is "reachable_snapshot_inv ?s'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_snapshot_inv (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachable_snapshot_inv s
sys_heap s r = None
fl = sys_fM s
valid_refs_inv s

goal (1 subgoal):
 1. reachable_snapshot_inv (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
[PROOF STEP]
unfolding reachable_snapshot_inv_def in_snapshot_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. reachable x s \<longrightarrow> black x s \<or> (\<exists>xa. (xa grey_protects_white x) s)
sys_heap s r = None
fl = sys_fM s
valid_refs_inv s

goal (1 subgoal):
 1. \<forall>x. reachable x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<longrightarrow> black x (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)) \<or> (\<exists>xa. (xa grey_protects_white x) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>)))
[PROOF STEP]
by (auto simp del: reachable_fun_upd)


[STATEMENT]
lemma reachable_snapshot_inv_discard_roots[simp]:
  "\<lbrakk> reachable_snapshot_inv s; roots' \<subseteq> roots (s (mutator m)) \<rbrakk>
     \<Longrightarrow> reachable_snapshot_inv (s(mutator m := (s (mutator m))\<lparr>roots := roots'\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable_snapshot_inv s; roots' \<subseteq> mut_roots s\<rbrakk> \<Longrightarrow> reachable_snapshot_inv (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>))
[PROOF STEP]
unfolding reachable_snapshot_inv_def reachable_def in_snapshot_def grey_protects_white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (\<exists>xa. xa \<in> mut_roots s \<union> mut_ghost_honorary_root s \<union> tso_store_refs s \<and> (xa reaches x) s) \<longrightarrow> black x s \<or> (\<exists>xa. grey xa s \<and> (xa has_white_path_to x) s); roots' \<subseteq> mut_roots s\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa. xa \<in> mut_roots (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>)) \<union> mut_ghost_honorary_root (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>)) \<union> tso_store_refs (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>)) \<and> (xa reaches x) (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>))) \<longrightarrow> black x (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>)) \<or> (\<exists>xa. grey xa (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>)) \<and> (xa has_white_path_to x) (s(mutator m := s (mutator m)\<lparr>roots := roots'\<rparr>)))
[PROOF STEP]
by (auto simp: fun_upd_apply)


[STATEMENT]
lemma reachable_snapshot_inv_load[simp]:
  "\<lbrakk> reachable_snapshot_inv s; sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'; r \<in> mut_roots s \<rbrakk>
     \<Longrightarrow> reachable_snapshot_inv (s(mutator m := s (mutator m)\<lparr> roots := mut_roots s \<union> Option.set_option r' \<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable_snapshot_inv s; sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'; r \<in> mut_roots s\<rbrakk> \<Longrightarrow> reachable_snapshot_inv (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
unfolding reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. reachable x s \<longrightarrow> black x s \<or> (\<exists>xa. grey xa s \<and> (xa has_white_path_to x) s); sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'; r \<in> mut_roots s\<rbrakk> \<Longrightarrow> \<forall>x. reachable x (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) \<longrightarrow> black x (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) \<or> (\<exists>xa. grey xa (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) \<and> (xa has_white_path_to x) (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)))
[PROOF STEP]
by (simp add: fun_upd_apply)


[STATEMENT]
lemma reachable_snapshot_inv_store_ins[simp]:
  "\<lbrakk> reachable_snapshot_inv s; r \<in> mut_roots s; (\<exists>r'. opt_r' = Some r') \<longrightarrow> the opt_r' \<in> mut_roots s \<rbrakk>
     \<Longrightarrow> reachable_snapshot_inv (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>,
                                  sys := s sys\<lparr>  mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r']) \<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable_snapshot_inv s; r \<in> mut_roots s; (\<exists>r'. opt_r' = Some r') \<longrightarrow> the opt_r' \<in> mut_roots s\<rbrakk> \<Longrightarrow> reachable_snapshot_inv (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>))
[PROOF STEP]
unfolding reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def reachable_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (\<exists>xa. xa \<in> mut_roots s \<union> mut_ghost_honorary_root s \<union> tso_store_refs s \<and> (xa reaches x) s) \<longrightarrow> black x s \<or> (\<exists>xa. grey xa s \<and> (xa has_white_path_to x) s); r \<in> mut_roots s; (\<exists>r'. opt_r' = Some r') \<longrightarrow> the opt_r' \<in> mut_roots s\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa. xa \<in> mut_roots (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<union> mut_ghost_honorary_root (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<union> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<and> (xa reaches x) (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>))) \<longrightarrow> black x (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<or> (\<exists>xa. grey xa (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<and> (xa has_white_path_to x) (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x. (\<exists>xa. (xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s) \<and> (xa reaches x) s) \<longrightarrow> black x s \<or> (\<exists>xa. grey xa s \<and> (xa has_white_path_to x) s); r \<in> mut_roots s; (\<exists>r'. opt_r' = Some r') \<longrightarrow> the opt_r' \<in> mut_roots s; xa \<in> mut_roots s \<or> xa \<in> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)); (xa reaches x) s; \<forall>xa. grey xa (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<longrightarrow> \<not> (xa has_white_path_to x) s\<rbrakk> \<Longrightarrow> black x (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>))
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; (\<exists>r'. opt_r' = Some r') \<longrightarrow> the opt_r' \<in> mut_roots s; xa \<in> mut_roots s \<or> xa \<in> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)); (xa reaches x) s; \<forall>xa. grey xa (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)) \<longrightarrow> \<not> (xa has_white_path_to x) s; (\<exists>xa. (xa \<in> mut_roots s \<or> xa \<in> mut_ghost_honorary_root s \<or> xa \<in> tso_store_refs s) \<and> (xa reaches x) s) \<longrightarrow> black x s \<or> (\<exists>xa. grey xa s \<and> (xa has_white_path_to x) s)\<rbrakk> \<Longrightarrow> black x (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>))
[PROOF STEP]
apply (auto simp: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; (xa reaches x) s; \<forall>xa. grey xa s \<longrightarrow> \<not> (xa has_white_path_to x) s; xa \<in> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f None])\<rparr>)); opt_r' = None; \<forall>xa. xa \<notin> mut_roots s \<and> xa \<notin> mut_ghost_honorary_root s \<and> xa \<notin> tso_store_refs s \<or> \<not> (xa reaches x) s\<rbrakk> \<Longrightarrow> black x s
 2. \<And>x xa. \<lbrakk>r \<in> mut_roots s; (xa reaches x) s; \<forall>xa. grey xa s \<longrightarrow> \<not> (xa has_white_path_to x) s; xa \<in> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)); the opt_r' \<in> mut_roots s; \<forall>xa. xa \<notin> mut_roots s \<and> xa \<notin> mut_ghost_honorary_root s \<and> xa \<notin> tso_store_refs s \<or> \<not> (xa reaches x) s\<rbrakk> \<Longrightarrow> black x s
[PROOF STEP]
(* FIXME what's gone wrong here? *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; (xa reaches x) s; \<forall>xa. grey xa s \<longrightarrow> \<not> (xa has_white_path_to x) s; xa \<in> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f None])\<rparr>)); opt_r' = None; \<forall>xa. xa \<notin> mut_roots s \<and> xa \<notin> mut_ghost_honorary_root s \<and> xa \<notin> tso_store_refs s \<or> \<not> (xa reaches x) s\<rbrakk> \<Longrightarrow> black x s
 2. \<And>x xa. \<lbrakk>r \<in> mut_roots s; (xa reaches x) s; \<forall>xa. grey xa s \<longrightarrow> \<not> (xa has_white_path_to x) s; xa \<in> tso_store_refs (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m := sys_mem_store_buffers (mutator m) s @ [mw_Mutate r f opt_r'])\<rparr>)); the opt_r' \<in> mut_roots s; \<forall>xa. xa \<notin> mut_roots s \<and> xa \<notin> mut_ghost_honorary_root s \<and> xa \<notin> tso_store_refs s \<or> \<not> (xa reaches x) s\<rbrakk> \<Longrightarrow> black x s
[PROOF STEP]
apply (subst (asm) tso_store_refs_simps; force)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WL_mo_co_mark[simp]:
  "ghost_honorary_grey (s p) = {}
     \<Longrightarrow> WL p' (s(p := s p\<lparr> ghost_honorary_grey := rs \<rparr>)) = WL p' s \<union> { r |r. p' = p \<and> r \<in> rs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghost_honorary_grey (s p) = {} \<Longrightarrow> WL p' (s(p := s p\<lparr>ghost_honorary_grey := rs\<rparr>)) = WL p' s \<union> {r |r. p' = p \<and> r \<in> rs}
[PROOF STEP]
unfolding WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghost_honorary_grey (s p) = {} \<Longrightarrow> W ((s(p := s p\<lparr>ghost_honorary_grey := rs\<rparr>)) p') \<union> ghost_honorary_grey ((s(p := s p\<lparr>ghost_honorary_grey := rs\<rparr>)) p') = W (s p') \<union> ghost_honorary_grey (s p') \<union> {r |r. p' = p \<and> r \<in> rs}
[PROOF STEP]
by (simp add: fun_upd_apply)


[STATEMENT]
lemma ghost_honorary_grey_mo_co_mark[simp]:
  "\<lbrakk> ghost_honorary_grey (s p) = {} \<rbrakk> \<Longrightarrow> black b (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<longleftrightarrow> black b s \<and> b \<noteq> r"
  "\<lbrakk> ghost_honorary_grey (s p) = {} \<rbrakk> \<Longrightarrow> grey g (s(p := (s p)\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<longleftrightarrow> grey g s \<or> g = r"
  "\<lbrakk> ghost_honorary_grey (s p) = {} \<rbrakk> \<Longrightarrow> white w (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))  \<longleftrightarrow> white w s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ghost_honorary_grey (s p) = {} \<Longrightarrow> black b (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) = (black b s \<and> b \<noteq> r)) &&& (ghost_honorary_grey (s p) = {} \<Longrightarrow> grey g (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) = (grey g s \<or> g = r)) &&& (ghost_honorary_grey (s p) = {} \<Longrightarrow> white w (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) = white w s)
[PROOF STEP]
unfolding black_def grey_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ghost_honorary_grey (s p) = {} \<Longrightarrow> (marked b (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<and> (\<nexists>x. b \<in> WL x (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)))) = ((marked b s \<and> (\<nexists>x. b \<in> WL x s)) \<and> b \<noteq> r)) &&& (ghost_honorary_grey (s p) = {} \<Longrightarrow> (\<exists>x. g \<in> WL x (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))) = ((\<exists>x. g \<in> WL x s) \<or> g = r)) &&& (ghost_honorary_grey (s p) = {} \<Longrightarrow> white w (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) = white w s)
[PROOF STEP]
by (auto simp: fun_upd_apply)


[STATEMENT]
lemma ghost_honorary_grey_mo_co_W[simp]:
  "ghost_honorary_grey (s p') = {r}
     \<Longrightarrow> (WL p (s(p' := (s p')\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>))) = (WL p s)"
  "ghost_honorary_grey (s p') = {r}
     \<Longrightarrow> grey g (s(p' := (s p')\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) \<longleftrightarrow> grey g s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ghost_honorary_grey (s p') = {r} \<Longrightarrow> WL p (s(p' := s p'\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) = WL p s) &&& (ghost_honorary_grey (s p') = {r} \<Longrightarrow> grey g (s(p' := s p'\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) = grey g s)
[PROOF STEP]
unfolding grey_def WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ghost_honorary_grey (s p') = {r} \<Longrightarrow> W ((s(p' := s p'\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) p) \<union> ghost_honorary_grey ((s(p' := s p'\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) p) = W (s p) \<union> ghost_honorary_grey (s p)) &&& (ghost_honorary_grey (s p') = {r} \<Longrightarrow> (\<exists>x. g \<in> W ((s(p' := s p'\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) x) \<union> ghost_honorary_grey ((s(p' := s p'\<lparr>W := insert r (W (s p')), ghost_honorary_grey := {}\<rparr>)) x)) = (\<exists>x. g \<in> W (s x) \<union> ghost_honorary_grey (s x)))
[PROOF STEP]
by (auto simp: fun_upd_apply split: process_name.splits if_splits)


[STATEMENT]
lemma reachable_sweep_loop_free:
  "mut_m.reachable m r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>))
   \<Longrightarrow> mut_m.reachable m r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mut_m.reachable m r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) \<Longrightarrow> mut_m.reachable m r s
[PROOF STEP]
unfolding mut_m.reachable_def reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> roots ((s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) (mutator m)) \<union> ghost_honorary_root ((s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) (mutator m)) \<union> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) \<and> (\<lambda>x y. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)))\<^sup>*\<^sup>* x r \<Longrightarrow> \<exists>x. x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x r
[PROOF STEP]
by (clarsimp simp: fun_upd_apply) (metis (no_types, lifting) mono_rtranclp)


[STATEMENT]
lemma reachable_deref_del[simp]:
  "\<lbrakk> sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; r \<in> mut_m.mut_roots m s; mut_m.mut_ghost_honorary_root m s = {} \<rbrakk>
   \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr> ghost_honorary_root := Option.set_option opt_r', ref := opt_r' \<rparr>))
   \<longleftrightarrow> mut_m.reachable m' y s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}\<rbrakk> \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)) = mut_m.reachable m' y s
[PROOF STEP]
unfolding mut_m.reachable_def reaches_def sys_load_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(do_load_action (mr_Ref r f) \<circ> processors_view_of_memory (mutator m)) (s sys) = mv_Ref opt_r'; r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}\<rbrakk> \<Longrightarrow> (\<exists>x. x \<in> roots ((s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)) (mutator m')) \<union> ghost_honorary_root ((s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)) (mutator m')) \<union> mut_m.tso_store_refs m' (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)) \<and> (\<lambda>x y. (x points_to y) (s(mutator m := s (mutator m)\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)))\<^sup>*\<^sup>* x y) = (\<exists>x. x \<in> roots (s (mutator m')) \<union> ghost_honorary_root (s (mutator m')) \<union> mut_m.tso_store_refs m' s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y)
[PROOF STEP]
apply (clarsimp simp: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y) = (\<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; \<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> roots (s (mutator m))\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 3. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 4. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 3. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (erule option_bind_invE; auto dest!: fold_stores_points_to)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Some x; m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields a f = Some x; (r points_to x) s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x a w. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Some x; m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields a f = Some x; w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 3. \<And>x. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 4. \<lbrakk>r \<in> roots (s (mutator m)); ghost_honorary_root (s (mutator m)) = {}; opt_r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); m' = m; \<exists>x. (x \<in> roots (s (mutator m)) \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> roots (s (mutator m)) \<or> Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some x \<or> x \<in> mut_m.tso_store_refs m s) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (auto elim!: converse_rtranclp_into_rtranclp[rotated]
              simp: mut_m.tso_store_refs_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma no_black_refs_dequeue[simp]:
  "\<lbrakk> sys_mem_store_buffers p s = mw_Mark r fl # ws; no_black_refs s; valid_W_inv s \<rbrakk>
   \<Longrightarrow> no_black_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))"
  "\<lbrakk> sys_mem_store_buffers p s = mw_Mutate r f r' # ws; no_black_refs s \<rbrakk>
     \<Longrightarrow> no_black_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := r')\<rparr>) (sys_heap s r)),
                                      mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_mem_store_buffers p s = mw_Mark r fl # ws; no_black_refs s; valid_W_inv s\<rbrakk> \<Longrightarrow> no_black_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))) &&& (\<lbrakk>sys_mem_store_buffers p s = mw_Mutate r f r' # ws; no_black_refs s\<rbrakk> \<Longrightarrow> no_black_refs (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)))
[PROOF STEP]
unfolding no_black_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_mem_store_buffers p s = mw_Mark r fl # ws; \<forall>x. \<not> black x s; valid_W_inv s\<rbrakk> \<Longrightarrow> \<forall>x. \<not> black x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))) &&& (\<lbrakk>sys_mem_store_buffers p s = mw_Mutate r f r' # ws; \<forall>x. \<not> black x s\<rbrakk> \<Longrightarrow> \<forall>x. \<not> black x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)))
[PROOF STEP]
by (auto simp: fun_upd_apply dest: valid_W_invD)