theory Detype_R

lemma placeNewObject_gets_globalPD_commute:
  "monad_commute
     (pspace_distinct' and pspace_aligned' and
      K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and
      pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) )
     (placeNewObject ptr val us) (gets (armKSGlobalPD \<circ> ksArchState))" apply (rule commute_name_pre_state) apply (rule monad_commute_guard_imp) apply (rule_tac commute_rewrite[where Q = "\<lambda>s.
    pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s
    \<and> pspace_distinct' s \<and> pspace_aligned' s" and R = "\<top>"]) apply (rule simpler_placeNewObject_def) apply simp+ apply wp apply (simp add:monad_commute_def gets_def get_def
     return_def bind_def simpler_modify_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) (placeNewObject ptr val us) (gets (armKSGlobalPD \<circ> ksArchState)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> monad_commute ((=) s) (placeNewObject ptr val us) (gets (armKSGlobalPD \<circ> ksArchState)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> monad_commute (?P2 s) (placeNewObject ptr val us) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ?P2 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> placeNewObject ptr val us sa = ?t5 s sa
 2. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> \<lbrace>?P5 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>x s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s\<rbrace>
 3. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> monad_commute (\<lambda>_. True) (?t5 s) (gets (armKSGlobalPD \<circ> ksArchState))
 4. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; s = sa\<rbrakk> \<Longrightarrow> (?P5 s and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>_. True)) sa proof (prove)
goal (7 subgoals):
 1. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> us < word_bits
 2. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + us)
 3. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) sa
 4. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) sa \<and> pspace_distinct' sa \<and> pspace_aligned' sa\<rbrakk> \<Longrightarrow> pspace_aligned' sa
 5. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> \<lbrace>?P5 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>x s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s\<rbrace>
 6. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace sa))) sa) (gets (armKSGlobalPD \<circ> ksArchState))
 7. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; s = sa\<rbrakk> \<Longrightarrow> (?P5 s and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s. pspace_distinct' s \<and> pspace_aligned' s \<and> us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<Longrightarrow> \<lbrace>?P5 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>x s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s\<rbrace>
 2. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace sa))) sa) (gets (armKSGlobalPD \<circ> ksArchState))
 3. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; s = sa\<rbrakk> \<Longrightarrow> (?P5 s and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>_. True)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>sa. modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace sa))) sa) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>_. True)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(pspace_distinct' and pspace_aligned' and K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_distinct' s \<and> pspace_aligned' s) and (\<lambda>_. True)) sa proof (prove)
goal:
No subgoals!