[STATEMENT]
lemma (in mut_m) marked_deletions_eq_imp:
  "eq_imp (\<lambda>r'. sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_fields (sys_heap s r')) \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')) \<^bold>\<otimes> tso_pending_mw_mutate (mutator m))
          marked_deletions"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (sys_fM s, map_option obj_fields (sys_heap s r'), map_option obj_mark (sys_heap s r'), filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s))) marked_deletions
[PROOF STEP]
unfolding eq_imp_def marked_deletions_def obj_at_field_on_heap_def ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (sys_fM s, map_option obj_fields (sys_heap s x), map_option obj_mark (sys_heap s x), filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = (sys_fM s', map_option obj_fields (sys_heap s' x), map_option obj_mark (sys_heap s' x), filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s'))) \<longrightarrow> (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case map_option obj_fields (sys_heap s r) of None \<Rightarrow> False | Some fs \<Rightarrow> case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s | _ \<Rightarrow> True)) = (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case map_option obj_fields (sys_heap s' r) of None \<Rightarrow> False | Some fs \<Rightarrow> case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s' | _ \<Rightarrow> True))
[PROOF STEP]
apply (clarsimp simp: all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s) = filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>fs. case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s) \<circ> obj_fields) x | _ \<Rightarrow> True)) = (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>fs. case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s') \<circ> obj_fields) x | _ \<Rightarrow> True))
[PROOF STEP]
apply (drule arg_cong[where f=set])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s'))\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>fs. case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s) \<circ> obj_fields) x | _ \<Rightarrow> True)) = (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>fs. case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s') \<circ> obj_fields) x | _ \<Rightarrow> True))
[PROOF STEP]
apply (subgoal_tac "\<forall>x. marked x s \<longleftrightarrow> marked x s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s')); \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>fs. case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s) \<circ> obj_fields) x | _ \<Rightarrow> True)) = (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>fs. case fs f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s') \<circ> obj_fields) x | _ \<Rightarrow> True))
 2. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s'))\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply (clarsimp cong: option.case_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); {x \<in> set (sys_mem_store_buffers (mutator m) s). is_mw_Mutate x} = {x \<in> set (sys_mem_store_buffers (mutator m) s'). is_mw_Mutate x}; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x2 \<Rightarrow> case obj_fields x2 f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s' | _ \<Rightarrow> True)) = (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x of mw_Mutate r f opt_r' \<Rightarrow> case sys_heap s' r of None \<Rightarrow> False | Some x2 \<Rightarrow> case obj_fields x2 f of None \<Rightarrow> True | Some r' \<Rightarrow> marked r' s' | _ \<Rightarrow> True))
 2. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s'))\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply (rule iffI; clarsimp simp: set_eq_iff split: option.splits mem_store_action.splits; blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = set (filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s'))\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); {x \<in> set (sys_mem_store_buffers (mutator m) s). is_mw_Mutate x} = {x \<in> set (sys_mem_store_buffers (mutator m) s'). is_mw_Mutate x}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
[PROOF STEP]
apply (rename_tac s s' x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); {x \<in> set (sys_mem_store_buffers (mutator m) s). is_mw_Mutate x} = {x \<in> set (sys_mem_store_buffers (mutator m) s'). is_mw_Mutate x}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
[PROOF STEP]
apply (drule_tac x=x in spec)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>sys_fM s = sys_fM s'; {x \<in> set (sys_mem_store_buffers (mutator m) s). is_mw_Mutate x} = {x \<in> set (sys_mem_store_buffers (mutator m) s'). is_mw_Mutate x}; map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
[PROOF STEP]
apply (force split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma marked_deletions_store_buffer_empty[intro]:
  "tso_pending_mutate (mutator m) s = [] \<Longrightarrow> mut_m.marked_deletions m s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = [] \<Longrightarrow> mut_m.marked_deletions m s
[PROOF STEP]
unfolding mut_m.marked_deletions_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = [] \<Longrightarrow> \<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> marked_deletion x s
[PROOF STEP]
by (auto simp: filter_empty_conv split: mem_store_action.splits)


[STATEMENT]
lemma obj_at_ref_sweep_loop_free[simp]:
  "obj_at P r (s(sys := (s sys)\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) \<longleftrightarrow> obj_at P r s \<and> r \<noteq> r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at P r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) = (obj_at P r s \<and> r \<noteq> r')
[PROOF STEP]
by (clarsimp simp: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma obj_at_alloc[simp]:
  "sys_heap s r' = None
  \<Longrightarrow> obj_at P r (s(m := mut_m_s', sys := (s sys)\<lparr> heap := sys_heap s(r' \<mapsto> obj) \<rparr>))
  \<longleftrightarrow> (obj_at P r s \<or> (r = r' \<and> P obj))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_heap s r' = None \<Longrightarrow> obj_at P r (s(m := mut_m_s', sys := s sys\<lparr>heap := sys_heap s(r' \<mapsto> obj)\<rparr>)) = (obj_at P r s \<or> r = r' \<and> P obj)
[PROOF STEP]
unfolding ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_heap s r' = None \<Longrightarrow> obj_at P r (s(m := mut_m_s', sys := s sys\<lparr>heap := sys_heap s(r' \<mapsto> obj)\<rparr>)) = (obj_at P r s \<or> r = r' \<and> P obj)
[PROOF STEP]
by (simp add: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma valid_ref_valid_null_ref_simps[simp]:
  "valid_ref r (s(sys := do_store_action w (s sys)\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) \<longleftrightarrow> valid_ref r s"
  "valid_null_ref r' (s(sys := do_store_action w (s sys)\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) \<longleftrightarrow> valid_null_ref r' s"
  "valid_null_ref r' (s(mutator m := mut_s', sys := (s sys)\<lparr> heap := (heap (s sys))(r'' \<mapsto> obj) \<rparr>)) \<longleftrightarrow> valid_null_ref r' s \<or> r' = Some r''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>s. True) r (s(sys := do_store_action w (s sys)\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = obj_at (\<lambda>s. True) r s &&& valid_null_ref r' (s(sys := do_store_action w (s sys)\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = valid_null_ref r' s &&& valid_null_ref r' (s(mutator m := mut_s', sys := s sys\<lparr>heap := sys_heap s(r'' \<mapsto> obj)\<rparr>)) = (valid_null_ref r' s \<or> r' = Some r'')
[PROOF STEP]
unfolding do_store_action_def valid_null_ref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>s. True) r (s(sys := (case w of mw_Mark r gc_mark \<Rightarrow> s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. gc_mark)) (sys_heap s r))\<rparr> | mw_Mutate r f new_r \<Rightarrow> s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := new_r)\<rparr>) (sys_heap s r))\<rparr> | mw_Mutate_Payload r f pl \<Rightarrow> s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r))\<rparr> | mw_fA gc_mark \<Rightarrow> s sys\<lparr>fA := gc_mark\<rparr> | mw_fM gc_mark \<Rightarrow> s sys\<lparr>fM := gc_mark\<rparr> | mw_Phase gc_phase \<Rightarrow> s sys\<lparr>phase := gc_phase\<rparr>)\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = obj_at (\<lambda>s. True) r s &&& (case r' of None \<Rightarrow> \<lambda>s. True | Some r' \<Rightarrow> obj_at (\<lambda>s. True) r') (s(sys := (case w of mw_Mark r gc_mark \<Rightarrow> s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. gc_mark)) (sys_heap s r))\<rparr> | mw_Mutate r f new_r \<Rightarrow> s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := new_r)\<rparr>) (sys_heap s r))\<rparr> | mw_Mutate_Payload r f pl \<Rightarrow> s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r))\<rparr> | mw_fA gc_mark \<Rightarrow> s sys\<lparr>fA := gc_mark\<rparr> | mw_fM gc_mark \<Rightarrow> s sys\<lparr>fM := gc_mark\<rparr> | mw_Phase gc_phase \<Rightarrow> s sys\<lparr>phase := gc_phase\<rparr>)\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = (case r' of None \<Rightarrow> \<lambda>s. True | Some r' \<Rightarrow> obj_at (\<lambda>s. True) r') s &&& (case r' of None \<Rightarrow> \<lambda>s. True | Some r' \<Rightarrow> obj_at (\<lambda>s. True) r') (s(mutator m := mut_s', sys := s sys\<lparr>heap := sys_heap s(r'' \<mapsto> obj)\<rparr>)) = ((case r' of None \<Rightarrow> \<lambda>s. True | Some r' \<Rightarrow> obj_at (\<lambda>s. True) r') s \<or> r' = Some r'')
[PROOF STEP]
by (auto simp: fun_upd_apply
        split: mem_store_action.splits obj_at_splits option.splits)


[STATEMENT]
lemma reachable_load[simp]:
  assumes "sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'"
  assumes "r \<in> mut_roots s"
  shows "mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr> roots := mut_roots s \<union> Option.set_option r' \<rparr>)) \<longleftrightarrow> mut_m.reachable m' y s" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
[PROOF STEP]
proof(cases "m' = m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m' = m \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
 2. m' \<noteq> m \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
m' = m

goal (2 subgoals):
 1. m' = m \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
 2. m' \<noteq> m \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) \<Longrightarrow> mut_m.reachable m' y s
 2. mut_m.reachable m' y s \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))

goal (2 subgoals):
 1. mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) \<Longrightarrow> mut_m.reachable m' y s
 2. mut_m.reachable m' y s \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
with assms True
[PROOF STATE]
proof (chain)
picking this:
sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'
r \<in> mut_roots s
m' = m
mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref r'
r \<in> mut_roots s
m' = m
mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))

