[STATEMENT]
lemma tso_store_inv_sys_load_GC[simp]:
  assumes "tso_store_inv s"
  shows "sys_load gc (mr_Ref r f) (s sys) = mv_Ref (Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f))" (is "?lhs = mv_Ref ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_load gc (mr_Ref r f) (s sys) = mv_Ref (Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
tso_store_inv s

goal (1 subgoal):
 1. sys_load gc (mr_Ref r f) (s sys) = mv_Ref (Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f))
[PROOF STEP]
unfolding sys_load_def fold_stores_def
[PROOF STATE]
proof (prove)
using this:
tso_store_inv s

goal (1 subgoal):
 1. (do_load_action (mr_Ref r f) \<circ> (\<lambda>s. fold (\<lambda>w. (\<circ>) (do_store_action w)) (mem_store_buffers s gc) id s)) (s sys) = mv_Ref (Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tso_store_inv s \<Longrightarrow> Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers gc s) id (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)
[PROOF STEP]
apply (rule fold_invariant[where P="\<lambda>fr. Option.bind (heap (fr (s sys)) r) (\<lambda>obj. obj_fields obj f) = ?rhs"
                             and Q="\<lambda>w. \<forall>r f r'. w \<noteq> mw_Mutate r f r'"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>tso_store_inv s; x \<in> set (sys_mem_store_buffers gc s)\<rbrakk> \<Longrightarrow> \<forall>r f r'. x \<noteq> mw_Mutate r f r'
 2. tso_store_inv s \<Longrightarrow> Option.bind (heap (id (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)
 3. \<And>x sa. \<lbrakk>tso_store_inv s; \<forall>r f r'. x \<noteq> mw_Mutate r f r'; Option.bind (heap (sa (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)\<rbrakk> \<Longrightarrow> Option.bind (heap ((do_store_action x \<circ> sa) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)
[PROOF STEP]
apply (fastforce simp: tso_store_inv_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. tso_store_inv s \<Longrightarrow> Option.bind (heap (id (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)
 2. \<And>x sa. \<lbrakk>tso_store_inv s; \<forall>r f r'. x \<noteq> mw_Mutate r f r'; Option.bind (heap (sa (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)\<rbrakk> \<Longrightarrow> Option.bind (heap ((do_store_action x \<circ> sa) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Option.bind (sys_heap s r) (\<lambda>obj. obj_fields obj f)
[PROOF STEP]
apply (auto simp: do_store_action_def map_option_case fun_upd_apply
            split: mem_store_action.splits option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tso_no_pending_marksD[simp]:
  assumes "tso_pending_mark p s = []"
  shows "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. sys_load p (mr_Mark r) (s sys) = mv_Mark (map_option obj_mark (sys_heap s r))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
filter is_mw_Mark (sys_mem_store_buffers p s) = []

goal (1 subgoal):
 1. 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)
using this:
filter is_mw_Mark (sys_mem_store_buffers p s) = []

goal (1 subgoal):
 1. (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. filter is_mw_Mark (sys_mem_store_buffers p s) = [] \<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>fl. w \<noteq> mw_Mark r fl"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>filter is_mw_Mark (sys_mem_store_buffers p s) = []; x \<in> set (sys_mem_store_buffers p s)\<rbrakk> \<Longrightarrow> \<forall>fl. x \<noteq> mw_Mark r fl
 2. filter is_mw_Mark (sys_mem_store_buffers p s) = [] \<Longrightarrow> map_option obj_mark (heap (id (s sys)) r) = map_option obj_mark (sys_heap s r)
 3. \<And>x sa. \<lbrakk>filter is_mw_Mark (sys_mem_store_buffers p s) = []; \<forall>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
             split: mem_store_action.splits option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma no_pending_phase_sys_load[simp]:
  assumes "tso_pending_phase p s = []"
  shows "sys_load p mr_Phase (s sys) = mv_Phase (sys_phase s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_load p mr_Phase (s sys) = mv_Phase (sys_phase s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
filter is_mw_Phase (sys_mem_store_buffers p s) = []

goal (1 subgoal):
 1. sys_load p mr_Phase (s sys) = mv_Phase (sys_phase s)
[PROOF STEP]
apply (clarsimp simp: sys_load_def fold_stores_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter is_mw_Phase (sys_mem_store_buffers p s) = [] \<Longrightarrow> phase (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers p s) id (s sys)) = sys_phase s
[PROOF STEP]
apply (rule fold_invariant[where P="\<lambda>fr. phase (fr (s sys)) = sys_phase s" and Q="\<lambda>w. \<forall>ph. w \<noteq> mw_Phase ph"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>filter is_mw_Phase (sys_mem_store_buffers p s) = []; x \<in> set (sys_mem_store_buffers p s)\<rbrakk> \<Longrightarrow> \<forall>ph. x \<noteq> mw_Phase ph
 2. filter is_mw_Phase (sys_mem_store_buffers p s) = [] \<Longrightarrow> phase (id (s sys)) = sys_phase s
 3. \<And>x sa. \<lbrakk>filter is_mw_Phase (sys_mem_store_buffers p s) = []; \<forall>ph. x \<noteq> mw_Phase ph; phase (sa (s sys)) = sys_phase s\<rbrakk> \<Longrightarrow> phase ((do_store_action x \<circ> sa) (s sys)) = sys_phase s
[PROOF STEP]
apply (auto simp: do_store_action_def filter_empty_conv
             split: mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gc_no_pending_fM_write[simp]:
  assumes "tso_pending_fM gc s = []"
  shows "sys_load gc mr_fM (s sys) = mv_Mark (Some (sys_fM s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_load gc mr_fM (s sys) = mv_Mark (Some (sys_fM s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
filter is_mw_fM (sys_mem_store_buffers gc s) = []

goal (1 subgoal):
 1. sys_load gc mr_fM (s sys) = mv_Mark (Some (sys_fM s))
[PROOF STEP]
apply (clarsimp simp: sys_load_def fold_stores_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter is_mw_fM (sys_mem_store_buffers gc s) = [] \<Longrightarrow> fM (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers gc s) id (s sys)) = sys_fM s
[PROOF STEP]
apply (rule fold_invariant[where P="\<lambda>fr. fM (fr (s sys)) = sys_fM s" and Q="\<lambda>w. \<forall>fl. w \<noteq> mw_fM fl"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>filter is_mw_fM (sys_mem_store_buffers gc s) = []; x \<in> set (sys_mem_store_buffers gc s)\<rbrakk> \<Longrightarrow> \<forall>fl. x \<noteq> mw_fM fl
 2. filter is_mw_fM (sys_mem_store_buffers gc s) = [] \<Longrightarrow> fM (id (s sys)) = sys_fM s
 3. \<And>x sa. \<lbrakk>filter is_mw_fM (sys_mem_store_buffers gc s) = []; \<forall>fl. x \<noteq> mw_fM fl; fM (sa (s sys)) = sys_fM s\<rbrakk> \<Longrightarrow> fM ((do_store_action x \<circ> sa) (s sys)) = sys_fM s
[PROOF STEP]
apply (auto simp: do_store_action_def filter_empty_conv
             split: mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tso_store_refs_simps[simp]:
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := roots'\<rparr>))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>ghost_honorary_root := {}\<rparr>,
                             sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate r f opt_r'])\<rparr>))
 = mut_m.tso_store_refs m s \<union> (if m' = m then store_refs (mw_Mutate r f opt_r') else {})"
  "mut_m.tso_store_refs m (s(sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate_Payload r f pl])\<rparr>))
 = mut_m.tso_store_refs m s \<union> (if m' = m then store_refs (mw_Mutate_Payload r f pl) else {})"
  "mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> obj)\<rparr>))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>ghost_honorary_root := Option.set_option opt_r', ref := opt_r'\<rparr>))
 = mut_m.tso_store_refs m s"
  "mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)),
                                          mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))
 = (if p = mutator m then \<Union>w \<in> set ws. store_refs w else mut_m.tso_store_refs m s)"
  "mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)),
                                          mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))
 = (if p = mutator m then \<Union>w \<in> set ws. store_refs w else mut_m.tso_store_refs m s)"
  "sys_mem_store_buffers p s = mw_Mark r fl # ws
\<Longrightarrow> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>))
 = mut_m.tso_store_refs m s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := roots'\<rparr>)) = mut_m.tso_store_refs m s &&& mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate r f opt_r'])\<rparr>)) = mut_m.tso_store_refs m s \<union> (if m' = m then store_refs (mw_Mutate r f opt_r') else {})) &&& mut_m.tso_store_refs m (s(sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate_Payload r f pl])\<rparr>)) = mut_m.tso_store_refs m s \<union> (if m' = m then store_refs (mw_Mutate_Payload r f pl) else {}) &&& mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)) = mut_m.tso_store_refs m s) &&& (mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> obj)\<rparr>)) = mut_m.tso_store_refs m s &&& mut_m.tso_store_refs m (s(mutator m' := s (mutator m')\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)) = mut_m.tso_store_refs m s) &&& mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = (if p = mutator m then \<Union> (store_refs ` set ws) else mut_m.tso_store_refs m s) &&& mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = (if p = mutator m then \<Union> (store_refs ` set ws) else mut_m.tso_store_refs m s) &&& (sys_mem_store_buffers p s = mw_Mark r fl # ws \<Longrightarrow> mut_m.tso_store_refs m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = mut_m.tso_store_refs m s)
[PROOF STEP]
unfolding mut_m.tso_store_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(mutator m' := s (mutator m')\<lparr>roots := roots'\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s)) &&& \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(mutator m' := s (mutator m')\<lparr>ghost_honorary_root := {}\<rparr>, sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate r f opt_r'])\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s)) \<union> (if m' = m then store_refs (mw_Mutate r f opt_r') else {})) &&& \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(sys := s sys\<lparr>mem_store_buffers := (mem_store_buffers (s sys))(mutator m' := sys_mem_store_buffers (mutator m') s @ [mw_Mutate_Payload r f pl])\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s)) \<union> (if m' = m then store_refs (mw_Mutate_Payload r f pl) else {}) &&& \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := None)\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s))) &&& (\<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(mutator m' := s (mutator m')\<lparr>roots := insert r (roots (s (mutator m')))\<rparr>, sys := s sys\<lparr>heap := sys_heap s(r \<mapsto> obj)\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s)) &&& \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(mutator m' := s (mutator m')\<lparr>ghost_honorary_root := set_option opt_r', ref := opt_r'\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s))) &&& \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)))) = (if p = mutator m then \<Union> (store_refs ` set ws) else \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s))) &&& \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_payload := (obj_payload obj)(f := pl)\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)))) = (if p = mutator m then \<Union> (store_refs ` set ws) else \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s))) &&& (sys_mem_store_buffers p s = mw_Mark r fl # ws \<Longrightarrow> \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)))) = \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s)))
[PROOF STEP]
by (auto simp: fun_upd_apply)


[STATEMENT]
lemma points_to_Mutate:
  "(x points_to y)
         (s(sys := (s sys)\<lparr> heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)),
                            mem_store_buffers := (mem_store_buffers (s sys))(p := ws) \<rparr>))
  \<longleftrightarrow> (r \<noteq> x \<and> (x points_to y) s) \<or> (r = x \<and> valid_ref r s \<and> (opt_r' = Some y \<or> ( (x points_to y) s \<and> obj_at (\<lambda>obj. \<exists>f'. obj_fields obj f' = Some y \<and> f \<noteq> f') r s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x points_to y) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = (r \<noteq> x \<and> (x points_to y) s \<or> r = x \<and> obj_at (\<lambda>s. True) r s \<and> (opt_r' = Some y \<or> (x points_to y) s \<and> obj_at (\<lambda>obj. \<exists>f'. obj_fields obj f' = Some y \<and> f \<noteq> f') r s))
