[STATEMENT]
lemma has_white_path_to_induct[consumes 1, case_names refl step, induct set: has_white_path_to]:
  assumes "(x has_white_path_to y) s"
  assumes "\<And>x. P x x"
  assumes "\<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z"
  shows "P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x has_white_path_to y) s
P ?x ?x
\<lbrakk>(?x has_white_path_to ?y) s; P ?x ?y; (?y points_to ?z) s; white ?z s\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P x y
[PROOF STEP]
unfolding has_white_path_to_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x y
P ?x ?x
\<lbrakk>(\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* ?x ?y; P ?x ?y; (?y points_to ?z) s; white ?z s\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P x y
[PROOF STEP]
by (rule rtranclp.induct; blast)


[STATEMENT]
lemma has_white_path_toD[dest]:
  "(x has_white_path_to y) s \<Longrightarrow> white y s \<or> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x has_white_path_to y) s \<Longrightarrow> white y s \<or> x = y
[PROOF STEP]
unfolding has_white_path_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x y \<Longrightarrow> white y s \<or> x = y
[PROOF STEP]
by (fastforce elim: rtranclp.cases)


[STATEMENT]
lemma has_white_path_to_refl[iff]:
  "(x has_white_path_to x) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x has_white_path_to x) s
[PROOF STEP]
unfolding has_white_path_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x x
[PROOF STEP]
by simp


[STATEMENT]
lemma has_white_path_to_step[intro]:
  "\<lbrakk>(x has_white_path_to y) s; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s"
  "\<lbrakk>(y has_white_path_to z) s; (x points_to y) s; white y s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(x has_white_path_to y) s; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s) &&& (\<lbrakk>(y has_white_path_to z) s; (x points_to y) s; white y s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s)
[PROOF STEP]
unfolding has_white_path_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x z) &&& (\<lbrakk>(\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* y z; (x points_to y) s; white y s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x z)
[PROOF STEP]
apply (simp add: rtranclp.rtrancl_into_rtrancl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* y z; (x points_to y) s; white y s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x z
[PROOF STEP]
apply (simp add: converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma has_white_path_toE[elim!]:
  "\<lbrakk> (x points_to y) s; white y s \<rbrakk> \<Longrightarrow> (x has_white_path_to y) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x points_to y) s; white y s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
[PROOF STEP]
unfolding has_white_path_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x points_to y) s; white y s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x y
[PROOF STEP]
by (auto elim: rtranclp.intros(2))


[STATEMENT]
lemma has_white_path_to_reaches[elim]:
  "(x has_white_path_to y) s \<Longrightarrow> (x reaches y) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x has_white_path_to y) s \<Longrightarrow> (x reaches y) s
[PROOF STEP]
unfolding has_white_path_to_def reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x y \<Longrightarrow> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
by (induct rule: rtranclp.induct) (auto intro: rtranclp.intros(2))


[STATEMENT]
lemma has_white_path_to_blacken[simp]:
  "(x has_white_path_to w) (s(gc := s gc\<lparr> W := gc_W s - rs \<rparr>)) \<longleftrightarrow> (x has_white_path_to w) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x has_white_path_to w) (s(gc := s gc\<lparr>W := gc_W s - rs\<rparr>)) = (x has_white_path_to w) s
[PROOF STEP]
unfolding has_white_path_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. (x points_to y) (s(gc := s gc\<lparr>W := gc_W s - rs\<rparr>)) \<and> white y (s(gc := s gc\<lparr>W := gc_W s - rs\<rparr>)))\<^sup>*\<^sup>* x w = (\<lambda>x y. (x points_to y) s \<and> white y s)\<^sup>*\<^sup>* x w
[PROOF STEP]
by (simp add: fun_upd_apply)


[STATEMENT]
lemma has_white_path_to_eq_imp': \<comment> \<open>Complicated condition takes care of \<open>alloc\<close>: collapses no object and object with no fields\<close>
  assumes "(x has_white_path_to y) s'"
  assumes "\<forall>r'. \<Union>(ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union>(ran ` obj_fields ` set_option (sys_heap s r'))"
  assumes "\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')"
  assumes "sys_fM s' = sys_fM s"
  shows "(x has_white_path_to y) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x has_white_path_to y) s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x has_white_path_to y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')
sys_fM s' = sys_fM s

goal (1 subgoal):
 1. (x has_white_path_to y) s
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to x) s
 2. \<And>x y z. \<lbrakk>(x has_white_path_to y) s'; \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s; (y points_to z) s'; white z s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s