goal (1 subgoal):
 1. mut_m.reachable m' y s
[PROOF STEP]
unfolding sys_load_def
[PROOF STATE]
proof (prove)
using this:
(do_load_action (mr_Ref r f) \<circ> processors_view_of_memory (mutator m)) (s sys) = mv_Ref r'
r \<in> mut_roots s
m' = m
mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))

goal (1 subgoal):
 1. mut_m.reachable m' y s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> mut_roots s; m' = m; reachable y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> (\<Union>x\<in>set_option (heap (processors_view_of_memory (mutator m) (s sys)) r). set_option (obj_fields x f))\<rparr>)); r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f)\<rbrakk> \<Longrightarrow> reachable y s
[PROOF STEP]
apply (clarsimp simp: reachable_def reaches_def tso_store_refs_def sys_load_def fold_stores_def fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); x \<in> mut_roots s \<or> (\<exists>xa\<in>set_option (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r). obj_fields xa f = Some x) \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<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> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_roots s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set_option (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r). obj_fields xa f = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 3. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_ghost_honorary_root s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 4. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa 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> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set_option (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r). obj_fields xa f = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_ghost_honorary_root s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 3. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa 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> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; x \<in> mut_ghost_honorary_root s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa 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> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 3. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set_option (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r). obj_fields xa f = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa 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> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set_option (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r). obj_fields xa f = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set_option (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r). obj_fields xa f = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (fold fold_stores_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Option.bind (heap (processors_view_of_memory (mutator m) (s sys)) r) (\<lambda>obj. obj_fields obj f); (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; \<exists>xa\<in>set_option (heap (processors_view_of_memory (mutator m) (s sys)) r). obj_fields xa f = Some x\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Some x; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields xa f = Some x; heap (processors_view_of_memory (mutator m) (s sys)) r = Some xa\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (drule (1) fold_stores_points_to)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Some x; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields xa f = Some x; (r points_to x) s \<or> (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> store_refs w)\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Some x; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields xa f = Some x; (r points_to x) s\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
 2. \<And>x xa. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Some x; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields xa f = Some x; \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> store_refs w\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (fastforce elim!: converse_rtranclp_into_rtranclp[rotated] split: obj_at_splits intro!: ranI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Some x; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields xa f = Some x; \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> store_refs w\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply (clarsimp split: mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa w. \<lbrakk>r \<in> mut_roots s; m' = m; r' = Some x; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; obj_fields xa f = Some x; w \<in> set (sys_mem_store_buffers (mutator m) s); \<forall>x11 x12. w \<noteq> mw_Mark x11 x12; \<forall>x21 x22 x23. w = mw_Mutate x21 x22 x23 \<longrightarrow> x = x21 \<or> x23 = Some x; \<forall>x31. (\<forall>x32 x33. w \<noteq> mw_Mutate_Payload x31 x32 x33) \<or> x = x31; \<forall>x4. w \<noteq> mw_fA x4; \<forall>x5. w \<noteq> mw_fM x5; \<forall>x6. w \<noteq> mw_Phase x6\<rbrakk> \<Longrightarrow> \<exists>x. (x \<in> mut_roots s \<or> x \<in> mut_ghost_honorary_root s \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). (\<forall>x11 x12. xa \<noteq> mw_Mark x11 x12) \<and> (\<forall>x21 x22 x23. xa = mw_Mutate x21 x22 x23 \<longrightarrow> x = x21 \<or> x23 = Some x) \<and> (\<forall>x31. (\<exists>x32 x33. xa = mw_Mutate_Payload x31 x32 x33) \<longrightarrow> x = x31) \<and> (\<forall>x4. xa \<noteq> mw_fA x4) \<and> (\<forall>x5. xa \<noteq> mw_fM x5) \<and> (\<forall>x6. xa \<noteq> mw_Phase x6))) \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
apply meson
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mut_m.reachable m' y s

goal (1 subgoal):
 1. mut_m.reachable m' y s \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mut_m.reachable m' y s \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
mut_m.reachable m' y s

goal (1 subgoal):
 1. mut_m.reachable m' y s \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
m' = m
mut_m.reachable m' y s
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
m' = m
mut_m.reachable m' y s

goal (1 subgoal):
 1. mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
unfolding mut_m.reachable_def
[PROOF STATE]
proof (prove)
using this:
m' = m
\<exists>x. x \<in> roots (s (mutator m')) \<union> ghost_honorary_root (s (mutator m')) \<union> mut_m.tso_store_refs m' s \<and> (x reaches y) s

goal (1 subgoal):
 1. \<exists>x. x \<in> roots ((s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) (mutator m')) \<union> ghost_honorary_root ((s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) (mutator m')) \<union> mut_m.tso_store_refs m' (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) \<and> (x reaches y) (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))
[PROOF STEP]
by (fastforce simp: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s

goal (1 subgoal):
 1. m' \<noteq> m \<Longrightarrow> mut_m.reachable m' y (s(mutator m := s (mutator m)\<lparr>roots := mut_roots s \<union> set_option r'\<rparr>)) = mut_m.reachable m' y s
[PROOF STEP]
qed (simp add: fun_upd_apply)


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


[STATEMENT]
lemma WL_hs_done[simp]:
  "ghost_honorary_grey (s (mutator m)) = {}
     \<Longrightarrow> WL p (s(mutator m := s (mutator m)\<lparr> W := {}, ghost_hs_phase := hp' \<rparr>,
                 sys   := s sys\<lparr> hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)),
                                 ghost_hs_in_sync := in' \<rparr>))
      = (case p of gc \<Rightarrow> WL gc s | mutator m' \<Rightarrow> (if m' = m then {} else WL (mutator m') s) | sys \<Rightarrow> WL sys s \<union> WL (mutator m) s)"
  "ghost_honorary_grey (s (mutator m)) = {}
     \<Longrightarrow> WL p (s(mutator m := s (mutator m)\<lparr> W := {} \<rparr>,
                 sys   := s sys\<lparr> hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)),
                                 ghost_hs_in_sync := in' \<rparr>))
      = (case p of gc \<Rightarrow> WL gc s | mutator m' \<Rightarrow> (if m' = m then {} else WL (mutator m') s) | sys \<Rightarrow> WL sys s \<union> WL (mutator m) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ghost_honorary_grey (s (mutator m)) = {} \<Longrightarrow> WL p (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hp'\<rparr>, sys := s sys\<lparr>hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := in'\<rparr>)) = (case p of mutator m' \<Rightarrow> if m' = m then {} else WL (mutator m') s | gc \<Rightarrow> WL gc s | sys \<Rightarrow> WL sys s \<union> WL (mutator m) s)) &&& (ghost_honorary_grey (s (mutator m)) = {} \<Longrightarrow> WL p (s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := in'\<rparr>)) = (case p of mutator m' \<Rightarrow> if m' = m then {} else WL (mutator m') s | gc \<Rightarrow> WL gc s | sys \<Rightarrow> WL sys s \<union> WL (mutator m) s))
[PROOF STEP]
unfolding WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ghost_honorary_grey (s (mutator m)) = {} \<Longrightarrow> W ((s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hp'\<rparr>, sys := s sys\<lparr>hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := in'\<rparr>)) p) \<union> ghost_honorary_grey ((s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hp'\<rparr>, sys := s sys\<lparr>hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := in'\<rparr>)) p) = (case p of mutator m' \<Rightarrow> if m' = m then {} else W (s (mutator m')) \<union> ghost_honorary_grey (s (mutator m')) | gc \<Rightarrow> gc_W s \<union> gc_ghost_honorary_grey s | sys \<Rightarrow> sys_W s \<union> sys_ghost_honorary_grey s \<union> (W (s (mutator m)) \<union> ghost_honorary_grey (s (mutator m))))) &&& (ghost_honorary_grey (s (mutator m)) = {} \<Longrightarrow> W ((s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := in'\<rparr>)) p) \<union> ghost_honorary_grey ((s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hsp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := in'\<rparr>)) p) = (case p of mutator m' \<Rightarrow> if m' = m then {} else W (s (mutator m')) \<union> ghost_honorary_grey (s (mutator m')) | gc \<Rightarrow> gc_W s \<union> gc_ghost_honorary_grey s | sys \<Rightarrow> sys_W s \<union> sys_ghost_honorary_grey s \<union> (W (s (mutator m)) \<union> ghost_honorary_grey (s (mutator m)))))
[PROOF STEP]
by (auto simp: fun_upd_apply split: process_name.splits)


[STATEMENT]
lemma colours_load_W[iff]:
  "gc_W s = {} \<Longrightarrow> black r (s(gc := (s gc)\<lparr>W := W (s sys)\<rparr>, sys := (s sys)\<lparr>W := {}\<rparr>)) \<longleftrightarrow> black r s"
  "gc_W s = {} \<Longrightarrow> grey r (s(gc := (s gc)\<lparr>W := W (s sys)\<rparr>, sys := (s sys)\<lparr>W := {}\<rparr>)) \<longleftrightarrow> grey r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gc_W s = {} \<Longrightarrow> black r (s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) = black r s) &&& (gc_W s = {} \<Longrightarrow> grey r (s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) = grey r s)
[PROOF STEP]
unfolding black_def grey_def WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gc_W s = {} \<Longrightarrow> (marked r (s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) \<and> (\<nexists>x. r \<in> W ((s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) x) \<union> ghost_honorary_grey ((s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) x))) = (marked r s \<and> (\<nexists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x)))) &&& (gc_W s = {} \<Longrightarrow> (\<exists>x. r \<in> W ((s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) x) \<union> ghost_honorary_grey ((s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) x)) = (\<exists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x)))
[PROOF STEP]
apply (simp_all add: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. gc_W s = {} \<Longrightarrow> (marked r s \<and> (\<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))))) = (marked r s \<and> (\<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x)))
 2. gc_W s = {} \<Longrightarrow> (\<exists>x. (x = gc \<longrightarrow> r \<in> sys_W s \<or> r \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<in> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)))) = (\<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (26 subgoals):
 1. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> W (s x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); r \<in> sys_W s\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); r \<in> gc_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> False
 5. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); sys \<noteq> gc; r \<in> sys_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> False
 6. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); x \<noteq> gc; x \<noteq> sys; r \<in> W (s x)\<rbrakk> \<Longrightarrow> False
 7. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); x \<noteq> gc; x \<noteq> sys; r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 8. \<And>x. \<lbrakk>gc_W s = {}; x \<noteq> gc; x \<noteq> sys; r \<in> W (s x)\<rbrakk> \<Longrightarrow> \<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)
 9. \<And>x. \<lbrakk>gc_W s = {}; x \<noteq> gc; x \<noteq> sys; r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)
 10. \<And>x. \<lbrakk>gc_W s = {}; sys \<noteq> gc; r \<in> sys_ghost_honorary_grey s; \<nexists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
