[STATEMENT]
lemma colours_blacken[simp]:
  "valid_W_inv s \<Longrightarrow> black b (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) \<longleftrightarrow> black b s \<or> (r \<in> gc_W s \<and> b = r)"
  "\<lbrakk> r \<in> gc_W s; valid_W_inv s \<rbrakk> \<Longrightarrow> grey g (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) \<longleftrightarrow> (grey g s \<and> g \<noteq> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (valid_W_inv s \<Longrightarrow> black b (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) = (black b s \<or> r \<in> gc_W s \<and> b = r)) &&& (\<lbrakk>r \<in> gc_W s; valid_W_inv s\<rbrakk> \<Longrightarrow> grey g (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) = (grey g s \<and> g \<noteq> r))
[PROOF STEP]
(*  "white w (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) \<longleftrightarrow> white w s" is redundant *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (valid_W_inv s \<Longrightarrow> black b (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) = (black b s \<or> r \<in> gc_W s \<and> b = r)) &&& (\<lbrakk>r \<in> gc_W s; valid_W_inv s\<rbrakk> \<Longrightarrow> grey g (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) = (grey g s \<and> g \<noteq> r))
[PROOF STEP]
unfolding black_def grey_def valid_W_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>x xa. xa \<in> W (s x) \<or> sys_mem_lock s \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s x) \<longrightarrow> marked xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. \<not> (xb \<in> ghost_honorary_grey (s x) \<and> xb \<in> W (s xa))) \<and> sys_ghost_honorary_grey s = {} \<and> (\<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]) \<Longrightarrow> (marked b (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)) \<and> (\<nexists>x. b \<in> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)))) = (marked b s \<and> (\<nexists>x. b \<in> WL x s) \<or> r \<in> gc_W s \<and> b = r)) &&& (\<lbrakk>r \<in> gc_W s; (\<forall>x xa. xa \<in> W (s x) \<or> sys_mem_lock s \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s x) \<longrightarrow> marked xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. \<not> (xb \<in> ghost_honorary_grey (s x) \<and> xb \<in> W (s xa))) \<and> sys_ghost_honorary_grey s = {} \<and> (\<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb])\<rbrakk> \<Longrightarrow> (\<exists>x. g \<in> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>))) = ((\<exists>x. g \<in> WL x s) \<and> g \<noteq> r))
[PROOF STEP]
apply (simp_all add: all_conj_distrib split: obj_at_splits if_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x)) \<and> (\<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s)); \<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s)\<rbrakk> \<Longrightarrow> (sys_heap s b = None \<longrightarrow> r \<in> gc_W s \<longrightarrow> b \<noteq> r) \<and> (\<forall>obj. sys_heap s b = Some obj \<longrightarrow> (obj_mark obj = sys_fM s \<and> (\<forall>x. b \<notin> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)))) = (obj_mark obj = sys_fM s \<and> (\<forall>x. b \<notin> WL x s) \<or> r \<in> gc_W s \<and> b = r))
 2. \<lbrakk>(\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x)) \<and> (\<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s)); \<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s)\<rbrakk> \<Longrightarrow> (\<exists>x. g \<in> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>))) = ((\<exists>x. g \<in> WL x s) \<and> g \<noteq> r)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = None; r \<in> gc_W s; b = r\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s b = Some obj; \<forall>x. b \<notin> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)); obj_mark obj; sys_fM s; r \<notin> gc_W s; b \<in> WL x s\<rbrakk> \<Longrightarrow> False
 3. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s b = Some obj; \<forall>x. b \<notin> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)); obj_mark obj; sys_fM s; b \<noteq> r; b \<in> WL x s\<rbrakk> \<Longrightarrow> False
 4. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s b = Some obj; \<forall>x. b \<notin> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)); \<not> obj_mark obj; \<not> sys_fM s; r \<notin> gc_W s; b \<in> WL x s\<rbrakk> \<Longrightarrow> False
 5. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s b = Some obj; \<forall>x. b \<notin> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>)); \<not> obj_mark obj; \<not> sys_fM s; b \<noteq> r; b \<in> WL x s\<rbrakk> \<Longrightarrow> False
 6. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s b = Some obj; \<forall>x. b \<notin> WL x s; obj_mark obj; sys_fM s; b \<in> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>))\<rbrakk> \<Longrightarrow> False
 7. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s b = Some obj; \<forall>x. b \<notin> WL x s; \<not> obj_mark obj; \<not> sys_fM s; b \<in> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>))\<rbrakk> \<Longrightarrow> False
 8. \<And>obj. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; obj_mark obj\<rbrakk> \<Longrightarrow> sys_fM s
 9. \<And>obj. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; sys_fM s\<rbrakk> \<Longrightarrow> obj_mark obj
 10. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; r \<in> WL x (s(gc := s gc\<lparr>W := gc_W s - {r}\<rparr>))\<rbrakk> \<Longrightarrow> False