[PROOF STEP]
unfolding ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. y \<in> {b. \<exists>a. obj_fields obj a = Some b}) x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)\<rparr>)) = (r \<noteq> x \<and> obj_at (\<lambda>obj. y \<in> {b. \<exists>a. obj_fields obj a = Some b}) x s \<or> r = x \<and> obj_at (\<lambda>s. True) r s \<and> (opt_r' = Some y \<or> obj_at (\<lambda>obj. y \<in> {b. \<exists>a. obj_fields obj a = Some b}) x s \<and> obj_at (\<lambda>obj. \<exists>f'. obj_fields obj f' = Some y \<and> f \<noteq> f') r s))
[PROOF STEP]
by (auto simp: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma \<comment> \<open>Sanity\<close>
  "hp' = hs_step hp \<Longrightarrow> \<exists>in' ht. (in', ht, hp', hp) \<in> hp_step_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hp' = hs_step hp \<Longrightarrow> \<exists>in' ht. (in', ht, hp', hp) \<in> hp_step_rel
[PROOF STEP]
by (cases hp) (auto simp: hp_step_rel_def)


[STATEMENT]
lemma \<comment> \<open>Sanity\<close>
  "(False, ht, hp', hp) \<in> hp_step_rel \<Longrightarrow> hp' = hp_step ht hp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (False, ht, hp', hp) \<in> hp_step_rel \<Longrightarrow> hp' = hp_step ht hp
[PROOF STEP]
by (cases ht) (auto simp: hp_step_rel_def)


[STATEMENT]
lemma (in mut_m) handshake_phase_invD:
  assumes "handshake_phase_inv s"
  shows "(sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, mut_ghost_hs_phase s) \<in> hp_step_rel
       \<and> (sys_hs_pending m s \<longrightarrow> \<not>sys_ghost_hs_in_sync m s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, mut_ghost_hs_phase s) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
handshake_phase_inv s

goal (1 subgoal):
 1. (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, mut_ghost_hs_phase s) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s)
