theory Detype_R

lemma placeNewObject_pspace_aligned':
  "\<lbrace>K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
        objBitsKO (injectKOS val) + us < word_bits) and
    pspace_aligned' and pspace_distinct' and
    pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\<rbrace>
   placeNewObject ptr val us
   \<lbrace>\<lambda>r s. pspace_aligned' s\<rbrace>" apply (clarsimp simp:valid_def) apply (simp add:simpler_placeNewObject_def simpler_modify_def) apply (subst data_map_insert_def[symmetric])+ apply (erule(2) Retype_R.retype_aligned_distinct' [unfolded data_map_insert_def[symmetric]]) apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>r. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (placeNewObject ptr val us s); is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> pspace_aligned' b proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val)) (2 ^ us) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + us)
 2. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) + us < word_bits
 3. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) \<le> objBitsKO (injectKOS val) + us
 4. \<And>s. \<lbrakk>is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits; pspace_distinct' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS val) + us - objBitsKO (injectKOS val)) * Suc 0 proof (prove)
goal:
No subgoals!