theory Detype_R

lemma placeNewObject_pspace_distinct':
  "\<lbrace>\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and>
        is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
        pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and>
        pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
   placeNewObject ptr val us
   \<lbrace>\<lambda>a. pspace_distinct'\<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>\<lambda>s. objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. pspace_distinct'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (placeNewObject ptr val us s); objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_distinct' b proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_distinct' (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>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_distinct' (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>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val)) (2 ^ us) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + us)
 2. \<And>s. \<lbrakk>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) + us < word_bits
 3. \<And>s. \<lbrakk>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) \<le> objBitsKO (injectKOS val) + us
 4. \<And>s. \<lbrakk>objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_distinct' s\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS val) + us - objBitsKO (injectKOS val)) * Suc 0 proof (prove)
goal:
No subgoals!