[PROOF STEP]
unfolding handshake_phase_inv_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (sys_ghost_hs_in_sync x s, sys_hs_type s, sys_ghost_hs_phase s, ghost_hs_phase (s (mutator x))) \<in> hp_step_rel \<and> (sys_hs_pending x s \<longrightarrow> \<not> sys_ghost_hs_in_sync x s)

goal (1 subgoal):
 1. (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, mut_ghost_hs_phase s) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s)
[PROOF STEP]
by simp


[STATEMENT]
lemma handshake_in_syncD:
  "\<lbrakk> All (ghost_hs_in_sync (s sys)); handshake_phase_inv s \<rbrakk>
     \<Longrightarrow> \<forall>m'. mut_m.mut_ghost_hs_phase m' s = sys_ghost_hs_phase s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>All (ghost_hs_in_sync (s sys)); handshake_phase_inv s\<rbrakk> \<Longrightarrow> \<forall>m'. ghost_hs_phase (s (mutator m')) = sys_ghost_hs_phase s
[PROOF STEP]
by clarsimp (auto simp: hp_step_rel_def dest!: mut_m.handshake_phase_invD)


[STATEMENT]
lemma phase_rel_invD:
  assumes "phase_rel_inv s"
  shows "(\<forall>m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, tso_pending_phase gc s) \<in> phase_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, filter is_mw_Phase (sys_mem_store_buffers gc s)) \<in> phase_rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
phase_rel_inv s

goal (1 subgoal):
 1. (\<forall>m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, filter is_mw_Phase (sys_mem_store_buffers gc s)) \<in> phase_rel
[PROOF STEP]
unfolding phase_rel_inv_def
[PROOF STATE]
proof (prove)
using this:
(All (ghost_hs_in_sync (s sys)), sys_ghost_hs_phase s, gc_phase s, sys_phase s, filter is_mw_Phase (sys_mem_store_buffers gc s)) \<in> phase_rel

goal (1 subgoal):
 1. (\<forall>m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, filter is_mw_Phase (sys_mem_store_buffers gc s)) \<in> phase_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma mut_m_not_idle_no_fM_write:
  "\<lbrakk> ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; fM_rel_inv s; handshake_phase_inv s; tso_store_inv s; p \<noteq> sys \<rbrakk>
     \<Longrightarrow> \<not>sys_mem_store_buffers p s = mw_fM fl # ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; fM_rel_inv s; handshake_phase_inv s; tso_store_inv s; p \<noteq> sys\<rbrakk> \<Longrightarrow> sys_mem_store_buffers p s \<noteq> mw_fM fl # ws
[PROOF STEP]
apply (drule mut_m.handshake_phase_invD[where m=m])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; fM_rel_inv s; tso_store_inv s; p \<noteq> sys; (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, ghost_hs_phase (s (mutator m))) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s)\<rbrakk> \<Longrightarrow> sys_mem_store_buffers p s \<noteq> mw_fM fl # ws
[PROOF STEP]
apply (drule fM_rel_invD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; tso_store_inv s; p \<noteq> sys; (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, ghost_hs_phase (s (mutator m))) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s); (\<forall>x. sys_ghost_hs_in_sync x s, sys_ghost_hs_phase s, gc_fM s, sys_fM s, filter is_mw_fM (sys_mem_store_buffers gc s), sys_mem_lock s = Some gc) \<in> fM_rel\<rbrakk> \<Longrightarrow> sys_mem_store_buffers p s \<noteq> mw_fM fl # ws
[PROOF STEP]
apply (clarsimp simp: hp_step_rel_def fM_rel_def filter_empty_conv p_not_sys)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; tso_store_inv s; p = gc \<or> (\<exists>m. p = mutator m); sys_fM s = gc_fM s \<and> (\<forall>x\<in>set (sys_mem_store_buffers gc s). \<forall>fl. x \<noteq> mw_fM fl) \<and> (sys_ghost_hs_phase s = hp_Idle \<longrightarrow> (\<exists>x. \<not> sys_ghost_hs_in_sync x s)) \<or> sys_ghost_hs_phase s = hp_Idle \<and> (\<forall>x\<in>set (sys_mem_store_buffers gc s). \<forall>fl. x \<noteq> mw_fM fl) \<and> All (ghost_hs_in_sync (s sys)) \<or> sys_ghost_hs_phase s = hp_Idle \<and> gc_fM s = (\<not> sys_fM s) \<and> filter is_mw_fM (sys_mem_store_buffers gc s) = [mw_fM (\<not> sys_fM s)] \<and> sys_mem_lock s \<noteq> Some gc \<and> All (ghost_hs_in_sync (s sys)); \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> sys_ghost_hs_phase s = hp_Idle \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> sys_ghost_hs_phase s = hp_InitMark \<and> ghost_hs_phase (s (mutator m)) = hp_IdleInit \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> sys_ghost_hs_phase s = hp_Mark \<and> ghost_hs_phase (s (mutator m)) = hp_InitMark \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetRoots \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_Mark \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetWork \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetRoots \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetWork \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> ghost_hs_phase (s (mutator m)) = sys_ghost_hs_phase s \<and> (sys_ghost_hs_phase s = hp_Idle \<or> sys_ghost_hs_phase s = hp_IdleInit \<or> sys_ghost_hs_phase s = hp_InitMark \<or> sys_ghost_hs_phase s = hp_Mark); sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s; sys_mem_store_buffers p s = mw_fM fl # ws\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis list.set_intros(1) tso_store_invD(4))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in mut_m) mut_ghost_handshake_phase_idle:
  "\<lbrakk> mut_ghost_hs_phase s = hp_Idle; handshake_phase_inv s; phase_rel_inv s \<rbrakk>
     \<Longrightarrow> sys_phase s = ph_Idle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mut_ghost_hs_phase s = hp_Idle; handshake_phase_inv s; phase_rel_inv s\<rbrakk> \<Longrightarrow> sys_phase s = ph_Idle