A total of 13 subgoals...
[PROOF STEP]
apply (simp_all add: WL_def fun_upd_apply split: if_splits)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = None; r \<in> gc_W s; b = r\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x. \<lbrakk>\<forall>x. (x = gc \<longrightarrow> b \<notin> gc_W s \<and> b \<notin> gc_ghost_honorary_grey s) \<and> (x = gc \<or> b \<notin> W (s x) \<and> b \<notin> ghost_honorary_grey (s x)); obj_mark obj; sys_fM s; b \<noteq> r; b \<in> W (s x) \<or> b \<in> ghost_honorary_grey (s x); \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj); sys_heap s b = Some obj\<rbrakk> \<Longrightarrow> False
 3. \<And>obj x. \<lbrakk>\<forall>x. (x = gc \<longrightarrow> b \<notin> gc_W s \<and> b \<notin> gc_ghost_honorary_grey s) \<and> (x = gc \<or> b \<notin> W (s x) \<and> b \<notin> ghost_honorary_grey (s x)); \<not> obj_mark obj; \<not> sys_fM s; b \<noteq> r; b \<in> W (s x) \<or> b \<in> ghost_honorary_grey (s x); \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> \<not> xb \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> \<not> obj_mark obj); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> \<not> obj_mark obj); sys_heap s b = Some obj\<rbrakk> \<Longrightarrow> False
 4. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 5. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x = gc; g \<in> gc_W s \<and> g \<noteq> r \<or> g \<in> gc_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 6. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 7. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 8. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply (metis option.distinct(1))
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>obj x. \<lbrakk>\<forall>x. (x = gc \<longrightarrow> b \<notin> gc_W s \<and> b \<notin> gc_ghost_honorary_grey s) \<and> (x = gc \<or> b \<notin> W (s x) \<and> b \<notin> ghost_honorary_grey (s x)); obj_mark obj; sys_fM s; b \<noteq> r; b \<in> W (s x) \<or> b \<in> ghost_honorary_grey (s x); \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj); sys_heap s b = Some obj\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x. \<lbrakk>\<forall>x. (x = gc \<longrightarrow> b \<notin> gc_W s \<and> b \<notin> gc_ghost_honorary_grey s) \<and> (x = gc \<or> b \<notin> W (s x) \<and> b \<notin> ghost_honorary_grey (s x)); \<not> obj_mark obj; \<not> sys_fM s; b \<noteq> r; b \<in> W (s x) \<or> b \<in> ghost_honorary_grey (s x); \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> \<not> xb \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> \<not> obj_mark obj); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> \<not> obj_mark obj); sys_heap s b = Some obj\<rbrakk> \<Longrightarrow> False
 3. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x = gc; g \<in> gc_W s \<and> g \<noteq> r \<or> g \<in> gc_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 5. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 6. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 7. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>obj x. \<lbrakk>\<forall>x. (x = gc \<longrightarrow> b \<notin> gc_W s \<and> b \<notin> gc_ghost_honorary_grey s) \<and> (x = gc \<or> b \<notin> W (s x) \<and> b \<notin> ghost_honorary_grey (s x)); \<not> obj_mark obj; \<not> sys_fM s; b \<noteq> r; b \<in> W (s x) \<or> b \<in> ghost_honorary_grey (s x); \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> \<not> xb \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> \<not> obj_mark obj); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> \<not> obj_mark obj); sys_heap s b = Some obj\<rbrakk> \<Longrightarrow> False
 2. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x = gc; g \<in> gc_W s \<and> g \<noteq> r \<or> g \<in> gc_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 4. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 5. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 6. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>obj x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); sys_heap s r = Some obj; r \<in> gc_W s; b = r; x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x = gc; g \<in> gc_W s \<and> g \<noteq> r \<or> g \<in> gc_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 3. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 4. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 5. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x = gc; g \<in> gc_W s \<and> g \<noteq> r \<or> g \<in> gc_ghost_honorary_grey s\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 2. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 3. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)
 2. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>g = r; \<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); x \<noteq> gc; r \<in> W (s x) \<or> r \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x xa. x \<noteq> xa \<longrightarrow> (W (s x) \<union> ghost_honorary_grey (s x)) \<inter> (W (s xa) \<union> ghost_honorary_grey (s xa)) = {}; \<forall>x xa xb. xb \<in> ghost_honorary_grey (s x) \<longrightarrow> xb \<notin> W (s xa); sys_ghost_honorary_grey s = {}; \<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longrightarrow> xb = sys_fM s \<and> xa \<in> ghost_honorary_grey (s x) \<and> sys_mem_lock s = Some x \<and> white xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb]; r \<in> gc_W s; \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x); \<forall>x xa. xa \<in> W (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> obj_mark obj = sys_fM s); \<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x); \<forall>x xa. xa \<in> ghost_honorary_grey (s x) \<longrightarrow> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> sys_mem_lock s = Some x \<or> obj_mark obj = sys_fM s); g \<noteq> r; g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x)\<rbrakk> \<Longrightarrow> \<exists>x. (x = gc \<longrightarrow> g \<in> gc_W s \<or> g \<in> gc_ghost_honorary_grey s) \<and> (x \<noteq> gc \<longrightarrow> g \<in> W (s x) \<or> g \<in> ghost_honorary_grey (s x))
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma no_black_refs_alloc[simp]:
  "\<lbrakk> heap (s sys) r' = None; no_black_refs s \<rbrakk>
     \<Longrightarrow> no_black_refs (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> fl \<noteq> sys_fM s \<or> grey r' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_heap s r' = None; no_black_refs s\<rbrakk> \<Longrightarrow> no_black_refs (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>)) = (fl \<noteq> sys_fM s \<or> grey r' s)
[PROOF STEP]
unfolding no_black_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_heap s r' = None; \<forall>x. \<not> black x s\<rbrakk> \<Longrightarrow> (\<forall>x. \<not> 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>))) = (fl \<noteq> sys_fM s \<or> grey r' s)
[PROOF STEP]
by simp


