theory CSpace1_R

lemma updateMDB_the_lot:
  assumes "(x, s'') \<in> fst (updateMDB p f s')"
  assumes "pspace_relations (ekheap s) (kheap s) (ksPSpace s')"
  assumes "pspace_aligned' s'" "pspace_distinct' s'" "no_0 (ctes_of s')"
  shows "ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and>
         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>
         ksSchedulerAction s'' = ksSchedulerAction s' \<and>
         ksInterruptState s'' = ksInterruptState s' \<and>
         ksArchState s'' = ksArchState s' \<and>
         gsUserPages s'' = gsUserPages s' \<and>
         gsCNodes s'' = gsCNodes s' \<and>
         pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \<and>
         pspace_aligned' s'' \<and> pspace_distinct' s'' \<and>
         no_0 (ctes_of s'') \<and>
         ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and>
         ksDomSchedule s''    = ksDomSchedule s' \<and>
         ksCurDomain s''      = ksCurDomain s' \<and>
         ksDomainTime s''     = ksDomainTime s'" using assms apply (simp add: updateMDB_eqs updateMDB_pspace_relations split del: if_split) apply (frule (1) updateMDB_ctes_of) apply clarsimp apply (rule conjI) apply (erule use_valid) apply wp apply simp apply (erule use_valid) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and> 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> ksSchedulerAction s'' = ksSchedulerAction s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \<and> pspace_aligned' s'' \<and> pspace_distinct' s'' \<and> no_0 (ctes_of 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')
pspace_relations (ekheap s) (kheap s) (ksPSpace s')
pspace_aligned' s'
pspace_distinct' s'
no_0 (ctes_of s')

goal (1 subgoal):
 1. ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and> 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> ksSchedulerAction s'' = ksSchedulerAction s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \<and> pspace_aligned' s'' \<and> pspace_distinct' s'' \<and> no_0 (ctes_of 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. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s')\<rbrakk> \<Longrightarrow> ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and> pspace_aligned' s'' \<and> pspace_distinct' s'' \<and> no_0 (ctes_of s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and> pspace_aligned' s'' \<and> pspace_distinct' s'' \<and> no_0 (ctes_of s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_aligned' s'' \<and> pspace_distinct' s'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_aligned' s''
 2. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_distinct' s'' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> \<lbrace>?P47\<rbrace> updateMDB p f \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
 2. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> ?P47 s'
 3. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_distinct' s'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_distinct' s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s'') \<in> fst (updateMDB p f s'); pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_distinct' s'' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> \<lbrace>?P53\<rbrace> updateMDB p f \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
 2. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> ?P53 s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relations (ekheap s) (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; no_0 (ctes_of s'); ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f)\<rbrakk> \<Longrightarrow> pspace_distinct' s' proof (prove)
goal:
No subgoals!