theory CSpace1_R

lemma updateCap_stuff:
  assumes "(x, s'') \<in> fst (updateCap p cap s')"
  shows "(ctes_of s'' = modify_map (ctes_of s') p (cteCap_update (K cap))) \<and>
         gsUserPages s'' = gsUserPages s' \<and>
         gsCNodes s'' = gsCNodes s' \<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>
         (ksArchState s'' = ksArchState s') \<and>
         (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and>
         (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'')" using assms apply (clarsimp simp: updateCap_def in_monad) apply (drule use_valid [where P="\<lambda>s. s2 = s" for s2, OF _ getCTE_sp refl]) apply (rule conjI) apply (erule use_valid [OF _ setCTE_ctes_of_wp]) apply (clarsimp simp: cte_wp_at_ctes_of modify_map_apply) apply (frule setCTE_pspace_only) apply (clarsimp simp: setCTE_def) apply (intro conjI impI) apply (erule(1) use_valid [OF _ setObject_aligned]) apply (erule(1) use_valid [OF _ setObject_distinct]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s'' = modify_map (ctes_of s') p (cteCap_update (K cap)) \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
using this:
(x, s'') \<in> fst (updateCap p cap s')

goal (1 subgoal):
 1. ctes_of s'' = modify_map (ctes_of s') p (cteCap_update (K cap)) \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (1 subgoal):
 1. \<And>s''a cte. \<lbrakk>(cte, s''a) \<in> fst (getCTE p s'); ((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a)\<rbrakk> \<Longrightarrow> ctes_of s'' = modify_map (ctes_of s') p (cteCap_update (\<lambda>y. cap)) \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (1 subgoal):
 1. \<And>s''a cte. \<lbrakk>((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a\<rbrakk> \<Longrightarrow> ctes_of s'' = modify_map (ctes_of s') p (cteCap_update (\<lambda>y. cap)) \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (2 subgoals):
 1. \<And>s''a cte. \<lbrakk>((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a\<rbrakk> \<Longrightarrow> ctes_of s'' = modify_map (ctes_of s') p (cteCap_update (\<lambda>y. cap))
 2. \<And>s''a cte. \<lbrakk>((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a\<rbrakk> \<Longrightarrow> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (2 subgoals):
 1. \<And>s'' cte. (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s'' \<Longrightarrow> (ctes_of s'')(p \<mapsto> cteCap_update (\<lambda>_. cap) cte) = modify_map (ctes_of s') p (cteCap_update (\<lambda>y. cap))
 2. \<And>s''a cte. \<lbrakk>((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a\<rbrakk> \<Longrightarrow> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (1 subgoal):
 1. \<And>s''a cte. \<lbrakk>((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a\<rbrakk> \<Longrightarrow> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (1 subgoal):
 1. \<And>s''a cte. \<lbrakk>((), s'') \<in> fst (setCTE p (cteCap_update (\<lambda>_. cap) cte) s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a; \<exists>ps'. s'' = s''a\<lparr>ksPSpace := ps'\<rparr>\<rbrakk> \<Longrightarrow> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<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> ksArchState s'' = ksArchState s' \<and> (pspace_aligned' s' \<longrightarrow> pspace_aligned' s'') \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' s'') proof (prove)
goal (1 subgoal):
 1. \<And>cte ps'. \<lbrakk>((), s'\<lparr>ksPSpace := ps'\<rparr>) \<in> fst (setObject p (cteCap_update (\<lambda>_. cap) cte) s'); cte_wp_at' (\<lambda>c. c = cte) p s'; s'' = s'\<lparr>ksPSpace := ps'\<rparr>\<rbrakk> \<Longrightarrow> (pspace_aligned' s' \<longrightarrow> pspace_aligned' (s'\<lparr>ksPSpace := ps'\<rparr>)) \<and> (pspace_distinct' s' \<longrightarrow> pspace_distinct' (s'\<lparr>ksPSpace := ps'\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>cte ps'. \<lbrakk>((), s'\<lparr>ksPSpace := ps'\<rparr>) \<in> fst (setObject p (cteCap_update (\<lambda>_. cap) cte) s'); cte_wp_at' (\<lambda>c. c = cte) p s'; s'' = s'\<lparr>ksPSpace := ps'\<rparr>; pspace_aligned' s'\<rbrakk> \<Longrightarrow> pspace_aligned' (s'\<lparr>ksPSpace := ps'\<rparr>)
 2. \<And>cte ps'. \<lbrakk>((), s'\<lparr>ksPSpace := ps'\<rparr>) \<in> fst (setObject p (cteCap_update (\<lambda>_. cap) cte) s'); cte_wp_at' (\<lambda>c. c = cte) p s'; s'' = s'\<lparr>ksPSpace := ps'\<rparr>; pspace_distinct' s'\<rbrakk> \<Longrightarrow> pspace_distinct' (s'\<lparr>ksPSpace := ps'\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>cte ps'. \<lbrakk>((), s'\<lparr>ksPSpace := ps'\<rparr>) \<in> fst (setObject p (cteCap_update (\<lambda>_. cap) cte) s'); cte_wp_at' (\<lambda>c. c = cte) p s'; s'' = s'\<lparr>ksPSpace := ps'\<rparr>; pspace_distinct' s'\<rbrakk> \<Longrightarrow> pspace_distinct' (s'\<lparr>ksPSpace := ps'\<rparr>) proof (prove)
goal:
No subgoals!