[STATEMENT]
lemma no_black_refs_mo_co_mark[simp]:
  "\<lbrakk> ghost_honorary_grey (s p) = {}; white r s \<rbrakk>
     \<Longrightarrow> no_black_refs (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<longleftrightarrow> no_black_refs s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ghost_honorary_grey (s p) = {}; white r s\<rbrakk> \<Longrightarrow> no_black_refs (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) = no_black_refs s
[PROOF STEP]
unfolding no_black_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ghost_honorary_grey (s p) = {}; white r s\<rbrakk> \<Longrightarrow> (\<forall>x. \<not> black x (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))) = (\<forall>x. \<not> black x s)
[PROOF STEP]
by auto


[STATEMENT]
lemma grey_protects_white_mark[simp]:
  assumes ghg: "ghost_honorary_grey (s p) = {}"
  shows "(\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr> ghost_honorary_grey := {r} \<rparr>)))
      \<longleftrightarrow> (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))) = ((\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<Longrightarrow> (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s
 2. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))

goal (2 subgoals):
 1. \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<Longrightarrow> (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s
 2. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
obtain g where "(g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))"
[PROOF STATE]
proof (prove)
using this:
\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))

goal (1 subgoal):
 1. (\<And>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))

goal (2 subgoals):
 1. \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<Longrightarrow> (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s
 2. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
from this ghg
[PROOF STATE]
proof (chain)
picking this:
(g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
ghost_honorary_grey (s p) = {}
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
(g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
ghost_honorary_grey (s p) = {}

goal (1 subgoal):
 1. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s
[PROOF STEP]
by induct (auto simp: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
(\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s

goal (1 subgoal):
 1. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
(\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s

goal (1 subgoal):
 1. (\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
(\<exists>g'. (g' grey_protects_white w) s) \<or> (r has_white_path_to w) s

goal (1 subgoal):
 1. \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
proof(safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>g'. (g' grey_protects_white w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
 2. (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>g'. (g' grey_protects_white w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
 2. (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
assume "(g grey_protects_white w) s"
[PROOF STATE]
proof (state)
this:
(g grey_protects_white w) s

goal (2 subgoals):
 1. \<And>g'. (g' grey_protects_white w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
 2. (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
from this ghg
[PROOF STATE]
proof (chain)
picking this:
(g grey_protects_white w) s
ghost_honorary_grey (s p) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(g grey_protects_white w) s
ghost_honorary_grey (s p) = {}

goal (1 subgoal):
 1. \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>grey x s; ghost_honorary_grey (s p) = {}\<rbrakk> \<Longrightarrow> \<exists>g. (g grey_protects_white x) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
 2. \<And>x y z. \<lbrakk>(x has_white_path_to y) s; ghost_honorary_grey (s p) = {} \<Longrightarrow> \<exists>g. (g grey_protects_white y) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)); (y points_to z) s; white z s; ghost_honorary_grey (s p) = {}\<rbrakk> \<Longrightarrow> \<exists>g. (g grey_protects_white z) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x has_white_path_to y) s; ghost_honorary_grey (s p) = {} \<Longrightarrow> \<exists>g. (g grey_protects_white y) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)); (y points_to z) s; white z s; ghost_honorary_grey (s p) = {}\<rbrakk> \<Longrightarrow> \<exists>g. (g grey_protects_white z) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
unfolding grey_protects_white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x has_white_path_to y) s; ghost_honorary_grey (s p) = {} \<Longrightarrow> \<exists>g. grey g (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<and> (g has_white_path_to y) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)); (y points_to z) s; white z s; ghost_honorary_grey (s p) = {}\<rbrakk> \<Longrightarrow> \<exists>g. grey g (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<and> (g has_white_path_to z) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
apply (auto simp: fun_upd_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))

goal (1 subgoal):
 1. (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
assume "(r has_white_path_to w) s"
[PROOF STATE]
proof (state)
this:
(r has_white_path_to w) s

goal (1 subgoal):
 1. (r has_white_path_to w) s \<Longrightarrow> \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
with ghg
[PROOF STATE]
proof (chain)
picking this:
ghost_honorary_grey (s p) = {}
(r has_white_path_to w) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ghost_honorary_grey (s p) = {}
(r has_white_path_to w) s

goal (1 subgoal):
 1. \<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))
[PROOF STEP]
unfolding grey_protects_white_def has_white_path_to_def
[PROOF STATE]
proof (prove)
using this:
ghost_honorary_grey (s p) = {}
(\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* r w

goal (1 subgoal):
 1. \<exists>g. grey g (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<and> (\<lambda>x y. (x points_to y) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)) \<and> white y (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>)))\<^sup>*\<^sup>* g w
[PROOF STEP]
by (auto simp: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>g. (g grey_protects_white w) (s(p := s p\<lparr>ghost_honorary_grey := {r}\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed