theory Refine_C

lemma user_memory_update_corres_C:
  "corres_underlying rf_sr False nf (%_ _. True)
     (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom um \<subseteq> dom (user_mem' s))
     \<top>
     (doMachineOp (user_memory_update um)) (setUserMem_C um)" supply option.case_cong_weak[cong] apply (clarsimp simp: corres_underlying_def) apply (rule conjI) prefer 2 apply (clarsimp simp add: setUserMem_C_def simpler_modify_def) apply (subgoal_tac
       "doMachineOp (user_memory_update um) a =
        modify (ksMachineState_update (underlying_memory_update
                 (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m [p\<leftarrow>enum. p \<in> dom um])))
               a") prefer 2 apply (clarsimp simp add: doMachineOp_def user_memory_update_def
                             simpler_modify_def simpler_gets_def select_f_def
                             Nondet_Monad.bind_def return_def) apply (thin_tac P for P)+ apply (case_tac a, clarsimp) apply (case_tac ksMachineStatea, clarsimp) apply (rule ext) apply (simp add: foldl_fun_upd_value dom_def split: option.splits) apply clarsimp apply (cut_tac s'=a and s="globals b" in user_mem_C_relation[symmetric]) apply (simp add: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) apply simp+ apply (simp add: setUserMem_C_def_foldl) apply (clarsimp simp add: simpler_modify_def) apply (thin_tac "doMachineOp p s = x" for p s x) apply (drule sym, simp) apply (rule user_memory_update_corres_C_helper,auto)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False nf (\<lambda>_ _. True) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom um \<subseteq> dom (user_mem' s)) (\<lambda>_. True) (doMachineOp (user_memory_update um)) (setUserMem_C um) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False nf (\<lambda>_ _. True) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> dom um \<subseteq> dom (user_mem' s)) (\<lambda>_. True) (doMachineOp (user_memory_update um)) (setUserMem_C um) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr) \<and> (nf \<longrightarrow> \<not> snd (setUserMem_C um b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> nf \<longrightarrow> \<not> snd (setUserMem_C um b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> nf \<longrightarrow> \<not> snd (setUserMem_C um b)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a)\<rbrakk> \<Longrightarrow> a\<lparr>ksMachineState := ksMachineState a\<lparr>underlying_memory := \<lambda>aa. case um aa of None \<Rightarrow> underlying_memory (ksMachineState a) aa | Some x \<Rightarrow> x\<rparr>\<rparr> = ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum))) a
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b. a\<lparr>ksMachineState := ksMachineState a\<lparr>underlying_memory := \<lambda>aa. case um aa of None \<Rightarrow> underlying_memory (ksMachineState a) aa | Some x \<Rightarrow> x\<rparr>\<rparr> = ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum))) a
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineStatea. ksMachineStatea\<lparr>underlying_memory := \<lambda>a. case um a of None \<Rightarrow> underlying_memory (ksMachineState \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineStatea\<rparr>) a | Some x \<Rightarrow> x\<rparr> = underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)) ksMachineStatea
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState irq_masks irq_state underlying_memorya device_state a b machine_state_rest. (\<lambda>aa. case um aa of None \<Rightarrow> underlying_memory (ksMachineState \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memorya, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>\<rparr>) aa | Some x \<Rightarrow> x) = foldl (\<lambda>f p. f(p := the (um p))) underlying_memorya (filter (\<lambda>p. p \<in> dom um) enum)
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState irq_masks irq_state underlying_memorya device_state a b machine_state_rest aa. (case um aa of None \<Rightarrow> underlying_memory (ksMachineState \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = \<lparr>irq_masks = irq_masks, irq_state = irq_state, underlying_memory = underlying_memorya, device_state = device_state, exclusive_state = (a, b), machine_state_rest = machine_state_rest\<rparr>\<rparr>) aa | Some x \<Rightarrow> x) = foldl (\<lambda>f p. f(p := the (um p))) underlying_memorya (filter (\<lambda>p. p \<in> dom um) enum) aa
 2. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (setUserMem_C um b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (user_memory_update um) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b)\<rbrakk> \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation
 2. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b)\<rbrakk> \<Longrightarrow> pspace_distinct' a
 3. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b); user_mem' a = user_mem_C (globals b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b)\<rbrakk> \<Longrightarrow> pspace_distinct' a
 2. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b); user_mem' a = user_mem_C (globals b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem_C (globals b)); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (setUserMem_C um b); user_mem' a = user_mem_C (globals b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem_C (globals b)); doMachineOp (user_memory_update um) a = modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a; ((), ba) \<in> fst (modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>t_hrs_' := (foldl (\<lambda>f p. f(p := the (um p))) (fst (t_hrs_' (globals s))) (filter (\<lambda>p. p \<in> dom um) enum), snd (t_hrs_' (globals s)))\<rparr>\<rparr>) b); user_mem' a = user_mem_C (globals b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (modify (ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum)))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem_C (globals b)); doMachineOp (user_memory_update um) a = ({((), ksMachineState_update (underlying_memory_update (\<lambda>m. foldl (\<lambda>f p. f(p := the (um p))) m (filter (\<lambda>p. p \<in> dom um) enum))) a)}, False); user_mem' a = user_mem_C (globals b)\<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) enum))) 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) enum), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem_C (globals b)); user_mem' a = user_mem_C (globals b)\<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) enum))) 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) enum), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; pspace_aligned' a; pspace_distinct' a; dom um \<subseteq> dom (user_mem' a); user_mem_C (globals b) = 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) enum))) 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) enum), snd (t_hrs_' (globals b)))\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal:
No subgoals!