theory CSpace1_R

lemma updateMDB_eqs:
  assumes "(x, s'') \<in> fst (updateMDB p f s')"
  shows "ksMachineState s'' = ksMachineState s' \<and>
         ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and>
         ksCurThread s'' = ksCurThread s' \<and>
         ksIdleThread s'' = ksIdleThread s' \<and>
         ksReadyQueues s'' = ksReadyQueues s' \<and>
         ksInterruptState s'' = ksInterruptState s' \<and>
         ksArchState s'' = ksArchState s' \<and>
         ksSchedulerAction s'' = ksSchedulerAction s' \<and>
         gsUserPages s'' = gsUserPages s' \<and>
         gsCNodes s'' = gsCNodes s' \<and>
         ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and>
         ksDomSchedule s''    = ksDomSchedule s' \<and>
         ksCurDomain s''      = ksCurDomain s' \<and>
         ksDomainTime s''     = ksDomainTime s'" using assms apply (clarsimp simp: updateMDB_def Let_def in_monad split: if_split_asm) apply (drule in_inv_by_hoareD [OF getCTE_inv]) apply (clarsimp simp: setCTE_def setObject_def in_monad split_def) apply (drule in_inv_by_hoareD [OF updateObject_cte_inv]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksMachineState s'' = ksMachineState s' \<and> ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and> ksCurThread s'' = ksCurThread s' \<and> ksIdleThread s'' = ksIdleThread s' \<and> ksReadyQueues s'' = ksReadyQueues s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> ksSchedulerAction s'' = ksSchedulerAction s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and> ksDomSchedule s'' = ksDomSchedule s' \<and> ksCurDomain s'' = ksCurDomain s' \<and> ksDomainTime s'' = ksDomainTime s' proof (prove)
using this:
(x, s'') \<in> fst (updateMDB p f s')

goal (1 subgoal):
 1. ksMachineState s'' = ksMachineState s' \<and> ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and> ksCurThread s'' = ksCurThread s' \<and> ksIdleThread s'' = ksIdleThread s' \<and> ksReadyQueues s'' = ksReadyQueues s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> ksSchedulerAction s'' = ksSchedulerAction s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and> ksDomSchedule s'' = ksDomSchedule s' \<and> ksCurDomain s'' = ksCurDomain s' \<and> ksDomainTime s'' = ksDomainTime s' proof (prove)
goal (1 subgoal):
 1. \<And>s''a cte. \<lbrakk>p \<noteq> 0; (cte, s''a) \<in> fst (getCTE p s'); ((), s'') \<in> fst (setCTE p (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) s''a)\<rbrakk> \<Longrightarrow> ksMachineState s'' = ksMachineState s' \<and> ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and> ksCurThread s'' = ksCurThread s' \<and> ksIdleThread s'' = ksIdleThread s' \<and> ksReadyQueues s'' = ksReadyQueues s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> ksSchedulerAction s'' = ksSchedulerAction s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and> ksDomSchedule s'' = ksDomSchedule s' \<and> ksCurDomain s'' = ksCurDomain s' \<and> ksDomainTime s'' = ksDomainTime s' proof (prove)
goal (1 subgoal):
 1. \<And>s''a cte. \<lbrakk>p \<noteq> 0; ((), s'') \<in> fst (setCTE p (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) s''a); s''a = s'\<rbrakk> \<Longrightarrow> ksMachineState s'' = ksMachineState s' \<and> ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and> ksCurThread s'' = ksCurThread s' \<and> ksIdleThread s'' = ksIdleThread s' \<and> ksReadyQueues s'' = ksReadyQueues s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> ksSchedulerAction s'' = ksSchedulerAction s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and> ksDomSchedule s'' = ksDomSchedule s' \<and> ksCurDomain s'' = ksCurDomain s' \<and> ksDomainTime s'' = ksDomainTime s' proof (prove)
goal (1 subgoal):
 1. \<And>cte a b s''a obj'. \<lbrakk>p \<noteq> 0; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); (obj', s''a) \<in> fst (updateObject (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) b p a (snd (lookupAround2 p (ksPSpace s'))) s'); s'' = s''a\<lparr>ksPSpace := (ksPSpace s')(a \<mapsto> obj')\<rparr>\<rbrakk> \<Longrightarrow> ksMachineState s''a = ksMachineState s' \<and> ksWorkUnitsCompleted s''a = ksWorkUnitsCompleted s' \<and> ksCurThread s''a = ksCurThread s' \<and> ksIdleThread s''a = ksIdleThread s' \<and> ksReadyQueues s''a = ksReadyQueues s' \<and> ksInterruptState s''a = ksInterruptState s' \<and> ksArchState s''a = ksArchState s' \<and> ksSchedulerAction s''a = ksSchedulerAction s' \<and> gsUserPages s''a = gsUserPages s' \<and> gsCNodes s''a = gsCNodes s' \<and> ksDomScheduleIdx s''a = ksDomScheduleIdx s' \<and> ksDomSchedule s''a = ksDomSchedule s' \<and> ksCurDomain s''a = ksCurDomain s' \<and> ksDomainTime s''a = ksDomainTime s' proof (prove)
goal (1 subgoal):
 1. \<And>cte a b s''a obj'. \<lbrakk>p \<noteq> 0; fst (lookupAround2 p (ksPSpace s')) = Some (a, b); s'' = s''a\<lparr>ksPSpace := (ksPSpace s')(a \<mapsto> obj')\<rparr>; s''a = s'\<rbrakk> \<Longrightarrow> ksMachineState s''a = ksMachineState s' \<and> ksWorkUnitsCompleted s''a = ksWorkUnitsCompleted s' \<and> ksCurThread s''a = ksCurThread s' \<and> ksIdleThread s''a = ksIdleThread s' \<and> ksReadyQueues s''a = ksReadyQueues s' \<and> ksInterruptState s''a = ksInterruptState s' \<and> ksArchState s''a = ksArchState s' \<and> ksSchedulerAction s''a = ksSchedulerAction s' \<and> gsUserPages s''a = gsUserPages s' \<and> gsCNodes s''a = gsCNodes s' \<and> ksDomScheduleIdx s''a = ksDomScheduleIdx s' \<and> ksDomSchedule s''a = ksDomSchedule s' \<and> ksCurDomain s''a = ksCurDomain s' \<and> ksDomainTime s''a = ksDomainTime s' proof (prove)
goal:
No subgoals!