theory Untyped_DR

lemma retype_transform_obj_ref_not_empty:
  "\<lbrakk>range_cover ptr sz (obj_bits_api tp us) n;
  is_aligned ptr (obj_bits_api tp us);
  y \<in> set (retype_addrs ptr tp n us)\<rbrakk>
   \<Longrightarrow> (retype_transform_obj_ref tp us y) \<noteq> {}" apply (frule(1) retype_addrs_aligned) apply (drule range_cover.sz,simp add:word_bits_def) apply (erule range_cover.sz) apply (clarsimp simp:retype_addrs_def retype_transform_obj_ref_def ptr_add_def) apply (rule is_aligned_no_overflow) apply (simp add:obj_bits_api_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> retype_transform_obj_ref tp us y \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> ?sz < word_bits
 2. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> obj_bits_api tp us \<le> ?sz
 3. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us); is_aligned y (obj_bits_api tp us)\<rbrakk> \<Longrightarrow> retype_transform_obj_ref tp us y \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us)\<rbrakk> \<Longrightarrow> obj_bits_api tp us \<le> sz
 2. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us); is_aligned y (obj_bits_api tp us)\<rbrakk> \<Longrightarrow> retype_transform_obj_ref tp us y \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; is_aligned ptr (obj_bits_api tp us); y \<in> set (retype_addrs ptr tp n us); is_aligned y (obj_bits_api tp us)\<rbrakk> \<Longrightarrow> retype_transform_obj_ref tp us y \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); is_aligned (ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us) (obj_bits_api apiobject_type.Untyped us); x < n; y = ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us; tp = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us + 2 ^ us - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); is_aligned (ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us) (obj_bits_api apiobject_type.Untyped us); x < n; y = ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us; tp = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type.Untyped us) us proof (prove)
goal:
No subgoals!