theory Retype_AI

lemma retype_addrs_subset_ptr_bits:
  assumes cover: "range_cover ptr sz (obj_bits_api ty us) n"
  shows "set (retype_addrs ptr ty n us) \<subseteq> {ptr .. (ptr &&~~ mask sz) + (2 ^ sz - 1)}" apply (clarsimp simp:retype_addrs_def ptr_add_def) apply (intro conjI) apply (rule word_plus_mono_right_split) apply (erule range_cover.range_cover_compare[OF cover]) using cover apply (simp add:range_cover_def) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (subst add.assoc) apply (rule word_plus_mono_right) apply (insert cover) apply (drule(1) range_cover.range_cover_compare) apply (rule iffD1[OF le_m1_iff_lt,THEN iffD2]) using cover apply (simp add: p2_gt_0 range_cover_def word_bits_def) apply (rule iffD2[OF word_less_nat_alt]) apply (rule le_less_trans[OF unat_plus_gt]) using cover apply (clarsimp simp: range_cover_def) apply (insert cover) apply (rule is_aligned_no_wrap'[where sz=sz]) apply (simp add: range_cover_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (retype_addrs ptr ty n us) \<subseteq> up_aligned_area ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa < n \<Longrightarrow> ptr \<le> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<and> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa < n \<Longrightarrow> ptr \<le> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us
 2. \<And>xa. xa < n \<Longrightarrow> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<And>xa. xa < n \<Longrightarrow> unat (ptr && mask (?sz10 xa)) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ ?sz10 xa
 2. \<And>xa. xa < n \<Longrightarrow> ?sz10 xa < LENGTH(32)
 3. \<And>xa. xa < n \<Longrightarrow> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa < n \<Longrightarrow> sz < LENGTH(32)
 2. \<And>xa. xa < n \<Longrightarrow> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (2 subgoals):
 1. \<And>xa. xa < n \<Longrightarrow> sz < LENGTH(32)
 2. \<And>xa. xa < n \<Longrightarrow> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa < n \<Longrightarrow> ptr + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa < n \<Longrightarrow> (ptr && mask sz) + (ptr && ~~ mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa < n \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa < n \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa < n \<Longrightarrow> (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> 2 ^ sz - 1
 2. \<And>xa. xa < n \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> 2 ^ sz - 1
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us \<le> 2 ^ sz - 1
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> 0 < 2 ^ sz
 2. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us < 2 ^ sz
 3. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (3 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> 0 < 2 ^ sz
 2. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us < 2 ^ sz
 3. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us < 2 ^ sz
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat xa * 2 ^ obj_bits_api ty us) < unat (2 ^ sz)
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < unat (2 ^ sz)
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat xa * 2 ^ obj_bits_api ty us) < unat (2 ^ sz)
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz
 2. \<And>xa. \<lbrakk>xa < n; range_cover ptr sz (obj_bits_api ty us) n; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> 2 ^ sz - 1 < 2 ^ sz proof (prove)
goal:
No subgoals!