theory Retype_AI

lemma  (in Retype_AI_retype_region_ret)  retype_region_aligned_for_init[wp]:
  "\<lbrace>\<lambda>s::'state_ext state. range_cover ptr sz (obj_bits_api new_type obj_sz) n\<rbrace>
     retype_region ptr n obj_sz new_type dev
   \<lbrace>\<lambda>rv s. \<forall>ref \<in> set rv. is_aligned ref (obj_bits_api new_type obj_sz)\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_chain, rule retype_region_ret) apply simp apply (clarsimp simp: ptr_add_def
                 dest!: less_two_pow_divD) apply (rule aligned_add_aligned) apply (fastforce simp:range_cover_def) apply (subst mult.commute, subst shiftl_t2n[symmetric],
           rule is_aligned_shiftl) apply simp apply (simp add:range_cover_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n\<rbrace> retype_region ptr n obj_sz new_type dev \<lbrace>\<lambda>rv s. \<forall>ref\<in>set rv. is_aligned ref (obj_bits_api new_type obj_sz)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n \<Longrightarrow> \<lbrace>\<lambda>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n\<rbrace> retype_region ptr n obj_sz new_type dev \<lbrace>\<lambda>rv s. \<forall>ref\<in>set rv. is_aligned ref (obj_bits_api new_type obj_sz)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; range_cover ptr sz (obj_bits_api new_type obj_sz) n\<rbrakk> \<Longrightarrow> True
 2. \<And>s rv sa. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api new_type obj_sz)) [0..<n]\<rbrakk> \<Longrightarrow> \<forall>ref\<in>set rv. is_aligned ref (obj_bits_api new_type obj_sz) proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api new_type obj_sz)) [0..<n]\<rbrakk> \<Longrightarrow> \<forall>ref\<in>set rv. is_aligned ref (obj_bits_api new_type obj_sz) proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat ref * 2 ^ obj_bits_api new_type obj_sz) (obj_bits_api new_type obj_sz) proof (prove)
goal (3 subgoals):
 1. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> is_aligned ptr (?n15 ref)
 2. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat ref * 2 ^ obj_bits_api new_type obj_sz) (obj_bits_api new_type obj_sz)
 3. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> obj_bits_api new_type obj_sz \<le> ?n15 ref proof (prove)
goal (2 subgoals):
 1. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat ref * 2 ^ obj_bits_api new_type obj_sz) (obj_bits_api new_type obj_sz)
 2. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> obj_bits_api new_type obj_sz \<le> obj_bits_api new_type obj_sz proof (prove)
goal (2 subgoals):
 1. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat ref) (obj_bits_api new_type obj_sz - obj_bits_api new_type obj_sz)
 2. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> obj_bits_api new_type obj_sz \<le> obj_bits_api new_type obj_sz proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrakk>range_cover ptr sz (obj_bits_api new_type obj_sz) n; ref < n\<rbrakk> \<Longrightarrow> obj_bits_api new_type obj_sz \<le> obj_bits_api new_type obj_sz proof (prove)
goal:
No subgoals!