theory Refine_C

lemma user_memory_update_corres_C_helper:
      "\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a;
        dom um \<subseteq> dom (user_mem' a)\<rbrakk>
       \<Longrightarrow> (ksMachineState_update
            (underlying_memory_update
              (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m [p\<leftarrow>e. p \<in> dom um])) a,
            b\<lparr>globals := globals b
               \<lparr>t_hrs_' :=
                  (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b)))
                    [p\<leftarrow>e. p \<in> dom um],
                   snd (t_hrs_' (globals b)))\<rparr>\<rparr>)
           \<in> rf_sr" apply (induct e) apply simp apply (subgoal_tac
            "ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a = a") apply (simp (no_asm_simp)) apply simp apply (rename_tac x xs) apply (simp add: foldl_fun_upd_eq_foldr) apply (case_tac "x \<in> dom um", simp_all) apply (frule_tac ptr=x and b="the (um x)" in storeByteUser_rf_sr_upd) apply simp apply simp apply (thin_tac "(x,y) : rf_sr" for x y)+ apply (fastforce simp add: pointerInUserData_def dom_user_mem') apply (simp add: o_def hrs_mem_update_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) e))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) e), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) []))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) []), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>x1 e. \<lbrakk>\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) e))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) e), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) (x1 # e)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) (x1 # e)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a, b) \<in> rf_sr
 2. \<And>x1 e. \<lbrakk>\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) e))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) e), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) (x1 # e)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) (x1 # e)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a = a\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a, b) \<in> rf_sr
 2. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a = a
 3. \<And>x1 e. \<lbrakk>\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) e))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) e), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) (x1 # e)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) (x1 # e)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> ksMachineState_update (underlying_memory_update (\<lambda>m. m)) a = a
 2. \<And>x1 e. \<lbrakk>\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) e))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) e), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) (x1 # e)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) (x1 # e)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x1 e. \<lbrakk>\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) e))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) e), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) (x1 # e)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) (x1 # e)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) xs), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) (x # xs)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals b))) (filter (\<lambda>p. p \<in> dom um) (x # xs)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (if x \<in> dom um then x # filter (\<lambda>p. p \<in> dom um) xs else filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (if x \<in> dom um then x # filter (\<lambda>p. p \<in> dom um) xs else filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) m)(x := the (um x)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := ((foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))))(x := the (um x)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (4 subgoals):
 1. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pspace_aligned' (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 2. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pspace_distinct' (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 3. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pointerInUserData x (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 4. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um; (ksMachineState_update (underlying_memory_update (\<lambda>m. m(x := the (um x)))) (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a), globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(x := the (um x))))) (b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>)) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) m)(x := the (um x)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := ((foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))))(x := the (um x)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pspace_distinct' (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 2. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pointerInUserData x (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 3. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um; (ksMachineState_update (underlying_memory_update (\<lambda>m. m(x := the (um x)))) (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a), globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(x := the (um x))))) (b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>)) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) m)(x := the (um x)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := ((foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))))(x := the (um x)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pointerInUserData x (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 2. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um; (ksMachineState_update (underlying_memory_update (\<lambda>m. m(x := the (um x)))) (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a), globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(x := the (um x))))) (b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>)) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) m)(x := the (um x)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := ((foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))))(x := the (um x)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um\<rbrakk> \<Longrightarrow> pointerInUserData x (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a)
 2. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um; (ksMachineState_update (underlying_memory_update (\<lambda>m. m(x := the (um x)))) (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a), globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(x := the (um x))))) (b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>)) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) m)(x := the (um x)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := ((foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))))(x := the (um x)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>(ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr; (a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); x \<in> dom um; (ksMachineState_update (underlying_memory_update (\<lambda>m. m(x := the (um x)))) (ksMachineState_update (underlying_memory_update (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs))) a), globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(x := the (um x))))) (b\<lparr>globals := globals b\<lparr>t_hrs_' := (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))), snd (t_hrs_' (globals b)))\<rparr>\<rparr>)) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. (foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) m)(x := the (um x)))) a, b\<lparr>globals := globals b\<lparr>t_hrs_' := ((foldr (\<lambda>p f. f(p := the (um p))) (filter (\<lambda>p. p \<in> dom um) xs) (fst (t_hrs_' (globals b))))(x := the (um x)), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal:
No subgoals!