A total of 26 subgoals...
[PROOF STEP]
apply (case_tac [!] x)
[PROOF STATE]
proof (prove)
goal (78 subgoals):
 1. \<And>x x1. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> W (s x); x = mutator x1\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> W (s x); x = gc\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> W (s x); x = sys\<rbrakk> \<Longrightarrow> False
 4. \<And>x x1. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> ghost_honorary_grey (s x); x = mutator x1\<rbrakk> \<Longrightarrow> False
 5. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> ghost_honorary_grey (s x); x = gc\<rbrakk> \<Longrightarrow> False
 6. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. (x = gc \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))); r \<in> ghost_honorary_grey (s x); x = sys\<rbrakk> \<Longrightarrow> False
 7. \<And>x x1. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); r \<in> sys_W s; x = mutator x1\<rbrakk> \<Longrightarrow> False
 8. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); r \<in> sys_W s; x = gc\<rbrakk> \<Longrightarrow> False
 9. \<And>x. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); r \<in> sys_W s; x = sys\<rbrakk> \<Longrightarrow> False
 10. \<And>x x1. \<lbrakk>gc_W s = {}; marked r s; \<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x); r \<in> gc_ghost_honorary_grey s; x = mutator x1\<rbrakk> \<Longrightarrow> False
A total of 78 subgoals...
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WL_load_W[simp]:
  "gc_W s = {}
    \<Longrightarrow> (WL p (s(gc := (s gc)\<lparr>W := sys_W s\<rparr>, sys := (s sys)\<lparr>W := {}\<rparr>)))
     = (case p of gc \<Rightarrow> WL gc s \<union> sys_W s | mutator m \<Rightarrow> WL (mutator m) s | sys \<Rightarrow> sys_ghost_honorary_grey s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gc_W s = {} \<Longrightarrow> WL p (s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) = (case p of mutator m \<Rightarrow> WL (mutator m) s | gc \<Rightarrow> WL gc s \<union> sys_W s | sys \<Rightarrow> sys_ghost_honorary_grey s)
[PROOF STEP]
unfolding WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gc_W s = {} \<Longrightarrow> W ((s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) p) \<union> ghost_honorary_grey ((s(gc := s gc\<lparr>W := sys_W s\<rparr>, sys := s sys\<lparr>W := {}\<rparr>)) p) = (case p of mutator m \<Rightarrow> W (s (mutator m)) \<union> ghost_honorary_grey (s (mutator m)) | gc \<Rightarrow> gc_W s \<union> gc_ghost_honorary_grey s \<union> sys_W s | sys \<Rightarrow> sys_ghost_honorary_grey s)
[PROOF STEP]
by (auto simp: fun_upd_apply split: process_name.splits)


[STATEMENT]
lemma no_grey_refs_eq_imp:
  "eq_imp (\<lambda>(_::unit). (\<lambda>s. \<Union>p. WL p s))
          no_grey_refs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. \<Union>p. WL p s) no_grey_refs
