theory Untyped_AI

lemma retype_region_refs_distinct[wp]:
  "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> retype_region ptr n us tp dev
   \<lbrace>\<lambda>rv s. distinct_prop
             (\<lambda>x y. obj_refs (default_cap tp (snd x) us dev)
                  \<inter> obj_refs (default_cap tp (snd y) us dev) = {})
             (zip xs rv)\<rbrace>" apply simp apply (rule hoare_gen_asm[where P'="\<top>", simplified]) apply (rule hoare_strengthen_post [OF retype_region_ret]) apply (subst distinct_prop_map[symmetric, where f=snd]) apply (rule distinct_prop_prefixE [OF _ map_snd_zip_prefix [unfolded less_eq_list_def]]) apply (clarsimp simp: retype_addrs_def distinct_prop_map
                        word_unat_power[symmetric] power_sub[symmetric]
                        power_add[symmetric] mult.commute
          | rule conjI distinct_prop_distinct [where xs="upt a b" for a b]
                 set_eqI diff_le_mono
          | erule(3) ptr_add_distinct_helper ptr_add_distinct_helper [OF _ not_sym]
          | drule subsetD [OF obj_refs_default_cap]
                  less_two_pow_divD)+ apply (simp add: range_cover_def word_bits_def) apply (erule range_cover.range_cover_n_le[where 'a=machine_word_len]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. distinct_prop (\<lambda>x y. obj_refs (default_cap tp (snd x) us dev) \<inter> obj_refs (default_cap tp (snd y) us dev) = {}) (zip xs rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. range_cover ptr sz (obj_bits_api tp us) n\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. distinct_prop (\<lambda>x y. obj_refs (default_cap tp (snd x) us dev) \<inter> obj_refs (default_cap tp (snd y) us dev) = {}) (zip xs rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api tp us) n \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. distinct_prop (\<lambda>x y. obj_refs (default_cap tp (snd x) us dev) \<inter> obj_refs (default_cap tp (snd y) us dev) = {}) (zip xs rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. obj_refs (default_cap tp (snd x) us dev) \<inter> obj_refs (default_cap tp (snd y) us dev) = {}) (zip xs rv) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>a b. obj_refs (default_cap tp a us dev) \<inter> obj_refs (default_cap tp b us dev) = {}) (map snd (zip xs rv)) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>a b. obj_refs (default_cap tp a us dev) \<inter> obj_refs (default_cap tp b us dev) = {}) rv proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x < n; y < n; x \<noteq> y\<rbrakk> \<Longrightarrow> obj_bits_api tp us < 32
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x < n; y < n; x \<noteq> y\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - obj_bits_api tp us) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x < n; y < n; x \<noteq> y\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - obj_bits_api tp us) proof (prove)
goal:
No subgoals!