[PROOF STEP]
case (step x y z)
[PROOF STATE]
proof (state)
this:
(x has_white_path_to y) s'
\<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
(y points_to z) s'
white z s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')
sys_fM s' = sys_fM s

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to x) s
 2. \<And>x y z. \<lbrakk>(x has_white_path_to y) s'; \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s; (y points_to z) s'; white z s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x has_white_path_to y) s'
\<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
(y points_to z) s'
white z s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')
sys_fM s' = sys_fM s
[PROOF STEP]
have "(y points_to z) s"
[PROOF STATE]
proof (prove)
using this:
(x has_white_path_to y) s'
\<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
(y points_to z) s'
white z s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')
sys_fM s' = sys_fM s

goal (1 subgoal):
 1. (y points_to z) s
[PROOF STEP]
by (cases "sys_heap s y")
       (auto 10 10 simp: ran_def obj_at_def split: option.splits dest!: spec[where x=y])
[PROOF STATE]
proof (state)
this:
(y points_to z) s

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to x) s
 2. \<And>x y z. \<lbrakk>(x has_white_path_to y) s'; \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s; (y points_to z) s'; white z s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
(x has_white_path_to y) s'
\<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
(y points_to z) s'
white z s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')
sys_fM s' = sys_fM s
(y points_to z) s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x has_white_path_to y) s'
\<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
(y points_to z) s'
white z s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
\<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r')
sys_fM s' = sys_fM s
(y points_to z) s