[PROOF STEP]
by (auto simp add: eq_imp_def grey_def no_grey_refs_def set_eq_iff)


[STATEMENT]
lemma no_grey_refs_no_pending_marks:
  "\<lbrakk> no_grey_refs s; valid_W_inv s \<rbrakk> \<Longrightarrow> tso_no_pending_marks s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_grey_refs s; valid_W_inv s\<rbrakk> \<Longrightarrow> \<forall>x. filter is_mw_Mark (sys_mem_store_buffers x s) = []
[PROOF STEP]
unfolding no_grey_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<not> grey x s; valid_W_inv s\<rbrakk> \<Longrightarrow> \<forall>x. filter is_mw_Mark (sys_mem_store_buffers x s) = []
[PROOF STEP]
by (auto intro!: filter_False dest: valid_W_invD(2))


[STATEMENT]
lemma no_grey_refs_not_grey_reachableD:
  "no_grey_refs s \<Longrightarrow> \<not>grey_reachable x s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_grey_refs s \<Longrightarrow> \<not> grey_reachable x s
[PROOF STEP]
by (clarsimp simp: no_grey_refs_def grey_reachable_def)


[STATEMENT]
lemma no_grey_refsD:
  "no_grey_refs s \<Longrightarrow> r \<notin> W (s p)"
  "no_grey_refs s \<Longrightarrow> r \<notin> WL p s"
  "no_grey_refs s \<Longrightarrow> r \<notin> ghost_honorary_grey (s p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (no_grey_refs s \<Longrightarrow> r \<notin> W (s p)) &&& (no_grey_refs s \<Longrightarrow> r \<notin> WL p s) &&& (no_grey_refs s \<Longrightarrow> r \<notin> ghost_honorary_grey (s p))
