[STATEMENT]
lemma no_black_refs_eq_imp:
  "eq_imp (\<lambda>r'. (\<lambda>s. (\<Union>p. WL p s)) \<^bold>\<otimes> sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')))
          no_black_refs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (\<Union>p. WL p s, sys_fM s, map_option obj_mark (sys_heap s r'))) no_black_refs
[PROOF STEP]
apply (clarsimp simp add: eq_imp_def no_black_refs_def black_def grey_def all_conj_distrib fun_eq_iff set_eq_iff split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longrightarrow> (\<exists>xa. x \<in> WL xa s')) = (\<forall>x. marked x s' \<longrightarrow> (\<exists>xa. x \<in> WL xa s'))
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longrightarrow> (\<exists>xa. x \<in> WL xa s')) = (\<forall>x. marked x s' \<longrightarrow> (\<exists>xa. x \<in> WL xa s'))
[PROOF STEP]
apply (subgoal_tac "\<forall>x. marked x s \<longleftrightarrow> marked x s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); \<forall>x. marked x s = marked x s'\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longrightarrow> (\<exists>xa. x \<in> WL xa s')) = (\<forall>x. marked x s' \<longrightarrow> (\<exists>xa. x \<in> WL xa s'))
 2. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> \<forall>x. marked x s = marked x s'
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. 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')))
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>\<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. 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')))
[PROOF STEP]
apply (drule_tac x=x in spec)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>sys_fM s = sys_fM s'; (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa 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')))
[PROOF STEP]
apply (auto split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done