goal (1 subgoal):
 1. (x has_white_path_to z) s
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x has_white_path_to y) s'; \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s; (y points_to z) s'; white z s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s; (y points_to z) s\<rbrakk> \<Longrightarrow> (x has_white_path_to z) s
[PROOF STEP]
apply (rule has_white_path_to_step, assumption, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x has_white_path_to y) s'; \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s; (y points_to z) s'; white z s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s; (y points_to z) s\<rbrakk> \<Longrightarrow> white z s
[PROOF STEP]
apply (clarsimp simp: white_def split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>obj obja objb. \<lbrakk>(x has_white_path_to y) s'; (x has_white_path_to y) s; sys_heap s' y = Some obj; z \<in> ran (obj_fields obj); sys_heap s' z = Some obja; obj_mark obja = (\<not> sys_fM s); \<forall>r'. (\<Union>a\<in>set_option (sys_heap s' r'). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s r'). ran (obj_fields a)); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s; sys_heap s y = Some objb; z \<in> ran (obj_fields objb)\<rbrakk> \<Longrightarrow> (\<exists>y. sys_heap s z = Some y) \<and> (\<forall>obj. sys_heap s z = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s))
[PROOF STEP]
apply (metis map_option_eq_Some option.sel)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(x has_white_path_to z) s

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')); \<forall>r'. map_option obj_mark (sys_heap s' r') = map_option obj_mark (sys_heap s r'); sys_fM s' = sys_fM s\<rbrakk> \<Longrightarrow> (x has_white_path_to x) s
[PROOF STEP]
qed simp


[STATEMENT]
lemma has_white_path_to_eq_imp:
  "eq_imp (\<lambda>r'. sys_fM \<^bold>\<otimes> (\<lambda>s. \<Union>(ran ` obj_fields ` set_option (sys_heap s r'))) \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')))
          (x has_white_path_to y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (sys_fM s, \<Union> (ran ` obj_fields ` set_option (sys_heap s r')), map_option obj_mark (sys_heap s r'))) (x has_white_path_to y)
[PROOF STEP]
unfolding eq_imp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (sys_fM s, \<Union> (ran ` obj_fields ` set_option (sys_heap s x)), map_option obj_mark (sys_heap s x)) = (sys_fM s', \<Union> (ran ` obj_fields ` set_option (sys_heap s' x)), map_option obj_mark (sys_heap s' x))) \<longrightarrow> (x has_white_path_to y) s = (x has_white_path_to y) s'
[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. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s = (x has_white_path_to y) s'
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); (x has_white_path_to y) s\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s'
 2. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); (x has_white_path_to y) s'\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
[PROOF STEP]
apply (erule has_white_path_to_eq_imp'; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); (x has_white_path_to y) s'\<rbrakk> \<Longrightarrow> (x has_white_path_to y) s
[PROOF STEP]
apply (erule has_white_path_to_eq_imp'; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma grey_protects_whiteD[dest]:
  "(g grey_protects_white w) s \<Longrightarrow> grey g s \<and> (g = w \<or> white w s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g grey_protects_white w) s \<Longrightarrow> grey g s \<and> (g = w \<or> white w s)
[PROOF STEP]
by (auto simp: grey_protects_white_def)


[STATEMENT]
lemma grey_protects_whiteI[iff]:
  "grey g s \<Longrightarrow> (g grey_protects_white g) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grey g s \<Longrightarrow> (g grey_protects_white g) s
[PROOF STEP]
by (simp add: grey_protects_white_def)


[STATEMENT]
lemma grey_protects_whiteE[elim!]:
  "\<lbrakk> (g points_to w) s; grey g s; white w s \<rbrakk> \<Longrightarrow> (g grey_protects_white w) s"
  "\<lbrakk> (g grey_protects_white y) s; (y points_to w) s; white w s \<rbrakk> \<Longrightarrow> (g grey_protects_white w) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(g points_to w) s; grey g s; white w s\<rbrakk> \<Longrightarrow> (g grey_protects_white w) s) &&& (\<lbrakk>(g grey_protects_white y) s; (y points_to w) s; white w s\<rbrakk> \<Longrightarrow> (g grey_protects_white w) s)
[PROOF STEP]
by (auto simp: grey_protects_white_def)


[STATEMENT]
lemma grey_protects_white_reaches[elim]:
  "(g grey_protects_white w) s \<Longrightarrow> (g reaches w) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g grey_protects_white w) s \<Longrightarrow> (g reaches w) s
[PROOF STEP]
by (auto simp: grey_protects_white_def)


[STATEMENT]
lemma grey_protects_white_induct[consumes 1, case_names refl step, induct set: grey_protects_white]:
  assumes "(g grey_protects_white w) s"
  assumes "\<And>x. grey x s \<Longrightarrow> P x x"
  assumes "\<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z"
  shows "P g w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P g w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(g grey_protects_white w) s
grey ?x s \<Longrightarrow> P ?x ?x
\<lbrakk>(?x has_white_path_to ?y) s; P ?x ?y; (?y points_to ?z) s; white ?z s\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P g w
[PROOF STEP]
unfolding grey_protects_white_def
[PROOF STATE]
proof (prove)
using this:
grey g s \<and> (g has_white_path_to w) s
grey ?x s \<Longrightarrow> P ?x ?x
\<lbrakk>(?x has_white_path_to ?y) s; P ?x ?y; (?y points_to ?z) s; white ?z s\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P g w
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>grey g s \<and> (g has_white_path_to w) s; \<And>x. grey x s \<Longrightarrow> P x x; \<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z\<rbrakk> \<Longrightarrow> P g w
[PROOF STEP]
apply (elim conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. grey x s \<Longrightarrow> P x x; \<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z; grey g s; (g has_white_path_to w) s\<rbrakk> \<Longrightarrow> P g w
[PROOF STEP]
apply (rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(g has_white_path_to w) s; \<And>x. grey x s \<Longrightarrow> P x x; \<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z; grey g s\<rbrakk> \<Longrightarrow> P g w
[PROOF STEP]
apply (induct rule: has_white_path_to_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. grey x s \<Longrightarrow> P x x; \<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z; grey x s\<rbrakk> \<Longrightarrow> P x x
 2. \<And>x y z. \<lbrakk>(x has_white_path_to y) s; \<lbrakk>\<And>x. grey x s \<Longrightarrow> P x x; \<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z; grey x s\<rbrakk> \<Longrightarrow> P x y; (y points_to z) s; white z s; \<And>x. grey x s \<Longrightarrow> P x x; \<And>x y z. \<lbrakk>(x has_white_path_to y) s; P x y; (y points_to z) s; white z s\<rbrakk> \<Longrightarrow> P x z; grey x s\<rbrakk> \<Longrightarrow> P x z
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma valid_W_inv_sys_ghg_empty_iff[elim!]:
  "valid_W_inv s \<Longrightarrow> sys_ghost_honorary_grey s = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_W_inv s \<Longrightarrow> sys_ghost_honorary_grey s = {}
[PROOF STEP]
unfolding 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> sys_ghost_honorary_grey s = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma WLI[intro]:
  "r \<in> W (s p) \<Longrightarrow> r \<in> WL p s"
  "r \<in> ghost_honorary_grey (s p) \<Longrightarrow> r \<in> WL p s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> W (s p) \<Longrightarrow> r \<in> WL p s) &&& (r \<in> ghost_honorary_grey (s p) \<Longrightarrow> r \<in> WL p s)
[PROOF STEP]
unfolding WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> W (s p) \<Longrightarrow> r \<in> W (s p) \<union> ghost_honorary_grey (s p)) &&& (r \<in> ghost_honorary_grey (s p) \<Longrightarrow> r \<in> W (s p) \<union> ghost_honorary_grey (s p))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma WL_eq_imp:
  "eq_imp (\<lambda>(_::unit) s. (ghost_honorary_grey (s p), W (s p)))
          (WL p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. (ghost_honorary_grey (s p), W (s p))) (WL p)
[PROOF STEP]
unfolding eq_imp_def WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (ghost_honorary_grey (s p), W (s p)) = (ghost_honorary_grey (s' p), W (s' p))) \<longrightarrow> W (s p) \<union> ghost_honorary_grey (s p) = W (s' p) \<union> ghost_honorary_grey (s' p)
[PROOF STEP]
by simp


[STATEMENT]
lemma valid_W_inv_eq_imp:
  "eq_imp (\<lambda>(p, r). (\<lambda>s. W (s p)) \<^bold>\<otimes> (\<lambda>s. ghost_honorary_grey (s p)) \<^bold>\<otimes> sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r)) \<^bold>\<otimes> sys_mem_lock \<^bold>\<otimes> tso_pending_mark p)
          valid_W_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>(p, r) s. (W (s p), ghost_honorary_grey (s p), sys_fM s, map_option obj_mark (sys_heap s r), sys_mem_lock s, filter is_mw_Mark (sys_mem_store_buffers p s))) valid_W_inv
[PROOF STEP]
apply (clarsimp simp: eq_imp_def valid_W_inv_def fun_eq_iff all_conj_distrib white_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. sys_mem_lock s' \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb])) = ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> marked xa s') \<and> (\<forall>x xa. 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. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s' \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb]))
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. sys_mem_lock s' \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb])) = ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> marked xa s') \<and> (\<forall>x xa. 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. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s' \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb]))
[PROOF STEP]
apply (subgoal_tac "\<forall>p. WL p s = WL p s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. sys_mem_lock s' \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb])) = ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> marked xa s') \<and> (\<forall>x xa. 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. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s' \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb]))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (subgoal_tac "\<forall>x. marked x s \<longleftrightarrow> marked x s'")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. sys_mem_lock s' \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb])) = ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> marked xa s') \<and> (\<forall>x xa. 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. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s' \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb]))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (subgoal_tac "\<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not>sys_fM s')) x s \<longleftrightarrow> obj_at (\<lambda>obj. obj_mark obj = (\<not>sys_fM s')) x s'")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'\<rbrakk> \<Longrightarrow> ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. sys_mem_lock s' \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb])) = ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> marked xa s') \<and> (\<forall>x xa. 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. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s' \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb]))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 4. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (subgoal_tac "\<forall>x xa xb. mw_Mark xa xb \<in> set (sys_mem_store_buffers x s) \<longleftrightarrow> mw_Mark xa xb \<in> set (sys_mem_store_buffers x s')")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'; \<forall>x xa xb. (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s)) = (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. sys_mem_lock s' \<noteq> Some x \<and> xa \<in> ghost_honorary_grey (s' x) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') xa s) \<and> (\<forall>x xa. x \<noteq> xa \<longrightarrow> WL x s \<inter> WL xa s = {}) \<and> (\<forall>x xa xb. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb])) = ((\<forall>x xa. xa \<in> W (s' x) \<longrightarrow> marked xa s') \<and> (\<forall>x xa. 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. xb \<in> ghost_honorary_grey (s' x) \<longrightarrow> xb \<notin> 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> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) xa s' \<and> filter is_mw_Mark (sys_mem_store_buffers x s') = [mw_Mark xa xb]))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'\<rbrakk> \<Longrightarrow> \<forall>x xa xb. (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s)) = (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s'))
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'
 4. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 5. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (simp; fail)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'\<rbrakk> \<Longrightarrow> \<forall>x xa xb. (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s)) = (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 4. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s' x xa xb. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'\<rbrakk> \<Longrightarrow> (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s)) = (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 4. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (rename_tac x xa xb)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s' x xa xb. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'\<rbrakk> \<Longrightarrow> (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s)) = (mw_Mark xa xb \<in> set (sys_mem_store_buffers x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 4. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (drule_tac x=x in spec, drule arg_cong[where f=set], fastforce)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s = obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s')) x s'
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s x = Some y) \<or> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> ((\<exists>y. sys_heap s' x = Some y) \<or> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s'))); \<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = sys_fM s')) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = sys_fM s') \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = (\<not> sys_fM s')) = (obj_mark obja = (\<not> sys_fM s'))))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s x = Some y) \<or> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> ((\<exists>y. sys_heap s' x = Some y) \<or> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s'))); \<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = sys_fM s')) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = sys_fM s') \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = (\<not> sys_fM s')) = (obj_mark obja = (\<not> sys_fM s'))))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply ( (drule_tac x=x in spec)+ )[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; ((\<exists>y. sys_heap s x = Some y) \<or> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> ((\<exists>y. sys_heap s' x = Some y) \<or> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s'))); map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = sys_fM s')) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = sys_fM s') \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = (\<not> sys_fM s')) = (obj_mark obja = (\<not> sys_fM s'))))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (case_tac "sys_heap s x", simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' x a. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; ((\<exists>y. sys_heap s' x = Some y) \<or> obj_mark a = (\<not> sys_fM s')) \<and> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> (obj_mark a = sys_fM s') = (obj_mark obj = sys_fM s')); Some (obj_mark a) = map_option obj_mark (sys_heap s' x); sys_heap s x = Some a\<rbrakk> \<Longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark a = sys_fM s') \<and> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> (obj_mark a = (\<not> sys_fM s')) = (obj_mark obj = (\<not> sys_fM s')))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
 3. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (case_tac "sys_heap s' x", auto)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (case_tac "sys_heap s x", simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x a. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s'); \<forall>p. WL p s = WL p s'; Some (obj_mark a) = map_option obj_mark (sys_heap s' x); sys_heap s x = Some a\<rbrakk> \<Longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark a = (\<not> sys_fM s')) \<and> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> (obj_mark a = sys_fM s') = (obj_mark obj = sys_fM s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (case_tac "sys_heap s' x", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>a. W (s a) = W (s' a); \<forall>a. ghost_honorary_grey (s a) = ghost_honorary_grey (s' a); sys_fM s = sys_fM s'; \<forall>b. map_option obj_mark (sys_heap s b) = map_option obj_mark (sys_heap s' b); sys_mem_lock s = sys_mem_lock s'; \<forall>a. filter is_mw_Mark (sys_mem_store_buffers a s) = filter is_mw_Mark (sys_mem_store_buffers a s')\<rbrakk> \<Longrightarrow> \<forall>p. WL p s = WL p s'
[PROOF STEP]
apply (simp add: WL_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma valid_W_invE[elim!]:
  "\<lbrakk> r \<in> W (s p); valid_W_inv s \<rbrakk> \<Longrightarrow> marked r s"
  "\<lbrakk> r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; valid_W_inv s \<rbrakk> \<Longrightarrow> marked r s"
  "\<lbrakk> r \<in> W (s p); valid_W_inv s \<rbrakk> \<Longrightarrow> valid_ref r s"
  "\<lbrakk> r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; valid_W_inv s \<rbrakk> \<Longrightarrow> valid_ref r s"
  "\<lbrakk> mw_Mark r fl \<in> set (sys_mem_store_buffers p s); valid_W_inv s \<rbrakk> \<Longrightarrow> r \<in> ghost_honorary_grey (s p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>r \<in> W (s p); valid_W_inv s\<rbrakk> \<Longrightarrow> marked r s) &&& (\<lbrakk>r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> marked r s)) &&& (\<lbrakk>r \<in> W (s p); valid_W_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) r s) &&& (\<lbrakk>r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) r s) &&& (\<lbrakk>mw_Mark r fl \<in> set (sys_mem_store_buffers p s); valid_W_inv s\<rbrakk> \<Longrightarrow> r \<in> ghost_honorary_grey (s p))
[PROOF STEP]
unfolding valid_W_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>r \<in> W (s p); (\<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> marked r s) &&& (\<lbrakk>r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; (\<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> marked r s)) &&& (\<lbrakk>r \<in> W (s p); (\<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> obj_at (\<lambda>s. True) r s) &&& (\<lbrakk>r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; (\<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> obj_at (\<lambda>s. True) r s) &&& (\<lbrakk>mw_Mark r fl \<in> set (sys_mem_store_buffers p 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> r \<in> ghost_honorary_grey (s p))
[PROOF STEP]
apply (simp_all add:  split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>r \<in> W (s p); \<forall>x xa. ((\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x) \<and> (sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x))) \<and> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> (xa \<in> W (s x) \<longrightarrow> obj_mark obj = sys_fM s) \<and> (xa \<in> ghost_honorary_grey (s x) \<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]\<rbrakk> \<Longrightarrow> \<exists>y. sys_heap s r = Some y
 2. \<lbrakk>r \<in> ghost_honorary_grey (s p); sys_mem_lock s \<noteq> Some p; \<forall>x xa. ((\<exists>y. sys_heap s xa = Some y) \<or> xa \<notin> W (s x) \<and> (sys_mem_lock s = Some x \<or> xa \<notin> ghost_honorary_grey (s x))) \<and> (\<forall>obj. sys_heap s xa = Some obj \<longrightarrow> (xa \<in> W (s x) \<longrightarrow> obj_mark obj = sys_fM s) \<and> (xa \<in> ghost_honorary_grey (s x) \<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]\<rbrakk> \<Longrightarrow> \<exists>y. sys_heap s r = Some y
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma valid_W_invD:
  "\<lbrakk> sys_mem_store_buffers p s = mw_Mark r fl # ws; valid_W_inv s \<rbrakk>
     \<Longrightarrow> fl = sys_fM s \<and> r \<in> ghost_honorary_grey (s p) \<and> tso_locked_by p s \<and> white r s \<and> filter is_mw_Mark ws = []"
  "\<lbrakk> mw_Mark r fl \<in> set (sys_mem_store_buffers p s); valid_W_inv s \<rbrakk>
     \<Longrightarrow> fl = sys_fM s \<and> r \<in> ghost_honorary_grey (s p) \<and> tso_locked_by p s \<and> white r s \<and> filter is_mw_Mark (sys_mem_store_buffers p s) = [mw_Mark r fl]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_mem_store_buffers p s = mw_Mark r fl # ws; valid_W_inv s\<rbrakk> \<Longrightarrow> fl = sys_fM s \<and> r \<in> ghost_honorary_grey (s p) \<and> sys_mem_lock s = Some p \<and> white r s \<and> filter is_mw_Mark ws = []) &&& (\<lbrakk>mw_Mark r fl \<in> set (sys_mem_store_buffers p s); valid_W_inv s\<rbrakk> \<Longrightarrow> fl = sys_fM s \<and> r \<in> ghost_honorary_grey (s p) \<and> sys_mem_lock s = Some p \<and> white r s \<and> filter is_mw_Mark (sys_mem_store_buffers p s) = [mw_Mark r fl])
[PROOF STEP]
unfolding valid_W_inv_def white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_mem_store_buffers p s = mw_Mark r fl # ws; (\<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> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb])\<rbrakk> \<Longrightarrow> fl = sys_fM s \<and> r \<in> ghost_honorary_grey (s p) \<and> sys_mem_lock s = Some p \<and> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s \<and> filter is_mw_Mark ws = []) &&& (\<lbrakk>mw_Mark r fl \<in> set (sys_mem_store_buffers p 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> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) xa s \<and> filter is_mw_Mark (sys_mem_store_buffers x s) = [mw_Mark xa xb])\<rbrakk> \<Longrightarrow> fl = sys_fM s \<and> r \<in> ghost_honorary_grey (s p) \<and> sys_mem_lock s = Some p \<and> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s \<and> filter is_mw_Mark (sys_mem_store_buffers p s) = [mw_Mark r fl])
[PROOF STEP]
by (clarsimp dest!: spec[where x=p], blast)+


[STATEMENT]
lemma valid_W_inv_colours:
  "\<lbrakk>white x s; valid_W_inv s\<rbrakk> \<Longrightarrow> x \<notin> W (s p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>white x s; valid_W_inv s\<rbrakk> \<Longrightarrow> x \<notin> W (s p)
[PROOF STEP]
using marked_not_white valid_W_invE(1)
[PROOF STATE]
proof (prove)
using this:
white ?r ?s \<Longrightarrow> \<not> marked ?r ?s
\<lbrakk>?r \<in> W (?s ?p); valid_W_inv ?s\<rbrakk> \<Longrightarrow> marked ?r ?s

goal (1 subgoal):
 1. \<lbrakk>white x s; valid_W_inv s\<rbrakk> \<Longrightarrow> x \<notin> W (s p)
[PROOF STEP]
by force


[STATEMENT]
lemma valid_W_inv_no_mark_stores_invD:
  "\<lbrakk> sys_mem_lock s \<noteq> Some p; valid_W_inv s \<rbrakk>
     \<Longrightarrow> tso_pending p is_mw_Mark s = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> filter is_mw_Mark (sys_mem_store_buffers p s) = []
[PROOF STEP]
by (auto dest: valid_W_invD(2) intro!: filter_False)


[STATEMENT]
lemma valid_W_inv_sys_load[simp]:
  "\<lbrakk> sys_mem_lock s \<noteq> Some p; valid_W_inv s \<rbrakk>
     \<Longrightarrow> sys_load p (mr_Mark r) (s sys) = mv_Mark (map_option obj_mark (sys_heap s r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> sys_load p (mr_Mark r) (s sys) = mv_Mark (map_option obj_mark (sys_heap s r))
[PROOF STEP]
unfolding sys_load_def fold_stores_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> (do_load_action (mr_Mark r) \<circ> (\<lambda>s. fold (\<lambda>w. (\<circ>) (do_store_action w)) (mem_store_buffers s p) id s)) (s sys) = mv_Mark (map_option obj_mark (sys_heap s r))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> map_option obj_mark (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers p s) id (s sys)) r) = map_option obj_mark (sys_heap s r)
[PROOF STEP]
apply (rule fold_invariant[where P="\<lambda>fr. map_option obj_mark (heap (fr (s sys)) r) = map_option obj_mark (sys_heap s r)"
                             and Q="\<lambda>w. \<forall>r fl. w \<noteq> mw_Mark r fl"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s; x \<in> set (sys_mem_store_buffers p s)\<rbrakk> \<Longrightarrow> \<forall>r fl. x \<noteq> mw_Mark r fl
 2. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s\<rbrakk> \<Longrightarrow> map_option obj_mark (heap (id (s sys)) r) = map_option obj_mark (sys_heap s r)
 3. \<And>x sa. \<lbrakk>sys_mem_lock s \<noteq> Some p; valid_W_inv s; \<forall>r fl. x \<noteq> mw_Mark r fl; map_option obj_mark (heap (sa (s sys)) r) = map_option obj_mark (sys_heap s r)\<rbrakk> \<Longrightarrow> map_option obj_mark (heap ((do_store_action x \<circ> sa) (s sys)) r) = map_option obj_mark (sys_heap s r)
[PROOF STEP]
apply (auto simp: map_option_case do_store_action_def filter_empty_conv fun_upd_apply
              dest: valid_W_invD(2)
             split: mem_store_action.splits option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma grey_reachable_eq_imp:
  "eq_imp (\<lambda>r'. (\<lambda>s. \<Union>p. WL p s) \<^bold>\<otimes> (\<lambda>s. Set.bind (Option.set_option (sys_heap s r')) (ran \<circ> obj_fields)))
          (grey_reachable r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (\<Union>p. WL p s, Set.bind (set_option (sys_heap s r')) (ran \<circ> obj_fields))) (grey_reachable r)
[PROOF STEP]
by (auto simp: eq_imp_def grey_reachable_def grey_def set_eq_iff reaches_fields)


[STATEMENT]
lemma grey_reachableI[intro]:
  "grey g s \<Longrightarrow> grey_reachable g s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grey g s \<Longrightarrow> grey_reachable g s
[PROOF STEP]
unfolding grey_reachable_def reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grey g s \<Longrightarrow> \<exists>x. grey x s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x g
[PROOF STEP]
by blast


[STATEMENT]
lemma grey_reachableE:
  "\<lbrakk> (g points_to y) s; grey_reachable g s \<rbrakk> \<Longrightarrow> grey_reachable y s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(g points_to y) s; grey_reachable g s\<rbrakk> \<Longrightarrow> grey_reachable y s
[PROOF STEP]
unfolding grey_reachable_def reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(g points_to y) s; \<exists>x. grey x s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x g\<rbrakk> \<Longrightarrow> \<exists>x. grey x s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
[PROOF STEP]
by (auto elim: rtranclp.intros(2))


[STATEMENT]
lemma valid_refs_invI:
  "\<lbrakk> \<And>m x y. \<lbrakk> (x reaches y) s; mut_m.root m x s \<or> grey x s \<rbrakk> \<Longrightarrow> valid_ref y s
   \<rbrakk> \<Longrightarrow> valid_refs_inv s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m x y. \<lbrakk>(x reaches y) s; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<or> grey x s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y s) \<Longrightarrow> valid_refs_inv s
[PROOF STEP]
by (auto simp: valid_refs_inv_def mut_m.reachable_def grey_reachable_def)