[PROOF STEP]
by (auto simp: no_grey_refs_def)


[STATEMENT]
lemma no_grey_refs_marked[dest]:
  "\<lbrakk> marked r s; no_grey_refs s \<rbrakk> \<Longrightarrow> black r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>marked r s; no_grey_refs s\<rbrakk> \<Longrightarrow> black r s
[PROOF STEP]
by (auto simp: no_grey_refs_def black_def)


[STATEMENT]
lemma no_grey_refs_bwD[dest]:
  "\<lbrakk> heap (s sys) r = Some obj; no_grey_refs s \<rbrakk> \<Longrightarrow> black r s \<or> white r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_heap s r = Some obj; no_grey_refs s\<rbrakk> \<Longrightarrow> black r s \<or> white r s
[PROOF STEP]
by (clarsimp simp: black_def grey_def no_grey_refs_def white_def split: obj_at_splits)


[STATEMENT]
lemma reachable_blackD:
  "\<lbrakk> no_grey_refs s; reachable_snapshot_inv s; reachable r s \<rbrakk> \<Longrightarrow> black r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_grey_refs s; reachable_snapshot_inv s; reachable r s\<rbrakk> \<Longrightarrow> black r s
[PROOF STEP]
by (simp add: no_grey_refs_def reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def)


[STATEMENT]
lemma no_grey_refs_not_reachable:
  "\<lbrakk> no_grey_refs s; reachable_snapshot_inv s; white r s \<rbrakk> \<Longrightarrow> \<not>reachable r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_grey_refs s; reachable_snapshot_inv s; white r s\<rbrakk> \<Longrightarrow> \<not> reachable r s
[PROOF STEP]
by (fastforce simp: no_grey_refs_def reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def
             split: obj_at_splits)


[STATEMENT]
lemma no_grey_refs_not_rootD:
  "\<lbrakk> no_grey_refs s; reachable_snapshot_inv s; white r s \<rbrakk>
     \<Longrightarrow> r \<notin> mut_roots s \<and> r \<notin> mut_ghost_honorary_root s \<and> r \<notin> tso_store_refs s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_grey_refs s; reachable_snapshot_inv s; white r s\<rbrakk> \<Longrightarrow> r \<notin> mut_roots s \<and> r \<notin> mut_ghost_honorary_root s \<and> r \<notin> tso_store_refs s
