theory Detype_R

lemma modify_obj_commute':
  "monad_commute (K (ptr\<noteq> ptr') and ko_wp_at' \<top> ptr')
     (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> ko))))
     (modify (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (the (ps ptr'))))))" apply (clarsimp simp:monad_commute_def return_def
    bind_def simpler_modify_def ko_wp_at'_def) apply (case_tac s) apply clarsimp apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K (ptr \<noteq> ptr') and ko_wp_at' (\<lambda>_. True) ptr') (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> ko)))) (modify (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> f (the (ps ptr')))))) proof (prove)
goal (1 subgoal):
 1. \<And>s koa. \<lbrakk>ptr \<noteq> ptr'; ksPSpace s ptr' = Some koa; is_aligned ptr' (objBitsKO koa); ps_clear ptr' (objBitsKO koa) s\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (the (ps ptr')))) \<circ> (\<lambda>ps. ps(ptr \<mapsto> ko))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> ko)) \<circ> (\<lambda>ps. ps(ptr' \<mapsto> f (the (ps ptr'))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s koa ksPSpacea gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState more. \<lbrakk>ptr \<noteq> ptr'; ksPSpace s ptr' = Some koa; is_aligned ptr' (objBitsKO koa); ps_clear ptr' (objBitsKO koa) s; s = \<lparr>ksPSpace = ksPSpacea, 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 = ksMachineState, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> f (the (ps ptr')))) \<circ> (\<lambda>ps. ps(ptr \<mapsto> ko))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> ko)) \<circ> (\<lambda>ps. ps(ptr' \<mapsto> f (the (ps ptr'))))) s proof (prove)
goal (1 subgoal):
 1. \<And>koa ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState more. \<lbrakk>ptr \<noteq> ptr'; ksPSpace ptr' = Some koa; is_aligned ptr' (objBitsKO koa); ps_clear ptr' (objBitsKO koa) \<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 = ksMachineState, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> ksPSpace(ptr \<mapsto> ko, ptr' \<mapsto> f koa) = ksPSpace(ptr' \<mapsto> f koa, ptr \<mapsto> ko) proof (prove)
goal (1 subgoal):
 1. \<And>koa ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState more x. \<lbrakk>ptr \<noteq> ptr'; ksPSpace ptr' = Some koa; is_aligned ptr' (objBitsKO koa); ps_clear ptr' (objBitsKO koa) \<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 = ksMachineState, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> (ksPSpace(ptr \<mapsto> ko, ptr' \<mapsto> f koa)) x = (ksPSpace(ptr' \<mapsto> f koa, ptr \<mapsto> ko)) x proof (prove)
goal:
No subgoals!