[PROOF STEP]
apply (drule phase_rel_invD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mut_ghost_hs_phase s = hp_Idle; handshake_phase_inv s; (\<forall>m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, filter is_mw_Phase (sys_mem_store_buffers gc s)) \<in> phase_rel\<rbrakk> \<Longrightarrow> sys_phase s = ph_Idle
[PROOF STEP]
apply (drule handshake_phase_invD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mut_ghost_hs_phase s = hp_Idle; (\<forall>m. sys_ghost_hs_in_sync m s, sys_ghost_hs_phase s, gc_phase s, sys_phase s, filter is_mw_Phase (sys_mem_store_buffers gc s)) \<in> phase_rel; (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, mut_ghost_hs_phase s) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s)\<rbrakk> \<Longrightarrow> sys_phase s = ph_Idle
[PROOF STEP]
apply (auto simp: phase_rel_def hp_step_rel_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mut_m_not_idle_no_fM_writeD:
  "\<lbrakk> sys_mem_store_buffers p s = mw_fM fl # ws; ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; fM_rel_inv s; handshake_phase_inv s; tso_store_inv s; p \<noteq> sys \<rbrakk>
     \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers p s = mw_fM fl # ws; ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; fM_rel_inv s; handshake_phase_inv s; tso_store_inv s; p \<noteq> sys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule mut_m.handshake_phase_invD[where m=m])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers p s = mw_fM fl # ws; ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; fM_rel_inv s; tso_store_inv s; p \<noteq> sys; (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, ghost_hs_phase (s (mutator m))) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule fM_rel_invD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers p s = mw_fM fl # ws; ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; tso_store_inv s; p \<noteq> sys; (sys_ghost_hs_in_sync m s, sys_hs_type s, sys_ghost_hs_phase s, ghost_hs_phase (s (mutator m))) \<in> hp_step_rel \<and> (sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s); (\<forall>x. sys_ghost_hs_in_sync x s, sys_ghost_hs_phase s, gc_fM s, sys_fM s, filter is_mw_fM (sys_mem_store_buffers gc s), sys_mem_lock s = Some gc) \<in> fM_rel\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp: hp_step_rel_def fM_rel_def filter_empty_conv p_not_sys)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers p s = mw_fM fl # ws; ghost_hs_phase (s (mutator m)) \<noteq> hp_Idle; tso_store_inv s; p = gc \<or> (\<exists>m. p = mutator m); sys_fM s = gc_fM s \<and> (\<forall>x\<in>set (sys_mem_store_buffers gc s). \<forall>fl. x \<noteq> mw_fM fl) \<and> (sys_ghost_hs_phase s = hp_Idle \<longrightarrow> (\<exists>x. \<not> sys_ghost_hs_in_sync x s)) \<or> sys_ghost_hs_phase s = hp_Idle \<and> (\<forall>x\<in>set (sys_mem_store_buffers gc s). \<forall>fl. x \<noteq> mw_fM fl) \<and> All (ghost_hs_in_sync (s sys)) \<or> sys_ghost_hs_phase s = hp_Idle \<and> gc_fM s = (\<not> sys_fM s) \<and> filter is_mw_fM (sys_mem_store_buffers gc s) = [mw_fM (\<not> sys_fM s)] \<and> sys_mem_lock s \<noteq> Some gc \<and> All (ghost_hs_in_sync (s sys)); \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> sys_ghost_hs_phase s = hp_Idle \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> sys_ghost_hs_phase s = hp_InitMark \<and> ghost_hs_phase (s (mutator m)) = hp_IdleInit \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> sys_ghost_hs_phase s = hp_Mark \<and> ghost_hs_phase (s (mutator m)) = hp_InitMark \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetRoots \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_Mark \<or> \<not> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetWork \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetRoots \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_GetWork \<and> sys_ghost_hs_phase s = hp_IdleMarkSweep \<and> ghost_hs_phase (s (mutator m)) = hp_IdleMarkSweep \<or> sys_ghost_hs_in_sync m s \<and> sys_hs_type s = ht_NOOP \<and> ghost_hs_phase (s (mutator m)) = sys_ghost_hs_phase s \<and> (sys_ghost_hs_phase s = hp_Idle \<or> sys_ghost_hs_phase s = hp_IdleInit \<or> sys_ghost_hs_phase s = hp_InitMark \<or> sys_ghost_hs_phase s = hp_Mark); sys_hs_pending m s \<longrightarrow> \<not> sys_ghost_hs_in_sync m s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis list.set_intros(1) tso_store_invD(4))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in mut_m) reachable_eq_imp:
  "eq_imp (\<lambda>r'. mut_roots \<^bold>\<otimes> mut_ghost_honorary_root \<^bold>\<otimes> (\<lambda>s. \<Union>(ran ` obj_fields ` set_option (sys_heap s r')))
              \<^bold>\<otimes> tso_pending_mutate (mutator m))
          (reachable r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (mut_roots s, mut_ghost_honorary_root s, \<Union> (ran ` obj_fields ` set_option (sys_heap s r')), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s))) (reachable r)
[PROOF STEP]
unfolding eq_imp_def reachable_def tso_store_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (mut_roots s, mut_ghost_honorary_root s, \<Union> (ran ` obj_fields ` set_option (sys_heap s x)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s)) = (mut_roots s', mut_ghost_honorary_root s', \<Union> (ran ` obj_fields ` set_option (sys_heap s' x)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'))) \<longrightarrow> (\<exists>x. x \<in> mut_roots s \<union> mut_ghost_honorary_root s \<union> \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s)) \<and> (x reaches r) s) = (\<exists>x. x \<in> mut_roots s' \<union> mut_ghost_honorary_root s' \<union> \<Union> (store_refs ` set (sys_mem_store_buffers (mutator m) s')) \<and> (x reaches r) s')
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s) = (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s'). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s')
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s) = (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s'). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s')
[PROOF STEP]
apply (subgoal_tac "\<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) \<longleftrightarrow> (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s) = (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s'). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s')
 2. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)
[PROOF STEP]
apply (subgoal_tac "\<forall>x. (x reaches r) s \<longleftrightarrow> (x reaches r) s'")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w); \<forall>x. (x reaches r) s = (x reaches r) s'\<rbrakk> \<Longrightarrow> (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s) = (\<exists>x. (x \<in> mut_roots s' \<or> x \<in> mut_ghost_honorary_root s' \<or> (\<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s'). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))) \<and> (x reaches r) s')
 2. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)\<rbrakk> \<Longrightarrow> \<forall>x. (x reaches r) s = (x reaches r) s'
 3. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)
[PROOF STEP]
apply (clarsimp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)\<rbrakk> \<Longrightarrow> \<forall>x. (x reaches r) s = (x reaches r) s'
 2. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)
[PROOF STEP]
apply (auto simp: reaches_fields; fail)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)
[PROOF STEP]
apply (drule arg_cong[where f=set])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root 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)); set (filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s)) = set (filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'))\<rbrakk> \<Longrightarrow> \<forall>r'. (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> store_refs w) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> store_refs w)
[PROOF STEP]
apply (clarsimp simp: set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x))\<rbrakk> \<Longrightarrow> (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) = (\<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
 2. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); w \<in> set (sys_mem_store_buffers (mutator m) s); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
 2. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (rename_tac s s' r' w)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); w \<in> set (sys_mem_store_buffers (mutator m) s); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
 2. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (drule_tac x=w in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
 2. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (rule_tac x=w in bexI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
 2. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> w \<in> set (sys_mem_store_buffers (mutator m) s')
 3. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (clarsimp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> w \<in> set (sys_mem_store_buffers (mutator m) s')
 2. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (clarsimp split: mem_store_action.splits; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' r'. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s'). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); w \<in> set (sys_mem_store_buffers (mutator m) s'); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (rename_tac s s' r' w)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); \<forall>x. (x \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)) = (x \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate x \<or> is_mw_Mutate_Payload x)); w \<in> set (sys_mem_store_buffers (mutator m) s'); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (drule_tac x=w in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s'); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> \<exists>w\<in>set (sys_mem_store_buffers (mutator m) s). r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
[PROOF STEP]
apply (rule_tac x=w in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s'); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})
 2. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s'); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> w \<in> set (sys_mem_store_buffers (mutator m) s)
[PROOF STEP]
apply (clarsimp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' w. \<lbrakk>\<forall>x. (x \<in> mut_roots s) = (x \<in> mut_roots s'); \<forall>x. (x \<in> mut_ghost_honorary_root s) = (x \<in> mut_ghost_honorary_root s'); \<forall>x xa. (\<exists>x\<in>set_option (sys_heap s x). xa \<in> ran (obj_fields x)) = (\<exists>x\<in>set_option (sys_heap s' x). xa \<in> ran (obj_fields x)); w \<in> set (sys_mem_store_buffers (mutator m) s'); r' \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (w \<in> set (sys_mem_store_buffers (mutator m) s) \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w)) = (w \<in> set (sys_mem_store_buffers (mutator m) s') \<and> (is_mw_Mutate w \<or> is_mw_Mutate_Payload w))\<rbrakk> \<Longrightarrow> w \<in> set (sys_mem_store_buffers (mutator m) s)
[PROOF STEP]
apply (clarsimp split: mem_store_action.splits; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma reachableI[intro]:
  "x \<in> mut_m.mut_roots m s \<Longrightarrow> mut_m.reachable m x s"
  "x \<in> mut_m.tso_store_refs m s \<Longrightarrow> mut_m.reachable m x s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> roots (s (mutator m)) \<Longrightarrow> mut_m.reachable m x s) &&& (x \<in> mut_m.tso_store_refs m s \<Longrightarrow> mut_m.reachable m x s)
[PROOF STEP]
by (auto simp: mut_m.reachable_def reaches_def)


[STATEMENT]
lemma reachable_points_to[elim]:
  "\<lbrakk> (x points_to y) s; mut_m.reachable m x s \<rbrakk> \<Longrightarrow> mut_m.reachable m y s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x points_to y) s; mut_m.reachable m x s\<rbrakk> \<Longrightarrow> mut_m.reachable m y s
[PROOF STEP]
by (auto simp: mut_m.reachable_def reaches_def elim: rtranclp.intros(2))


[STATEMENT]
lemma (in mut_m) mut_reachableE[consumes 1, case_names mut_root tso_store_refs]:
  "\<lbrakk> reachable y s;
     \<And>x. \<lbrakk> (x reaches y) s; x \<in> mut_roots s \<rbrakk> \<Longrightarrow> Q;
     \<And>x. \<lbrakk> (x reaches y) s; x \<in> mut_ghost_honorary_root s \<rbrakk> \<Longrightarrow> Q;
     \<And>x. \<lbrakk> (x reaches y) s; x \<in> tso_store_refs s \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable y s; \<And>x. \<lbrakk>(x reaches y) s; x \<in> mut_roots s\<rbrakk> \<Longrightarrow> Q; \<And>x. \<lbrakk>(x reaches y) s; x \<in> mut_ghost_honorary_root s\<rbrakk> \<Longrightarrow> Q; \<And>x. \<lbrakk>(x reaches y) s; x \<in> tso_store_refs s\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by (auto simp: reachable_def)


[STATEMENT]
lemma reachable_induct[consumes 1, case_names root ghost_honorary_root tso_root reaches]:
  assumes r: "mut_m.reachable m y s"
  assumes root: "\<And>x. \<lbrakk> x \<in> mut_m.mut_roots m s \<rbrakk> \<Longrightarrow> P x"
  assumes ghost_honorary_root: "\<And>x. \<lbrakk> x \<in> mut_m.mut_ghost_honorary_root m s \<rbrakk> \<Longrightarrow> P x"
  assumes tso_root: "\<And>x. x \<in> mut_m.tso_store_refs m s \<Longrightarrow> P x"
  assumes reaches: "\<And>x y. \<lbrakk> mut_m.reachable m x s; (x points_to y) s; P x \<rbrakk> \<Longrightarrow> P y"
  shows "P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P y
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
mut_m.reachable m y s

goal (1 subgoal):
 1. P y
[PROOF STEP]
unfolding mut_m.reachable_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<and> (x reaches y) s

goal (1 subgoal):
 1. P y
[PROOF STEP]
proof(clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s; (x reaches y) s\<rbrakk> \<Longrightarrow> P y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s; (x reaches y) s\<rbrakk> \<Longrightarrow> P y
[PROOF STEP]
assume "(x reaches y) s" and "x \<in> mut_m.mut_roots m s \<union> mut_m.mut_ghost_honorary_root m s \<union> mut_m.tso_store_refs m s"
[PROOF STATE]
proof (state)
this:
(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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s; (x reaches y) s\<rbrakk> \<Longrightarrow> P y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(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
[PROOF STEP]
show "P y"
[PROOF STATE]
proof (prove)
using this:
(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

goal (1 subgoal):
 1. P y
[PROOF STEP]
unfolding reaches_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. P y
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P x
 2. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; (y points_to z) s; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> P z
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s

goal (2 subgoals):
 1. x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P x
 2. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; (y points_to z) s; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> P z
[PROOF STEP]
with root ghost_honorary_root tso_root
[PROOF STATE]
proof (chain)
picking this:
?x \<in> roots (s (mutator m)) \<Longrightarrow> P ?x
?x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> P ?x
?x \<in> mut_m.tso_store_refs m s \<Longrightarrow> P ?x
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x \<in> roots (s (mutator m)) \<Longrightarrow> P ?x
?x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> P ?x
?x \<in> mut_m.tso_store_refs m s \<Longrightarrow> P ?x
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. P x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; (y points_to z) s; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> P z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; (y points_to z) s; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> P z
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
(y points_to z) s
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; (y points_to z) s; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y; x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s\<rbrakk> \<Longrightarrow> P z
[PROOF STEP]
with reaches
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>mut_m.reachable m ?x s; (?x points_to ?y) s; P ?x\<rbrakk> \<Longrightarrow> P ?y
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
(y points_to z) s
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mut_m.reachable m ?x s; (?x points_to ?y) s; P ?x\<rbrakk> \<Longrightarrow> P ?y
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
(y points_to z) s
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. P z
[PROOF STEP]
unfolding mut_m.reachable_def reaches_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>x. x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x ?x; (?x points_to ?y) s; P ?x\<rbrakk> \<Longrightarrow> P ?y
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
(y points_to z) s
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<Longrightarrow> P y
x \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s

goal (1 subgoal):
 1. P z
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
P z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mutator_reachable_tso:
  "sys_mem_store_buffers (mutator m) s = mw_Mutate r f opt_r' # ws
    \<Longrightarrow> mut_m.reachable m r s \<and> (\<forall>r'. opt_r' = Some r' \<longrightarrow> mut_m.reachable m r' s)"
  "sys_mem_store_buffers (mutator m) s = mw_Mutate_Payload r f pl # ws
    \<Longrightarrow> mut_m.reachable m r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sys_mem_store_buffers (mutator m) s = mw_Mutate r f opt_r' # ws \<Longrightarrow> mut_m.reachable m r s \<and> (\<forall>r'. opt_r' = Some r' \<longrightarrow> mut_m.reachable m r' s)) &&& (sys_mem_store_buffers (mutator m) s = mw_Mutate_Payload r f pl # ws \<Longrightarrow> mut_m.reachable m r s)
[PROOF STEP]
by (auto simp: mut_m.tso_store_refs_def)


[STATEMENT]
lemma greyI[intro]:
  "r \<in> ghost_honorary_grey (s p) \<Longrightarrow> grey r s"
  "r \<in> W (s p) \<Longrightarrow> grey r s"
  "r \<in> WL p s \<Longrightarrow> grey r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> ghost_honorary_grey (s p) \<Longrightarrow> grey r s) &&& (r \<in> W (s p) \<Longrightarrow> grey r s) &&& (r \<in> WL p s \<Longrightarrow> grey r s)
[PROOF STEP]
unfolding grey_def WL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r \<in> ghost_honorary_grey (s p) \<Longrightarrow> \<exists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x)) &&& (r \<in> W (s p) \<Longrightarrow> \<exists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x)) &&& (r \<in> W (s p) \<union> ghost_honorary_grey (s p) \<Longrightarrow> \<exists>x. r \<in> W (s x) \<union> ghost_honorary_grey (s x))
[PROOF STEP]
by (case_tac [!] p) auto


[STATEMENT]
lemma blackD[dest]:
  "black r s \<Longrightarrow> marked r s"
  "black r s \<Longrightarrow> r \<notin> WL p s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (black r s \<Longrightarrow> marked r s) &&& (black r s \<Longrightarrow> r \<notin> WL p s)
[PROOF STEP]
unfolding black_def grey_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (marked r s \<and> (\<nexists>x. r \<in> WL x s) \<Longrightarrow> marked r s) &&& (marked r s \<and> (\<nexists>x. r \<in> WL x s) \<Longrightarrow> r \<notin> WL p s)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma whiteI[intro]: (* FIXME simp normal form of def *)
  "obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s)) r s \<Longrightarrow> white r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s)) r s \<Longrightarrow> white r s
[PROOF STEP]
unfolding white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s)) r s \<Longrightarrow> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s
[PROOF STEP]
by simp


[STATEMENT]
lemma marked_not_white[dest]:
  "white r s \<Longrightarrow> \<not>marked r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. white r s \<Longrightarrow> \<not> marked r s
[PROOF STEP]
unfolding white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s \<Longrightarrow> \<not> marked r s
[PROOF STEP]
by (simp_all split: obj_at_splits)


[STATEMENT]
lemma white_valid_ref[elim!]:
  "white r s \<Longrightarrow> valid_ref r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. white r s \<Longrightarrow> obj_at (\<lambda>s. True) r s
[PROOF STEP]
unfolding white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s \<Longrightarrow> obj_at (\<lambda>s. True) r s
[PROOF STEP]
by (simp_all split: obj_at_splits)


[STATEMENT]
lemma not_white_marked[elim!]:
  "\<lbrakk>\<not> white r s; valid_ref r s\<rbrakk> \<Longrightarrow> marked r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> white r s; obj_at (\<lambda>s. True) r s\<rbrakk> \<Longrightarrow> marked r s
[PROOF STEP]
unfolding white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s; obj_at (\<lambda>s. True) r s\<rbrakk> \<Longrightarrow> marked r s
[PROOF STEP]
by (simp split: obj_at_splits)


[STATEMENT]
lemma black_eq_imp:
  "eq_imp (\<lambda>_::unit. (\<lambda>s. r \<in> (\<Union>p. WL p s)) \<^bold>\<otimes> sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r)))
          (black r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. (r \<in> (\<Union>p. WL p s), sys_fM s, map_option obj_mark (sys_heap s r))) (black r)
[PROOF STEP]
unfolding eq_imp_def black_def grey_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (r \<in> (\<Union>p. WL p s), sys_fM s, map_option obj_mark (sys_heap s r)) = (r \<in> (\<Union>p. WL p s'), sys_fM s', map_option obj_mark (sys_heap s' r))) \<longrightarrow> (marked r s \<and> (\<nexists>x. r \<in> WL x s)) = (marked r s' \<and> (\<nexists>x. r \<in> WL x s'))
[PROOF STEP]
by (auto split: obj_at_splits)


[STATEMENT]
lemma grey_eq_imp:
  "eq_imp (\<lambda>_::unit. (\<lambda>s. r \<in> (\<Union>p. WL p s)))
          (grey r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. r \<in> (\<Union>p. WL p s)) (grey r)
[PROOF STEP]
unfolding eq_imp_def grey_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (r \<in> (\<Union>p. WL p s)) = (r \<in> (\<Union>p. WL p s'))) \<longrightarrow> (\<exists>x. r \<in> WL x s) = (\<exists>x. r \<in> WL x s')
[PROOF STEP]
by auto


[STATEMENT]
lemma white_eq_imp:
  "eq_imp (\<lambda>_::unit. sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r)))
          (white r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. (sys_fM s, map_option obj_mark (sys_heap s r))) (white r)
[PROOF STEP]
unfolding eq_imp_def white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (sys_fM s, map_option obj_mark (sys_heap s r)) = (sys_fM s', map_option obj_mark (sys_heap s' r))) \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s = obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s') r s'
[PROOF STEP]
by (auto split: obj_at_splits)


[STATEMENT]
lemma black_heap_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')))
          black_heap"
[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'))) black_heap
[PROOF STEP]
apply (clarsimp simp: eq_imp_def black_heap_def black_def grey_def all_conj_distrib fun_eq_iff split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s)) = (\<forall>x. obj_at (\<lambda>s. True) x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s'))
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s)) = (\<forall>x. obj_at (\<lambda>s. True) x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> 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>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s)) = (\<forall>x. obj_at (\<lambda>s. True) x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s'))
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (subgoal_tac "\<forall>x. valid_ref x s \<longleftrightarrow> valid_ref x s'")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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'; \<forall>x. obj_at (\<lambda>s. True) x s = obj_at (\<lambda>s. True) x s'\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s)) = (\<forall>x. obj_at (\<lambda>s. True) x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s'))
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s = obj_at (\<lambda>s. True) x s'
 3. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (subgoal_tac "\<forall>x. (\<forall>p. x \<notin> WL p s) \<longleftrightarrow> (\<forall>p. x \<notin> WL p s')")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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'; \<forall>x. obj_at (\<lambda>s. True) x s = obj_at (\<lambda>s. True) x s'; \<forall>x. (\<forall>p. x \<notin> WL p s) = (\<forall>p. x \<notin> WL p s')\<rbrakk> \<Longrightarrow> (\<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s)) = (\<forall>x. obj_at (\<lambda>s. True) x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s'))
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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'; \<forall>x. obj_at (\<lambda>s. True) x s = obj_at (\<lambda>s. True) x s'\<rbrakk> \<Longrightarrow> \<forall>x. (\<forall>p. x \<notin> WL p s) = (\<forall>p. x \<notin> WL p s')
 3. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s = obj_at (\<lambda>s. True) x s'
 4. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (3 subgoals):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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'; \<forall>x. obj_at (\<lambda>s. True) x s = obj_at (\<lambda>s. True) x s'\<rbrakk> \<Longrightarrow> \<forall>x. (\<forall>p. x \<notin> WL p s) = (\<forall>p. x \<notin> WL p s')
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s = obj_at (\<lambda>s. True) x s'
 3. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (auto simp: set_eq_iff)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>s. True) x s = obj_at (\<lambda>s. True) x s'
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (2 subgoals):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) x s = obj_at (\<lambda>s. True) x s'
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (rename_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) x s = obj_at (\<lambda>s. True) x s'
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (rule eq_impD[OF obj_at_eq_imp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'\<rbrakk> \<Longrightarrow> \<forall>xa. map_option (\<lambda>s. True) (sys_heap s x) = map_option (\<lambda>s. True) (sys_heap s' x)
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p s'); sys_fM s = sys_fM s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'; map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> \<forall>xa. map_option (\<lambda>s. True) (sys_heap s x) = map_option (\<lambda>s. True) (sys_heap s' x)
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 (drule_tac f="map_option \<langle>True\<rangle>" in arg_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p s'); sys_fM s = sys_fM s'; \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'; map_option (\<lambda>s. True) (map_option obj_mark (sys_heap s x)) = map_option (\<lambda>s. True) (map_option obj_mark (sys_heap s' x))\<rbrakk> \<Longrightarrow> \<forall>xa. map_option (\<lambda>s. True) (sys_heap s x) = map_option (\<lambda>s. True) (sys_heap s' x)
 2. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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 fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
[PROOF STEP]
apply (rule eq_impD[OF obj_at_eq_imp])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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>xa. map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s x) = map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s' x)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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> map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s x) = map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s' x)
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p 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> map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s x) = map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s' x)
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p s'); sys_fM s = sys_fM s'; map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s x) = map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s' x)
[PROOF STEP]
apply (drule_tac f="map_option (\<lambda>fl. fl = sys_fM s)" in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>(\<Union>p. WL p s) = (\<Union>p. WL p s'); sys_fM s = sys_fM s'; map_option (\<lambda>fl. fl = sys_fM s) (map_option obj_mark (sys_heap s x)) = map_option (\<lambda>fl. fl = sys_fM s) (map_option obj_mark (sys_heap s' x))\<rbrakk> \<Longrightarrow> map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s x) = map_option (\<lambda>obj. obj_mark obj = sys_fM s') (sys_heap s' x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma white_heap_eq_imp:
  "eq_imp (\<lambda>r'. sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')))
          white_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (sys_fM s, map_option obj_mark (sys_heap s r'))) white_heap
[PROOF STEP]
apply (clarsimp simp: all_conj_distrib eq_imp_def white_def white_heap_def obj_at_def fun_eq_iff
               split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>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 x2. sys_heap s x = Some x2 \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')) = (\<forall>x x2. sys_heap s' x = Some x2 \<longrightarrow> obj_mark x2 = (\<not> sys_fM 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. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); \<forall>x x2. sys_heap s x = Some x2 \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')\<rbrakk> \<Longrightarrow> \<forall>x x2. sys_heap s' x = Some x2 \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')
 2. \<And>s s'. \<lbrakk>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 x2. sys_heap s' x = Some x2 \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')\<rbrakk> \<Longrightarrow> \<forall>x x2. sys_heap s x = Some x2 \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')
[PROOF STEP]
apply (metis (opaque_lifting, no_types) map_option_eq_Some)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma white_heap_imp_no_black_refs[elim!]:
  "white_heap s \<Longrightarrow> no_black_refs s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. white_heap s \<Longrightarrow> no_black_refs s
[PROOF STEP]
apply (clarsimp simp: white_def white_heap_def no_black_refs_def black_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s)) x s; marked x s\<rbrakk> \<Longrightarrow> grey x s
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s)) x s; marked x s\<rbrakk> \<Longrightarrow> grey x s
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>marked x s; obj_at (\<lambda>s. True) x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = (\<not> sys_fM s)) x s\<rbrakk> \<Longrightarrow> grey x s
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma black_heap_no_greys[elim]:
  "\<lbrakk> no_grey_refs s; \<forall>r. marked r s \<or> \<not>valid_ref r s \<rbrakk> \<Longrightarrow> black_heap s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_grey_refs s; \<forall>r. marked r s \<or> \<not> obj_at (\<lambda>s. True) r s\<rbrakk> \<Longrightarrow> black_heap s
[PROOF STEP]
unfolding black_def black_heap_def no_grey_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<not> grey x s; \<forall>r. marked r s \<or> \<not> obj_at (\<lambda>s. True) r s\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>s. True) x s \<longrightarrow> marked x s \<and> \<not> grey x s
[PROOF STEP]
by fastforce


[STATEMENT]
lemma heap_colours_colours:
  "black_heap s \<Longrightarrow> \<not>white r s"
  "white_heap s \<Longrightarrow> \<not>black r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (black_heap s \<Longrightarrow> \<not> white r s) &&& (white_heap s \<Longrightarrow> \<not> black r s)
[PROOF STEP]
by (auto simp: black_heap_def white_def white_heap_def
        dest!: spec[where x=r]
        split: obj_at_splits)


[STATEMENT]
lemma strong_tricolour_invD:
  "\<lbrakk> black x s; (x points_to y) s; valid_ref y s; strong_tricolour_inv s \<rbrakk>
     \<Longrightarrow> marked y s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>black x s; (x points_to y) s; obj_at (\<lambda>s. True) y s; strong_tricolour_inv s\<rbrakk> \<Longrightarrow> marked y s
[PROOF STEP]
unfolding strong_tricolour_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>black x s; (x points_to y) s; obj_at (\<lambda>s. True) y s; \<forall>x xa. black x s \<longrightarrow> \<not> ((x points_to xa) s \<and> white xa s)\<rbrakk> \<Longrightarrow> marked y s
[PROOF STEP]
by fastforce


[STATEMENT]
lemma no_black_refsD:
  "no_black_refs s \<Longrightarrow> \<not>black r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_black_refs s \<Longrightarrow> \<not> black r s
[PROOF STEP]
unfolding no_black_refs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<not> black x s \<Longrightarrow> \<not> black r s
[PROOF STEP]
by simp