[PROOF STEP]
apply (drule (2) no_grey_refs_not_reachable)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable_snapshot_inv s; white r s; \<not> reachable r s\<rbrakk> \<Longrightarrow> r \<notin> mut_roots s \<and> r \<notin> mut_ghost_honorary_root s \<and> r \<notin> tso_store_refs s
[PROOF STEP]
apply (force simp: reachable_def reaches_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma reachable_snapshot_inv_white_root:
  "\<lbrakk> white w s; w \<in> mut_roots s \<or> w \<in> mut_ghost_honorary_root s; reachable_snapshot_inv s \<rbrakk> \<Longrightarrow> \<exists>g. (g grey_protects_white w) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>white w s; w \<in> mut_roots s \<or> w \<in> mut_ghost_honorary_root s; reachable_snapshot_inv s\<rbrakk> \<Longrightarrow> \<exists>g. (g grey_protects_white w) s
[PROOF STEP]
unfolding reachable_snapshot_inv_def in_snapshot_def reachable_def grey_protects_white_def reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>white w s; w \<in> mut_roots s \<or> w \<in> mut_ghost_honorary_root s; \<forall>x. (\<exists>xa. xa \<in> mut_roots s \<union> mut_ghost_honorary_root s \<union> tso_store_refs s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x) \<longrightarrow> black x s \<or> (\<exists>xa. grey xa s \<and> (xa has_white_path_to x) s)\<rbrakk> \<Longrightarrow> \<exists>g. grey g s \<and> (g has_white_path_to w) s
[PROOF STEP]
by auto


[STATEMENT]
lemma black_dequeue_Mark[simp]:
  "black b (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>))
\<longleftrightarrow> (black b s \<and> b \<noteq> r) \<or> (b = r \<and> fl = sys_fM s \<and> valid_ref r s \<and> \<not>grey r s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. black b (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>)) = (black b s \<and> b \<noteq> r \<or> b = r \<and> fl = sys_fM s \<and> obj_at (\<lambda>s. True) r s \<and> \<not> grey r s)
[PROOF STEP]
unfolding black_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (marked b (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>)) \<and> \<not> grey b (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>))) = ((marked b s \<and> \<not> grey b s) \<and> b \<noteq> r \<or> b = r \<and> fl = sys_fM s \<and> obj_at (\<lambda>s. True) r s \<and> \<not> grey r s)
[PROOF STEP]
by (auto simp: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma colours_sweep_loop_free[iff]:
  "black r (s(sys := s sys\<lparr>heap := (heap (s sys))(r' := None)\<rparr>)) \<longleftrightarrow> (black r s \<and> r \<noteq> r')"
  "grey r (s(sys := s sys\<lparr>heap := (heap (s sys))(r' := None)\<rparr>)) \<longleftrightarrow> (grey r s)"
  "white r (s(sys := s sys\<lparr>heap := (heap (s sys))(r' := None)\<rparr>)) \<longleftrightarrow> (white r s \<and> r \<noteq> r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. black r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) = (black r s \<and> r \<noteq> r') &&& grey r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) = grey r s &&& white r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) = (white r s \<and> r \<noteq> r')
[PROOF STEP]
unfolding black_def grey_def white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (marked r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) \<and> (\<nexists>x. r \<in> WL x (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)))) = ((marked r s \<and> (\<nexists>x. r \<in> WL x s)) \<and> r \<noteq> r') &&& (\<exists>x. r \<in> WL x (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>))) = (\<exists>x. r \<in> WL x s) &&& obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>))) r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) = (obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s \<and> r \<noteq> r')
[PROOF STEP]
by (auto simp: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma colours_get_work_done[simp]:
  "black r (s(mutator m := (s (mutator m))\<lparr>W := {}\<rparr>,
              sys := (s sys)\<lparr> hs_pending := hp', W := W (s sys) \<union> W (s (mutator m)),
                              ghost_hs_in_sync := his' \<rparr>)) \<longleftrightarrow> black r s"
  "grey r (s(mutator m := (s (mutator m))\<lparr>W := {}\<rparr>,
              sys := (s sys)\<lparr> hs_pending := hp', W := W (s sys) \<union> W (s (mutator m)),
                              ghost_hs_in_sync := his' \<rparr>)) \<longleftrightarrow> grey r s"
  "white r (s(mutator m := (s (mutator m))\<lparr>W := {}\<rparr>,
              sys := (s sys)\<lparr> hs_pending := hp', W := W (s sys) \<union> W (s (mutator m)),
                              ghost_hs_in_sync := his' \<rparr>)) \<longleftrightarrow> white r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. black r (s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = black r s &&& grey r (s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = grey r s &&& white r (s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = white r s
[PROOF STEP]
unfolding black_def grey_def WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (marked r (s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) \<and> (\<nexists>x. r \<in> W ((s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x) \<union> ghost_honorary_grey ((s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x))) = (marked r s \<and> (\<nexists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x))) &&& (\<exists>x. r \<in> W ((s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x) \<union> ghost_honorary_grey ((s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x)) = (\<exists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x)) &&& white r (s(mutator m := s (mutator m)\<lparr>W := {}\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = white r s
[PROOF STEP]
apply (simp_all add: fun_upd_apply split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>obj. sys_heap s r = Some obj \<longrightarrow> (obj_mark obj = sys_fM s \<and> (\<forall>x. (x = mutator m \<longrightarrow> r \<notin> ghost_honorary_grey (s (mutator m))) \<and> (x \<noteq> mutator m \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> W (s (mutator m)) \<and> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))))) = (obj_mark obj = sys_fM s \<and> (\<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x)))
 2. (\<exists>x. (x = mutator m \<longrightarrow> r \<in> ghost_honorary_grey (s (mutator m))) \<and> (x \<noteq> mutator m \<longrightarrow> (x = sys \<longrightarrow> r \<in> sys_W s \<or> r \<in> W (s (mutator m)) \<or> r \<in> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)))) = (\<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (x = mutator m \<longrightarrow> r \<in> ghost_honorary_grey (s (mutator m))) \<and> (x \<noteq> mutator m \<longrightarrow> (x = sys \<longrightarrow> r \<in> sys_W s \<or> r \<in> W (s (mutator m)) \<or> r \<in> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)))) = (\<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply (metis process_name.distinct(3))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma colours_get_roots_done[simp]:
  "black r (s(mutator m := (s (mutator m))\<lparr> W := {}, ghost_hs_phase := hs' \<rparr>,
              sys := (s sys)\<lparr> hs_pending := hp', W := W (s sys) \<union> W (s (mutator m)),
                              ghost_hs_in_sync := his' \<rparr>)) \<longleftrightarrow> black r s"
  "grey r (s(mutator m := (s (mutator m))\<lparr> W := {}, ghost_hs_phase := hs' \<rparr>,
              sys := (s sys)\<lparr> hs_pending := hp', W := W (s sys) \<union> W (s (mutator m)),
                              ghost_hs_in_sync := his' \<rparr>)) \<longleftrightarrow> grey r s"
  "white r (s(mutator m := (s (mutator m))\<lparr> W := {}, ghost_hs_phase := hs' \<rparr>,
              sys := (s sys)\<lparr> hs_pending := hp', W := W (s sys) \<union> W (s (mutator m)),
                              ghost_hs_in_sync := his' \<rparr>)) \<longleftrightarrow> white r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. black r (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = black r s &&& grey r (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = grey r s &&& white r (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = white r s
[PROOF STEP]
unfolding black_def grey_def WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (marked r (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) \<and> (\<nexists>x. r \<in> W ((s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x) \<union> ghost_honorary_grey ((s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x))) = (marked r s \<and> (\<nexists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x))) &&& (\<exists>x. r \<in> W ((s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x) \<union> ghost_honorary_grey ((s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) x)) = (\<exists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x)) &&& white r (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = white r s
[PROOF STEP]
apply (simp_all add: fun_upd_apply split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>obj. sys_heap s r = Some obj \<longrightarrow> (obj_mark obj = sys_fM s \<and> (\<forall>x. (x = mutator m \<longrightarrow> r \<notin> ghost_honorary_grey (s (mutator m))) \<and> (x \<noteq> mutator m \<longrightarrow> (x = sys \<longrightarrow> r \<notin> sys_W s \<and> r \<notin> W (s (mutator m)) \<and> r \<notin> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x))))) = (obj_mark obj = sys_fM s \<and> (\<forall>x. r \<notin> W (s x) \<and> r \<notin> ghost_honorary_grey (s x)))
 2. (\<exists>x. (x = mutator m \<longrightarrow> r \<in> ghost_honorary_grey (s (mutator m))) \<and> (x \<noteq> mutator m \<longrightarrow> (x = sys \<longrightarrow> r \<in> sys_W s \<or> r \<in> W (s (mutator m)) \<or> r \<in> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)))) = (\<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (x = mutator m \<longrightarrow> r \<in> ghost_honorary_grey (s (mutator m))) \<and> (x \<noteq> mutator m \<longrightarrow> (x = sys \<longrightarrow> r \<in> sys_W s \<or> r \<in> W (s (mutator m)) \<or> r \<in> sys_ghost_honorary_grey s) \<and> (x \<noteq> sys \<longrightarrow> r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)))) = (\<exists>x. r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply (metis process_name.distinct(3))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma colours_flip_fM[simp]:
  "fl \<noteq> sys_fM s \<Longrightarrow> black b (s(sys := (s sys)\<lparr>fM := fl, mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) \<longleftrightarrow> white b s \<and> \<not>grey b s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl \<noteq> sys_fM s \<Longrightarrow> black b (s(sys := s sys\<lparr>fM := fl, mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = (white b s \<and> \<not> grey b s)
[PROOF STEP]
unfolding black_def white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fl \<noteq> sys_fM s \<Longrightarrow> (marked b (s(sys := s sys\<lparr>fM := fl, mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) \<and> \<not> grey b (s(sys := s sys\<lparr>fM := fl, mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))) = (obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) b s \<and> \<not> grey b s)
[PROOF STEP]
by (simp add: fun_upd_apply)


[STATEMENT]
lemma colours_alloc[simp]:
  "heap (s sys) r' = None
     \<Longrightarrow> black r (s(mutator m := (s (mutator m))\<lparr> roots := roots' \<rparr>, sys := (s sys)\<lparr>heap := heap (s sys)(r' \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
     \<longleftrightarrow> black r s \<or> (r' = r \<and> fl = sys_fM s \<and> \<not>grey r' s)"
  "grey r (s(mutator m := (s (mutator m))\<lparr> roots := roots' \<rparr>, sys := (s sys)\<lparr>heap := heap (s sys)(r' \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
     \<longleftrightarrow> grey r s"
  "heap (s sys) r' = None
     \<Longrightarrow> white r (s(mutator m := (s (mutator m))\<lparr> roots := roots' \<rparr>, sys := (s sys)\<lparr>heap := heap (s sys)(r' \<mapsto> \<lparr>obj_mark = fl, obj_fields = Map.empty, obj_payload = Map.empty\<rparr>)\<rparr>))
     \<longleftrightarrow> white r s \<or> (r' = r \<and> fl \<noteq> sys_fM s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sys_heap s r' = None \<Longrightarrow> black r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = (black r s \<or> r' = r \<and> fl = sys_fM s \<and> \<not> grey r' s)) &&& grey r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = grey r s &&& (sys_heap s r' = None \<Longrightarrow> white r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = (white r s \<or> r' = r \<and> fl \<noteq> sys_fM s))
[PROOF STEP]
unfolding black_def white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sys_heap s r' = None \<Longrightarrow> (marked r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> \<not> grey r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>))) = (marked r s \<and> \<not> grey r s \<or> r' = r \<and> fl = sys_fM s \<and> \<not> grey r' s)) &&& grey r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = grey r s &&& (sys_heap s r' = None \<Longrightarrow> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>))) r (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = (obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s \<or> r' = r \<and> fl \<noteq> sys_fM s))
[PROOF STEP]
by (auto simp: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma heap_colours_alloc[simp]:
  "\<lbrakk> heap (s sys) r' = None; valid_refs_inv s \<rbrakk>
  \<Longrightarrow> black_heap (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> black_heap s \<and> fl = sys_fM s"
  "heap (s sys) r' = None
  \<Longrightarrow> white_heap (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> white_heap s \<and> fl \<noteq> sys_fM s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_heap s r' = None; valid_refs_inv s\<rbrakk> \<Longrightarrow> black_heap (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = (black_heap s \<and> fl = sys_fM s)) &&& (sys_heap s r' = None \<Longrightarrow> white_heap (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = (white_heap s \<and> fl \<noteq> sys_fM s))
[PROOF STEP]
unfolding black_heap_def white_def white_heap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_heap s r' = None; valid_refs_inv s\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>s. True) x (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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 := roots'\<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>))) = ((\<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> black x s) \<and> fl = sys_fM s)) &&& (sys_heap s r' = None \<Longrightarrow> (\<forall>x. obj_at (\<lambda>s. True) x (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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 (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>))) = ((\<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) x s) \<and> fl \<noteq> sys_fM s))
[PROOF STEP]
apply (simp_all add: fun_upd_apply split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sys_heap s r' = None; valid_refs_inv s\<rbrakk> \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))) = ((\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s)
 2. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s
 2. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; (\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))
 3. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply (intro allI conjI impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s)); \<exists>obj. sys_heap s x = Some obj\<rbrakk> \<Longrightarrow> black x s
 2. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))\<rbrakk> \<Longrightarrow> fl = sys_fM s
 3. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; (\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))
 4. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s)); \<exists>obj. sys_heap s x = Some obj\<rbrakk> \<Longrightarrow> black x s
 2. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))\<rbrakk> \<Longrightarrow> fl = sys_fM s
 3. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; (\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))
 4. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<exists>obj. sys_heap s x = Some obj; (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))\<rbrakk> \<Longrightarrow> black x s
 2. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))\<rbrakk> \<Longrightarrow> fl = sys_fM s
 3. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; (\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))
 4. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))\<rbrakk> \<Longrightarrow> fl = sys_fM s
 2. \<lbrakk>sys_heap s r' = None; valid_refs_inv s; (\<forall>x. (\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> black x s) \<and> fl = sys_fM s\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s) \<and> ((\<exists>obj. sys_heap s x = Some obj) \<longrightarrow> (black x s \<or> r' = x \<and> fl = sys_fM s \<and> \<not> grey r' s) \<and> (x = r' \<longrightarrow> black r' s \<or> fl = sys_fM s \<and> \<not> grey r' s))
 3. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply (drule spec[where x=r'], auto simp: reaches_def dest!: valid_refs_invD split: obj_at_splits)[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_heap s r' = None \<Longrightarrow> (\<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))) = ((\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))\<rbrakk> \<Longrightarrow> (\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s)
 2. \<lbrakk>sys_heap s r' = None; (\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s)\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))
[PROOF STEP]
apply (intro allI conjI impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x obj. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s))); sys_heap s x = Some obj\<rbrakk> \<Longrightarrow> obj_mark obj = (\<not> sys_fM s)
 2. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))\<rbrakk> \<Longrightarrow> fl = (\<not> sys_fM s)
 3. \<lbrakk>sys_heap s r' = None; (\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s)\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))
[PROOF STEP]
apply (rename_tac x obj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x obj. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s))); sys_heap s x = Some obj\<rbrakk> \<Longrightarrow> obj_mark obj = (\<not> sys_fM s)
 2. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))\<rbrakk> \<Longrightarrow> fl = (\<not> sys_fM s)
 3. \<lbrakk>sys_heap s r' = None; (\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s)\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x obj. \<lbrakk>sys_heap s r' = None; sys_heap s x = Some obj; (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))\<rbrakk> \<Longrightarrow> obj_mark obj = (\<not> sys_fM s)
 2. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))\<rbrakk> \<Longrightarrow> fl = (\<not> sys_fM s)
 3. \<lbrakk>sys_heap s r' = None; (\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s)\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sys_heap s r' = None; \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))\<rbrakk> \<Longrightarrow> fl = (\<not> sys_fM s)
 2. \<lbrakk>sys_heap s r' = None; (\<forall>x obj. sys_heap s x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s)) \<and> fl = (\<not> sys_fM s)\<rbrakk> \<Longrightarrow> \<forall>x. (sys_heap s x = None \<longrightarrow> x = r' \<longrightarrow> fl = (\<not> sys_fM s)) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (obj_mark obj = (\<not> sys_fM s) \<or> x = r' \<and> fl = (\<not> sys_fM s)) \<and> (x = r' \<longrightarrow> fl = (\<not> sys_fM s)))
[PROOF STEP]
apply (drule spec[where x=r'], auto dest!: valid_refs_invD split: obj_at_splits)[2]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma grey_protects_white_hs_done[simp]:
  "(g grey_protects_white w) (s(mutator m := s (mutator m)\<lparr> W := {}, ghost_hs_phase := hs' \<rparr>,
                              sys := s sys\<lparr> hs_pending := hp', W := sys_W s \<union> W (s (mutator m)),
                                            ghost_hs_in_sync := his' \<rparr>))
  \<longleftrightarrow> (g grey_protects_white w) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g grey_protects_white w) (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) = (g grey_protects_white w) s
[PROOF STEP]
unfolding grey_protects_white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (grey g (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>)) \<and> (g has_white_path_to w) (s(mutator m := s (mutator m)\<lparr>W := {}, ghost_hs_phase := hs'\<rparr>, sys := s sys\<lparr>hs_pending := hp', W := sys_W s \<union> W (s (mutator m)), ghost_hs_in_sync := his'\<rparr>))) = (grey g s \<and> (g has_white_path_to w) s)
[PROOF STEP]
by (simp add: fun_upd_apply)


[STATEMENT]
lemma grey_protects_white_alloc[simp]:
  "\<lbrakk> fl = sys_fM s; sys_heap s r = None \<rbrakk>
     \<Longrightarrow> (g grey_protects_white w) (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> (g grey_protects_white w) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fl = sys_fM s; sys_heap s r = None\<rbrakk> \<Longrightarrow> (g grey_protects_white w) (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)) = (g grey_protects_white w) s
[PROOF STEP]
unfolding grey_protects_white_def has_white_path_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fl = sys_fM s; sys_heap s r = None\<rbrakk> \<Longrightarrow> (grey g (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> (\<lambda>x y. (x points_to y) (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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> white y (s(mutator m := s (mutator m)\<lparr>roots := roots'\<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>)))\<^sup>*\<^sup>* g w) = (grey g s \<and> (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* g w)
[PROOF STEP]
by simp